Skip to content

Commit d22612b

Browse files
rcosta358rcosta358
authored
Propagate Function Invocations (#216)
1 parent 447b469 commit d22612b

4 files changed

Lines changed: 298 additions & 767 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import liquidjava.rj_language.ast.BinaryExpression;
44
import liquidjava.rj_language.ast.Expression;
5+
import liquidjava.rj_language.ast.FunctionInvocation;
56
import liquidjava.rj_language.ast.UnaryExpression;
67
import liquidjava.rj_language.ast.Var;
78
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
@@ -23,7 +24,7 @@ public class VariablePropagation {
2324
*/
2425
public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
2526
Map<String, Expression> substitutions = VariableResolver.resolve(exp);
26-
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
27+
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
2728
Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
2829
for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
2930
Expression value = entry.getValue();
@@ -69,6 +70,12 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
6970
return new ValDerivationNode(var, null);
7071
}
7172

73+
if (exp instanceof FunctionInvocation) {
74+
Expression value = subs.get(exp.toString());
75+
if (value != null)
76+
return new ValDerivationNode(value.clone(), new VarDerivationNode(exp.toString()));
77+
}
78+
7279
// lift unary origin
7380
if (exp instanceof UnaryExpression unary) {
7481
ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins);

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java‎

Lines changed: 70 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77

88
import liquidjava.rj_language.ast.BinaryExpression;
99
import liquidjava.rj_language.ast.Expression;
10+
import liquidjava.rj_language.ast.FunctionInvocation;
1011
import liquidjava.rj_language.ast.Var;
1112

1213
public class VariableResolver {
@@ -25,7 +26,7 @@ public static Map<String, Expression> resolve(Expression exp) {
2526
resolveRecursive(exp, map);
2627

2728
// remove variables that were not used in the expression
28-
map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey()));
29+
map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue()));
2930

3031
// transitively resolve variables
3132
return resolveTransitive(map);
@@ -45,33 +46,49 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
4546
if ("&&".equals(op)) {
4647
resolveRecursive(be.getFirstOperand(), map);
4748
resolveRecursive(be.getSecondOperand(), map);
48-
} else if ("==".equals(op)) {
49-
Expression left = be.getFirstOperand();
50-
Expression right = be.getSecondOperand();
51-
if (left instanceof Var var && right.isLiteral()) {
52-
map.put(var.getName(), right.clone());
53-
} else if (right instanceof Var var && left.isLiteral()) {
54-
map.put(var.getName(), left.clone());
55-
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
56-
// to substitute internal variable with user-facing variable
57-
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
58-
map.put(leftVar.getName(), right.clone());
59-
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
60-
map.put(rightVar.getName(), left.clone());
61-
} else if (isInternal(leftVar) && isInternal(rightVar)) {
62-
// to substitute the lower-counter variable with the higher-counter one
63-
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
64-
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
65-
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
66-
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
67-
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
68-
}
69-
} else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
70-
map.put(var.getName(), right.clone());
49+
return;
50+
}
51+
if (!"==".equals(op))
52+
return;
53+
54+
Expression left = be.getFirstOperand();
55+
Expression right = be.getSecondOperand();
56+
String leftKey = substitutionKey(left);
57+
String rightKey = substitutionKey(right);
58+
59+
if (leftKey != null && right.isLiteral()) {
60+
map.put(leftKey, right.clone());
61+
} else if (rightKey != null && left.isLiteral()) {
62+
map.put(rightKey, left.clone());
63+
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
64+
// to substitute internal variable with user-facing variable
65+
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
66+
map.put(leftVar.getName(), right.clone());
67+
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
68+
map.put(rightVar.getName(), left.clone());
69+
} else if (isInternal(leftVar) && isInternal(rightVar)) {
70+
// to substitute the lower-counter variable with the higher-counter one
71+
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
72+
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
73+
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
74+
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
75+
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
7176
}
77+
} else if (left instanceof Var var && canSubstitute(var, right)) {
78+
map.put(var.getName(), right.clone());
79+
} else if (left instanceof FunctionInvocation && !containsExpression(right, left)) {
80+
map.put(leftKey, right.clone());
7281
}
7382
}
7483

84+
private static String substitutionKey(Expression exp) {
85+
if (exp instanceof Var var)
86+
return var.getName();
87+
if (exp instanceof FunctionInvocation)
88+
return exp.toString();
89+
return null;
90+
}
91+
7592
/**
7693
* Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
7794
*
@@ -98,10 +115,10 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
98115
* @return resolved expression
99116
*/
100117
private static Expression lookup(Expression exp, Map<String, Expression> map, Set<String> seen) {
101-
if (!(exp instanceof Var))
118+
String name = substitutionKey(exp);
119+
if (name == null)
102120
return exp;
103121

104-
String name = exp.toString();
105122
if (seen.contains(name))
106123
return exp; // circular reference
107124

@@ -121,27 +138,36 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
121138
*
122139
* @return true if used, false otherwise
123140
*/
124-
private static boolean hasUsage(Expression exp, String name) {
141+
private static boolean hasUsage(Expression exp, String name, Expression value) {
125142
// exclude own definitions
126143
if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
127144
Expression left = binary.getFirstOperand();
128145
Expression right = binary.getSecondOperand();
129-
if (left instanceof Var v && v.getName().equals(name)
146+
if (left instanceof Var v && v.getName().equals(name) && right.equals(value)
130147
&& (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
131148
return false;
132-
if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
149+
if (left instanceof FunctionInvocation && left.toString().equals(name) && right.equals(value)
150+
&& (right.isLiteral() || (!(right instanceof Var) && !containsExpression(right, left))))
151+
return false;
152+
if (right instanceof Var v && v.getName().equals(name) && left.equals(value) && left.isLiteral())
153+
return false;
154+
if (right instanceof FunctionInvocation && right.toString().equals(name) && left.equals(value)
155+
&& left.isLiteral())
133156
return false;
134157
}
135158

136159
// usage found
137160
if (exp instanceof Var var && var.getName().equals(name)) {
138161
return true;
139162
}
163+
if (exp instanceof FunctionInvocation && exp.toString().equals(name)) {
164+
return true;
165+
}
140166

141167
// recurse children
142168
if (exp.hasChildren()) {
143169
for (Expression child : exp.getChildren())
144-
if (hasUsage(child, name))
170+
if (hasUsage(child, name, value))
145171
return true;
146172
}
147173

@@ -185,4 +211,18 @@ private static boolean containsVariable(Expression exp, String name) {
185211
}
186212
return false;
187213
}
214+
215+
private static boolean containsExpression(Expression exp, Expression target) {
216+
if (exp.equals(target))
217+
return true;
218+
219+
if (!exp.hasChildren())
220+
return false;
221+
222+
for (Expression child : exp.getChildren()) {
223+
if (containsExpression(child, target))
224+
return true;
225+
}
226+
return false;
227+
}
188228
}

0 commit comments

Comments
 (0)