[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

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

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

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

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

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]
 

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
 

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
 

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
 

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

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
 

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

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

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 =

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

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

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

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);
+}