CONTRACTS: dfcc_is_cprover_symbol now uses allow lists to match symbols

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c

@@ -0,0 +1,23 @@
+void foo()
+{
+  int nondet_var;
+  int __VERIFIER_var;
+  int __CPROVER_var;
+  for(int i = 10; i > 0; i--)
+    // clang-format off
+  __CPROVER_assigns(i)
+  __CPROVER_loop_invariant(0 <= i && i <= 10)
+  __CPROVER_decreases(i)
+    // clang-format on
+    {
+      nondet_var = 0;
+      __VERIFIER_var = 0;
+      __CPROVER_var = 0;
+    }
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that program variables with special name prefixes
+__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking.

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c

@@ -0,0 +1,23 @@
+void foo()
+{
+  int nondet_var;
+  int __VERIFIER_var;
+  int __CPROVER_var;
+  for(int i = 10; i > 0; i--)
+    // clang-format off
+  __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)
+  __CPROVER_loop_invariant(0 <= i && i <= 10)
+  __CPROVER_decreases(i)
+    // clang-format on
+    {
+      nondet_var = 0;
+      __VERIFIER_var = 0;
+      __CPROVER_var = 0;
+    }
+}
+
+int main()
+{
+  foo();
+  return 0;
+}

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] line \d+ Check that nondet_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that __VERIFIER_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_var is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that when program variables names have special prefixes
+__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them
+assignable.

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

@@ -794,7 +794,7 @@ static bool must_check_lhs_from_local_and_tracked(
       return true;
     }
     const auto &id = to_symbol_expr(expr).get_identifier();
-    if(dfcc_is_cprover_symbol(id))
+    if(dfcc_is_cprover_static_symbol(id))
     {
       // Skip the check if we have a single cprover symbol as root object
       // cprover symbols are used for generic checks instrumentation and are

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

@@ -235,7 +235,7 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const
 bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const
 {
   return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
-         (dfcc_is_cprover_symbol(id) || is_internal_symbol(id));
+         (dfcc_is_cprover_function_symbol(id) || is_internal_symbol(id));
 }
 
 void dfcc_instrumentt::instrument_harness_function(

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

@@ -14,9 +14,141 @@ Date: March 2023
 #include <util/prefix.h>
 #include <util/suffix.h>
 
-bool dfcc_is_cprover_symbol(const irep_idt &id)
+#include <unordered_set>
+
+static void
+init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
+{
+  // the set of all CPROVER symbols that we know of
+  if(function_symbols.empty())
+  {
+    function_symbols.insert(CPROVER_PREFIX "_start");
+    function_symbols.insert(CPROVER_PREFIX "array_copy");
+    function_symbols.insert(CPROVER_PREFIX "array_replace");
+    function_symbols.insert(CPROVER_PREFIX "array_set");
+    function_symbols.insert(CPROVER_PREFIX "assert");
+    function_symbols.insert(CPROVER_PREFIX "assignable");
+    function_symbols.insert(CPROVER_PREFIX "assume");
+    function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
+    function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
+    function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
+    function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert");
+    function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove");
+    function_symbols.insert(
+      CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
+    function_symbols.insert(CPROVER_PREFIX "contracts_free");
+    function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable");
+    function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
+    function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
+    function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
+    function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_obj_set_create_indexed_by_object_id");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
+    function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
+    function_symbols.insert(CPROVER_PREFIX "contracts_was_freed");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable");
+    function_symbols.insert(
+      CPROVER_PREFIX
+      "contracts_write_set_check_allocated_deallocated_is_empty");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_array_copy");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_array_replace");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_array_set");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_assignment");
+    function_symbols.insert(
+      CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_deallocate");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_frees_clause_inclusion");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_check_havoc_object");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_deallocate_freeable");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_havoc_get_assignable_target");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_havoc_object_whole");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_insert_assignable");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_insert_object_from");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_insert_object_upto");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_insert_object_whole");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead");
+    function_symbols.insert(CPROVER_PREFIX
+                            "contracts_write_set_record_deallocated");
+    function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release");
+    function_symbols.insert(CPROVER_PREFIX "deallocate");
+    function_symbols.insert(CPROVER_PREFIX "freeable");
+    function_symbols.insert(CPROVER_PREFIX "havoc_object");
+    function_symbols.insert(CPROVER_PREFIX "havoc_slice");
+    function_symbols.insert(CPROVER_PREFIX "initialize");
+    function_symbols.insert(CPROVER_PREFIX "is_freeable");
+    function_symbols.insert(CPROVER_PREFIX "is_fresh");
+    function_symbols.insert(CPROVER_PREFIX "obeys_contract");
+    function_symbols.insert(CPROVER_PREFIX "object_from");
+    function_symbols.insert(CPROVER_PREFIX "object_upto");
+    function_symbols.insert(CPROVER_PREFIX "object_whole");
+    function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc");
+    function_symbols.insert(CPROVER_PREFIX "precondition");
+    function_symbols.insert(CPROVER_PREFIX "printf");
+    function_symbols.insert(CPROVER_PREFIX "was_freed");
+  }
+}
+
+static void init_static_symbols(std::unordered_set<irep_idt> &static_symbols)
+{
+  if(static_symbols.empty())
+  {
+    static_symbols.insert(CPROVER_PREFIX "dead_object");
+    static_symbols.insert(CPROVER_PREFIX "deallocated");
+    static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
+    static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
+    static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
+    static_symbols.insert(CPROVER_PREFIX
+                          "malloc_failure_mode_assert_then_assume");
+    static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
+    static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
+    static_symbols.insert(CPROVER_PREFIX "memory_leak");
+    static_symbols.insert(CPROVER_PREFIX "pipe_offset");
+    static_symbols.insert(CPROVER_PREFIX "pipes");
+    static_symbols.insert(CPROVER_PREFIX "rounding_mode");
+  }
+}
+
+bool dfcc_is_cprover_function_symbol(const irep_idt &id)
 {
+  std::unordered_set<irep_idt> function_symbols;
+  init_function_symbols(function_symbols);
   std::string str = id2string(id);
-  return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") ||
-         has_prefix(str, "nondet") || has_suffix(str, "$object");
+  return function_symbols.find(id) != function_symbols.end() ||
+         // nondet functions
+         has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
+}
+
+bool dfcc_is_cprover_static_symbol(const irep_idt &id)
+{
+  std::unordered_set<irep_idt> static_symbols;
+  init_static_symbols(static_symbols);
+  return static_symbols.find(id) != static_symbols.end() ||
+         // auto objects from pointer derefs
+         has_suffix(id2string(id), "$object");
 }

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

@@ -15,8 +15,13 @@ Date: March 2023
 
 #include <util/irep.h>
 
-/// \return True iff the id starts with CPROVER_PREFIX, `__VERIFIER`, `nondet`
-/// or ends with `$object`.
-bool dfcc_is_cprover_symbol(const irep_idt &id);
+/// Returns `true` iff id is one of the known CPROVER functions or starts with
+/// `__VERIFIER` or `nondet`.
+bool dfcc_is_cprover_function_symbol(const irep_idt &id);
+
+/// Returns `true` iff the symbol is one of the known CPROVER static
+/// instrumentation variables or ends with `$object` and represents an
+/// auto-generated object following a pointer dereference.
+bool dfcc_is_cprover_static_symbol(const irep_idt &id);
 
 #endif