SV-COMP fixes

regression/memsafety/built_from_end/test.desc

@@ -1,35 +1,6 @@
-KNOWNBUG
+CORE
 main.c
 --heap --intervals --pointer-check --no-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
---
-CBMC 5.9 introduced changes to its implementation of some built-in functions,
-the ones affecting this test are malloc and free. Malloc changes have been
-already accounted for in 2LS codebase, however the control flow of free
-is most likely causing problems in this test making one of the asserts fail:
-
-[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN
-
-This may be related to double free assertion, where GOTO changed from:
-
-...
-    IF !(__CPROVER_deallocated == ptr) THEN GOTO 6
-    // 144 file <builtin-library-free> line 18 function free
-    ASSERT 0 != 0 // double free
-    // 145 no location
-    ASSUME 0 != 0
-    // 146 file <builtin-library-free> line 29 function free
- 6: _Bool record;
-...
-
-to:
-    ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free
-
-Note the new ptr == NULL condition, this could be the root cause of
-the problem. However further investigation is required
-and will be done once the CBMC rebase is completed. According to the
-C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't
-seem to handle this case correctly.

regression/memsafety/double_free/main.c

@@ -0,0 +1,9 @@
+void *my_malloc(unsigned int size) {
+    return malloc(size);
+}
+
+int main() {
+    void *a = my_malloc(sizeof(int));
+    free(a);
+    free(a);
+}

regression/memsafety/double_free/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--pointer-check --inline
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[free.precondition.6\] free argument must be NULL or valid pointer: FAILURE

regression/memsafety/simple_true/test.desc

@@ -1,36 +1,6 @@
-KNOWNBUG
+CORE
 main.c
 --heap --intervals --pointer-check --no-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
---
-CBMC 5.9 introduced changes to its implementation of some built-in functions,
-the ones affecting this test are malloc and free. Malloc changes have been
-already accounted for in 2LS codebase, however the control flow of free
-is most likely causing problems in this test making one of the asserts fail:
-
-[main.pointer_dereference.27] dereference failure: deallocated dynamic object in *p: UNKNOWN
-
-This may be related to double free assertion, where GOTO changed from:
-
-...
-    IF !(__CPROVER_deallocated == ptr) THEN GOTO 6
-    // 144 file <builtin-library-free> line 18 function free
-    ASSERT 0 != 0 // double free
-    // 145 no location
-    ASSUME 0 != 0
-    // 146 file <builtin-library-free> line 29 function free
- 6: _Bool record;
-...
-
-to:
-    ASSERT ptr == NULL || __CPROVER_deallocated != ptr // double free
-
-Note the new ptr == NULL condition, this could be the root cause of
-the problem. However further investigation is required
-and will be done once the CBMC rebase is completed. According to the
-C standard, free(NULL) is a valid construct (no operation) but 2LS doesn't
-seem to handle this case correctly.
-

regression/preconditions/precond_contextsensitive1/test.desc

@@ -3,4 +3,4 @@ main.c
 --context-sensitive --preconditions
 ^EXIT=5$
 ^SIGNAL=0$
-^\[sign\]: sign#return_value#phi20 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi20\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$
+^\[sign\]: sign#return_value#phi21 <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)sign#return_value#phi21\) <= 0 ==> x <= 0 && -\(\(signed __CPROVER_bitvector\[33\]\)x\) <= 0$

src/2ls/2ls_parse_options.cpp

@@ -1141,6 +1141,12 @@ bool twols_parse_optionst::process_goto_program(
 
     remove_dead_goto(goto_model);
 
+    // There's a bug in SSA creation that causes problems when a single SKIP
+    // instruction is a target of both a forward and a backward GOTO.
+    // This transformation fixes that by splitting such SKIPs into two.
+    // TODO: fix this properly in SSA, if possible.
+    fix_goto_targets(goto_model);
+
     if(cmdline.isset("competition-mode"))
     {
       limit_array_bounds(goto_model);

src/2ls/2ls_parse_options.h

@@ -197,6 +197,7 @@ class twols_parse_optionst:
   void handle_freed_ptr_compare(goto_modelt &goto_model);
   void assert_no_builtin_functions(goto_modelt &goto_model);
   void assert_no_atexit(goto_modelt &goto_model);
+  void fix_goto_targets(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/preprocessing_util.cpp

@@ -674,7 +674,7 @@ void twols_parse_optionst::limit_array_bounds(goto_modelt &goto_model)
           if(size_expr.id()==ID_constant)
           {
             int size=std::stoi(
-              id2string(to_constant_expr(size_expr).get_value()), nullptr, 2);
+              id2string(to_constant_expr(size_expr).get_value()), nullptr, 16);
             // @TODO temporary solution - there seems to be a bug in the solver
             assert(size<=50000);
           }
@@ -856,3 +856,51 @@ void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model)
     }
   }
 }
