Added enum types and verification by cheestree · Pull Request #168 · liquid-java/liquidjava

cheestree · 2026-03-03T18:20:23Z

This would fix #23 with the addition of enum types and verifications.

The grammar was implemented taking into consideration the concerns of verbosity and ambiguity. The solution developed uses a Enum.Value format, as Value formats were failing due to ambiguity. This was discussed briefly with @rcosta358 in regards to using something like enum() instead, but it was found a bit too off/verbose.

The default branch in TranslatorContextToZ3 was changed. Enum types fall into a sort-of fallback option due to being treated as an OBJECT_TYPE. By checking if the type is, in fact, an enum, other cases can fall into mkUninterpretedSort.
The field metadata is inserted similarly to other types, but with a specific format (ENUM_VALUE).

Treating an enum as an OBJECT_TYPE is the main "issue" I'm having, as it looks as though it's being treated as a fallback approach due to dot consumption early on. However, this might be my lack of experience.

Another visual issue that I had was the Refinement Error message (as shown in EnumRefinementMessage), as it's not clear enough as to why the refinement failed.

Added a test for enums to, in the future, help clean the refinement message.

rcosta358

Nice work! Left some feedback about the parsing, representation, scoping and translation of enums.
Additionally, we need more tests to verify the correctness of this implementation.

rcosta358 · 2026-03-04T14:35:16Z

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

 	ID_UPPER '(' args? ')';

+enumCall: 
+	OBJECT_TYPE;


I understand you used OBJECT_TYPE because of the rule ambiguity. However, this raises a concern, because it allows for multiple chaining of ids (e.g., Mode.photo.photo, Mode.photo.photo.photo, etc.) which should not be syntactically valid.

We could avoid the ambiguity by forcing the OBJECT_TYPE to always start with a lowercase letter and declare enumCall as ID '.' ID, but Java packages are allowed start with an uppercase letter (even though it's highly discouraged).

So, we can introduce another terminal, just for enums:

enumCall: ENUM_CALL; // ... ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*;

This way, you guarantee the enums are always represented by two ids separated by a dot, without ambiguity.

That's understandable, my issue with that, at the time of development, was if ID and ID_UPPER wouldn't, even if they are slightly different, lead to ambiguity due to other grammar rules. I should've explored more formats.

rcosta358 · 2026-03-04T14:38:24Z

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

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


I don't like the "enum#%s#%s" format because it's hard to read in the error messages. Here you can simply return the enumText, and everywhere else still use this format but change it to "%s.%s" instead.

I should've gone with a better format, I admit. I wasn't sure due to the rest of the existing types.

rcosta358 · 2026-03-04T14:38:51Z

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

            return new Var(((VarContext) rc).ID().getText());
-
+        else if (rc instanceof EnumContext) {
+            return new Var(enumCreate((EnumContext) rc));


I don't think the enums should be represented as variables. They should have its own AST node and also its own representation in the context.

rcosta358 · 2026-03-04T14:54:00Z

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

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


Why global? Shouldn't it only be visible within the class or package where it was declared?

If there is an enum that is used across methods, and a shared package is needed, when the context is reinitialized, the local context is cleaned. If it's kept in the global context, the placement is irrelevant.
For example, the following common package a layer above the testSuite.

When line 134 is changed to context.addVarToContext(varName, enumRead.getReference(), refinement, enumRead), the following occurs:

That's not really a shared package because it's not even included in the verification, each test is ran individually from its file or folder.

The issue is: if I declare an enum X in class A, should I be able to use it in class B? It might be fine, just raising some questions about how it should work.

Also, if we can use enums from different classes, we should make sure they have their fully qualified name to distinguish enums with the same name from different classes.

I didn't realize the testing was that restrictive. I can try and create some test scenarios that take into consideration global and local context. The other option would be to restrict enum verification to only in the same file, but that feels like a cop-out instead of an actual fix/intended functionality. 🤔

rcosta358 · 2026-03-04T14:55:52Z

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

    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";


Suggested change

public static final String ENUM_VALUE = "enum#%s#%s";

public static final String ENUM = "%s.%s";

rcosta358 · 2026-03-04T15:04:48Z

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

+        case "java.lang.Enum" -> z3.mkIntConst(name);
+        default -> {
+            if (type.isEnum())
+                yield z3.mkIntConst(name);
+            yield z3.mkConst(name, z3.mkUninterpretedSort(typeName));
+        }


Converting the enums to integers is makes sense, but we can improve it. Instead, we can use the Z3 EnumSort, so the error messages and the counterexamples show the enum values instead of the integers they represent, which I can help you with.

rcosta358 · 2026-03-04T15:14:23Z

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

+        int ordinal = 0;
+        for (CtEnumValue ev : enumRead.getEnumValues()) {


Using a traditional for loop here might be a good idea, but that's also fine. Also, you should use CtEnumValue<?> here.

Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format.

cheestree · 2026-03-04T19:53:27Z

The change to using EnumSort seems to have worked, but I'm still unsure of how exactly tests for this should be created if some problematic areas are based off of package/class location. Is there a currently implemented test that runs off of its own folder and has multiple components in different files?

rcosta358 · 2026-03-04T20:00:07Z

Currently every test file/folder is verified completely isolated from one another. Everything needed for it should be in the corresponding file/folder, even if that means unwanted repetition.

Fixed grammar so that it required uppercase start for both parts. Differentiates between types and calls.

This reverts commit c831921.

This reverts commit d785934.

cheestree added 2 commits March 3, 2026 00:45

Added enum type support with tests

a08dbad

Added EnumRefinementMessage test

3835584

Added a test for enums to, in the future, help clean the refinement message.

rcosta358 requested changes Mar 4, 2026

View reviewed changes

rcosta358 assigned cheestree Mar 4, 2026

rcosta358 added the enhancement New feature or request label Mar 4, 2026

Applied fixes and suggestions for enums

3d7fb5d

Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format.

cheestree added 3 commits March 4, 2026 20:07

Fixed grammar

c831921

Fixed grammar so that it required uppercase start for both parts. Differentiates between types and calls.

Revert "Fixed grammar"

d785934

This reverts commit c831921.

Reapply "Fixed grammar"

66e982f

This reverts commit d785934.

	public static final String ENUM_VALUE = "enum#%s#%s";
	public static final String ENUM = "%s.%s";

		int ordinal = 0;
		for (CtEnumValue ev : enumRead.getEnumValues()) {

Conversation

cheestree commented Mar 3, 2026

Uh oh!

rcosta358 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rcosta358 Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

cheestree commented Mar 4, 2026

Uh oh!

rcosta358 commented Mar 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

rcosta358 left a comment •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading

rcosta358 Mar 4, 2026 •

edited

Loading