Skip to content

Commit 3d7fb5d

Browse files
cheestreecheestree
committed
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.
1 parent 3835584 commit 3d7fb5d

10 files changed

Lines changed: 118 additions & 23 deletions

File tree

‎liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ aliasCall:
5757
ID_UPPER '(' args? ')';
5858

5959
enumCall:
60-
OBJECT_TYPE;
60+
ENUM_CALL;
6161

6262
args: pred (',' pred)* ;
6363

@@ -97,6 +97,7 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<';
9797
ARITHOP : '+'|'*'|'/'|'%';//|'-';
9898

9999
BOOL : 'true' | 'false';
100+
ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*;
100101
ID_UPPER: ([A-Z][a-zA-Z0-9]*);
101102
OBJECT_TYPE:
102103
(([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java‎

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -126,13 +126,9 @@ public <R> void visitCtMethod(CtMethod<R> method) {
126126
public <T extends Enum<?>> void visitCtEnum(CtEnum<T> enumRead) {
127127
String enumName = enumRead.getSimpleName();
128128
String qualifiedEnumName = enumRead.getQualifiedName();
129-
int ordinal = 0;
130-
for (CtEnumValue ev : enumRead.getEnumValues()) {
131-
String varName = String.format(Formats.ENUM_VALUE, enumName, ev.getSimpleName());
132-
Predicate refinement = Predicate.createEquals(Predicate.createVar(varName),
133-
Predicate.createLit(String.valueOf(ordinal), Types.INT));
134-
context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), refinement);
135-
ordinal++;
129+
for (CtEnumValue<?> ev : enumRead.getEnumValues()) {
130+
String varName = String.format(Formats.ENUM, enumName, ev.getSimpleName());
131+
context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), null);
136132
}
137133
super.visitCtEnum(enumRead);
138134
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,7 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
271271
BuiltinFunctionPredicate.length(targetName, fieldRead)));
272272
} else if (fieldRead.getVariable().getDeclaringType().isEnum()) {
273273
String target = fieldRead.getVariable().getDeclaringType().getSimpleName();
274-
String enumLiteral = String.format(Formats.ENUM_VALUE, target, fieldName);
274+
String enumLiteral = String.format(Formats.ENUM, target, fieldName);
275275
fieldRead.putMetadata(Keys.REFINEMENT,
276276
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral)));
277277
} else {

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
package liquidjava.rj_language.ast;
2+
3+
import java.util.List;
4+
5+
import liquidjava.diagnostics.errors.LJError;
6+
import liquidjava.rj_language.visitors.ExpressionVisitor;
7+
8+
public class Enumerate extends Expression {
9+
10+
private final String enumTypeName;
11+
private final String enumConstantName;
12+
13+
public Enumerate(String enumTypeName, String enumConstantName) {
14+
this.enumTypeName = enumTypeName;
15+
this.enumConstantName = enumConstantName;
16+
}
17+
18+
public String getEnumTypeName() {
19+
return enumTypeName;
20+
}
21+
22+
public String getEnumConstantName() {
23+
return enumConstantName;
24+
}
25+
26+
@Override
27+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
28+
return visitor.visitEnumerate(this);
29+
}
30+
31+
@Override
32+
public void getVariableNames(List<String> toAdd) {
33+
// end leaf
34+
}
35+
36+
@Override
37+
public void getStateInvocations(List<String> toAdd, List<String> all) {
38+
// end leaf
39+
}
40+
41+
@Override
42+
public boolean isBooleanTrue() {
43+
return false;
44+
}
45+
46+
@Override
47+
public String toString() {
48+
return enumTypeName + "." + enumConstantName;
49+
}
50+
51+
@Override
52+
public int hashCode() {
53+
final int prime = 31;
54+
int result = 1;
55+
result = prime * result + ((enumTypeName == null) ? 0 : enumTypeName.hashCode());
56+
result = prime * result + ((enumConstantName == null) ? 0 : enumConstantName.hashCode());
57+
return result;
58+
}
59+
60+
@Override
61+
public boolean equals(Object obj) {
62+
if (this == obj)
63+
return true;
64+
if (obj == null || getClass() != obj.getClass())
65+
return false;
66+
Enumerate other = (Enumerate) obj;
67+
return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName);
68+
}
69+
70+
@Override
71+
public Expression clone() {
72+
return new Enumerate(enumTypeName, enumConstantName);
73+
}
74+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import liquidjava.diagnostics.errors.SyntaxError;
88
import liquidjava.rj_language.ast.AliasInvocation;
99
import liquidjava.rj_language.ast.BinaryExpression;
10+
import liquidjava.rj_language.ast.Enumerate;
1011
import liquidjava.rj_language.ast.Expression;
1112
import liquidjava.rj_language.ast.FunctionInvocation;
1213
import liquidjava.rj_language.ast.GroupExpression;
@@ -161,7 +162,7 @@ else if (rc instanceof LitContext)
161162
else if (rc instanceof VarContext)
162163
return new Var(((VarContext) rc).ID().getText());
163164
else if (rc instanceof EnumContext) {
164-
return new Var(enumCreate((EnumContext) rc));
165+
return enumCreate((EnumContext) rc);
165166
} else {
166167
return create(((InvocationContext) rc).functionCall());
167168
}
@@ -237,13 +238,12 @@ private List<Expression> getArgs(ArgsContext args) throws LJError {
237238
return le;
238239
}
239240

