From c70cc5a8ea91399409e80388ae2a6f6606d4c4b6 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 01/13] 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 000000000..0d0d09579 --- /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 000000000..57e6818ed --- /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 d6f7f45f7..c84b4468d 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 e764d4534..32a1a91f3 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 d3d95bbd0..fbcd03042 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 d906772c2..7d6491344 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 c660d12b8..c9b80ebae 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 f3ae77f0b..0b4ac7e52 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 e77a33b5f63d2c7cf448328aab990beecd9eac73 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 02/13] 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 000000000..fcba04bae --- /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 a359d1f9c5a33345c9905f11d9fecf0a71ca9e8f 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 03/13] 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 c84b4468d..e0e402e92 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 32a1a91f3..581b46443 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 fbcd03042..829888190 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 000000000..7f9341c1e --- /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 7d6491344..df5b8ccc3 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 e3db3938e..4b9808fc1 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 4a45b1d87..9da522d96 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 c9b80ebae..7c35885a9 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 bfc756c2c..920c0b707 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.processor.context.AliasWrapper; import liquidjava.utils.Pair; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import com.microsoft.z3.enumerations.Z3_sort_kind; @@ -121,6 +123,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 0b4ac7e52..7bd8557e6 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 a6a4055a761475f2df24b8b2c135f4b530e48dc7 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 04/13] 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 e0e402e92..b2ac847c4 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 0ab2098859b4baf1b7d1a84214f6aa267e6c6521 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 05/13] 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 b2ac847c4..e0e402e92 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 44758c795d32d4587f2db713e86cf447eec49800 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 06/13] 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 e0e402e92..b2ac847c4 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 b610928ff2979132e3b382cbd8638ba2f2d72727 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 07/13] 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 7c35885a9..512fbc83c 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 cdf192e01b23ed26a09ebe1de4c54ff88508f588 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 08/13] 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 512fbc83c..76a20bea0 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, From d7dea402405947adde92ef0015cd1bce69abe517 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Sun, 8 Mar 2026 00:41:02 +0000 Subject: [PATCH 09/13] Added enum tests Added 2 error tests for enum: when setting null on a field with an enum refinement, and on a function parameter refinement. A successful error test was added as well to test backtracking to a null state. --- .../java/testSuite/CorrectEnumResetMode.java | 44 +++++++++++++++++++ .../ErrorEnumFunctionRefinement.java | 22 ++++++++++ .../main/java/testSuite/ErrorEnumNull.java | 16 +++++++ 3 files changed, 82 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java new file mode 100644 index 000000000..1703df9b2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java @@ -0,0 +1,44 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@SuppressWarnings("unused") +@StateSet({"photoMode", "videoMode", "noMode"}) +class CorrectEnumResetMode { + enum Mode { + Photo, Video, Unknown + } + + Mode mode; + + @StateRefinement(to="noMode(this)") + public CorrectEnumResetMode() {} + + @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)", to="noMode(this)") + @StateRefinement(from="videoMode(this)", to="noMode(this)") + public void resetMode() { + this.mode = null; + } + + @StateRefinement(from="photoMode(this)") + public void takePhoto() {} + + @StateRefinement(from="videoMode(this)") + public void takeVideo() {} + + public static void main(String[] args) { + CorrectEnumResetMode st = new CorrectEnumResetMode(); + st.setMode(Mode.Photo); // noMode -> photoMode + st.takePhoto(); + st.resetMode(); // photoMode -> noMode + st.setMode(Mode.Video); // noMode -> videoMode + st.takeVideo(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java new file mode 100644 index 000000000..4698f33c7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java @@ -0,0 +1,22 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class ErrorEnumFunctionRefinement { + enum Color { Red, Green, Blue } + + Color c; + + Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green") Color newColor) { + c = newColor; // correct + return c; + } + + public static void main(String[] args) { + ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement(); + e.changeColor(Color.Red); // correct + e.changeColor(Color.Blue); // error + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java new file mode 100644 index 000000000..25e938d90 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java @@ -0,0 +1,16 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class ErrorEnumNull { + enum Color { + Red, Green, Blue + } + + public static void main(String[] args) { + @Refinement("c == Color.Red || c == Color.Green") + Color c = null; // error + } +} \ No newline at end of file From e3e49d28b5a454822b319c47ff8addd89019d206 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 11 Mar 2026 12:10:27 +0000 Subject: [PATCH 10/13] Added enum tests, adjusted grammar Added some more enum tests for different situations (like as parameters or fields with enum refinements). Merged CorrectEnumResetMode into CorrectEnumUsage (redundant having a separate one that only tests resetting to null) Refactored enumCreate as suggested. Refactored grammar to follow Enumerate class. --- .../main/java/testSuite/CorrectEnumField.java | 23 ++++++++++ .../main/java/testSuite/CorrectEnumParam.java | 19 ++++++++ .../java/testSuite/CorrectEnumResetMode.java | 44 ------------------- .../main/java/testSuite/CorrectEnumUsage.java | 14 +++++- .../java/testSuite/ErrorEnumNegation.java | 19 ++++++++ .../EnumRefinementMessage.java | 2 +- .../src/main/antlr4/rj/grammar/RJ.g4 | 13 +++--- .../visitors/CreateASTVisitor.java | 8 ++-- 8 files changed, 85 insertions(+), 57 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumField.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java delete mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java new file mode 100644 index 000000000..05c1d21d2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class CorrectEnumField { + enum Color { + Red, Green, Blue + } + + @Refinement("color != Color.Blue") + Color color; + + void setColor(@Refinement("c != Color.Blue") Color c) { + color = c; + } + + public static void main(String[] args) { + CorrectEnumField cef = new CorrectEnumField(); + cef.setColor(Color.Red); // correct + cef.setColor(Color.Green); // correct + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java new file mode 100644 index 000000000..7e942c209 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class CorrectEnumParam { + enum Status { + Active, Inactive, Pending + } + + Status process(@Refinement("status == Status.Inactive") Status status) { + return Status.Active; + } + + public static void main(String[] args) { + CorrectEnumParam cep = new CorrectEnumParam(); + cep.process(Status.Inactive); // correct + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java deleted file mode 100644 index 1703df9b2..000000000 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java +++ /dev/null @@ -1,44 +0,0 @@ -package testSuite; - -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@SuppressWarnings("unused") -@StateSet({"photoMode", "videoMode", "noMode"}) -class CorrectEnumResetMode { - enum Mode { - Photo, Video, Unknown - } - - Mode mode; - - @StateRefinement(to="noMode(this)") - public CorrectEnumResetMode() {} - - @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)", to="noMode(this)") - @StateRefinement(from="videoMode(this)", to="noMode(this)") - public void resetMode() { - this.mode = null; - } - - @StateRefinement(from="photoMode(this)") - public void takePhoto() {} - - @StateRefinement(from="videoMode(this)") - public void takeVideo() {} - - public static void main(String[] args) { - CorrectEnumResetMode st = new CorrectEnumResetMode(); - st.setMode(Mode.Photo); // noMode -> photoMode - st.takePhoto(); - st.resetMode(); // photoMode -> noMode - st.setMode(Mode.Video); // noMode -> videoMode - st.takeVideo(); - } -} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java index 0d0d09579..87c7cdce0 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -19,15 +19,27 @@ public CorrectEnumUsage() {} public void setMode(Mode mode) { this.mode = mode; } + + @StateRefinement(from="photoMode(this)", to="noMode(this)") + @StateRefinement(from="videoMode(this)", to="noMode(this)") + public void resetMode() { + this.mode = null; + } @StateRefinement(from="photoMode(this)") public void takePhoto() {} + + @StateRefinement(from="videoMode(this)") + public void takeVideo() {} public static void main(String[] args) { // Correct CorrectEnumUsage st = new CorrectEnumUsage(); - st.setMode(Mode.Photo); + st.setMode(Mode.Photo); // noMode -> photoMode st.takePhoto(); + st.resetMode(); // photoMode -> noMode + st.setMode(Mode.Video); // noMode -> videoMode + st.takeVideo(); } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java new file mode 100644 index 000000000..3534bf247 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java @@ -0,0 +1,19 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +class ErrorEnumNegation { + enum Status { + Active, Inactive, Pending + } + + void process(@Refinement("status != Status.Inactive") Status status) {} + + public static void main(String[] args) { + ErrorEnumNegation e = new ErrorEnumNegation(); + e.process(Status.Active); // correct + e.process(Status.Inactive); // error + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java index fcba04bae..2c8e0f1dd 100644 --- a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java +++ b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java @@ -2,7 +2,7 @@ import liquidjava.specification.Refinement; -public class EnumRefinementMessage { +class EnumRefinementMessage { enum Mode { Photo, Video, Unknown } diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index b2ac847c4..ebb4c73fd 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -38,13 +38,14 @@ literalExpression: | literal #lit | ID #var | functionCall #invocation - | enumCall #enum + | enumerate #enum ; - functionCall: +functionCall: ghostCall | aliasCall - | dotCall; + | dotCall + ; dotCall: OBJECT_TYPE '(' args? ')' @@ -56,8 +57,8 @@ ghostCall: aliasCall: ID_UPPER '(' args? ')'; -enumCall: - ENUM_CALL; +enumerate: + ENUM; args: pred (',' pred)* ; @@ -98,7 +99,7 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; ID_UPPER: ([A-Z][a-zA-Z0-9]*); -ENUM_CALL: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*; +ENUM: [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_#]*; 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 df5b8ccc3..eefc1e11b 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 @@ -239,11 +239,9 @@ private List getArgs(ArgsContext args) throws LJError { } private Enumerate enumCreate(EnumContext enumContext) { - String enumText = enumContext.enumCall().getText(); - int lastDot = enumText.lastIndexOf('.'); - String enumTypeName = enumText.substring(0, lastDot); - String enumConstName = enumText.substring(lastDot + 1); - return new Enumerate(enumTypeName, enumConstName); + String enumText = enumContext.enumerate().getText(); + String[] parts = enumText.split("\\."); + return new Enumerate(parts[0], parts[1]); } private Expression literalCreate(LiteralContext literalContext) throws LJError { From aafde534ffefc2f9143de34c80f14d47d6dc03fb Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 11 Mar 2026 12:19:07 +0000 Subject: [PATCH 11/13] Moved RefinementMessage test Moved and refactored the RefinmentMessage test to be a very simple Refinement checker. --- .../java/testSuite/CorrectEnumRefinement.java | 15 +++++++++++++++ .../testingInProgress/EnumRefinementMessage.java | 15 --------------- 2 files changed, 15 insertions(+), 15 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java delete mode 100644 liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java new file mode 100644 index 000000000..3b261d8e4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class CorrectEnumRefinement { + enum Lever { + Up, Down, Middle + } + + public static void main(String[] args) { + @Refinement("_==Lever.Up || _==Lever.Down") + Lever lever = Lever.Up; + System.out.println(lever); + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java deleted file mode 100644 index 2c8e0f1dd..000000000 --- a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java +++ /dev/null @@ -1,15 +0,0 @@ -package testingInProgress; - -import liquidjava.specification.Refinement; - -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 7a7e074774a0603ecdadd6e4dedf9fe05d58d4e2 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 11 Mar 2026 16:09:10 +0000 Subject: [PATCH 12/13] Changed Enumerate to Enum --- .../rj_language/ast/{Enumerate.java => Enum.java} | 10 +++++----- .../rj_language/visitors/CreateASTVisitor.java | 6 +++--- .../rj_language/visitors/ExpressionVisitor.java | 4 ++-- .../java/liquidjava/smt/ExpressionToZ3Visitor.java | 4 ++-- 4 files changed, 12 insertions(+), 12 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/{Enumerate.java => Enum.java} (86%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java similarity index 86% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java index 7f9341c1e..a790e16d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java @@ -5,12 +5,12 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; -public class Enumerate extends Expression { +public class Enum extends Expression { private final String enumTypeName; private final String enumConstantName; - public Enumerate(String enumTypeName, String enumConstantName) { + public Enum(String enumTypeName, String enumConstantName) { this.enumTypeName = enumTypeName; this.enumConstantName = enumConstantName; } @@ -25,7 +25,7 @@ public String getEnumConstantName() { @Override public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitEnumerate(this); + return visitor.visitEnum(this); } @Override @@ -63,12 +63,12 @@ public boolean equals(Object obj) { return true; if (obj == null || getClass() != obj.getClass()) return false; - Enumerate other = (Enumerate) obj; + Enum other = (Enum) obj; return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName); } @Override public Expression clone() { - return new Enumerate(enumTypeName, enumConstantName); + return new Enum(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 eefc1e11b..5efee64f1 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,7 +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.Enum; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; @@ -238,10 +238,10 @@ private List getArgs(ArgsContext args) throws LJError { return le; } - private Enumerate enumCreate(EnumContext enumContext) { + private Enum enumCreate(EnumContext enumContext) { String enumText = enumContext.enumerate().getText(); String[] parts = enumText.split("\\."); - return new Enumerate(parts[0], parts[1]); + return new Enum(parts[0], parts[1]); } 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 4b9808fc1..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 @@ -3,7 +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.Enum; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -41,7 +41,7 @@ public interface ExpressionVisitor { T visitUnaryExpression(UnaryExpression exp) throws LJError; - T visitEnumerate(Enumerate en) 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 9da522d96..8570d10c9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -5,7 +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.Enum; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -123,7 +123,7 @@ public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { } @Override - public Expr visitEnumerate(Enumerate en) throws LJError { + public Expr visitEnum(Enum en) throws LJError { return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName()); } } From 96905c1ce4ddb7f29a4fcf2a857147816117b4d4 Mon Sep 17 00:00:00 2001 From: Daniel <101189638+cheestree@users.noreply.github.com> Date: Wed, 11 Mar 2026 16:15:14 +0000 Subject: [PATCH 13/13] Renamed fields and getters/setters --- .../java/liquidjava/rj_language/ast/Enum.java | 28 +++++++++---------- .../liquidjava/smt/ExpressionToZ3Visitor.java | 2 +- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java index a790e16d2..17c8e17b6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.java @@ -7,20 +7,20 @@ public class Enum extends Expression { - private final String enumTypeName; - private final String enumConstantName; + private final String typeName; + private final String constName; - public Enum(String enumTypeName, String enumConstantName) { - this.enumTypeName = enumTypeName; - this.enumConstantName = enumConstantName; + public Enum(String typeName, String constName) { + this.typeName = typeName; + this.constName = constName; } - public String getEnumTypeName() { - return enumTypeName; + public String getTypeName() { + return typeName; } - public String getEnumConstantName() { - return enumConstantName; + public String getConstName() { + return constName; } @Override @@ -45,15 +45,15 @@ public boolean isBooleanTrue() { @Override public String toString() { - return enumTypeName + "." + enumConstantName; + return typeName + "." + constName; } @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()); + result = prime * result + ((typeName == null) ? 0 : typeName.hashCode()); + result = prime * result + ((constName == null) ? 0 : constName.hashCode()); return result; } @@ -64,11 +64,11 @@ public boolean equals(Object obj) { if (obj == null || getClass() != obj.getClass()) return false; Enum other = (Enum) obj; - return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName); + return typeName.equals(other.typeName) && constName.equals(other.constName); } @Override public Expression clone() { - return new Enum(enumTypeName, enumConstantName); + return new Enum(typeName, constName); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 8570d10c9..8bb46c05d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -124,6 +124,6 @@ public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { @Override public Expr visitEnum(Enum en) throws LJError { - return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName()); + return ctx.makeEnum(en.getTypeName(), en.getConstName()); } }