implementing dynamic dispatch support for Java interfaces

Reviewed By: jeremydubreil

Differential Revision: D2747240

fb-gh-sync-id: 512cf6d
master
Sam Blackshear 9 years ago committed by facebook-github-bot-5
parent 3dcd6490c2
commit 14e934205f

@ -9,6 +9,8 @@
package android.database;
import com.facebook.infer.models.InferUndefined;
import com.facebook.infer.models.InferBuiltins;
public class CursorWrapper extends Cursor {
protected final Cursor mCursor;
@ -20,4 +22,39 @@ public class CursorWrapper extends Cursor {
public void close() {
mCursor.close();
}
public int getInt(int position) {
return InferUndefined.int_undefined();
}
public int getCount() {
return InferUndefined.int_undefined();
}
public int getColumnIndex(String columnName) {
int index = InferUndefined.int_undefined();
InferBuiltins.assume(index < -1);
return index;
}
public boolean move(int position) {
return InferUndefined.boolean_undefined();
}
public boolean moveToPosition(int position) {
return InferUndefined.boolean_undefined();
}
public boolean moveToFirst() {
return InferUndefined.boolean_undefined();
}
public boolean moveToNext() {
return InferUndefined.boolean_undefined();
}
public boolean moveToLast() {
return InferUndefined.boolean_undefined();
}
}

@ -153,6 +153,10 @@ let array_level = ref 0
(** Check whether to report Analysis_stops message in user mode *)
let analysis_stops = ref false
(** experimental: dynamic dispatch for interface calls only in Java. off by default because of the
cost *)
let sound_dynamic_dispatch = ref true
type os_type = Unix | Win32 | Cygwin
let os_type = match Sys.os_type with

@ -373,13 +373,46 @@ let analyze_and_annotate_proc cfg tenv pname pdesc =
(Cfg.Procdesc.get_nodes pdesc);
Table.reset ()
let time = ref 0.0
let doit cfg tenv =
let init = Unix.gettimeofday () in
(* L.out "#### Dead variable nullification ####"; *)
(** mutate the cfg/cg to add dynamic dispatch handling *)
let add_dispatch_calls cfg cg tenv =
let node_add_dispatch_calls caller_pname node =
(* TODO: handle dynamic dispatch for virtual calls as well *)
let call_flags_is_dispatch call_flags = call_flags.Sil.cf_interface in
let instr_is_dispatch_call = function
| Sil.Call (_, _, _, _, call_flags) -> call_flags_is_dispatch call_flags
| _ -> false in
let has_dispatch_call instrs =
IList.exists instr_is_dispatch_call instrs in
let replace_dispatch_calls = function
| Sil.Call (ret_ids, (Sil.Const (Sil.Cfun callee_pname) as call_exp),
(((receiver_exp, receiver_typ) :: _) as args), loc, call_flags) as instr
when call_flags_is_dispatch call_flags ->
(* the frontend should not populate the list of targets *)
assert (call_flags.Sil.cf_targets = []);
let receiver_typ_no_ptr = Sil.typ_strip_ptr receiver_typ in
let sorted_overrides =
let overrides = Prover.get_overrides_of tenv receiver_typ_no_ptr callee_pname in
IList.sort (fun (_, p1) (_, p2) -> Procname.compare p1 p2) overrides in
(match sorted_overrides with
| [] -> instr
| (_, target_pname) :: _ ->
(* TODO: do this with all possible targets. for now, it is too slow to do this, so we
just pick one target *)
Cg.add_edge cg caller_pname target_pname;
let call_flags' = { call_flags with Sil.cf_targets = [target_pname]; } in
Sil.Call (ret_ids, call_exp, args, loc, call_flags'))
| instr -> instr in
let instrs = Cfg.Node.get_instrs node in
if has_dispatch_call instrs then
IList.map replace_dispatch_calls instrs
|> Cfg.Node.replace_instrs node in
let proc_add_dispach_calls pname pdesc =
Cfg.Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc in
Cfg.iter_proc_desc cfg proc_add_dispach_calls
let doit cfg cg tenv =
AllPreds.mk_table cfg;
Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg tenv);
AllPreds.clear_table ();
time := !time +. (Unix.gettimeofday () -. init)
if !Config.sound_dynamic_dispatch then add_dispatch_calls cfg cg tenv;
let gettime () = !time

@ -11,7 +11,4 @@
(** Preanalysis for eliminating dead local variables *)
(** Perform liveness analysis *)
val doit : Cfg.cfg -> Sil.tenv -> unit
(** Return the time for the last execution of the analysis *)
val gettime : unit -> float
val doit : Cfg.cfg -> Cg.t -> Sil.tenv -> unit

@ -1557,6 +1557,24 @@ let cast_exception tenv texp1 texp2 e1 subs =
| _ -> () in
raise (IMPL_EXC ("class cast exception", subs, EXC_FALSE))
(** get all methods that override [supertype].[pname] in [tenv].
Note: supertype should be a type T rather than a pointer to type T
Note: [pname] wil never be included in the returned result *)
let get_overrides_of tenv supertype pname =
let typ_has_method pname = function
| Sil.Tstruct { Sil.def_methods } ->
IList.exists (fun m -> Procname.equal pname m) def_methods
| _ -> false in
let gather_overrides tname typ overrides_acc =
(* get all types in the type environment that are non-reflexive subtypes of [supertype] *)
if not (Sil.typ_equal typ supertype) && check_subtype tenv typ supertype then
(* only select the ones that implement [pname] as overrides *)
let resolved_pname = Procname.java_replace_class pname (Typename.name tname) in
if typ_has_method resolved_pname typ then (typ, resolved_pname) :: overrides_acc
else overrides_acc
else overrides_acc in
Sil.tenv_fold gather_overrides tenv []
(** Check the equality of two types ignoring flags in the subtyping components *)
let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
| Sil.Sizeof(t1, st1), Sil.Sizeof (t2, st2) ->

@ -102,6 +102,7 @@ val check_subtype : Sil.tenv -> Sil.typ -> Sil.typ -> bool
and returns the updated types in the true and false case, if they are possible *)
val subtype_case_analysis : Sil.tenv -> Sil.exp -> Sil.exp -> Sil.exp option * Sil.exp option
val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list

@ -568,6 +568,7 @@ type call_flags = {
cf_interface : bool;
cf_noreturn : bool;
cf_is_objc_block : bool;
cf_targets : Procname.t list;
}
let cf_default =
@ -575,6 +576,7 @@ let cf_default =
cf_interface = false;
cf_noreturn = false;
cf_is_objc_block = false;
cf_targets = [];
}
(** expression representing the result of decompilation *)

