Skip to content

Commit 89a4ea0

Browse files
auroraberryjjppp
auroraberry
and
jjppp
authored
Model Arrays.copyOf for non-functional arrays for soundness (#191)
Co-authored-by: jpwang <[email protected]>
1 parent dde6c6c commit 89a4ea0

File tree

6 files changed

+121
-38
lines changed

6 files changed

+121
-38
lines changed

‎src/main/java/pascal/taie/analysis/pta/core/heap/AbstractHeapModel.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ public abstract class AbstractHeapModel implements HeapModel {
9797

9898
private final Map<Type, Obj> zeroLengthArrays = Maps.newMap();
9999

100-
private static final Descriptor zeroLengthArrayDesc = () -> "ZeroLengthArray";
100+
private static final Descriptor ZERO_LENGTH_ARRAY_DESC = () -> "ZeroLengthArray";
101101

102102
/**
103103
* Counter for indexing Objs.
@@ -204,7 +204,7 @@ protected NewObj getNewObj(New allocSite) {
204204
*/
205205
protected Obj getZeroLengthArrayObj(Type type) {
206206
return zeroLengthArrays.computeIfAbsent(type,
207-
t -> getMockObj(zeroLengthArrayDesc,
207+
t -> getMockObj(ZERO_LENGTH_ARRAY_DESC,
208208
"<Merged zero-length " + t + ">", t, false));
209209
}
210210

‎src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayModel.java‎

Lines changed: 71 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -22,14 +22,19 @@
2222

2323
package pascal.taie.analysis.pta.plugin.natives;
2424

25+
import pascal.taie.analysis.pta.core.cs.context.Context;
26+
import pascal.taie.analysis.pta.core.cs.element.CSObj;
27+
import pascal.taie.analysis.pta.core.heap.Descriptor;
28+
import pascal.taie.analysis.pta.core.heap.Obj;
2529
import pascal.taie.analysis.pta.core.solver.Solver;
30+
import pascal.taie.analysis.pta.plugin.util.AnalysisModelPlugin;
2631
import pascal.taie.analysis.pta.plugin.util.IRModelPlugin;
2732
import pascal.taie.analysis.pta.plugin.util.InvokeHandler;
33+
import pascal.taie.analysis.pta.pts.PointsToSet;
2834
import pascal.taie.ir.exp.ArrayAccess;
2935
import pascal.taie.ir.exp.CastExp;
3036
import pascal.taie.ir.exp.Var;
3137
import pascal.taie.ir.stmt.Cast;
32-
import pascal.taie.ir.stmt.Copy;
3338
import pascal.taie.ir.stmt.Invoke;
3439
import pascal.taie.ir.stmt.LoadArray;
3540
import pascal.taie.ir.stmt.Stmt;
@@ -42,47 +47,78 @@
4247

4348
import java.util.List;
4449

45-
public class ArrayModel extends IRModelPlugin {
50+
public class ArrayModel {
4651

47-
private final ClassType objType;
52+
private static final Descriptor COPY_OF_ARRAY_DESC = () -> "ArrayGeneratedByCopyOfModel";
4853

49-
private final ArrayType objArrayType;
54+
public static class AnalysisModel extends AnalysisModelPlugin {
5055

51-
/**
52-
* Counter for naming temporary variables.
53-
*/
54-
private int counter = 0;
56+
AnalysisModel(Solver solver) {
57+
super(solver);
58+
}
5559

56-
ArrayModel(Solver solver) {
57-
super(solver);
58-
objType = typeSystem.getClassType(ClassNames.OBJECT);
59-
objArrayType = typeSystem.getArrayType(objType, 1);
60-
}
60+
@Override
61+
public void onStart() {
62+
// Solver should ignore `Arrays.copyOf()` to avoid spurious flows merging from other
63+
// callsites, as in the `IRModelPlugin.onStart()`.
64+
handlers.keySet().forEach(solver::addIgnoredMethod);
65+
}
6166

62-
@InvokeHandler(signature = "<java.util.Arrays: java.lang.Object[] copyOf(java.lang.Object[],int)>")
63-
public List<Stmt> arraysCopyOf(Invoke invoke) {
64-
Var result = invoke.getResult();
65-
return result != null
66-
? List.of(new Copy(result, invoke.getInvokeExp().getArg(0)))
67-
: List.of();
67+
@InvokeHandler(signature = "<java.util.Arrays: java.lang.Object[] copyOf(java.lang.Object[],int)>", argIndexes = {0})
68+
public void arraysCopyOf(Context context, Invoke invoke, PointsToSet from) {
69+
JMethod container = invoke.getContainer();
70+
Var result = invoke.getResult();
71+
if (result != null) {
72+
from.getObjects().forEach(csObj -> {
73+
// When the array object from the first argument is not functional,
74+
// create a new functional array
75+
if (!csObj.getObject().isFunctional()) {
76+
Type type = csObj.getObject().getType();
77+
Obj newArray = heapModel.getMockObj(COPY_OF_ARRAY_DESC, invoke, type, container);
78+
CSObj csNewArray = csManager.getCSObj(context, newArray);
79+
solver.addVarPointsTo(context, result, csNewArray);
80+
} else {
81+
solver.addVarPointsTo(context, result, csObj);
82+
}
83+
});
84+
}
85+
}
6886
}
6987

70-
@InvokeHandler(signature = "<java.lang.System: void arraycopy(java.lang.Object,int,java.lang.Object,int,int)>")
71-
public List<Stmt> systemArraycopy(Invoke invoke) {
72-
JMethod container = invoke.getContainer();
73-
Var src = getTempVar(container, "src", objArrayType);
74-
Var dest = getTempVar(container, "dest", objArrayType);
75-
Var temp = getTempVar(container, "temp", objType);
76-
List<Var> args = invoke.getInvokeExp().getArgs();
77-
return List.of(
78-
new Cast(src, new CastExp(args.get(0), objArrayType)),
79-
new Cast(dest, new CastExp(args.get(2), objArrayType)),
80-
new LoadArray(temp, new ArrayAccess(src, args.get(1))),
81-
new StoreArray(new ArrayAccess(dest, args.get(3)), temp));
82-
}
88+
public static class IRModel extends IRModelPlugin {
89+
90+
private final ClassType objType;
91+
92+
private final ArrayType objArrayType;
93+
94+
/**
95+
* Counter for naming temporary variables.
96+
*/
97+
private int counter = 0;
98+
99+
IRModel(Solver solver) {
100+
super(solver);
101+
objType = typeSystem.getClassType(ClassNames.OBJECT);
102+
objArrayType = typeSystem.getArrayType(objType, 1);
103+
}
104+
105+
@InvokeHandler(signature = "<java.lang.System: void arraycopy(java.lang.Object,int,java.lang.Object,int,int)>")
106+
public List<Stmt> systemArraycopy(Invoke invoke) {
107+
JMethod container = invoke.getContainer();
108+
Var src = getTempVar(container, "src", objArrayType);
109+
Var dest = getTempVar(container, "dest", objArrayType);
110+
Var temp = getTempVar(container, "temp", objType);
111+
List<Var> args = invoke.getInvokeExp().getArgs();
112+
return List.of(
113+
new Cast(src, new CastExp(args.get(0), objArrayType)),
114+
new Cast(dest, new CastExp(args.get(2), objArrayType)),
115+
new LoadArray(temp, new ArrayAccess(src, args.get(1))),
116+
new StoreArray(new ArrayAccess(dest, args.get(3)), temp));
117+
}
83118

84-
private Var getTempVar(JMethod container, String name, Type type) {
85-
String varName = "%native-arraycopy-" + name + counter++;
86-
return new Var(container, varName, type, -1);
119+
private Var getTempVar(JMethod container, String name, Type type) {
120+
String varName = "%native-arraycopy-" + name + counter++;
121+
return new Var(container, varName, type, -1);
122+
}
87123
}
88124
}

‎src/main/java/pascal/taie/analysis/pta/plugin/natives/NativeModeller.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ public class NativeModeller extends CompositePlugin {
3333

3434
@Override
3535
public void setSolver(Solver solver) {
36-
addPlugin(new ArrayModel(solver),
36+
addPlugin(new ArrayModel.AnalysisModel(solver),
37+
new ArrayModel.IRModel(solver),
3738
new UnsafeModel(solver),
3839
new DoPriviledgedModel(solver));
3940
}

‎src/test/java/pascal/taie/analysis/pta/BasicTestFull.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,11 @@
2222

2323
package pascal.taie.analysis.pta;
2424

25+
import org.junit.jupiter.api.Test;
2526
import org.junit.jupiter.params.ParameterizedTest;
27+
import pascal.taie.Main;
2628
import pascal.taie.analysis.Tests;
29+
import pascal.taie.analysis.pta.plugin.assertion.AssertionChecker;
2730
import pascal.taie.util.MultiStringsSource;
2831

2932
public class BasicTestFull extends BasicTest {
@@ -55,4 +58,17 @@ void testFull(String mainClass, String... opts) {
5558
Tests.testPTA(DIR, mainClass, opts);
5659
}
5760

61+
@Test
62+
void testZeroLengthArrayWithArraysCopyOf() {
63+
String ptaTestRoot = "src/test/resources/pta";
64+
String classPath = ptaTestRoot + "/" + DIR;
65+
Main.main("-pp",
66+
"-cp", ptaTestRoot,
67+
"-cp", classPath,
68+
"-m", "ZeroLengthArrayWithArraysCopyOf",
69+
"-a", "pta=implicit-entries:false;" +
70+
"plugins:[" + AssertionChecker.class.getName() + "]"
71+
);
72+
}
73+
5874
}

‎src/test/resources/pta/basic/ZeroLengthArrayWithArraysCopyOf.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import java.util.Arrays;
2+
3+
public class ZeroLengthArrayWithArraysCopyOf {
4+
5+
public static void main(String[] args) {
6+
testZeroLengthArrayPath();
7+
}
8+
9+
public static void testZeroLengthArrayPath() {
10+
String[] original = new String[0];
11+
String[] copy = Arrays.copyOf(original, original.length + 1);
12+
PTAAssert.sizeEquals(1, copy);
13+
PTAAssert.notEquals(original, copy);
14+
String src = getSourceData();
15+
copy[copy.length - 1] = src;
16+
String dst = copy[copy.length - 1];
17+
PTAAssert.equals(dst, src);
18+
}
19+
20+
public static String getSourceData() {
21+
return "source_data";
22+
}
23+
24+
}

‎src/test/resources/pta/taint/taint-config-zero-length-array-with-arrays-copy-of.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
sources:
2+
- { kind: call, method: "<ZeroLengthArrayWithArraysCopyOf: java.lang.String getSourceData()>", index: result }
3+
4+
sinks:
5+
- { method: "<ZeroLengthArrayWithArraysCopyOf: void sink(java.lang.String)>", index: 0 }
6+

0 commit comments

Comments
 (0)