Initial support for lazy dynamic dispatch

Summary:public
Lazy dynamic dispatch handling works as follows:

Assuming a call of the form:

  foo(a);

where the static type of `a` is `A`. If during the symbolic execution, the dynamic type of the variable `a` is `B` where `B <: A`, then we create on-demand a copy `foo(B)` of `foo(A)` where all the uses of the typed parameter `a` are replaced with a parameter of type `B`. Especially, if `foo` contains virtual call, say `get` where `a` is the receiver, then the call gets redirected to the overridden method in `B`, which simulates the runtime behavior of Java.

This lazy dynamic dispatch mode is only turn on for the tracing mode for now in order to avoid conflicts with sblackshear's approach for sound dynamic dispatch.

Reviewed By: sblackshear

Differential Revision: D2888922

fb-gh-sync-id: 3250c9e
shipit-source-id: 3250c9e

infer/lib/python/inferlib/analyze.py

@@ -332,6 +332,9 @@ class AnalyzerWrapper(object):
         javac_original_arguments = \
             self.javac.original_arguments if self.javac is not None else []
 
+        if self.args.analyzer == config.ANALYZER_TRACING:
+            os.environ['INFER_LAZY_DYNAMIC_DISPATCH'] = 'Y'
+
         if self.args.multicore == 1:
             analysis_start_time = time.time()
             analyze_cmd = infer_analyze + infer_options

infer/src/backend/cfg.ml

@@ -179,11 +179,17 @@ module Node = struct
   let get_succs node = node.nd_succs
 
   type node = t
+
   module NodeSet = Set.Make(struct
       type t = node
       let compare = compare
     end)
 
+  module NodeMap = Map.Make(struct
+      type t = node
+      let compare = compare
+    end)
+
   let get_sliced_succs node f =
     let visited = ref NodeSet.empty in
     let rec slice_nodes nodes : NodeSet.t =
@@ -586,15 +592,117 @@ module Node = struct
     let fold_node acc node =
       IList.fold_left (fun acc instr -> f acc node instr) acc (get_instrs node) in
     proc_desc_fold_nodes fold_node acc proc_desc
