First version of a devirtualization pre-analysis (Java frontend)

Reviewed By: jvillard

Differential Revision: D20692190

fbshipit-source-id: e1ac5c454

Author: davidpichardie

infer/src/IR/Procdesc.ml

@@ -253,6 +253,16 @@ module Node = struct
       true )
 
 
+  (** Map and replace the instructions to be executed using a context *)
+  let replace_instrs_using_context node ~f ~update_context ~context_at_node =
+    let f node context instr = (update_context context instr, f node context instr) in
+    let instrs' = Instrs.map_and_fold node.instrs ~f:(f node) ~init:context_at_node in
+    if phys_equal instrs' node.instrs then false
+    else (
+      node.instrs <- instrs' ;
+      true )
+
+
   (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *)
   let replace_instrs_by node ~f =
     let instrs' = Instrs.concat_map node.instrs ~f:(f node) in
@@ -558,6 +568,14 @@ let replace_instrs pdesc ~f =
   update_nodes pdesc ~update
 
 
+let replace_instrs_using_context pdesc ~f ~update_context ~context_at_node =
+  let update node =
+    Node.replace_instrs_using_context ~f ~update_context ~context_at_node:(context_at_node node)
+      node
+  in
+  update_nodes pdesc ~update
+
+
 let replace_instrs_by pdesc ~f =
   let update node = Node.replace_instrs_by ~f node in
   update_nodes pdesc ~update

infer/src/IR/Procdesc.mli

@@ -268,6 +268,15 @@ val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr) -> bool
 (** Map and replace the instructions to be executed. Returns true if at least one substitution
     occured. *)
 
