Merge pull request #5942 from padhi-aws-forks/side_effects_fix

Invariant predicates were being cleaned (C -> logic via `clean_expr`) within `convert_loop_invariant` and were rejected if any intermediate goto instructions were introduced during the cleaning process. However, this check is overly conservative -- it ends up rejecting some complex, but pure, Boolean expressions that are compiled to multiple goto instructions.

We replace this logic with a call to `has_subexpr` with `ID_side_effect`.

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

@@ -20,7 +20,6 @@ Date: February 2016
 
 #include <ansi-c/c_expr.h>
 
-#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/remove_skip.h>
 
 #include <util/arith_tools.h>
@@ -34,8 +33,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`.
@@ -74,11 +71,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());
 
@@ -96,16 +94,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;
@@ -116,17 +116,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");
+    code_assertt assertion{invariant};
+    assertion.add_source_location() = 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));
+  code_assumet assumption{invariant};
+  assumption.add_source_location() = 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())
@@ -142,11 +145,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;
+    code_assertt assertion{invariant};
+    assertion.add_source_location() = 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)
@@ -158,15 +164,6 @@ static void check_apply_invariants(
     loop_end->set_condition(boolean_negate(loop_end->get_condition()));
 }
 
-void code_contractst::convert_to_goto(
-  const codet &code,
-  const irep_idt &mode,
-  goto_programt &program)
-{
-  goto_convertt converter(symbol_table, log.get_message_handler());
-  converter.goto_convert(code, program, mode);
-}
-
 bool code_contractst::has_contract(const irep_idt fun_name)
 {
   const symbolt &function_symbol = ns.lookup(fun_name);
@@ -322,7 +319,7 @@ code_contractst::create_ensures_instruction(
 
   // Create instructions corresponding to the ensures clause
   goto_programt ensures_program;
-  convert_to_goto(expression, mode, ensures_program);
+  converter.goto_convert(expression, ensures_program, mode);
 
   // return a pair containing:
   // 1. instructions corresponding to the ensures clause
@@ -424,10 +421,10 @@ bool code_contractst::apply_function_contract(
   if(requires.is_not_nil())
   {
     goto_programt assertion;
-    convert_to_goto(
+    converter.goto_convert(
       code_assertt(requires),
-      symbol_table.lookup_ref(function).mode,
-      assertion);
+      assertion,
+      symbol_table.lookup_ref(function).mode);
     auto lines_to_iterate = assertion.instructions.size();
     goto_program.insert_before_swap(target, assertion);
     std::advance(target, lines_to_iterate);
@@ -483,15 +480,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(
@@ -966,8 +969,8 @@ void code_contractst::add_contract_check(
     replace(requires_cond);
 
     goto_programt assumption;
-    convert_to_goto(
-      code_assumet(requires_cond), function_symbol.mode, assumption);
+    converter.goto_convert(
+      code_assumet(requires_cond), assumption, function_symbol.mode);
     check.destructive_append(assumption);
   }
 
@@ -1078,7 +1081,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);
 }
@@ -1098,7 +1101,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

@@ -19,14 +19,18 @@ Date: February 2016
 #include <string>
 #include <unordered_set>
 
+#include <goto-programs/goto_convert_class.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 
+#include "loop_utils.h"
+
 class assigns_clauset;
+class local_may_aliast;
 class replace_symbolt;
 
 class code_contractst
@@ -36,8 +40,9 @@ class code_contractst
     : ns(goto_model.symbol_table),
       symbol_table(goto_model.symbol_table),
       goto_functions(goto_model.goto_functions),
-      temporary_counter(0),
-      log(log)
+      log(log),
+      converter(symbol_table, log.get_message_handler())
+
   {
   }
 
@@ -89,26 +94,27 @@ 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:
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 
-  unsigned temporary_counter;
   messaget &log;
+  goto_convertt converter;
 
   std::unordered_set<irep_idt> summarized;
 
   /// \brief Enforce contract of a single function
   bool enforce_contract(const std::string &);
 
-  /// \brief Create goto instructions based on code and add them to program.
-  void convert_to_goto(
-    const codet &code,
-    const irep_idt &mode,
-    goto_programt &program);
-
   /// Insert assertion statements into the goto program to ensure that
   /// assigned memory is within the assignable memory frame.
   bool add_pointer_checks(const std::string &);
@@ -159,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_subexpr(invariant, ID_side_effect))
+  {
+    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_class.h

@@ -97,7 +97,6 @@ class goto_convertt:public messaget
 
   void rewrite_boolean(exprt &dest);
 
-  static bool has_sideeffect(const exprt &expr);
   static bool has_function_call(const exprt &expr);
 
   void remove_side_effect(