Add Support for Char Literals (#153)

rcosta358 · web-flow · commit 1bd08b45396c · 2026-02-23T13:41:08.000Z
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectChars.java b/liquidjava-example/src/main/java/testSuite/CorrectChars.java
@@ -0,0 +1,36 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectChars {
+
+    @Refinement("_ == 65")
+    int getA() {
+        return 'A';
+    }
+
+    void test() {
+        printLetter('A');
+        printLetter('Z');
+        printLetter('a');
+        printLetter('z');
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+
+    void test2() {
+        @Refinement("_ == 97")
+        char c = 'a';
+        
+        @Refinement("_ == 98")
+        int res = inc(c);
+    }
+
+    @Refinement("_ == x + 1")
+    int inc(int x) {
+        return x + 1;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java
@@ -0,0 +1,15 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorChars {
+
+    void test() {
+        printLetter('$'); // error
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
@@ -94,6 +94,7 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
             String retType = sg.getReturnType().toString();
             Predicate typePredicate = switch (retType) {
             case "int" -> Predicate.createLit("0", Types.INT);
+            case "char" -> Predicate.createLit("\u0000", Types.CHAR);
             case "boolean" -> Predicate.createLit("false", Types.BOOLEAN);
             case "double" -> Predicate.createLit("0.0", Types.DOUBLE);
             default -> throw new RuntimeException("Ghost not implemented for type " + retType);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -20,6 +20,7 @@
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
@@ -236,6 +237,7 @@ public static Predicate createLit(String value, String type) {
         case Types.INT, Types.SHORT -> new LiteralInt(value);
         case Types.LONG -> new LiteralLong(value);
         case Types.DOUBLE, Types.FLOAT -> new LiteralReal(value);
+        case Types.CHAR -> new LiteralChar(value);
         default -> throw new IllegalArgumentException("Unsupported literal type: " + type);
         };
         return new Predicate(exp);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
@@ -56,7 +56,7 @@ public void setChild(int index, Expression element) {
 
     public boolean isLiteral() {
         return this instanceof LiteralInt || this instanceof LiteralLong || this instanceof LiteralReal
-                || this instanceof LiteralBoolean;
+                || this instanceof LiteralBoolean || this instanceof LiteralChar;
     }
 
     /**
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralChar.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralChar.java
@@ -0,0 +1,70 @@
+package liquidjava.rj_language.ast;
+
+import java.util.List;
+
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
+
+public class LiteralChar extends Expression {
+
+    private final char value;
+
+    public LiteralChar(char value) {
+        this.value = value;
+    }
+
+    public LiteralChar(String value) {
+        this.value = value.charAt(0);
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitLiteralChar(this);
+    }
+
+    public char getValue() {
+        return value;
+    }
+
+    @Override
+    public String toString() {
+        return "'" + value + "'";
+    }
+
+    @Override
+    public void getVariableNames(List<String> toAdd) {
+        // end leaf
+    }
+
+    @Override
+    public void getStateInvocations(List<String> toAdd, List<String> all) {
+        // end leaf
+    }
+
+    @Override
+    public Expression clone() {
+        return new LiteralChar(value);
+    }
+
+    @Override
+    public boolean isBooleanTrue() {
+        return false;
+    }
+
+    @Override
+    public int hashCode() {
+        return Character.hashCode(value);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null)
+            return false;
+        if (getClass() != obj.getClass())
+            return false;
+        LiteralChar other = (LiteralChar) obj;
+        return value == other.value;
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
@@ -10,6 +10,7 @@
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
@@ -38,6 +39,8 @@ else if (e instanceof LiteralLong)
             return Optional.of(Utils.getType("long", factory));
         else if (e instanceof LiteralReal)
             return Optional.of(Utils.getType("double", factory));
+        else if (e instanceof LiteralChar)
+            return Optional.of(Utils.getType("char", factory));
         else if (e instanceof LiteralBoolean)
             return boolType(factory);
         else if (e instanceof Var)
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
@@ -7,6 +7,7 @@
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
@@ -31,6 +32,8 @@ public interface ExpressionVisitor<T> {
 
     T visitLiteralBoolean(LiteralBoolean lit) throws LJError;
 
+    T visitLiteralChar(LiteralChar lit) throws LJError;
+
     T visitLiteralReal(LiteralReal lit) throws LJError;
 
     T visitLiteralString(LiteralString lit) throws LJError;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
@@ -9,6 +9,7 @@
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralChar;
 import liquidjava.rj_language.ast.LiteralInt;
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
@@ -96,6 +97,11 @@ public Expr<?> visitLiteralBoolean(LiteralBoolean lit) {
         return ctx.makeBooleanLiteral(lit.isBooleanTrue());
     }
 
+    @Override
+    public Expr<?> visitLiteralChar(LiteralChar lit) {
+        return ctx.makeIntegerLiteral(lit.getValue());
+    }
+
     @Override
     public Expr<?> visitLiteralReal(LiteralReal lit) {
         return ctx.makeDoubleLiteral(lit.getValue());
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
@@ -42,7 +42,8 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
     private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
         String typeName = type.getQualifiedName();
         return switch (typeName) {
-        case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.mkIntConst(name);
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3
+                .mkIntConst(name);
         case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
         case "long", "java.lang.Long" -> z3.mkRealConst(name);
         case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
@@ -81,7 +82,7 @@ private static void addBuiltinFunctions(Context z3, Map<String, FuncDecl<?>> fun
 
     static Sort getSort(Context z3, String sort) {
         return switch (sort) {
-        case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.getIntSort();
+        case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3.getIntSort();
         case "boolean", "java.lang.Boolean" -> z3.getBoolSort();
         case "long", "java.lang.Long" -> z3.getRealSort();
         case "float", "java.lang.Float" -> z3.mkFPSort32();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java
@@ -10,6 +10,7 @@ public class Types {
     public static final String SHORT = "short";
     public static final String LONG = "long";
     public static final String FLOAT = "float";
+    public static final String CHAR = "char";
     public static final String NULL = "<nulltype>";
-    public static final String[] IMPLEMENTED = { "boolean", "int", "short", "long", "float", "double" };
+    public static final String[] IMPLEMENTED = { "boolean", "int", "short", "long", "float", "double", "char" };
 }

Original file line number	Diff line number	Diff line change
`@@ -56,7 +56,7 @@ public void setChild(int index, Expression element) {`
`56`	`56`
`57`	`57`	`public boolean isLiteral() {`
`58`	`58`	`return this instanceof LiteralInt \|\| this instanceof LiteralLong \|\| this instanceof LiteralReal`
`59`		`- \|\| this instanceof LiteralBoolean;`
	`59`	`+ \|\| this instanceof LiteralBoolean \|\| this instanceof LiteralChar;`
`60`	`60`	`}`
`61`	`61`
`62`	`62`	`/**`