Crucible/LLVM: Override matching branches on concrete bitvector equalities

[langston-barrett]

Summary

When using multiple overrides for the same function, SAW/Crucible is branching on more of them than necessary/what I would expect. In particular, if you have two overrides for the same function that pass some literal integer as an argument, SAW will branch and follow both of them, instead of realizing that one is infeasible.

The two big disadvantages here are performance and error messages. When symbolic simulation fails on both paths, the user might have a hard time distinguishing which path was actually feasible.

Example

Here's an example C program and SAW spec, tarball attached below.

#include "stdlib.h"
#include "string.h"

unsigned f(unsigned *xs, unsigned size) {
  memset(xs, size, 1);
  return size;
}

unsigned g(unsigned size) {
  unsigned *xs = malloc(size * sizeof(unsigned));
  if (size == 32) {
    return f(xs, size);
  }
  return 0;
}

let f_spec (size : Int) : CrucibleSetup () = do {
  pointer_to_xs <- crucible_alloc (llvm_array size (llvm_int 32));
  crucible_precond {{ `size > (0 : [32]) }};
  crucible_precond {{ `size < (512 : [32]) }};
  crucible_execute_func [pointer_to_xs, crucible_term {{ `size : [32] }}];
  crucible_return (crucible_term {{ `size : [32] }});
};

let g_spec : CrucibleSetup () = do {
  crucible_execute_func [crucible_term {{ 32 : [32] }}];
  crucible_return (crucible_term {{ 32 : [32] }});
};

let main : TopLevel () = do {
  m <- llvm_load_module "test.bc";
  f_32_ov <- crucible_llvm_verify m "f" [] false (f_spec 32) z3;
  f_42_ov <- crucible_llvm_verify m "f" [] false (f_spec 42) z3;
  crucible_llvm_verify m "g" [f_32_ov, f_42_ov] false g_spec z3;
  print "done";
};

When run with a variant of #540 that shows the arguments for each override call, the log shows:

[17:32:28.244] Loading file "/home/siddharthist/code/tmp/symbolic-branch/test.saw"
[17:32:28.349] Verifying f ...
[17:32:28.357] Simulating f ...
[17:32:28.363] Checking proof obligations f ...
[17:32:28.383] Proof succeeded! f
[17:32:28.452] Verifying f ...
[17:32:28.459] Simulating f ...
[17:32:28.462] Checking proof obligations f ...
[17:32:28.488] Proof succeeded! f
[17:32:28.510] Verifying g ...
[17:32:28.516] Simulating g ...
[17:32:28.516] Registering overrides for `f`
[17:32:28.516]   variant `f`
[17:32:28.518] Matching 2 overrides of  f ... Arguments:
 - concrete pointer: allocation = 8, offset = 0
- literal integer: unsigned value = 32, signed value =  32, width = 32
[17:32:28.521] Branching on 2 override variants of f ...
[17:32:28.545] Applied override! f
[17:32:28.545] Symbolic simulation completed with side conditions.
[17:32:28.547] Checking proof obligations g ...
[17:32:28.611] Proof succeeded! g
[17:32:28.611] done

You can see that the Crucible value being passed to the override is definitely a concrete integer, and that SAW is branching on both overrides, instead of just the one that should match.

test.tar.gz

Possible code path

What's should be happening here is partitionOWPsConcrete should sort the erroneous override into the "concretely failing" bin. The What4.Interface.Pred that it's examining comes from methodSpecHandler_prestate, and more specifically, the assertion corresponding to the argument's value should come from the first case of matchArg. So what might be happening is that somewhere along the valueToSC/matchTerm/scEq/resolveSAWPred call chain, the concreteness is being lost/forgotten/left unused, and the What4.Interface.Pred you get out at the end is not concrete.

[robdockins]

I thought this would be fixed by #887, but apparently it was fixed already at some earlier time. I can't reproduce this behavior, master SAW reports only branching on 1 override.