Guards: Refactor representation of false.

This commit is contained in:
Anders Schack-Mulligen
2025-09-22 12:44:36 +02:00
parent 402d58bc3a
commit 64caae554a

View File

@@ -202,12 +202,14 @@ module Make<
private newtype TAbstractSingleValue =
TValueNull() or
TValueTrue() or
TValueBool(Boolean b) or
TValueInt(int i) { exists(ConstantExpr c | c.asIntegerValue() = i) or i = 0 } or
TValueConstant(ConstantValue c) { exists(ConstantExpr ce | ce.asConstantValue() = c) }
private newtype TGuardValue =
TValue(TAbstractSingleValue val, Boolean isVal) or
TValue(TAbstractSingleValue val, Boolean isVal) {
val instanceof TValueBool implies isVal = true
} or
TIntRange(int bound, Boolean upper) {
exists(ConstantExpr c | c.asIntegerValue() + [-1, 0, 1] = bound) and
// exclude edge cases to avoid overflow issues when computing duals
@@ -221,7 +223,9 @@ module Make<
string toString() {
result = "null" and this instanceof TValueNull
or
result = "true" and this instanceof TValueTrue
result = "true" and this = TValueBool(true)
or
result = "false" and this = TValueBool(false)
or
exists(int i | result = i.toString() and this = TValueInt(i))
or
@@ -244,6 +248,11 @@ module Make<
result = TValue(val, isVal.booleanNot())
)
or
exists(boolean b |
this = TValue(TValueBool(b), true) and
result = TValue(TValueBool(b.booleanNot()), true)
)
or
exists(int bound, int d, boolean upper |
upper = true and d = 1
or
@@ -275,7 +284,7 @@ module Make<
int asIntValue() { this = TValue(TValueInt(result), true) }
/** Gets the boolean that this value represents, if any. */
boolean asBooleanValue() { this = TValue(TValueTrue(), result) }
boolean asBooleanValue() { this = TValue(TValueBool(result), true) }
/** Gets the constant that this value represents, if any. */
ConstantValue asConstantValue() { this = TValue(TValueConstant(result), true) }
@@ -293,9 +302,7 @@ module Make<
/** Gets a textual representation of this value. */
string toString() {
result = this.asBooleanValue().toString()
or
exists(AbstractSingleValue val | not val instanceof TValueTrue |
exists(AbstractSingleValue val |
this = TValue(val, true) and result = val.toString()
or
this = TValue(val, false) and result = "not " + val.toString()
@@ -365,15 +372,10 @@ module Make<
}
private predicate branchEdge(BasicBlock bb1, BasicBlock bb2, GuardValue v) {
exists(ConditionalSuccessor s |
bb1.getASuccessor(s) = bb2 and
exists(AbstractSingleValue val |
s instanceof NullnessSuccessor and val = TValueNull()
or
s instanceof BooleanSuccessor and val = TValueTrue()
|
v = TValue(val, s.getValue())
)
exists(ConditionalSuccessor s | bb1.getASuccessor(s) = bb2 |
s instanceof NullnessSuccessor and v = TValue(TValueNull(), s.getValue())
or
s instanceof BooleanSuccessor and v = TValue(TValueBool(s.getValue()), true)
)
or
exceptionBranchPoint(bb1, bb2, _) and v = TException(false)