diff --git a/lib/bap_primus/bap_primus_lisp_attribute.ml b/lib/bap_primus/bap_primus_lisp_attribute.ml
index 49761ff49..f687f87f9 100644
--- a/lib/bap_primus/bap_primus_lisp_attribute.ml
+++ b/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)
diff --git a/plugins/bil/bil_ir.ml b/plugins/bil/bil_ir.ml
index d7e0ffce1..4062c1621 100644
--- a/plugins/bil/bil_ir.ml
+++ b/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,32 +56,42 @@ 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 &&
@@ -88,30 +99,52 @@ module BIR = struct
       | 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
@@ -119,7 +152,7 @@ module BIR = struct
   *)
   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
diff --git a/plugins/ghidra/semantics/pcode.lisp b/plugins/ghidra/semantics/pcode.lisp
index 4cab3caca..f99e30f05 100644
--- a/plugins/ghidra/semantics/pcode.lisp
+++ b/plugins/ghidra/semantics/pcode.lisp
@@ -158,3 +158,119 @@
 
 (defun BOOL_XOR (tr r tx x ty y)
   (set# tr r (get# logxor tx x ty y)))
+
+(defparameter fp-rmode 'rne
+  "the floating-point operations rounding mode")
+
+(defparameter fp-format 'ieee754_binary
+  "the floating-point representation")
+
+
+(defmacro fp-binary (name tr r tx x ty y)
+  (set# tr r
+        (intrinsic
+         (symbol-concat name fp-rmode fp-format :sep '_)
+         (get# tx x)
+         (get# ty y)
+         :result tr)))
+
+(defmacro fp-unary (name tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat name fp-format :sep '_)
+         (get# tx x)
+         :result tr)))
+
+(defmacro fp-unary/rmode (name tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat name fp-rmode fp-format :sep '_)
+         (get# tx x)
+         :result tr)))
+
+(defmacro fp-predicate (name tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat 'is name fp-format :sep '_)
+         (get# tx x)
+         :result tr)))
+
+(defun fp-order (tx x ty y)
+  (intrinsic 'forder_ieee754_binary
+             (get# tx x)
+             (get# ty y)
+             :result 8))
+
+(defun fp-round (tr tx x)
+  (intrinsic
+   (symbol-concat 'fround fp-rmode fp-format :sep '_)
+   (get# tx x)
+   :result tr))
+
+(defun INT2FLOAT (tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat 'cast_sfloat fp-rmode fp-format :sep '_)
+         (get# tx x)
+         :result tr)))
+
+(defun TRUNC (tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat 'cast_sint 'rtz fp-format :sep '_)
+         (get# tx x)
+         :result tr)))
+
+(defun FLOAT2FLOAT (tr r tx x)
+  (set# tr r
+        (intrinsic
+         (symbol-concat 'fconvert fp-rmode fp-format)
+         (get# tx x)
+         :result tr)))
+
+(defun FLOAT_ADD (tr r tx x ty y)
+  (fp-binary 'fadd tr r tx x ty y))
+
+(defun FLOAT_SUB (tr r tx x ty y)
+  (fp-binary 'fsub tr r tx x ty y))
+
+(defun FLOAT_DIV (tr r tx x ty y)
+  (fp-binary 'fdiv tr r tx x ty y))
+
+(defun FLOAT_MULT (tr r tx x ty y)
+  (fp-binary 'fmul tr r tx x ty y))
+
+(defun FLOAT_NEG (tr r tx x)
+  (fp-unary 'fneg tr r tx x))
+
+(defun FLOAT_ABS (tr r tx x)
+  (fp-unary 'fabs tr r tx x))
+
+(defun FLOAT_SQRT (tr r tx x)
+  (fp-unary/rmode 'fsqrt tr r tx x))
+
+(defun FLOAT_NAN (tr r tx x)
+  (fp-predicate 'fnan tr r tx x))
+
+(defun FLOAT_EQUAL (tr r tx x ty y)
+  (set# tr r (is-zero (fp-order tx x ty y))))
+
+(defun FLOAT_NOTEQUAL (tr r tx x ty y)
+  (set# tr r (not (is-zero (fp-order tx x ty y)))))
+
+(defun FLOAT_LESS (tr r tx x ty y)
+  (set# tr r (is-negative (fp-order tx x ty y))))
+
+(defun FLOAT_LESSEQUAL (tr r tx x ty y)
+  (set# tr r (not (is-positive tx x ty y))))
+
+(defun FLOAT_ROUND (tr r tx x)
+  (set# tr r (fp-round tr tx x)))
+
+(defun FLOAT_CEIL (tr r tx x)
+  (let ((fp-rmode 'rtp))
+    (set# tr r (fp-round tr tx x))))
+
+(defun FLOAT_FLOOR (tr r tx x)
+  (let ((fp-rmode 'rtn))
+    (set# tr r (fp-round tr tx x))))
diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
index 4946f5762..0bab7f66d 100644
--- a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
+++ b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
@@ -201,6 +201,12 @@ let export = Primus.Lisp.Type.Spec.[
     "is-symbol", one any @-> bool,
     "(is-symbol X) is true if X has a symbolic value.";
 
+    "symbol-concat", all sym @-> sym,
+    "(symbol-concat S1 S2 .. SN OPT?) concatenates symbols
+    S1 till S2. An optional separator keyworded argument
+    takes form :sep SEP, where SEP is the separator that is
+    used to concatenate symbols";
+
     "alias-base-register", one int @-> int,
     "(alias-base-register x) if X has a symbolic value that is an
      aliased register returns the base register";
@@ -237,7 +243,24 @@ let export = Primus.Lisp.Type.Spec.[
     "special", (one sym @-> any),
     "(special :NAME) produces a special effect denoted by the keyword :NAME.
     The effect will be reified into the to the special:name subroutine. ";
-  ]
+    "intrinsic", tuple [sym] // all any @-> any,
+    "(intrinsic 'NAME ARG1 ARG2 ... ARGN PARAMS..) produces a call to
+     an intrinsic function with the given NAME. Arguments could be
+     regular semantic values. They are passed to the intrinsic
+     function in order, with the first argument passed via the
+     intrinsic:x0 ... intrinsic:xN variables. The keyworded parameters
+     are optional. And could be either :return SIZE, which indicates
+     that the call evaluates to a bitvector value of the given SIZE;
+     :writes REG SIZE? denotes that writes the result to a variable
+     REG (the size is optional if REG is a known target register);
+     :stores PTR SIZE? denotes that the intrinsic is storing output of
+     the given SIZE in bits at the memory location pointer by PTR.
+     When SIZE is omitted, it defaults to the data address size of the
+     target. The :result parameter may occur at most once. All other
+     parameters can be repeated. The intrinisic output is passed via
+     the intrinisic:y0,...,intrinisic:yM vector, with the first
+     element assigned to the :result, then to all :writes registers,
+     and after that to all :stores addresses." ]
 
 type KB.conflict += Illformed of string
                  | Failed_primitive of KB.Name.t * unit Theory.value list * string
@@ -305,6 +328,8 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
   let set_const v x =
     KB.Value.put Primus.Lisp.Semantics.static v (Some x)
   let const_int s x = CT.int s x >>| fun v -> set_const v x
+  let set_sym n v =
+    KB.Value.put Primus.Lisp.Semantics.symbol v (Some n)
   let int s x = const_int s @@ Bitvec.(int x mod modulus (size s))
   let true_ = CT.b1 >>| fun v -> set_const v Bitvec.one
   let false_ = CT.b0 >>| fun v -> set_const v Bitvec.zero
@@ -619,13 +644,161 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
         CT.var reg >>| fun v ->
         KB.Value.put Primus.Lisp.Semantics.symbol v (Some name)
 
+  module Intrinsic = struct
+    type param =
+      | Inputs
+      | Result
+      | Writes
+      | Stores
+      | Aborts
+    [@@deriving equal, compare, sexp, variants]
+
+    type arg = unit Theory.value
+
+    let sexp_of_arg v =
+      Sexp.Atom (Format.asprintf "%a" KB.Value.pp v)
+
+    type args = (param * arg list) list [@@deriving sexp_of]
+
+    let params = [
+      (* skip inputs as they are passed directly *)
+      ":result", result;
+      ":writes", writes;
+      ":stores", stores;
+      ":aborts", aborts;
+    ]
+
+
+    let parse_param input =
+      Option.(symbol input >>=
+              List.Assoc.find ~equal:String.equal params)
+
+    let parse_args args =
+      List.fold args ~init:([],[],Inputs) ~f:(fun (parsed,current,state) v ->
+          match parse_param v with
+          | Some state' ->
+            let parsed = (state,List.rev current) :: parsed in
+            (parsed,[],state')
+          | None -> (parsed,v::current,state))
+      |> fun (parsed,last,state) ->
+      List.rev ((state, List.rev last) :: parsed)
+
+    let get kw args =
+      List.Assoc.find ~equal:equal_param args kw |> function
+      | None -> []
+      | Some args -> args
+
+    let mk_var d i s =
+      Theory.Var.define s (sprintf "intrinsic:%c%d" d i)
+
+    let ivar = mk_var 'x'
+    let ovar = mk_var 'y'
+
+    let assign_inputs args =
+      seq@@List.mapi (get inputs args) ~f:(fun i x ->
+          let s = Theory.Value.sort x in
+          CT.set (ivar i s) !!x)
+
+    let invoke_symbol name =
+      let name = KB.Name.(unqualified@@read name) in
+      let* dst = Theory.Label.for_name (sprintf "intrinsic:%s" name) in
+      KB.provide Theory.Label.is_subroutine dst (Some true) >>= fun () ->
+      CT.goto dst
+
+    (* starts a new group on each symbol *)
+    let group_by_symbols =
+      List.group ~break:(fun _ v -> Option.is_some (symbol v))
+
+    let write_single t i v =
+      require_symbol v @@ fun v ->
+      match Theory.Target.var t v with
+      | None -> illformed ":writes argument is not a register"
+      | Some v ->
+        let s = Theory.Var.sort v in
+        CT.set (ovar i s) (CT.var v)
+
+    let write_typed t i v =
+      require_symbol v @@ fun v ->
+      let* t = static t in
+      let s = Theory.Value.Sort.forget@@Theory.Bitv.define t in
+      let v = Theory.Var.define s v in
+      CT.set (ovar i s) (CT.var v)
+
+    let group what args = group_by_symbols@@get what args
+    let result = get result
+    let writes = group writes
+    let stores = group stores
+
+    let assign_writes t xs =
+      let base = List.length (result xs) in
+      seq@@List.mapi (writes xs) ~f:(fun i -> function
+          | [reg] -> write_single t (base+i) reg
+          | [reg; typ] -> write_typed typ (base+i) reg
+          | _ -> illformed "incorrect :writes parameters")
+
+    let mk_store size t i ptr =
+      let s = Theory.Value.Sort.forget@@Theory.Bitv.define size in
+      let* v = CT.var (ovar i s) in
+      store_word t [ptr; v]
+
+    let store_word t =
+      mk_store (Theory.Target.data_addr_size t) t
+
+    let store t i ptr typ =
+      let* typ = static typ in
+      mk_store typ t i ptr
+
+    let assign_stores t xs =
+      let base = List.length (result xs) + List.length (writes xs) in
+      seq@@List.mapi (stores xs) ~f:(fun i -> function
+          | [ptr] -> store_word t (base+i) ptr
+          | [ptr; typ] -> store t (base+i) ptr typ
+          | _ -> illformed "incorrect :stores parameters")
+
+    let make_result size =
+      let* size = static size in
+      let s = Theory.Value.Sort.forget@@Theory.Bitv.define size in
+      CT.var@@ovar 0 s
+
+
+    let call t name args =
+      require_symbol name @@ fun name ->
+      let args = parse_args args in
+      let eff = seq [
+          data@@assign_inputs args;
+          ctrl@@invoke_symbol name;
+          data@@assign_writes t args;
+          data@@assign_stores t args;
+        ] in
+      match result args with
+      | [] -> eff
+      | [t] -> full eff (make_result t)
+      | _ -> illformed ":result may occur once and with a single argument"
+  end
+
+
+  let make_symbol s name =
+    intern name >>= const_int s >>| set_sym name |> forget
+
+  let symbol_concat s syms =
+    List.map syms ~f:symbol |> Option.all |> function
+    | None -> illformed "require all symbols"
+    | Some syms ->
+      let syms,sep =
+        List.split_while syms ~f:(Fn.non@@String.equal ":sep") in
+      let* sep = match sep with
+        | [] -> KB.return ""
+        | [_; sep] -> KB.return sep
+        | _ -> illformed ":sep must be last and followed by an argument" in
+      make_symbol s (String.concat ~sep syms)
+
   let symbol s v =
-    match KB.Value.get Primus.Lisp.Semantics.symbol v with
-    | Some name ->
-      intern name >>= const_int s |> forget
+    match symbol v with
+    | Some name -> make_symbol s name
     | None ->
       illformed "symbol requires a symbolic value"
 
+
   let is_symbol v =
     forget@@match KB.Value.get Primus.Lisp.Semantics.symbol v with
     | Some _ -> true_
@@ -799,6 +972,7 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | "get-program-counter",[]
     | "get-current-program-counter",[] -> pure@@get_pc s lbl
     | "set-symbol-value",[sym;x] -> data@@set_symbol t sym x
+    | "symbol-concat",syms -> pure@@symbol_concat s syms
     | "symbol",[x] ->  pure@@symbol s x
     | "is-symbol", [x] -> pure@@is_symbol x
     | "alias-base-register", [x] -> pure@@alias_base_register t x
@@ -810,6 +984,7 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | "concat", xs -> pure@@concat xs
     | ("select"|"nth"),xs -> pure@@select s xs
     | "empty",[] -> nop ()
+    | "intrinsic",(dst::args) -> Intrinsic.call t dst args
     | "special",[dst] -> ctrl@@special dst
     | "invoke-subroutine",[dst] -> ctrl@@invoke_subroutine dst
     | _ -> !!nothing
diff --git a/plugins/x86/semantics/pcode-cpuid.lisp b/plugins/x86/semantics/pcode-cpuid.lisp
new file mode 100644
index 000000000..7dea8fd41
--- /dev/null
+++ b/plugins/x86/semantics/pcode-cpuid.lisp
@@ -0,0 +1,58 @@
+(defpackage pcode-x86 (:use pcode))
+(in-package pcode-x86)
+
+(require pcode)
+
+(defmacro cpuid-subr (name tr r tx x)
+  (set# tr r (intrinsic name
+                        (get# tx x)
+                        :result tr)))
+
+(defun cpuid (tr r tx x)
+  (cpuid-subr 'cpuid tr r tx x))
+
+(defun cpuid_basic_info (tr r tx x)
+  (cpuid-subr 'cpuid_basic_info tr r tx x))
+
+(defun cpuid_Version_info (tr r tx x)
+  (cpuid-subr 'cpuid_version_info tr r tx x))
+
+(defun cpuid_cache_tlb_info (tr r tx x)
+  (cpuid-subr 'cpuid_cache_tlb_info tr r tx x))
+
+(defun cpuid_serial_info (tr r tx x)
+  (cpuid-subr 'cpuid_serial_info tr r tx x))
+
+(defun cpuid_Deterministic_Cache_Parameters_info (tr r tx x)
+  (cpuid-subr 'cpuid_deterministic_cache_parameters_info tr r tx x))
+
+(defun cpuid_MONITOR_MWAIT_Features_info (tr r tx x)
+  (cpuid-subr 'cpuid_monitor_mwait_features_info tr r tx x))
+
+(defun cpuid_Extended_Feature_Enumeration_info (tr r tx x)
+  (cpuid-subr 'cpuid_extended_feature_enumeration_info tr r tx x))
+
+(defun cpuid_Direct_Cache_Access_info (tr r tx x)
+  (cpuid-subr 'cpuid_direct_cache_access_info tr r tx x))
+
+(defun cpuid_Architectural_Performance_Monitoring_info (tr r tx x)
+  (cpuid-subr 'cpuid_architectural_performance_monitoring_info tr r tx x))
+
+
+(defun cpuid_Extended_Topology_info (tr r tx x)
+  (cpuid-subr 'cpuid_extended_topology_info tr r tx x))
+
+(defun cpuid_Processor_Extended_States_info (tr r tx x)
+  (cpuid-subr 'cpuid_processor_extended_states_info tr r tx x))
+
+(defun cpuid_Quality_of_Service_info (tr r tx x)
+  (cpuid-subr 'cpuid_quality_of_service_info tr r tx x))
+
+(defun cpuid_brand_part1_info (tr r tx x)
+  (cpuid-subr 'cpuid_brand_part1_info tr r tx x))
+
+(defun cpuid_brand_part2_info (tr r tx x)
+  (cpuid-subr 'cpuid_brand_part2_info tr r tx x))
+
+(defun cpuid_brand_part3_info (tr r tx x)
+  (cpuid-subr 'cpuid_brand_part3_info tr r tx x))