Merge branch 'small-fix' into PointerADT

.mill-jvm-opts

@@ -1,2 +1,2 @@
--Xss32m
+-Xss128m
 -Xmx2G

mill-build/util/src/util/JavaModule.scala

@@ -6,7 +6,7 @@ import scalalib.{JavaModule => BaseJavaModule}
 trait JavaModule extends BaseJavaModule {
   // https://github.com/viperproject/silicon/issues/748
   // 32MB is enough stack space for silicon, a 100% marco guarantee
-  override def forkArgs = Seq("-Xmx2G", "-Xss32m")
+  override def forkArgs = Seq("-Xmx2G", "-Xss128m")
 
   def classPathFileElements = T { runClasspath().map(_.path.toString) }
 

res/universal/res/c/math.h

@@ -1,37 +1,226 @@
 #ifndef MATH_H
 #define MATH_H
 
+# define M_PI           3.14159265358979323846  /* pi */
+
 /*@
-  ensures \result == (\is_int(x) ? x : (double)((int)x + 1));
   decreases;
+pure double M_PI() = 3.14159265358979323846;
 @*/
-double /*@ pure @*/ ceil(double x);
 
 /*@
-  ensures \result == (x >= 0 ? x : -x);
+  requires x>= 0;
+  ensures \result == \pow(x, 0.5);
   decreases;
 @*/
-double /*@ pure @*/ fabs(double x);
+float /*@ pure @*/ sqrtf(float x);
+
+/*@ ensures \result >= -1 && \result <= 1;
+    decreases;
+@*/
+float /*@ pure @*/ sinf(float x);
 
 /*@
-  ensures \result == (double)((int)x);
+  requires x >= -1 && x <= 1;
+  ensures \result >= -M_PI()/2 && \result <= M_PI()/2;
   decreases;
 @*/
-double /*@ pure @*/ floor(double x);
+float /*@ pure @*/ asinf(float x);
+/*@
+  ensures \result >= -1 && \result <= 1;
+  decreases;
+@*/
+float /*@ pure @*/ cosf(float x);
+
+/*@
+  requires x >= -1 && x <= 1;
+  ensures \result >= 0 && \result <= M_PI();
+  decreases;
+@*/
+float /*@ pure @*/ acosf(float x);
+
+/*@
+  ensures x == 0 ==> \result == 0;
+  decreases;
+@*/
+float /*@ pure @*/ tanf(float x);
+
+/*@
+  ensures \result >= -M_PI()/2 && \result <= M_PI()/2;
+  decreases;
+@*/
+float /*@ pure @*/ atanf(float x);
+
+/*@
+  ensures -M_PI() <= \result && \result <= M_PI();
+  decreases;
+@*/
+float /*@ pure @*/ atan2f(float x, float y);
+
+/*@
+  ensures \result == (expf(x) - expf(-x)) \ 2;
+  decreases;
+@*/
+float /*@ pure @*/ sinhf(float x);
+
+/*@
+  ensures \result == (expf(x) + expf(-x)) \ 2;
+  decreases;
+@*/
+float /*@ pure @*/ coshf(float x);
+
+/*@
+  ensures \result == (expf(x) - expf(-x)) \ (expf(x) + expf(-x));
+  decreases;
+@*/
+float /*@ pure @*/ tanhf(float x);
+
+/*@
+  ensures \result == powf(x*x + y*y, 0.5);
+  decreases;
+@*/
+float /*@ pure @*/ hypotf(float x, float y);
+
+/*@
+  ensures \result == powf(2.7182818284, x);
+  decreases;
+@*/
+float /*@ pure @*/ expf(float x);
+
+/*@
+  decreases;
+@*/
+float /*@ pure @*/ logf(float x);
 
 /*@
-  // Gets replaced by internal SMT function in VerCors
   ensures \result == \pow(x, y);
+  ensures x > 0 ==> \result > 0;
   decreases;
 @*/
-double /*@ pure @*/ pow(double x, double y);
+float /*@ pure @*/ powf(float x, float y);
 
 /*@
-  ensures \result == \pow(x, 0.5);
+  ensures \result == (float)((int)x);
+  decreases;
+@*/
+float /*@ pure @*/ floorf(float x);
+
+/*@
+  ensures \result == (\is_int(x) ? x : (float)((int)x + 1));
+  decreases;
+@*/
+float /*@ pure @*/ ceilf(float x);
+
+/*@
+  ensures !(x < 0 && \is_int(x-0.5)) ==> \result == (float)(int)(x + 0.5);
+  ensures (x < 0 && \is_int(x-0.5)) ==> \result == x-0.5;
+  decreases;
+@*/
+float /*@ pure @*/ roundf(float x);
+
+/*@
+  requires x>= 0;
+  ensures \result == pow(x, 0.5);
   decreases;
 @*/
 double /*@ pure @*/ sqrt(double x);
 
+/*@ ensures \result >= -1 && \result <= 1;
+    decreases;
+@*/
+double /*@ pure @*/ sin(double x);
+
+/*@
+  requires x >= -1 && x <= 1;
+  ensures \result >= -M_PI()/2 && \result <= M_PI()/2;
+  decreases;
+@*/
+double /*@ pure @*/ asin(double x);
+/*@
+  ensures \result >= -1 && \result <= 1;
+  decreases;
+@*/
+double /*@ pure @*/ cos(double x);
+
+/*@
+  requires x >= -1 && x <= 1;
+  ensures \result >= 0 && \result <= M_PI();
+  decreases;
+@*/
+double /*@ pure @*/ acos(double x);
+
+/*@
+  ensures x == 0 ==> \result == 0;
+  decreases;
+@*/
+double /*@ pure @*/ tan(double x);
+
+/*@
+  ensures \result >= -M_PI()/2 && \result <= M_PI()/2;
+  decreases;
+@*/
+double /*@ pure @*/ atan(double x);
+
+/*@
+  ensures -M_PI() <= \result && \result <= M_PI();
+  decreases;
+@*/
+double /*@ pure @*/ atan2(double x, double y);
+
+/*@
+  //ensures \result == (exp(x) - exp(-x)) \ 2;
+  decreases;
+@*/
+double /*@ pure @*/ sinh(double x);
+
+/*@
+  ensures \result == (exp(x) + exp(-x)) \ 2;
+  decreases;
+@*/
+double /*@ pure @*/ cosh(double x);
+
+/*@
+  ensures \result == (exp(x) - exp(-x)) \ (exp(x) + exp(-x));
+  decreases;
+@*/
+double /*@ pure @*/ tanh(double x);
+
+/*@
+  ensures \result == pow(x*x + y*y, 0.5);
+  decreases;
+@*/
+double /*@ pure @*/ hypot(double x, double y);
+
+/*@
+  ensures \result == pow(2.7182818284, x);
+  decreases;
+@*/
+double /*@ pure @*/ exp(double x);
+
+/*@
+  decreases;
+@*/
+double /*@ pure @*/ log(double x);
+
+/*@
+  ensures \result == \pow(x, y);
+  ensures x > 0 ==> \result > 0;
+  decreases;
+@*/
+double /*@ pure @*/ pow(double x, double y);
+
+/*@
+  ensures \result == (double)((int)x);
+  decreases;
+@*/
+double /*@ pure @*/ floor(double x);
+
+/*@
+  ensures \result == (\is_int(x) ? x : (double)((int)x + 1));
+  decreases;
+@*/
+double /*@ pure @*/ ceil(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;

src/col/vct/col/ast/type/typeclass/FloatTypeImpl.scala

@@ -5,6 +5,7 @@ import vct.col.ast.{CPrimitiveType, CSpecificationType, FloatType, TCFloat, TFlo
 import vct.col.origin.{DiagnosticOrigin, Origin}
 import vct.col.print.{Ctx, Doc, Text}
 import vct.col.typerules.CoercionUtils
+import vct.col.resolve.lang.C
 
 // https://en.wikipedia.org/wiki/Single-precision_floating-point_format#IEEE_754_standard:_binary32
 // https://en.wikipedia.org/wiki/Double-precision_floating-point_format#IEEE_754_double-precision_binary_floating-point_format:_binary64
@@ -17,7 +18,9 @@ object TFloats {
 
   // Only returns a float, when one of the types is floating itself
   // Returns to biggest float, e.g. (float32, float64) should return float64
-  def getFloatMax[G](l: Type[G], r: Type[G]): Option[FloatType[G]] = {
+  def getFloatMax[G](ll: Type[G], rr: Type[G]): Option[FloatType[G]] = {
+    val l = C.stripCPrimitiveType(ll)
+    val r = C.stripCPrimitiveType(rr)
     val promote = (l, r) match {
       case (_: TFloat[G], _) => true
       case (_, _: TFloat[G]) => true
@@ -29,9 +32,6 @@ object TFloats {
     }
 
     (l, r) match {
-      // Work for CPrimitive Types
-      case (CPrimitiveType(Seq(CSpecificationType(innerL))), r) => getFloatMax(innerL, r)
-      case (l, CPrimitiveType(Seq(CSpecificationType(innerR)))) => getFloatMax(l, innerR)
       case (l: FloatType[G], r: FloatType[G]) if r.exponent == l.exponent && r.mantissa == l.mantissa => Some(promoting(l))
       case (l: FloatType[G], r: FloatType[G]) if l.exponent < r.exponent && l.mantissa < r.mantissa => Some(promoting(r))
       case (l: FloatType[G], r: FloatType[G]) if r.exponent < l.exponent && r.mantissa < l.mantissa => Some(promoting(l))

src/col/vct/col/resolve/lang/C.scala

@@ -120,19 +120,25 @@ case object C {
       case target: RefCFunctionDefinition[G] if target.name == nameFromDeclarator(declarator) => target
     }
 
+  def stripCPrimitiveType[G](t: Type[G]): Type[G] = t match {
+    case CPrimitiveType(specs) => getPrimitiveType(specs)
+    case _ => t
+  }
+
+
   def findPointerDeref[G](obj: Expr[G], name: String, ctx: ReferenceResolutionContext[G], blame: Blame[BuiltinError]): Option[CDerefTarget[G]] =
-    obj.t match {
-      case CPrimitiveType(Seq(CSpecificationType(CTPointer(innerType: TNotAValue[G])))) => innerType.decl.get match {
+    stripCPrimitiveType(obj.t) match {
+      case CTPointer(innerType: TNotAValue[G]) => innerType.decl.get match {
         case RefCStruct(decl) => getCStructDeref(decl, name)
         case _ => None
       }
-      case CPrimitiveType(Seq(CSpecificationType(CTPointer(struct: CTStruct[G])))) =>
+      case CTPointer(struct: CTStruct[G]) =>
         getCStructDeref(struct.ref.decl, name)
-      case CPrimitiveType(Seq(CSpecificationType(CTArray(_, innerType: TNotAValue[G])))) => innerType.decl.get match {
+      case CTArray(_, innerType: TNotAValue[G]) => innerType.decl.get match {
         case RefCStruct(decl) => getCStructDeref(decl, name)
         case _ => None
       }
-      case CPrimitiveType(Seq(CSpecificationType(CTArray(_, struct: CTStruct[G])))) =>
+      case CTArray(_, struct: CTStruct[G]) =>
         getCStructDeref(struct.ref.decl, name)
       case CTPointer(struct: CTStruct[G]) => getCStructDeref(struct.ref.decl, name)
       case CTArray(_, struct: CTStruct[G]) => getCStructDeref(struct.ref.decl, name)
@@ -149,16 +155,14 @@ case object C {
     }
 
   def findDeref[G](obj: Expr[G], name: String, ctx: ReferenceResolutionContext[G], blame: Blame[BuiltinError]): Option[CDerefTarget[G]] =
-    (obj.t match {
+    (stripCPrimitiveType(obj.t) match {
       case t: TNotAValue[G] => t.decl.get match {
         case RefAxiomaticDataType(decl) => decl.decls.flatMap(Referrable.from).collectFirst {
           case ref: RefADTFunction[G] if ref.name == name => ref
         }
         case RefCStruct(decl: CGlobalDeclaration[G]) => getCStructDeref(decl, name)
         case _ => None
       }
-      case CPrimitiveType(Seq(CSpecificationType(struct: CTStruct[G]))) =>
-        getCStructDeref(struct.ref.decl, name)
       case struct: CTStruct[G] =>
         getCStructDeref(struct.ref.decl, name)
       case CTCudaVec() =>

src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala

@@ -33,12 +33,14 @@ case class ExtractInlineQuantifierPatterns[Pre <: Generation]() extends Rewriter
 
   case class MakePattern(pattern: Pattern) extends Rewriter[Pre] {
     override val allScopes = outer.allScopes
+    var inScale: Boolean = false
 
     override def dispatch(e: Expr[Pre]): Expr[Post] = e match {
       // PB: don't add nodes here just to be conservative: in general all terms are allowable in patterns, *except*
       // that z3 disallows all Bool-related operators, and Viper additionally disallows all arithmetic operators. Any
       // other operators is necessarily encoded as an smt function (allowed), or banned due to being a side effect
       // (later dealt with rigorously).
+      case e if inScale => e.rewriteDefault()
 
       case And(_, _) | Or(_, _) | Implies(_, _) | Star(_, _) | Wand(_, _) | PolarityDependent(_, _) =>
         throw NotAllowedInTrigger(e)
@@ -56,6 +58,12 @@ case class ExtractInlineQuantifierPatterns[Pre <: Generation]() extends Rewriter
 
       case Local(Ref(v)) if pattern.letBindingsHere.contains(v) => dispatch(pattern.letBindingsHere(v))
 
+      case p@PredicateApply(ref, args, perm) =>
+        inScale = true
+        val newPerm = dispatch(perm)
+        inScale = false
+        PredicateApply(succ[Predicate[Post]](ref.decl), args.map(dispatch), newPerm)(e.o)
+
       case e => rewriteDefault(e)
     }
   }

src/rewrite/vct/rewrite/ResolveScale.scala

@@ -71,7 +71,7 @@ case class ResolveScale[Pre <: Generation]() extends Rewriter[Pre] {
       case s: Starall[Pre] => s.rewrite(body = scale(s.body, amount))
 
       case l: Let[Pre] => l.rewrite(main = scale(l.main, amount))
-
+      case InlinePattern(inner, parent, group) => InlinePattern(scale(inner, amount), parent, group)
       case other => throw WrongScale(other)
     }
   }