removes the special Primus Lisp primitive

lib/bap_sema/bap_sema_lift.ml

@@ -333,7 +333,7 @@ let link_call symtab addr sub_of_blk jmp =
 
 let is_intrinsic sub =
   match KB.Name.package @@ KB.Name.read (Ir_sub.name sub) with
-  | "intrinsic" | "special" -> true
+  | "intrinsic" -> true
   | _ -> false
 
 let create_synthetic tid =

lib/bap_types/bap_ir.ml

@@ -125,8 +125,10 @@ module Tid = struct
   let pp ppf tid = Format.fprintf ppf "%s" (to_string tid)
 
   let name t = match get_name t with
-    | None -> to_string t
     | Some name -> sprintf "@%s" name
+    | None -> match get_ivec t with
+      | None -> to_string t
+      | Some ivec -> sprintf "@interrupt:#%d" ivec
 
   let from_string_exn = of_string
   let from_string x = Ok (from_string_exn x)
@@ -1662,7 +1664,7 @@ module Ir_blk = struct
     let (++) = Set.union and (--) = Set.diff in
     let init = Bap_var.Set.empty,Bap_var.Set.empty in
     fst @@ Seq.fold (elts blk) ~init ~f:(fun (vars,kill) -> function
-        | `Phi phi -> vars, kill
+        | `Phi _ -> vars, kill
         | `Def def ->
           Ir_def.free_vars def -- kill ++ vars,
           Set.add kill (Ir_def.lhs def)
@@ -1731,14 +1733,19 @@ end
 module Ir_sub = struct
   type t = sub term
 
-  let new_empty ?(tid=Tid.create ()) ?name () : t =
-    let name = match name with
+  let make_name ?name tid =
+    match name with
+    | Some name -> name
+    | None -> match Tid.get_name tid with
       | Some name -> name
-      | None -> match Tid.get_name tid with
+      | None -> match Tid.get_ivec tid with
         | None -> Tid.to_string tid
-        | Some name -> name in
+        | Some ivec ->
+          Format.asprintf "interrupt:#%d" ivec
+
+  let new_empty ?(tid=Tid.create ()) ?name () : t =
     make_term tid {
-      name;
+      name = make_name ?name tid;
       args = [| |] ;
       blks = [| |] ;
     }
@@ -1872,9 +1879,7 @@ module Ir_sub = struct
         | None -> Tid.create () in
       let args = Vec.to_array args in
       let blks = Vec.to_array blks in
-      let name = match name with
-        | Some name -> name
-        | None -> Format.asprintf "sub_%a" Tid.pp tid in
+      let name = make_name ?name tid in
       make_term tid {name; args; blks}
   end
 

plugins/arm/semantics/aarch64-atomic.lisp

@@ -12,9 +12,9 @@
    acquire and release are booleans indicating whether load-acquire and
    store-release ordering is to be enforced."
    (let ((data (load rn)))
-    (when acquire (special :load-acquire))
+    (when acquire (intrinsic 'load-acquire))
     (when (= data rs)
-      (when release (special :store-release))
+      (when release (intrinsic 'store-release))
       (store rn rt))
     (set rs data)))
 
@@ -79,4 +79,4 @@
 (defun CSINVWr (rd rn rm cnd) (CSop*r setw lnot rd rn rm cnd))
 (defun CSINVXr (rd rn rm cnd) (CSop*r set$ lnot rd rn rm cnd))
 (defun CSNEGWr (rd rn rm cnd) (CSop*r setw neg  rd rn rm cnd))  ;; 2's complement negation
-(defun CSNEGXr (rd rn rm cnd) (CSop*r set$ neg  rd rn rm cnd))  ;; 2's complement negation
+(defun CSNEGXr (rd rn rm cnd) (CSop*r set$ neg  rd rn rm cnd))  ;; 2's complement negation

plugins/arm/semantics/aarch64-special.lisp

@@ -5,19 +5,21 @@
 ;;; SPECIAL INSTRUCTIONS
 
 (defun make-barrier (barrier-type option)
-  (special (symbol-concat :barrier barrier-type (barrier-option-to-symbol option))))
+  (intrinsic (symbol-concat 'barrier
+                             barrier-type
+                             (barrier-option-to-symbol option))))
 
-(defun DMB (option) (make-barrier :dmb option))
+(defun DMB (option) (make-barrier 'dmb option))
 
-(defun DSB (option) (make-barrier :dsb option))
+(defun DSB (option) (make-barrier 'dsb option))
 
 ;; strictly speaking, only the sy option is valid and is
 ;; the default option (it can be omitted from the mnemonic).
 ;; still including option here though
-(defun ISB (option) (make-barrier :isb option))
+(defun ISB (option) (make-barrier 'isb option))
 
 (defun HINT (_)
   (empty))
 
 (defun UDF (exn)
-  (special :undefined-instruction))
+  (intrinsic 'undefined-instruction))

plugins/primus_lisp/primus_lisp_semantic_primitives.ml

@@ -241,9 +241,6 @@ let export = Primus.Lisp.Type.Spec.[
      The function is equivalent to (select N X)";
     "empty", (unit @-> any),
     "(empty) denotes an instruction that does nothing, i.e., a nop.";
-    "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
@@ -820,15 +817,6 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | Some _ -> true_
     | _ -> false_
 
-  let is_keyword = String.is_prefix ~prefix:":"
-
-  let special dst =
-    require_symbol dst @@ fun dst ->
-    if is_keyword dst then
-      let* dst = Theory.Label.for_name ("special"^dst) in
-      CT.goto dst
-    else illformed "special requires a keyword as the tag, e.g., :hlt"
-
   let invoke_subroutine dst =
     require_symbol dst @@ fun dst ->
     let* dst = Theory.Label.for_name dst in
@@ -992,7 +980,6 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | ("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
 end

plugins/relocatable/rel_symbolizer.ml

@@ -163,11 +163,8 @@ let plt_size label =
   List.find_map plt_sizes ~f:(fun (p,s) ->
       Option.some_if (Theory.Target.belongs p t) s)
 
-let is_intrinsic name =
-  List.exists ~f:(fun prefix -> String.is_prefix ~prefix name) [
-    "intrinsic:";
-    "special:";
-  ]
+let is_intrinsic =
+  String.is_prefix ~prefix:"intrinsic:"
 
 let demangle s = match String.chop_suffix ~suffix:":external" s with
   | None -> s

plugins/x86/semantics/x86-common.lisp

@@ -9,7 +9,7 @@
 (in-package x86-common)
 
 (defun HLT ()
-  (special :hlt))
+  (intrinsic 'hlt))
 
 (defun NOOP ()
   (empty))