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,16 @@
+#include <assert.h>
+#include <stdlib.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

@@ -15,8 +15,7 @@ Date: February 2016
 
 #include <algorithm>
 
-#include <analyses/local_may_alias.h>
-
+#include <goto-programs/goto_program.h>
 #include <goto-programs/remove_skip.h>
 
 #include <util/arith_tools.h>
@@ -30,8 +29,6 @@ Date: February 2016
 #include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
 
-#include "loop_utils.h"
-
 /// Predicate to be used with the exprt::visit() function. The function
 /// found_return_value() will return `true` iff this predicate is called on an
 /// expr that contains `__CPROVER_return_value`.
@@ -70,11 +67,12 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log)
   return result;
 }
 
-static void check_apply_invariants(
+void code_contractst::check_apply_invariants(
   goto_functionst::goto_functiont &goto_function,
   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());
 
@@ -92,16 +90,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;
@@ -112,17 +112,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())
@@ -138,11 +141,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)
@@ -370,15 +376,21 @@ 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);
 
-  // iterate over the (natural) loops in the function
+  // Iterate over the (natural) loops in the function,
+  // and apply any invariant annotations that we find.
   for(const auto &loop : natural_loops.loop_map)
     check_apply_invariants(
-      goto_function, local_may_alias, loop.first, loop.second);
+      goto_function,
+      local_may_alias,
+      loop.first,
+      loop.second,
+      symbol_table.lookup_ref(function_name).mode);
 }
 
 const symbolt &code_contractst::new_tmp_symbol(
@@ -953,7 +965,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);
 }
@@ -973,7 +985,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

@@ -18,6 +18,8 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+#include <analyses/local_may_alias.h>
+
 #include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
@@ -26,6 +28,8 @@ Date: February 2016
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 
+#include "loop_utils.h"
+
 class assigns_clauset;
 class replace_symbolt;
 
@@ -90,6 +94,13 @@ class code_contractst
     const irep_idt &function_id,
     const irep_idt &mode);
 
+  void check_apply_invariants(
+    goto_functionst::goto_functiont &goto_function,
+    const local_may_aliast &local_may_alias,
+    const goto_programt::targett loop_head,
+    const loopt &loop,
+    const irep_idt &mode);
+
   namespacet ns;
 
 protected:
@@ -154,7 +165,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());
+  if(has_sideeffect(invariant))
+  {
+    throw incorrect_goto_program_exceptiont(
+      "Loop invariant is not side-effect free.", code.find_source_location());
+  }
 
   PRECONDITION(loop->is_goto());
   loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);

src/goto-programs/goto_convert_side_effect.cpp

@@ -35,6 +35,24 @@ bool goto_convertt::has_function_call(const exprt &expr)
   return false;
 }
 
+bool goto_convertt::has_sideeffect(const exprt &expr)
+{
+  // TODO: In the future, we want to allow some function calls,
+  // specifically those which have an empty ASSIGNS clause annotation.
+  if(expr.id() == ID_side_effect)
+  {
+    return true;
+  }
+
+  for(const auto &op : expr.operands())
+  {
+    if(goto_convertt::has_sideeffect(op))
+      return true;
+  }
+
+  return false;
+}
+
 void goto_convertt::remove_assignment(
   side_effect_exprt &expr,
   goto_programt &dest,