llvm_field doesn't work as expected when passed to llvm_execute_func

[RyanGlScott]

If I have the following files:

// llvm_field.c

#include <stdint.h>

struct s {
  uint8_t *t;
};

uint8_t f(const struct s *ss, const uint8_t *tt) {
  return (*ss->t + *tt);
}

// llvm_field.saw

let f_spec = do {
  ss <- llvm_alloc_readonly (llvm_alias "struct.s");
  tt_var <- llvm_fresh_var "t" (llvm_int 8);
  tt <- llvm_alloc_readonly (llvm_int 8);
  llvm_points_to tt (llvm_term tt_var);
  llvm_points_to (llvm_field ss "t") tt;

  llvm_execute_func [ss, tt];
  // llvm_execute_func [ss, llvm_field ss "t"];

  llvm_return (llvm_term {{ 2*tt_var : [8] }});
};

m <- llvm_load_module "llvm_field.bc";
llvm_verify m "f" [] true f_spec abc;

Then f_spec will verify, as expected:

$ clang-10 -g -emit-llvm -c llvm_field.c 
$ ~/Software/saw-0.8/bin/saw llvm_field.saw


[13:56:20.299] Loading file "/home/rscott/Documents/Hacking/SAW/llvm_field.saw"
[13:56:20.343] Verifying f ...
[13:56:20.361] Simulating f ...
[13:56:20.370] Checking proof obligations f ...
[13:56:20.421] Proof succeeded! f

However, if I change the llvm_execute_func line to use llvm_field, like so:

-  llvm_execute_func [ss, tt];
+  llvm_execute_func [ss, llvm_field ss "t"];

Then the proof will no longer work:

$ ~/Software/saw-0.8/bin/saw llvm_field.saw


[13:59:23.836] Loading file "/home/rscott/Documents/Hacking/SAW/llvm_field.saw"
[13:59:23.856] Verifying f ...
[13:59:23.856] Simulating f ...
[13:59:23.857] Checking proof obligations f ...
[13:59:23.877] Subgoal failed: f safety assertion:
llvm_field.c:10:20: error: in f
Error during memory load

[13:59:23.880] SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 25}
[13:59:23.880] ----------Counterexample----------
[13:59:23.880] <<All settings of the symbolic variables constitute a counterexample>>
[13:59:23.880] ----------------------------------
[13:59:23.880] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/SAW/llvm_field.saw:17:1-17:12):
Proof failed.

I find this rather strange, since I would have expected llvm_field ss "t" to be equivalent to tt. This isn't a huge deal, since I can always use tt instead, but I found it strange nonetheless.

I originally encountered this in a context where ss is computed by an auxiliary SAW function, so I had to do a fair bit of plumbing to get the auxiliary function to return its equivalent of tt. I could have avoided this extra plumbing if llvm_field ss "t" worked as expected.

[atomb]

The difference here is that llvm_field ss "t" is the address of field t, whereas tt is the value stored at that address (although it is, itself, also a pointer).

[RyanGlScott]

Ah, I see. I'll close this then.