Merge pull request #6365 from padhi-aws-forks/chain-validate

A predicate to validate all pointer derefs in an expression AST

Author: SaswatPadhi

regression/contracts/assigns_enforce_structs_07/main.c

@@ -25,9 +25,12 @@ void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
 
 int main()
 {
-  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  struct pair *p = malloc(sizeof(*p));
   f1(p);
+
   struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  if(pp)
+    pp->p = malloc(sizeof(*(pp->p)));
   f2(pp);
 
   return 0;

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -1,17 +1,16 @@
-KNOWNBUG
+CORE
 main.c
---enforce-all-contracts _ --pointer-check
+--enforce-all-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$
 ^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$
 ^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
 Checks whether CBMC properly evaluates write set of members
 from invalid objects. In this case, they are not writable.
-
-Bug: We need to check the validity of each dereference
-when accessing struct members.

regression/contracts/assigns_replace_07/main.c

@@ -2,24 +2,23 @@
 #include <stdint.h>
 #include <stdlib.h>
 
-struct pair
+struct test
 {
-  uint8_t *buf;
-  size_t size;
+  uint8_t buf[8];
 };
 
-void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
-  __CPROVER_ensures(p->buf[0] == 0)
+void f1(struct test *p) __CPROVER_assigns(p->buf)
+  __CPROVER_ensures((p == NULL) || p->buf[0] == 0)
 {
-  p->buf[0] = 0;
+  if(p != NULL)
+    p->buf[0] = 0;
 }
 
 int main()
 {
-  struct pair *p = nondet_bool() ? malloc(sizeof(*p)) : NULL;
+  struct test *p = malloc(sizeof(*p));
+  uint8_t buf_1 = (p == NULL) ? 0 : p->buf[1];
   f1(p);
-  // clang-format off
-  assert(p != NULL ==> p->buf[0] == 0);
-  // clang-format on
-  return 0;
+  assert(p == NULL || p->buf[0] == 0);
+  assert(p == NULL || p->buf[1] == buf_1);
 }

regression/contracts/assigns_replace_07/test.desc

@@ -1,12 +1,13 @@
 CORE
 main.c
---replace-all-calls-with-contracts _ --pointer-check
+--replace-all-calls-with-contracts _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[0\] == 0: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion p == NULL \|\| p->buf\[1\] == buf_1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
-Checks whether CBMC properly evaluates write set of members
-from invalid objects. In this case, they are not writable.
+Checks whether CBMC properly evaluates write set of members from invalid objects.
+Functions are not expected to write to invalid locations; CBMC flags such writes.
+For contract checking, we ignore invalid targets in assigns clauses and assignment LHS.

regression/contracts/invar_loop-entry_check/main.c

@@ -33,17 +33,17 @@ void main()
   assert(x2 == z2);
 
   int y3;
-  s *s1, *s2;
+  s s0, s1, *s2 = &s0;
   s2->n = malloc(sizeof(int));
-  s1->n = s2->n;
+  s1.n = s2->n;
 
   while(y3 > 0)
-    __CPROVER_loop_invariant(s1->n == __CPROVER_loop_entry(s1->n))
+    __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n))
     {
       --y3;
-      s1->n = s1->n + 1;
-      s1->n = s1->n - 1;
+      s0.n = s0.n + 1;
+      s2->n = s2->n - 1;
     }
 
-  assert(*(s1->n) == *(s2->n));
+  assert(*(s1.n) == *(s2->n));
 }

regression/contracts/invar_loop-entry_check/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
@@ -11,7 +11,7 @@ main.c
 ^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
 ^\[main.5\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.3\] .* assertion \*\(s1->n\) == \*\(s2->n\): SUCCESS$
+^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

src/goto-instrument/Makefile

@@ -17,8 +17,9 @@ SRC = accelerate/accelerate.cpp \
       branch.cpp \
       call_sequences.cpp \
       contracts/assigns.cpp \
-      contracts/memory_predicates.cpp \
       contracts/contracts.cpp \
+      contracts/memory_predicates.cpp \
+      contracts/utils.cpp \
       concurrency.cpp \
       count_eloc.cpp \
       cover.cpp \

src/goto-instrument/contracts/assigns.cpp

