CONTRACTS: disable checks on cprover_contracts.c

Prevents a 5-10x blowup in the number of generated checks for
DFCC instrumented programs.

Functions in `cprover_contracts.c` contain assertions that
check for possible overflows of null pointers where needed,
so we guard against automatic checks instantiation by adding
"checked" pragmas to all instructions of the library.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -109,13 +109,6 @@ __CPROVER_contracts_car_t
 __CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size)
 {
 __CPROVER_HIDE:;
-#pragma CPROVER check push
-#pragma CPROVER check disable "pointer"
-#pragma CPROVER check disable "pointer-primitive"
-#pragma CPROVER check disable "unsigned-overflow"
-#pragma CPROVER check disable "signed-overflow"
-#pragma CPROVER check disable "undefined-shift"
-#pragma CPROVER check disable "conversion"
   __CPROVER_assert(
     ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
     "ptr NULL or writable up to size");
@@ -129,7 +122,6 @@ __CPROVER_HIDE:;
     "no offset bits overflow on CAR upper bound computation");
   return (__CPROVER_contracts_car_t){
     .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
-#pragma CPROVER check pop
 }
 
 /// \brief Initialises a __CPROVER_contracts_car_set_ptr_t object
@@ -163,14 +155,6 @@ void __CPROVER_contracts_car_set_insert(
   __CPROVER_size_t size)
 {
 __CPROVER_HIDE:;
-#pragma CPROVER check push
-#pragma CPROVER check disable "pointer"
-#pragma CPROVER check disable "pointer-overflow"
-#pragma CPROVER check disable "pointer-primitive"
-#pragma CPROVER check disable "unsigned-overflow"
-#pragma CPROVER check disable "signed-overflow"
-#pragma CPROVER check disable "undefined-shift"
-#pragma CPROVER check disable "conversion"
 #ifdef DFCC_DEBUG
   __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access");
 #endif
@@ -188,7 +172,6 @@ __CPROVER_HIDE:;
   __CPROVER_contracts_car_t *elem = set->elems + idx;
   *elem = (__CPROVER_contracts_car_t){
     .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
-#pragma CPROVER check pop
 }
 
 /// \brief Invalidates all cars in the \p set that point into the same object
@@ -1062,18 +1045,10 @@ __CPROVER_HIDE:;
     void *ptr = *current;
 
     // call free only iff the pointer is valid preconditions are met
-#pragma CPROVER check push
-#pragma CPROVER check disable "pointer"
-#pragma CPROVER check disable "pointer-primitive"
-#pragma CPROVER check disable "unsigned-overflow"
-#pragma CPROVER check disable "signed-overflow"
-#pragma CPROVER check disable "undefined-shift"
-#pragma CPROVER check disable "conversion"
     // skip checks on r_ok, dynamic_object and pointer_offset
     __CPROVER_bool preconditions =
       (ptr == 0) | (__CPROVER_r_ok(ptr, 0) & __CPROVER_DYNAMIC_OBJECT(ptr) &
                     (__CPROVER_POINTER_OFFSET(ptr) == 0));
-#pragma CPROVER check pop
     // If there is aliasing between the pointers in the freeable set,
     // and we attempt to free again one of the already freed pointers,
     // the r_ok condition above will fail, preventing us to deallocate
@@ -1204,13 +1179,6 @@ __CPROVER_HIDE:;
   __CPROVER_assert(
     write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
 #endif
-#pragma CPROVER check push
-#pragma CPROVER check disable "pointer"
-#pragma CPROVER check disable "pointer-primitive"
-#pragma CPROVER check disable "pointer-overflow"
-#pragma CPROVER check disable "signed-overflow"
-#pragma CPROVER check disable "unsigned-overflow"
-#pragma CPROVER check disable "conversion"
   if(write_set->assume_requires_ctx)
   {
 #ifdef DFCC_DEBUG
@@ -1311,7 +1279,6 @@ __CPROVER_HIDE:;
     __CPROVER_assume(0);
     return 0; // to silence libcheck
   }
-#pragma CPROVER check pop
 }
 
 /// \brief Returns the start address of the conditional address range found at

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -248,6 +248,9 @@ void dfcct::link_model_and_load_dfcc_library()
   // load the dfcc library before instrumentation starts
   library.load(other_symbols);
 
+  // disable checks on all library functions
+  library.disable_checks();
+
   // add C prover lib again to fetch any dependencies of the dfcc functions
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);

src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp

@@ -209,6 +209,29 @@ dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
     return {};
 }
 
+static void add_checked_pragmas(source_locationt &sl)
+{
+  sl.add_pragma("disable:pointer-check");
+  sl.add_pragma("disable:pointer-primitive-check");
+  sl.add_pragma("disable:pointer-overflow-check");
+  sl.add_pragma("disable:signed-overflow-check");
+  sl.add_pragma("disable:unsigned-overflow-check");
+  sl.add_pragma("disable:conversion-check");
+  sl.add_pragma("disable:undefined-shift-check");
+}
+
+void dfcc_libraryt::disable_checks()
+{
+  for(const auto &pair : dfcc_fun_to_name)
+  {
+    auto &function = goto_model.goto_functions.function_map[pair.second];
+    for(auto &inst : function.body.instructions)
+    {
+      add_checked_pragmas(inst.source_location_nonconst());
+    }
+  }
+}
+
 std::set<irep_idt> dfcc_libraryt::get_missing_funs()
 {
   std::set<irep_idt> missing;

src/goto-instrument/contracts/dynamic-frames/dfcc_library.h

@@ -244,6 +244,10 @@ class dfcc_libraryt
   /// Sets the given hide flag on all instructions of all library functions
   void set_hide(bool hide);
 
+  /// Adds "checked" pragmas to instructions of all library functions
+  /// instructions. By default checks are not disabled.
+  void disable_checks();
+
   /// Returns true iff the given function_id is one of `__CPROVER_assignable`,
   /// `__CPROVER_object_whole`, `__CPROVER_object_from`,
   /// `__CPROVER_object_upto`, `__CPROVER_freeable`