From 55dfce6f88b4ce53482bc92d8a748012ce521389 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:37:50 -0800
Subject: [PATCH] [sledge] Add LLAIR expression form for function names

Summary:
Distinguish expressions that name functions from registers. This leads
to clearer code, and function names are semantically distinct from
general registers. In particular, they are constant, so any machinery
for handling assignment does not need to consider them. Unlike general
globals, they never have initializer expressions, and in particular
not recursive initializers. This diff only adds the distinction to
LLAIR, it is not pushed through to FOL, which will come later.

Reviewed By: jvillard

Differential Revision: D24846672

fbshipit-source-id: 2101f353f
---
 sledge/cli/domain_itv.ml           |  9 ++--
 sledge/cli/frontend.ml             | 27 ++++++++----
 sledge/cli/sledge_cli.ml           | 13 ++++--
 sledge/src/control.ml              | 49 ++++++++++-----------
 sledge/src/control.mli             |  4 +-
 sledge/src/domain_intf.ml          |  7 ++-
 sledge/src/domain_sh.ml            |  6 +--
 sledge/src/domain_unit.ml          |  4 +-
 sledge/src/domain_used_globals.ml  | 16 +++----
 sledge/src/domain_used_globals.mli |  4 +-
 sledge/src/llair/exp.ml            | 53 +++++++++++++++-------
 sledge/src/llair/exp.mli           | 26 +++++++++--
 sledge/src/llair/function.ml       | 10 +++++
 sledge/src/llair/function.mli      | 12 +++++
 sledge/src/llair/llair.ml          | 70 ++++++++++++++++--------------
 sledge/src/llair/llair.mli         | 18 +++++---
 sledge/src/llair_to_Fol.ml         |  5 +++
 sledge/src/llair_to_Fol.mli        |  1 +
 sledge/src/report.ml               |  7 +--
 19 files changed, 218 insertions(+), 123 deletions(-)
 create mode 100644 sledge/src/llair/function.ml
 create mode 100644 sledge/src/llair/function.mli

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 4667d170c..f3ebcfb78 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -65,7 +65,8 @@ let rec apron_typ_of_llair_typ : Llair.Typ.t -> Texpr1.typ option = function
 
 let rec apron_texpr_of_llair_exp exp q =
   match (exp : Llair.Exp.t) with
-  | Reg {name} -> Some (Texpr1.Var (apron_var_of_name name))
+  | Reg {name} | Function {name} ->
+      Some (Texpr1.Var (apron_var_of_name name))
   | Integer {data} -> Some (Texpr1.Cst (Coeff.s_of_int (Z.to_int data)))
   | Float {data} -> (
     match Float.of_string_exn data with
@@ -198,7 +199,7 @@ let exec_inst i q =
 
 (** Treat any intrinsic function as havoc on the return register [aret] *)
 let exec_intrinsic ~skip_throw:_ aret i _ pre =
-  let name = Llair.Reg.name i in
+  let name = Llair.Function.name i in
   if
     List.exists
       [ "malloc"
@@ -302,8 +303,8 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
 let dnf q = [q]
 
 let resolve_callee lookup ptr q =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), q)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, q)
   | None -> ([], q)
 
 type summary = t
diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index dbdee9567..2b8fc867c 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -18,7 +18,7 @@ let pp_llblock fs t =
   Format.pp_print_string fs (Llvm.string_of_llvalue (Llvm.value_of_block t))
 
 ;;
-Reg.demangle :=
+Exp.demangle :=
   let open Ctypes in
   let cxa_demangle =
     (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
@@ -452,7 +452,12 @@ and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Inst.t list * Exp.t
     | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
      |Argument ->
         ([], Exp.reg (xlate_name x llv))
-    | Function | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
+    | Function ->
+        ( []
+        , Exp.function_
+            (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv))
+        )
+    | GlobalVariable -> ([], Exp.reg (xlate_global x llv).reg)
     | GlobalAlias -> xlate_value x (Llvm.operand llv 0)
     | ConstantInt -> ([], xlate_int x llv)
     | ConstantFP -> ([], xlate_float x llv)
@@ -916,7 +921,11 @@ let pp_code fs (insts, term, blocks) =
 
 let rec xlate_func_name x llv =
   match Llvm.classify_value llv with
-  | Function | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
+  | Function ->
+      ( []
+      , Exp.function_
+          (Function.mk (xlate_type x (Llvm.type_of llv)) (find_name llv)) )
+  | GlobalVariable -> ([], Exp.reg (xlate_name x ~global:() llv))
   | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
   | Argument | Instruction _ -> xlate_value x llv
   | GlobalAlias -> xlate_func_name x (Llvm.operand llv 0)
