implements pcode floating-point and special operators (#1452)

Adds an `intrinsic` and `symbol-concat` primitives to Primus Lisp and
uses them to implement all floating-point operators in pcode and cpuid
routines for pcode-x86.

Author: ivg

lib/bap_primus/bap_primus_lisp_attribute.ml

@@ -3,7 +3,6 @@ open Bap_core_theory
 open Bap.Std
 
 open Bap_primus_lisp_types
-
 module Name = KB.Name
 
 type cls
@@ -14,7 +13,7 @@ let cls : (cls,unit) KB.cls = KB.Class.declare  "attributes" ()
 type attrs = (cls,unit) KB.cls KB.Value.t
 type set = attrs
 
-type error = ..
+type error = exn = ..
 
 exception Unknown_attr of string * tree
 exception Failure of error * tree list
@@ -38,8 +37,6 @@ module Parse = struct
 
   type error += Expect_atom | Expect_list
 
-
-
   let atom = function
     | {data=Atom s} -> Some s
     | _ -> None
@@ -101,3 +98,11 @@ module Set = struct
 
   include Self
 end
+
+
+let () = Caml.Printexc.register_printer (function
+    | Failure (error,_) ->
+      let msg = Format.asprintf "Attribute parse error: %s"
+          (Caml.Printexc.to_string error) in
+      Some msg
+    | _ -> None)

plugins/bil/bil_ir.ml

@@ -27,6 +27,7 @@ type t = cfg
 
 let null = KB.Object.null Theory.Program.cls
 let is_null x = KB.Object.is_null x
+let is_call jmp = Option.is_some (Jmp.alt jmp)
 let is_empty = function
   | {entry; blks=[]} -> is_null entry
   | _ -> false
@@ -55,71 +56,103 @@ module BIR = struct
     Blk.Builder.result b :: blks |>
     List.rev
 
-  let resolve jmp = Option.(Jmp.(dst jmp >>| resolve))
+  let dst jmp =
+    match Option.(Jmp.(dst jmp >>| resolve)) with
+    | Some First tid -> Some tid
+    | _ -> None
+
+  let dsts blk =
+    List.filter_map blk.jmps ~f:dst
+
 
   let references blks =
     List.fold ~init:Tid.Map.empty ~f:(fun refs {jmps} ->
         List.fold jmps ~init:refs ~f:(fun refs jmp ->
-            match resolve jmp with
-            | Some (First tid) when Set.mem blks tid ->
+            match dst jmp with
+            | Some tid when Map.mem blks tid ->
               Map.update refs tid ~f:(function
                   | None -> 1
                   | Some refs -> refs+1)
             | _ -> refs))
 
-  let names =
-    List.fold ~init:Tid.Set.empty ~f:(fun blks {name} ->
-        Set.add blks name)
+  let graph = List.fold
+      ~init:(Theory.Label.null,Tid.Map.empty)
+      ~f:(fun (_,blks) blk ->
+          blk.name, Map.add_exn blks blk.name blk)
 
   let single_dst = function
     | [] | _ :: _ :: _ -> None
-    | [x] -> match resolve x with
-      | Some First tid -> Some tid
+    | [x] -> match dst x with
+      | Some tid when not (is_call x) -> Some tid
       | _ -> None
 
+
   let is_sub {weak; keep} = keep && weak
 
   let can_contract refs b1 b2 =
-    is_sub b1 && is_sub b2 && match single_dst b1.jmps with
+    not (Tid.equal b1.name b2.name) &&
+    b2.weak && match single_dst b1.jmps with
     | None -> false
     | Some dst ->
       Tid.equal dst b2.name &&
       match Map.find refs dst with
       | Some 1 -> true
       | _ -> false
 
-  (* pre: can_contract b1 b2 /\
-          can_contract b2 b3 .. *)
-  let contract blks = match List.hd blks, List.last blks with
-    | Some first,Some last -> {
-        first with
-        defs = List.(rev@@concat_map blks ~f:(fun {defs} -> List.rev defs));
-        jmps = last.jmps;
-      }
-    | _ -> assert false
-
-  let normalize blks =
-    let names = names blks in
-    let refs = references names blks in
-    List.sort blks ~compare:(fun b1 b2 ->
-        Tid.compare b1.name b2.name) |>
-    List.group ~break:(fun b1 b2 ->
-        not @@ can_contract refs b1 b2) |>
-    List.map ~f:contract
+  (* pre: can_contract b1 b2 *)
+  let join x y = {
+    x with
+    defs = y.defs @ x.defs;
+    jmps = y.jmps
+  }
+
+  let (//) graph node =
+    Map.remove graph node.name
+
+  let has_name name blk = Tid.equal name blk.name
+
+  let removed exit parent dst =
+    if has_name exit dst then parent.name else exit
+
+  let contract refs graph ~entry ~exit =
+    let rec contract output graph exit node =
+      match Option.(single_dst node.jmps >>= Map.find graph) with
+      | Some dst when can_contract refs node dst ->
+        let node = join node dst in
+        contract output (graph//dst) (removed exit node dst) node
+      | _ -> follow output graph exit node
+    and follow output graph exit node = List.fold (dsts node)
+        ~init:(node::output,graph//node,exit)
+        ~f:(fun (output,graph,exit) name ->
+            match Map.find graph name with
+            | None -> output,graph,exit
+            | Some node -> contract output graph exit node) in
+    contract [] graph exit (Map.find_exn graph entry)
+
+  let normalize entry blks =
+    let exit,graph = graph blks in
+    let refs = references graph blks in
+    let blks,leftovers,exit = contract refs graph ~entry ~exit in
+    assert (Map.is_empty leftovers);
+    match blks with
+    | blk::_ as blks when has_name exit blk -> blks
+    | blks ->
+      List.find_exn blks ~f:(has_name exit) ::
+      List.filter blks ~f:(Fn.non (has_name exit))
 
   let has_subs = List.exists ~f:is_sub
 
-  let normalize = function
+  let normalize entry = function
     | [] | [_] as xs -> xs
-    | xs -> if has_subs xs then normalize xs else xs
+    | xs -> if has_subs xs then normalize entry xs else xs
 
   (* postconditions:
      - the first block is the entry block
      - the last block is the exit block
   *)
   let reify {entry; blks} =
     if is_null entry then [] else
-      normalize blks |>
+      normalize entry blks |>
       List.fold ~init:(None,[]) ~f:(fun (s,blks) b ->
           match make_blk b with
           | [] -> assert false
@@ -168,8 +201,8 @@ let slot = graph
 module IR = struct
   include Theory.Empty
   let ret = Knowledge.return
-  let blk ?(keep=true) tid =
-    {name=tid; defs=[]; jmps=[]; keep; weak=false}
+  let blk ?(keep=false) ?(weak=false) tid =
+    {name=tid; defs=[]; jmps=[]; keep; weak}
 
   let def = (fun x -> x.defs), (fun x d -> {x with defs = d})
   let jmp = (fun x -> x.jmps), (fun x d -> match x.jmps with
@@ -227,7 +260,7 @@ module IR = struct
                   | `Relinked,blks -> KB.return blks
                   | `Relink dst, blks ->
                     let+ tid = fresh in
-                    blks @ [blk label ++ goto ~tid dst]
+                    blks @ [blk ~weak label ++ goto ~tid dst]
                   | `Unbound,[] -> assert false
                   | `Unbound,_ -> assert false      in
       {entry = label; blks}
@@ -241,7 +274,7 @@ module IR = struct
       blks = [{
           name=entry;
           keep=false;
-          weak=false;
+          weak=true;
           jmps=[];
           defs=[Def.reify ~tid v x]
         }]
@@ -268,6 +301,7 @@ module IR = struct
       if <body> is empty.
   *)
   let repeat cnd body =
+    let keep = true in
     cnd >>= fun cnd ->
     body >>| reify >>= function
     | {blks=[]} ->               (* empty denotation *)
@@ -277,7 +311,7 @@ module IR = struct
         entry = head;
         blks = [{
             name = head;
-            keep = true;
+            keep;
             weak = false;
             defs = [];
             jmps = [goto ~cnd ~tid head]}]}
@@ -289,13 +323,14 @@ module IR = struct
       fresh >>= fun jmp3 ->
       data {
         entry = head;
-        blks = blk tail ++ goto ~tid:jmp1 ~cnd loop ::
-               blk head ++ goto ~tid:jmp2 tail ::
+        blks = blk ~keep tail ++ goto ~tid:jmp1 ~cnd loop ::
+               blk ~keep head ++ goto ~tid:jmp2 tail ::
                b ++ goto ~tid:jmp3 tail ::
                blks
       }
 
   let branch cnd yes nay =
+    let keep = true in
     fresh >>= fun head ->
     fresh >>= fun tail ->
     cnd >>= fun cnd ->
@@ -314,8 +349,8 @@ module IR = struct
       ret {
         entry = head;
         blks =
-          blk tail ::
-          blk head ++
+          blk ~keep tail ::
+          blk ~keep head ++
           jump ~tid:jmp1 lhs ++
           goto ~tid:jmp2 tail ::
           b ++ goto ~tid:jmp3 tail ::
@@ -328,8 +363,8 @@ module IR = struct
       ret {
         entry = head;
         blks =
-          blk tail ::
-          blk head ++
+          blk ~keep tail ::
+          blk ~keep head ++
           jump ~tid:jmp1 tail ++
           goto ~tid:jmp2 rhs ::
           b ++ goto ~tid:jmp3 tail ::
@@ -343,8 +378,8 @@ module IR = struct
       ret {
         entry = head;
         blks =
-          blk tail ::
-          blk head ++
+          blk ~keep tail ::
+          blk ~keep head ++
           jump ~tid:jmp1 lhs ++
           goto ~tid:jmp2 rhs ::
           yes ++ goto ~tid:jmp3 tail ::
@@ -357,8 +392,8 @@ module IR = struct
       ret {
         entry = head;
         blks = [
-          blk tail;
-          blk head ++ jump ~tid:jmp1 tail ++ goto ~tid:jmp2 tail
+          blk ~keep tail;
+          blk ~keep head ++ jump ~tid:jmp1 tail ++ goto ~tid:jmp2 tail
         ]
       }
 
@@ -368,11 +403,9 @@ module IR = struct
     fresh >>= fun tid ->
     ctrl {
       entry;
-      blks = [blk ~keep:false entry ++ Jmp.reify ~tid ~dst:(Jmp.indirect dst) ()]
+      blks = [blk entry ++ Jmp.reify ~tid ~dst:(Jmp.indirect dst) ()]
     }
 
-  let is_call jmp = Option.is_some (Jmp.alt jmp)
-
   let is_unconditional jmp = match Jmp.cond jmp with
     | Int w when Word.(w = b1) -> true
     | _ -> false