@@ -17,42 +17,85 @@ import codingstandards.c.Expr
1717import codingstandards.c.SideEffects
1818import codingstandards.c.Ordering
1919
20- predicate isCandidatePair ( Expr parentExpr , Expr e1 , Expr e2 ) {
21- parentExpr .getAChild + ( ) = e1 and
22- parentExpr .getAChild + ( ) = e2
20+ predicate isOrHasSideEffect ( Expr e ) {
21+ e instanceof VariableEffect or
22+ any ( VariableEffect ve ) .getAnAccess ( ) = e
23+ }
24+
25+ predicate originatingInStatement ( Expr e , FullExpr fe ) {
26+ isOrHasSideEffect ( e ) and
27+ (
28+ e .( VariableEffect ) .getAnAccess ( ) = fe .getAChild + ( )
29+ or
30+ e .( VariableAccess ) = fe .getAChild + ( )
31+ )
2332}
2433
2534class ConstituentExprOrdering extends Ordering:: Configuration {
2635 ConstituentExprOrdering ( ) { this = "ConstituentExprOrdering" }
2736
2837 override predicate isCandidate ( Expr e1 , Expr e2 ) {
29- // Two different expressions part of the same full expression.
30- isCandidatePair ( _, e1 , e2 )
38+ exists ( FullExpr fe |
39+ originatingInStatement ( e1 , fe ) and
40+ originatingInStatement ( e2 , fe )
41+ )
3142 }
3243}
3344
45+ pragma [ noinline]
46+ predicate sameFullExpr ( FullExpr fe , Expr e1 , Expr e2 ) {
47+ originatingInStatement ( e1 , fe ) and
48+ originatingInStatement ( e2 , fe )
49+ }
50+
51+ predicate effect ( VariableEffect ve , VariableAccess va , Variable v ) {
52+ ve .getAnAccess ( ) = va and
53+ va .getTarget ( ) = v and
54+ ve .getTarget ( ) = v
55+ }
56+
3457from
3558 ConstituentExprOrdering orderingConfig , FullExpr fullExpr , VariableEffect variableEffect1 ,
36- VariableEffect variableEffect2
59+ VariableEffect variableEffect2 , VariableAccess va1 , VariableAccess va2 , Variable v1 , Variable v2
3760where
3861 not isExcluded ( fullExpr , SideEffects3Package:: unsequencedSideEffectsQuery ( ) ) and
62+ sameFullExpr ( fullExpr , va1 , va2 ) and
63+ effect ( variableEffect1 , va1 , v1 ) and
64+ effect ( variableEffect2 , va2 , v2 ) and
65+ variableEffect1 != variableEffect2 and
3966 // If the effect is local we can directly check if it is unsequenced.
4067 // If the effect is not local (happens in a different function) we use the access as a proxy.
41- orderingConfig .isUnsequenced ( variableEffect1 , variableEffect2 ) and
42- fullExpr .getAChild + ( ) = variableEffect1 and
43- fullExpr .getAChild + ( ) = variableEffect2 and
68+ (
69+ va1 .getEnclosingStmt ( ) = variableEffect1 .getEnclosingStmt ( ) and
70+ va2 .getEnclosingStmt ( ) = variableEffect2 .getEnclosingStmt ( ) and
71+ orderingConfig .isUnsequenced ( variableEffect1 , variableEffect2 )
72+ or
73+ va1 .getEnclosingStmt ( ) = variableEffect1 .getEnclosingStmt ( ) and
74+ not va2 .getEnclosingStmt ( ) = variableEffect2 .getEnclosingStmt ( ) and
75+ exists ( Call call |
76+ call .getAnArgument ( ) = va2 and call .getEnclosingStmt ( ) = va1 .getEnclosingStmt ( )
77+ |
78+ orderingConfig .isUnsequenced ( variableEffect1 , call )
79+ )
80+ or
81+ not va1 .getEnclosingStmt ( ) = variableEffect1 .getEnclosingStmt ( ) and
82+ va2 .getEnclosingStmt ( ) = variableEffect2 .getEnclosingStmt ( ) and
83+ exists ( Call call |
84+ call .getAnArgument ( ) = va1 and call .getEnclosingStmt ( ) = va2 .getEnclosingStmt ( )
85+ |
86+ orderingConfig .isUnsequenced ( call , variableEffect2 )
87+ )
88+ ) and
4489 // Both are evaluated
4590 not exists ( ConditionalExpr ce |
46- ce .getThen ( ) .getAChild * ( ) = variableEffect1 and ce .getElse ( ) .getAChild * ( ) = variableEffect2
91+ ce .getThen ( ) .getAChild * ( ) = va1 and ce .getElse ( ) .getAChild * ( ) = va2
4792 ) and
4893 // Break the symmetry of the ordering relation by requiring that the first expression is located before the second.
4994 // This builds upon the assumption that the expressions are part of the same full expression as specified in the ordering configuration.
5095 exists ( int offset1 , int offset2 |
51- variableEffect1 .getLocation ( ) .charLoc ( _, offset1 , _) and
52- variableEffect2 .getLocation ( ) .charLoc ( _, offset2 , _) and
96+ va1 .getLocation ( ) .charLoc ( _, offset1 , _) and
97+ va2 .getLocation ( ) .charLoc ( _, offset2 , _) and
5398 offset1 < offset2
5499 )
55100select fullExpr , "The expression contains unsequenced $@ to $@ and $@ to $@." , variableEffect1 ,
56- "side effect" , variableEffect1 .getAnAccess ( ) , variableEffect1 .getTarget ( ) .getName ( ) ,
57- variableEffect2 , "side effect" , variableEffect2 .getAnAccess ( ) ,
58- variableEffect2 .getTarget ( ) .getName ( )
101+ "side effect" , va1 , v1 .getName ( ) , variableEffect2 , "side effect" , va2 , v2 .getName ( )
0 commit comments