Path satisfiability checking is not working

[weaversa]

I challenge anyone to find an example where setting the flag to true does something other than slow down symbolic execution. A simple example of this failure in action is attached.

gcd.tar.gz

#include <stdint.h>
#include <stdio.h>

uint8_t gcd(uint32_t depth, uint8_t a, uint8_t b) {
  printf("depth = %u\n", depth);
  if(b == 0)
    return a;
  return gcd(depth+1, b, a%b);
}

let gcd_spec = do {
  a <- crucible_fresh_var "a" (llvm_int 1);
  b <- crucible_fresh_var "b" (llvm_int 1);

  crucible_execute_func [crucible_term {{ 0 : [32] }}, crucible_term {{ 0 # a : [8] }}, crucible_term {{ 0 # b : [8] }}];
};

m <- llvm_load_module "gcd.bc";
crucible_llvm_verify m "gcd" [] false gcd_spec z3;
crucible_llvm_verify m "gcd" [] true gcd_spec z3;

$ tar -xzvf gcd.tar.gz
$ cd gcd
$ saw gcd.saw
[01:23:42.225] Loading file "gcd.saw"
[01:23:42.291] Verifying gcd ...
[01:23:42.292] Simulating gcd ...
depth = 0
depth = 1
depth = 2
depth = 3
depth = 4
...
depth = 253
depth = 254
depth = 255
[01:23:42.523] Checking proof obligations gcd ...
[01:23:50.835] Proof succeeded! gcd
[01:23:50.895] Verifying gcd ...
[01:23:50.897] Simulating gcd ...
depth = 0
depth = 1
depth = 2
depth = 3
depth = 4
...
depth = 253
depth = 254
depth = 255
[01:25:22.127] Checking proof obligations gcd ...
[01:25:30.441] Proof succeeded! gcd

Less than a second to symbolically execute with false, a minute an a half for true.

[weaversa]

Incidentally, it is kind of strange that the example above stops at all. Why does saw stop at depth = 255?

[robdockins]

In this case, I'm pretty sure this terminates due to arithmetic interval information. At each step the modulus operation reduces the arithmetic interval by 1; this eventually drive the interval down to 0 and the loop terminates.

The theoretical upper bound on the number of gcd calls required is rather less than that, I think, but it probably relies on nonlinear arithmetic to discover; I'm not surprised path sat checking doesn't help here.

[weaversa]

The recursion depth for an n-bit GCD is the nth fIbonacci number.

[weaversa]

However, the recursion depth of the proof above is 1, since only the low bit of each input is symbolic.

[robdockins]

OK, yeah, something very weird is going on with SAW's path sat checking. Running the following program through crux with path sat checking on only counts up to depth = 12 iterations, which is the actual worst case, I think.

#include <stdint.h>
#include <stdio.h>
#include <crucible.h>

uint8_t gcd(uint32_t depth, uint8_t a, uint8_t b) {
  printf("depth = %u\n", depth);
  if(b == 0)
    return a;
  return gcd(depth+1, b, a%b);
}


int main ( )
{
  uint8_t a = crucible_uint8_t( "a" );
  uint8_t b = crucible_uint8_t( "b" );

  uint8_t x = gcd( 0, a, b);

  printf( "%d\n", x );
  return 0;
}

[weaversa]

This is the first breaking nightly --- https://saw.galois.com/builds/nightly/saw-0.2-2018-12-13-MacOSX-64.tar.gz

This one works --- https://saw.galois.com/builds/nightly/saw-0.2-2018-12-06-MacOSX-64.tar.gz

$ saw-0.2-2018-12-06-MacOSX-64/bin/saw gcd.saw 
Loading file "gcd.saw"
depth = 0
depth = 1
Proof succeeded! gcd

Unfortunately there's a weeklong gap between the two nightlies. :-(

[robdockins]

As far as I can tell, this problem stems from GaloisInc/crucible@d429bcb. At around this time, SAW satisfiability checking was moved to use the "path satisfiability" feature. However, the IsBoolSolver implementation for the SAWCore backend does not communicate with the connected solver to update path conditions; it merely asks for satisfiability of the given condition in isolation.

We need to do the same solver communication steps as are done in the crucible OnlineBackend. As a quick fix we can probably just copy/paste the implementation of the relevant methods. However, we should really find a good way to share the relevant implementation.

[robdockins]

Fixed via #873