SAW and function pointers

While entertaining an effort to verify C code with function pointers (which I suspect cannot be expressed in SAWScript), I encountered some notable behaviors. Consider the following, for which I don't see how SAWScript could verify the calc function:

// funpoint.c

#include "stddef.h"
#include "stdint.h"

typedef uint32_t (* pbf_u32)(uint32_t, uint32_t);

uint32_t dft(uint32_t a, uint32_t b) { return a ^ b ^ b ^ a; }

uint32_t add(uint32_t a, uint32_t b) { return a + b; }
uint32_t sub(uint32_t a, uint32_t b) { return a - b; }
uint32_t mul(uint32_t a, uint32_t b) { return a * b; }
uint32_t dvd(uint32_t a, uint32_t b) { return b == 0 ? 0 : a / b; }
uint32_t mod(uint32_t a, uint32_t b) { return b == 0 ? 0 : a % b; }

const pbf_u32 OPS[] = { add, sub, mul, dvd, mod };
const size_t LEN_OPS = sizeof(OPS) / sizeof(OPS[0]);

uint32_t calc(uint32_t a, uint32_t b, size_t i) {
  pbf_u32 op = (i >= LEN_OPS) ? dft : OPS[i];

  return op(a, b);
}

$ clang -g -c -emit-llvm funpoint.c -o funpoint.bc
$ saw
sawscript> funpoint_bc <- llvm_load_module "funpoint.bc";
sawscript> enable_experimental
sawscript> llvm_boilerplate "funpoint.saw" funpoint_bc []
saw: BPException "Unsupported type FunTy (PrimType (Integer 32)) [PrimType (Integer 32),PrimType (Integer 32)] False"
$

Not surprisingly, llvm_boilerplate throws an exception when encountering the function pointer array. Uncaught, this exception crashes SAW. Proceeding with a manually generated SAW script:

// funpoint.saw
let size_t = llvm_int 64;
let uint32_t = llvm_int 32;

let {{
  type size_t = [64]

  OPS = [(+), (-), (*), (/), (%)]
  [ADD, SUB, MUL, DVD, MOD] = take [0...] :[_]size_t
}};

let add_setup = do {
  a <- crucible_fresh_var "a" uint32_t;
  b <- crucible_fresh_var "b" uint32_t;
  crucible_execute_func [crucible_term a, crucible_term b];
  crucible_return (crucible_term {{ a + b }});
};
// ...
calc_setup = do {
  a <- crucible_fresh_var "a" uint32_t;
  b <- crucible_fresh_var "b" uint32_t;
  i <- crucible_fresh_var "i" size_t;// `length OPS` throws an error from `Verifier.SAW.Simulator.toBool`, crashing out of SAW

  // `length OPS` throws an error from `Verifier.SAW.Simulator.toBool`, crashing out of SAW
  crucible_precond {{ i < (if b == 0 then DVD else MOD + 1) }};
  crucible_execute_func [crucible_term a, crucible_term b, crucible_term i];
  crucible_return (crucible_term {{ (OPS@i) a b }});
};

let main = do {
  funpoint_bc <- llvm_load_module "funpoint.bc";

  add_method_spec <- crucible_llvm_verify funpoint_bc "add" [] false add_setup z3;
  // ...

  // requires about 27s to complete
  calc_method_spec <- crucible_llvm_verify funpoint_bc "calc"
    [ add_method_spec, sub_method_spec, mul_method_spec
    , dvd_method_spec, mod_method_spec ] false calc_shim_setup z3;

  print "Verified `funpoint_shim.c`!";
};

$ saw funpoint.saw
[22:38:40.053] Loading file ".../funpoint.saw"
...
[22:38:40.546] Verifying calc ...
[22:38:40.551] Simulating calc ...
[22:38:40.552] Registering overrides...
[22:38:40.553] "crucible_llvm_verify" (.../funpoint.saw:69:23-69:43):
Symbolic execution failed.
Abort due to false assumption:
  Cannot resolve a symbolic pointer to a function handle:
...
$

Another crash out of SAW. Undeterred, suppose we continue with an attempt to verify an adaptation of funpoint.c, with comments indicating crashes and examples of code variations that SAWScript cannot verify:

// funpoint_shim.c

// add, sub, etc. defined as before

typedef enum op { ADD = 0, SUB, MUL, DVD, MOD } op_t;

uint32_t calc_shim(uint32_t a, uint32_t b, op_t i) {
  pbf_u32 op;
  uint32_t r;

  switch (i) {
  case ADD: op = add; r = op(a,b); break;
  case SUB: op = sub; r = op(a,b); break;
  case MUL: op = mul; r = op(a,b); break;
  case DVD: op = dvd; r = op(a,b); break;
  case MOD: op = mod; r = op(a,b); break;
  default:  op = dft; r = op(a,b); break;  // below error occurs with or without `default` case
  }

  // throws a symbolic execution error
  // "Abort due to false assumption:
  //    Cannot resolve a symbolic pointer to a function handle"
  /* r = op(a,b); */

  return r;
}

let op_t = llvm_int 32;
let uint32_t = llvm_int 32;

let {{
  type op_t = [32]

  OPS = [(+), (-), (*), (/), (%)]
  [ADD, SUB, MUL, DVD, MOD] = take [0...] :[_]op_t
}};

let add_setup = do {
  a <- crucible_fresh_var "a" uint32_t;
  b <- crucible_fresh_var "b" uint32_t;
  crucible_execute_func [crucible_term a, crucible_term b];
  crucible_return (crucible_term {{ a + b }});
};
// ...
let calc_shim_setup = do {
  a <- crucible_fresh_var "a" uint32_t;
  b <- crucible_fresh_var "b" uint32_t;
  i <- crucible_fresh_var "i" op_t;

  // replacing `MOD + 1` with `length OPS` throws an error from `Verifier.SAW.Simulator.toBool`, crashing out of SAW
  crucible_precond {{ i < (if b == 0 then DVD else MOD + 1) }};
  crucible_execute_func [crucible_term a, crucible_term b, crucible_term i];
  crucible_return (crucible_term {{ (OPS@i) a b }});
};

let main = do {
  funpoint_bc <- llvm_load_module "funpoint_shim.bc";

  add_method_spec <- crucible_llvm_verify funpoint_bc "add" [] false add_setup z3;
  sub_method_spec <- crucible_llvm_verify funpoint_bc "sub" [] false sub_setup z3;
  mul_method_spec <- crucible_llvm_verify funpoint_bc "mul" [] false mul_setup z3;
  dvd_method_spec <- crucible_llvm_verify funpoint_bc "dvd" [] false dvd_setup z3;
  mod_method_spec <- crucible_llvm_verify funpoint_bc "mod" [] false mod_setup z3;

  // requires about 27s to complete
  calc_shim_method_spec <- crucible_llvm_verify funpoint_bc "calc_shim"
    [ add_method_spec, sub_method_spec, mul_method_spec
    , dvd_method_spec, mod_method_spec ] false calc_shim_setup z3;

  print "Verified `funpoint_shim.c`!";
};

The altered implementation requires about 27 seconds to verify. If we defer r = op(a, b) from each case to after the switch statement, the (symbolic) pointer cannot be resolved. If we change the calc_shim precondition from i < (if b == 0 then DVD else MOD + 1) to i < (if b == 0 then DVD else length OPS), SAW fails to convert the Boolean and crashes.

I've uploaded example files here: funpoint.zip

GaloisInc / saw-script

SAW and function pointers #579