adds semantics and supporting code for several x86 instructions

Adds the following instructions:
 - shufps
 - pmuldq
 - [v]packusdw
 - [v]packuswb
 - [v]packssdw
 - [v]packsswb
 - vzeroupper
 - movntd
 - xchgb

The generated code for signed and unsigned saturation (the pack*
family of instructions) is thoroughly optimized to minimize branching
and comparison, which negatively affects analysis performance. Both
signed and unsigned saturation are implemented as a lisp primitive
that generates pure code with a single ite instruction and any
comparisons are made with zero, i.e., no inequalities.

To following extra changes support the added instructions:

1) [NEW] Extend x86 CPU family definition with 8-bit registers, e.g.,
   AL,BL,CL,DL,AH,BH,CH,DH,SIL,DIL,BPL, and SPL.
2) [NEW] Added EFLAGS and RFLAGS aliases to the set of flag registers.
3) [NEW] It is now possible to use bool registers in the aliasing
   specifications.
4) [NEW] Added system and control register flags.
5) [FIX] Fixed a bug with incorrect reification of higher parts of
   aliased registers.
6) [NEW] Added a `dolist` macro to Primus Lisp.
7) [NEW] Added the `unquote` primitive to Primus Lisp.
8) [NEW] Added the `cast-saturate` primitive to Primus Lisp.
9) [NEW] Improved BIL code generation in case of empty if statements.

Author: ivg

.github/workflows/full.yml

@@ -32,8 +32,20 @@ jobs:
           dune-cache: true
           opam-disable-sandboxing: true
 
+      - name: Install BAP Dependencies
+        run: opam install . --deps-only
+
+      - name: Configure BAP
+        run: opam exec -- ocaml tools/configure.ml --with-llvm-config=$(opam var conf-bap-llvm:config)
+
+      - name: Build BAP
+        run: opam exec -- dune build
+
       - name: Install BAP
-        run: opam install . --with-test
+        run: opam exec -- dune install
+
+      - name: Run Unit Tests
+        run: opam exec -- dune test --display=short
 
       - name: Run Functional Tests
         run: opam exec -- make check

.github/workflows/main.yml

@@ -9,17 +9,13 @@ jobs:
       matrix:
         os:
           - ubuntu-20.04
-          - macos-11
         ocaml-compiler:
           - 4.08.x
           - 4.14.x
-        exclude:
-          - os: macos-11
-            ocaml-compiler: 4.08.x
 
 
     runs-on: ${{ matrix.os }}
-    continue-on-error: ${{ matrix.os == 'macos-11'}}
+    continue-on-error: ${{ matrix.os == 'macos-latest'}}
 
     env:
       TMPDIR: /tmp
@@ -39,16 +35,16 @@ jobs:
           sudo apt-get install dejagnu -y
 
       - name: Prepare macOS
-        if: matrix.os == 'macos-11'
+        if: matrix.os == 'macos-latest'
         run: |
           echo 'LLVM_CONFIG=/usr/local/opt/llvm@9/bin/llvm-config' >> $GITHUB_ENV
-          brew install deja-gnu
+          brew install deja-gnu zstd
 
       - name: Install OCaml
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          dune-cache: ${{  matrix.os != 'macos-11' }}
+          dune-cache: ${{  matrix.os != 'macos-latest' }}
           opam-disable-sandboxing: true
           opam-local-packages: |
             *.opam
@@ -62,7 +58,7 @@ jobs:
             bap: git+https://github.com/BinaryAnalysisPlatform/opam-repository#testing
 
       - name: Build BAP
-        run: opam install bap.dev --with-test
+        run: opam install bap.dev
 
       - name: Run MC Functional Tests
         run: |

.github/workflows/nightly.yml

@@ -35,7 +35,7 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          dune-cache: ${{  matrix.os != 'macos-11' }}
+          dune-cache: ${{  matrix.os != 'macos-latest' }}
           opam-pin: false
           opam-disable-sandboxing: true
           opam-repositories: |

.github/workflows/oasis.yml

