From c2af2be30d42df909ea0a34cbd333ca8756f830a Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 22 Apr 2024 17:09:03 +0200 Subject: [PATCH 1/3] Trigger in pred and type C array types fixes --- src/col/vct/col/resolve/lang/C.scala | 20 ++++++----- src/rewrite/vct/rewrite/lang/LangCToCol.scala | 36 ++++++------------- .../viper/api/transform/ColToSilver.scala | 14 +++++++- 3 files changed, 35 insertions(+), 35 deletions(-) diff --git a/src/col/vct/col/resolve/lang/C.scala b/src/col/vct/col/resolve/lang/C.scala index 60eb22603c..352c637562 100644 --- a/src/col/vct/col/resolve/lang/C.scala +++ b/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 _ => None } @@ -147,7 +153,7 @@ 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 @@ -155,8 +161,6 @@ case object C { 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() => diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala index 5718d5f263..83b9941a98 100644 --- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala @@ -276,13 +276,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz case _ => false } - def getBaseType(t: Type[Pre]): Type[Pre] = t match { + def getBaseType[G](t: Type[G]): Type[G] = t match { case CPrimitiveType(specs) => -// val typeSpecs = specs.collect { case spec: CTypeSpecifier[Pre] => spec } -// typeSpecs match { -// case Seq(defn @ CStructSpecifier(_)) => t -// case other => CPrimitiveType(other) -// } C.getPrimitiveType(specs) case _ => t } @@ -876,17 +871,13 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz )(KernelBarrierFailure(barrier)) } - def isPointer(t: Type[Pre]) : Boolean = t match { + def isPointer(t: Type[Pre]) : Boolean = getBaseType(t) match { case TPointer(_) => true - case CPrimitiveType(specs) => - specs.collectFirst{case CSpecificationType(TPointer(_)) => }.nonEmpty case _ => false } - def isNumeric(t: Type[Pre]): Boolean = t match{ + def isNumeric(t: Type[Pre]): Boolean = getBaseType(t) match{ case _: NumericType[Pre] => true - case CPrimitiveType(specs) => - specs.collectFirst{case CSpecificationType(_ : NumericType[Pre]) =>}.nonEmpty case _ => false } @@ -996,10 +987,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz case struct: RefCStruct[Pre] => ??? case struct: RefCStructField[Pre] => val b: Blame[PointerDerefError] = deref.blame - val structRef = deref.struct.t match { - case t@CPrimitiveType(specs) => - val struct = specs.collectFirst { case CSpecificationType(CTPointer(CTStruct(ref))) => ref } - struct.getOrElse(throw WrongStructType(t)) + val structRef = getBaseType(deref.struct.t) match { + case CTPointer(CTStruct(struct)) => struct case t => throw WrongStructType(t) } Deref[Post](DerefPointer(rw.dispatch(deref.struct))(b), cStructFieldsSuccessor.ref((structRef.decl, struct.decls)))(deref.blame)(deref.o) @@ -1048,17 +1037,16 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz } def assignStruct(assign: PreAssignExpression[Pre]): Expr[Post] = { - assign.target.t match { - case CPrimitiveType(Seq(CSpecificationType(CTStruct(ref)))) => + getBaseType(assign.target.t) match { + case CTStruct(ref) => val copy = createStructCopy(rw.dispatch(assign.value), ref.decl, (f: InstanceField[_]) => StructCopyFailed(assign, f)) PreAssignExpression(rw.dispatch(assign.target), copy)(AssignLocalOk)(assign.o) case _ => throw WrongStructType(assign.target) } } - def isCPointer(t: Type[_]) = t match { + def isCPointer(t: Type[_]) = getBaseType(t) match { case CTPointer(_) => true - case CPrimitiveType(Seq(CSpecificationType(CTPointer(_)))) => true case _ => false } @@ -1067,12 +1055,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz // Create copy for any direct structure arguments val newArgs = args.map(a => - a.t match { - case CPrimitiveType(specs) if specs.collectFirst { case CSpecificationType(_: CTStruct[Pre]) => () }.isDefined => - specs match { - case Seq(CSpecificationType(CTStruct(ref))) => createStructCopy(rw.dispatch(a), ref.decl, (f: InstanceField[_]) => StructCopyBeforeCallFailed(inv, f)) - case _ => throw WrongStructType(a) - } + getBaseType(a.t) match { + case CTStruct(ref) => createStructCopy(rw.dispatch(a), ref.decl, (f: InstanceField[_]) => StructCopyBeforeCallFailed(inv, f)) case _ => rw.dispatch(a) } ) diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala index 997dddcd86..980bbfe904 100644 --- a/src/viper/viper/api/transform/ColToSilver.scala +++ b/src/viper/viper/api/transform/ColToSilver.scala @@ -39,6 +39,8 @@ case class ColToSilver(program: col.Program[_]) { val currentMapGet: ScopedStack[col.MapGet[_]] = ScopedStack() val currentDividingExpr: ScopedStack[col.DividingExpr[_]] = ScopedStack() + var inTriggers = false + case class NotSupported(node: col.Node[_]) extends SystemError { override def text: String = program.highlight(node).messageInContext(s"This kind of node (${node.getClass.getSimpleName}) is not supported by silver directly. Is there a rewrite missing?") @@ -321,8 +323,12 @@ case class ColToSilver(program: col.Program[_]) { case starall @ col.Starall(bindings, triggers, body) => scoped { currentStarall.having(starall) { + val newBindings = bindings.map(variable) + inTriggers = true + val newTriggers = triggers.map(trigger) + inTriggers = false val foralls: Seq[silver.Forall] = silver.utility.QuantifiedPermissions.desugarSourceQuantifiedPermissionSyntax( - silver.Forall(bindings.map(variable), triggers.map(trigger), exp(body))(pos=pos(e), info=expInfo(e)) + silver.Forall(newBindings, newTriggers, exp(body))(pos=pos(e), info=expInfo(e)) ) foralls.reduce[silver.Exp] { case (l, r) => silver.And(l, r)(pos=pos(e), info=expInfo(e)) } @@ -350,6 +356,9 @@ case class ColToSilver(program: col.Program[_]) { permValue.info.asInstanceOf[NodeInfo[_]].permissionValuePermissionNode = Some(res) silver.FieldAccessPredicate(silver.FieldAccess(exp(obj), fields(field))(pos=pos(res), info=expInfo(res)), permValue)(pos=pos(res), info=expInfo(res)) case res: col.PredicateApply[_] => + if(inTriggers){ + return predInTrigger(res) + } val silver = pred(res) silver.perm.info.asInstanceOf[NodeInfo[_]].permissionValuePermissionNode = Some(res) silver @@ -468,6 +477,9 @@ case class ColToSilver(program: col.Program[_]) { def pred(p: col.PredicateApply[_]): silver.PredicateAccessPredicate = silver.PredicateAccessPredicate(silver.PredicateAccess(p.args.map(exp), ref(p.ref))(pos=pos(p), info=expInfo(p)), exp(p.perm))(pos=pos(p), info=expInfo(p)) + def predInTrigger(p: col.PredicateApply[_]): silver.PredicateAccess = + silver.PredicateAccess(p.args.map(exp), ref(p.ref))(pos=pos(p), info=expInfo(p)) + def acc(e: col.Expr[_]): silver.LocationAccess = e match { case col.PredicateApply(Ref(pred), args, _) => silver.PredicateAccess(args.map(exp), ref(pred))(pos=pos(pred), info=expInfo(pred)) case col.SilverDeref(obj, Ref(field)) => silver.FieldAccess(exp(obj), fields(field))(pos=pos(e), info=expInfo(e)) From 3452dc0024b16d90c3b38ed47e5eb5b194abeea4 Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 6 May 2024 19:10:31 +0200 Subject: [PATCH 2/3] Predicate triggers, float types math.h fixes --- res/universal/res/c/math.h | 207 +++++++++++++++++- .../ast/type/typeclass/FloatTypeImpl.scala | 8 +- .../ExtractInlineQuantifierPatterns.scala | 8 + src/rewrite/vct/rewrite/ResolveScale.scala | 2 +- 4 files changed, 211 insertions(+), 14 deletions(-) diff --git a/res/universal/res/c/math.h b/res/universal/res/c/math.h index c201da0c00..6f40141252 100644 --- a/res/universal/res/c/math.h +++ b/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; diff --git a/src/col/vct/col/ast/type/typeclass/FloatTypeImpl.scala b/src/col/vct/col/ast/type/typeclass/FloatTypeImpl.scala index f23abff2b4..5431475459 100644 --- a/src/col/vct/col/ast/type/typeclass/FloatTypeImpl.scala +++ b/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)) diff --git a/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala b/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala index 577e251d8b..07818f1783 100644 --- a/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala +++ b/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) } } diff --git a/src/rewrite/vct/rewrite/ResolveScale.scala b/src/rewrite/vct/rewrite/ResolveScale.scala index ecd90e986d..997a1510e2 100644 --- a/src/rewrite/vct/rewrite/ResolveScale.scala +++ b/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) } } From 8b621c85855fa3d5d8c6df2db68177b5ab28906f Mon Sep 17 00:00:00 2001 From: Lars Date: Mon, 6 May 2024 19:10:43 +0200 Subject: [PATCH 3/3] Increase stack size --- .mill-jvm-opts | 2 +- mill-build/util/src/util/JavaModule.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.mill-jvm-opts b/.mill-jvm-opts index e8d9149fc5..b28dfe06ac 100644 --- a/.mill-jvm-opts +++ b/.mill-jvm-opts @@ -1,2 +1,2 @@ --Xss32m +-Xss128m -Xmx2G diff --git a/mill-build/util/src/util/JavaModule.scala b/mill-build/util/src/util/JavaModule.scala index c95faae830..849d427c83 100644 --- a/mill-build/util/src/util/JavaModule.scala +++ b/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) }