adds semantics for the x86 SSE floating-point instructions (#1466)

* marks synthetic subroutines with proper attributes All synthetic subroutines are marked with the synthetic attribute, and special together with intrinsic functions are marked as intrinsic. * prevents C ABI pass from clobbering registers on intrinsic calls a little bit hacky, but will make it better in the future * do not correct the stack pointer on calls to intrinsic functions * adds the MXCSR register to the x86-64 environment * fixes a bug in the intrinisic primtive the repetitive parameters were ignored * fixes the IR contraction procedure again and enables unconditionally * adds the semantics of the basic SSE floating-point operations * adds the implementation of some ieee754 intrinsics * relaxes the contraction predicate * fixes the pcode floating-point lifter we now are passing the tests! * makes the word-width primitive equal in both versions of Primus * adds the ieee754-is-nan primitive * adds more SSE instruction, implements branchless comparison * allows the normalization procedure to fail The Ghidra lifter generates code that is either invalid or our interpretation of it is not valid, e.g., `int3` instructioin on x86 is lifted as ``` CALL x; RETURN y; ``` where according to the documentation both CALL and RETURN should be treated initially as indirect jumps * renames the `system` feature in Lisp context to the target-system to prevent clashing with the Primus Lisp systems * adds the Lisp.Semantics.context to control the Lisp definitions * disables x86 FP intrinsic semantics when the legacy lifter is used Otherwise, they both try to provide semantics that is conflicting. * adds the --x86-disable-floating-point-intrinsics as an escape hatch This option makes it possible to still use the old BIL plugin feature that translates unknown (to the BIL lifters) instructions into intrinsic calls. * updates the testsuite revision
BinaryAnalysisPlatform · Apr 15, 2022 · a360700 · a360700
1 parent 1e9dc7d
commit a360700
Show file tree

Hide file tree

Showing 27 changed files with 555 additions and 75 deletions.
diff --git a/Makefile b/Makefile
@@ -55,7 +55,7 @@ testsuite:
 	git clone https://github.com/BinaryAnalysisPlatform/bap-testsuite.git testsuite
 
 check: testsuite
-	make REVISION=44771dd -C testsuite
+	make REVISION=044dabe -C testsuite
 
 .PHONY: indent check-style status-clean
 

diff --git a/lib/bap/bap.mli b/lib/bap/bap.mli
@@ -8741,6 +8741,12 @@ module Std : sig
     (** a subroutine is the binary entry point *)
     val entry_point : unit tag
 
+    (** a subroutine is an intrinisic or special instruction
+        not a real subroutine.
+
+        @since 2.5.0 *)
+    val intrinsic : unit tag
+
     (** Subroutine builder *)
     module Builder : sig
       type t

diff --git a/lib/bap_c/bap_c_abi.ml b/lib/bap_c/bap_c_abi.ml
@@ -109,6 +109,7 @@ let registry = Hashtbl.create (module String)
 let register name abi = Hashtbl.set registry ~key:name ~data:abi
 let get_processor name = Hashtbl.find registry name
 
+
 let get_prototype gamma name = match gamma name with
   | Some (`Function proto) -> proto
   | _ ->
@@ -141,12 +142,15 @@ let create_api_processor size abi : Bap_api.t =
       else self#apply_proto sub
 
     method private apply_proto sub =
-      let name = Sub.name sub in
-      let {Bap_c_type.Spec.t; attrs} = get_prototype gamma name in
-      let sub = self#apply_args sub attrs t in
-      let sub = Term.set_attr sub Attrs.proto t in
-      let sub = List.fold_right ~init:sub attrs ~f:Bap_c_attr.apply in
-      abi.apply_attrs attrs sub
+      if Term.has_attr sub Sub.intrinsic
+      then sub
+      else
+        let name = Sub.name sub in
+        let {Bap_c_type.Spec.t; attrs} = get_prototype gamma name in
+        let sub = self#apply_args sub attrs t in
+        let sub = Term.set_attr sub Attrs.proto t in
+        let sub = List.fold_right ~init:sub attrs ~f:Bap_c_attr.apply in
+        abi.apply_attrs attrs sub
 
 
     method private apply_args sub attrs t =

diff --git a/lib/bap_primus/bap_primus.mli b/lib/bap_primus/bap_primus.mli
@@ -3298,7 +3298,7 @@ module Std : sig
         syntactic level, the syntax of Primus Lisp itself is
         context-dependent.
 
-        {3 Context}
+        {3:context Context}
 
         A context (from the perspective of the type system) is a set
         of type class instances. The context is fixed when a program
@@ -3622,6 +3622,14 @@ text ::= ?any atom that is not recognized as a <word>?
       (** an abstract type representing a lisp program  *)
       type program
 
+      (** the set of type classes that constrain the context of
+          applicability of Primus Lisp definitions.
+
+          @see {{!context}the context section for more information}.
+          @since 2.5.0
+      *)
+      type context
+
 
       (** an abstract type that represents messages send with the
           [msg] form. *)
@@ -3658,6 +3666,29 @@ text ::= ?any atom that is not recognized as a <word>?
         val pp_program : Format.formatter -> program -> unit
       end
 
+
+      (** The set of constraints.
+
+          See {{!context} the context section for more information}.
+
+          Note, the context is automatically generated from the
+          project, when a Primus Lisp program is loaded. But it is
+          also possible to refine it using the unit's
+          {!Lisp.Semantics.context} slot.
+
+          @since 2.5.0
+      *)
+      module Context : sig
+        type t = context
+
+
+        (** [create [c1, f1;...; cN, fN]] creates the context.
+
+            The created context will have classes [c1,...,cN] defined
+            with feature sets [f1,...,fN] correspondingly. *)
+        val create : (string * string list) list -> context
+      end
+
       module Doc : sig
 
         (** Abstract Element of a document.
@@ -3913,6 +3944,20 @@ text ::= ?any atom that is not recognized as a <word>?
         val program : (Theory.Source.cls, program) KB.slot
 
 
+        (** Primus Lisp definitions constraints.
+
+            The set of type classes that describe the unit constraints
+            and limits applicability of Primus Lisp definitions to the
+            selected compilation unit.
+
+            Each Primus Lisp definition has a {!context} class of its
+            applicability. The definition will only be used if its
+            context is a subtype of the unit context.
+
+            @since 2.5.0  *)
+        val context : (Theory.Unit.cls, context) KB.slot
+
+
         (** The Primus Lisp definition to which the program belongs.
 
             This property stores the label to the original program for

diff --git a/lib/bap_primus/bap_primus_lisp.ml b/lib/bap_primus/bap_primus_lisp.ml
@@ -468,6 +468,7 @@ module type Primitives = Lisp.Def.Primitives
 module Primitive = Lisp.Def.Primitive
 type closure = Lisp.Def.closure
 type program = Lisp.Program.t
+type context = Lisp.Context.t
 module Load = Bap_primus_lisp_parse
 module Type = struct
   include Lisp.Program.Type
@@ -931,3 +932,4 @@ end
 
 module Unit = Semantics.Unit
 module Attribute = Lisp.Attribute
+module Context = Lisp.Context
diff --git a/lib/bap_primus/bap_primus_lisp.mli b/lib/bap_primus/bap_primus_lisp.mli
@@ -5,6 +5,7 @@ open Bap_primus_types
 open Bap_core_theory
 
 type program
+type context
 type message
 
 
@@ -15,6 +16,11 @@ module Load : sig
   val pp_error : formatter -> error -> unit
 end
 
+module Context : sig
+  type t = context
+  val create : (string * string list) list -> context
+end
+
 module Doc : sig
   module type Element = sig
     type t
@@ -152,6 +158,7 @@ module Semantics : sig
   type KB.conflict += Failed_primitive of KB.Name.t * string
 
   val program : (Theory.Source.cls, program) KB.slot
+  val context : (Theory.Unit.cls, context) KB.slot
   val definition : (Theory.program, Theory.Label.t option) KB.slot
   val name : (Theory.program, KB.Name.t option) KB.slot
   val args : (Theory.program, unit Theory.Value.t list option) KB.slot

diff --git a/lib/bap_primus/bap_primus_lisp_context.ml b/lib/bap_primus/bap_primus_lisp_context.ml
@@ -9,7 +9,7 @@ module Attribute = Bap_primus_lisp_attribute
 module Feature = String
 module Name = String
 
-type t = Feature.Set.t Name.Map.t [@@deriving compare, equal, sexp]
+type t = Feature.Set.t Name.Map.t [@@deriving bin_io, compare, equal, sexp]
 let empty = Name.Map.empty
 
 type Attribute.error += Unterminated_quote
@@ -60,7 +60,7 @@ let of_project proj =
     features [sprintf "%d" (Theory.Target.data_addr_size t)];
     "code-addr-size",
     features [sprintf "%d" (Theory.Target.code_addr_size t)];
-    "system", features [
+    "target-system", features [
       Theory.System.to_string @@ Theory.Target.system t
     ];
 
@@ -169,8 +169,17 @@ let join xs ys = Ok (merge xs ys)
 
 let domain = KB.Domain.define "context"
     ~empty ~order ~join
+    ~inspect:sexp_of
 
 let t = Attribute.declare "context"
     ~package:"core"
     ~domain
     ~parse
+
+let slot =
+  KB.Class.property Theory.Unit.cls "primus-lisp-context"
+    ~public:true
+    ~persistent:(KB.Persistent.of_binable (module struct
+                   type nonrec t = t [@@deriving bin_io]
+                 end))
+    ~package:"bap" domain
diff --git a/lib/bap_primus/bap_primus_lisp_context.mli b/lib/bap_primus/bap_primus_lisp_context.mli
@@ -240,7 +240,7 @@ open Bap.Std
 
 module Attribute = Bap_primus_lisp_attribute
 
-type t
+type t [@@deriving bin_io]
 
 val t : t Attribute.t
 
@@ -257,3 +257,4 @@ val (<=) : t -> t -> bool
 val pp : Format.formatter -> t -> unit
 
 val merge : t -> t -> t
+val slot : (Theory.Unit.cls, t) KB.slot
diff --git a/lib/bap_primus/bap_primus_lisp_semantics.ml b/lib/bap_primus/bap_primus_lisp_semantics.ml
@@ -8,6 +8,7 @@ open Bap_primus_lisp_attributes
 
 module Attribute = Bap_primus_lisp_attribute
 module Program = Bap_primus_lisp_program
+module Context = Bap_primus_lisp_context
 module Source = Bap_primus_lisp_source
 module Resolve = Bap_primus_lisp_resolve
 module Def = Bap_primus_lisp_def
@@ -59,6 +60,8 @@ let program =
     ~equal:Program.equal
     ~join:(fun x y -> Ok (Program.merge x y))
 
+let context = Context.slot
+
 
 type kind = Prim | Defn | Meth | Data [@@deriving sexp]
 
@@ -728,8 +731,11 @@ let link_library target prog =
 
 let collect_names kind key prog =
   Program.fold prog key ~f:(fun ~package def names ->
-      let name = Def.name def in
-      Map.set names (KB.Name.create ~package name) kind)
+      if Program.is_applicable prog def
+      then
+        let name = Def.name def in
+        Map.set names (KB.Name.create ~package name) kind
+      else names)
     ~init:(Map.empty (module KB.Name))
 
 let merge_names names =
@@ -747,9 +753,13 @@ let obtain_typed_program unit =
   match KB.Value.get typed src with
   | Some prog -> !!prog
   | None ->
+    let* context = unit-->context in
+    let input =
+      let init = KB.Value.get program src in
+      Program.with_context init @@
+      Context.merge (Program.context init) context in
     let* prog =
-      link_library target @@
-      Program.with_places (KB.Value.get program src) target in
+      link_library target @@ Program.with_places input target in
     let tprog = Program.Type.infer prog in
     let prog = Program.Type.program tprog in
     let places = Program.fold prog Key.place

diff --git a/lib/bap_primus/bap_primus_lisp_semantics.mli b/lib/bap_primus/bap_primus_lisp_semantics.mli
@@ -1,3 +1,4 @@
+open Core_kernel
 open Bap_core_theory
 open Bap.Std
 open Bap_primus_lisp_types
@@ -9,6 +10,7 @@ type KB.conflict += Illtyped_program of Type.error list
 type KB.conflict += Failed_primitive of KB.Name.t * string
 
 val program : (Theory.Source.cls, program) KB.slot
+val context : (Theory.Unit.cls, Bap_primus_lisp_context.t) KB.slot
 val definition : (Theory.program, Theory.Label.t option) KB.slot
 val name : (Theory.program, KB.Name.t option) KB.slot
 val args : (Theory.program, unit Theory.Value.t list option) KB.slot

diff --git a/lib/bap_sema/bap_sema_lift.ml b/lib/bap_sema/bap_sema_lift.ml
@@ -331,6 +331,19 @@ let link_call symtab addr sub_of_blk jmp =
           jmp ~dst ~alt:(Some alt))
       | None -> jmp
 
+let is_intrinsic sub =
+  match KB.Name.package @@ KB.Name.read (Ir_sub.name sub) with
+  | "intrinsic" | "special" -> true
+  | _ -> false
+
+let create_synthetic tid =
+  let sub = Ir_sub.create ~tid () in
+  let tags = List.filter_opt [
+      Some Term.synthetic;
+      Option.some_if (is_intrinsic sub) Ir_sub.intrinsic;
+    ] in
+  List.fold tags ~init:sub ~f:(fun sub tag ->
+      Term.set_attr sub tag ())
 
 let insert_synthetic prog =
   Term.enum sub_t prog |>
@@ -348,7 +361,7 @@ let insert_synthetic prog =
                   then prog
                   else
                     Term.append sub_t prog @@
-                    Ir_sub.create ~tid:dst ())))
+                    create_synthetic dst)))
 
 
 let program symtab =

diff --git a/lib/bap_types/bap_ir.ml b/lib/bap_types/bap_ir.ml
@@ -1846,6 +1846,13 @@ module Ir_sub = struct
       ~name:"entry-point"
       ~uuid:"d1eaff96-4ed4-4405-9305-63508440ccc1"
 
+  let intrinsic = Bap_value.Tag.register (module Unit)
+      ~package
+      ~public:true
+      ~desc:"the subroutine is an intrinsic or special instruction"
+      ~name:"intrinsic"
+      ~uuid:"68be4fa5-f8f4-4219-b89c-42718c59f09b"
+
   module Builder = struct
     type t =
       tid option * arg term vector * blk term vector * string option

diff --git a/lib/bap_types/bap_ir.mli b/lib/bap_types/bap_ir.mli
@@ -231,6 +231,7 @@ module Ir_sub : sig
   val returns_twice : unit tag
   val nothrow : unit tag
   val entry_point : unit tag
+  val intrinsic : unit tag
   val pp_slots : string list -> Format.formatter -> t -> unit
   include Regular.S with type t := t
 end

diff --git a/lib/x86_cpu/x86_target.ml b/lib/x86_cpu/x86_target.ml
@@ -190,6 +190,7 @@ module M64 = struct
   let mmx = M32.mmx
   let xmmx = array r128 "XMM" 16
   let ymmx = array r256 "YMM" 16
+  let mxsr = reg r32 "MXCSR"
 
   let flags = M32.flags
   let mems = Theory.Mem.define r64 r8
@@ -198,7 +199,7 @@ module M64 = struct
   let aliases = M32.aliases @< M32.main @< M32.index @< xmmx
 
   let vars = main @< index @< segment @< rx @< stx @< mmx @< ymmx @<
-             flags @< [data]
+             flags @< [data] @< [mxsr]
 
   let regs =  Theory.Role.Register.[
       [general; integer], main @< index @< segment @< rx;
@@ -207,6 +208,7 @@ module M64 = struct
       [frame_pointer], untyped [reg r64 "RBP"];
       [Role.index], untyped index;
       [Role.segment], untyped segment;
+      [status], untyped [mxsr];
       [alias], aliases;
     ] @ M16.status_regs
 

diff --git a/oasis/x86 b/oasis/x86
@@ -24,7 +24,7 @@ Library x86_plugin
  Path:             plugins/x86
  FindlibName:      bap-plugin-x86
  BuildDepends:     bap, bap-abi, bap-c, bap-x86-cpu, bap-llvm, core_kernel,
-                   ppx_bap, bap-main, bap-future, bap-api, ogre,
+                   ppx_bap, bap-main, bap-future, bap-api, ogre, bap-primus,
                    zarith, bap-core-theory, bap-knowledge, bitvec, str
  Modules:          X86_backend, X86_prefix
  InternalModules:  X86_abi,