Improvements to code contracts [depends-on: #2646, #2676, blocks: #2712]

.gitignore

@@ -19,6 +19,8 @@ src/.settings/*
 # Visual Studio
 Debug/*
 Release/*
+#vi(m)
+*.swp
 
 # compilation files
 *.lo
@@ -65,6 +67,8 @@ jbmc/regression/**/tests-symex-driven-loading.log
 
 # files stored by editors
 *~
+.*.swp
+.*.swo
 
 # libs downloaded by make [name]-download
 minisat*/

regression/ansi-c/code_contracts1/main.c

@@ -0,0 +1,17 @@
+int foo()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1})
+{
+  return 1;
+}
+
+int bar()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1} &&
+                  __CPROVER_return_value == 1)
+{
+  return 1;
+}
+
+int main() {
+  foo();
+  bar();
+}

regression/ansi-c/code_contracts1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/contracts/function_apply_01/test.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 main.c
 --apply-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Applying code contracts currently also checks them.

regression/contracts/function_check_01/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/function_check_04/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.assertion.1\] assertion x == 0: SUCCESS$
 ^\[foo.1\] : FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/function_check_05/test.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
 ^\[main.assertion.1\] assertion y == 0: FAILURE$
 ^\[main.assertion.2\] assertion z == 1: SUCCESS$
 ^\[foo.1\] : SUCCESS$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 --
-Contract checking does not properly havoc function calls.

regression/contracts/function_check_mem_01/main.c

@@ -33,7 +33,7 @@ void foo(bar *x)
   __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
 {
   x->x += 1;
-  return
+  return;
 }
 
 int main()

regression/contracts/function_check_mem_01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --check-code-contracts
 ^EXIT=0$

regression/contracts/invar_check_01/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_02/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_03/test.desc

@@ -1,11 +1,8 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/contracts/invar_check_04/test.desc

@@ -1,12 +1,9 @@
 CORE
 main.c
---apply-code-contracts
+--check-code-contracts
 ^\[main.1\] Loop invariant violated before entry: SUCCESS$
 ^\[main.2\] Loop invariant not preserved: SUCCESS$
 ^\[main.assertion.1\] assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
---check-code-contracts not implemented yet.
---apply-code-contracts is the current name for the flag. This should be
-updated as the flag changes.

regression/goto-instrument/slice19/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$

regression/goto-instrument/slice24/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static void f(int *x) { *x = 5; }
+static void g(int *x) { assert(*x == 5); }
+
+int main(int argc, char **argv)
+{
+  int *x = (int*)malloc(sizeof(int));
+  f(x);
+  g(x);
+
+  return 0;
+}

regression/goto-instrument/slice24/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+Data dependencies across function calls are still not working correctly.

src/analyses/dependence_graph.cpp

@@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies(
     {
       bool found=false;
       for(const auto &wr : w_range.second)
+      {
         for(const auto &r_range : r_ranges)
+        {
           if(!found &&
              may_be_def_use_pair(wr.first, wr.second,
                                  r_range.first, r_range.second))
@@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies(
             data_deps.insert(w_range.first);
             found=true;
           }
+        }
+      }
     }
 
     dep_graph.reaching_definitions()[to].clear_cache(it->first);

src/analyses/goto_rw.cpp

@@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
-  if(mode!=get_modet::READ)
-    get_objects_rec(mode, pointer);
 }
 
 void rw_range_sett::get_objects_byte_extract(
@@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id() == ID_string_constant ||
+  if(object.id() == ID_symbol ||
+     object.id() == ID_string_constant ||
      object.id() == ID_label ||
      object.id() == ID_array ||
      object.id() == ID_null_object)
     // constant, nothing to do
+  {
     return;
-  else if(object.id()==ID_symbol)
-    get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_dereference)
+  {
     get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(object);
@@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec(
     get_objects_array(mode, to_array_expr(expr), range_start, size);
   else if(expr.id()==ID_struct)
     get_objects_struct(mode, to_struct_expr(expr), range_start, size);
+  else if(expr.id()==ID_dynamic_object)
+  {
+    const auto obj_instance = to_dynamic_object_expr(expr).get_instance();
+    add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1);
+  }
   else if(expr.id()==ID_symbol)
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
@@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec(
   {
     // dereferencing may yield some weird ones, ignore these
   }
-  else if(mode==get_modet::LHS_W)
-  {
-    forall_operands(it, expr)
-      get_objects_rec(mode, *it);
-  }
   else
     throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
 }
@@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference(
   exprt object=deref;
   dereference(target, object, ns, value_sets);
 
+  PRECONDITION(object.is_not_nil());
+
   range_spect new_size=
     to_range_spect(pointer_offset_bits(object.type(), ns));
 

src/analyses/reaching_definitions.cpp

@@ -307,19 +307,19 @@ void rd_range_domaint::transform_assign(
   {
     const irep_idt &identifier=it->first;
     // ignore symex::invalid_object
-    const symbolt *symbol_ptr;
-    if(ns.lookup(identifier, symbol_ptr))
+    const symbolt *symbol_ptr = nullptr;
+    bool not_found = ns.lookup(identifier, symbol_ptr);
+    if(not_found && has_prefix(id2string(identifier), "symex::invalid_object"))
+    {
       continue;
-    INVARIANT_STRUCTURED(
-      symbol_ptr!=nullptr,
-      nullptr_exceptiont,
-      "Symbol is in symbol table");
+    }
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
     if(is_must_alias &&
        (!rd.get_is_threaded()(from) ||
-        (!symbol_ptr->is_shared() &&
+        (symbol_ptr != nullptr &&
+         symbol_ptr->is_shared() &&
          !rd.get_is_dirty()(identifier))))
       for(const auto &range : ranges)
         kill(identifier, range.first, range.second);

src/ansi-c/c_typecheck_base.cpp

@@ -760,11 +760,15 @@ void c_typecheck_baset::typecheck_declaration(
       typet ret_type=empty_typet();
       if(new_symbol.type.id()==ID_code)
         ret_type=to_code_type(new_symbol.type).return_type();
-      assert(parameter_map.empty());
       if(ret_type.id()!=ID_empty)
+      {
+        DATA_INVARIANT(
+          parameter_map.empty(), "parameter map should be cleared");
         parameter_map["__CPROVER_return_value"]=ret_type;
+      }
       typecheck_spec_expr(contract, ID_C_spec_ensures);
-      parameter_map.clear();
+      if(ret_type.id()!=ID_empty)
+        parameter_map.clear();
 
       if(contract.find(ID_C_spec_requires).is_not_nil())
         new_symbol.type.add(ID_C_spec_requires)=

src/ansi-c/c_typecheck_expr.cpp

@@ -2141,7 +2141,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
+    exprt dynamic_object_expr=exprt(ID_is_dynamic_object, expr.type());
     dynamic_object_expr.operands()=expr.arguments();
     dynamic_object_expr.add_source_location()=source_location;
 

src/ansi-c/expr2c.cpp

@@ -3574,8 +3574,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_invalid_pointer)
     return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
 
-  else if(src.id()==ID_dynamic_object)
-    return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
+  else if(src.id()==ID_is_dynamic_object)
+    return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16);
 
   else if(src.id()=="is_zero_string")
     return convert_function(src, "IS_ZERO_STRING", precedence=16);