adds support for mode events

lib/veri.ml

@@ -44,11 +44,8 @@ module Disasm = struct
     match Dis.insn_of_mem dis mem with
     | Error er -> Error (`Disasm_error er)
     | Ok r -> match r with
-      | mem', Some insn, `finished -> Ok (mem',insn)
-      | _, None, _ ->
-        let er = Error.of_string "nothing was disasmed" in
-        Error (`Disasm_error er)
-      | _, _, `left _ -> Error `Overloaded_chunk
+      | _, Some _, `left _ -> Error `Overloaded_chunk
+      | mem', insn, _ -> Ok (mem',insn)
 
   let insn_name = Dis.Insn.name
 end
@@ -63,6 +60,7 @@ class context stat policy trace = object(self:'s)
   val other : 's option = None
   val insn  : string option = None
   val code  : Chunk.t option = None
+  val mode  : Mode.t option = None
   val stat  : Veri_stat.t = stat
   val bil   : bil = []
 
@@ -72,6 +70,7 @@ class context stat policy trace = object(self:'s)
       ~left:(Set.to_list (Option.value_exn other)#events)
       ~insn:(Option.value_exn insn)
       ~code:(Option.value_exn code |> Chunk.data)
+      ~mode
 
   method private finish_step stat =
     let s = {< other = None; error = None; insn = None; bil = [];
@@ -98,12 +97,14 @@ class context stat policy trace = object(self:'s)
     s#drop_pc
 
   method code  = code
+  method mode = mode
   method stat  = stat
   method other = other
   method events  = events
   method reports = fst stream
   method set_bil  b = {< bil = b >}
   method set_code c = {< code = Some c >}
+  method set_mode m = {< mode = Some m >}
   method set_insn s = {< insn = Some s >}
   method notify_error er   = {< error = Some er >}
   method register_event ev = {< events = Set.add events ev; >}
@@ -112,31 +113,49 @@ class context stat policy trace = object(self:'s)
   method drop_pc = self#with_pc Bil.Bot
 end
 
+type KB.conflict += Veri_error of Veri_error.t
 
-let new_insn arch mem insn =
+let trace_unit = KB.Symbol.intern "trace" Theory.Unit.cls
+
+let new_insn arch mode mem =
   let open KB.Syntax in
   let addr = Memory.min_addr mem in
   let* code = Theory.Label.for_addr (Word.to_bitvec addr) in
-  let* unit = KB.Symbol.intern "trace" Theory.Unit.cls in
+  let* unit = trace_unit in
   KB.sequence [
-    KB.provide Arch.slot code arch;
     KB.provide Image.Spec.slot unit (Image.Spec.from_arch arch);
     KB.provide Theory.Label.unit code (Some unit);
-    KB.provide Memory.slot code (Some mem);
-    KB.provide Dis.Insn.slot code (Some insn);
-  ] >>| fun () ->
-  code
-
-let lift arch mem insn =
-  match Toplevel.try_eval Theory.Semantics.slot (new_insn arch mem insn) with
-  | Ok sema -> Ok (Insn.bil sema)
+    match mode with
+    | Some mode -> KB.provide Mode.slot code mode
+    | None -> KB.return ()
+  ] >>= fun () ->
+  let* target = KB.collect Theory.Unit.target unit in
+  let* coding = KB.collect Theory.Label.encoding code in
+  let dis = Dis.lookup target coding |> Or_error.ok_exn in
+  match Disasm.insn dis mem with
+  | Error er -> KB.fail (Veri_error er)
+  | Ok (mem, insn) ->
+    KB.provide Memory.slot code (Some mem) >>= fun () ->
+    KB.provide Dis.Insn.slot code insn >>= fun () ->
+    KB.promising Theory.Label.unit ~promise:(fun _ -> !!(Some unit)) @@ fun () ->
+    KB.collect Theory.Semantics.slot code >>| fun _ ->
+    code
+
+let disasm_and_lift arch mode mem =
+  let code = new_insn arch mode mem in
+  match Toplevel.try_eval Theory.Semantics.slot code with
+  | Error (Veri_error er) -> Error er
   | Error c ->
     let er = Error.of_string (Sexp.to_string (KB.sexp_of_conflict c)) in
-    Error er
+    Error (`Disasm_error er)
+  | Ok sema ->
+    match Toplevel.eval Dis.Insn.slot code with
+    | None -> Error (`Disasm_error (Error.of_string "nothing was disasmed"))
+    | Some insn -> Ok (sema, insn)
 
 let target_info arch =
   let module Target = (val target_of_arch arch) in
-  Target.CPU.mem, lift arch
+  Target.CPU.mem
 
 let memory_of_chunk endian chunk =
   Bigstring.of_string (Chunk.data chunk) |>
@@ -154,9 +173,9 @@ let same_addr addr mv = Addr.equal addr (Move.cell mv)
 
 type find = [ `Addr of addr | `Var of var ]
 
-class ['a] t arch dis =
+class ['a] t arch =
   let endian = Arch.endian arch in
-  let mem_var, lift = target_info arch in
+  let mem_var = target_info arch in
 
   object(self)
     constraint 'a = #context
@@ -254,24 +273,19 @@ class ['a] t arch dis =
     method! eval bil =
       super#eval (Stmt.normalize ~normalize_exp:true bil)
 
-    method private eval_insn (mem, insn) =
-      let name = Disasm.insn_name insn in
-      SM.update (fun c -> c#set_insn name) >>= fun () ->
-      match lift mem insn with
-      | Error er ->
-        SM.update (fun c -> c#notify_error (`Lifter_error (name, er)))
-      | Ok bil ->
-        SM.update (fun c -> c#set_bil bil) >>= fun () ->
-        self#eval bil
-
     method private eval_chunk chunk =
       self#update_event (Value.create Event.pc_update (Chunk.addr chunk)) >>= fun () ->
       match memory_of_chunk endian chunk with
       | Error er -> SM.update (fun c -> c#notify_error (`Damaged_chunk er))
-      | Ok mem ->
-        match Disasm.insn dis mem with
+      | Ok mem -> SM.get () >>= fun ctxt ->
+        match disasm_and_lift arch ctxt#mode mem with
+        | Ok (sema, insn) ->
+          let name = Disasm.insn_name insn in
+          SM.update (fun c -> c#set_insn name) >>= fun () ->
+          let bil = Insn.bil sema in
+          SM.update (fun c -> c#set_bil bil) >>= fun () ->
+          self#eval bil
         | Error er -> SM.update (fun c -> c#notify_error er)
-        | Ok insn -> self#eval_insn insn
 
     method! eval_memory_load mv =
       let addr = Bil.int @@ Move.cell mv in
@@ -294,11 +308,16 @@ class ['a] t arch dis =
       super#eval_exec code >>= fun () ->
       SM.update (fun c -> c#set_code code)
 
+    method! eval_mode mode =
+      super#eval_mode mode >>= fun () ->
+      SM.update (fun c -> c#set_mode mode)
+
     method! eval_event ev =
       super#eval_event ev >>= fun () ->
       Value.Match.(
         select @@
         case Event.code_exec    (fun _ -> SM.return ()) @@
+        case Event.mode         (fun _ -> SM.return ()) @@
         case Event.memory_store (fun _ -> SM.return ()) @@
         case Event.memory_load  (fun _ -> SM.return ()) @@
         default (fun () -> self#update_event ev)) ev

lib/veri.mli

@@ -19,17 +19,19 @@ class context: Veri_stat.t -> Veri_policy.t -> Trace.t -> object('s)
     method switch: 's
     method stat : Veri_stat.t
     method code : Chunk.t option
+    method mode : Mode.t option
     method events : Value.Set.t
     method reports : Veri_report.t stream
     method register_event : Trace.event -> 's
     method notify_error: Veri_error.t -> 's
     method set_bil : bil -> 's
     method set_code : Chunk.t -> 's
+    method set_mode : Mode.t -> 's
     method set_insn: string -> 's
     method drop_pc : 's
   end
 
-class ['a] t : arch -> Disasm.t -> object('s)
+class ['a] t : arch -> object('s)
     constraint 'a = #context
     inherit ['a] Veri_traci.t
   end

lib/veri_report.ml

@@ -11,6 +11,7 @@ type t = {
   bil  : bil;
   insn : string;
   code : string;
+  mode : Mode.t option;
   left : event list;
   right: event list;
   data : (rule * matched) list;
@@ -31,6 +32,10 @@ include Regular.Make(struct
         String.iter ~f:(fun c -> Format.fprintf fmt "%02X " (Char.to_int c)) s in
       Format.fprintf fmt "@[<h>%a@]" pp s
 
+    let pp_mode fmt = function
+      | Some m -> Format.fprintf fmt "(%a)" Mode.pp m
+      | None -> ()
+
     let pp_evs fmt evs =
       List.iter ~f:(fun ev ->
           Format.(fprintf std_formatter "%a; " Value.pp ev)) evs
@@ -41,8 +46,8 @@ include Regular.Make(struct
 
     let pp fmt t =
       let bil = Stmt.simpl t.bil in
-      Format.fprintf fmt "@[<v>%s %a@,left:  %a@,right: %a@,%a@]@."
-        t.insn pp_code t.code pp_evs t.left pp_evs t.right Bil.pp bil;
+      Format.fprintf fmt "@[<v>%s %a%a@,left:  %a@,right: %a@,%a@]@."
+        t.insn pp_code t.code pp_mode t.mode pp_evs t.left pp_evs t.right Bil.pp bil;
       List.iter ~f:(pp_data fmt) t.data;
       Format.print_newline ()
 

lib/veri_report.mli

@@ -14,12 +14,14 @@ val create :
   bil:Bap.Std.bil ->
   insn:string ->
   code:string ->
+  mode: Mode.t option ->
   left:event list ->
   right:event list ->
   data:(rule * matched) list -> t
 
 val bil  : t -> bil
 val code : t -> string
+val mode : t -> Mode.t option
 val insn : t -> string
 val left : t -> Trace.event list
 val right: t -> Trace.event list

lib/veri_traci.ml

@@ -76,6 +76,7 @@ class ['a] t arch =
         case Event.register_read self#eval_register_read @@
         case Event.register_write self#eval_register_write @@
         case Event.code_exec self#eval_exec @@
+        case Event.mode self#eval_mode @@
         case Event.pc_update self#eval_pc_update @@
         case Event.context_switch self#eval_context_switch @@
         case Event.syscall self#eval_syscall @@
@@ -97,6 +98,7 @@ class ['a] t arch =
 
     method eval_exec: chunk -> 'a u = stub
     method eval_context_switch: int -> 'a u = stub
+    method eval_mode: Mode.t -> 'a u = stub
     method eval_syscall: syscall -> 'a u = stub
     method eval_call: call -> 'a u = stub
     method eval_return: return -> 'a u = stub

lib/veri_traci.mli

@@ -23,6 +23,7 @@ class ['a] t: arch -> object('s)
   method eval_exec : chunk -> 'a u
   method eval_pc_update : addr -> 'a u
   method eval_context_switch : int -> 'a u
+  method eval_mode: Mode.t -> 'a u
   method eval_syscall : syscall -> 'a u
   method eval_exn : exn -> 'a u
   method eval_call : call -> 'a u

plugin/veri_bil.ml

@@ -64,14 +64,12 @@ let eval_file file policy show_errs =
     match Dict.find (Trace.meta trace) Meta.arch with
     | None -> mk_er "trace of unknown arch"
     | Some arch ->
-      Dis.with_disasm ~backend:"llvm" (Arch.to_string arch) ~f:(fun dis ->
-          let dis = Dis.store_asm dis |> Dis.store_kinds in
-          let stat = Veri_stat.empty in
-          let ctxt = new Veri.context stat policy trace in
-          let veri = new Veri.t arch dis in
-          if show_errs then errors_stream ctxt#reports;
-          let ctxt' = Monad.State.exec (veri#eval_trace trace) ctxt in
-          Ok ctxt'#stat)
+      let stat = Veri_stat.empty in
+      let ctxt = new Veri.context stat policy trace in
+      let veri = new Veri.t arch in
+      if show_errs then errors_stream ctxt#reports;
+      let ctxt' = Monad.State.exec (veri#eval_trace trace) ctxt in
+      Ok ctxt'#stat
 
 let read_dir path =
   let dir = Caml_unix.opendir path in