Verify that pointers used in pointer primitives are either null or valid

regression/cbmc/pointer-primitive-check-01/main.c

@@ -0,0 +1,28 @@
+
+void main()
+{
+  // we need a new variable for each check, as goto_checkt removes redundant
+  // assertions, and if we would use the same variable all pointer primitive
+  // assertions would look the same
+
+  char *p1;
+  __CPROVER_same_object(p1, p1);
+
+  char *p2;
+  __CPROVER_POINTER_OFFSET(p2);
+
+  char *p3;
+  __CPROVER_POINTER_OBJECT(p3);
+
+  char *p4;
+  __CPROVER_OBJECT_SIZE(p4);
+
+  char *p5;
+  __CPROVER_r_ok(p5, 1);
+
+  char *p6;
+  __CPROVER_w_ok(p6, 1);
+
+  char *p7;
+  __CPROVER_DYNAMIC_OBJECT(p7);
+}

regression/cbmc/pointer-primitive-check-01/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OFFSET.*: FAILURE
+\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in OBJECT_SIZE.*: FAILURE
+\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
+\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in W_OK.*: FAILURE
+\*\* 7 of \d+ failed
+--
+^warning: ignoring
+--
+Verifies that checks are added for all pointer primitives

regression/cbmc/pointer-primitive-check-02/main.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+char *p1;
+
+void main()
+{
+  __CPROVER_POINTER_OBJECT(p1);
+
+  char *p2 = NULL;
+  __CPROVER_POINTER_OBJECT(p2);
+}

regression/cbmc/pointer-primitive-check-02/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verifies that a null pointer does not fail the pointer primitives check

regression/cbmc/pointer-primitive-check-03/main.c

@@ -0,0 +1,40 @@
+#include <stdlib.h>
+
+void main()
+{
+  // uninitialized pointer
+  char *p1;
+  __CPROVER_POINTER_OBJECT(p1);
+
+  // special value of invalid pointer
+  char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8);
+  __CPROVER_POINTER_OBJECT(p2);
+
+  // pointer object 123, offset 123, not pointing to valid memory
+  char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123;
+  __CPROVER_POINTER_OBJECT(p3);
+
+  // negative offset
+  char *p4 = malloc(1);
+  p4 -= 1;
+  __CPROVER_POINTER_OBJECT(p4);
+
+  // offset out of bounds
+  char *p5 = malloc(10);
+  p5 += 10;
+  __CPROVER_POINTER_OBJECT(p5);
+
+  // dead
+  char *p6;
+  {
+    char c;
+    p6 = &c;
+  }
+  __CPROVER_POINTER_OBJECT(p6);
+  *p6;
+
+  // deallocated
+  char *p7 = malloc(1);
+  free(p7);
+  __CPROVER_POINTER_OBJECT(p7);
+}

regression/cbmc/pointer-primitive-check-03/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\[main.pointer_primitives.7\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
+\*\* 7 of \d+ failed
+--
+^warning: ignoring
+--
+Verifies that the pointer primitives check fails for the various forms of
+invalid pointers

regression/cbmc/pointer-primitive-check-04/main.c

@@ -0,0 +1,6 @@
+
+void main()
+{
+  char *p;
+  __CPROVER_assume(__CPROVER_r_ok(p, 1));
+}

regression/cbmc/pointer-primitive-check-04/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-primitive-check
+^EXIT=10$
+^SIGNAL=0$
+\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
+\*\* 1 of \d+ failed
+--
+^warning: ignoring
+--
+Verifies that the check fails for a primitive in an assume that uses an
+uninitialized pointer

src/analyses/goto_check.cpp

@@ -72,6 +72,8 @@ class goto_checkt
     enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
+    enable_pointer_primitive_check =
+      _options.get_bool_option("pointer-primitive-check");
   }
 
   typedef goto_functionst::goto_functiont goto_functiont;
@@ -185,6 +187,20 @@ class goto_checkt
     const exprt &src_expr,
     const guardt &guard);
 
+  /// Generates VCCs to check that pointers passed to pointer primitives are
+  /// either null or valid
+  ///
+  /// \param expr: the pointer primitive expression
+  /// \param guard: the condition under which the operation happens
+  void pointer_primitive_check(const exprt &expr, const guardt &guard);
+
+  /// Returns true if the given expression is a pointer primitive such as
+  /// __CPROVER_r_ok()
+  ///
+  /// \param expr expression
+  /// \return true if the given expression is a pointer primitive
+  bool is_pointer_primitive(const exprt &expr);
+
   conditionst address_check(const exprt &address, const exprt &size);
   void integer_overflow_check(const exprt &, const guardt &);
   void conversion_check(const exprt &, const guardt &);
