Java: add a failing test for stateful in/out barriers

Author: asgerf

java/ql/test/library-tests/dataflow/inoutbarriers/test.expected

@@ -1,3 +1,8 @@
+inconsistentFlow
+| A.java:9:16:9:19 | fsrc | A.java:15:10:15:10 | s | spurious state-flow in configuration sinkbarrier |
+| A.java:12:9:12:14 | src(...) | A.java:15:10:15:10 | s | spurious state-flow in configuration both |
+| A.java:12:9:12:14 | src(...) | A.java:15:10:15:10 | s | spurious state-flow in configuration sinkbarrier |
+#select
 | A.java:9:16:9:19 | fsrc | A.java:13:10:13:10 | s | nobarrier, sinkbarrier |
 | A.java:9:16:9:19 | fsrc | A.java:15:10:15:10 | s | nobarrier |
 | A.java:10:10:10:13 | fsrc | A.java:10:10:10:13 | fsrc | both, nobarrier, sinkbarrier, srcbarrier |

java/ql/test/library-tests/dataflow/inoutbarriers/test.ql

@@ -46,6 +46,46 @@ module Conf4 implements ConfigSig {
   predicate isBarrierOut(Node n) { sink0(n) }
 }
 
+module StateConf1 implements StateConfigSig {
+  class FlowState = Unit;
+
+  predicate isSource(Node n, FlowState state) { src0(n) and exists(state) }
+
+  predicate isSink(Node n, FlowState state) { sink0(n) and exists(state) }
+}
+
+module StateConf2 implements StateConfigSig {
+  class FlowState = Unit;
+
+  predicate isSource(Node n, FlowState state) { src0(n) and exists(state) }
+
+  predicate isSink(Node n, FlowState state) { sink0(n) and exists(state) }
+
+  predicate isBarrierIn(Node n, FlowState state) { isSource(n, state) }
+}
+
+module StateConf3 implements StateConfigSig {
+  class FlowState = Unit;
+
+  predicate isSource(Node n, FlowState state) { src0(n) and exists(state) }
+
+  predicate isSink(Node n, FlowState state) { sink0(n) and exists(state) }
+
+  predicate isBarrierOut(Node n, FlowState state) { isSink(n, state) }
+}
+
+module StateConf4 implements StateConfigSig {
+  class FlowState = Unit;
+
+  predicate isSource(Node n, FlowState state) { src0(n) and exists(state) }
+
+  predicate isSink(Node n, FlowState state) { sink0(n) and exists(state) }
+
+  predicate isBarrierIn(Node n, FlowState state) { isSource(n, state) }
+
+  predicate isBarrierOut(Node n, FlowState state) { isSink(n, state) }
+}
+
 predicate flow(Node src, Node sink, string s) {
   Global<Conf1>::flow(src, sink) and s = "nobarrier"
   or
@@ -56,6 +96,26 @@ predicate flow(Node src, Node sink, string s) {
   Global<Conf4>::flow(src, sink) and s = "both"
 }
 
+predicate stateFlow(Node src, Node sink, string s) {
+  GlobalWithState<StateConf1>::flow(src, sink) and s = "nobarrier"
+  or
+  GlobalWithState<StateConf2>::flow(src, sink) and s = "srcbarrier"
+  or
+  GlobalWithState<StateConf3>::flow(src, sink) and s = "sinkbarrier"
+  or
+  GlobalWithState<StateConf4>::flow(src, sink) and s = "both"
+}
+
+query predicate inconsistentFlow(Node src, Node sink, string message) {
+  exists(string kind |
+    (flow(src, sink, kind) and not stateFlow(src, sink, kind)) and
+    message = "missing state-flow in configuration " + kind
+    or
+    (not flow(src, sink, kind) and stateFlow(src, sink, kind)) and
+    message = "spurious state-flow in configuration " + kind
+  )
+}
+
 from Node src, Node sink, string s
 where flow(src, sink, _) and s = concat(any(string s0 | flow(src, sink, s0)), ", ")
 select src, sink, s