Skip to content

Commit 6c91867

Browse files
alexetalexet
committed
Make it so obvelray infomredness doesn't always apply.
1 parent aa500df commit 6c91867

File tree

5 files changed

+427
-220
lines changed

5 files changed

+427
-220
lines changed

‎java/ql/lib/experimental/quantum/JCA.qll‎

Lines changed: 16 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -556,40 +556,32 @@ module JCAModel {
556556

557557
module GetInstanceToInitToUseFlow = DataFlow::GlobalWithState<GetInstanceToInitToUseConfig>;
558558

559-
GetInstance getInstantiationFromUse(
560-
Use use, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
561-
) {
562-
src.getNode().asExpr() = result and
563-
sink.getNode().asExpr() = use.(MethodCall).getQualifier() and
564-
GetInstanceToInitToUseFlow::flowPath(src, sink)
559+
GetInstance getInstantiationFromUse(Use use, DataFlow::Node src, DataFlow::Node sink) {
560+
src.asExpr() = result and
561+
sink.asExpr() = use.(MethodCall).getQualifier() and
562+
GetInstanceToInitToUseFlow::flow(src, sink)
565563
}
566564

567-
GetInstance getInstantiationFromInit(
568-
Init init, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
569-
) {
570-
src.getNode().asExpr() = result and
571-
sink.getNode().asExpr() = init.(MethodCall).getQualifier() and
572-
GetInstanceToInitToUseFlow::flowPath(src, sink)
565+
GetInstance getInstantiationFromInit(Init init, DataFlow::Node src, DataFlow::Node sink) {
566+
src.asExpr() = result and
567+
sink.asExpr() = init.(MethodCall).getQualifier() and
568+
GetInstanceToInitToUseFlow::flow(src, sink)
573569
}
574570

575-
Init getInitFromUse(
576-
Use use, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
577-
) {
578-
src.getNode().asExpr() = result.(MethodCall).getQualifier() and
579-
sink.getNode().asExpr() = use.(MethodCall).getQualifier() and
580-
GetInstanceToInitToUseFlow::flowPath(src, sink)
571+
Init getInitFromUse(Use use, DataFlow::Node src, DataFlow::Node sink) {
572+
src.asExpr() = result.(MethodCall).getQualifier() and
573+
sink.asExpr() = use.(MethodCall).getQualifier() and
574+
GetInstanceToInitToUseFlow::flow(src, sink)
581575
}
582576

583577
predicate hasInit(Use use) { exists(getInitFromUse(use, _, _)) }
584578

585-
Use getAnIntermediateUseFromFinalUse(
586-
Use final, GetInstanceToInitToUseFlow::PathNode src, GetInstanceToInitToUseFlow::PathNode sink
587-
) {
579+
Use getAnIntermediateUseFromFinalUse(Use final, DataFlow::Node src, DataFlow::Node sink) {
588580
not final.isIntermediate() and
589581
result.isIntermediate() and
590-
src.getNode().asExpr() = result.(MethodCall).getQualifier() and
591-
sink.getNode().asExpr() = final.(MethodCall).getQualifier() and
592-
GetInstanceToInitToUseFlow::flowPath(src, sink)
582+
src.asExpr() = result.(MethodCall).getQualifier() and
583+
sink.asExpr() = final.(MethodCall).getQualifier() and
584+
GetInstanceToInitToUseFlow::flow(src, sink)
593585
}
594586
}
595587

‎shared/dataflow/codeql/dataflow/DataFlow.qll‎

Lines changed: 130 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -657,7 +657,7 @@ private module PathGraphSigMod {
657657
}
658658
}
659659

660-
module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
660+
module DataFlowMakeCore<LocationSig Location, InputSig<Location> Lang> {
661661
private import Lang
662662
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
663663
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
@@ -703,58 +703,6 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
703703
predicate flowToExpr(DataFlowExpr sink);
704704
}
705705

706-
/**
707-
* Constructs a global data flow computation.
708-
*/
709-
module Global<ConfigSig Config> implements GlobalFlowSig {
710-
private module C implements FullStateConfigSig {
711-
import DefaultState<Config>
712-
import Config
713-
714-
predicate accessPathLimit = Config::accessPathLimit/0;
715-
716-
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
717-
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
718-
}
719-
}
720-
721-
private module Stage1 = ImplStage1<C>;
722-
723-
import Stage1::PartialFlow
724-
725-
private module Flow = Impl<C, Stage1::Stage1NoState>;
726-
727-
import Flow
728-
}
729-
730-
/**
731-
* Constructs a global data flow computation using flow state.
732-
*/
733-
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
734-
private module C implements FullStateConfigSig {
735-
import Config
736-
737-
predicate accessPathLimit = Config::accessPathLimit/0;
738-
739-
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
740-
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
741-
}
742-
743-
predicate isAdditionalFlowStep(
744-
Node node1, FlowState state1, Node node2, FlowState state2, string model
745-
) {
746-
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
747-
}
748-
}
749-
750-
private module Stage1 = ImplStage1<C>;
751-
752-
import Stage1::PartialFlow
753-
754-
private module Flow = Impl<C, Stage1::Stage1WithState>;
755-
756-
import Flow
757-
}
758706

