Add support for Long operations inside predicates

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;
+    }
+
 }

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;
+    }
+}

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;                                                                                                                       
+  } 
+}

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;                                                                                                                                     
+    }
+}

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);

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;
     }
 
     /**

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> 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;
+    }
+}

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<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)

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)

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");
     }

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> {
 
     T visitLiteralInt(LiteralInt lit) throws LJError;
 
+    T visitLiteralLong(LiteralLong lit) throws LJError;
+
     T visitLiteralBoolean(LiteralBoolean lit) throws LJError;
 
     T visitLiteralReal(LiteralReal lit) throws LJError;

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());

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -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);
     }
 
@@ -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) {