+
+/// Searches for SKIP instructions that are a target of both a forward and
+/// a backward GOTO. Such instructions are split into 2 - the first one is
+/// made the target of forward GOTOs and the second one is made the target of
+/// backward GOTOs.
+void twols_parse_optionst::fix_goto_targets(goto_modelt &goto_model)
+{
+  for (auto &f_it : goto_model.goto_functions.function_map)
+  {
+    Forall_goto_program_instructions(i_it, f_it.second.body)
+    {
+      if (i_it->incoming_edges.size() <= 1)
+        continue;
+      if (!i_it->is_skip())
+        continue;
+
+      bool has_backwards_goto = false;
+      bool has_forward_goto = false;
+      for (auto &incoming : i_it->incoming_edges)
+      {
+        if (incoming->location_number < i_it->location_number)
+          has_forward_goto = true;
+        if (incoming->location_number > i_it->location_number)
+          has_backwards_goto = true;
+      }
+      if (has_forward_goto && has_backwards_goto)
+      {
+        auto new_skip = f_it.second.body.insert_after(
+          i_it,
+          goto_programt::make_skip(i_it->source_location));
+
+        for (auto &incoming : i_it->incoming_edges)
+        {
+          if (incoming->location_number > i_it->location_number)
+          {
+            // Redirect backward GOTOs to the new skip
+            for (auto &target : incoming->targets)
+            {
+              if (target == i_it)
+                target = new_skip;
+            }
+          }
+        }
+      }
+    }
+    goto_model.goto_functions.update();
+  }
+}

src/domains/heap_domain.cpp

