Add Support for Char Literals

Author: rcosta358

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

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

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;
     }
 
     /**

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

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;
@@ -40,6 +41,8 @@ else if (e instanceof LiteralReal)
             return Optional.of(Utils.getType("double", factory));
         else if (e instanceof LiteralBoolean)
             return boolType(factory);
+        else if (e instanceof LiteralChar)
+            return Optional.of(Utils.getType("char", factory));
         else if (e instanceof Var)
             return varType(ctx, (Var) e);
         else if (e instanceof UnaryExpression)

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;

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

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