From 0c04ecc9aaa588a05b911b406a4ddd34566bd743 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 8 Oct 2019 06:24:41 -0700 Subject: [PATCH] [sledge] Change Llair representation of functions to a String map Summary: Using a type of keys richer than strings, which are the unique symbol names at the C/LLVM level, is unnecessary. Reviewed By: ngorogiannis Differential Revision: D17665262 fbshipit-source-id: 6b8c31146 --- sledge/src/control.ml | 3 +-- sledge/src/domain/domain_sig.ml | 2 +- sledge/src/domain/unit.ml | 4 ++-- sledge/src/domain/used_globals.ml | 2 +- sledge/src/llair/llair.ml | 12 ++++++++---- sledge/src/llair/llair.mli | 2 +- sledge/src/symbheap/sh_domain.ml | 6 +++--- 7 files changed, 17 insertions(+), 14 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index e3472d78d..d7780af7c 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -479,8 +479,7 @@ module Make (Dom : Domain_sig.Dom) = struct let harness : exec_opts -> Llair.t -> (int -> Work.t) option = fun opts pgm -> let entry_points = Config.find_list "entry-points" in - List.find_map entry_points ~f:(fun name -> - Llair.Func.find pgm.functions (Var.program ~global:() name) ) + List.find_map ~f:(Llair.Func.find pgm.functions) entry_points |> function | Some {name= {var}; locals; params= []; entry} -> Some diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index 70b95e4e0..26b2d169c 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -45,7 +45,7 @@ module type Dom = sig val dnf : t -> t list val resolve_callee : - (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list * t + (string -> Llair.func list) -> Exp.t -> t -> Llair.func list * t type summary diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index ce7e375f4..8b628f1cf 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -28,9 +28,9 @@ let post _ _ () = () let retn _ _ _ _ = () let dnf () = [()] -let resolve_callee lookup ptr () = +let resolve_callee lookup ptr _ = match Var.of_exp ptr with - | Some callee_name -> (lookup callee_name, ()) + | Some callee -> (lookup (Var.name callee), ()) | None -> ([], ()) type summary = unit diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index d6ec071d4..e91e39248 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -67,7 +67,7 @@ let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st = let resolve_callee lookup ptr st = let st = used_globals ~init:st ptr in match Var.of_exp ptr with - | Some callee_name -> (lookup callee_name, st) + | Some callee -> (lookup (Var.name callee), st) | None -> ([], st) (* A function summary is the set of global variables accessed by that diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index ab1b040a7..c2e72f450 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -121,7 +121,7 @@ let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} = let compare_block x y = Int.compare x.sort_index y.sort_index let equal_block x y = Int.equal x.sort_index y.sort_index -type functions = func Var.Map.t [@@deriving sexp_of] +type functions = func Map.M(String).t [@@deriving sexp_of] type t = {globals: Global.t vector; functions: functions} [@@deriving sexp_of] @@ -551,7 +551,9 @@ let set_derived_metadata functions = jump els | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump | Call ({callee; return; throw; _} as call) -> - ( match Var.of_exp callee >>= Func.find functions with + ( match + Var.of_exp callee >>| Var.name >>= Func.find functions + with | Some func -> if Set.mem ancestors func.entry then call.recursive <- true else visit ancestors func func.entry @@ -579,8 +581,10 @@ let set_derived_metadata functions = (Vector.to_array cfg) ) in let functions = - List.fold functions ~init:Var.Map.empty ~f:(fun m func -> - Map.add_exn m ~key:func.name.var ~data:func ) + List.fold functions + ~init:(Map.empty (module String)) + ~f:(fun m func -> + Map.add_exn m ~key:(Var.name func.name.var) ~data:func ) in let roots = compute_roots functions in let tips_to_roots = topsort functions roots in diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index cd02fce51..b56c4d1ad 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -191,7 +191,7 @@ module Func : sig val mk_undefined : name:Global.t -> params:Var.t list -> t - val find : functions -> Var.t -> func option + val find : functions -> string -> func option (** Look up a function of the given name in the given functions. *) val is_undefined : func -> bool diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index bc3d14967..391b406b9 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -151,10 +151,10 @@ let retn formals freturn {areturn; subst; frame} q = |> [%Trace.retn fun {pf} -> pf "%a" pp] -let resolve_callee lookup ptr st = +let resolve_callee lookup ptr q = match Var.of_exp ptr with - | Some callee_name -> (lookup callee_name, st) - | None -> ([], st) + | Some callee -> (lookup (Var.name callee), q) + | None -> ([], q) type summary = {xs: Var.Set.t; foot: t; post: t}