Add apply_loop_contracts in dfcc

Author: qinheping

regression/contracts-dfcc/invar_assigns_opt/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+int main()
+{
+  foo();
+}
+
+int foo()
+{
+  int r1, s1 = 1;
+  __CPROVER_assume(r1 >= 0);
+  while(r1 > 0)
+    __CPROVER_loop_invariant(r1 >= 0 && s1 == 1) __CPROVER_decreases(r1)
+    {
+      s1 = 1;
+      r1--;
+    }
+  assert(r1 == 0);
+
+  int r2, s2 = 1;
+  __CPROVER_assume(r2 >= 0);
+  while(r2 > 0)
+    __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)
+      __CPROVER_decreases(r2)
+    {
+      s2 = 1;
+      r2--;
+    }
+  assert(r2 == 0);
+  return 0;
+}

regression/contracts-dfcc/invar_assigns_opt/test.desc

@@ -0,0 +1,22 @@
+CORE
+main.c
+--dfcc main
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that adding assigns clause is optional
+and that if a proof does not require it, then adding an
+appropriate assigns clause does not lead to any 
+unexpected behavior. 

regression/contracts-dfcc/loop_assigns-01/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  foo();
+}
+
+void foo()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_object_whole(b->data))
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b->data[i] = 1;
+    }
+
+  assert(b->data[5] == 0);
+}

regression/contracts-dfcc/loop_assigns-01/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--dfcc main
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test (taken from #6021) shows the need for assigns clauses on loops.
+The alias analysis in this case returns `unknown`,
+and so we must manually annotate an assigns clause on the loop.

regression/contracts-dfcc/loop_assigns_inference-02/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  foo();
+}
+
+void foo()
+{
+  int *b = malloc(SIZE * sizeof(int));
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b[i] = 1;
+    }
+}

regression/contracts-dfcc/loop_assigns_inference-02/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--dfcc main
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns clauses (i, __CPROVER_POINTER_OBJECT(b)) is inferred,
+and widened correctly.

src/goto-instrument/Makefile

@@ -18,6 +18,8 @@ SRC = accelerate/accelerate.cpp \
       call_sequences.cpp \
       contracts/contracts.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
+      contracts/dynamic-frames/dfcc_loop_utils.cpp \
+      contracts/dynamic-frames/dfcc_loop_instrument.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \

src/goto-instrument/contracts/cfg_info.h

@@ -26,6 +26,7 @@ Date: June 2022
 
 #include <analyses/dirty.h>
 #include <analyses/locals.h>
+#include <goto-instrument/contracts/dynamic-frames/dfcc_loop_utils.h>
 #include <goto-instrument/havoc_utils.h>
 #include <goto-instrument/loop_utils.h>
 
@@ -152,6 +153,26 @@ class loop_cfg_infot : public cfg_infot
     }
   }
 
