Conditional points-to

[andreistefanescu]

Consider the get_rand_mod_len function that may write to *x_ptr and returns 1 if it does and 0 if it doesn't:

#include <stdint.h>
#include <stdlib.h>

uint32_t get_rand_mod_len(uint32_t *x_ptr, uint32_t len, uint32_t max_tries) {
  while (max_tries) {
    uint32_t x = rand();
    if (x < len) {
      *x_ptr = x;
      return 1;
    }
    --max_tries;
  }
  return 0;
}

Currently, saw does not support specifying the post-condition of this function. A possible solution would require something like crucible_conditional_points_to, and then the post-condition would look like:

ret <- crucible_fresh_var "ret" (llvm_int 32);
x <- crucible_fresh_var "x" (llvm_int 32);
crucible_postcond {{ ret == 0 \/ ret == 1 }};
crucible_postcond {{ ret == 1 ==> x < len }};
crucible_conditional_points_to {{ ret == 1 }} x_ptr (crucible_term x);
crucible_return (crucible_term ret);

Let's discuss what would be the best way to add support for this kind of specifications in saw.

cc @atomb @brianhuffman @robdockins @chameco

[weaversa]

I don't think the proposed crucible_conditional_points_to is a good idea since it acts like an if-then-else, without the else. Since x_ptr is not fully described, this function would fail when used as an override.

Maybe something like this, which has the else case, would be better:
crucible_conditional_points_to {{ predicate }} pointer (crucible_term thencase) (crucible_term elsecase).

[weaversa]

Below is a full run, if anyone else wants to play with it. I'm currently stuck on ambiguous collection of variables

let alloc_init ty v = do {
  p <- crucible_alloc ty;
  crucible_points_to p v;
  return p;
};

let ptr_to_fresh n ty = do {
  x <- crucible_fresh_var n ty;
  p <- alloc_init ty (crucible_term x);
  return (x, p);
};

let rand_spec = do {
  crucible_execute_func [];

  ret <- crucible_fresh_var "ret" (llvm_int 32);

  crucible_return (crucible_term {{ ret }});
};

