Model Arrays.copyOf for non-functional arrays for soundness

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

@@ -97,7 +97,7 @@ public abstract class AbstractHeapModel implements HeapModel {
 
     private final Map<Type, Obj> zeroLengthArrays = Maps.newMap();
 
-    private static final Descriptor zeroLengthArrayDesc = () -> "ZeroLengthArray";
+    public static final Descriptor ZERO_LENGTH_ARRAY_DESC = () -> "ZeroLengthArray";
 
     /**
      * Counter for indexing Objs.
@@ -204,7 +204,7 @@ protected NewObj getNewObj(New allocSite) {
      */
     protected Obj getZeroLengthArrayObj(Type type) {
         return zeroLengthArrays.computeIfAbsent(type,
-                t -> getMockObj(zeroLengthArrayDesc,
+                t -> getMockObj(ZERO_LENGTH_ARRAY_DESC,
                         "<Merged zero-length " + t + ">", t, false));
     }
 

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

@@ -29,7 +29,6 @@
 import pascal.taie.ir.exp.CastExp;
 import pascal.taie.ir.exp.Var;
 import pascal.taie.ir.stmt.Cast;
-import pascal.taie.ir.stmt.Copy;
 import pascal.taie.ir.stmt.Invoke;
 import pascal.taie.ir.stmt.LoadArray;
 import pascal.taie.ir.stmt.Stmt;
@@ -42,7 +41,7 @@
 
 import java.util.List;
 
-public class ArrayModel extends IRModelPlugin {
+public class ArrayCopyModel extends IRModelPlugin {
 
     private final ClassType objType;
 
@@ -53,20 +52,12 @@ public class ArrayModel extends IRModelPlugin {
      */
     private int counter = 0;
 
-    ArrayModel(Solver solver) {
+    ArrayCopyModel(Solver solver) {
         super(solver);
         objType = typeSystem.getClassType(ClassNames.OBJECT);
         objArrayType = typeSystem.getArrayType(objType, 1);
     }
 
-    @InvokeHandler(signature = "<java.util.Arrays: java.lang.Object[] copyOf(java.lang.Object[],int)>")
-    public List<Stmt> arraysCopyOf(Invoke invoke) {
-        Var result = invoke.getResult();
-        return result != null
-                ? List.of(new Copy(result, invoke.getInvokeExp().getArg(0)))
-                : List.of();
-    }
-
     @InvokeHandler(signature = "<java.lang.System: void arraycopy(java.lang.Object,int,java.lang.Object,int,int)>")
     public List<Stmt> systemArraycopy(Invoke invoke) {
         JMethod container = invoke.getContainer();

src/main/java/pascal/taie/analysis/pta/plugin/natives/ArrayCopyOfModel.java

@@ -0,0 +1,70 @@
+/*
+ * Tai-e: A Static Analysis Framework for Java
+ *
+ * Copyright (C) 2022 Tian Tan <tiantan@nju.edu.cn>
+ * Copyright (C) 2022 Yue Li <yueli@nju.edu.cn>
+ *
+ * This file is part of Tai-e.
+ *
+ * Tai-e is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU Lesser General Public License
+ * as published by the Free Software Foundation, either version 3
+ * of the License, or (at your option) any later version.
+ *
+ * Tai-e is distributed in the hope that it will be useful,but WITHOUT
+ * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+ * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General
+ * Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with Tai-e. If not, see <https://www.gnu.org/licenses/>.
+ */
+
+package pascal.taie.analysis.pta.plugin.natives;
+
+import pascal.taie.analysis.pta.core.cs.context.Context;
+import pascal.taie.analysis.pta.core.cs.element.CSObj;
+import pascal.taie.analysis.pta.core.cs.element.Pointer;
+import pascal.taie.analysis.pta.core.heap.AbstractHeapModel;
+import pascal.taie.analysis.pta.core.heap.Descriptor;
+import pascal.taie.analysis.pta.core.heap.MockObj;
+import pascal.taie.analysis.pta.core.solver.Solver;
+import pascal.taie.analysis.pta.plugin.util.AnalysisModelPlugin;
+import pascal.taie.analysis.pta.plugin.util.InvokeHandler;
+import pascal.taie.analysis.pta.pts.PointsToSet;
+import pascal.taie.ir.exp.Var;
+import pascal.taie.ir.stmt.Invoke;
+import pascal.taie.util.collection.Sets;
+
+import java.util.Set;
+
+public class ArrayCopyOfModel extends AnalysisModelPlugin {
+
+    private static final Descriptor COPYOF_ARRAY_DESC = () -> "ArrayGeneratedByCopyOfModel";
+
+    ArrayCopyOfModel(Solver solver) {
+        super(solver);
+    }
+
+    @InvokeHandler(signature = "<java.util.Arrays: java.lang.Object[] copyOf(java.lang.Object[],int)>", argIndexes = {0})
+    public void arraysCopyOf(Context context, Invoke invoke, PointsToSet from) {
+        Var result = invoke.getResult();
+        if(result != null){
+            Pointer to = solver.getCSManager().getCSVar(context, result);
+            Set<CSObj> toObjs = Sets.newHybridSet();
+            from.getObjects().forEach(csObj -> {
+                // handle the argument0's obj is zero-length-array obj
+                if(csObj.getObject() instanceof MockObj mockObj
+                        && mockObj.getDescriptor().equals(AbstractHeapModel.ZERO_LENGTH_ARRAY_DESC)){
+                    toObjs.add(solver.getCSManager().getCSObj(context,
+                            heapModel.getMockObj(COPYOF_ARRAY_DESC, invoke, mockObj.getType())));
+                }
+                else {
+                    toObjs.add(csObj);
+                }
+            });
+            toObjs.forEach(csObj -> solver.addPointsTo(to, csObj));
+        }
+    }
+
+}

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

@@ -33,7 +33,8 @@ public class NativeModeller extends CompositePlugin {
 
     @Override
     public void setSolver(Solver solver) {
-        addPlugin(new ArrayModel(solver),
+        addPlugin(new ArrayCopyModel(solver),
+                new ArrayCopyOfModel(solver),
                 new UnsafeModel(solver),
                 new DoPriviledgedModel(solver));
     }

src/test/java/pascal/taie/analysis/pta/TaintTest.java

@@ -74,6 +74,8 @@ public class TaintTest {
             TAINT_CONFIG_PREFIX + "taint-config-call-source.yml"})
     @MultiStringsSource({"CallSiteMode",
             TAINT_CONFIG_PREFIX + "taint-config-call-site-model.yml"})
+    @MultiStringsSource({"ZeroLengthArrayWithArraysCopyOf",
+            TAINT_CONFIG_PREFIX + "taint-config-zero-length-array-with-arrays-copy-of.yml"})
     void test(String mainClass, String... opts) {
         testInNonInteractiveMode(mainClass, opts);
         testInInteractiveMode(mainClass, opts);

src/test/resources/pta/taint/ZeroLengthArrayWithArraysCopyOf-pta-expected.txt

@@ -0,0 +1,2 @@
+Detected 1 taint flow(s):
+TaintFlow{<ZeroLengthArrayWithArraysCopyOf: void testZeroLengthArrayPath()>[10@L12] temp$8 = invokestatic ZeroLengthArrayWithArraysCopyOf.getSourceData()/result -> <ZeroLengthArrayWithArraysCopyOf: void testZeroLengthArrayPath()>[15@L13] invokestatic ZeroLengthArrayWithArraysCopyOf.sink(temp$13)/0}

src/test/resources/pta/taint/ZeroLengthArrayWithArraysCopyOf.java

@@ -0,0 +1,24 @@
+import java.util.Arrays;
+
+public class ZeroLengthArrayWithArraysCopyOf{
+
+    public static void main(String[] args) {
+        testZeroLengthArrayPath();
+    }
+
+    public static void testZeroLengthArrayPath() {
+        String[] original = new String[0];
+        String[] copy = Arrays.copyOf(original, original.length + 1);
+        copy[copy.length - 1] = getSourceData();
+        sink(copy[copy.length - 1]);
+    }
+
+    public static String getSourceData() {
+        return "source_data";
+    }
+
+    public static void sink(String data) {
+        System.out.println("Sink: " + data);
+    }
+
+}

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

@@ -0,0 +1,6 @@
+sources:
+  - { kind: call, method: "<ZeroLengthArrayWithArraysCopyOf: java.lang.String getSourceData()>", index: result }
+
+sinks:
+  - { method: "<ZeroLengthArrayWithArraysCopyOf: void sink(java.lang.String)>", index: 0 }
+