|
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