Merge pull request #7936 from esteffin/esteffin/pointer-check-for-sm-address

Add --pointer-check for shadow memory address

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/pointer-checks1/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+extern _Bool nondet();
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+
+  char *buffer[10];
+
+  __CPROVER_set_field(&buffer[9], "field1", 1);
+  assert(__CPROVER_get_field(&buffer[9], "field1") == 1);
+  __CPROVER_set_field(&buffer[10], "field1", 1);
+  if(nondet())
+  {
+    assert(__CPROVER_get_field(&buffer[10], "field1") == 1);
+  }
+}

regression/cbmc-shadow-memory/pointer-checks1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--verbosity 10 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 13 dereference failure: pointer outside object bounds.*: FAILURE
+line 16 dereference failure: pointer outside object bounds.*: FAILURE
+--
+^warning: ignoring
+line 11 dereference failure: pointer outside object bounds.*: FAILURE
+line 12 dereference failure: pointer outside object bounds.*: FAILURE

regression/cbmc-shadow-memory/pointer-checks2/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("uninitialized", (char)0);
+
+  char a;
+  int *i = &a;
+
+  __CPROVER_set_field(i, "uninitialized", 1); // should this fail?
+
+  assert(__CPROVER_get_field(&a, "uninitialized") == 1);
+  assert(__CPROVER_get_field(&a + 1, "uninitialized") == 1);
+  assert(__CPROVER_get_field(i, "uninitialized") == 1);
+}

regression/cbmc-shadow-memory/pointer-checks2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--verbosity 10 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 10 dereference failure: pointer outside object bounds in \*i.*: FAILURE
+line 13 dereference failure: pointer outside object bounds in \(&a\).*: FAILURE
+line 14 dereference failure: pointer outside object bounds in \*i.*: FAILURE
+--

src/ansi-c/goto_check_c.cpp

@@ -103,6 +103,8 @@ class goto_check_ct
   using guardt = std::function<exprt(exprt)>;
   const guardt identity = [](exprt expr) { return expr; };
 
+  void check_shadow_memory_api_calls(const goto_programt::instructiont &);
+
   /// Check an address-of expression:
   ///  if it is a dereference then check the pointer
   ///  if it is an index then address-check the array and then check the index
@@ -2142,6 +2144,8 @@ void goto_check_ct::goto_check(
       for(const auto &arg : i.call_arguments())
         check(arg);
 
+      check_shadow_memory_api_calls(i);
+
       // the call might invalidate any assertion
       assertions.clear();
     }
@@ -2243,6 +2247,25 @@ void goto_check_ct::goto_check(
     remove_skip(goto_program);
 }
 
+void goto_check_ct::check_shadow_memory_api_calls(
+  const goto_programt::instructiont &i)
+{
+  if(i.call_function().id() != ID_symbol)
+    return;
+
+  const irep_idt &identifier =
+    to_symbol_expr(i.call_function()).get_identifier();
+
+  if(
+    identifier == CPROVER_PREFIX "get_field" || identifier == CPROVER_PREFIX
+                                                  "set_field")
+  {
+    const exprt &expr = i.call_arguments()[0];
+    PRECONDITION(expr.type().id() == ID_pointer);
+    check(dereference_exprt(expr));
+  }
+}
+
 goto_check_ct::conditionst
 goto_check_ct::get_pointer_points_to_valid_memory_conditions(
   const exprt &address,