Avoid branches in CPROVER library for --paths mode

regression/cbmc/BV_Arithmetic3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 main.c
 --verbosity 8
 ^EXIT=0$
@@ -7,3 +7,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+rewrites branches into conditional assignments, which changes the number of
+generated VCCs (68 vs 73); the verification result is unchanged.

regression/cbmc/destructors/compound_literal.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 main.c
 --unwind 10 --show-goto-functions --no-standard-checks
 activate-multi-line-match
@@ -20,3 +20,7 @@ Checks for:
 
 This asserts that when you've created a compound literal that both temp and real
 variable gets killed.
+
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+rewrites branches into conditional assignments, changing the --show-goto-functions
+output this test pins; the behaviour under test is unaffected.

regression/cbmc/destructors/enter_lexical_block.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
@@ -35,3 +35,7 @@ Checks for:
 This asserts that when the GOTO is going into a lexical block that destructors
 are not omitted. This used to be a limitation with the previous implementation
 and has now been fixed.
+
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+rewrites branches into conditional assignments, changing the --show-goto-functions
+output this test pins; the behaviour under test is unaffected.

regression/cbmc/if-conversion-clobber/main.c

@@ -0,0 +1,26 @@
+// If-conversion snapshots the branch condition before linearising a region.
+// This is required for soundness when an earlier assignment in the region
+// overwrites a variable that the condition reads: the generated conditional
+// expressions must all use the condition's value as it was at the branch, not
+// a value clobbered part-way through the region.
+//
+// Here the branch is taken (x = 1 > 0), so the original program sets y = 7.
+// Without snapshotting, the rewrite of `y = 7` would re-evaluate `x > 0` after
+// `x` had been set to -5, wrongly leaving y at 9 and reporting a spurious
+// counterexample under --paths.
+
+int main(void)
+{
+  int x = 1;
+  int y = 9;
+
+  if(x > 0)
+  {
+    x = -5;
+    y = 7;
+  }
+
+  __CPROVER_assert(y == 7, "the branch is taken, so y is 7");
+
+  return 0;
+}

regression/cbmc/if-conversion-clobber/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+If-conversion must snapshot the branch condition before linearising a region,
+so that a guarded assignment does not re-read a variable that an earlier
+assignment in the same region has clobbered. Without the snapshot this test
+reports a spurious VERIFICATION FAILED under --paths.

regression/cbmc/if-conversion-deref/main.c

@@ -0,0 +1,20 @@
+// Soundness check for if-conversion: rewriting `if(p) x = *p;` into
+// `x = p ? *p : x` must keep the dereference guarded by the condition, so
+// that the NULL-pointer check does not fire on the path where the branch is
+// not taken. With p constrained to be NULL, the original program never
+// dereferences and verification succeeds; an unsound conversion that
+// evaluates `*p` unconditionally would report a spurious NULL dereference.
+
+int main(void)
+{
+  int *p;
+  __CPROVER_assume(p == (int *)0);
+
+  int x = 0;
+  if(p != (int *)0)
+    x = *p;
+
+  __CPROVER_assert(x == 0, "x is unchanged when p is NULL");
+
+  return 0;
+}

regression/cbmc/if-conversion-deref/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--paths lifo --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^\[main.pointer_dereference.\d+\] .*FAILURE$
+--
+Soundness of if-conversion: the dereference in `if(p) x = *p;` must stay
+guarded by `p != NULL` after being rewritten to a conditional expression, so
+no spurious NULL dereference is reported on the path where p is NULL. goto_check
+guards the operand checks of the generated `?:` by its condition, which this
+test confirms end-to-end under --paths.

regression/cbmc/if-conversion-paths/main.c

