Resource values

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 {

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

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]

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()
+}

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()
+}

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()
+}

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()
+}

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

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

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()
+}

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] =>

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

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

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] =>
+
+}

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

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

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

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)

src/col/vct/col/typerules/CoercionUtils.scala

@@ -15,7 +15,12 @@ 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 (_, TAnyValue()) => CoerceSomethingAnyValue(source)
 
       case (source @ TOption(innerSource), target @ TOption(innerTarget)) =>
         CoerceMapOption(getCoercion(innerSource, innerTarget).getOrElse(return None), innerSource, innerTarget)
@@ -60,7 +65,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 +240,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 +262,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 +273,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
   }

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

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

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,