Skip to content

Commit 1d3a553

Browse files
CatarinaGamboaCatarinaGamboa
committed
add support for long operations with proper long values and long operations inside predicates
1 parent 791d404 commit 1d3a553

File tree

13 files changed

+197
-14
lines changed

13 files changed

+197
-14
lines changed

‎liquidjava-example/src/main/java/testSuite/CorrectLongUsage.java‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,4 +36,31 @@ public static void main(String[] args) {
3636
@Refinement("_ > 10")
3737
long f = doubleBiggerThanTwenty(2 * 80);
3838
}
39+
40+
41+
void testSmallLong() {
42+
@Refinement("v > 0")
43+
long v = 42L;
44+
}
45+
46+
void testDoublePrecisionBoundary() {
47+
@Refinement("v == 9007199254740993")
48+
long v = 9007199254740993L;
49+
}
50+
51+
void testLargeSubtraction() {
52+
@Refinement("v - 9007199254740992 == 1")
53+
long v = 9007199254740993L;
54+
}
55+
56+
void testMaxValueModulo() {
57+
@Refinement("v % 1000 == 807")
58+
long v = 9223372036854775807L;
59+
}
60+
61+
void testUUID(){
62+
@Refinement("((v/4096) % 16) == 1")
63+
long v = 0x01000000122341666L;
64+
}
65+
3966
}

‎liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates1.java‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Refinement;
5+
6+
public class ErrorLongUsagePredicates1 {
7+
void testUUID(){
8+
@Refinement("((v/4096) % 16) == 2")
9+
long v = 0x01000000122341666L;
10+
}
11+
}

‎liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates2.java‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Refinement;
5+
6+
public class ErrorLongUsagePredicates2 {
7+
void testLargeSubtractionWrong() {
8+
@Refinement("v - 9007199254740992 == 2")
9+
long v = 9007199254740993L;
10+
}
11+
}