@@ -0,0 +1,49 @@
+// If-conversion linearises side-effect-free conditional assignments so that
+// --paths mode does not fork at them. The 16 independent conditional
+// assignments below would create 2^16 = 65536 symbolic-execution paths
+// without the transformation (timing out under the harness limit); with it
+// they become 16 branch-free guarded assignments and a single path remains.
+// Reverting the pass is therefore observable here as a timeout.
+
+int main(void)
+{
+  unsigned int cond; // nondeterministic
+  int g = 0;
+
+  if(cond & (1u << 0))
+    g = 1;
+  if(cond & (1u << 1))
+    g = 2;
+  if(cond & (1u << 2))
+    g = 3;
+  if(cond & (1u << 3))
+    g = 4;
+  if(cond & (1u << 4))
+    g = 5;
+  if(cond & (1u << 5))
+    g = 6;
+  if(cond & (1u << 6))
+    g = 7;
+  if(cond & (1u << 7))
+    g = 8;
+  if(cond & (1u << 8))
+    g = 9;
+  if(cond & (1u << 9))
+    g = 10;
+  if(cond & (1u << 10))
+    g = 11;
+  if(cond & (1u << 11))
+    g = 12;
+  if(cond & (1u << 12))
+    g = 13;
+  if(cond & (1u << 13))
+    g = 14;
+  if(cond & (1u << 14))
+    g = 15;
+  if(cond & (1u << 15))
+    g = 16;
+
+  __CPROVER_assert(g >= 0 && g <= 16, "g stays within bounds");
+
+  return 0;
+}

regression/cbmc/if-conversion-paths/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Side-effect-free conditional assignments are linearised by if-conversion so
+that --paths mode does not fork at them. Without the pass the 16 independent
+branches here fork into 2^16 paths and the test times out; with it a single
+path remains. This pins the optimisation against accidental removal.

regression/cbmc/path-branch-malloc-free/main.c

@@ -0,0 +1,39 @@
+#include <stdlib.h>
+
+// Each `free` call previously triggered two GOTO branches in the CPROVER
+// library bookkeeping (one in `free` itself for the memory-leak update and
+// one in `__CPROVER_deallocate` for the nondeterministic deallocation
+// tracking). Under `--paths lifo`, those branches multiplied the symex
+// state space by ~4 per call, so a handful of `malloc`/`free` pairs caused
+// exponential path explosion and reliably timed out before the bookkeeping
+// was rewritten as conditional expressions. With the rewrite this same
+// program runs in seconds; without it, ctest's 1200s per-profile timeout
+// is comfortably exceeded.
+int main(void)
+{
+  void *p0 = malloc(8);
+  void *p1 = malloc(8);
+  void *p2 = malloc(8);
+  void *p3 = malloc(8);
+  void *p4 = malloc(8);
+  void *p5 = malloc(8);
+  void *p6 = malloc(8);
+  void *p7 = malloc(8);
+  void *p8 = malloc(8);
+  void *p9 = malloc(8);
+  void *pA = malloc(8);
+
+  free(p0);
+  free(p1);
+  free(p2);
+  free(p3);
+  free(p4);
+  free(p5);
+  free(p6);
+  free(p7);
+  free(p8);
+  free(p9);
+  free(pA);
+
+  return 0;
+}

regression/cbmc/path-branch-malloc-free/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test pins down the CPROVER-library `--paths`-friendliness of `free` and
+`__CPROVER_deallocate`: the bookkeeping in those two functions used to emit
+GOTO branches that, under `--paths lifo`, multiplied the symex state space
+exponentially with the number of `free` calls. With those branches replaced
+by conditional expressions, this test runs in a handful of paths instead of
+4^N. Without the fix it would time out at the harness limit, so reverting
+the optimisation is observable here.

regression/cbmc/reachability-slice/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 test.c
 --no-standard-checks --reachability-slice --show-goto-functions --cover location --property foo.coverage.2
 ^EXIT=0$
@@ -9,3 +9,7 @@ test.c
 = 1005
 --
 We do not include 1002 and 1003, whether this is hit depends on where assertion is put
+
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+removes branches, which changes the --cover location output; the slicing
+behaviour under test is unaffected.

regression/cbmc/reachability-slice/test2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 test.c
 --no-standard-checks --reachability-slice-fb --show-goto-functions --cover location --property foo.coverage.2
 ^EXIT=0$
