Added enum type support with tests

cheestree · cheestree · commit a08dbad873b6 · 2026-03-03T00:45:55.000Z
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java 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();
+	}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java 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
+	}
+}
diff --git 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
@@ -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 <R> void visitCtMethod(CtMethod<R> method) {
         }
         context.exitContext();
     }
+
+    @Override
+    public <T extends Enum<?>> void visitCtEnum(CtEnum<T> 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
@@ -269,7 +269,11 @@ public <T> void visitCtFieldRead(CtFieldRead<T> 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
@@ -19,13 +19,15 @@
 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;
 import org.apache.commons.lang3.NotImplementedException;
 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<Expression> 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
@@ -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
@@ -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";
 }

Original file line number	Diff line number	Diff line change
`@@ -5,4 +5,5 @@ public final class Formats {`
`5`	`5`	`public static final String INSTANCE = "#%s_%d";`
`6`	`6`	`public static final String THIS = "this#%s";`
`7`	`7`	`public static final String RET = "#ret_%d";`
	`8`	`+ public static final String ENUM_VALUE = "enum#%s#%s";`
`8`	`9`	`}`