search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
847 stars 262 forks source link

[RFC] SMT Plan #6134

Open TGWDB opened 3 years ago

TGWDB commented 3 years ago

Executive Summary

This RFC outlines an implementation plan for adding a standard and easily switchable SMT backend to CBMC. The goal of this work is to address two main areas. The first is to improve performance of CBMC by being able to both: use (runtime) switchable SMT solvers, and be extendable to exploit different theories. The second is for CBMC to have a high quality (clean, clear, robust, extensible, and maintainable) interaction with SMT solvers. This document includes the main details and measures for delivery of the project; the project plan; and key milestones and deliverables to be performed in a mostly iterative manner over vertical slices.

Project Goals

The motivation for this project is to improve CBMC performance via SMT solvers. This has two main underlying aspects that both need to be addressed for this project to achieve long term success. The first is to allow CBMC to support (runtime) switchable SMT solvers and support multiple different theories. The second is to ensure that the SMT interaction with CBMC is high quality (clean, clear, robust, extensible and maintainable). These motivations drive the rest of the project detailed below.

The goal of this project is thus to allow CBMC to support multiple SMT solvers by using a common interface (SMT2LIB) and communication via a configurable interface (e.g. ports or pipes). The goals relating to the quality of the interaction should be taken into account and is somewhat reflected in the deliverables and overall project plan (incrementally developing a whole new SMT2 interaction rather than simply making small changes to the current SMT translation that is NOT clear, clean, robust, or maintainable).

The measures for delivery of the project are the following:

  1. CBMC will have an interface based on SMT2LIB that allows communication with any SMT2LIB compliant SMT solver.
  2. CBMC will be able to take the SMT solver as a configuration option and thus allow different SMT2LIB compliant solvers to be chosen at CBMC invocation time (not compile time).
  3. CBMC is able to exploit different theories in the SMT solver to improve results. (Note that the current SMT interaction already supports more SMT theories than simply SAT, but this goal is to ensure improvement and parity.)

Note that these are not able to capture the detail of the quality, but quality should be kept in mind as it is one of the motivations of this project.

Project Deliverables & Milestones

The plan for this project is to do vertical slices of the functionality with the goal that each step along the way can be used, even if this is an incomplete fragment. The rest of this section overviews both the iterative process for each vertical slice, as well as some details on what the slices are and how to progress through them. Note that while the main body of the project is an iteration with sub-deliverables, there are five others: two earlier ones (Foundation and Communication) and three later ones (Parsing SMT Output, Runtime Swapping Solvers and Final Steps). Only Foundation and Final Steps are strictly at the beginning or end, although Communication must occur before Runtime Swapping Solvers.

Below is a list of the SSA types and the SMT theories they will be translated into taken from knowledge of the current SMT translation in CBMC. These provide a useful starting point for a list of slices that can be implemented.

Note that additional slices may be considered, however the above provide at least the coverage of the existing SMT solver usage of CBMC.

The rest of this section details the plan and deliverables that can be used to iterate through the vertical slices, including an initial Foundation stage and two concluding stages.

Foundation

This is a one-off part of the project that needs to be completed as a foundation for the rest of the SMT development. This involves adding a new flag to turn on the new functionality and ensuring that when this flag is enabled CBMC will attempt to use the new SMT backend.

Note that the invocation of SMT solvers through the new code path implemented here will be using incremental solving. This should be set as the default for how the interaction with all new SMT solvers will be conducted.

At the completion of the Foundation deliverable CBMC will be able to be invoked with the new flag. CBMC will behave normally when invoked with the new flag until the solver is invoked (or some other unimplemented feature is encountered), at which point the default unimplemented behaviour will occur, which is to report the error and terminate.

Once the Foundation is complete the (see below) Iteration deliverable (and sub-deliverables) will be iterated upon for each of the vertical slices. The following deliverable on Communication can be done at any point after the Foundation deliverable.

Communication

The Communication deliverable will implement invoking the first chosen SMT solver (here Z3) and setting up connection between CBMC and SMT solver.

