Add --expand-pointer-predicates to goto-instrument

regression/contracts/argument_sanity/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int *r;
+  __CPROVER_points_to_valid_memory(r, "huh?");
+}

regression/contracts/argument_sanity/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=1$
+^SIGNAL=0$
+^main.c:\d+:\d+: error: size argument to points_to_valid_memory must be coercible to size_t$
+^CONVERSION ERROR$
+--
+--

regression/goto-instrument/expand-pointer-predicates1/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates1/test.desc

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

regression/goto-instrument/expand-pointer-predicates2/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  *x = 1;
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates2/test.desc

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

regression/goto-instrument/expand-pointer-predicates3/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, sizeof(int)));
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x, sizeof(int)), "Assert matches assume");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates3/test.desc

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

regression/goto-instrument/expand-pointer-predicates4/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  int *y = &x;
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(y), "Assert works on &");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates4/test.desc

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

regression/goto-instrument/expand-pointer-predicates5/main.c

@@ -0,0 +1,19 @@
+struct bar
+{
+  int w;
+  int x;
+  int y;
+  int z;
+};
+
+int main()
+{
+  struct bar s;
+  s.z = 5;
+  int *x_pointer = &(s.x);
+  __CPROVER_assert(
+    __CPROVER_points_to_valid_memory(x_pointer, 3 * sizeof(int)),
+    "Variable length assert");
+  assert(x_pointer[2] == 5);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates5/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] line \d+ Variable length assert: SUCCESS$
+^\[main.assertion.2\] line \d+ assertion x_pointer\[\(signed long( long)? int\)2\] == 5: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates6/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field1;
+  int *field2;
+};
+
+void example(struct my_struct *s)
+{
+  s->field2 = malloc(sizeof(*(s->field2)));
+}
+
+int main()
+{
+  struct my_struct *s;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  example(s);
+  __CPROVER_assert(__CPROVER_points_to_valid_memory(s->field2), "");
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates6/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.assertion.1\] line \d+ assertion: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/goto-instrument/expand-pointer-predicates7/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+struct my_struct
+{
+  int *field;
+};
+
+void example(struct my_struct *s)
+{
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s));
+  size_t size;
+  __CPROVER_assume(size == sizeof(*(s->field)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(s->field, size));
+  int read = *(s->field);
+}
+
+int main()
+{
+  struct my_struct *s;
+  example(s);
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates7/test.desc

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

regression/goto-instrument/expand-pointer-predicates8/main.c

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *x;
+  int *y;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x, 2 * sizeof(int)));
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(y, 2 * sizeof(int) - 1));
+  (void)(x[0]);  // Should succeed
+  (void)(x[1]);  // Should succeed
+  (void)(x[2]);  // Should fail
+  (void)(x[-1]); // Should fail
+  (void)(y[0]);  // Should succeed
+  (void)(y[1]);  // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates8/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)1\]: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

regression/goto-instrument/expand-pointer-predicates9/main.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+int main()
+{
+  char *x;
+  __CPROVER_assume(__CPROVER_points_to_valid_memory(x));
+  (void)(*x);       // Should succeed
+  (void)(*(x + 1)); // Should fail
+  (void)(*(x - 1)); // Should fail
+  return 0;
+}

regression/goto-instrument/expand-pointer-predicates9/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check --expand-pointer-predicates
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] line \d+ dereference failure: pointer outside object bounds in \*\(x - \(signed long( long)? int\)1\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

src/ansi-c/c_typecheck_expr.cpp

@@ -34,6 +34,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "anonymous_member.h"
 #include "padding.h"
 
+bool is_lvalue(const exprt &expr);
+
 void c_typecheck_baset::typecheck_expr(exprt &expr)
 {
   if(expr.id()==ID_already_typechecked)
@@ -2109,6 +2111,63 @@ exprt c_typecheck_baset::do_special_functions(
 
     return same_object_expr;
   }
+  else if(identifier == CPROVER_PREFIX "points_to_valid_memory")
+  {
+    if(expr.arguments().size() != 2 && expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "points_to_valid_memory expects one or two operands" << eom;
+      throw 0;
+    }
+    if(!is_lvalue(expr.arguments().front()))
+    {
+      error().source_location = f_op.source_location();
+      error() << "ptr argument to points_to_valid_memory"
+              << " must be an lvalue" << eom;
+      throw 0;
+    }
+
+    exprt same_object_expr;
+    if(expr.arguments().size() == 2)
+    {
+      if(
+        expr.arguments()[1].type().id() != ID_unsignedbv &&
+        expr.arguments()[1].type().id() != ID_signedbv)
+      {
+        error().source_location = f_op.source_location();
+        error() << "size argument to points_to_valid_memory"
+                << " must be coercible to size_t" << eom;
+        throw 0;
+      }
+      same_object_expr =
+        points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]);
+    }
+    else if(expr.arguments().size() == 1)
+    {
+      PRECONDITION(expr.arguments()[0].type().id() == ID_pointer);
+
+      const typet &base_type = expr.arguments()[0].type().subtype();
+      auto expr_size = size_of_expr(base_type, *this);
+      if(!expr_size)
+      {
+        error().source_location = expr.source_location();
+        error() << "cannot determine size of pointed-to memory region" << eom;
+        throw 0;
+      }
+
+      expr_size->add(ID_C_c_sizeof_type) = base_type;
+
+      same_object_expr =
+        points_to_valid_memory(expr.arguments()[0], *expr_size);
+    }
+    else
+    {
+      UNREACHABLE;
+    }
+    same_object_expr.add_source_location() = source_location;
+
+    return same_object_expr;
+  }
   else if(identifier==CPROVER_PREFIX "buffer_size")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -6,6 +6,7 @@ void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_invalid_pointer(const void *);
+__CPROVER_bool __CPROVER_points_to_valid_memory(const void *, ...);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);

src/ansi-c/expr2c.cpp

@@ -3432,6 +3432,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_good_pointer)
     return convert_function(src, "GOOD_POINTER", precedence=16);
 
+  else if(src.id() == ID_points_to_valid_memory)
+    return convert_function(src, "POINTS_TO_VALID_MEMORY", precedence = 16);
+
   else if(src.id()==ID_object_size)
     return convert_function(src, "OBJECT_SIZE", precedence=16);
 

src/goto-instrument/Makefile

@@ -32,6 +32,7 @@ SRC = accelerate/accelerate.cpp \
       document_properties.cpp \
       dot.cpp \
       dump_c.cpp \
+      expand_pointer_predicates.cpp \
       full_slicer.cpp \
       function.cpp \
       function_modifies.cpp \