Merge pull request #15976 from MathiasVP/guards-eq-follow-up

C++: Fix interface for `GuardCondition.comparesEq` and `GuardCondition.ensuresEq`
This commit is contained in:
Mathias Vorreiter Pedersen
2024-03-19 16:45:38 +00:00
committed by GitHub
4 changed files with 51 additions and 54 deletions

View File

@@ -138,9 +138,9 @@ class GuardCondition extends Expr {
cached
predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) { none() }
/** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
/** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */
cached
predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) { none() }
predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) { none() }
/**
* Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
@@ -196,17 +196,18 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
)
}
override predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) {
exists(boolean partIsTrue, GuardCondition part |
this.(BinaryLogicalOperation).impliesValue(part, partIsTrue, testIsTrue)
override predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) {
exists(BooleanValue partValue, GuardCondition part |
this.(BinaryLogicalOperation)
.impliesValue(part, partValue.getValue(), value.(BooleanValue).getValue())
|
part.comparesEq(e, k, areEqual, partIsTrue)
part.comparesEq(e, k, areEqual, partValue)
)
}
override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
exists(boolean testIsTrue |
this.comparesEq(e, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
exists(AbstractValue value |
this.comparesEq(e, k, areEqual, value) and this.valueControls(block, value)
)
}
}
@@ -270,18 +271,18 @@ private class GuardConditionFromIR extends GuardCondition {
)
}
override predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) {
override predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value) {
exists(Instruction i |
i.getUnconvertedResultExpression() = e and
ir.comparesEq(i.getAUse(), k, areEqual, testIsTrue)
ir.comparesEq(i.getAUse(), k, areEqual, value)
)
}
override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
exists(Instruction i, boolean testIsTrue |
exists(Instruction i, AbstractValue value |
i.getUnconvertedResultExpression() = e and
ir.comparesEq(i.getAUse(), k, areEqual, testIsTrue) and
this.controls(block, testIsTrue)
ir.comparesEq(i.getAUse(), k, areEqual, value) and
this.valueControls(block, value)
)
}
@@ -492,19 +493,10 @@ class IRGuardCondition extends Instruction {
)
}
/** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
/** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
cached
predicate comparesEq(Operand op, int k, boolean areEqual, boolean testIsTrue) {
exists(MatchValue mv |
compares_eq(this, op, k, areEqual, mv) and
// A match value cannot be dualized, so `testIsTrue` is always true
testIsTrue = true
)
or
exists(BooleanValue bv |
compares_eq(this, op, k, areEqual, bv) and
bv.getValue() = testIsTrue
)
predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) {
compares_eq(this, op, k, areEqual, value)
}
/**

View File

@@ -4,8 +4,8 @@ import semmle.code.cpp.controlflow.IRGuards
query predicate astGuards(GuardCondition guard) { any() }
query predicate astGuardsCompare(int startLine, string msg) {
exists(GuardCondition guard, Expr left, int k, string which, string op |
exists(boolean sense |
exists(GuardCondition guard, Expr left, int k, string op |
exists(boolean sense, string which |
sense = true and which = "true"
or
sense = false and which = "false"
@@ -21,14 +21,16 @@ query predicate astGuardsCompare(int startLine, string msg) {
|
msg = left + op + right + "+" + k + " when " + guard + " is " + which
)
)
or
exists(AbstractValue value |
guard.comparesEq(left, k, true, value) and op = " == "
or
(
guard.comparesEq(left, k, true, sense) and op = " == "
or
guard.comparesEq(left, k, false, sense) and op = " != "
) and
msg = left + op + k + " when " + guard + " is " + which
) and
guard.comparesEq(left, k, false, value) and op = " != "
|
msg = left + op + k + " when " + guard + " is " + value
)
|
startLine = guard.getLocation().getStartLine()
)
}
@@ -71,8 +73,8 @@ query predicate astGuardsEnsure_const(
query predicate irGuards(IRGuardCondition guard) { any() }
query predicate irGuardsCompare(int startLine, string msg) {
exists(IRGuardCondition guard, Operand left, int k, string which, string op |
exists(boolean sense |
exists(IRGuardCondition guard, Operand left, int k, string op |
exists(boolean sense, string which |
sense = true and which = "true"
or
sense = false and which = "false"
@@ -91,16 +93,18 @@ query predicate irGuardsCompare(int startLine, string msg) {
right.getAnyDef().getUnconvertedResultExpression() + "+" + k + " when " + guard + " is "
+ which
)
)
or
exists(AbstractValue value |
guard.comparesEq(left, k, true, value) and op = " == "
or
(
guard.comparesEq(left, k, true, sense) and op = " == "
or
guard.comparesEq(left, k, false, sense) and op = " != "
) and
guard.comparesEq(left, k, false, value) and op = " != "
|
msg =
left.getAnyDef().getUnconvertedResultExpression() + op + k + " when " + guard + " is " +
which
) and
value
)
|
startLine = guard.getLocation().getStartLine()
)
}

View File

@@ -55,9 +55,9 @@
| 58 | y < 0+0 when ... < ... is true |
| 58 | y >= 0+0 when ... < ... is false |
| 58 | y >= 0+0 when ... \|\| ... is false |
| 61 | i == 0 when i is true |
| 61 | i == 1 when i is true |
| 61 | i == 2 when i is true |
| 61 | i == 0 when i is Case[0] |
| 61 | i == 1 when i is Case[1] |
| 61 | i == 2 when i is Case[2] |
| 75 | 0 != x+0 when ... == ... is false |
| 75 | 0 == x+0 when ... == ... is true |
| 75 | x != 0 when ... == ... is false |

View File

@@ -7,9 +7,9 @@
import cpp
import semmle.code.cpp.controlflow.Guards
from GuardCondition guard, Expr left, int k, string which, string op, string msg
from GuardCondition guard, Expr left, int k, string op, string msg
where
exists(boolean sense |
exists(boolean sense, string which |
sense = true and which = "true"
or
sense = false and which = "false"
@@ -25,12 +25,13 @@ where
|
msg = left + op + right + "+" + k + " when " + guard + " is " + which
)
)
or
exists(AbstractValue value |
guard.comparesEq(left, k, true, value) and op = " == "
or
(
guard.comparesEq(left, k, true, sense) and op = " == "
or
guard.comparesEq(left, k, false, sense) and op = " != "
) and
msg = left + op + k + " when " + guard + " is " + which
guard.comparesEq(left, k, false, value) and op = " != "
|
msg = left + op + k + " when " + guard + " is " + value
)
select guard.getLocation().getStartLine(), msg