pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fixing unsound old devirtualization performed in Java frontend

Browse Source 
Summary:
The java frontend used an unsound flow insensitive class analysis to devirtualize
some virtual calls. We remove it and let the recent devirtualizer preanalysis do the job.

This unsoudness in the Java frontend may have been here for a long time. Removing it may
modify several analysis results (specially Nullsafe) where virtual calls may look different
now.

Reviewed By: jvillard

Differential Revision: D22662739

fbshipit-source-id: c45296dce
master
David Pichardie 5 years ago committed by Facebook GitHub Bot
parent 2547a75b8b
commit f6b125c928
7 changed files with 13 additions and 39 deletions
Show Stats Download Patch File Download Diff File

12
infer/src/java/jTrans.ml
Unescape View File

@ -1070,17 +1070,7 @@ let instruction (context : JContext.t) pc instr : translation =
let call_node = create_node node_kind (instrs @ call_instrs) in
call_node
in
let trans_virtual_call original_cn invoke_kind =
let cn' =
match JTransType.extract_cn_no_obj sil_obj_type with
| Some cn ->
cn
| None ->
original_cn
in
let call_node = create_call_node cn' invoke_kind in
Instr call_node
in
let trans_virtual_call cn invoke_kind = Instr (create_call_node cn invoke_kind) in
match call_kind with
| JBir.VirtualCall obj_type ->
let cn =

9
infer/src/java/jTransType.ml
Unescape View File

@ -71,15 +71,6 @@ let rec create_array_type typ dim =
else typ
let extract_cn_no_obj (typ : Typ.t) =
match typ.desc with
| Tptr ({desc= Tstruct (JavaClass _ as name)}, Pk_pointer) ->
let class_name = JBasics.make_cn (Typ.Name.name name) in
if JBasics.cn_equal class_name JBasics.java_lang_object then None else Some class_name
| _ ->
None
(** Printing types *)
let object_type_to_string ot =
let rec array_type_to_string (vt : JBasics.value_type) =

4
infer/src/java/jTransType.mli
Unescape View File

@ -64,9 +64,5 @@ val package_to_string : string list -> string option
val create_array_type : Typ.t -> int -> Typ.t
(** [create_array_type typ dim] creates an array type with dimension dim and content typ *)
val extract_cn_no_obj : Typ.t -> JBasics.class_name option
(** [extract_cn_type_np] returns the Java class name of typ when typ is a pointer type, otherwise
returns None *)
val object_type_to_string : JBasics.object_type -> string
(** returns a string representation of an object Java type *)

2
infer/tests/codetoanalyze/java/biabduction/ReaderLeaks.java
Unescape View File

@ -34,7 +34,7 @@ public class ReaderLeaks {
}
}
public void readerClosed() throws IOException {
public void readerClosed_FP() throws IOException {
Reader r = null;
try {
r = new FileReader("testing.txt");

1
infer/tests/codetoanalyze/java/biabduction/issues.exp
Unescape View File

@ -137,6 +137,7 @@ codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.Reader
codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConnect(java.io.PipedWriter):void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConnect(...),exception java.io.IOException]
codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pipedReaderNotClosedAfterConstructedWithWriter():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pipedReaderNotClosedAfterConstructedWithWriter(),exception java.io.IOException]
codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.pushbackReaderNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure pushbackReaderNotClosedAfterRead(),Skipping PushbackReader(...): unknown method,exception java.io.IOException]
codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerClosed_FP():void, 8, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerClosed_FP(),Skipping FileReader(...): unknown method,exception java.io.IOException,Switch condition is true. Entering switch case,Taking true branch]
codetoanalyze/java/biabduction/ReaderLeaks.java, codetoanalyze.java.infer.ReaderLeaks.readerNotClosedAfterRead():void, 6, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure readerNotClosedAfterRead(),Skipping FileReader(...): unknown method,exception java.io.IOException]
codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.NoResourceLeakWarningAfterCheckState(java.io.File,int):void, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure NoResourceLeakWarningAfterCheckState(...),Taking false branch]
codetoanalyze/java/biabduction/ResourceLeaks.java, codetoanalyze.java.infer.ResourceLeaks.activityObtainTypedArrayAndLeak(android.app.Activity):void, 2, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure activityObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(TypedArray)]

22
infer/tests/codetoanalyze/java/pulse/DefaultInInterface.java
Unescape View File

@ -45,23 +45,19 @@ public class DefaultInInterface {
}
}
static void FN_uncertainCallNPE(int i) {
A firstAthenB = new A();
static void uncertainCallMethod1NPE(int i) {
A aAorB = new A();
if (i > 0) { // feasible path
firstAthenB = new B();
aAorB = new B();
}
System.out.println(firstAthenB.defaultMethod1().toString());
System.out.println(aAorB.defaultMethod1().toString());
}
static boolean alwaysFalse() {
return false;
}
static void FP_uncertainCallOk(int i) {
A firstAthenB = new A();
if (alwaysFalse()) { // unfeasible path
firstAthenB = new B();
static void FN_uncertainCallMethod2NPE(int i) {
A aAorB = new A();
if (i > 0) { // feasible path
aAorB = new B();
}
System.out.println(firstAthenB.defaultMethod2().toString());
System.out.println(aAorB.defaultMethod2().toString());
}
}

2
infer/tests/codetoanalyze/java/pulse/issues.exp
Unescape View File

@ -1,6 +1,6 @@
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$A.defaultCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface$B.overridenCallNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.FP_uncertainCallOk(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$B.defaultMethod2()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$B.defaultMethod2()`,return from call to `Object DefaultInInterface$B.defaultMethod2()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DefaultInInterface.java, DefaultInInterface.uncertainCallMethod1NPE(int):void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DefaultInInterface$I.defaultMethod1()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DefaultInInterface$I.defaultMethod1()`,return from call to `Object DefaultInInterface$I.defaultMethod1()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Supertype.bar()`,return from call to `Object DynamicDispatch$Supertype.bar()`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeOK_FP():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]
codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)` here,when calling `Object DynamicDispatch$Supertype.bar()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,return from call to `Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)`,assigned,invalid access occurs here]

Write Preview
Loading…
Cancel
Save