Skip to content

Add support for Long operations inside predicates #139

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 2 commits into from
Jan 30, 2026
Merged

Add support for Long operations inside predicates #139

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1d3a553
add support for long operations with proper long values and long oper…
CatarinaGamboa Jan 30, 2026
d490f28
change catch to if max values
CatarinaGamboa Jan 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

}
11 changes: 11 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
}
11 changes: 11 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

public class ErrorLongUsagePredicates2 {
void testLargeSubtractionWrong() {
@Refinement("v - 9007199254740992 == 2")
long v = 9007199254740993L;
}
}
11 changes: 11 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
// Refinement Error
package testSuite;

import liquidjava.specification.Refinement;

public class ErrorLongUsagePredicates3 {
void testWrongSign() {
@Refinement("v < 0")
long v = 42L;
}
}
4 changes: 3 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
3 changes: 2 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

/**
Expand Down
72 changes: 72 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralLong.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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> T accept(ExpressionVisitor<T> visitor) throws LJError {
return visitor.visitLiteralLong(this);
}

public String toString() {
return Long.toString(value);
}

public long getValue() {
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 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;
}
}
3 changes: 3 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -33,6 +34,8 @@ public static Optional<CtTypeReference<?>> 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)
Expand Down
3 changes: 3 additions & 0 deletions ...-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -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)
Expand Down
12 changes: 9 additions & 3 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -196,9 +197,14 @@ 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();
try {
return new LiteralInt(text);
} catch (NumberFormatException e) {
return new LiteralLong(text);
Copy link
Copy Markdown
Collaborator

@rcosta358 rcosta358 Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So we only convert a long to a LiteralLong if it overflows 32 bits, even if it was declared as a long, right?

Also, instead of using a try-catch here, we could do this:

String text = literalContext.INT().getText();
long value = Long.parseLong(text);
if (value >= Integer.MIN_VALUE && value <= Integer.MAX_VALUE) {
    return new LiteralInt(text);
} else {
    return new LiteralLong(text);
}

Both are fine for me. Which one do you prefer?

Copy link
Copy Markdown
Collaborator Author

@CatarinaGamboa CatarinaGamboa Jan 30, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

to have literalContext.LONG() i needed to change the grammar in .g4 and i didn't want to 😅 ‍
We could not catch the exception its true, it probably is more readable so I'll change it! Athough we usually have more examples with ints but its fine

}
} else if (literalContext.REAL() != null)
return new LiteralReal(literalContext.REAL().getText());
throw new NotImplementedException("Literal type not implemented");
}
Expand Down
3 changes: 3 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -26,6 +27,8 @@ public interface ExpressionVisitor<T> {

T visitLiteralInt(LiteralInt lit) throws LJError;

T visitLiteralLong(LiteralLong lit) throws LJError;

T visitLiteralBoolean(LiteralBoolean lit) throws LJError;

T visitLiteralReal(LiteralReal lit) throws LJError;
Expand Down
6 changes: 6 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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());
Expand Down
45 changes: 36 additions & 9 deletions liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,39 +157,44 @@ 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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

Expand Down Expand Up @@ -226,40 +231,62 @@ 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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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);
}

@SuppressWarnings({ "unchecked", "rawtypes" })
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) {
Expand Down