Merge pull request #157 from viktormalik/svcomp22-fixes

SV-COMP fixes

regression/kiki/hard2_unwindbound5/main.c

@@ -0,0 +1,61 @@
+/*
+  hardware integer division program, by Manna
+  returns q==A//B
+  */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "hard2.c", 8, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int counter = 0;
+int main() {
+    int A, B;
+    int r, d, p, q;
+    A = __VERIFIER_nondet_int();
+    B = 1;
+
+    r = A;
+    d = B;
+    p = 1;
+    q = 0;
+
+    while (counter++<5) {
+        __VERIFIER_assert(q == 0);
+        __VERIFIER_assert(r == A);
+        __VERIFIER_assert(d == B * p);
+        if (!(r >= d)) break;
+
+        d = 2 * d;
+        p = 2 * p;
+    }
+
+    while (counter++<5) {
+        __VERIFIER_assert(A == q*B + r);
+        __VERIFIER_assert(d == B*p);
+
+        if (!(p != 1)) break;
+
+        d = d / 2;
+        p = p / 2;
+        if (r >= d) {
+            r = r - d;
+            q = q + p;
+        }
+    }
+
+    __VERIFIER_assert(A == d*q + r);
+    __VERIFIER_assert(B == d);
+    return 0;
+}

regression/kiki/hard2_unwindbound5/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--heap --values-refine --k-induction --competition-mode
+^EXIT=10$
+^SIGNAL=0$
+^.*FAILURE$
+--
+--
+This is a past incorrect true benchmark from SV-comp which was caused by a bug
+in SSA unwinder where the generated constraints made the analysis unsound.

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

@@ -22,6 +22,7 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <ansi-c/ansi_c_language.h>
 #include <ansi-c/cprover_library.h>
+#include <ansi-c/gcc_version.h>
 #include <cpp/cpp_language.h>
 
 #include <goto-programs/goto_convert_functions.h>
@@ -396,6 +397,14 @@ int twols_parse_optionst::doit()
 
   register_languages();
 
+  // configure gcc, if required
+  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
+  {
+    gcc_versiont gcc_version;
+    gcc_version.get("gcc");
+    configure_gcc(gcc_version);
+  }
+
   if(get_goto_program(options))
     return 6;
 
@@ -1141,6 +1150,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())