Skip to content

Commit 50fac30

Browse files
committed
C++: split RA into constant and relative phases
1 parent ce937e7 commit 50fac30

File tree

1 file changed

+80
-4
lines changed

1 file changed

+80
-4
lines changed

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

Lines changed: 80 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,30 @@ private import RangeAnalysisSpecific
33
private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
44
private import RangeUtils
55
private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
6+
private import semmle.code.cpp.ir.IR as IR
67

7-
module Bounds implements BoundSig<FloatDelta> {
8+
private module ConstantBounds implements BoundSig<FloatDelta> {
89
class SemBound instanceof SemanticBound::SemBound {
10+
SemBound() {
11+
this instanceof SemanticBound::SemZeroBound
12+
or
13+
this.(SemanticBound::SemSsaBound).getExpr(0) instanceof IR::PhiInstruction
14+
}
15+
16+
string toString() { result = super.toString() }
17+
18+
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
19+
}
20+
21+
class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
22+
23+
class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
24+
SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
25+
}
26+
}
27+
28+
private module RelativeBounds implements BoundSig<FloatDelta> {
29+
class SemBound instanceof SemanticBound::SemSsaBound {
930
string toString() { result = super.toString() }
1031

1132
SemExpr getExpr(float delta) { result = super.getExpr(delta) }
@@ -18,7 +39,62 @@ module Bounds implements BoundSig<FloatDelta> {
1839
}
1940
}
2041

21-
private module CppRangeAnalysis =
22-
RangeStage<FloatDelta, Bounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
42+
private module ConstantStage =
43+
RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
44+
45+
private module RelativeStage =
46+
RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
47+
48+
private newtype TSemReason =
49+
TSemNoReason() or
50+
TSemCondReason(SemGuard guard) {
51+
guard = any(ConstantStage::SemCondReason reason).getCond()
52+
or
53+
guard = any(RelativeStage::SemCondReason reason).getCond()
54+
}
55+
56+
/**
57+
* A reason for an inferred bound. This can either be `CondReason` if the bound
58+
* is due to a specific condition, or `NoReason` if the bound is inferred
59+
* without going through a bounding condition.
60+
*/
61+
abstract class SemReason extends TSemReason {
62+
/** Gets a textual representation of this reason. */
63+
abstract string toString();
64+
}
65+
66+
/**
67+
* A reason for an inferred bound that indicates that the bound is inferred
68+
* without going through a bounding condition.
69+
*/
70+
class SemNoReason extends SemReason, TSemNoReason {
71+
override string toString() { result = "NoReason" }
72+
}
73+
74+
/** A reason for an inferred bound pointing to a condition. */
75+
class SemCondReason extends SemReason, TSemCondReason {
76+
/** Gets the condition that is the reason for the bound. */
77+
SemGuard getCond() { this = TSemCondReason(result) }
2378

24-
import CppRangeAnalysis
79+
override string toString() { result = getCond().toString() }
80+
}
81+
82+
private ConstantStage::SemReason constantReason(SemReason reason) {
83+
result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
84+
or
85+
result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
86+
}
87+
88+
private RelativeStage::SemReason relativeReason(SemReason reason) {
89+
result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
90+
or
91+
result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
92+
}
93+
94+
predicate semBounded(
95+
SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
96+
) {
97+
ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
98+
or
99+
RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
100+
}

0 commit comments

Comments
 (0)