Unsound compositional proof

[msaaltink]

I'm getting an unsound result from a composite proof of this simple code:

#include <stdint.h>

uint32_t side_effect(uint32_t *a) {
  uint32_t v;
  v = *a;
  *a = 0;
  return v;
}

uint32_t foo(uint32_t x) {
  uint32_t b = x;
  side_effect(&b);
  return side_effect(&b);
}

Here's the SAWscript:

c <- llvm_load_module "side.bc";

let side_spec = do {
  a <- llvm_ptr "a" (llvm_int 32);
  llvm_return {{ a }};
  llvm_ensure_eq "*a" {{ 0:[32] }};
  llvm_verify_tactic abc;
  };

side_proof <- llvm_verify c "side_effect" [] side_spec;

let foo_spec = do {
  x <- llvm_var "x" (llvm_int 32);
  llvm_return {{ x }};
  llvm_verify_tactic abc;
  };

bad <- llvm_verify c "foo" [side_proof] foo_spec;

This supposed proof works fine in the latest saw-script interpreter. Oddly enough, a non-compositional proof knows the righty answer:

foo_fn <- llvm_extract c "foo" llvm_pure;
prove_print abc {{\x -> foo_fn x == 0}};

[atomb]

This is fixed in 43cc206. The code to override functions based on previous proofs had an embarrassing bug: it completely ignored state changes made by the overridden function, propagating only the return value. It's no longer quite so broken.

[msaaltink]

Not quite so broken, yes, but still broken. Consider this small change to the example, where one of the effects is commented out of the first specification:

c <- llvm_load_module "side.bc";

let part_side_spec = do {
  a <- llvm_ptr "a" (llvm_int 32);
  llvm_return {{ a }};
  // llvm_ensure_eq "*a" {{ 0:[32] }};
  llvm_verify_tactic abc;
  };

side_proof <- llvm_verify c "side_effect" [] part_side_spec;

Fine so far, that's a true fact, albeit an incomplete description. It can be used unsoundly:

let foo_spec = do {
  x <- llvm_var "x" (llvm_int 32);
  llvm_return {{ x }};
  llvm_verify_tactic abc;
  };

bad <- llvm_verify c "foo" [side_proof] foo_spec;

Typically, specifications for called routines will need to make some honest statement about what they can modify, but this is missing here.

[atomb]

This is a known issue which should have already had its own ticket. I believe I'd mentioned it to you in earlier discussions, @msaaltink. Apologies if I didn't.

One of the key reasons for a formalization of what these specifications mean is that, for the memory model used by the LLVM simulator, it's unclear exactly what we need to check to ensure that functions do not have effects beyond what's specified.

[langston-barrett]

I'm not sure if this would fix all instances of this unsoundness, but a first approximation might be: For each variable (global, parameter, etc.) appearing in a precondition, unless it's value is also uniquely determined by a postcondition*, creating a new postcondition stating that it's value doesn't change.

It might be best if the SAW manual included a note about this for 0.3.

*This is probably the challenging bit.