Part of the Communication deliverable is to also choose how the communication and invocation of the SMT solver will be done. To be completed this must also allow CBMC to receive responses from the SMT solver.

Note that this is distinct from the Foundation and the previous approach used by CBMC since one of the project goals is to have more uniformly swappable SMT solvers. The main purpose of the Communication deliverable is to ensure this is supported and designed with good quality.

This deliverable should first be implemented for Linux and macOS, with later iterations of this deliverable supporting the communication on Windows.

Iteration (per Slice)

Note that for each slice the scope/target is already defined (see discussion at the start of the Project Deliverables & Milestones section). The rest of this section overviews the parts of an iteration. Also in each sub-deliverable is some text (in italics) for an example of doing a slice for Integers.

Tests

This is the first step in each iteration and the deliverable for this is a collection of tests that demonstrate the capabilities and limitations (i.e. scope) of the slice. This includes all the structures and examples that should be covered.

Note that when creating the tests for a given slice this should also consider (or use) the existing regression tests that should be solvable when this slice is complete (including building on prior slices).

For example, the Integer tests would include all the basic Integer operations. This would ensure coverage of both the translation of the operations on Integers, and also be able to validate that the SMT solver is understanding them correctly (i.e. no bugs in translation of configuration). Note that this would also include ensuring the correct handling of Integers when considering control flow (so the first slice must include basic control flow, and all following slices must ensure their handling of control flow). Similarly, casting to and from all previous (potentially castable types) and Integers are included in the Integer slice.

Internal Structure

This step is to implement a CBMC internal structure for the primitive chosen that can be mapped to the appropriate SMT2 representation. This should be based upon the existing irep structure, and provide a well defined structure for the primitive of this slice. For example, an internal irep-based structure to represent integers

This deliverable is complete when all the structure/forms required for this slice can be represented by the internal irep-based structure.

For example, the internal structure for Integers must be able to represent all the base structures for Integers themselves, as well as all Integer unique structures. Further, all the existing structures may need to be extended to also account for the new Integer structures (e.g. if the plus or assign operator is already defined, it must now be extended to accept plus or assign of Integers).

Internal Structure Output (Pretty Printing)

This step is to convert the internal structure into a suitable format for the SMT2 solver (e.g. a string). This should ideally also be usable for output in debugging.

This is complete when all of the internal structure as defined in the previous step can be output in an SMT2LIB format suitable for the SMT solver.

For example, the output would not be able to output all the internal structures added in the previous sub-deliverable. This would also include understanding how to output in the correct format for the SMT2LIB representation of Integers.

SMT2LIB Translation

This step is to do the translation from CBMC’s SSA representation into the new structure that maps to the SMT2LIB format.

This deliverable is complete when all the identified/appropriate CBMC internal SSA expressions are able to be translated into the SMT2LIB internal irep-based structure.

Note that this does not require the previous sub-deliverable (Internal Structure Output) to be complete, however this may be hard to debug and evaluate without the Internal Structure Output.

For example, this should not be able to handle all the tests generated before or extended with Integers and be able to translate them into the internal structure (including with the new Integer internal structures). This will include both writing new Integer specific translation functions, but also extending prior functions that before may have reported errors when passed Integer values (e.g. assign may not have been defined for Integers prior to this slice). Similarly, the functions created/extended here must also be written to handle (by reporting an error) incorrect usage that should be fixed in future slices (e.g. assignment to an Integer from an Array -- assuming the array slice has not been done prior to the Integer slice).

Validation & Testing

The final deliverable is validation that all the above fit together and that the expected tests are passed. This is an explicit deliverable since it is expected there will be bugs that are found in final validation and testing that need to be repaired. This may also involve the creation of further tests that catch new/interesting cases.

For example, this would involve ensuring all the tests developed for this slice and all previous slices that passed before still pass. Bugs or errors detected along the way would need to be fixed. Further, testing against the general regression tests should be done to ensure Integers are generally handled there and to evaluate the status and stability of the slice after Integers are added.

This ends the iteration part. Note that this is designed so that the project can be paused at any point and can also progress to the following three steps, although the Final Step may be undesirable if SMT2 coverage is limited.

Parsing SMT Output

