CONTRATCS: force success for some pointer predicates

Force success for pointer predicates that must
necessarily hold if they ever get invoked in
an assumption context. This ensures that the value sets
of pointers as as small as possible after assuming
a requires or an ensures clause and 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, DFCC instrumentation sets the `may_fail`
parameter to true or false using recursive algorithm.

Author: Remi Delmas

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,

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

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";
+}

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

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"
@@ -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));
         }

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));
 

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)
     {

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));
         }

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

@@ -25,6 +25,7 @@
 
 #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,103 @@
   postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl));
 }
 
+/// Recursively traverses expression, adding "no_fail" attributes to pointer
+/// predicates that we know cannot fail when invoked in an assume context:
+/// Starting from the root with "no_fail" true, we recurse over the boolean
+/// structure, setting the "no_fail" false for all but the last operand
+/// disjunctive operators like `||` and `==>`, and distributing the current
+/// "no_fail" status over disjunctions.
+///
+/// For instance:
+/// ```
+/// (len > 0):no_fail=false ==> is_fresh(p, len):no_fail=true
+/// ```
+///
+/// ```
+/// is_fresh(p, len):no_fail=true && is_fresh(q, len):no_fail=true
+/// ```
+///
+/// ```
+/// is_fresh(p, len):no_fail=false ||
+/// is_fresh(q, len):no_fail=false ||
+/// is_fresh(r, len):no_fail=true
+/// ```
+///
+/// ```
+/// is_fresh(p, len):no_fail=false ||
+/// (
+///    is_fresh(q, len):no_fail=true &&
+///    (
+///      (len>0):no_fail=true ==> is_fresh(r, len):no_fail=true
+///    )
+/// )
+/// ```
+/// \param expr The expression to traverse
+/// \param no_fail The current no_fail value based on logical context
+void disable_may_fail_rec(exprt &expr, bool no_fail)
+{
+  if(expr.id() == ID_side_effect)
+  {
+    // Base case: pointer predicate function call
+    side_effect_exprt &side_effect = to_side_effect_expr(expr);
+    if(side_effect.get_statement() == ID_function_call)
+    {
+      exprt &function = side_effect.operands()[0];
+      if(function.id() == ID_symbol)
+      {
+        const irep_idt &func_name = to_symbol_expr(function).get_identifier();
+        if(dfcc_is_cprover_pointer_predicate(func_name))
+        {
+          function.add_source_location().set("no_fail", no_fail);
+        }
+      }
+    }
+    return;
+  }
+  else if(expr.id() == ID_and)
+  {
+    // Shortcutting AND: propagate current no_fail value to all operands
+    for(auto &op : expr.operands())
+    {
+      disable_may_fail_rec(op, no_fail);
+    }
+  }
+  else if(expr.id() == ID_or)
+  {
+    // Shortcutting OR: set no_fail=false for all but last operand
+    auto &ops = expr.operands();
+    // Process all operands except the last one with no_fail=false
+    for(std::size_t i = 0; i < ops.size() - 1; ++i)
+    {
+      disable_may_fail_rec(ops[i], false);
+    }
+    // Process last operand with current no_fail value
+    if(!ops.empty())
+    {
+      disable_may_fail_rec(ops.back(), no_fail);
+    }
+  }
+  else if(expr.id() == ID_implies)
+  {
+    // Shortcutting implies: false for antecedent, current value for consequent
+    INVARIANT(
+      expr.operands().size() == 2,
+      "Implication expression must have two operands");
+    disable_may_fail_rec(expr.operands()[0], false);
+    disable_may_fail_rec(expr.operands()[1], no_fail);
+  }
+  else
+  {
+    // bail on other types of expressions
+    return;
+  }
+}
+
+void disable_may_fail(exprt &expr)
+{
+  disable_may_fail_rec(expr, true);
+}
+
 void dfcc_wrapper_programt::encode_requires_clauses()
 {
   // we use this empty requires write set to check for the absence of side
@@ -556,6 +654,9 @@
   {
     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 +706,9 @@
                       .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);