Legacy floating point lifter

Makefile

@@ -55,7 +55,7 @@ testsuite:
 	git clone https://github.com/BinaryAnalysisPlatform/bap-testsuite.git testsuite
 
 check: testsuite
-	make REVISION=7f51548cc3e -C testsuite
+	make REVISION=3eb55ac2b5085445 -C testsuite
 
 .PHONY: indent check-style status-clean
 

lib/bap_types/bap_helpers.ml

@@ -91,9 +91,7 @@ class substitution x y = object(self)
   method! map_let z ~exp ~body =
     if Bap_var.(z = x)
     then Let (z,self#map_exp exp,body)
-    else super#map_let z
-        ~exp:(self#map_exp exp)
-        ~body:(self#map_exp body)
+    else super#map_let z ~exp ~body
   method! map_var z =
     match super#map_var z with
     | Exp.Var z when Bap_var.(z = x) -> y

oasis/x86

@@ -24,7 +24,8 @@ 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,
+                   zarith, bap-core-theory, bap-knowledge, bitvec
  Modules:          X86_backend, X86_prefix
  InternalModules:  X86_abi,
                    X86_btx,
@@ -57,7 +58,23 @@ Library x86_plugin
                    X86_tools_reg,
                    X86_tools_types,
                    X86_tools_vector,
-                   X86_utils
+                   X86_utils,
+                   X86_legacy_bil,
+                   X86_legacy_bil_ast,
+                   X86_legacy_bil_type,
+                   X86_legacy_bil_var,
+                   X86_legacy_bil_lifter,
+                   X86_legacy_bil_semantics,
+                   X86_legacy_bil_pp,
+                   X86_legacy_bil_arithmetic,
+                   X86_legacy_bil_big_int_convenience,
+                   X86_legacy_bil_convenience,
+                   X86_legacy_bil_disasm_i386,
+                   X86_legacy_bil_typecheck,
+                   X86_legacy_bil_var_temp,
+                   X86_legacy_fp_lifter,
+                   X86_legacy_bil_register,
+                   X86_legacy_operands
  XMETAExtraLines:  tags="disassembler, lifter, x86, abi"
 
 Library x86_test

plugins/bil/bil_main.ml

@@ -169,16 +169,16 @@ let () =
       ~package:"bap" ~name:"bil"
       ~desc:"semantics in BIL"
       ~provides:["bil"; "lifter"];
-
-    Theory.declare !!(module Bil_semantics.Core_with_fp_emulation : Theory.Core)
-      ~package:"bap" ~name:"bil-fp-emu"
-      ~extends:["bap:bil"]
-      ~desc: "semantics in BIL, including FP emulation"
-      ~context:["floating-point"]
-      ~provides:[
-        "bil";
-        "floating-point";
-        "lifter";
-      ];
+    if Syntax.(ctxt-->enable_fp_emu)
+    then Theory.declare !!(module Bil_semantics.Core_with_fp_emulation : Theory.Core)
+        ~package:"bap" ~name:"bil-fp-emu"
+        ~extends:["bap:bil"]
+        ~desc: "semantics in BIL, including FP emulation"
+        ~context:["floating-point"]
+        ~provides:[
+          "bil";
+          "floating-point";
+          "lifter";
+        ];
     Ok ()
   end

plugins/x86/.merlin

@@ -1,3 +1,4 @@
+PKG zarith
 B ../../_build/plugins/x86
 B ../../_build/lib/bap_abi
 B ../../_build/lib/bap_api

plugins/x86/x86_legacy_bil.ml

@@ -0,0 +1,3 @@
+module Ast = X86_legacy_bil_ast
+module Type = X86_legacy_bil_type
+module Var = X86_legacy_bil_var

plugins/x86/x86_legacy_bil_arithmetic.ml

@@ -0,0 +1,159 @@
+(* Copyright (C) 2017 ForAllSecure, Inc. - All Rights Reserved. *)
+(** Basic integer arithmetic on N-bit integers
+
+    These are common operations which are needed for constant folding or
+    evaluation.
+
+    @author Ivan Jager
+*)
+
+module Bil = X86_legacy_bil
+
+open Big_int_Z
+open X86_legacy_bil_big_int_convenience
+open Bil.Type
+
+
+
+exception ArithmeticEx of string
+
+let memoize ?(size = 128) f =
+  let results = Hashtbl.create size in
+  fun x ->
+    try Hashtbl.find results x
+    with Not_found ->
+      let y = f x in
+      Hashtbl.add results x y;
+      y
+
+let power_of_two = memoize (shift_left_big_int bi1)
+let bitmask = memoize (fun i -> power_of_two i -% bi1)
+
+let bits_of_width = function
+  | Reg n -> n
+  | Float float_size -> float_size.exp_bits + float_size.sig_bits
+  | _ -> failwith "Expected register type"
+
+(* drop high bits to type t *)
+let to_big_int (i,t) =
+  let bits = bits_of_width t in
+  and_big_int i (bitmask bits)
+
+(* sign extend to type t *)
+let to_sbig_int (i,t) =
+  let bits = bits_of_width t in
+  let final = to_big_int (i, Reg(bits-1)) in
+  (* mod always returns a positive number *)
+  let sign = i >>% (bits-1) in
+  if bi_is_zero sign then (* positive *) final else (* negative *) minus_big_int ((power_of_two (bits-1) -% final))
+
+let t_div dividend divisor =
+  Z.div dividend divisor
+
+let t_mod dividend divisor =
+  Z.rem dividend divisor
+
+(* shifting by more than the number of bits or by negative values will
+ * be the same as shifting by the max number of bits. *)
+let toshift shiftedt v =
+  let max = bits_of_width shiftedt
+  and i = to_big_int v in
+  assert (i >=% bi0);
+  let max_bi = (big_int_of_int max) in
+  if i <=% max_bi then
+    int_of_big_int i
+  else
+    let error_str = Caml.Printf.sprintf "shifting %d-bit value by %s" max (string_of_big_int i) in
+    let () = failwith error_str
+    in max
+
+(* "cast" an int64 to a value *)
+let to_val t i =
+  (to_big_int (i,t), t)
+
+let exp_bool =
+  let t = (unit_big_int, Reg(1))
+  and f = (zero_big_int, Reg(1)) in
+  (fun b -> if b then t else f)
+
+(** [binop operand lhs lhst rhs rhst] *)
+let binop op ((_,t) as v1) v2 =
+  match op with
+  | PLUS -> to_val t (add_big_int (to_big_int v1) (to_big_int v2))
+  | MINUS -> to_val t (sub_big_int (to_big_int v1) (to_big_int v2))
+  | TIMES -> to_val t (mult_big_int (to_big_int v1) (to_big_int v2))
+  | AND -> to_val t (and_big_int (to_big_int v1) (to_big_int v2))
+  | OR -> to_val t (or_big_int (to_big_int v1) (to_big_int v2))
+  | XOR -> to_val t (xor_big_int (to_big_int v1) (to_big_int v2))
+  | EQ -> exp_bool(eq_big_int (to_big_int v1) (to_big_int v2))
+  | NEQ -> exp_bool(not (eq_big_int (to_big_int v1) (to_big_int v2)))
+  | LSHIFT -> to_val t (shift_left_big_int (to_big_int v1) (toshift t v2))
+  | RSHIFT -> to_val t (shift_right_big_int (to_big_int v1) (toshift t v2))
+  | ARSHIFT -> to_val t (shift_right_big_int (to_sbig_int v1) (toshift t v2))
+  | DIVIDE -> to_val t (div_big_int (to_big_int v1) (to_big_int v2))
+  | SDIVIDE -> to_val t (t_div (to_sbig_int v1) (to_sbig_int v2))
+  | MOD -> to_val t (mod_big_int (to_big_int v1) (to_big_int v2))
+  | SMOD -> to_val t (t_mod (to_sbig_int v1) (to_sbig_int v2))
+  | SLT -> exp_bool(lt_big_int (to_sbig_int v1) (to_sbig_int v2))
+  | SLE -> exp_bool(le_big_int (to_sbig_int v1) (to_sbig_int v2))
+  | LT -> exp_bool(lt_big_int (to_big_int v1) (to_big_int v2))
+  | LE -> exp_bool(le_big_int (to_big_int v1) (to_big_int v2))
+  | FP _ -> failwith "Concrete arithmetic on floating point is not allowed"
+
+
+let unop op ((_,t) as v) =
+  match op with
+  | NEG -> to_val t (minus_big_int (to_big_int v))
+  | NOT -> (* implemented as xor with -1 *)
+    to_val t (xor_big_int (to_big_int (bim1,t)) (to_big_int v))
+
+  | FP _ -> failwith "Concrete arithmetic on floating point is not allowed"
+
+let cast ct ((_,t) as v) t2 =
+  let bits1 = bits_of_width t
+  and bits = bits_of_width t2 in
+  (match ct with
+   | CAST_UNSIGNED ->
+     to_val t2 (to_big_int v)
+   | CAST_SIGNED ->
+     to_val t2 (to_sbig_int v)
+   | CAST_HIGH ->
+     to_val t2
+       (shift_right_big_int (to_big_int v) (bits1-bits))
+   | CAST_LOW ->
+     to_val t2 (to_big_int v)
+  )
+
+
+let extract h l ((_,t) as v) =
+  let n = (h -% l) +% bi1 in
+  let nt = Reg(int_of_big_int n) in
+  let s = binop RSHIFT v (l,t) in
+  cast CAST_LOW s nt
+
+
+let concat ((_,lt) as lv) ((_,rt) as rv) =
+  let bitsl,bitsr =
+    match lt, rt with
+    | Reg(bitsl), Reg(bitsr) -> bitsl, bitsr
+    | _ -> failwith "concat"
+  in
+  let nt = Reg(bitsl + bitsr) in
+  let lv = cast CAST_UNSIGNED lv nt in
+  let rv = cast CAST_UNSIGNED rv nt in
+  let lv = binop LSHIFT lv (biconst bitsr, nt) in
+  binop OR lv rv
+
+
+let is_zero v =
+  let v = to_big_int v in
+  sign_big_int v = 0
+
+let bytes_to_int64 e bs =
+  match e with
+  | `Little -> List.fold_right (fun b i ->
+      let old = Int64.shift_left i 8 in
+      Int64.add old b) bs 0L
+  | `Big -> List.fold_left (fun i b ->
+      let old = Int64.shift_left i 8 in
+      Int64.add old b) 0L bs

plugins/x86/x86_legacy_bil_arithmetic.mli

@@ -0,0 +1,20 @@
+(* Copyright (C) 2017 ForAllSecure, Inc. - All Rights Reserved. *)
+
+module Bil = X86_legacy_bil
+open Bil
+
+exception ArithmeticEx of string
+(*val memoize : ?size:int -> ('a -> 'b) -> 'a -> 'b *)
+val power_of_two : Type.bv_size -> Z.t
+val bitmask : Type.bv_size -> Z.t
+val bits_of_width : Type.typ -> Type.bv_size
+val to_big_int : Z.t * Type.typ -> Z.t
+val to_sbig_int : Z.t * Type.typ -> Z.t
+val binop :
+  Type.binop_type -> Z.t * Type.typ -> Z.t * Type.typ -> Z.t * Type.typ
+val unop : Type.unop_type -> Z.t * Type.typ -> Z.t * Type.typ
+val cast : Type.cast_type -> Z.t * Type.typ -> Type.typ -> Z.t * Type.typ
+val extract : Z.t -> Z.t -> Z.t * Type.typ -> Z.t * Type.typ
+val concat : Z.t * Type.typ -> Z.t * Type.typ -> Z.t * Type.typ
+val is_zero : Z.t * Type.typ -> bool
+val bytes_to_int64 : [< `Big | `Little ] -> int64 list -> int64

plugins/x86/x86_legacy_bil_ast.ml

@@ -0,0 +1,88 @@
+(* Copyright (C) 2017 ForAllSecure, Inc. - All Rights Reserved. *)
+(**
+    The Abstract Syntax Tree.
+    This IL allows nested expressions, making it closer to VEX and
+    the concrete syntax than our SSA form. However, in most cases, this
+    makes analysis harder, so you will generally want to convert to SSA
+    for analysis.
+
+    @author Ivan Jager
+*)
+
+open X86_legacy_bil_type
+open X86_legacy_bil_var
+open Big_int_Z
+
+module Type = X86_legacy_bil_type
+module Var = X86_legacy_bil_var
+
+
+(* TODO: remove if Core.Std is opened in this file. *)
+let string_of_sexp = Core_kernel.string_of_sexp
+let sexp_of_string = Core_kernel.sexp_of_string
+
+(** Support for s-expressions *)
+let big_int_of_sexp sexp =
+  Core_kernel.String.t_of_sexp sexp |> Big_int_Z.big_int_of_string
+let sexp_of_big_int bi =
+  Big_int_Z.string_of_big_int bi |> Core_kernel.String.sexp_of_t
+
+type var = Var.t [@@deriving sexp]
+
+type exp =
+  | Load of (exp * exp * exp * typ)  (** Load(arr,idx,endian,t) *)
+  | Store of (exp * exp * exp * exp * typ)  (** Store(arr,idx,val,endian,t) *)
+  | BinOp of (binop_type * exp * exp)
+  | UnOp of (unop_type * exp)
+  | Var of var
+  | Lab of string
+  | Int of (big_int * typ)
+  | Cast of (cast_type * typ * exp) (** Cast to a new type. *)
+  | Let of (var * exp * exp)
+  | Unknown of (string * typ)
+  (* Expression types below here are just syntactic sugar for the above *)
+  | Ite of (exp * exp * exp)
+  | Extract of (big_int * big_int * exp) (** Extract hbits to lbits of e (Reg type) *)
+  | Concat of (exp * exp) (** Concat two reg expressions together *)
+[@@deriving sexp]
+
+type attrs = Type.attributes
+
+type stmt =
+  | Move of (var * exp * attrs)  (** Assign the value on the right to the
+                                     var on the left *)
+  | Jmp of (exp * attrs) (** Jump to a label/address *)
+  | CJmp of (exp * exp * attrs)
+  (** Conditional jump. If e1 is true, jumps to e2, otherwise fallthrough *)
+  | Label of (label * attrs) (** A label we can jump to *)
+  | Halt of (exp * attrs)
+  | Assert of (exp * attrs)
+  | Assume of (exp * attrs)
+  | Comment of (string * attrs) (** A comment to be ignored *)
+  | Special of (string * defuse option * attrs) (** A "special" statement. (does magic) *)
+
+type program = stmt list
+
+(* XXX: Should we move all of these to ast_convenience? *)
+
+
+(** If possible, make a label that would be refered to by the given
+    expression. *)
+let lab_of_exp =
+  let re = Str.regexp "^pc_\\(.*\\)+" in
+  function
+  (* VEX style pc_0x1234 labels *)
+  | Lab s when Str.string_match re s 0 ->
+    Some(Addr(big_int_of_string (Str.matched_group 1 s)))
+  | Lab s -> Some(Name s)
+  | Int(i, t) ->
+    Some(Addr i)
+  | _ -> None
+
+(** False constant. (If convenient, refer to this rather than building your own.) *)
+let exp_false = Int(Big_int_Z.zero_big_int, reg_1)
+(** True constant. *)
+let exp_true = Int(Big_int_Z.unit_big_int, reg_1)
+
+let little_endian = exp_false
+let big_endian = exp_true