WIP: Smtlib Prelude Injection

wp/lib/bap_wp/src/runner.ml

@@ -229,13 +229,17 @@ let post_reg_values
 
 (* Parses the user's smtlib queries for use in comparative analysis. *)
 let smtlib
+    ~orig:(sub1,env1)
+    ~modif:(sub2,env2)
     ~precond:(precond : string)
     ~postcond:(postcond : string)
   : (Comp.comparator * Comp.comparator) option =
   if String.is_empty precond && String.is_empty postcond then
     None
   else
-    Some (Comp.compare_subs_smtlib ~smtlib_hyp:precond ~smtlib_post:postcond)
+    let prelude = Z3_utils.compare_prelude_smtlib2 sub1 sub2 env1 env2 in
+    info "Injected CBAT smtlib prelude: %s" prelude;
+    Some (Comp.compare_subs_smtlib ~smtlib_hyp:(prelude ^ precond) ~smtlib_post:(prelude ^ postcond))
 
 (* obtain a set of general purpose registers
  * based on their string names and architecture. *)
@@ -294,7 +298,8 @@ let comparators_of_flags
     func_calls p.compare_func_calls;
     post_reg_values p.compare_post_reg_values
       ~orig:(sub1, env1) ~modif:(sub2, env2);
-    smtlib ~precond:p.precond ~postcond:p.postcond;
+    smtlib ~orig:(sub1, env1) ~modif:(sub2, env2)
+      ~precond:p.precond ~postcond:p.postcond;
     gen_pointer_flag_comparators p.pointer_reg_list
       env1 env2 pointer_env1_vars pointer_env2_vars;
     mem_eq p.rewrite_addresses

wp/lib/bap_wp/src/z3_utils.ml

@@ -100,6 +100,113 @@ let get_z3_name (map : Constr.z3_expr Var.Map.t) (name : string) (fmt : Var.t ->
         else
           None)
 
+(** Sexp.t helper constructors for smtlib constructs *)
+let define_fun name args retsort body =
+  let args = List.map ~f:(fun (v,sort) -> Sexp.List [v; sort]) args in
+  Sexp.List [Sexp.Atom "define-fun"; Sexp.Atom name; Sexp.List args; retsort; body]
+let synonym name ret body = define_fun name [] ret body
+let define_sort (name : string) s = Sexp.List [
+ Sexp.Atom "define-sort"; Sexp.Atom name; Sexp.List []; s]
+let sexp_of_sort (s : Z3.Sort.sort) : Sexp.t = Sexp.of_string (Z3.Sort.to_string s)
+
+(* [make_arg_synonyms] constructs smtlib formula for the arguments of a subroutine.
+   This make synonyms that for high level c-like names ot low level locations *)
+let make_arg_synonyms
+  ?postfix:(postfix = "")
+  (sub : Sub.t)
+  (init_var_map : Expr.expr Var.Map.t)
+  (var_map : Expr.expr Var.Map.t) : Sexp.t list =
+  let args = Term.enum arg_t sub |> Seq.to_list in
+  List.concat_map args ~f:(fun arg ->
+    let cname = Arg.lhs arg in
+    let syn prefix z3_reg =
+      let sort = Sexp.of_string (Z3.Sort.to_string (Z3.Expr.get_sort z3_reg)) in
+      synonym (prefix ^ Var.name cname ^ postfix) sort
+      (Sexp.Atom  (Expr.to_string z3_reg))
+    in
+    let reg = Arg.rhs arg in
+    match reg with
+    | Var reg -> begin
+         match Arg.intent arg with
+           | Some In   -> [syn "init_" (Var.Map.find_exn init_var_map reg)]
+           | Some Out  -> [syn "" (Var.Map.find_exn var_map reg)]
+           | Some Both -> [syn "init_" (Var.Map.find_exn init_var_map reg);
+                           syn "" (Var.Map.find_exn var_map reg)]
+           | None -> []
+    end
+    | _ -> [] (* We don't make synonym unless c variable is just held in a bap variable *)
+    )
+
+(** [args_prelude_compare] builds smtlib synonyms in a comparison for the arguments of
+    two compared subroutines. *)
+let args_prelude_compare
+  (main_sub1 : Sub.t)
+  (main_sub2 : Sub.t)
+  (env1 : Env.t)
+  (env2 : Env.t) : Sexp.t list =
+  let var_map1 = Env.get_var_map env1 in
+  let var_map2 = Env.get_var_map env2 in
+  let init_var_map1 = Env.get_init_var_map env1 in
+  let init_var_map2 = Env.get_init_var_map env2 in
+  let syn1 = make_arg_synonyms ~postfix:"_orig" main_sub1 init_var_map1 var_map1 in
+  let syn2 = make_arg_synonyms ~postfix:"_mod" main_sub2 init_var_map2 var_map2 in
+  syn1 @ syn2
+
+
+
+(** [def_pointer_sort] constructs an smtlib sort synonym of pointer sort.
+    Typically it will be `(define-sort pointer () BV64)` *)
+let def_pointer_sort env =
+  let mem = Env.get_mem env in
+  let var_map = Env.get_var_map env in
+  let z3_mem = Var.Map.find_exn var_map mem in
+  let pointer_sort = Z3.Z3Array.get_domain (Expr.get_sort z3_mem) in
+  define_sort "pointer" (sexp_of_sort pointer_sort)
+
+(** [def_mem_sort] constructs an smtlib sort synonym of the memory array.
+    Typically it will be `(define-sort memsort () (Array (BV64 BV8))` *)
+let def_mem_sort env =
+    let mem = Env.get_mem env in
+    let var_map = Env.get_var_map env in
+    let z3_mem = Var.Map.find_exn var_map mem in
+    define_sort "memsort" (sexp_of_sort (Z3.Expr.get_sort z3_mem))
+
+let compare_prelude_smtlib2  main_sub1 main_sub2 (env1 : Env.t) (env2 : Env.t) : string =
+ let std_prelude = "
+        (
+        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+        ; Sort synonyms
+        (define-sort BV8 () (_ BitVec 8))
+        (define-sort BV16 () (_ BitVec 16))
+        (define-sort BV32 () (_ BitVec 32))
+        (define-sort BV64 () (_ BitVec 64))
+        (define-sort char () (_ BitVec 8))
+        (define-sort byte () (_ BitVec 8))
+        (define-sort int16 () (_ BitVec 16))
+        (define-sort int32 () (_ BitVec 32))
+        (define-sort int64 () (_ BitVec 64))
+        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+        ;; Predefined predicates
+        (define-fun init-mem-equal () Bool (= init_mem_orig init_mem_mod))
+        (define-fun mem-equal () Bool (= mem_orig mem_mod))
+        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+        )" in
+  let std_prelude = match Sexp.of_string std_prelude with
+                    | Sexp.List l -> l
+                    | _ ->
+                    failwith "compare_prelude_smtlib2: Improper constant sexp string"
+  in
+  let cvar_defs = args_prelude_compare main_sub1 main_sub2 env1 env2 in
+  let prelude_sexp = [
+    def_pointer_sort env1;
+    def_mem_sort env1;
+    ] @
+    std_prelude @
+    cvar_defs
+  in
+  let prelude_sexp = List.map ~f:Sexp.to_string_hum prelude_sexp in
+  String.concat ~sep:"\n" prelude_sexp
+
 (** [mk_smtlib2_compare] builds a constraint out of an smtlib2 string that can be used
     as a comparison predicate between an original and modified binary. *)
 let mk_smtlib2_compare (env1 : Env.t) (env2 : Env.t) (smtlib_str : string) : Constr.t =
@@ -130,7 +237,7 @@ let mk_smtlib2_compare (env1 : Env.t) (env2 : Env.t) (smtlib_str : string) : Con
   let declsym = declsym1 @ declsym2 in
   let ctx = Env.get_context env1 in
   mk_smtlib2 ctx smtlib_str declsym
-  
+
 let mk_smtlib2_single ?(name = None) (env : Env.t) (smt_post : string) : Constr.t =
   let var_map = Env.get_var_map env in
   let init_var_map = Env.get_init_var_map env in

wp/lib/bap_wp/src/z3_utils.mli

@@ -66,3 +66,7 @@ val check_external : Z3.Solver.solver
 (** [mk_smtlib2_compare] builds a constraint out of an smtlib2 string that can be used
     as a comparison predicate between an original and modified binary. *)
 val mk_smtlib2_compare : Env.t -> Env.t -> string -> Constr.t
+
+(** [compare_prelude_smtlib2] constructs an smtlib2 string of useful definitions for
+     specification. *)
+val compare_prelude_smtlib2 :  Bap.Std.Sub.t -> Bap.Std.Sub.t -> Env.t -> Env.t -> string

wp/resources/sample_binaries/prelude_test/Makefile

@@ -0,0 +1,13 @@
+SRC_DIR = src
+BIN_DIR = bin
+
+all: $(BIN_DIR)/main_1 $(BIN_DIR)/main_2
+
+$(BIN_DIR):
+	mkdir -p $@
+
+$(BIN_DIR)/%: $(SRC_DIR)/%.c $(BIN_DIR)
+	gcc -Wall -g -o $@ $<
+
+clean:
+	rm -rf $(BIN_DIR)

wp/resources/sample_binaries/prelude_test/c/main_1.h

@@ -0,0 +1 @@
+int foo(int a, int b, int c);

wp/resources/sample_binaries/prelude_test/run_wp.sh

@@ -0,0 +1,20 @@
+# A test that gives RAX the value of RDI + 1. The two binaries differ in the
+# order of the increment and move instructions, but have the same output.
+
+# Runs WP with a postcondition that states that the end value of RAX in the
+# modified binary is equal to the initial value of RDI in the original
+# binary + 1.
+
+# Should return UNSAT
+ #--compare-post-reg-values=RAX \
+
+run () {
+  bap wp \
+    --func=main \
+    --precond="(assert (= init_main_argc_mod init_main_argc_orig))" \
+    --postcond="(assert (= main_result_mod main_result_orig))" \
+    --no-glibc-runtime \
+    -- ./bin/main_1 ./bin/main_2
+}
+
+run

wp/resources/sample_binaries/prelude_test/run_wp_sat.sh

@@ -0,0 +1,19 @@
+# A test that gives RAX the value of RDI + 1. The two binaries differ in the
+# order of the increment and move instructions, but have the same output.
+
+# Runs WP with a postcondition that states that the end value of RAX in the
+# modified binary is equal to the initial value of RDI in the original
+# binary + 2, which is impossible.
+
+# Should return SAT
+
+run () {
+  bap wp \
+    --func=main \
+    --compare-post-reg-values=RAX \
+    --postcond="(assert (= RAX_mod (bvadd init_RDI_orig #x0000000000000002)))" \
+    --no-glibc-runtime \
+    -- ./bin/main_1 ./bin/main_2
+}
+
+run

wp/resources/sample_binaries/prelude_test/src/main_1.c

@@ -0,0 +1,8 @@
+
+int foo(int a, int b, int c){
+    return a + b * c;
+}
+
+int main(int argc, char* argv[]){
+    return foo(argc, 1, 2);
+}

wp/resources/sample_binaries/prelude_test/src/main_2.c

@@ -0,0 +1,8 @@
+
+int foo(int a, int b, int c){
+    return a + b * c;
+}
+
+int main(int argc, char* argv[]){
+    return foo(argc, 1, 2);
+}