Patch set for SV-COMP'19 [depends-on: #2000, #3462]

regression/cbmc/Local_out_of_scope4/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int *p = 0;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    {
+      int x = 42;
+      p = &x;
+      *p = 1;
+    }
+  }
+
+  return 0;
+}

regression/cbmc/Local_out_of_scope4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Memory_leak_abort/main.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  if(*p == 0)
+    abort();
+  if(*p == 1)
+    exit(1);
+  if(*p == 2)
+    _Exit(1);
+  if(*p == 3)
+    __VERIFIER_error();
+  free(p);
+  return 0;
+}

regression/cbmc/Memory_leak_abort/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--memory-leak-check --no-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+_Exit\.memory-leak\.1.*FAILURE
+__CPROVER__start\.memory-leak\.1.*SUCCESS
+abort\.memory-leak\.1.*FAILURE
+exit\.memory-leak\.1.*FAILURE
+main\.memory-leak\.1.*FAILURE
+--
+main\.assertion\.1.*FAILURE
+^warning: ignoring

regression/cbmc/alloca1/main.c

@@ -0,0 +1,8 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = alloca(sizeof(int));
+  *p = 42;
+  free(p);
+}

regression/cbmc/alloca1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+free called for stack-allocated object: FAILURE$
+^\*\* 1 of 12 failed
+--
+^warning: ignoring

regression/cbmc/graphml_witness1/test.desc

@@ -7,34 +7,21 @@ main.c
 <graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
   <key attr.name="invariant" attr.type="string" for="node" id="invariant"/>
   <key attr.name="invariant.scope" attr.type="string" for="node" id="invariant.scope"/>
-  <key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
-    <default>path</default>
-  </key>
-  <key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
-    <default>false</default>
-  </key>
   <key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
     <default>false</default>
   </key>
   <key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
     <default>false</default>
   </key>
-  <key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
-    <default>false</default>
-  </key>
   <key attr.name="enterLoopHead" attr.type="boolean" for="edge" id="enterLoopHead">
     <default>false</default>
   </key>
-  <key attr.name="threadNumber" attr.type="int" for="node" id="thread">
-    <default>0</default>
-  </key>
   <key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
   <key attr.name="programFile" attr.type="string" for="graph" id="programfile"/>
   <key attr.name="programHash" attr.type="string" for="graph" id="programhash"/>
   <key attr.name="specification" attr.type="string" for="graph" id="specification"/>
   <key attr.name="architecture" attr.type="string" for="graph" id="architecture"/>
   <key attr.name="producer" attr.type="string" for="graph" id="producer"/>
-  <key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
   <key attr.name="startline" attr.type="int" for="edge" id="startline"/>
   <key attr.name="control" attr.type="string" for="edge" id="control"/>
   <key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
@@ -45,7 +32,6 @@ main.c
   <key attr.name="witness-type" attr.type="string" for="graph" id="witness-type"/>
   <graph edgedefault="directed">
     <data key="sourcecodelang">C</data>
-    <node id="sink"/>
     <node id="[0-9\.]*">
       <data key="entry">true</data>
     </node>
@@ -68,10 +54,6 @@ main.c
     <node id="[0-9\.]*">
       <data key="violation">true</data>
     </node>
-    <edge source="[0-9\.]*" target="sink">
-      <data key="originfile">main.c</data>
-      <data key="startline">31</data>
-    </edge>
   </graph>
 </graphml>
 --

regression/goto-analyzer/constant_propagation_01/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring

regression/goto-analyzer/constant_propagation_02/test.desc

@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
 --
 ^warning: ignoring

regression/goto-instrument/print_global_state_size1/main.c

@@ -3,7 +3,7 @@
 uint32_t some_global_var;
 int8_t other_global_var;
 
-int main(int argc, char *argv[])
+int main()
 {
   return 0;
 }

scripts/delete_failing_smt2_solver_tests

