Disabling pointer checks on CAR inclusion instructions. Enabling pointer overflow checks on CAR upper bound computation.

Author: Remi Delmas

regression/contracts/quantifiers-forall-ensures-enforce/main.c

@@ -23,7 +23,7 @@ int f1(int *arr, int len)
 int main()
 {
   int len;
-  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+  __CPROVER_assume(0 < len && len <= MAX_LEN);
 
   int *arr = malloc(len * sizeof(int));
   f1(arr, len);

src/goto-instrument/contracts/assigns.cpp

@@ -12,6 +12,7 @@ Date: July 2021
 /// Specify write set in code contracts
 
 #include "assigns.h"
+#include "utils.h"
 
 #include <analyses/call_graph.h>
 
@@ -87,41 +88,54 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   const
 {
   goto_programt instructions;
-
-  instructions.add(goto_programt::make_decl(validity_condition_var, location));
-  instructions.add(goto_programt::make_decl(lower_bound_address_var, location));
-  instructions.add(goto_programt::make_decl(upper_bound_address_var, location));
+  // adding pragmas to the location to selectively disable checks
+  // where it is sound to do so
+  source_locationt location_no_checks = location;
+  disable_pointer_checks(location_no_checks);
+
+  instructions.add(
+    goto_programt::make_decl(validity_condition_var, location_no_checks));
+  instructions.add(
+    goto_programt::make_decl(lower_bound_address_var, location_no_checks));
+  instructions.add(
+    goto_programt::make_decl(upper_bound_address_var, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
     lower_bound_address_var,
     null_pointer_exprt{to_pointer_type(slice.first.type())},
-    location));
+    location_no_checks));
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
     null_pointer_exprt{to_pointer_type(slice.first.type())},
-    location));
+    location_no_checks));
 
   goto_programt skip_program;
-  const auto skip_target = skip_program.add(goto_programt::make_skip(location));
+  const auto skip_target =
+    skip_program.add(goto_programt::make_skip(location_no_checks));
 
   const auto validity_check_expr =
     and_exprt{all_dereferences_are_valid(source_expr, parent.ns),
               w_ok_exprt{slice.first, slice.second}};
   instructions.add(goto_programt::make_assignment(
-    validity_condition_var, validity_check_expr, location));
+    validity_condition_var, validity_check_expr, location_no_checks));
 
   instructions.add(goto_programt::make_goto(
-    skip_target, not_exprt{validity_condition_var}, location));
+    skip_target, not_exprt{validity_condition_var}, location_no_checks));
 
   instructions.add(goto_programt::make_assignment(
-    lower_bound_address_var, slice.first, location));
+    lower_bound_address_var, slice.first, location_no_checks));
+
+  // the computation of the CAR upper bound can overflow into the object ID bits
+  // of the pointer with very large allocation sizes.
+  // We enable pointer overflow checks to detect such cases.
+  source_locationt location_overflow_check = location;
+  location_overflow_check.add_pragma("enable:pointer-overflow-check");
 
   instructions.add(goto_programt::make_assignment(
     upper_bound_address_var,
     minus_exprt{plus_exprt{slice.first, slice.second},
                 from_integer(1, slice.second.type())},
-    location));
-
+    location_overflow_check));
   instructions.destructive_append(skip_program);
 
   // The assignments above are only performed on locally defined temporaries
