From eca5cc5d6c5516c497c74404b366621b5080f258 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Mon, 23 Aug 2021 16:57:51 -0400 Subject: [PATCH 1/2] Initial commit of smtlib prelude injection --- wp/lib/bap_wp/src/runner.ml | 9 +- wp/lib/bap_wp/src/z3_utils.ml | 130 +++++++++++++++++- wp/lib/bap_wp/src/z3_utils.mli | 4 + .../sample_binaries/prelude_test/Makefile | 13 ++ .../sample_binaries/prelude_test/bin/main_1 | Bin 0 -> 17728 bytes .../sample_binaries/prelude_test/bin/main_2 | Bin 0 -> 17728 bytes .../sample_binaries/prelude_test/c/main_1.h | 1 + .../sample_binaries/prelude_test/run_wp.sh | 20 +++ .../prelude_test/run_wp_sat.sh | 19 +++ .../sample_binaries/prelude_test/src/main_1.c | 8 ++ .../sample_binaries/prelude_test/src/main_2.c | 8 ++ 11 files changed, 209 insertions(+), 3 deletions(-) create mode 100644 wp/resources/sample_binaries/prelude_test/Makefile create mode 100755 wp/resources/sample_binaries/prelude_test/bin/main_1 create mode 100755 wp/resources/sample_binaries/prelude_test/bin/main_2 create mode 100644 wp/resources/sample_binaries/prelude_test/c/main_1.h create mode 100755 wp/resources/sample_binaries/prelude_test/run_wp.sh create mode 100755 wp/resources/sample_binaries/prelude_test/run_wp_sat.sh create mode 100644 wp/resources/sample_binaries/prelude_test/src/main_1.c create mode 100644 wp/resources/sample_binaries/prelude_test/src/main_2.c diff --git a/wp/lib/bap_wp/src/runner.ml b/wp/lib/bap_wp/src/runner.ml index 1db5cdd3..e1bf35dc 100644 --- a/wp/lib/bap_wp/src/runner.ml +++ b/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 diff --git a/wp/lib/bap_wp/src/z3_utils.ml b/wp/lib/bap_wp/src/z3_utils.ml index 957e34a2..ab98869a 100644 --- a/wp/lib/bap_wp/src/z3_utils.ml +++ b/wp/lib/bap_wp/src/z3_utils.ml @@ -100,6 +100,134 @@ 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 bv_sort width = Sexp.List [ + Sexp.Atom "_"; + Sexp.Atom "BitVec"; + Sexp.Atom (Int.to_string width); + ] +let mem_sort dom cod = Sexp.List [Sexp.Atom "Array"; dom ; cod ] +let bv_sort_of_var (v : Var.t) : Sexp.t = + let typ = Var.typ v in + match typ with + | Imm w -> bv_sort w + | Type.Mem (i_size, w_size) -> mem_sort + (bv_sort (Size.in_bits i_size)) + (bv_sort (Size.in_bits w_size)) + | Unk -> failwith "bv_sort_of_var: Unrecognized sort type" +let bv_sort (width : int) : Sexp.t = Sexp.List + [ + Sexp.Atom "_"; + Sexp.Atom "BitVec"; + Sexp.Atom (Int.to_string width); + ] +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) +let sexp_of_expr (x : Expr.expr) : Sexp.t = Sexp.of_string (Expr.to_string x) + +(* [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 +258,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 diff --git a/wp/lib/bap_wp/src/z3_utils.mli b/wp/lib/bap_wp/src/z3_utils.mli index e20339f7..b8a59229 100644 --- a/wp/lib/bap_wp/src/z3_utils.mli +++ b/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 \ No newline at end of file diff --git a/wp/resources/sample_binaries/prelude_test/Makefile b/wp/resources/sample_binaries/prelude_test/Makefile new file mode 100644 index 00000000..3d2c6a2d --- /dev/null +++ b/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) diff --git a/wp/resources/sample_binaries/prelude_test/bin/main_1 b/wp/resources/sample_binaries/prelude_test/bin/main_1 new file mode 100755 index 0000000000000000000000000000000000000000..1721dbd4af8973bf49d6c3f8ee841a8895ca062c GIT binary patch literal 17728 zcmeHOe{5UT6~4CP#3hO2ChbTYpe}1i%dnl4wxoqnJHP5wX$vJ8MWZ|%`z0~+kIa6i z4FgtGhGunvZkk|dOzS|JChZS2iD}cOjj&D(G;ITEVvG%~Vlc9aL0|=CqtyG(efK!_ zi?eEMe@xT6l6~&^?)lEW@7(*|yVt(=vjf9}PKQHqa*1mNX4w*g#D}TxI>oE=OE4?Y!tmMXj=luC|m-x^9K0;y!Ca3pY~dwXE})?hvx+#>6yc2ONPrgrZe z6>u|4mWTYLKKbOf_S0WwA5*&Z{B97_ixNHOGbQCOQ?LD9WJwVm%zzAyYM&4LAW-!gt$Iq-zd za>iMIahHixUr~LWPFLXECMuh&zuz`M324Ui5_?VHY7y!bF+rC^j!4VPd%rko6@#N0l!n)_!vaXIzjf( zek8SiA@#1m4i%rjC0cwXdhFHt>qdrW+z(>v8=YxhCq>UI@Kjoz1Le$#=uFSU$V6w{ zUm~$%!B~x|_fZ~IuPB{vS$C8wKBXk=lhS_M7>Uj2qQ&{>Q*Z8yKDFSAI-ZU`f6iD1 z2OE_GPwDh{%R01+`PAN{Jya|TA0Le#>v2*xT71oDiXQK&hcdUhR4UCS@b$F&1FX6o zhrq4k|M@Tq$#KAPKqu2hOX^?}P+*Y!IUpW)&=!^JoIi?2sYtNsu@cFGam@p9oW)PJ8m6uCKa zC~`|gJ2k#oCAE@zmZa?Wa!<<^*a_&0XqVA1ndad5wIihe;NS? z{sVJ#xULT4`Wo=LXuec3Ag_RY1o9fln;|#8T`D~RISBb{$U7m=K)wNa4VJg7kf-Fh zqz9=H!>^|2*3fh(taOe3EG2dIAQ#zWbbg&GiRSF;pu5GCsGVd^2RZ{8qCZKM{y0 z@HvWdoyrHjz6YE`-uC-l17813-GFz~7u@~c&im@4-tJ=!yS?Fzw>#qPjCeQodi}lL z_Fk{A*Xxo0C!PiUTkvE5A4h?-lN|v&0(J!K2-p#@BVb3sj({BjI|BbJ5#W7|ypNIo znWV(B$yCc5C7YGLp!P$qQ9AFJ>`*%IgQR_>lz87Ht-~mB`Mc*zS<+9c&5pcgI#@?2 z?{O948C8CP35&awr2VFp+D#!=E6GC9#H`vUNo!h49#s*yV^*R!&oK&ii=%Kxr(ZkKZZ-xIt){6F-_`&W1O_3iX;8XYTS zjDmkh@XBCkpzErFRJ-op(i!aBy4i%~&RKIOs~M}!YJ}`rrX@cIZU)68gVppBfEj#h z5uIn-k-$Zi8rSytdJW@VQ%% z9fDE4!n|mw^yaa8d#D$;AV#xGm6*Q7^=Q3Ie3Y)i@xHei-||ogBJIfM;zH0yYppAY zYk-OSVzI)>*WTuC^|ZOYC)|#k-0M5tO`ee3;puVWXCVhRrThE3t};8^A4nU8jNUV$ zXY^b$4mFmGPxhD_ec`gZkDyOFk30*Vvyde;iP&p*A+(cXkNW>>& zIRW){1Znx?LJ-?)+|Vxkmd58UD%mdd44#G6HDP25{PS5)B!(PT2SxB3ct~6a2oa^yb2^i~OFd#_?9E@mzI@kCfjl)%Ljg!$gmE2b>{hzFCzPg?Nx z3g>x+=|zaEkip$jjsw+4X%HVrjrh}H7OI!$DP&7&8Xt#P+K*oWUaS4fUDr3HpH?wK z4Ys6Oejb-LZA-?Z@-uL(sBEi^s{taJ&X%*ilz6R8+a??Gp}BX zJbzjZ+%M~>{<=xxOUGvyaG$ua+%L>(0p99ddOvm(&PEmTM&-vk{u99c6?UA>17GR9 zQ1E<%@uP&JMNCrDC-DGqy56JedUZwky2AM_wqD^sg!Ey&wTBg;#35xLR^v9L@W+6Y zz4bnQT-jSEA5Q?M_FL^|f%~hgl-f(cS@10`JSb7AqVP@hrX63_TI-?%dv4+lY=@CAC;C7n|1bip))m@mwseYl%WS zJq=2QroqyvGA+LpHEr-fWbc4Bu&-akS*vQxgwXnL+85b7)K^_14|M^;#6cT~Di6{A z147$9yuUXxtnD8hykTHO8;SG|50F=R6fB-E$Tt7$!(VzLX2h7XczP@xt~x%Zk(GHw z47Szh#k52|t4+o-2|7zQv>#RpOo|G59hbA%5(t|A z51&;ZcdKrm2dn3&F>3R4<6v*dO?m&c5%O3_e;2~ms)A}FspIF&L4eFZ17$Qb$& zeA8HhWmX11s86cVGnoLNHIr`+Ba^{-IFF^1aWseeE{J%FAcio_+<@t0g$Y>3G7}i@ zN=;_Qvz(8Ojpg*)S;IL@o%4v9^?v%0I=xwOi{e>pCZ5-^w7y}vEP{KcBs| zwm$|wt;w0s>vonWRK0YK6g%egdOHb>E}8i}k7dd0ewfH)jsK^C(i)ukJl|!>zh`j! z*^cGi;M1C(b)FZq^vhb!KB{cLg5?61V#@sT?+oh2JgW@3e(Uu=gmUuB<@5@aNlEL> z&)R=qgK;I_uXrrko$_jRFCMkn#5WZc7E9*E0(NfJkg-YKuDKH2&++v<%xxX+u&7wewX6r7e_X6h?VC_Df>skIa6i z2?JKtjm_#Zx@qELVuFD*P1+x564NH8ZDE}lXxawS#MqZs!4TcVAh3eMDD{5ly?Y${ z#aT7BKc?wj$v*e|?)ja2-?{g_cdvc#X9h=xT#6z%xy99jw6M=Y!m?ogDw%-@i*C_` z?~BDIQ4hV&#H{kLB~WUmmt57-D{(g@@!BX;LtbFPf+e?*B=J^C&w8v9mO@?!@ysHr zGtSZ@+sTsga(#YTqfH)^4P#l!qu4A2EZ#zIwe-vSwo1u7Qi&&mmOZ+|N>a|t`dD&2 zDJJykmhrSpzvV@+wDS&1o?Q+|9!si&()F(zi4RlXwUSroH{A%kJwY z^P9W*fUIw&e(=fovy|Z#p;U6bYey)R2&9sk!c1VMyDQMOBbd(yx0`iSyQmHtQ+xJ} z3AmXjOoq|yi?vdx@}0MIX(K(a1RuQVsrH+mpZWYFsrQoXgX$z3O2p?OK|1BB4zjVX z{~qMzScZH-|7F?)R`}`$?ypg{0a!~7d=!|!1|DAlZv=jE4SRw3#VK4}Let_iF>NB5 ziKUWv=uoLh%Nwzrp`~NVjMy_W+}E#d4{i_c6x#6UUM->L^vPu2&~u}E`%~GBJ{lWO z5pyz~%}AzZnbtHk+hawMW2qp56hj^tg$>D76y3{Y+xh+W zXPotyc3U|071hV-WChM`qOwyJIFB8|7b+>UlJpW1t*mx@K0^V7%})%TF8<`$;2GulLnqh((e%M6S}ZJ}+2sjb=KaGHb z|G<=u?kmH%z6N|QSSXbY$jcxfhP(>$X2>mXl}b-S4nh7J@=nOpkgr2th2`y9+2sjaNBH%>8iGULUCjw3c{#PQv`x<#4BmFZ; ziREfbEpL=;lKP_D54m3IykByo)OjBy?JK3k`zC1}Mv2ScIa|t-{;1sS$ZMv9b%gRB zS0SF2<>y(jxJydfZ%V1n5@MZ{EF?|L%YBlxrlsVS6>&S}O;iYM0yPu+yGZJ6_kPK0 zFXCfD_y^W(|0&sC{G)5?96u}rP5nh#{+`siUDEx3Pw@Wm|Ij1vU)|H+zstXMY`l;$ z3jUtp<-v|X=M@E0?Yw(?N3dhZHVZa)&RRQJtypc7BjlPDTJm$?R#3bOjVg1beGQpf zMAz#mQ0hGyh-;){a~V(Y!-TqDGc8ogyS|)qziX-+3Z{CisH^iNGluYZKMla+y$9d* zO8r|94HMa{P+X>Ku6h%2O3K6D7|NQYQ|~yGwU#pFjYHXJDG8XaQMRb9jc#?Lx<+Yf z@STrl1eM+E-RiE!D;s+nFIhj_N(JGz`}@`_t!S`EaM^IH3*)VBvuJF*y3vjBd76FJl)-HK}VA3C$h~;N9@u^%klP%-}h0Nh(CJ``bA9o&w*!>;LFZ!ODwaQD3eEIn71nv{(m-~fT&A?k+%kRf-!r7=o-XQ(h$A1F2zrv2QdEjeY=L?>1 zFn)w^w1`P^`XufHPS<-xUau|*k4T)~Vw)uX14tjnTU%HHQXG=@VL5I?5`P>x+1u~a zC#1c7^6?~aYQNon9=N}{N>lqCaPyB0ds#eZ%(7qB4)&xvUGYZ9IiS(rjeC(L=3jo z=f$){KC4Z|G6_0MHoPBJ2~3I#c^#Lt)DjAbpgE$Zjpy^ym3dB0({LP(148H2Y92nT zKJHfCJQ2*#rZEYEG;)@l;vA-{dTv?-Gnf+vCo_d0W=GR{&X}!$#tTWDNK7Uq6zLnr zlxk9#=2Mt5iC|(jgDNa(_`C^`zhFrh>`X4|!`Q>tY1)51p`^?YY ze_w}jCEqW3EZLp(YIiRlv+;S}&hlLRZ`=4`NnrV1TZh^GeaFVCo<%d2GLN1^#W4_$xM)($2qR1%6MbMY!)A{GBWCpOyTvbMPaQ zZ@(zNYzOS@G*82wPGN!*|O{#XT!`ySbHn(48!?{Y=5#HM1+ QQJbH+(jtu52sTyx6T9}*iU0rr literal 0 HcmV?d00001 diff --git a/wp/resources/sample_binaries/prelude_test/c/main_1.h b/wp/resources/sample_binaries/prelude_test/c/main_1.h new file mode 100644 index 00000000..d8af0f52 --- /dev/null +++ b/wp/resources/sample_binaries/prelude_test/c/main_1.h @@ -0,0 +1 @@ +int foo(int a, int b, int c); \ No newline at end of file diff --git a/wp/resources/sample_binaries/prelude_test/run_wp.sh b/wp/resources/sample_binaries/prelude_test/run_wp.sh new file mode 100755 index 00000000..3753bf8b --- /dev/null +++ b/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 diff --git a/wp/resources/sample_binaries/prelude_test/run_wp_sat.sh b/wp/resources/sample_binaries/prelude_test/run_wp_sat.sh new file mode 100755 index 00000000..0c7930e1 --- /dev/null +++ b/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 diff --git a/wp/resources/sample_binaries/prelude_test/src/main_1.c b/wp/resources/sample_binaries/prelude_test/src/main_1.c new file mode 100644 index 00000000..12043b8c --- /dev/null +++ b/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); +} \ No newline at end of file diff --git a/wp/resources/sample_binaries/prelude_test/src/main_2.c b/wp/resources/sample_binaries/prelude_test/src/main_2.c new file mode 100644 index 00000000..12043b8c --- /dev/null +++ b/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); +} \ No newline at end of file From f995806c5a178d4a7cc58d6250387bc50f72f395 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Mon, 23 Aug 2021 17:26:35 -0400 Subject: [PATCH 2/2] removed unneeded functions --- wp/lib/bap_wp/src/z3_utils.ml | 21 --------------------- wp/lib/bap_wp/src/z3_utils.mli | 2 +- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/wp/lib/bap_wp/src/z3_utils.ml b/wp/lib/bap_wp/src/z3_utils.ml index ab98869a..597fd1a6 100644 --- a/wp/lib/bap_wp/src/z3_utils.ml +++ b/wp/lib/bap_wp/src/z3_utils.ml @@ -105,30 +105,9 @@ 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 bv_sort width = Sexp.List [ - Sexp.Atom "_"; - Sexp.Atom "BitVec"; - Sexp.Atom (Int.to_string width); - ] -let mem_sort dom cod = Sexp.List [Sexp.Atom "Array"; dom ; cod ] -let bv_sort_of_var (v : Var.t) : Sexp.t = - let typ = Var.typ v in - match typ with - | Imm w -> bv_sort w - | Type.Mem (i_size, w_size) -> mem_sort - (bv_sort (Size.in_bits i_size)) - (bv_sort (Size.in_bits w_size)) - | Unk -> failwith "bv_sort_of_var: Unrecognized sort type" -let bv_sort (width : int) : Sexp.t = Sexp.List - [ - Sexp.Atom "_"; - Sexp.Atom "BitVec"; - Sexp.Atom (Int.to_string width); - ] 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) -let sexp_of_expr (x : Expr.expr) : Sexp.t = Sexp.of_string (Expr.to_string x) (* [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 *) diff --git a/wp/lib/bap_wp/src/z3_utils.mli b/wp/lib/bap_wp/src/z3_utils.mli index b8a59229..1ccc5bb2 100644 --- a/wp/lib/bap_wp/src/z3_utils.mli +++ b/wp/lib/bap_wp/src/z3_utils.mli @@ -69,4 +69,4 @@ 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 \ No newline at end of file +val compare_prelude_smtlib2 : Bap.Std.Sub.t -> Bap.Std.Sub.t -> Env.t -> Env.t -> string