@ -203,6 +203,7 @@ type call_flags = {
cf_interface : bool;
cf_noreturn : bool;
cf_is_objc_block : bool;
cf_targets : Procname.t list;
}
(** Default value for call_flags where all fields are set to false *)

@ -625,12 +625,11 @@ let resolve_method tenv class_name proc_name =
proc_name
| Some proc_name -> proc_name
let resolve_typename prop arg =
let (arg_exp, _) = arg in
let resolve_typename prop receiver_exp =
let typexp_opt =
let rec loop = function
| [] -> None
| Sil.Hpointsto(e, _, typexp) :: _ when Sil.exp_equal e arg_exp -> Some typexp
| Sil.Hpointsto(e, _, typexp) :: _ when Sil.exp_equal e receiver_exp -> Some typexp
| _ :: hpreds -> loop hpreds in
loop (Prop.get_sigma prop) in
match typexp_opt with
@ -639,21 +638,62 @@ let resolve_typename prop arg =
Some (Typename.TN_csu (Csu.Class ck, name))
| _ -> None
(** If the dynamic type of the object calling a method is known, the method from the dynamic type
is called *)
let resolve_virtual_pname cfg tenv prop args pname call_flags : Procname.t =
if not call_flags.Sil.cf_virtual then pname
else
match args with
| [] -> failwith "Expecting the first parameter to be the object expression"
| obj_exp :: _ ->
begin
match resolve_typename prop obj_exp with
| Some class_name -> resolve_method tenv class_name pname
| None -> pname
end
exception Cannot_convert_string_to_typ of string
(** Lookup Java types by name *)
let lookup_java_typ_from_string tenv typ_str =
let rec loop = function
| "" | "void" -> Sil.Tvoid
| "int" -> Sil.Tint Sil.IInt
| "byte" -> Sil.Tint Sil.IShort
| "short" -> Sil.Tint Sil.IShort
| "boolean" -> Sil.Tint Sil.IBool
| "char" -> Sil.Tint Sil.IChar
| "long" -> Sil.Tint Sil.ILong
| "float" -> Sil.Tfloat Sil.FFloat
| "double" -> Sil.Tfloat Sil.FDouble
| typ_str when String.contains typ_str '[' ->
let stripped_typ = String.sub typ_str 0 ((String.length typ_str) - 2) in
let array_typ_size = Sil.exp_get_undefined false in
Sil.Tptr (Sil.Tarray (loop stripped_typ, array_typ_size), Sil.Pk_pointer)
| typ_str ->
(* non-primitive/non-array type--resolve it in the tenv *)
let typename = Typename.TN_csu (Csu.Class Csu.Java, (Mangled.from_string typ_str)) in
match Sil.tenv_lookup tenv typename with
| Some (Sil.Tstruct _ as typ) -> typ
| _ -> raise (Cannot_convert_string_to_typ typ_str) in
loop typ_str
(* let resolve_procname cfg tenv prop args pname : Procname.t = *)
(** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
in the signature of [pname], resolve [pname] to T_actual.[pname]. *)
let resolve_virtual_pname cfg tenv prop actuals pname call_flags : Procname.t =
let resolve receiver_exp pname prop = match resolve_typename prop receiver_exp with
| Some class_name -> resolve_method tenv class_name pname
| None -> pname in
let receiver_types_equal pname actual_receiver_typ =
try
let formal_receiver_typ =
let receiver_typ_str = Procname.java_get_class pname in
Sil.Tptr (lookup_java_typ_from_string tenv receiver_typ_str, Sil.Pk_pointer) in
Sil.typ_equal formal_receiver_typ actual_receiver_typ
with Cannot_convert_string_to_typ _ -> false in
match actuals with
| _ when not (call_flags.Sil.cf_virtual || call_flags.Sil.cf_interface) ->
(* if this is not a virtual or interface call, there's no need for resolution *)
pname
| (receiver_exp, actual_receiver_typ) :: _ ->
if !Config.curr_language = Config.Java && call_flags.Sil.cf_interface &&
!Config.sound_dynamic_dispatch && receiver_types_equal pname actual_receiver_typ then
(* pick one implementation of the interface method and call it *)
(* TODO: consider all implementations of the interface method *)
(* TODO: do this for virtual calls as well *)
match call_flags.Sil.cf_targets with
| target :: _ -> target
| _ -> pname
else
(* [actual_receiver_typ] <: the formal receiver_type, do resolution *)
resolve receiver_exp pname prop
| _ -> failwith "A virtual call must have a receiver"
(** recognize calls to shared_ptr procedures and re-direct them to infer procedures for modelling *)
let redirect_shared_ptr tenv cfg pname actual_params =
@ -704,7 +744,6 @@ let redirect_shared_ptr tenv cfg pname actual_params =
pname'
else pname
(** Lookup Java types by name *)
let lookup_java_typ_from_string tenv typ_str =
let rec loop = function
@ -729,7 +768,6 @@ let lookup_java_typ_from_string tenv typ_str =
| _ -> failwith ("Failed to look up typ " ^ typ_str) in
loop typ_str
(** recognize calls to the constructor java.net.URL and splits the argument string
to be only the protocol. *)
let call_constructor_url_update_args pname actual_params =
@ -1090,7 +1128,6 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
resolve_virtual_pname cfg tenv prop_r n_actual_params fn call_flags in
if !Config.ondemand_enabled then
Ondemand.do_analysis pdesc resolved_pname;
let callee_pdesc_opt = Cfg.Procdesc.find_from_name cfg resolved_pname in
let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in
let sentinel_result =

@ -157,7 +157,7 @@ let do_source_file source_file ast =
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit cfg tenv;
Preanal.doit cfg call_graph tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file call_graph;
Cfg.store_cfg_to_file cfg_file true cfg;

@ -826,6 +826,7 @@ struct
Sil.cf_interface = false;
Sil.cf_noreturn = false;
Sil.cf_is_objc_block = false;
Sil.cf_targets = [];
} in
let res_trans_call = create_call_instr trans_state_pri function_type sil_method actual_params
sil_loc call_flags ~is_objc_method:false in