@@ -134,14 +148,16 @@ const exprt
 assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check(
   const conditional_address_ranget &lhs) const
 {
+  // remark: both lb and ub are derived from the same object so checking
+  // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
+  // is redundant
   return conjunction(
     {validity_condition_var,
      same_object(lower_bound_address_var, lhs.lower_bound_address_var),
-     same_object(lhs.upper_bound_address_var, upper_bound_address_var),
-     less_than_or_equal_exprt{lower_bound_address_var,
-                              lhs.lower_bound_address_var},
-     less_than_or_equal_exprt{lhs.upper_bound_address_var,
-                              upper_bound_address_var}});
+     less_than_or_equal_exprt{pointer_offset(lower_bound_address_var),
+                              pointer_offset(lhs.lower_bound_address_var)},
+     less_than_or_equal_exprt{pointer_offset(lhs.upper_bound_address_var),
+                              pointer_offset(upper_bound_address_var)}});
 }
 
 assigns_clauset::assigns_clauset(

src/goto-instrument/contracts/contracts.cpp

@@ -911,6 +911,9 @@ void code_contractst::instrument_call_statement(
   }
   else if(callee_name == "free")
   {
+    source_locationt location_no_checks =
+      instruction_it->source_location();
+    disable_pointer_checks(location_no_checks);
     const auto free_car = add_inclusion_check(
       body,
       assigns,
@@ -920,10 +923,9 @@ void code_contractst::instrument_call_statement(
     // skip all invalidation business if we're freeing invalid memory
     goto_programt alias_checking_instructions, skip_program;
     alias_checking_instructions.add(goto_programt::make_goto(
-      skip_program.add(
-        goto_programt::make_skip(instruction_it->source_location())),
+      skip_program.add(goto_programt::make_skip(location_no_checks)),
       not_exprt{free_car.validity_condition_var},
-      instruction_it->source_location()));
+      location_no_checks));
 
     // Since the argument to free may be an "alias" (but not identical)
     // to existing CARs' source_expr, structural equality wouldn't work.
@@ -943,8 +945,8 @@ void code_contractst::instrument_call_statement(
           .symbol_expr();
       write_set_validity_addrs.insert(object_validity_var_addr);
 
-      alias_checking_instructions.add(goto_programt::make_decl(
-        object_validity_var_addr, instruction_it->source_location()));
+      alias_checking_instructions.add(
+        goto_programt::make_decl(object_validity_var_addr, location_no_checks));
       // if the CAR was defined on the same_object as the one being `free`d,
       // record its validity variable's address, otherwise record NULL
       alias_checking_instructions.add(goto_programt::make_assignment(
@@ -956,7 +958,7 @@ void code_contractst::instrument_call_statement(
               free_car.lower_bound_address_var, w_car.lower_bound_address_var)},
           address_of_exprt{w_car.validity_condition_var},
           null_pointer_exprt{to_pointer_type(object_validity_var_addr.type())}},
-        instruction_it->source_location()));
+        location_no_checks));
     }
 
     alias_checking_instructions.destructive_append(skip_program);
@@ -972,24 +974,22 @@ void code_contractst::instrument_call_statement(
     goto_programt invalidation_instructions;
     skip_program.clear();
     invalidation_instructions.add(goto_programt::make_goto(
-      skip_program.add(
-        goto_programt::make_skip(instruction_it->source_location())),
+      skip_program.add(goto_programt::make_skip(location_no_checks)),
       not_exprt{free_car.validity_condition_var},
-      instruction_it->source_location()));
+      location_no_checks));
 
     // invalidate all recorded CAR validity variables
     for(const auto &w_car_validity_addr : write_set_validity_addrs)
     {
       goto_programt w_car_skip_program;
       invalidation_instructions.add(goto_programt::make_goto(
-        w_car_skip_program.add(
-          goto_programt::make_skip(instruction_it->source_location())),
+        w_car_skip_program.add(goto_programt::make_skip(location_no_checks)),
         null_pointer(w_car_validity_addr),
-        instruction_it->source_location()));
+        location_no_checks));
       invalidation_instructions.add(goto_programt::make_assignment(
         dereference_exprt{w_car_validity_addr},
         false_exprt{},
-        instruction_it->source_location()));
+        location_no_checks));
       invalidation_instructions.destructive_append(w_car_skip_program);
     }
 
@@ -1175,6 +1175,10 @@ void code_contractst::check_frame_conditions(
     else if(instruction_it->is_dead())
     {
       const auto &symbol = instruction_it->dead_symbol();
+      source_locationt location_no_checks =
+        instruction_it->source_location();
+      disable_pointer_checks(location_no_checks);
+
       // CAR equality and hash are defined on source_expr alone,
       // therefore this temporary CAR should be "found"
       const auto &symbol_car = assigns.get_write_set().find(
@@ -1228,10 +1232,13 @@ code_contractst::add_inclusion_check(
     program, instruction_it, snapshot_instructions);
 
   goto_programt assertion;
-  assertion.add(goto_programt::make_assertion(
-    assigns.generate_inclusion_check(car), instruction_it->source_location()));
-  assertion.instructions.back().source_location_nonconst().set_comment(
+  source_locationt location_no_checks =
+    instruction_it->source_location_nonconst();
+  disable_pointer_checks(location_no_checks);
+  location_no_checks.set_comment(
     "Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
+  assertion.add(goto_programt::make_assertion(
+    assigns.generate_inclusion_check(car), location_no_checks));
   insert_before_swap_and_advance(program, instruction_it, assertion);
 
   return car;

src/goto-instrument/contracts/utils.cpp

@@ -156,4 +156,10 @@ const symbolt &new_tmp_symbol(
     new_symbol.is_auxiliary = is_auxiliary;
     return new_symbol;
 }
+
+void disable_pointer_checks(source_locationt &source_location)
+{
+  source_location.add_pragma("disable:pointer-check");
+  source_location.add_pragma("disable:pointer-primitive-check");
+  source_location.add_pragma("disable:pointer-overflow-check");
 }

src/goto-instrument/contracts/utils.h

@@ -122,4 +122,7 @@ const symbolt &new_tmp_symbol(
   std::string suffix = "tmp_cc",
   bool is_auxiliary = false);
 
+/// Add disable pragmas for all pointer checks on the given location
+void disable_pointer_checks(source_locationt &source_location);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H