introduces BIL special encodings and publishes BIL CT parser

lib/bap/bap.mli

@@ -2127,6 +2127,8 @@ module Std : sig
     (** [special msg -> Special msg]  *)
     val special : string -> stmt
 
+
+
     (** [while_ cond stmts -> While (cond,stmts)]  *)
     val while_ : exp -> stmt list -> stmt
 
@@ -2332,6 +2334,94 @@ module Std : sig
         @since 1.5 *)
     val prune_dead_virtuals : stmt list -> stmt list
 
+
+    (** {3 BIL Special values}
+
+        The [Special] statement enables encoding of arbitrary
+        semantics using [encode attr values] and [decode attr]
+        to get the values back. The meaning of the [attr] and
+        [values] is specific to the user domain.
+
+        Example, [encode call "malloc"], where
+        [call] is the BIL attribute that denotes a call to a
+        function. See {!call} for more information.
+
+    *)
+
+
+    (** BIL attributes.
+
+        BIL attributes serve the role of constructor for encoding
+        values as special statements. The attribute defines methods
+        for encoding and decoding values as a string as well as a
+        unique attribute name.
+
+        @since 2.3.0
+    *)
+    module Attribute : sig
+
+      (** the type of attributes  *)
+      type 'a t
+
+
+      (** [declare ?package name ~encode ~decode] declares a new attribute.
+
+          The attribute [package], [name] pair should be unique. If an
+          attribute with the given name is already registered the
+          registration will fail. *)
+      val declare :
+        ?package:string ->
+        encode:('a -> string) ->
+        decode:(string -> 'a) ->
+        string ->
+        'a t
+    end
+
+
+    (** [encode attr value] encodes [value] as a special statement.
+
+        @since 2.3.0    *)
+    val encode : 'a Attribute.t -> 'a -> stmt
+
+
+    (** [decode attr s] is [Some v] if [s] is [encode attr v].
+
+        @since 2.3.0
+    *)
+    val decode : 'a Attribute.t -> stmt -> 'a option
+
+    (** [call] is the attribute name for encoding calls.
+
+        @since 2.3.0
+    *)
+    val call : string Attribute.t
+
+
+    (** [intrinsic] is the attribute for intrinsic calls.
+
+        An intrinsic is a low-level, usually microarchitectural
+        operation.
+
+        @since 2.3.0
+    *)
+    val intrinsic: string Attribute.t
+
+
+    (** Core Theory specification of BIL.  *)
+    module Theory : sig
+
+
+      (** [parser] the parser enables reflection of the bil statements
+          into core theory terms. To reflect a bil program [prog] into
+          the theory [Theory], use
+          {[
+            let module Parser = Theory.Parser.Make(Theory) in
+            Parser.run Bil.Theory.parser bil
+          ]}
+      *)
+      val parser : (exp,_,stmt) Theory.Parser.t
+    end
+
     (** Maps BIL operators to bitvectors.
         @since 1.3
     *)

lib/bap_types/bap_core_theory_bil_parser.ml

@@ -0,0 +1,183 @@
+open Core_kernel
+open Bap_core_theory
+open Theory.Parser
+
+include Bap_main.Loggers()
+
+module Exp = Bap_exp.Exp
+module Bil = Bap_bil
+module Word = Bap_bitvector
+module Type = Bap_common.Type
+module Size = Bap_size
+module Stmt = Bap_stmt.Stmt
+
+type stmt = Bil.stmt
+
+
+type context = [`Bitv | `Bool | `Mem ] [@@deriving sexp]
+let fail exp ctx =
+  error "ill-formed expression in %a ctxt: %a"
+    Sexp.pp (sexp_of_context ctx) Bap_exp.pp exp
+
+type exp = Bil.exp
+module Var = Bap_var
+let rec uncat acc : exp -> exp list = function
+  | Concat ((Concat (x,y)), z) -> uncat (y::z::acc) x
+  | Concat (x,y) -> x::y::acc
+  | x -> x::acc
+
+let bits_of_var v = match Var.typ v with
+  | Imm x -> x
+  | _ -> failwith "not a bitv var"
+
+let byte x = Exp.int (Word.of_int ~width:8 x)
+let is_big e =
+  Exp.int @@
+  if [%compare.equal : Word.endian] e BigEndian
+  then Word.b1 else Word.b0
+
+let is_reg v = match Var.typ v with
+  | Type.Imm 1 | Type.Mem _ -> false
+  | _ -> true
+
+let is_bit v = match Var.typ v with
+  | Type.Imm 1 -> true
+  | _ -> false
+
+let is_mem v = match Var.typ v with
+  | Type.Mem _ -> true
+  | _ -> false
+
+let bitv : type t r. (t,exp,r) bitv_parser =
+  fun (module S) -> function
+    | Cast (HIGH,n,x) -> S.high n x
+    | Cast (LOW,n,x) -> S.low n x
+    | Cast (UNSIGNED,n,x) -> S.unsigned n x
+    | Cast (SIGNED,n,x) -> S.signed n x
+    | BinOp(PLUS,x,y) -> S.add x y
+    | BinOp(MINUS,x,y) -> S.sub x y
+    | BinOp(TIMES,x,y) -> S.mul x y
+    | BinOp(DIVIDE,x,y) -> S.div x y
+    | BinOp(SDIVIDE,x,y) -> S.sdiv x y
+    | BinOp(MOD,x,y) -> S.modulo x y
+    | BinOp(SMOD,x,y) -> S.smodulo x y
+    | BinOp(LSHIFT,x,y) -> S.lshift x y
+    | BinOp(RSHIFT,x,y) -> S.rshift x y
+    | BinOp(ARSHIFT,x,y) -> S.arshift x y
+    | BinOp(AND,x,y) -> S.logand x y
+    | BinOp(OR,x,y) -> S.logor x y
+    | BinOp(XOR,x,y) -> S.logxor x y
+    | UnOp(NEG,x) -> S.neg x
+    | UnOp(NOT,x) -> S.not x
+    | Load(m,k,e,s) ->
+      S.load_word (Size.in_bits s) (is_big e) m k
+    | Var v -> S.var (Var.name v) (bits_of_var v)
+    | Int x -> S.int (Word.to_bitvec x) (Word.bitwidth x)
+    | Let (v,y,z) when is_bit v -> S.let_bit (Var.name v) y z
+    | Let (v,y,z) when is_reg v -> S.let_reg (Var.name v) y z
+    | Let (v,y,z) when is_mem v -> S.let_mem (Var.name v) y z
+    | Ite (x,y,z) -> S.ite x y z
+    | Extract (hi,lo,x) ->
+      let s = max 0 (hi-lo+1) in
+      S.extract s (byte hi) (byte lo) x
+    | Concat (_,_) as cat -> S.concat (uncat [] cat)
+    | Unknown (_, Imm s) -> S.unknown s
+    | BinOp ((EQ|NEQ|LT|LE|SLT|SLE), _, _) as op ->
+      S.ite op (Int Word.b1) (Int Word.b0)
+
+    (* ill-formed expressions *)
+    | Let _
+    | Store (_, _, _, _, _)
+    | Unknown (_, (Mem _|Unk)) as exp -> fail exp `Bitv; S.error
+
+
+
+let mem : type t. (t,exp) mem_parser =
+  fun (module S) -> function
+    | Unknown (_,Mem (k,v)) ->
+      S.unknown (Size.in_bits k) (Size.in_bits v)
+    | Store (m,k,v,e,_) ->
+      S.store_word (is_big e) m k v
+    | Var v  ->
+      let with_mem_types v f = match Var.typ v with
+        | Mem (ks,vs) -> f (Size.in_bits ks) (Size.in_bits vs)
+        | _ -> fail (Bil.Exp.Var v) `Mem; S.error in
+      with_mem_types v (S.var (Var.name v))
+    | Let (v,y,z) when is_bit v -> S.let_bit (Var.name v) y z
+    | Let (v,y,z) when is_reg v -> S.let_reg (Var.name v) y z
+    | Let (v,y,z) when is_mem v -> S.let_mem (Var.name v) y z
+    | Ite (c,x,y) ->  S.ite c x y
+    (* the rest is ill-formed *)
+    | Let _
+    | Unknown (_,_)
+    | Load (_,_,_,_)
+    | BinOp (_,_,_)
+    | UnOp (_,_)
+    | Int _
+    | Cast (_,_,_)
+    | Extract (_,_,_)
+    | Concat (_,_) as exp -> fail exp `Mem; S.error
+
+let float _ _ = assert false
+let rmode _ _ = assert false
+
+let bool : type t r. (t,exp,r) bool_parser =
+  fun (module S) -> function
+    | Var x -> S.var (Var.name x)
+    | Int x -> S.int (Word.to_bitvec x)
+    | Cast (HIGH,1,x) -> S.high x
+    | Cast (LOW,1,x) -> S.low x
+    | BinOp (EQ,x,y) -> S.eq x y
+    | BinOp (NEQ,x,y) -> S.neq x y
+    | BinOp (LT,x,y) -> S.lt x y
+    | BinOp (LE,x,y) -> S.le x y
+    | BinOp (SLT,x,y) -> S.slt x y
+    | BinOp (SLE,x,y) -> S.sle x y
+    | BinOp (OR,x,y) -> S.logor x y
+    | BinOp (AND,x,y) -> S.logand x y
+    | BinOp (XOR,x,y) -> S.logxor x y
+    | UnOp (NOT,x) -> S.not x
+    | Let (v,y,z) when is_bit v -> S.let_bit (Var.name v) y z
+    | Let (v,y,z) when is_reg v -> S.let_reg (Var.name v) y z
+    | Let (v,y,z) when is_mem v -> S.let_mem (Var.name v) y z
+    | Ite (x,y,z) -> S.ite x y z
+    | Extract (hi,lo,x) when hi = lo -> S.extract hi x
+    | Unknown (_,_) -> S.unknown ()
+    | Let _
+    | Extract _
+    | UnOp (NEG,_)
+    | Cast (_,_,_)
+    | Load (_,_,_,_)
+    | Store (_,_,_,_,_)
+    | Concat (_,_)
+    | BinOp ((PLUS|MINUS|TIMES|DIVIDE|SDIVIDE|
+              MOD|SMOD|LSHIFT|RSHIFT|ARSHIFT),_,_) as exp
+      -> fail exp `Bool; S.error
+
+
+let stmt : type t r. (t,exp,r,stmt) stmt_parser =
+  fun (module S) ->
+  let set v x =
+    let n = Var.name v in
+    match Var.typ v with
+    | Unk ->
+      error "can't reify the variable %s: unknown type" (Var.name v);
+      S.error
+    | Imm 1 -> S.set_bit n x
+    | Imm m -> S.set_reg n m x
+    | Mem (ks,vs) ->
+      S.set_mem n (Size.in_bits ks) (Size.in_bits vs) x in
+  fun s -> match Stmt.(decode call s) with
+    | Some dst -> S.call dst
+    | None -> match Stmt.(decode intrinsic s) with
+      | Some data -> S.call data
+      | None -> match s with
+        | Move (v,x) -> set v x
+        | Jmp (Int x) -> S.goto (Word.to_bitvec x)
+        | Jmp x -> S.jmp x
+        | Special s -> S.special s
+        | While (c,xs) -> S.while_ c xs
+        | If (c,xs,ys) -> S.if_ c xs ys
+        | CpuExn n -> S.cpuexn n
+
+let t = {bitv; mem; stmt; bool; float; rmode}

lib/bap_types/bap_core_theory_bil_parser.mli

@@ -0,0 +1,4 @@
+open Bap_core_theory
+open Bap_bil
+
+val t : (exp,_,stmt) Theory.Parser.t

lib/bap_types/bap_stmt.ml

@@ -6,14 +6,82 @@ open Bap_common
 open Format
 open Bap_bil
 
+
+module Attribute = struct
+  type 'a t = {
+    constr : KB.Name.t;
+    encode : 'a -> string;
+    decode : string -> 'a;
+  }
+
+  let known = Hash_set.create (module KB.Name)
+
+  let declare ?package ~encode ~decode name =
+    let constr = KB.Name.create ?package name in
+    if Hash_set.mem known constr
+    then failwithf "The BIL attribute %s is already \
+                    registered. Please choose another name."
+        (KB.Name.show constr) ();
+    {encode; decode; constr}
+end
+
+module Special = struct
+  let call = Attribute.declare "call"
+      ~encode:ident
+      ~decode:ident
+      ~package:"bap"
+
+  let intrinsic = Attribute.declare "intrinsic"
+      ~encode:ident
+      ~decode:ident
+      ~package:"bap"
+
+
+  let prefix = "@attribute:"
+  let encode {Attribute.constr; encode} data =
+    prefix ^
+    Sexp.to_string @@
+    Sexp.List [
+      Atom (KB.Name.show constr);
+      Atom (encode data);
+    ]
+
+  let decode_payload {Attribute.constr; decode} name data =
+    let name = KB.Name.read name in
+    if KB.Name.equal name constr
+    then Some (decode data)
+    else None
+
+
+  let decode attr s = match String.chop_prefix ~prefix s with
+    | None -> None
+    | Some payload -> match Sexp.of_string payload with
+      | exception _ -> None
+      | Sexp.List [Atom name; Atom data] -> decode_payload attr name data
+      | _ -> None
+
+  let pp_default ppf s = fprintf ppf "special@ @[<1>(%s)@]" s
+
+  let pp ppf s = match String.chop_prefix ~prefix s with
+    | None -> pp_default ppf s
+    | Some data -> match Sexp.of_string data with
+      | exception _ -> pp_default ppf s
+      | Sexp.List (Atom cons::vals) ->
+        let pp_vals ppf xs = pp_print_list
+            ~pp_sep:(fun ppf () -> pp_print_string ppf ", ")
+            Sexp.pp_hum ppf xs in
+        fprintf ppf "%s(@[<hv2>%a@])" cons pp_vals vals
+      | _ -> pp_default ppf s
+end
+
 let rec pp fmt s =
   let open Stmt in match s with
   | Move (var, exp) ->
     fprintf fmt "@[<2>%a :=@ %a@]" Bap_var.pp var Bap_exp.pp exp
   | Jmp (Exp.Var _ | Exp.Int _ as exp) ->
     fprintf fmt "@[<2>jmp@ %a@]" Bap_exp.pp exp
   | Jmp exp -> fprintf fmt "@[<2>jmp@ (%a)@]" Bap_exp.pp exp
-  | Special s -> fprintf fmt "special@ @[<1>(%s)@]" s
+  | Special s -> Special.pp fmt s
   | While (cond, body) ->
     fprintf fmt "@[<v0>@[<v2>while (@[%a@]) {@;%a@]@;}@]"
       Bap_exp.pp cond pp_list body
@@ -43,6 +111,12 @@ module Stmt = struct
   let while_ x s1  = While (x,s1)
   let if_ x s1 s2 = If (x,s1,s2)
   let cpuexn n = CpuExn n
+  let encode s xs = special @@ Special.encode s xs
+  let decode n = function
+    | Special s -> Special.decode n s
+    | _ -> None
+  let call = Special.call
+  let intrinsic = Special.intrinsic
 end
 
 module Infix = struct