From 08da86ae624c4bf301bc7c44b575b3a3d58e8148 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 11:41:23 -0700 Subject: [PATCH] [sledge] Switch from Base.Hash_set to CCHashSet Reviewed By: ngorogiannis Differential Revision: D24306099 fbshipit-source-id: 673179d90 --- sledge/cli/frontend.ml | 37 +++++++++++++++++++----------------- sledge/nonstdlib/NS.ml | 1 + sledge/nonstdlib/NS.mli | 2 +- sledge/nonstdlib/NS0.ml | 1 - sledge/nonstdlib/dune | 3 ++- sledge/nonstdlib/hashSet.ml | 29 ++++++++++++++++++++++++++++ sledge/nonstdlib/hashSet.mli | 18 ++++++++++++++++++ sledge/src/llair/llair.ml | 9 +++++++-- 8 files changed, 78 insertions(+), 22 deletions(-) create mode 100644 sledge/nonstdlib/hashSet.ml create mode 100644 sledge/nonstdlib/hashSet.mli diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 311b962d3..528c61cb5 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -897,7 +897,9 @@ let rec xlate_func_name x llv = | ConstantPointerNull -> todo "call null: %a" pp_llvalue llv () | _ -> todo "function kind in %a" pp_llvalue llv () -let ignored_callees = Hash_set.create (module String) +module StringS = HashSet.Make (String) + +let ignored_callees = StringS.create 0 let xlate_size_of x llv = Exp.integer Typ.siz (Z.of_int (size_of x (Llvm.type_of llv))) @@ -977,9 +979,8 @@ let xlate_instr : in let fname = Llvm.value_name llfunc in let skip msg = - ( match Hash_set.strict_add ignored_callees fname with - | Ok () -> warn "ignoring uninterpreted %s %s" msg fname () - | Error _ -> () ) ; + if StringS.add ignored_callees fname then + warn "ignoring uninterpreted %s %s" msg fname () ; let reg = xlate_name_opt x instr in emit_inst (Inst.nondet ~reg ~msg:fname ~loc) in @@ -1066,13 +1067,14 @@ let xlate_instr : Llvm.num_arg_operands instr else let fname = Llvm.value_name llfunc in - ( match Hash_set.strict_add ignored_callees fname with - | Ok () when not (Llvm.is_declaration llfunc) -> - warn - "ignoring variable arguments to variadic \ - function: %a" - Exp.pp callee () - | _ -> () ) ; + if + StringS.add ignored_callees fname + && not (Llvm.is_declaration llfunc) + then + warn + "ignoring variable arguments to variadic function: \ + %a" + Exp.pp callee () ; let llfty = Llvm.element_type lltyp in ( match Llvm.classify_type llfty with | Function -> () @@ -1103,11 +1105,12 @@ let xlate_instr : if not (Llvm.is_var_arg (Llvm.element_type lltyp)) then Llvm.num_arg_operands instr else ( - ( match Hash_set.strict_add ignored_callees fname with - | Ok () when not (Llvm.is_declaration llfunc) -> - warn "ignoring variable arguments to variadic function: %a" - Global.pp (xlate_global x llfunc) () - | _ -> () ) ; + if + StringS.add ignored_callees fname + && not (Llvm.is_declaration llfunc) + then + warn "ignoring variable arguments to variadic function: %a" + Global.pp (xlate_global x llfunc) () ; assert (Poly.(Llvm.classify_type lltyp = Pointer)) ; Array.length (Llvm.param_types (Llvm.element_type lltyp)) ) in @@ -1523,7 +1526,7 @@ let cleanup llmodule llcontext = Hashtbl.clear memo_type ; Hashtbl.clear memo_global ; Hashtbl.clear memo_value ; - Hash_set.clear ignored_callees ; + StringS.clear ignored_callees ; Gc.full_major () ; Llvm.dispose_module llmodule ; Llvm.dispose_context llcontext diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index 1de4811c5..50fca23f9 100644 --- a/sledge/nonstdlib/NS.ml +++ b/sledge/nonstdlib/NS.ml @@ -10,6 +10,7 @@ include NS0 module Array = Array module Float = Float +module HashSet = HashSet module IArray = IArray include IArray.Import module Int = Int diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index ad615f3fd..8cbb8f54c 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -147,7 +147,7 @@ module Set = Set module Map = Map module Multiset = Multiset module Hashtbl = Base.Hashtbl -module Hash_set = Base.Hash_set +module HashSet = HashSet module Hash_queue = Core_kernel.Hash_queue (** Input / Output *) diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml index 6532c468b..4dd7a2924 100644 --- a/sledge/nonstdlib/NS0.ml +++ b/sledge/nonstdlib/NS0.ml @@ -126,7 +126,6 @@ module Either = struct end module Hashtbl = Base.Hashtbl -module Hash_set = Base.Hash_set module Hash_queue = Core_kernel.Hash_queue (** Input / Output *) diff --git a/sledge/nonstdlib/dune b/sledge/nonstdlib/dune index 4307e56a1..9898b26fd 100644 --- a/sledge/nonstdlib/dune +++ b/sledge/nonstdlib/dune @@ -6,7 +6,8 @@ (library (name NS) (public_name nonstdlib) - (libraries containers core core_kernel.fheap iter zarith trace) + (libraries containers containers-data core core_kernel.fheap iter zarith + trace) (flags (:standard)) (preprocess (pps ppx_sledge ppx_trace)) diff --git a/sledge/nonstdlib/hashSet.ml b/sledge/nonstdlib/hashSet.ml new file mode 100644 index 000000000..29cc77a2c --- /dev/null +++ b/sledge/nonstdlib/hashSet.ml @@ -0,0 +1,29 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +include CCHashSet + +module Make (E : ELEMENT) = struct + include CCHashSet.Make (E) + + let update s e ~f = + let eo = find s e in + match (eo, f eo) with + | None, None -> () + | Some e, Some e' when e == e' -> () + | Some _, None -> remove s e + | _, Some e' -> insert s e' + + let add s e = + let change = ref false in + update s e ~f:(function + | None -> + change := true ; + Some e + | Some e -> Some e ) ; + !change +end diff --git a/sledge/nonstdlib/hashSet.mli b/sledge/nonstdlib/hashSet.mli new file mode 100644 index 000000000..1fbe7824c --- /dev/null +++ b/sledge/nonstdlib/hashSet.mli @@ -0,0 +1,18 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +include module type of CCHashSet with module Make := CCHashSet.Make + +module Make (E : ELEMENT) : sig + include module type of CCHashSet.Make (E) + + val add : t -> elt -> bool + (** [add s x] adds [x] into [s] and returns whether [s] was changed, that + is, [add s x = not (mem s x)] *) + + val update : t -> elt -> f:(elt option -> elt option) -> unit +end diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 7fc66f773..179e30c00 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -392,6 +392,10 @@ module Block_label = struct [%compare: string * Global.t] (x.lbl, x.parent.name) (y.lbl, y.parent.name) + let equal x y = + [%equal: string * Global.t] (x.lbl, x.parent.name) + (y.lbl, y.parent.name) + let hash b = [%hash: string * Global.t] (b.lbl, b.parent.name) end @@ -399,6 +403,7 @@ module Block_label = struct module Set = Set.Make (T) end +module BlockS = HashSet.Make (Block_label) module BlockQ = Hash_queue.Make (Block_label) module FuncQ = Hash_queue.Make (Reg) @@ -412,9 +417,9 @@ module Func = struct | _ -> false let fold_cfg ~init ~f func = - let seen = Hash_set.create (module Block_label) in + let seen = BlockS.create 0 in let rec fold_cfg_ s blk = - if Result.is_error (Hash_set.strict_add seen blk) then s + if not (BlockS.add seen blk) then s else let s = let f s j = fold_cfg_ s j.dst in