Fixed side-effect checking for invariant contracts

Moved side-effect checking on invariant contracts to goto-instrument. Since invariant contracts are expanded to multiple assertions (and assumptions) around the loop, it is cleaner to expand them only when they are enforced.

Author: SaswatPadhi

regression/contracts/invariant_side_effects/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main()
+{
+  unsigned N, *a = malloc(sizeof(unsigned int));
+
+  *a = 0;
+  while(*a < N)
+    __CPROVER_loop_invariant((0 <= *a) && (*a <= N))
+    {
+      ++(*a);
+    }
+
+  assert(*a == N);
+}

regression/contracts/invariant_side_effects/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion \*a == N: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that C expressions are correctly converted to logic
+when enforcing loop invariant annotations.

src/goto-instrument/code_contracts.cpp

@@ -17,6 +17,7 @@ Date: February 2016
 
 #include <analyses/local_may_alias.h>
 
+#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/remove_skip.h>
 
 #include <linking/static_lifetime_init.h>
@@ -74,9 +75,11 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
 
 static void check_apply_invariants(
   goto_functionst::goto_functiont &goto_function,
+  goto_convertt &converter,
   const local_may_aliast &local_may_alias,
   const goto_programt::targett loop_head,
-  const loopt &loop)
+  const loopt &loop,
+  const irep_idt &mode)
 {
   PRECONDITION(!loop.empty());
 
@@ -94,16 +97,18 @@ static void check_apply_invariants(
   if(invariant.is_nil())
     return;
 
-  // change H: loop; E: ...
+  // change
+  //   H: loop;
+  //   E: ...
   // to
-  // H: assert(invariant);
-  // havoc;
-  // assume(invariant);
-  // if(guard) goto E:
-  // loop;
-  // assert(invariant);
-  // assume(false);
-  // E: ...
+  //   H: assert(invariant);
+  //   havoc;
+  //   assume(invariant);
+  //   if(guard) goto E:
+  //   loop;
+  //   assert(invariant);
+  //   assume(false);
+  //   E: ...
 
   // find out what can get changed in the loop
   modifiest modifies;
@@ -114,17 +119,20 @@ static void check_apply_invariants(
 
   // assert the invariant
   {
-    goto_programt::targett a = havoc_code.add(
-      goto_programt::make_assertion(invariant, loop_head->source_location));
-    a->source_location.set_comment("Check loop invariant before entry");
+    auto assertion = code_assertt(invariant);
+    assertion.add_source_location().swap(loop_head->source_location);
+    converter.goto_convert(assertion, havoc_code, mode);
+    havoc_code.instructions.back().source_location.set_comment(
+      "Check loop invariant before entry");
   }
 
   // havoc variables being written to
   build_havoc_code(loop_head, modifies, havoc_code);
 
   // assume the invariant
-  havoc_code.add(
-    goto_programt::make_assumption(invariant, loop_head->source_location));
+  auto assumption = code_assumet(invariant);
+  assumption.add_source_location().swap(loop_head->source_location);
+  converter.goto_convert(assumption, havoc_code, mode);
 
   // non-deterministically skip the loop if it is a do-while loop
   if(!loop_head->is_goto())
@@ -140,11 +148,14 @@ static void check_apply_invariants(
 
   // assert the invariant at the end of the loop body
   {
-    goto_programt::instructiont a =
-      goto_programt::make_assertion(invariant, loop_end->source_location);
-    a.source_location.set_comment("Check that loop invariant is preserved");
-    goto_function.body.insert_before_swap(loop_end, a);
-    ++loop_end;
+    auto assertion = code_assertt(invariant);
+    assertion.add_source_location().swap(loop_end->source_location);
+    converter.goto_convert(assertion, havoc_code, mode);
+    havoc_code.instructions.back().source_location.set_comment(
+      "Check that loop invariant is preserved");
+    auto offset = havoc_code.instructions.size();
+    goto_function.body.insert_before_swap(loop_end, havoc_code);
+    std::advance(loop_end, offset);
   }
 
   // change the back edge into assume(false) or assume(guard)
@@ -290,15 +301,24 @@ bool code_contractst::apply_function_contract(
 }
 
 void code_contractst::apply_loop_contract(
+  const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function)
 {
   local_may_aliast local_may_alias(goto_function);
   natural_loops_mutablet natural_loops(goto_function.body);
 
+  // setup goto_convertt to convert C expressions to logic
+  goto_convertt converter(symbol_table, log.get_message_handler());
+
   // iterate over the (natural) loops in the function
   for(const auto &loop : natural_loops.loop_map)
     check_apply_invariants(
-      goto_function, local_may_alias, loop.first, loop.second);
+      goto_function,
+      converter,
+      local_may_alias,
+      loop.first,
+      loop.second,
+      symbol_table.lookup_ref(function_name).mode);
 }
 
 const symbolt &code_contractst::new_tmp_symbol(
@@ -889,7 +909,7 @@ bool code_contractst::enforce_contracts()
     if(has_contract(goto_function.first))
       funs_to_enforce.insert(id2string(goto_function.first));
     else
-      apply_loop_contract(goto_function.second);
+      apply_loop_contract(goto_function.first, goto_function.second);
   }
   return enforce_contracts(funs_to_enforce);
 }
@@ -909,7 +929,7 @@ bool code_contractst::enforce_contracts(
                   << messaget::eom;
       continue;
     }
-    apply_loop_contract(goto_function->second);
+    apply_loop_contract(goto_function->first, goto_function->second);
 
     if(!has_contract(fun))
     {

src/goto-instrument/code_contracts.h

@@ -153,7 +153,9 @@ class code_contractst
     const exprt &lhs,
     std::vector<exprt> &aliasable_references);
 
-  void apply_loop_contract(goto_functionst::goto_functiont &goto_function);
+  void apply_loop_contract(
+    const irep_idt &function_name,
+    goto_functionst::goto_functiont &goto_function);
 
   /// \brief Does the named function have a contract?
   bool has_contract(const irep_idt);

src/goto-programs/goto_convert.cpp

@@ -868,13 +868,11 @@ void goto_convertt::convert_loop_invariant(
   if(invariant.is_nil())
     return;
 
-  goto_programt no_sideeffects;
-  clean_expr(invariant, no_sideeffects, mode);
-
-  INVARIANT_WITH_DIAGNOSTICS(
-    no_sideeffects.instructions.empty(),
-    "loop invariant is not side-effect free",
-    code.find_source_location());
+  // Loop contracts are expanded to assertions (and assumptions)
+  // at multiple code points around a loop.
+  // Rather than performing `clean_expr` during compilation,
+  // we convert the invariant to logic at these various code points
+  // only when they are enforced (using goto-instrument).
 
   PRECONDITION(loop->is_goto());
   loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);