[sledge] Switch from Base.Hash_set to CCHashSet

Reviewed By: ngorogiannis

Differential Revision: D24306099

fbshipit-source-id: 673179d90
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent b6a77f6567
commit 08da86ae62

@ -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

@ -10,6 +10,7 @@
include NS0
module Array = Array
module Float = Float
module HashSet = HashSet
module IArray = IArray
include IArray.Import
module Int = Int

@ -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 *)

@ -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 *)

@ -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))

@ -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

@ -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

@ -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

Loading…
Cancel
Save