Skip to content

Propagate Function Invocations #216

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.

Sign up for GitHub

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

Open
rcosta358 wants to merge 12 commits into
base: main
Choose a base branch
from
Open

Propagate Function Invocations #216

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
b3c83ce
Propagate Expressions
rcosta358 May 9, 2026
c7afdde
Fold Adjacent Constants
rcosta358 May 9, 2026
1516285
Add Function Invocation Simplification
rcosta358 May 9, 2026
9970654
Trigger Workflow
rcosta358 May 9, 2026
d7dbef0
Merge branch 'main' into improve-simplification
rcosta358 May 9, 2026
2072c59
Merge branch 'improve-simplification' into function-invocation-simpli…
rcosta358 May 9, 2026
2696792
Merge branch 'main' into function-invocation-simplification
rcosta358 May 11, 2026
78d70cc
Minor Change
rcosta358 May 11, 2026
6b8b334
Add More Tests
rcosta358 May 11, 2026
91d8699
Refactor Simplification Tests
rcosta358 May 11, 2026
b7c463a
Formatting
rcosta358 May 11, 2026
647f13c
Replace String Check with AST Check
rcosta358 May 11, 2026
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
9 changes: 8 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import liquidjava.rj_language.ast.BinaryExpression;
import liquidjava.rj_language.ast.Expression;
import liquidjava.rj_language.ast.FunctionInvocation;
import liquidjava.rj_language.ast.UnaryExpression;
import liquidjava.rj_language.ast.Var;
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
Expand All @@ -23,7 +24,7 @@ public class VariablePropagation {
*/
public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
Map<String, Expression> substitutions = VariableResolver.resolve(exp);
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
Expression value = entry.getValue();
Expand Down Expand Up @@ -69,6 +70,12 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
return new ValDerivationNode(var, null);
}

if (exp instanceof FunctionInvocation) {
Expression value = subs.get(exp.toString());
if (value != null)
return new ValDerivationNode(value.clone(), new VarDerivationNode(exp.toString()));
}

// lift unary origin
if (exp instanceof UnaryExpression unary) {
ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins);
Expand Down
71 changes: 48 additions & 23 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@

import liquidjava.rj_language.ast.BinaryExpression;
import liquidjava.rj_language.ast.Expression;
import liquidjava.rj_language.ast.FunctionInvocation;
import liquidjava.rj_language.ast.Var;

public class VariableResolver {
Expand Down Expand Up @@ -45,33 +46,49 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
if ("&&".equals(op)) {
resolveRecursive(be.getFirstOperand(), map);
resolveRecursive(be.getSecondOperand(), map);
} else if ("==".equals(op)) {
Expression left = be.getFirstOperand();
Expression right = be.getSecondOperand();
if (left instanceof Var var && right.isLiteral()) {
map.put(var.getName(), right.clone());
} else if (right instanceof Var var && left.isLiteral()) {
map.put(var.getName(), left.clone());
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
// to substitute internal variable with user-facing variable
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
map.put(leftVar.getName(), right.clone());
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
map.put(rightVar.getName(), left.clone());
} else if (isInternal(leftVar) && isInternal(rightVar)) {
// to substitute the lower-counter variable with the higher-counter one
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
}
} else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
map.put(var.getName(), right.clone());
return;
}
if (!"==".equals(op))
return;

Expression left = be.getFirstOperand();
Expression right = be.getSecondOperand();
String leftKey = substitutionKey(left);
String rightKey = substitutionKey(right);
Copy link
Copy Markdown
Collaborator

@CatarinaGamboa CatarinaGamboa May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is using strings for substitution really the best approach?


