CONTRATCS: force success for unit pointer predicates

Force success for pointer predicates that appear as
top level units in requires or ensures clauses.
For example `__CPROVER_ensures(__CPROVER_is_fresh(p,size))`
is a unit. This ensures that the value set of `p`
after assuming the clause contains a unique valid
target. It solves a performance issue with z3.
All predicates in the `cprover_contracts.c` library
now have an extra input `may_fail` controlling the
failure behaviour, instrumentation detects units in
contracts and sets the `may_fail` parameter accordingly.

Author: Remi Delmas

Diff for: regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc

@@ -1,4 +1,4 @@
-FUTURE dfcc-only smt-backend broken-cprover-smt-backend
+CORE dfcc-only smt-backend broken-cprover-smt-backend
 main.c
 --dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks
 ^EXIT=0$
@@ -8,11 +8,6 @@ main.c
 ^warning: ignoring
 --
 
-Marked as FUTURE because:
-- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`,
- but the CI uses older versions;
-- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI.
-
 Tests support for quantifiers in loop contracts with the SMT backend.
 When quantified loop invariants are used, they are inserted three times
 in the transformed program (base case assertion, step case assumption,

Diff for: src/ansi-c/library/cprover_contracts.c

@@ -1166,6 +1166,7 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr)
 ///
 /// \param ptr1 First argument of the `pointer_equals` predicate
 /// \param ptr2 Second argument of the `pointer_equals` predicate
+/// \param may_fail Allow predicate to fail in assume mode
 /// \param write_set Write set which conveys the invocation context
 ///   (requires/ensures clause, assert/assume context);
 ///
@@ -1179,6 +1180,7 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr)
 __CPROVER_bool __CPROVER_contracts_pointer_equals(
   void **ptr1,
   void *ptr2,
+  __CPROVER_bool may_fail,
   __CPROVER_contracts_write_set_ptr_t write_set)
 {
 __CPROVER_HIDE:;
@@ -1195,7 +1197,8 @@ __CPROVER_HIDE:;
 #endif
   if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
   {
-    if(__VERIFIER_nondet___CPROVER_bool())
+    // SOUNDNESS: allow predicate to fail
+    if(may_fail && __VERIFIER_nondet___CPROVER_bool())
     {
       __CPROVER_contracts_make_invalid_pointer(ptr1);
       return 0;
@@ -1224,8 +1227,9 @@ __CPROVER_HIDE:;
 /// The behaviour depends on the boolean flags carried by \p write_set
 /// which reflect the invocation context: checking vs. replacing a contract,
 /// in a requires or an ensures clause context.
-/// \param elem First argument of the `is_fresh` predicate
-/// \param size Second argument of the `is_fresh` predicate
+/// \param elem Pointer to the target pointer of the check
+/// \param size Size to check for
+/// \param may_fail Allow predicate to fail in assume mode
 /// \param write_set Write set in which seen/allocated objects are recorded;
 ///
 /// \details The behaviour is as follows:
@@ -1242,6 +1246,7 @@ __CPROVER_HIDE:;
 __CPROVER_bool __CPROVER_contracts_is_fresh(
   void **elem,
   __CPROVER_size_t size,
+  __CPROVER_bool may_fail,
   __CPROVER_contracts_write_set_ptr_t write_set)
 {
 __CPROVER_HIDE:;
@@ -1289,7 +1294,7 @@ __CPROVER_HIDE:;
     }
 
     // SOUNDNESS: allow predicate to fail
-    if(__VERIFIER_nondet___CPROVER_bool())
+    if(may_fail && __VERIFIER_nondet___CPROVER_bool())
     {
       __CPROVER_contracts_make_invalid_pointer(elem);
       return 0;
@@ -1349,7 +1354,7 @@ __CPROVER_HIDE:;
     }
 
     // SOUNDNESS: allow predicate to fail
-    if(__VERIFIER_nondet___CPROVER_bool())
+    if(may_fail && __VERIFIER_nondet___CPROVER_bool())
     {
       __CPROVER_contracts_make_invalid_pointer(elem);
       return 0;
@@ -1436,6 +1441,7 @@ __CPROVER_HIDE:;
 /// \param lb Lower bound pointer
 /// \param ptr Target pointer of the predicate
 /// \param ub Upper bound pointer
+/// \param may_fail Allow predicate to fail in assume mode
 /// \param write_set Write set in which seen/allocated objects are recorded;
 ///
 /// \details The behaviour is as follows:
@@ -1449,6 +1455,7 @@ __CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc(
   void *lb,
   void **ptr,
   void *ub,
+  __CPROVER_bool may_fail,
   __CPROVER_contracts_write_set_ptr_t write_set)
 {
 __CPROVER_HIDE:;
@@ -1470,9 +1477,9 @@ __CPROVER_HIDE:;
     lb_offset <= ub_offset, "lb and ub pointers must be ordered");
   if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
   {
-    if(__VERIFIER_nondet___CPROVER_bool())
+    // SOUNDNESS: allow predicate to fail
+    if(may_fail && __VERIFIER_nondet___CPROVER_bool())
     {
-      // SOUNDNESS: allow predicate to fail
       __CPROVER_contracts_make_invalid_pointer(ptr);
       return 0;
     }
@@ -1647,6 +1654,7 @@ __CPROVER_HIDE:;
 __CPROVER_bool __CPROVER_contracts_obeys_contract(
   void (**function_pointer)(void),
   void (*contract)(void),
+  __CPROVER_bool may_fail,
   __CPROVER_contracts_write_set_ptr_t set)
 {
 __CPROVER_HIDE:;
@@ -1657,8 +1665,8 @@ __CPROVER_HIDE:;
     "__CPROVER_obeys_contract is used only in requires or ensures clauses");
   if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1))
   {
-    // decide if predicate must hold
-    if(__VERIFIER_nondet___CPROVER_bool())
+    // SOUDNESS: allow predicate to fail
+    if(may_fail && __VERIFIER_nondet___CPROVER_bool())
       return 0;
 
     // must hold, assign the function pointer to the contract function

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp

@@ -156,3 +156,11 @@ bool dfcc_is_cprover_static_symbol(const irep_idt &id)
          // going_to variables converted from goto statements
          has_prefix(id2string(id), CPROVER_PREFIX "going_to");
 }
+
+bool dfcc_is_cprover_pointer_predicate(const irep_idt &id)
+{
+  return id == CPROVER_PREFIX "pointer_equals" ||
+         id == CPROVER_PREFIX "is_fresh" ||
+         id == CPROVER_PREFIX "pointer_in_range_dfcc" ||
+         id == CPROVER_PREFIX "obeys_contract";
+}

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.h

@@ -24,4 +24,7 @@ bool dfcc_is_cprover_function_symbol(const irep_idt &id);
 /// auto-generated object following a pointer dereference.
 bool dfcc_is_cprover_static_symbol(const irep_idt &id);
 
+/// Returns `true` iff the symbol is one of the CPROVER pointer predicates
+bool dfcc_is_cprover_pointer_predicate(const irep_idt &id);
+
 #endif

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp

@@ -11,6 +11,8 @@ Date: August 2022
 
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
+#include <util/prefix.h>
+#include <util/suffix.h>
 #include <util/symbol.h>
 
 #include "dfcc_cfg_info.h"
@@ -33,7 +35,7 @@ void dfcc_is_fresht::rewrite_calls(
     program.instructions.end(),
     cfg_info);
 }
-
+#include <iostream>
 void dfcc_is_fresht::rewrite_calls(
   goto_programt &program,
   goto_programt::targett first_instruction,
@@ -50,8 +52,7 @@ void dfcc_is_fresht::rewrite_calls(
       if(function.id() == ID_symbol)
       {
         const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
-
-        if(fun_name == CPROVER_PREFIX "is_fresh")
+        if(has_prefix(id2string(fun_name), CPROVER_PREFIX "is_fresh"))
         {
           // add address on first operand
           target->call_arguments()[0] =
@@ -61,6 +62,12 @@ void dfcc_is_fresht::rewrite_calls(
           to_symbol_expr(target->call_function())
             .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name);
 
+          // pass the may_fail flag
+          if(function.source_location().get_bool("no_fail"))
+            target->call_arguments().push_back(false_exprt());
+          else
+            target->call_arguments().push_back(true_exprt());
+
           // pass the write_set
           target->call_arguments().push_back(cfg_info.get_write_set(target));
         }

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp

@@ -12,6 +12,7 @@ Date: August 2022
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
+#include <util/suffix.h>
 #include <util/symbol.h>
 
 #include <langapi/language_util.h>
@@ -87,6 +88,12 @@ void dfcc_obeys_contractt::rewrite_calls(
             .set_identifier(
               library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name);
 
+          // pass the may_fail flag
+          if(function.source_location().get_bool("no_fail"))
+            target->call_arguments().push_back(false_exprt());
+          else
+            target->call_arguments().push_back(true_exprt());
+
           // pass the write_set
           target->call_arguments().push_back(cfg_info.get_write_set(target));
 

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp

@@ -13,9 +13,11 @@ Date: Jan 2025
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
 #include <util/pointer_expr.h>
+#include <util/prefix.h>
 #include <util/replace_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
+#include <util/suffix.h>
 #include <util/symbol.h>
 
 #include "dfcc_cfg_info.h"
@@ -56,7 +58,7 @@ void dfcc_pointer_equalst::rewrite_calls(
       {
         const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
 
-        if(fun_name == CPROVER_PREFIX "pointer_equals")
+        if(has_prefix(id2string(fun_name), CPROVER_PREFIX "pointer_equals"))
         {
           // add address on first operand
           target->call_arguments()[0] =
@@ -67,6 +69,12 @@ void dfcc_pointer_equalst::rewrite_calls(
             .set_identifier(
               library.dfcc_fun_symbol[dfcc_funt::POINTER_EQUALS].name);
 
+          // pass the may_fail flag
+          if(function.source_location().get_bool("no_fail"))
+            target->call_arguments().push_back(false_exprt());
+          else
+            target->call_arguments().push_back(true_exprt());
+
           // pass the write_set
           target->call_arguments().push_back(cfg_info.get_write_set(target));
         }
@@ -106,7 +114,8 @@ class pointer_equality_visitort : public expr_visitort
        code_typet::parametert(pointer_type(void_type()))},
       bool_typet());
 
-    symbol_exprt pointer_equals("ID_pointer_equals", pointer_equals_type);
+    symbol_exprt pointer_equals(
+      CPROVER_PREFIX "pointer_equals", pointer_equals_type);
 
     for(exprt *expr_ptr : equality_exprs_to_transform)
     {

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp

@@ -11,8 +11,10 @@ Date: August 2022
 
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
+#include <util/prefix.h>
 #include <util/replace_expr.h>
 #include <util/std_code.h>
+#include <util/suffix.h>
 #include <util/symbol.h>
 
 #include "dfcc_cfg_info.h"
@@ -53,7 +55,8 @@ void dfcc_pointer_in_ranget::rewrite_calls(
       {
         const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
 
-        if(fun_name == CPROVER_PREFIX "pointer_in_range_dfcc")
+        if(has_prefix(
+             id2string(fun_name), CPROVER_PREFIX "pointer_in_range_dfcc"))
         {
           // add address on second operand
           target->call_arguments()[1] =
@@ -64,6 +67,13 @@ void dfcc_pointer_in_ranget::rewrite_calls(
             .set_identifier(
               library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name);
 
+          // pass the may_fail flag
+          // pass the may_fail flag
+          if(function.source_location().get_bool("no_fail"))
+            target->call_arguments().push_back(false_exprt());
+          else
+            target->call_arguments().push_back(true_exprt());
+
           // pass the write_set
           target->call_arguments().push_back(cfg_info.get_write_set(target));
         }

Diff for: src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -25,6 +25,7 @@ Author: Remi Delmas, [email protected]
 
 #include "dfcc_contract_functions.h"
 #include "dfcc_instrument.h"
+#include "dfcc_is_cprover_symbol.h"
 #include "dfcc_library.h"
 #include "dfcc_lift_memory_predicates.h"
 #include "dfcc_pointer_equals.h"
@@ -535,6 +536,37 @@ void dfcc_wrapper_programt::encode_is_fresh_set()
   postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl));
 }
 
+#include <iostream>
+
+/// If the expression is a function call to one of the pointer predicates,
+/// adds a "_no_fail" prefix to the function name. This is later picked up
+/// by fix_calls to synthesize the value of the `may_fail` parameter for
+/// pointer predicates.
+bool disable_may_fail(exprt &expr)
+{
+  if(expr.id() != ID_side_effect)
+    return false;
+
+  side_effect_exprt &side_effect = to_side_effect_expr(expr);
+  if(side_effect.get_statement() != ID_function_call)
+    return false;
+
+  exprt &function = side_effect.operands()[0];
+  if(function.id() != ID_symbol)
+    return false;
+
+  const irep_idt &func_name = to_symbol_expr(function).get_identifier();
+
+  if(dfcc_is_cprover_pointer_predicate(func_name))
+  {
+    // tag call as no_fail
+    function.add_source_location().set("no_fail", true);
+    return true;
+  }
+
+  return false;
+}
+
 void dfcc_wrapper_programt::encode_requires_clauses()
 {
   // we use this empty requires write set to check for the absence of side
@@ -556,6 +588,9 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   {
     exprt requires_lmbd =
       to_lambda_expr(r).application(contract_lambda_parameters);
+
+    // add "no_fail" suffix to predicates required as units
+    disable_may_fail(requires_lmbd);
     source_locationt sl(r.source_location());
     if(statement_type == ID_assert)
     {
@@ -605,6 +640,9 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
                       .application(contract_lambda_parameters)
                       .with_source_location(e);
 
+    // add "no_fail" suffix to unit pointer predicates
+    disable_may_fail(ensures);
+
     // this also rewrites ID_old expressions to fresh variables
     generate_history_variables_initialization(
       goto_model.symbol_table, ensures, language_mode, history);