SAW handles calls to the same unint function as separate functions

[TomMD]

Consider the C code that says g(x)-g(x) == 0. (N.B. simpler claims such as g x = g x also exhibit the same issue as shown below)

extern int g(int);
int test(int x) { return ((g(x) - g(x)) == 0); }

Using the saw script:

v1 <- llvm_load_module "the.bc";
let v2 =
    do {
        v3 <- llvm_var "args[0]" (llvm_int 32);
        llvm_return_arbitrary;
        llvm_no_simulate;
    };
v4 <- llvm_verify v1 "g" [] v2;
let v5 =
    do {
        v6 <- llvm_var "args[0]" (llvm_int 32);
        llvm_verify_tactic abc;
        llvm_return {{1 : [32]}};
    };
v7 <- llvm_verify v1 "test" [v4] v5;

The clang and saw commands:

clang -c -emit-llvm the.c -o the.bc && saw the.saw

The result:

Loading module Cryptol
Loading file "/private/tmp/the.saw"
WARNING: skipping simulation of @g
When verifying @test:
Proof of return value failed.
Counterexample:
  lss__return_g: 4294967295
  lss__return_g: 0
return value
Encountered:  0
Expected:     1
saw: user error ("llvm_verify" (/private/tmp/the.saw:15:7):
Proof failed.)

As the title says, I believe the two separate calls to g are being treated as separate uninterpreted functions. I have not examined what is being delivered to the solver (is there a flag for that?).

[atomb]

Perhaps it's something that needs to be better documented, but the behavior of llvm_return_arbitrary isn't exactly the same as an uninterpreted function. It's intended especially to be used in cases where we don't know, don't care, or can't even refer to the mechanism by which the return value is derived (as might be the case for I/O functions). So we don't require that the user has specified all possible inputs to the function, and therefore we can't guarantee that the real code will always return the same result given the same actual parameters.

To treat g as being modeled by an uninterpreted function of its argument, you could use llvm_return {{ f v3 }}, where f is some function that either has no definition or an ignored definition. Then you can use unint_z3 ["f"] as the verification tactic to indicate that f should be treated as uninterpreted.

[TomMD]

Thanks!