diff --git a/vsa/explicit_edge/explicit_edge.ml b/vsa/explicit_edge/explicit_edge.ml index 552006af..270162ee 100644 --- a/vsa/explicit_edge/explicit_edge.ml +++ b/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 diff --git a/vsa/value_set/lib/cbat_value_set.opam b/vsa/value_set/lib/cbat_value_set.opam index 67efa9ff..f9f63131 100644 --- a/vsa/value_set/lib/cbat_value_set.opam +++ b/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" diff --git a/vsa/value_set/lib/src/cbat_ai_memmap.ml b/vsa/value_set/lib/src/cbat_ai_memmap.ml index bb8a1a06..5a4d0327 100644 --- a/vsa/value_set/lib/src/cbat_ai_memmap.ml +++ b/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 diff --git a/vsa/value_set/lib/src/cbat_lattice_intf.ml b/vsa/value_set/lib/src/cbat_lattice_intf.ml index 72bc1261..95ad9b55 100644 --- a/vsa/value_set/lib/src/cbat_lattice_intf.ml +++ b/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") diff --git a/vsa/value_set/lib/src/cbat_vsa.ml b/vsa/value_set/lib/src/cbat_vsa.ml index 158b2ad5..5e299473 100644 --- a/vsa/value_set/lib/src/cbat_vsa.ml +++ b/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 diff --git a/vsa/value_set/plugin/value_set.ml b/vsa/value_set/plugin/value_set.ml index e8c332e4..21591869 100644 --- a/vsa/value_set/plugin/value_set.ml +++ b/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 ->