This deliverable is to enable parsing of the SMT solver output back into a useful internal form for cbmc. This involves replacing/rewriting the existing (hand crafted parser) with a parse-generator version (e.g. flex/bison).

This deliverable is complete when the output from SMT can be robustly handled to produce the traces necessary for cbmc traces. This should also include significant testing of the parser, i.e. unit tests and end-to-end tests.

Runtime Swapping Solvers

This deliverable is to extend the Communication step to be able to support multiple SMT solvers using a simple flag or option. Ideally the above will turn out to be suitable SMT2 solver agnostic that any SMT2LIB conformant solver can simply be added here with a simple change to how CBMC invokes (and/or maybe interacts with) to allow runtime invocation and swapping of SMT solvers.

This deliverable will be complete when CBMC can take a runtime argument to run with the chosen SMT2-compliant solver. Note that this deliverable also involves implementing, testing, and completing the communication on all support operating systems.

This may involve some small amount of work to provide preamble/configuration details that CBMC can invoke to ensure the runtime choice is as seamless as possible.

Note, this should include CI for validation that the multiple solvers are supported. This should include at least: Z3 and one other solver (to be decided, e.g. CVC4, Boolector, Mathsat5, Yices2).

Final Step

The final step is to remove/deprecate the old SMT solver(s) and use the new SMT interaction and translation developed here. This should only be considered when suitable coverage is achieved with the new SMT2 translation and communication.

Note that this should also involve all the CI and other details related to changing the default behaviour of CBMC to use the new solver.

Note: this should be sure to reinstate the cprover_init removal done in the Foundation if it has not been (re)enabled before.

(Bonus) Dynamic SMT Solver Configuration

This deliverable is to enable more dynamic and subtle control of the SMT solver(s) via some kind of configurations either inside CBMC or through a configuration option that CBMC can pass through. The goal is to be able to pass through knowledge or information to the (specific?) SMT solver that can improve the performance.

Progress Summary

This is a very brief summary of the progress so far with ~strikethrough~ indicating this is complete and merged:

TGWDB commented 3 years ago

Note that PR #6131 is a large part of the foundation deliverable mentioned above.

martin-cs commented 3 years ago

Thank you for posting this; it is helpful to understand the context of what you are trying to achieve.

I am really supportive of this idea. If I am picking up a lot of points it is because I really care about doing this right and helping you avoid some of the issues I have had in working on and with SMT solvers. I'm happy to discuss any of this at a meeting if it would help.

On Fri, 2021-05-21 at 00:34 -0700, TGWDB wrote:

Executive Summary

This RFC outlines an implementation plan for adding a standard and easily switchable SMT backend to CBMC. The goal of this work is to address two main areas. The first is to improve performance of CBMC by being able to both: use (runtime) switchable SMT solvers,

When you say performance... are you talking wall-clock time or CPU time? If it is wall-clock time then I would strongly recommend that you support portfolios of solver. Portfolio solvers work so well they are now banned from SMT-COMP. We are not yet (and I hope will never be) at a point where the gap between the best portfolio and the best solver is small. Given a bit of time, almost every system that uses SMT solvers develops portfolio support. It helps smooth the performance and makes a real difference to commercial uses. I am not sure of the current state of Par4 and whether it is maintained / extensible but that would be one route.

and be extendable to exploit different theories.

Which ones specifically? It matters because standardised theories are a much easier target than in-development ones.

The second is for CBMC to have a high quality (clean, clear, robust, extensible, and maintainable) interaction with SMT solvers.

That would be amazing.

I note that there is nothing here about incremental solving. For reasons that are a bit lengthy to go into here, I think that incrementality is really important. It is hard to retro-fit as it requires a change of architecture from the flat conversion we have, so it makes sense to think about when writing a new back-end.

Depending on what you want to do with the incrementality and specifically the number and speed of calls you want to make, there are different architectures. If it is lots of small / fast goals (like incremental coverage, for example) then API integration is the way to go. If it is few, larger goals then pipes will probably be OK.

The goal of this project is thus to allow CBMC to support multiple SMT solvers by using a common interface (SMT2LIB)

