CONTRACTS: track multiple malloc'd regions

For malloc we were fetching the address range from the
malloc_return_value which is a unique global variable.  As a result we
would only track a single malloc'd location at a time.
we now track a list of objects, from all occurrences of the variable.

Author: Remi Delmas

regression/contracts/assigns_enforce_malloc_03/main.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+void foo() __CPROVER_assigns()
+{
+  char *loc1 = malloc(1);
+  char *loc2 = malloc(1);
+  int c;
+  if(c)
+    *loc1 = 0;
+  else
+    *loc2 = 0;
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts/assigns_enforce_malloc_03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-contract foo
+^\[foo.assigns.\d+\].* Check that \*loc1 is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that \*loc2 is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Checks that multiple malloc'd objects are tracked by assigns clause checking.

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

@@ -48,8 +48,8 @@ void havoc_assigns_clause_targetst::get_instructions(goto_programt &dest)
   for(const auto &pair : from_stack_alloc)
     havoc_if_valid(pair.second, havoc_program);
 
-  for(const auto &pair : from_heap_alloc)
-    havoc_if_valid(pair.second, havoc_program);
+  for(const auto &car : from_heap_alloc)
+    havoc_if_valid(car, havoc_program);
 
   for(const auto &pair : from_static_local)
   {

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -131,7 +131,14 @@ void instrument_spec_assignst::track_heap_allocated(
   const exprt &expr,
   goto_programt &dest)
 {
-  create_snapshot(create_car_from_heap_alloc(expr), dest);
+  // insert in tracking set
+  const auto &car = create_car_from_heap_alloc(expr);
+
+  // generate target validity check for this target.
+  target_validity_assertion(car, true, dest);
+
+  // generate snapshot instructions for this target.
+  create_snapshot(car, dest);
 }
 
 void instrument_spec_assignst::check_inclusion_assignment(
@@ -416,7 +423,7 @@ void instrument_spec_assignst::track_spec_target_group(
   cleanert cleaner(st, log.get_message_handler());
   exprt condition(group.condition());
   if(has_subexpr(condition, ID_side_effect))
-    cleaner.clean(condition, dest, st.lookup_ref(function_id).mode);
+    cleaner.clean(condition, dest, mode);
 
   // create conditional address ranges by distributing the condition
   for(const auto &target : group.targets())
@@ -451,8 +458,7 @@ const symbolt instrument_spec_assignst::create_fresh_symbol(
   const typet &type,
   const source_locationt &location) const
 {
-  return new_tmp_symbol(
-    type, location, st.lookup_ref(function_id).mode, st, suffix);
+  return new_tmp_symbol(type, location, mode, st, suffix);
 }
 
 car_exprt instrument_spec_assignst::create_car_expr(
@@ -714,12 +720,25 @@ exprt instrument_spec_assignst::inclusion_check_full(
 
   // Build a disjunction over all tracked locations
   exprt::operandst disjuncts;
+  log.debug() << LOG_HEADER << " inclusion check: \n"
+              << from_expr_using_mode(ns, mode, car.target()) << " in {"
+              << messaget::eom;
 
   for(const auto &pair : from_spec_assigns)
+  {
     disjuncts.push_back(inclusion_check_single(car, pair.second));
+    log.debug() << "\t(spec) "
+                << from_expr_using_mode(ns, mode, pair.second.target())
+                << messaget::eom;
+  }
 
-  for(const auto &pair : from_heap_alloc)
-    disjuncts.push_back(inclusion_check_single(car, pair.second));
+  for(const auto &heap_car : from_heap_alloc)
+  {
+    disjuncts.push_back(inclusion_check_single(car, heap_car));
+    log.debug() << "\t(heap) "
+                << from_expr_using_mode(ns, mode, heap_car.target())
+                << messaget::eom;
+  }
 
   if(include_stack_allocated)
   {
@@ -732,12 +751,21 @@ exprt instrument_spec_assignst::inclusion_check_full(
         continue;
 
       disjuncts.push_back(inclusion_check_single(car, pair.second));
+      log.debug() << "\t(stack) "
+                  << from_expr_using_mode(ns, mode, pair.second.target())
+                  << messaget::eom;
     }
 
     // static locals are stack allocated and can never be DEAD
     for(const auto &pair : from_static_local)
+    {
       disjuncts.push_back(inclusion_check_single(car, pair.second));
+      log.debug() << "\t(static) "
+                  << from_expr_using_mode(ns, mode, pair.second.target())
+                  << messaget::eom;
+    }
   }
+  log.debug() << "}" << messaget::eom;
 
   if(allow_null_lhs)
     return or_exprt{
@@ -793,21 +821,10 @@ const car_exprt &instrument_spec_assignst::create_car_from_stack_alloc(
 const car_exprt &
 instrument_spec_assignst::create_car_from_heap_alloc(const exprt &target)
 {
-  const auto &found = from_heap_alloc.find(target);
-  if(found != from_heap_alloc.end())
-  {
-    log.warning() << "Ignored duplicate heap-allocated target '"
-                  << from_expr(ns, target.id(), target) << "' at "
-                  << target.source_location().as_string() << messaget::eom;
-    return found->second;
-  }
-  else
-  {
-    log.debug() << LOG_HEADER << "creating CAR for heap-allocated target "
-                << format(target) << messaget::eom;
-    from_heap_alloc.insert({target, create_car_expr(true_exprt{}, target)});
-    return from_heap_alloc.find(target)->second;
-  }
+  log.debug() << LOG_HEADER << "creating CAR for heap-allocated target "
+              << format(target) << messaget::eom;
+  from_heap_alloc.emplace_back(create_car_expr(true_exprt{}, target));
+  return from_heap_alloc.back();
 }
 
 const car_exprt &instrument_spec_assignst::create_car_from_static_local(
@@ -854,8 +871,8 @@ void instrument_spec_assignst::invalidate_heap_and_spec_aliases(
   for(const auto &pair : from_spec_assigns)
     invalidate_car(pair.second, freed_car, dest);
 
-  for(const auto &pair : from_heap_alloc)
-    invalidate_car(pair.second, freed_car, dest);
+  for(const auto &car : from_heap_alloc)
+    invalidate_car(car, freed_car, dest);
 }
 
 /// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented.

src/goto-instrument/contracts/instrument_spec_assigns.h

@@ -209,7 +209,8 @@ class instrument_spec_assignst
       functions(_functions),
       st(_st),
       ns(_st),
-      log(_message_handler)
+      log(_message_handler),
+      mode(st.lookup_ref(function_id).mode)
   {
   }
 
@@ -507,6 +508,9 @@ class instrument_spec_assignst
   /// Logger
   messaget log;
 
+  /// Language mode
+  const irep_idt &mode;
+
   /// Track and generate snaphsot instructions and target validity
   /// checking assertions for a conditional target group from an assigns clause
   void track_spec_target_group(
@@ -655,8 +659,9 @@ class instrument_spec_assignst
   using exprt_to_car_mapt =
     std::unordered_map<const exprt, const car_exprt, irep_hash>;
 
-  /// Map from malloc'd symbols to corresponding conditional address ranges.
-  exprt_to_car_mapt from_heap_alloc;
+  /// List of malloc'd conditional address ranges.
+  using car_expr_listt = std::list<car_exprt>;
+  car_expr_listt from_heap_alloc;
 
   const car_exprt &create_car_from_heap_alloc(const exprt &target);