Clean up SMT functions to_int, pow (^) + to_real

examples/concepts/c/math.c

@@ -2,9 +2,9 @@
 #include <math.h>
 
 int main(){
-    // TODO: This file fails, although given directly to silicon it does not fail, no clue what is going on.
     //@ assert(ceil(1.5) == 2.0);
     //@ assert(ceil(2.0) == 2.0);
+    // TODO: Below test case fails, although given directly to silicon it does not fail, no clue what is going on.
     //@ assert(ceil(-1.5) == -1.0);
 
     //@ assert(floor(1.5) == 1.0);
@@ -15,9 +15,10 @@ int main(){
     //@ assert(round(1.4) == 1.0);
     //@ assert(round(2.0) == 2.0);
     //@ assert(round(-1.5) == -2.0);
+    // TODO: Below fails
     //@ assert(round(-1.4) == -1.0);
 
-
+    // TODO: Below fails
     //@ assert(fabs(-1.5) == 1.5);
     //@ assert(fabs(1.5) == 1.5);
 

res/universal/res/c/math.h

@@ -1,21 +1,8 @@
 #ifndef MATH_H
 #define MATH_H
 
-
-/*@
-  // Gets replaced by internal SMT function in VerCors
-  decreases;
-pure bool is_int(float x);
-@*/
-
-/*@
-  // Gets replaced by internal SMT function in VerCors
-  decreases;
-pure double pow_math_h(double x, double y);
-@*/
-
 /*@
-  ensures \result == (is_int(x) ? x : (double)((int)x + 1));
+  ensures \result == (\is_int(x) ? x : (double)((int)x + 1));
   decreases;
 @*/
 double /*@ pure @*/ ceil(double x);
@@ -34,20 +21,20 @@ double /*@ pure @*/ floor(double x);
 
 /*@
   // Gets replaced by internal SMT function in VerCors
-  ensures \result == pow_math_h(x, y);
+  ensures \result == \pow(x, y);
   decreases;
 @*/
 double /*@ pure @*/ pow(double x, double y);
 
 /*@
-  ensures \result == pow_math_h(x, 0.5);
+  ensures \result == \pow(x, 0.5);
   decreases;
 @*/
 double /*@ pure @*/ sqrt(double x);
 
 /*@
-  ensures !(x < 0 && is_int(x-0.5)) ==> \result == (double)(int)(x + 0.5);
-  ensures (x < 0 && is_int(x-0.5)) ==> \result == x-0.5;
+  ensures !(x < 0 && \is_int(x-0.5)) ==> \result == (double)(int)(x + 0.5);
+  ensures (x < 0 && \is_int(x-0.5)) ==> \result == x-0.5;
   decreases;
 @*/
 double /*@ pure @*/ round(double x);

src/col/vct/col/ast/Node.scala

@@ -801,8 +801,9 @@ case class SmtlibFpToReal[G](arg: Expr[G])(implicit val o: Origin) extends Smtli
 case class SmtlibFpToSInt[G](arg: Expr[G], bits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpToSIntImpl[G]
 case class SmtlibFpToUInt[G](arg: Expr[G], bits: Int)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibFpToUIntImpl[G]
 
-case class SmtlibToInt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibToIntImpl[G]
 case class SmtlibIsInt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibIsIntImpl[G]
+case class SmtlibToInt[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibToIntImpl[G]
+case class SmtlibToReal[G](arg: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibToRealImpl[G]
 case class SmtlibPow[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends SmtlibExpr[G] with BinExpr[G] with SmtlibPowImpl[G]
 
 case class SmtlibLiteralString[G](data: String)(implicit val o: Origin) extends SmtlibExpr[G] with SmtlibLiteralStringImpl[G]

src/col/vct/col/ast/lang/smt/SmtlibToRealImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.lang.smt
+
+import vct.col.ast.{SmtlibToReal, TRational, Type}
+import vct.col.print._
+
+trait SmtlibToRealImpl[G] { this: SmtlibToReal[G] =>
+  override def t: Type[G] = TRational()
+  override def layout(implicit ctx: Ctx): Doc = Text("to_real(") <> arg <> ")"
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -1452,12 +1452,13 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case SmtlibFpToReal(arg) => SmtlibFpToReal(fp(arg)._1)
       case SmtlibFpToSInt(arg, bits) => SmtlibFpToSInt(fp(arg)._1, bits)
       case SmtlibFpToUInt(arg, bits) => SmtlibFpToUInt(fp(arg)._1, bits)
-      case SmtlibToInt(arg) => SmtlibToInt(rat(arg))
       case SmtlibIsInt(arg) =>
         firstOk(e, s"Expected operand to be floating, but got ${arg.t}.",
           SmtlibIsInt(float(arg)),
           SmtlibIsInt(rat(arg)),
         )
+      case SmtlibToInt(arg) => SmtlibToInt(rat(arg))
+      case SmtlibToReal(arg) => SmtlibToReal(int(arg))
       case SmtlibPow(left, right) =>
         firstOk(e, s"Expected args to be numerical, but got ${left.t} and ${right.t}.",
           SmtlibPow(int(left), int(right)),

src/parsers/antlr4/SpecLexer.g4

@@ -150,8 +150,6 @@ POINTER_INDEX: '\\pointer_index';
 POINTER_BLOCK_LENGTH: '\\pointer_block_length';
 POINTER_BLOCK_OFFSET: '\\pointer_block_offset';
 POINTER_LENGTH: '\\pointer_length';
-EUCLIDIAN_DIV: '\\euclidean_div';
-EUCLIDIAN_MOD: '\\euclidean_mod';
 SHARED_MEM_SIZE: '\\shared_mem_size';
 VALUES: '\\values';
 VCMP: '\\vcmp';
@@ -169,6 +167,11 @@ POLARITY_DEPENDENT: '\\polarity_dependent';
 SMT_LIB: '\\smtlib';
 BOOGIE: '\\boogie';
 
+EUCLIDIAN_DIV: '\\euclidean_div';
+EUCLIDIAN_MOD: '\\euclidean_mod';
+POW: '\\pow';
+IS_INT: '\\is_int';
+
 NONE: 'none';
 OPTION_NONE: 'None';
 WRITE: 'write';

src/parsers/antlr4/SpecParser.g4

@@ -185,8 +185,6 @@ valPrimaryPermission
  | '\\pointer_block_offset' '(' langExpr ')' # valPointerBlockOffset
  | '\\pointer_length' '(' langExpr ')' # valPointerLength
  | '\\polarity_dependent' '(' langExpr ',' langExpr ')' # valPolarityDependent
- | '\\euclidean_div' '(' langExpr ',' langExpr ')' # valEuclideanDiv
- | '\\euclidean_mod' '(' langExpr ',' langExpr ')' # valEuclideanMod
  ;
 
 valForall: '\\forall' | '\u2200';
@@ -289,6 +287,10 @@ valPrimary
  | '\\nd_index' '(' langExpr ',' langExpr valExprPair* ')' # valNdIndex
  | '\\nd_partial_index' '(' valExpressionList ';' valExpressionList ')' # valNdLIndex
  | '\\nd_length' '(' valExpressionList ')' # ValNdLength
+ | '\\euclidean_div' '(' langExpr ',' langExpr ')' # valEuclideanDiv
+ | '\\euclidean_mod' '(' langExpr ',' langExpr ')' # valEuclideanMod
+ | '\\pow' '(' langExpr ',' langExpr ')' # valPow
+ | '\\is_int' '(' langExpr ')' # valIsInt
  ;
 
 // Out spec: defined meaning: a language local

src/parsers/vct/parsers/transform/CPPToCol.scala

@@ -1386,8 +1386,6 @@ case class CPPToCol[G](override val baseOrigin: Origin,
     case ValPointerBlockOffset(_, _, ptr, _) => PointerBlockOffset(convert(ptr))(blame(e))
     case ValPointerLength(_, _, ptr, _) => PointerLength(convert(ptr))(blame(e))
     case ValPolarityDependent(_, _, onInhale, _, onExhale, _) => PolarityDependent(convert(onInhale), convert(onExhale))
-    case ValEuclideanDiv(_, _, left, _, right, _) => FloorDiv(convert(left), convert(right))(blame(e))
-    case ValEuclideanMod(_, _, left, _, right, _) => col.Mod(convert(left), convert(right))(blame(e))
   }
 
   def convert(implicit v: ValBindingContext): (Variable[G], Seq[Expr[G]]) = v match {
@@ -1488,6 +1486,10 @@ case class CPPToCol[G](override val baseOrigin: Origin,
       val allIndices = convert(indices)
       NdPartialIndex(allIndices.init, allIndices.last, convert(dims))
     case ValNdLength(_, _, dims, _) => NdLength(convert(dims))
+    case ValEuclideanDiv(_, _, left, _, right, _) => FloorDiv(convert(left), convert(right))(blame(e))
+    case ValEuclideanMod(_, _, left, _, right, _) => col.Mod(convert(left), convert(right))(blame(e))
+    case ValPow(_, _, left, _, right, _) => SmtlibPow(convert(left), convert(right))
+    case ValIsInt(_, _, arg, _) => SmtlibIsInt(convert(arg))
   }
 
   def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = e match {

src/parsers/vct/parsers/transform/CToCol.scala

@@ -1134,8 +1134,6 @@ case class CToCol[G](override val baseOrigin: Origin,
     case ValPointerBlockOffset(_, _, ptr, _) => PointerBlockOffset(convert(ptr))(blame(e))
     case ValPointerLength(_, _, ptr, _) => PointerLength(convert(ptr))(blame(e))
     case ValPolarityDependent(_, _, onInhale, _, onExhale, _) => PolarityDependent(convert(onInhale), convert(onExhale))
-    case ValEuclideanDiv(_, _, left, _, right, _) => FloorDiv(convert(left), convert(right))(blame(e))
-    case ValEuclideanMod(_, _, left, _, right, _) => col.Mod(convert(left), convert(right))(blame(e))
   }
 
   def convert(implicit v: ValBindingContext): (Variable[G], Seq[Expr[G]]) = v match {
@@ -1236,6 +1234,10 @@ case class CToCol[G](override val baseOrigin: Origin,
       val allIndices = convert(indices)
       NdPartialIndex(allIndices.init, allIndices.last, convert(dims))
     case ValNdLength(_, _, dims, _) => NdLength(convert(dims))
+    case ValEuclideanDiv(_, _, left, _, right, _) => FloorDiv(convert(left), convert(right))(blame(e))
+    case ValEuclideanMod(_, _, left, _, right, _) => col.Mod(convert(left), convert(right))(blame(e))
+    case ValPow(_, _, left, _, right, _) => SmtlibPow(convert(left), convert(right))
+    case ValIsInt(_, _, arg, _) => SmtlibIsInt(convert(arg))
   }
 
   def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) = e match {