ThepresentworkwassubmittedtotheLuFGTheoryofHybridSystems MASTER OF SCIENCE THESIS B SMT-RAT ITVECTORS IN T A T AND HEIR PPLICATION O I A NTEGER RITHMETICS Andreas Krüger Examiners: Prof. Dr. Erika Ábrahám Prof. Dr. Jürgen Giesl Additional Advisor: M.Sc. Gereon Kremer Aachen, 08.10.2015 Abstract Oneofthemostprominentapproachesinthefieldofsoftwareverificationisbasedonthe problemofSatisfiabilityModuloTheories(SMT).DecidinganSMTinstancemeansdeciding whether a given first-order formula is satisfiable in the context of a fixed background theory. A theory that is specifically designed for software and hardware verification purposes is the theory of fixed-size bitvector logic (BV). It provides an expressive language to reason about many operations that are implemented in state-of-the-art CPUs. This thesis presents a novel module for the SMT toolbox SMT-RAT that can decide the satisfiability of quantifier-free formulas in bitvector logic. It makes use of a reduction to the well-known propositional satisfiability problem (SAT). This approach, which is often referredtoasflatteningorbit-blasting,highlybenefitsfromthesuccessesinthedevelopment of efficient SAT solvers throughout the last decades. Whileflatteningisthepredominantmethodfordecidingproblemsinbitvectorlogic, itis also possible to transfer this idea to different SMT theories, which are less strongly related to SAT. As the second part of this thesis, an application of bit-blasting to the theory of nonlinear integer arithmetics (NIA) is presented, where the properties of integrality and nonlinearity are typically a burden on classical arithmetic decision procedures. Especially on small domains, an encoding to SAT can be a superior alternative. InsteadofdirectlyencodingtoSAT,atechniqueisdemonstratedthatreducesNIAprob- lems on a small domain to bitvector arithmetic. We further explain how to apply Interval Constraint Propagation (ICP) for reducing the complexity of the created bitvector formulas and thereby improve the performance of the solver. AnevaluationshowsthatthenewlycreatedbitvectormoduleinSMT-RATalreadygives decent performance results. On the NIA theory, the proposed reduction to bitvector arith- metic proves to be highly competitive with common arithmetic decision procedures. iv v Erklärung Hiermit versichere ich, dass ich die vorgelegte Arbeit selbstständig verfasst und noch nicht anderweitig zu Prüfungszwecken vorgelegt habe. Alle benutzten Quellen und Hilfsmittel sind angegeben, wörtliche und sinngemäße Zitate wurden als solche gekennzeichnet. Andreas Krüger Aachen, den 08. Oktober 2015 Danksagung Ich danke den folgenden Personen für ihre Unterstützung während der Erstellung dieser Arbeit: • Prof. Dr. Erika Ábrahám für die Möglichkeit, meine Masterarbeit in dem spannenden Gebiet des SMT-Solvings zu verfassen, sowie für die hilfreichen Impulse und wertvollen Ratschläge. • Prof. Dr. Jürgen Giesl für die Bereitschaft, meine Arbeit als Zweitgutachter zu begleiten. • Meinem Betreuer Gereon Kremer für die kontinuierliche Unterstützung, zahlreiche frucht- bare Anregungen und den produktiven Austausch. • Florian Corzilius für viel Hilfsbereitschaft und eine fortwährend sehr angenehme Zusam- menarbeit. • Meiner Familie, insbesondere meiner Frau Julia, meinen Eltern und meiner Schwiegermut- ter, für den starken Rückhalt in dieser Zeit und während meines gesamten Studiums. vi Contents 1 Introduction 9 2 Background 13 2.1 SAT and SMT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.1 SAT and the DPLL Algorithm . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.2 SMT and the DPLL(T) Algorithm . . . . . . . . . . . . . . . . . . . . . . 15 2.1.3 SMT-LIB . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2 SMT-RAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3 Bitvector Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3.1 The SMT Logic QF_BV . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3.2 Decision Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.4 Integer Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4.1 The SMT Logics QF_LIA and QF_NIA . . . . . . . . . . . . . . . . . . . 28 2.4.2 Decision Procedures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 Solving Bitvector Arithmetic 31 3.1 BVModule Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Encoding to SAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.2.1 Functional Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 3.2.2 Encoding Simple Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 3.2.3 Encoding Shifts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.2.4 Encoding Addition, Subtraction and Negation . . . . . . . . . . . . . . . . 38 3.2.5 Encoding Relational Operators . . . . . . . . . . . . . . . . . . . . . . . . 41 3.2.6 Encoding Multiplication, Division and Remainder . . . . . . . . . . . . . . 42 3.3 Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 4 Solving Integer Arithmetic 47 4.1 IntBlastModule Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.2 Constraint Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.3 Encoding to Bitvector Arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.3.1 Annotated Bitvector Terms . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.3.2 Integer Mapping Creation . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.3.3 Translation of Constraint Trees . . . . . . . . . . . . . . . . . . . . . . . . 59 4.4 Bounds from Interval Constraint Propagation . . . . . . . . . . . . . . . . . . . . 64 4.4.1 Introduction to ICP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 4.4.2 Bound Generation for Polynomial Tree Nodes . . . . . . . . . . . . . . . . 66 4.4.3 Applying Inferred Bounds for Width Reduction . . . . . . . . . . . . . . . 67 4.5 SMT-Compliance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 4.6 Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 viii Contents 5 Evaluation 73 5.1 SMT-COMP 2015 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 5.2 BVModule Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 5.3 IntBlastModule Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 6 Conclusion 77 6.1 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Bibliography 79 Chapter 1 Introduction Throughoutthelastdecades, theimpactoftechnologyonmankindhasincreasedtoanenormous level. We live in a world where we are used to permanently interact with technical systems, consciouslyorunconsciously,inalmosteveryaspectofoureverydaylives. Oneofthemaindrivers for this ongoing development is the performance and availability of computerized systems. The omnipresence of software has caused a trend to hand over more and more tasks to the control of machines,sincetheiractionsareperceivedasmorereliable,morepredictableandlesserror-prone than human behavior. The development of self-driving cars or autonomously acting missiles, for example, is a manifestation of the trust our society puts in technology. However, this progression also burdens software engineers with a much higher responsibility for their products, a challenge that is usually addressed by an exhaustive testing procedure as an integral part of the software development process. Nonetheless, a characteristic of testing is that it can only prove the presence of errors, not their absence. When it comes to heavily safety- critical applications, it is desirable to obtain stronger statements on the accurate functioning of software. This desire has given rise to the approach of verification, i.e. the application of formal methods to software with the aim to prove its correctness on the basis of a mathematical calculus. The typical procedure of verification consists of three steps: First, the software to be verified is transformed into a mathematical model. Afterwards, the properties that should be proven are formalized on the basis of this model. Typical properties are the unreachability of certain states that are attributed as bad or harmful, the absence of programming mistakes which can make the system behavior nondeterministic, the correctness of the program output under all possible inputs, orthefulfillmentoflivenesspropertiesexpressingthatthesystemalwaysrespondswithin a certain time frame. Due to the variety of applications and programming languages, the set of constraints varies within different domains and employed techniques. Since the choice of the mathematical model usedforverificationpurposesalsodeterminesthespectrumofstatementswhichcanbeconcluded on its basis, it is a natural consequence that there is not a unique modeling scheme that is suited for all practices. Instead, there is a multitude of logics and theories to choose from, under consideration of their respective strengths and weaknesses. A very important group of problems is the set of problems which ask for the satisfiability of some first-order logic formula ϕ in the context of a given theory T. Depending on the concrete application, different theories can be suitable as background theory T. Problems of arithmetic nature, for example, may be described using a theory of arithmetics over integer or real num- 10 Chapter 1. Introduction bers, while problems with a more logical than arithmetic character may be based on a theory of uninterpreted functions. The union of all problems following this scheme is referred to as the problem of Satisfiability Modulo Theory (SMT). It can be seen as a generalization of the fa- mous satisfiability problem (SAT), which addresses the question of satisfiability of propositional formulas. During the last years, SAT and SMT solving have gained a lot of attraction. SAT is typically well-known for its theoretical properties in the field of complexity theory: The SAT problem is NP-complete, which states that it is an NP-hard problem on which all other NP-hard problems can be reduced in polynomial time. It is one of the most important open questions of theoretical computer science whether NP-complete problems like SAT can be solved efficiently, i.e. by a polynomial algorithm on a deterministic Turing machine, but the commonly shared belief is that this is not the case. However, this is a theoretical property concerning the SAT problem in its general form, which does not imply that every SAT problem instance is hard to solve. In fact, a lot of progress has been achieved in building automated solvers that operate efficiently on many instances of SAT arising from practical problems. The advances in the field of SAT solving have also contributed a lot to the area of SMT solving. State-of-the-art SMT solvers are typically based on an internal SAT solver, equipped with additional solvers for the specific background theory T. As a result of this setup, any per- formance gains achieved in SAT solving also have a direct effect on the SMT solver performance. In addition, there are also important developments in the field of SMT on its own: In 2003, an internationalinitiativenamedSMT-LIB[BST10]hasbeenbuilt,whichaimsattheestablishment of common standards in the field of SMT. A general syntax for SMT problem specification has been developed, which is now widely supported by different SMT solvers. Moreover, a number of background theories has been precisely specified in terms of their syntax and semantics. These common standards allow for a direct comparison of SMT solvers, which is the goal of the SMT-COMP contest [CDW15]: Since 2005, SMT solvers have the chance to participate in thisannualcompetition,inwhichtheirperformanceisevaluatedonhugeamountsofbenchmarks invariouscategories. Theresultsofthelastyearsmakeitevidentthatmostsolversarestillunder active development and that a lot of research is performed in the extension and improvement of SMT solvers. Startingin2012,theresearchgroupTheoryofHybridSystemsattheRWTHAachen,leadby Prof. Dr. ErikaÁbrahám,initiatedthecreationofanownSMTsolvingenginenamedSMT-RAT (Satisfiability-Modulo-Theories Real Algebra Toolbox) [CKJ+15]. Built on C++, SMT-RAT is provided as free software, designed with the objectives extensibility, modularity and flexibility in mind. At its heart, it consists of several solver modules which can be composed to a user-defined strategy. Depending on the configuration, the generated program is either a full-blown SMT solver or only a theory solver which can be embedded into different SMT solving engines. Regarding the project name SMT-RAT and its development history, it is obvious that SMT- RAT started with a main focus on theories considering nonlinear real and integer arithmetics. However, it is the ambition of the project to extend its capabilities towards other theories. With the development of modules for linear arithmetics and for uninterpreted sort and function symbols, ashifttowardsamoreuniversalsolverhasbegun. Withthe contributionsofthisthesis, we want to further widen the scope of application of SMT-RAT by creating a designated module for the theory of quantifier-free fixed-size bitvectors (QF_BV in SMT-LIB). The theory of fixed-size bitvectors originates directly from the software and hardware ver- ification domain. A bitvector is a vector of Boolean values and serves as the model of CPU registers, variables or memory areas in general. With its rich set of predicate and function sym-