Dataflow: Add support for synthetic global fields in MaD.

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

@@ -83,6 +83,8 @@ predicate jumpStep(Node node1, Node node2) {
   or
   any(AdditionalValueStep a).step(node1, node2) and
   node1.getEnclosingCallable() != node2.getEnclosingCallable()
+  or
+  FlowSummaryImpl::Private::Steps::summaryJumpStep(node1, node2)
 }
 
 /**

java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll

@@ -61,6 +61,20 @@ module Public {
 
     /** Gets a summary component for a return of kind `rk`. */
     SummaryComponent return(ReturnKind rk) { result = TReturnSummaryComponent(rk) }
+
+    /** Gets a summary component for synthetic global `sg`. */
+    SummaryComponent syntheticGlobal(SyntheticGlobal sg) {
+      result = TSyntheticGlobalSummaryComponent(sg)
+    }
+
+    /**
+     * A synthetic global. This represents some form of global state, which
+     * summaries can read and write individually.
+     */
+    abstract class SyntheticGlobal extends string {
+      bindingset[this]
+      SyntheticGlobal() { any() }
+    }
   }
 
   /**
@@ -256,6 +270,7 @@ module Private {
     TParameterSummaryComponent(ArgumentPosition pos) or
     TArgumentSummaryComponent(ParameterPosition pos) or
     TReturnSummaryComponent(ReturnKind rk) or
+    TSyntheticGlobalSummaryComponent(SummaryComponent::SyntheticGlobal sg) or
     TWithoutContentSummaryComponent(ContentSet c) or
     TWithContentSummaryComponent(ContentSet c)
 
@@ -563,6 +578,11 @@ module Private {
             getCallbackReturnType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
                   s.tail())), rk)
         )
+        or
+        exists(SummaryComponent::SyntheticGlobal sg |
+          head = TSyntheticGlobalSummaryComponent(sg) and
+          result = getSyntheticGlobalType(sg)
+        )
       )
       or
       n = summaryNodeOutputState(c, s) and
@@ -582,6 +602,11 @@ module Private {
             getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
                   s.tail())), pos)
         )
+        or
+        exists(SummaryComponent::SyntheticGlobal sg |
+          head = TSyntheticGlobalSummaryComponent(sg) and
+          result = getSyntheticGlobalType(sg)
+        )
       )
     )
   }
@@ -692,6 +717,18 @@ module Private {
       )
     }
 
+    /**
+     * Holds if there is a jump step from `pred` to `succ`, which is synthesized
+     * from a flow summary.
+     */
+    predicate summaryJumpStep(Node pred, Node succ) {
+      exists(SummaryComponentStack s |
+        s = SummaryComponentStack::singleton(SummaryComponent::syntheticGlobal(_)) and
+        pred = summaryNodeOutputState(_, s) and
+        succ = summaryNodeInputState(_, s)
+      )
+    }
+
     /**
      * Holds if values stored inside content `c` are cleared at `n`. `n` is a
      * synthesized summary node, so in order for values to be cleared at calls
@@ -871,18 +908,28 @@ module Private {
       AccessPathRange() { relevantSpec(this) }
     }
 
-    /** Holds if specification component `c` parses as parameter `n`. */
+    /** Holds if specification component `token` parses as parameter `pos`. */
     predicate parseParam(AccessPathToken token, ArgumentPosition pos) {
       token.getName() = "Parameter" and
       pos = parseParamBody(token.getAnArgument())
     }
 
-    /** Holds if specification component `c` parses as argument `n`. */
+    /** Holds if specification component `token` parses as argument `pos`. */
     predicate parseArg(AccessPathToken token, ParameterPosition pos) {
       token.getName() = "Argument" and
       pos = parseArgBody(token.getAnArgument())
     }
 
+    /** Holds if specification component `token` parses as synthetic global `sg`. */
+    predicate parseSynthGlobal(AccessPathToken token, string sg) {
+      token.getName() = "SyntheticGlobal" and
+      sg = token.getAnArgument()
+    }
+
+    private class SyntheticGlobalFromAccessPath extends SummaryComponent::SyntheticGlobal {
+      SyntheticGlobalFromAccessPath() { parseSynthGlobal(_, this) }
+    }
+
     private SummaryComponent interpretComponent(AccessPathToken token) {
       exists(ParameterPosition pos |
         parseArg(token, pos) and result = SummaryComponent::argument(pos)
@@ -894,6 +941,10 @@ module Private {
       or
       token = "ReturnValue" and result = SummaryComponent::return(getReturnValueKind())
       or
+      exists(string sg |
+        parseSynthGlobal(token, sg) and result = SummaryComponent::syntheticGlobal(sg)
+      )
+      or
       result = interpretComponentSpecific(token)
     }
 

java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll

@@ -55,6 +55,12 @@ DataFlowType getCallbackReturnType(DataFlowType t, ReturnKind rk) {
   exists(rk)
 }
 
+/** Gets the type of synthetic global `sg`. */
+DataFlowType getSyntheticGlobalType(SummaryComponent::SyntheticGlobal sg) {
+  exists(sg) and
+  result instanceof TypeObject
+}
+
 bindingset[provenance]
 private boolean isGenerated(string provenance) {
   provenance = "generated" and result = true

java/ql/test/library-tests/dataflow/synth-global/A.java

@@ -0,0 +1,25 @@
+package my.qltest.synth;
+
+public class A {
+  void storeInArray(String x) { }
+  void storeTaintInArray(String x) { }
+  void storeValue(String x) { }
+
+  String readValue() { return null; }
+  String readArray() { return null; }
+
+  String source(String tag) { return "tainted"; }
+
+  void sink(Object o) { }
+
+  void stores() {
+    storeInArray(source("A"));
+    storeTaintInArray(source("B"));
+    storeValue(source("C"));
+  }
+
+  void reads() {
+    sink(readValue()); // $ hasValueFlow=C
+    sink(readArray()); // $ hasValueFlow=A hasTaintFlow=B hasTaintFlow=C
+  }
+}

java/ql/test/library-tests/dataflow/synth-global/test.expected

@@ -0,0 +1,2 @@
+failures
+invalidModelRow

java/ql/test/library-tests/dataflow/synth-global/test.ql

@@ -0,0 +1,17 @@
+import java
+import TestUtilities.InlineFlowTest
+import semmle.code.java.dataflow.ExternalFlow
+import CsvValidation
+
+class SummaryModelTest extends SummaryModelCsv {
+  override predicate row(string row) {
+    row =
+      [
+        "my.qltest.synth;A;false;storeInArray;(String);;Argument[0];SyntheticGlobal[db1].ArrayElement;value;manual",
+        "my.qltest.synth;A;false;storeTaintInArray;(String);;Argument[0];SyntheticGlobal[db1].ArrayElement;taint;manual",
+        "my.qltest.synth;A;false;storeValue;(String);;Argument[0];SyntheticGlobal[db1];value;manual",
+        "my.qltest.synth;A;false;readValue;();;SyntheticGlobal[db1];ReturnValue;value;manual",
+        "my.qltest.synth;A;false;readArray;();;SyntheticGlobal[db1].ArrayElement;ReturnValue;value;manual",
+      ]
+  }
+}