termination and order of conditions

[msaaltink]

Consider this code:

#include <stdint.h>

uint64_t g1(uint64_t x) {
  int i = 0;
  uint64_t r = x;
  do {
    r = r+1;
  } while ( i++ < 3 && r == 0 );
  return r;
}

uint64_t g2(uint64_t x) {
  int i = 0;
  uint64_t r = x;
  do {
    r = r+1;
  } while ( r == 0 && i++ < 3 );
  return r;
}

Both g1 and g2 are guaranteed to terminate. If we try a simple proof in SAW:

m <- llvm_load_module "termination.bc";

let g_spec = do {
  x <- crucible_fresh_var "x" (llvm_int 64);
  crucible_execute_func [crucible_term x];
  };

crucible_llvm_verify m "g1" [] false g_spec z3;

crucible_llvm_verify m "g2" [] false g_spec z3;

the verification of g1 completes, while for g2 the simulator never stops.

Some simple variation makes the problem disappear. For example, if the increment of i is moved in the
loop, then both proofs work.

[atomb]

If you set the fourth argument to crucible_llvm_verify to true in both cases, do they both terminate?

[weaversa]

If you set the fourth argument to crucible_llvm_verify to true in both cases, do they both terminate?

Isn’t that still broken? See #723

[robdockins]

Humm, yeah g2 is interesting. I can see why the simulator would have trouble with that. I'd expect SAT branch checking to fix the issue, but as @weaversa mentions, that feature has some sort of bug that I need to track down.

[robdockins]

Follow up: compiling g2 with -O1 apparently does enough code motion that the simulator terminates. With crux-llvm I can get g2 to terminate using -O0 provided path-sat checking is enabled, which is what I would expect.

So, simulator path-sat checking does work, there's just something weird about the integration with SAW. This is consistent with what we were seeing in #723. Interestingly, I can see that the simulator is communicating with the solver during simulation (via top), so the feature is enabled and doing something; but it's not clear why it isn't properly pruning branches.

[robdockins]

Following #873, and with path satisfiability checking enabled, the simulator now promptly terminates on g2.