update

Author: Aalok Thakkar

src/ansi-c/c_typecheck_base.h

@@ -144,6 +144,7 @@ class c_typecheck_baset:
   virtual void typecheck_while(code_whilet &code);
   virtual void typecheck_dowhile(code_dowhilet &code);
   virtual void typecheck_start_thread(codet &code);
+  virtual void typecheck_spec_assigns(codet &code);
   virtual void typecheck_spec_loop_invariant(codet &code);
   virtual void typecheck_spec_decreases(codet &code);
 

src/ansi-c/c_typecheck_code.cpp

@@ -484,6 +484,7 @@ void c_typecheck_baset::typecheck_for(codet &code)
     typecheck_code(code); // recursive call
   }
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
@@ -773,6 +774,7 @@ void c_typecheck_baset::typecheck_while(code_whilet &code)
   break_is_allowed=old_break_is_allowed;
   continue_is_allowed=old_continue_is_allowed;
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
@@ -807,10 +809,29 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code)
   break_is_allowed=old_break_is_allowed;
   continue_is_allowed=old_continue_is_allowed;
 
+  typecheck_spec_assigns(code);
   typecheck_spec_loop_invariant(code);
   typecheck_spec_decreases(code);
 }
 
+void c_typecheck_baset::typecheck_spec_assigns(codet &code)
+{
+  if(code.find(ID_C_spec_assigns).is_not_nil())
+  {
+    for(const exprt &operand : static_cast<exprt &>(code.add(ID_C_spec_assigns)).operands())
+    {
+      if(
+        operand.id() != ID_symbol && operand.id() != ID_ptrmember &&
+        operand.id() != ID_member && operand.id() != ID_dereference)
+      {
+        error().source_location = code.source_location();
+        error() << "illegal target in assigns clause" << eom;
+        throw 0;
+      }
+    }
+  }
+}
+
 void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code)
 {
   if(code.find(ID_C_spec_loop_invariant).is_not_nil())

src/ansi-c/parser.y

@@ -2453,6 +2453,9 @@ iteration_statement:
           statement($$, ID_while);
           parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8)));
 
+          if(!parser_stack($4).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($4)); 
+
           if(!parser_stack($6).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands());
 
@@ -2468,6 +2471,9 @@ iteration_statement:
           statement($$, ID_dowhile);
           parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
 
+          if(!parser_stack($7).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($7));
+
           if(!parser_stack($8).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
 
@@ -2499,6 +2505,9 @@ iteration_statement:
           mto($$, $7);
           mto($$, $12);
 
+          if(!parser_stack($9).is_not_nil())
+            parser_stack($$).add(ID_C_spec_assigns).swap(parser_stack($9));
+
           if(!parser_stack($10).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands());
 

src/goto-instrument/contracts/assigns.cpp

@@ -238,6 +238,11 @@ goto_programt assigns_clauset::havoc_code(
   return havoc_statements;
 }
 
+std::vector<assigns_clause_targett *> assigns_clauset::getTargets()
+{
+    return targets;
+}
+
 exprt assigns_clauset::alias_expression(const exprt &lhs)
 {
   if(targets.empty())

src/goto-instrument/contracts/assigns.h

@@ -73,6 +73,7 @@ class assigns_clauset
     irep_idt function_name,
     irep_idt language_mode);
   exprt alias_expression(const exprt &lhs);
+  std::vector<assigns_clause_targett *> getTargets();
 
   exprt compatible_expression(const assigns_clauset &called_assigns);
 

src/goto-instrument/contracts/contracts.cpp

@@ -70,7 +70,10 @@ void code_contractst::check_apply_loop_contracts(
       t->location_number > loop_end->location_number)
       loop_end = t;
 
-  // see whether we have an invariant and a decreases clause
+  // see whether we have an assigns clause, an invariant and a decreases clause
+
+  exprt assigns = static_cast<const exprt &>(
+    loop_end->get_condition().find(ID_C_spec_assigns));
   exprt invariant = static_cast<const exprt &>(
     loop_end->get_condition().find(ID_C_spec_loop_invariant));
   exprt decreases_clause = static_cast<const exprt &>(
@@ -119,12 +122,57 @@ void code_contractst::check_apply_loop_contracts(
   //   assume(false);
   //   E: ...
 
-  // find out what can get changed in the loop
+  // Check that the assigns clause for loop is compatible
+  // with the assigns clause for the calling function.
+
+  assigns_clauset assigns_clause(assigns, *this, mode, log);
+
+  if(assigns.is_not_nil())
+  {
+    // extract the assigns clause of the function:
+    const symbolt &function_symbol = ns.lookup(function_name);
+    const auto &code_type = to_code_with_contract_type(function_symbol.type);
+    exprt function_assigns = code_type.assigns();
+
+    auto instruction_iterator = loop_head;
+
+    if(function_assigns.is_not_nil())
+    {
+      // check compatibility of assigns clause with the called function
+      assigns_clauset function_assigns_clause(function_assigns, *this, function_name, log);
+      exprt compatible = assigns_clause.compatible_expression(function_assigns_clause);
+      goto_programt alias_assertion;
+      alias_assertion.add(goto_programt::make_assertion(
+        compatible, instruction_iterator->source_location));
+      alias_assertion.instructions.back().source_location.set_comment(
+        "Check compatibility of assigns clause with the called function");
+      goto_function.body.insert_before_swap(instruction_iterator, alias_assertion);
+      ++instruction_iterator;
+    }
+  }
+
+  // Identify the variables to havoc.
   modifiest modifies;
-  get_modifies(local_may_alias, loop, modifies);
 
+  if(assigns.is_not_nil())
+  {
+    // If there is an assigns clause, identify the variables in the assigns clause.
+    for(auto assigns_clause_target : assigns_clause.getTargets()){
+      modifies.insert(assigns_clause_target->get_direct_pointer());
+    }
+  } else
+  {
+    throw std::invalid_argument( "assigns is nil" );
+    // If there is no assigns clause, find out what can get changed in the loop.
+    get_modifies(local_may_alias, loop, modifies);
+  }
+  
   // build the havocking code
   goto_programt havoc_code;
+  build_havoc_code(loop_head, modifies, havoc_code);
+
+  // Insert assertions at assignment
+  // check_frame_conditions(havoc_code, ns.lookup(function_name));
 
   // process quantified variables correctly (introduce a fresh temporary)
   // and return a copy of the invariant
@@ -135,6 +183,7 @@ void code_contractst::check_apply_loop_contracts(
     replace(invariant_copy);
     return invariant_copy;
   };
+  
 
   // Generate: assert(invariant) just before the loop
   // We use a block scope to create a temporary assertion,
@@ -147,9 +196,6 @@ void code_contractst::check_apply_loop_contracts(
       "Check loop invariant before entry");
   }
 
-  // havoc variables being written to
-  build_havoc_code(loop_head, modifies, havoc_code);
-
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,
   // and immediately convert it to goto instructions.