Update value-set analysis for BAP 2.x (#303)

Co-authored-by: Xudong WANG <xudongw@cse.unsw.edu.au>

vsa/explicit_edge/explicit_edge.ml

@@ -1,3 +1,4 @@
+
 (***************************************************************************)
 (*                                                                         *)
 (*  Copyright (C) 2018/2019 The Charles Stark Draper Laboratory, Inc.      *)
@@ -37,7 +38,7 @@ let specialize_cond cond e w : exp =
 
 let create_label terms w : label =
   let has_address w b = Option.value_map ~default:false
-      (Term.get_attr b address) ~f:(fun addr -> addr = w) in
+      (Term.get_attr b address) ~f:(fun addr -> Word.(addr = w)) in
   match Seq.find terms ~f:(has_address w) with
   | Some b -> (Direct (Term.tid b))
   | None -> (Indirect (Bil.Int w))
@@ -83,7 +84,7 @@ let add_edges (prog : program term) (s : sub term) (postcondition : AI.t) (b : b
     | Goto (Indirect e) | Ret (Indirect e) ->
       let targets = Utils.exn_on_err @@ Vsa.denote_imm_exp e postcondition in
       let cardn = Clp.cardinality targets in
-      if cardn > Word.of_int !Utils.max_edge_explosion ~width:(Word.bitwidth cardn)
+      if Word.(cardn > of_int !Utils.max_edge_explosion ~width:(bitwidth cardn))
       then Printf.printf "//Edge transform produced edge explosion (>%d)@.\n" !Utils.max_edge_explosion
       else List.iter (Clp.iter targets) ~f:begin fun w ->
           (* TODO: this cond is computed twice; fix *)
@@ -104,7 +105,7 @@ let add_edges (prog : program term) (s : sub term) (postcondition : AI.t) (b : b
         | Indirect e ->
           let targets = Utils.exn_on_err @@ Vsa.denote_imm_exp e postcondition in
           let cardn = Clp.cardinality targets in
-          if cardn > Word.of_int !Utils.max_edge_explosion ~width:(Word.bitwidth cardn)
+          if Word.(cardn > of_int !Utils.max_edge_explosion ~width:(bitwidth cardn))
           then Printf.printf "//Edge transform produced edge explosion@."
           else List.iter (Clp.iter targets) ~f:begin fun w ->
               let cond = specialize_cond (Jmp.cond j) e w in
@@ -141,11 +142,12 @@ let insert_edges prog sub sol : sub term * is_done =
 end
 
 let rec do_until_done ?fuel (f : 'a -> 'a * is_done) (arg : 'a) : 'a =
-  if fuel = Some 0 then begin
-    Printf.printf "@.Giving up on edge addition; could not find fixpoint!@.";
-    arg
-  end else
-    let res1, done_ = f arg in
+  match fuel with
+  | Some 0 -> begin
+      Printf.printf "@.Giving up on edge addition; could not find fixpoint!@.";
+      arg
+    end
+  | _ -> let res1, done_ = f arg in
     match done_ with
     | Done -> res1
     | EdgesAdded -> do_until_done ?fuel:(Option.map fuel ~f:pred) f res1
@@ -168,7 +170,7 @@ let main (sub_name : string option) (max_edges : int) (proj : project) : project
     Term.enum sub_t prog
     |> Seq.fold ~init:(prog, Done) ~f:begin fun (prog, done_) sub ->
       let sname = Sub.name sub in
-      if Option.value ~default:sname sub_name = sname then
+      if String.(Option.value ~default:sname sub_name = sname) then
         let sol = Option.value_exn ~message:"VSA not stored!" (Vsa.load sub) in
         let sub', edges_added = insert_edges prog sub sol in
         let prog' = Term.update sub_t prog sub' in

vsa/value_set/lib/cbat_value_set.opam

@@ -14,7 +14,7 @@ homepage: "https://github.com/draperlaboratory/cbat_tools"
 bug-reports: "https://github.com/draperlaboratory/cbat_tools"
 dev-repo: "git+https://github.com/draperlaboratory/cbat_tools"
 depends: [
-  "bap" {>= "master"}
+  "bap" {>= "2.1.0"}
   "core" {>= "0.12.4"}
   "ppx_deriving"
   "ppx_bin_prot"

vsa/value_set/lib/src/cbat_ai_memmap.ml

@@ -50,7 +50,7 @@ module Key = struct
 
 
   let create ~lo ~hi : t Or_error.t =
-    if lo <= hi then Result.Ok {lo; hi}
+    if Word.(lo <= hi) then Result.Ok {lo; hi}
     else Or_error.error "attempted to create key with lo above hi"
         (lo, hi) (fun (lo, hi) -> Sexp.List[Word.sexp_of_t lo;
                                             Word.sexp_of_t hi])
@@ -242,12 +242,14 @@ end = struct
     let top = 1, BigEndian
 
     let join (w1, e1 : t) (w2, e2 : t) : t =
-      if e1 = e2 then min w1 w2, e1 else min addressable_width (min w1 w2), e1
+      if Bitvector.compare_endian e1 e2 = 0
+      then min w1 w2, e1
+      else min addressable_width (min w1 w2), e1
 
     let widen_join = join
 
     let precedes (w1, e1 : t) (w2, e2 : t) : bool =
-      w1 >= w2 && (w2 <= addressable_width || e1 = e2)
+      w1 >= w2 && (w2 <= addressable_width || Bitvector.compare_endian e1 e2 = 0)
 
     let equal i1 i2 : bool = precedes i1 i2 && precedes i2 i1
 
@@ -266,7 +268,7 @@ end = struct
   let get_idx (v : t) : idx = WordSet.bitwidth v.data, v.endian
 
   let idx_equal (w1, e1 : idx) (w2, e2 : idx) : bool =
-    w1 = w2 && (w1 <= addressable_width || e1 = e2)
+    w1 = w2 && (w1 <= addressable_width || Bitvector.compare_endian e1 e2 = 0)
 
   let lift_in (f : WordSet.t -> 'a) (v : t) : 'a = f v.data
 
@@ -329,7 +331,7 @@ end = struct
   let cast_seq (sz, e : idx) (v : t) : WordSet.t seq =
     (* TODO: if v has size < 8, this could result in an unnecessary
        loss of precision at replication *)
-    let sz = if e = v.endian then sz else addressable_width in
+    let sz = if Bitvector.compare_endian e v.endian = 0 then sz else addressable_width in
     let w, e = get_idx v in
     let top = Seq.singleton @@ WordSet.top sz in
     let p = replicate_wordset v.data sz in
@@ -464,7 +466,7 @@ let meet_add : t -> key:Key.t -> data:Val.t -> t = op_add Val.meet_poly
 *)
 let add (m : t) ~key : data:Val.t -> t =
   (* TODO: op is unsound in the case that d' is longer than d*)
-  if Key.lower key = Key.upper key then op_add (fun d _ -> d) m ~key
+  if Word.(Key.lower key = Key.upper key) then op_add (fun d _ -> d) m ~key
   else join_add m ~key
 
 (* Retrieves a WORDSET representing the set of possible values stored
@@ -480,8 +482,8 @@ let find' (i : Val.idx) (m : itree) (k : Key.t) : Val.t =
        only one intersection.
     *)
     Seq.fold ints ~init:hd ~f:(fun v (k',v') ->
-        let lo_key_start = min (Key.lower k) (Key.lower k') in
-        let hi_key_start = max (Key.lower k) (Key.lower k') in
+        let lo_key_start = Word.(min (Key.lower k) (Key.lower k')) in
+        let hi_key_start = Word.(max (Key.lower k) (Key.lower k')) in
         let keys_aligned =
           Word.is_zero (Word.modulo (Word.sub hi_key_start lo_key_start)
                           (Word.of_int (fst i) ~width:(Addr.bitwidth lo_key_start))) in

vsa/value_set/lib/src/cbat_lattice_intf.ml

@@ -139,7 +139,7 @@ end = struct
   let meet a b = a && b
   let join a b = a || b
   let widen_join = join
-  let equal a b = a = b
+  let equal = Bool.(=)
   let precedes a b = (not a) || b (* definition of classical implication *)
 
   let pp ppf (b : t) = Format.fprintf ppf (if b then "top" else "bottom")

vsa/value_set/lib/src/cbat_vsa.ml

@@ -262,7 +262,7 @@ let rec denote_exp (e : exp) (env : AI.t) : val_t or_type_error =
     let sz = Size.in_bits s in
     let exp = Type.imm sz in
     let u_type_error = Type.Error.bad_type ~exp ~got:u_typ in
-    monadic_assert (exp = u_typ) u_type_error >>= fun () ->
+    monadic_assert Type.(exp = u_typ) u_type_error >>= fun () ->
     denote_exp a env >>= val_as_imm >>= fun addr ->
     denote_exp m env >>= val_as_mem >>= fun mv ->
     denote_exp u env >>= val_as_imm >>= fun v ->
@@ -364,7 +364,7 @@ let denote_jump (denote_call : sub:tid -> AI.t -> target:tid -> AI.t)
       Format.printf "//Assuming a well-formed call-return control flow@.";
       match Call.return c with
         | None -> AI.bottom
-        | Some (Direct tid) when not (target = tid) -> AI.bottom
+        | Some (Direct tid) when compare_tid target tid <> 0 -> AI.bottom
         | Some (Indirect _)
         | Some (Direct _) ->
           (* In this case, the call might return to target *)
@@ -376,7 +376,7 @@ let denote_jump (denote_call : sub:tid -> AI.t -> target:tid -> AI.t)
       | Int _ -> not_implemented ~top:AI.top "interrupt denotation"
       | Call c -> inspect_call c
       | Goto (Direct tid)
-      | Ret (Direct tid) ->  if target = tid then env else AI.bottom
+      | Ret (Direct tid) ->  if compare_tid target tid = 0 then env else AI.bottom
       | Goto (Indirect _)
       | Ret (Indirect _) -> env
       end

vsa/value_set/plugin/value_set.ml

@@ -30,11 +30,12 @@ let main (sub : string option) (fail_not_impl : bool) (unsound_stack : bool) (sh
   Utils.unsound_stack := unsound_stack;
   let prog = Project.program proj in
   let prog = match sub with
-  | Some sname -> Term.filter sub_t prog ~f:(fun s -> sname = Sub.name s)
+  | Some sname -> Term.filter sub_t prog ~f:(fun s -> String.(sname = Sub.name s))
   | None -> prog in
   let process_sub s =
     let sname = Sub.name s in
-    if Option.value ~default:sname sub = sname then begin
+    let vname = Option.value ~default:sname sub in
+    if String.(sname = vname) then begin
       if show_vsa then Format.printf "Analyzing routine %s@." sname;
       let vsa = Vsa.static_graph_vsa [] prog s (Vsa.init_sol s) in
       Term.concat_map blk_t s ~f:begin fun b ->