Skip to content

Commit 9cef73a

Browse files
philzook58philzook58
committed
cleanup. Renamed errenous bir variable to sem
1 parent 70c1cdf commit 9cef73a

File tree

11 files changed

+75
-64
lines changed

11 files changed

+75
-64
lines changed

‎bap-vibes/src/compiler.ml‎

Lines changed: 18 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -42,19 +42,19 @@ let create_vibes_ir
4242
(* Compile one patch from BIR to VIBES IR *)
4343
let compile_one_vibes_ir (count : int KB.t) (patch : Data.Patch.t) : int KB.t =
4444
count >>= fun n ->
45-
Data.Patch.get_assembly patch >>= (fun asm ->
46-
match asm with
47-
| Some _asm ->
48-
Events.(send @@ Info "The patch has no IR to translate.\n");
49-
KB.return () (* Assembly already set. Presumably by the user. *)
50-
| None ->
45+
Data.Patch.get_patch_code_exn patch >>= (fun code ->
46+
match code with
47+
| ASMCode _asm ->
48+
Events.(send @@ Info "Assembly patch has no IR to translate.\n");
49+
KB.return ()
50+
| PrimusCode _ | CCode _ ->
5151
begin
5252
let info_str =
5353
Format.asprintf "Translating patch %s BIR to VIBES IR..."
5454
(string_of_int n)
5555
in
5656
Events.(send @@ Info info_str);
57-
Data.Patch.get_bir patch >>= fun bir ->
57+
Data.Patch.get_sem patch >>= fun bir ->
5858

5959
let info_str = Format.asprintf "\nPatch: %a\n\n%!" KB.Value.pp bir in
6060
Events.(send @@ Info info_str);
@@ -81,13 +81,10 @@ let compile_one_assembly
8181
(Ir.t * Minizinc.sol) KB.t)
8282
(count : int KB.t) (patch : Data.Patch.t) : int KB.t =
8383
count >>= fun n ->
84-
Data.Patch.get_assembly patch >>= (fun asm ->
84+
Data.Patch.get_patch_code_exn patch >>= (fun asm ->
8585
match asm with
86-
| Some _asm ->
87-
Events.(send @@ Info "The patch already has assembly\n");
88-
Events.(send @@ Rule);
89-
KB.return () (* Assembly already set. Presumably by the user. *)
90-
| None ->
86+
| ASMCode asm -> KB.return [asm]
87+
| PrimusCode _ | CCode _ ->
9188
begin
9289
let info_str =
9390
Format.asprintf "Translating patch %s VIBES IR to assembly..."
@@ -102,13 +99,14 @@ let compile_one_assembly
10299
create_assembly
103100
(solver target lang prev_sols)
104101
ir >>= fun (assembly, new_sol) ->
105-
Data.Patch.set_assembly patch (Some assembly) >>= fun () ->
106-
Events.(send @@ Info "The patch has the following assembly:\n");
107-
Events.(send @@ Rule);
108-
Events.(send @@ Info (String.concat ~sep:"\n" assembly));
109-
Events.(send @@ Rule);
110-
Data.Patch.add_minizinc_solution patch new_sol
111-
end) >>= fun () ->
102+
Data.Patch.add_minizinc_solution patch new_sol >>= fun () ->
103+
KB.return assembly
104+
end) >>= fun assembly ->
105+
Data.Patch.set_assembly patch (Some assembly) >>= fun () ->
106+
Events.(send @@ Info "The patch has the following assembly:\n");
107+
Events.(send @@ Rule);
108+
Events.(send @@ Info (String.concat ~sep:"\n" assembly));
109+
Events.(send @@ Rule);
112110
KB.return (n + 1)
113111

114112
(* Converts the patch (as BIR) to VIBES IR instructions. *)

‎bap-vibes/src/data.ml‎

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
We expect much evolution here... *)
33

44
open !Core_kernel
5-
open Bap.Std
65
open Bap_knowledge
76
open Bap_core_theory
87
open Knowledge.Syntax
@@ -137,13 +136,10 @@ module Patch = struct
137136
| Some value -> KB.return value
138137