@@ -53,6 +53,7 @@ rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
+rm Memory_leak_abort/test.desc
 rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
 rm Multi_Dimensional_Array3/test.desc

src/analyses/goto_check.cpp

@@ -103,6 +103,7 @@ class goto_checkt
 
   void bounds_check(const index_exprt &, const guardt &);
   void div_by_zero_check(const div_exprt &, const guardt &);
+  void memory_leak_check(const irep_idt &function_id);
   void mod_by_zero_check(const mod_exprt &, const guardt &);
   void undefined_shift_check(const shift_exprt &, const guardt &);
   void pointer_rel_check(const exprt &, const guardt &);
@@ -1515,6 +1516,30 @@ void goto_checkt::rw_ok_check(exprt &expr)
   }
 }
 
+void goto_checkt::memory_leak_check(const irep_idt &function_id)
+{
+  const symbolt &leak = ns.lookup(CPROVER_PREFIX "memory_leak");
+  const symbol_exprt leak_expr = leak.symbol_expr();
+
+  // add self-assignment to get helpful counterexample output
+  goto_programt::targett t = new_code.add_instruction();
+  t->make_assignment();
+  t->code = code_assignt(leak_expr, leak_expr);
+
+  source_locationt source_location;
+  source_location.set_function(function_id);
+
+  equal_exprt eq(leak_expr, null_pointer_exprt(to_pointer_type(leak.type)));
+
+  add_guarded_claim(
+    eq,
+    "dynamically allocated memory never freed",
+    "memory-leak",
+    source_location,
+    eq,
+    guardt());
+}
+
 void goto_checkt::goto_check(
   goto_functiont &goto_function,
   const irep_idt &_mode)