@@ -15,10 +15,13 @@ Date: July 2021
 
 #include <goto-instrument/havoc_utils.h>
 
-#include <util/arith_tools.h>
-#include <util/c_types.h>
+#include <langapi/language_util.h>
+
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
+#include "utils.h"
+
 assigns_clauset::targett::targett(
   const assigns_clauset &parent,
   const exprt &expr)
@@ -43,27 +46,16 @@ exprt assigns_clauset::targett::normalize(const exprt &expr)
 exprt assigns_clauset::targett::generate_containment_check(
   const address_of_exprt &lhs_address) const
 {
-  exprt::operandst address_validity;
-  exprt::operandst containment_check;
-
-  // __CPROVER_w_ok(target, sizeof(target))
-  address_validity.push_back(w_ok_exprt(
-    address,
-    size_of_expr(dereference_exprt(address).type(), parent.ns).value()));
+  const auto address_validity = and_exprt{
+    all_dereferences_are_valid(dereference_exprt{address}, parent.ns),
+    all_dereferences_are_valid(dereference_exprt{lhs_address}, parent.ns)};
 
-  // __CPROVER_w_ok(lhs, sizeof(lhs))
-  address_validity.push_back(w_ok_exprt(
-    lhs_address,
-    size_of_expr(dereference_exprt(lhs_address).type(), parent.ns).value()));
-
-  // __CPROVER_same_object(lhs, target)
+  exprt::operandst containment_check;
   containment_check.push_back(same_object(lhs_address, address));
 
   // If assigns target was a dereference, comparing objects is enough
-  // and the resulting condition will be
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
+  // and the resulting condition will be:
+  // VALID(self) && VALID(lhs) ==> __CPROVER_same_object(lhs, self)
   if(id != ID_dereference)
   {
     const auto lhs_offset = pointer_offset(lhs_address);
@@ -86,19 +78,17 @@ exprt assigns_clauset::targett::generate_containment_check(
       own_offset);
 
     // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-    // (sizeof(target) + __CPROVER_offset(target))
+    // (sizeof(self) + __CPROVER_offset(self))
     containment_check.push_back(
       binary_relation_exprt(lhs_region, ID_le, own_region));
   }
 
-  // __CPROVER_w_ok(target, sizeof(target))
-  // && __CPROVER_w_ok(lhs, sizeof(lhs))
-  // ==> __CPROVER_same_object(lhs, target)
-  //     && __CPROVER_offset(lhs) >= __CPROVER_offset(target)
-  //     && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
-  //        (sizeof(target) + __CPROVER_offset(target))
-  return binary_relation_exprt(
-    conjunction(address_validity), ID_implies, conjunction(containment_check));
+  // VALID(self) && VALID(lhs)
+  // ==> __CPROVER_same_object(lhs, self)
+  //  && __CPROVER_offset(lhs) >= __CPROVER_offset(self)
+  //  && (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+  //        (sizeof(self) + __CPROVER_offset(self))
+  return or_exprt{not_exprt{address_validity}, conjunction(containment_check)};
 }
 
 assigns_clauset::assigns_clauset(
@@ -147,12 +137,13 @@ goto_programt assigns_clauset::generate_havoc_code() const
   modifiest modifies;
   for(const auto &target : global_write_set)
     modifies.insert(target.address.object());
-
   for(const auto &target : local_write_set)
     modifies.insert(target.address.object());
 
   goto_programt havoc_statements;
-  append_havoc_code(location, modifies, havoc_statements);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(location, havoc_statements);
+
   return havoc_statements;
 }
 

src/goto-instrument/contracts/assigns.h

@@ -14,9 +14,12 @@ Date: July 2021
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H
 
-#include "contracts.h"
+#include <unordered_set>
 
-#include <util/pointer_offset_size.h>
+#include <goto-programs/goto_model.h>
+
+#include <util/message.h>
+#include <util/pointer_expr.h>
 
 /// \brief A class for representing assigns clauses in code contracts
 class assigns_clauset

src/goto-instrument/contracts/contracts.cpp

@@ -24,73 +24,21 @@ Date: February 2016
 
 #include <goto-programs/remove_skip.h>
 
+#include <langapi/language_util.h>
+
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
 
 #include "assigns.h"
 #include "memory_predicates.h"
