implements floating-point intrinsic subroutines (#1483)

* implements Primus Lisp floating-point primitives

* adds the bitvector emulation of the is_nan operation

* implements emulation of the floating-point predicates

* implements the emulation of rounding modes

* renames some internal modules to make things less confusing

* adds primitives for floating-point predicates

* implements emulation of floating-point conversions to integers

* enables static and disables dynamic floating-point emulation

* adds round, abs, and sqrt operations

* adds the cast-(s)float operations

* adds cast_int operations and fixes the intrinsic reification

plugins/bil/bil_float.ml

@@ -283,6 +283,10 @@ module Make(B : Theory.Core) = struct
   let is_subnormal fsort x =
     unpack_raw fsort x @@ fun _ e _ -> B.is_zero e
 
+
+  let is_fpos = B.is_positive
+  let is_fneg = B.is_negative
+
   let is_zero x =
     let open B in
     x >>-> fun s x ->

plugins/bil/bil_float.mli

@@ -1,18 +1,41 @@
+(* Transforms floating-point operations into bitvector operations.
+
+   The reason why this module is in BIL is because it is not a theory
+   but a theory transformer in other words it is not a structure but
+   a functor that requires other theory. Right now, the other theory
+   is hardcoded to be the BIL theory and using this transformation
+   will not affect any other theories. To be able to remove this
+   transformation from the BIL plugin we need to finish the Core
+   Theory passes framework. Until then, we will keep it here.
+
+   Otherwise, the trasnformation (this module) is totally generic and
+   is independent of BIL and could be put into a library if
+   necessary.
+
+*)
+
 open Bap_knowledge
 open Bap_core_theory
 
 open Theory
 
 type ('b,'e,'t,'s) fsort = (('b,'e,'t) IEEE754.t,'s) format Float.t Value.sort
 
-module Make(B : Theory.Core) : sig
+module Make(_ : Theory.Core) : sig
 
   val fadd : ('b,'e,'t,'s) fsort -> rmode -> 's bitv ->  's bitv -> 's bitv
   val fsub : ('b,'e,'t,'s) fsort -> rmode -> 's bitv ->  's bitv -> 's bitv
   val fmul : ('b,'e,'t,'s) fsort -> rmode -> 's bitv ->  's bitv -> 's bitv
   val fdiv : ('b,'e,'t,'s) fsort -> rmode -> 's bitv ->  's bitv -> 's bitv
   val fsqrt : ('b,'e,'t,'s) fsort -> rmode -> 's bitv -> 's bitv
 
+  val is_nan : ('b,'e,'t,'s) fsort -> 's bitv -> bool
+  val is_finite : ('b,'e,'t,'s) fsort -> 's bitv -> bool
+  val is_inf : ('b,'e,'t,'s) fsort -> 's bitv -> bool
+  val is_zero : 's bitv -> bool
+  val is_fpos : 's bitv -> bool
+  val is_fneg : 's bitv -> bool
+
   val cast_int :  ('a, 'b, 'c, 'd) fsort -> 'e Bitv.t Value.sort -> 'd bitv -> 'e bitv
   val cast_float : ('a, 'b, 'c, 'd) fsort -> rmode -> 'e bitv -> 'd bitv
   val cast_float_signed : ('a, 'b, 'c, 'd) fsort -> rmode -> 'e bitv -> 'd bitv

plugins/bil/bil_main.ml

@@ -124,9 +124,15 @@ let () =
       "Selects the list and the order of analyses to be applied during
        the lifing to BIL code." in
     Configuration.(parameter Type.(list pass) ~doc "passes") in
-  let enable_fp_emu = Configuration.flag "enable-fp-emulation"
-      ~doc:"Enable the floating point emulation mode.
-      When specified, enables reification of the floating point
+  let enable_fp_emu = Configuration.parameter
+      Type.(bool =? true)
+      "floating-point-emulation"
+      ~aliases:["enable-fp-emulation"]
+      ~as_flag:true
+      ~doc:"Enable/disable floating-point emulation (on by default).
+      When enabled the floating-point operations will be reified into
+      BIL expressions using bitvector arithmetic. Only IEEE754 binary
+      formats are supported.
       operations into Bil expressions that denote those operations
       in terms of bitvector arithmetic. This may lead to very large
       denotations." in
@@ -174,7 +180,6 @@ let () =
         ~package:"bap" ~name:"bil-fp-emu"
         ~extends:["bap:bil"]
         ~desc: "semantics in BIL, including FP emulation"
-        ~context:["floating-point"]
         ~provides:[
           "bil";
           "floating-point";

plugins/bil/bil_semantics.ml

@@ -14,6 +14,9 @@ let bool = Theory.Bool.t
 let bits = Theory.Bitv.define
 let size = Theory.Bitv.size
 let sort = Theory.Value.sort
+let resort s x = KB.Value.refine x s
+
+
 (* we need to recurse intelligently, only if optimization
    occured, that might open a new optimization opportunity,
    and continue recursion only if we have progress.
@@ -503,14 +506,36 @@ module Basic : Theory.Basic = struct
     unk @@ Theory.Float.bits (sort x)
 end
 
-module Core : Theory.Core = struct
+module Rmode = struct
+  open KB.Syntax
+  let s = bits 8
+
+  let rmode n =
+    let+ n = Basic.int s (Bitvec.M8.int n) in
+    resort Theory.Rmode.t n
+
+  let rne = rmode 0
+  let rna = rmode 1
+  let rtp = rmode 2
+  let rtn = rmode 3
+  let rtz = rmode 4
+
+  let requal x y =
+    let* x = x >>| resort s in
+    let* y = y >>| resort s in
+    Basic.eq !!x !!y
+
+end
+
+module CT : Theory.Core = struct
   include Theory.Empty
   include Basic
+  include Rmode
 end
 
-module FBil = Bil_float.Make(Core)
+module Float = Bil_float.Make(CT)
 
-module FPEmulator = struct
+module Emulator = struct
   open Knowledge.Syntax
   type 'a t = 'a knowledge
 
@@ -526,52 +551,48 @@ module FPEmulator = struct
     List.find supported ~f:(fun p ->
         Theory.Value.Sort.same s (Theory.IEEE754.Sort.define p))
 
-  let resort s x = KB.Value.refine x s
-
   let fbits x =
     x >>| fun x -> resort (Theory.Float.bits (sort x)) x
 
   let float s x =
     x >>| fun x -> resort s x
 
 
+  let with_fsort ~unk_s s f =
+    match ieee754_of_sort s with
+    | None -> CT.unk unk_s
+    | Some ({Theory.IEEE754.k} as p) ->
+      f (bits k) (Theory.IEEE754.Sort.define p)
+
   let fop : type f.
     (_ -> _ -> _ Theory.bitv -> _ Theory.bitv -> _ Theory.bitv) ->
     _ -> f Theory.float -> f Theory.float -> f Theory.float =
     fun op rm x y ->
     x >>= fun x ->
     y >>= fun y ->
     let xs = sort x in
-    match ieee754_of_sort xs with
-    | None -> Core.unk xs
-    | Some ({Theory.IEEE754.k} as p) ->
-      let bs = bits k in
-      let x = resort bs x and y = resort bs y in
-      let s = Theory.IEEE754.Sort.define p in
-      float xs (op s rm !!x !!y)
+    with_fsort xs ~unk_s:xs @@ fun bs s ->
+    let x = resort bs x and y = resort bs y in
+    float xs (op s rm !!x !!y)
 
-  let fadd rm = fop FBil.fadd rm
-  let fsub rm = fop FBil.fsub rm
-  let fmul rm = fop FBil.fmul rm
-  let fdiv rm = fop FBil.fdiv rm
+  let fadd rm = fop Float.fadd rm
+  let fsub rm = fop Float.fsub rm
+  let fmul rm = fop Float.fmul rm
+  let fdiv rm = fop Float.fdiv rm
 
   let fuop : type f.
     _ ->
     _ -> f Theory.float -> f Theory.float =
     fun op rm x ->
     x >>= fun x ->
     let xs = sort x in
-    match ieee754_of_sort xs with
-    | None -> Core.unk xs
-    | Some ({Theory.IEEE754.k} as p) ->
-      let bs = bits k in
-      let x = resort bs x in
-      let s = Theory.IEEE754.Sort.define p in
-      float xs (op s rm !!x)
+    with_fsort ~unk_s:xs xs @@ fun bs s ->
+    let x = resort bs x in
+    float xs (op s rm !!x)
 
-  let fsqrt rm x = fuop FBil.fsqrt rm x
+  let fsqrt rm x = fuop Float.fsqrt rm x
 
-  open Core
+  open CT
 
   let small s x =
     let m = Bitvec.modulus (size s) in
@@ -600,19 +621,38 @@ module FPEmulator = struct
 
   let make_cast_float cast s m v =
     match ieee754_of_sort s with
-    | None -> Core.unk s
+    | None -> CT.unk s
     | Some p ->
       cast (Theory.IEEE754.Sort.define p) m v >>| resort s
 
-  let cast_float s m v = make_cast_float FBil.cast_float s m v
-  let cast_sfloat s m v = make_cast_float FBil.cast_float_signed s m v
+  let cast_float s m v = make_cast_float Float.cast_float s m v
+  let cast_sfloat s m v = make_cast_float Float.cast_float_signed s m v
+
+  let cast_int ts _ v =
+    v >>= fun v ->
+    with_fsort ~unk_s:ts (sort v) @@ fun bs s ->
+    Float.cast_int s ts !!(resort bs v)
+
+  let cast_sint = cast_int
+
+  let case f x =
+    x >>= fun x ->
+    with_fsort (sort x) ~unk_s:bool @@ fun bs fs ->
+    f fs !!(resort bs x)
+
+  let is_finite x = case Float.is_finite x
+  let is_nan x = case Float.is_nan x
+  let is_inf x = case Float.is_inf x
+  let is_fzero x = case (fun _ -> Float.is_zero) x
+  let is_fpos x = case (fun _ -> Float.is_fpos) x
+  let is_fneg x = case (fun _ -> Float.is_fneg) x
 
   let forder x y =
     x >>= fun x ->
     y >>= fun y ->
     let xs = sort x in
     match ieee754_of_sort xs with
-    | None -> Core.unk bool
+    | None -> CT.unk bool
     | Some ({Theory.IEEE754.k; w; t}) ->
       let bs = bits k and ms = bits (k-1)in
       let x = resort bs x and y = resort bs y in
@@ -639,7 +679,8 @@ module FPEmulator = struct
       ]
 end
 
+module Core = CT
 module Core_with_fp_emulation = struct
   include Core
-  include FPEmulator
+  include Emulator
 end