update code to PR BinaryAnalysisPlatform#1410 in main repo

lib/bap_disasm/bap_disasm_insn.ml

@@ -34,8 +34,6 @@ let affect_control_flow = prop "affect-control-flow"
 let load                = prop "load"
 let store               = prop "store"
 
-
-
 module Props = struct
   type t = Z.t [@@deriving compare]
   module Bits = struct
@@ -84,7 +82,6 @@ end
 type t = Theory.Semantics.t
 type op = Op.t [@@deriving bin_io, compare, sexp]
 
-
 module Slot = struct
   type 'a t = (Theory.Effect.cls, 'a) KB.slot
   let empty = "#undefined"
@@ -215,62 +212,57 @@ module Slot = struct
       domain
 end
 
-let normalize_asm asm =
-  String.substr_replace_all asm ~pattern:"\t"
-    ~with_:" " |> String.strip
-
-type vis = {
-  jump : bool;
-  cond : bool;
-  indirect : bool;
-}
-
-let lookup_jumps bil =
-  let jump ?(cond=false) v = { v with jump = true; cond } in
-  let conditional v = jump ~cond:true v in
-  let indirect f v = f { v with indirect=true } in
-  let cons check x xs = if check then x :: xs else xs in
-  (object
-    inherit [vis] Stmt.visitor
-    method! enter_jmp ex vis = match ex with
-      | Bil.Int _ when under_condition -> conditional vis
-      | Bil.Int _ -> jump vis
-      | _ when under_condition -> indirect conditional vis
-      | _ -> indirect jump vis
-  end)#run bil {jump=false;cond=false;indirect=false} |> fun v ->
-  if not v.jump then []
-  else
-    cons (not v.cond) `Unconditional_branch [] |>
-    cons v.cond `Conditional_branch |>
-    cons v.indirect `Indirect_branch
-
-let lookup_side_effects bil = (object
-  inherit [kind list] Stmt.visitor
-  method! enter_store ~mem:_ ~addr:_ ~exp:_ _ _ acc =
-    `May_store :: acc
-  method! enter_load ~mem:_ ~addr:_ _ _ acc =
-    `May_load :: acc
-end)#run bil []
-
-let (<--) slot value insn = KB.Value.put slot insn value
-
-let write init ops =
-  List.fold ~init ops ~f:(fun init f -> f init)
+module Analyzer = struct
+  module Effects = Set.Make(struct
+      type t = Kind.t [@@deriving compare, sexp]
+    end)
+  type vis = {
+    jump : bool;
+    cond : bool;
+    indirect : bool;
+  }
+
+  let no_jumps = {jump=false;cond=false;indirect=false}
+
+  let analyzer =
+    let jump ?(cond=false) v = { v with jump = true; cond } in
+    let conditional v = jump ~cond:true v in
+    let indirect f v = f { v with indirect=true } in
+    object
+      inherit [Effects.t * vis] Stmt.visitor as super
+      method! enter_store ~mem:_ ~addr:_ ~exp:_ _ _ (effs,jumps) =
+        Set.add effs `May_store,jumps
+      method! enter_load ~mem:_ ~addr:_ _ _ (effs,jumps) =
+        Set.add effs `May_load,jumps
+      method! enter_jmp ex (effs,jumps) = effs,match ex with
+        | Bil.Int _ when under_condition -> conditional jumps
+        | Bil.Int _ -> jump jumps
+        | _ when under_condition -> indirect conditional jumps
+        | _ -> indirect jump jumps
+      method! enter_stmt s (effs,jumps) = match Bil.(decode call s) with
+        | None -> super#enter_stmt s (effs,jumps)
+        | Some _ -> Effects.add effs `Call, jumps
+    end
+
+  let run bil =
+    let cons c = Fn.flip @@ if c then Effects.add else Fn.const in
+    let effs,jump = analyzer#run bil (Effects.empty,no_jumps) in
+    if not jump.jump then effs
+    else
+      cons (not jump.cond) `Unconditional_branch effs |>
+      cons jump.cond `Conditional_branch |>
+      cons jump.indirect `Indirect_branch
+end
 
 let derive_props ?bil insn =
-  (* assert false; *)   (*! this runs*)
-  let bil_kinds = match bil with
-    | Some bil -> lookup_jumps bil @ lookup_side_effects bil
-    | None -> [] in
+  let bil_effects = match bil with
+    | Some bil -> Analyzer.run bil
+    | None -> Analyzer.Effects.empty in
   let is = Insn.is insn in
-  let is_bil kind =
-    if Option.is_some bil
-    then List.mem ~equal:[%compare.equal : kind] bil_kinds kind
-    else is kind in
-  (* those two are the only which we can't get from the BIL semantics *)
+  let is_bil = if Option.is_some bil
+    then Analyzer.Effects.mem bil_effects else is in
   let is_return = is `Return in
