removes the special Primus Lisp primitive (#1477)

* unifies name generation for IR subroutines

It turned out that empty subroutines and non-empty subroutines could
have had different names.

* implements a new naming scheme for interrupts

* removes the special Primus Lisp primitive

This primitive is now fully subsumed by the `intrinsic` primitive so
there's no need to have two names for the same thing. To update the
existing code that uses special, substitute every occurence of
`(special :foo)` with `(intrinsic 'foo)`

Author: ivg

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 =

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))