From 7a8de62da7bd87bfc7562b5d66455e8449914e1c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Feb 2026 22:04:36 +0000 Subject: [PATCH 1/4] Add Null & Boxed Types Support --- .../src/main/antlr4/rj/grammar/RJ.g4 | 4 +- .../RefinementTypeChecker.java | 15 +++++- .../general_checkers/OperationsChecker.java | 2 +- .../liquidjava/rj_language/Predicate.java | 11 ++++- .../rj_language/ast/Expression.java | 2 +- .../rj_language/ast/LiteralNull.java | 49 +++++++++++++++++++ .../rj_language/ast/typing/TypeInfer.java | 5 ++ .../rj_language/opt/ExpressionSimplifier.java | 40 +++++++++++++++ .../derivation_node/ValDerivationNode.java | 3 ++ .../visitors/CreateASTVisitor.java | 12 ++--- .../visitors/ExpressionVisitor.java | 3 ++ .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 +++ .../liquidjava/smt/TranslatorContextToZ3.java | 18 +++---- .../java/liquidjava/smt/TranslatorToZ3.java | 16 +++++- .../src/main/java/liquidjava/utils/Utils.java | 17 +++++++ 15 files changed, 179 insertions(+), 24 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralNull.java diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e34f40ad..1fe7b619 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -58,7 +58,8 @@ literal: BOOL | STRING | INT - | REAL; + | REAL + | NULL; //----------------------- Declarations ----------------------- @@ -89,6 +90,7 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<'; ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; +NULL : 'null'; ID_UPPER: ([A-Z][a-zA-Z0-9]*); OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 43791ccd..b5075e01 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -13,8 +13,11 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.LiteralNull; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import org.apache.commons.lang3.NotImplementedException; @@ -136,6 +139,9 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { if (refinementFound == null) { refinementFound = new Predicate(); } + if (Utils.isBoxedType(localVariable.getType()) && !Utils.isNullLiteral(e)) { + refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq()); + } context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); AuxStateHandler.addStateRefinements(this, varName, e); @@ -219,9 +225,9 @@ public void visitCtLiteral(CtLiteral lit) { Predicate.createLit(lit.getValue().toString(), type))); } else if (lit.getType().getQualifiedName().equals("java.lang.String")) { - // Only taking care of strings inside refinements + lit.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq()); } else if (type.equals(Types.NULL)) { - // Skip null literals + lit.putMetadata(Keys.REFINEMENT, Predicate.createNullEq()); } else { throw new NotImplementedException( String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName())); @@ -373,12 +379,14 @@ public void visitCtConditional(CtConditional conditional) { @Override public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { super.visitCtConstructorCall(ctConstructorCall); + ctConstructorCall.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq()); mfc.getConstructorInvocationRefinements(ctConstructorCall); } @Override public void visitCtNewClass(CtNewClass newClass) { super.visitCtNewClass(newClass); + newClass.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq()); } // ############################### Inner Visitors @@ -396,6 +404,9 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< refinementFound = new Predicate(); } } + if (Utils.isBoxedType(type) && !Utils.isNullLiteral(assignment)) { + refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq()); + } Optional r = context.getLastVariableInstance(name); // AQUI!! r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName())); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 779d68a9..bce8b594 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -221,7 +221,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return new Predicate(); } if (l.getValue() == null) - throw new CustomError("Null literals are not supported"); + return new Predicate("null", element); return new Predicate(l.getValue().toString(), element); 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 565de7e3..e299f77c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -6,9 +6,7 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.ArgumentMismatchError; import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -22,6 +20,7 @@ import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; @@ -255,4 +254,12 @@ public static Predicate createInvocation(String name, Predicate... Predicates) { le.add(c.getExpression()); return new Predicate(new FunctionInvocation(name, le)); } + + public static Predicate createNonNullEq() { + return Predicate.createOperation(Predicate.createVar(Keys.WILDCARD), Ops.NEQ, new Predicate(new LiteralNull())); + } + + public static Predicate createNullEq() { + return Predicate.createOperation(Predicate.createVar(Keys.WILDCARD), Ops.EQ, new Predicate(new LiteralNull())); + } } 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 9b4b2e17..761ad7c1 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 @@ -67,7 +67,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 LiteralNull; } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralNull.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralNull.java new file mode 100644 index 00000000..e7512eb0 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralNull.java @@ -0,0 +1,49 @@ +package liquidjava.rj_language.ast; + +import java.util.List; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; + +public class LiteralNull extends Expression { + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitLiteralNull(this); + } + + @Override + public String toString() { + return "null"; + } + + @Override + public void getVariableNames(List toAdd) { + // end leaf + } + + @Override + public void getStateInvocations(List toAdd, List all) { + // end leaf + } + + @Override + public Expression clone() { + return new LiteralNull(); + } + + @Override + public boolean isBooleanTrue() { + return false; + } + + @Override + public int hashCode() { + return 31; + } + + @Override + public boolean equals(Object obj) { + return obj != null && getClass() == obj.getClass(); + } +} 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..554a0303 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 @@ -12,6 +12,7 @@ import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -24,6 +25,8 @@ public class TypeInfer { public static boolean checkCompatibleType(String type, Expression e, Context ctx, Factory factory) { + if (e instanceof LiteralNull) + return !Utils.isPrimitiveType(type); Optional> t1 = getType(ctx, factory, e); CtTypeReference t2 = Utils.getType(type, factory); return t1.isPresent() && t1.get().equals(t2); @@ -40,6 +43,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 LiteralNull) + return Optional.of(Utils.getType("java.lang.Object", factory)); else if (e instanceof Var) return varType(ctx, (Var) e); else if (e instanceof UnaryExpression) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 2e43e326..5e266557 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -3,6 +3,7 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; @@ -58,6 +59,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod rightSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getSecondOperand(), null)); } + // remove null check when equality already implies non-null + if (isNullCheckImpliedBy(rightSimplified.getValue(), leftSimplified.getValue())) + return leftSimplified; + if (isNullCheckImpliedBy(leftSimplified.getValue(), rightSimplified.getValue())) + return rightSimplified; + // check if either side is redundant if (isRedundant(leftSimplified.getValue())) return rightSimplified; @@ -83,6 +90,9 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod return node; } + /** + * Checks if a binary expression is of the form x == y && y == x, which can be simplified to x == y + */ private static boolean isSymmetricEquality(Expression left, Expression right) { if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2 && "==".equals(b2.getOperator())) { @@ -96,6 +106,36 @@ private static boolean isSymmetricEquality(Expression left, Expression right) { return false; } + /** + * Checks if a null check (x != null) is implied by an equality check (x == y) where y is not null + */ + private static boolean isNullCheckImpliedBy(Expression nullCheck, Expression context) { + + // check if in form of x != null + if (!(nullCheck instanceof BinaryExpression nb) || !"!=".equals(nb.getOperator())) + return false; + + // identify the variable being checked for null + Expression checkedVar; + if (nb.getFirstOperand() instanceof LiteralNull && !(nb.getSecondOperand() instanceof LiteralNull)) { + checkedVar = nb.getSecondOperand(); + } else if (nb.getSecondOperand() instanceof LiteralNull && !(nb.getFirstOperand() instanceof LiteralNull)) { + checkedVar = nb.getFirstOperand(); + } else { + return false; + } + + // check if context contains an equality check of the form x == y where y is not null + if (!(context instanceof BinaryExpression cb) || !"==".equals(cb.getOperator())) + return false; + + // check if either side of the equality is the checked variable and the other side is not null + Expression left = cb.getFirstOperand(); + Expression right = cb.getSecondOperand(); + return (left.equals(checkedVar) && !(right instanceof LiteralNull)) + || (right.equals(checkedVar) && !(left instanceof LiteralNull)); + } + /** * Checks if an expression is redundant (e.g. true or x == x) */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index 64eb4fad..cdb1a5b7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -13,6 +13,7 @@ import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.Var; @@ -49,6 +50,8 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo return new JsonPrimitive(((LiteralReal) exp).getValue()); if (exp instanceof LiteralBoolean) return new JsonPrimitive(exp.isBooleanTrue()); + if (exp instanceof LiteralNull) + return JsonNull.INSTANCE; if (exp instanceof Var) return new JsonPrimitive(((Var) exp).getName()); return new JsonPrimitive(exp.toString()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 1bedda99..d798840c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -4,7 +4,6 @@ import java.util.List; import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; @@ -16,6 +15,7 @@ import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.utils.Utils; @@ -53,7 +53,6 @@ import rj.grammar.RJParser.StartPredContext; import rj.grammar.RJParser.TargetInvocationContext; import rj.grammar.RJParser.VarContext; -import spoon.reflect.cu.SourcePosition; import liquidjava.diagnostics.errors.ArgumentMismatchError; /** @@ -200,13 +199,12 @@ else if (literalContext.STRING() != null) else if (literalContext.INT() != null) { String text = literalContext.INT().getText(); long value = Long.parseLong(text); - if (value <= Integer.MAX_VALUE && value >= Integer.MIN_VALUE) { - return new LiteralInt((int) value); - } else { - return new LiteralLong(value); - } + return value <= Integer.MAX_VALUE && value >= Integer.MIN_VALUE ? new LiteralInt((int) value) + : new LiteralLong(value); } else if (literalContext.REAL() != null) return new LiteralReal(literalContext.REAL().getText()); + else if (literalContext.NULL() != null) + return new LiteralNull(); throw new NotImplementedException("Literal type not implemented"); } } 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..ebfe3f99 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 @@ -9,6 +9,7 @@ import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -35,6 +36,8 @@ public interface ExpressionVisitor { T visitLiteralString(LiteralString lit) throws LJError; + T visitLiteralNull(LiteralNull lit) throws LJError; + T visitUnaryExpression(UnaryExpression exp) throws LJError; T visitVar(Var var) 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..173fb733 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -11,6 +11,7 @@ import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralNull; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -106,6 +107,11 @@ public Expr visitLiteralString(LiteralString lit) { return ctx.makeString(lit.toString()); } + @Override + public Expr visitLiteralNull(LiteralNull lit) { + return ctx.makeNullLiteral(); + } + @Override public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { return switch (exp.getOp()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index c3fb32dc..08749a07 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -42,10 +42,10 @@ 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" -> z3.mkIntConst(name); - case "boolean" -> z3.mkBoolConst(name); - case "long" -> z3.mkRealConst(name); - case "float", "double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); + case "int", "short", "java.lang.Integer", "java.lang.Short" -> 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()); case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); }; @@ -81,11 +81,11 @@ private static void addBuiltinFunctions(Context z3, Map> fun static Sort getSort(Context z3, String sort) { return switch (sort) { - case "int" -> z3.getIntSort(); - case "boolean" -> z3.getBoolSort(); - case "long" -> z3.getRealSort(); - case "float" -> z3.mkFPSort32(); - case "double" -> z3.mkFPSortDouble(); + case "int", "short", "java.lang.Integer", "java.lang.Short" -> z3.getIntSort(); + case "boolean", "java.lang.Boolean" -> z3.getBoolSort(); + case "long", "java.lang.Long" -> z3.getRealSort(); + case "float", "java.lang.Float" -> z3.mkFPSort32(); + case "double", "java.lang.Double" -> z3.mkFPSortDouble(); case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); case "String" -> z3.getStringSort(); case "void" -> z3.mkUninterpretedSort("void"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b207552f..063e8229 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -1,6 +1,5 @@ package liquidjava.smt; -import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; @@ -69,6 +68,10 @@ public Expr makeBooleanLiteral(boolean value) { return z3.mkBool(value); } + public Expr makeNullLiteral() { + return z3.mkConst("null", z3.mkUninterpretedSort("java.lang.Object")); + } + private Expr getVariableTranslation(String name) throws LJError { if (!varTranslation.containsKey(name)) throw new NotFoundError(name, Keys.VARIABLE); @@ -155,6 +158,8 @@ private Expr makeStore(Expr[] params) { // #####################Boolean Operations##################### public Expr makeEquals(Expr e1, Expr e2) { + e1 = convertNullToSort(e1, e2); + e2 = convertNullToSort(e2, e1); if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPEq(toFP(e1), toFP(e2)); if (e1 instanceof RealExpr || e2 instanceof RealExpr) @@ -162,6 +167,15 @@ public Expr makeEquals(Expr e1, Expr e2) { return z3.mkEq(e1, e2); } + private Expr convertNullToSort(Expr nullable, Expr other) { + // convert null literals to the sort of the other expression + if (nullable != null && other != null && nullable.isConst() && "null".equals(nullable.toString()) + && !nullable.getSort().equals(other.getSort())) + return z3.mkConst("null", other.getSort()); + + return nullable; + } + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeLt(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 7d690d1c..86d4d1a0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -3,6 +3,8 @@ import java.util.Set; import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtLiteral; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; @@ -11,6 +13,9 @@ public class Utils { private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); + private static final Set PRIMITIVE_TYPES = Set.of("int", "boolean", "long", "short", "float", "double"); + private static final Set BOXED_TYPES = Set.of("java.lang.Integer", "java.lang.Boolean", "java.lang.Long", "java.lang.Short", + "java.lang.Float", "java.lang.Double"); public static CtTypeReference getType(String type, Factory factory) { // TODO: complete with other types @@ -25,6 +30,18 @@ public static CtTypeReference getType(String type, Factory factory) { }; } + public static boolean isNullLiteral(CtExpression assignment) { + return assignment instanceof CtLiteral lit && lit.getValue() == null; + } + + public static boolean isBoxedType(CtTypeReference type) { + return BOXED_TYPES.contains(type.getQualifiedName()); + } + + public static boolean isPrimitiveType(String type) { + return PRIMITIVE_TYPES.contains(type); + } + public static String getSimpleName(String name) { return name.contains(".") ? name.substring(name.lastIndexOf('.') + 1) : name; } From c2ae323ac47635cafbf202cffd5512dbcbd212bd Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Feb 2026 22:04:49 +0000 Subject: [PATCH 2/4] Add Tests --- .../java/testSuite/CorrectNullChecks.java | 123 ++++++++++++++++++ .../java/testSuite/ErrorAliasNotFound.java | 1 + .../java/testSuite/ErrorBoxedBoolean.java | 12 ++ .../main/java/testSuite/ErrorBoxedDouble.java | 12 ++ .../java/testSuite/ErrorBoxedInteger.java | 12 ++ .../java/testSuite/ErrorGhostNotFound.java | 1 + .../testSuite/ErrorLongUsagePredicates1.java | 1 + .../testSuite/ErrorLongUsagePredicates2.java | 1 + .../testSuite/ErrorLongUsagePredicates3.java | 1 + .../ErrorNullCheckAssignNonNull.java | 12 ++ .../testSuite/ErrorNullCheckAssignNull.java | 12 ++ .../ErrorNullCheckAssignNullAfter.java | 13 ++ .../ErrorNullCheckAssignNullObject.java | 14 ++ .../java/testSuite/ErrorNullCheckMethod.java | 12 ++ .../AtomicReferenceRefinements.java | 19 +++ .../AtomicReferenceTest.java | 15 +++ .../classes/atomic_reference_error/.expected | 1 + .../AtomicReferenceRefinements.java | 19 +++ .../AtomicReferenceTest.java | 13 ++ 19 files changed, 294 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java b/liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java new file mode 100644 index 00000000..27a6db37 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectNullChecks.java @@ -0,0 +1,123 @@ +package testSuite; + +import java.util.ArrayList; +import java.util.Date; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class CorrectNullChecks { + + void testNullInteger() { + Integer i = null; + + @Refinement("_ == null") + Integer i1 = i; + + i = 123; + + @Refinement("_ != null") + Integer i2 = i; + } + + void testNullString() { + String s = null; + + @Refinement("_ == null") + String s1 = s; + + s = "hello"; + + @Refinement("_ != null") + String s2 = s; + } + + void testNulls() { + @Refinement("_ == null") + String s = null; + + @Refinement("_ == null") + Integer i = null; + + @Refinement("_ == null") + Boolean b = null; + + @Refinement("_ == null") + Double d = null; + + @Refinement("_ == null") + Long l = null; + + @Refinement("_ == null") + Float f = null; + + @Refinement("_ == null") + Date dt = null; + + @Refinement("_ == null") + ArrayList lst = null; + } + + void testNonNulls() { + @Refinement("_ != null") + String s = "hello"; + + @Refinement("_ != null") + Integer i = 123; + + @Refinement("_ != null") + Boolean b = true; + + @Refinement("_ != null") + Double d = 1.0; + + @Refinement("_ != null") + Long l = 2L; + + @Refinement("_ != null") + Float f = 1.0f; + + @Refinement("_ != null") + Date dt = new Date(); + + @Refinement("_ != null") + ArrayList lst = new ArrayList<>(); + } + + void testNullChecksInMethods() { + @Refinement("_ != null") + String x = returnNotNullIf(null); + + @Refinement("_ != null") + String y = returnNotNullTernary(null); + + @Refinement("_ != null") + String z = returnNotNullParam("not null"); + + @Refinement("_ == null") + String w = returnNull(); + } + + @Refinement("_ != null") + String returnNotNullIf(String s) { + if (s == null) + s = "default"; + + return s; + } + + @Refinement("_ != null") + String returnNotNullTernary(String s) { + return s != null ? s : "default"; + } + + @Refinement("_ != null") + String returnNotNullParam(@Refinement("_ != null") String s) { + return s; + } + + @Refinement("_ == null") + String returnNull() { + return null; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java index ca21871a..ed9b882a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java @@ -3,6 +3,7 @@ import liquidjava.specification.Refinement; +@SuppressWarnings("unused") public class ErrorAliasNotFound { public static void main(String[] args) { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java new file mode 100644 index 00000000..93c6a3c1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedBoolean.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedBoolean { + public static void main(String[] args) { + @Refinement("_ == true") + Boolean b = false; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java new file mode 100644 index 00000000..643b509a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedDouble.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedDouble { + public static void main(String[] args) { + @Refinement("_ > 0") + Double d = -1.0; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java new file mode 100644 index 00000000..2d937e20 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorBoxedInteger.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorBoxedInteger { + public static void main(String[] args) { + @Refinement("_ > 0") + Integer j = -1; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java index be2af75c..15291a28 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -3,6 +3,7 @@ import liquidjava.specification.Refinement; +@SuppressWarnings("unused") public class ErrorGhostNotFound { public void test() { diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java index 55504b0d..7596dfcf 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java @@ -3,6 +3,7 @@ import liquidjava.specification.Refinement; +@SuppressWarnings("unused") public class ErrorLongUsagePredicates1 { void testUUID(){ @Refinement("((v/4096) % 16) == 2") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java index fc760314..d7465e9a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java @@ -3,6 +3,7 @@ import liquidjava.specification.Refinement; +@SuppressWarnings("unused") public class ErrorLongUsagePredicates2 { void testLargeSubtractionWrong() { @Refinement("v - 9007199254740992 == 2") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java index e5412994..30f4e5d6 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java @@ -3,6 +3,7 @@ import liquidjava.specification.Refinement; +@SuppressWarnings("unused") public class ErrorLongUsagePredicates3 { void testWrongSign() { @Refinement("v < 0") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java new file mode 100644 index 00000000..8218f3e2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNonNull.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorNullCheckAssignNonNull { + public static void main(String[] args) { + @Refinement("_ == null") + String s = "not null"; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java new file mode 100644 index 00000000..225719ea --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNull.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorNullCheckAssignNull { + public static void main(String[] args) { + @Refinement("_ != null") + String s = null; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java new file mode 100644 index 00000000..5ec2c135 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullAfter.java @@ -0,0 +1,13 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorNullCheckAssignNullAfter { + public static void main(String[] args) { + @Refinement("_ != null") + String s = "not null"; + s = null; // error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java new file mode 100644 index 00000000..22992825 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckAssignNullObject.java @@ -0,0 +1,14 @@ +// Refinement Error +package testSuite; + +import java.util.Date; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorNullCheckAssignNullObject { + public static void main(String[] args) { + @Refinement("_ != null") + Date date = null; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java new file mode 100644 index 00000000..3806dbd4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNullCheckMethod.java @@ -0,0 +1,12 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorNullCheckMethod { + + @Refinement("_ != null") + String returnNotNull(String s) { + return s; // error: s can be null + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java new file mode 100644 index 00000000..fa810853 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceRefinements.java @@ -0,0 +1,19 @@ +package testSuite.classes.atomic_reference_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "holding"}) +@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference") +public interface AtomicReferenceRefinements { + + @StateRefinement(to="initialValue == null ? empty(this) : holding(this)") + public void AtomicReference(V initialValue); + + @StateRefinement(from="holding(this)") + public V get(); + + @StateRefinement(to="newValue == null ? empty(this) : holding(this)") + public void set(V newValue); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java new file mode 100644 index 00000000..8907c7d5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_correct/AtomicReferenceTest.java @@ -0,0 +1,15 @@ +package testSuite.classes.atomic_reference_correct; + +import java.util.concurrent.atomic.AtomicReference; + +@SuppressWarnings("unused") +public class AtomicReferenceTest { + + public void testOk() { + AtomicReference ref = new AtomicReference<>("hello"); + String s = ref.get(); + + ref.set("world"); + String s2 = ref.get(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected new file mode 100644 index 00000000..47ef7162 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/.expected @@ -0,0 +1 @@ +State Refinement Error \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java new file mode 100644 index 00000000..f12d8667 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceRefinements.java @@ -0,0 +1,19 @@ +package testSuite.classes.atomic_reference_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"empty", "holding"}) +@ExternalRefinementsFor("java.util.concurrent.atomic.AtomicReference") +public interface AtomicReferenceRefinements { + + @StateRefinement(to="initialValue == null ? empty(this) : holding(this)") + public void AtomicReference(V initialValue); + + @StateRefinement(from="holding(this)") + public V get(); + + @StateRefinement(to="newValue == null ? empty(this) : holding(this)") + public void set(V newValue); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java new file mode 100644 index 00000000..66f704f7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/atomic_reference_error/AtomicReferenceTest.java @@ -0,0 +1,13 @@ +package testSuite.classes.atomic_reference_error; + +import java.util.concurrent.atomic.AtomicReference; + +@SuppressWarnings("unused") +public class AtomicReferenceTest { + + public void testError() { + AtomicReference ref = new AtomicReference<>(null); + String s = ref.get(); // error + } +} + From d73b81c6954c118bb160634d558fce3b55d24d4f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 7 Feb 2026 22:24:06 +0000 Subject: [PATCH 3/4] Minor Changes --- .../general_checkers/OperationsChecker.java | 4 +++- .../src/main/java/liquidjava/rj_language/Predicate.java | 1 - 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index bce8b594..70ee89c1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -16,6 +16,8 @@ import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.LiteralNull; + import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -221,7 +223,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return new Predicate(); } if (l.getValue() == null) - return new Predicate("null", element); + return new Predicate(new LiteralNull()); return new Predicate(l.getValue().toString(), element); 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 e299f77c..0921151a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -76,7 +76,6 @@ public Predicate(String ref, CtElement element, String prefix) throws LJError { } } - /** Create a predicate with the expression true */ public Predicate(Expression e) { exp = e; } From f24dc28dec63b6fd41d4045c4e8e4cc9d1d1d1bf Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 8 Feb 2026 12:03:53 +0000 Subject: [PATCH 4/4] Unused Imports --- .../processor/refinement_checker/RefinementTypeChecker.java | 2 -- liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java | 4 ++-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index b5075e01..9c543c87 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -13,11 +13,9 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.LiteralNull; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; -import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import org.apache.commons.lang3.NotImplementedException; diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 86d4d1a0..0f4a3288 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -14,8 +14,8 @@ public class Utils { private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); private static final Set PRIMITIVE_TYPES = Set.of("int", "boolean", "long", "short", "float", "double"); - private static final Set BOXED_TYPES = Set.of("java.lang.Integer", "java.lang.Boolean", "java.lang.Long", "java.lang.Short", - "java.lang.Float", "java.lang.Double"); + private static final Set BOXED_TYPES = Set.of("java.lang.Integer", "java.lang.Boolean", "java.lang.Long", + "java.lang.Short", "java.lang.Float", "java.lang.Double"); public static CtTypeReference getType(String type, Factory factory) { // TODO: complete with other types