@@ -20,60 +20,41 @@ int argumentPosition(FunctionCall fc, Expr exp, int n) {
2020}
2121
2222/** Holds if a nonsensical type conversion situation is found. */
23- predicate conversionDoneLate ( MulExpr mexp , Expr e1 , Expr e2 ) {
24- mexp .getConversion ( ) .hasExplicitConversion ( ) and
25- mexp .getConversion ( ) instanceof ParenthesisExpr and
26- mexp .getConversion ( ) .getConversion ( ) instanceof CStyleCast and
27- mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > mexp .getType ( ) .getSize ( ) and
28- mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > e2 .getType ( ) .getSize ( ) and
29- mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > e1 .getType ( ) .getSize ( ) and
30- exists ( Expr e0 |
31- e0 .( AssignExpr ) .getRValue ( ) = mexp .getParent * ( ) and
32- e0 .( AssignExpr ) .getLValue ( ) .getType ( ) .getSize ( ) =
33- mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
34- or
35- mexp .getEnclosingElement ( ) .( ComparisonOperation ) .hasOperands ( mexp , e0 ) and
36- e0 .getType ( ) .getSize ( ) = mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
37- or
38- e0 .( FunctionCall )
39- .getTarget ( )
40- .getParameter ( argumentPosition ( e0 .( FunctionCall ) , mexp , _) )
41- .getType ( )
42- .getSize ( ) = mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
43- )
44- }
45-
46- /** Holds if the situation of a possible signed overflow used in pointer arithmetic is found. */
47- predicate signSmallerWithEqualSizes ( MulExpr mexp , Expr e1 , Expr e2 ) {
48- mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e1 .getUnderlyingType ( ) .getSize ( ) and
49- (
50- e2 .isConstant ( ) or
51- mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e2 .getUnderlyingType ( ) .getSize ( )
52- ) and
53- mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e1 .getUnderlyingType ( ) .getSize ( ) and
54- exists ( AssignExpr ae |
55- ae .getRValue ( ) = mexp .getParent * ( ) and
56- ae .getRValue ( ) .getUnderlyingType ( ) .( IntegralType ) .isUnsigned ( ) and
57- ae .getLValue ( ) .getUnderlyingType ( ) .( IntegralType ) .isSigned ( ) and
23+ predicate conversionDoneLate ( MulExpr mexp ) {
24+ exists ( Expr e1 , Expr e2 |
25+ mexp .hasOperands ( e1 , e2 ) and
26+ not e1 .isConstant ( ) and
27+ not e1 .hasConversion ( ) and
28+ not e1 .hasConversion ( ) and
5829 (
59- not exists ( DivExpr de | mexp .getParent * ( ) = de )
60- or
61- exists ( DivExpr de , Expr ec |
62- e2 .isConstant ( ) and
63- de .hasOperands ( mexp .getParent * ( ) , ec ) and
64- ec .isConstant ( ) and
65- e2 .getValue ( ) .toInt ( ) > ec .getValue ( ) .toInt ( )
66- )
30+ e2 .isConstant ( ) or
31+ not e2 .hasConversion ( )
6732 ) and
68- exists ( PointerAddExpr pa |
69- ae .getASuccessor + ( ) = pa and
70- pa .getAnOperand ( ) .( VariableAccess ) .getTarget ( ) = ae .getLValue ( ) .( VariableAccess ) .getTarget ( )
33+ mexp .getConversion ( ) .hasExplicitConversion ( ) and
34+ mexp .getConversion ( ) instanceof ParenthesisExpr and
35+ mexp .getConversion ( ) .getConversion ( ) instanceof CStyleCast and
36+ mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > mexp .getType ( ) .getSize ( ) and
37+ mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > e2 .getType ( ) .getSize ( ) and
38+ mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( ) > e1 .getType ( ) .getSize ( ) and
39+ exists ( Expr e0 |
40+ e0 .( AssignExpr ) .getRValue ( ) = mexp .getParent * ( ) and
41+ e0 .( AssignExpr ) .getLValue ( ) .getType ( ) .getSize ( ) =
42+ mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
43+ or
44+ mexp .getEnclosingElement ( ) .( ComparisonOperation ) .hasOperands ( mexp , e0 ) and
45+ e0 .getType ( ) .getSize ( ) = mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
46+ or
47+ e0 .( FunctionCall )
48+ .getTarget ( )
49+ .getParameter ( argumentPosition ( e0 .( FunctionCall ) , mexp , _) )
50+ .getType ( )
51+ .getSize ( ) = mexp .getConversion ( ) .getConversion ( ) .getType ( ) .getSize ( )
7152 )
7253 )
7354}
7455
75- from MulExpr mexp , string msg
76- where
56+ /** Holds if the situation of a possible signed overflow used in pointer arithmetic is found. */
57+ predicate signSmallerWithEqualSizes ( MulExpr mexp ) {
7758 exists ( Expr e1 , Expr e2 |
7859 mexp .hasOperands ( e1 , e2 ) and
7960 not e1 .isConstant ( ) and
@@ -83,12 +64,39 @@ where
8364 e2 .isConstant ( ) or
8465 not e2 .hasConversion ( )
8566 ) and
67+ mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e1 .getUnderlyingType ( ) .getSize ( ) and
8668 (
87- conversionDoneLate ( mexp , e1 , e2 ) and
88- msg = "This transformation is applied after multiplication."
89- or
90- signSmallerWithEqualSizes ( mexp , e1 , e2 ) and
91- msg = "Possible signed overflow followed by offset of the pointer out of bounds."
69+ e2 .isConstant ( ) or
70+ mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e2 .getUnderlyingType ( ) .getSize ( )
71+ ) and
72+ mexp .getConversion + ( ) .getUnderlyingType ( ) .getSize ( ) = e1 .getUnderlyingType ( ) .getSize ( ) and
73+ exists ( AssignExpr ae |
74+ ae .getRValue ( ) = mexp .getParent * ( ) and
75+ ae .getRValue ( ) .getUnderlyingType ( ) .( IntegralType ) .isUnsigned ( ) and
76+ ae .getLValue ( ) .getUnderlyingType ( ) .( IntegralType ) .isSigned ( ) and
77+ (
78+ not exists ( DivExpr de | mexp .getParent * ( ) = de )
79+ or
80+ exists ( DivExpr de , Expr ec |
81+ e2 .isConstant ( ) and
82+ de .hasOperands ( mexp .getParent * ( ) , ec ) and
83+ ec .isConstant ( ) and
84+ e2 .getValue ( ) .toInt ( ) > ec .getValue ( ) .toInt ( )
85+ )
86+ ) and
87+ exists ( PointerAddExpr pa |
88+ ae .getASuccessor + ( ) = pa and
89+ pa .getAnOperand ( ) .( VariableAccess ) .getTarget ( ) = ae .getLValue ( ) .( VariableAccess ) .getTarget ( )
90+ )
9291 )
9392 )
93+ }
94+
95+ from MulExpr mexp , string msg
96+ where
97+ conversionDoneLate ( mexp ) and
98+ msg = "This transformation is applied after multiplication."
99+ or
100+ signSmallerWithEqualSizes ( mexp ) and
101+ msg = "Possible signed overflow followed by offset of the pointer out of bounds."
94102select mexp , msg
0 commit comments