Memory predicate tests and one-argument form [depends-on: #2644]

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,8 @@
+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,18 @@
+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\] Variable length assert: SUCCESS$
+^\[main.assertion.2\] 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\] : 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]+\] dereference failure: dead object in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)2\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)-1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: dead object in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in y\[\(signed long( long)? int\)0\]: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] 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]+\] dereference failure: dead object in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[main.pointer_dereference.[0-9]+\] dereference failure: pointer outside object bounds in x\[\(signed long( long)? int\)1\]: FAILURE$
+^\[main.pointer_dereference.[0-9]+\] 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

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -32,6 +33,8 @@ Author: Daniel Kroening, [email protected]
 #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)
@@ -2085,6 +2088,60 @@ 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)
+    {
+      err_location(f_op);
+      error() << "points_to_valid_memory expects one or two operands" << eom;
+      throw 0;
+    }
+    if(!is_lvalue(expr.arguments().front()))
+    {
+      err_location(f_op);
+      error() << "ptr argument to points_to_valid_memory"
+              << " must be an lvalue" << eom;
+      throw 0;
+    }
+
+    exprt same_object_expr;
+    if(expr.arguments().size() == 2)
+    {
+      // TODO: We should add some way to enforce that the second argument
+      // has a reasonable type (coercible to __CPROVER_size_t).
+#if 0
+      if(expr.arguments()[1].type() <[cannot be coerced to size_t]>)
+      {
+        err_location(f_op);
+        error() << "size argument to points_to_valid_memory"
+                << " must be coercible to size_t" << eom;
+        throw 0;
+      }
+#endif
+      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();
+      exprt sizeof_expr = size_of_expr(base_type, *this);
+      sizeof_expr.add(ID_C_c_sizeof_type)=base_type;
+
+      same_object_expr = points_to_valid_memory(
+        expr.arguments()[0],
+        sizeof_expr);
+    }
+    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

@@ -3521,6 +3521,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 \