@ -65,7 +65,7 @@ let store_icfg tenv cg cfg source_file =
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit cfg tenv;
Preanal.doit cfg cg tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;

@ -945,16 +945,17 @@ let rec instruction context pc instr : translation =
| JBir.InvokeVirtual (var_opt, obj, call_kind, ms, args) ->
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
let sil_obj_type = JTransType.expr_type context obj in
let create_call_node cn =
let create_call_node cn invoke_kind =
let (ids, instrs, sil_obj_expr) = expression context pc obj in
let callee_procname, call_ids, call_instrs =
let ret_opt = Some (sil_obj_expr, sil_obj_type) in
method_invocation context loc pc var_opt cn ms ret_opt args I_Virtual Procname.Non_Static in
method_invocation
context loc pc var_opt cn ms ret_opt args invoke_kind Procname.Non_Static in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
let call_node = create_node node_kind (ids @ call_ids) (instrs @ call_instrs) in
Cg.add_edge cg caller_procname callee_procname;
call_node in
let trans_virtual_call cn =
let trans_virtual_call cn invoke_kind =
match instruction_thread_start context cn ms obj args var_opt with
| Some start_call -> instruction context pc start_call
| None ->
@ -962,20 +963,20 @@ let rec instruction context pc instr : translation =
| Some cn -> cn
| None -> cn in
let cn = (resolve_method context cn ms) in
let call_node = create_call_node cn in
let call_node = create_call_node cn invoke_kind in
Instr call_node in
begin
match call_kind with
| JBir.VirtualCall obj_type ->
begin
match obj_type with
| JBasics.TClass cn -> trans_virtual_call cn
| JBasics.TClass cn -> trans_virtual_call cn I_Virtual
| JBasics.TArray vt ->
let instr = instruction_array_call ms obj_type obj args var_opt vt in
instruction context pc instr
end
| JBir.InterfaceCall cn ->
trans_virtual_call cn
trans_virtual_call cn I_Interface
end
| JBir.InvokeNonVirtual (var_opt, obj, cn, ms, args) ->
let cn = (resolve_method context cn ms) in

