From f5879a90003ed17eba5340359e5f93637e85ae4a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Oct 2025 14:03:03 +0100 Subject: [PATCH] Decouple Z3 From Expressions --- .../rj_language/ast/AliasInvocation.java | 12 +- .../rj_language/ast/BinaryExpression.java | 45 +------ .../rj_language/ast/Expression.java | 6 +- .../rj_language/ast/FunctionInvocation.java | 12 +- .../rj_language/ast/GroupExpression.java | 8 +- .../java/liquidjava/rj_language/ast/Ite.java | 8 +- .../rj_language/ast/LiteralBoolean.java | 9 +- .../rj_language/ast/LiteralInt.java | 12 +- .../rj_language/ast/LiteralReal.java | 12 +- .../rj_language/ast/LiteralString.java | 10 +- .../rj_language/ast/UnaryExpression.java | 14 +-- .../java/liquidjava/rj_language/ast/Var.java | 8 +- .../visitors/ExpressionVisitor.java | 37 ++++++ .../liquidjava/smt/ExpressionToZ3Visitor.java | 110 ++++++++++++++++++ .../java/liquidjava/smt/SMTEvaluator.java | 4 +- 15 files changed, 205 insertions(+), 102 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index cdd89591..afe7b518 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -1,10 +1,10 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.ArrayList; import java.util.List; import java.util.stream.Collectors; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class AliasInvocation extends Expression { String name; @@ -24,12 +24,8 @@ public List getArgs() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - Expr[] argsExpr = new Expr[getArgs().size()]; - for (int i = 0; i < argsExpr.length; i++) { - argsExpr[i] = getArgs().get(i).eval(ctx); - } - return ctx.makeFunctionInvocation(name, argsExpr); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitAliasInvocation(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index ad7973cd..899b2367 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class BinaryExpression extends Expression { @@ -40,45 +40,8 @@ public boolean isArithmeticOperation() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - Expr ee1 = getFirstOperand().eval(ctx); - Expr ee2 = getSecondOperand().eval(ctx); - return evalBinaryOp(ctx, ee1, ee2); - } - - private Expr evalBinaryOp(TranslatorToZ3 ctx, Expr e1, Expr e2) { - switch (op) { - case "&&": - return ctx.makeAnd(e1, e2); - case "||": - return ctx.makeOr(e1, e2); - case "-->": - return ctx.makeImplies(e1, e2); - case "==": - return ctx.makeEquals(e1, e2); - case "!=": - return ctx.mkNot(ctx.makeEquals(e1, e2)); - case ">=": - return ctx.makeGtEq(e1, e2); - case ">": - return ctx.makeGt(e1, e2); - case "<=": - return ctx.makeLtEq(e1, e2); - case "<": - return ctx.makeLt(e1, e2); - case "+": - return ctx.makeAdd(e1, e2); - case "-": - return ctx.makeSub(e1, e2); - case "*": - return ctx.makeMul(e1, e2); - case "/": - return ctx.makeDiv(e1, e2); - case "%": - return ctx.makeMod(e1, e2); - default: // last case % - throw new RuntimeException("Operation " + op + "not supported by z3"); - } + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitBinaryExpression(this); } @Override 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 da75ec71..2cf469a4 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 @@ -1,19 +1,19 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.ArrayList; import java.util.List; import java.util.Map; + import liquidjava.processor.context.Context; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.ast.typing.TypeInfer; -import liquidjava.smt.TranslatorToZ3; +import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; import spoon.reflect.factory.Factory; public abstract class Expression { - public abstract Expr eval(TranslatorToZ3 ctx) throws Exception; + public abstract T accept(ExpressionVisitor visitor) throws Exception; public abstract void getVariableNames(List toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index f920ff7f..f2c4984f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -1,10 +1,10 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.ArrayList; import java.util.List; import java.util.stream.Collectors; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; public class FunctionInvocation extends Expression { @@ -30,12 +30,8 @@ public void setChild(int index, Expression element) { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - Expr[] argsExpr = new Expr[getArgs().size()]; - for (int i = 0; i < argsExpr.length; i++) { - argsExpr[i] = getArgs().get(i).eval(ctx); - } - return ctx.makeFunctionInvocation(name, argsExpr); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitFunctionInvocation(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index f7d7dcf3..a2be4ea2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class GroupExpression extends Expression { @@ -15,8 +15,8 @@ public Expression getExpression() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - return getExpression().eval(ctx); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitGroupExpression(this); } public String toString() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index 4accd126..44f90965 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class Ite extends Expression { @@ -25,8 +25,8 @@ public Expression getElse() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx)); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitIte(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java index 3d223697..85127fff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralBoolean extends Expression { @@ -16,8 +16,9 @@ public LiteralBoolean(String value) { this.value = Boolean.parseBoolean(value); } - public Expr eval(TranslatorToZ3 ctx) { - return ctx.makeBooleanLiteral(value); + @Override + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitLiteralBoolean(this); } public String toString() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java index 6a4e97f1..582ecd92 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralInt extends Expression { @@ -17,14 +17,18 @@ public LiteralInt(String v) { } @Override - public Expr eval(TranslatorToZ3 ctx) { - return ctx.makeIntegerLiteral(value); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitLiteralInt(this); } public String toString() { return Integer.toString(value); } + public int getValue() { + return value; + } + @Override public void getVariableNames(List toAdd) { // end leaf diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java index 2ddc8430..c80bf750 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralReal extends Expression { @@ -17,14 +17,18 @@ public LiteralReal(String v) { } @Override - public Expr eval(TranslatorToZ3 ctx) { - return ctx.makeDoubleLiteral(value); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitLiteralReal(this); } public String toString() { return Double.toString(value); } + public double getValue() { + return value; + } + @Override public void getVariableNames(List toAdd) { // end leaf diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java index eed7ec71..38577671 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralString extends Expression { private String value; @@ -12,8 +12,8 @@ public LiteralString(String v) { } @Override - public Expr eval(TranslatorToZ3 ctx) { - return ctx.makeString(value); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitLiteralString(this); } public String toString() { @@ -23,13 +23,11 @@ public String toString() { @Override public void getVariableNames(List toAdd) { // end leaf - } @Override public void getStateInvocations(List toAdd, List all) { // end leaf - } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index df5eb888..9bfdfec5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class UnaryExpression extends Expression { @@ -22,14 +22,8 @@ public String getOp() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - switch (op) { - case "-": - return ctx.makeMinus(getExpression().eval(ctx)); - case "!": - return ctx.mkNot(getExpression().eval(ctx)); - } - return null; + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitUnaryExpression(this); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java index 2e5c3b1d..2ab08d4f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java @@ -1,8 +1,8 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.List; -import liquidjava.smt.TranslatorToZ3; + +import liquidjava.rj_language.visitors.ExpressionVisitor; public class Var extends Expression { @@ -17,8 +17,8 @@ public String getName() { } @Override - public Expr eval(TranslatorToZ3 ctx) throws Exception { - return ctx.makeVariable(name); + public T accept(ExpressionVisitor visitor) throws Exception { + return visitor.visitVar(this); } public String toString() { 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 new file mode 100644 index 00000000..51ab5357 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -0,0 +1,37 @@ +package liquidjava.rj_language.visitors; + +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; + +public interface ExpressionVisitor { + T visitAliasInvocation(AliasInvocation alias) throws Exception; + + T visitBinaryExpression(BinaryExpression exp) throws Exception; + + T visitFunctionInvocation(FunctionInvocation fun) throws Exception; + + T visitGroupExpression(GroupExpression exp) throws Exception; + + T visitIte(Ite ite) throws Exception; + + T visitLiteralInt(LiteralInt lit) throws Exception; + + T visitLiteralBoolean(LiteralBoolean lit) throws Exception; + + T visitLiteralReal(LiteralReal lit) throws Exception; + + T visitLiteralString(LiteralString lit) throws Exception; + + T visitUnaryExpression(UnaryExpression exp) throws Exception; + + T visitVar(Var var) throws Exception; +} \ 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 new file mode 100644 index 00000000..40c025b3 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -0,0 +1,110 @@ +package liquidjava.smt; + +import com.microsoft.z3.Expr; + +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.visitors.ExpressionVisitor; + +public class ExpressionToZ3Visitor implements ExpressionVisitor> { + + private final TranslatorToZ3 ctx; + + public ExpressionToZ3Visitor(TranslatorToZ3 ctx) { + this.ctx = ctx; + } + + @Override + public Expr visitAliasInvocation(AliasInvocation alias) throws Exception { + Expr[] argsExpr = new Expr[alias.getArgs().size()]; + for (int i = 0; i < argsExpr.length; i++) { + argsExpr[i] = alias.getArgs().get(i).accept(this); + } + return ctx.makeFunctionInvocation(alias.getName(), argsExpr); + } + + @Override + public Expr visitBinaryExpression(BinaryExpression exp) throws Exception { + Expr e1 = exp.getFirstOperand().accept(this); + Expr e2 = exp.getSecondOperand().accept(this); + return switch (exp.getOperator()) { + case "&&" -> ctx.makeAnd(e1, e2); + case "||" -> ctx.makeOr(e1, e2); + case "-->" -> ctx.makeImplies(e1, e2); + case "==" -> ctx.makeEquals(e1, e2); + case "!=" -> ctx.mkNot(ctx.makeEquals(e1, e2)); + case ">=" -> ctx.makeGtEq(e1, e2); + case ">" -> ctx.makeGt(e1, e2); + case "<=" -> ctx.makeLtEq(e1, e2); + case "<" -> ctx.makeLt(e1, e2); + case "+" -> ctx.makeAdd(e1, e2); + case "-" -> ctx.makeSub(e1, e2); + case "*" -> ctx.makeMul(e1, e2); + case "/" -> ctx.makeDiv(e1, e2); + case "%" -> ctx.makeMod(e1, e2); + default -> throw new RuntimeException("Operation " + exp.getOperator() + " not supported by z3"); + }; + } + + @Override + public Expr visitFunctionInvocation(FunctionInvocation fun) throws Exception { + Expr[] argsExpr = new Expr[fun.getArgs().size()]; + for (int i = 0; i < argsExpr.length; i++) { + argsExpr[i] = fun.getArgs().get(i).accept(this); + } + return ctx.makeFunctionInvocation(fun.getName(), argsExpr); + } + + @Override + public Expr visitGroupExpression(GroupExpression exp) throws Exception { + return exp.getExpression().accept(this); + } + + @Override + public Expr visitIte(Ite ite) throws Exception { + return ctx.makeIte(ite.getCondition().accept(this), ite.getThen().accept(this), ite.getElse().accept(this)); + } + + @Override + public Expr visitVar(Var var) throws Exception { + return ctx.makeVariable(var.getName()); + } + + @Override + public Expr visitLiteralInt(LiteralInt lit) throws Exception { + return ctx.makeIntegerLiteral(lit.getValue()); + } + + @Override + public Expr visitLiteralBoolean(LiteralBoolean lit) throws Exception { + return ctx.makeBooleanLiteral(lit.isBooleanTrue()); + } + + @Override + public Expr visitLiteralReal(LiteralReal lit) throws Exception { + return ctx.makeDoubleLiteral(lit.getValue()); + } + + @Override + public Expr visitLiteralString(LiteralString lit) throws Exception { + return ctx.makeString(lit.toString()); + } + + @Override + public Expr visitUnaryExpression(UnaryExpression exp) throws Exception { + return switch (exp.getOp()) { + case "-" -> ctx.makeMinus(exp.getExpression().accept(this)); + case "!" -> ctx.mkNot(exp.getExpression().accept(this)); + default -> null; + }; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 621a2420..68dc4862 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -22,8 +22,8 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) Expression exp = toVerify.getExpression(); Status s; try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) { - // com.microsoft.z3.Expr - Expr e = exp.eval(tz3); + ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3); + Expr e = exp.accept(visitor); s = tz3.verifyExpression(e); if (s.equals(Status.SATISFIABLE)) {