+
 (*
   (** Set the proc desc of the node *)
   let node_set_proc_desc pdesc node =
     node.nd_proc <- Some pdesc
 
+
   let remove_node cfg node =
     remove_node' (fun node' -> not (equal node node'))
       cfg node
 *)
+
+  (* clone a procedure description and apply the type substitutions where
+     the parameters are used *)
+  let proc_desc_specialize_types cfg callee_proc_desc resolved_attributes substitutions =
+    let resolved_proc_desc = proc_desc_create cfg resolved_attributes in
+    let resolved_proc_name = proc_desc_get_proc_name resolved_proc_desc
+    and callee_start_node = proc_desc_get_start_node callee_proc_desc
+    and callee_exit_node = proc_desc_get_exit_node callee_proc_desc in
+    let convert_pvar pvar =
+      Sil.mk_pvar (Sil.pvar_get_name pvar) resolved_proc_name in
+    let convert_exp = function
+      | Sil.Lvar origin_pvar ->
+          Sil.Lvar (convert_pvar origin_pvar)
+      | exp -> exp in
+    let extract_class_name = function
+      | Sil.Tptr (Sil.Tstruct { Sil.struct_name }, _) when struct_name <> None ->
+          Mangled.to_string (Option.get struct_name)
+      | _ -> failwith "Expecting classname for Java types" in
+    let subst_map = ref Ident.IdentMap.empty in
+    let redirected_class_name origin_id =
+      try
+        Some (Ident.IdentMap.find origin_id !subst_map)
+      with Not_found -> None in
+    let convert_instr instrs = function
+      | Sil.Letderef (id, (Sil.Lvar origin_pvar as origin_exp), origin_typ, loc) ->
+          let (_, specialized_typ) =
+            let pvar_name = Sil.pvar_get_name origin_pvar in
+            try
+              IList.find
+                (fun (n, _) -> Mangled.equal n pvar_name)
+                substitutions
+            with Not_found ->
+              (pvar_name, origin_typ) in
+          subst_map := Ident.IdentMap.add id specialized_typ !subst_map;
+          Sil.Letderef (id, convert_exp origin_exp, specialized_typ, loc) :: instrs
+      | Sil.Letderef (id, origin_exp, origin_typ, loc) ->
+          Sil.Letderef (id, convert_exp origin_exp, origin_typ, loc) :: instrs
+      | Sil.Set (assignee_exp, origin_typ, origin_exp, loc) ->
+          let set_instr =
+            Sil.Set (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc) in
+          set_instr :: instrs
+      | Sil.Call (return_ids, Sil.Const (Sil.Cfun callee_pname),
+                  (Sil.Var id, _) :: origin_args, loc, call_flags)
+        when call_flags.Sil.cf_virtual && redirected_class_name id <> None ->
+          let redirected_typ  = Option.get (redirected_class_name id) in
+          let redirected_pname =
+            Procname.java_replace_class
+              callee_pname (extract_class_name redirected_typ)
+          and args =
+            let other_args = (IList.map (fun (exp, typ) -> (convert_exp exp, typ)) origin_args) in
+            (Sil.Var id, redirected_typ) :: other_args in
+          let call_instr =
+            Sil.Call (return_ids, Sil.Const (Sil.Cfun redirected_pname), args, loc, call_flags) in
+          call_instr :: instrs
+      | Sil.Call (return_ids, origin_call_exp, origin_args, loc, call_flags) ->
+          let converted_args = IList.map (fun (exp, typ) -> (convert_exp exp, typ)) origin_args in
+          let call_instr =
+            Sil.Call (return_ids, convert_exp origin_call_exp, converted_args, loc, call_flags) in
+          call_instr :: instrs
+      | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) ->
+          Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind):: instrs
+      | Sil.Nullify (origin_pvar, loc, deallocate) ->
+          Sil.Nullify (convert_pvar origin_pvar, loc, deallocate) :: instrs
+      | Sil.Declare_locals (typed_vars, loc) ->
+          let new_typed_vars = IList.map (fun (pvar, typ) -> (convert_pvar pvar, typ)) typed_vars in
+          (Sil.Declare_locals (new_typed_vars, loc)) :: instrs
+      | instr -> instr :: instrs in
+    let convert_node_kind = function
+      | Start_node _ -> Start_node resolved_proc_desc
+      | Exit_node _ -> Exit_node resolved_proc_desc
+      | node_kind -> node_kind in
+    let node_map = ref NodeMap.empty in
+    let rec convert_node node =
+      let loc = get_loc node
+      and kind = convert_node_kind (get_kind node)
+      and instrs =
+        IList.fold_left convert_instr [] (get_instrs node) in
+      create cfg loc kind (IList.rev instrs) resolved_proc_desc (get_temps node)
+    and loop callee_nodes =
+      match callee_nodes with
+      | [] -> []
+      | node :: other_node ->
+          let converted_node =
+            try
+              NodeMap.find node !node_map
+            with Not_found ->
+              let new_node = convert_node node
+              and successors = get_succs node
+              and exn_nodes = get_exn node in
+              node_map := NodeMap.add node new_node !node_map;
+              if equal node callee_start_node then
+                proc_desc_set_start_node resolved_proc_desc new_node;
+              if equal node callee_exit_node then
+                proc_desc_set_exit_node resolved_proc_desc new_node;
+              set_succs_exn new_node (loop successors) (loop exn_nodes);
+              new_node in
+          converted_node :: (loop other_node) in
+    ignore (loop [callee_start_node]);
+    pdesc_tbl_add cfg resolved_proc_name resolved_proc_desc
+
 end
 (* =============== END of module Node =============== *)
 
@@ -639,6 +747,7 @@ module Procdesc = struct
   let set_flag = Node.proc_desc_set_flag
   let set_start_node = Node.proc_desc_set_start_node
   let append_locals = Node.proc_desc_append_locals