+val replace_instrs_using_context :
+     t
+  -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr)
+  -> update_context:('a -> Sil.instr -> 'a)
+  -> context_at_node:(Node.t -> 'a)
+  -> bool
+(** Map and replace the instructions to be executed using a context that we built with previous
+    instructions in the node. Returns true if at least one substitution occured. *)
+
 val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool
 (** Like [replace_instrs], but slower, and each instruction may be replaced by 0, 1, or more
     instructions. *)

infer/src/backend/Devirtualizer.ml

@@ -0,0 +1,171 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+module L = Logging
+
+module VDom = AbstractDomain.Flat (JavaClassName)
+(** value domain, with the following concretization function [gamma]:
+
+    {[
+      gamma(VDom.top) = { any value }
+      gamma(VDom.v A) = { any ref of exact class A }
+      gamma(VDom.bot) = emptyset
+    ]} *)
+
+module CFG = ProcCfg.Normal
+module Domain = AbstractDomain.Map (Var) (VDom)
+
+let get_var (astate : Domain.t) (v : Var.t) : VDom.t =
+  match Domain.find_opt v astate with Some ab -> ab | None -> VDom.bottom
+
+
+let rec eval_expr (astate : Domain.t) (expr : Exp.t) : VDom.t =
+  match expr with
+  | Var id ->
+      get_var astate (Var.of_id id)
+  | UnOp _ | BinOp _ | Exn _ | Closure _ ->
+      VDom.top
+  | Const _ ->
+      VDom.top (* could be more precise for Cstr and Cclass *)
+  | Cast (_, e) ->
+      eval_expr astate e (* could be more precise for final class *)
+  | Lvar v ->
+      get_var astate (Var.of_pvar v)
+  | Lfield _ ->
+      VDom.top (* could be more precise for final class *)
+  | Lindex _ ->
+      VDom.top
+  | Sizeof _ ->
+      VDom.top
+
+
+let eval_fun pname args =
+  (* can be extended later if we decide to handle more builtins *)
+  if Procname.equal pname BuiltinDecl.__new then
+    match args with
+    | (_, typ) :: _ when Typ.is_pointer typ -> (
+      match Typ.name (Typ.strip_ptr typ) with Some (Typ.JavaClass cn) -> VDom.v cn | _ -> VDom.top )
+    | _ ->
+        VDom.top
+  else VDom.top
+
+
+let eval_instr (astate : Domain.t) (instr : Sil.instr) : Domain.t =
+  match instr with
+  | Load {id} when Ident.is_none id ->
+      astate
+  | Load {id; e} ->
+      let aval = eval_expr astate e in
+      Domain.add (Var.of_id id) aval astate
+  | Call ((id, _), Const (Const.Cfun pname), args, _, _) ->
+      let aval = eval_fun pname args in
+      Domain.add (Var.of_id id) aval astate
+  | Call ((id, _), _, _, _, _) ->
+      Domain.add (Var.of_id id) VDom.top astate
+  | Store {e1= Lvar pvar; e2} ->
+      let aval = eval_expr astate e2 in
+      Domain.add (Var.of_pvar pvar) aval astate
+  | Store _ | Prune _ | Metadata _ ->
+      astate
+
+
+module TransferFunctions = struct
+  module CFG = CFG
+  module Domain = Domain
+
+  type analysis_data = unit
+
+  let exec_instr astate _ _node instr = eval_instr astate instr
+
+  let pp_session_name node fmt =
+    Format.fprintf fmt "devirtualizer analysis %a" CFG.Node.pp_id (CFG.Node.id node)
+end
+
+module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions)
+
+let analyze_at_node (map : Analyzer.invariant_map) node : Domain.t =
+  match Analyzer.InvariantMap.find_opt (Procdesc.Node.get_id node) map with
+  | Some abstate ->
+      abstate.pre
+  | None ->
+      Domain.bottom
+
+
+(* inspired from biabduction/Symexec.ml, function resolve_method  *)
+let resolve_method tenv class_name proc_name =
+  let method_exists pname methods = List.exists ~f:(Procname.equal pname) methods in
+  let rec resolve class_name =
+    let resolved_proc_name = Procname.replace_class proc_name class_name in
+    match Tenv.lookup tenv class_name with
+    | Some {methods; supers} when Typ.Name.is_class class_name -> (
+        if method_exists resolved_proc_name methods then Some resolved_proc_name
+        else match supers with super_classname :: _ -> resolve super_classname | _ -> None )
+    | _ ->
+        None
+  in
+  resolve class_name
+
+
+let process summary tenv =
+  let pdesc = Summary.get_proc_desc summary in
+  let node_cfg = CFG.from_pdesc pdesc in
+  let all_params = Procdesc.get_pvar_formals pdesc in
+  let initial =
+    (* all params -> top, bottom otherwise *)
+    (* we could use param type (if final) to get more precision *)
+    List.fold_left ~init:Domain.empty
+      ~f:(fun acc (pvar, _) -> Domain.add (Var.of_pvar pvar) VDom.top acc)
+      all_params
+  in
+  let map = Analyzer.exec_cfg node_cfg () ~initial in
+  let is_virtual_call call_flags =
+    call_flags.CallFlags.cf_virtual || call_flags.CallFlags.cf_interface
+  in
+  let replace_instr node (astate : Domain.t) (instr : Sil.instr) : Sil.instr =
+    let kind = `ExecNode in
+    let pp_name fmt = Format.pp_print_string fmt "devirtualizer" in
+    NodePrinter.with_session (CFG.Node.underlying_node node) ~kind ~pp_name ~f:(fun () ->
+        match instr with
+        | Call
+            ( ret_id_typ
+            , Const (Const.Cfun callee_pname)
+            , ((this_expr, _) :: _ as actual_params)
+            , loc
+            , call_flags )
+          when is_virtual_call call_flags -> (
+            L.d_printfln "virtual call %a " Procname.pp callee_pname ;
+            let aval = eval_expr astate this_expr in
+            match VDom.get aval with
+            | Some dyn_typ -> (
+              match resolve_method tenv (Typ.JavaClass dyn_typ) callee_pname with
+              | None ->
+                  L.d_printfln "(unexpected: no resolved method found)" ;
+                  instr
+              | Some resolved_callee_pname ->
+                  let resolved_call_flags =
+                    {call_flags with cf_virtual= false; cf_interface= false}
+                  in
+                  L.d_printfln "replaced by nonvirtual <%a>\n" Procname.pp resolved_callee_pname ;
+                  Sil.Call
+                    ( ret_id_typ
+                    , Const (Const.Cfun resolved_callee_pname)
+                    , actual_params
+                    , loc
+                    , resolved_call_flags ) )
+            | _ ->
+                Logging.debug Capture Verbose "unchanged\n" ;
+                instr )
+        | _ ->
+            instr )
+  in
+  let update_context = eval_instr in
+  let context_at_node node = analyze_at_node map node in
+  let _has_changed : bool =
+    Procdesc.replace_instrs_using_context pdesc ~f:replace_instr ~update_context ~context_at_node
+  in
+  ()

infer/src/backend/Devirtualizer.mli

@@ -0,0 +1,13 @@
+(*
+ * 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.
+ *)
+
+(** {1 Simple devirtualization pre-analysis using a flow-sensitive tracking of dynamic classes} *)
+
+open! IStd
+
+val process : Summary.t -> Tenv.t -> unit
+(** Run the devirtualization pass by replacing some virtual calls by resolved calls *)

infer/src/backend/preanal.ml

@@ -379,5 +379,6 @@ let do_preanalysis exe_env pdesc =
     FunctionPointerSubstitution.process pdesc ;
   Liveness.process summary tenv ;
   AddAbstractionInstructions.process pdesc ;
+  if Procname.is_java proc_name then Devirtualizer.process summary tenv ;
   NoReturn.process tenv pdesc ;
   ()

infer/tests/codetoanalyze/java/biabduction/issues.exp

@@ -26,7 +26,6 @@ codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.ja
 codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.leakFoundWhenIndirectlyImplementingCloseable():void, 1, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure leakFoundWhenIndirectlyImplementingCloseable(),start of procedure CloseableAsResourceExample$MyResource(...),return from a call to CloseableAsResourceExample$MyResource.<init>(CloseableAsResourceExample)]
 codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.notClosingCloseable():void, 1, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure notClosingCloseable(),start of procedure SomeResource(),return from a call to SomeResource.<init>()]
 codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.notClosingWrapper():void, 2, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure notClosingWrapper(),start of procedure Resource(),return from a call to Resource.<init>(),start of procedure Sub(...),start of procedure Wrapper(...),return from a call to Wrapper.<init>(Resource),return from a call to Sub.<init>(Resource),start of procedure close(),return from a call to void Resource.close()]
-codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.skippedVritualCallDoesNotCloseResourceOnReceiver():void, 2, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure skippedVritualCallDoesNotCloseResourceOnReceiver(),start of procedure SomeResource(),return from a call to SomeResource.<init>(),Skipping foo(...): unknown method,Definition of foo(...)]
 codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.sourceOfNullWithResourceLeak():codetoanalyze.java.infer.T, 1, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure sourceOfNullWithResourceLeak(),start of procedure SomeResource(),return from a call to SomeResource.<init>()]
 codetoanalyze/java/biabduction/CloseableAsResourceExample.java, codetoanalyze.java.infer.CloseableAsResourceExample.withException():void, 4, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure withException(),start of procedure SomeResource(),return from a call to SomeResource.<init>(),start of procedure doSomething(),Skipping star(): unknown method,Definition of star(),Taking true branch,start of procedure LocalException(),return from a call to LocalException.<init>(),exception codetoanalyze.java.infer.LocalException,return from a call to void SomeResource.doSomething()]
 codetoanalyze/java/biabduction/CursorLeaks.java, codetoanalyze.java.infer.CursorLeaks.completeDownloadNotClosed(android.app.DownloadManager):int, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure completeDownloadNotClosed(...),Taking false branch,Skipping getColumnIndex(...): unknown method]

infer/tests/codetoanalyze/java/nullsafe/issues.exp

@@ -325,19 +325,19 @@ codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`nonStrictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 137.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition NonStrict.nonnull might be always true according to the existing annotations.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldIsBad():void, 2, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.nonnull`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. This field is used at line 133. Either add a local check for null or assertion, or make `NonStrict` nullsafe strict.]
-codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition lang.String(o)V might be always true: `NonStrict.getNonnull()` is not annotated as `@Nullable`.]
+codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition lang.String(o) might be always true: `NonStrict.getNonnull()` is not annotated as `@Nullable`.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodIsBad():void, 2, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 115. Either add a local check for null or assertion, or make `NonStrict` nullsafe strict.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullStaticMethodIsBad():void, 2, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.staticNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 124. Either add a local check for null or assertion, or make `NonStrict` nullsafe strict.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`.]
-codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.]
+codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`getNullable(...)` is nullable and is not locally checked for null when calling `toString()`: call to getNullable() at line 110.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableStaticMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`sameClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 65.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`Strict.nullable` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`getNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableStaticMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`strictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 99.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`.]
-codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.]
+codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`getNullable(...)` is nullable and is not locally checked for null when calling `toString()`: call to getNullable() at line 75.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableStaticMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe/StrictModeForThirdParty.java, Linters_dummy_method, 19, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], StrictModeForThirdParty, codetoanalyze.java.nullsafe_default, issues: 5, curr_mode: "Strict"
 codetoanalyze/java/nullsafe/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.dereferenceFieldIsBAD():void, 1, ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE, no_bucket, ERROR, [`ThirdPartyTestClass.nonNullableField`: `@NullsafeStrict` mode prohibits using values coming from third-party classes without a check. This field is used at line 49. Either add a local check for null or assertion, or access `nonNullableField` via a nullsafe strict getter.]