@@ -30,8 +30,7 @@ predicate isDefOf(ControlFlowNode node, Variable var) {
3030 */
3131pragma [ nomagic]
3232predicate isDecInComparison (
33- PostfixDecrExpr dec , VariableAccess varAcc ,
34- ComparisonOperation cmp , Variable var
33+ PostfixDecrExpr dec , VariableAccess varAcc , ComparisonOperation cmp , Variable var
3534) {
3635 varAcc = var .getAnAccess ( ) and
3736 dec .getOperand ( ) = varAcc .getExplicitlyConverted ( ) and
@@ -62,23 +61,17 @@ class DecOverflowReach extends StackVariableReachability {
6261 isDecInComparison ( _, _, node , v )
6362 }
6463
65- override predicate isSink ( ControlFlowNode node , StackVariable v ) {
66- isReadOf ( node , v )
67- }
64+ override predicate isSink ( ControlFlowNode node , StackVariable v ) { isReadOf ( node , v ) }
6865
69- override predicate isBarrier ( ControlFlowNode node , StackVariable v ) {
70- isDefOf ( node , v )
71- }
66+ override predicate isBarrier ( ControlFlowNode node , StackVariable v ) { isDefOf ( node , v ) }
7267}
7368
7469/**
7570 * BB-level reachability for non-stack variables (globals, static locals).
7671 * Holds if `sink` is reachable from the entry of `bb` without crossing
7772 * a definition of `var`.
7873 */
79- private predicate nonStackBBEntryReaches (
80- BasicBlock bb , Variable var , ControlFlowNode sink
81- ) {
74+ private predicate nonStackBBEntryReaches ( BasicBlock bb , Variable var , ControlFlowNode sink ) {
8275 exists ( int n |
8376 sink = bb .getNode ( n ) and
8477 isReadOf ( sink , var ) and
@@ -94,9 +87,7 @@ private predicate nonStackBBEntryReaches(
9487 * without crossing a definition of `var`.
9588 */
9689pragma [ nomagic]
97- predicate nonStackReaches (
98- ComparisonOperation source , Variable var , ControlFlowNode sink
99- ) {
90+ predicate nonStackReaches ( ComparisonOperation source , Variable var , ControlFlowNode sink ) {
10091 not var instanceof StackVariable and
10192 exists ( BasicBlock bb , int i |
10293 bb .getNode ( i ) = source and
@@ -115,8 +106,8 @@ predicate nonStackReaches(
115106}
116107
117108from
118- Variable var , VariableAccess varAcc , PostfixDecrExpr dec ,
119- VariableAccess varAccAfterOverflow , ComparisonOperation cmp
109+ Variable var , VariableAccess varAcc , PostfixDecrExpr dec , VariableAccess varAccAfterOverflow ,
110+ ComparisonOperation cmp
120111where
121112 isDecInComparison ( dec , varAcc , cmp , var ) and
122113 isReadOf ( varAccAfterOverflow , var ) and
@@ -132,14 +123,11 @@ where
132123 // var-- > 0 (0 < var--) then only accesses in false branch matter
133124 (
134125 if
135- (
136- cmp instanceof GTExpr and cmp .getRightOperand ( ) instanceof Zero
137- or
138- cmp instanceof LTExpr and cmp .getLeftOperand ( ) instanceof Zero
139- )
126+ cmp instanceof GTExpr and cmp .getRightOperand ( ) instanceof Zero
127+ or
128+ cmp instanceof LTExpr and cmp .getLeftOperand ( ) instanceof Zero
140129 then cmp .getAFalseSuccessor ( ) .getASuccessor * ( ) = varAccAfterOverflow
141130 else any ( )
142131 )
143-
144132select dec , "Unsigned decrementation in comparison ($@) - $@" , cmp , cmp .toString ( ) ,
145133 varAccAfterOverflow , varAccAfterOverflow .toString ( )
0 commit comments