@@ -9,17 +9,12 @@ jobs:
       matrix:
         os:
           - ubuntu-20.04
-          - macos-11
         ocaml-compiler:
-          - 4.08.x
           - 4.14.x
-        exclude:
-          - os: macos-11
-            ocaml-compiler: 4.08.x
 
 
     runs-on: ${{ matrix.os }}
-    continue-on-error: ${{ matrix.os == 'macos-11'}}
+    continue-on-error: ${{ matrix.os == 'macos-latest'}}
 
     env:
       TMPDIR: /tmp
@@ -39,7 +34,7 @@ jobs:
           sudo apt-get install dejagnu -y
 
       - name: Prepare macOS
-        if: matrix.os == 'macos-11'
+        if: matrix.os == 'macos-latest'
         run: |
           echo 'LLVM_CONFIG=/usr/local/opt/llvm@9/bin/llvm-config' >> $GITHUB_ENV
           brew install deja-gnu
@@ -48,17 +43,22 @@ jobs:
         uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          dune-cache: ${{  matrix.os != 'macos-11' }}
+          dune-cache: ${{  matrix.os != 'macos-latest' }}
           opam-disable-sandboxing: true
           opam-repositories: |
             default: git+https://github.com/ocaml/opam-repository.git
             bap: git+https://github.com/BinaryAnalysisPlatform/opam-repository#testing
+          opam-local-packages: |
+            *.opam
+            !ppx_bap.opam
+            !bap-ghidra.opam
+            !bap-primus-symbolic-executor.opam
 
       - name: Install OPAM dependencies
         run: opam install . --deps-only
 
       - name: Install dependencies requires for the OASIS build
-        run: opam install oasis ppx_bap conf-bap-llvm conf-binutils
+        run: opam install oasis ppx_bap.master conf-bap-llvm conf-binutils
 
       - name: Configure BAP
         run: >-

dune

@@ -39,7 +39,9 @@
    ppx_optcomp
    ppx_sexp_conv
    ppx_sexp_value
-   ppx_variants_conv)
+   ppx_variants_conv
+   ppx_expect
+   ppx_inline_test)
  (preprocess no_preprocessing))
 
 (alias

dune-project

@@ -1,4 +1,5 @@
 (lang dune 3.1)
+(cram enable)
 (using dune_site 0.1)
 
 (name bap)
@@ -1607,6 +1608,8 @@ and updating documents")
   (ppx_here (and (>= v0.14) (< v0.16)))
   (ppxlib (>= 0.15.0))
   (ppx_optcomp (and (>= v0.14) (< v0.16)))
+  (ppx_expect (and (>= v0.14) (< v0.16)))
+  (ppx_inline_test (and (>= v0.14) (< v0.16)))
   (ppx_sexp_conv (and (>= v0.14) (< v0.16)))
   (ppx_sexp_value (and (>= v0.14) (< v0.16)))
   (ppx_variants_conv (and (>= v0.14) (< v0.16)))))

lib/bap_core_theory/bap_core_theory.mli

@@ -2140,6 +2140,10 @@ module Theory : sig
     (** [reg x] defines [x] as a part.   *)
     val reg : 'a Bitv.t Var.t -> 'a part
 
+    (** [bit x] defines a boolean register [x] as a part.
+        @since 2.5.0 *)
+    val bit : Bool.t Var.t -> Bool.t part
+
     (** [unk] defines an unnamed part of the register.   *)
     val unk : 'a part
   end
