C++: Add AST wrappers for the new predicates.

This commit is contained in:
Mathias Vorreiter Pedersen
2024-03-18 16:26:36 +00:00
parent decede51dc
commit dbd47b387a

View File

@@ -137,6 +137,17 @@ 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`. */
cached
predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) { none() }
/**
* Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
* If `areEqual = false` then this implies `e != k`.
*/
cached
predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) { none() }
}
/**
@@ -184,6 +195,20 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
this.comparesEq(left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
)
}
override predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) {
exists(boolean partIsTrue, GuardCondition part |
this.(BinaryLogicalOperation).impliesValue(part, partIsTrue, testIsTrue)
|
part.comparesEq(e, k, areEqual, partIsTrue)
)
}
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)
)
}
}
/**
@@ -245,6 +270,21 @@ private class GuardConditionFromIR extends GuardCondition {
)
}
override predicate comparesEq(Expr e, int k, boolean areEqual, boolean testIsTrue) {
exists(Instruction i |
i.getUnconvertedResultExpression() = e and
ir.comparesEq(i.getAUse(), k, areEqual, testIsTrue)
)
}
override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
exists(Instruction i, boolean testIsTrue |
i.getUnconvertedResultExpression() = e and
ir.comparesEq(i.getAUse(), k, areEqual, testIsTrue) and
this.controls(block, testIsTrue)
)
}
/**
* Holds if this condition controls `block`, meaning that `block` is only
* entered if the value of this condition is `v`. This helper