let get_rand_mod_len_10_spec = do {
  (x_ptr, px_ptr) <- ptr_to_fresh "x_ptr" (llvm_int 32);

  len <- crucible_fresh_var "len" (llvm_int 32);

  crucible_execute_func [px_ptr, crucible_term {{ len }}, crucible_term {{ 10 : [32] }}];

  ret <- crucible_fresh_var "ret" (llvm_int 32);
  crucible_return (crucible_term ret);

  rand <- crucible_fresh_var "rand" (llvm_int 32);

  x_ptr' <- crucible_fresh_var "x_ptr'" (llvm_int 32);
  crucible_points_to px_ptr (crucible_term x_ptr');

  crucible_postcond {{ ret == 0 \/ ret == 1 }};
  crucible_postcond {{ if ret == 1 then (x_ptr' < len) && (x_ptr' == rand)
                                   else x_ptr' == x_ptr }};
};

test_bc <- llvm_load_module "test.bc";

rand_ov <- crucible_llvm_unsafe_assume_spec test_bc "rand" rand_spec;

get_rand_mod_len_10_ov <-
  crucible_llvm_verify test_bc "get_rand_mod_len" [rand_ov] true get_rand_mod_len_10_spec z3;

#include <stdint.h>
#include <stdlib.h>

uint32_t get_rand_mod_len(uint32_t *x_ptr, uint32_t len, uint32_t max_tries) {
  while (max_tries) {
    uint32_t x = rand();
    if (x < len) {
      *x_ptr = x;
      return 1;
    }
    --max_tries;
  }
  return 0;
}

$ clang -emit-llvm test.c -o test.bc -c -g && saw test.saw
[15:22:39.535] Loading file "test.saw"
[15:22:39.555] Assume override rand
[15:22:39.605] Verifying get_rand_mod_len ...
[15:22:39.607] Simulating get_rand_mod_len ...
[15:22:39.609] Registering overrides for `rand`
[15:22:39.609]   variant `Symbol "rand"`
[15:22:39.610] Matching 1 overrides of  rand ...
[15:22:39.610] Branching on 1 override variants of rand ...
[15:22:39.610] Applied override! rand
[15:22:39.614] Matching 1 overrides of  rand ...
[15:22:39.614] Branching on 1 override variants of rand ...
[15:22:39.614] Applied override! rand
[15:22:39.615] Matching 1 overrides of  rand ...
[15:22:39.615] Branching on 1 override variants of rand ...
[15:22:39.615] Applied override! rand
[15:22:39.616] Matching 1 overrides of  rand ...
[15:22:39.616] Branching on 1 override variants of rand ...
[15:22:39.616] Applied override! rand
[15:22:39.617] Matching 1 overrides of  rand ...
[15:22:39.617] Branching on 1 override variants of rand ...
[15:22:39.617] Applied override! rand
[15:22:39.618] Matching 1 overrides of  rand ...
[15:22:39.618] Branching on 1 override variants of rand ...
[15:22:39.618] Applied override! rand
[15:22:39.619] Matching 1 overrides of  rand ...
[15:22:39.619] Branching on 1 override variants of rand ...
[15:22:39.619] Applied override! rand
[15:22:39.620] Matching 1 overrides of  rand ...
[15:22:39.620] Branching on 1 override variants of rand ...
[15:22:39.620] Applied override! rand
[15:22:39.621] Matching 1 overrides of  rand ...
[15:22:39.621] Branching on 1 override variants of rand ...
[15:22:39.621] Applied override! rand
[15:22:39.622] Matching 1 overrides of  rand ...
[15:22:39.622] Branching on 1 override variants of rand ...
[15:22:39.622] Applied override! rand
[15:22:39.623] "crucible_llvm_verify" (test.saw:46:3-46:23):
at test.saw:46:3
ambiguous collection of variables
  rand : [32]

[brianhuffman]

Instead of

crucible_conditional_points_to : Term -> SetupValue -> SetupValue -> CrucibleSetup ()

perhaps it would be better to have a more general-purpose conditional construct

crucible_conditional : Term -> CrucibleSetup () -> CrucibleSetup () -> CrucibleSetup ()

where you could have a separate setup block in each branch of the conditional. I think this would be expressive enough to handle all the use cases we might want. I expect it would be rather challenging to implement, but I haven't thought very hard yet about an implementation would work.

Thoughts?

[andreistefanescu]

@weaversa thank you for the feedback, and for taking the time to try out an example!

This is the specification I have in mind for get_rand_mod_len:

let rand_spec = do {
  crucible_execute_func [];

  ret <- crucible_fresh_var "ret" (llvm_int 32);
  crucible_return (crucible_term ret);
};

let get_rand_mod_len_10_spec = do {
  x_ptr <- crucible_alloc (llvm_int 32);
  len <- crucible_fresh_var "len" (llvm_int 32);

  crucible_execute_func [x_ptr, (crucible_term len), (crucible_term {{ 10 : [32] }})];

  ret <- crucible_fresh_var "ret" (llvm_int 32);
  crucible_return (crucible_term ret);

  rand <- crucible_fresh_var "rand" (llvm_int 32);
  crucible_conditional_points_to {{ ret == 1 }} x_ptr (crucible_term rand);

  crucible_postcond {{ ret == 0 \/ ret == 1 }};
  crucible_postcond {{ ret == 1 ==> rand < len }};
};

Basically, the specification treats x_ptr as an write-only parameter, and does not require it to be initialized before the call to get_rand_mod_len. This specification is required if the caller uses get_rand_mod_len to initialize a variable, for example:

uint32_t foo()
{
  uint32_t x;
  if (0 == get_rand_mod_len(&x, 256, 10))
  {
    return 0;
  }
  // use x
}

Separately, a crucible_if_then_else_points_to with both a then branch and an else branch would be required if a function conditionally writes values with different Cryptol types. This could be achieved by multiple crucible_conditional_points_to statements, but this is not yet supported.

[andreistefanescu]

@brianhuffman I like you proposal, it would cover all cases discussed here. Implementing it, on the other hand, would take some more effort. The conditional blocks could be nested, and one would have to consider the effects of the condition all statements, not just crucible_points_to.

[brianhuffman]

I think we can consider this issue closed by #657, as the llvm_conditional_points_to command has now been in use for some time.