Added enum types and verification (#168)

cheestree · web-flow · commit a3b04c6bc48c · 2026-04-11T11:59:36.000+01:00
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java 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
@@ -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
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumRefinement.java 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/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java
@@ -0,0 +1,45 @@
+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)", 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);  // 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
@@ -0,0 +1,23 @@
+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;
+		return c;
+	}
+
+	public static void main(String[] args) {
+		ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement();
+		e.changeColor(Color.Red);
+		e.changeColor(Color.Blue); // Refinement Error
+	}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java
@@ -0,0 +1,18 @@
+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);
+        e.process(Status.Inactive); // Refinement Error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java
@@ -0,0 +1,15 @@
+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; // Refinement Error
+	}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java
@@ -0,0 +1,33 @@
+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(); // State Refinement Error
+	}
+}
diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
@@ -38,12 +38,14 @@ literalExpression:
 	|	literal						#lit
 	| 	ID 							#var
 	|	functionCall				#invocation
+	|	enumerate					#enum
 	;
 
- functionCall:
+functionCall:
  		ghostCall
  	|	aliasCall
-	|	dotCall;
+	|	dotCall
+	;
 
 dotCall:
 		OBJECT_TYPE '(' args? ')'
@@ -55,6 +57,9 @@ ghostCall:
 aliasCall:
 	ID_UPPER '(' args? ')';
 
+enumerate: 
+	ENUM;
+
 args:	pred (',' pred)* ;
 
 
@@ -94,6 +99,7 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-';
 
 BOOL    : 'true' | 'false';
 ID_UPPER: ([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/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,15 @@ 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();
+        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
@@ -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, 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/ast/Enum.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enum.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 Enum extends Expression {
+
+    private final String typeName;
+    private final String constName;
+
+    public Enum(String typeName, String constName) {
+        this.typeName = typeName;
+        this.constName = constName;
+    }
+
+    public String getTypeName() {
+        return typeName;
+    }
+
+    public String getConstName() {
+        return constName;
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitEnum(this);
+    }
+
+    @Override
+    public void getVariableNames(List<String> toAdd) {
+        // end leaf
+    }
+
+    @Override
+    public void getStateInvocations(List<String> toAdd, List<String> all) {
+        // end leaf
+    }
+
+    @Override
+    public boolean isBooleanTrue() {
+        return false;
+    }
+
+    @Override
+    public String toString() {
+        return typeName + "." + constName;
+    }
+
+    @Override
+    public int hashCode() {
+        final int prime = 31;
+        int result = 1;
+        result = prime * result + ((typeName == null) ? 0 : typeName.hashCode());
+        result = prime * result + ((constName == null) ? 0 : constName.hashCode());
+        return result;
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null || getClass() != obj.getClass())
+            return false;
+        Enum other = (Enum) obj;
+        return typeName.equals(other.typeName) && constName.equals(other.constName);
+    }
+
+    @Override
+    public Expression clone() {
+        return new Enum(typeName, constName);
+    }
+}
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
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
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java
