diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectElaboration.scala b/core/src/main/scala/stainless/extraction/imperative/EffectElaboration.scala index 9d53393313..96ba99d02c 100644 --- a/core/src/main/scala/stainless/extraction/imperative/EffectElaboration.scala +++ b/core/src/main/scala/stainless/extraction/imperative/EffectElaboration.scala @@ -143,7 +143,8 @@ trait RefTransform case AnyHeapRefType() => true // We lookup the parents through the cache so that the hierarchy is traversed at most once case ct: ClassType => ct.tcd.parents.exists(a => erasesToHeapRef(a.toType)) - case _ => false + // Slow path + case _ => symbols.isSubtypeOf(tpe, AnyHeapRefType()) } private def freshStateParam(): ValDef = "heap0" :: HeapMapType @@ -157,7 +158,10 @@ trait RefTransform def unchecked(expr: Expr): Expr = Annotated(expr, Seq(DropVCs)).copiedFrom(expr) def classTypeInHeap(ct: ClassType): ClassType = - ClassType(ct.id, ct.tps.map(typeOnlyRefTransformer.transform)).copiedFrom(ct) + ClassType( + ct.id, + dropTypeArgs(ct.tcd.cd.tparams, ct.tps).map(typeOnlyRefTransformer.transform) + ).copiedFrom(ct) def makeClassUnapply(cd: ClassDef): Option[FunDef] = { if (!erasesToHeapRef(cd.typed.toType)) @@ -191,6 +195,15 @@ trait RefTransform } .copiedFrom(cd)) } + // We drop type parameters that are upper bounded by AnyHeapRef, + // since they erase to HeapRefs anyways. + def shouldDropTypeParam(tparam: TypeParameterDef): Boolean = + symbols.isSubtypeOf(tparam.tp, AnyHeapRefType()) + + // Remove all those type arguments that correspond to type params which should be dropped. + def dropTypeArgs(tparams: Seq[TypeParameterDef], args: Seq[Type]): Seq[Type] = + tparams.zip(args).collect { case (tparam, arg) if !shouldDropTypeParam(tparam) => arg } + // Reduce all mutation to assignments of a local heap variable // TODO: Handle mutable types other than classes abstract class RefTransformer extends oo.DefinitionTransformer { @@ -200,12 +213,13 @@ trait RefTransform override def transform(tpe: Type, env: Env): Type = tpe match { case HeapType() => HeapMapType - case ct: ClassType if erasesToHeapRef(ct) => + case _ if erasesToHeapRef(tpe) => + // Slow path ^ HeapRefType - // case FunctionType(_, _) => - // val FunctionType(from, to) = super.transform(tpe, env) - // FunctionType(HeapMapType +: from, T(to, HeapMapType)) - // TODO: PiType + case ct @ ClassType(id, tps) => + // NOTE(gsps): What we do here should never be necessary for ADTTypes, I think. + val ct1 = ct.copy(tps = dropTypeArgs(ct.tcd.cd.tparams, tps)).copiedFrom(tpe) + super.transform(ct1, env) case _ => super.transform(tpe, env) } @@ -214,14 +228,16 @@ trait RefTransform val env = initEnv // FIXME: Transform type arguments in parents? - val newParents = cd.parents.filter { - case AnyHeapRefType() => false - case _ => true - } + val newParents = cd.parents + .filter { + case AnyHeapRefType() => false + case _ => true + } + .map(ct => transform(ct, env).asInstanceOf[t.ClassType]) new ClassDef( transform(cd.id, env), - cd.tparams.map(transform(_, env)), + cd.tparams.filterNot(shouldDropTypeParam).map(transform(_, env)), newParents, cd.fields.map(transform(_, env)), cd.flags.map(transform(_, env)) @@ -391,7 +407,7 @@ trait RefTransform LetVar(heapVd, heap1, value1).setPos(e) case fi @ FunctionInvocation(id, targs, vargs) => - val targs1 = targs.map(transform(_, env)) + val targs1 = dropTypeArgs(fi.tfd.fd.tparams, targs).map(transform(_, env)) val vargs1 = vargs.map(transform(_, env)) effectLevel(id) match { @@ -404,7 +420,7 @@ trait RefTransform lazy val modifiesDom = env.expectModifiesV(e.getPos, "call heap-modifying function") val call = - if (readsDom.isEmpty && modifiesDom.isEmpty) { + if (readsDom.isEmpty && (!writes || modifiesDom.isEmpty)) { // NOTE: Workaround for the case where both readsDom and modifiesDom is None, // i.e. all reads and modifications are permitted. FunctionInvocation(id, targs1, Seq(heapVd.toVariable) ++ vargs1).copiedFrom(e) @@ -455,7 +471,7 @@ trait RefTransform binder.map(transform(_, env)), Seq(heapVd.toVariable, readsDomArg), unapplyId(ct.id), - ct.tps.map(transform(_, env)), + dropTypeArgs(ct.tcd.cd.tparams, ct.tps).map(transform(_, env)), Seq(newClassPat) ).copiedFrom(pat) case _ => @@ -496,22 +512,18 @@ trait RefTransform heapVdOpt0: Option[ValDef], heapVdOpt1: Option[ValDef]): Expr = { val replaceRes = resVd != valueVd + // Transform postcondition body in post-state (ignoring `old(...)` parts) + val post1 = funRefTransformer.transform(post, specEnv(heapVdOpt1)) // Rewrite the value result variable (used if `resVd` now also contains the heap state) - val post1 = postMap { + // and transform `old(...)` parts of postcondition body in pre-state. + postMap { case v: Variable if replaceRes && v.id == resVd.id => Some(valueVd.toVariable.copiedFrom(v)) - case _ => - None - }(post) - // Transform postcondition body in post-state (ignoring `old(...)` parts) - val post2 = funRefTransformer.transform(post1, specEnv(heapVdOpt1)) - // Transform `old(...)` parts of postcondition body in pre-state - postMap { case Old(e) => Some(funRefTransformer.transform(e, specEnv(heapVdOpt0))) case _ => None - }(post2) + }(post1) } // Unpack specs from the existing function @@ -580,7 +592,9 @@ trait RefTransform case None => body } - val newTParams = fd.tparams.map(typeOnlyRefTransformer.transform) + val newTParams = fd.tparams + .filterNot(shouldDropTypeParam) + .map(typeOnlyRefTransformer.transform) val newFlags = fd.flags.map(typeOnlyRefTransformer.transform) /* diff --git a/frontends/benchmarks/full-imperative/valid/AllocatorMonoAbstract.scala b/frontends/benchmarks/full-imperative/valid/AllocatorMonoAbstract.scala new file mode 100644 index 0000000000..ba19528a05 --- /dev/null +++ b/frontends/benchmarks/full-imperative/valid/AllocatorMonoAbstract.scala @@ -0,0 +1,55 @@ +import stainless.lang._ +import stainless.collection._ +import stainless.lang.Option._ +import stainless.annotation._ +import stainless.lang.StaticChecks._ + +// A slightly better model of an allocator that elides its implementation. +object AllocatorMonoAbstractExample { + case class Box(var v: BigInt) extends AnyHeapRef + + case class BoxAllocator( + @ghost var bound: BigInt, + var alloc: List[Box], + var free: List[Box] + ) extends AnyHeapRef { + @ghost + def evolved(from: Heap): Boolean = { + reads(Set(this)) + ( free.content subsetOf from.eval(free.content )) && + (from.eval(alloc.content) subsetOf alloc.content ) + } + + // Set that is practically needed to allocate and initialize new objects. + @ghost + def access: Set[AnyHeapRef] = { + reads(Set(this)) + free.content.asRefs + this + } + + // FIXME: Figure out why this fails with @extern (add missing case in ChooseInjector & more) + @extern + def apply(): Box = { + reads(Set(this)) + modifies(Set(this)) + ??? : Box + } ensuring { o => evolved(old(Heap.get)) && + old(!alloc.contains(o) && free.contains(o)) && alloc.contains(o) && !free.contains(o) + } + } + + def freshList(ator: BoxAllocator, xs: List[Box], v: BigInt): List[Box] = { + reads(ator.access) + modifies(ator.access) + require(xs.content subsetOf ator.alloc.content) + xs match { + case Nil() => Nil[Box]() + case Cons(x, xs_) => + val b = ator() + b.v = v + Cons(b, freshList(ator, xs_, v)) + } + } ensuring { res => + res.size == xs.size && (res.content & old(ator.alloc.content)).isEmpty + } +} diff --git a/frontends/benchmarks/full-imperative/valid/AllocatorPolyAbstract.scala b/frontends/benchmarks/full-imperative/valid/AllocatorPolyAbstract.scala new file mode 100644 index 0000000000..bdff0a109c --- /dev/null +++ b/frontends/benchmarks/full-imperative/valid/AllocatorPolyAbstract.scala @@ -0,0 +1,55 @@ +import stainless.lang._ +import stainless.collection._ +import stainless.lang.Option._ +import stainless.annotation._ +import stainless.lang.StaticChecks._ + +// A slightly better model of an allocator that elides its implementation and is polymorphic. +object AllocatorPolyAbstractExample { + case class Box(var v: BigInt) extends AnyHeapRef + + case class Allocator[T <: AnyHeapRef]( + @ghost var bound: BigInt, + var alloc: List[T], + var free: List[T] + ) extends AnyHeapRef { + @ghost + def evolved(from: Heap): Boolean = { + reads(Set(this)) + ( free.content subsetOf from.eval(free.content )) && + (from.eval(alloc.content) subsetOf alloc.content ) + } + + // Set that is practically needed to allocate and initialize new objects. + @ghost + def access: Set[AnyHeapRef] = { + reads(Set(this)) + free.content.asRefs + this + } + + // FIXME(gsps): Figure out why this fails with @extern (add missing case in ChooseInjector & more) + @extern + def apply(): T = { + reads(Set(this)) + modifies(Set(this)) + ??? : T + } ensuring { o => evolved(old(Heap.get)) && + old(!alloc.contains(o) && free.contains(o)) && alloc.contains(o) && !free.contains(o) + } + } + + def freshList(ator: Allocator[Box], xs: List[Box], v: BigInt): List[Box] = { + reads(ator.access) + modifies(ator.access) + require(xs.content subsetOf ator.alloc.content) + xs match { + case Nil() => Nil[Box]() + case Cons(x, xs_) => + val b = ator() + b.v = v + Cons(b, freshList(ator, xs_, v)) + } + } ensuring { res => + res.size == xs.size && (res.content & old(ator.alloc.content)).isEmpty + } +}