-  let is_call = is `Call in
-
+  let is_call = is_bil `Call || is `Call in
   let is_conditional_jump = is_bil `Conditional_branch in
   let is_jump = is_conditional_jump || is_bil `Unconditional_branch in
   let is_indirect_jump = is_bil `Indirect_branch in
@@ -291,10 +283,15 @@ let derive_props ?bil insn =
   Props.set_if may_load load                               |>
   Props.set_if may_store store
 
+let (<--) slot value insn = KB.Value.put slot insn value
+
+let write init ops =
+  List.fold ~init ops ~f:(fun init f -> f init)
+
 let set_basic effect insn : t =
   write effect Slot.[
       name <-- Insn.name insn;
-      asm <-- normalize_asm (Insn.asm insn);
+      asm <-- Insn.asm insn;
       ops <-- Some (Insn.ops insn);
     ]
 
@@ -324,7 +321,7 @@ let should = must
 let shouldn't = mustn't
 
 let name = KB.Value.get Slot.name
-let asm = KB.Value.get Slot.asm
+let asm  = KB.Value.get Slot.asm
 let bil insn = KB.Value.get Bil.slot insn
 let ops s = match KB.Value.get Slot.ops s with
   | None -> [||]
@@ -402,7 +399,7 @@ include Regular.Make(struct
   end)
 
 let pp_asm ppf insn =
-  Format.fprintf ppf "%s" (normalize_asm (asm insn))
+  Format.fprintf ppf "%s" (asm insn)
 
 
 module Seqnum = struct
@@ -434,41 +431,6 @@ module Seqnum = struct
   let fresh = KB.Syntax.(freshnum >>= label)
 end
 
-
-
-let provide_sequence_semantics () =
-  let open KB.Syntax in
-  KB.promise Theory.Semantics.slot @@ fun obj ->
-  KB.collect Insn.slot obj >>= function
-  | None -> !!Theory.Semantics.empty
-  | Some insn when not (String.equal (Insn.name insn) "seq") ->
-    !!Theory.Semantics.empty
-  | Some insn -> match Insn.subs insn with
-    | [||] -> !!Theory.Semantics.empty
-    | subs ->
-      Theory.instance () >>= Theory.require >>= fun (module CT) ->
-      let subs = Array.to_list subs |>
-                 List.map ~f:(fun sub ->
-                     Seqnum.fresh >>| fun lbl ->
-                     lbl,sub) in
-      KB.all subs >>=
-      KB.List.map ~f:(fun (obj,sub) ->
-          KB.provide Insn.slot obj (Some sub) >>= fun () ->
-          KB.collect Theory.Semantics.slot obj >>= fun sema ->
-          let nil = Theory.Effect.empty Theory.Effect.Sort.bot in
-          CT.seq (CT.blk obj !!nil !!nil) !!sema) >>=
-      KB.List.reduce ~f:(fun s1 s2 -> CT.seq !!s1 !!s2) >>| function
-      | None -> empty
-      | Some sema -> with_basic sema insn
-
-let () =
-  let open KB.Rule in
-  declare "sequential-instruction" |>
-  require Insn.slot |>
-  provide Theory.Semantics.slot |>
-  comment "computes sequential instructions semantics";
-  provide_sequence_semantics ()
-
 let () =
   Data.Write.create ~pp:Adt.pp () |>
   add_writer ~desc:"Abstract Data Type pretty printing format"

plugins/arm/semantics/aarch64.lisp

@@ -250,3 +250,10 @@
 (defun Bcc (cnd off)
   (when (condition-holds cnd)
     (relative-jump off)))
+
+(defun HINT (_)
+  (empty))
+
+
+(defun UDF (exn)
+  (special :undefined-instruction))

plugins/primus_lisp/primus_lisp_main.ml

@@ -430,7 +430,6 @@ let () =
       Channels.init !!redirects;
       Primitives.init ();
       Semantics_primitives.provide ();
-      Semantics_primitives.enable_extraction ();
       Semantics.load_lisp_unit ~paths ~features;
       let stdout = Option.map !!semantics_stdout ~f:(fun file ->
           let ch = Out_channel.create file in