diff --git a/liquidjava-example/src/main/java/testSuite/CorrectChars.java b/liquidjava-example/src/main/java/testSuite/CorrectChars.java new file mode 100644 index 00000000..6a8f6bd0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectChars.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +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); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorChars.java b/liquidjava-example/src/main/java/testSuite/ErrorChars.java new file mode 100644 index 00000000..cbaf4b1d --- /dev/null +++ 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 index facbd2c1..3ec62036 100644 --- 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 index eecfaa10..87e18a39 100644 --- 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 index 58ea8e93..3859c530 100644 --- 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 new file mode 100644 index 00000000..54756d29 --- /dev/null +++ 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 accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitLiteralChar(this); + } + + public char getValue() { + return value; + } + + @Override + public String toString() { + return "'" + value + "'"; + } + + @Override + public void getVariableNames(List toAdd) { + // end leaf + } + + @Override + public void getStateInvocations(List toAdd, List 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; + } +} \ No newline at end of file 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 index 085f015d..0fa965cd 100644 --- 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 index 52e37319..e3db3938 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 @@ -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 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 index 35e74803..4a45b1d8 100644 --- 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 index 08749a07..8e5ece7d 100644 --- 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 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> 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 index 39472de2..e71b277f 100644 --- 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 = ""; - public static final String[] IMPLEMENTED = { "boolean", "int", "short", "long", "float", "double" }; + public static final String[] IMPLEMENTED = { "boolean", "int", "short", "long", "float", "double", "char" }; } \ No newline at end of file