conditional assigns clauses

Author: kroening

regression/cprover/contracts/check_assigns6.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 check_assigns6.c
 
 ^EXIT=10$

src/cprover/instrument_contracts.cpp

@@ -44,7 +44,7 @@ static bool is_symbol_member(const exprt &expr)
 static exprt
 make_assigns_assertion(const exprt::operandst &assigns, const exprt &lhs)
 {
-  // trivial?
+  // trivial match?
   if(is_symbol_member(lhs))
   {
     for(auto &a : assigns)
@@ -56,11 +56,28 @@ make_assigns_assertion(const exprt::operandst &assigns, const exprt &lhs)
 
   for(auto &a : assigns)
   {
-    auto a_address = make_address(a);
-    auto lhs_address = make_address(lhs);
-    lhs_address =
-      typecast_exprt::conditional_cast(lhs_address, a_address.type());
-    disjuncts.push_back(equal_exprt(a_address, lhs_address));
+    if(a.id() == ID_conditional_target_group)
+    {
+      auto &condition = to_binary_expr(a).op0();
+      auto &targets = to_multi_ary_expr(to_binary_expr(a).op1());
+      for(auto &target : targets.operands())
+      {
+        auto target_address = make_address(target);
+        auto lhs_address = make_address(lhs);
+        lhs_address =
+          typecast_exprt::conditional_cast(lhs_address, target_address.type());
+        disjuncts.push_back(
+          and_exprt(condition, equal_exprt(target_address, lhs_address)));
+      }
+    }
+    else
+    {
+      auto target_address = make_address(a);
+      auto lhs_address = make_address(lhs);
+      lhs_address =
+        typecast_exprt::conditional_cast(lhs_address, target_address.type());
+      disjuncts.push_back(equal_exprt(target_address, lhs_address));
+    }
   }
 
   return disjunction(disjuncts);
@@ -288,6 +305,9 @@ void replace_function_calls_by_contracts(
         replace_symbol.insert(
           symbol_exprt("__CPROVER_return_value", call_lhs.type()), call_lhs);
 
+        goto_programt dest;
+
+        // assert the preconditions
         for(auto &precondition : contract.requires())
         {
           auto location = it->source_location();
@@ -298,32 +318,57 @@ void replace_function_calls_by_contracts(
           auto replaced_precondition = precondition;
           replace_symbol(replaced_precondition);
 
-          auto assertion_instruction =
-            goto_programt::make_assertion(replaced_precondition, location);
-
-          body.insert_before_swap(it, assertion_instruction);
+          dest.add(
+            goto_programt::make_assertion(replaced_precondition, location));
         }
 
-        // advance the iterator
-        it = std::next(it, contract.requires().size());
-
         // havoc the 'assigned' variables
-        for(auto &lhs : contract.assigns())
+        for(auto &assigns_clause : contract.assigns())
         {
           auto location = it->source_location();
 
-          auto rhs = side_effect_expr_nondett(lhs.type(), location);
-          auto replaced_lhs = lhs;
-          replace_symbol(replaced_lhs);
+          if(assigns_clause.id() == ID_conditional_target_group)
+          {
+            const auto &condition = to_binary_expr(assigns_clause).op0();
+            auto replaced_condition = condition;
+            replace_symbol(replaced_condition);
 
-          auto assignment_instruction =
-            goto_programt::make_assignment(replaced_lhs, rhs, location);
+            const auto &targets =
+              to_multi_ary_expr(to_binary_expr(assigns_clause).op1())
+                .operands();
 
-          body.insert_before_swap(it, assignment_instruction);
-        }
+            for(auto &target : targets)
+            {
+              auto rhs = side_effect_expr_nondett(target.type(), location);
 
-        // advance the iterator
-        it = std::next(it, contract.assigns().size());
+              auto replaced_lhs = target;
+              replace_symbol(replaced_lhs);
+
+              auto goto_instruction =
+                dest.add(goto_programt::make_incomplete_goto(
+                  not_exprt(replaced_condition), location));
+
+              dest.add(
+                goto_programt::make_assignment(replaced_lhs, rhs, location));
+
+              auto skip_instruction =
+                dest.add(goto_programt::make_skip(location));
+
+              goto_instruction->complete_goto(skip_instruction);
+            }
+          }
+          else
+          {
+            const auto &lhs = assigns_clause;
+            auto rhs = side_effect_expr_nondett(lhs.type(), location);
+
+            auto replaced_lhs = lhs;
+            replace_symbol(replaced_lhs);
+
+            dest.add(
+              goto_programt::make_assignment(replaced_lhs, rhs, location));
+          }
+        }
 
         // assume the postconditions
         for(auto &postcondition : contract.ensures())
@@ -333,17 +378,15 @@ void replace_function_calls_by_contracts(
           auto replaced_postcondition = postcondition;
           replace_symbol(replaced_postcondition);
 
-          auto assumption_instruction =
-            goto_programt::make_assumption(replaced_postcondition, location);
-
-          body.insert_before_swap(it, assumption_instruction);
+          dest.add(
+            goto_programt::make_assumption(replaced_postcondition, location));
         }
 
-        // advance the iterator
-        it = std::next(it, contract.ensures().size());
-
         // remove the function call
         it->turn_into_skip();
+
+        // insert after 'it' to preserve branches to the call
+        body.destructive_insert(std::next(it), dest);
       }
     }
   }