adds several new Primus Lisp primitives and new instructions (#1410)

* adds several new Primus Lisp primitives and new instructions

This commit adds three new primitives that could be used in definition
instruction semantics:

 - invoke-subroutine, especially useful for intrinsic calls
 - empty, which denotes empty semantics, useful for nops
 - special to denote special semantics, like `hlt`

It also implements semantics for several missing semantics (detected
with `--print-missing`), mostly nops, but there's one significant
finding - the `popa` (POPA32 in llvm parlance) instruction from x86,
which was surprisingly missing.

* adds support for specials in the BIL effect analyzer

this enables proper handling of specially encoded calls and intrinsics

Author: ivg

lib/bap_disasm/bap_disasm_insn.ml

@@ -229,7 +229,7 @@ module Analyzer = struct
     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
+      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) =
@@ -239,6 +239,9 @@ module Analyzer = struct
         | 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 =
@@ -258,9 +261,8 @@ let derive_props ?bil insn =
   let is = Insn.is insn in
   let is_bil = if Option.is_some bil
     then Analyzer.Effects.mem bil_effects else is in
-  (* those two are the only which we can't get from the BIL semantics *)
   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

oasis/powerpc

@@ -40,6 +40,7 @@ Library powerpc_plugin
                     Powerpc_shift,
                     Powerpc_store,
                     Powerpc_sub
+  DataFiles:        semantics/*.lisp ($datadir/bap/primus/semantics)
   XMETAExtraLines:  tags="powerpc, lifter"
 
 Library powerpc_test

oasis/x86

@@ -75,6 +75,7 @@ Library x86_plugin
                    X86_legacy_fp_lifter,
                    X86_legacy_bil_register,
                    X86_legacy_operands
+ DataFiles:        semantics/*.lisp ($datadir/bap/primus/semantics)
  XMETAExtraLines:  tags="disassembler, lifter, x86, abi"
 
 Library x86_test

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

plugins/powerpc/semantics/powerpc.lisp

@@ -0,0 +1,8 @@
+(declare (context (target powerpc)))
+
+(defpackage powerpc (:use core target))
+(defpackage llvm-powerpc32 (:use powerpc))
+
+
+(defun NOP ()
+  (empty))

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
@@ -433,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
@@ -620,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 ->
@@ -784,12 +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 Lisp = Primus.Lisp.Semantics
 
 let provide () =

plugins/riscv/semantics/riscv.lisp

@@ -214,3 +214,10 @@
 
 (defun C_BNEZ (rs1 off)
   (conditional-jump (not (is-zero rs1)) off))
+
+
+(defun C_NOP ()
+  (empty))
+
+(defun NOP ()
+  (empty))

plugins/x86/semantics/x86-32.lisp

@@ -0,0 +1,18 @@
+(declare (context (target i386) (bits 32)))
+
+(require x86-common)
+(in-package x86-32)
+
+(defun pop (dst)
+  (set$ dst (load-word ESP))
+  (+= ESP 4))
+
+(defun POPA32 ()
+  (pop 'EDI)
+  (pop 'ESI)
+  (pop 'EBP)
+  (+= ESP 4)
+  (pop 'EBX)
+  (pop 'EDX)
+  (pop 'ECX)
+  (pop 'EAX))

plugins/x86/semantics/x86-64.lisp

@@ -0,0 +1,2 @@
+(declare (context (target amd 64) (bits 64)))
+(require x86-common)

plugins/x86/semantics/x86-common.lisp

@@ -0,0 +1,21 @@
+(declare (context (target x86)))
+
+(defpackage x86-common (:use core target))
+(defpackage x86-32 (:use x86-common))
+(defpackage x86-64 (:use x86-common))
+(defpackage llvm-x86 (:use x86-32))
+(defpackage llvm-x86_64 (:use x86-64))
+
+(in-package x86-common)
+
+(defun HLT ()
+  (special :hlt))
+
+(defun NOOP ()
+  (empty))
+
+(defun NOOPL (_ _ _ _ _)
+  (empty))
+
+(defun NOOPW (_ _ _ _ _)
+  (empty))