Rangeanalysis: Preparatory refactor for bounds sharing.

This commit is contained in:
Anders Schack-Mulligen
2023-11-29 09:24:42 +01:00
parent d8f53e5524
commit 6b178fb64a
4 changed files with 25 additions and 4 deletions

View File

@@ -25,4 +25,8 @@ module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
* Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
predicate includeConstantBounds() { any() }
predicate includeRelativeBounds() { none() }
} }

View File

@@ -173,11 +173,11 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
} }
module ConstantStage = module ConstantStage =
RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant, RangeStage<SemLocation, Sem, FloatDelta, AllBounds, FloatOverflow, CppLangImplConstant,
SignAnalysis, ModulusAnalysisInstantiated>; SignAnalysis, ModulusAnalysisInstantiated>;
module RelativeStage = module RelativeStage =
RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative, RangeStage<SemLocation, Sem, FloatDelta, AllBounds, FloatOverflow, CppLangImplRelative,
SignAnalysis, ModulusAnalysisInstantiated>; SignAnalysis, ModulusAnalysisInstantiated>;
private newtype TSemReason = private newtype TSemReason =

View File

@@ -57,4 +57,8 @@ module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
* Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`).
*/ */
predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() }
predicate includeConstantBounds() { none() }
predicate includeRelativeBounds() { any() }
} }

View File

@@ -289,6 +289,10 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
predicate ignoreExprBound(Sem::Expr e); predicate ignoreExprBound(Sem::Expr e);
default predicate javaCompatibility() { none() } default predicate javaCompatibility() { none() }
default predicate includeConstantBounds() { any() }
default predicate includeRelativeBounds() { any() }
} }
signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> { signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
@@ -983,6 +987,13 @@ module RangeStage<
) )
} }
private predicate includeBound(SemBound b) {
// always include phi bounds
b.(SemSsaBound).getVariable() instanceof Sem::SsaPhiNode
or
if b instanceof SemZeroBound then includeConstantBounds() else includeRelativeBounds()
}
/** /**
* Holds if `e` has an upper (for `upper = true`) or lower * Holds if `e` has an upper (for `upper = true`) or lower
* (for `upper = false`) bound of `b`. * (for `upper = false`) bound of `b`.
@@ -1122,13 +1133,15 @@ module RangeStage<
(upper = true or upper = false) and (upper = true or upper = false) and
fromBackEdge = false and fromBackEdge = false and
origdelta = delta and origdelta = delta and
reason = TSemNoReason() reason = TSemNoReason() and
includeBound(b)
or or
baseBound(e, delta, upper) and baseBound(e, delta, upper) and
b instanceof SemZeroBound and b instanceof SemZeroBound and
fromBackEdge = false and fromBackEdge = false and
origdelta = delta and origdelta = delta and
reason = TSemNoReason() reason = TSemNoReason() and
includeBound(b)
or or
exists(Sem::SsaVariable v, SsaReadPositionBlock bb | exists(Sem::SsaVariable v, SsaReadPositionBlock bb |
boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and