139138
let set_patch_code (obj : t) (data : Config.patch_code option) : unit KB.t =
140-
KB.provide patch_code obj data (* (Option.map ~f:(fun c -> Config.CCode c) data) *)
139+
KB.provide patch_code obj data
141140

142141
let get_patch_code (obj : t) : Config.patch_code option KB.t =
143-
KB.collect patch_code obj (* >>= fun res ->
144-
match res with
145-
| Some (CCode code) -> KB.return (Some code)
146-
| _ -> KB.return None *)
142+
KB.collect patch_code obj
147143

148144
let get_patch_code_exn (obj : t) : Config.patch_code KB.t =
149145
get_patch_code obj >>= fun result ->
@@ -179,13 +175,13 @@ module Patch = struct
179175
KB.Object.create Theory.Program.cls >>= fun lab ->
180176
KB.provide patch_label obj (Some lab)
181177

182-
let set_bir (obj : t) (sem : Insn.t) : unit KB.t =
178+
let set_sem (obj : t) (sem : Theory.Semantics.t) : unit KB.t =
183179
KB.collect patch_label obj >>= fun olab ->
184180
(* FIXME: fail more gracefully *)
185181
let lab = Option.value_exn olab in
186182
KB.provide Theory.Semantics.slot lab sem
187183

188-
let get_bir (obj : t) : Insn.t KB.t =
184+
let get_sem (obj : t) : Theory.Semantics.t KB.t =
189185
KB.collect patch_label obj >>= fun olab ->
190186
(* FIXME: fail more gracefully *)
191187
let lab = Option.value_exn olab in

‎bap-vibes/src/data.mli‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
properties that the VIBES toolchain defines and manipulates *)
33

44
open !Core_kernel
5-
open Bap.Std
65
open Bap_knowledge
76
open Bap_core_theory
87

@@ -84,8 +83,8 @@ module Patch : sig
8483
that will contain the semantics. This *must* be called before
8584
set_bir! *)
8685
val init_sem : t -> unit KB.t
87-
val set_bir : t -> insn -> unit KB.t
88-
val get_bir : t -> insn KB.t
86+
val set_sem : t -> Theory.Semantics.t -> unit KB.t
87+
val get_sem : t -> Theory.Semantics.t KB.t
8988

9089
val set_raw_ir : t -> Ir.t option -> unit KB.t
9190
val get_raw_ir : t -> Ir.t option KB.t

‎bap-vibes/src/patch_ingester.ml‎

Lines changed: 23 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open Bap_primus.Std
1010
module KB = Knowledge
1111
open KB.Let
1212

13-
let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t =
13+
let provide_sem (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t =
1414
Theory.instance () >>=
1515
Theory.require >>= fun (module Core) ->
1616
let module CParser = Core_c.Eval(Core) in
@@ -19,30 +19,32 @@ let provide_bir (tgt : Theory.target) (patch : Data.Patch.t) : unit KB.t =
1919
Events.(send @@ Info (Printf.sprintf "Patch %s" name));
2020
Data.Patch.get_patch_code_exn patch >>= fun code ->
2121
(* Get the patch (as BIR). *)
22-
let* bir = match code with
23-
| CCode code -> begin
22+
let* sem = match code with
23+
| CCode code ->
24+
begin
2425
let code_str = Utils.print_c Cprint.print_def code in
2526
Events.(send @@ Info (Printf.sprintf "%s" code_str));
2627
CParser.c_patch_to_eff tgt code
27-
end
28-
| PrimusCode name -> begin
29-
Primus.Lisp.Unit.create tgt >>= fun unit ->
30-
KB.Object.scoped Theory.Program.cls @@ fun obj ->
31-
KB.sequence [
32-
KB.provide Theory.Label.unit obj (Some unit);
33-
(* KB.provide Theory.Label.addr obj addr; *)
34-
KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name));
35-
] >>= fun () ->
36-
KB.collect Theory.Semantics.slot obj
37-
end
38-
| ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented "yolo")
28+
end
29+
| PrimusCode name ->
30+
begin
31+
Primus.Lisp.Unit.create tgt >>= fun unit ->
32+
KB.Object.scoped Theory.Program.cls @@ fun obj ->
33+
KB.sequence [
34+
KB.provide Theory.Label.unit obj (Some unit);
35+
KB.provide Primus.Lisp.Semantics.name obj (Some (KB.Name.create name));
36+
] >>= fun () ->
37+
KB.collect Theory.Semantics.slot obj
38+
end
39+
| ASMCode _asm -> Kb_error.fail (Kb_error.Not_implemented
40+
"[Patch_ingester.provide_sem] called on assembly patch")
3941
in
4042
Events.(send @@ Info "The patch has the following BIL:");
4143
Events.(send @@ Rule);
42-
let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot bir) in
44+
let bir_str = Format.asprintf "%a" Bil.pp (KB.Value.get Bil.slot sem) in
4345
Events.(send @@ Info bir_str);
4446
Events.(send @@ Rule);
45-
Data.Patch.set_bir patch bir
47+
Data.Patch.set_sem patch sem
4648

