Simplifies assigns clause implementation

No need to track write set with temporary variables.
This also avoids reporting NULL dereferences when users
adds targets that might be NULL in the assigns clause.

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_structs_07/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+struct pair
+{
+  uint8_t *buf;
+  size_t size;
+};
+
+struct pair_of_pairs
+{
+  struct pair *p;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
+{
+  p->buf[0] = 0;
+}
+
+void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
+{
+  pp->p->buf[0] = 0;
+}
+
+int main()
+{
+  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  f1(p);
+  struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  f2(pp);
+
+  return 0;
+}

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts _ --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure\: pointer NULL in p\-\>buf\: FAILURE$
+^\[f2.\d+\] line \d+ Check that pp\-\>p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure\: pointer NULL in pp\-\>p\-\>buf\: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from invalid objects. In this case, they are not writable.

regression/contracts/assigns_replace_07/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+struct pair
+{
+  uint8_t *buf;
+  size_t size;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
+  __CPROVER_ensures(p->buf[0] == 0)
+{
+  p->buf[0] = 0;
+}
+
+int main()
+{
+  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  f1(p);
+  assert(p != NULL == > p->buf[0] == 0);
+
+  return 0;
+}

regression/contracts/assigns_replace_07/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts _ --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure\: pointer NULL in p\-\>buf\: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=\> p\-\>buf\[0\] \=\= 0\: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from invalid objects. In this case, they are not writable.

src/goto-instrument/contracts/assigns.cpp

@@ -24,49 +24,30 @@ assigns_clause_targett::assigns_clause_targett(
   code_contractst &contract,
   messaget &log_parameter,
   const irep_idt &function_id)
-  : pointer_object(pointer_for(object)),
-    contract(contract),
+  : contract(contract),
     init_block(),
     log(log_parameter),
-    target(typet()),
+    target(pointer_for(object)),
     target_id(object.id())
 {
   INVARIANT(
-    pointer_object.type().id() == ID_pointer,
+    target.type().id() == ID_pointer,
     "Assigns clause targets should be stored as pointer expressions.");
-  const symbolt &function_symbol = contract.ns.lookup(function_id);
-
-  // Declare a new symbol to stand in for the reference
-  symbolt standin_symbol = contract.new_tmp_symbol(
-    pointer_object.type(),
-    function_symbol.location,
-    function_symbol.mode);
-
-  target = standin_symbol.symbol_expr();
-
-  // Build standin variable initialization block
-  init_block.add(goto_programt::make_decl(target, function_symbol.location));
-  init_block.add(goto_programt::make_assignment(
-    code_assignt(target, pointer_object), function_symbol.location));
 }
 
 assigns_clause_targett::~assigns_clause_targett()
 {
 }
 
-std::vector<symbol_exprt> assigns_clause_targett::temporary_declarations() const
-{
-  std::vector<symbol_exprt> result;
-  result.push_back(target);
-  return result;
-}
-
 exprt assigns_clause_targett::alias_expression(const exprt &lhs)
 {
   exprt::operandst condition;
   exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object()
                                               : pointer_for(lhs);
 
+  // NULL targets aren't writable
+  condition.push_back(not_exprt(null_pointer(target)));
+
   // __CPROVER_same_object(lhs, target)
   condition.push_back(same_object(lhs_ptr, target));
 
@@ -103,17 +84,12 @@ exprt assigns_clause_targett::alias_expression(const exprt &lhs)
 exprt assigns_clause_targett::compatible_expression(
   const assigns_clause_targett &called_target)
 {
-  return same_object(called_target.get_direct_pointer(), target);
-}
-
-const exprt &assigns_clause_targett::get_direct_pointer() const
-{
-  return pointer_object;
+  return same_object(called_target.get_target(), target);
 }
 
-goto_programt &assigns_clause_targett::get_init_block()
+const exprt &assigns_clause_targett::get_target() const
 {
-  return init_block;
+  return target;
 }
 
 assigns_clauset::assigns_clauset(
@@ -140,7 +116,7 @@ assigns_clauset::~assigns_clauset()
   }
 }
 
-assigns_clause_targett *assigns_clauset::add_target(exprt target)
+void assigns_clauset::add_target(exprt target)
 {
   assigns_clause_targett *new_target = new assigns_clause_targett(
     (target.id() == ID_address_of)
@@ -150,42 +126,13 @@ assigns_clause_targett *assigns_clauset::add_target(exprt target)
     log,
     function_id);
   targets.push_back(new_target);
-  return new_target;
-}
-
-goto_programt assigns_clauset::init_block()
-{
-  goto_programt result;
-  for(assigns_clause_targett *target : targets)
-  {
-    for(goto_programt::instructiont inst :
-        target->get_init_block().instructions)
-    {
-      result.add(goto_programt::instructiont(inst));
-    }
-  }
-  return result;
-}
-
-goto_programt assigns_clauset::dead_stmts()
-{
-  goto_programt dead_statements;
-  for(assigns_clause_targett *target : targets)
-  {
-    for(symbol_exprt symbol : target->temporary_declarations())
-    {
-      dead_statements.add(
-        goto_programt::make_dead(symbol, symbol.source_location()));
-    }
-  }
-  return dead_statements;
 }
 
 goto_programt assigns_clauset::havoc_code()
 {
   modifiest modifies;
   for(const auto &t : targets)
-    modifies.insert(to_address_of_expr(t->get_direct_pointer()).object());
+    modifies.insert(to_address_of_expr(t->get_target()).object());
 
   goto_programt havoc_statements;
   append_havoc_code(assigns.source_location(), modifies, havoc_statements);
@@ -231,7 +178,7 @@ exprt assigns_clauset::compatible_expression(
 
         // Validating the called target through __CPROVER_w_ok() is
         // only useful when the called target is a dereference
-        const auto &called_target_ptr = called_target->get_direct_pointer();
+        const auto &called_target_ptr = called_target->get_target();
         if(
           to_address_of_expr(called_target_ptr).object().id() == ID_dereference)
         {

src/goto-instrument/contracts/assigns.h

@@ -29,23 +29,20 @@ class assigns_clause_targett
     const irep_idt &function_id);
   ~assigns_clause_targett();
 
-  std::vector<symbol_exprt> temporary_declarations() const;
   exprt alias_expression(const exprt &lhs);
   exprt compatible_expression(const assigns_clause_targett &called_target);
-  const exprt &get_direct_pointer() const;
-  goto_programt &get_init_block();
+  const exprt &get_target() const;
 
   static exprt pointer_for(const exprt &object)
   {
     return address_of_exprt(object);
   }
 
 protected:
-  const exprt pointer_object;
   const code_contractst &contract;
   goto_programt init_block;
   messaget &log;
-  symbol_exprt target;
+  exprt target;
   const irep_idt &target_id;
 };
 
@@ -59,9 +56,7 @@ class assigns_clauset
     messaget log_parameter);
   ~assigns_clauset();
 
-  assigns_clause_targett *add_target(exprt target);
-  goto_programt init_block();
-  goto_programt dead_stmts();
+  void add_target(exprt target);
   goto_programt havoc_code();
   exprt alias_expression(const exprt &lhs);
   exprt compatible_expression(const assigns_clauset &called_assigns);

src/goto-instrument/contracts/contracts.cpp

@@ -750,11 +750,7 @@ void code_contractst::instrument_call_statement(
       typet cast_type = rhs.type();
 
       // Make freshly allocated memory assignable, if we can determine its type.
-      assigns_clause_targett *new_target =
-        assigns_clause.add_target(dereference_exprt(rhs));
-      goto_programt &pointer_capture = new_target->get_init_block();
-      insert_before_swap_and_advance(
-        program, instruction_iterator, pointer_capture);
+      assigns_clause.add_target(dereference_exprt(rhs));
     }
     return; // assume malloc edits no pre-existing memory objects.
   }
@@ -895,7 +891,12 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     return true;
   }
   goto_programt &program = old_function->second.body;