@@ -216,6 +216,8 @@ const exprt heap_domaint::get_points_to_dest(
 {
   // Value from the solver must be converted into an expression
   exprt ptr_value=value_to_ptr_exprt(solver_value);
+  if(ptr_value.id()==ID_typecast)
+    ptr_value=to_typecast_expr(ptr_value).op();
 
   if((ptr_value.id()==ID_constant &&
       to_constant_expr(ptr_value).get_value()==ID_NULL) ||
@@ -228,18 +230,30 @@ const exprt heap_domaint::get_points_to_dest(
   {
     // Template row pointer points to the heap (p = &obj)
     assert(ptr_value.id()==ID_address_of);
-    if(to_address_of_expr(ptr_value).object().id()!=ID_symbol)
+    exprt obj=to_address_of_expr(ptr_value).object();
+    if(obj.id()==ID_member)
+    {
+      // &(X.field) where field has offset 0 is equal to &X
+      auto &member=to_member_expr(obj);
+      auto field=member.get_component_name();
+      auto struct_type=ns.follow(member.compound().type());
+      if(struct_type.id()==ID_struct &&
+         to_struct_type(struct_type).component_number(field)==0)
+      {
+        obj=member.compound();
+      }
+    }
+    if(obj.id()!=ID_symbol)
     {
       // If solver did not return address of a symbol, it is considered
       // as nondet value.
       return nil_exprt();
     }
 
-    symbol_exprt obj=to_symbol_expr(
-      to_address_of_expr(ptr_value).object());
+    symbol_exprt symbol_obj=to_symbol_expr(obj);
 
-    if(obj.type()!=templ_row_expr.type() &&
-       ns.follow(templ_row_expr.type().subtype())!=ns.follow(obj.type()))
+    if(symbol_obj.type()!=templ_row_expr.type() &&
+       ns.follow(templ_row_expr.type().subtype())!=ns.follow(symbol_obj.type()))
     {
       if(!is_cprover_symbol(templ_row_expr))
       {
@@ -249,7 +263,7 @@ const exprt heap_domaint::get_points_to_dest(
     }
 
     // Add equality p == &obj
-    return std::move(obj);
+    return std::move(symbol_obj);
   }
   else
     return nil_exprt();

src/ssa/dynobj_instance_analysis.cpp

@@ -213,6 +213,7 @@ bool dynobj_instance_domaint::merge(
   trace_ptrt trace_to)
 {
   bool result=has_values.is_false() && !other.has_values.is_false();
+  has_values=tvt::unknown();
   for(auto &obj : other.must_alias_relations)
   {
     if(must_alias_relations.find(obj.first)==must_alias_relations.end())

src/ssa/local_ssa.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/pointer_expr.h>
 #include <util/byte_operators.h>
+#include <util/optional.h>
 #include <solvers/decision_procedure.h>
 
 #include <goto-programs/adjust_float_expressions.h>
@@ -50,6 +51,9 @@ void local_SSAt::build_SSA()
     build_function_call(i_it);
 //    build_unknown_objs(i_it);
     collect_record_frees(i_it);
+
+    if (options.get_bool_option("competition-mode"))
+      disable_unsupported_instructions(i_it);
   }
 
   // collect custom templates in loop heads
@@ -883,17 +887,18 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const
   {
     // If the last definition of an object is at its allocation, we can only use
     // the corresponding symbol if the object has truly been allocated
-    // (allocation guard holds). Otherwise we need to use the last definition
-    // before the allocation.
+    // (allocation guard holds). After the rebase to a newer version of CBMC,
+    // the last definition may also be a PHI node at the end of malloc (
+    // which covers the case-split whether malloc can fail).
+    // Otherwise we need to use the last definition before the allocation.
     auto def_it=ssa_analysis[loc].def_map.find(object.get_identifier());
-    if(def_it!=ssa_analysis[loc].def_map.end() &&
-       def_it->second.def.kind==ssa_domaint::deft::ALLOCATION)
+    auto maybe_alloc_def=get_recent_object_alloc_def(loc, def_it);
+    if(maybe_alloc_def.has_value())
     {
-      locationt alloc_loc=def_it->second.def.loc;
       return if_exprt(
-        read_rhs(def_it->second.def.guard, alloc_loc),
+        read_rhs(maybe_alloc_def->guard, maybe_alloc_def->loc),
         read_rhs(object, loc),
-        read_rhs(object, alloc_loc));
+        read_rhs(object, maybe_alloc_def->loc));
     }
     else
       return read_rhs(object, loc);
@@ -904,6 +909,32 @@ exprt local_SSAt::read_rhs_rec(const exprt &expr, locationt loc) const
   }
 }
 
+/// Checks whether the last definition of the object is its allocation and
+/// if so, return the allocation def. Otherwise returns nullopt.
+optionalt<ssa_domaint::deft> local_SSAt::get_recent_object_alloc_def(
+  locationt loc,
+  const ssa_domaint::def_mapt::const_iterator &def) const
+{
+  if(def==ssa_analysis[loc].def_map.end())
+    return nullopt;
+
+  if(def->second.def.is_allocation())
+    return def->second.def;
+
+  // Not a direct allocation, follow the split if it is a phi node and add
+  // guard if at least one of the branches is an allocation.
+  if(def->second.def.is_phi())
+  {
+    const auto &phi_branches=
+      ssa_analysis[def->second.def.loc].phi_nodes.find(def->first);
+    if(phi_branches!=ssa_analysis[def->second.def.loc].phi_nodes.end())
+      for(const auto &phi_branch : phi_branches->second)
+        if(phi_branch.second.is_allocation())
+          return phi_branch.second;
+  }
+  return nullopt;
+}
+
 void local_SSAt::replace_side_effects_rec(
   exprt &expr, locationt loc, unsigned &counter) const
 {
@@ -1110,40 +1141,8 @@ void local_SSAt::assign_rec(
   {
     const if_exprt &if_expr=to_if_expr(lhs);
 
-    exprt::operandst other_cond_conj;
-    if(if_expr.true_case().get_bool("#heap_access") &&
-       if_expr.cond().id()==ID_equal)
-    {
-      const exprt heap_object=if_expr.true_case();
-      const ssa_objectt ptr_object(to_equal_expr(if_expr.cond()).lhs(), ns);
-      if(ptr_object)
-      {
-        const irep_idt ptr_id=ptr_object.get_identifier();
-        const exprt cond=read_rhs(if_expr.cond(), loc);
-
-        for(const dyn_obj_assignt &do_assign : dyn_obj_assigns[heap_object])
-        {
-          if(!alias_analysis[loc].aliases.same_set(
-            ptr_id, do_assign.pointer_id))
-          {
-            other_cond_conj.push_back(do_assign.cond);
-          }
-        }
-
-        dyn_obj_assigns[heap_object].emplace_back(ptr_id, cond);
-      }
-    }
-
-    exprt cond=if_expr.cond();
-    if(!other_cond_conj.empty())
-    {
-      const exprt other_cond=or_exprt(
-        not_exprt(conjunction(other_cond_conj)),
-        name(guard_symbol(), OBJECT_SELECT, loc));
-      cond=and_exprt(cond, other_cond);
-    }
     exprt orig_rhs=fresh_rhs ? name(ssa_objectt(rhs, ns), OUT, loc) : rhs;
-    exprt new_rhs=if_exprt(cond, orig_rhs, if_expr.true_case());
+    exprt new_rhs=if_exprt(if_expr.cond(), orig_rhs, if_expr.true_case());
     assign_rec(
       if_expr.true_case(),
       new_rhs,
@@ -1545,10 +1544,10 @@ void local_SSAt::collect_allocation_guards(
 
 void local_SSAt::collect_record_frees(local_SSAt::locationt loc)
 {
-  if(loc->is_decl())
+  if(loc->is_assign())
   {
-    const code_declt &code_decl=code_declt{loc->decl_symbol()};
-    const exprt &symbol=code_decl.symbol();
+    const code_assignt &code_assign=to_code_assign(loc->get_code());
+    const exprt &symbol=code_assign.lhs();
     if(symbol.id()!=ID_symbol)
       return;
 
@@ -1648,3 +1647,13 @@ bool local_SSAt::can_reuse_symderef(
 
   return true;
 }
+
+void local_SSAt::disable_unsupported_instructions(locationt loc)
+{
+  if (loc->is_other())
+  {
+    auto st = loc->get_code().get_statement();
+    if(st=="array_copy" || st=="array_replace")
+      assert(false);
+  }
+}