ite-handling in Primus and allowing the user to disable ite-hoisting.

The semantics of ite evaluation in Primus follow the latest updates
in the BIL specification:

   BinaryAnalysisPlatform/bil#9

The extra option in the BIL normalization function enables the
user to preserve ite if that is desirable.

lib/bap/bap.mli

@@ -3653,8 +3653,8 @@ module Std : sig
     *)
     val is_referenced : var -> t -> bool
 
-    (** [normalize ?normalize_exp xs] produces a normalized BIL program
-        with the same[^1] semantics but in the BIL normalized
+    (** [normalize ?keep_ites ?normalize_exp xs] produces a normalized BIL
+        program with the same[^1] semantics but in the BIL normalized
         form (BNF). There are two normalized forms, both described
         below. The first form (BNF1) is more readable, the second form
         (BNF2) is more strict, but sometimes yields a code, that is hard
@@ -3721,8 +3721,12 @@ module Std : sig
         @param normalize_exp (defaults to [false]) if set to [true] then
         the returned program will be in BNF2.
 
+        @param keep_ites (defaults to [false]) if set to [true] then
+        the returned program will preserve ite expressions.
+
         @since 1.3 *)
-    val normalize : ?normalize_exp:bool -> stmt list -> stmt list
+    val normalize : ?keep_ites:bool -> ?normalize_exp:bool
+       -> stmt list -> stmt list
 
     (** [simpl ?ignore xs] recursively applies [Exp.simpl] and also
         simplifies [if] and [while] expressions with statically known

lib/bap_primus/bap_primus.mli

@@ -851,6 +851,11 @@ module Std : sig
           and produces [z] as a result.*)
       val concat : ((value * value) * value) observation
 
+      (** [ite ((cond, yes, no), res)] happens after the ite expression
+          that corresponds to ite([cond], [yes], [no]) is evaluated
+          to [res]. *)
+      val ite : ((value * value * value) * value) observation
+
       (** an identifier of a term that will be executed next.   *)
       val enter_term : tid observation
 

lib/bap_primus/bap_primus_interpreter.ml

@@ -140,6 +140,12 @@ let sexp_of_concat ((x,y),r) = results r @@ sexps [
     string_of_value y;
   ]
 
+let sexp_of_ite ((cond, yes, no), r) = results r @@ sexps [
+  string_of_value cond;
+  string_of_value yes;
+  string_of_value no;
+]
+
 let binop,on_binop =
   Observation.provide ~inspect:sexp_of_binop "binop"
 
@@ -158,6 +164,9 @@ let concat,on_concat =
 let const,on_const =
   Observation.provide ~inspect:sexp_of_value "const"
 
+let ite, on_ite =
+  Observation.provide ~inspect:sexp_of_ite "ite"
+
 let sexp_of_name = function
   | `symbol name -> Sexp.Atom name
   | `tid tid -> Sexp.Atom (Tid.name tid)
@@ -303,6 +312,10 @@ module Make (Machine : Machine) = struct
     trapped_memory_access (Memory.set a.value x) >>= fun () ->
     !!on_stored (a,x)
 
+  let ite cond yes no =
+    value (if Word.is_one cond.value then yes.value else no.value) >>= fun r ->
+    !!on_ite ((cond, yes, no), r) >>| fun () -> r
+
   let rec eval_exp x =
     let eval = function
       | Bil.Load (Bil.Var _, a,_,`r8) -> eval_load a
@@ -315,13 +328,19 @@ module Make (Machine : Machine) = struct
       | Bil.Unknown (x,typ) -> eval_unknown x typ
       | Bil.Extract (hi,lo,x) -> eval_extract hi lo x
       | Bil.Concat (x,y) -> eval_concat x y
+      | Bil.Ite (cond, yes, no) -> eval_ite cond yes no
       | exp ->
         invalid_argf "precondition failed: denormalized exp: %s"
           (Exp.to_string exp) () in
     !!exp_entered x >>= fun () ->
     eval x >>= fun r ->
     !!exp_left x >>| fun () -> r
   and eval_load a = eval_exp a >>= load_byte
+  and eval_ite cond yes no =
+    eval_exp yes >>= fun yes ->
+    eval_exp no >>= fun no ->
+    eval_exp cond >>= fun cond ->
+    ite cond yes no
   and eval_store m a x =
     eval_storage m >>= fun () ->
     eval_exp a >>= fun a ->

lib/bap_primus/bap_primus_interpreter.mli

@@ -27,6 +27,7 @@ val unop : ((unop * value) * value) observation
 val cast : ((cast * int * value) * value) observation
 val extract : ((int * int * value) * value) observation
 val concat : ((value * value) * value) observation
+val ite : ((value * value * value) * value) observation
 
 
 val enter_exp : exp observation

lib/bap_types/bap_helpers.ml

@@ -1092,8 +1092,9 @@ module Normalize = struct
           hoist_stores (Move (v,store) :: substitute store (Var v) [stmt])
     end) bil
 
-  let bil ?normalize_exp:(ne=false) xs =
+  let bil ?(keep_ites=false) ?normalize_exp:(ne=false) xs =
     let normalize_exp = if ne then normalize_exp else ident in
+    let split_ite = if keep_ites then ident else split_ite in
     let rec run xs =
       List.concat_map ~f:hoist_non_generative_expressions xs |>
       normalize_conditionals |>

lib/bap_types/bap_helpers.mli

@@ -21,7 +21,7 @@ val prune_unreferenced :
   ?virtuals:bool ->
   bil -> bil
 
-val normalize : ?normalize_exp:bool -> bil -> bil
+val normalize : ?keep_ites:bool -> ?normalize_exp:bool -> bil -> bil
 val normalize_negatives : bil -> bil
 val substitute : exp -> exp -> bil -> bil
 val substitute_var : var -> exp -> bil -> bil
@@ -106,7 +106,8 @@ module Stmt : sig
   val is_referenced : var -> stmt -> bool
   val fixpoint : (stmt -> stmt) -> (stmt -> stmt)
   val free_vars : stmt -> Bap_var.Set.t
-  val normalize : ?normalize_exp:bool -> stmt list -> stmt list
+  val normalize : ?keep_ites:bool -> ?normalize_exp:bool
+    -> stmt list -> stmt list
 end