Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add global heap variables #1047

Merged
merged 2 commits into from
Jun 23, 2023
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/col/vct/col/ast/Node.scala
Original file line number Diff line number Diff line change
@@ -221,6 +221,7 @@ final case class ModelDo[G](model: Expr[G], perm: Expr[G], after: Expr[G], actio
sealed trait Declaration[G] extends Node[G] with DeclarationImpl[G]

sealed trait GlobalDeclaration[G] extends Declaration[G] with GlobalDeclarationImpl[G]
final class HeapVariable[G](val t: Type[G])(implicit val o: Origin) extends GlobalDeclaration[G] with HeapVariableImpl[G]
final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
final class AxiomaticDataType[G](val decls: Seq[ADTDeclaration[G]], val typeArgs: Seq[Variable[G]])(implicit val o: Origin) extends GlobalDeclaration[G] with AxiomaticDataTypeImpl[G]
final class Class[G](val declarations: Seq[ClassDeclaration[G]], val supports: Seq[Ref[G, Class[G]]], val intrinsicLockInvariant: Expr[G])(implicit val o: Origin) extends GlobalDeclaration[G] with ClassImpl[G]
@@ -464,6 +465,7 @@ final case class ScopedExpr[G](declarations: Seq[Variable[G]], body: Expr[G])(im
final case class Local[G](ref: Ref[G, Variable[G]])(implicit val o: Origin) extends Expr[G] with LocalImpl[G]
final case class EnumUse[G](enum: Ref[G, Enum[G]], const: Ref[G, EnumConstant[G]])(implicit val o: Origin) extends Expr[G] with EnumUseImpl[G]
sealed trait HeapDeref[G] extends Expr[G] with HeapDerefImpl[G]
final case class DerefHeapVariable[G](ref: Ref[G, HeapVariable[G]])(val blame: Blame[InsufficientPermission])(implicit val o: Origin) extends Expr[G] with HeapDeref[G] with DerefHeapVariableImpl[G]
final case class Deref[G](obj: Expr[G], ref: Ref[G, InstanceField[G]])(val blame: Blame[InsufficientPermission])(implicit val o: Origin) extends Expr[G] with HeapDeref[G] with DerefImpl[G]
final case class ModelDeref[G](obj: Expr[G], ref: Ref[G, ModelField[G]])(val blame: Blame[ModelInsufficientPermission])(implicit val o: Origin) extends Expr[G] with ModelDerefImpl[G]
final case class DerefPointer[G](pointer: Expr[G])(val blame: Blame[PointerDerefError])(implicit val o: Origin) extends Expr[G] with DerefPointerImpl[G]
@@ -552,6 +554,7 @@ final case class PolarityDependent[G](onInhale: Expr[G], onExhale: Expr[G])(impl
final case class Unfolding[G](res: Expr[G], body: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends Expr[G] with UnfoldingImpl[G]

sealed trait Location[G] extends NodeFamily[G] with LocationImpl[G]
final case class HeapVariableLocation[G](ref: Ref[G, HeapVariable[G]])(implicit val o: Origin) extends Location[G] with HeapVariableLocationImpl[G]
final case class FieldLocation[G](obj: Expr[G], field: Ref[G, InstanceField[G]])(implicit val o: Origin) extends Location[G] with FieldLocationImpl[G]
final case class ModelLocation[G](obj: Expr[G], field: Ref[G, ModelField[G]])(implicit val o: Origin) extends Location[G] with ModelLocationImpl[G]
final case class SilverFieldLocation[G](obj: Expr[G], field: Ref[G, SilverField[G]])(implicit val o: Origin) extends Location[G] with SilverFieldLocationImpl[G]
14 changes: 14 additions & 0 deletions src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
package vct.col.ast.declaration.global

import vct.col.ast.HeapVariable
import vct.col.print._

trait HeapVariableImpl[G] { this: HeapVariable[G] =>
override def layout(implicit ctx: Ctx): Doc = ctx.syntax match {
case Ctx.C | Ctx.Cuda | Ctx.OpenCL =>
val (spec, decl) = t.layoutSplitDeclarator
spec <+> decl <> ctx.name(this) <> ";"
case _ =>
t.show <+> ctx.name(this) <> ";"
}
}
11 changes: 11 additions & 0 deletions src/col/vct/col/ast/expr/heap/read/DerefHeapVariableImpl.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
package vct.col.ast.expr.heap.read

import vct.col.ast.{DerefHeapVariable, Type}
import vct.col.print._

trait DerefHeapVariableImpl[G] { this: DerefHeapVariable[G] =>
override def t: Type[G] = ref.decl.t

override def precedence: Int = Precedence.ATOMIC
override def layout(implicit ctx: Ctx): Doc = Text(ctx.name(ref))
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
package vct.col.ast.family.location

import vct.col.ast.HeapVariableLocation

trait HeapVariableLocationImpl[G] { this: HeapVariableLocation[G] =>

}
14 changes: 10 additions & 4 deletions src/col/vct/col/resolve/Resolve.scala
Original file line number Diff line number Diff line change
@@ -294,10 +294,16 @@ case object ResolveReferences extends LazyLogging {
if(func.decl.contract.nonEmpty && func.decl.inits.size > 1) {
throw MultipleForwardDeclarationContractError(func)
}
ctx
.declare(C.paramsFromDeclarator(func.decl.inits.head.decl) ++ func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
.copy(currentResult=C.getDeclaratorInfo(func.decl.inits.head.decl)
.params.map(_ => RefCGlobalDeclaration(func, initIdx = 0)))

func.decl.inits.zipWithIndex.foldLeft(
ctx.declare(func.decl.contract.givenArgs ++ func.decl.contract.yieldsArgs)
) {
case (ctx, (init, idx)) =>
val info = C.getDeclaratorInfo(init.decl)
ctx
.declare(info.params.getOrElse(Nil))
.copy(currentResult=info.params.map(_ => RefCGlobalDeclaration(func, idx)))
}
case par: ParStatement[G] => ctx
.declare(scanBlocks(par.impl).map(_.decl))
case Scope(locals, body) => ctx
6 changes: 6 additions & 0 deletions src/col/vct/col/typerules/CoercingRewriter.scala
Original file line number Diff line number Diff line change
@@ -892,6 +892,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
//DerefVeyMontThread( TVeyMontThread[Pre](ref))
case deref @ Deref(obj, ref) =>
Deref(cls(obj), ref)(deref.blame)
case deref @ DerefHeapVariable(ref) =>
DerefHeapVariable(ref)(deref.blame)
case deref @ DerefPointer(p) =>
DerefPointer(pointer(p)._1)(deref.blame)
case deref @ DerefVeyMontThread(ref) => deref
@@ -1599,6 +1601,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
decl match {
case unit: CTranslationUnit[Pre] =>
new CTranslationUnit(unit.declarations)
case variable: HeapVariable[Pre] =>
new HeapVariable(variable.t)
case rule: SimplificationRule[Pre] =>
new SimplificationRule[Pre](bool(rule.axiom))
case dataType: AxiomaticDataType[Pre] =>
@@ -1819,6 +1823,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
def coerce(node: Location[Pre]): Location[Pre] = {
implicit val o: Origin = node.o
node match {
case HeapVariableLocation(ref) =>
HeapVariableLocation(ref)
case FieldLocation(obj, field) =>
FieldLocation(cls(obj), field)
case ModelLocation(obj, field) =>
9 changes: 0 additions & 9 deletions src/main/vct/main/stages/Resolution.scala
Original file line number Diff line number Diff line change
@@ -87,15 +87,6 @@ case class Resolution[G <: Generation]
override def progressWeight: Int = 1

override def run(in: ParseResult[G]): Verification[_ <: Generation] = {
in.decls.foreach(_.transSubnodes.foreach {
case decl: CGlobalDeclaration[_] => decl.decl.inits.foreach(init => {
if(C.getDeclaratorInfo(init.decl).params.isEmpty) {
throw TemporarilyUnsupported("GlobalCVariable", Seq(decl))
}
})
case _ =>
})

implicit val o: Origin = FileSpanningOrigin

val parsedProgram = Program(in.decls)(blameProvider())
2 changes: 2 additions & 0 deletions src/main/vct/main/stages/Transformation.scala
Original file line number Diff line number Diff line change
@@ -22,6 +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

object Transformation {
case class TransformationCheckError(pass: RewriterBuilder, errors: Seq[CheckError]) extends SystemError {
@@ -242,6 +243,7 @@ case class SilverTransformation
ResolveScale,
// No more classes
ClassToRef,
HeapVariableToRef,

CheckContractSatisfiability.withArg(checkSat),

2 changes: 1 addition & 1 deletion src/rewrite/vct/rewrite/DesugarPermissionOperators.scala
Original file line number Diff line number Diff line change
@@ -32,7 +32,6 @@ case object DesugarPermissionOperators extends RewriterBuilder {

case class PredicateValueError(loc: Location[_]) extends UserError {
override def code: String = "predicateValue"

override def text: String = loc.o.messageInContext("The predicate has a location but does not point to a value.")
}

@@ -42,6 +41,7 @@ case class DesugarPermissionOperators[Pre <: Generation]() extends Rewriter[Pre]

def extractValueFromLocation(loc: Location[Pre]): Expr[Pre] = {
loc match {
case HeapVariableLocation(field) => DerefHeapVariable(field)(PointsToDeref)(loc.o)
case FieldLocation(obj, field) => Deref(obj, field)(PointsToDeref)(loc.o)
case ModelLocation(obj, field) => ModelDeref(obj, field)(PointsToDeref)(loc.o)
case SilverFieldLocation(obj, field) => SilverDeref(obj, field)(PointsToDeref)(loc.o)
2 changes: 2 additions & 0 deletions src/rewrite/vct/rewrite/DisambiguateLocation.scala
Original file line number Diff line number Diff line change
@@ -26,6 +26,8 @@ case object DisambiguateLocation extends RewriterBuilder {

case class DisambiguateLocation[Pre <: Generation]() extends Rewriter[Pre] {
def exprToLoc(expr: Expr[Pre], blame: Blame[PointerLocationError])(implicit o: Origin): Location[Post] = expr match {
case DerefHeapVariable(ref) =>
HeapVariableLocation(succ(ref.decl))
case Deref(obj, ref) =>
FieldLocation(dispatch(obj), succ(ref.decl))
case ModelDeref(obj, ref) =>
52 changes: 52 additions & 0 deletions src/rewrite/vct/rewrite/HeapVariableToRef.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
package vct.rewrite

import vct.col.ast._
import vct.col.origin.{AbstractApplicable, Origin, PanicBlame, TrueSatisfiable}
import vct.col.ref.Ref
import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder, Rewritten}
import vct.col.util.AstBuildHelpers.{function, functionInvocation}
import vct.col.util.SuccessionMap

case object HeapVariableToRef extends RewriterBuilder {
override def key: String = "heapVarToRef"
override def desc: String = "Translate global heap variables to the field of a constant Ref"

case object GlobalsOrigin extends Origin {
override def preferredName: String = "globals"
override def context: String = "At: [globals]"
override def inlineContext: String = "[globals]"
override def shortPosition: String = "generated"
}
}

case class HeapVariableToRef[Pre <: Generation]() extends Rewriter[Pre] {
import HeapVariableToRef._

lazy val globalsFunction: Function[Post] = {
implicit val o: Origin = GlobalsOrigin
globalDeclarations.declare(function[Post](AbstractApplicable, TrueSatisfiable, returnType = TRef()))
}

def globals(implicit o: Origin): Expr[Post] =
functionInvocation[Post](PanicBlame("Precondition is `true`"), globalsFunction.ref)

val heapVariableField: SuccessionMap[HeapVariable[Pre], SilverField[Post]] = SuccessionMap()

override def dispatch(decl: Declaration[Pre]): Unit = decl match {
case v: HeapVariable[Pre] =>
heapVariableField(v) = globalDeclarations.declare(new SilverField(dispatch(v.t))(v.o))
case other => rewriteDefault(other)
}

override def dispatch(e: Expr[Pre]): Expr[Post] = e match {
case hv @ DerefHeapVariable(Ref(v)) =>
SilverDeref[Post](globals(e.o), heapVariableField.ref(v))(hv.blame)(e.o)
case other => rewriteDefault(other)
}

override def dispatch(location: Location[Pre]): Location[Post] = location match {
case HeapVariableLocation(Ref(v)) =>
SilverFieldLocation[Post](globals(location.o), heapVariableField.ref(v))(location.o)
case other => rewriteDefault(other)
}
}
1 change: 1 addition & 0 deletions src/rewrite/vct/rewrite/ResolveExpressionSideEffects.scala
Original file line number Diff line number Diff line change
@@ -371,6 +371,7 @@ case class ResolveExpressionSideEffects[Pre <: Generation]() extends Rewriter[Pr
def assignTarget(target: Expr[Pre]): Expr[Post] = {
val result = target match {
case Local(Ref(v)) => Local[Post](succ(v))(target.o)
case deref @ DerefHeapVariable(Ref(v)) => DerefHeapVariable[Post](succ(v))(deref.blame)(target.o)
case Deref(obj, Ref(f)) => Deref[Post](notInlined(obj), succ(f))(DerefAssignTarget)(target.o)
case ArraySubscript(arr, index) => ArraySubscript[Post](notInlined(arr), notInlined(index))(SubscriptAssignTarget)(target.o)
case PointerSubscript(arr, index) => PointerSubscript[Post](notInlined(arr), notInlined(index))(SubscriptAssignTarget)(target.o)
10 changes: 8 additions & 2 deletions src/rewrite/vct/rewrite/lang/LangCToCol.scala
Original file line number Diff line number Diff line change
@@ -133,6 +133,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
val cFunctionSuccessor: SuccessionMap[CFunctionDefinition[Pre], Procedure[Post]] = SuccessionMap()
val cFunctionDeclSuccessor: SuccessionMap[(CGlobalDeclaration[Pre], Int), Procedure[Post]] = SuccessionMap()
val cNameSuccessor: SuccessionMap[CNameTarget[Pre], Variable[Post]] = SuccessionMap()
val cGlobalNameSuccessor: SuccessionMap[CNameTarget[Pre], HeapVariable[Post]] = SuccessionMap()
val cCurrentDefinitionParamSubstitutions: ScopedStack[Map[CParam[Pre], CParam[Pre]]] = ScopedStack()

val cudaCurrentThreadIdx: ScopedStack[CudaVec] = ScopedStack()
@@ -600,7 +601,8 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
)
)
case None =>
throw CGlobalStateNotSupported(init)
cGlobalNameSuccessor(RefCGlobalDeclaration(decl, idx)) =
rw.globalDeclarations.declare(new HeapVariable(t)(init.o))
}
}
}
@@ -745,7 +747,11 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) extends Laz
else
Local(cNameSuccessor.ref(ref))
case RefCFunctionDefinition(_) => throw NotAValue(local)
case RefCGlobalDeclaration(_, _) => throw NotAValue(local)
case ref @ RefCGlobalDeclaration(decl, initIdx) =>
C.getDeclaratorInfo(decl.decl.inits(initIdx).decl).params match {
case None => DerefHeapVariable[Post](cGlobalNameSuccessor.ref(ref))(local.blame)
case Some(_) => throw NotAValue(local)
}
case ref: RefCLocalDeclaration[Pre] => Local(cNameSuccessor.ref(ref))
case _: RefCudaVec[Pre] => throw NotAValue(local)
}