-  if(program.instructions.empty()) // empty function body
+
+  if(
+    program.empty() ||
+    (program.instructions.size() <= 2 &&
+     program.instructions.front().is_skip() &&
+     program.instructions.back().is_end_function())) // empty function body
   {
     return false;
   }
@@ -923,33 +924,17 @@ void code_contractst::check_frame_conditions(
   // Create a list of variables that are okay to assign.
   std::set<irep_idt> freely_assignable_symbols;
 
-  // Create temporary variables to hold the assigns
-  // clause targets before they can be modified.
-  goto_programt standin_decls = assigns.init_block();
-  // Create dead statements for temporary variables
-  goto_programt mark_dead = assigns.dead_stmts();
-
-  // Skip lines with temporary variable declarations
-  auto instruction_it = program.instructions.begin();
-  insert_before_swap_and_advance(program, instruction_it, standin_decls);
-
-  for(; instruction_it != program.instructions.end(); ++instruction_it)
+  for(auto instruction_it = program.instructions.begin();
+      instruction_it != program.instructions.end();
+      ++instruction_it)
   {
     if(instruction_it->is_decl())
     {
       // Local variables are always freely assignable
       freely_assignable_symbols.insert(
         instruction_it->get_decl().symbol().get_identifier());
 
-      assigns_clause_targett *new_target =
-        assigns.add_target(instruction_it->get_decl().symbol());
-      goto_programt &pointer_capture = new_target->get_init_block();
-
-      for(auto in : pointer_capture.instructions)
-      {
-        program.insert_after(instruction_it, in);
-        ++instruction_it;
-      }
+      assigns.add_target(instruction_it->get_decl().symbol());
     }
     else if(instruction_it->is_assign())
     {
@@ -970,15 +955,6 @@ void code_contractst::check_frame_conditions(
         assigns);
     }
   }
-
-  // Walk the iterator back to the last statement
-  while(!instruction_it->is_end_function())
-  {
-    --instruction_it;
-  }
-
-  // Make sure the temporary symbols are marked dead
-  program.insert_before_swap(instruction_it, mark_dead);
 }
 
 bool code_contractst::enforce_contract(const irep_idt &function)