@@ -1424,21 +1433,23 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
 
 let report_undefined func name =
   if Option.is_some (Llvm.use_begin func) then
-    [%Trace.info "undefined function: %a" Global.pp name]
+    [%Trace.info "undefined function: %a" Function.pp name]
 
 let xlate_function : x -> Llvm.llvalue -> Llair.func =
  fun x llf ->
   [%Trace.call fun {pf} -> pf "%a" pp_llvalue llf]
   ;
   undef_count := 0 ;
-  let name = xlate_global x llf in
+  let loc = find_loc llf in
+  let typ = xlate_type x (Llvm.type_of llf) in
+  let name = Function.mk typ (find_name llf) in
   let formals =
     Llvm.fold_left_params
       (fun rev_args param -> xlate_name x param :: rev_args)
       [] llf
   in
   let freturn =
-    match Reg.typ name.reg with
+    match typ with
     | Pointer {elt= Function {return= Some typ; _}} ->
         Some (Reg.program typ "freturn")
     | _ -> None
@@ -1466,10 +1477,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
+      Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc
   | At_end _ ->
       report_undefined llf name ;
-      Func.mk_undefined ~name ~formals ~freturn ~fthrow )
+      Func.mk_undefined ~name ~formals ~freturn ~fthrow ~loc )
   |>
   [%Trace.retn fun {pf} -> pf "@\n%a" Func.pp]
 
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index c7ce96d83..5aeb3a79f 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -75,6 +75,14 @@ let unmarshal file () =
     ~f:(fun ic -> (Marshal.from_channel ic : Llair.program))
     file
 
+let entry_points =
+  let void_to_void =
+    Llair.Typ.pointer
+      ~elt:(Llair.Typ.function_ ~args:IArray.empty ~return:None)
+  in
+  List.map (Config.find_list "entry-points") ~f:(fun name ->
+      Llair.Function.mk void_to_void name )
+
 let used_globals pgm preanalyze : Domain_used_globals.r =
   if preanalyze then
     let summary_table =
@@ -82,12 +90,12 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
         { bound= 1
         ; skip_throw= false
         ; function_summaries= true
-        ; entry_points= Config.find_list "entry-points"
+        ; entry_points
         ; globals= Declared Llair.Reg.Set.empty }
         pgm
     in
     Per_function
-      (Llair.Reg.Map.map summary_table ~f:Llair.Reg.Set.union_list)
+      (Llair.Function.Map.map summary_table ~f:Llair.Reg.Set.union_list)
   else
     Declared
       (Llair.Reg.Set.of_iter
@@ -128,7 +136,6 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
-    let entry_points = Config.find_list "entry-points" in
     let skip_throw = not exceptions in
     Domain_sh.simplify_states := not no_simplify_states ;
     Timer.enabled := stats ;
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 3a0abe908..2de05504e 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -13,7 +13,7 @@ type exec_opts =
   { bound: int
   ; skip_throw: bool
   ; function_summaries: bool
-  ; entry_points: string list
+  ; entry_points: Llair.Function.t list
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) = struct
@@ -258,16 +258,14 @@ module Make (Dom : Domain_intf.Dom) = struct
   let exec_jump stk state block Llair.{dst; retreating} =
     Work.add ~prev:block ~retreating stk state dst
 
-  module RegTbl = HashTable.Make (Llair.Reg)
-
-  let summary_table = RegTbl.create ()
+  let summary_table = Llair.Function.Tbl.create ()
 
   let exec_call opts stk state block call globals =
     let Llair.{callee; actuals; areturn; return; recursive} = call in
     let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
-      pf "%a from %a with state@ %a" Llair.Reg.pp name.reg Llair.Reg.pp
-        return.dst.parent.name.reg Dom.pp state]
+      pf "%a from %a with state@ %a" Llair.Function.pp name
+        Llair.Function.pp return.dst.parent.name Dom.pp state]
     ;
     let dnf_states =
       if opts.function_summaries then Dom.dnf state else [state]
@@ -281,7 +279,7 @@ module Make (Dom : Domain_intf.Dom) = struct
           else
             let maybe_summary_post =
               let state = fst (domain_call ~summaries:false state) in