759707
signature class PathNodeSig {
760708
/** Gets a textual representation of this element. */
@@ -1153,3 +1101,132 @@ module DataFlowMake<LocationSig Location, InputSig<Location> Lang> {
11531101
import PathGraph
11541102
}
11551103
}
1104+
1105+
private module DataFlowMakeNonOverlayInformed<LocationSig Location, InputSig<Location> Lang> {
1106+
import DataFlowMakeCore<Location, Lang>
1107+
private import Lang
1108+
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
1109+
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
1110+
/**
1111+
* Constructs a global data flow computation.
1112+
*/
1113+
module Global<ConfigSig Config> implements GlobalFlowSig {
1114+
private module C implements FullStateConfigSig {
1115+
import DefaultState<Config>
1116+
import Config
1117+
1118+
predicate accessPathLimit = Config::accessPathLimit/0;
1119+
1120+
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
1121+
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
1122+
}
1123+
predicate observeOverlayInformedIncrementalMode() { none() }
1124+
}
1125+
1126+
private module Stage1 = ImplStage1<C>;
1127+
1128+
import Stage1::PartialFlow
1129+
1130+
private module Flow = Impl<C, Stage1::Stage1NoState>;
1131+
1132+
import Flow
1133+
}
1134+
1135+
/**
1136+
* Constructs a global data flow computation using flow state.
1137+
*/
1138+
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
1139+
private module C implements FullStateConfigSig {
1140+
import Config
1141+
1142+
predicate accessPathLimit = Config::accessPathLimit/0;
1143+
1144+
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
1145+
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
1146+
}
1147+
1148+
predicate isAdditionalFlowStep(
1149+
Node node1, FlowState state1, Node node2, FlowState state2, string model
1150+
) {
1151+
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
1152+
}
1153+
1154+
predicate observeOverlayInformedIncrementalMode() { none() }
1155+
}
1156+
1157+
private module Stage1 = ImplStage1<C>;
1158+
1159+
import Stage1::PartialFlow
1160+
1161+
private module Flow = Impl<C, Stage1::Stage1WithState>;
1162+
1163+
import Flow
1164+
}
1165+
1166+
}
1167+
1168+
private module DataFlowMakeOverlayInformed<LocationSig Location, InputSig<Location> Lang> {
1169+
import DataFlowMakeCore<Location, Lang>
1170+
private import Lang
1171+
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
1172+
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
1173+
1174+
1175+
1176+
import DataFlowMakeCore<Location, Lang>
1177+
private import Lang
1178+
private import internal.DataFlowImpl::MakeImpl<Location, Lang>
1179+
private import internal.DataFlowImplStage1::MakeImplStage1<Location, Lang>
1180+
/**
1181+
* Constructs a global data flow computation.
1182+
*/
1183+
module Global<ConfigSig Config> implements GlobalFlowSig {
1184+
private module C implements FullStateConfigSig {
1185+
import DefaultState<Config>
1186+
import Config
1187+
1188+
predicate accessPathLimit = Config::accessPathLimit/0;
1189+
1190+
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
1191+
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
1192+
}
1193+
}
1194+
1195+
private module Stage1 = ImplStage1<C>;
1196+
1197+
import Stage1::PartialFlow
1198+
1199+
private module Flow = OverlayImpl<C, Stage1::Stage1NoState>;
1200+
1201+
import Flow
1202+
}
1203+
1204+
/**
1205+
* Constructs a global data flow computation using flow state.
1206+
*/
1207+
module GlobalWithState<StateConfigSig Config> implements GlobalFlowSig {
1208+
private module C implements FullStateConfigSig {
1209+
import Config
1210+
1211+
predicate accessPathLimit = Config::accessPathLimit/0;
1212+
1213+
predicate isAdditionalFlowStep(Node node1, Node node2, string model) {
1214+
Config::isAdditionalFlowStep(node1, node2) and model = "Config"
1215+
}
1216+
1217+
predicate isAdditionalFlowStep(
1218+
Node node1, FlowState state1, Node node2, FlowState state2, string model
1219+
) {
1220+
Config::isAdditionalFlowStep(node1, state1, node2, state2) and model = "Config"
1221+
}
1222+
}
1223+
1224+
private module Stage1 = ImplStage1<C>;
1225+
1226+
import Stage1::PartialFlow
1227+
1228+
private module Flow = OverlayImpl<C, Stage1::Stage1WithState>;
1229+
1230+
import Flow
1231+
}
1232+
}

0 commit comments

Comments
 (0)