From 8c82072cb06b9c3cc4ca1e0901468f1c8a7d7685 Mon Sep 17 00:00:00 2001 From: David Pichardie Date: Mon, 18 May 2020 09:43:32 -0700 Subject: [PATCH] First version of a devirtualization pre-analysis (Java frontend) Reviewed By: jvillard Differential Revision: D20692190 fbshipit-source-id: e1ac5c454 --- infer/src/IR/Procdesc.ml | 18 ++ infer/src/IR/Procdesc.mli | 9 + infer/src/backend/Devirtualizer.ml | 171 ++++++++++++++++++ infer/src/backend/Devirtualizer.mli | 13 ++ infer/src/backend/preanal.ml | 1 + .../codetoanalyze/java/biabduction/issues.exp | 1 - .../codetoanalyze/java/nullsafe/issues.exp | 6 +- 7 files changed, 215 insertions(+), 4 deletions(-) create mode 100644 infer/src/backend/Devirtualizer.ml create mode 100644 infer/src/backend/Devirtualizer.mli diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 825414438..08755ff07 100644 --- a/infer/src/IR/Procdesc.ml +++ b/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 diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index ef3c7b3c7..5d5a0d544 100644 --- a/infer/src/IR/Procdesc.mli +++ b/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. *) diff --git a/infer/src/backend/Devirtualizer.ml b/infer/src/backend/Devirtualizer.ml new file mode 100644 index 000000000..89cee6fd3 --- /dev/null +++ b/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 + () diff --git a/infer/src/backend/Devirtualizer.mli b/infer/src/backend/Devirtualizer.mli new file mode 100644 index 000000000..4457039af --- /dev/null +++ b/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 *) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 3c79d13fb..009d29c36 100644 --- a/infer/src/backend/preanal.ml +++ b/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 ; () diff --git a/infer/tests/codetoanalyze/java/biabduction/issues.exp b/infer/tests/codetoanalyze/java/biabduction/issues.exp index 38fb22aef..3b2459e48 100644 --- a/infer/tests/codetoanalyze/java/biabduction/issues.exp +++ b/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.(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.()] 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.(),start of procedure Sub(...),start of procedure Wrapper(...),return from a call to Wrapper.(Resource),return from a call to Sub.(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.(),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.()] 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.(),start of procedure doSomething(),Skipping star(): unknown method,Definition of star(),Taking true branch,start of procedure LocalException(),return from a call to LocalException.(),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] diff --git a/infer/tests/codetoanalyze/java/nullsafe/issues.exp b/infer/tests/codetoanalyze/java/nullsafe/issues.exp index d13bdc57f..1252781a4 100644 --- a/infer/tests/codetoanalyze/java/nullsafe/issues.exp +++ b/infer/tests/codetoanalyze/java/nullsafe/issues.exp @@ -325,11 +325,11 @@ 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()`.] @@ -337,7 +337,7 @@ codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default 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.]