From 455ed1f4973bc42576486a3797c9afc9d98bcecf Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Mon, 23 Oct 2023 18:01:32 +0200 Subject: [PATCH 1/7] add coercions for resource values, start working on encoding --- src/col/vct/col/ast/Node.scala | 8 + .../ResourceOfResourceValueImpl.scala | 7 + .../ast/expr/resource/ResourceValueImpl.scala | 7 + .../CoerceResourceResourceValImpl.scala | 7 + .../CoerceResourceValResourceImpl.scala | 7 + .../ast/family/coercion/CoercionImpl.scala | 3 + .../family/coercion/SomethingAnyImpl.scala | 2 +- .../coercion/SomethingAnyValueImpl.scala | 7 + ...lverPartialADTFunctionInvocationImpl.scala | 4 +- src/col/vct/col/ast/type/TAnyImpl.scala | 3 +- src/col/vct/col/ast/type/TAnyValueImpl.scala | 8 + .../vct/col/ast/type/TResourceValImpl.scala | 7 + src/col/vct/col/ast/type/TVarImpl.scala | 6 +- src/col/vct/col/feature/FeatureRainbow.scala | 3 +- src/col/vct/col/resolve/lang/Java.scala | 2 +- .../vct/col/typerules/CoercingRewriter.scala | 11 +- src/col/vct/col/typerules/CoercionUtils.scala | 12 +- src/col/vct/col/typerules/Types.scala | 8 +- src/col/vct/col/util/DeclarationBox.scala | 22 +++ .../vct/parsers/transform/CPPToCol.scala | 4 +- .../vct/parsers/transform/CToCol.scala | 4 +- .../vct/parsers/transform/JavaToCol.scala | 4 +- .../vct/parsers/transform/PVLToCol.scala | 4 +- .../vct/rewrite/EncodeProofHelpers.scala | 2 +- .../vct/rewrite/EncodeResourceValues.scala | 161 ++++++++++++++++++ .../vct/rewrite/ExplicitResourceValues.scala | 19 +++ .../rewrite/ResolveExpressionSideChecks.scala | 8 +- src/rewrite/vct/rewrite/adt/ImportADT.scala | 3 +- src/rewrite/vct/rewrite/adt/ImportAny.scala | 8 +- .../viper/api/transform/SilverToCol.scala | 2 +- 30 files changed, 315 insertions(+), 38 deletions(-) create mode 100644 src/col/vct/col/ast/expr/resource/ResourceOfResourceValueImpl.scala create mode 100644 src/col/vct/col/ast/expr/resource/ResourceValueImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceResourceResourceValImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/CoerceResourceValResourceImpl.scala create mode 100644 src/col/vct/col/ast/family/coercion/SomethingAnyValueImpl.scala create mode 100644 src/col/vct/col/ast/type/TAnyValueImpl.scala create mode 100644 src/col/vct/col/ast/type/TResourceValImpl.scala create mode 100644 src/col/vct/col/util/DeclarationBox.scala create mode 100644 src/rewrite/vct/rewrite/EncodeResourceValues.scala create mode 100644 src/rewrite/vct/rewrite/ExplicitResourceValues.scala diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index da1f74f45a..14331df515 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -108,10 +108,12 @@ final case class TMatrix[G](element: Type[G])(implicit val o: Origin = Diagnosti sealed trait PrimitiveType[G] extends Type[G] with PrimitiveTypeImpl[G] final case class TAny[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TAnyImpl[G] final case class TNothing[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TNothingImpl[G] +final case class TAnyValue[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TAnyValueImpl[G] final case class TVoid[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TVoidImpl[G] final case class TNull[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TNullImpl[G] final case class TBool[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TBoolImpl[G] final case class TResource[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TResourceImpl[G] +final case class TResourceVal[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TResourceValImpl[G] final case class TChar[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TCharImpl[G] final case class TString[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TStringImpl[G] final case class TRef[G]()(implicit val o: Origin = DiagnosticOrigin) extends PrimitiveType[G] with TRefImpl[G] @@ -335,11 +337,14 @@ final case class CoercionSequence[G](coercions: Seq[Coercion[G]])(implicit val o final case class CoerceNothingSomething[G](target: Type[G])(implicit val o: Origin) extends Coercion[G] with NothingSomethingImpl[G] final case class CoerceSomethingAny[G](source: Type[G])(implicit val o: Origin) extends Coercion[G] with SomethingAnyImpl[G] +final case class CoerceSomethingAnyValue[G](source: Type[G])(implicit val o: Origin) extends Coercion[G] with SomethingAnyValueImpl[G] final case class CoerceJoinUnion[G](inner: Seq[Coercion[G]], source: Seq[Type[G]], target: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceJoinUnionImpl[G] final case class CoerceSelectUnion[G](inner: Coercion[G], source: Type[G], targetAlts: Seq[Type[G]], index: Int)(implicit val o: Origin) extends Coercion[G] with CoerceSelectUnionImpl[G] final case class CoerceBoolResource[G]()(implicit val o: Origin) extends Coercion[G] with CoerceBoolResourceImpl[G] +final case class CoerceResourceResourceVal[G]()(implicit val o: Origin) extends Coercion[G] with CoerceResourceResourceValImpl[G] +final case class CoerceResourceValResource[G]()(implicit val o: Origin) extends Coercion[G] with CoerceResourceValResourceImpl[G] final case class CoerceNullRef[G]()(implicit val o: Origin) extends Coercion[G] with CoerceNullRefImpl[G] final case class CoerceNullArray[G](arrayElementType: Type[G])(implicit val o: Origin) extends Coercion[G] with CoerceNullArrayImpl[G] @@ -574,6 +579,9 @@ final case class ValidMatrix[G](mat: Expr[G], w: Expr[G], h: Expr[G])(implicit v final case class PermPointer[G](p: Expr[G], len: Expr[G], perm: Expr[G])(implicit val o: Origin) extends Expr[G] with PermPointerImpl[G] final case class PermPointerIndex[G](p: Expr[G], idx: Expr[G], perm: Expr[G])(implicit val o: Origin) extends Expr[G] with PermPointerIndexImpl[G] +final case class ResourceOfResourceValue[G](res: Expr[G])(implicit val o: Origin) extends Expr[G] with ResourceOfResourceValueImpl[G] +final case class ResourceValue[G](res: Expr[G])(implicit val o: Origin) extends Expr[G] with ResourceValueImpl[G] + sealed trait Comparison[G] extends BinExpr[G] with ComparisonImpl[G] final case class Eq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends Comparison[G] with EqImpl[G] final case class Neq[G](left: Expr[G], right: Expr[G])(implicit val o: Origin) extends Comparison[G] with NeqImpl[G] diff --git a/src/col/vct/col/ast/expr/resource/ResourceOfResourceValueImpl.scala b/src/col/vct/col/ast/expr/resource/ResourceOfResourceValueImpl.scala new file mode 100644 index 0000000000..583be4169c --- /dev/null +++ b/src/col/vct/col/ast/expr/resource/ResourceOfResourceValueImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.expr.resource + +import vct.col.ast.{ResourceOfResourceValue, TResource} + +trait ResourceOfResourceValueImpl[G] { this: ResourceOfResourceValue[G] => + override def t: TResource[G] = TResource() +} diff --git a/src/col/vct/col/ast/expr/resource/ResourceValueImpl.scala b/src/col/vct/col/ast/expr/resource/ResourceValueImpl.scala new file mode 100644 index 0000000000..375fb4263f --- /dev/null +++ b/src/col/vct/col/ast/expr/resource/ResourceValueImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.expr.resource + +import vct.col.ast.{ResourceValue, TResourceVal} + +trait ResourceValueImpl[G] { this: ResourceValue[G] => + override def t: TResourceVal[G] = TResourceVal() +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceResourceResourceValImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceResourceResourceValImpl.scala new file mode 100644 index 0000000000..7f404ef0fe --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceResourceResourceValImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceResourceResourceVal, TResourceVal} + +trait CoerceResourceResourceValImpl[G] { this: CoerceResourceResourceVal[G] => + override def target: TResourceVal[G] = TResourceVal() +} diff --git a/src/col/vct/col/ast/family/coercion/CoerceResourceValResourceImpl.scala b/src/col/vct/col/ast/family/coercion/CoerceResourceValResourceImpl.scala new file mode 100644 index 0000000000..82cbfa3ab0 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/CoerceResourceValResourceImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceResourceValResource, TResource} + +trait CoerceResourceValResourceImpl[G] { this: CoerceResourceValResource[G] => + override def target: TResource[G] = TResource() +} diff --git a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala index 722e6bd615..69e3f023e2 100644 --- a/src/col/vct/col/ast/family/coercion/CoercionImpl.scala +++ b/src/col/vct/col/ast/family/coercion/CoercionImpl.scala @@ -10,6 +10,7 @@ trait CoercionImpl[G] { this: Coercion[G] => case CoercionSequence(coercions) => coercions.forall(_.isPromoting) case CoerceNothingSomething(_) => true case CoerceSomethingAny(_) => true + case CoerceSomethingAnyValue(_) => true case CoerceJoinUnion(inner, _, _) => inner.forall(_.isPromoting) case CoerceSelectUnion(inner, _, _, _) => inner.isPromoting case CoerceBoolResource() => true @@ -39,6 +40,8 @@ trait CoercionImpl[G] { this: Coercion[G] => case CoerceColToCPPPrimitive(_, _) => true case CoerceCPPArrayPointer(_) => true case CoerceCArrayPointer(_) => true + case CoerceResourceResourceVal() => true + case CoerceResourceValResource() => true case CoerceMapOption(inner, _, _) => inner.isPromoting case CoerceMapTuple(inner, _, _) => inner.forall(_.isPromoting) case CoerceMapEither(inner, _, _) => inner._1.isPromoting && inner._2.isPromoting diff --git a/src/col/vct/col/ast/family/coercion/SomethingAnyImpl.scala b/src/col/vct/col/ast/family/coercion/SomethingAnyImpl.scala index 01967010cd..90db44441a 100644 --- a/src/col/vct/col/ast/family/coercion/SomethingAnyImpl.scala +++ b/src/col/vct/col/ast/family/coercion/SomethingAnyImpl.scala @@ -1,6 +1,6 @@ package vct.col.ast.family.coercion -import vct.col.ast.{CoerceSomethingAny, TAny, Type} +import vct.col.ast.{CoerceSomethingAny, Type, TAny} trait SomethingAnyImpl[G] { this: CoerceSomethingAny[G] => override def target: Type[G] = TAny() diff --git a/src/col/vct/col/ast/family/coercion/SomethingAnyValueImpl.scala b/src/col/vct/col/ast/family/coercion/SomethingAnyValueImpl.scala new file mode 100644 index 0000000000..fa89ae0818 --- /dev/null +++ b/src/col/vct/col/ast/family/coercion/SomethingAnyValueImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.family.coercion + +import vct.col.ast.{CoerceSomethingAnyValue, TAnyValue, Type} + +trait SomethingAnyValueImpl[G] { this: CoerceSomethingAnyValue[G] => + override def target: Type[G] = TAnyValue() +} diff --git a/src/col/vct/col/ast/lang/SilverPartialADTFunctionInvocationImpl.scala b/src/col/vct/col/ast/lang/SilverPartialADTFunctionInvocationImpl.scala index e45a204642..4cc73a990b 100644 --- a/src/col/vct/col/ast/lang/SilverPartialADTFunctionInvocationImpl.scala +++ b/src/col/vct/col/ast/lang/SilverPartialADTFunctionInvocationImpl.scala @@ -1,7 +1,7 @@ package vct.col.ast.lang -import vct.col.ast.{ADTFunction, AxiomaticDataType, SilverPartialADTFunctionInvocation, TAny, Type} -import vct.col.print.{Ctx, Doc, Precedence, Text, Group} +import vct.col.ast.{ADTFunction, AxiomaticDataType, SilverPartialADTFunctionInvocation, Type} +import vct.col.print._ import vct.col.ref.Ref trait SilverPartialADTFunctionInvocationImpl[G] { this: SilverPartialADTFunctionInvocation[G] => diff --git a/src/col/vct/col/ast/type/TAnyImpl.scala b/src/col/vct/col/ast/type/TAnyImpl.scala index b5afa08141..a6d2adeceb 100644 --- a/src/col/vct/col/ast/type/TAnyImpl.scala +++ b/src/col/vct/col/ast/type/TAnyImpl.scala @@ -1,8 +1,7 @@ package vct.col.ast.`type` import vct.col.ast.TAny -import vct.col.print.{Ctx, Doc, Text} trait TAnyImpl[G] { this: TAny[G] => - override def layout(implicit ctx: Ctx): Doc = Text("any") + } \ No newline at end of file diff --git a/src/col/vct/col/ast/type/TAnyValueImpl.scala b/src/col/vct/col/ast/type/TAnyValueImpl.scala new file mode 100644 index 0000000000..71fe965c34 --- /dev/null +++ b/src/col/vct/col/ast/type/TAnyValueImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.`type` + +import vct.col.ast.TAnyValue +import vct.col.print.{Ctx, Doc, Text} + +trait TAnyValueImpl[G] { this: TAnyValue[G] => + override def layout(implicit ctx: Ctx): Doc = Text("any") +} diff --git a/src/col/vct/col/ast/type/TResourceValImpl.scala b/src/col/vct/col/ast/type/TResourceValImpl.scala new file mode 100644 index 0000000000..d1c8f91a9c --- /dev/null +++ b/src/col/vct/col/ast/type/TResourceValImpl.scala @@ -0,0 +1,7 @@ +package vct.col.ast.`type` + +import vct.col.ast.TResourceVal + +trait TResourceValImpl[G] { this: TResourceVal[G] => + +} diff --git a/src/col/vct/col/ast/type/TVarImpl.scala b/src/col/vct/col/ast/type/TVarImpl.scala index a3ac92e292..ede22e75c6 100644 --- a/src/col/vct/col/ast/type/TVarImpl.scala +++ b/src/col/vct/col/ast/type/TVarImpl.scala @@ -1,14 +1,14 @@ package vct.col.ast.`type` -import vct.col.ast.{TAny, TType, TVar} +import vct.col.ast.{TAnyValue, TType, TVar} import vct.col.check.{CheckContext, CheckError, GenericTypeError} import vct.col.print.{Ctx, Doc, Text} trait TVarImpl[G] { this: TVar[G] => override def check(context: CheckContext[G]): Seq[CheckError] = context.checkInScope(this, ref) ++ - (if(TType(TAny()).superTypeOf(ref.decl.t)) Nil - else Seq(GenericTypeError(this, TType(TAny())))) + (if(TType(TAnyValue()).superTypeOf(ref.decl.t)) Nil + else Seq(GenericTypeError(this, TType(TAnyValue())))) override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref)) } \ No newline at end of file diff --git a/src/col/vct/col/feature/FeatureRainbow.scala b/src/col/vct/col/feature/FeatureRainbow.scala index e77482b95b..3de40ce258 100644 --- a/src/col/vct/col/feature/FeatureRainbow.scala +++ b/src/col/vct/col/feature/FeatureRainbow.scala @@ -140,7 +140,7 @@ class FeatureRainbow[G] { case node: CoerceNullRef[G] => Coercions case node: CoerceRatZFrac[G] => Coercions case node: CoerceSelectUnion[G] => Coercions - case node: CoerceSomethingAny[G] => Coercions + case node: CoerceSomethingAnyValue[G] => Coercions case node: CoerceSupports[G] => Coercions case node: CoerceUnboundInt[G] => Coercions case node: CoerceWidenBound[G] => Coercions @@ -258,6 +258,7 @@ class FeatureRainbow[G] { case node: SignalsClause[G] => Exceptions case node: TAny[G] => ExoticTypes + case node: TAnyValue[G] => ExoticTypes case node: TNothing[G] => ExoticTypes case node: TUnion[G] => ExoticTypes case node: TBoundedInt[G] => ExoticTypes diff --git a/src/col/vct/col/resolve/lang/Java.scala b/src/col/vct/col/resolve/lang/Java.scala index 25185ac9c7..01174033e1 100644 --- a/src/col/vct/col/resolve/lang/Java.scala +++ b/src/col/vct/col/resolve/lang/Java.scala @@ -5,7 +5,7 @@ import hre.io.RWFile import hre.util.FuncTools import vct.col.ast.lang.JavaAnnotationEx import vct.col.ast.`type`.TFloats -import vct.col.ast.{ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaModifier, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAny, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void} +import vct.col.ast.{ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaModifier, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void} import vct.col.origin._ import vct.col.ref.Ref import vct.col.resolve.ResolveTypes.JavaClassPathEntry diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala index 60dfd89f44..0135d6e91a 100644 --- a/src/col/vct/col/typerules/CoercingRewriter.scala +++ b/src/col/vct/col/typerules/CoercingRewriter.scala @@ -67,6 +67,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr case CoercionSequence(cs) => cs.foldLeft(e) { case (e, c) => applyCoercion(e, c) } case CoerceNothingSomething(_) => e case CoerceSomethingAny(_) => e + case CoerceSomethingAnyValue(_) => e case CoerceMapOption(inner, _, target) => Select(OptEmpty(e), OptNoneTyped(dispatch(target)), OptSomeTyped(dispatch(target), applyCoercion(OptGet(e)(NeverNone), inner))) case CoerceMapEither((innerLeft, innerRight), _, _) => @@ -165,6 +166,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr ??? case CoerceBoolResource() => e + case CoerceResourceResourceVal() => e + case CoerceResourceValResource() => e case CoerceBoundIntFrac() => e case CoerceBoundIntZFrac(_) => e case CoerceBoundIntFloat(_, _) => e @@ -1264,6 +1267,10 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr ReadPerm() case RemoveAt(xs, i) => RemoveAt(seq(xs)._1, int(i)) + case ResourceOfResourceValue(r) => + ResourceOfResourceValue(coerce(r, TResourceVal())) + case ResourceValue(r) => + ResourceValue(res(r)) case Result(ref) => Result(ref) case s @ Scale(scale, r) => @@ -1554,11 +1561,11 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr case Z3SeqLen(arg) => Z3SeqLen(z3seq(arg)._1) case Z3SeqMap(f, seq) => val (cf, arrt) = smtarr(f) - if(arrt.index.size != 1) coerce(f, TSmtlibArray(Seq(TAny()), arrt.value)) + if(arrt.index.size != 1) coerce(f, TSmtlibArray(Seq(TAnyValue()), arrt.value)) Z3SeqMap(cf, coerce(seq, TSmtlibSeq(arrt.index.head))) case Z3SeqMapI(f, offset, seq) => val (cf, arrt) = smtarr(f) - if(arrt.index.size != 2) coerce(f, TSmtlibArray(Seq(TInt(), TAny()), arrt.value)) + if(arrt.index.size != 2) coerce(f, TSmtlibArray(Seq(TInt(), TAnyValue()), arrt.value)) Z3SeqMapI(cf, int(offset), coerce(seq, TSmtlibSeq(arrt.index(1)))) case Z3SeqNth(seq, offset) => Z3SeqNth(z3seq(seq)._1, int(offset)) case Z3SeqPrefixOf(pre, subseq) => Z3SeqPrefixOf(z3seq(pre)._1, z3seq(subseq)._1) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 1e12e8dc3b..8e6e3c1979 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -15,7 +15,10 @@ case object CoercionUtils { case (TNothing(), _) => CoerceNothingSomething(target) case (_, TAny()) => CoerceSomethingAny(source) - + case (TResource(), TAnyValue()) => CoercionSequence(Seq(CoerceResourceResourceVal(), CoerceSomethingAnyValue(TResourceVal()))) + case (TResource(), TResourceVal()) => CoerceResourceResourceVal() + case (TResourceVal(), TResource()) => CoerceResourceValResource() + case (TBool(), TResource()) => CoerceBoolResource() case (source @ TOption(innerSource), target @ TOption(innerTarget)) => CoerceMapOption(getCoercion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget) @@ -60,7 +63,6 @@ case object CoercionUtils { case (_@CPPTArray(_, innerType), _@TArray(element)) if element == innerType => CoerceCPPArrayPointer(element) - case (TBool(), TResource()) => CoerceBoolResource() case (TFraction(), TZFraction()) => CoerceFracZFrac() case (TFraction(), TRational()) => CoercionSequence(Seq(CoerceFracZFrac(), CoerceZFracRat())) case (TZFraction(), TRational()) => CoerceZFracRat() @@ -236,7 +238,7 @@ case object CoercionUtils { case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyPointerCoercion) case t: CPPTArray[G] => Some((CoerceCPPArrayPointer(t.innerType), TPointer(t.innerType))) case _: TNull[G] => - val t = TPointer[G](TAny()) + val t = TPointer[G](TAnyValue()) Some((CoerceNullPointer(t), t)) case _ => None } @@ -258,7 +260,7 @@ case object CoercionUtils { case t: CPPPrimitiveType[G] => chainCPPCoercion(t, getAnyArrayCoercion) case t: TArray[G] => Some((CoerceIdentity(source), t)) case _: TNull[G] => - val t = TArray[G](TAny()) + val t = TArray[G](TAnyValue()) Some((CoerceNullArray(t), t)) case _ => None } @@ -269,7 +271,7 @@ case object CoercionUtils { case t @ TArray(TArray(_)) => Some((CoerceIdentity(source), t)) case TArray(TNull()) => Some(???) case TNull() => - val t = TArray[G](TArray[G](TAny())) + val t = TArray[G](TArray[G](TAnyValue())) Some((CoerceNullArray(t), t)) case _ => None } diff --git a/src/col/vct/col/typerules/Types.scala b/src/col/vct/col/typerules/Types.scala index 6c5aeb464b..cd50410071 100644 --- a/src/col/vct/col/typerules/Types.scala +++ b/src/col/vct/col/typerules/Types.scala @@ -47,7 +47,7 @@ object Types { case (TMap(leftK, leftV), TMap(rightK, rightV)) => // Map is not covariant in the key, so if the keys are inequal the best we can do is Any if(leftK == rightK) TMap(leftK, leastCommonSuperType(leftV, rightV)) - else TAny() + else TAnyValue() case (TType(left), TType(right)) => TType(leastCommonSuperType(left, right)) @@ -83,6 +83,10 @@ object Types { case (left, right) if TRational().superTypeOf(left) && TRational().superTypeOf(right) => TRational() - case (_, _) => TAny() + case (left, right) if TAnyValue().superTypeOf(left) && TAnyValue().superTypeOf(right) => + TAnyValue() + + case (_, _) => + TAny() } } \ No newline at end of file diff --git a/src/col/vct/col/util/DeclarationBox.scala b/src/col/vct/col/util/DeclarationBox.scala new file mode 100644 index 0000000000..b4b1ff81ef --- /dev/null +++ b/src/col/vct/col/util/DeclarationBox.scala @@ -0,0 +1,22 @@ +package vct.col.util + +import vct.col.ast.Declaration +import vct.col.ref.{LazyRef, Ref} + +import scala.reflect.ClassTag + +case class DeclarationBox[G, Decl <: Declaration[G]]()(implicit tag: ClassTag[Decl]) { + private var decl: Option[Decl] = None + + def ref: Ref[G, Decl] = new LazyRef(decl.get) + + def isFilled: Boolean = decl.isDefined + def isEmpty: Boolean = decl.isEmpty + + def get: Decl = decl.get + + def fill[T <: Decl](decl: T): T = { + this.decl = Some(decl) + decl + } +} diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala index 85dfa10bf9..13e21ea5d7 100644 --- a/src/parsers/vct/parsers/transform/CPPToCol.scala +++ b/src/parsers/vct/parsers/transform/CPPToCol.scala @@ -1224,7 +1224,7 @@ case class CPPToCol[G](override val baseOrigin: Origin, def convert(implicit ts: ValTypeVarsContext): Seq[Variable[G]] = ts match { case ValTypeVars0(_, names, _) => - convert(names).map(name => new Variable(TType(TAny()))(origin(ts).replacePrefName(name))) + convert(names).map(name => new Variable(TType(TAnyValue()))(origin(ts).replacePrefName(name))) } def convert(implicit decl: ValAdtDeclarationContext): ADTDeclaration[G] = decl match { @@ -1257,7 +1257,7 @@ case class CPPToCol[G](override val baseOrigin: Origin, case "rational" => TRational() case "bool" => TBool() case "ref" => TRef() - case "any" => TAny() + case "any" => TAnyValue() case "nothing" => TNothing() } case ValSeqType(_, _, element, _) => TSeq(convert(element)) diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index 6ebd859590..f287b9d2cf 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -939,7 +939,7 @@ case class CToCol[G](override val baseOrigin: Origin, def convert(implicit ts: ValTypeVarsContext): Seq[Variable[G]] = ts match { case ValTypeVars0(_, names, _) => - convert(names).map(name => new Variable(TType(TAny()))(origin(ts).replacePrefName(name))) + convert(names).map(name => new Variable(TType(TAnyValue()))(origin(ts).replacePrefName(name))) } def convert(implicit decl: ValAdtDeclarationContext): ADTDeclaration[G] = decl match { @@ -968,7 +968,7 @@ case class CToCol[G](override val baseOrigin: Origin, case "rational" => TRational() case "bool" => TBool() case "ref" => TRef() - case "any" => TAny() + case "any" => TAnyValue() case "nothing" => TNothing() } case ValSeqType(_, _, element, _) => TSeq(convert(element)) diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala index 842b875408..87711f0474 100644 --- a/src/parsers/vct/parsers/transform/JavaToCol.scala +++ b/src/parsers/vct/parsers/transform/JavaToCol.scala @@ -1300,7 +1300,7 @@ case class JavaToCol[G](override val baseOrigin: Origin, def convert(implicit ts: ValTypeVarsContext): Seq[Variable[G]] = ts match { case ValTypeVars0(_, names, _) => - convert(names).map(name => new Variable(TType(TAny()))(origin(ts).replacePrefName(name))) + convert(names).map(name => new Variable(TType(TAnyValue()))(origin(ts).replacePrefName(name))) } def convert(implicit decl: ValAdtDeclarationContext): ADTDeclaration[G] = decl match { @@ -1329,7 +1329,7 @@ case class JavaToCol[G](override val baseOrigin: Origin, case "rational" => TRational() case "bool" => TBool() case "ref" => TRef() - case "any" => TAny() + case "any" => TAnyValue() case "nothing" => TNothing() case "string" => TString() } diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 91c2bbe577..6ae8769505 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -969,7 +969,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, def convert(implicit ts: ValTypeVarsContext): Seq[Variable[G]] = ts match { case ValTypeVars0(_, names, _) => - convert(names).map(name => new Variable(TType(TAny()))(origin(ts).replacePrefName(name))) + convert(names).map(name => new Variable(TType(TAnyValue()))(origin(ts).replacePrefName(name))) } def convert(implicit decl: ValAdtDeclarationContext): ADTDeclaration[G] = decl match { @@ -998,7 +998,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, case "rational" => TRational() case "bool" => TBool() case "ref" => TRef() - case "any" => TAny() + case "any" => TAnyValue() case "nothing" => TNothing() case "string" => TString() } diff --git a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala b/src/rewrite/vct/rewrite/EncodeProofHelpers.scala index 05b32c8a91..2be12675af 100644 --- a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala +++ b/src/rewrite/vct/rewrite/EncodeProofHelpers.scala @@ -64,7 +64,7 @@ case class EncodeProofHelpers[Pre <: Generation](inferHeapContextIntoFrame: Bool implicit val o: Origin = stat.o val beforeLabel = new LabelDecl[Post]()(Before) - val locValue = new Variable[Post](TAny())(BeforeVar("x")) + val locValue = new Variable[Post](TAnyValue())(BeforeVar("x")) val allLocationsSame = ForPermWithValue(locValue, locValue.get === Old(locValue.get, Some(beforeLabel.ref))(PanicBlame("loop body reached after label before it"))) val allLocationsSameOnInhale = diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala new file mode 100644 index 0000000000..174e18547d --- /dev/null +++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala @@ -0,0 +1,161 @@ +package vct.rewrite + +import hre.util.ScopedStack +import vct.col.ast +import vct.col.ast._ +import vct.col.origin.Origin +import vct.col.rewrite.ResolveScale.WrongScale +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.util.DeclarationBox +import vct.result.VerificationError.{SystemError, UserError} +import vct.rewrite.EncodeResourceValues.{UnknownResourceValue, UnsupportedResourceValue} +import vct.col.util.AstBuildHelpers.forall + +import scala.collection.mutable + +case object EncodeResourceValues extends RewriterBuilder { + override def key: String = "resourceValues2" + override def desc: String = "Encode resource value conversions." + + case class UnsupportedResourceValue(node: Node[_], kind: String) extends UserError { + override def code: String = "wrongResourceValue" + override def text: String = + node.o.messageInContext(s"$kind cannot yet be stored in a resource value") + } + + case class UnknownResourceValue(node: Expr[_]) extends SystemError { + override def text: String = node.o.messageInContext("Unknown resource kind") + } +} + +case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] { + sealed trait ResourcePattern + + object ResourcePattern { + import vct.col.{ast => col} + object Bool extends ResourcePattern + case class Perm(loc: ResourcePatternLoc) extends ResourcePattern + case class Value(loc: ResourcePatternLoc) extends ResourcePattern + case class Predicate(p: col.Predicate[Pre]) extends ResourcePattern + case class InstancePredicate(p: col.InstancePredicate[Pre]) extends ResourcePattern + case class Star(left: ResourcePattern, right: ResourcePattern) extends ResourcePattern + case class Implies(res: ResourcePattern) extends ResourcePattern + case class Select(whenTrue: ResourcePattern, whenFalse: ResourcePattern) extends ResourcePattern + // Let, Starall: probably need to support lambda's first? + // Scale: I don't know about wf concerns, maybe just encode it away first? + + sealed trait ResourcePatternLoc + final case class HeapVariableLocation(ref: col.HeapVariable[Pre]) extends ResourcePatternLoc + final case class FieldLocation(ref: col.InstanceField[Pre]) extends ResourcePatternLoc + final case class ModelLocation(ref: col.ModelField[Pre]) extends ResourcePatternLoc + final case class SilverFieldLocation(ref: col.SilverField[Pre]) extends ResourcePatternLoc + final case class ArrayLocation(t: Type[Pre]) extends ResourcePatternLoc + final case class PointerLocation(t: Type[Pre]) extends ResourcePatternLoc + final case class PredicateLocation(ref: col.Predicate[Pre]) extends ResourcePatternLoc + final case class InstancePredicateLocation(ref: col.InstancePredicate[Pre]) extends ResourcePatternLoc + + def scan(loc: col.Location[Pre]): ResourcePatternLoc = loc match { + case col.HeapVariableLocation(ref) => HeapVariableLocation(ref.decl) + case col.FieldLocation(_, field) => FieldLocation(field.decl) + case col.ModelLocation(_, field) => ModelLocation(field.decl) + case col.SilverFieldLocation(_, field) => SilverFieldLocation(field.decl) + case col.ArrayLocation(arr, _) => ArrayLocation(arr.t.asArray.get.element) + case col.PointerLocation(ptr) => PointerLocation(ptr.t.asPointer.get.element) + case col.PredicateLocation(predicate, _) => PredicateLocation(predicate.decl) + case col.InstancePredicateLocation(predicate, _, _) => InstancePredicateLocation(predicate.decl) + case AmbiguousLocation(expr) => throw UnknownResourceValue(expr) + } + + def scan(e: Expr[Pre]): ResourcePattern = e match { + case s: Scale[Pre] => throw UnsupportedResourceValue(s, "Scaled resources") + case s: Starall[Pre] => throw UnsupportedResourceValue(s, "Quantified resources") + case l: Let[Pre] => throw UnsupportedResourceValue(l, "Let expressions") + + case e if TBool().superTypeOf(e.t) => Bool + case col.Perm(loc, _) => Perm(scan(loc)) + case col.Value(loc) => Value(scan(loc)) + case apply: PredicateApply[Pre] => Predicate(apply.ref.decl) + case apply: InstancePredicateApply[Pre] => InstancePredicate(apply.ref.decl) + + case col.Star(left, right) => Star(scan(left), scan(right)) + case col.Implies(_, res) => Implies(scan(res)) + case col.Select(_, whenTrue, whenFalse) => Select(scan(whenTrue), scan(whenFalse)) + + case other => throw UnknownResourceValue(other) + } + } + + case class PatternBuilder(index: Int, toValue: Expr[Pre] => Expr[Post], fromValue: Expr[Pre] => Expr[Post]) + + val patternBuilders: ScopedStack[Map[ResourcePattern, PatternBuilder]] = ScopedStack() + + override def dispatch(program: Program[Pre]): Program[Post] = { + implicit val o: Origin = program.o + + val patterns = program.collect { + case ResourceValue(res) => ResourcePattern.scan(res) + } + + if (patterns.isEmpty) { + return patternBuilders.having(Map.empty) { + rewriteDefault(program) + } + } + + val fieldOwner = program.flatCollect { + case cls: Class[Pre] => cls.collect { + case field: Field[Pre] => field -> cls + } + }.toMap + + val modelFieldOwner = program.flatCollect { + case model: Model[Pre] => model.collect { + case field: ModelField[Pre] => field -> model + } + }.toMap + + val predicateOwner = program.flatCollect { + case cls: Class[Pre] => cls.collect { + case pred: InstancePredicate[Pre] => pred -> cls + } + }.toMap + + val m = mutable.Map[ResourcePattern, PatternBuilder]() + + val adt = DeclarationBox[Post, AxiomaticDataType[Post]]() + val valType = TAxiomatic(adt.ref, Nil) + val kind = new ADTFunction[Post](Seq(new Variable(valType)), TInt()) + + val decls = patterns.zipWithIndex.flatMap { case (pattern, index) => + def freeTypesLoc(location: ResourcePattern.ResourcePatternLoc): Seq[Type[Post]] = location match { + case ResourcePattern.HeapVariableLocation(_) => Nil + case ResourcePattern.FieldLocation(f) => Seq(TClass(succ(fieldOwner(f)))) + case ResourcePattern.ModelLocation(f) => Seq(TModel(succ(modelFieldOwner(f)))) + case ResourcePattern.SilverFieldLocation(_) => Seq(TRef()) + case ResourcePattern.ArrayLocation(t) => Seq(TArray(dispatch(t)), TInt()) + case ResourcePattern.PointerLocation(t) => Seq(TPointer(dispatch(t))) + case ResourcePattern.PredicateLocation(ref) => ref.args.map(_.t).map(dispatch) + case ResourcePattern.InstancePredicateLocation(ref) => TClass[Post](succ(predicateOwner(ref))) +: ref.args.map(_.t).map(dispatch) + } + + def freeTypes(pattern: ResourcePattern): Seq[Type[Post]] = pattern match { + case ResourcePattern.Bool => Nil + case ResourcePattern.Perm(loc) => freeTypesLoc(loc) :+ TRational() + case ResourcePattern.Value(loc) => freeTypesLoc(loc) + case ResourcePattern.Predicate(p) => p.args.map(_.t).map(dispatch) + case ResourcePattern.InstancePredicate(p) => TClass[Post](succ(predicateOwner(p))) +: p.args.map(_.t).map(dispatch) + case ResourcePattern.Star(left, right) => freeTypes(left) ++ freeTypes(right) + case ResourcePattern.Implies(res) => freeTypes(res) + case ResourcePattern.Select(whenTrue, whenFalse) => freeTypes(whenTrue) ++ freeTypes(whenFalse) + } + + val ts = freeTypes(pattern) + + Nil + } + + patternBuilders.having(m.toMap) { + rewriteDefault(program) + } + } +} diff --git a/src/rewrite/vct/rewrite/ExplicitResourceValues.scala b/src/rewrite/vct/rewrite/ExplicitResourceValues.scala new file mode 100644 index 0000000000..71513f0333 --- /dev/null +++ b/src/rewrite/vct/rewrite/ExplicitResourceValues.scala @@ -0,0 +1,19 @@ +package vct.rewrite + +import vct.col.ast.{CoerceResourceResourceVal, CoerceResourceValResource, Coercion, Expr, ResourceOfResourceValue, ResourceValue} +import vct.col.origin.Origin +import vct.col.rewrite.{Generation, RewriterBuilder} +import vct.col.typerules.CoercingRewriter + +case object ExplicitResourceValues extends RewriterBuilder { + override def key: String = "resourceValues1" + override def desc: String = "Encode resoure value <-> resource conversion explicitly in the AST for later accounting." +} + +case class ExplicitResourceValues[Pre <: Generation]() extends CoercingRewriter[Pre] { + override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(implicit o: Origin): Expr[Post] = coercion match { + case CoerceResourceResourceVal() => ResourceValue(e) + case CoerceResourceValResource() => ResourceOfResourceValue(e) + case other => super.applyCoercion(e, other) + } +} diff --git a/src/rewrite/vct/rewrite/ResolveExpressionSideChecks.scala b/src/rewrite/vct/rewrite/ResolveExpressionSideChecks.scala index c45011a400..b87edf7e74 100644 --- a/src/rewrite/vct/rewrite/ResolveExpressionSideChecks.scala +++ b/src/rewrite/vct/rewrite/ResolveExpressionSideChecks.scala @@ -26,8 +26,8 @@ case class ResolveExpressionSideChecks[Pre <: Generation]() extends Rewriter[Pre lazy val withEval: Function[Post] = { implicit val o: Origin = EvalCheckFunction() - val t = new Variable[Post](TType(TAny()))(EvalCheckFunction("T")) - val checkValue = new Variable[Post](TAny())(EvalCheckFunction("checkedValue")) + val t = new Variable[Post](TType(TAnyValue()))(EvalCheckFunction("T")) + val checkValue = new Variable[Post](TAnyValue())(EvalCheckFunction("checkedValue")) val value = new Variable[Post](TVar(t.ref))(EvalCheckFunction("value")) globalDeclarations.declare(function[Post]( @@ -43,9 +43,9 @@ case class ResolveExpressionSideChecks[Pre <: Generation]() extends Rewriter[Pre lazy val thenEval: Function[Post] = { implicit val o: Origin = EvalCheckFunction() - val t = new Variable[Post](TType(TAny()))(EvalCheckFunction("T")) + val t = new Variable[Post](TType(TAnyValue()))(EvalCheckFunction("T")) val value = new Variable[Post](TVar(t.ref))(EvalCheckFunction("value")) - val checkValue = new Variable[Post](TAny())(EvalCheckFunction("checkedValue")) + val checkValue = new Variable[Post](TAnyValue())(EvalCheckFunction("checkedValue")) globalDeclarations.declare(function[Post]( blame = PanicBlame("theneval ensures nothing"), diff --git a/src/rewrite/vct/rewrite/adt/ImportADT.scala b/src/rewrite/vct/rewrite/adt/ImportADT.scala index ebd6050a41..8c69a82ad6 100644 --- a/src/rewrite/vct/rewrite/adt/ImportADT.scala +++ b/src/rewrite/vct/rewrite/adt/ImportADT.scala @@ -49,7 +49,8 @@ case object ImportADT { case TBag(element) => "bag_" + typeText(element) case TMatrix(element) => "mat_" + typeText(element) case TType(t) => "typ_" + typeText(t) - case TAny() => "any" + case TAny() => "top" + case TAnyValue() => "any" case TNothing() => "nothing" case TNull() => "null" case TResource() => "res" diff --git a/src/rewrite/vct/rewrite/adt/ImportAny.scala b/src/rewrite/vct/rewrite/adt/ImportAny.scala index 93eb10407e..39817d469c 100644 --- a/src/rewrite/vct/rewrite/adt/ImportAny.scala +++ b/src/rewrite/vct/rewrite/adt/ImportAny.scala @@ -1,7 +1,7 @@ package vct.col.rewrite.adt import hre.util.ScopedStack -import vct.col.ast.{AxiomaticDataType, CoerceSomethingAny, Coercion, Expr, Function, FunctionInvocation, TAny, TAxiomatic, TType, Type} +import vct.col.ast.{AxiomaticDataType, CoerceSomethingAnyValue, Coercion, Expr, Function, FunctionInvocation, TAnyValue, TAxiomatic, TType, Type} import vct.col.origin.{Origin, PanicBlame} import vct.col.ref.LazyRef import vct.col.rewrite.Generation @@ -17,17 +17,17 @@ case class ImportAny[Pre <: Generation](importer: ImportADTImporter) extends Imp private lazy val anyFrom = find[Function[Post]](anyFile, "as_any") override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(implicit o: Origin): Expr[Post] = coercion match { - case CoerceSomethingAny(source) => + case CoerceSomethingAnyValue(source) => FunctionInvocation[Post](anyFrom.ref, Seq(e), Seq(dispatch(source)), Nil, Nil)(PanicBlame("coercing to any requires nothing.")) case other => super.applyCoercion(e, other) } override def postCoerce(t: Type[Pre]): Type[Post] = t match { - case TType(TAny()) => + case TType(TAnyValue()) => // Only the any adt definition refers to itself, so this is the only place this trick is necessary. if(inAnyLoad.isEmpty) rewriteDefault(t) else TType(TAxiomatic(new LazyRef(anyAdt), Nil)) - case TAny() => TAxiomatic(anyAdt.ref, Nil) + case TAnyValue() => TAxiomatic(anyAdt.ref, Nil) case other => rewriteDefault(other) } } diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala index d8a42ff875..7ca3bb670c 100644 --- a/src/viper/viper/api/transform/SilverToCol.scala +++ b/src/viper/viper/api/transform/SilverToCol.scala @@ -111,7 +111,7 @@ case class SilverToCol[G](program: silver.Program, blameProvider: BlameProvider) )(origin(domain)) def transform(o: Origin)(tVar: silver.TypeVar): col.Variable[G] = - new col.Variable(col.TType(col.TAny()))(o.replacePrefName(tVar.name)) + new col.Variable(col.TType(col.TAnyValue()))(o.replacePrefName(tVar.name)) def transform(func: silver.DomainFunc): col.ADTFunction[G] = new col.ADTFunction( From e5b65c9fab080b709c5ca477bc1120c5fd38fa8f Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Mon, 23 Oct 2023 22:14:02 +0200 Subject: [PATCH 2/7] finish adt encoding --- src/main/vct/main/stages/Transformation.scala | 4 +- .../vct/parsers/transform/CPPToCol.scala | 2 +- .../vct/parsers/transform/CToCol.scala | 2 +- .../vct/parsers/transform/JavaToCol.scala | 2 +- .../vct/parsers/transform/PVLToCol.scala | 2 +- .../vct/rewrite/EncodeResourceValues.scala | 112 ++++++++++++------ 6 files changed, 81 insertions(+), 43 deletions(-) diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index 8b7b6f6243..d697d578ed 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -22,7 +22,7 @@ import vct.options.Options import vct.options.types.{Backend, PathOrStd} import vct.resources.Resources import vct.result.VerificationError.SystemError -import vct.rewrite.HeapVariableToRef +import vct.rewrite.{EncodeResourceValues, ExplicitResourceValues, HeapVariableToRef} import vct.rewrite.lang.ReplaceSYCLTypes object Transformation { @@ -211,6 +211,8 @@ case class SilverTransformation InlineApplicables, PureMethodsToFunctions, RefuteToInvertedAssert, + ExplicitResourceValues, + EncodeResourceValues, // Encode parallel blocks EncodeSendRecv, diff --git a/src/parsers/vct/parsers/transform/CPPToCol.scala b/src/parsers/vct/parsers/transform/CPPToCol.scala index 13e21ea5d7..7a3d6e8726 100644 --- a/src/parsers/vct/parsers/transform/CPPToCol.scala +++ b/src/parsers/vct/parsers/transform/CPPToCol.scala @@ -1250,7 +1250,7 @@ case class CPPToCol[G](override val baseOrigin: Origin, def convert(implicit t: ValTypeContext): Type[G] = t match { case ValPrimaryType(name) => name match { - case "resource" => TResource() + case "resource" => TResourceVal() case "process" => TProcess() case "frac" => TFraction() case "zfrac" => TZFraction() diff --git a/src/parsers/vct/parsers/transform/CToCol.scala b/src/parsers/vct/parsers/transform/CToCol.scala index f287b9d2cf..6fc1dcbd47 100644 --- a/src/parsers/vct/parsers/transform/CToCol.scala +++ b/src/parsers/vct/parsers/transform/CToCol.scala @@ -961,7 +961,7 @@ case class CToCol[G](override val baseOrigin: Origin, def convert(implicit t: ValTypeContext): Type[G] = t match { case ValPrimaryType(name) => name match { - case "resource" => TResource() + case "resource" => TResourceVal() case "process" => TProcess() case "frac" => TFraction() case "zfrac" => TZFraction() diff --git a/src/parsers/vct/parsers/transform/JavaToCol.scala b/src/parsers/vct/parsers/transform/JavaToCol.scala index 87711f0474..78108b70b8 100644 --- a/src/parsers/vct/parsers/transform/JavaToCol.scala +++ b/src/parsers/vct/parsers/transform/JavaToCol.scala @@ -1322,7 +1322,7 @@ case class JavaToCol[G](override val baseOrigin: Origin, def convert(implicit t: ValTypeContext): Type[G] = t match { case ValPrimaryType(name) => name match { - case "resource" => TResource() + case "resource" => TResourceVal() case "process" => TProcess() case "frac" => TFraction() case "zfrac" => TZFraction() diff --git a/src/parsers/vct/parsers/transform/PVLToCol.scala b/src/parsers/vct/parsers/transform/PVLToCol.scala index 6ae8769505..7cb11b97de 100644 --- a/src/parsers/vct/parsers/transform/PVLToCol.scala +++ b/src/parsers/vct/parsers/transform/PVLToCol.scala @@ -991,7 +991,7 @@ case class PVLToCol[G](override val baseOrigin: Origin, def convert(implicit t: ValTypeContext): Type[G] = t match { case ValPrimaryType(name) => name match { - case "resource" => TResource() + case "resource" => TResourceVal() case "process" => TProcess() case "frac" => TFraction() case "zfrac" => TZFraction() diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala index 174e18547d..f7261ffdca 100644 --- a/src/rewrite/vct/rewrite/EncodeResourceValues.scala +++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala @@ -1,15 +1,17 @@ package vct.rewrite +import com.typesafe.scalalogging.LazyLogging import hre.util.ScopedStack import vct.col.ast -import vct.col.ast._ +import vct.col.ast.RewriteHelpers.RewriteProgram +import vct.col.ast.{Forall, _} import vct.col.origin.Origin import vct.col.rewrite.ResolveScale.WrongScale import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.util.DeclarationBox import vct.result.VerificationError.{SystemError, UserError} import vct.rewrite.EncodeResourceValues.{UnknownResourceValue, UnsupportedResourceValue} -import vct.col.util.AstBuildHelpers.forall +import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const, forall} import scala.collection.mutable @@ -28,7 +30,7 @@ case object EncodeResourceValues extends RewriterBuilder { } } -case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] { +case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging { sealed trait ResourcePattern object ResourcePattern { @@ -88,13 +90,14 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] { case class PatternBuilder(index: Int, toValue: Expr[Pre] => Expr[Post], fromValue: Expr[Pre] => Expr[Post]) val patternBuilders: ScopedStack[Map[ResourcePattern, PatternBuilder]] = ScopedStack() + val valAdt: ScopedStack[AxiomaticDataType[Post]] = ScopedStack() override def dispatch(program: Program[Pre]): Program[Post] = { implicit val o: Origin = program.o val patterns = program.collect { case ResourceValue(res) => ResourcePattern.scan(res) - } + }.toIndexedSeq if (patterns.isEmpty) { return patternBuilders.having(Map.empty) { @@ -120,42 +123,75 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] { } }.toMap - val m = mutable.Map[ResourcePattern, PatternBuilder]() - - val adt = DeclarationBox[Post, AxiomaticDataType[Post]]() - val valType = TAxiomatic(adt.ref, Nil) - val kind = new ADTFunction[Post](Seq(new Variable(valType)), TInt()) - - val decls = patterns.zipWithIndex.flatMap { case (pattern, index) => - def freeTypesLoc(location: ResourcePattern.ResourcePatternLoc): Seq[Type[Post]] = location match { - case ResourcePattern.HeapVariableLocation(_) => Nil - case ResourcePattern.FieldLocation(f) => Seq(TClass(succ(fieldOwner(f)))) - case ResourcePattern.ModelLocation(f) => Seq(TModel(succ(modelFieldOwner(f)))) - case ResourcePattern.SilverFieldLocation(_) => Seq(TRef()) - case ResourcePattern.ArrayLocation(t) => Seq(TArray(dispatch(t)), TInt()) - case ResourcePattern.PointerLocation(t) => Seq(TPointer(dispatch(t))) - case ResourcePattern.PredicateLocation(ref) => ref.args.map(_.t).map(dispatch) - case ResourcePattern.InstancePredicateLocation(ref) => TClass[Post](succ(predicateOwner(ref))) +: ref.args.map(_.t).map(dispatch) - } - - def freeTypes(pattern: ResourcePattern): Seq[Type[Post]] = pattern match { - case ResourcePattern.Bool => Nil - case ResourcePattern.Perm(loc) => freeTypesLoc(loc) :+ TRational() - case ResourcePattern.Value(loc) => freeTypesLoc(loc) - case ResourcePattern.Predicate(p) => p.args.map(_.t).map(dispatch) - case ResourcePattern.InstancePredicate(p) => TClass[Post](succ(predicateOwner(p))) +: p.args.map(_.t).map(dispatch) - case ResourcePattern.Star(left, right) => freeTypes(left) ++ freeTypes(right) - case ResourcePattern.Implies(res) => freeTypes(res) - case ResourcePattern.Select(whenTrue, whenFalse) => freeTypes(whenTrue) ++ freeTypes(whenFalse) + program.rewrite(globalDeclarations.collect { + val adt = DeclarationBox[Post, AxiomaticDataType[Post]]() + val valType = TAxiomatic(adt.ref, Nil) + val kind = new ADTFunction[Post](Seq(new Variable(valType)), TInt())(o.replacePrefName("kind")) + + val m = mutable.Map[ResourcePattern, PatternBuilder]() + + val decls = patterns.zipWithIndex.flatMap { case (pattern, index) => + def freeTypesLoc(location: ResourcePattern.ResourcePatternLoc): Seq[Type[Post]] = location match { + case ResourcePattern.HeapVariableLocation(_) => Nil + case ResourcePattern.FieldLocation(f) => Seq(TClass(succ(fieldOwner(f)))) + case ResourcePattern.ModelLocation(f) => Seq(TModel(succ(modelFieldOwner(f)))) + case ResourcePattern.SilverFieldLocation(_) => Seq(TRef()) + case ResourcePattern.ArrayLocation(t) => Seq(TArray(dispatch(t)), TInt()) + case ResourcePattern.PointerLocation(t) => Seq(TPointer(dispatch(t))) + case ResourcePattern.PredicateLocation(ref) => ref.args.map(_.t).map(dispatch) + case ResourcePattern.InstancePredicateLocation(ref) => TClass[Post](succ(predicateOwner(ref))) +: ref.args.map(_.t).map(dispatch) + } + + def freeTypes(pattern: ResourcePattern): Seq[Type[Post]] = pattern match { + case ResourcePattern.Bool => Nil + case ResourcePattern.Perm(loc) => freeTypesLoc(loc) :+ TRational() + case ResourcePattern.Value(loc) => freeTypesLoc(loc) + case ResourcePattern.Predicate(p) => p.args.map(_.t).map(dispatch) + case ResourcePattern.InstancePredicate(p) => TClass[Post](succ(predicateOwner(p))) +: p.args.map(_.t).map(dispatch) + case ResourcePattern.Star(left, right) => freeTypes(left) ++ freeTypes(right) + case ResourcePattern.Implies(res) => freeTypes(res) + case ResourcePattern.Select(whenTrue, whenFalse) => freeTypes(whenTrue) ++ freeTypes(whenFalse) + } + + val ts = freeTypes(pattern) + + val buildFunc = new ADTFunction(ts.map(new Variable[Post](_)), valType)(o.replacePrefName(s"ResVal$index")) + + val kindAxiom = { + val vars = ts.map(new Variable[Post](_)(o.replacePrefName("x"))) + new ADTAxiom(Forall( + vars, + Nil, + ADTFunctionInvocation[Post](Some(adt.ref -> Nil), kind.ref, Seq( + ADTFunctionInvocation[Post](Some(adt.ref -> Nil), buildFunc.ref, vars.map(v => Local[Post](v.ref))) + )) === const(index) + )) + } + + val getters = ts.zipWithIndex.map { case (t, typeIndex) => + new ADTFunction[Post](Seq(new Variable(valType)(o.replacePrefName("val"))), t)(o.replacePrefName(s"ResVal${index}_get$typeIndex")) + } + + val getterAxioms = ts.zipWithIndex.map { case (t, index) => + val vars = ts.map(new Variable[Post](_)(o.replacePrefName("x"))) + new ADTAxiom(Forall( + vars, + Nil, + ADTFunctionInvocation[Post](Some(adt.ref -> Nil), getters(index).ref, Seq( + ADTFunctionInvocation[Post](Some(adt.ref -> Nil), buildFunc.ref, vars.map(v => Local[Post](v.ref))) + )) === Local(vars(index).ref) + + )) + } + + buildFunc +: kindAxiom +: (getters ++ getterAxioms) } - val ts = freeTypes(pattern) + adt.fill(globalDeclarations.declare(new AxiomaticDataType[Post](kind +: decls, Nil)(o.replacePrefName("ResourceVal")))) - Nil - } - - patternBuilders.having(m.toMap) { - rewriteDefault(program) - } + patternBuilders.having(m.toMap) { + program.declarations.foreach(dispatch) + } + }._1) } } From 865a2c1a4975be5b9b64ea1014e20ba9cb73e17f Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 24 Oct 2023 14:42:01 +0200 Subject: [PATCH 3/7] make value builder and unbuilder, finish encoding --- .../vct/rewrite/EncodeResourceValues.scala | 137 +++++++++++++++++- 1 file changed, 130 insertions(+), 7 deletions(-) diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala index f7261ffdca..acb7130005 100644 --- a/src/rewrite/vct/rewrite/EncodeResourceValues.scala +++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala @@ -5,12 +5,12 @@ import hre.util.ScopedStack import vct.col.ast import vct.col.ast.RewriteHelpers.RewriteProgram import vct.col.ast.{Forall, _} -import vct.col.origin.Origin +import vct.col.origin.{Origin, PanicBlame} import vct.col.rewrite.ResolveScale.WrongScale -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten} import vct.col.util.DeclarationBox import vct.result.VerificationError.{SystemError, UserError} -import vct.rewrite.EncodeResourceValues.{UnknownResourceValue, UnsupportedResourceValue} +import vct.rewrite.EncodeResourceValues.{UnknownResourceValue, UnsupportedResourceValue, WrongResourcePattern} import vct.col.util.AstBuildHelpers.{ExprBuildHelpers, const, forall} import scala.collection.mutable @@ -28,6 +28,10 @@ case object EncodeResourceValues extends RewriterBuilder { case class UnknownResourceValue(node: Expr[_]) extends SystemError { override def text: String = node.o.messageInContext("Unknown resource kind") } + + case class WrongResourcePattern(node: Node[_]) extends SystemError { + override def text: String = node.o.messageInContext("Wrong resource pattern encoding") + } } case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with LazyLogging { @@ -87,10 +91,12 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with } } - case class PatternBuilder(index: Int, toValue: Expr[Pre] => Expr[Post], fromValue: Expr[Pre] => Expr[Post]) + case class PatternBuilder(index: Int, toValue: Expr[Pre] => Expr[Post], fromValue: Expr[Post] => Expr[Post]) val patternBuilders: ScopedStack[Map[ResourcePattern, PatternBuilder]] = ScopedStack() val valAdt: ScopedStack[AxiomaticDataType[Post]] = ScopedStack() + val kindFunc: ScopedStack[ADTFunction[Post]] = ScopedStack() + val arbitraryResourceValue: ScopedStack[Predicate[Post]] = ScopedStack() override def dispatch(program: Program[Pre]): Program[Post] = { implicit val o: Origin = program.o @@ -126,7 +132,7 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with program.rewrite(globalDeclarations.collect { val adt = DeclarationBox[Post, AxiomaticDataType[Post]]() val valType = TAxiomatic(adt.ref, Nil) - val kind = new ADTFunction[Post](Seq(new Variable(valType)), TInt())(o.replacePrefName("kind")) + val kind = new ADTFunction[Post](Seq(new Variable(valType)(o.replacePrefName("val"))), TInt())(o.replacePrefName("kind")) val m = mutable.Map[ResourcePattern, PatternBuilder]() @@ -155,7 +161,7 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with val ts = freeTypes(pattern) - val buildFunc = new ADTFunction(ts.map(new Variable[Post](_)), valType)(o.replacePrefName(s"ResVal$index")) + val buildFunc = new ADTFunction(ts.map(new Variable[Post](_)(o.replacePrefName("x"))), valType)(o.replacePrefName(s"ResVal$index")) val kindAxiom = { val vars = ts.map(new Variable[Post](_)(o.replacePrefName("x"))) @@ -184,14 +190,131 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with )) } + def makeLoc(loc: Location[Pre], pat: ResourcePattern.ResourcePatternLoc): Seq[Expr[Post]] = (pat, loc) match { + case ResourcePattern.HeapVariableLocation(_) -> HeapVariableLocation(_) => + Nil + case ResourcePattern.FieldLocation(_) -> FieldLocation(obj, _) => + Seq(dispatch(obj)) + case ResourcePattern.ModelLocation(_) -> ModelLocation(model, _) => + Seq(dispatch(model)) + case ResourcePattern.SilverFieldLocation(_) -> SilverFieldLocation(ref, _) => + Seq(dispatch(ref)) + case ResourcePattern.ArrayLocation(_) -> ArrayLocation(arr, idx) => + Seq(dispatch(arr), dispatch(idx)) + case ResourcePattern.PointerLocation(_) -> PointerLocation(ptr) => + Seq(dispatch(ptr)) + case ResourcePattern.PredicateLocation(_) -> PredicateLocation(_, args) => + args.map(dispatch) + case ResourcePattern.InstancePredicateLocation(_) -> InstancePredicateLocation(_, obj, args) => + dispatch(obj) +: args.map(dispatch) + } + + def make(e: Expr[Pre], pat: ResourcePattern): Seq[Expr[Post]] = (pat, e) match { + case ResourcePattern.Bool -> e => + Seq(dispatch(e)) + case ResourcePattern.Perm(locPat) -> Perm(loc, perm) => + makeLoc(loc, locPat) :+ dispatch(perm) + case ResourcePattern.Value(locPat) -> Value(loc) => + makeLoc(loc, locPat) + case ResourcePattern.Predicate(_) -> PredicateApply(_, args, perm) => + args.map(dispatch) :+ dispatch(perm) + case ResourcePattern.InstancePredicate(p) -> InstancePredicateApply(obj, _, args, perm) => + Seq(dispatch(obj)) ++ args.map(dispatch) ++ Seq(dispatch(perm)) + case ResourcePattern.Star(leftPat, rightPat) -> Star(left, right) => + make(left, leftPat) ++ make(right, rightPat) + case ResourcePattern.Implies(pat) -> Implies(cond, res) => + dispatch(cond) +: make(res, pat) + case ResourcePattern.Select(whenTruePat, whenFalsePat) -> Select(cond, whenTrue, whenFalse) => + Seq(dispatch(cond)) ++ make(whenTrue, whenTruePat) ++ make(whenFalse, whenFalsePat) + case pat -> e => + throw WrongResourcePattern(e) + } + + def toResourceLoc(getters: Seq[Expr[Post]], pat: ResourcePattern.ResourcePatternLoc)(implicit o: Origin): Location[Post] = pat match { + case ResourcePattern.HeapVariableLocation(ref) => HeapVariableLocation(succ(ref)) + case ResourcePattern.FieldLocation(ref) => FieldLocation(getters.head, succ(ref)) + case ResourcePattern.ModelLocation(ref) => ModelLocation(getters.head, succ(ref)) + case ResourcePattern.SilverFieldLocation(ref) => SilverFieldLocation(getters.head, succ(ref)) + case ResourcePattern.ArrayLocation(t) => ArrayLocation(getters(0), getters(1))(PanicBlame("Design flaw: the structure should include wf somehow")) + case ResourcePattern.PointerLocation(t) => PointerLocation(getters.head)(PanicBlame("Design flaw: the structure should include wf somehow")) + case ResourcePattern.PredicateLocation(ref) => PredicateLocation(succ(ref), getters) + case ResourcePattern.InstancePredicateLocation(ref) => InstancePredicateLocation(succ(ref), getters.head, getters.tail) + } + + def toResource(getters: Seq[Expr[Post]], pat: ResourcePattern)(implicit o: Origin): Expr[Post] = pat match { + case ResourcePattern.Bool => getters.head + case ResourcePattern.Perm(loc) => Perm(toResourceLoc(getters.init, loc), getters.last) + case ResourcePattern.Value(loc) => Value(toResourceLoc(getters, loc)) + case ResourcePattern.Predicate(p) => PredicateApply(succ(p), getters.init, getters.last) + case ResourcePattern.InstancePredicate(p) => InstancePredicateApply(getters.head, succ(p), getters.tail.init, getters.last) + case ResourcePattern.Star(left, right) => + val split = freeTypes(left).size // indicative of a Really Good Abstraction + Star(toResource(getters.take(split), left), toResource(getters.drop(split), right)) + case ResourcePattern.Implies(res) => + Implies(getters.head, toResource(getters.tail, res)) + case ResourcePattern.Select(whenTrue, whenFalse) => + val whenTrueCount = freeTypes(whenTrue).size + Select( + getters.head, + toResource(getters.tail.take(whenTrueCount), whenTrue), + toResource(getters.tail.drop(whenTrueCount), whenFalse), + ) + } + + m(pattern) = PatternBuilder( + index = index, + toValue = e => ADTFunctionInvocation[Post](Some(adt.ref -> Nil), buildFunc.ref, make(e, pattern)), + fromValue = e => toResource(getters.map(getter => ADTFunctionInvocation(Some(adt.ref -> Nil), getter.ref, Seq(e))), pattern) + ) + buildFunc +: kindAxiom +: (getters ++ getterAxioms) } adt.fill(globalDeclarations.declare(new AxiomaticDataType[Post](kind +: decls, Nil)(o.replacePrefName("ResourceVal")))) + val arbitraryValue = new Predicate(Seq(new Variable(valType)(o.replacePrefName("val"))), None)(o.replacePrefName("arbitraryResourceValue")) + globalDeclarations.declare(arbitraryValue) + patternBuilders.having(m.toMap) { - program.declarations.foreach(dispatch) + valAdt.having(adt.get) { + arbitraryResourceValue.having(arbitraryValue) { + kindFunc.having(kind) { + program.declarations.foreach(dispatch) + } + } + } } }._1) } + + override def dispatch(e: Expr[Pre]): Expr[Post] = e match { + case ResourceValue(res) => + patternBuilders.top(ResourcePattern.scan(res)).toValue(res) + + case ResourceOfResourceValue(resourceValue) => + implicit val o: Origin = e.o + val binding = new Variable[Post](TAxiomatic(valAdt.top.ref, Nil))(e.o.replacePrefName("v")) + val v = Local[Post](binding.ref) + + val alts: Seq[(Expr[Post], Expr[Post])] = patternBuilders.top.values.map { builder => + val cond = ADTFunctionInvocation[Post](Some(valAdt.top.ref -> Nil), kindFunc.top.ref, Seq(v)) === const(builder.index) + val res = builder.fromValue(v) + cond -> res + }.toSeq + + val otherwise = PredicateApply[Post](arbitraryResourceValue.top.ref, Seq(v), WritePerm()) + + val select = alts.foldRight[Expr[Post]](otherwise) { + case (cond -> res, otherwise) => Select(cond, res, otherwise) + } + + Let(binding, dispatch(resourceValue), select) + + case other => rewriteDefault(other) + } + + override def dispatch(t: Type[Pre]): Type[Post] = t match { + case TResourceVal() => TAxiomatic(valAdt.top.ref, Nil) + case other => rewriteDefault(other) + } } From 6073bed225b36c0afaee428bfd04a8db9e2f66b1 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 24 Oct 2023 15:09:53 +0200 Subject: [PATCH 4/7] add a lock example --- examples/concepts/resourceValues/Lock.pvl | 34 +++++++++++++++++++ .../vct/rewrite/EncodeResourceValues.scala | 2 +- 2 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 examples/concepts/resourceValues/Lock.pvl diff --git a/examples/concepts/resourceValues/Lock.pvl b/examples/concepts/resourceValues/Lock.pvl new file mode 100644 index 0000000000..751eb217e4 --- /dev/null +++ b/examples/concepts/resourceValues/Lock.pvl @@ -0,0 +1,34 @@ +class Lock { + final resource inv; + + given resource inv; + requires inv; + ensures this.inv == inv; + constructor() { + this.inv = inv; + exhale inv; // commit the invariant + } + + ensures inv; + void getLock(); + + requires inv; + void releaseLock(); +} + +class Use { + int a; + int b; + + requires Perm(a, write); + requires Perm(b, write); + void test() { + a = 4; + b = 6; + Lock l = new Lock() given { inv = Perm(a, write) ** Perm(b, write) ** a + b == 10 }; + + l.getLock(); + b = 3; + l.releaseLock(); + } +} \ No newline at end of file diff --git a/src/rewrite/vct/rewrite/EncodeResourceValues.scala b/src/rewrite/vct/rewrite/EncodeResourceValues.scala index acb7130005..48a8d3cf0b 100644 --- a/src/rewrite/vct/rewrite/EncodeResourceValues.scala +++ b/src/rewrite/vct/rewrite/EncodeResourceValues.scala @@ -149,7 +149,7 @@ case class EncodeResourceValues[Pre <: Generation]() extends Rewriter[Pre] with } def freeTypes(pattern: ResourcePattern): Seq[Type[Post]] = pattern match { - case ResourcePattern.Bool => Nil + case ResourcePattern.Bool => Seq(TBool()) case ResourcePattern.Perm(loc) => freeTypesLoc(loc) :+ TRational() case ResourcePattern.Value(loc) => freeTypesLoc(loc) case ResourcePattern.Predicate(p) => p.args.map(_.t).map(dispatch) From da448ce675cd1a46ad7ff0e246130076013c66cd Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 25 Oct 2023 08:21:05 +0200 Subject: [PATCH 5/7] revalidate scalapb compiler --- build.sc | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/build.sc b/build.sc index bbb3fe595a..525ba694a9 100644 --- a/build.sc +++ b/build.sc @@ -132,6 +132,17 @@ object util { trait ScalaPBModule extends BaseScalaPBModule with ScalaModule { def scalaPBVersion = "0.11.11" + + override def scalaPBClasspath: T[mill.api.Loose.Agg[PathRef]] = T { + mill.scalalib.Lib.resolveDependencies( + Seq( + coursier.LocalRepositories.ivy2Local, + coursier.MavenRepository("https://repo1.maven.org/maven2") + ), + Seq(ivy"com.thesamet.scalapb::scalapbc:${scalaPBVersion()}") + .map(Lib.depToBoundDep(_, "2.13.1")) + ).map(_.map(_.withRevalidateOnce)) + } } trait SeparatePackedResourcesModule extends JavaModule { From bb99abcbe05ecd90a5d2dbbe7f6764f60d6c68ee Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 25 Oct 2023 09:26:09 +0200 Subject: [PATCH 6/7] allow anything expect TResource to coerce to TAnyValue without other coercions --- src/col/vct/col/typerules/CoercionUtils.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/col/vct/col/typerules/CoercionUtils.scala b/src/col/vct/col/typerules/CoercionUtils.scala index 8e6e3c1979..49ed0c92fe 100644 --- a/src/col/vct/col/typerules/CoercionUtils.scala +++ b/src/col/vct/col/typerules/CoercionUtils.scala @@ -20,6 +20,8 @@ case object CoercionUtils { case (TResourceVal(), TResource()) => CoerceResourceValResource() case (TBool(), TResource()) => CoerceBoolResource() + case (_, TAnyValue()) => CoerceSomethingAnyValue(source) + case (source @ TOption(innerSource), target @ TOption(innerTarget)) => CoerceMapOption(getCoercion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget) case (source @ TTuple(Seq(leftSource, rightSource)), target @ TTuple(Seq(leftTarget, rightTarget))) => From bffc5f9a6b298d435a1446f13d81961364a27686 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 25 Oct 2023 14:25:53 +0200 Subject: [PATCH 7/7] disable example for now --- .../vct/test/integration/examples/ResourceValuesSpec.scala | 7 +++++++ test/main/vct/test/integration/helper/ExampleFiles.scala | 1 + 2 files changed, 8 insertions(+) create mode 100644 test/main/vct/test/integration/examples/ResourceValuesSpec.scala diff --git a/test/main/vct/test/integration/examples/ResourceValuesSpec.scala b/test/main/vct/test/integration/examples/ResourceValuesSpec.scala new file mode 100644 index 0000000000..227c4d3958 --- /dev/null +++ b/test/main/vct/test/integration/examples/ResourceValuesSpec.scala @@ -0,0 +1,7 @@ +package vct.test.integration.examples + +import vct.test.integration.helper.VercorsSpec + +class ResourceValuesSpec extends VercorsSpec { + // vercors should error withCode "henk" example "concepts/resourceValues/Lock.pvl" +} diff --git a/test/main/vct/test/integration/helper/ExampleFiles.scala b/test/main/vct/test/integration/helper/ExampleFiles.scala index fcbde8f933..5866ba2fab 100644 --- a/test/main/vct/test/integration/helper/ExampleFiles.scala +++ b/test/main/vct/test/integration/helper/ExampleFiles.scala @@ -9,6 +9,7 @@ case object ExampleFiles { "examples/archive/", "examples/technical/veymont-check/", "examples/technical/veymont-seq-progs/", + "examples/concepts/resourceValues", ).map(_.replaceAll("/", File.separator)) val IGNORE_EXTS: Seq[String] = Seq(