‎liquidjava-example/src/main/java/testSuite/ErrorLongUsagePredicates3.java‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// Refinement Error
2+
package testSuite;
3+
4+
import liquidjava.specification.Refinement;
5+
6+
public class ErrorLongUsagePredicates3 {
7+
void testWrongSign() {
8+
@Refinement("v < 0")
9+
long v = 42L;
10+
}
11+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
import liquidjava.rj_language.ast.Ite;
2222
import liquidjava.rj_language.ast.LiteralBoolean;
2323
import liquidjava.rj_language.ast.LiteralInt;
24+
import liquidjava.rj_language.ast.LiteralLong;
2425
import liquidjava.rj_language.ast.LiteralReal;
2526
import liquidjava.rj_language.ast.UnaryExpression;
2627
import liquidjava.rj_language.ast.Var;
@@ -233,7 +234,8 @@ public static Predicate createLit(String value, String type) {
233234
Expression exp = switch (type) {
234235
case Types.BOOLEAN -> new LiteralBoolean(value);
235236
case Types.INT, Types.SHORT -> new LiteralInt(value);
236-
case Types.DOUBLE, Types.LONG, Types.FLOAT -> new LiteralReal(value);
237+
case Types.LONG -> new LiteralLong(value);
238+
case Types.DOUBLE, Types.FLOAT -> new LiteralReal(value);
237239
default -> throw new IllegalArgumentException("Unsupported literal type: " + type);
238240
};
239241
return new Predicate(exp);

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,8 @@ public void setChild(int index, Expression element) {
6666
}
6767

6868
public boolean isLiteral() {
69-
return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean;
69+
return this instanceof LiteralInt || this instanceof LiteralLong || this instanceof LiteralReal
70+
|| this instanceof LiteralBoolean;
7071
}
7172

7273
/**

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralLong.java‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
package liquidjava.rj_language.ast;
2+
3+
import java.util.List;
4+
5+
import liquidjava.diagnostics.errors.LJError;
6+
import liquidjava.rj_language.visitors.ExpressionVisitor;
7+
8+
public class LiteralLong extends Expression {
9+
10+
private final long value;
11+
12+
public LiteralLong(long v) {
13+
value = v;
14+
}
15+
16+
public LiteralLong(String v) {
17+
value = Long.parseLong(v);
18+
}
19+
20+
@Override
21+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
22+
return visitor.visitLiteralLong(this);
23+
}
24+
25+
public String toString() {
26+
return Long.toString(value);
27+
}
28+
29+
public long getValue() {
30+
return value;
31+
}
32+
33+
@Override
34+
public void getVariableNames(List<String> toAdd) {
35+
// end leaf
36+
}
37+
38+
@Override
39+
public void getStateInvocations(List<String> toAdd, List<String> all) {
40+
// end leaf
41+
}
42+
43+
@Override
44+
public Expression clone() {
45+
return new LiteralLong(value);
46+
}
47+
48+
@Override
49+
public boolean isBooleanTrue() {
50+
return false;
51+
}
52+
53+
@Override
54+
public int hashCode() {
55+
final int prime = 31;
56+
int result = 1;
57+
result = prime * result + Long.hashCode(value);
58+
return result;
59+
}
60+
61+
@Override
62+
public boolean equals(Object obj) {
63+
if (this == obj)
64+
return true;
65+
if (obj == null)
66+
return false;
67+
if (getClass() != obj.getClass())
68+
return false;
69+
LiteralLong other = (LiteralLong) obj;
70+
return value == other.value;
71+
}
72+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import liquidjava.rj_language.ast.Ite;
1212
import liquidjava.rj_language.ast.LiteralBoolean;
1313
import liquidjava.rj_language.ast.LiteralInt;
14+
import liquidjava.rj_language.ast.LiteralLong;
1415
import liquidjava.rj_language.ast.LiteralReal;
1516
import liquidjava.rj_language.ast.LiteralString;
1617
import liquidjava.rj_language.ast.UnaryExpression;
@@ -33,6 +34,8 @@ public static Optional<CtTypeReference<?>> getType(Context ctx, Factory factory,
3334
return Optional.of(Utils.getType("String", factory));
3435
else if (e instanceof LiteralInt)
3536
return Optional.of(Utils.getType("int", factory));
37+
else if (e instanceof LiteralLong)
38+
return Optional.of(Utils.getType("long", factory));
3639
else if (e instanceof LiteralReal)
3740
return Optional.of(Utils.getType("double", factory));
3841
else if (e instanceof LiteralBoolean)

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import liquidjava.rj_language.ast.Expression;
1313
import liquidjava.rj_language.ast.LiteralBoolean;
1414
import liquidjava.rj_language.ast.LiteralInt;
15+
import liquidjava.rj_language.ast.LiteralLong;
1516
import liquidjava.rj_language.ast.LiteralReal;
1617
import liquidjava.rj_language.ast.Var;
1718

@@ -42,6 +43,8 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo
4243
return JsonNull.INSTANCE;
4344
if (exp instanceof LiteralInt)
4445
return new JsonPrimitive(((LiteralInt) exp).getValue());
46+
if (exp instanceof LiteralLong)
47+
return new JsonPrimitive(((LiteralLong) exp).getValue());
4548
if (exp instanceof LiteralReal)
4649
return new JsonPrimitive(((LiteralReal) exp).getValue());
4750
if (exp instanceof LiteralBoolean)

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java‎

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import liquidjava.rj_language.ast.Ite;
1414
import liquidjava.rj_language.ast.LiteralBoolean;
1515
import liquidjava.rj_language.ast.LiteralInt;
16+
import liquidjava.rj_language.ast.LiteralLong;
1617
import liquidjava.rj_language.ast.LiteralReal;
1718
import liquidjava.rj_language.ast.LiteralString;
1819
import liquidjava.rj_language.ast.UnaryExpression;
@@ -196,9 +197,14 @@ private Expression literalCreate(LiteralContext literalContext) throws LJError {
196197
return new LiteralBoolean(literalContext.BOOL().getText());
197198
else if (literalContext.STRING() != null)
198199
return new LiteralString(literalContext.STRING().getText());
199-
else if (literalContext.INT() != null)
200-
return new LiteralInt(literalContext.INT().getText());
201-
else if (literalContext.REAL() != null)
200+
else if (literalContext.INT() != null) {
201+
String text = literalContext.INT().getText();
202+
try {
203+
return new LiteralInt(text);
204+
} catch (NumberFormatException e) {
205+
return new LiteralLong(text);
206+
}
207+
} else if (literalContext.REAL() != null)
202208
return new LiteralReal(literalContext.REAL().getText());
203209
throw new NotImplementedException("Literal type not implemented");
204210
}

0 commit comments

Comments
 (0)