Skip to content

Commit

Permalink
TEMP: Make sure type-based reasons propagate through bounds for add e…
Browse files Browse the repository at this point in the history
…xpressions.
  • Loading branch information
MathiasVP committed Aug 1, 2023
1 parent 854cff5 commit 36ffa12
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
abstract class SemReason extends TSemReason {
/** Gets a textual representation of this reason. */
abstract string toString();

abstract SemReason combineWith(SemReason reason);
}

/**
Expand All @@ -28,6 +30,8 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
*/
class SemNoReason extends SemReason, TSemNoReason {
override string toString() { result = "NoReason" }

override SemReason combineWith(SemReason reason) { result = reason }
}

/** A reason for an inferred bound pointing to a condition. */
Expand All @@ -36,10 +40,16 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
SemGuard getCond() { this = TSemCondReason(result) }

override string toString() { result = this.getCond().toString() }

override SemReason combineWith(SemReason reason) {
if reason instanceof SemTypeReason then result instanceof SemTypeReason else result = this
}
}

class SemTypeReason extends SemReason, TSemTypeReason {
override string toString() { result = "TypeReason" }

override SemReason combineWith(SemReason reason) { result = this and exists(reason) }
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
abstract class SemReason extends TSemReason {
/** Gets a textual representation of this reason. */
abstract string toString();

abstract SemReason combineWith(SemReason reason);
}

/**
Expand All @@ -42,6 +44,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
*/
class SemNoReason extends SemReason, TSemNoReason {
override string toString() { result = "NoReason" }

override SemReason combineWith(SemReason reason) { result = reason }
}

/** A reason for an inferred bound pointing to a condition. */
Expand All @@ -50,6 +54,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
SemGuard getCond() { this = TSemCondReason(result) }

override string toString() { result = this.getCond().toString() }

override SemReason combineWith(SemReason reason) { result = reason }
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,9 @@ signature module DeltaSig {
}

signature module LangSig<DeltaSig D> {
class SemReason;
class SemReason {
SemReason combineWith(SemReason reason);
}

class SemNoReason extends SemReason;

Expand Down Expand Up @@ -1120,9 +1122,15 @@ module RangeStage<
delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
b = bLeft and
origdelta = odLeft and
reason = rLeft.combineWith(rRight) and
bRight instanceof SemZeroBound
or
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
b = bRight and
origdelta = odRight and
reason = rRight.combineWith(rLeft) and
bLeft instanceof SemZeroBound
)
or
exists(
Expand Down

0 comments on commit 36ffa12

Please sign in to comment.