@@ -1678,6 +1703,16 @@ void goto_checkt::goto_check(
     }
     else if(i.is_assume())
     {
+      // These are further 'exit points' of the program
+      const exprt simplified_guard = simplify_expr(i.guard, ns);
+      if(
+        enable_memory_leak_check && simplified_guard.is_false() &&
+        (i.function == "abort" || i.function == "exit" ||
+         i.function == "_Exit" ||
+         (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort")))
+      {
+        memory_leak_check(i.function);
+      }
       if(!enable_assumptions)
       {
         i.make_skip();
@@ -1711,32 +1746,41 @@ void goto_checkt::goto_check(
         }
       }
     }
-    else if(i.is_end_function())
+    else if(i.is_decl())
     {
-      if(i.function==goto_functionst::entry_point() &&
-         enable_memory_leak_check)
+      if(enable_pointer_check)
       {
-        const symbolt &leak=ns.lookup(CPROVER_PREFIX "memory_leak");
-        const symbol_exprt leak_expr=leak.symbol_expr();
-
-        // add self-assignment to get helpful counterexample output
-        goto_programt::targett t=new_code.add_instruction();
-        t->make_assignment();
-        t->code=code_assignt(leak_expr, leak_expr);
-
-        source_locationt source_location;
-        source_location.set_function(i.function);
+        assert(i.code.operands().size()==1);
+        const symbol_exprt &variable=to_symbol_expr(i.code.op0());
 
-        equal_exprt eq(
-          leak_expr,
-          null_pointer_exprt(to_pointer_type(leak.type)));
-        add_guarded_claim(
-          eq,
-          "dynamically allocated memory never freed",
-          "memory-leak",
-          source_location,
-          eq,
-          guardt());
+        // is it dirty?
+        if(local_bitvector_analysis->dirty(variable))
+        {
+          // reset the dead marker
+          goto_programt::targett t=new_code.add_instruction(ASSIGN);
+          exprt address_of_expr=address_of_exprt(variable);
+          exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
+          if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
+            address_of_expr.make_typecast(lhs.type());
+          exprt rhs=
+            if_exprt(
+              equal_exprt(lhs, address_of_expr),
+              null_pointer_exprt(to_pointer_type(address_of_expr.type())),
+              lhs,
+              lhs.type());
+          t->source_location=i.source_location;
+          t->code=code_assignt(lhs, rhs);
+          t->code.add_source_location()=i.source_location;
+        }
+      }
+    }
+    else if(i.is_end_function())
+    {
+      if(
+        i.function == goto_functionst::entry_point() &&
+        enable_memory_leak_check)
+      {
+        memory_leak_check(i.function);
       }
     }
 

src/ansi-c/ansi_c_internal_additions.cpp

@@ -136,6 +136,12 @@ void ansi_c_internal_additions(std::string &code)
     CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
       CPROVER_PREFIX "constant_infinity_uint];\n"
     "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
+    CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys["
+      CPROVER_PREFIX "constant_infinity_uint];\n"
+    CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors["
+      CPROVER_PREFIX "constant_infinity_uint])(void *);\n"
+    CPROVER_PREFIX "thread_local unsigned long "
+      CPROVER_PREFIX "next_thread_key = 0;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
@@ -148,6 +154,7 @@ void ansi_c_internal_additions(std::string &code)
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
+    "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

src/ansi-c/c_typecheck_argc_argv.cpp

@@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argc_symbol.type=op0.type();
     argc_symbol.is_static_lifetime=true;
     argc_symbol.is_lvalue=true;
+    argc_symbol.value = side_effect_expr_nondett(op0.type());
 
     if(argc_symbol.type.id()!=ID_signedbv &&
        argc_symbol.type.id()!=ID_unsignedbv)
@@ -81,6 +82,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     argv_symbol.type=argv_type;
     argv_symbol.is_static_lifetime=true;
     argv_symbol.is_lvalue=true;
+    argv_symbol.value = side_effect_expr_nondett(argv_type);
 
     symbolt *argv_new_symbol;
     move_symbol(argv_symbol, argv_new_symbol);
@@ -99,6 +101,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
     envp_size_symbol.name="envp_size'";
     envp_size_symbol.type=op0.type(); // same type as argc!
     envp_size_symbol.is_static_lifetime=true;
+    envp_size_symbol.value = side_effect_expr_nondett(op0.type());
     move_symbol(envp_size_symbol, envp_new_size_symbol);
 
     if(envp_symbol.type.id()!=ID_pointer)
@@ -113,6 +116,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
 
     envp_symbol.type.id(ID_array);
     envp_symbol.type.add(ID_size).swap(size_expr);
+    envp_symbol.value = side_effect_expr_nondett(envp_symbol.type);
 
     symbolt *envp_new_symbol;
     move_symbol(envp_symbol, envp_new_symbol);

src/ansi-c/expr2c.cpp

@@ -39,7 +39,8 @@ expr2c_configurationt expr2c_configurationt::default_configuration
   true,
   true,
   "TRUE",
-  "FALSE"
+  "FALSE",
+  "NULL"
 };
 
 expr2c_configurationt expr2c_configurationt::clean_configuration
@@ -48,6 +49,7 @@ expr2c_configurationt expr2c_configurationt::clean_configuration
   false,
   false,
   "1",
+  "0",
   "0"
 };
 
@@ -715,6 +717,7 @@ std::string expr2ct::convert_struct_type(
   if(tag!="")
     dest+=" "+id2string(tag);
 
+#if 0
   if(inc_struct_body)
   {
     dest+=" {";
@@ -737,6 +740,7 @@ std::string expr2ct::convert_struct_type(
 
     dest+=" }";
   }
+#endif
 
   dest+=declarator;
 
@@ -1970,14 +1974,14 @@ std::string expr2ct::convert_constant(
   {
     if(value==ID_NULL)
     {
-      dest="NULL";
+      dest = configuration.null_pointer_string;
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }
     else if(value==std::string(value.size(), '0') &&
             config.ansi_c.NULL_is_zero)
     {
-      dest="NULL";
+      dest = configuration.null_pointer_string;
       if(type.subtype().id()!=ID_empty)
         dest="(("+convert(type)+")"+dest+")";
     }