+  let specialize_types = Node.proc_desc_specialize_types
 end
 
 (* =============== END of module Procdesc =============== *)
@@ -1043,3 +1152,39 @@ let store_cfg_to_file (filename : DB.filename) (save_sources : bool) (cfg : cfg)
     end;
   save_attributes cfg;
   Serialization.to_file cfg_serializer filename cfg
+
+
+(** Creates a copy of a procedure description and a list of type substitutions of the form
+    (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but
+    all the type of the parameters are replaced in the instructions according to the list.
+    The virtual calls are also replaced to match the parameter types *)
+let specialize_types cfg callee_proc_name resolved_proc_name args =
+  (* TODO (#9333890): This currently only works when the callee is defined in the same file.
+         Add support to search for the callee procedure description in the execution environment *)
+  match Procdesc.find_from_name cfg resolved_proc_name with
+  | Some _ -> ()
+  | None ->
+      begin
+        match Procdesc.find_from_name cfg callee_proc_name with
+        | None -> ()
+        | Some callee_proc_desc ->
+            let callee_attributes = Procdesc.get_attributes callee_proc_desc in
+            let resolved_formals =
+              IList.fold_left2
+                (fun accu (name, _) (_, arg_typ) -> (name, arg_typ) :: accu)
+                [] callee_attributes.ProcAttributes.formals args |> IList.rev in
+            let resolved_attributes =
+              { callee_attributes with
+                ProcAttributes.formals = resolved_formals;
+                proc_name = resolved_proc_name;
+              } in
+            AttributesTable.store_attributes resolved_attributes;
+            Procdesc.specialize_types cfg callee_proc_desc resolved_attributes resolved_formals;
+            begin
+              let source_file = resolved_attributes.ProcAttributes.loc.Location.file in
+              let source_dir = DB.source_dir_from_source_file source_file in
+              let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
+              let save_sources = false in
+              store_cfg_to_file cfg_file save_sources cfg
+            end
+      end

infer/src/backend/cfg.mli

@@ -117,6 +117,7 @@ module Procdesc : sig
 
   (** append a list of new local variables to the existing list of local variables *)
   val append_locals : t -> (Mangled.t * Sil.typ) list -> unit
+
 end
 
 (** node of the control flow graph *)
@@ -314,3 +315,9 @@ val get_block_pdesc : cfg -> Mangled.t -> Procdesc.t option
 
 (** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
 val remove_seed_captured_vars_block : Mangled.t list -> Prop.normal Prop.t -> Prop.normal Prop.t
+
+(** Creates a copy of a procedure description and a list of type substitutions of the form
+    (name, typ) where name is a parameter. The resulting procedure CFG is isomorphic but
+    all the type of the parameters are replaced in the instructions according to the list.
+    The virtual calls are also replaced to match the parameter types *)
+val specialize_types : cfg -> Procname.t -> Procname.t -> (Sil.exp * Sil.typ) list -> unit

infer/src/backend/config.ml

@@ -355,6 +355,11 @@ let analyze_models = from_env_variable "INFER_ANALYZE_MODELS"
     cost *)
 let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH"
 
+(** experimental: handle dynamic dispatch by following the JVM semantics and creating
+    during the symbolic excution procedure descriptions using the types information
+    found in the abstract state *)
+let lazy_dynamic_dispatch = from_env_variable "INFER_LAZY_DYNAMIC_DISPATCH"
+
 module Experiment = struct
 
   (** if true, a precondition with e.g. index 3 in an array does not require the caller to have index 3 too

infer/src/backend/ident.ml

@@ -77,6 +77,12 @@ module IdentSet = Set.Make
       let compare = compare
     end)
 
+module IdentMap = Map.Make
+    (struct
+      type t = _ident
+      let compare = compare
+    end)
+
 module IdentHash =
   Hashtbl.Make(struct
     type t = _ident

infer/src/backend/ident.mli

@@ -28,6 +28,9 @@ module IdentSet : Set.S with type elt = t
 (** Hash table with ident as key. *)
 module IdentHash : Hashtbl.S with type key = t
 
+(** Map with ident as key. *)
+module IdentMap : Map.S with type key = t
+
 (** Set for fieldnames *)
 module FieldSet : Set.S with type elt = fieldname
 

infer/src/backend/ondemand.ml

@@ -45,7 +45,7 @@ type callbacks =
 
 let callbacks_ref = ref None
 
-let set_callbacks  (callbacks : callbacks) =
+let set_callbacks (callbacks : callbacks) =
   callbacks_ref := Some callbacks
 
 let unset_callbacks () =

infer/src/backend/symExec.ml

@@ -668,6 +668,61 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
         end
   | _ -> failwith "A virtual call must have a receiver"
 
+
+(** Resolve the name of the procedure to call based on the type of the arguments *)
+let resolve_java_pname tenv prop args pname call_flags : Procname.t =
+  let resolve_from_args pname args =
+    let parameters = Procname.java_get_parameters pname in
+    if IList.length args <> IList.length parameters then
+      pname
+    else
+      let resolved_params =
+        IList.fold_left2
+          (fun accu (arg_exp, _) name ->
+             match resolve_typename prop arg_exp with
+             | Some class_name ->
+                 (Procname.split_classname (Typename.name class_name)) :: accu
+             | None -> name :: accu)
+          [] args (Procname.java_get_parameters pname) |> IList.rev in
+      Procname.java_replace_parameters pname resolved_params in
+  let resolved_pname, other_args =
+    match args with
+    | [] -> pname, []
+    | (first_arg, _) :: other_args when call_flags.Sil.cf_virtual ->
+        let resolved =
+          begin
+            match resolve_typename prop first_arg with
+            | Some class_name -> resolve_method tenv class_name pname
+            | None -> pname
+          end in
+        resolved, other_args
+    | _ :: other_args when Procname.is_constructor pname ->
+        pname, other_args
+    | args ->
+        pname, args in
+  resolve_from_args resolved_pname other_args
+
+
+(** Resolved the procedure name and run the analysis of the resolved procedure
+    if not already analyzed *)
+let resolve_and_analyze
+    cfg tenv caller_pdesc prop args callee_pname call_flags : Procname.t * Specs.summary option =
+  let resolved_pname =
+    (* TODO (#9333890): Fix conflict with method overloading by encoding in the procedure name
+         whether the method is defined or generated by the specialization *)
+    begin
+      let res_pname =
+        resolve_java_pname tenv prop args callee_pname call_flags in
+      if Procname.equal res_pname callee_pname then callee_pname
+      else
+        (if not (Specs.summary_exists res_pname) then
+           Cfg.specialize_types cfg callee_pname res_pname args;
+         res_pname)
+    end in
+  Ondemand.do_analysis ~propagate_exceptions:true caller_pdesc resolved_pname;
+  resolved_pname, Specs.get_summary resolved_pname
+
+
 (** recognize calls to shared_ptr procedures and re-direct them to infer procedures for modelling *)
 let redirect_shared_ptr tenv cfg pname actual_params =
   let class_shared_ptr typ =
@@ -678,7 +733,7 @@ let redirect_shared_ptr tenv cfg pname actual_params =
       | _ -> false
     with exn when exn_not_failure exn -> false in
   (* We pattern match over some specific library function, *)
-  (* so we make precise matching to distinghuis between *)
+  (* so we make precise matching to distinguish between *)
   (* references and pointers in C++ *)
   let ptr_to filter = function
     | Sil.Tptr (t, Sil.Pk_pointer)
@@ -1080,6 +1135,29 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
     when function_is_builtin callee_pname ->
       let sym_exe_builtin = Builtin.get_sym_exe_builtin callee_pname in
       sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
+
+  | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags)
+    when !Config.curr_language = Config.Java && Config.lazy_dynamic_dispatch ->
+      let norm_prop, norm_args = normalize_params pname _prop actual_params in
+      let exec_skip_call skipped_pname ret_type =
+        skip_call norm_prop path skipped_pname loc ret_ids (Some ret_type) norm_args in
+      let resolved_pname, summary_opt =
+        resolve_and_analyze cfg tenv pdesc norm_prop norm_args callee_pname call_flags in
+      begin
+        match summary_opt with
+        | None ->
+            let ret_typ_str = Procname.java_get_return_type pname in
+            let ret_typ =
+              match lookup_java_typ_from_string tenv ret_typ_str with
+              | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer)
+              | typ -> typ in
+            exec_skip_call resolved_pname ret_typ
+        | Some summary when call_should_be_skipped resolved_pname summary ->
+            exec_skip_call resolved_pname summary.Specs.attributes.ProcAttributes.ret_type
+        | Some summary ->
+            sym_exec_call cfg pdesc tenv norm_prop path ret_ids norm_args summary loc
+      end
+
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags)
     when !Config.curr_language = Config.Java ->
       do_error_checks (Paths.Path.curr_node path) instr pname pdesc;

infer/tests/codetoanalyze/java/infer/ClassCastExceptions.java

@@ -22,6 +22,10 @@ class SubClassA extends SuperClass {
 class SubClassB extends SuperClass {
 }
 
+interface MyInterface {
+  public int getInt();
+}
+
 class ImplementationOfInterface implements MyInterface {
 
   public int getInt() {
@@ -35,10 +39,6 @@ class AnotherImplementationOfInterface implements MyInterface {
   }
 }
 
-interface MyInterface {
-  public int getInt();
-}
-
 
 public class ClassCastExceptions {
 

infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java

@@ -0,0 +1,39 @@
+/*
+ * Copyright (c) 2015 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package codetoanalyze.java.tracing;
+
+class A {
+
+  public T get() {
+    return new T();
+  }
+
+}
+
+class B extends A  {
+
+  public T get() {
+    return null;
+  }
+
+}
+
+public class LazyDynamicDispatchExample {
+
+  static T foo(A a) {
+    return a.get();
+  }
+
+  static void bar() {
+    B b = new B();
+    foo(b).f();
+  }
+
+}

infer/tests/endtoend/java/comparison/ClassCastExceptionTest.java

@@ -43,6 +43,7 @@ public class ClassCastExceptionTest {
     String[] methods = {
         "classCastException",
         "classCastExceptionImplementsInterface",
+        "openHttpURLConnection",
     };
     assertThat(
         "Results should contain " + CLASS_CAST_EXCEPTION,
@@ -55,5 +56,4 @@ public class ClassCastExceptionTest {
     );
   }
 
-
 }

infer/tests/endtoend/java/tracing/LazyDynamicDispatchTest.java

@@ -0,0 +1,58 @@
+/*
+ * Copyright (c) 2015 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+
+package endtoend.java.tracing;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class LazyDynamicDispatchTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java";
+
+  public static final String NPE =
+      "java.lang.NullPointerException";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void loadResults() throws InterruptedException, IOException {
+    inferResults = InferResults.loadTracingResults(
+        LazyDynamicDispatchTest.class,
+        SOURCE_FILE);
+  }
+
+  @Test
+  public void matchErrors()
+      throws IOException, InterruptedException, InferException {
+    String[] methods = {
+        "bar"
+    };
+    assertThat(
+        "Results should contain " + NPE,
+        inferResults,
+        containsExactly(
+            NPE,
+            SOURCE_FILE,
+            methods
+        )
+    );
+  }
+
+}

infer/tests/endtoend/java/tracing/NullPointerExceptionTest.java

@@ -34,7 +34,7 @@ public class NullPointerExceptionTest {
   @BeforeClass
   public static void loadResults() throws InterruptedException, IOException {
     inferResults = InferResults.loadTracingResults(
-        ArrayIndexOutOfBoundsExceptionTest.class,
+        NullPointerExceptionTest.class,
         SOURCE_FILE);
   }