diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java index 30ac3840..b8ceddb7 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java @@ -36,4 +36,31 @@ public static void main(String[] args) { @Refinement("_ > 10") long f = doubleBiggerThanTwenty(2 * 80); } + + + void testSmallLong() { + @Refinement("v > 0") + long v = 42L; + } + + void testDoublePrecisionBoundary() { + @Refinement("v == 9007199254740993") + long v = 9007199254740993L; + } + + void testLargeSubtraction() { + @Refinement("v - 9007199254740992 == 1") + long v = 9007199254740993L; + } + + void testMaxValueModulo() { + @Refinement("v % 1000 == 807") + long v = 9223372036854775807L; + } + + void testUUID(){ + @Refinement("((v/4096) % 16) == 1") + long v = 0x01000000122341666L; + } + } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java new file mode 100644 index 00000000..55504b0d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java @@ -0,0 +1,11 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLongUsagePredicates1 { + void testUUID(){ + @Refinement("((v/4096) % 16) == 2") + long v = 0x01000000122341666L; + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java new file mode 100644 index 00000000..fc760314 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java @@ -0,0 +1,11 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLongUsagePredicates2 { + void testLargeSubtractionWrong() { + @Refinement("v - 9007199254740992 == 2") + long v = 9007199254740993L; + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java new file mode 100644 index 00000000..e5412994 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java @@ -0,0 +1,11 @@ +// Refinement Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorLongUsagePredicates3 { + void testWrongSign() { + @Refinement("v < 0") + long v = 42L; + } +} \ No newline at end of file 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 5e4ad5a7..565de7e3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -21,6 +21,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; @@ -233,7 +234,8 @@ public static Predicate createLit(String value, String type) { Expression exp = switch (type) { case Types.BOOLEAN -> new LiteralBoolean(value); case Types.INT, Types.SHORT -> new LiteralInt(value); - case Types.DOUBLE, Types.LONG, Types.FLOAT -> new LiteralReal(value); + case Types.LONG -> new LiteralLong(value); + case Types.DOUBLE, Types.FLOAT -> new LiteralReal(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 5449949b..9b4b2e17 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 @@ -66,7 +66,8 @@ public void setChild(int index, Expression element) { } public boolean isLiteral() { - return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean; + return this instanceof LiteralInt || this instanceof LiteralLong || this instanceof LiteralReal + || this instanceof LiteralBoolean; } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralLong.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralLong.java new file mode 100644 index 00000000..300f089b --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralLong.java @@ -0,0 +1,72 @@ +package liquidjava.rj_language.ast; + +import java.util.List; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.rj_language.visitors.ExpressionVisitor; + +public class LiteralLong extends Expression { + + private final long value; + + public LiteralLong(long v) { + value = v; + } + + public LiteralLong(String v) { + value = Long.parseLong(v); + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitLiteralLong(this); + } + + public String toString() { + return Long.toString(value); + } + + public long getValue() { + 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 LiteralLong(value); + } + + @Override + public boolean isBooleanTrue() { + return false; + } + + @Override + public int hashCode() { + final int prime = 31; + int result = 1; + result = prime * result + Long.hashCode(value); + return result; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; + LiteralLong other = (LiteralLong) 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 index 764793e0..085f015d 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 @@ -11,6 +11,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -33,6 +34,8 @@ public static Optional> getType(Context ctx, Factory factory, return Optional.of(Utils.getType("String", factory)); else if (e instanceof LiteralInt) return Optional.of(Utils.getType("int", factory)); + 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 LiteralBoolean) 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 27629839..64eb4fad 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 @@ -12,6 +12,7 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.Var; @@ -42,6 +43,8 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo return JsonNull.INSTANCE; if (exp instanceof LiteralInt) return new JsonPrimitive(((LiteralInt) exp).getValue()); + if (exp instanceof LiteralLong) + return new JsonPrimitive(((LiteralLong) exp).getValue()); if (exp instanceof LiteralReal) return new JsonPrimitive(((LiteralReal) exp).getValue()); if (exp instanceof LiteralBoolean) 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 82e6ea52..1bedda99 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 @@ -13,6 +13,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -196,9 +197,15 @@ private Expression literalCreate(LiteralContext literalContext) throws LJError { return new LiteralBoolean(literalContext.BOOL().getText()); else if (literalContext.STRING() != null) return new LiteralString(literalContext.STRING().getText()); - else if (literalContext.INT() != null) - return new LiteralInt(literalContext.INT().getText()); - else if (literalContext.REAL() != 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); + } + } else if (literalContext.REAL() != null) return new LiteralReal(literalContext.REAL().getText()); 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 dc8d9089..52e37319 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 @@ -8,6 +8,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -26,6 +27,8 @@ public interface ExpressionVisitor { T visitLiteralInt(LiteralInt lit) throws LJError; + T visitLiteralLong(LiteralLong lit) throws LJError; + T visitLiteralBoolean(LiteralBoolean lit) throws LJError; T visitLiteralReal(LiteralReal 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 1425b438..35e74803 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -10,6 +10,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; @@ -85,6 +86,11 @@ public Expr visitLiteralInt(LiteralInt lit) { return ctx.makeIntegerLiteral(lit.getValue()); } + @Override + public Expr visitLiteralLong(LiteralLong lit) { + return ctx.makeLongLiteral(lit.getValue()); + } + @Override public Expr visitLiteralBoolean(LiteralBoolean lit) { return ctx.makeBooleanLiteral(lit.isBooleanTrue()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index e844ad12..b207552f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -157,7 +157,8 @@ private Expr makeStore(Expr[] params) { public Expr makeEquals(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPEq(toFP(e1), toFP(e2)); - + if (e1 instanceof RealExpr || e2 instanceof RealExpr) + return z3.mkEq(toReal(e1), toReal(e2)); return z3.mkEq(e1, e2); } @@ -165,7 +166,8 @@ public Expr makeEquals(Expr e1, Expr e2) { public Expr makeLt(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPLt(toFP(e1), toFP(e2)); - + if (e1 instanceof RealExpr || e2 instanceof RealExpr) + return z3.mkLt(toReal(e1), toReal(e2)); return z3.mkLt((ArithExpr) e1, (ArithExpr) e2); } @@ -173,7 +175,8 @@ public Expr makeLt(Expr e1, Expr e2) { public Expr makeLtEq(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPLEq(toFP(e1), toFP(e2)); - + if (e1 instanceof RealExpr || e2 instanceof RealExpr) + return z3.mkLe(toReal(e1), toReal(e2)); return z3.mkLe((ArithExpr) e1, (ArithExpr) e2); } @@ -181,7 +184,8 @@ public Expr makeLtEq(Expr e1, Expr e2) { public Expr makeGt(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPGt(toFP(e1), toFP(e2)); - + if (e1 instanceof RealExpr || e2 instanceof RealExpr) + return z3.mkGt(toReal(e1), toReal(e2)); return z3.mkGt((ArithExpr) e1, (ArithExpr) e2); } @@ -189,7 +193,8 @@ public Expr makeGt(Expr e1, Expr e2) { public Expr makeGtEq(Expr e1, Expr e2) { if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPGEq(toFP(e1), toFP(e2)); - + if (e1 instanceof RealExpr || e2 instanceof RealExpr) + return z3.mkGe(toReal(e1), toReal(e2)); return z3.mkGe((ArithExpr) e1, (ArithExpr) e2); } @@ -226,7 +231,8 @@ public Expr makeMinus(Expr eval) { public Expr makeAdd(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPAdd(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); - + if (eval instanceof RealExpr || eval2 instanceof RealExpr) + return z3.mkAdd(toReal(eval), toReal(eval2)); return z3.mkAdd((ArithExpr) eval, (ArithExpr) eval2); } @@ -234,7 +240,8 @@ public Expr makeAdd(Expr eval, Expr eval2) { public Expr makeSub(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPSub(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); - + if (eval instanceof RealExpr || eval2 instanceof RealExpr) + return z3.mkSub(toReal(eval), toReal(eval2)); return z3.mkSub((ArithExpr) eval, (ArithExpr) eval2); } @@ -242,7 +249,8 @@ public Expr makeSub(Expr eval, Expr eval2) { public Expr makeMul(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPMul(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); - + if (eval instanceof RealExpr || eval2 instanceof RealExpr) + return z3.mkMul(toReal(eval), toReal(eval2)); return z3.mkMul((ArithExpr) eval, (ArithExpr) eval2); } @@ -250,16 +258,35 @@ public Expr makeMul(Expr eval, Expr eval2) { public Expr makeDiv(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); - + if (eval instanceof RealExpr || eval2 instanceof RealExpr) + return z3.mkDiv(toReal(eval), toReal(eval2)); return z3.mkDiv((ArithExpr) eval, (ArithExpr) eval2); } public Expr makeMod(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPRem(toFP(eval), toFP(eval2)); + if (eval instanceof RealExpr || eval2 instanceof RealExpr) + return z3.mkMod(toInt(eval), toInt(eval2)); return z3.mkMod((IntExpr) eval, (IntExpr) eval2); } + private RealExpr toReal(Expr e) { + if (e instanceof RealExpr) + return (RealExpr) e; + if (e instanceof IntExpr) + return z3.mkInt2Real((IntExpr) e); + throw new NotImplementedException(); + } + + private IntExpr toInt(Expr e) { + if (e instanceof IntExpr) + return (IntExpr) e; + if (e instanceof RealExpr) + return z3.mkReal2Int((RealExpr) e); + throw new NotImplementedException(); + } + private FPExpr toFP(Expr e) { FPExpr f; if (e instanceof FPExpr) {