-              let* summary = RegTbl.find summary_table name.reg in
+              let* summary = Llair.Function.Tbl.find summary_table name in
               List.find_map ~f:(Dom.apply_summary state) summary
             in
             [%Trace.info
@@ -310,27 +308,26 @@ module Make (Dom : Domain_intf.Dom) = struct
   let pp_st () =
     [%Trace.printf
       "@[<v>%t@]" (fun fs ->
-          RegTbl.iteri summary_table ~f:(fun ~key ~data ->
-              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Reg.pp key
+          Llair.Function.Tbl.iteri summary_table ~f:(fun ~key ~data ->
+              Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Llair.Function.pp key
                 (List.pp "@," Dom.pp_summary)
                 data ) )]
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
     let Llair.{name; formals; freturn; locals} = block.parent in
-    [%Trace.call fun {pf} -> pf "from: %a" Llair.Reg.pp name.reg]
+    [%Trace.call fun {pf} -> pf "from: %a" Llair.Function.pp name]
     ;
     let summarize post_state =
       if not opts.function_summaries then post_state
       else
-        let globals =
-          Domain_used_globals.by_function opts.globals name.reg
-        in
+        let globals = Domain_used_globals.by_function opts.globals name in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
             ~formals:
               (Llair.Reg.Set.union (Llair.Reg.Set.of_list formals) globals)
         in
-        RegTbl.add_multi ~key:name.reg ~data:function_summary summary_table ;
+        Llair.Function.Tbl.add_multi ~key:name ~data:function_summary
+          summary_table ;
         pp_st () ;
         post_state
     in
@@ -350,8 +347,7 @@ module Make (Dom : Domain_intf.Dom) = struct
         (* Create and store a function summary for main *)
         if
           opts.function_summaries
-          && List.exists opts.entry_points
-               ~f:(String.equal (Llair.Reg.name name.reg))
+          && List.exists ~f:(Llair.Function.equal name) opts.entry_points
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -359,7 +355,7 @@ module Make (Dom : Domain_intf.Dom) = struct
 
   let exec_throw stk pre_state (block : Llair.block) exc =
     let func = block.parent in
-    [%Trace.call fun {pf} -> pf "from %a" Llair.Reg.pp func.name.reg]
+    [%Trace.call fun {pf} -> pf "from %a" Llair.Function.pp func.name]
     ;
     let unwind formals scope from_call state =
       Dom.retn formals (Some func.fthrow) from_call
@@ -424,7 +420,7 @@ module Make (Dom : Domain_intf.Dom) = struct
               Dom.exec_assume state
                 (Llair.Exp.eq ptr
                    (Llair.Exp.label
-                      ~parent:(Llair.Reg.name jump.dst.parent.name.reg)
+                      ~parent:(Llair.Function.name jump.dst.parent.name)
                       ~name:jump.dst.lbl))
             with
             | Some state -> exec_jump stk state block jump |> Work.seq x
@@ -440,7 +436,7 @@ module Make (Dom : Domain_intf.Dom) = struct
             List.fold callees Work.skip ~f:(fun callee x ->
                 ( match
                     Dom.exec_intrinsic ~skip_throw:opts.skip_throw areturn
-                      callee.name.reg actuals state
+                      callee.name actuals state
                   with
                 | Some None ->
                     Report.invalid_access_term
@@ -454,7 +450,7 @@ module Make (Dom : Domain_intf.Dom) = struct
                 | None ->
                     exec_call opts stk state block {call with callee}
                       (Domain_used_globals.by_function opts.globals
-                         callee.name.reg) )
+                         callee.name) )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->
@@ -495,13 +491,13 @@ module Make (Dom : Domain_intf.Dom) = struct
       ~f:(fun entry_point -> Llair.Func.find entry_point pgm.functions)
       opts.entry_points
     |> function
-    | Some {name= {reg}; formals= []; freturn; locals; entry} ->
+    | Some {name; formals= []; freturn; locals; entry} ->
         Some
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
                    ~globals:
-                     (Domain_used_globals.by_function opts.globals reg)
+                     (Domain_used_globals.by_function opts.globals name)
                    ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
                    (Dom.init pgm.globals)))
              entry)
@@ -513,9 +509,12 @@ module Make (Dom : Domain_intf.Dom) = struct
     | Some work -> Work.run ~f:(exec_block opts pgm) (work opts.bound)
     | None -> fail "no applicable harness" ()
 
-  let compute_summaries opts pgm : Dom.summary list Llair.Reg.Map.t =
+  let compute_summaries opts pgm : Dom.summary list Llair.Function.Map.t =
     assert opts.function_summaries ;
     exec_pgm opts pgm ;