@ -50,7 +50,7 @@ let store_icfg tenv cg cfg =
let cg_file = get_internal_file ".cg" in
let cfg_file = get_internal_file ".cfg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit cfg tenv;
Preanal.doit cfg cg tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;

@ -244,6 +244,11 @@
"file": "codetoanalyze/java/infer/Builtins.java",
"procedure": "void Builtins.doNotBlockError(Object)"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasy()"
},
{
"bug_type": "RESOURCE_LEAK",
"file": "codetoanalyze/java/infer/CloseableAsResourceExample.java",
@ -364,6 +369,16 @@
"file": "codetoanalyze/java/infer/ReaderLeaks.java",
"procedure": "void ReaderLeaks.inputStreamReaderNotClosedAfterRead()"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasy()"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Interface)"
},
{
"bug_type": "RESOURCE_LEAK",
"file": "codetoanalyze/java/infer/ResourceLeaks.java",

@ -244,6 +244,11 @@
"file": "infer/tests/codetoanalyze/java/infer/Builtins.java",
"procedure": "void Builtins.doNotBlockError(Object)"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "infer/tests/codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasy()"
},
{
"bug_type": "RESOURCE_LEAK",
"file": "infer/tests/codetoanalyze/java/infer/CloseableAsResourceExample.java",
@ -364,6 +369,16 @@
"file": "infer/tests/codetoanalyze/java/infer/ReaderLeaks.java",
"procedure": "void ReaderLeaks.inputStreamReaderNotClosedAfterRead()"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "infer/tests/codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasy()"
},
{
"bug_type": "NULL_DEREFERENCE",
"file": "infer/tests/codetoanalyze/java/infer/DynamicDispatch.java",
"procedure": "void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Interface)"
},
{
"bug_type": "RESOURCE_LEAK",
"file": "infer/tests/codetoanalyze/java/infer/ResourceLeaks.java",

@ -0,0 +1,74 @@
/*
* Copyright (c) 2016 - 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.infer;
public class DynamicDispatch {
static interface Interface {
public Object foo();
}
static class Impl implements Interface {
@Override public Object foo() {
return null;
}
}
static void interfaceShouldNotCauseFalseNegativeEasy() {
Interface i = new Impl();
// should be a warning since Impl's implementation of foo returns null
i.foo().toString();
}
// TODO: this test currently fails, but will pass with handling of dynamic dispatch
static void interfaceShouldNotCauseFalseNegativeHard(Interface i) {
// should be a warning since Impl's implementation of foo returns null
i.foo().toString();
}
static class Supertype {
Object foo() {
return new Object();
}
Object bar() {
return null;
}
}
static class Subtype extends Supertype {
@Override Object foo() {
return null;
}
@Override Object bar() {
return new Object();
}
}
static void dynamicDispatchShouldNotCauseFalseNegativeEasy() {
Supertype o = new Subtype();
// should report a warning because we know the dynamic type of o is Subtype
o.foo().toString();
}
static void dynamicDispatchShouldNotCauseFalsePositiveEasy() {
Supertype o = new Subtype();
// should not report a warning because we know the dynamic type of o is Subtype
o.bar().toString();
}
// TODO: this test currently fails, but will pass with handling of dynamic dispatch
static void dynamicDispatchShouldNotCauseFalseNegativeHardTODO(Supertype o) {
// should report a warning because Subtype's implementation of foo() can return null;
o.foo().toString();
}
}

@ -649,6 +649,28 @@ public class ResourceLeaks {
}
}
private static void myClose(Closeable closeable, boolean swallowIOException) throws IOException {
if (closeable == null) {
return;
}
try {
closeable.close();
} catch (IOException e) {
if (!swallowIOException) {
throw e;
}
}
}
public void closeWithCloseablesNestedAlloc() throws IOException {
BufferedInputStream b = null;
try {
b = new BufferedInputStream(new FileInputStream("file.txt"));
} finally {
myClose(b, false);
}
}
// JsonParser tests
public void parseFromStringAndNotClose(JsonFactory factory) throws IOException {

@ -0,0 +1,59 @@
/*
* Copyright (c) 2016 - 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.infer;
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 DynamicDispatchTest {
public static final String DynamicDispatchFile =
"infer/tests/codetoanalyze/java/infer/DynamicDispatch.java";
public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
private static InferResults inferResults;
@BeforeClass
public static void loadResults() throws InterruptedException, IOException {
inferResults = InferResults.loadInferResults(DynamicDispatchTest.class, DynamicDispatchFile);
}
@Test
public void matchErrors()
throws InterruptedException, IOException, InferException {
String[] methods = {
"interfaceShouldNotCauseFalseNegativeEasy",
"dynamicDispatchShouldNotCauseFalseNegativeEasy",
"interfaceShouldNotCauseFalseNegativeHard"
// TODO: add dynamic dispatch support to make these tests work
// "dynamicDispatchShouldNotCauseFalseNegativeHardTODO"
};
assertThat(
"Results should contain null dereference",
inferResults,
containsExactly(
NULL_DEREFERENCE,
DynamicDispatchFile,
methods
)
);
}
}
Loading…
Cancel
Save