Merge pull request #7132 from thomasspriggs/tas/more_smt_docs

Add documentation of the structure of the SMT incremental decision procedure

Author: thomasspriggs

src/solvers/smt2_incremental/README.md

@@ -1,5 +1,7 @@
 # Incremental SMT backend
 
+## General usage
+
 CBMC comes with a solver-agnostic incremental SMT backend.
 
 The SMT incremental backend supports the following `C` features:
@@ -40,3 +42,60 @@ removed from the formula to be converted.
 
 As we move forward with our array-support implementation, we anticipate that the
 need for this extra flag will be diminished.
+
+## Internal code architecture
+
+### Overview of the sequence of data processing and data flow -
+
+1. Other parts of the cbmc code base send `exprt` based expressions to the
+decision procedure through the `handle`, `set_to` and `get` member functions.
+See the base class `decision_proceduret` for doxygen of these functions.
+
+2. The `smt2_incremental_decision_proceduret` is responsible for holding state
+and building commands to send to the solver. It uses `convert_expr_to_smt` for
+the state free (pure) portion of the `exprt` to `termt` conversions.
+
+3. `smt2_incremental_decision_proceduret` sends `smt_commandt` to
+`smt_piped_solver_processt`. Although `exprt` is broadly equivalent to `termt`,
+the terms must be part of a command giving them a broader meaning before they
+are sent to the solver.
+
+4. `smt_piped_solver_processt` uses the `smt_to_smt2_string` function to perform
+the conversion from the tree structure of the `smt_commandt` into the linear
+structure of the string for sending to the solver.
+
+5. `smt_piped_solver_processt` sends `std::string` to `piped_processt`.
+
+6. `piped_processt` has operating system specific implementations which use
+POSIX / Windows API calls to send the strings to the solver process via a pipe.
+Note that the solver is kept in a operating system separated process, not a
+thread. This supports multiprocessing with the solver ingesting commands whilst
+the cbmc process continues symex to generate the following commands.
+
+7. `piped_processt` receives output strings from the solver process using OS API
+calls and a buffer, when the `smt_piped_solver_processt` requests them.
+
+8. The response strings returned to `smt_solve_processt` are converted into type
+less parse trees in the form of raw `irept`s using `smt2irep`. `smt2irep` is
+essentially just an S-expression parser.
+
+9. `smt_piped_solver_processt` uses `validate_smt_response` to convert the
+`irept` parse tree into either a set of validation errors or a `smt_responset`.
+The case of validation errors is considered to be an error with the solver.
+Therefore an exception may be thrown for use as user feedback rather than
+violating an `INVARIANT` as would be the case for an internal cbmc error.
+
+10. The well sorted `smt_reponset` is then returned to the
+`smt2_incremental_decision_proceduret`.
+
+11. In the case of `smt2_incremental_decision_proceduret::get` the response is
+expected to be an `smt_get_value_responset`. The decision procedure uses
+`construct_value_expr_from_smt` to convert the value term in the response from
+the solver into an expression value. This requires information from the decision
+procedure about the kind of type the constructed expression should have. The
+reason for this is that the smt formula (although well sorted) does not encode
+cbmc's notion of types and a given value in SMT terms could correspond to
+multiple different types of cbmc expression.
+
+12. The constructed expression can then be returned to the rest of the cbmc code
+base outside the decision procedure.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -138,6 +138,13 @@ class smt2_incremental_decision_proceduret final
   /// array expressions when support for them is implemented.
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_identifiers;
+  /// This maps from the unsorted/untyped string/symbol for the identifiers
+  /// which we have declared in SMT solver to the corresponding sorted/typed
+  /// `smt_identifier_termt`. This enables type checking the parse trees of
+  /// responses received back from the solver. It is required because without
+  /// the definitive sorts we would need to attempt to infer the sorts of
+  /// identifiers from the surrounding terms which would be a looser check with
+  /// a more complex implementation.
   std::unordered_map<irep_idt, smt_identifier_termt> identifier_table;
   /// This map is used to track object related state. See documentation in
   /// object_tracking.h for details.