|
1 |
| -private import RangeAnalysisStage |
2 |
| -private import RangeAnalysisSpecific |
3 |
| -private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta |
4 |
| -private import RangeUtils |
5 |
| -private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound |
6 |
| -private import semmle.code.cpp.ir.IR as IR |
7 |
| - |
8 |
| -private module ConstantBounds implements BoundSig<FloatDelta> { |
9 |
| - 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 { |
30 |
| - string toString() { result = super.toString() } |
31 |
| - |
32 |
| - SemExpr getExpr(float delta) { result = super.getExpr(delta) } |
33 |
| - } |
34 |
| - |
35 |
| - class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } |
36 |
| - |
37 |
| - class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { |
38 |
| - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } |
39 |
| - } |
40 |
| -} |
41 |
| - |
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) } |
78 |
| - |
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 |
| -} |
| 1 | +import RangeAnalysisImpl |
| 2 | +import experimental.semmle.code.cpp.semantic.SemanticBound |
0 commit comments