visitor darft

Kirill Golubev · Kirill Golubev · commit b50c2e1e3870 · 2022-11-12T14:30:19.000+03:00
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java
@@ -6,6 +6,7 @@
 
 import com.microsoft.z3.Expr;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -26,6 +27,11 @@ public List<Expression> getArgs() {
         return children;
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {
+        getArgs().forEach(a -> a.accept(v));
+    }
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java
@@ -6,6 +6,7 @@
 
 import com.microsoft.z3.Expr;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -44,6 +45,12 @@ public boolean isArithmeticOperation() {
         return !isLogicOperation() && !isBooleanOperation();
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {
+        getFirstOperand().accept(v);
+        getSecondOperand().accept(v);
+    }
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         ExprWrapper ee1 = getFirstOperand().eval(ctx);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
@@ -7,12 +7,15 @@
 import liquidjava.processor.context.Context;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.typing.TypeInfer;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 import spoon.reflect.factory.Factory;
 
 public abstract class Expression {
 
+    public abstract void accept(ExpressionVisitor v);
+
     public abstract ExprWrapper eval(SMTWrapper ctx) throws Exception;
 
     public abstract void getVariableNames(List<String> toAdd);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java
@@ -6,6 +6,7 @@
 
 import com.microsoft.z3.Expr;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -31,6 +32,11 @@ public void setChild(int index, Expression element) {
         getArgs().set(index, element);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {
+        getArgs().forEach(a -> a.accept(v));
+    }
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -15,6 +16,11 @@ public Expression getExpression() {
         return children.get(0);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {
+        getExpression().accept(v);
+    }
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         return getExpression().eval(ctx);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -25,6 +26,13 @@ public Expression getElse() {
         return children.get(2);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {
+        getCondition().accept(v);
+        getThen().accept(v);
+        getElse().accept(v);
+    }
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx));
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -17,6 +18,9 @@ public LiteralBoolean(String value) {
         this.value = Boolean.parseBoolean(value);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     public ExprWrapper eval(SMTWrapper ctx) {
         return ctx.makeBooleanLiteral(value);
     }
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -17,6 +18,9 @@ public LiteralInt(String v) {
         value = Integer.parseInt(v);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) {
         return ctx.makeIntegerLiteral(value);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -17,6 +18,9 @@ public LiteralReal(String v) {
         value = Double.parseDouble(v);
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) {
         return ctx.makeDoubleLiteral(value);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -12,6 +13,9 @@ public LiteralString(String v) {
         value = v;
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) {
         return ctx.makeString(value);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -22,6 +23,9 @@ public String getOp() {
         return op;
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         switch (op) {
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java
@@ -2,6 +2,7 @@
 
 import java.util.List;
 
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.smt.solver_wrapper.ExprWrapper;
 import liquidjava.smt.solver_wrapper.SMTWrapper;
 
@@ -17,6 +18,9 @@ public String getName() {
         return name;
     }
 
+    @Override
+    public void accept(ExpressionVisitor v) {}
+
     @Override
     public ExprWrapper eval(SMTWrapper ctx) throws Exception {
         return ctx.makeVariable(name);
diff --git a/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
@@ -0,0 +1,17 @@
+package liquidjava.rj_language.visitors;
+
+import liquidjava.rj_language.ast.*;
+
+public interface ExpressionVisitor {
+    void visitAliasInvocation(AliasInvocation ai);
+    void visitBinaryExpression(BinaryExpression be);
+    void visitFunctionInvocation(FunctionInvocation fi);
+    void visitGroupExpression(GroupExpression ge);
+    void visitITE(Ite ite);
+    void visitLiteralBoolean(LiteralBoolean lb);
+    void visitLiteralInt(LiteralInt li);
+    void visitLiteralReal(LiteralReal lr);
+    void visitLiteralString(LiteralString ls);
+    void visitUnaryExpression(UnaryExpression ue);
+    void visitVar(Var v);
+}

Original file line number	Diff line number	Diff line change
`@@ -2,6 +2,7 @@`
`2`	`2`
`3`	`3`	`import java.util.List;`
`4`	`4`
	`5`	`+import liquidjava.rj_language.visitors.ExpressionVisitor;`
`5`	`6`	`import liquidjava.smt.solver_wrapper.ExprWrapper;`
`6`	`7`	`import liquidjava.smt.solver_wrapper.SMTWrapper;`
`7`	`8`
`@@ -17,6 +18,9 @@ public LiteralBoolean(String value) {`
`17`	`18`	`this.value = Boolean.parseBoolean(value);`
`18`	`19`	`}`
`19`	`20`
	`21`	`+ @Override`
	`22`	`+ public void accept(ExpressionVisitor v) {}`
	`23`	`+`
`20`	`24`	`public ExprWrapper eval(SMTWrapper ctx) {`
`21`	`25`	`return ctx.makeBooleanLiteral(value);`
`22`	`26`	`}`