-    RegTbl.fold summary_table Llair.Reg.Map.empty ~f:(fun ~key ~data map ->
-        match data with [] -> map | _ -> Llair.Reg.Map.add ~key ~data map )
+    Llair.Function.Tbl.fold summary_table Llair.Function.Map.empty
+      ~f:(fun ~key ~data map ->
+        match data with
+        | [] -> map
+        | _ -> Llair.Function.Map.add ~key ~data map )
 end
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index a528e59e0..3dc3a5545 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -11,12 +11,12 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
-  ; entry_points: string list
+  ; entry_points: Llair.Function.t list
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) : sig
   val exec_pgm : exec_opts -> Llair.program -> unit
 
   val compute_summaries :
-    exec_opts -> Llair.program -> Dom.summary list Llair.Reg.Map.t
+    exec_opts -> Llair.program -> Dom.summary list Llair.Function.Map.t
 end
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index 65fdaa8e1..57688cccd 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -23,7 +23,7 @@ module type Dom = sig
   val exec_intrinsic :
        skip_throw:bool
     -> Llair.Reg.t option
-    -> Llair.Reg.t
+    -> Llair.Function.t
     -> Llair.Exp.t list
     -> t
     -> t option option
@@ -45,7 +45,10 @@ module type Dom = sig
   val retn : Llair.Reg.t list -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
