Pzucker/precondition

wp/lib/bap_wp/src/compare.ml

@@ -116,19 +116,43 @@ let compare_subs_empty_post
   in
   compare_subs ~postcond:postcond ~hyps:hyps ~original:original ~modified:modified
 
+(** [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 =
+  let var_map1 = (Env.get_var_map env1) in
+  let var_map2 = (Env.get_var_map env2) in
+  let smtlib_str = Env.EnvMap.fold var_map1 ~init:smtlib_str 
+      ~f:(fun ~key:var ~data:z3_var smtlib_str ->
+          String.substr_replace_all smtlib_str ~pattern:((Var.name var) ^ "_orig") ~with_:(Z3.Expr.to_string z3_var)
+        ) in
+  let smtlib_str = Env.EnvMap.fold var_map2 ~init:smtlib_str 
+      ~f:(fun ~key:var ~data:z3_var smtlib_str ->
+          String.substr_replace_all smtlib_str ~pattern:((Var.name var) ^ "_mod") ~with_:(Z3.Expr.to_string z3_var)
+        ) in
+  info "New smtlib string: %s \n" smtlib_str;
+  let declsym1 = Z3_utils.get_decls_and_symbols env1 in
+  let declsym2 = Z3_utils.get_decls_and_symbols env2 in
+  let declsym = declsym1 @ declsym2 in
+  let ctx = Env.get_context env1 in
+  Z3_utils.mk_smtlib2 ctx smtlib_str declsym
+
 let compare_subs_eq
     ~input:(input : Var.Set.t)
     ~output:(output : Var.Set.t)
     ~original:(original : Sub.t * Env.t)
     ~modified:(modified : Sub.t * Env.t)
+    ~smtlib_post:(smtlib_post : string)
+    ~smtlib_hyp:(smtlib_hyp : string)
   : Constr.t * Env.t * Env.t =
   let postcond ~original:(_, env1) ~modified:(_, env2) ~rename_set:_ =
     let post_eqs, env1, env2 = set_to_eqs env1 env2 output in
-    Constr.mk_clause [] post_eqs, env1, env2
+    let post' = mk_smtlib2_compare env1 env2 smtlib_post in 
+    Constr.mk_clause [] (post' :: post_eqs), env1, env2
   in
   let hyps ~original:(_, env1) ~modified:(_, env2) ~rename_set:_ =
     let pre_eqs, env1, env2 = set_to_eqs env1 env2 input in
-    Constr.mk_clause [] pre_eqs, env1, env2
+    let pre' = mk_smtlib2_compare env1 env2 smtlib_hyp in 
+    Constr.mk_clause [] (pre' :: pre_eqs), env1, env2
   in
   compare_subs ~postcond:postcond ~hyps:hyps ~original:original ~modified:modified
 

wp/lib/bap_wp/src/compare.mli

@@ -53,6 +53,8 @@ val compare_subs_eq
   -> output:Bap.Std.Var.Set.t
   -> original:(Bap.Std.Sub.t * Env.t)
   -> modified:(Bap.Std.Sub.t * Env.t)
+  -> smtlib_post:string
+  -> smtlib_hyp:string 
   -> Constr.t * Env.t * Env.t
 
 (** Compare two subroutines by composition for an empty postcondition:

wp/lib/bap_wp/src/constraint.ml

@@ -269,3 +269,5 @@ let get_refuted_goals ?filter_out:(filter_out = []) (constr : t)
       worker e current_path current_registers (olds @ o) (news @ n')
   in
   worker constr Jmp.Map.empty Jmp.Map.empty [] []
+
+

wp/lib/bap_wp/src/constraint.mli

@@ -127,4 +127,4 @@ val eval_model_exn : Z3.Model.model -> z3_expr -> z3_expr
 (** Gets the model of the last check to the Z3 solver. An error will be raised
     if retrieving the model fails in the case that [check] was not yet called
     to the solver or the result of the last [check] did not result in SAT. *)
-val get_model_exn : Z3.Solver.solver -> Z3.Model.model
+val get_model_exn : Z3.Solver.solver -> Z3.Model.model

wp/lib/bap_wp/src/dune

@@ -1,4 +1,4 @@
 (library
-  (name bap_wp)
-  (public_name bap_wp)
-  (libraries bap bap-x86-cpu z3 oUnit))
+   (name bap_wp)
+   (public_name bap_wp)
+   (libraries bap bap-x86-cpu z3 oUnit))

wp/lib/bap_wp/src/environment.ml

@@ -255,6 +255,9 @@ let set_freshen (env : t) (freshen : bool) = { env with freshen = freshen }
 let add_var (env : t) (v : Var.t) (x : Constr.z3_expr) : t =
   { env with var_map = EnvMap.set env.var_map ~key:v ~data:x }
 
+let remove_var (env :t) (v : Var.t) : t =
+  { env with var_map = EnvMap.remove env.var_map v }
+
 let mk_exp_conds (env : t) (e : exp) : Constr.goal list * Constr.goal list =
   let { exp_conds; _ } = env in
   let conds = List.map exp_conds ~f:(fun gen -> gen env e) in
@@ -271,6 +274,9 @@ let get_subs (env : t) : Sub.t Seq.t =
 let get_var_map (env : t) : Constr.z3_expr EnvMap.t =
   env.var_map
 
+let find_var (env : t) (var : Var.t) : Constr.z3_expr option =
+  EnvMap.find env.var_map var
+
 let get_var (env : t) (var : Var.t) : Constr.z3_expr * t =
   let mv = EnvMap.find env.var_map var in
   match mv with

wp/lib/bap_wp/src/environment.mli

@@ -127,6 +127,12 @@ val wp_rec_call :
     typically a constant. *)
 val add_var : t -> Bap.Std.Var.t -> Constr.z3_expr -> t
 
+(** Remove a binding in the environment for a bap variable. *)
+val remove_var : t -> Bap.Std.Var.t -> t
+
+(** Looks up the Z3 variable that represents a BIR variable. *)
+val find_var : t -> Bap.Std.Var.t -> Constr.z3_expr option
+
 (** Add a precondition to be associated to a block b to the environment. *)
 val add_precond : t -> Bap.Std.Tid.t -> Constr.t -> t
 
@@ -146,7 +152,7 @@ val get_subs : t -> Bap.Std.Sub.t Bap.Std.Seq.t
 (** Obtains the var_map containing a mapping of BIR variables to Z3 variables. *)
 val get_var_map : t -> Constr.z3_expr EnvMap.t
 
-(** Looks up the Z3 variable that represents a BIR variable. *)
+(** Looks up the Z3 variable that represents a BIR variable. Produces fresh z3_expr if not found. *)
 val get_var : t -> Bap.Std.Var.t -> Constr.z3_expr * t
 
 (** Looks up the precondition for a given block in the environment. Currently returns

wp/lib/bap_wp/src/precondition.ml

@@ -217,11 +217,14 @@ let exp_to_z3 (exp : Exp.t) (env : Env.t) : Constr.z3_expr * Constr.t list * Con
       debug "Visiting let %s = %s in %s%!"
         (Var.to_string v) (Exp.to_string exp) (Exp.to_string body);
       let exp_val, env = exp_to_z3_body exp env in
-      (* FIXME: we're handling this incorrectly! The variable should
-         be removed from the context after leaving the scope of the
-         Let! *)
+      let old_val = Env.find_var env v in
       let env' = Env.add_var env v exp_val in
-      exp_to_z3_body body env'
+      let z3_expr, env = exp_to_z3_body body env' in
+      let env = Env.remove_var env v in
+      let env = match old_val with
+        | None -> env
+        | Some exp_val -> Env.add_var env v exp_val in
+      (z3_expr, env)
     | Unknown (str, typ) ->
       debug "Visiting unknown: %s  Type:%s%!" str (Type.to_string typ);
       Env.new_z3_expr env ~name:("unknown_" ^ str) typ, env
@@ -847,42 +850,6 @@ let non_null_assert : Env.exp_cond = fun env exp ->
   else
     Some (Assume (Constr.mk_goal "assume" (Bool.mk_and ctx conds)))
 
-let mk_smtlib2_post (env : Env.t) (smt_post : string) : Constr.t =
-  let ctx = Env.get_context env in
-  let sort_symbols = [] in
-  let sorts = [] in
-  let fun_decls =
-    Env.EnvMap.fold (Env.get_var_map env) ~init:[]
-      ~f:(fun ~key:_ ~data:z3_var decls ->
-          assert (Z3.Expr.is_const z3_var);
-          Z3.FuncDecl.mk_const_decl_s ctx
-            (Z3.Expr.to_string z3_var)
-            (Z3.Expr.get_sort z3_var)
-          ::decls
-        )
-  in
-  let fun_symbols =
-    Env.EnvMap.fold (Env.get_var_map env) ~init:[]
-      ~f:(fun ~key:_ ~data:z3_var decls ->
-          assert (Z3.Expr.is_const z3_var);
-          Z3.Symbol.mk_string ctx
-            (Z3.Expr.to_string z3_var)
-          ::decls
-        )
-  in
-  let asts = Z3.SMT.parse_smtlib2_string ctx smt_post
-      sort_symbols
-      sorts
-      fun_symbols
-      fun_decls
-  in
-  let goals = List.map (Z3.AST.ASTVector.to_expr_list asts)
-      ~f:(fun e ->
-          e
-          |> Constr.mk_goal (Expr.to_string e)
-          |> Constr.mk_constr)
-  in
-  Constr.mk_clause [] goals
 
 let check ?refute:(refute = true) (solver : Solver.solver) (ctx : Z3.context)
     (pre : Constr.t) : Solver.status =
@@ -895,6 +862,7 @@ let check ?refute:(refute = true) (solver : Solver.solver) (ctx : Z3.context)
     else
       pre'
   in
+  info "Z3 Query:\n%s\n" (Z3.Expr.to_string (Z3.Expr.simplify is_correct None));
   let () = Z3.Solver.add solver [is_correct] in
   Z3.Solver.check solver []
 

wp/lib/bap_wp/src/precondition.mli

@@ -196,14 +196,6 @@ val mk_env
   -> Env.var_gen
   -> Env.t
 
-(** [mk_smtlib2_post env sub post] takes in a string representing a
-    valid SMT-Lib-2 statement, and turns it into a valid postcondition
-    to be passed to {!visit_sub}.
-
-    The variables in the SMT-Lib statements need to appear in the
-    environment. *)
-val mk_smtlib2_post : Env.t -> string -> Constr.t
-
 (** Create a precondition for a given jump expression, depending on the postcondition
     and (potentially) the preconditions for the jump targets or the loop invariants.
 

wp/lib/bap_wp/src/z3_utils.ml

@@ -0,0 +1,71 @@
+(***************************************************************************)
+(*                                                                         *)
+(*  Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc.      *)
+(*                                                                         *)
+(*  This file is provided under the license found in the LICENSE file in   *)
+(*  the top-level directory of this project.                               *)
+(*                                                                         *)
+(*  This work is funded in part by ONR/NAWC Contract N6833518C0107.  Its   *)
+(*  content does not necessarily reflect the position or policy of the US  *)
+(*  Government and no official endorsement should be inferred.             *)
+(*                                                                         *)
+(***************************************************************************)
+
+open !Core_kernel
+open Bap.Std
+
+include Self()
+
+module Expr = Z3.Expr
+module Arith = Z3.Arithmetic
+module BV = Z3.BitVector
+module Bool = Z3.Boolean
+module Z3Array = Z3.Z3Array
+module FuncDecl = Z3.FuncDecl
+module Symbol = Z3.Symbol
+module Solver = Z3.Solver
+module Env = Environment
+module Constr = Constraint
+
+let get_decls_and_symbols (env : Env.t) : ((FuncDecl.func_decl * Symbol.symbol) list) = 
+  let var_map = Env.get_var_map env in
+  let ctx = Env.get_context env in
+  Env.EnvMap.fold var_map ~init:[]
+    ~f:(fun ~key:_ ~data:z3_var decls ->
+        assert (Expr.is_const z3_var);
+        let decl = FuncDecl.mk_const_decl_s ctx
+            (Expr.to_string z3_var)
+            (Expr.get_sort z3_var) in
+        let sym =  Symbol.mk_string ctx (Expr.to_string z3_var) in
+        (decl,sym)::decls
+      )
+
+let mk_smtlib2 (ctx : Z3.context) (smtlib_str : string) (decl_syms : (Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) : Constr.t =
+  let fun_decls, fun_symbols = List.unzip decl_syms in
+  let sort_symbols = [] in
+  let sorts = [] in
+  let asts = Z3.SMT.parse_smtlib2_string ctx smtlib_str
+      sort_symbols
+      sorts
+      fun_symbols
+      fun_decls
+  in
+  let goals = List.map (Z3.AST.ASTVector.to_expr_list asts)
+      ~f:(fun e ->
+          e
+          |> Constr.mk_goal (Expr.to_string e)
+          |> Constr.mk_constr)
+  in
+  Constr.mk_clause [] goals
+
+let mk_smtlib2_single (env : Env.t) (smt_post : string) : Constr.t =
+  let var_map = Env.get_var_map env in
+  let smt_post = Env.EnvMap.fold var_map ~init:smt_post 
+      ~f:(fun ~key:var ~data:z3_var smt_post ->
+          String.substr_replace_all smt_post ~pattern:((Var.name var) ^ " ") ~with_:((Expr.to_string z3_var) ^ " ")
+        ) in
+  info "New smt-lib string : %s\n" smt_post;
+  let decl_syms = get_decls_and_symbols env in
+  let ctx = Env.get_context env in
+  mk_smtlib2 ctx smt_post decl_syms 
+

wp/lib/bap_wp/src/z3_utils.mli

@@ -0,0 +1,47 @@
+(***************************************************************************)
+(*                                                                         *)
+(*  Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc.      *)
+(*                                                                         *)
+(*  This file is provided under the license found in the LICENSE file in   *)
+(*  the top-level directory of this project.                               *)
+(*                                                                         *)
+(*  This work is funded in part by ONR/NAWC Contract N6833518C0107.  Its   *)
+(*  content does not necessarily reflect the position or policy of the US  *)
+(*  Government and no official endorsement should be inferred.             *)
+(*                                                                         *)
+(***************************************************************************)
+
+(**
+
+   This module exports types and utilities to process and report results found
+   using the WP plugin.
+
+   The report contains information about the result of the WP analysis, and in
+   the case the result is [SAT], prints out the model that contains the input
+   register and memory values that result in the program refuting a goal, the path
+   taken to the refuted goal, and the register values at each jump in the path.
+
+*)
+
+module Env = Environment
+module Constr = Constraint
+
+
+(** [get_decls_and_symbols] builds from a the var_map in an environment 
+    a mapping of all Z3 func_decl to their symbol. This is a helper function for
+    [mk_smtlib2] *)
+val get_decls_and_symbols : Env.t -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list) 
+
+(** [mk_smtlib2_single env smtlib_str] takes in a string representing a
+    valid SMT-Lib-2 statement. 
+    The variables in the SMT-Lib statements need to appear in the
+    environment. The intended purpose of this function is generating hypothesis
+     and postconditions for single binary analysis *)
+val mk_smtlib2_single : Env.t -> string -> Constr.t
+
+(** [mk_smtlib2] parses a smtlib2 string in the context that has a mapping of func_decl 
+    to symbols and returns a constraint [Constr.t] corresponding to the smtlib2 string. 
+    The [func_decl * symbol] mapping can be constructed from an [Env.t] using the 
+    [get_decls_and_symbols] function. *)
+
+val mk_smtlib2 : Z3.context -> string -> ((Z3.FuncDecl.func_decl * Z3.Symbol.symbol) list)  -> Constr.t