|
13 | 13 | import csharp |
14 | 14 |
|
15 | 15 | /** |
16 | | - * Holds if expression `expr` has Boolean `value` at child `child`. |
17 | | - * No other child nodes are boolean literals. |
| 16 | + * Holds if the left operand of a binary operation is a Boolean literal with the specified value |
| 17 | + * and the right operand is not a Boolean literal. |
18 | 18 | */ |
19 | | -predicate literalChild(Expr expr, int child, boolean value) { |
20 | | - value = expr.getChild(child).(BoolLiteral).getBoolValue() and |
21 | | - forall(int c | c != child | not expr.getChild(c) instanceof BoolLiteral) |
| 19 | +predicate binaryLiteralLeft(BinaryOperation op, boolean value) { |
| 20 | + value = op.getLeftOperand().(BoolLiteral).getBoolValue() and |
| 21 | + not op.getRightOperand() instanceof BoolLiteral |
22 | 22 | } |
23 | 23 |
|
24 | 24 | /** |
25 | | - * Expression `expr` has Boolean `value1` at child `child1`, and boolean `value2` at `child2`. |
26 | | - * No other child nodes are boolean literals. |
| 25 | + * Holds if the right operand of a binary operation is a Boolean literal with the specified value |
| 26 | + * and the left operand is not a Boolean literal. |
27 | 27 | */ |
28 | | -predicate literalChildren(Expr expr, int child1, boolean value1, int child2, boolean value2) { |
29 | | - value1 = expr.getChild(child1).(BoolLiteral).getBoolValue() and |
30 | | - value2 = expr.getChild(child2).(BoolLiteral).getBoolValue() and |
31 | | - forall(int c | c != child1 and c != child2 | not expr.getChild(c) instanceof BoolLiteral) |
| 28 | +predicate binaryLiteralRight(BinaryOperation op, boolean value) { |
| 29 | + value = op.getRightOperand().(BoolLiteral).getBoolValue() and |
| 30 | + not op.getLeftOperand() instanceof BoolLiteral |
32 | 31 | } |
33 | 32 |
|
34 | | -predicate rewriteBinaryExpr(BinaryOperation op, boolean value, string oldPattern) { |
35 | | - literalChild(op, 0, value) and oldPattern = value + " " + op.getOperator() + " A" |
36 | | - or |
37 | | - literalChild(op, 1, value) and oldPattern = "A " + op.getOperator() + " " + value |
| 33 | +/** |
| 34 | + * Holds if the 'then' branch of a conditional expression is a Boolean literal with the specified value |
| 35 | + * and the 'condition' or 'else' branch are not Boolean literals. |
| 36 | + */ |
| 37 | +predicate conditionalThenLiteral(ConditionalExpr cond, boolean value) { |
| 38 | + value = cond.getThen().(BoolLiteral).getBoolValue() and |
| 39 | + not cond.getCondition() instanceof BoolLiteral and |
| 40 | + not cond.getElse() instanceof BoolLiteral |
38 | 41 | } |
39 | 42 |
|
40 | | -bindingset[withFalseOperand, withTrueOperand] |
41 | | -predicate rewriteBinaryExpr( |
42 | | - BinaryOperation op, string oldPattern, string withFalseOperand, string withTrueOperand, |
43 | | - string newPattern |
44 | | -) { |
45 | | - rewriteBinaryExpr(op, false, oldPattern) and newPattern = withFalseOperand |
46 | | - or |
47 | | - rewriteBinaryExpr(op, true, oldPattern) and newPattern = withTrueOperand |
| 43 | +/** |
| 44 | + * Holds if the 'else' branch of a conditional expression is a Boolean literal with the specified value |
| 45 | + * and the 'condition' or 'then' branch are not Boolean literals. |
| 46 | + */ |
| 47 | +predicate conditionalElseLiteral(ConditionalExpr cond, boolean value) { |
| 48 | + value = cond.getElse().(BoolLiteral).getBoolValue() and |
| 49 | + not cond.getCondition() instanceof BoolLiteral and |
| 50 | + not cond.getThen() instanceof BoolLiteral |
| 51 | +} |
| 52 | + |
| 53 | +/** |
| 54 | + * Holds if both the 'then' and 'else' branches of a conditional expression are Boolean literals with the specified values |
| 55 | + * and the 'condition' branch is not a Boolean literal. |
| 56 | + */ |
| 57 | +predicate conditionalThenAndElseLiteral(ConditionalExpr cond, boolean thenValue, boolean elseValue) { |
| 58 | + thenValue = cond.getThen().(BoolLiteral).getBoolValue() and |
| 59 | + elseValue = cond.getElse().(BoolLiteral).getBoolValue() and |
| 60 | + not cond.getCondition() instanceof BoolLiteral |
| 61 | +} |
| 62 | + |
| 63 | +predicate rewriteBinaryExpr(BinaryOperation op, boolean value, string oldPattern) { |
| 64 | + op.getLeftOperand().getType() instanceof BoolType and |
| 65 | + op.getRightOperand().getType() instanceof BoolType and |
| 66 | + ( |
| 67 | + binaryLiteralLeft(op, value) and oldPattern = value + " " + op.getOperator() + " A" |
| 68 | + or |
| 69 | + binaryLiteralRight(op, value) and oldPattern = "A " + op.getOperator() + " " + value |
| 70 | + ) |
48 | 71 | } |
49 | 72 |
|
50 | 73 | predicate rewriteConditionalExpr(ConditionalExpr cond, string oldPattern, string newPattern) { |
51 | | - literalChild(cond, 1, false) and oldPattern = "A ? false : B" and newPattern = "!A && B" |
52 | | - or |
53 | | - literalChild(cond, 1, true) and oldPattern = "A ? true : B" and newPattern = "A || B" |
54 | | - or |
55 | | - literalChild(cond, 2, false) and oldPattern = "A ? B : false" and newPattern = "A && B" |
56 | | - or |
57 | | - literalChild(cond, 2, true) and oldPattern = "A ? B : true" and newPattern = "!A || B" |
58 | | - or |
59 | | - exists(boolean b | literalChildren(cond, 1, b, 2, b) | |
60 | | - oldPattern = "A ? " + b + " : " + b and newPattern = b.toString() |
| 74 | + cond.getCondition().getType() instanceof BoolType and |
| 75 | + cond.getThen().getType() instanceof BoolType and |
| 76 | + cond.getElse().getType() instanceof BoolType and |
| 77 | + ( |
| 78 | + conditionalThenLiteral(cond, false) and oldPattern = "A ? false : B" and newPattern = "!A && B" |
| 79 | + or |
| 80 | + conditionalThenLiteral(cond, true) and oldPattern = "A ? true : B" and newPattern = "A || B" |
| 81 | + or |
| 82 | + conditionalElseLiteral(cond, false) and oldPattern = "A ? B : false" and newPattern = "A && B" |
| 83 | + or |
| 84 | + conditionalElseLiteral(cond, true) and oldPattern = "A ? B : true" and newPattern = "!A || B" |
| 85 | + or |
| 86 | + exists(boolean b | conditionalThenAndElseLiteral(cond, b, b) | |
| 87 | + oldPattern = "A ? " + b + " : " + b and newPattern = b.toString() |
| 88 | + ) |
| 89 | + or |
| 90 | + conditionalThenAndElseLiteral(cond, true, false) and |
| 91 | + oldPattern = "A ? true : false" and |
| 92 | + newPattern = "A" |
| 93 | + or |
| 94 | + conditionalThenAndElseLiteral(cond, false, true) and |
| 95 | + oldPattern = "A ? false : true" and |
| 96 | + newPattern = "!A" |
61 | 97 | ) |
62 | | - or |
63 | | - literalChildren(cond, 1, true, 2, false) and oldPattern = "A ? true : false" and newPattern = "A" |
64 | | - or |
65 | | - literalChildren(cond, 1, false, 2, true) and oldPattern = "A ? false : true" and newPattern = "!A" |
66 | 98 | } |
67 | 99 |
|
68 | 100 | predicate negatedOperators(string op, string negated) { |
@@ -115,12 +147,20 @@ predicate pushNegation(LogicalNotExpr expr, string oldPattern, string newPattern |
115 | 147 | ) |
116 | 148 | } |
117 | 149 |
|
118 | | -predicate rewrite(Expr expr, string oldPattern, string newPattern) { |
| 150 | +predicate rewriteBinaryOperation(BinaryOperation op, string oldPattern, string newPattern) { |
119 | 151 | exists(string withFalseOperand, string withTrueOperand | |
120 | | - simplifyBinaryExpr(expr.(BinaryOperation).getOperator(), withFalseOperand, withTrueOperand) |
| 152 | + simplifyBinaryExpr(op.getOperator(), withFalseOperand, withTrueOperand) |
121 | 153 | | |
122 | | - rewriteBinaryExpr(expr, oldPattern, withFalseOperand, withTrueOperand, newPattern) |
| 154 | + rewriteBinaryExpr(op, false, oldPattern) and |
| 155 | + newPattern = withFalseOperand |
| 156 | + or |
| 157 | + rewriteBinaryExpr(op, true, oldPattern) and |
| 158 | + newPattern = withTrueOperand |
123 | 159 | ) |
| 160 | +} |
| 161 | + |
| 162 | +predicate rewrite(Expr expr, string oldPattern, string newPattern) { |
| 163 | + rewriteBinaryOperation(expr, oldPattern, newPattern) |
124 | 164 | or |
125 | 165 | rewriteConditionalExpr(expr, oldPattern, newPattern) |
126 | 166 | or |
|
0 commit comments