From 4091d361dffe666b371560f5c79e53ca4d5ad1f6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 11:19:11 +0100 Subject: [PATCH 01/22] Add SimplifiedExpression --- .../rj_language/ast/Expression.java | 5 + .../rj_language/ast/SimplifiedExpression.java | 124 ++++++++++++++++++ .../ast/formatter/ExpressionFormatter.java | 14 +- .../ast/formatter/ExpressionPrecedence.java | 3 + .../rj_language/ast/typing/TypeInfer.java | 3 + .../visitors/ExpressionVisitor.java | 5 +- .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 + 7 files changed, 157 insertions(+), 3 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index ee638262e..20c9fe84e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -82,6 +82,9 @@ public boolean isLiteral() { * @return true if it is a boolean expression, false otherwise */ public boolean isBooleanExpression() { + if (this instanceof SimplifiedExpression node) { + return node.getSimplifiedExpression().isBooleanExpression(); + } if (this instanceof LiteralBoolean || this instanceof Ite || this instanceof AliasInvocation || this instanceof FunctionInvocation) { return true; @@ -99,6 +102,8 @@ public boolean isBooleanExpression() { } public List getConjuncts() { + if (this instanceof SimplifiedExpression node) + return node.getSimplifiedExpression().getConjuncts(); if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) { List conjuncts = new ArrayList<>(); conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java new file mode 100644 index 000000000..e06bbc2dc --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java @@ -0,0 +1,124 @@ +package liquidjava.rj_language.ast; + +import java.util.ArrayList; +import java.util.List; +import java.util.Objects; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; +import spoon.reflect.reference.CtTypeReference; + +public class SimplifiedExpression extends Expression { + + private final Expression origin; + private final List binders; + + public SimplifiedExpression(Expression simplified, Expression origin) { + this(simplified, origin, List.of()); + } + + public SimplifiedExpression(Expression simplified, Expression origin, List binders) { + addChild(simplified); + this.origin = origin; + this.binders = new ArrayList<>(binders); + } + + public Expression getSimplifiedExpression() { + return children.get(0); + } + + public Expression getOrigin() { + return origin; + } + + public List getBinders() { + return binders; + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitSimplifiedNode(this); + } + + @Override + public void getVariableNames(List toAdd) { + getSimplifiedExpression().getVariableNames(toAdd); + } + + @Override + public void getStateInvocations(List toAdd, List all) { + getSimplifiedExpression().getStateInvocations(toAdd, all); + } + + @Override + public boolean isBooleanTrue() { + return getSimplifiedExpression().isBooleanTrue(); + } + + @Override + public Expression clone() { + return new SimplifiedExpression(getSimplifiedExpression().clone(), origin.clone(), binders); + } + + @Override + public String toString() { + return getSimplifiedExpression().toString(); + } + + @Override + public int hashCode() { + return Objects.hash(getSimplifiedExpression(), origin, binders); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + SimplifiedExpression other = (SimplifiedExpression) obj; + return getSimplifiedExpression().equals(other.getSimplifiedExpression()) && origin.equals(other.origin) + && binders.equals(other.binders); + } + + public static class Binder { + private final String name; + private final String type; + + public Binder(String name, String type) { + this.name = name; + this.type = type; + } + + public Binder(String name, CtTypeReference type) { + this(name, type.getQualifiedName()); + } + + public String getName() { + return name; + } + + public String getType() { + return type; + } + + @Override + public int hashCode() { + return Objects.hash(name, type); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + Binder other = (Binder) obj; + return name.equals(other.name) && type.equals(other.type); + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index cf6e4fdce..34d71a1d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -17,6 +17,7 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.Enum; +import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -61,8 +62,12 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression group) - expression = group.getExpression(); + while (expression instanceof GroupExpression || expression instanceof SimplifiedExpression) { + if (expression instanceof GroupExpression group) + expression = group.getExpression(); + else if (expression instanceof SimplifiedExpression node) + expression = node.getSimplifiedExpression(); + } return expression; } @@ -161,6 +166,11 @@ public String visitLiteralString(LiteralString lit) { return lit.toString(); } + @Override + public String visitSimplifiedNode(SimplifiedExpression node) { + return formatExpression(node.getSimplifiedExpression()); + } + @Override public String visitUnaryExpression(UnaryExpression exp) { return exp.getOp() + formatOperand(exp, exp.getExpression(), true); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java index fbaa95cbe..ce9678c52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java @@ -4,6 +4,7 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; public enum ExpressionPrecedence { @@ -16,6 +17,8 @@ public boolean isLowerThan(ExpressionPrecedence other) { public static ExpressionPrecedence of(Expression expression) { if (expression instanceof GroupExpression group) return of(group.getExpression()); + if (expression instanceof SimplifiedExpression node) + return of(node.getSimplifiedExpression()); if (expression instanceof Ite) return TERNARY; if (expression instanceof UnaryExpression) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 0fa965cde..140c7ed88 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -15,6 +15,7 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; @@ -57,6 +58,8 @@ else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); + else if (e instanceof SimplifiedExpression) + return getType(ctx, factory, ((SimplifiedExpression) e).getSimplifiedExpression()); return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java index 904690a79..cd2e9e384 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -13,6 +13,7 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; @@ -39,9 +40,11 @@ public interface ExpressionVisitor { T visitLiteralString(LiteralString lit) throws LJError; + T visitSimplifiedNode(SimplifiedExpression node) throws LJError; + T visitUnaryExpression(UnaryExpression exp) throws LJError; T visitEnum(Enum en) throws LJError; T visitVar(Var var) throws LJError; -} \ No newline at end of file +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 464cd9898..edf4ba9be 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -15,6 +15,7 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -113,6 +114,11 @@ public Expr visitLiteralString(LiteralString lit) { return ctx.makeString(lit.toString()); } + @Override + public Expr visitSimplifiedNode(SimplifiedExpression node) throws LJError { + return node.getSimplifiedExpression().accept(this); + } + @Override public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { return switch (exp.getOp()) { From cfa1be1ef85b9024e1fa1551b624a65d5f104ae2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:23:48 +0100 Subject: [PATCH 02/22] Change SimplifiedExpression to SimplifiedPredicate --- .../rj_language/ast/Expression.java | 5 - .../rj_language/ast/SimplifiedExpression.java | 124 ------------------ .../ast/formatter/ExpressionFormatter.java | 10 +- .../ast/formatter/ExpressionPrecedence.java | 3 - .../rj_language/ast/typing/TypeInfer.java | 4 - .../visitors/ExpressionVisitor.java | 3 - .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 - 7 files changed, 1 insertion(+), 154 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 20c9fe84e..ee638262e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -82,9 +82,6 @@ public boolean isLiteral() { * @return true if it is a boolean expression, false otherwise */ public boolean isBooleanExpression() { - if (this instanceof SimplifiedExpression node) { - return node.getSimplifiedExpression().isBooleanExpression(); - } if (this instanceof LiteralBoolean || this instanceof Ite || this instanceof AliasInvocation || this instanceof FunctionInvocation) { return true; @@ -102,8 +99,6 @@ public boolean isBooleanExpression() { } public List getConjuncts() { - if (this instanceof SimplifiedExpression node) - return node.getSimplifiedExpression().getConjuncts(); if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) { List conjuncts = new ArrayList<>(); conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java deleted file mode 100644 index e06bbc2dc..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java +++ /dev/null @@ -1,124 +0,0 @@ -package liquidjava.rj_language.ast; - -import java.util.ArrayList; -import java.util.List; -import java.util.Objects; - -import liquidjava.diagnostics.errors.LJError; -import liquidjava.rj_language.visitors.ExpressionVisitor; -import spoon.reflect.reference.CtTypeReference; - -public class SimplifiedExpression extends Expression { - - private final Expression origin; - private final List binders; - - public SimplifiedExpression(Expression simplified, Expression origin) { - this(simplified, origin, List.of()); - } - - public SimplifiedExpression(Expression simplified, Expression origin, List binders) { - addChild(simplified); - this.origin = origin; - this.binders = new ArrayList<>(binders); - } - - public Expression getSimplifiedExpression() { - return children.get(0); - } - - public Expression getOrigin() { - return origin; - } - - public List getBinders() { - return binders; - } - - @Override - public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitSimplifiedNode(this); - } - - @Override - public void getVariableNames(List toAdd) { - getSimplifiedExpression().getVariableNames(toAdd); - } - - @Override - public void getStateInvocations(List toAdd, List all) { - getSimplifiedExpression().getStateInvocations(toAdd, all); - } - - @Override - public boolean isBooleanTrue() { - return getSimplifiedExpression().isBooleanTrue(); - } - - @Override - public Expression clone() { - return new SimplifiedExpression(getSimplifiedExpression().clone(), origin.clone(), binders); - } - - @Override - public String toString() { - return getSimplifiedExpression().toString(); - } - - @Override - public int hashCode() { - return Objects.hash(getSimplifiedExpression(), origin, binders); - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - SimplifiedExpression other = (SimplifiedExpression) obj; - return getSimplifiedExpression().equals(other.getSimplifiedExpression()) && origin.equals(other.origin) - && binders.equals(other.binders); - } - - public static class Binder { - private final String name; - private final String type; - - public Binder(String name, String type) { - this.name = name; - this.type = type; - } - - public Binder(String name, CtTypeReference type) { - this(name, type.getQualifiedName()); - } - - public String getName() { - return name; - } - - public String getType() { - return type; - } - - @Override - public int hashCode() { - return Objects.hash(name, type); - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - Binder other = (Binder) obj; - return name.equals(other.name) && type.equals(other.type); - } - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 34d71a1d2..2135f41d4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -17,7 +17,6 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.Enum; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -62,11 +61,9 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression || expression instanceof SimplifiedExpression) { + while (expression instanceof GroupExpression) { if (expression instanceof GroupExpression group) expression = group.getExpression(); - else if (expression instanceof SimplifiedExpression node) - expression = node.getSimplifiedExpression(); } return expression; } @@ -166,11 +163,6 @@ public String visitLiteralString(LiteralString lit) { return lit.toString(); } - @Override - public String visitSimplifiedNode(SimplifiedExpression node) { - return formatExpression(node.getSimplifiedExpression()); - } - @Override public String visitUnaryExpression(UnaryExpression exp) { return exp.getOp() + formatOperand(exp, exp.getExpression(), true); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java index ce9678c52..fbaa95cbe 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java @@ -4,7 +4,6 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; public enum ExpressionPrecedence { @@ -17,8 +16,6 @@ public boolean isLowerThan(ExpressionPrecedence other) { public static ExpressionPrecedence of(Expression expression) { if (expression instanceof GroupExpression group) return of(group.getExpression()); - if (expression instanceof SimplifiedExpression node) - return of(node.getSimplifiedExpression()); if (expression instanceof Ite) return TERNARY; if (expression instanceof UnaryExpression) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 140c7ed88..59cd6a0f2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -15,7 +15,6 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; @@ -58,9 +57,6 @@ else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); - else if (e instanceof SimplifiedExpression) - return getType(ctx, factory, ((SimplifiedExpression) e).getSimplifiedExpression()); - return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java index cd2e9e384..24d030fc9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -13,7 +13,6 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; @@ -40,8 +39,6 @@ public interface ExpressionVisitor { T visitLiteralString(LiteralString lit) throws LJError; - T visitSimplifiedNode(SimplifiedExpression node) throws LJError; - T visitUnaryExpression(UnaryExpression exp) throws LJError; T visitEnum(Enum en) throws LJError; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index edf4ba9be..464cd9898 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -15,7 +15,6 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.visitors.ExpressionVisitor; @@ -114,11 +113,6 @@ public Expr visitLiteralString(LiteralString lit) { return ctx.makeString(lit.toString()); } - @Override - public Expr visitSimplifiedNode(SimplifiedExpression node) throws LJError { - return node.getSimplifiedExpression().accept(this); - } - @Override public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { return switch (exp.getOp()) { From abc5a0219408bc3eff8a506f6467a87a8a1818d4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 13:48:42 +0100 Subject: [PATCH 03/22] Requested Changes --- .../rj_language/ast/formatter/ExpressionFormatter.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 2135f41d4..b26026f6c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -61,9 +61,8 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression) { - if (expression instanceof GroupExpression group) - expression = group.getExpression(); + while (expression instanceof GroupExpression group) { + expression = group.getExpression(); } return expression; } From 3c358a9dc1c9ecd3afa24922ee185bb24c48cf7d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:08:10 +0100 Subject: [PATCH 04/22] Formatting --- .../rj_language/ast/formatter/ExpressionFormatter.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index b26026f6c..cf6e4fdce 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -61,9 +61,8 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression group) { + while (expression instanceof GroupExpression group) expression = group.getExpression(); - } return expression; } From 8229c6077d5fbb24d189ac5785aa9fe064161098 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:44:29 +0100 Subject: [PATCH 05/22] Minor Changes --- .../main/java/liquidjava/rj_language/ast/typing/TypeInfer.java | 1 + .../java/liquidjava/rj_language/visitors/ExpressionVisitor.java | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 59cd6a0f2..0fa965cde 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -57,6 +57,7 @@ else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); + return Optional.empty(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java index 24d030fc9..904690a79 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -44,4 +44,4 @@ public interface ExpressionVisitor { T visitEnum(Enum en) throws LJError; T visitVar(Var var) throws LJError; -} +} \ No newline at end of file From a61f0f70bdc5ebefd822fe160a0f8eaeb070ac5d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 16:51:53 +0100 Subject: [PATCH 06/22] Add VC Substitution --- .../liquidjava/processor/VCImplication.java | 8 + .../rj_language/SimplifiedPredicate.java | 5 + .../rj_language/opt/VCSimplifier.java | 10 + .../rj_language/opt/VCSubstitution.java | 183 ++++++++++++++++++ .../rj_language/opt/VCSubstitutionTest.java | 100 ++++++++++ .../java/liquidjava/utils/VCTestUtils.java | 129 ++++++++++++ 6 files changed, 435 insertions(+) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index a5b44f1d0..e8cfa3ca7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -47,6 +47,14 @@ public VCImplication getNext() { return next; } + public boolean hasNext() { + return next != null; + } + + public boolean hasBinder() { + return name != null && type != null; + } + public String toString() { if (name != null && type != null) { String qualType = type.getQualifiedName(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index bf86d4c20..dcc10d34f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -88,6 +88,11 @@ public String getType() { return type; } + @Override + public String toString() { + return name + ":" + type; + } + @Override public int hashCode() { return Objects.hash(name, type); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java new file mode 100644 index 000000000..ef501bf39 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java @@ -0,0 +1,10 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.VCImplication; + +public class VCSimplifier { + + public static VCImplication simplifyOnce(VCImplication implication) { + return VCSubstitution.apply(implication); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java new file mode 100644 index 000000000..7d6d74916 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -0,0 +1,183 @@ +package liquidjava.rj_language.opt; + +import java.util.ArrayList; +import java.util.List; +import java.util.Optional; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.SimplifiedExpression; +import liquidjava.rj_language.ast.Var; + +/** + * Simplifies VCImplication chains by replacing binder equalities with their known values + */ +public class VCSubstitution { + + /** + * A substitution discovered from an implication node + */ + private record Substitution(VCImplication source, Expression value) { + } + + /** + * Applies all available binder equality substitutions in a VC chain + */ + public static VCImplication apply(VCImplication implication) { + if (implication == null) + return null; + + VCImplication result = implication.clone(); + Optional substitutionOpt = VCSubstitution.findSubstitution(result); + + // keep applying substitutions until there are no more substitutions available + while (substitutionOpt.isPresent()) { + VCSubstitution.Substitution substitution = substitutionOpt.get(); + result = VCSubstitution.substitute(result, substitution.source(), substitution.value()); + substitutionOpt = VCSubstitution.findSubstitution(result); + } + return result; + } + + /** + * Applies one substitution in a VC chain + */ + public static VCImplication applyOnce(VCImplication implication) { + if (implication == null) + return null; + + VCImplication result = implication.clone(); + Optional substitutionOpt = VCSubstitution.findSubstitution(result); + + // apply only the first available substitution + if (substitutionOpt.isPresent()) { + VCSubstitution.Substitution substitution = substitutionOpt.get(); + result = VCSubstitution.substitute(result, substitution.source(), substitution.value()); + } + return result; + } + + /** + * Rewrites one VC chain with a single substitution and removes its source node + */ + private static VCImplication substitute(VCImplication implication, VCImplication source, Expression value) { + if (implication == null) + return null; + + // skip the source node to remove it from the chain and start substitution from the next node + if (implication == source) + return substitute(implication.getNext(), source, value); + + Predicate refinement = substituteRefinement(implication.getRefinement(), source, value); + VCImplication result = copyWithRefinement(implication, refinement); + result.setNext(substitute(implication.getNext(), source, value)); + return result; + } + + /** + * Substitutes a source binder inside one predicate while preserving simplification metadata + */ + private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { + Expression expression = refinement.getExpression(); + Expression active = activeExpression(expression); + SimplifiedExpression.Binder binder = new SimplifiedExpression.Binder(source.getName(), source.getType()); + Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); + + return new Predicate(new SimplifiedExpression(substituted, originExpression(expression), + bindersAfterSubstitution(expression, active, binder))); + } + + /** + * Copies an implication node with a replacement refinement + */ + private static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { + if (implication.hasBinder()) + return new VCImplication(implication.getName(), implication.getType(), refinement); + return new VCImplication(refinement); + } + + /** + * Returns the expression that should be shown as the original formula + */ + private static Expression originExpression(Expression expression) { + if (expression instanceof SimplifiedExpression simplified) + return simplified.getOrigin().clone(); + return expression.clone(); + } + + /** + * Builds the binder metadata after one substitution + */ + private static List bindersAfterSubstitution(Expression expression, Expression active, + SimplifiedExpression.Binder binder) { + List binders = expression instanceof SimplifiedExpression previous + ? new ArrayList<>(previous.getBinders()) : new ArrayList<>(); + if (containsVariable(active, binder.getName()) && !binders.contains(binder)) + binders.add(binder); + return binders; + } + + /** + * Finds the first substitution candidate in the VC chain + */ + private static Optional findSubstitution(VCImplication implication) { + if (implication == null) + return Optional.empty(); + + Optional current = getSubstitution(implication); + if (current.isPresent()) + return current; + + return findSubstitution(implication.getNext()); + } + + /** + * Extracts a substitution from one binder equality + */ + private static Optional getSubstitution(VCImplication implication) { + if (!implication.hasBinder()) + return Optional.empty(); + + Expression refinement = activeExpression(implication.getRefinement().getExpression()); + if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) + return Optional.empty(); + + String name = implication.getName(); + Expression left = binary.getFirstOperand(); + Expression right = binary.getSecondOperand(); + + if (isVar(left, name) && !containsVariable(right, name)) + return Optional.of(new Substitution(implication, right.clone())); + if (isVar(right, name) && !containsVariable(left, name)) + return Optional.of(new Substitution(implication, left.clone())); + + return Optional.empty(); + } + + /** + * Checks whether an expression is a variable with a given name + */ + private static boolean isVar(Expression expression, String name) { + return expression instanceof Var var && name.equals(var.getName()); + } + + /** + * Checks whether an expression contains a variable name + */ + private static boolean containsVariable(Expression expression, String name) { + List names = new ArrayList<>(); + expression.getVariableNames(names); + return names.contains(name); + } + + /** + * Returns the expression used for matching and substitution + */ + private static Expression activeExpression(Expression expression) { + if (expression instanceof SimplifiedExpression simplified) + return simplified.getSimplifiedExpression().clone(); + return expression.clone(); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java new file mode 100644 index 000000000..a62b7810b --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -0,0 +1,100 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertNotSame; +import static org.junit.jupiter.api.Assertions.assertNull; + +import liquidjava.processor.VCImplication; +import org.junit.jupiter.api.Test; + +class VCSubstitutionTest { + + @Test + void applyReturnsNullForNullImplication() { + assertNull(VCSubstitution.apply(null)); + } + + @Test + void substitutesBinderEqualityIntoWholeChain() { + VCImplication implication = vc("∀x:int. x == 3", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); + } + + @Test + void substitutesReverseBinderEquality() { + VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); + } + + @Test + void substitutesCompoundKnownValue() { + VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int")); + } + + @Test + void usesFirstSubstitutionFoundInChain() { + VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int")); + } + + @Test + void substitutesInnerKnownValueAcrossNestedImplications() { + VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"), + simplified("1 + z > 0", "y + z > 0", "y:int")); + } + + @Test + void substitutesOuterKnownValueIntoNestedBinderRefinements() { + VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("3 + 1 > 3", "y > x", "x:int, y:int")); + } + + @Test + void ignoresRecursiveBinderEquality() { + VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertNotSame(implication, result); + assertVC(result, "x == x + 1", "x > 0"); + } + + @Test + void ignoresNonEqualityBinderRefinement() { + VCImplication implication = vc("∀x:int. x > 3", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertNotSame(implication, result); + assertVC(result, "x > 3", "x > 0"); + } + + @Test + void ignoresEqualityWithoutBinder() { + VCImplication implication = vc("x == 3", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertVC(result, "x == 3", "x > 0"); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java new file mode 100644 index 000000000..334712fae --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -0,0 +1,129 @@ +package liquidjava.utils; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; +import static org.junit.jupiter.api.Assertions.assertNull; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.SimplifiedExpression; +import liquidjava.rj_language.parsing.RefinementsParser; +import spoon.Launcher; +import spoon.reflect.reference.CtTypeReference; + +public class VCTestUtils { + + private static final CtTypeReference INT = new Launcher().getFactory().Type().INTEGER_PRIMITIVE; + + public static Expression parse(String refinement) { + return RefinementsParser.createAST(refinement, ""); + } + + public static VCImplication vc(String... implications) { + VCImplication first = null; + VCImplication last = null; + for (String implication : implications) { + VCImplication node = parseImplication(implication); + if (first == null) + first = node; + if (last != null) + last.setNext(node); + last = node; + } + return first; + } + + private static VCImplication parseImplication(String implication) { + if (!implication.startsWith("∀")) + return new VCImplication(new Predicate(parse(implication))); + + int refinementStart = implication.indexOf('.'); + String binder = implication.substring(1, refinementStart).trim(); + String refinement = implication.substring(refinementStart + 1).trim(); + String[] parts = binder.split(":"); + return new VCImplication(parts[0].trim(), type(parts[1].trim()), new Predicate(parse(refinement))); + } + + private static CtTypeReference type(String name) { + if ("int".equals(name)) + return INT; + throw new IllegalArgumentException("Unsupported test type: " + name); + } + + public static void assertSimplifiedVC(VCImplication implication, String... expected) { + ExpectedSimplifiedExpression[] expressions = java.util.Arrays.stream(expected) + .map(VCTestUtils::parseExpectedSimplifiedExpression).toArray(ExpectedSimplifiedExpression[]::new); + assertSimplifiedVC(implication, expressions); + } + + public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedExpression... expected) { + VCImplication current = implication; + for (int i = 0; i < expected.length; i++) { + ExpectedSimplifiedExpression expectedExpression = expected[i]; + SimplifiedExpression expression = simplifiedExpression(current, i); + assertEquals(expectedExpression.simplified(), expression.getSimplifiedExpression().toString(), + "Unexpected simplified expression at implication " + i); + if (expectedExpression.origin() != null) + assertEquals(expectedExpression.origin(), expression.getOrigin().toString(), + "Unexpected origin expression at implication " + i); + if (expectedExpression.binders() != null) + assertEquals(expectedExpression.binders(), formatBinders(expression), + "Unexpected binders at implication " + i); + current = current.getNext(); + } + assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); + } + + public static ExpectedSimplifiedExpression simplified(String simplified) { + return new ExpectedSimplifiedExpression(simplified, null, null); + } + + public static ExpectedSimplifiedExpression simplified(String simplified, String origin) { + return new ExpectedSimplifiedExpression(simplified, origin, null); + } + + public static ExpectedSimplifiedExpression simplified(String simplified, String origin, String binders) { + return new ExpectedSimplifiedExpression(simplified, origin, binders); + } + + public static void assertVC(VCImplication implication, String... expected) { + VCImplication current = implication; + for (int i = 0; i < expected.length; i++) { + assertEquals(expected[i], current.getRefinement().getExpression().toString(), + "Unexpected expression at implication " + i); + current = current.getNext(); + } + assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); + } + + public static SimplifiedExpression simplifiedExpression(VCImplication implication, int index) { + assertInstanceOf(SimplifiedExpression.class, implication.getRefinement().getExpression(), + "Expected implication " + index + " to contain a SimplifiedExpression"); + return (SimplifiedExpression) implication.getRefinement().getExpression(); + } + + private static String formatBinders(SimplifiedExpression expression) { + return expression.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType()) + .collect(java.util.stream.Collectors.joining(", ")); + } + + private static ExpectedSimplifiedExpression parseExpectedSimplifiedExpression(String expected) { + String binders = null; + String expression = expected.trim(); + int binderStart = expression.lastIndexOf('['); + if (binderStart >= 0) { + int binderEnd = expression.lastIndexOf(']'); + binders = expression.substring(binderStart + 1, binderEnd).trim(); + expression = expression.substring(0, binderStart).trim(); + } + + String[] parts = expression.split("<-", 2); + String simplified = parts[0].trim(); + String origin = parts.length > 1 ? parts[1].trim() : null; + return new ExpectedSimplifiedExpression(simplified, origin, binders); + } + + public record ExpectedSimplifiedExpression(String simplified, String origin, String binders) { + } +} From 176f337f6cac9bbe112a8d9ee4f2d01bc89eb261 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 17:12:50 +0100 Subject: [PATCH 07/22] Add Comments --- .../main/java/liquidjava/rj_language/opt/VCSimplifier.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java index ef501bf39..a970174e1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java @@ -4,7 +4,11 @@ public class VCSimplifier { - public static VCImplication simplifyOnce(VCImplication implication) { + /** + * Applies all available simplification steps to a VC chain + */ + public static VCImplication simplify(VCImplication implication) { + // TODO: implement remaining simplification steps return VCSubstitution.apply(implication); } } From 03f1d8831d8ced74cc33c0d4077f67cc3cbb93b3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:32:56 +0100 Subject: [PATCH 08/22] SimplifiedPredicate Follow-Up --- .../rj_language/opt/VCSubstitution.java | 33 ++++++------ .../java/liquidjava/utils/VCTestUtils.java | 54 +++++++++---------- 2 files changed, 43 insertions(+), 44 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 7d6d74916..5e0a3dd99 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -6,9 +6,9 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.SimplifiedPredicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.ast.Var; /** @@ -80,13 +80,12 @@ private static VCImplication substitute(VCImplication implication, VCImplication * Substitutes a source binder inside one predicate while preserving simplification metadata */ private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { - Expression expression = refinement.getExpression(); - Expression active = activeExpression(expression); - SimplifiedExpression.Binder binder = new SimplifiedExpression.Binder(source.getName(), source.getType()); + Expression active = activeExpression(refinement); + SimplifiedPredicate.Binder binder = new SimplifiedPredicate.Binder(source.getName(), source.getType()); Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); - return new Predicate(new SimplifiedExpression(substituted, originExpression(expression), - bindersAfterSubstitution(expression, active, binder))); + return new SimplifiedPredicate(new Predicate(substituted), originPredicate(refinement), + bindersAfterSubstitution(refinement, active, binder)); } /** @@ -101,18 +100,18 @@ private static VCImplication copyWithRefinement(VCImplication implication, Predi /** * Returns the expression that should be shown as the original formula */ - private static Expression originExpression(Expression expression) { - if (expression instanceof SimplifiedExpression simplified) + private static Predicate originPredicate(Predicate refinement) { + if (refinement instanceof SimplifiedPredicate simplified) return simplified.getOrigin().clone(); - return expression.clone(); + return refinement.clone(); } /** * Builds the binder metadata after one substitution */ - private static List bindersAfterSubstitution(Expression expression, Expression active, - SimplifiedExpression.Binder binder) { - List binders = expression instanceof SimplifiedExpression previous + private static List bindersAfterSubstitution(Predicate refinement, Expression active, + SimplifiedPredicate.Binder binder) { + List binders = refinement instanceof SimplifiedPredicate previous ? new ArrayList<>(previous.getBinders()) : new ArrayList<>(); if (containsVariable(active, binder.getName()) && !binders.contains(binder)) binders.add(binder); @@ -140,7 +139,7 @@ private static Optional getSubstitution(VCImplication implication) if (!implication.hasBinder()) return Optional.empty(); - Expression refinement = activeExpression(implication.getRefinement().getExpression()); + Expression refinement = activeExpression(implication.getRefinement()); if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) return Optional.empty(); @@ -175,9 +174,9 @@ private static boolean containsVariable(Expression expression, String name) { /** * Returns the expression used for matching and substitution */ - private static Expression activeExpression(Expression expression) { - if (expression instanceof SimplifiedExpression simplified) - return simplified.getSimplifiedExpression().clone(); - return expression.clone(); + private static Expression activeExpression(Predicate refinement) { + if (refinement instanceof SimplifiedPredicate simplified) + return simplified.getSimplifiedPredicate().getExpression().clone(); + return refinement.getExpression().clone(); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 334712fae..c526d132d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -6,8 +6,8 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.SimplifiedPredicate; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.SimplifiedExpression; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; import spoon.reflect.reference.CtTypeReference; @@ -52,39 +52,39 @@ private static CtTypeReference type(String name) { } public static void assertSimplifiedVC(VCImplication implication, String... expected) { - ExpectedSimplifiedExpression[] expressions = java.util.Arrays.stream(expected) - .map(VCTestUtils::parseExpectedSimplifiedExpression).toArray(ExpectedSimplifiedExpression[]::new); - assertSimplifiedVC(implication, expressions); + ExpectedSimplifiedPredicate[] predicates = java.util.Arrays.stream(expected) + .map(VCTestUtils::parseExpectedSimplifiedPredicate).toArray(ExpectedSimplifiedPredicate[]::new); + assertSimplifiedVC(implication, predicates); } - public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedExpression... expected) { + public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedPredicate... expected) { VCImplication current = implication; for (int i = 0; i < expected.length; i++) { - ExpectedSimplifiedExpression expectedExpression = expected[i]; - SimplifiedExpression expression = simplifiedExpression(current, i); - assertEquals(expectedExpression.simplified(), expression.getSimplifiedExpression().toString(), + ExpectedSimplifiedPredicate expectedPredicate = expected[i]; + SimplifiedPredicate predicate = simplifiedPredicate(current, i); + assertEquals(expectedPredicate.simplified(), predicate.getSimplifiedPredicate().toString(), "Unexpected simplified expression at implication " + i); - if (expectedExpression.origin() != null) - assertEquals(expectedExpression.origin(), expression.getOrigin().toString(), + if (expectedPredicate.origin() != null) + assertEquals(expectedPredicate.origin(), predicate.getOrigin().toString(), "Unexpected origin expression at implication " + i); - if (expectedExpression.binders() != null) - assertEquals(expectedExpression.binders(), formatBinders(expression), + if (expectedPredicate.binders() != null) + assertEquals(expectedPredicate.binders(), formatBinders(predicate), "Unexpected binders at implication " + i); current = current.getNext(); } assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); } - public static ExpectedSimplifiedExpression simplified(String simplified) { - return new ExpectedSimplifiedExpression(simplified, null, null); + public static ExpectedSimplifiedPredicate simplified(String simplified) { + return new ExpectedSimplifiedPredicate(simplified, null, null); } - public static ExpectedSimplifiedExpression simplified(String simplified, String origin) { - return new ExpectedSimplifiedExpression(simplified, origin, null); + public static ExpectedSimplifiedPredicate simplified(String simplified, String origin) { + return new ExpectedSimplifiedPredicate(simplified, origin, null); } - public static ExpectedSimplifiedExpression simplified(String simplified, String origin, String binders) { - return new ExpectedSimplifiedExpression(simplified, origin, binders); + public static ExpectedSimplifiedPredicate simplified(String simplified, String origin, String binders) { + return new ExpectedSimplifiedPredicate(simplified, origin, binders); } public static void assertVC(VCImplication implication, String... expected) { @@ -97,18 +97,18 @@ public static void assertVC(VCImplication implication, String... expected) { assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); } - public static SimplifiedExpression simplifiedExpression(VCImplication implication, int index) { - assertInstanceOf(SimplifiedExpression.class, implication.getRefinement().getExpression(), - "Expected implication " + index + " to contain a SimplifiedExpression"); - return (SimplifiedExpression) implication.getRefinement().getExpression(); + public static SimplifiedPredicate simplifiedPredicate(VCImplication implication, int index) { + assertInstanceOf(SimplifiedPredicate.class, implication.getRefinement(), + "Expected implication " + index + " to contain a SimplifiedPredicate"); + return (SimplifiedPredicate) implication.getRefinement(); } - private static String formatBinders(SimplifiedExpression expression) { - return expression.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType()) + private static String formatBinders(SimplifiedPredicate predicate) { + return predicate.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType()) .collect(java.util.stream.Collectors.joining(", ")); } - private static ExpectedSimplifiedExpression parseExpectedSimplifiedExpression(String expected) { + private static ExpectedSimplifiedPredicate parseExpectedSimplifiedPredicate(String expected) { String binders = null; String expression = expected.trim(); int binderStart = expression.lastIndexOf('['); @@ -121,9 +121,9 @@ private static ExpectedSimplifiedExpression parseExpectedSimplifiedExpression(St String[] parts = expression.split("<-", 2); String simplified = parts[0].trim(); String origin = parts.length > 1 ? parts[1].trim() : null; - return new ExpectedSimplifiedExpression(simplified, origin, binders); + return new ExpectedSimplifiedPredicate(simplified, origin, binders); } - public record ExpectedSimplifiedExpression(String simplified, String origin, String binders) { + public record ExpectedSimplifiedPredicate(String simplified, String origin, String binders) { } } From 3fc150d9b7ca7b6030b15fbf957c53951747980a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:34:59 +0100 Subject: [PATCH 09/22] Add `simplifyOnce` --- .../java/liquidjava/rj_language/opt/VCSimplifier.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java index a970174e1..84be7a270 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java @@ -11,4 +11,12 @@ public static VCImplication simplify(VCImplication implication) { // TODO: implement remaining simplification steps return VCSubstitution.apply(implication); } + + /** + * Applies one simplification step to a VC chain + */ + public static VCImplication simplifyOnce(VCImplication implication) { + // TODO: implement remaining simplification steps + return VCSubstitution.applyOnce(implication); + } } From da87af947f9966e09de5f02d42ee702485b794f8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:39:47 +0100 Subject: [PATCH 10/22] Add Property Based Test using JUnit Quickcheck --- liquidjava-verifier/pom.xml | 32 +++-- .../opt/VCImplicationGenerator.java | 89 ++++++++++++ .../VCSimplificationPropertyBasedTest.java | 127 ++++++++++++++++++ 3 files changed, 238 insertions(+), 10 deletions(-) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index a463457cc..4967db246 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -301,16 +301,28 @@ junit-vintage-engine test - - org.junit.jupiter - junit-jupiter-params - test - - - ch.qos.logback - logback-classic - 1.4.12 - + + org.junit.jupiter + junit-jupiter-params + test + + + com.pholser + junit-quickcheck-core + 1.0 + test + + + com.pholser + junit-quickcheck-generators + 1.0 + test + + + ch.qos.logback + logback-classic + 1.4.12 + org.mdkt.compiler InMemoryJavaCompiler diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java new file mode 100644 index 000000000..c39e9dc6d --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java @@ -0,0 +1,89 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.vc; + +import com.pholser.junit.quickcheck.generator.GenerationStatus; +import com.pholser.junit.quickcheck.generator.Generator; +import com.pholser.junit.quickcheck.random.SourceOfRandomness; +import liquidjava.processor.VCImplication; + +public class VCImplicationGenerator extends Generator { + + static final String[] BINDERS = { "x", "y", "z" }; + static final String[] FREE_VARS = { "a", "b", "c" }; + private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" }; + + public VCImplicationGenerator() { + super(VCImplication.class); + } + + @Override + public VCImplication generate(SourceOfRandomness random, GenerationStatus status) { + return switch (random.nextInt(0, 5)) { + case 0 -> vc(substitution(random, "x"), comparison(random, "x")); + case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x")); + case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y")); + case 3 -> vc(substitution(random, "x"), dependentSubstitution(random), comparison(random, "y")); + case 4 -> vc("∀y:int. true", "∀x:int. x == y + 1", comparison(random, "x")); + default -> vc(substitution(random, "x"), substitution(random, "y"), comparison(random, "z")); + }; + } + + private static String substitution(SourceOfRandomness random, String binder) { + String value = value(random); + if (random.nextBoolean()) + return "∀" + binder + ":int. " + binder + " == " + value; + return "∀" + binder + ":int. " + value + " == " + binder; + } + + private static String reverseSubstitution(SourceOfRandomness random, String binder) { + return "∀" + binder + ":int. " + value(random) + " == " + binder; + } + + private static String dependentSubstitution(SourceOfRandomness random) { + int offset = random.nextInt(-3, 3); + return "∀y:int. y == x " + signed(offset); + } + + private static String nonSubstitution(SourceOfRandomness random, String binder) { + if (random.nextBoolean()) + return "∀" + binder + ":int. " + binder + " > " + intLiteral(random); + return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5)); + } + + private static String comparison(SourceOfRandomness random, String preferredVar) { + String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar); + String right = random.nextBoolean() ? intLiteral(random) + : arithmetic(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]); + return left + " " + COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)] + " " + right; + } + + private static String value(SourceOfRandomness random) { + String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]; + return switch (random.nextInt(0, 3)) { + case 0 -> intLiteral(random); + case 1 -> var; + case 2 -> var + " " + signed(random.nextInt(-4, 4)); + default -> arithmetic(random, var); + }; + } + + private static String arithmetic(SourceOfRandomness random, String var) { + int constant = random.nextInt(-3, 3); + return switch (random.nextInt(0, 2)) { + case 0 -> var + " " + signed(constant); + case 1 -> var + " * " + random.nextInt(1, 5); + default -> "(" + var + " " + signed(constant) + ")"; + }; + } + + private static String signed(int value) { + if (value < 0) + return "- " + Math.abs(value); + return "+ " + value; + } + + private static String intLiteral(SourceOfRandomness random) { + return Integer.toString(random.nextInt(-7, 7)); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java new file mode 100644 index 000000000..7ead2d20f --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -0,0 +1,127 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.vc; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import com.pholser.junit.quickcheck.From; +import com.pholser.junit.quickcheck.Property; +import com.pholser.junit.quickcheck.runner.JUnitQuickcheck; +import java.util.ArrayList; +import java.util.List; +import liquidjava.processor.VCImplication; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.SimplifiedPredicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; +import liquidjava.smt.SMTEvaluator; +import liquidjava.smt.SMTResult; +import liquidjava.utils.TestUtils; +import org.junit.runner.RunWith; + +@RunWith(JUnitQuickcheck.class) +public class VCSimplificationPropertyBasedTest { + + private static final int TRIALS = 800; + + @Property(trials = TRIALS) + public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) { + setUpContext(); + VCImplication current = vc; + + for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) { + VCImplication simplified = VCSimplifier.simplifyOnce(current); + if (sameVc(current, simplified)) + break; + + assertEquivalent(current, simplified, step); + current = simplified; + } + System.out.println("---------------------------------------------------------"); + } + + private static void setUpContext() { + Context.getInstance().reinitializeAllContext(); + for (String variable : VCImplicationGenerator.BINDERS) + TestUtils.addIntVariableToContext(variable); + for (String variable : VCImplicationGenerator.FREE_VARS) + TestUtils.addIntVariableToContext(variable); + } + + private static boolean sameVc(VCImplication left, VCImplication right) { + return left.toString().equals(right.toString()); + } + + private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) { + Predicate premises = substitutionPremises(unsimplified); + Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified))); + Predicate simplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(simplified))); + System.out.println(unsimplifiedFormula); + System.out.println("=>"); + System.out.println(simplifiedFormula); + assertImplies(unsimplifiedFormula, simplifiedFormula, unsimplified, simplified, step, + "unsimplified => simplified"); + assertImplies(simplifiedFormula, unsimplifiedFormula, unsimplified, simplified, step, + "simplified => unsimplified"); + } + + private static Expression vcFormula(VCImplication implication) { + Expression refinement = activeExpression(implication.getRefinement()).clone(); + if (!implication.hasNext()) + return refinement; + return new BinaryExpression(refinement, "-->", vcFormula(implication.getNext())); + } + + private static Predicate substitutionPremises(VCImplication implication) { + Predicate premises = new Predicate(); + for (VCImplication current = implication; current != null; current = current.getNext()) { + if (isSubstitution(current)) + premises = Predicate.createConjunction(premises, current.getRefinement()); + } + return premises; + } + + private static boolean isSubstitution(VCImplication implication) { + if (!implication.hasBinder()) + return false; + + Expression refinement = activeExpression(implication.getRefinement()); + if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) + return false; + + String name = implication.getName(); + Expression left = binary.getFirstOperand(); + Expression right = binary.getSecondOperand(); + return isVar(left, name) && !containsVariable(right, name) + || isVar(right, name) && !containsVariable(left, name); + } + + private static void assertImplies(Predicate antecedent, Predicate consequent, VCImplication unsimplified, + VCImplication simplified, int step, String direction) { + try { + SMTResult result = new SMTEvaluator().verifySubtype(antecedent, consequent, Context.getInstance(), true); + assertTrue(result.isOk(), () -> direction + " failed at step " + step + "\nunsimplified: " + unsimplified + + "\nsimplified: " + simplified); + } catch (Exception e) { + throw new AssertionError(direction + " could not be checked at step " + step + "\nunsimplified: " + + unsimplified + "\nsimplified: " + simplified, e); + } + } + + private static boolean isVar(Expression expression, String name) { + return expression instanceof Var var && name.equals(var.getName()); + } + + private static boolean containsVariable(Expression expression, String name) { + List names = new ArrayList<>(); + expression.getVariableNames(names); + return names.contains(name); + } + + private static Expression activeExpression(Predicate predicate) { + if (predicate instanceof SimplifiedPredicate simplified) + return simplified.getSimplifiedPredicate().getExpression(); + return predicate.getExpression(); + } +} From 39be6f6b8147ad6ecc87dd9cf812231fa08fdb73 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:43:22 +0100 Subject: [PATCH 11/22] Minor Changes --- .../opt/VCSimplificationPropertyBasedTest.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 7ead2d20f..7c1ac027d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -23,7 +23,7 @@ @RunWith(JUnitQuickcheck.class) public class VCSimplificationPropertyBasedTest { - private static final int TRIALS = 800; + private static final int TRIALS = 500; @Property(trials = TRIALS) public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) { @@ -38,7 +38,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera assertEquivalent(current, simplified, step); current = simplified; } - System.out.println("---------------------------------------------------------"); + // System.out.println("---------------------------------------------------------"); } private static void setUpContext() { @@ -57,9 +57,9 @@ private static void assertEquivalent(VCImplication unsimplified, VCImplication s Predicate premises = substitutionPremises(unsimplified); Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified))); Predicate simplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(simplified))); - System.out.println(unsimplifiedFormula); - System.out.println("=>"); - System.out.println(simplifiedFormula); + // System.out.println(unsimplifiedFormula); + // System.out.println("=>"); + // System.out.println(simplifiedFormula); assertImplies(unsimplifiedFormula, simplifiedFormula, unsimplified, simplified, step, "unsimplified => simplified"); assertImplies(simplifiedFormula, unsimplifiedFormula, unsimplified, simplified, step, From 8adba6804ab02f3597378acfa0974a6d9162928f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:34:51 +0100 Subject: [PATCH 12/22] Code Refactoring --- .../rj_language/opt/VCSubstitution.java | 11 +++++---- .../VCSimplificationPropertyBasedTest.java | 24 +++---------------- 2 files changed, 9 insertions(+), 26 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 5e0a3dd99..fb152da68 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -7,6 +7,7 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.SimplifiedPredicate; +import liquidjava.rj_language.SimplifiedPredicate.Binder; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; @@ -81,7 +82,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication */ private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { Expression active = activeExpression(refinement); - SimplifiedPredicate.Binder binder = new SimplifiedPredicate.Binder(source.getName(), source.getType()); + Binder binder = new Binder(source.getName(), source.getType()); Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); return new SimplifiedPredicate(new Predicate(substituted), originPredicate(refinement), @@ -109,7 +110,7 @@ private static Predicate originPredicate(Predicate refinement) { /** * Builds the binder metadata after one substitution */ - private static List bindersAfterSubstitution(Predicate refinement, Expression active, + private static List bindersAfterSubstitution(Predicate refinement, Expression active, SimplifiedPredicate.Binder binder) { List binders = refinement instanceof SimplifiedPredicate previous ? new ArrayList<>(previous.getBinders()) : new ArrayList<>(); @@ -158,14 +159,14 @@ private static Optional getSubstitution(VCImplication implication) /** * Checks whether an expression is a variable with a given name */ - private static boolean isVar(Expression expression, String name) { + public static boolean isVar(Expression expression, String name) { return expression instanceof Var var && name.equals(var.getName()); } /** * Checks whether an expression contains a variable name */ - private static boolean containsVariable(Expression expression, String name) { + public static boolean containsVariable(Expression expression, String name) { List names = new ArrayList<>(); expression.getVariableNames(names); return names.contains(name); @@ -174,7 +175,7 @@ private static boolean containsVariable(Expression expression, String name) { /** * Returns the expression used for matching and substitution */ - private static Expression activeExpression(Predicate refinement) { + public static Expression activeExpression(Predicate refinement) { if (refinement instanceof SimplifiedPredicate simplified) return simplified.getSimplifiedPredicate().getExpression().clone(); return refinement.getExpression().clone(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 7c1ac027d..b1d58a668 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -1,20 +1,18 @@ package liquidjava.rj_language.opt; -import static liquidjava.utils.VCTestUtils.vc; +import static liquidjava.rj_language.opt.VCSubstitution.activeExpression; +import static liquidjava.rj_language.opt.VCSubstitution.containsVariable; +import static liquidjava.rj_language.opt.VCSubstitution.isVar; import static org.junit.jupiter.api.Assertions.assertTrue; import com.pholser.junit.quickcheck.From; import com.pholser.junit.quickcheck.Property; import com.pholser.junit.quickcheck.runner.JUnitQuickcheck; -import java.util.ArrayList; -import java.util.List; import liquidjava.processor.VCImplication; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.SimplifiedPredicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.Var; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; import liquidjava.utils.TestUtils; @@ -108,20 +106,4 @@ private static void assertImplies(Predicate antecedent, Predicate consequent, VC + unsimplified + "\nsimplified: " + simplified, e); } } - - private static boolean isVar(Expression expression, String name) { - return expression instanceof Var var && name.equals(var.getName()); - } - - private static boolean containsVariable(Expression expression, String name) { - List names = new ArrayList<>(); - expression.getVariableNames(names); - return names.contains(name); - } - - private static Expression activeExpression(Predicate predicate) { - if (predicate instanceof SimplifiedPredicate simplified) - return simplified.getSimplifiedPredicate().getExpression(); - return predicate.getExpression(); - } } From d55680dcd1f8c803d2bdedb4a37785133dab0c86 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:42:41 +0100 Subject: [PATCH 13/22] Add Comment --- .../src/main/java/liquidjava/rj_language/opt/VCSimplifier.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java index 84be7a270..082d48df2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java @@ -2,6 +2,9 @@ import liquidjava.processor.VCImplication; +/** + * Simplifies VCImplication chains by applying various simplification steps + */ public class VCSimplifier { /** From 6e4e1cd994df13eb2311ee83ef0620a9c5da194d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 16:00:05 +0100 Subject: [PATCH 14/22] Code Refactoring --- .../opt/VCSimplificationUtils.java | 46 +++++++++++++++++++ .../rj_language/opt/VCSimplifier.java | 10 +--- .../rj_language/opt/VCSubstitution.java | 45 ++---------------- .../VCSimplificationPropertyBasedTest.java | 2 +- .../rj_language/opt/VCSubstitutionTest.java | 25 +++++----- 5 files changed, 64 insertions(+), 64 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java new file mode 100644 index 000000000..e5ce9fa74 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java @@ -0,0 +1,46 @@ +package liquidjava.rj_language.opt; + +import java.util.ArrayList; +import java.util.List; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.SimplifiedPredicate; +import liquidjava.rj_language.SimplifiedPredicate.Binder; +import liquidjava.rj_language.ast.Expression; + +class VCSimplificationUtils { + + private VCSimplificationUtils() { + } + + static Expression activeExpression(Predicate refinement) { + if (refinement instanceof SimplifiedPredicate simplified) + return simplified.getSimplifiedPredicate().getExpression().clone(); + return refinement.getExpression().clone(); + } + + static Predicate originPredicate(Predicate refinement) { + if (refinement instanceof SimplifiedPredicate simplified) + return simplified.getOrigin().clone(); + return refinement.clone(); + } + + static List binders(Predicate refinement) { + if (refinement instanceof SimplifiedPredicate simplified) + return new ArrayList<>(simplified.getBinders()); + return new ArrayList<>(); + } + + static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { + if (implication.hasBinder()) + return new VCImplication(implication.getName(), implication.getType(), refinement); + return new VCImplication(refinement); + } + + static boolean sameVc(VCImplication left, VCImplication right) { + if (left == null || right == null) + return left == right; + return left.toString().equals(right.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java index 082d48df2..9beb9571c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java @@ -11,15 +11,7 @@ public class VCSimplifier { * Applies all available simplification steps to a VC chain */ public static VCImplication simplify(VCImplication implication) { - // TODO: implement remaining simplification steps - return VCSubstitution.apply(implication); - } - - /** - * Applies one simplification step to a VC chain - */ - public static VCImplication simplifyOnce(VCImplication implication) { - // TODO: implement remaining simplification steps + // TODO: implement remaining simplification steps with fixed point iteration return VCSubstitution.applyOnce(implication); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index fb152da68..2888b3d2e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -23,25 +23,6 @@ public class VCSubstitution { private record Substitution(VCImplication source, Expression value) { } - /** - * Applies all available binder equality substitutions in a VC chain - */ - public static VCImplication apply(VCImplication implication) { - if (implication == null) - return null; - - VCImplication result = implication.clone(); - Optional substitutionOpt = VCSubstitution.findSubstitution(result); - - // keep applying substitutions until there are no more substitutions available - while (substitutionOpt.isPresent()) { - VCSubstitution.Substitution substitution = substitutionOpt.get(); - result = VCSubstitution.substitute(result, substitution.source(), substitution.value()); - substitutionOpt = VCSubstitution.findSubstitution(result); - } - return result; - } - /** * Applies one substitution in a VC chain */ @@ -72,7 +53,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication return substitute(implication.getNext(), source, value); Predicate refinement = substituteRefinement(implication.getRefinement(), source, value); - VCImplication result = copyWithRefinement(implication, refinement); + VCImplication result = VCSimplificationUtils.copyWithRefinement(implication, refinement); result.setNext(substitute(implication.getNext(), source, value)); return result; } @@ -85,28 +66,10 @@ private static Predicate substituteRefinement(Predicate refinement, VCImplicatio Binder binder = new Binder(source.getName(), source.getType()); Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); - return new SimplifiedPredicate(new Predicate(substituted), originPredicate(refinement), + return new SimplifiedPredicate(new Predicate(substituted), VCSimplificationUtils.originPredicate(refinement), bindersAfterSubstitution(refinement, active, binder)); } - /** - * Copies an implication node with a replacement refinement - */ - private static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { - if (implication.hasBinder()) - return new VCImplication(implication.getName(), implication.getType(), refinement); - return new VCImplication(refinement); - } - - /** - * Returns the expression that should be shown as the original formula - */ - private static Predicate originPredicate(Predicate refinement) { - if (refinement instanceof SimplifiedPredicate simplified) - return simplified.getOrigin().clone(); - return refinement.clone(); - } - /** * Builds the binder metadata after one substitution */ @@ -176,8 +139,6 @@ public static boolean containsVariable(Expression expression, String name) { * Returns the expression used for matching and substitution */ public static Expression activeExpression(Predicate refinement) { - if (refinement instanceof SimplifiedPredicate simplified) - return simplified.getSimplifiedPredicate().getExpression().clone(); - return refinement.getExpression().clone(); + return VCSimplificationUtils.activeExpression(refinement); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index b1d58a668..0de7572d4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -29,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera VCImplication current = vc; for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) { - VCImplication simplified = VCSimplifier.simplifyOnce(current); + VCImplication simplified = VCSimplifier.simplify(current); if (sameVc(current, simplified)) break; diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index a62b7810b..938dc0f63 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -10,15 +10,15 @@ class VCSubstitutionTest { @Test - void applyReturnsNullForNullImplication() { - assertNull(VCSubstitution.apply(null)); + void applyOnceReturnsNullForNullImplication() { + assertNull(VCSubstitution.applyOnce(null)); } @Test void substitutesBinderEqualityIntoWholeChain() { VCImplication implication = vc("∀x:int. x == 3", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); } @@ -27,7 +27,7 @@ void substitutesBinderEqualityIntoWholeChain() { void substitutesReverseBinderEquality() { VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); } @@ -36,7 +36,7 @@ void substitutesReverseBinderEquality() { void substitutesCompoundKnownValue() { VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int")); } @@ -45,7 +45,7 @@ void substitutesCompoundKnownValue() { void usesFirstSubstitutionFoundInChain() { VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int")); } @@ -54,7 +54,7 @@ void usesFirstSubstitutionFoundInChain() { void substitutesInnerKnownValueAcrossNestedImplications() { VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"), simplified("1 + z > 0", "y + z > 0", "y:int")); @@ -64,16 +64,17 @@ void substitutesInnerKnownValueAcrossNestedImplications() { void substitutesOuterKnownValueIntoNestedBinderRefinements() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("3 + 1 > 3", "y > x", "x:int, y:int")); + assertSimplifiedVC(result, simplified("y == 3 + 1", "y == x + 1", "x:int"), + simplified("y > 3", "y > x", "x:int")); } @Test void ignoresRecursiveBinderEquality() { VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertNotSame(implication, result); assertVC(result, "x == x + 1", "x > 0"); @@ -83,7 +84,7 @@ void ignoresRecursiveBinderEquality() { void ignoresNonEqualityBinderRefinement() { VCImplication implication = vc("∀x:int. x > 3", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertNotSame(implication, result); assertVC(result, "x > 3", "x > 0"); @@ -93,7 +94,7 @@ void ignoresNonEqualityBinderRefinement() { void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0"); - VCImplication result = VCSubstitution.apply(implication); + VCImplication result = VCSubstitution.applyOnce(implication); assertVC(result, "x == 3", "x > 0"); } From 39e54c465ddcd089746646814f5f653afcd96827 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 16:14:11 +0100 Subject: [PATCH 15/22] Add Fixed Point Iteration --- .../rj_language/opt/VCSimplification.java | 44 +++++++++++++++++++ .../opt/VCSimplificationUtils.java | 17 ++----- .../rj_language/opt/VCSimplifier.java | 17 ------- .../rj_language/opt/VCSubstitution.java | 9 +--- .../VCSimplificationPropertyBasedTest.java | 8 +--- 5 files changed, 52 insertions(+), 43 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java new file mode 100644 index 000000000..9b579ff7d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -0,0 +1,44 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.VCImplication; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.*; + +/** + * Simplifies VCImplication chains by applying various simplification steps + */ +public class VCSimplification { + + /** + * Applies all available simplification steps to a VC chain + */ + public static VCImplication simplify(VCImplication implication) { + if (implication == null) + return null; + + // keep applying simplification steps until a fixed point is reached + VCImplication current = implication.clone(); + while (true) { + VCImplication simplified = simplifyOnce(current); + if (sameVc(current, simplified)) // fixed point reached + return simplified; + current = simplified; + } + } + + /** + * Applies one simplification step to a VC chain + */ + public static VCImplication simplifyOnce(VCImplication implication) { + if (implication == null) + return null; + + // first try to apply substitution, then folding + VCImplication substituted = VCSubstitution.applyOnce(implication); + if (!sameVc(implication, substituted)) + return substituted; + + // TODO: add more simplification steps here (e.g., folding) + return substituted; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java index e5ce9fa74..ee79633a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java @@ -11,34 +11,25 @@ class VCSimplificationUtils { - private VCSimplificationUtils() { - } - - static Expression activeExpression(Predicate refinement) { + public static Expression activeExpression(Predicate refinement) { if (refinement instanceof SimplifiedPredicate simplified) return simplified.getSimplifiedPredicate().getExpression().clone(); return refinement.getExpression().clone(); } - static Predicate originPredicate(Predicate refinement) { + public static Predicate originPredicate(Predicate refinement) { if (refinement instanceof SimplifiedPredicate simplified) return simplified.getOrigin().clone(); return refinement.clone(); } - static List binders(Predicate refinement) { - if (refinement instanceof SimplifiedPredicate simplified) - return new ArrayList<>(simplified.getBinders()); - return new ArrayList<>(); - } - - static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { + public static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { if (implication.hasBinder()) return new VCImplication(implication.getName(), implication.getType(), refinement); return new VCImplication(refinement); } - static boolean sameVc(VCImplication left, VCImplication right) { + public static boolean sameVc(VCImplication left, VCImplication right) { if (left == null || right == null) return left == right; return left.toString().equals(right.toString()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java deleted file mode 100644 index 9beb9571c..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplifier.java +++ /dev/null @@ -1,17 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.processor.VCImplication; - -/** - * Simplifies VCImplication chains by applying various simplification steps - */ -public class VCSimplifier { - - /** - * Applies all available simplification steps to a VC chain - */ - public static VCImplication simplify(VCImplication implication) { - // TODO: implement remaining simplification steps with fixed point iteration - return VCSubstitution.applyOnce(implication); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 2888b3d2e..a42c36a5f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -12,6 +12,8 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; +import static liquidjava.rj_language.opt.VCSimplificationUtils.*; + /** * Simplifies VCImplication chains by replacing binder equalities with their known values */ @@ -134,11 +136,4 @@ public static boolean containsVariable(Expression expression, String name) { expression.getVariableNames(names); return names.contains(name); } - - /** - * Returns the expression used for matching and substitution - */ - public static Expression activeExpression(Predicate refinement) { - return VCSimplificationUtils.activeExpression(refinement); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 0de7572d4..1eb08dab7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -1,6 +1,6 @@ package liquidjava.rj_language.opt; -import static liquidjava.rj_language.opt.VCSubstitution.activeExpression; +import static liquidjava.rj_language.opt.VCSimplificationUtils.*; import static liquidjava.rj_language.opt.VCSubstitution.containsVariable; import static liquidjava.rj_language.opt.VCSubstitution.isVar; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -29,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera VCImplication current = vc; for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) { - VCImplication simplified = VCSimplifier.simplify(current); + VCImplication simplified = VCSimplification.simplify(current); if (sameVc(current, simplified)) break; @@ -47,10 +47,6 @@ private static void setUpContext() { TestUtils.addIntVariableToContext(variable); } - private static boolean sameVc(VCImplication left, VCImplication right) { - return left.toString().equals(right.toString()); - } - private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) { Predicate premises = substitutionPremises(unsimplified); Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified))); From 92f3d127d136f1de1aaa8e26384ed325946e6f86 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 16:57:05 +0100 Subject: [PATCH 16/22] Requested Changes --- .../liquidjava/processor/VCImplication.java | 30 +++++++++++++++ .../liquidjava/rj_language/Predicate.java | 9 +++++ .../rj_language/SimplifiedPredicate.java | 1 + .../rj_language/opt/VCSimplification.java | 6 +-- .../opt/VCSimplificationUtils.java | 37 ------------------- .../rj_language/opt/VCSubstitution.java | 10 ++--- .../VCSimplificationPropertyBasedTest.java | 7 ++-- 7 files changed, 49 insertions(+), 51 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index e8cfa3ca7..bbc276966 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -1,5 +1,7 @@ package liquidjava.processor; +import java.util.Objects; + import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; import spoon.reflect.reference.CtTypeReference; @@ -23,6 +25,12 @@ public VCImplication(Predicate ref) { this.refinement = ref; } + public VCImplication(VCImplication implication, Predicate ref) { + this.name = implication.name; + this.type = implication.type; + this.refinement = ref; + } + public void setNext(VCImplication c) { next = c; } @@ -87,4 +95,26 @@ public VCImplication clone() { vc.next = this.next.clone(); return vc; } + + @Override + public int hashCode() { + return Objects.hash(name, typeName(), refinement, next); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + VCImplication other = (VCImplication) obj; + return Objects.equals(name, other.name) && Objects.equals(typeName(), other.typeName()) + && Objects.equals(refinement, other.refinement) && Objects.equals(next, other.next); + } + + private String typeName() { + return type == null ? null : type.getQualifiedName(); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 64da35b2e..e6a4f04fb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -235,6 +235,11 @@ public Predicate clone() { return new Predicate(exp.clone()); } + @Override + public int hashCode() { + return exp.hashCode(); + } + @Override public boolean equals(Object obj) { if (this == obj) @@ -251,6 +256,10 @@ public Expression getExpression() { return exp; } + public Predicate getOrigin() { + return this; + } + public ValDerivationNode simplify(Context context) { // collect aliases from context Map aliases = new HashMap<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index dcc10d34f..b8148731d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -33,6 +33,7 @@ public Predicate getSimplifiedPredicate() { return new Predicate(getExpression()); } + @Override public Predicate getOrigin() { return origin; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 9b579ff7d..2d8009556 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -2,8 +2,6 @@ import liquidjava.processor.VCImplication; -import static liquidjava.rj_language.opt.VCSimplificationUtils.*; - /** * Simplifies VCImplication chains by applying various simplification steps */ @@ -20,7 +18,7 @@ public static VCImplication simplify(VCImplication implication) { VCImplication current = implication.clone(); while (true) { VCImplication simplified = simplifyOnce(current); - if (sameVc(current, simplified)) // fixed point reached + if (current.equals(simplified)) // fixed point reached return simplified; current = simplified; } @@ -35,7 +33,7 @@ public static VCImplication simplifyOnce(VCImplication implication) { // first try to apply substitution, then folding VCImplication substituted = VCSubstitution.applyOnce(implication); - if (!sameVc(implication, substituted)) + if (!implication.equals(substituted)) return substituted; // TODO: add more simplification steps here (e.g., folding) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java deleted file mode 100644 index ee79633a2..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java +++ /dev/null @@ -1,37 +0,0 @@ -package liquidjava.rj_language.opt; - -import java.util.ArrayList; -import java.util.List; - -import liquidjava.processor.VCImplication; -import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.SimplifiedPredicate; -import liquidjava.rj_language.SimplifiedPredicate.Binder; -import liquidjava.rj_language.ast.Expression; - -class VCSimplificationUtils { - - public static Expression activeExpression(Predicate refinement) { - if (refinement instanceof SimplifiedPredicate simplified) - return simplified.getSimplifiedPredicate().getExpression().clone(); - return refinement.getExpression().clone(); - } - - public static Predicate originPredicate(Predicate refinement) { - if (refinement instanceof SimplifiedPredicate simplified) - return simplified.getOrigin().clone(); - return refinement.clone(); - } - - public static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { - if (implication.hasBinder()) - return new VCImplication(implication.getName(), implication.getType(), refinement); - return new VCImplication(refinement); - } - - public static boolean sameVc(VCImplication left, VCImplication right) { - if (left == null || right == null) - return left == right; - return left.toString().equals(right.toString()); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index a42c36a5f..dbc3e2be1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -12,8 +12,6 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; -import static liquidjava.rj_language.opt.VCSimplificationUtils.*; - /** * Simplifies VCImplication chains by replacing binder equalities with their known values */ @@ -55,7 +53,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication return substitute(implication.getNext(), source, value); Predicate refinement = substituteRefinement(implication.getRefinement(), source, value); - VCImplication result = VCSimplificationUtils.copyWithRefinement(implication, refinement); + VCImplication result = new VCImplication(implication, refinement); result.setNext(substitute(implication.getNext(), source, value)); return result; } @@ -64,11 +62,11 @@ private static VCImplication substitute(VCImplication implication, VCImplication * Substitutes a source binder inside one predicate while preserving simplification metadata */ private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { - Expression active = activeExpression(refinement); + Expression active = refinement.getExpression().clone(); Binder binder = new Binder(source.getName(), source.getType()); Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); - return new SimplifiedPredicate(new Predicate(substituted), VCSimplificationUtils.originPredicate(refinement), + return new SimplifiedPredicate(new Predicate(substituted), refinement.getOrigin().clone(), bindersAfterSubstitution(refinement, active, binder)); } @@ -105,7 +103,7 @@ private static Optional getSubstitution(VCImplication implication) if (!implication.hasBinder()) return Optional.empty(); - Expression refinement = activeExpression(implication.getRefinement()); + Expression refinement = implication.getRefinement().getExpression().clone(); if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) return Optional.empty(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 1eb08dab7..57f373d6b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -1,6 +1,5 @@ package liquidjava.rj_language.opt; -import static liquidjava.rj_language.opt.VCSimplificationUtils.*; import static liquidjava.rj_language.opt.VCSubstitution.containsVariable; import static liquidjava.rj_language.opt.VCSubstitution.isVar; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -30,7 +29,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) { VCImplication simplified = VCSimplification.simplify(current); - if (sameVc(current, simplified)) + if (current.equals(simplified)) break; assertEquivalent(current, simplified, step); @@ -61,7 +60,7 @@ private static void assertEquivalent(VCImplication unsimplified, VCImplication s } private static Expression vcFormula(VCImplication implication) { - Expression refinement = activeExpression(implication.getRefinement()).clone(); + Expression refinement = implication.getRefinement().getExpression().clone(); if (!implication.hasNext()) return refinement; return new BinaryExpression(refinement, "-->", vcFormula(implication.getNext())); @@ -80,7 +79,7 @@ private static boolean isSubstitution(VCImplication implication) { if (!implication.hasBinder()) return false; - Expression refinement = activeExpression(implication.getRefinement()); + Expression refinement = implication.getRefinement().getExpression().clone(); if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) return false; From c42edc8a24944a4a7b1c6a67e5fb56fb55eaf658 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 17:19:22 +0100 Subject: [PATCH 17/22] Rename --- .../liquidjava/rj_language/opt/VCSubstitution.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index dbc3e2be1..97100a87c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -62,22 +62,22 @@ private static VCImplication substitute(VCImplication implication, VCImplication * Substitutes a source binder inside one predicate while preserving simplification metadata */ private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { - Expression active = refinement.getExpression().clone(); + Expression exp = refinement.getExpression().clone(); Binder binder = new Binder(source.getName(), source.getType()); - Expression substituted = active.substitute(new Var(binder.getName()), value.clone()); + Expression substituted = exp.substitute(new Var(binder.getName()), value.clone()); return new SimplifiedPredicate(new Predicate(substituted), refinement.getOrigin().clone(), - bindersAfterSubstitution(refinement, active, binder)); + bindersAfterSubstitution(refinement, exp, binder)); } /** * Builds the binder metadata after one substitution */ - private static List bindersAfterSubstitution(Predicate refinement, Expression active, + private static List bindersAfterSubstitution(Predicate refinement, Expression exp, SimplifiedPredicate.Binder binder) { List binders = refinement instanceof SimplifiedPredicate previous ? new ArrayList<>(previous.getBinders()) : new ArrayList<>(); - if (containsVariable(active, binder.getName()) && !binders.contains(binder)) + if (containsVariable(exp, binder.getName()) && !binders.contains(binder)) binders.add(binder); return binders; } From 9c54833ba61891bd86d931281a0777b28c99bfc7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 18:59:01 +0100 Subject: [PATCH 18/22] Replace `SimplifiedPredicate` with `SimplifiedVCImplication` --- .../processor/SimplifiedVCImplication.java | 52 ++++++++ .../liquidjava/processor/VCImplication.java | 4 + .../rj_language/SimplifiedPredicate.java | 114 ------------------ .../rj_language/opt/VCSubstitution.java | 54 ++++----- .../rj_language/opt/VCSubstitutionTest.java | 21 ++-- .../java/liquidjava/utils/VCTestUtils.java | 63 ++++------ 6 files changed, 119 insertions(+), 189 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java new file mode 100644 index 000000000..804f0b2b8 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java @@ -0,0 +1,52 @@ +package liquidjava.processor; + +import java.util.Objects; + +import liquidjava.rj_language.Predicate; + +/** + * Represents a VC implication node whose refinement was simplified from another quantified VC shape. + */ +public class SimplifiedVCImplication extends VCImplication { + + private final VCImplication origin; + + public SimplifiedVCImplication(VCImplication implication, Predicate refinement, VCImplication origin) { + super(implication, refinement); + this.origin = origin.clone(); + } + + public VCImplication getOrigin() { + return origin; + } + + @Override + public VCImplication copyWithRefinement(Predicate refinement) { + return new SimplifiedVCImplication(this, refinement, origin); + } + + @Override + public SimplifiedVCImplication clone() { + SimplifiedVCImplication vc = new SimplifiedVCImplication(this, this.refinement.clone(), origin); + if (this.next != null) + vc.next = this.next.clone(); + return vc; + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), origin); + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (!(obj instanceof SimplifiedVCImplication)) + return false; + if (!super.equals(obj)) + return false; + SimplifiedVCImplication other = (SimplifiedVCImplication) obj; + return origin.equals(other.origin); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index bbc276966..125d1632c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -31,6 +31,10 @@ public VCImplication(VCImplication implication, Predicate ref) { this.refinement = ref; } + public VCImplication copyWithRefinement(Predicate refinement) { + return new VCImplication(this, refinement); + } + public void setNext(VCImplication c) { next = c; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java deleted file mode 100644 index b8148731d..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ /dev/null @@ -1,114 +0,0 @@ -package liquidjava.rj_language; - -import java.util.ArrayList; -import java.util.List; -import java.util.Objects; - -import spoon.reflect.reference.CtTypeReference; - -/** - * Represents a predicate simplified from another predicate. Stores the original predicate and any variables that must - * be reintroduced as binders when relating the simplified predicate back to its origin. - *

- * For example, simplifying {@code x == 1 && y > x} with binders {@code x: int, y: int} may produce {@code y > 1}. The - * origin {@code x == 1 && y > x} and binder {@code x: int} are kept so we can relate the simplified predicate back to - * the original. - */ -public class SimplifiedPredicate extends Predicate { - - private final Predicate origin; - private final List binders; - - public SimplifiedPredicate(Predicate simplified, Predicate origin) { - this(simplified, origin, List.of()); - } - - public SimplifiedPredicate(Predicate simplified, Predicate origin, List binders) { - super(simplified.getExpression()); - this.origin = origin; - this.binders = new ArrayList<>(binders); - } - - public Predicate getSimplifiedPredicate() { - return new Predicate(getExpression()); - } - - @Override - public Predicate getOrigin() { - return origin; - } - - public List getBinders() { - return binders; - } - - @Override - public SimplifiedPredicate clone() { - return new SimplifiedPredicate(new Predicate(getExpression().clone()), origin.clone(), binders); - } - - @Override - public int hashCode() { - return Objects.hash(getExpression(), origin, binders); - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - SimplifiedPredicate other = (SimplifiedPredicate) obj; - return getExpression().equals(other.getExpression()) && origin.equals(other.origin) - && binders.equals(other.binders); - } - - /** - * Represents a variable that must be bound when relating the simplified predicate to its origin - */ - public static class Binder { - private final String name; - private final String type; - - public Binder(String name, String type) { - this.name = name; - this.type = type; - } - - public Binder(String name, CtTypeReference type) { - this(name, type.getQualifiedName()); - } - - public String getName() { - return name; - } - - public String getType() { - return type; - } - - @Override - public String toString() { - return name + ":" + type; - } - - @Override - public int hashCode() { - return Objects.hash(name, type); - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - Binder other = (Binder) obj; - return name.equals(other.name) && type.equals(other.type); - } - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 97100a87c..022a81c32 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -4,10 +4,9 @@ import java.util.List; import java.util.Optional; +import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.SimplifiedPredicate; -import liquidjava.rj_language.SimplifiedPredicate.Binder; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; @@ -20,7 +19,7 @@ public class VCSubstitution { /** * A substitution discovered from an implication node */ - private record Substitution(VCImplication source, Expression value) { + private record Substitution(VCImplication node, Expression replacement) { } /** @@ -36,7 +35,7 @@ public static VCImplication applyOnce(VCImplication implication) { // apply only the first available substitution if (substitutionOpt.isPresent()) { VCSubstitution.Substitution substitution = substitutionOpt.get(); - result = VCSubstitution.substitute(result, substitution.source(), substitution.value()); + result = VCSubstitution.substitute(result, substitution.node(), substitution.replacement()); } return result; } @@ -44,42 +43,39 @@ public static VCImplication applyOnce(VCImplication implication) { /** * Rewrites one VC chain with a single substitution and removes its source node */ - private static VCImplication substitute(VCImplication implication, VCImplication source, Expression value) { + private static VCImplication substitute(VCImplication implication, VCImplication node, Expression replacement) { if (implication == null) return null; // skip the source node to remove it from the chain and start substitution from the next node - if (implication == source) - return substitute(implication.getNext(), source, value); + if (implication == node) + return substitute(implication.getNext(), node, replacement); - Predicate refinement = substituteRefinement(implication.getRefinement(), source, value); - VCImplication result = new VCImplication(implication, refinement); - result.setNext(substitute(implication.getNext(), source, value)); + VCImplication result = substituteNode(implication, node, replacement); + result.setNext(substitute(implication.getNext(), node, replacement)); return result; } /** - * Substitutes a source binder inside one predicate while preserving simplification metadata + * Substitutes a source binder inside one VC node while preserving simplification metadata */ - private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) { - Expression exp = refinement.getExpression().clone(); - Binder binder = new Binder(source.getName(), source.getType()); - Expression substituted = exp.substitute(new Var(binder.getName()), value.clone()); - - return new SimplifiedPredicate(new Predicate(substituted), refinement.getOrigin().clone(), - bindersAfterSubstitution(refinement, exp, binder)); + private static VCImplication substituteNode(VCImplication implication, VCImplication node, Expression replacement) { + Expression exp = implication.getRefinement().getExpression().clone(); + if (!containsVar(exp, node.getName())) + return implication.copyWithRefinement(new Predicate(exp)); + + Expression substituted = exp.substitute(new Var(node.getName()), replacement.clone()); + VCImplication origin = new VCImplication(node.getName(), node.getType(), origin(implication)); + return new SimplifiedVCImplication(implication, new Predicate(substituted), origin); } /** - * Builds the binder metadata after one substitution + * Uses the earliest original predicate available when simplifying an already-simplified node */ - private static List bindersAfterSubstitution(Predicate refinement, Expression exp, - SimplifiedPredicate.Binder binder) { - List binders = refinement instanceof SimplifiedPredicate previous - ? new ArrayList<>(previous.getBinders()) : new ArrayList<>(); - if (containsVariable(exp, binder.getName()) && !binders.contains(binder)) - binders.add(binder); - return binders; + private static Predicate origin(VCImplication implication) { + if (implication instanceof SimplifiedVCImplication simplified) + return simplified.getOrigin().getRefinement().clone(); + return implication.getRefinement().clone(); } /** @@ -111,9 +107,9 @@ private static Optional getSubstitution(VCImplication implication) Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); - if (isVar(left, name) && !containsVariable(right, name)) + if (isVar(left, name) && !containsVar(right, name)) return Optional.of(new Substitution(implication, right.clone())); - if (isVar(right, name) && !containsVariable(left, name)) + if (isVar(right, name) && !containsVar(left, name)) return Optional.of(new Substitution(implication, left.clone())); return Optional.empty(); @@ -129,7 +125,7 @@ public static boolean isVar(Expression expression, String name) { /** * Checks whether an expression contains a variable name */ - public static boolean containsVariable(Expression expression, String name) { + public static boolean containsVar(Expression expression, String name) { List names = new ArrayList<>(); expression.getVariableNames(names); return names.contains(name); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index 938dc0f63..a19dd374d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -1,6 +1,7 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotSame; import static org.junit.jupiter.api.Assertions.assertNull; @@ -20,7 +21,7 @@ void substitutesBinderEqualityIntoWholeChain() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); + assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0")); } @Test @@ -29,7 +30,7 @@ void substitutesReverseBinderEquality() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int")); + assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0")); } @Test @@ -38,7 +39,7 @@ void substitutesCompoundKnownValue() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int")); + assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y")); } @Test @@ -47,7 +48,9 @@ void usesFirstSubstitutionFoundInChain() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int")); + assertVC(result, "x > 0", "x + 4 > 0"); + assertEquals(VCImplication.class, result.getClass()); + assertSimplifiedVC(result.getNext(), simplified("x + 4 > 0", "∀y:int. x + y > 0")); } @Test @@ -56,8 +59,10 @@ void substitutesInnerKnownValueAcrossNestedImplications() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"), - simplified("1 + z > 0", "y + z > 0", "y:int")); + assertVC(result, "true", "z > 1", "1 + z > 0"); + assertEquals(VCImplication.class, result.getClass()); + assertSimplifiedVC(result.getNext(), simplified("z > 1", "∀y:int. z > y"), + simplified("1 + z > 0", "∀y:int. y + z > 0")); } @Test @@ -66,8 +71,8 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() { VCImplication result = VCSubstitution.applyOnce(implication); - assertSimplifiedVC(result, simplified("y == 3 + 1", "y == x + 1", "x:int"), - simplified("y > 3", "y > x", "x:int")); + assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"), + simplified("y > 3", "∀x:int. y > x")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index c526d132d..046e4f9b7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -4,9 +4,9 @@ import static org.junit.jupiter.api.Assertions.assertInstanceOf; import static org.junit.jupiter.api.Assertions.assertNull; +import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.SimplifiedPredicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; @@ -52,39 +52,34 @@ private static CtTypeReference type(String name) { } public static void assertSimplifiedVC(VCImplication implication, String... expected) { - ExpectedSimplifiedPredicate[] predicates = java.util.Arrays.stream(expected) - .map(VCTestUtils::parseExpectedSimplifiedPredicate).toArray(ExpectedSimplifiedPredicate[]::new); + ExpectedSimplifiedVCImplication[] predicates = java.util.Arrays.stream(expected) + .map(VCTestUtils::parseExpectedSimplifiedVCImplication).toArray(ExpectedSimplifiedVCImplication[]::new); assertSimplifiedVC(implication, predicates); } - public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedPredicate... expected) { + public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedVCImplication... expected) { VCImplication current = implication; for (int i = 0; i < expected.length; i++) { - ExpectedSimplifiedPredicate expectedPredicate = expected[i]; - SimplifiedPredicate predicate = simplifiedPredicate(current, i); - assertEquals(expectedPredicate.simplified(), predicate.getSimplifiedPredicate().toString(), + ExpectedSimplifiedVCImplication expectedPredicate = expected[i]; + SimplifiedVCImplication simplified = simplifiedImplication(current, i); + assertEquals(Predicate.class, simplified.getRefinement().getClass(), + "Expected simplified refinement at implication " + i + " to be a plain Predicate"); + assertEquals(expectedPredicate.simplified(), simplified.getRefinement().toString(), "Unexpected simplified expression at implication " + i); if (expectedPredicate.origin() != null) - assertEquals(expectedPredicate.origin(), predicate.getOrigin().toString(), - "Unexpected origin expression at implication " + i); - if (expectedPredicate.binders() != null) - assertEquals(expectedPredicate.binders(), formatBinders(predicate), - "Unexpected binders at implication " + i); + assertEquals(expectedPredicate.origin(), formatOrigin(simplified.getOrigin()), + "Unexpected origin VC at implication " + i); current = current.getNext(); } assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); } - public static ExpectedSimplifiedPredicate simplified(String simplified) { - return new ExpectedSimplifiedPredicate(simplified, null, null); + public static ExpectedSimplifiedVCImplication simplified(String simplified) { + return new ExpectedSimplifiedVCImplication(simplified, null); } - public static ExpectedSimplifiedPredicate simplified(String simplified, String origin) { - return new ExpectedSimplifiedPredicate(simplified, origin, null); - } - - public static ExpectedSimplifiedPredicate simplified(String simplified, String origin, String binders) { - return new ExpectedSimplifiedPredicate(simplified, origin, binders); + public static ExpectedSimplifiedVCImplication simplified(String simplified, String origin) { + return new ExpectedSimplifiedVCImplication(simplified, origin); } public static void assertVC(VCImplication implication, String... expected) { @@ -97,33 +92,25 @@ public static void assertVC(VCImplication implication, String... expected) { assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); } - public static SimplifiedPredicate simplifiedPredicate(VCImplication implication, int index) { - assertInstanceOf(SimplifiedPredicate.class, implication.getRefinement(), - "Expected implication " + index + " to contain a SimplifiedPredicate"); - return (SimplifiedPredicate) implication.getRefinement(); + public static SimplifiedVCImplication simplifiedImplication(VCImplication implication, int index) { + return assertInstanceOf(SimplifiedVCImplication.class, implication, + "Expected implication " + index + " to be a SimplifiedVCImplication"); } - private static String formatBinders(SimplifiedPredicate predicate) { - return predicate.getBinders().stream().map(binder -> binder.getName() + ":" + binder.getType()) - .collect(java.util.stream.Collectors.joining(", ")); + private static String formatOrigin(VCImplication origin) { + if (!origin.hasBinder()) + return origin.getRefinement().toString(); + return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + origin.getRefinement(); } - private static ExpectedSimplifiedPredicate parseExpectedSimplifiedPredicate(String expected) { - String binders = null; + private static ExpectedSimplifiedVCImplication parseExpectedSimplifiedVCImplication(String expected) { String expression = expected.trim(); - int binderStart = expression.lastIndexOf('['); - if (binderStart >= 0) { - int binderEnd = expression.lastIndexOf(']'); - binders = expression.substring(binderStart + 1, binderEnd).trim(); - expression = expression.substring(0, binderStart).trim(); - } - String[] parts = expression.split("<-", 2); String simplified = parts[0].trim(); String origin = parts.length > 1 ? parts[1].trim() : null; - return new ExpectedSimplifiedPredicate(simplified, origin, binders); + return new ExpectedSimplifiedVCImplication(simplified, origin); } - public record ExpectedSimplifiedPredicate(String simplified, String origin, String binders) { + public record ExpectedSimplifiedVCImplication(String simplified, String origin) { } } From e486e28daa388176cf38c110d1381e9e9954ca8d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 19:01:11 +0100 Subject: [PATCH 19/22] Fix --- .../rj_language/opt/VCSimplificationPropertyBasedTest.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 57f373d6b..3dc9d9eac 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -1,6 +1,6 @@ package liquidjava.rj_language.opt; -import static liquidjava.rj_language.opt.VCSubstitution.containsVariable; +import static liquidjava.rj_language.opt.VCSubstitution.containsVar; import static liquidjava.rj_language.opt.VCSubstitution.isVar; import static org.junit.jupiter.api.Assertions.assertTrue; @@ -86,8 +86,7 @@ private static boolean isSubstitution(VCImplication implication) { String name = implication.getName(); Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); - return isVar(left, name) && !containsVariable(right, name) - || isVar(right, name) && !containsVariable(left, name); + return isVar(left, name) && !containsVar(right, name) || isVar(right, name) && !containsVar(left, name); } private static void assertImplies(Predicate antecedent, Predicate consequent, VCImplication unsimplified, From a487ea9d51a873e2910d313ea723811217139f7c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 21:34:34 +0100 Subject: [PATCH 20/22] Refactoring --- .../processor/SimplifiedVCImplication.java | 5 +++++ .../liquidjava/processor/VCImplication.java | 4 ++++ .../rj_language/opt/VCSimplification.java | 4 ++-- .../rj_language/opt/VCSubstitution.java | 13 ++---------- .../VCSimplificationPropertyBasedTest.java | 2 +- .../rj_language/opt/VCSubstitutionTest.java | 20 +++++++++---------- 6 files changed, 24 insertions(+), 24 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java index 804f0b2b8..ffa8ebfd3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java @@ -20,6 +20,11 @@ public VCImplication getOrigin() { return origin; } + @Override + public Predicate getOriginRefinement() { + return origin.getRefinement().clone(); + } + @Override public VCImplication copyWithRefinement(Predicate refinement) { return new SimplifiedVCImplication(this, refinement, origin); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 125d1632c..1af4429ca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -31,6 +31,10 @@ public VCImplication(VCImplication implication, Predicate ref) { this.refinement = ref; } + public Predicate getOriginRefinement() { + return refinement.clone(); + } + public VCImplication copyWithRefinement(Predicate refinement) { return new VCImplication(this, refinement); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 2d8009556..1c2f3fd64 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -10,7 +10,7 @@ public class VCSimplification { /** * Applies all available simplification steps to a VC chain */ - public static VCImplication simplify(VCImplication implication) { + public static VCImplication simplifyToFixedPoint(VCImplication implication) { if (implication == null) return null; @@ -32,7 +32,7 @@ public static VCImplication simplifyOnce(VCImplication implication) { return null; // first try to apply substitution, then folding - VCImplication substituted = VCSubstitution.applyOnce(implication); + VCImplication substituted = VCSubstitution.apply(implication); if (!implication.equals(substituted)) return substituted; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 022a81c32..37dd16bf9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -25,7 +25,7 @@ private record Substitution(VCImplication node, Expression replacement) { /** * Applies one substitution in a VC chain */ - public static VCImplication applyOnce(VCImplication implication) { + public static VCImplication apply(VCImplication implication) { if (implication == null) return null; @@ -65,19 +65,10 @@ private static VCImplication substituteNode(VCImplication implication, VCImplica return implication.copyWithRefinement(new Predicate(exp)); Expression substituted = exp.substitute(new Var(node.getName()), replacement.clone()); - VCImplication origin = new VCImplication(node.getName(), node.getType(), origin(implication)); + VCImplication origin = new VCImplication(node.getName(), node.getType(), implication.getOriginRefinement()); return new SimplifiedVCImplication(implication, new Predicate(substituted), origin); } - /** - * Uses the earliest original predicate available when simplifying an already-simplified node - */ - private static Predicate origin(VCImplication implication) { - if (implication instanceof SimplifiedVCImplication simplified) - return simplified.getOrigin().getRefinement().clone(); - return implication.getRefinement().clone(); - } - /** * Finds the first substitution candidate in the VC chain */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 3dc9d9eac..d6e3ecc36 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -28,7 +28,7 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera VCImplication current = vc; for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) { - VCImplication simplified = VCSimplification.simplify(current); + VCImplication simplified = VCSimplification.simplifyToFixedPoint(current); if (current.equals(simplified)) break; diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index a19dd374d..cc0e4612f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -12,14 +12,14 @@ class VCSubstitutionTest { @Test void applyOnceReturnsNullForNullImplication() { - assertNull(VCSubstitution.applyOnce(null)); + assertNull(VCSubstitution.apply(null)); } @Test void substitutesBinderEqualityIntoWholeChain() { VCImplication implication = vc("∀x:int. x == 3", "x > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0")); } @@ -28,7 +28,7 @@ void substitutesBinderEqualityIntoWholeChain() { void substitutesReverseBinderEquality() { VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertSimplifiedVC(result, simplified("3 > 0", "∀x:int. x > 0")); } @@ -37,7 +37,7 @@ void substitutesReverseBinderEquality() { void substitutesCompoundKnownValue() { VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y")); } @@ -46,7 +46,7 @@ void substitutesCompoundKnownValue() { void usesFirstSubstitutionFoundInChain() { VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertVC(result, "x > 0", "x + 4 > 0"); assertEquals(VCImplication.class, result.getClass()); @@ -57,7 +57,7 @@ void usesFirstSubstitutionFoundInChain() { void substitutesInnerKnownValueAcrossNestedImplications() { VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertVC(result, "true", "z > 1", "1 + z > 0"); assertEquals(VCImplication.class, result.getClass()); @@ -69,7 +69,7 @@ void substitutesInnerKnownValueAcrossNestedImplications() { void substitutesOuterKnownValueIntoNestedBinderRefinements() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertSimplifiedVC(result, simplified("y == 3 + 1", "∀x:int. y == x + 1"), simplified("y > 3", "∀x:int. y > x")); @@ -79,7 +79,7 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() { void ignoresRecursiveBinderEquality() { VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertNotSame(implication, result); assertVC(result, "x == x + 1", "x > 0"); @@ -89,7 +89,7 @@ void ignoresRecursiveBinderEquality() { void ignoresNonEqualityBinderRefinement() { VCImplication implication = vc("∀x:int. x > 3", "x > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertNotSame(implication, result); assertVC(result, "x > 3", "x > 0"); @@ -99,7 +99,7 @@ void ignoresNonEqualityBinderRefinement() { void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0"); - VCImplication result = VCSubstitution.applyOnce(implication); + VCImplication result = VCSubstitution.apply(implication); assertVC(result, "x == 3", "x > 0"); } From bd77390325023a3ad9ce2620df4aa453971fd577 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 21:40:44 +0100 Subject: [PATCH 21/22] Minor Change --- .../java/liquidjava/processor/SimplifiedVCImplication.java | 6 +----- .../src/main/java/liquidjava/processor/VCImplication.java | 6 +++++- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java index ffa8ebfd3..7c741cdea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java @@ -16,15 +16,11 @@ public SimplifiedVCImplication(VCImplication implication, Predicate refinement, this.origin = origin.clone(); } + @Override public VCImplication getOrigin() { return origin; } - @Override - public Predicate getOriginRefinement() { - return origin.getRefinement().clone(); - } - @Override public VCImplication copyWithRefinement(Predicate refinement) { return new SimplifiedVCImplication(this, refinement, origin); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 1af4429ca..88f6811b8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -31,8 +31,12 @@ public VCImplication(VCImplication implication, Predicate ref) { this.refinement = ref; } + public VCImplication getOrigin() { + return new VCImplication(this, refinement.clone()); + } + public Predicate getOriginRefinement() { - return refinement.clone(); + return getOrigin().getRefinement().clone(); } public VCImplication copyWithRefinement(Predicate refinement) { From 07e0fa7b5f015504b32f9c760727d31b0241b96f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 11 Jun 2026 12:46:39 +0100 Subject: [PATCH 22/22] Add Tests --- .../rj_language/opt/VCSubstitutionTest.java | 50 ++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index cc0e4612f..aef90ff77 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -11,7 +11,7 @@ class VCSubstitutionTest { @Test - void applyOnceReturnsNullForNullImplication() { + void applyReturnsNullForNullImplication() { assertNull(VCSubstitution.apply(null)); } @@ -42,6 +42,44 @@ void substitutesCompoundKnownValue() { assertSimplifiedVC(result, simplified("y + 1 > y", "∀x:int. x > y")); } + @Test + void substitutesOnlyWholeVariableReferences() { + VCImplication implication = vc("∀x:int. x == 3", "xx > x"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("xx > 3", "∀x:int. xx > x")); + } + + @Test + void substitutesEveryOccurrenceInPredicate() { + VCImplication implication = vc("∀x:int. x == 2", "x + x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertSimplifiedVC(result, simplified("2 + 2 > 0", "∀x:int. x + x > 0")); + } + + @Test + void preservesRemainingBinderAfterSubstitution() { + VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertEquals("y", result.getName()); + assertEquals("y > 3", result.getRefinement().toString()); + assertVC(result.getNext(), "y > 0"); + } + + @Test + void removesSourceNodeWhenItIsLastInChain() { + VCImplication implication = vc("x > 0", "∀y:int. y == 1"); + + VCImplication result = VCSubstitution.apply(implication); + + assertVC(result, "x > 0"); + } + @Test void usesFirstSubstitutionFoundInChain() { VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); @@ -95,6 +133,16 @@ void ignoresNonEqualityBinderRefinement() { assertVC(result, "x > 3", "x > 0"); } + @Test + void ignoresDerivedBinderEquality() { + VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0"); + + VCImplication result = VCSubstitution.apply(implication); + + assertNotSame(implication, result); + assertVC(result, "x + 1 == 3", "x > 0"); + } + @Test void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0");