From 41bb72062fc3e4008f9dd040137c572ffe6413c0 Mon Sep 17 00:00:00 2001
From: DukMastaaa <64053792+DukMastaaa@users.noreply.github.com>
Date: Fri, 4 Feb 2022 00:56:01 +0000
Subject: [PATCH] update code to PR #1410 in main repo

---
 lib/bap_disasm/bap_disasm_insn.ml             | 148 ++---
 plugins/arm/semantics/aarch64.lisp            |   7 +
 plugins/primus_lisp/primus_lisp_main.ml       |   1 -
 .../primus_lisp_semantic_primitives.ml        | 532 +-----------------
 .../primus_lisp_semantic_primitives.mli       |   1 -
 5 files changed, 92 insertions(+), 597 deletions(-)

diff --git a/lib/bap_disasm/bap_disasm_insn.ml b/lib/bap_disasm/bap_disasm_insn.ml
index 3638ac229..a7528ec07 100644
--- a/lib/bap_disasm/bap_disasm_insn.ml
+++ b/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"
diff --git a/plugins/arm/semantics/aarch64.lisp b/plugins/arm/semantics/aarch64.lisp
index 3773b6735..90978c302 100644
--- a/plugins/arm/semantics/aarch64.lisp
+++ b/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))
diff --git a/plugins/primus_lisp/primus_lisp_main.ml b/plugins/primus_lisp/primus_lisp_main.ml
index d8a64abed..72e1da025 100644
--- a/plugins/primus_lisp/primus_lisp_main.ml
+++ b/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
diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
index 83d51de5d..4946f5762 100644
--- a/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
+++ b/plugins/primus_lisp/primus_lisp_semantic_primitives.ml
@@ -144,7 +144,10 @@ let export = Primus.Lisp.Type.Spec.[
      machine word.";
 
     "exec-addr", one int @-> any,
-    "(exec-addr ADDR) transfers control flow to ADDR.";
+    "(exec-addr ADDR) transfers control to ADDR.";
+
+    "invoke-subroutine", one sym @-> any,
+    "(invoke-subroutine NAME) passes control to the subroutine NAME.";
 
     "goto-subinstruction", one int @-> any,
     "(goto-subinstruction N) transfers control flow to a
@@ -188,7 +191,7 @@ let export = Primus.Lisp.Type.Spec.[
     "get-current-program-counter", unit @-> int,
     "(get-current-program-counter) is an alias to (get-program-counter)";
 
-    "set-symbol-value", tuple [int; a] @-> a,
+    "set-symbol-value", tuple [any; a] @-> a,
     "(set-symbol-value S X) sets the value of the symbol S to X.
          Returns X";
 
@@ -229,6 +232,11 @@ let export = Primus.Lisp.Type.Spec.[
     "nth", (one any @-> bool),
     "(nth N X) returns the Nth bit of X. N must be static. \
      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. ";
   ]
 
 type KB.conflict += Illformed of string
@@ -251,19 +259,6 @@ let () = KB.Conflict.register_printer (function
     | _ -> None)
 
 
-let domain = KB.Domain.optional "cst"
-    ~equal:Sexp.equal
-    ~inspect:ident
-
-let eslot = KB.Class.property Theory.Semantics.cls "eff"
-    ~package:"core"
-    ~public:true
-    domain
-
-let pslot = KB.Class.property Theory.Value.cls "val"
-    ~package:"core"
-    ~public:true
-    domain
 
 let nothing = KB.Value.empty Theory.Semantics.cls
 let size = Theory.Bitv.size
@@ -446,6 +441,9 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
   let memory eff res =
     full CT.(blk null (perform eff) skip) res
 
+  let nop () =
+    CT.perform Theory.Effect.Sort.bot
+
   let loads = memory Theory.Effect.Sort.rmem
   let stores = memory Theory.Effect.Sort.wmem
   let loads = pure
@@ -483,11 +481,6 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
         let dst = Bitvec.to_int dst + pos in
         Bap.Std.Insn.Seqnum.label dst >>=
         CT.goto
-  
-    (*! trying to make special in semantic primitives*)
-  (* let make_special lbl args =
-    (* Bap.Std.Bil.Types.Special "hello" *)
-    CT.blk lbl (seq []) (Theory.Stmt) *)
 
   let load_byte t xs =
     let mem = CT.var @@ Theory.Target.data t in
@@ -638,6 +631,20 @@ 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
+    CT.goto dst
+
   let mk_cast t cast xs =
     binary xs @@ fun sz x ->
     to_sort sz >>= fun s ->
@@ -781,7 +788,6 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | "word-width",_-> pure@@word_width s args
     | "exec-addr",_-> ctrl@@exec_addr args
     | "goto-subinstruction",_ -> ctrl@@goto_subinstruction lbl args
-    (* | "make-special",_ -> ctrl@@make_special lbl args *)
     | ("load-byte"|"memory-read"),_-> pure@@load_byte t args
     | "load-word",_-> pure@@load_word t args
     | "load-hword",_-> pure@@load_half t args
@@ -803,483 +809,12 @@ module Primitives(CT : Theory.Core)(T : Target) = struct
     | "extract",xs -> pure@@extract xs
     | "concat", xs -> pure@@concat xs
     | ("select"|"nth"),xs -> pure@@select s xs
+    | "empty",[] -> nop ()
+    | "special",[dst] -> ctrl@@special dst
+    | "invoke-subroutine",[dst] -> ctrl@@invoke_subroutine dst
     | _ -> !!nothing
 end
 
-
-module CST : Theory.Core = struct
-  type t = Sexp.t
-
-
-  let pure s cst = KB.Value.put pslot (Theory.Value.empty s) (Some cst)
-  let eff s cst = KB.Value.put eslot (Theory.Effect.empty s) (Some cst)
-  let data = eff Theory.Effect.Sort.bot
-  let ctrl = eff Theory.Effect.Sort.bot
-  let ret = KB.return
-  let atom s = Sexp.Atom s
-
-  let list = function
-    | [Sexp.Atom op;
-       List ((Atom opx) :: xs);
-       List ((Atom opy) :: ys)]
-      when String.(op = opx && op = opy) ->
-      Sexp.List (Atom op :: List.append xs ys)
-    | [Sexp.Atom op; List ((Atom opx) :: xs); y]
-      when String.(op = opx) ->
-      Sexp.List (Sexp.Atom op :: xs@[y])
-    | [Sexp.Atom op; x; List ((Atom opy) :: ys)]
-      when String.(op = opy) ->
-      Sexp.List (Sexp.Atom op :: x :: ys)
-    | xs -> Sexp.List xs
-
-  let app x xs = list (atom x :: xs)
-
-  let psort = Theory.Value.sort
-  let esort = Theory.Effect.sort
-
-  let (>>->) x f =
-    x >>= fun v ->
-    let s = psort v in
-    f s (KB.Value.get pslot v)
-
-  let (>>|>) x f = x >>-> fun s v -> ret (f s v)
-
-  let (>>->?) x f =
-    x >>= fun v ->
-    let s = psort v in
-    match KB.Value.get pslot v with
-    | None -> ret (Theory.Value.empty s)
-    | Some v -> f s v
-
-
-  let (>>|>?) x f = x >>->? fun s v -> ret (f s v)
-
-  let (>>=>) x f =
-    x >>= fun v ->
-    let s = esort v in
-    f s (KB.Value.get eslot v)
-
-  let (>>=>?) x f =
-    x >>= fun v ->
-    let s = esort v in
-    match KB.Value.get eslot v with
-    | None -> f s (list [])
-    | Some x -> f s x
-
-
-  let empty = Theory.Value.empty
-
-  let unary_s s op x = x >>|> fun _ -> function
-    | None -> empty s
-    | Some v -> pure s @@ app op [v]
-
-  let unary op x = x >>|>? fun s v -> pure s @@ app op [v]
-
-  let monoid_s s op x y =
-    x >>-> fun _ x ->
-    y >>|> fun _ y ->
-    match x, y with
-    | Some x, Some y -> pure s @@ app op [x; y]
-    | _ -> empty s
-
-  let monoid op x y =
-    x >>->? fun s x ->
-    y >>|>? fun _ y ->
-    pure s @@ app op [x; y]
-
-  module Minimal = struct
-    let b0 = ret@@pure Theory.Bool.t (atom "0")
-    let b1 = ret@@pure Theory.Bool.t (atom "1")
-
-    let unk s = ret@@empty s
-
-    let var v =
-      let s = Theory.Var.sort v in
-      ret@@pure s@@atom (Theory.Var.name v)
-
-    let let_ v x y =
-      x >>-> fun _ x ->
-      y >>|> fun s y ->
-      let name = Theory.Var.name v in
-      match x,y with
-      | Some x, Some y ->
-        pure s@@app "let" [atom name; x; y]
-      | _ -> empty s
-
-    let ite c x y =
-      c >>-> fun _ c ->
-      x >>->? fun s x ->
-      y >>|>? fun _ y -> match c with
-      | None -> empty s
-      | Some c -> pure s@@app "ite" [c; x; y]
-
-    let inv = unary "not"
-    let and_ = monoid "logand"
-    let or_ = monoid "logor"
-    let int s x = ret@@pure s@@atom (Bitvec.to_string x)
-    let msb x = unary_s Theory.Bool.t "msb" x
-    let lsb x = unary_s Theory.Bool.t "lsb" x
-    let neg x = unary "-" x
-    let not x = unary "not" x
-    let add x = monoid "+" x
-    let sub x = monoid "-" x
-    let mul x = monoid "*" x
-    let div x = monoid "/" x
-    let sdiv x = monoid "s/" x
-    let modulo x = monoid "mod" x
-    let smodulo x = monoid "signed-mod" x
-    let logand x = monoid "logand" x
-    let logor x = monoid "logor" x
-    let logxor x = monoid "logxor" x
-
-    let genshift name fill x off =
-      fill >>-> fun _ fill ->
-      x >>-> fun s x ->
-      off >>|> fun _ off ->
-      match fill, x, off with
-      | Some fill, Some x, Some off ->
-        pure s @@ app name [fill; x; off]
-      | _ -> empty s
-    let shiftr x = genshift "shiftr" x
-    let shiftl x = genshift "shiftl" x
-    let sle x = monoid_s Theory.Bool.t "s<=" x
-    let ule x = monoid_s Theory.Bool.t "<" x
-
-
-    let cast s fill exp =
-      fill >>-> fun _ fill ->
-      exp >>|> fun s' x ->
-      let ct = sprintf "%d" @@ Theory.Bitv.size s in
-      match fill, x  with
-      | Some fill, Some x ->
-        if Theory.Value.Sort.same s s'
-        then pure s x
-        else
-          pure s@@list [
-            atom "cast";
-            atom ct;
-            fill;
-            x
-          ]
-      | _ -> empty s
-
-    let concat s xs =
-      List.map xs ~f:(fun x -> x >>|> fun _ -> ident) |>
-      KB.List.all >>| Option.all >>| function
-      | None -> empty s
-      | Some xs -> pure s @@ app "concat" xs
-
-    let append s x y = monoid_s s "append" x y
-
-    let load m x =
-      m >>-> fun s m ->
-      x >>|> fun _ x ->
-      let s = Theory.Mem.vals s in
-      match m, x with
-      | Some m, Some x -> pure s @@ app "load" [m; x]
-      | _ -> empty s
-
-    let store m p x =
-      m >>-> fun s m ->
-      p >>-> fun _ p ->
-      x >>|> fun _ x ->
-      match m, p, x with
-      | Some m, Some p, Some x ->
-        pure s @@ app "store" [m; p; x]
-      | _ -> empty s
-
-    let nil = Theory.Effect.empty Theory.Effect.Sort.bot
-
-    let perform eff = ret (Theory.Effect.empty eff)
-
-    let set v x = x >>|> fun _ x ->
-      match x with
-      | None -> nil
-      | Some x -> data@@app "set" [
-          atom (Theory.Var.name v);
-          x
-        ]
-
-    let jmp x = x >>|> fun _ x -> match x with
-      | None -> nil
-      | Some x -> ctrl@@app "goto" [x]
-
-    let goto dst =
-      KB.collect Theory.Label.addr dst >>= function
-      | Some dst ->
-        ret@@ctrl@@app "goto" [atom (Bitvec.to_string dst)]
-      | None ->
-        KB.Object.repr Theory.Program.cls dst >>= fun dst ->
-        ret@@ctrl@@app "goto" [atom dst]
-
-    let both s xs ys =
-      match xs,ys with
-      | None,None -> ret nil
-      | Some r,None
-      | None, Some r -> ret@@eff s r
-      | Some xs, Some ys ->
-        ret@@eff s@@list [xs; ys]
-
-    let seq xs ys =
-      xs >>=> fun s xs ->
-      ys >>=> fun _ ys ->
-      both s xs ys
-
-    let blk _ xs ys =
-      xs >>=> fun _ xs ->
-      ys >>=> fun _ ys ->
-      both Theory.Effect.Sort.top xs ys
-
-    let repeat cnd body =
-      cnd >>-> fun _ cnd ->
-      body >>=>? fun s body ->
-      match cnd with
-      | None -> ret@@nil
-      | Some cnd ->
-        ret@@eff s@@app "while" [cnd; body]
-
-    let branch cnd yes nay =
-      cnd >>-> fun _ cnd ->
-      yes >>=>? fun s yes ->
-      nay >>=>? fun _ nay ->
-      match cnd with
-      | None -> ret@@nil
-      | Some cnd ->
-        ret@@eff s@@app "if" [cnd; yes; nay]
-  end
-  include Theory.Basic.Make(Minimal)
-
-  let mk_cast name s x =
-    x >>|> fun s' x -> match x with
-    | None -> empty s
-    | Some x ->
-      if Theory.Value.Sort.same s s'
-      then pure s x
-      else pure s@@app name [
-          atom@@sprintf "%d" (Theory.Bitv.size s);
-          x
-        ]
-
-  let high s = mk_cast "high" s
-  let low s = mk_cast "low" s
-  let signed s = mk_cast "signed" s
-  let unsigned s = mk_cast "unsigned" s
-
-  let extract s lo hi x =
-    lo >>-> fun _ lo ->
-    hi >>-> fun _ hi ->
-    x >>|> fun _ x ->
-    match lo,hi,x with
-    | Some lo, Some hi, Some x ->
-      pure s@@app "extract" [lo; hi; x]
-    | _ -> empty s
-
-  let loadw s dir mem ptr =
-    dir >>-> fun _ dir ->
-    mem >>-> fun _ mem ->
-    ptr >>|> fun _ ptr ->
-    match dir,mem,ptr with
-    | Some dir, Some mem, Some ptr ->
-      pure s@@app "loadw" [
-        atom@@sprintf "%d" (Theory.Bitv.size s);
-        dir;
-        mem;
-        ptr
-      ]
-    | _ -> empty s
-
-  let storew dir mem ptr exp =
-    dir >>-> fun _ dir ->
-    mem >>-> fun s mem ->
-    ptr >>-> fun _ ptr ->
-    exp >>|> fun _ exp ->
-    match Option.all [dir; mem; ptr; exp] with
-    | Some args -> pure s@@app "storew" args
-    | _ -> empty s
-
-  let mk_shift name x m =
-    x >>->? fun s x ->
-    m >>|> fun _ -> function
-    | None -> empty s
-    | Some m -> pure s@@app name [x; m]
-
-  let arshift x = mk_shift "arshift" x
-  let rshift x = mk_shift "rshift" x
-  let lshift x = mk_shift "lshift" x
-  let eq x = monoid_s Theory.Bool.t "=" x
-  let neq x = monoid_s Theory.Bool.t "/=" x
-  let slt x = monoid_s Theory.Bool.t "s<" x
-  let ult x = monoid_s Theory.Bool.t "<" x
-  let sgt x = monoid_s Theory.Bool.t "s>" x
-  let ugt x = monoid_s Theory.Bool.t ">" x
-  let sge x = monoid_s Theory.Bool.t "s>=" x
-  let uge x = monoid_s Theory.Bool.t ">=" x
-
-  let asort s =
-    atom@@Format.asprintf "%a" Theory.Value.Sort.pp (Theory.Value.Sort.forget s)
-
-
-  let wellknown = Theory.IEEE754.[
-      binary16,  ":b16";
-      binary32,  ":b32";
-      binary64,  ":b64";
-      binary80,  ":b80";
-      binary128, ":b128";
-      decimal32, ":d32";
-      decimal64, ":d64";
-      decimal128, ":d128";
-    ]
-
-  let format s =
-    let s = Theory.Value.Sort.forget s in
-    match Theory.Float.(refine s) with
-    | None -> asort s
-    | Some s ->
-      List.find_map wellknown ~f:(fun (par,name) ->
-          let s' = Theory.IEEE754.Sort.define par in
-          if Theory.Value.Sort.same s s'
-          then Some (atom name)
-          else None) |> function
-      | Some s -> s
-      | None -> asort s
-
-
-
-  let float s x =
-    x >>|> fun _ x -> match x with
-    | None -> empty s
-    | Some x -> pure s@@app "float" [format s; x]
-
-  let fbits x =
-    x >>|> fun s x ->
-    let s = Theory.Float.bits s in
-    match x with
-    | None -> empty s
-    | Some x -> pure s@@app "fbits" [x]
-
-  let is_finite x = unary_s Theory.Bool.t "is-finite" x
-  let is_nan x = unary_s Theory.Bool.t "is-nan" x
-  let is_inf x = unary_s Theory.Bool.t "is-inf" x
-  let is_fzero x = unary_s Theory.Bool.t "is-fzero" x
-  let is_fpos x = unary_s Theory.Bool.t "is-fpos" x
-  let is_fneg x = unary_s Theory.Bool.t "is-fneg" x
-
-  let rmode s = ret@@pure Theory.Rmode.t @@ atom s
-  let rne = rmode ":rne"
-  let rna = rmode ":rna"
-  let rtp = rmode ":rtp"
-  let rtn = rmode ":rtn"
-  let rtz = rmode ":rtz"
-  let requal = eq
-
-  let mk_fcast name s m x =
-    m >>-> fun _ m ->
-    x >>|> fun _ x ->
-    match m,x with
-    | Some m, Some x -> pure s@@app name [m;x]
-    | _ -> empty s
-
-  let cast_float s = mk_fcast "cast-float" s
-  let cast_sfloat s = mk_fcast "cast-sfloat" s
-  let cast_int s = mk_fcast "cast-int" s
-  let cast_sint s = mk_fcast "cast-sint" s
-
-  let fneg x = unary "fneg" x
-  let fabs x = unary "fabs" x
-
-  let monoid_f name m x y =
-    x >>->? fun s x ->
-    y >>->? fun _ y ->
-    m >>|> fun _ m ->
-    match m with
-    | None -> empty s
-    | Some m -> pure s@@app name [m; x; y]
-
-  let unary_f name m x =
-    x >>->? fun s x ->
-    m >>|> fun _ m ->
-    match m with
-    | None -> empty s
-    | Some m -> pure s@@app name [m; x]
-
-  let ternary_f name m x y z =
-    x >>->? fun s x ->
-    y >>->? fun _ y ->
-    z >>->? fun _ z ->
-    m >>|> fun _ m ->
-    match m with
-    | None -> empty s
-    | Some m -> pure s@@app name [m; x; y; z]
-
-  let binary_fi name m f x =
-    f >>->? fun s f ->
-    m >>-> fun _ m ->
-    x >>|> fun _ x ->
-    match m,x with
-    | Some m, Some x -> pure s@@app name [m; f; x]
-    | _ -> empty s
-
-
-  let fadd m = monoid_f "+." m
-  let fsub m = monoid_f "-." m
-  let fmul m = monoid_f "*." m
-  let fdiv m = monoid_f "/." m
-  let fmodulo m = monoid_f "mod." m
-  let fsqrt m = unary_f "fsqrt" m
-  let fround m = unary_f "fround" m
-  let fmad m = ternary_f "fmad" m
-  let fsucc x = unary "fsucc" x
-  let fpred x = unary "fpred" x
-  let forder x = monoid_s Theory.Bool.t "forder" x
-
-  let fconvert s m x =
-    m >>-> fun _ m ->
-    x >>|> fun _ x ->
-    match m,x with
-    | Some m, Some x -> pure s@@app "fconvert" [
-        format s; m; x
-      ]
-    | _ -> empty s
-
-  let pow m = monoid_f "pow" m
-  let hypot m = monoid_f "hypot" m
-
-  let rsqrt m = unary_f "rsqrt" m
-  let exp m = unary_f "exp" m
-  let expm1 m = unary_f "expm1" m
-  let exp2 m = unary_f "exp2" m
-  let exp2m1 m = unary_f "exp2m1" m
-  let exp10 m = unary_f "exp10" m
-  let exp10m1 m = unary_f "exp10m1" m
-  let log m = unary_f "log" m
-  let log2 m = unary_f "log2" m
-  let log10 m = unary_f "log10" m
-  let logp1 m = unary_f "logp1" m
-  let log2p1 m = unary_f "log2p1" m
-  let log10p1 m = unary_f "log10p1" m
-  let sin m = unary_f "sin" m
-  let cos m = unary_f "cos" m
-  let tan m = unary_f "tan" m
-  let sinpi m = unary_f "sinpi" m
-  let cospi m = unary_f "cospi" m
-  let atanpi m = unary_f "atanpi" m
-  let atan2pi m = monoid_f "atan2pi" m
-  let asin m = unary_f "asin" m
-  let acos m = unary_f "acos" m
-  let atan m = unary_f "atan" m
-  let atan2 m = monoid_f "atan2" m
-  let sinh m = unary_f "sinh" m
-  let cosh m = unary_f "cosh" m
-  let tanh m = unary_f "tanh" m
-  let asinh m = unary_f "asinh" m
-  let acosh m = unary_f "acosh" m
-  let atanh m = unary_f "atanh" m
-
-  let compound m = binary_fi "compound" m
-  let rootn m = binary_fi "rootn" m
-  let pown m = binary_fi "pown" m
-end
-
 module Lisp = Primus.Lisp.Semantics
 
 let provide () =
@@ -1295,10 +830,3 @@ let provide () =
               let name = KB.Name.create ~package:"core" name in
               KB.fail (Failed_primitive (name,args,err))
             | other -> KB.fail other))
-
-
-let enable_extraction () =
-  Theory.declare ~provides:["extraction"; "primus-lisp"; "lisp"]
-    ~package:"core"
-    ~name:"syntax" (KB.return (module CST : Theory.Core))
-
diff --git a/plugins/primus_lisp/primus_lisp_semantic_primitives.mli b/plugins/primus_lisp/primus_lisp_semantic_primitives.mli
index f6e3a38f1..74ab45393 100644
--- a/plugins/primus_lisp/primus_lisp_semantic_primitives.mli
+++ b/plugins/primus_lisp/primus_lisp_semantic_primitives.mli
@@ -1,2 +1 @@
 val provide : unit -> unit
-val enable_extraction : unit -> unit