[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

@@ -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 ->
+    List.find_map ~f:(Llair.Func.find pgm.functions) entry_points
-        Llair.Func.find pgm.functions (Var.program ~global:() name) )
     |> function
     | Some {name= {var}; locals; params= []; entry} ->
         Some

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
 

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

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

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 ->
+    List.fold functions
-        Map.add_exn m ~key:func.name.var ~data:func )
+      ~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

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

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)
+  | Some callee -> (lookup (Var.name callee), q)
-  | None -> ([], st)
+  | None -> ([], q)
 
 type summary = {xs: Var.Set.t; foot: t; post: t}