Enabling poitner-overflow-check where needed on CAR instrumentation

Author: Remi Delmas

src/goto-instrument/contracts/assigns.cpp

@@ -41,9 +41,10 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
       size.has_value(),
       "`sizeof` must always be computable on l-value assigns clause targets.");
 
-    return {typecast_exprt::conditional_cast(
-              address_of_exprt{expr}, pointer_type(char_type())),
-            typecast_exprt::conditional_cast(size.value(), signed_size_type())};
+    return {
+      typecast_exprt::conditional_cast(
+        address_of_exprt{expr}, pointer_type(char_type())),
+      typecast_exprt::conditional_cast(size.value(), signed_size_type())};
   }
 
   UNREACHABLE;
@@ -72,9 +73,11 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
     validity_condition_var(
       generate_new_symbol("__car_valid", bool_typet(), location).symbol_expr()),
     lower_bound_address_var(
-      generate_new_symbol("__car_lb", slice.first.type(), location).symbol_expr()),
+      generate_new_symbol("__car_lb", slice.first.type(), location)
+        .symbol_expr()),
     upper_bound_address_var(
-      generate_new_symbol("__car_ub", slice.first.type(), location).symbol_expr())
+      generate_new_symbol("__car_ub", slice.first.type(), location)
+        .symbol_expr())
 {
 }
 
@@ -90,9 +93,12 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   location_no_checks.add_pragma("disable:pointer-primitive-check");
   location_no_checks.add_pragma("disable:pointer-overflow-check");
 
-  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_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,
@@ -104,7 +110,8 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
     location_no_checks));
 
   goto_programt skip_program;
-  const auto skip_target = skip_program.add(goto_programt::make_skip(location_no_checks));
+  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),
@@ -118,14 +125,16 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions()
   instructions.add(goto_programt::make_assignment(
     lower_bound_address_var, slice.first, location_no_checks));
 
+  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())},
-      // TODO activate pointer-overflow checks
-    // keeping checks since the pointer addition can overflow
-    location));
+    // activate pointer-overflow checks to guard against overflow on this addition
+    location_overflow_check));
   instructions.destructive_append(skip_program);
   return instructions;
 }
@@ -137,8 +146,8 @@ assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check(
   return conjunction(
     {validity_condition_var,
      same_object(lower_bound_address_var, lhs.lower_bound_address_var),
-     // should become redudant if they are derived from the same object and no pointer overflow
-     same_object(lhs.upper_bound_address_var, upper_bound_address_var),
+     // redudant now that we guard against pointer overflow
+     // same_object(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)},