diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java new file mode 100644 index 00000000..0d0d0957 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -0,0 +1,33 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@SuppressWarnings("unused") +@StateSet({"photoMode", "videoMode", "noMode"}) +class CorrectEnumUsage { + enum Mode { + Photo, Video, Unknown + } + + Mode mode; + @StateRefinement(to="noMode(this)") + public CorrectEnumUsage() {} + + @StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)") + @StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)") + public void setMode(Mode mode) { + this.mode = mode; + } + + @StateRefinement(from="photoMode(this)") + public void takePhoto() {} + + + public static void main(String[] args) { + // Correct + CorrectEnumUsage st = new CorrectEnumUsage(); + st.setMode(Mode.Photo); + st.takePhoto(); + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java new file mode 100644 index 00000000..57e6818e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java @@ -0,0 +1,35 @@ +// State Refinement Error +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + + +@SuppressWarnings("unused") +@StateSet({"photoMode", "videoMode", "noMode"}) +class ErrorEnumUsage { + enum Mode { + Photo, Video, Unknown + } + + Mode mode; + @StateRefinement(to="noMode(this)") + public ErrorEnumUsage() {} + + @StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)") + @StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)") + public void setMode(Mode mode) { + this.mode = mode; + } + + @StateRefinement(from="photoMode(this)") + public void takePhoto() {} + + + public static void main(String[] args) { + // Correct + ErrorEnumUsage st = new ErrorEnumUsage(); + st.setMode(Mode.Video); + st.takePhoto(); //error + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java new file mode 100644 index 00000000..fcba04ba --- /dev/null +++ b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java @@ -0,0 +1,15 @@ +package testingInProgress; + +import liquidjava.specification.Refinement; + +public class EnumRefinementMessage { + enum Mode { + Photo, Video, Unknown + } + + public static void main(String[] args) { + @Refinement("_==Mode.Photo") + Mode test = Mode.Video; + System.out.println(test); + } +} diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index d6f7f45f..b2ac847c 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: + 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_#]*; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index e764d453..581b4644 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -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 void visitCtMethod(CtMethod method) { } context.exitContext(); } + + @Override + public > void visitCtEnum(CtEnum 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 index d3d95bbd..82988819 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -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, 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/Enumerate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java new file mode 100644 index 00000000..7f9341c1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java @@ -0,0 +1,74 @@ +package liquidjava.rj_language.ast; + +import java.util.List; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; + +public class Enumerate extends Expression { + + private final String enumTypeName; + private final String enumConstantName; + + public Enumerate(String enumTypeName, String enumConstantName) { + this.enumTypeName = enumTypeName; + this.enumConstantName = enumConstantName; + } + + public String getEnumTypeName() { + return enumTypeName; + } + + public String getEnumConstantName() { + return enumConstantName; + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitEnumerate(this); + } + + @Override + public void getVariableNames(List toAdd) { + // end leaf + } + + @Override + public void getStateInvocations(List toAdd, List all) { + // end leaf + } + + @Override + public boolean isBooleanTrue() { + return false; + } + + @Override + public String toString() { + return enumTypeName + "." + enumConstantName; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + ((enumTypeName == null) ? 0 : enumTypeName.hashCode()); + result = prime * result + ((enumConstantName == null) ? 0 : enumConstantName.hashCode()); + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null || getClass() != obj.getClass()) + return false; + Enumerate other = (Enumerate) obj; + return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName); + } + + @Override + public Expression clone() { + return new Enumerate(enumTypeName, enumConstantName); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index d906772c..df5b8ccc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -7,6 +7,7 @@ import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; @@ -19,6 +20,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 +28,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 +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 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()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java index e3db3938..4b9808fc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -3,6 +3,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -40,5 +41,7 @@ public interface ExpressionVisitor { T visitUnaryExpression(UnaryExpression exp) throws LJError; + T visitEnumerate(Enumerate en) throws LJError; + T visitVar(Var var) throws LJError; } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 4a45b1d8..9da522d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -5,6 +5,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Enumerate; import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; @@ -120,4 +121,9 @@ public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { default -> null; }; } + + @Override + public Expr visitEnumerate(Enumerate en) throws LJError { + return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName()); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index c660d12b..76a20bea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -1,11 +1,13 @@ 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; 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; @@ -13,20 +15,51 @@ import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; +import spoon.reflect.declaration.CtEnum; 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<>(); - for (String name : ctx.keySet()) - varTranslation.put(name, getExpr(z3, name, ctx.get(name))); + for (Map.Entry> entry : ctx.entrySet()) { + String name = entry.getKey(); + CtTypeReference type = entry.getValue(); + + 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; + } + varTranslation.put(name, getExpr(z3, name, type)); + } varTranslation.put("true", z3.mkBool(true)); varTranslation.put("false", z3.mkBool(false)); } + 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, Map>> varSuperTypes) { for (RefinedVariable v : variables) { @@ -41,6 +74,7 @@ public static void storeVariablesSubtypes(Context z3, List vari private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); + return switch (typeName) { case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3 .mkIntConst(name); @@ -88,6 +122,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/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..02fed44a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -3,6 +3,7 @@ import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.EnumSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; @@ -26,6 +27,7 @@ import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import com.microsoft.z3.enumerations.Z3_sort_kind; @@ -119,6 +121,11 @@ public Expr makeVariable(String name) throws LJError { return expr; } + public Expr makeEnum(String enumTypeName, String enumConstantName) throws LJError { + String varName = String.format(Formats.ENUM, enumTypeName, enumConstantName); + return getVariableTranslation(varName); + } + public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { if (name.equals("addToIndex")) return makeStore(params); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java index f3ae77f0..7bd8557e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -5,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 = "%s.%s"; } \ No newline at end of file