Documenting semantic of loop invariant synthesizers

Author: qinheping

doc/cprover-manual/loop-invariant-synthesizer.md

@@ -0,0 +1,37 @@
+[CPROVER Manual TOC](../)
+
+## Loop Invariant Synthesis with goto-instrument
+
+This is a loop invariant synthesizer built in goto-instrument that 
+synthesize [loop invariants](contracts-invariants.md) for a 
+pre-existing GOTO binary, annotate the invariant clause into 
+the GOTO binary, and produce an annotated binary as output.
+
+All synthesized loop invariants must be inductive, i.e., 
+all [loop-invariant checks](contracts-invariants.md#semantics)
+succeed in the instrumented GOTO binary.
+
+For different synthesis strategies, there are different guarantees 
+beyond the inductiveness on the synthesized loop invariants, 
+summarized in the following table.
+
+Strategy         | Flag                                           | Guarantees
+-----------------|------------------------------------------------|----
+Enumerative      | --synthesize-loop-invariants-enumerative       | All checks will succeeded in the annotated GOTO binary
+
+### Enumerative Synthesizer
+
+This synthesizer is designed for GOTO binary that contains only checks instrumented 
+with the flag  ```--pointer-check```, and synthesizes loop invariants that make
+all checks succeeded. The idea of the synthesizer is first inferring a clause, 
+using the idea of weakest preconditions, for each violated check to make it succeed, 
+and then enumerating a strengthening clause to make the inferred clause inductive.
+
+If the input GOTO binary contains a violated check that is not a pointer check, 
+the synthesizer will skip the inferring step and simply enumerate predicate that 
+is inductive and can make the check succeed.
+
+## Additional Resources
+
+- [Loop Contracts](contracts-loops.md)
+- [Inductive Invariant Generation via Abductive Inference](https://www.cs.utexas.edu/~isil/oopsla13.pdf)

regression/contracts/loop_invariant_synthesis_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---synthesize-loop-invariants --apply-loop-contracts
+--synthesize-loop-invariants-enumerative --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1146,7 +1146,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
   }
 
-  if(cmdline.isset("synthesize-loop-invariants"))
+  if(cmdline.isset("synthesize-loop-invariants-enumerative"))
   {
     log.warning() << "Loop invariant synthesizer is still work in progress. "
                      "It only generates TRUE as invariants."

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

@@ -21,8 +21,10 @@ Author: Qinheping Hu
 class messaget;
 
 /// Enumerative loop invariant synthesizers.
-/// It handles `goto_model` containing only checks instrumented by
-/// `goto-instrument` with the `--pointer-check` flag.
+/// It is designed for `goto_model` containing only checks instrumented by
+/// `goto-instrument` with the `--pointer-check` flag. H
+/// When other checks present, it will just enumerate candidates and check
+/// if they are valid.
 class enumerative_loop_invariant_synthesizert
   : public loop_invariant_synthesizer_baset
 {
@@ -34,6 +36,8 @@ class enumerative_loop_invariant_synthesizert
   {
   }
 
+  /// This synthesizer guarantees that, with the synthesized loop invariants,
+  /// all checks in the annotated GOTO program pass.
   invariant_mapt synthesize_all() override;
   exprt synthesize(loop_idt loop_id) override;
 

src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h

@@ -16,9 +16,10 @@ Author: Qinheping Hu
 
 #include "synthesizer_utils.h"
 
-#define OPT_SYNTHESIZE_LOOP_INVARIANTS "(synthesize-loop-invariants)"
+#define OPT_SYNTHESIZE_LOOP_INVARIANTS                                         \
+  "(synthesize-loop-invariants-enumerative)"
 #define HELP_LOOP_INVARIANT_SYNTHESIZER                                        \
-  " --synthesize-loop-invariants\n"                                            \
+  " --synthesize-loop-invariants-enumerative\n"                                \
   "                              synthesize and apply loop invariants\n"
 
 class messaget;
@@ -38,12 +39,13 @@ class loop_invariant_synthesizer_baset
   }
   virtual ~loop_invariant_synthesizer_baset() = default;
 
-  /// Synthesize loop invariants with which all checks in `goto_model`
-  /// succeed. The result is a map from `loop_idt` ids of loops to `exprt`
-  /// the goto-expression representation of synthesized invariants.
+  /// Synthesize loop invariants that are inductive in the given GOTO program.
+  ///
+  /// The result is a map from `loop_idt` ids of loops to `exprt`
+  /// the GOTO-expression representation of synthesized invariants.
   virtual invariant_mapt synthesize_all() = 0;
 
-  /// Synthesize loop invariant for a specified loop in the `goto_model`
+  /// Synthesize loop invariant for a specified loop in the `goto_model`.
   virtual exprt synthesize(loop_idt) = 0;
 
 protected: