From f04e9cce83bcb2b05cd218a3ffa057a3b9f51e07 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Tue, 28 Dec 2021 16:11:02 -0500 Subject: [PATCH 1/4] Enabled patches written in primus lisp. I am shocked this is working at all --- bap-vibes/src/config.ml | 5 +- bap-vibes/src/config.mli | 2 +- bap-vibes/src/data.ml | 17 +-- bap-vibes/src/data.mli | 10 +- bap-vibes/src/patch_ingester.ml | 28 +++-- bap-vibes/src/seeder.ml | 3 +- plugin/lib/vibes_plugin_parameters.ml | 19 ++-- resources/exes/arm-simple-primus/Makefile | 106 ++++++++++++++++++ resources/exes/arm-simple-primus/README.md | 29 +++++ resources/exes/arm-simple-primus/config.json | 25 +++++ resources/exes/arm-simple-primus/main.c | 4 + .../arm-simple-primus/main.patched.reference | Bin 0 -> 7968 bytes .../exes/arm-simple-primus/main.reference | Bin 0 -> 7968 bytes resources/exes/arm-simple-primus/main.s | 33 ++++++ resources/exes/arm-simple-primus/patch.lisp | 4 + 15 files changed, 254 insertions(+), 31 deletions(-) create mode 100644 resources/exes/arm-simple-primus/Makefile create mode 100644 resources/exes/arm-simple-primus/README.md create mode 100644 resources/exes/arm-simple-primus/config.json create mode 100644 resources/exes/arm-simple-primus/main.c create mode 100755 resources/exes/arm-simple-primus/main.patched.reference create mode 100755 resources/exes/arm-simple-primus/main.reference create mode 100644 resources/exes/arm-simple-primus/main.s create mode 100644 resources/exes/arm-simple-primus/patch.lisp diff --git a/bap-vibes/src/config.ml b/bap-vibes/src/config.ml index fdf594d5..d3ed61e8 100644 --- a/bap-vibes/src/config.ml +++ b/bap-vibes/src/config.ml @@ -5,7 +5,7 @@ open !Core_kernel module Hvar = Higher_var module Wp_params = Bap_wp.Run_parameters -type patch_code = CCode of Cabs.definition | ASMCode of string +type patch_code = CCode of Cabs.definition | ASMCode of string | PrimusCode of string (* A type to represent a patch. *) type patch = @@ -104,7 +104,8 @@ let string_of_hvar (v : Hvar.t) : string = let patch_to_string (p : patch) : string = let code = match p.patch_code with | CCode ccode -> Utils.print_c Cprint.print_def ccode - | ASMCode asmcode -> asmcode in + | ASMCode asmcode -> asmcode + | PrimusCode funname -> funname in let h_vars = String.concat ~sep:"\n" (List.map p.patch_vars ~f:string_of_hvar) in diff --git a/bap-vibes/src/config.mli b/bap-vibes/src/config.mli index 4f9d257e..33cff49a 100644 --- a/bap-vibes/src/config.mli +++ b/bap-vibes/src/config.mli @@ -13,7 +13,7 @@ type patch type t (** A type to represent patch cody which may either be C or literal assembly *) -type patch_code = CCode of Cabs.definition | ASMCode of string +type patch_code = CCode of Cabs.definition | ASMCode of string | PrimusCode of string (** A type to represent known regions that may be overwritten with patch code *) type patch_space = { diff --git a/bap-vibes/src/data.ml b/bap-vibes/src/data.ml index f84c4882..4100ea8a 100644 --- a/bap-vibes/src/data.ml +++ b/bap-vibes/src/data.ml @@ -44,7 +44,7 @@ let sexp_domain : Sexp.t option KB.Domain.t = KB.Domain.optional "sexp-domain" (* Optional C definition domain for the patch code. *) -let source_domain : Cabs.definition option KB.Domain.t = KB.Domain.optional +let source_domain : Config.patch_code option KB.Domain.t = KB.Domain.optional ~equal:Poly.equal "source-domain" @@ -101,7 +101,7 @@ module Patch = struct let patch_name : (patch_cls, string option) KB.slot = KB.Class.property ~package patch "patch-name" string_domain - let patch_code : (patch_cls, Cabs.definition option) KB.slot = + let patch_code : (patch_cls, Config.patch_code option) KB.slot = KB.Class.property ~package patch "patch-code" source_domain let patch_label : (patch_cls, Theory.label option) KB.slot = @@ -150,13 +150,16 @@ module Patch = struct | None -> Kb_error.fail Kb_error.Missing_patch_name | Some value -> KB.return value - let set_patch_code (obj : t) (data : Cabs.definition option) : unit KB.t = - KB.provide patch_code obj data + let set_patch_code (obj : t) (data : Config.patch_code option) : unit KB.t = + KB.provide patch_code obj data (* (Option.map ~f:(fun c -> Config.CCode c) data) *) - let get_patch_code (obj : t) : Cabs.definition option KB.t = - KB.collect patch_code obj + let get_patch_code (obj : t) : Config.patch_code option KB.t = + KB.collect patch_code obj (* >>= fun res -> + match res with + | Some (CCode code) -> KB.return (Some code) + | _ -> KB.return None *) - let get_patch_code_exn (obj : t) : Cabs.definition KB.t = + let get_patch_code_exn (obj : t) : Config.patch_code KB.t = get_patch_code obj >>= fun result -> match result with | None -> Kb_error.fail Kb_error.Missing_patch_code diff --git a/bap-vibes/src/data.mli b/bap-vibes/src/data.mli index 51cd80c0..0ef9699d 100644 --- a/bap-vibes/src/data.mli +++ b/bap-vibes/src/data.mli @@ -14,7 +14,7 @@ val int_domain : int option KB.Domain.t val int64_domain : int64 option KB.Domain.t val bitvec_domain : Bitvec.t option KB.Domain.t val sexp_domain : Sexp.t option KB.Domain.t -val source_domain : Cabs.definition option KB.Domain.t +val source_domain : Config.patch_code option KB.Domain.t val assembly_domain : string list option KB.Domain.t val unit_domain : unit KB.Domain.t val higher_vars_domain : Hvar.t list option KB.Domain.t @@ -49,7 +49,7 @@ module Patch : sig include Knowledge.Object.S with type t := t val patch_name : (patch_cls, string option) KB.slot - val patch_code : (patch_cls, Cabs.definition option) KB.slot + val patch_code : (patch_cls, Config.patch_code option) KB.slot val patch_point : (patch_cls, Bitvec.t option) KB.slot val patch_size : (patch_cls, int option) KB.slot val patch_label : (patch_cls, Theory.label option) KB.slot @@ -70,9 +70,9 @@ module Patch : sig val get_patch_name : t -> string option KB.t val get_patch_name_exn : t -> string KB.t - val set_patch_code : t -> Cabs.definition option -> unit KB.t - val get_patch_code : t -> Cabs.definition option KB.t - val get_patch_code_exn : t -> Cabs.definition KB.t + val set_patch_code : t -> Config.patch_code option -> unit KB.t + val get_patch_code : t -> Config.patch_code option KB.t + val get_patch_code_exn : t -> Config.patch_code KB.t val set_patch_point : t -> Bitvec.t option -> unit KB.t val get_patch_point : t -> Bitvec.t option KB.t diff --git a/bap-vibes/src/patch_ingester.ml b/bap-vibes/src/patch_ingester.ml index 21e3dc09..63f2f759 100644 --- a/bap-vibes/src/patch_ingester.ml +++ b/bap-vibes/src/patch_ingester.ml @@ -5,6 +5,7 @@ open Bap_knowledge open Knowledge.Syntax open Core_kernel open Bap_core_theory +open Bap_primus.Std module KB = Knowledge open KB.Let @@ -15,15 +16,28 @@ let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t = let module CParser = Core_c.Eval(Core) in Data.Patch.init_sem patch >>= fun () -> Data.Patch.get_patch_name_exn patch >>= fun name -> - Data.Patch.get_patch_code_exn patch >>= fun code -> Events.(send @@ Info (Printf.sprintf "Patch %s" name)); - let code_str = Utils.print_c Cprint.print_def code in - Events.(send @@ Info (Printf.sprintf "%s" code_str)); - + Data.Patch.get_patch_code_exn patch >>= fun code -> (* Get the patch (as BIR). *) - let* hvars = Data.Patch.get_patch_vars_exn patch in - let* bir = CParser.c_patch_to_eff hvars tgt code in - + let* hvars = Data.Patch.get_patch_vars_exn patch in + let* bir = match code with + | CCode code -> begin + let code_str = Utils.print_c Cprint.print_def code in + Events.(send @@ Info (Printf.sprintf "%s" code_str)); + CParser.c_patch_to_eff hvars tgt code + end + | PrimusCode name -> begin + Primus.Lisp.Unit.create tgt >>= fun unit -> + KB.Object.scoped Theory.Program.cls @@ fun obj -> + KB.sequence [ + KB.provide Theory.Label.unit obj (Some unit); + (* KB.provide Theory.Label.addr obj addr; *) + KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name)); + ] >>= fun () -> + KB.collect Theory.Semantics.slot obj + end + | ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented "yolo") + in Events.(send @@ Info "The patch has the following BIL:"); Events.(send @@ Rule); let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot bir) in diff --git a/bap-vibes/src/seeder.ml b/bap-vibes/src/seeder.ml index b39a8b72..d7c145b0 100644 --- a/bap-vibes/src/seeder.ml +++ b/bap-vibes/src/seeder.ml @@ -69,9 +69,10 @@ let create_patches ~addr:(Config.patch_point p) in let* () = Data.Patch.set_patch_name obj (Some patch_name) in + let* () = Data.Patch.set_patch_code obj (Some (Config.patch_code p)) in let* () = match Config.patch_code p with - | CCode ccode -> Data.Patch.set_patch_code obj (Some ccode) | ASMCode asmcode -> Data.Patch.set_assembly obj (Some [asmcode]) + | _ -> KB.return () in let* () = Data.Patch.set_patch_point obj (Some (Config.patch_point p)) in let* () = Data.Patch.set_patch_size obj (Some (Config.patch_size p)) in diff --git a/plugin/lib/vibes_plugin_parameters.ml b/plugin/lib/vibes_plugin_parameters.ml index c9ae1e21..302706ce 100644 --- a/plugin/lib/vibes_plugin_parameters.ml +++ b/plugin/lib/vibes_plugin_parameters.ml @@ -87,15 +87,18 @@ let validate_patch_name (obj : Json.t) : (string, error) Stdlib.result = into a [Cabs.definition] *) let validate_patch_code (nm : string) (obj : Json.t) : (Vibes_config.patch_code, error) Stdlib.result = - match Json.Util.member "patch-code" obj, Json.Util.member "asm-code" obj with - | `String s, `Null -> - (match Parse_c.parse_c_patch s with - | Ok code -> Ok (Vibes_config.CCode code) - | Error msg -> Error (Errors.Invalid_patch_code msg)) - | `Null, `String s -> Ok (Vibes_config.ASMCode s) - | `String s, `String s' -> Error + match Json.Util.member "patch-code" obj, Json.Util.member "asm-code" obj, Json.Util.member "lisp-code" obj with + | `String s, `Null, `Null -> + (match Parse_c.parse_c_patch s with + | Ok code -> Ok (Vibes_config.CCode code) + | Error msg -> Error (Errors.Invalid_patch_code msg)) + | `Null, `String s, `Null -> Ok (Vibes_config.ASMCode s) + | `Null, `Null, `String s -> Ok (Vibes_config.PrimusCode s) + | `String s, `String s', _ + | _, `String s', `String s + | `String s, _, `String s' -> Error (Errors.Invalid_patch_code "Specified both assembly and C code in patch") - | _, _ -> Err.fail Errors.Missing_patch_code + | _, _, _ -> Err.fail Errors.Missing_patch_code (* Extract the patch point field and parse the hex string into a bitvector, or error. *) diff --git a/resources/exes/arm-simple-primus/Makefile b/resources/exes/arm-simple-primus/Makefile new file mode 100644 index 00000000..8bc2e9b5 --- /dev/null +++ b/resources/exes/arm-simple-primus/Makefile @@ -0,0 +1,106 @@ +SRC := main.c + +PROG := main +PATCHED_PROG := main.patched + +REF_PROG := main.reference +PATCHED_REF_PROG := main.patched.reference + +PATCHED_PROG_FOR_TESTING := test.patched.by.vibes + + +##################################################### +# DEFAULT +##################################################### + +.DEFAULT_GOAL := all +all: clean build patch + + +##################################################### +# BUILD +##################################################### + +build: $(PROG) +$(PROG): $(SRC) + arm-linux-gnueabi-gcc -marm -o $@ $< + + +##################################################### +# CLEAN +##################################################### + +.PHONY: clean +clean: + rm -rf $(OBJ) $(PROG) $(PATCHED_PROG) $(PATCHED_PROG_FOR_TESTING) + + +##################################################### +# PATCH +##################################################### + +$(PATCHED_PROG): $(PROG) + bap vibes $(PROG) \ + --config=config.json \ + --primus-lisp-load=patch \ + -o $(PATCHED_PROG) \ + --verbose + chmod +x $(PATCHED_PROG) + +patch: $(PATCHED_PROG) + + +##################################################### +# PATCH THE REFERENCE EXECUTABLE +##################################################### + +$(PATCHED_PROG_FOR_TESTING): $(REF_PROG) + bap vibes $(REF_PROG) \ + --config=config.json \ + -o $(PATCHED_PROG_FOR_TESTING) \ + --verbose + chmod +x $(PATCHED_PROG_FOR_TESTING) + +patch.reference: $(PATCHED_PROG_FOR_TESTING) + + +##################################################### +# CREATE REFERENCE FILES +##################################################### + +$(REF_PROG): + $(MAKE) $(PROG) + cp $(PROG) $(REF_PROG) + +$(PATCHED_REF_PROG): + $(MAKE) patch.reference + cp $(PATCHED_PROG_FOR_TESTING) $(PATCHED_REF_PROG) + +reference: + rm -rf $(REF_PROG) $(PATCHED_REF_PROG) + $(MAKE) $(REF_PROG) + $(MAKE) $(PATCHED_REF_PROG) + + +##################################################### +# RUN +##################################################### + +.PHONY: run.orig +run.orig: $(PROG) + -QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PROG) + +.PHONY: run.patched +run.patched: $(PATCHED_PROG) + -QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PATCHED_PROG) + +.PHONY: run.ref +run.ref: $(REF_PROG) + -QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(REF_PROG) + +.PHONY: run.patched-ref +run.patched-ref: $(PATCHED_REF_PROG) + -QEMU_LD_PREFIX=/usr/arm-linux-gnueabi qemu-arm $(PATCHED_REF_PROG) + +.PHONY: run.test +run.test: run.orig run.patched diff --git a/resources/exes/arm-simple-primus/README.md b/resources/exes/arm-simple-primus/README.md new file mode 100644 index 00000000..411761fc --- /dev/null +++ b/resources/exes/arm-simple-primus/README.md @@ -0,0 +1,29 @@ +# ARM Simple Compiled + +To clean, build, and patch: + + make + +To build: + + make build + +To patch: + + make patch + +To run the executable and the patched executable (in qemu): + + make run.test + +To create reference versions of the executables: + + make reference + +To patch the reference executable: + + make patch.reference + +To clean: + + make clean diff --git a/resources/exes/arm-simple-primus/config.json b/resources/exes/arm-simple-primus/config.json new file mode 100644 index 00000000..e267eba7 --- /dev/null +++ b/resources/exes/arm-simple-primus/config.json @@ -0,0 +1,25 @@ +{ + "max-tries": 3, + "wp-params": { + "func": "main", + "postcond" : "(assert (= (bvadd R0_mod #x00000002) R0_orig))" + }, + "patches" : [ + {"patch-name" : "ret-3", + "lisp-code" : "ret-3", + "patch-point" : "0x103d4", + "patch-size" : 8, + "patch-vars": [ + {"name": "retvar", + "at-entry": { + "stored-in": "register", + "register": "R0" + }, + "at-exit": { + "stored-in": "register", + "register": "R12" + }} + ] + } + ] +} diff --git a/resources/exes/arm-simple-primus/main.c b/resources/exes/arm-simple-primus/main.c new file mode 100644 index 00000000..98941446 --- /dev/null +++ b/resources/exes/arm-simple-primus/main.c @@ -0,0 +1,4 @@ + +int main() { + return 5; +} diff --git a/resources/exes/arm-simple-primus/main.patched.reference b/resources/exes/arm-simple-primus/main.patched.reference new file mode 100755 index 0000000000000000000000000000000000000000..b1da377ce360cb8564e4390b1c66799ac6f99297 GIT binary patch literal 7968 zcmeHMUu;`f89&!{x|AlJle(GPWt*i1=#YHlwi#QdBISQt%}qn=RYO#}xv_5&YqoD> zUqdpDuE5YHG1LM>n$Si(3Go1v2nfUjbSi9u36L0qhdm6*PGZ(kkix?TFVy^g=lCQy zT_?1MNj&&#znt%PzVCeJobQ}_@A;0O7*9?Zh9NWs#34cSM!*mQD4#osKLOD;AYx)S zba#ke>K9WXAyOejayv}OsFJ)3CEE_bk{m+=vepNoO97|QFL@s@nR--9M$wcEF#`p; ztyxE#@U7&4W6c7tl9(4E1EK`*hvQ0KSLVJ`6q$ zy}$oW)REbqW9!dlXZv%RcrIHgFPSCRJgRhTOa0{3L-;EM!z8b2=>!IpOeQ)(*wSDvD z`gA7@e|>Q+{M%>NrvLMcx|Waoi7*}XDjyZpAtqr=Ms9>n9dtn1(t8Grk-%ie~)RWUI z^<6U;t8LTZnTe`ctkjGPm0I8u#st3;_G)eOsmtwRsIqPhJ-HT2d~0JjV%Hw7)NT=# z+EMrliLoRXhonEfmQ@s5okrA z6@mZz2)v5(|MOs;U&$TdXORmdff2`%BOE}7DX}ZqZtOO?L;H+~vER5Y7&Q(U2e-RsH(SIz0a8$| zfXdSqRt=us(#z-x##`yRA}Zbr%Pd*0gTm^DK*uR4Zeg`x97#bLSru=EcguRNgTh=z zwI38#*)wCNFn5c(J5iXsM(rDg_ewmCeWb8T*LjbkFn5L!=eDrQ*16wELAeXmep8sc zLEUpG%o_wyGw%#GcUkWi?vZMpmj>l7lU4FhQ0_oKKG0kNRTmQfY&;B+cP5Gg;b*tJ)Rnb$ofRqW%9&i$48^Pfvfxw&LF@$H%)F-Tub)puK)x zc)RrqOf^<-&t_8;9M2!2*YoFm)`0ap5VslP8nB)p_1A&*^JL(8V!ZV8&aVUeU)|b2 z9a8@jAC4gO96#So-Po^_z{hhxC!f%Sgt3iODt0`vLgc)Rd?ejAwUGXu=={{`{zkMBX~_47~t z_ksQT9|Qa6_cAc|1HYHFf5oR~|9=41#PRadQ$Nq${Cf76OGSCXI-gF*(?z#b>bHw| zb=Ml7FO>P&>A$bvG`Ii1SI-MtSg=SJy~Cy}`ZA)={xF`-VdO<*jtiEjT6I)n;64KIhKbIVF=wp7}>mA0IW?b*#rr;w3-vPxO#*4r1{LqqR-!;K)8Tx-EDWO9zMPMm^^ zOtxT^OAf}pJqpeUSa-HH8X@n`Eh}|$v^jfu$L{Y?n5E^sXV0SaimF`DQnr94T@+@) z^&E3}1>0G@YevW=WXNg4zMfTrIvb*D{>i`D_{;x^Sc%ASS}Z z?#p9G3F*%Eykd5?>|w8d0Jp7v;`e)qw953(k8aunh) zDzqKXnNPz(pEg3N?ZzO#i!(R<@%;Hx(@vc@l^t!Tz&s_=j(NcAup5HRlPE;#kEgz~ zV4h}a$Gm}`0OkvtXiMVxh-ZG<@f@3kzwH?1RZ@}LoE1IPJJqN7q_lkwxZKyA|MbC(5bKqCP1PH9`-OKJBe9GK?)BWyioJ|o#T_- zbe+&1Ch_2}{c^tF`M&d=bG~!#z2`fAd@MO`7>3Xk5C;U&n*l=%pnQHm{sctZfQX5m z(A^<=sb5High+)9$?Y&9qe}7)lx#ZyOL7bi$XXwSE(M%IzvMl@Wa?2Z8AVev#55G- zwq_k|!ncwGk|U^yg4r)y2kwQVVOgxPN}gTxth}8qh>7I!;SuYQIRM>U-YqnBmh=?B2o3p9#fp`Y zY_^jlzq{F2G#n6nF^LY8J(xh4C2)i#CeuC`f9DP%uC<@PbTw3s*F)9i`tIt5YWv2k z^{Gx6{`$gd__xojPW|T>buAzB$%B+vDr=%zSqp_`Je5=h(mM`?Gk@x zKWpLhm!egS)kt7&iP!7ESJ}s3F|N=`9CQB0Y8!MxQK^Y5Pp^hnUR=l6Y8w;rcaqb~ z_2krYeaG~LYTFcedb}zYDmCMLr53n|F~RS+y;9qF@>07PtgIP>PppO#-(KH|*tLf% zwOioxFnoo?ncBY^js38@+Pe#}0<#aU8P|(X-xJpxk7Jcu)QUhW0<8$NBG8IJD*~+u zv?9=o!2f*&UdQ?W1u)OAh-1hR_Mv3nc{@txY)p?Mz`afU?)8TI3UW&3 zXJNEs&Ugj*V3?KSHDukedfJpB7V3mD-WJK zc)yt#xJT8Bp?lECcI=s~Fz$lbc5h1T2(}wLjqcDMBVz0|ZVN_@ea8N+uG!5d@lJpg zlq;a}bcI!er#AI6dV=v*daj6yx56?@mg}Ifx*^bU3W{4;Ef_~qP)1h8Tj8Cup6j46 zS5fT;g;n;J-%L`EaKbx8r&8>-GGFxK--)_=M;Y4>v7Yus`~b_}c%}hXZ&j=|ADq)1J?( zqFr))d~Ox(7QbprEVTa@Zm>`K?Dy%WKKuK9{q;ewu^!JuK0U{i@!?OvUSn;4(WmEp zV$JnpJlLM^BSoF!2t5uOxMSH}jbdg?=h@zAFz&J81Z`m_&{_0i4Sel_lP@z^?vRayTy?k z?8kt$|1kWY0@lQDi0i{K;B&xwzjXzA#M8ihJ~`elJfGhI=K4$nbNqinJpAMPEcE*M zr~doEe*KSu{quVjnEQd>OWMEY)3g6S0BhoSdFiR2=Wc#I`^%-GykMP6r{n3OTPpS2 z#k{&}jn5Uz{Ot7K*Ke9z|KG3Y1uZOCq>J7`(-nOg(Pw`Y&a-fywsSe_OOE}BHCy;7 z`Y5oEqF3_Dv$JMeWSpWimo0ft(emE`-b#i?C^jOMD4Gky9 z=t5pmr%PoyRN$FXY4cXvax%7OH!Gb&M)t`nWuaSdU2qQ$e&7u^f>?5`dApFwIl?-A z5-u{?f>ka#828pFI3r-)+2&}3yg#?B)QOSi?ByN1ze8b`mhzrGgVHOia$ZZ>0+w_^ zm<88!%%S1qanGJ>B5Ztfrkur(4%v(_iRSInyf8CM1^82?S5%rWI>l1fEo=i8bVVme zdnGL7JYmXtn4Yr;nVSGAR|eA@I(5Qy7PFZ}VLJ0_2Pkv3_{v<%aBAnXX>{nqk#c~T z2ot+6j~ykXJKOV$*_pD3z4{^OcG&V2&DVzdJxQIBwF~MdWZw4DU=lt??~0asu*2$?5Qh|(WV zeP_Tt&C-r}13v-G7c|k9#Pbo){IugaHVJ|GfbN&|JRP6-vnzrerMizqet>divvc zy$^Q&dC&*x?_kOa0ub%AOiUg5T`+ttppcY;-KR7_sr|9U(r?mv`a=Nt{PP*(7*Hkm esGKWg(h5?Zs;{B;$IQxacM*wwn^r=n#s322-x2u$ literal 0 HcmV?d00001 diff --git a/resources/exes/arm-simple-primus/main.s b/resources/exes/arm-simple-primus/main.s new file mode 100644 index 00000000..94617049 --- /dev/null +++ b/resources/exes/arm-simple-primus/main.s @@ -0,0 +1,33 @@ + .arch armv5t + .eabi_attribute 20, 1 + .eabi_attribute 21, 1 + .eabi_attribute 23, 3 + .eabi_attribute 24, 1 + .eabi_attribute 25, 1 + .eabi_attribute 26, 2 + .eabi_attribute 30, 6 + .eabi_attribute 34, 0 + .eabi_attribute 18, 4 + .file "main.c" + .text + .align 2 + .global main + .syntax unified + .arm + .fpu softvfp + .type main, %function +main: + @ args = 0, pretend = 0, frame = 0 + @ frame_needed = 1, uses_anonymous_args = 0 + @ link register save eliminated. + str fp, [sp, #-4]! + add fp, sp, #0 + mov r3, #5 + mov r0, r3 + add sp, fp, #0 + @ sp needed + ldr fp, [sp], #4 + bx lr + .size main, .-main + .ident "GCC: (Ubuntu/Linaro 7.5.0-3ubuntu1~18.04) 7.5.0" + .section .note.GNU-stack,"",%progbits diff --git a/resources/exes/arm-simple-primus/patch.lisp b/resources/exes/arm-simple-primus/patch.lisp new file mode 100644 index 00000000..e52d3754 --- /dev/null +++ b/resources/exes/arm-simple-primus/patch.lisp @@ -0,0 +1,4 @@ +(defun ret-3 () + ; (external "ret_patch") + (set R0 3) +) \ No newline at end of file From 18ff13318216ebdda43d8fa26f374ac401ee9173 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Mon, 3 Jan 2022 17:17:17 -0500 Subject: [PATCH 2/4] cleanup. Renamed errenous bir variable to sem --- bap-vibes/src/compiler.ml | 79 +++++++++++--------- bap-vibes/src/data.ml | 12 +-- bap-vibes/src/data.mli | 5 +- bap-vibes/src/patch_ingester.ml | 52 ++++++------- bap-vibes/src/seeder.ml | 4 - bap-vibes/tests/integration/test_minizinc.ml | 2 +- bap-vibes/tests/unit/test_compiler.ml | 2 +- bap-vibes/tests/unit/test_patch_ingester.ml | 6 +- bin/system-tests/tests/test-arm-exes.bash | 20 +++++ plugin/lib/vibes_plugin_parameters.ml | 4 +- resources/exes/arm-simple-primus/patch.lisp | 3 +- 11 files changed, 104 insertions(+), 85 deletions(-) diff --git a/bap-vibes/src/compiler.ml b/bap-vibes/src/compiler.ml index 89bfcc94..925969b6 100644 --- a/bap-vibes/src/compiler.ml +++ b/bap-vibes/src/compiler.ml @@ -61,20 +61,24 @@ let create_vibes_ir ir, exclude_regs (* Compile one patch from BIR to VIBES IR *) -let compile_one_vibes_ir - (isel_model_filepath : string option) +let compile_one_vibes_ir + (isel_model_filepath : string option) (count : int KB.t) (patch : Data.Patch.t) : int KB.t = - count >>= fun n -> Data.Patch.get_assembly patch >>= begin function - | Some _asm -> - Events.(send @@ Info "The patch has no IR to translate.\n"); - KB.return () (* Assembly already set. Presumably by the user. *) - | None -> + count >>= fun n -> + Data.Patch.get_patch_code_exn patch >>= (fun code -> + match code with + | ASMCode _asm -> + Events.(send @@ Info "Assembly patch has no IR to translate.\n"); + KB.return () + | PrimusCode _ | CCode _ -> + begin let info_str = - Format.sprintf "Translating patch %d BIR to VIBES IR..." n + Format.asprintf "Translating patch %s BIR to VIBES IR..." + (string_of_int n) in Events.(send @@ Info info_str); - Data.Patch.get_bir patch >>= fun bir -> + Data.Patch.get_sem patch >>= fun bir -> let info_str = Format.asprintf "\nPatch: %a\n\n%!" KB.Value.pp bir in Events.(send @@ Info info_str); @@ -103,34 +107,35 @@ let compile_one_assembly Ir.t -> (Ir.t * Minizinc.sol) KB.t) (count : int KB.t) (patch : Data.Patch.t) : int KB.t = - count >>= fun n -> Data.Patch.get_assembly patch >>= begin function - | Some _asm -> - Events.(send @@ Info "The patch already has assembly\n"); - Events.(send @@ Rule); - KB.return () (* Assembly already set. Presumably by the user. *) - | None -> - let info_str = - Format.asprintf "Translating patch %s VIBES IR to assembly..." - (string_of_int n) - in - Events.(send @@ Info info_str); - Data.Patch.get_raw_ir_exn patch >>= fun ir -> - Data.Patch.get_exclude_regs patch >>= fun exclude_regs -> - let exclude_regs = Option.value exclude_regs ~default:String.Set.empty in - Data.Patch.get_minizinc_solutions patch >>= fun prev_sols -> - Data.Patch.get_target patch >>= fun target -> - Data.Patch.get_lang patch >>= fun lang -> - let prev_sols = Set.to_list prev_sols in - create_assembly - (solver target lang prev_sols ~exclude_regs) - ir >>= fun (assembly, new_sol) -> - Data.Patch.set_assembly patch (Some assembly) >>= fun () -> - Events.(send @@ Info "The patch has the following assembly:\n"); - Events.(send @@ Rule); - Events.(send @@ Info (String.concat ~sep:"\n" assembly)); - Events.(send @@ Rule); - Data.Patch.add_minizinc_solution patch new_sol - end >>= fun () -> KB.return (n + 1) + count >>= fun n -> + Data.Patch.get_patch_code_exn patch >>= (fun asm -> + match asm with + | ASMCode asm -> KB.return [asm] + | PrimusCode _ | CCode _ -> + begin + let info_str = + Format.asprintf "Translating patch %s VIBES IR to assembly..." + (string_of_int n) + in + Events.(send @@ Info info_str); + Data.Patch.get_raw_ir_exn patch >>= fun ir -> + Data.Patch.get_exclude_regs patch >>= fun exclude_regs -> + Data.Patch.get_minizinc_solutions patch >>= fun prev_sols -> + Data.Patch.get_target patch >>= fun target -> + Data.Patch.get_lang patch >>= fun lang -> + let prev_sols = Set.to_list prev_sols in + create_assembly + (solver target lang prev_sols ~exclude_regs) + ir >>= fun (assembly, new_sol) -> + Data.Patch.add_minizinc_solution patch new_sol >>= fun () -> + KB.return assembly + end) >>= fun assembly -> + Data.Patch.set_assembly patch (Some assembly) >>= fun () -> + Events.(send @@ Info "The patch has the following assembly:\n"); + Events.(send @@ Rule); + Events.(send @@ Info (String.concat ~sep:"\n" assembly)); + Events.(send @@ Rule); + KB.return (n + 1) (* Converts the patch (as BIR) to VIBES IR instructions. *) let compile_ir ?(isel_model_filepath = None) (obj : Data.t) : unit KB.t = diff --git a/bap-vibes/src/data.ml b/bap-vibes/src/data.ml index 4100ea8a..dea6199a 100644 --- a/bap-vibes/src/data.ml +++ b/bap-vibes/src/data.ml @@ -2,7 +2,6 @@ We expect much evolution here... *) open !Core_kernel -open Bap.Std open Bap_knowledge open Bap_core_theory open Knowledge.Syntax @@ -151,13 +150,10 @@ module Patch = struct | Some value -> KB.return value let set_patch_code (obj : t) (data : Config.patch_code option) : unit KB.t = - KB.provide patch_code obj data (* (Option.map ~f:(fun c -> Config.CCode c) data) *) + KB.provide patch_code obj data let get_patch_code (obj : t) : Config.patch_code option KB.t = - KB.collect patch_code obj (* >>= fun res -> - match res with - | Some (CCode code) -> KB.return (Some code) - | _ -> KB.return None *) + KB.collect patch_code obj let get_patch_code_exn (obj : t) : Config.patch_code KB.t = get_patch_code obj >>= fun result -> @@ -193,13 +189,13 @@ module Patch = struct KB.Object.create Theory.Program.cls >>= fun lab -> KB.provide patch_label obj (Some lab) - let set_bir (obj : t) (sem : Insn.t) : unit KB.t = + let set_sem (obj : t) (sem : Theory.Semantics.t) : unit KB.t = KB.collect patch_label obj >>= fun olab -> (* FIXME: fail more gracefully *) let lab = Option.value_exn olab in KB.provide Theory.Semantics.slot lab sem - let get_bir (obj : t) : Insn.t KB.t = + let get_sem (obj : t) : Theory.Semantics.t KB.t = KB.collect patch_label obj >>= fun olab -> (* FIXME: fail more gracefully *) let lab = Option.value_exn olab in diff --git a/bap-vibes/src/data.mli b/bap-vibes/src/data.mli index 0ef9699d..6e3132cb 100644 --- a/bap-vibes/src/data.mli +++ b/bap-vibes/src/data.mli @@ -2,7 +2,6 @@ properties that the VIBES toolchain defines and manipulates *) open !Core_kernel -open Bap.Std open Bap_knowledge open Bap_core_theory @@ -86,8 +85,8 @@ module Patch : sig that will contain the semantics. This *must* be called before set_bir! *) val init_sem : t -> unit KB.t - val set_bir : t -> insn -> unit KB.t - val get_bir : t -> insn KB.t + val set_sem : t -> Theory.Semantics.t -> unit KB.t + val get_sem : t -> Theory.Semantics.t KB.t val set_raw_ir : t -> Ir.t option -> unit KB.t val get_raw_ir : t -> Ir.t option KB.t diff --git a/bap-vibes/src/patch_ingester.ml b/bap-vibes/src/patch_ingester.ml index 63f2f759..fb2b41b9 100644 --- a/bap-vibes/src/patch_ingester.ml +++ b/bap-vibes/src/patch_ingester.ml @@ -10,7 +10,7 @@ open Bap_primus.Std module KB = Knowledge open KB.Let -let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t = +let provide_sem (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t = Theory.instance () >>= Theory.require >>= fun (module Core) -> let module CParser = Core_c.Eval(Core) in @@ -20,30 +20,32 @@ let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t = Data.Patch.get_patch_code_exn patch >>= fun code -> (* Get the patch (as BIR). *) let* hvars = Data.Patch.get_patch_vars_exn patch in - let* bir = match code with - | CCode code -> begin - let code_str = Utils.print_c Cprint.print_def code in - Events.(send @@ Info (Printf.sprintf "%s" code_str)); - CParser.c_patch_to_eff hvars tgt code - end - | PrimusCode name -> begin - Primus.Lisp.Unit.create tgt >>= fun unit -> - KB.Object.scoped Theory.Program.cls @@ fun obj -> - KB.sequence [ - KB.provide Theory.Label.unit obj (Some unit); - (* KB.provide Theory.Label.addr obj addr; *) - KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name)); - ] >>= fun () -> - KB.collect Theory.Semantics.slot obj - end - | ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented "yolo") - in + let* sem = match code with + | CCode code -> + begin + let code_str = Utils.print_c Cprint.print_def code in + Events.(send @@ Info (Printf.sprintf "%s" code_str)); + CParser.c_patch_to_eff hvars tgt code + end + | PrimusCode name -> + begin + Primus.Lisp.Unit.create tgt >>= fun unit -> + KB.Object.scoped Theory.Program.cls @@ fun obj -> + KB.sequence [ + KB.provide Theory.Label.unit obj (Some unit); + KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name)); + ] >>= fun () -> + KB.collect Theory.Semantics.slot obj + end + | ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented + "[Patch_ingester.provide_sem] called on assembly patch") + in Events.(send @@ Info "The patch has the following BIL:"); Events.(send @@ Rule); - let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot bir) in + let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot sem) in Events.(send @@ Info bir_str); Events.(send @@ Rule); - Data.Patch.set_bir patch bir + Data.Patch.set_sem patch sem (* Ingests a single patch, populating the relevant fields of the KB, most notably the semantics field of the corresponding patch (and @@ -52,10 +54,10 @@ let ingest_one (tgt : Theory.target) (patch_num : int KB.t) (patch : Data.Patch. : int KB.t = patch_num >>= fun patch_num -> Events.(send @@ Info (Printf.sprintf "\nIngesting patch %d." patch_num)); - (Data.Patch.get_assembly patch >>= fun asm -> - match asm with - | Some _asm -> KB.return () (* Assembly is user provided *) - | None -> provide_bir tgt patch) >>= fun () -> + (Data.Patch.get_patch_code_exn patch >>= fun code -> + match code with + | ASMCode _asm -> KB.return () (* Assembly is user provided *) + | PrimusCode _ | CCode _ -> provide_sem tgt patch) >>= fun () -> KB.return @@ patch_num+1 (* Processes the whole patch associated with [obj], populating all the diff --git a/bap-vibes/src/seeder.ml b/bap-vibes/src/seeder.ml index d7c145b0..d5294420 100644 --- a/bap-vibes/src/seeder.ml +++ b/bap-vibes/src/seeder.ml @@ -70,10 +70,6 @@ let create_patches in let* () = Data.Patch.set_patch_name obj (Some patch_name) in let* () = Data.Patch.set_patch_code obj (Some (Config.patch_code p)) in - let* () = match Config.patch_code p with - | ASMCode asmcode -> Data.Patch.set_assembly obj (Some [asmcode]) - | _ -> KB.return () - in let* () = Data.Patch.set_patch_point obj (Some (Config.patch_point p)) in let* () = Data.Patch.set_patch_size obj (Some (Config.patch_size p)) in let* () = Data.Patch.set_lang obj lang in diff --git a/bap-vibes/tests/integration/test_minizinc.ml b/bap-vibes/tests/integration/test_minizinc.ml index 67d60ff3..2a5f0dfc 100644 --- a/bap-vibes/tests/integration/test_minizinc.ml +++ b/bap-vibes/tests/integration/test_minizinc.ml @@ -110,7 +110,7 @@ let test_minizinc_ex1 (ctxt : test_ctxt) : unit = KB.Object.create Data.Patch.patch >>= fun patch -> Data.Patch.init_sem patch >>= fun () -> Patches.get_bir "ret-3" 32 >>= fun bil -> - Data.Patch.set_bir patch bil >>= fun () -> + Data.Patch.set_sem patch bil >>= fun () -> Data.Patched_exe.set_patches obj (Data.Patch_set.singleton patch) >>= fun () -> (* Now run the compiler. *) diff --git a/bap-vibes/tests/unit/test_compiler.ml b/bap-vibes/tests/unit/test_compiler.ml index b7c6d4fc..c1c3b2a3 100644 --- a/bap-vibes/tests/unit/test_compiler.ml +++ b/bap-vibes/tests/unit/test_compiler.ml @@ -26,7 +26,7 @@ let test_compile (_ : test_ctxt) : unit = obj (Some H.minizinc_model_filepath) >>= fun () -> Patches.get_bir H.patch 32 >>= fun bil -> KB.Object.create Data.Patch.patch >>= fun patch -> - Data.Patch.set_bir patch bil >>= fun _ -> + Data.Patch.set_sem patch bil >>= fun _ -> Data.Patched_exe.set_patches obj (Data.Patch_set.singleton patch) >>= fun _ -> diff --git a/bap-vibes/tests/unit/test_patch_ingester.ml b/bap-vibes/tests/unit/test_patch_ingester.ml index b0d06077..6f328029 100644 --- a/bap-vibes/tests/unit/test_patch_ingester.ml +++ b/bap-vibes/tests/unit/test_patch_ingester.ml @@ -27,7 +27,7 @@ let test_ingest (_ : test_ctxt) : unit = match Data.Patch_set.to_list patches with | [] -> assert_failure "Result patch missing." | (p :: []) -> - Data.Patch.get_bir p >>= fun bir -> + Data.Patch.get_sem p >>= fun bir -> Patches.Ret_3.prog 32 >>= fun expected -> let open Bap.Std in let expected = KB.Value.get Bil.slot expected in @@ -61,7 +61,7 @@ let test_ingest_with_no_patch (_ : test_ctxt) : unit = let result = KB.run Data.cls computation KB.empty in (* The ingester should diverge with the appropriate error. *) - let expected = Kb_error.Problem Kb_error.Missing_patch_name in + let expected = Kb_error.Problem Kb_error.Missing_patch_code in H.assert_error Data.Patched_exe.patches expected result (* Test that [Patch_ingester.ingest] errors with no addr_size in the KB. *) @@ -100,7 +100,7 @@ let test_ingest_with_no_patch_vars (_ : test_ctxt) : unit = KB.Object.create Data.Patch.patch >>= fun patch -> let code = H.dummy_code in - Data.Patch.set_patch_code patch (Some code) >>= fun () -> + Data.Patch.set_patch_code patch (Some (CCode code)) >>= fun () -> Data.Patch.set_patch_name patch (Some H.patch) >>= fun () -> Data.Patched_exe.set_patches obj (Data.Patch_set.singleton patch) >>= fun () -> diff --git a/bin/system-tests/tests/test-arm-exes.bash b/bin/system-tests/tests/test-arm-exes.bash index 9adfbf33..50b3a978 100644 --- a/bin/system-tests/tests/test-arm-exes.bash +++ b/bin/system-tests/tests/test-arm-exes.bash @@ -219,9 +219,26 @@ test_arm_linear_ssa () { run_make "make patch.reference -C ${TEST_DIR}" 0 run_arm_exe "${TEST_PATCH_EXE}" 3 } +test_arm_primus () { + local TEST_DIR="${EXES_DIR}/arm-simple-primus" + local MAIN_EXE="${TEST_DIR}/main.reference" + local PATCH_EXE="${TEST_DIR}/main.patched.reference" + local TEST_PATCH_EXE="${TEST_DIR}/test.patched.by.vibes" + + print_header "Checking ${TEST_DIR}" + # Check the precompiled executables. + run_arm_exe "${MAIN_EXE}" 15 + run_arm_exe "${PATCH_EXE}" 17 + + # Check that vibes patches correctly. + run_make "make clean -C ${TEST_DIR}" 0 + run_make "make patch.reference -C ${TEST_DIR}" 0 + run_arm_exe "${TEST_PATCH_EXE}" 3 +} test_arm_simple_sum () { local TEST_DIR="${EXES_DIR}/arm-simple-sum" + local MAIN_EXE="${TEST_DIR}/main.reference" local PATCH_EXE="${TEST_DIR}/main.patched.reference" local TEST_PATCH_EXE="${TEST_DIR}/test.patched.by.vibes" @@ -232,6 +249,7 @@ test_arm_simple_sum () { run_arm_exe "${MAIN_EXE}" 5 run_arm_exe "${PATCH_EXE}" 9 + # Check that vibes patches correctly. run_make "make clean -C ${TEST_DIR}" 0 run_make "make patch.reference -C ${TEST_DIR}" 0 @@ -276,12 +294,14 @@ test_arm_branch_bsi () { run_make "make clean -C ${TEST_DIR}" 0 run_make "make main.patched -C ${TEST_DIR}" 0 run_arm_exe "${TEST_PATCH_EXE}" 2 + } # Run all tests run_all () { test_arm_simple test_arm_simple_sum + test_arm_primus test_arm_simple_inline test_arm_simple_cegis test_arm_simple_compiled diff --git a/plugin/lib/vibes_plugin_parameters.ml b/plugin/lib/vibes_plugin_parameters.ml index 302706ce..135ad1b6 100644 --- a/plugin/lib/vibes_plugin_parameters.ml +++ b/plugin/lib/vibes_plugin_parameters.ml @@ -87,7 +87,9 @@ let validate_patch_name (obj : Json.t) : (string, error) Stdlib.result = into a [Cabs.definition] *) let validate_patch_code (nm : string) (obj : Json.t) : (Vibes_config.patch_code, error) Stdlib.result = - match Json.Util.member "patch-code" obj, Json.Util.member "asm-code" obj, Json.Util.member "lisp-code" obj with + match Json.Util.member "patch-code" obj, + Json.Util.member "asm-code" obj, + Json.Util.member "lisp-code" obj with | `String s, `Null, `Null -> (match Parse_c.parse_c_patch s with | Ok code -> Ok (Vibes_config.CCode code) diff --git a/resources/exes/arm-simple-primus/patch.lisp b/resources/exes/arm-simple-primus/patch.lisp index e52d3754..e5531601 100644 --- a/resources/exes/arm-simple-primus/patch.lisp +++ b/resources/exes/arm-simple-primus/patch.lisp @@ -1,4 +1,3 @@ (defun ret-3 () - ; (external "ret_patch") (set R0 3) -) \ No newline at end of file +) From a427e35fa6573980e685aa0847324d4709953ea8 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Mon, 3 Jan 2022 17:29:04 -0500 Subject: [PATCH 3/4] fixed test --- bin/system-tests/tests/test-arm-exes.bash | 6 +++--- resources/exes/arm-simple-primus/Makefile | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/bin/system-tests/tests/test-arm-exes.bash b/bin/system-tests/tests/test-arm-exes.bash index 50b3a978..94edbc3a 100644 --- a/bin/system-tests/tests/test-arm-exes.bash +++ b/bin/system-tests/tests/test-arm-exes.bash @@ -228,9 +228,9 @@ test_arm_primus () { print_header "Checking ${TEST_DIR}" # Check the precompiled executables. - run_arm_exe "${MAIN_EXE}" 15 - run_arm_exe "${PATCH_EXE}" 17 - + run_arm_exe "${MAIN_EXE}" 5 + run_arm_exe "${PATCH_EXE}" 3 + # Check that vibes patches correctly. run_make "make clean -C ${TEST_DIR}" 0 run_make "make patch.reference -C ${TEST_DIR}" 0 diff --git a/resources/exes/arm-simple-primus/Makefile b/resources/exes/arm-simple-primus/Makefile index 8bc2e9b5..c9c8a24a 100644 --- a/resources/exes/arm-simple-primus/Makefile +++ b/resources/exes/arm-simple-primus/Makefile @@ -57,6 +57,7 @@ patch: $(PATCHED_PROG) $(PATCHED_PROG_FOR_TESTING): $(REF_PROG) bap vibes $(REF_PROG) \ --config=config.json \ + --primus-lisp-load=patch \ -o $(PATCHED_PROG_FOR_TESTING) \ --verbose chmod +x $(PATCHED_PROG_FOR_TESTING) From 4e1003909cc467b549f65c7f9446d52c2cbe8797 Mon Sep 17 00:00:00 2001 From: Philip Zucker Date: Wed, 2 Feb 2022 11:09:33 -0500 Subject: [PATCH 4/4] updated primus test with larger max iteration. Has something changed in preassignment? --- bap-vibes/src/compiler.ml | 3 ++- resources/exes/arm-simple-primus/README.md | 4 +++- resources/exes/arm-simple-primus/config.json | 2 +- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/bap-vibes/src/compiler.ml b/bap-vibes/src/compiler.ml index 925969b6..259dc0bb 100644 --- a/bap-vibes/src/compiler.ml +++ b/bap-vibes/src/compiler.ml @@ -95,7 +95,7 @@ let compile_one_vibes_ir Events.(send @@ Info (Ir.pretty_ir ir)); Events.(send @@ Rule); KB.return () - end >>= fun () -> KB.return (n + 1) + end) >>= fun () -> KB.return (n + 1) (* Compile one patch from VIBES IR to assembly *) let compile_one_assembly @@ -120,6 +120,7 @@ let compile_one_assembly Events.(send @@ Info info_str); Data.Patch.get_raw_ir_exn patch >>= fun ir -> Data.Patch.get_exclude_regs patch >>= fun exclude_regs -> + let exclude_regs = Option.value exclude_regs ~default:String.Set.empty in Data.Patch.get_minizinc_solutions patch >>= fun prev_sols -> Data.Patch.get_target patch >>= fun target -> Data.Patch.get_lang patch >>= fun lang -> diff --git a/resources/exes/arm-simple-primus/README.md b/resources/exes/arm-simple-primus/README.md index 411761fc..00168e8e 100644 --- a/resources/exes/arm-simple-primus/README.md +++ b/resources/exes/arm-simple-primus/README.md @@ -1,4 +1,6 @@ -# ARM Simple Compiled +# ARM Simple Primus + +Testing the primus code specification To clean, build, and patch: diff --git a/resources/exes/arm-simple-primus/config.json b/resources/exes/arm-simple-primus/config.json index e267eba7..5ebd5cd3 100644 --- a/resources/exes/arm-simple-primus/config.json +++ b/resources/exes/arm-simple-primus/config.json @@ -1,5 +1,5 @@ { - "max-tries": 3, + "max-tries": 15, "wp-params": { "func": "main", "postcond" : "(assert (= (bvadd R0_mod #x00000002) R0_orig))"