From 4605f505cefd89edb503827e1e3a359fa4841892 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:48:43 -0800
Subject: [PATCH] [sledge] Strengthen dynamic resolution of indirect calls

Summary:
Use the equality class information in the symbolic state to resolve
callees of indirect calls.

Reviewed By: jvillard

Differential Revision: D25146160

fbshipit-source-id: a1c39bbe1
---
 sledge/cli/domain_itv.ml          |  2 +-
 sledge/cli/sledge_cli.ml          |  8 +------
 sledge/src/control.ml             | 13 +++++------
 sledge/src/control.mli            |  2 +-
 sledge/src/domain_intf.ml         |  5 +----
 sledge/src/domain_relation.ml     |  5 ++---
 sledge/src/domain_sh.ml           |  8 +++----
 sledge/src/domain_unit.ml         |  2 +-
 sledge/src/domain_used_globals.ml |  2 +-
 sledge/src/fol/funsym.ml          |  6 +----
 sledge/src/llair/exp.ml           |  6 +++++
 sledge/src/llair/exp.mli          |  6 +++++
 sledge/src/llair/llair.ml         |  3 ++-
 sledge/src/llair/llair.mli        |  2 +-
 sledge/src/llair_to_Fol.ml        |  7 +++++-
 sledge/src/llair_to_Fol.mli       |  1 +
 sledge/test/analyze/icall.c       | 37 +++++++++++++++++++++++++++++++
 17 files changed, 78 insertions(+), 37 deletions(-)
 create mode 100644 sledge/test/analyze/icall.c

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 209b4f06e..92dae6d87 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -275,7 +275,7 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     (q''', {areturn; caller_q= q})
 
 let dnf q = [q]
-let resolve_callee _ _ q = ([], q)
+let resolve_callee _ _ _ = []
 
 type summary = t
 
diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index a18a220cc..d920af30a 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/sledge/cli/sledge_cli.ml
@@ -76,13 +76,7 @@ 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 entry_points = Config.find_list "entry-points"
 
 let used_globals pgm preanalyze : Domain_used_globals.r =
   if preanalyze then
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 1ed7f4abc..802150538 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: Llair.Function.t list
+  ; entry_points: string list
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) = struct
@@ -365,7 +365,9 @@ module Make (Dom : Domain_intf.Dom) = struct
         (* Create and store a function summary for main *)
         if
           opts.function_summaries
-          && List.exists ~f:(Llair.Function.equal name) opts.entry_points
+          && List.mem ~eq:String.equal
+               (Llair.Function.name name)
+               opts.entry_points
         then summarize exit_state |> (ignore : Dom.t -> unit) ;
         Work.skip )
     |>
@@ -435,11 +437,8 @@ module Make (Dom : Domain_intf.Dom) = struct
         exec_call opts stk state block call
           (Domain_used_globals.by_function opts.globals callee.name)
     | ICall ({callee; areturn; return} as call) -> (
-        let lookup name =
-          Option.to_list (Llair.Func.find name pgm.functions)
-        in
-        let callees, state = Dom.resolve_callee lookup callee state in
-        match callees with
+        let lookup name = Llair.Func.find name pgm.functions in
+        match Dom.resolve_callee lookup callee state with
         | [] -> exec_skip_func stk state block areturn return
         | callees ->
             List.fold callees Work.skip ~f:(fun callee x ->
diff --git a/sledge/src/control.mli b/sledge/src/control.mli
index 3dc3a5545..d97d08aef 100644
--- a/sledge/src/control.mli
+++ b/sledge/src/control.mli
@@ -11,7 +11,7 @@ type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
-  ; entry_points: Llair.Function.t list
+  ; entry_points: string list  (** C linkage names of entry points *)
   ; globals: Domain_used_globals.r }
 
 module Make (Dom : Domain_intf.Dom) : sig
diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml
index 28d564a6d..851c1323a 100644
--- a/sledge/src/domain_intf.ml
+++ b/sledge/src/domain_intf.ml
@@ -37,10 +37,7 @@ module type Dom = sig
   val retn : Llair.Reg.t iarray -> Llair.Reg.t option -> from_call -> t -> t
 
   val resolve_callee :
-       (Llair.Function.t -> Llair.func list)
-    -> Llair.Exp.t
-    -> t
-    -> Llair.func list * t
+    (string -> Llair.func option) -> Llair.Exp.t -> t -> Llair.func list
 
   val recursion_beyond_bound : [`skip | `prune]
 
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index 6eaf10e54..524fdee4b 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -99,9 +99,8 @@ module Make (State_domain : State_domain_sig) = struct
   let dnf (entry, current) =
     List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current)
 
-  let resolve_callee f e (entry, current) =
-    let callees, next = State_domain.resolve_callee f e current in
-    (callees, (entry, next))
+  let resolve_callee f e (_, current) =
+    State_domain.resolve_callee f e current
 
   type summary = State_domain.summary
 
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 9b5edff1e..7176a37f8 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -226,10 +226,10 @@ let retn formals freturn {areturn; unshadow; frame} q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
-let resolve_callee lookup ptr q =
-  match Llair.Function.of_exp ptr with
-  | Some callee -> (lookup callee, q)
-  | None -> ([], q)
+let resolve_callee lookup ptr (q : Sh.t) =
+  Context.class_of q.ctx (X.term ptr)
+  |> List.find_map ~f:(X.lookup_func lookup)
+  |> Option.to_list
 
 let recursion_beyond_bound = `prune
 
diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml
index ec81601f2..d02efde6b 100644
--- a/sledge/src/domain_unit.ml
+++ b/sledge/src/domain_unit.ml
@@ -29,7 +29,7 @@ let recursion_beyond_bound = `skip
 let post _ _ () = ()
 let retn _ _ _ _ = ()
 let dnf () = [()]
-let resolve_callee _ _ q = ([], q)
+let resolve_callee _ _ _ = []
 
 type summary = unit
 
diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml
index 2e008d373..4050a4555 100644
--- a/sledge/src/domain_used_globals.ml
+++ b/sledge/src/domain_used_globals.ml
@@ -52,7 +52,7 @@ let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~freturn:_
     ~locals:_ st =
   (empty, IArray.fold ~f:used_globals actuals st)
 
-let resolve_callee _ _ q = ([], q)
+let resolve_callee _ _ _ = []
 
 (* A function summary is the set of global registers accessed by that
    function and its transitive callees *)
diff --git a/sledge/src/fol/funsym.ml b/sledge/src/fol/funsym.ml
index 059c135db..9737eb89c 100644
--- a/sledge/src/fol/funsym.ml
+++ b/sledge/src/fol/funsym.ml
@@ -32,11 +32,7 @@ let pp ppf f =
   | BitAshr -> pf "ashr"
   | Signed n -> pf "(s%i)" n
   | Unsigned n -> pf "(u%i)" n
-  | Uninterp sym ->
-      if String.is_empty sym then pf ""
-      else if Char.equal sym.[0] '@' || Char.equal sym.[0] '%' then
-        Trace.pp_styled `Bold "%s" ppf sym
-      else pf "%s" sym
+  | Uninterp sym -> Trace.pp_styled `Bold "%s" ppf sym
 
 let uninterp s = Uninterp s
 
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 0a2adf96b..81ef42b91 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -352,6 +352,12 @@ module Function = struct
 
   let mk typ name = Function {name; typ} |> check invariant
 
+  let counterfeit =
+    let dummy_function_type =
+      Typ.pointer ~elt:(Typ.function_ ~args:IArray.empty ~return:None)
+    in
+    fun name -> mk dummy_function_type name
+
   module Map = Map
   module Tbl = Tbl
 end
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index b4cd3c6a7..70eb323e7 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -157,6 +157,12 @@ module Function : sig
 
   val of_exp : exp -> t option
   val mk : Typ.t -> string -> t
+
+  val counterfeit : string -> t
+  (** [compare] ignores [Function.typ], so it is possible to construct
+      [Function] names using a dummy type that compare equal to their
+      genuine counterparts. *)
+
   val name : t -> string
   val typ : t -> Typ.t
 end
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index ef4b4db23..a1f252777 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -638,7 +638,8 @@ module Func = struct
         iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
-  let find functions name = Function.Map.find functions name
+  let find name functions =
+    Function.Map.find (Function.counterfeit name) functions
 
   let mk ~name ~formals ~freturn ~fthrow ~entry ~cfg ~loc =
     let locals =
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 699e69740..a3940253b 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -223,7 +223,7 @@ module Func : sig
     -> loc:Loc.t
     -> t
 
-  val find : Function.t -> functions -> t option
+  val find : string -> functions -> t option
   (** Look up a function of the given name in the given functions. *)
 
   val fold_cfg : func -> 'a -> f:(block -> 'a -> 'a) -> 'a
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 83ed46363..f9f818bcb 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -9,7 +9,12 @@ open Fol
 module T = Term
 module F = Formula
 
-let uconst name = T.apply (Funsym.uninterp ("@" ^ name)) [||]
+let lookup_func lookup term =
+  match Term.get_trm term with
+  | Some (Apply (Uninterp name, [||])) -> lookup name
+  | _ -> None
+
+let uconst name = T.apply (Funsym.uninterp name) [||]
 let global g = uconst (Llair.Global.name g)
 let reg r = Var.program ~name:(Llair.Reg.name r)
 let regs rs = Var.Set.of_iter (Iter.map ~f:reg (Llair.Reg.Set.to_iter rs))
diff --git a/sledge/src/llair_to_Fol.mli b/sledge/src/llair_to_Fol.mli
index 18bfac78a..8615e20f6 100644
--- a/sledge/src/llair_to_Fol.mli
+++ b/sledge/src/llair_to_Fol.mli
@@ -7,6 +7,7 @@
 
 open Fol
 
+val lookup_func : (string -> 'a option) -> Term.t -> 'a option
 val global : Llair.Global.t -> Term.t
 val reg : Llair.Reg.t -> Var.t
 val regs : Llair.Reg.Set.t -> Var.Set.t
diff --git a/sledge/test/analyze/icall.c b/sledge/test/analyze/icall.c
new file mode 100644
index 000000000..8bb2cdcd4
--- /dev/null
+++ b/sledge/test/analyze/icall.c
@@ -0,0 +1,37 @@
+/*
+ * 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 <assert.h>
+
+typedef struct _ {
+  int a;
+  int b;
+  int c;
+} S;
+
+typedef int* (*F)(S*);
+
+int* g(S* x) { return &(x->b); }
+
+int* h(S* x) { return &(x->c); }
+
+void main() {
+  S t;
+  void* x;
+  int* y;
+  F f;
+
+  f = &g;
+  x = &(t.a);
+  y = (*f)(x);
+  assert(x != y);
+
+  f = &h;
+  x = &(t.a);
+  y = (*f)(x);
+  assert(x != y);
+}