Would this be a bad time to point out that SMT-LIB 3.0 is due to be finalised this summer? Drafts are here:

http://smtlib.cs.uiowa.edu/version3.shtml

It will be mostly (but not entirely) backwards compatible. The way that logics are handled will probably be the biggest change.

> Below is a list of the SSA types and the SMT theories they will be > translated into taken from knowledge of the current SMT translation > in CBMC. These provide a useful starting point for a list of slices > that can be implemented. > > - Integer types: BitVec > - Floating point types: BitVec or FloatingPoint (with --fpa) Depending on which solvers you are targetting, I would suggest having FloatingPoint as default and only implementing the bit vector translations yourself if you want to support a solver that doesn't have them. Support for the theory of floating-point is now quite wide- spread and papers on native translations pre-solvers show a performance penalty that is likely to increase with time. > - Pointers: BitVec This would work but a little more thought here could give quite some performance improvement. The base objects can be an uninterpreted sort which will improve the equality reasoning and has the advantages of being able to have "or something else" objects which would give some very interesting options for modular handling of dynamic memory. Offsets make sense to have a bit-vectors but I don't know how much this will be needed post symex. > - Structs: flattened per field into BitVec or data types (with --z3) 1. Data types are now in SMT-LIB so they aren't just a --z3 option. 2. Flattening is problematic, see below... 3. Given the work @tautschnig has done on field-sensitive SSA, do you want / need to handle these? > - Unions: BitVec See point about flattening below... > - Arrays: Array > - String literals: Array of BitVec If one of your goals is to use additional theories, why not consider the theory of strings? It will perform way better than the array + instantiated quantifier approach. The controversial move would be to use it for arrays as well as strings. We need to talk about flattening. There are basically two approaches to an SMT back-end, you can either go low-level and aim for bit-level fidelity. If you go this route, then, yes flatten everything and you are basically doing an SMT version of the SAT back-end. It works but it prevents you using more advanced theories. This is what the current back-end does and why I have long thought a rewrite was needed. The other approach is to aim high-level and assume that the formula are type safe and that encoded type-unsafe things are rare oddities to work around. This means that you can actually do reasonable theory reasoning about strings, arrays, floating-point, etc. without having to forcibly flatten everything every other operation. @tautschnig has done a lot of the symex work to make this viable but it is going to have some really fiddly corners. I think it might be possible to create a back-end that can switch between them but be aware that flattening, when and how, are decisions with significant architectural consequence. > Note that additional slices may be considered, however the above > provide at least the coverage of the existing SMT solver usage of > CBMC. ( IIRC we do support mathematical ints and reals as well, although they are rarely used. ) You might also want to think about what you are going to do about quantifiers, esp. at the rate that the code contract folks are adding them. > Note that the invocation of SMT solvers through the new code path > implemented here will be using incremental solving. This should be > set as the default for how the interaction with all new SMT solvers > will be conducted. Agreed but see previous point about the tightness of integration and it's relation to incrementality. > ### Communication > > This deliverable should first be implemented for Linux and macOS, > with later iterations of this deliverable supporting the > communication on Windows. As discussed elsewhere, you really want to make sure there is a way of doing this on Windows before committing. > #### Tests > Note that when creating the tests for a given slice this should also > consider (or use) the existing regression tests that should be > solvable when this slice is complete (including building on prior > slices). Given that there is a functional SMT front-end that parses s- expressions to exprt and you are doing exprt to s-expressions, why not make use of the SMT-LIB benchmark library and solvers and you can automatically find when you back-end mistranslates things. It is not the whole story because "exprts that symex generates" and "exprts that the SMT front-end creates" are both different subsets of exprts but it will very quickly find issues with your translations. > _For example, the Integer tests would include all the basic Integer > operations. This would ensure coverage of both the translation of the > operations on Integers, and also be able to validate that the SMT > solver is understanding them correctly (i.e. no bugs in translation > of configuration). Note that this would also include ensuring the > correct handling of Integers when considering control flow (so the > first slice must include basic control flow, and all following slices > must ensure their handling of control flow). Similarly, casting to > and from all previous (potentially castable types) and Integers are > included in the Integer slice._ With respect; why do you care about control-flow? By the time anything gets to the back-end, all control flow is long gone and it is just formulae. > #### Internal Structure > > This step is to implement a CBMC internal structure for the primitive > chosen that can be mapped to the appropriate SMT2 representation. > This should be based upon the existing irep structure, and provide a > well defined structure for the primitive of this slice. For example, > an internal irep-based structure to represent integers How will this be any different to exprt? The semantics of exprt and SMT-LIB are close enough that there are large subsets that agree. By all means have a wrapper around exprt to mark when it has been through trnaslations but I really, really don't think you need this. It is overkill. Have a look at the way the SMT-LIB front-end works. > #### Internal Structure Output (Pretty Printing) How does this differ from lispirep and lispexpr? > ### Parsing SMT Output > > This deliverable is to enable parsing of the SMT solver output back > into a useful internal form for cbmc. This involves > replacing/rewriting the existing (hand crafted parser) with a parse- > generator version (e.g. flex/bison). Why use a bison parser for s-expressions? It is over-kill. > ### Runtime Swapping Solvers > Note, this should include CI for validation that the multiple solvers > are supported. This should include at least: Z3 and one other solver > (to be decided, e.g. CVC4, Boolector, Mathsat5, Yices2). In general I would suggest CVC5 and Bitwuzla instead of CVC4 and Boolector. You might also want to look at OpenSMT (as their group does maintain tools that user CPROVER and so might well be willing to help) and maybe STP. As for CI, I would recommend against MathSAT and Yices due to licensing restrictions. > ### (Bonus) Dynamic SMT Solver Configuration > > This deliverable is to enable more dynamic and subtle control of the > SMT solver(s) via some kind of configurations either inside CBMC or > through a configuration option that CBMC can pass through. The goal > is to be able to pass through knowledge or information to the > (specific?) SMT solver that can improve the performance. Have a look at paraMILS and also talk to solver authors. We currently have a good set of auto-tuned options for MathSAT from Alberto. Hope that helped and happy to advise / expand on any of the issues raised.
thomasspriggs commented 3 years ago

