Merge pull request #7007 from Herbping/loop_invariant_synthesis

CONTRACTS: New classes for loop-invariant-synthesizer interface

Author: feliperodri

regression/contracts/loop_invariant_synthesis_01/main.c

@@ -0,0 +1,27 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned int size;
+  __CPROVER_assume(size < 50);
+  int *p = malloc(size * 4);
+  int result = 0;
+
+  for(unsigned int i = 0; i < size; i++)
+  {
+    result += p[i];
+  }
+
+  for(unsigned int i = 0; i < size; i++)
+    // clang-format off
+  __CPROVER_loop_invariant(1 == 1)
+    // clang-format on
+    {
+      result += p[i];
+    }
+
+  for(unsigned int i = 0; i < size; i++)
+  {
+    result += p[i];
+  }
+}

regression/contracts/loop_invariant_synthesis_01/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--synthesize-loop-invariants --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line 10 Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line 15 Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line 15 Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line 23 Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line 23 Check that loop invariant is preserved: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test case checks if invariants are generated for unannotated loops.

src/goto-instrument/Makefile

@@ -68,6 +68,8 @@ SRC = accelerate/accelerate.cpp \
       source_lines.cpp \
       splice_call.cpp \
       stack_depth.cpp \
+      synthesizer/enumerative_loop_invariant_synthesizer.cpp \
+      synthesizer/synthesizer_utils.cpp \
       thread_instrumentation.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1146,6 +1146,17 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
   }
 
+  if(cmdline.isset("synthesize-loop-invariants"))
+  {
+    log.warning() << "Loop invariant synthesizer is still work in progress. "
+                     "It only generates TRUE as invariants."
+                  << messaget::eom;
+
+    // Synthesize loop invariants and annotate them into `goto_model`
+    enumerative_loop_invariant_synthesizert synthesizer(goto_model, log);
+    annotate_invariants(synthesizer.synthesize_all(), goto_model, log);
+  }
+
   if(
     cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
     cmdline.isset(FLAG_ENFORCE_CONTRACT))
@@ -1895,6 +1906,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Code contracts:\n"
     HELP_LOOP_CONTRACTS
+    HELP_LOOP_INVARIANT_SYNTHESIZER
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT
     "\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -41,6 +41,7 @@ Author: Daniel Kroening, [email protected]
 #include "unwindset.h"
 
 #include "contracts/contracts.h"
+#include "synthesizer/enumerative_loop_invariant_synthesizer.h"
 #include "wmm/weak_memory.h"
 
 // clang-format off
@@ -116,6 +117,7 @@ Author: Daniel Kroening, [email protected]
   OPT_NONDET_VOLATILE \
   "(ensure-one-backedge-per-target)" \
   OPT_CONFIG_LIBRARY \
+  OPT_SYNTHESIZE_LOOP_INVARIANTS \
   // empty last line
 
 // clang-format on

src/goto-instrument/module_dependencies.txt

@@ -10,5 +10,6 @@ langapi # should go away
 linking
 pointer-analysis
 solvers
+synthesizer
 util
 wmm

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+Module: Enumerative Loop Invariant Synthesizer
+
+Author: Qinheping Hu
+
+\*******************************************************************/
+
+/// \file
+/// Enumerative Loop Invariant Synthesizer
+
+#include "enumerative_loop_invariant_synthesizer.h"
+
+void enumerative_loop_invariant_synthesizert::init_candidates()
+{
+  for(auto &function_p : goto_model.goto_functions.function_map)
+  {
+    natural_loopst natural_loops;
+    natural_loops(function_p.second.body);
+
+    // Initialize invariants for unannotated loops as true
+    for(const auto &loop_head_and_content : natural_loops.loop_map)
+    {
+      goto_programt::const_targett loop_end =
+        get_loop_end_from_loop_head_and_content(
+          loop_head_and_content.first, loop_head_and_content.second);
+
+      loop_idt new_id(function_p.first, loop_end->loop_number);
+
+      // we only synthesize invariants for unannotated loops
+      if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())
+      {
+        invariant_candiate_map[new_id] = true_exprt();
+      }
+    }
+  }
+}
+
+invariant_mapt enumerative_loop_invariant_synthesizert::synthesize_all()
+{
+  init_candidates();
+
+  // Now this method only generate true for all unnotated loops.
+  // The implementation will be added later.
+  return invariant_candiate_map;
+}
+
+exprt enumerative_loop_invariant_synthesizert::synthesize(loop_idt loop_id)
+{
+  return true_exprt();
+}

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: Enumerative Loop Invariant Synthesizer
+
+Author: Qinheping Hu
+
+\*******************************************************************/
+
+/// \file
+/// Enumerative Loop Invariant Synthesizer
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H
+// NOLINTNEXTLINE(whitespace/line_length)
+#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H
+
+#include <goto-programs/goto_model.h>
+
+#include "loop_invariant_synthesizer_base.h"
+
+class messaget;
+
+/// Enumerative loop invariant synthesizers.
+/// It handles `goto_model` containing only checks instrumented by
+/// `goto-instrument` with the `--pointer-check` flag.
+class enumerative_loop_invariant_synthesizert
+  : public loop_invariant_synthesizer_baset
+{
+public:
+  enumerative_loop_invariant_synthesizert(
+    const goto_modelt &goto_model,
+    messaget &log)
+    : loop_invariant_synthesizer_baset(goto_model, log)
+  {
+  }
+
+  invariant_mapt synthesize_all() override;
+  exprt synthesize(loop_idt loop_id) override;
+
+private:
+  /// Initialize invariants as true for all unannotated loops.
+  void init_candidates();
+
+  invariant_mapt invariant_candiate_map;
+};
+
+// NOLINTNEXTLINE(whitespace/line_length)
+#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H

src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Loop Invariant Synthesizer Interface
+
+Author: Qinheping Hu
+
+\*******************************************************************/
+
+/// \file
+/// Loop Invariant Synthesizer Interface
+
+#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H
+#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H
+
+#include <goto-programs/goto_model.h>
+
+#include "synthesizer_utils.h"
+
+#define OPT_SYNTHESIZE_LOOP_INVARIANTS "(synthesize-loop-invariants)"
+#define HELP_LOOP_INVARIANT_SYNTHESIZER                                        \
+  " --synthesize-loop-invariants\n"                                            \
+  "                              synthesize and apply loop invariants\n"
+
+class messaget;
+
+/// A base class for loop invariant synthesizers.
+/// Provides a method for synthesizing loop invariants in a given `goto_model`.
+///
+/// Derived class should clarify what types of `goto_model` they targets, e.g.,
+/// a `goto_model` contains only memory safety checks, or a `goto_model`
+/// contains both memory safety checks and correctness checks.
+class loop_invariant_synthesizer_baset
+{
+public:
+  loop_invariant_synthesizer_baset(const goto_modelt &goto_model, messaget &log)
+    : goto_model(goto_model), log(log)
+  {
+  }
+  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.
+  virtual invariant_mapt synthesize_all() = 0;
+
+  /// Synthesize loop invariant for a specified loop in the `goto_model`
+  virtual exprt synthesize(loop_idt) = 0;
+
+protected:
+  const goto_modelt &goto_model;
+  messaget &log;
+};
+
+#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H

src/goto-instrument/synthesizer/module_dependencies.txt

@@ -0,0 +1,8 @@
+analyses
+ansi-c
+goto-instrument/contracts
+goto-instrument/synthesizer
+goto-instrument
+goto-programs
+langapi
+util