makes bit-twiddling easier to read and analyze (#1492)

This PR improves legibility of the lifted code by using
extract/cast/concat combinations instead of bit masking, for assigning
aliased subregisters. In addition, it changes the default
pretty-printing syntax of BIL by making the `extract` keyword optional
in the extract operator, i.e., `extract:56:32[RAX]` will be now
printed as just `56:32[RAX]`. Finally, the PR adds several
optimization rules for extract/cast/concat combinations.

Makefile

@@ -55,7 +55,7 @@ testsuite:
 	git clone https://github.com/BinaryAnalysisPlatform/bap-testsuite.git testsuite
 
 check: testsuite
-	make REVISION=044dabe -C testsuite
+	make REVISION=07fe3462a62da1f -C testsuite
 
 .PHONY: indent check-style status-clean
 

lib/bap_core_theory/bap_core_theory_pass.ml

@@ -88,24 +88,25 @@ 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)
+
     let assign_sub dst src off =
       src >>= fun src ->
       let s = Var.sort dst in
       let dst_len = Val.Bitv.size s
       and src_len = Val.Bitv.size @@ Val.sort src in
-      let src = CT.unsigned s !!src in
-      let open Bitvec.Make(struct
-          let modulus = Bitvec.modulus dst_len
-        end) in
-      let mask =
-        lnot ((one lsl int src_len - one) lsl int off) in
-      let x = CT.(logand (var dst) (int s mask)) in
-      let off = int off in
-      let y = if Bitvec.equal off zero
-        then src
-        else CT.(lshift src (int s off)) in
-      CT.(set dst (logor x y))
-
+      let ulen = dst_len - src_len - off in
+      CT.set dst @@ match ulen,off with
+      | 0,0 -> !!src
+      | _,0 -> CT.append s (take CT.high ulen dst) !!src
+      | 0,_ -> CT.append s !!src (take CT.low off dst)
+      | _,_ -> CT.concat s [
+          take CT.high ulen dst;
+          !!src;
+          take CT.low off dst
+        ]
 
     let pos x =
       let module Pos = Bitvec.M32 in

lib/bap_types/bap_exp.ml

@@ -104,7 +104,7 @@ module PP = struct
     | Ite (ce, te, fe) ->
       pr "@[if %a@;then %a@;else %a@]" pp ce pp te pp fe
     | Extract (hi, lo, exp) ->
-      pr "extract:%d:%d[%a]" hi lo pp exp
+      pr "%d:%d[%a]" hi lo pp exp
     | Concat (le, re) as p ->
       pr (pfmt p le ^^ "." ^^ pfmt p re) pp le pp re
     | BinOp (EQ,e, Int x) when is_b1 x -> pr ("%a") pp e

plugins/bil/bil_semantics.ml

@@ -31,19 +31,41 @@ module Simpl = struct
   let ones width = Bil.Int (Word.ones width)
   let app2 = Bil.Apply.binop
 
+  let infer x = match Type.infer_exn x with
+    | Bil.Imm n -> n
+    | _ -> 0
+
+  let equal_cast = [%compare.equal: cast]
+
   let exp width =
     let concat x y = match x, y with
       | Int x, Int y -> Int (Word.concat x y)
+      | Cast (HIGH,s,(Var x as v)), Extract(p,q,Var x')
+        when Var.equal x x' && infer v - s - 1 = p ->
+        Cast (HIGH,s + p - q + 1,v)
+      | Cast (HIGH,s,(Var x as v)), Concat ((Extract(p,q,Var x')),z)
+        when Var.equal x x' && infer v - s - 1 = p ->
+        Concat (Cast (HIGH,s + p - q + 1,v),z)
       | x,y -> Concat (x,y)
 
     and cast t s x = match x with
       | Cast (_,s',_) as x when s = s' -> x
-      | Cast (t',s',x) when [%compare.equal: cast] t t' && s' > s -> Cast (t,s,x)
+      | Cast (t',s',x) when equal_cast t t' && s' >= s ->
+        Cast (t,s,x)
+      | Cast (UNSIGNED as t',s',x)
+      | Cast (SIGNED as t',s',x) when equal_cast t t' && s' <= s ->
+        Cast (t,s,x)
+      | Extract(p,_,x) when equal_cast t HIGH ->
+        Extract(p,p-s+1,x)
       | Int w -> Int (Bil.Apply.cast t s w)
+      | x when infer x = s -> x
       | _ -> Cast (t,s,x)
 
     and extract hi lo x = match x with
       | Int w -> Int (Word.extract_exn ~hi ~lo w)
+      | Extract (p,q,x) when hi <= p && lo >= q ->
+        Extract (hi,lo,x)
+      | x when lo = 0 && infer x = hi + 1 -> x
       | x -> Extract (hi,lo,x)
 
     and unop op x = match op,x with