4749
(* Ingests a single patch, populating the relevant fields of the KB,
4850
most notably the semantics field of the corresponding patch (and
@@ -51,10 +53,10 @@ let ingest_one (tgt : Theory.target) (patch_num : int KB.t) (patch : Data.Patch.
5153
: int KB.t =
5254
patch_num >>= fun patch_num ->
5355
Events.(send @@ Info (Printf.sprintf "\nIngesting patch %d." patch_num));
54-
(Data.Patch.get_assembly patch >>= fun asm ->
55-
match asm with
56-
| Some _asm -> KB.return () (* Assembly is user provided *)
57-
| None -> provide_bir tgt patch) >>= fun () ->
56+
(Data.Patch.get_patch_code_exn patch >>= fun code ->
57+
match code with
58+
| ASMCode _asm -> KB.return () (* Assembly is user provided *)
59+
| PrimusCode _ | CCode _ -> provide_sem tgt patch) >>= fun () ->
5860
KB.return @@ patch_num+1
5961

6062
(* Processes the whole patch associated with [obj], populating all the

‎bap-vibes/src/seeder.ml‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -68,10 +68,6 @@ let create_patches
6868
in
6969
let* () = Data.Patch.set_patch_name obj (Some patch_name) in
7070
let* () = Data.Patch.set_patch_code obj (Some (Config.patch_code p)) in
71-
let* () = match Config.patch_code p with
72-
| ASMCode asmcode -> Data.Patch.set_assembly obj (Some [asmcode])
73-
| _ -> KB.return ()
74-
in
7571
let* () = Data.Patch.set_patch_point obj (Some (Config.patch_point p)) in
7672
let* () = Data.Patch.set_patch_size obj (Some (Config.patch_size p)) in
7773
let* () = Data.Patch.set_lang obj lang in

‎bap-vibes/tests/integration/test_minizinc.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ let test_minizinc_ex1 (ctxt : test_ctxt) : unit =
113113
KB.Object.create Data.Patch.patch >>= fun patch ->
114114
Data.Patch.init_sem patch >>= fun () ->
115115
Patches.get_bir "ret-3" 32 >>= fun bil ->
116-
Data.Patch.set_bir patch bil >>= fun () ->
116+
Data.Patch.set_sem patch bil >>= fun () ->
117117
Data.Patched_exe.set_patches obj
118118
(Data.Patch_set.singleton patch) >>= fun () ->
119119
(* Now run the compiler. *)

‎bap-vibes/tests/unit/test_compiler.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ let test_compile (_ : test_ctxt) : unit =
2525
obj (Some H.minizinc_model_filepath) >>= fun () ->
2626
Patches.get_bir H.patch 32 >>= fun bil ->
2727
KB.Object.create Data.Patch.patch >>= fun patch ->
28-
Data.Patch.set_bir patch bil >>= fun _ ->
28+
Data.Patch.set_sem patch bil >>= fun _ ->
2929
Data.Patched_exe.set_patches obj
3030
(Data.Patch_set.singleton patch) >>= fun _ ->
3131

‎bap-vibes/tests/unit/test_patch_ingester.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ let test_ingest (_ : test_ctxt) : unit =
2727
match Data.Patch_set.to_list patches with
2828
| [] -> assert_failure "Result patch missing."
2929
| (p :: []) ->
30-
Data.Patch.get_bir p >>= fun bir ->
30+
Data.Patch.get_sem p >>= fun bir ->
3131
Patches.Ret_3.prog 32 >>= fun expected ->
3232
let open Bap.Std in
3333
let expected = KB.Value.get Bil.slot expected in
@@ -61,7 +61,7 @@ let test_ingest_with_no_patch (_ : test_ctxt) : unit =
6161
let result = KB.run Data.cls computation KB.empty in
6262

6363
(* The ingester should diverge with the appropriate error. *)
64-
let expected = Kb_error.Problem Kb_error.Missing_patch_name in
64+
let expected = Kb_error.Problem Kb_error.Missing_patch_code in
6565
H.assert_error Data.Patched_exe.patches expected result
6666

6767
(* 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 =
100100
KB.Object.create Data.Patch.patch >>= fun patch ->
101101

102102
let code = H.dummy_code in
103-
Data.Patch.set_patch_code patch (Some code) >>= fun () ->
103+
Data.Patch.set_patch_code patch (Some (CCode code)) >>= fun () ->
104104
Data.Patch.set_patch_name patch (Some H.patch) >>= fun () ->
105105
Data.Patched_exe.set_patches obj
106106
(Data.Patch_set.singleton patch) >>= fun () ->

‎bin/system-tests/tests/test-arm-exes.bash‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,9 +220,28 @@ test_arm_linear_ssa () {
220220
run_arm_exe "${TEST_PATCH_EXE}" 3
221221
}
222222

223+
test_arm_primus () {
224+
local TEST_DIR="${EXES_DIR}/arm-simple-primus"
225+
local MAIN_EXE="${TEST_DIR}/main.reference"
226+
local PATCH_EXE="${TEST_DIR}/main.patched.reference"
227+
local TEST_PATCH_EXE="${TEST_DIR}/test.patched.by.vibes"
228+
229+
print_header "Checking ${TEST_DIR}"
230+
231+
# Check the precompiled executables.
232+
run_arm_exe "${MAIN_EXE}" 15
233+
run_arm_exe "${PATCH_EXE}" 17
234+
235+
# Check that vibes patches correctly.
236+
run_make "make clean -C ${TEST_DIR}" 0
237+
run_make "make patch.reference -C ${TEST_DIR}" 0
238+
run_arm_exe "${TEST_PATCH_EXE}" 3
239+
}
240+
223241
# Run all tests
224242
run_all () {
225243
test_arm_simple
244+
test_arm_primus
226245
test_arm_simple_inline
227246
test_arm_simple_cegis
228247
test_arm_simple_compiled

‎plugin/lib/vibes_plugin_parameters.ml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,9 @@ let validate_patch_name (obj : Json.t) : (string, error) Stdlib.result =
8787
into a [Cabs.definition] *)
8888
let validate_patch_code (nm : string) (obj : Json.t)
8989
: (Vibes_config.patch_code, error) Stdlib.result =
90-
match Json.Util.member "patch-code" obj, Json.Util.member "asm-code" obj, Json.Util.member "lisp-code" obj with
90+
match Json.Util.member "patch-code" obj,
91+
Json.Util.member "asm-code" obj,
92+
Json.Util.member "lisp-code" obj with
9193
| `String s, `Null, `Null ->
9294
(match Parse_c.parse_c_patch s with
9395
| Ok code -> Ok (Vibes_config.CCode code)

0 commit comments

Comments
 (0)