if (leftKey != null && right.isLiteral()) {
map.put(leftKey, right.clone());
} else if (rightKey != null && left.isLiteral()) {
map.put(rightKey, left.clone());
} else if (left instanceof Var leftVar && right instanceof Var rightVar) {
// to substitute internal variable with user-facing variable
if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
map.put(leftVar.getName(), right.clone());
} else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
map.put(rightVar.getName(), left.clone());
} else if (isInternal(leftVar) && isInternal(rightVar)) {
// to substitute the lower-counter variable with the higher-counter one
boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
Var higherVar = isLeftCounterLower ? rightVar : leftVar;
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
}
} else if (left instanceof Var var && canSubstitute(var, right)) {
map.put(var.getName(), right.clone());
} else if (left instanceof FunctionInvocation && !right.toString().contains(leftKey)) {
map.put(leftKey, right.clone());
Copy link
Copy Markdown
Collaborator

@CatarinaGamboa CatarinaGamboa May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this means we would not substitute something like:
f(a) == ff(a) + b

because the string on the right contains f(a) even though they are not related, right?
Ig better be conservative but we should be aware of this limitation

Copy link
Copy Markdown
Collaborator Author

@rcosta358 rcosta358 May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, I'll replace that string check with an AST check.

}
}

private static String substitutionKey(Expression exp) {
if (exp instanceof Var var)
return var.getName();
if (exp instanceof FunctionInvocation)
return exp.toString();
return null;
}

/**
* Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
*
Expand Down Expand Up @@ -129,14 +146,22 @@ private static boolean hasUsage(Expression exp, String name) {
if (left instanceof Var v && v.getName().equals(name)
&& (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
return false;
if (left instanceof FunctionInvocation && left.toString().equals(name)
&& (right.isLiteral() || (!(right instanceof Var) && !right.toString().contains(name))))
return false;
if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
return false;
if (right instanceof FunctionInvocation && right.toString().equals(name) && left.isLiteral())
return false;
}

// usage found
if (exp instanceof Var var && var.getName().equals(name)) {
return true;
}
if (exp instanceof FunctionInvocation && exp.toString().equals(name)) {
return true;
}

// recurse children
if (exp.hasChildren()) {
Expand Down
25 changes: 25 additions & 0 deletions liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
import liquidjava.rj_language.ast.AliasInvocation;
import liquidjava.rj_language.ast.BinaryExpression;
import liquidjava.rj_language.ast.Expression;
import liquidjava.rj_language.ast.FunctionInvocation;
import liquidjava.rj_language.ast.Ite;
import liquidjava.rj_language.ast.LiteralBoolean;
import liquidjava.rj_language.ast.LiteralInt;
Expand Down Expand Up @@ -1133,4 +1134,28 @@ void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() {
assertEquals("x + 3", ExpressionSimplifier.simplify(xPlus1Plus2).getValue().toString());
assertEquals("x", ExpressionSimplifier.simplify(xPlus1Minus1).getValue().toString());
}

@Test
void testFunctionInvocationEqualitiesPropagateTransitively() {
// Given: size(x3) == size(x2) - 1 && size(x2) == size(x1) + 1 && size(x1) == 0
// Expected: size(x3) == 0
Expression x1 = new Var("x1");
Expression x2 = new Var("x2");
Expression x3 = new Var("x3");
Expression sizeX1 = new FunctionInvocation("size", List.of(x1));
Expression sizeX2 = new FunctionInvocation("size", List.of(x2));
Expression sizeX3 = new FunctionInvocation("size", List.of(x3));

Expression sizeX3EqualsSizeX2Minus1 = new BinaryExpression(sizeX3, "==",
new BinaryExpression(sizeX2, "-", new LiteralInt(1)));
Expression sizeX2EqualsSizeX1Plus1 = new BinaryExpression(sizeX2, "==",
new BinaryExpression(sizeX1, "+", new LiteralInt(1)));
Expression sizeX1Equals0 = new BinaryExpression(sizeX1, "==", new LiteralInt(0));
Expression fullExpression = new BinaryExpression(sizeX3EqualsSizeX2Minus1, "&&",
new BinaryExpression(sizeX2EqualsSizeX1Plus1, "&&", sizeX1Equals0));

ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);

assertEquals("size(x3) == 0", result.getValue().toString());
}
Copy link
Copy Markdown
Collaborator

@CatarinaGamboa CatarinaGamboa May 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we need a couple more tests for this, I'm not very convinced

}
Loading