uninterpreted constants

[msaaltink]

There are some difficulties in doing proofs while trying not to expand a cryptol constant. (I might want to do this because, say, the exact value of the constant is immaterial and I want the proof to reflect that.) For example, with this C code

#include <stdint.h>

uint8_t c[3] = {1,2,3};

void foo(uint8_t p[3]) {
  int i;
  for(i=0;i<3;i++) p[i] =i+1; // {p[i]=c[i];}
}

uint8_t bar(uint8_t p[3]) {
  return p[1];
}

uint8_t baz() {
  uint8_t p[3];
  foo(p);
  return bar(p);
}

and this saw-script

m <- llvm_load_module "const.bc";

let {{ c = [1, 2, 3]:[3][8]
     f: [3][8] -> [8]
     f [_,x,_] = x }};

let ty = llvm_array 3 (llvm_int 8);

let foo_spec = do {
  pp <- crucible_alloc ty;
  crucible_execute_func [pp];
  crucible_points_to pp (crucible_term {{ c }});
  };

p_foo <- crucible_llvm_verify m "foo" [] false foo_spec yices;

let bar_spec = do {
  pp <- crucible_alloc ty;
  p <- crucible_fresh_var "p" ty;
  crucible_points_to pp (crucible_term p);
  crucible_execute_func [pp];
  crucible_return (crucible_term {{ f p }});
  };

p_bar <- crucible_llvm_verify m "bar" [] false bar_spec yices;

let baz_spec = do {
  crucible_execute_func [];
  crucible_return (crucible_term {{ f c }});
  };

we can complete proofs if nothing's uninterpreted:

crucible_llvm_verify m "baz" [] false baz_spec yices;
crucible_llvm_verify m "baz" [p_foo, p_bar] false baz_spec yices;

If we try to not expand f and c, the proof fails.

crucible_llvm_verify m "baz" [p_foo, p_bar] false baz_spec (unint_yices ["f", "c"]);

Printing the goal shows why,

crucible_llvm_verify m "baz" [p_foo, p_bar] false baz_spec
    (do {print_goal; offline_unint_smtlib2 ["f", "c"] "const-vcs";});

shows

Goal baz (safety assertion: literal equality postcondition):
Prelude.EqTrue
  (Prelude.implies Prelude.True
    (Prelude.implies Prelude.True
      (Prelude.eq (Prelude.Vec 8 Prelude.Bool) (Prelude.bvNat 8 2)
         (f c))))

That (Prelude.bvNat 8 2) must have come from either the overrides not kicking in, or something expanding out when they did. The smtlib2 output is equally clear in this regard, but as can be seen it is already too late for the proof script to keep things unfolded.

A function that just calls bar can keep f unfolded, but a caller of foo apparently always sees the expansion of c; if we add this C function

void foo2(uint8_t p[3]) {
  foo(p);
}

and the saw-script

crucible_llvm_verify m "foo2" [p_foo] false foo_spec (do {print_goal; assume_unsat;});

we can see that after the call, the constant was already expanded:

Goal foo2 (safety assertion: literal equality postcondition):
let { x@1 = Prelude.bitvector 8
  }
 in Prelude.EqTrue
    (Prelude.implies Prelude.True
       (Prelude.implies Prelude.True
         (Prelude.eq (Prelude.Vec 3 x@1)
            [Prelude.bvNat 8 1,Prelude.bvNat 8 2,Prelude.bvNat 8 3]
            c)))

Is there any work-around for this?

[robdockins]

I'm trying to reproduce this issue, but I think the behavior here has changed enough that I can't quite get into the situation as described here. @msaaltink, are you still experiencing issues in this area?

[msaaltink]

This has not come up in anything I've worked on in the past while. I think I did see something like this last fall, when it appeared that any closed Cryptol expression in the pre- or postconditions of a called routine would be fully evaluated during simulation, but I don't think it became a problem.

[robdockins]

OK, I'll close this then. Controlling the degree of evaluation and unfolding is part of a larger batch of work I think we'll need to do soonish, however.