From a08dbad873b6030cd605afa6265d9f732609bb91 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Tue, 3 Mar 2026 00:45:55 +0000 Subject: [PATCH 1/8] Added enum type support with tests --- .../main/java/testSuite/CorrectEnumUsage.java | 33 +++++++++++++++++ .../main/java/testSuite/ErrorEnumUsage.java | 35 +++++++++++++++++++ .../src/main/antlr4/rj/grammar/RJ.g4 | 4 +++ .../MethodsFirstChecker.java | 20 +++++++++++ .../RefinementTypeChecker.java | 6 +++- .../visitors/CreateASTVisitor.java | 16 +++++++-- .../liquidjava/smt/TranslatorContextToZ3.java | 8 ++++- .../liquidjava/utils/constants/Formats.java | 1 + 8 files changed, 119 insertions(+), 4 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java new file mode 100644 index 00000000..0d0d0957 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -0,0 +1,33 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@SuppressWarnings("unused") +@StateSet({"photoMode", "videoMode", "noMode"}) +class CorrectEnumUsage { + enum Mode { + Photo, Video, Unknown + } + + Mode mode; + @StateRefinement(to="noMode(this)") + public CorrectEnumUsage() {} + + @StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)") + @StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)") + public void setMode(Mode mode) { + this.mode = mode; + } + + @StateRefinement(from="photoMode(this)") + public void takePhoto() {} + + + public static void main(String[] args) { + // Correct + CorrectEnumUsage st = new CorrectEnumUsage(); + st.setMode(Mode.Photo); + st.takePhoto(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java new file mode 100644 index 00000000..57e6818e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java @@ -0,0 +1,35 @@ +// State Refinement Error +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@SuppressWarnings("unused") +@StateSet({"photoMode", "videoMode", "noMode"}) +class ErrorEnumUsage { + enum Mode { + Photo, Video, Unknown + } + + Mode mode; + @StateRefinement(to="noMode(this)") + public ErrorEnumUsage() {} + + @StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)") + @StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)") + public void setMode(Mode mode) { + this.mode = mode; + } + + @StateRefinement(from="photoMode(this)") + public void takePhoto() {} + + + public static void main(String[] args) { + // Correct + ErrorEnumUsage st = new ErrorEnumUsage(); + st.setMode(Mode.Video); + st.takePhoto(); //error + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index d6f7f45f..c84b4468 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -38,6 +38,7 @@ literalExpression: | literal #lit | ID #var | functionCall #invocation + | enumCall #enum ; functionCall: @@ -55,6 +56,9 @@ ghostCall: aliasCall: ID_UPPER '(' args? ')'; +enumCall: + OBJECT_TYPE; + args: pred (',' pred)* ; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index e764d453..32a1a91f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -7,8 +7,13 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Formats; +import liquidjava.utils.constants.Types; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtConstructor; +import spoon.reflect.declaration.CtEnum; +import spoon.reflect.declaration.CtEnumValue; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtType; @@ -116,4 +121,19 @@ public void visitCtMethod(CtMethod method) { } context.exitContext(); } + + @Override + public > void visitCtEnum(CtEnum enumRead) { + String enumName = enumRead.getSimpleName(); + String qualifiedEnumName = enumRead.getQualifiedName(); + int ordinal = 0; + for (CtEnumValue ev : enumRead.getEnumValues()) { + String varName = String.format(Formats.ENUM_VALUE, enumName, ev.getSimpleName()); + Predicate refinement = Predicate.createEquals(Predicate.createVar(varName), + Predicate.createLit(String.valueOf(ordinal), Types.INT)); + context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), refinement); + ordinal++; + } + super.visitCtEnum(enumRead); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index d3d95bbd..fbcd0304 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -269,7 +269,11 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String targetName = fieldRead.getTarget().toString(); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.length(targetName, fieldRead))); - + } else if (fieldRead.getVariable().getDeclaringType().isEnum()) { + String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); + String enumLiteral = String.format(Formats.ENUM_VALUE, target, fieldName); + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral))); } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE? diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index d906772c..7d649134 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -19,6 +19,7 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import org.antlr.v4.runtime.tree.ParseTree; @@ -26,6 +27,7 @@ import rj.grammar.RJParser.AliasCallContext; import rj.grammar.RJParser.ArgsContext; import rj.grammar.RJParser.DotCallContext; +import rj.grammar.RJParser.EnumContext; import rj.grammar.RJParser.ExpBoolContext; import rj.grammar.RJParser.ExpContext; import rj.grammar.RJParser.ExpGroupContext; @@ -156,9 +158,10 @@ private Expression literalExpressionCreate(ParseTree rc) throws LJError { return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); else if (rc instanceof LitContext) return create(((LitContext) rc).literal()); - else if (rc instanceof VarContext) { + else if (rc instanceof VarContext) return new Var(((VarContext) rc).ID().getText()); - + else if (rc instanceof EnumContext) { + return new Var(enumCreate((EnumContext) rc)); } else { return create(((InvocationContext) rc).functionCall()); } @@ -234,6 +237,15 @@ private List getArgs(ArgsContext args) throws LJError { return le; } + private String enumCreate(EnumContext rc) { + String enumText = rc.enumCall().getText(); + int lastDot = enumText.lastIndexOf('.'); + String enumClass = enumText.substring(0, lastDot); + String enumConst = enumText.substring(lastDot + 1); + String varName = String.format(Formats.ENUM_VALUE, enumClass, enumConst); + return varName; + } + private Expression literalCreate(LiteralContext literalContext) throws LJError { if (literalContext.BOOL() != null) return new LiteralBoolean(literalContext.BOOL().getText()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index c660d12b..c9b80eba 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -48,7 +48,12 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) case "long", "java.lang.Long" -> z3.mkRealConst(name); case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); - default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); + case "java.lang.Enum" -> z3.mkIntConst(name); + default -> { + if (type.isEnum()) + yield z3.mkIntConst(name); + yield z3.mkConst(name, z3.mkUninterpretedSort(typeName)); + } }; } @@ -88,6 +93,7 @@ static Sort getSort(Context z3, String sort) { case "float", "java.lang.Float" -> z3.mkFPSort32(); case "double", "java.lang.Double" -> z3.mkFPSortDouble(); case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); + case "java.lang.Enum" -> z3.getIntSort(); case "String" -> z3.getStringSort(); case "void" -> z3.mkUninterpretedSort("void"); default -> z3.mkUninterpretedSort(sort); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index f3ae77f0..0b4ac7e5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -5,4 +5,5 @@ public final class Formats { public static final String INSTANCE = "#%s_%d"; public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; + public static final String ENUM_VALUE = "enum#%s#%s"; } \ No newline at end of file From 3835584b566f7cba407455a93b08bc736a480bf5 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Tue, 3 Mar 2026 18:01:10 +0000 Subject: [PATCH 2/8] Added EnumRefinementMessage test Added a test for enums to, in the future, help clean the refinement message. --- .../testingInProgress/EnumRefinementMessage.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java diff --git a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java new file mode 100644 index 00000000..fcba04ba --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java @@ -0,0 +1,15 @@ +package testingInProgress; + +import liquidjava.specification.Refinement; + +public class EnumRefinementMessage { + enum Mode { + Photo, Video, Unknown + } + + public static void main(String[] args) { + @Refinement("_==Mode.Photo") + Mode test = Mode.Video; + System.out.println(test); + } +} From 3d7fb5db74a3f6f095591f36a5e60594d0d7718c Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 4 Mar 2026 19:46:22 +0000 Subject: [PATCH 3/8] Applied fixes and suggestions for enums Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format. --- .../src/main/antlr4/rj/grammar/RJ.g4 | 3 +- .../MethodsFirstChecker.java | 10 +-- .../RefinementTypeChecker.java | 2 +- .../liquidjava/rj_language/ast/Enumerate.java | 74 +++++++++++++++++++ .../visitors/CreateASTVisitor.java | 14 ++-- .../visitors/ExpressionVisitor.java | 3 + .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 ++ .../liquidjava/smt/TranslatorContextToZ3.java | 20 +++-- .../java/liquidjava/smt/TranslatorToZ3.java | 7 ++ .../liquidjava/utils/constants/Formats.java | 2 +- 10 files changed, 118 insertions(+), 23 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index c84b4468..e0e402e9 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -57,7 +57,7 @@ aliasCall: ID_UPPER '(' args? ')'; enumCall: - OBJECT_TYPE; + ENUM_CALL; args: pred (',' pred)* ; @@ -97,6 +97,7 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; +ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*; ID_UPPER: ([A-Z][a-zA-Z0-9]*); OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 32a1a91f..581b4644 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -126,13 +126,9 @@ public void visitCtMethod(CtMethod method) { public > void visitCtEnum(CtEnum enumRead) { String enumName = enumRead.getSimpleName(); String qualifiedEnumName = enumRead.getQualifiedName(); - int ordinal = 0; - for (CtEnumValue ev : enumRead.getEnumValues()) { - String varName = String.format(Formats.ENUM_VALUE, enumName, ev.getSimpleName()); - Predicate refinement = Predicate.createEquals(Predicate.createVar(varName), - Predicate.createLit(String.valueOf(ordinal), Types.INT)); - context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), refinement); - ordinal++; + for (CtEnumValue ev : enumRead.getEnumValues()) { + String varName = String.format(Formats.ENUM, enumName, ev.getSimpleName()); + context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), null); } super.visitCtEnum(enumRead); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index fbcd0304..82988819 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -271,7 +271,7 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { BuiltinFunctionPredicate.length(targetName, fieldRead))); } else if (fieldRead.getVariable().getDeclaringType().isEnum()) { String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); - String enumLiteral = String.format(Formats.ENUM_VALUE, target, fieldName); + String enumLiteral = String.format(Formats.ENUM, target, fieldName); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral))); } else { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java new file mode 100644 index 00000000..7f9341c1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java @@ -0,0 +1,74 @@ +package liquidjava.rj_language.ast; + +import java.util.List; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; + +public class Enumerate extends Expression { + + private final String enumTypeName; + private final String enumConstantName; + + public Enumerate(String enumTypeName, String enumConstantName) { + this.enumTypeName = enumTypeName; + this.enumConstantName = enumConstantName; + } + + public String getEnumTypeName() { + return enumTypeName; + } + + public String getEnumConstantName() { + return enumConstantName; + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitEnumerate(this); + } + + @Override + public void getVariableNames(List toAdd) { + // end leaf + } + + @Override + public void getStateInvocations(List toAdd, List all) { + // end leaf + } + + @Override + public boolean isBooleanTrue() { + return false; + } + + @Override + public String toString() { + return enumTypeName + "." + enumConstantName; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((enumTypeName == null) ? 0 : enumTypeName.hashCode()); + result = prime * result + ((enumConstantName == null) ? 0 : enumConstantName.hashCode()); + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null || getClass() != obj.getClass()) + return false; + Enumerate other = (Enumerate) obj; + return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName); + } + + @Override + public Expression clone() { + return new Enumerate(enumTypeName, enumConstantName); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 7d649134..df5b8ccc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -7,6 +7,7 @@ import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; @@ -161,7 +162,7 @@ else if (rc instanceof LitContext) else if (rc instanceof VarContext) return new Var(((VarContext) rc).ID().getText()); else if (rc instanceof EnumContext) { - return new Var(enumCreate((EnumContext) rc)); + return enumCreate((EnumContext) rc); } else { return create(((InvocationContext) rc).functionCall()); } @@ -237,13 +238,12 @@ private List getArgs(ArgsContext args) throws LJError { return le; } - private String enumCreate(EnumContext rc) { - String enumText = rc.enumCall().getText(); + private Enumerate enumCreate(EnumContext enumContext) { + String enumText = enumContext.enumCall().getText(); int lastDot = enumText.lastIndexOf('.'); - String enumClass = enumText.substring(0, lastDot); - String enumConst = enumText.substring(lastDot + 1); - String varName = String.format(Formats.ENUM_VALUE, enumClass, enumConst); - return varName; + String enumTypeName = enumText.substring(0, lastDot); + String enumConstName = enumText.substring(lastDot + 1); + return new Enumerate(enumTypeName, enumConstName); } private Expression literalCreate(LiteralContext literalContext) throws LJError { 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 e3db3938..4b9808fc 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 @@ -3,6 +3,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -40,5 +41,7 @@ public interface ExpressionVisitor { T visitUnaryExpression(UnaryExpression exp) throws LJError; + T visitEnumerate(Enumerate 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 4a45b1d8..9da522d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -5,6 +5,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -120,4 +121,9 @@ public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { default -> null; }; } + + @Override + public Expr visitEnumerate(Enumerate en) throws LJError { + return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName()); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index c9b80eba..7c35885a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -1,6 +1,7 @@ package liquidjava.smt; import com.microsoft.z3.Context; +import com.microsoft.z3.EnumSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; @@ -13,6 +14,8 @@ import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; +import spoon.reflect.declaration.CtEnum; +import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtTypeReference; public class TranslatorContextToZ3 { @@ -41,6 +44,16 @@ public static void storeVariablesSubtypes(Context z3, List vari private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); + + if (type.isEnum()) { + CtType decl = type.getDeclaration(); + if (decl instanceof CtEnum enumDecl) { + String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()).toArray(String[]::new); + EnumSort enumSort = z3.mkEnumSort(typeName, enumValueNames); + return z3.mkConst(name, enumSort); + } + } + return switch (typeName) { case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3 .mkIntConst(name); @@ -48,12 +61,7 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) case "long", "java.lang.Long" -> z3.mkRealConst(name); case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); - case "java.lang.Enum" -> z3.mkIntConst(name); - default -> { - if (type.isEnum()) - yield z3.mkIntConst(name); - yield z3.mkConst(name, z3.mkUninterpretedSort(typeName)); - } + default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..02fed44a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -3,6 +3,7 @@ import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.EnumSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; @@ -26,6 +27,7 @@ import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import com.microsoft.z3.enumerations.Z3_sort_kind; @@ -119,6 +121,11 @@ public Expr makeVariable(String name) throws LJError { return expr; } + public Expr makeEnum(String enumTypeName, String enumConstantName) throws LJError { + String varName = String.format(Formats.ENUM, enumTypeName, enumConstantName); + return getVariableTranslation(varName); + } + public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { if (name.equals("addToIndex")) return makeStore(params); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index 0b4ac7e5..7bd8557e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -5,5 +5,5 @@ public final class Formats { public static final String INSTANCE = "#%s_%d"; public static final String THIS = "this#%s"; public static final String RET = "#ret_%d"; - public static final String ENUM_VALUE = "enum#%s#%s"; + public static final String ENUM = "%s.%s"; } \ No newline at end of file From c831921b54ad34c9953ac39e8675ac6702ee877c Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 4 Mar 2026 20:07:48 +0000 Subject: [PATCH 4/8] Fixed grammar Fixed grammar so that it required uppercase start for both parts. Differentiates between types and calls. --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e0e402e9..b2ac847c 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -97,8 +97,8 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; -ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*; ID_UPPER: ([A-Z][a-zA-Z0-9]*); +ENUM_CALL: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*; OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*; From d785934ee7b7ec479805709b968fc1d276a68ff7 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 4 Mar 2026 22:11:42 +0000 Subject: [PATCH 5/8] Revert "Fixed grammar" This reverts commit c831921b54ad34c9953ac39e8675ac6702ee877c. --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index b2ac847c..e0e402e9 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -97,8 +97,8 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; +ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*; ID_UPPER: ([A-Z][a-zA-Z0-9]*); -ENUM_CALL: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*; OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*; From 66e982f2c8ab855af36d24f15cda8d7ddfc23f57 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 4 Mar 2026 22:59:27 +0000 Subject: [PATCH 6/8] Reapply "Fixed grammar" This reverts commit d785934ee7b7ec479805709b968fc1d276a68ff7. --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e0e402e9..b2ac847c 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -97,8 +97,8 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; -ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*; ID_UPPER: ([A-Z][a-zA-Z0-9]*); +ENUM_CALL: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*; OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*; From 66bebc2edd3d70db7524759b20bb480ac89a7d2b Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 5 Mar 2026 21:25:16 +0000 Subject: [PATCH 7/8] Separated translation into phases Translation is now done in 2 phases: a first one for enums, and storing their constant values and names, and the second one as previously done, but with special attention now due to the presence of enums. If the variable, when translating, is already present, it isn't added, and there are no duplicates. --- .../liquidjava/smt/TranslatorContextToZ3.java | 60 +++++++++++++++---- 1 file changed, 49 insertions(+), 11 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 7c35885a..512fbc83 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -7,6 +7,7 @@ import com.microsoft.z3.FuncDecl; import com.microsoft.z3.Sort; import java.util.ArrayList; +import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.stream.Stream; @@ -23,13 +24,59 @@ public class TranslatorContextToZ3 { static void translateVariables(Context z3, Map> ctx, Map> varTranslation) { - for (String name : ctx.keySet()) - varTranslation.put(name, getExpr(z3, name, ctx.get(name))); + Map> enumSorts = new HashMap<>(); + translateEnums(z3, ctx, varTranslation, enumSorts); + translateNonEnumVariables(z3, ctx, varTranslation, enumSorts); varTranslation.put("true", z3.mkBool(true)); varTranslation.put("false", z3.mkBool(false)); } + private static void translateEnums(Context z3, Map> ctx, + Map> varTranslation, Map> enumSorts) { + // First pass: create one EnumSort per enum type and store actual enum constants + for (Map.Entry> entry : ctx.entrySet()) { + CtTypeReference type = entry.getValue(); + if (!type.isEnum()) + continue; + String typeName = type.getQualifiedName(); + if (enumSorts.containsKey(typeName)) + continue; + CtType decl = type.getDeclaration(); + if (decl instanceof CtEnum enumDecl) { + String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()) + .toArray(String[]::new); + EnumSort enumSort = z3.mkEnumSort(typeName, enumValueNames); + enumSorts.put(typeName, enumSort); + + // Store actual enum constant values (not free variables) + Expr[] consts = enumSort.getConsts(); + for (int i = 0; i < enumValueNames.length; i++) { + String varName = enumDecl.getSimpleName() + "." + enumValueNames[i]; + varTranslation.put(varName, consts[i]); + } + } + } + } + + private static void translateNonEnumVariables(Context z3, Map> ctx, + Map> varTranslation, Map> enumSorts) { + // Second pass: translate non-enum variables and enum-typed variables (not constants) + for (Map.Entry> entry : ctx.entrySet()) { + String name = entry.getKey(); + if (varTranslation.containsKey(name)) + continue; // Already translated as an enum constant + CtTypeReference type = entry.getValue(); + if (type.isEnum()) { + String typeName = type.getQualifiedName(); + EnumSort enumSort = enumSorts.get(typeName); + varTranslation.put(name, z3.mkConst(name, enumSort)); + } else { + varTranslation.put(name, getExpr(z3, name, type)); + } + } + } + public static void storeVariablesSubtypes(Context z3, List variables, Map>> varSuperTypes) { for (RefinedVariable v : variables) { @@ -44,15 +91,6 @@ public static void storeVariablesSubtypes(Context z3, List vari private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); - - if (type.isEnum()) { - CtType decl = type.getDeclaration(); - if (decl instanceof CtEnum enumDecl) { - String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()).toArray(String[]::new); - EnumSort enumSort = z3.mkEnumSort(typeName, enumValueNames); - return z3.mkConst(name, enumSort); - } - } return switch (typeName) { case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3 From 9e79999c36ede5edfd1e093045e07a49ffda4d40 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Thu, 5 Mar 2026 22:31:51 +0000 Subject: [PATCH 8/8] Refactored variable translation --- .../liquidjava/smt/TranslatorContextToZ3.java | 73 +++++++------------ 1 file changed, 28 insertions(+), 45 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 512fbc83..76a20bea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -16,65 +16,48 @@ import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; import spoon.reflect.declaration.CtEnum; -import spoon.reflect.declaration.CtType; import spoon.reflect.reference.CtTypeReference; public class TranslatorContextToZ3 { static void translateVariables(Context z3, Map> ctx, - Map> varTranslation) { - + Map> varTranslation) { + // Translates all variables into z3 expressions, creating EnumSorts once per unique enum type. Map> enumSorts = new HashMap<>(); - translateEnums(z3, ctx, varTranslation, enumSorts); - translateNonEnumVariables(z3, ctx, varTranslation, enumSorts); - - varTranslation.put("true", z3.mkBool(true)); - varTranslation.put("false", z3.mkBool(false)); - } - private static void translateEnums(Context z3, Map> ctx, - Map> varTranslation, Map> enumSorts) { - // First pass: create one EnumSort per enum type and store actual enum constants for (Map.Entry> entry : ctx.entrySet()) { + String name = entry.getKey(); CtTypeReference type = entry.getValue(); - if (!type.isEnum()) - continue; - String typeName = type.getQualifiedName(); - if (enumSorts.containsKey(typeName)) + + if (varTranslation.containsKey(name)) continue; + + if (type.isEnum() && type.getDeclaration() instanceof CtEnum enumDecl) { + EnumSort enumSort = translateEnum(z3, varTranslation, enumSorts, type, enumDecl); + // translateEnum may have already registered name as a literal constant + // (e.g. Mode.Photo), no need to overwrite + if (!varTranslation.containsKey(name)) + varTranslation.put(name, z3.mkConst(name, enumSort)); continue; - CtType decl = type.getDeclaration(); - if (decl instanceof CtEnum enumDecl) { - String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()) - .toArray(String[]::new); - EnumSort enumSort = z3.mkEnumSort(typeName, enumValueNames); - enumSorts.put(typeName, enumSort); - - // Store actual enum constant values (not free variables) - Expr[] consts = enumSort.getConsts(); - for (int i = 0; i < enumValueNames.length; i++) { - String varName = enumDecl.getSimpleName() + "." + enumValueNames[i]; - varTranslation.put(varName, consts[i]); - } } + varTranslation.put(name, getExpr(z3, name, type)); } + + varTranslation.put("true", z3.mkBool(true)); + varTranslation.put("false", z3.mkBool(false)); } - private static void translateNonEnumVariables(Context z3, Map> ctx, - Map> varTranslation, Map> enumSorts) { - // Second pass: translate non-enum variables and enum-typed variables (not constants) - for (Map.Entry> entry : ctx.entrySet()) { - String name = entry.getKey(); - if (varTranslation.containsKey(name)) - continue; // Already translated as an enum constant - CtTypeReference type = entry.getValue(); - if (type.isEnum()) { - String typeName = type.getQualifiedName(); - EnumSort enumSort = enumSorts.get(typeName); - varTranslation.put(name, z3.mkConst(name, enumSort)); - } else { - varTranslation.put(name, getExpr(z3, name, type)); - } - } + private static EnumSort translateEnum(Context z3, Map> varTranslation, Map> enumSorts, CtTypeReference type, CtEnum enumDecl) { + // Creates (and caches if needed) a z3 EnumSort for a given enum type. Registers enum literal constants + // on first creation. + return enumSorts.computeIfAbsent(type.getQualifiedName(), k -> { + String[] enumValueNames = enumDecl.getEnumValues().stream() + .map(ev -> ev.getSimpleName()).toArray(String[]::new); + EnumSort enumSort = z3.mkEnumSort(k, enumValueNames); + Expr[] consts = enumSort.getConsts(); + for (int i = 0; i < enumValueNames.length; i++) + varTranslation.put(enumDecl.getSimpleName() + "." + enumValueNames[i], consts[i]); + return enumSort; + }); } public static void storeVariablesSubtypes(Context z3, List variables,