SAT branches not working?

[weaversa]

#include <stdint.h>

uint32_t f(uint32_t n) {
  uint32_t i, x = 0;
  for(i = 0; i < n; i++) {
    x++;
  }
  return x;
}

let f_spec = do {
  n <- crucible_fresh_var "n" (llvm_int 32);

  crucible_precond {{ n == 0 }};

  crucible_execute_func [ crucible_term n ];

  crucible_return (crucible_term {{ n }});
};

test_bc <- llvm_load_module "test.bc";

f_result <- crucible_llvm_verify test_bc "f" [] true f_spec z3;

clang -O0 test.c -o test.bc -emit-llvm -c && saw test.saw          
[13:57:04.986] Loading file "test.saw"
[13:57:05.029] Verifying f ...
[13:57:05.029] Simulating f ...

And this seems to run forever. Isn't the SAT branches argument supposed to force the simulator to call yices at conditional branches? I feel like this is similar, but more general than GaloisInc/crucible#468

[robdockins]

The reason is different, but it is related to the secondary issue we discussed in GaloisInc/crucible#468. Basically, we are not currently exposing the structure of SAW assertions to the crucible level, which is where path SAT checking happens. This is a relic from days before we had code available to evaluate SAWCore terms into What4.

I just took a minute to look into this, and I think it would be less work than I expected to do better here. There are relatively few places where bindSAWTerm occurs that would need to be replaced with code that actually evaluates the terms.

[weaversa]

Just here to say that this feature used to exist, see #121. Also, I tried using crucible_equal and the new enable_crucible_assert_then_assume, but no luck. What does this new command do?

let f_spec = do {
  n <- crucible_fresh_var "n" (llvm_int 32);

  crucible_equal (crucible_term n) (crucible_term {{ 0 : [32] }});

  crucible_execute_func [ crucible_term n ];

  crucible_return (crucible_term {{ n }});
};

test_bc <- llvm_load_module "test.bc";

enable_crucible_assert_then_assume;
f_result <- crucible_llvm_verify test_bc "f" [] true f_spec z3;

[robdockins]

Fixed via #873