@@ -238,6 +254,7 @@ class goto_checkt
   bool enable_assertions;
   bool enable_built_in_assertions;
   bool enable_assumptions;
+  bool enable_pointer_primitive_check;
 
   typedef optionst::value_listt error_labelst;
   error_labelst error_labels;
@@ -1163,6 +1180,53 @@ void goto_checkt::pointer_validity_check(
   }
 }
 
+void goto_checkt::pointer_primitive_check(
+  const exprt &expr,
+  const guardt &guard)
+{
+  if(!enable_pointer_primitive_check)
+    return;
+
+  const exprt pointer = (expr.id() == ID_r_ok || expr.id() == ID_w_ok)
+                          ? to_binary_expr(expr).lhs()
+                          : to_unary_expr(expr).op();
+
+  CHECK_RETURN(pointer.type().id() == ID_pointer);
+
+  const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns);
+
+  const exprt size = !size_of_expr_opt.has_value()
+                       ? from_integer(1, size_type())
+                       : size_of_expr_opt.value();
+
+  const conditionst &conditions = address_check(pointer, size);
+
+  exprt::operandst conjuncts;
+
+  for(const auto &c : conditions)
+    conjuncts.push_back(c.assertion);
+
+  const or_exprt or_expr(null_object(pointer), conjunction(conjuncts));
+
+  add_guarded_property(
+    or_expr,
+    "pointer in pointer primitive is neither null nor valid",
+    "pointer primitives",
+    expr.source_location(),
+    expr,
+    guard);
+}
+
+bool goto_checkt::is_pointer_primitive(const exprt &expr)
+{
+  // we don't need to include the __CPROVER_same_object primitive here as it
+  // is replaced by lower level primitives in the special function handling
+  // during typechecking (see c_typecheck_expr.cpp)
+  return expr.id() == ID_pointer_object || expr.id() == ID_pointer_offset ||
+         expr.id() == ID_object_size || expr.id() == ID_r_ok ||
+         expr.id() == ID_w_ok || expr.id() == ID_is_dynamic_object;
+}
+
 goto_checkt::conditionst
 goto_checkt::address_check(const exprt &address, const exprt &size)
 {
@@ -1740,6 +1804,10 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
   {
     pointer_validity_check(to_dereference_expr(expr), expr, guard);
   }
+  else if(is_pointer_primitive(expr))
+  {
+    pointer_primitive_check(expr, guard);
+  }
 }
 
 void goto_checkt::check(const exprt &expr)
@@ -1860,6 +1928,8 @@ void goto_checkt::goto_check(
         flag_resetter.set_flag(enable_undefined_shift_check, false);
       else if(d.first == "disable:nan-check")
         flag_resetter.set_flag(enable_nan_check, false);
+      else if(d.first == "disable:pointer-primitive-check")
+        flag_resetter.set_flag(enable_pointer_primitive_check, false);
     }
 
     new_code.clear();
@@ -2049,7 +2119,7 @@ void goto_checkt::goto_check(
     }
     else if(i.is_dead())
     {
-      if(enable_pointer_check)
+      if(enable_pointer_check || enable_pointer_primitive_check)
       {
         assert(i.code.operands().size()==1);
         const symbol_exprt &variable=to_symbol_expr(i.code.op0());

src/analyses/goto_check.h

@@ -38,7 +38,8 @@ void goto_check(
   "(div-by-zero-check)(enum-range-check)(signed-overflow-check)(unsigned-"     \
   "overflow-check)"                                                            \
   "(pointer-overflow-check)(conversion-check)(undefined-shift-check)"          \
-  "(float-overflow-check)(nan-check)(no-built-in-assertions)"
+  "(float-overflow-check)(nan-check)(no-built-in-assertions)"                  \
+  "(pointer-primitive-check)"
 
 // clang-format off
 #define HELP_GOTO_CHECK \
@@ -55,7 +56,7 @@ void goto_check(
   " --nan-check                  check floating-point for NaN\n" \
   " --no-built-in-assertions     ignore assertions in built-in library\n" \
   " --enum-range-check           checks that all enum type expressions have values in the enum range\n" /* NOLINT(whitespace/line_length) */ \
-// clang-format on
+  " --pointer-primitive-check    checks that all pointers in pointer primitives are valid or null\n" /* NOLINT(whitespace/line_length) */
 
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
   options.set_option("bounds-check", cmdline.isset("bounds-check")); \
@@ -70,6 +71,8 @@ void goto_check(
   options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
-  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")) /* NOLINT(whitespace/line_length) */
+  options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
+  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")) /* NOLINT(whitespace/line_length) */
+// clang-format on
 
 #endif // CPROVER_ANALYSES_GOTO_CHECK_H