-    (string -> Llair.func list) -> Llair.Exp.t -> t -> Llair.func list * t
+       (Llair.Function.t -> Llair.func list)
+    -> Llair.Exp.t
+    -> t
+    -> Llair.func list * t
 
   val recursion_beyond_bound : [`skip | `prune]
 
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 34988aca2..fc61d8612 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -69,7 +69,7 @@ let exec_inst inst pre =
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =
-  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.reg i)
+  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.func i)
     (List.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
@@ -236,8 +236,8 @@ let retn formals freturn {areturn; unshadow; frame} q =
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let resolve_callee lookup ptr q =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), q)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, q)
   | None -> ([], q)
 
 let recursion_beyond_bound = `prune
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index fd494b79d..5d0ffb849 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -32,8 +32,8 @@ let retn _ _ _ _ = ()
 let dnf () = [()]
 
 let resolve_callee lookup ptr _ =
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), ())
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, ())
   | None -> ([], ())
 
 type summary = unit
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 82be51b26..9b2c57c42 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -43,7 +43,7 @@ let exec_inst inst st =
     Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
 let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
-  let name = Llair.Reg.name intrinsic in
+  let name = Llair.Function.name intrinsic in
   if
     List.exists
       [ "malloc"
@@ -79,8 +79,8 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
 
 let resolve_callee lookup ptr st =
   let st = used_globals ptr st in
-  match Llair.Reg.of_exp ptr with
-  | Some callee -> (lookup (Llair.Reg.name callee), st)
+  match Llair.Function.of_exp ptr with
+  | Some callee -> (lookup callee, st)
   | None -> ([], st)
 
 (* A function summary is the set of global registers accessed by that
@@ -94,22 +94,22 @@ let apply_summary st summ = Some (Llair.Reg.Set.union st summ)
 (** Query *)
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
+  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
   | Declared of Llair.Reg.Set.t
 
-let by_function : r -> Llair.Reg.t -> t =
+let by_function : r -> Llair.Function.t -> t =
  fun s fn ->
-  [%Trace.call fun {pf} -> pf "%a" Llair.Reg.pp fn]
+  [%Trace.call fun {pf} -> pf "%a" Llair.Function.pp fn]
   ;
   ( match s with
   | Declared set -> set
   | Per_function map -> (
-    match Llair.Reg.Map.find fn map with
+    match Llair.Function.Map.find fn map with
     | Some gs -> gs
     | None ->
         fail
           "main analysis reached function %a that was not reached by \
            used-globals pre-analysis "
-          Llair.Reg.pp fn () ) )
+          Llair.Function.pp fn () ) )
   |>
   [%Trace.retn fun {pf} r -> pf "%a" Llair.Reg.Set.pp r]
diff --git a/sledge/src/domain_used_globals.mli b/sledge/src/domain_used_globals.mli
index e858a03ec..2fe681252 100644
--- a/sledge/src/domain_used_globals.mli
+++ b/sledge/src/domain_used_globals.mli
@@ -10,8 +10,8 @@
 include Domain_intf.Dom with type summary = Llair.Reg.Set.t
 
 type r =
-  | Per_function of Llair.Reg.Set.t Llair.Reg.Map.t
+  | Per_function of Llair.Reg.Set.t Llair.Function.Map.t
       (** per-function used-globals map *)
   | Declared of Llair.Reg.Set.t  (** program-wide set *)
 
-val by_function : r -> Llair.Reg.t -> summary
+val by_function : r -> Llair.Function.t -> summary
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 7cd7d92b8..896a65c9f 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -63,6 +63,7 @@ module T = struct
 
   type t =
     | Reg of {name: string; global: bool; typ: Typ.t}
+    | Function of {name: string; typ: Typ.t [@ignore]}
     | Label of {parent: string; name: string}
     | Integer of {data: Z.t; typ: Typ.t}
     | Float of {data: string; typ: Typ.t}
@@ -81,6 +82,15 @@ module Set = struct
 end
 
 module Map = Map.Make (T)
+module Tbl = HashTable.Make (T)
+
+let demangle = ref (fun _ -> None)
+
+let pp_demangled ppf name =
+  match !demangle name with
+  | Some demangled when not (String.equal name demangled) ->
+      Format.fprintf ppf "“%s”" demangled
+  | _ -> ()
 
 let pp_op2 fs op =
   let pf fmt = Format.fprintf fs fmt in
@@ -120,6 +130,7 @@ let rec pp fs exp =
   match exp with
   | Reg {name; global= true} -> pf "%@%s" name
   | Reg {name; global= false} -> pf "%%%s" name
+  | Function {name} -> pf "&%s%a" name pp_demangled name
   | Label {name} -> pf "%s" name
   | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
   | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
@@ -162,6 +173,8 @@ let rec invariant exp =
   let@ () = Invariant.invariant [%here] exp [%sexp_of: t] in
   match exp with
   | Reg {typ} -> assert (Typ.is_sized typ)
+  | Function {typ= Pointer {elt= Function _}} -> ()
+  | Function _ -> assert false
   | Integer {data; typ} -> (
     match typ with
     | Integer {bits} ->
@@ -238,7 +251,7 @@ let rec invariant exp =
 
 and typ_of exp =
   match exp with
-  | Reg {typ} | Integer {typ} | Float {typ} -> typ
+  | Reg {typ} | Function {typ} | Integer {typ} | Float {typ} -> typ
   | Label _ -> Typ.ptr
   | Ap1 ((Signed _ | Unsigned _ | Convert _ | Splat), dst, _) -> dst
   | Ap1 (Select idx, typ, _) -> (
@@ -277,19 +290,6 @@ module Reg = struct
     let pp = Set.pp pp_exp
   end
 
-  module Map = Map
-
-  let demangle = ref (fun _ -> None)
-
-  let pp_demangled fs = function
-    | Reg {name} -> (
-      match !demangle name with
-      | Some demangled when not (String.equal name demangled) ->
-          Format.fprintf fs "“%s”" demangled
-      | _ -> () )
-    | _ -> ()
-    [@@warning "-9"]
-
   let invariant x =
     let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
     match x with Reg _ -> invariant x | _ -> assert false
@@ -297,7 +297,7 @@ module Reg = struct
   let name = function Reg x -> x.name | r -> violates invariant r
   let typ = function Reg x -> x.typ | r -> violates invariant r
   let is_global = function Reg x -> x.global | r -> violates invariant r
-  let of_ = function Reg _ as r -> r | _ -> invalid_arg "Reg.of_"
+  let pp_demangled ppf r = pp_demangled ppf (name r)
 
   let of_exp = function
     | Reg _ as e -> Some (e |> check invariant)
@@ -307,6 +307,28 @@ module Reg = struct
     Reg {name; global= Option.is_some global; typ} |> check invariant
 end
 
+(** Function names are the expressions constructed by [Function] *)
+module Function = struct
+  include T
+
+  let pp = pp
+  let name = function Function x -> x.name | r -> violates invariant r
+  let typ = function Function x -> x.typ | r -> violates invariant r
+
+  let invariant x =
+    let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+    match x with Function _ -> invariant x | _ -> assert false
+
+  let of_exp = function
+    | Function _ as e -> Some (e |> check invariant)
+    | _ -> None
+
+  let mk typ name = Function {name; typ} |> check invariant
+
+  module Map = Map
+  module Tbl = Tbl
+end
+
 (** Construct *)
 
 (* registers *)
@@ -315,6 +337,7 @@ let reg x = x
 
 (* constants *)
 
+let function_ f = f
 let label ~parent ~name = Label {parent; name} |> check invariant
 let integer typ data = Integer {data; typ} |> check invariant
 let null = integer Typ.ptr Z.zero
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 3e701d046..1f0b7a32c 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -73,6 +73,7 @@ type opN = Record  (** Record (array / struct) constant *)
 
 type t = private
   | Reg of {name: string; global: bool; typ: Typ.t}  (** Virtual register *)
+  | Function of {name: string; typ: Typ.t [@ignore]}  (** Function name *)
   | Label of {parent: string; name: string}
       (** Address of named code block within parent function *)
   | Integer of {data: Z.t; typ: Typ.t}  (** Integer constant *)
@@ -87,6 +88,8 @@ val pp : t pp
 
 include Invariant.S with type t := t
 
+val demangle : (string -> string option) ref
+
 (** Exp.Reg is re-exported as Reg *)
 module Reg : sig
   type exp := t
@@ -100,15 +103,11 @@ module Reg : sig
     val pp : t pp
   end
 
-  module Map : Map.S with type key := t
-
-  val demangle : (string -> string option) ref
   val pp : t pp
   val pp_demangled : t pp
 
   include Invariant.S with type t := t
 
-  val of_ : exp -> t
   val of_exp : exp -> t option
   val program : ?global:unit -> Typ.t -> string -> t
   val name : t -> string
@@ -116,12 +115,31 @@ module Reg : sig
   val is_global : t -> bool
 end
 
+(** Exp.Function is re-exported as Function *)
+module Function : sig
+  type exp := t
+  type t = private exp [@@deriving compare, equal, hash, sexp]
+
+  module Map : Map.S with type key := t
+  module Tbl : HashTable.S with type key := t
+
+  val pp : t pp
+
+  include Invariant.S with type t := t
+
+  val of_exp : exp -> t option
+  val mk : Typ.t -> string -> t
+  val name : t -> string
+  val typ : t -> Typ.t
+end
+
 (** Construct *)
 
 (* registers *)
 val reg : Reg.t -> t
 
 (* constants *)
+val function_ : Function.t -> t
 val label : parent:string -> name:string -> t
 val null : t
 val bool : bool -> t
diff --git a/sledge/src/llair/function.ml b/sledge/src/llair/function.ml
new file mode 100644
index 000000000..d6efda53a
--- /dev/null
+++ b/sledge/src/llair/function.ml
@@ -0,0 +1,10 @@
+(*
+ * 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.
+ *)
+
+(** Function names *)
+
+include Exp.Function
diff --git a/sledge/src/llair/function.mli b/sledge/src/llair/function.mli
new file mode 100644
index 000000000..09c61ca99
--- /dev/null
+++ b/sledge/src/llair/function.mli
@@ -0,0 +1,12 @@
+(*
+ * 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.
+ *)
+
+(** Function names *)
+
+include module type of struct
+  include Exp.Function
+end
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 7be1ade09..0f13731cd 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -13,6 +13,7 @@ module Loc = Loc
 module Typ = Typ
 module Reg = Reg
 module Exp = Exp
+module Function = Function
 module Global = Global
 
 type inst =
@@ -59,12 +60,13 @@ and block =
   ; mutable sort_index: int }
 
 and func =
-  { name: Global.t
+  { name: Function.t
   ; formals: Reg.t list
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t
-  ; entry: block }
+  ; entry: block
+  ; loc: Loc.t }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -104,23 +106,24 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
     { lbl: label
     ; cmnd: cmnd
     ; term: term
-    ; parent: Reg.t = parent.name.reg
+    ; parent: Function.t = parent.name
     ; sort_index: int }]
 
-let sexp_of_func {name; formals; freturn; fthrow; locals; entry} =
+let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} =
   [%sexp
-    { name: Global.t
+    { name: Function.t
     ; formals: Reg.t list
     ; freturn: Reg.t option
     ; fthrow: Reg.t
     ; locals: Reg.Set.t
-    ; entry: block }]
+    ; entry: block
+    ; loc: Loc.t }]
 
 (* blocks in a [t] are uniquely identified by [sort_index] *)
 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 String.Map.t [@@deriving sexp_of]
+type functions = func Function.Map.t [@@deriving sexp_of]
 
 type program = {globals: Global.t iarray; functions: functions}
 [@@deriving sexp_of]
@@ -219,13 +222,16 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
-  let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
-  { name= Global.mk dummy_reg Loc.none
+  { name=
+      Function.mk
+        (Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None))
+        "dummy"
   ; formals= []
   ; freturn= None
-  ; fthrow= dummy_reg
+  ; fthrow= Reg.program Typ.ptr "dummy"
   ; locals= Reg.Set.empty
-  ; entry= dummy_block }
+  ; entry= dummy_block
+  ; loc= Loc.none }
 
 (** Instructions *)
 
@@ -387,14 +393,14 @@ module Block_label = struct
     type t = block [@@deriving sexp_of]
 
     let compare x y =
-      [%compare: string * Global.t] (x.lbl, x.parent.name)
+      [%compare: string * Function.t] (x.lbl, x.parent.name)
         (y.lbl, y.parent.name)
 
     let equal x y =
-      [%equal: string * Global.t] (x.lbl, x.parent.name)
+      [%equal: string * Function.t] (x.lbl, x.parent.name)
         (y.lbl, y.parent.name)
 
-    let hash b = [%hash: string * Global.t] (b.lbl, b.parent.name)
+    let hash b = [%hash: string * Function.t] (b.lbl, b.parent.name)
   end
 
   include T
@@ -403,7 +409,7 @@ end
 
 module BlockS = HashSet.Make (Block_label)
 module BlockQ = HashQueue.Make (Block_label)
-module FuncQ = HashQueue.Make (Reg)
+module FuncQ = HashQueue.Make (Function)
 
 (** Functions *)
 
@@ -437,16 +443,16 @@ module Func = struct
   let entry_cfg func = fold_cfg ~f:(fun blk cfg -> blk :: cfg) func []
 
   let pp fs func =
-    let {name; formals; freturn; entry; _} = func in
+    let {name; formals; freturn; entry; loc; _} = func in
     let {cmnd; term; sort_index; _} = entry in
     let pp_if cnd str fs = if cnd then Format.fprintf fs str in
     Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
       (Option.pp "%a " Typ.pp)
-      ( match Reg.typ name.reg with
+      ( match Function.typ name with
       | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
       (Option.pp " %a := " Reg.pp)
-      freturn Global.pp name (pp_actuals pp_formal) formals
+      freturn Function.pp name (pp_actuals pp_formal) formals
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
@@ -454,7 +460,7 @@ module Func = struct
             List.sort ~cmp:Block.compare (List.tl_exn (entry_cfg func))
           in
           Format.fprintf fs " { #%i %a@;<1 4>@[<v>%a@ %a@]%t%a@]@ }"
-            sort_index Loc.pp name.loc pp_cmnd cmnd Term.pp term
+            sort_index Loc.pp loc pp_cmnd cmnd Term.pp term
             (pp_if (not (List.is_empty cfg)) "@ @   ")
             (List.pp "@\n@\n  " Block.pp)
             cfg )
@@ -462,7 +468,7 @@ module Func = struct
   let invariant func =
     assert (func == func.entry.parent) ;
     let@ () = Invariant.invariant [%here] func [%sexp_of: t] in
-    match Reg.typ func.name.reg with
+    match Function.typ func.name with
     | Pointer {elt= Function {return; _}; _} ->
         assert (
           not
@@ -475,9 +481,9 @@ module Func = struct
         iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
-  let find functions name = String.Map.find functions name
+  let find functions name = Function.Map.find functions name
 
-  let mk ~(name : Global.t) ~formals ~freturn ~fthrow ~entry ~cfg =
+  let mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc =
     let locals =
       let locals_cmnd locals cmnd =
         IArray.fold_right ~f:Inst.union_locals cmnd locals
@@ -487,7 +493,7 @@ module Func = struct
       in
       IArray.fold ~f:locals_block cfg (locals_block entry Reg.Set.empty)
     in
-    let func = {name; formals; freturn; fthrow; locals; entry} in
+    let func = {name; formals; freturn; fthrow; locals; entry; loc} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
@@ -522,13 +528,13 @@ end
 let set_derived_metadata functions =
   let compute_roots functions =
     let roots = FuncQ.create () in
-    String.Map.iter functions ~f:(fun func ->
-        FuncQ.enqueue_back_exn roots func.name.reg func ) ;
-    String.Map.iter functions ~f:(fun func ->
+    Function.Map.iter functions ~f:(fun func ->
+        FuncQ.enqueue_back_exn roots func.name func ) ;
+    Function.Map.iter functions ~f:(fun func ->
         Func.iter_term func ~f:(fun term ->
             match term with
             | Call {callee; _} -> (
-              match Reg.of_exp callee with
+              match Function.of_exp callee with
               | Some callee ->
                   FuncQ.remove roots callee |> (ignore : [> ] -> unit)
               | None -> () )
@@ -553,8 +559,8 @@ let set_derived_metadata functions =
         | Iswitch {tbl; _} -> IArray.iter tbl ~f:jump
         | Call ({callee; return; throw; _} as call) ->
             ( match
-                let* reg = Reg.of_exp callee in
-                Func.find (Reg.name reg) functions
+                let* name = Function.of_exp callee in
+                Func.find name functions
               with
             | Some func ->
                 if Block_label.Set.mem func.entry ancestors then
@@ -579,8 +585,8 @@ let set_derived_metadata functions =
         index := !index - 1 )
   in
   let functions =
-    List.fold functions String.Map.empty ~f:(fun func m ->
-        String.Map.add_exn ~key:(Reg.name func.name.reg) ~data:func m )
+    List.fold functions Function.Map.empty ~f:(fun func m ->
+        Function.Map.add_exn ~key:func.name ~data:func m )
   in
   let roots = compute_roots functions in
   let tips_to_roots = topsort functions roots in
@@ -607,7 +613,7 @@ module Program = struct
       (IArray.pp "@\n@\n" Global.pp_defn)
       globals
       (List.pp "@\n@\n" Func.pp)
-      ( String.Map.values functions
+      ( Function.Map.values functions
       |> Iter.to_list
       |> List.sort ~cmp:(fun x y -> compare_block x.entry y.entry) )
 end
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index dad96f0da..640012fd1 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -12,6 +12,7 @@ module Loc = Loc
 module Typ = Typ
 module Reg = Reg
 module Exp = Exp
+module Function = Function
 module Global = Global
 
 (** Instructions for memory manipulation or other non-control effects. *)
@@ -92,12 +93,13 @@ and block = private
 (** A function is a control-flow graph with distinguished entry block, whose
     parameters are the function parameters. *)
 and func = private
-  { name: Global.t
+  { name: Function.t
   ; formals: Reg.t list  (** Formal parameters, first-param-last stack *)
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t  (** Local registers *)
-  ; entry: block }
+  ; entry: block
+  ; loc: Loc.t }
 
 type functions
 
@@ -180,25 +182,27 @@ module Func : sig
   include Invariant.S with type t := t
 
   val mk :
-       name:Global.t
+       name:Function.t
     -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
     -> cfg:block iarray
-    -> func
+    -> loc:Loc.t
+    -> t
 
   val mk_undefined :
-       name:Global.t
+       name:Function.t
     -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
+    -> loc:Loc.t
     -> t
 
-  val find : string -> functions -> func option
+  val find : Function.t -> functions -> t option
   (** Look up a function of the given name in the given functions. *)
 
-  val is_undefined : func -> bool
+  val is_undefined : t -> bool
   (** Holds of functions that are declared but not defined. *)
 end
 
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index dd26b2375..a7de81324 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -9,6 +9,10 @@ open Fol
 module T = Term
 module F = Formula
 
+let func f =
+  let name = Llair.Function.name f in
+  Var.program ~name ~global:true
+
 let reg r =
   let name = Llair.Reg.name r in
   let global = Llair.Reg.is_global r in
@@ -64,6 +68,7 @@ and term : Llair.Exp.t -> T.t =
         (F.cond ~cnd:(formula cnd) ~pos:(formula pos) ~neg:(formula neg))
   (* terms *)
   | Reg {name; global; typ= _} -> T.var (Var.program ~name ~global)
+  | Function {name; typ= _} -> T.var (Var.program ~name ~global:true)
   | Label {parent; name} ->
       uap0 (Funsym.uninterp ("label_" ^ parent ^ "_" ^ name))
   | Integer {typ= _; data} -> T.integer data
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index cc501922d..8ca00887c 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/sledge/src/llair_to_Fol.mli
@@ -7,6 +7,7 @@
 
 open Fol
 
+val func : Llair.Function.t -> Var.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
 val term : Llair.Exp.t -> Term.t
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index 29f361021..b0760aa0e 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -14,12 +14,7 @@ let unknown_call call =
       (fun fs call -> Llair.Loc.pp fs (Llair.Term.loc call))
       call
       (fun fs (call : Llair.Term.t) ->
-        match call with
-        | Call {callee} -> (
-          match Llair.Reg.of_exp callee with
-          | Some reg -> Llair.Reg.pp_demangled fs reg
-          | None -> Llair.Exp.pp fs callee )
-        | _ -> () )
+        match call with Call {callee} -> Llair.Exp.pp fs callee | _ -> () )
       call Llair.Term.pp call]
 
 let invalid_access_count = ref 0