1414import cpp
1515import LeapYear
1616
17- from FunctionCall fcall , TimeConversionFunction trf , Variable var
18- where
17+ signature module InputSig {
18+ predicate isSource ( ControlFlowNode n ) ;
19+
20+ predicate isSink ( ControlFlowNode n ) ;
21+ }
22+
23+ module ControlFlowReachability< InputSig Input> {
24+ pragma [ nomagic]
25+ private predicate fwd ( ControlFlowNode n ) {
26+ Input:: isSource ( n )
27+ or
28+ exists ( ControlFlowNode n0 |
29+ fwd ( n0 ) and
30+ n0 .getASuccessor ( ) = n
31+ )
32+ }
33+
34+ pragma [ nomagic]
35+ private predicate rev ( ControlFlowNode n ) {
36+ fwd ( n ) and
37+ (
38+ Input:: isSink ( n )
39+ or
40+ exists ( ControlFlowNode n1 |
41+ rev ( n1 ) and
42+ n .getASuccessor ( ) = n1
43+ )
44+ )
45+ }
46+
47+ pragma [ nomagic]
48+ private predicate prunedSuccessor ( ControlFlowNode n1 , ControlFlowNode n2 ) {
49+ rev ( n1 ) and
50+ rev ( n2 ) and
51+ n1 .getASuccessor ( ) = n2
52+ }
53+
54+ pragma [ nomagic]
55+ predicate isSource ( ControlFlowNode n ) {
56+ Input:: isSource ( n ) and
57+ rev ( n )
58+ }
59+
60+ pragma [ nomagic]
61+ predicate isSink ( ControlFlowNode n ) {
62+ Input:: isSink ( n ) and
63+ rev ( n )
64+ }
65+
66+ pragma [ nomagic]
67+ private predicate successorPlus ( ControlFlowNode n1 , ControlFlowNode n2 ) =
68+ doublyBoundedFastTC( prunedSuccessor / 2 , isSource / 1 , isSink / 1 ) ( n1 , n2 )
69+
70+ predicate flowsTo ( ControlFlowNode n1 , ControlFlowNode n2 ) {
71+ successorPlus ( n1 , n2 )
72+ or
73+ n1 = n2 and
74+ isSource ( n1 ) and
75+ isSink ( n2 )
76+ }
77+ }
78+
79+ predicate isUnpackedTimeTypeVar ( Variable var , FunctionCall fcall , TimeConversionFunction trf ) {
1980 fcall = trf .getACallToThisFunction ( ) and
2081 fcall instanceof ExprInVoidContext and
2182 var .getUnderlyingType ( ) instanceof UnpackedTimeType and
@@ -29,34 +90,93 @@ where
2990 fcall .getAnArgument ( ) = va and
3091 var .getAnAccess ( ) = va
3192 )
32- ) and
33- exists ( DateStructModifiedFieldAccess dsmfa , VariableAccess modifiedVarAccess |
93+ )
94+ }
95+
96+ predicate isModifiedFieldAccessToTimeConversionSource (
97+ ControlFlowNode modifiedVarAccess , Variable var
98+ ) {
99+ exists ( DateStructModifiedFieldAccess dsmfa |
100+ isUnpackedTimeTypeVar ( var , _, _) and
34101 modifiedVarAccess = var .getAnAccess ( ) and
35- modifiedVarAccess = dsmfa .getQualifier ( ) and
36- modifiedVarAccess = fcall .getAPredecessor * ( )
102+ modifiedVarAccess = dsmfa .getQualifier ( )
103+ )
104+ }
105+
106+ module ModifiedFieldAccessToTimeConversionConfig implements InputSig {
107+ predicate isSource ( ControlFlowNode modifiedVarAccess ) {
108+ isModifiedFieldAccessToTimeConversionSource ( modifiedVarAccess , _)
109+ }
110+
111+ predicate isSink ( ControlFlowNode fcall ) { isUnpackedTimeTypeVar ( _, fcall , _) }
112+ }
113+
114+ module ModifiedFieldAccessToTimeConversion =
115+ ControlFlowReachability< ModifiedFieldAccessToTimeConversionConfig > ;
116+
117+ module SafeTimeGatheringFunctionCallToTimeConversionFunctionCallConfig implements InputSig {
118+ predicate isSource ( ControlFlowNode n ) {
119+ n = any ( SafeTimeGatheringFunction stgf ) .getACallToThisFunction ( )
120+ }
121+
122+ predicate isSink ( ControlFlowNode fcall ) { ModifiedFieldAccessToTimeConversion:: isSink ( fcall ) }
123+ }
124+
125+ module SafeTimeGatheringFunctionCallToTimeConversionFunctionCall =
126+ ControlFlowReachability< SafeTimeGatheringFunctionCallToTimeConversionFunctionCallConfig > ;
127+
128+ module SafeTimeGatheringFunctionCallToModifiedFieldAccessConfig implements InputSig {
129+ predicate isSource ( ControlFlowNode n ) {
130+ n = any ( SafeTimeGatheringFunction stgf ) .getACallToThisFunction ( ) and
131+ SafeTimeGatheringFunctionCallToTimeConversionFunctionCall:: isSource ( n )
132+ }
133+
134+ predicate isSink ( ControlFlowNode modifiedVarAccess ) {
135+ ModifiedFieldAccessToTimeConversion:: flowsTo ( modifiedVarAccess , _)
136+ }
137+ }
138+
139+ module SafeTimeGatheringFunctionCallToModifiedFieldAccess =
140+ ControlFlowReachability< SafeTimeGatheringFunctionCallToModifiedFieldAccessConfig > ;
141+
142+ module ModifiedMonthFieldAccessToTimeConversionConfig implements InputSig {
143+ predicate isSource ( ControlFlowNode n ) {
144+ exists ( Variable var , MonthFieldAccess mfa , AssignExpr ae |
145+ n = mfa and
146+ isUnpackedTimeTypeVar ( var , _, _) and
147+ mfa .getQualifier ( ) = var .getAnAccess ( ) and
148+ mfa .isModified ( ) and
149+ ae = mfa .getEnclosingElement ( ) and
150+ ae .getAnOperand ( ) .getValue ( ) .toInt ( ) = 1
151+ )
152+ }
153+
154+ predicate isSink ( ControlFlowNode fcall ) { ModifiedFieldAccessToTimeConversion:: flowsTo ( _, fcall ) }
155+ }
156+
157+ module ModifiedMonthFieldAccessToTimeConversion =
158+ ControlFlowReachability< ModifiedMonthFieldAccessToTimeConversionConfig > ;
159+
160+ from FunctionCall fcall , TimeConversionFunction trf , Variable var
161+ where
162+ isUnpackedTimeTypeVar ( var , fcall , trf ) and
163+ exists ( VariableAccess modifiedVarAccess |
164+ isModifiedFieldAccessToTimeConversionSource ( modifiedVarAccess , var ) and
165+ ModifiedFieldAccessToTimeConversion:: flowsTo ( modifiedVarAccess , fcall )
37166 ) and
38167 // Remove false positives
39168 not (
40169 // Remove any instance where the predecessor is a SafeTimeGatheringFunction and no change to the data happened in between
41170 exists ( FunctionCall pred |
42- pred = fcall .getAPredecessor * ( ) and
43- exists ( SafeTimeGatheringFunction stgf | pred = stgf .getACallToThisFunction ( ) ) and
44- not exists ( DateStructModifiedFieldAccess dsmfa , VariableAccess modifiedVarAccess |
45- modifiedVarAccess = var .getAnAccess ( ) and
46- modifiedVarAccess = dsmfa .getQualifier ( ) and
47- modifiedVarAccess = fcall .getAPredecessor * ( ) and
48- modifiedVarAccess = pred .getASuccessor * ( )
171+ SafeTimeGatheringFunctionCallToTimeConversionFunctionCall:: flowsTo ( pred , fcall ) and
172+ not exists ( VariableAccess modifiedVarAccess |
173+ ModifiedFieldAccessToTimeConversion:: flowsTo ( modifiedVarAccess , fcall ) and
174+ SafeTimeGatheringFunctionCallToModifiedFieldAccess:: flowsTo ( pred , modifiedVarAccess )
49175 )
50176 )
51177 or
52178 // Remove any instance where the year is changed, but the month is set to 1 (year wrapping)
53- exists ( MonthFieldAccess mfa , AssignExpr ae |
54- mfa .getQualifier ( ) = var .getAnAccess ( ) and
55- mfa .isModified ( ) and
56- mfa = fcall .getAPredecessor * ( ) and
57- ae = mfa .getEnclosingElement ( ) and
58- ae .getAnOperand ( ) .getValue ( ) .toInt ( ) = 1
59- )
179+ ModifiedMonthFieldAccessToTimeConversion:: isSink ( fcall )
60180 )
61181select fcall ,
62182 "$@: Return value of $@ function should be verified to check for any error because variable $@ is not guaranteed to be safe." ,
0 commit comments