@@ -4108,6 +4108,86 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4108
4108
)
4109
4109
}
4110
4110
4111
+ private module Stage6Param implements MkStage< Stage5 > :: StageParam {
4112
+ private module PrevStage = Stage5;
4113
+
4114
+ class Typ = DataFlowType ;
4115
+
4116
+ class Ap = AccessPath ;
4117
+
4118
+ class ApNil = AccessPathNil ;
4119
+
4120
+ pragma [ nomagic]
4121
+ PrevStage:: Ap getApprox ( Ap ap ) { result = ap .getApprox ( ) }
4122
+
4123
+ Typ getTyp ( DataFlowType t ) { result = t }
4124
+
4125
+ bindingset [ c, t, tail]
4126
+ Ap apCons ( Content c , Typ t , Ap tail ) { result .isCons ( c , t , tail ) }
4127
+
4128
+ class ApHeadContent = Content ;
4129
+
4130
+ pragma [ noinline]
4131
+ ApHeadContent getHeadContent ( Ap ap ) { result = ap .getHead ( ) }
4132
+
4133
+ ApHeadContent projectToHeadContent ( Content c ) { result = c }
4134
+
4135
+ private module ApOption = Option< AccessPath > ;
4136
+
4137
+ class ApOption = ApOption:: Option ;
4138
+
4139
+ ApOption apNone ( ) { result .isNone ( ) }
4140
+
4141
+ ApOption apSome ( Ap ap ) { result = ApOption:: some ( ap ) }
4142
+
4143
+ private module CallContextSensitivityInput implements CallContextSensitivityInputSig {
4144
+ predicate relevantCallEdgeIn = PrevStage:: relevantCallEdgeIn / 2 ;
4145
+
4146
+ predicate relevantCallEdgeOut = PrevStage:: relevantCallEdgeOut / 2 ;
4147
+
4148
+ predicate reducedViableImplInCallContextCand =
4149
+ Stage5Param:: reducedViableImplInCallContext / 3 ;
4150
+
4151
+ predicate reducedViableImplInReturnCand = Stage5Param:: reducedViableImplInReturn / 2 ;
4152
+ }
4153
+
4154
+ import CallContextSensitivity< CallContextSensitivityInput >
4155
+ import LocalCallContext
4156
+
4157
+ predicate localStep (
4158
+ NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
4159
+ Typ t , LocalCc lcc , string label
4160
+ ) {
4161
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
4162
+ PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
4163
+ PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
4164
+ }
4165
+
4166
+ bindingset [ node, state, t0, ap]
4167
+ predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
4168
+ strengthenType ( node , t0 , t ) and
4169
+ exists ( state ) and
4170
+ exists ( ap )
4171
+ }
4172
+
4173
+ pragma [ nomagic]
4174
+ private predicate clearExceptStore ( NodeEx node , Ap ap ) {
4175
+ Stage4Param:: clearContent ( node , ap .getHead ( ) , true )
4176
+ }
4177
+
4178
+ bindingset [ node, ap, isStoreStep]
4179
+ predicate stepFilter ( NodeEx node , Ap ap , boolean isStoreStep ) {
4180
+ if clearExceptStore ( node , ap ) then isStoreStep = true else any ( )
4181
+ }
4182
+
4183
+ bindingset [ typ, contentType]
4184
+ predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
4185
+ compatibleTypesFilter ( typ , contentType )
4186
+ }
4187
+ }
4188
+
4189
+ module Stage6 = MkStage< Stage5 > :: Stage< Stage6Param > ;
4190
+
4111
4191
private module PrunedCallContextSensitivityStage5 {
4112
4192
private module CallContextSensitivityInput implements CallContextSensitivityInputSig {
4113
4193
predicate relevantCallEdgeIn = Stage5:: relevantCallEdgeIn / 2 ;
0 commit comments