240-
private String enumCreate(EnumContext rc) {
241-
String enumText = rc.enumCall().getText();
241+
private Enumerate enumCreate(EnumContext enumContext) {
242+
String enumText = enumContext.enumCall().getText();
242243
int lastDot = enumText.lastIndexOf('.');
243-
String enumClass = enumText.substring(0, lastDot);
244-
String enumConst = enumText.substring(lastDot + 1);
245-
String varName = String.format(Formats.ENUM_VALUE, enumClass, enumConst);
246-
return varName;
244+
String enumTypeName = enumText.substring(0, lastDot);
245+
String enumConstName = enumText.substring(lastDot + 1);
246+
return new Enumerate(enumTypeName, enumConstName);
247247
}
248248

249249
private Expression literalCreate(LiteralContext literalContext) throws LJError {

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import liquidjava.diagnostics.errors.LJError;
44
import liquidjava.rj_language.ast.AliasInvocation;
55
import liquidjava.rj_language.ast.BinaryExpression;
6+
import liquidjava.rj_language.ast.Enumerate;
67
import liquidjava.rj_language.ast.FunctionInvocation;
78
import liquidjava.rj_language.ast.GroupExpression;
89
import liquidjava.rj_language.ast.Ite;
@@ -40,5 +41,7 @@ public interface ExpressionVisitor<T> {
4041

4142
T visitUnaryExpression(UnaryExpression exp) throws LJError;
4243

44+
T visitEnumerate(Enumerate en) throws LJError;
45+
4346
T visitVar(Var var) throws LJError;
4447
}

‎liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import liquidjava.diagnostics.errors.LJError;
66
import liquidjava.rj_language.ast.AliasInvocation;
77
import liquidjava.rj_language.ast.BinaryExpression;
8+
import liquidjava.rj_language.ast.Enumerate;
89
import liquidjava.rj_language.ast.FunctionInvocation;
910
import liquidjava.rj_language.ast.GroupExpression;
1011
import liquidjava.rj_language.ast.Ite;
@@ -120,4 +121,9 @@ public Expr<?> visitUnaryExpression(UnaryExpression exp) throws LJError {
120121
default -> null;
121122
};
122123
}
124+
125+
@Override
126+
public Expr<?> visitEnumerate(Enumerate en) throws LJError {
127+
return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName());
128+
}
123129
}

‎liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java‎

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package liquidjava.smt;
22

33
import com.microsoft.z3.Context;
4+
import com.microsoft.z3.EnumSort;
45
import com.microsoft.z3.Expr;
56
import com.microsoft.z3.FPExpr;
67
import com.microsoft.z3.FuncDecl;
@@ -13,6 +14,8 @@
1314
import liquidjava.processor.context.GhostFunction;
1415
import liquidjava.processor.context.GhostState;
1516
import liquidjava.processor.context.RefinedVariable;
17+
import spoon.reflect.declaration.CtEnum;
18+
import spoon.reflect.declaration.CtType;
1619
import spoon.reflect.reference.CtTypeReference;
1720

1821
public class TranslatorContextToZ3 {
@@ -41,19 +44,24 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
4144

4245
private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
4346
String typeName = type.getQualifiedName();
47+
48+
if (type.isEnum()) {
49+
CtType<?> decl = type.getDeclaration();
50+
if (decl instanceof CtEnum<?> enumDecl) {
51+
String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()).toArray(String[]::new);
52+
EnumSort<Object> enumSort = z3.mkEnumSort(typeName, enumValueNames);
53+
return z3.mkConst(name, enumSort);
54+
}
55+
}
56+
4457
return switch (typeName) {
4558
case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3
4659
.mkIntConst(name);
4760
case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
4861
case "long", "java.lang.Long" -> z3.mkRealConst(name);
4962
case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
5063
case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort());
51-
case "java.lang.Enum" -> z3.mkIntConst(name);
52-
default -> {
53-
if (type.isEnum())
54-
yield z3.mkIntConst(name);
55-
yield z3.mkConst(name, z3.mkUninterpretedSort(typeName));
56-
}
64+
default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName));
5765
};
5866
}
5967

‎liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import com.microsoft.z3.ArithExpr;
44
import com.microsoft.z3.ArrayExpr;
55
import com.microsoft.z3.BoolExpr;
6+
import com.microsoft.z3.EnumSort;
67
import com.microsoft.z3.Expr;
78
import com.microsoft.z3.FPExpr;
89
import com.microsoft.z3.FuncDecl;
@@ -26,6 +27,7 @@
2627
import liquidjava.diagnostics.errors.NotFoundError;
2728
import liquidjava.processor.context.AliasWrapper;
2829
import liquidjava.utils.Utils;
30+
import liquidjava.utils.constants.Formats;
2931
import liquidjava.utils.constants.Keys;
3032
import com.microsoft.z3.enumerations.Z3_sort_kind;
3133

@@ -119,6 +121,11 @@ public Expr<?> makeVariable(String name) throws LJError {
119121
return expr;
120122
}
121123

124+
public Expr<?> makeEnum(String enumTypeName, String enumConstantName) throws LJError {
125+
String varName = String.format(Formats.ENUM, enumTypeName, enumConstantName);
126+
return getVariableTranslation(varName);
127+
}
128+
122129
public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJError {
123130
if (name.equals("addToIndex"))
124131
return makeStore(params);

‎liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ public final class Formats {
55
public static final String INSTANCE = "#%s_%d";
66
public static final String THIS = "this#%s";
77
public static final String RET = "#ret_%d";
8-
public static final String ENUM_VALUE = "enum#%s#%s";
8+
public static final String ENUM = "%s.%s";
99
}

0 commit comments

Comments
 (0)