+  loop_cfg_infot(
+    goto_functiont &_goto_function,
+    const std::vector<std::size_t> nesting_ids)
+    : is_dirty(_goto_function)
+  {
+    for(auto it = _goto_function.body.instructions.begin();
+        it != _goto_function.body.instructions.end();
+        it++)
+    {
+      if(
+        it->is_decl() && !get_loop_instr_type(it).empty() &&
+        std::find(
+          nesting_ids.begin(), nesting_ids.end(), get_loop_nesting_id(it)) !=
+          nesting_ids.end())
+      {
+        locals.insert(it->decl_symbol().get_identifier());
+      }
+    }
+  }
+
   /// Returns true iff `ident` is a loop local.
   bool is_local(const irep_idt &ident) const override
   {
@@ -201,7 +222,7 @@ class goto_program_cfg_infot : public cfg_infot
 public:
   explicit goto_program_cfg_infot(const goto_programt &goto_program)
   {
-    // collect symbols declared in the insruction sequence as locals
+    // collect symbols declared in the instruction sequence as locals
     goto_program.get_decl_identifiers(locals);
 
     // collect dirty locals

src/goto-instrument/contracts/contracts.cpp

@@ -220,7 +220,7 @@ void code_contractst::check_apply_loop_contracts(
 
       // If the set contains pairs (i, a[i]),
       // we widen them to (i, __CPROVER_POINTER_OBJECT(a))
-      widen_assigns(to_havoc, ns);
+      widen_assigns(to_havoc, ns, false);
 
       log.debug() << "No loop assigns clause provided. Inferred targets: {";
       // Add inferred targets to the loop assigns clause.

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -38,7 +38,6 @@ Author: Remi Delmas, [email protected]
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
 #include <goto-instrument/contracts/cfg_info.h>
-#include <goto-instrument/contracts/instrument_spec_assigns.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/nondet_static.h>
 #include <langapi/language.h>
@@ -188,15 +187,9 @@ dfcct::dfcct(
     utils(goto_model, message_handler),
     library(goto_model, utils, message_handler),
     ns(goto_model.symbol_table),
-    instrument(goto_model, message_handler, utils, library),
     memory_predicates(goto_model, utils, library, instrument, message_handler),
     spec_functions(goto_model, message_handler, utils, library, instrument),
-    contract_clauses_codegen(
-      goto_model,
-      message_handler,
-      utils,
-      library,
-      spec_functions),
+    contract_clauses_codegen(goto_model, message_handler, utils, library),
     contract_handler(
       goto_model,
       message_handler,
@@ -214,6 +207,13 @@ dfcct::dfcct(
       instrument,
       spec_functions,
       contract_handler),
+    loop_instrument(
+      goto_model,
+      message_handler,
+      library,
+      spec_functions,
+      contract_clauses_codegen),
+    instrument(goto_model, message_handler, utils, loop_instrument, library),
     max_assigns_clause_size(0)
 {
   transform_goto_model();
@@ -377,7 +377,7 @@ void dfcct::wrap_checked_function()
     if(other_symbols.find(wrapper_id) != other_symbols.end())
       other_symbols.erase(wrapper_id);
 
-    // upate max contract size
+    // update max contract size
     const std::size_t assigns_clause_size =
       contract_handler.get_assigns_clause_size(contract_id);
     if(assigns_clause_size > max_assigns_clause_size)
@@ -492,8 +492,13 @@ void dfcct::instrument_other_functions()
 
   // TODO specialise the library functions for the max size of
   // loop and function contracts
-  if(to_check.has_value())
+  if(to_check.has_value() || loop_instrument.max_nof_assigns != 0)
   {
+    max_assigns_clause_size =
+      loop_instrument.max_nof_assigns > max_assigns_clause_size
+        ? loop_instrument.max_nof_assigns
+        : max_assigns_clause_size;
+
     log.status() << "Specializing cprover_contracts functions for assigns "
                     "clauses of at most "
                  << max_assigns_clause_size << " targets" << messaget::eom;

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -38,6 +38,7 @@ Author: Remi Delmas, [email protected]
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_lift_memory_predicates.h"
+#include "dfcc_loop_instrument.h"
 #include "dfcc_spec_functions.h"
 #include "dfcc_swap_and_wrap.h"
 #include "dfcc_utils.h"
@@ -214,12 +215,13 @@ class dfcct
   dfcc_utilst utils;
   dfcc_libraryt library;
   namespacet ns;
-  dfcc_instrumentt instrument;
   dfcc_lift_memory_predicatest memory_predicates;
   dfcc_spec_functionst spec_functions;
   dfcc_contract_clauses_codegent contract_clauses_codegen;
   dfcc_contract_handlert contract_handler;
   dfcc_swap_and_wrapt swap_and_wrap;
+  dfcc_loop_instrumentt loop_instrument;
+  dfcc_instrumentt instrument;
 
   /// Tracks the maximum number of targets in any assigns clause handled in the
   /// transformation (used to specialize/unwind loops in DFCC library functions)

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

@@ -30,14 +30,12 @@ dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent(
   goto_modelt &goto_model,
   message_handlert &message_handler,
   dfcc_utilst &utils,
-  dfcc_libraryt &library,
-  dfcc_spec_functionst &spec_functions)
+  dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(utils),
     library(library),
-    spec_functions(spec_functions),
     ns(goto_model.symbol_table)
 {
 }
@@ -63,6 +61,7 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
 
   // inline resulting program and check for loops
   inline_and_check_warnings(dest);
+  dest.update();
   PRECONDITION_WITH_DIAGNOSTICS(
     utils.has_no_loops(dest),
     "loops in assigns clause specification functions must be unwound before "

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h

@@ -29,7 +29,6 @@ class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
 class dfcc_utilst;
-class dfcc_spec_functionst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
 
@@ -40,14 +39,11 @@ class dfcc_contract_clauses_codegent
   /// \param message_handler used debug/warning/error messages
   /// \param utils utility class for dynamic frames
   /// \param library the contracts instrumentation library
-  /// \param spec_functions provides translation methods for assignable set
-  /// or freeable set specification functions.
   dfcc_contract_clauses_codegent(
     goto_modelt &goto_model,
     message_handlert &message_handler,
     dfcc_utilst &utils,
-    dfcc_libraryt &library,
-    dfcc_spec_functionst &spec_functions);
+    dfcc_libraryt &library);
 
   /// \brief Generates instructions encoding the \p assigns_clause targets and
   /// adds them to \p dest.
@@ -85,7 +81,6 @@ class dfcc_contract_clauses_codegent
   messaget log;
   dfcc_utilst &utils;
   dfcc_libraryt &library;
-  dfcc_spec_functionst &spec_functions;
   namespacet ns;
 
   /// Generates GOTO instructions to build the representation of the given