1212import cpp
1313import LeapYear
1414
15- /**
16- * Holds if there is no known leap-year verification for the given `YearWriteOp`.
17- * Binds the `var` argument to the qualifier of the `ywo` argument.
18- */
19- bindingset [ ywo]
20- predicate isYearModifedWithoutExplicitLeapYearCheck ( Variable var , YearWriteOp ywo ) {
21- exists ( VariableAccess va , YearFieldAccess yfa |
22- yfa = ywo .getYearAccess ( ) and
23- yfa .getQualifier ( ) = va and
24- var .getAnAccess ( ) = va and
25- // Avoid false positives
26- not (
27- // If there is a local check for leap year after the modification
28- exists ( LeapYearFieldAccess yfacheck |
29- yfacheck .getQualifier ( ) = var .getAnAccess ( ) and
30- yfacheck .isUsedInCorrectLeapYearCheck ( ) and
31- yfacheck .getBasicBlock ( ) = yfa .getBasicBlock ( ) .getASuccessor * ( )
32- )
33- or
34- // If there is a data flow from the variable that was modified to a function that seems to check for leap year
35- exists ( VariableAccess source , ChecksForLeapYearFunctionCall fc |
36- source = var .getAnAccess ( ) and
37- LeapYearCheckFlow:: flow ( DataFlow:: exprNode ( source ) , DataFlow:: exprNode ( fc .getAnArgument ( ) ) )
38- )
39- or
40- // If there is a data flow from the field that was modified to a function that seems to check for leap year
41- exists ( VariableAccess vacheck , YearFieldAccess yfacheck , ChecksForLeapYearFunctionCall fc |
42- vacheck = var .getAnAccess ( ) and
43- yfacheck .getQualifier ( ) = vacheck and
44- LeapYearCheckFlow:: flow ( DataFlow:: exprNode ( yfacheck ) , DataFlow:: exprNode ( fc .getAnArgument ( ) ) )
45- )
46- or
47- // If there is a successor or predecessor that sets the month or day to a fixed value
48- exists ( FieldAccess mfa , AssignExpr ae , int val |
49- mfa instanceof MonthFieldAccess or mfa instanceof DayFieldAccess
50- |
51- mfa .getQualifier ( ) = var .getAnAccess ( ) and
52- mfa .isModified ( ) and
53- (
54- mfa .getBasicBlock ( ) = yfa .getBasicBlock ( ) .getASuccessor * ( ) or
55- yfa .getBasicBlock ( ) = mfa .getBasicBlock ( ) .getASuccessor + ( )
56- ) and
57- ae = mfa .getEnclosingElement ( ) and
58- ae .getAnOperand ( ) .getValue ( ) .toInt ( ) = val
59- )
60- )
61- )
62- }
63-
6415/**
6516 * The set of all write operations to the Year field of a date struct.
6617 */
@@ -70,6 +21,61 @@ abstract class YearWriteOp extends Operation {
7021
7122 /** Get the expression which represents the new value. */
7223 abstract Expr getMutationExpr ( ) ;
24+
25+ /**
26+ * Checks if this Operation is a simple normalization, converting between formats.
27+ */
28+ predicate isNormalizationOperation ( ) {
29+ isNormalizationOperation ( this .getMutationExpr ( ) )
30+ }
31+
32+ /**
33+ * Holds if there is no known leap-year verification for the `YearWriteOp`.
34+ * Binds the `var` argument to the qualifier of the `ywo` argument.
35+ */
36+ predicate isYearModifedWithoutExplicitLeapYearCheck ( Variable var ) {
37+ exists ( VariableAccess va , YearFieldAccess yfa |
38+ yfa = this .getYearAccess ( ) and
39+ yfa .getQualifier ( ) = va and
40+ var .getAnAccess ( ) = va and
41+ // Avoid false positives
42+ not (
43+ // If there is a local check for leap year after the modification
44+ exists ( LeapYearFieldAccess yfacheck |
45+ yfacheck .getQualifier ( ) = var .getAnAccess ( ) and
46+ yfacheck .isUsedInCorrectLeapYearCheck ( ) and
47+ yfacheck .getBasicBlock ( ) = yfa .getBasicBlock ( ) .getASuccessor * ( )
48+ )
49+ or
50+ // If there is a data flow from the variable that was modified to a function that seems to check for leap year
51+ exists ( VariableAccess source , ChecksForLeapYearFunctionCall fc |
52+ source = var .getAnAccess ( ) and
53+ LeapYearCheckFlow:: flow ( DataFlow:: exprNode ( source ) , DataFlow:: exprNode ( fc .getAnArgument ( ) ) )
54+ )
55+ or
56+ // If there is a data flow from the field that was modified to a function that seems to check for leap year
57+ exists ( VariableAccess vacheck , YearFieldAccess yfacheck , ChecksForLeapYearFunctionCall fc |
58+ vacheck = var .getAnAccess ( ) and
59+ yfacheck .getQualifier ( ) = vacheck and
60+ LeapYearCheckFlow:: flow ( DataFlow:: exprNode ( yfacheck ) , DataFlow:: exprNode ( fc .getAnArgument ( ) ) )
61+ )
62+ or
63+ // If there is a successor or predecessor that sets the month or day to a fixed value
64+ exists ( FieldAccess mfa , AssignExpr ae , int val |
65+ mfa instanceof MonthFieldAccess or mfa instanceof DayFieldAccess
66+ |
67+ mfa .getQualifier ( ) = var .getAnAccess ( ) and
68+ mfa .isModified ( ) and
69+ (
70+ mfa .getBasicBlock ( ) = yfa .getBasicBlock ( ) .getASuccessor * ( ) or
71+ yfa .getBasicBlock ( ) = mfa .getBasicBlock ( ) .getASuccessor + ( )
72+ ) and
73+ ae = mfa .getEnclosingElement ( ) and
74+ ae .getAnOperand ( ) .getValue ( ) .toInt ( ) = val
75+ )
76+ )
77+ )
78+ }
7379}
7480
7581/**
@@ -125,14 +131,37 @@ module OperationToYearAssignmentConfig implements DataFlow::ConfigSig {
125131
126132module OperationToYearAssignmentFlow = DataFlow:: Global< OperationToYearAssignmentConfig > ;
127133
128- from Variable var , YearWriteOp ywo , Expr mutationExpr
134+ /**
135+ * A Call to some known Time conversion function, which maps between time structs or scalars.
136+ */
137+ class TimeConversionCall extends Call {
138+ TimeConversionCall ( ) {
139+ this = any ( TimeConversionFunction f ) .getACallToThisFunction ( )
140+ }
141+
142+ bindingset [ var]
143+ predicate converts ( Variable var ) {
144+ this .getAnArgument ( ) .getAChild * ( ) = var .getAnAccess ( )
145+ }
146+ }
147+
148+ /**
149+ * A YearWriteOp that is non-mutating (AddressOfExpr *could* mutate but doesnt)
150+ */
151+ class NonMutatingYearWriteOp extends Operation instanceof YearWriteOp {
152+ NonMutatingYearWriteOp ( ) {
153+ this instanceof AddressOfExpr
154+ }
155+ }
156+
157+ from Variable var , YearWriteOp ywo
129158where
130- mutationExpr = ywo .getMutationExpr ( ) and
131- isYearModifedWithoutExplicitLeapYearCheck ( var , ywo ) and
132- not isNormalizationOperation ( mutationExpr ) and
133- not ywo instanceof AddressOfExpr and
134- not exists ( Call c , TimeConversionFunction f | f . getACallToThisFunction ( ) = c |
135- c .getAnArgument ( ) . getAChild * ( ) = var . getAnAccess ( ) and
159+ not ywo .isNormalizationOperation ( ) and
160+ not ywo instanceof NonMutatingYearWriteOp and
161+ ywo . isYearModifedWithoutExplicitLeapYearCheck ( var ) and
162+ // If there is a Time conversion after, which utilizes the variable - could lead to false negatives maybe?
163+ not exists ( TimeConversionCall c |
164+ c .converts ( var ) and
136165 ywo .getASuccessor * ( ) = c
137166 )
138167select ywo ,
0 commit comments