@@ -2156,13 +2160,16 @@ module Theory : sig
       origin register(s) and ['k] denotes the kind of relationship
       between the alias and its origin.
 
-      Currently, we recognize two kinds of relationships. The [sub]
+      Currently, we recognize three kinds of relationships. The [sub]
       kind defines the alias as a subset of the origin register, i.e.,
       a contiguous sequnce of bits that are fully enclosed in the
       origin register. The [sup] kind defines an alias as a superset
       of a number of origin registers, i.e., it is a contiguous
       sequence of bits formed as a concatenation of the origin
-      registers.
+      registers. Finally, the [set] register defines an alias as
+      superset of a numbero of origin register, where each origin
+      register is a boolean flag, i.e., an alias is a contiguous
+      sequence of one-bit flags.
 
       More kinds of relationships could be added later.
 
@@ -2193,12 +2200,17 @@ module Theory : sig
     (** the type index for the super-registers  *)
     type sup
 
+    (** the type index for a set of bits registers *)
+    type set
+
     (** [cast_sub origin] recovers the kind of the origin.  *)
     val cast_sub : ('a,unit) t -> ('a,sub) t option
 
     (** [cast_sup origin] recovers the kind of the origin.  *)
     val cast_sup : ('a,unit) t -> ('a,sup) t option
 
+    (** [cast_set origin] recovers the kind of the origin.  *)
+    val cast_set : ('a,unit) t -> (Bool.t,set) t option
 
     (** [reg origin] is the base register.
 
@@ -2218,7 +2230,7 @@ module Theory : sig
         register. *)
     val hi : ('a,sub) t -> int
 
-    (** [lo origin] returns the inclusive upper bound of the origin register
+    (** [lo origin] returns the inclusive lowe bound of the origin register
         to which an alias belongs. *)
     val lo : ('a,sub) t -> int
 
@@ -2229,10 +2241,21 @@ module Theory : sig
         first element of the list corresponds to the most significant
         part of the base register. This is the same order, in which
         the aliasing was specified, e.g., if the aliasing was defined
-        as, [def x [reg hix; reg lox], then [regs] will
+        as, [def x [reg hix; reg lox]], then [regs] will
         return [hix; lox].*)
     val regs : ('a,sup) t -> 'a Bitv.t Var.t list
 
+
+    (** [bits origin] an list of flags that comprise the register.
+        The bits are sorted in the big endian order, i.e., the first
+        element of the list is the most significant part of the
+        alias. This is the same order, in which the aliasing was
+        specified, e.g., if the aliasing was defined as,
+        [def status [bit cf; bit zf]], then [regs] will return [cf; zf].
+
+        @since 2.5.0 *)
+    val bits : (Bool.t,set) t -> Bool.t Var.t list
+
   end
 
   (** A target-specific role of program entities.
@@ -2305,7 +2328,7 @@ module Theory : sig
       (** the register is used by the integer arithmetic unit
 
           This role can be assigned both to general and special
-          purpose registers. E.g., to get integer arithemtic status
+          purpose registers. E.g., to get integer arithmetic status
           control registers use [[special; integer]].  *)
       val integer : t
 
@@ -2347,10 +2370,20 @@ module Theory : sig
       (** the constant register that always holds zero.  *)
       val zero : t
 
+      (** the constant register that always holds one.
+          @since 2.5.0 *)
+      val one : t
 
-      (** the program status register  *)
+      (** the program status register.  *)
       val status : t
 
+      (** a register for controlling operating system.  *)
+      val system : t
+
+      (** a register that controls CPU or other device.
+          @since 2.5.0 *)
+      val control : t
+
       (** the zero flag register
 
           Is set when an arithmetic operation results in zero.*)

lib/bap_core_theory/bap_core_theory_pass.ml

@@ -88,7 +88,6 @@ module Desugar(CT : Core) : Core = struct
 
     let pass = Effect.empty Effect.Sort.bot
 
-
     let take what bits x =
       what (Val.Bitv.define bits) (CT.var x)
 
@@ -112,24 +111,24 @@ module Desugar(CT : Core) : Core = struct
       let module Pos = Bitvec.M32 in
       CT.int (Val.Bitv.define 32) (Pos.int x)
 
-    let assign_regs lhs rhs =
+    let assign_multi size cast lhs rhs =
       rhs >>= fun rhs ->
       let total = Val.(Bitv.size (sort rhs)) in
-      fst@@List.fold lhs ~init:(!!pass,total+1) ~f:(fun (data,hi) lhs ->
+      fst@@List.fold lhs ~init:(!!pass,total+1) ~f: (fun (data,hi) lhs ->
           let s = Var.sort lhs in
-          let bits = Val.Bitv.size s in
+          let bits = size s in
           let lo = hi - bits in
-          let rhs = CT.extract s (pos hi) (pos lo) !!rhs in
+          let s' = Val.Bitv.define bits in
+          let rhs = cast (CT.extract s' (pos hi) (pos lo) !!rhs) in
           CT.(seq data (set lhs rhs),hi - bits))
 
+    let assign_regs lhs rhs = assign_multi Val.Bitv.size Fn.id lhs rhs
+    let assign_bits lhs rhs =
+      assign_multi (Fn.const 1) CT.(fun v ->ite (is_zero v) b0 b1) lhs rhs
 
     (* module Alias ensures that only bitvec registers
        are involved in aliasing *)
-    let cast_var v =
-      match Val.Bitv.refine @@ Val.Sort.forget @@ Var.sort v with
-      | None -> assert false
-      | Some s -> Var.resort v s
-    and cast_val v = v >>| fun v ->
+    let cast_val v = v >>| fun v ->
       match Val.resort Val.Bitv.refine (Val.forget v) with
       | None -> assert false
       | Some v -> v
@@ -150,22 +149,35 @@ module Desugar(CT : Core) : Core = struct
               CT.set (Origin.reg s) x
             | Some s -> assign_sub (Origin.reg s) x (Origin.lo s)
             | None -> match Origin.cast_sup origin with
-              | None -> !!pass
               | Some s -> assign_regs (Origin.regs s) x
+              | None -> match Origin.cast_set origin with
+                | Some s -> assign_bits (Origin.bits s) x
+                | None -> !!pass
+
 
-    let var r =
+    let const role value ret t r s =
+      if Target.has_roles t [role] r
+      then match Val.Bitv.refine (Val.Sort.forget s) with
+        | None -> Some (CT.unk s)
+        | Some s' -> Some (ret@@CT.int s' value)
+      else None
+
+    let consts = [
+      Target.Role.Register.zero, Bitvec.zero;
+      Target.Role.Register.one, Bitvec.one;
+    ]
+
+    let var (type a) r  =
       Scope.mem r >>= function
       | true -> CT.var r
       | false ->
         let* t = target in
         let s = Var.sort r in
         let ret x = x >>| fun x -> KB.Value.refine x s in
-        if Target.has_roles t [Target.Role.Register.zero] r
-        then match Val.Bitv.refine (Val.Sort.forget s) with
-          | None -> CT.unk s
-          | Some s' ->
-            ret@@CT.int s' Bitvec.zero
-        else
+        List.find_map consts ~f:(fun (role,value) ->
+            const role value ret t r s) |> function
+        | Some v -> v
+        | None ->
           match Target.unalias t r with
           | None -> CT.var r
           | Some origin ->
@@ -178,13 +190,25 @@ module Desugar(CT : Core) : Core = struct
               ret @@
               CT.extract bs (pos hi) (pos lo) (CT.var (Origin.reg sub))
             | None -> match Origin.cast_sup origin with
-              | None -> CT.unk s
               | Some sup ->
                 let regs = Origin.regs sup in
                 let total = List.sum (module Int) regs ~f:(fun r ->
                     Val.Bitv.size (Var.sort r)) in
                 let bs = Val.Bitv.define total in
                 ret @@ CT.concat bs (List.map regs ~f:CT.var)
+              | None ->
+                match Origin.cast_set origin with
+                | Some set ->
+                  let bits = Origin.bits set in
+                  let n = List.length bits in
+                  let bs = Val.Bitv.define n in
+                  let us = Val.Bitv.define 1 in
+                  let m0 = CT.int us Bitvec.zero
+                  and m1 = CT.int us Bitvec.one in
+                  ret @@ CT.concat bs (List.map bits ~f:(fun v ->
+                      CT.(ite (var v) m1 m0)))
+                | none -> CT.unk s
+
 
     let let_ v x y =
       x >>= fun x ->