Verfying a function with a while loop using llvm_assert never finishes

[ttaubert]

Assume a function with a loop:

typedef struct {
    uint8_t len;
} str;

uint8_t test(str* s) {
    while (s->len-- > 0);
    return 0;
}

One might be able to reproduce without the struct, but due to #106 I can't use llvm_assert_eq with an argument. Now here's the SAW code to verify that function with s->len = 1:

llvm_verify m "test" [] do {
    llvm_ptr "s" (llvm_struct "struct.str");
    len <- llvm_var "s->0" (llvm_int 8);
    llvm_sat_branches true;
    llvm_assert {{ len == 1 }};
    llvm_return {{ 0:[8] }};
    llvm_verify_tactic abc;
};

It seems to loop forever, at least doesn't finish in an appropriate amount of time. It does however finish very fast when you replace llvm_assert {{ len == 1 }} with llvm_assert_eq "s->0" {{ 1:[8] }}. It seems like those two shouldn't yield a behavior that different, right?

Trying to verify the function's behavior for llvm_assert {{ len > 0 }} doesn't finish either. I hope that might be fixed as well with this issue as there's no way to define this assertion with llvm_assert_eq.

[ttaubert]

Also puzzling is that llvm_verify_tactic (quickcheck 10) never finishes either. I would've expected to be able to use this while the issue exists.

[atomb]

At the moment, llvm_assert creates pre-conditions that are used during verification but not symbolic execution, leading to this behavior, while llvm_assert_eq actually changes the symbolic state. Although this is the "intended" behavior in some sense, I think we're seeing enough cases where assertions are important for termination (or safety) to suggest that it's not the right behavior.

The reason for the quickcheck behavior you're seeing is that the random testing occurs on the model of the program, after symbolic execution, not directly on the C code. So if symbolic execution doesn't terminate, the random testing never runs.

[atomb]

This works correctly with crucible_llvm_verify.