Added enum types and verification

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();
+	}
+}

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
+	}
+}

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);
+    }
+}

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: 
+	ENUM_CALL;
+
 args:	pred (',' pred)* ;
 
 
@@ -94,6 +98,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_]*;
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
 ID     	: '#'*[a-zA-Z_][a-zA-Z0-9_#]*;

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);
+    }
 }

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?

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> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitEnumerate(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 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);
+    }
+}

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;
@@ -19,13 +20,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 +159,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 enumCreate((EnumContext) rc);
         } else {
             return create(((InvocationContext) rc).functionCall());
         }
@@ -234,6 +238,14 @@ private List<Expression> getArgs(ArgsContext args) throws LJError {
         return le;
     }
 
+    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);
+    }
+
     private Expression literalCreate(LiteralContext literalContext) throws LJError {
         if (literalContext.BOOL() != null)
             return new LiteralBoolean(literalContext.BOOL().getText());

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> {
 
     T visitUnaryExpression(UnaryExpression exp) throws LJError;
 
+    T visitEnumerate(Enumerate en) throws LJError;
+
     T visitVar(Var var) throws LJError;
 }

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());
+    }
 }