I think we should use --slice-formula instead of skipping the initialise function. It seems like a lower risk approach and moves the temporary work around from the implementation to the the tests.

thomasspriggs commented 3 years ago

I note that there is nothing here about incremental solving. For reasons that are a bit lengthy to go into here, I think that incrementality is really important. It is hard to retro-fit as it requires a change of architecture from the flat conversion we have, so it makes sense to think about when writing a new back-end. Depending on what you want to do with the incrementality and specifically the number and speed of calls you want to make, there are different architectures. If it is lots of small / fast goals (like incremental coverage, for example) then API integration is the way to go. If it is few, larger goals then pipes will probably be OK.

I am of the same opinion that incremental support is important and difficult to retrofit. Indeed, this is one reason in favour of doing a large refactor / rewrite. I'd like to make an incremental example one of the earlier things we get working and test against.

martin-cs commented 3 years ago

I am of the same opinion that incremental support is important and difficult to retrofit. Indeed, this is one reason in favour of doing a large refactor / rewrite. I'd like to make an incremental example one of the earlier things we get working and test against.

Great! It would be something really good to have. May I suggest starting with a solver other than Z3 as it has notably bad incremental performance. Also it might be worth getting more tests running with one of the analyses that actually makes use of the incremental interface. At the moment I think that is:

HTH

thomasspriggs commented 1 year ago

The user-facing documentation for the new SMT backend has been merged in this PR - https://github.com/diffblue/cbmc/pull/7363

It should be possible to find it on https://diffblue.github.io/cbmc/ once the publishing job has completed. The links to follow to find it will be -

  1. Go to https://diffblue.github.io/cbmc/
  2. User Guide in the side bar.
  3. The link to "A short manual" in that pages's content.
  4. The new page link will be under item 10.
thomasspriggs commented 1 year ago

The publishing job succeeded. The direct link is here - https://diffblue.github.io/cbmc/cprover-manual/md_smt2_incr.html