-
-// Create a lexicographic less-than relation between two tuples of variables.
-// This is used in the implementation of multidimensional decreases clauses.
-static exprt create_lexicographic_less_than(
-  const std::vector<symbol_exprt> &lhs,
-  const std::vector<symbol_exprt> &rhs)
-{
-  PRECONDITION(lhs.size() == rhs.size());
-
-  if(lhs.empty())
-  {
-    return false_exprt();
-  }
-
-  // Store conjunctions of equalities.
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
-  // s1 == l1 && s2 == l2 && s3 == l3>.
-  // In fact, the last element is unnecessary, so we do not create it.
-  exprt::operandst equality_conjunctions(lhs.size());
-  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
-  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
-  {
-    binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
-    equality_conjunctions[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_equality);
-  }
-
-  // Store inequalities between the i-th components of the input vectors
-  // (i.e. lhs and rhs).
-  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
-  // l2, l3>.
-  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
-  // s2 == l2 && s3 < l3>.
-  exprt::operandst lexicographic_individual_comparisons(lhs.size());
-  lexicographic_individual_comparisons[0] =
-    binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
-  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
-  {
-    binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
-    lexicographic_individual_comparisons[i] =
-      and_exprt(equality_conjunctions[i - 1], component_i_less_than);
-  }
-  return disjunction(lexicographic_individual_comparisons);
-}
-
-static void insert_before_swap_and_advance(
-  goto_programt &program,
-  goto_programt::targett &target,
-  goto_programt &payload)
-{
-  const auto offset = payload.instructions.size();
-  program.insert_before_swap(target, payload);
-  std::advance(target, offset);
-}
+#include "utils.h"
 
 void code_contractst::check_apply_loop_contracts(
   goto_functionst::goto_functiont &goto_function,
@@ -203,7 +151,8 @@ void code_contractst::check_apply_loop_contracts(
   }
 
   // havoc the variables that may be modified
-  append_havoc_code(loop_head->source_location, modifies, havoc_code);
+  havoc_if_validt havoc_gen(modifies, ns);
+  havoc_gen.append_full_havoc_code(loop_head->source_location, havoc_code);
 
   // Generate: assume(invariant) just after havocing
   // We use a block scope to create a temporary assumption,
@@ -289,7 +238,8 @@ void code_contractst::check_apply_loop_contracts(
     // after the loop is smaller than the value before the loop.
     // Here, we use the lexicographic order.
     code_assertt monotonic_decreasing_assertion{
-      create_lexicographic_less_than(new_decreases_vars, old_decreases_vars)};
+      generate_lexicographic_less_than_check(
+        new_decreases_vars, old_decreases_vars)};
     monotonic_decreasing_assertion.add_source_location() =
       loop_head->source_location;
     converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);
@@ -418,6 +368,11 @@ void code_contractst::replace_history_parameter(
 
       if(it == parameter2history.end())
       {
+        // 0. Create a skip target to jump to, if the parameter is invalid
+        goto_programt skip_program;
+        const auto skip_target =
+          skip_program.add(goto_programt::make_skip(location));
+
         // 1. Create a temporary symbol expression that represents the
         // history variable
         symbol_exprt tmp_symbol =
@@ -428,14 +383,23 @@ void code_contractst::replace_history_parameter(
         parameter2history[parameter] = tmp_symbol;
 
         // 3. Add the required instructions to the instructions list
-        // 3.1 Declare the newly created temporary variable
+        // 3.1. Declare the newly created temporary variable
         history.add(goto_programt::make_decl(tmp_symbol, location));
 
-        // 3.2 Add an assignment such that the value pointed to by the new
+        // 3.2. Skip storing the history if the expression is invalid
+        history.add(goto_programt::make_goto(
+          skip_target,
+          not_exprt{all_dereferences_are_valid(parameter, ns)},
+          location));
+
+        // 3.3. Add an assignment such that the value pointed to by the new
         // temporary variable is equal to the value of the corresponding
         // parameter
         history.add(
           goto_programt::make_assignment(tmp_symbol, parameter, location));
+
+        // 3.4. Add a skip target
+        history.destructive_append(skip_program);
       }
 
       expr = parameter2history[parameter];