Skip to content

C++: Fix interface for GuardCondition.comparesEq and GuardCondition.ensuresEq #15976

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 19, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 17 additions & 25 deletions cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down Expand Up @@ -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)
)
}
}
Expand Down Expand Up @@ -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)
)
}

Expand Down Expand Up @@ -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)
}

/**
Expand Down
40 changes: 22 additions & 18 deletions cpp/ql/test/library-tests/controlflow/guards-ir/tests.ql
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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()
)
}
Expand Down Expand Up @@ -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"
Expand All @@ -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()
)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down
17 changes: 9 additions & 8 deletions cpp/ql/test/library-tests/controlflow/guards/GuardsCompare.ql
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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