Enable patches specified in Primus lisp

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);
@@ -91,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
@@ -103,34 +107,36 @@ 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 ->
+        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.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 =

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

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 = {

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
@@ -44,7 +43,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 +100,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 +149,13 @@ 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 =
+  let set_patch_code (obj : t) (data : Config.patch_code option) : unit KB.t =
     KB.provide patch_code obj data
 
-  let get_patch_code (obj : t) : Cabs.definition option KB.t =
+  let get_patch_code (obj : t) : Config.patch_code option KB.t =
     KB.collect patch_code obj
 
-  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
@@ -190,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

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
 
@@ -14,7 +13,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 +48,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 +69,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
@@ -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

bap-vibes/src/patch_ingester.ml

@@ -5,31 +5,47 @@ open Bap_knowledge
 open Knowledge.Syntax
 open Core_kernel
 open Bap_core_theory
+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
   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* 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
@@ -38,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

bap-vibes/src/seeder.ml

@@ -69,10 +69,7 @@ let create_patches
         ~addr:(Config.patch_point p)
     in
     let* () = Data.Patch.set_patch_name obj (Some patch_name) 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])
-    in
+    let* () = Data.Patch.set_patch_code obj (Some (Config.patch_code p)) 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

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. *)

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 _ ->
 

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 () ->