Merge pull request #7698 from aschackmull/java/bitwise-assignop-guards

Java: Add support for bitwise compound assignments in Guards.
This commit is contained in:
Anders Schack-Mulligen
2022-01-24 09:11:53 +01:00
committed by GitHub
3 changed files with 55 additions and 7 deletions

View File

@@ -23,19 +23,23 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
or
g1.(OrBitwiseExpr).getAnOperand() = g2 and b1 = false and b2 = false
or
g1.(AssignAndExpr).getSource() = g2 and b1 = true and b2 = true
or
g1.(AssignOrExpr).getSource() = g2 and b1 = false and b2 = false
or
g1.(AndLogicalExpr).getAnOperand() = g2 and b1 = true and b2 = true
or
g1.(OrLogicalExpr).getAnOperand() = g2 and b1 = false and b2 = false
or
g1.(LogNotExpr).getExpr() = g2 and
b1 = b2.booleanNot() and
(b1 = true or b1 = false)
b1 = [true, false]
or
exists(EqualityTest eqtest, boolean polarity, BooleanLiteral boollit |
eqtest = g1 and
eqtest.hasOperands(g2, boollit) and
eqtest.polarity() = polarity and
(b1 = true or b1 = false) and
b1 = [true, false] and
b2 = b1.booleanXor(polarity).booleanXor(boollit.getBooleanValue())
)
or
@@ -56,16 +60,20 @@ predicate implies_v1(Guard g1, boolean b1, Guard g2, boolean b2) {
exists(MethodAccess check | check = g1 |
conditionCheck(check, _) and
g2 = check.getArgument(0) and
(b1 = true or b1 = false) and
b1 = [true, false] and
b2 = b1
)
or
exists(BaseSsaUpdate vbool |
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
vbool.getDefiningExpr().(AssignOp) = g2
|
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
(b1 = true or b1 = false) and
b1 = [true, false] and
b2 = b1
)
or
g1.(AssignExpr).getSource() = g2 and b2 = b1 and b1 = [true, false]
}
/**
@@ -79,9 +87,11 @@ predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
implies_v1(g1, b1, g2, b2)
or
exists(SsaExplicitUpdate vbool |
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 or
vbool.getDefiningExpr().(AssignOp) = g2
|
vbool.getAUse() = g1 and
vbool.getDefiningExpr().(VariableAssign).getSource() = g2 and
(b1 = true or b1 = false) and
b1 = [true, false] and
b2 = b1
)
or