@@ -9,3 +9,7 @@ test.c
 = 1005
 --
 = 1004
+--
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+removes branches, which changes the --cover location output; the slicing
+behaviour under test is unaffected.

regression/cbmc/reachability-slice/test3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE paths-lifo-expected-failure
 test.c
 --reachability-slice --show-goto-functions --cover location
 ^EXIT=0$
@@ -10,3 +10,7 @@ test.c
 --
 --
 We do not include 1005 since it might or might not be present based on where the assertion is in the block.
+
+Tagged paths-lifo-expected-failure: under --paths the if-conversion pass
+removes branches, which changes the --cover location output; the slicing
+behaviour under test is unaffected.

scripts/check_help.sh

@@ -74,6 +74,7 @@ for t in  \
         -all-claims -all-properties -claim -show-claims \
         -document-subgoals \
         -no-propagation -no-simplify -no-simplify-if \
+        -no-if-conversion \
         -floatbv -no-unwinding-assertions \
         -slice-by-trace ; do
         echo "$undoc" >> help_string

src/analyses/local_safe_pointers.cpp

@@ -14,6 +14,8 @@ Author: Diffblue Ltd
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
 
 /// Return structure for `get_null_checked_expr` and
 /// `get_conditional_checked_expr`
@@ -74,6 +76,43 @@ static std::optional<goto_null_checkt> get_null_checked_expr(const exprt &expr)
   return {};
 }
 
+/// Collect dereferences that are guarded by a conditional null-check in
+/// `expr`, i.e. a dereference `*p` in the operand of `(p != null) ? ... : ...`
+/// (the true operand) or `(p == null) ? ... : ...` (the false operand) that is
+/// only evaluated when `p` is known to be non-null. Such conditional
+/// expressions are produced by if-conversion in place of `if(p != null) *p`.
+/// The collected dereferences are appended to `result`.
+static void
+collect_if_guarded_dereferences(const exprt &expr, std::vector<exprt> &result)
+{
+  if(const auto *if_expr = expr_try_dynamic_cast<if_exprt>(expr))
+  {
+    if(auto check = get_null_checked_expr(if_expr->cond()))
+    {
+      // The guarded operand is the one evaluated when the pointer is non-null.
+      const exprt &guarded_operand = check->checked_when_taken
+                                       ? if_expr->true_case()
+                                       : if_expr->false_case();
+      const exprt checked_pointer = skip_typecast(check->checked_expr);
+      for(auto it = guarded_operand.depth_begin(),
+               end = guarded_operand.depth_end();
+          it != end;
+          ++it)
+      {
+        if(
+          it->id() == ID_dereference &&
+          skip_typecast(to_dereference_expr(*it).pointer()) == checked_pointer)
+        {
+          result.push_back(*it);
+        }
+      }
+    }
+  }
+
+  for(const auto &op : expr.operands())
+    collect_if_guarded_dereferences(op, result);
+}
+
 /// Compute safe dereference expressions for a given GOTO program. This
 /// populates `non_null_expressions` mapping instruction location numbers
 /// onto a set of expressions that are known to be non-null BEFORE that
@@ -85,6 +124,22 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 
   for(const auto &instruction : goto_program.instructions)
   {
+    // Record dereferences guarded by a conditional null-check within this
+    // instruction (e.g. `(p != null) ? *p : x`, as produced by if-conversion).
+    // This is independent of the control-flow tracking below.
+    {
+      std::vector<exprt> guarded;
+      instruction.apply([&guarded](const exprt &e)
+                        { collect_if_guarded_dereferences(e, guarded); });
+      if(!guarded.empty())
+      {
+        auto &guarded_set =
+          if_guarded_dereferences[instruction.location_number];
+        for(auto &deref : guarded)
+          guarded_set.insert(std::move(deref));
+      }
+    }
+
     // Handle control-flow convergence pessimistically:
     if(instruction.incoming_edges.size() > 1)
       checked_expressions.clear();