From 7d8907e07bb298aa30a0e08c79e53304a324c2a0 Mon Sep 17 00:00:00 2001 From: Alexander Stekelenburg Date: Fri, 22 Nov 2024 13:07:08 +0100 Subject: [PATCH] Finish cherry-picking Asserting/Assuming changes from Bob's branch --- .../vct/col/ast/unsorted/AssertingImpl.scala | 11 -- src/col/vct/col/origin/Blame.scala | 3 + src/hre/hre/io/ChecksumReadableFile.scala | 2 +- src/hre/hre/io/RWFile.scala | 2 +- src/main/vct/main/stages/Transformation.scala | 4 +- src/main/vct/options/types/PathOrStd.scala | 2 +- .../vct/rewrite/EncodeAssertingAssuming.scala | 106 ------------------ src/rewrite/vct/rewrite/EncodeAssuming.scala | 56 +++++++++ 8 files changed, 64 insertions(+), 122 deletions(-) delete mode 100644 src/col/vct/col/ast/unsorted/AssertingImpl.scala delete mode 100644 src/rewrite/vct/rewrite/EncodeAssertingAssuming.scala create mode 100644 src/rewrite/vct/rewrite/EncodeAssuming.scala diff --git a/src/col/vct/col/ast/unsorted/AssertingImpl.scala b/src/col/vct/col/ast/unsorted/AssertingImpl.scala deleted file mode 100644 index d889b860f6..0000000000 --- a/src/col/vct/col/ast/unsorted/AssertingImpl.scala +++ /dev/null @@ -1,11 +0,0 @@ -package vct.col.ast.unsorted - -import vct.col.ast.{Asserting, Type} -import vct.col.print._ -import vct.col.ast.ops.AssertingOps - -trait AssertingImpl[G] extends AssertingOps[G] { - this: Asserting[G] => - // override def layout(implicit ctx: Ctx): Doc = ??? - override def t: Type[G] = inner.t -} diff --git a/src/col/vct/col/origin/Blame.scala b/src/col/vct/col/origin/Blame.scala index 2a203d5f87..4124b5d31d 100644 --- a/src/col/vct/col/origin/Blame.scala +++ b/src/col/vct/col/origin/Blame.scala @@ -1545,6 +1545,9 @@ object NonNullPointerNull object UnsafeDontCare { case class Satisfiability(reason: String) extends UnsafeDontCare[NontrivialUnsatisfiable] + case class Contract(reason: String) extends UnsafeDontCare[ContractedFailure] + case class Invocation(reason: String) + extends UnsafeDontCare[InvocationFailure] } trait UnsafeDontCare[T <: VerificationFailure] diff --git a/src/hre/hre/io/ChecksumReadableFile.scala b/src/hre/hre/io/ChecksumReadableFile.scala index fac5d4c7d8..8903dd51f5 100644 --- a/src/hre/hre/io/ChecksumReadableFile.scala +++ b/src/hre/hre/io/ChecksumReadableFile.scala @@ -18,7 +18,7 @@ case class ChecksumReadableFile( checksumKind: String, ) extends InMemoryCachedReadable { override def underlyingPath: Option[Path] = Some(file) - override def fileName: String = file.toString + override def fileName: String = file.getFileName.toString override def isRereadable: Boolean = true private var checksumCache: Option[String] = None diff --git a/src/hre/hre/io/RWFile.scala b/src/hre/hre/io/RWFile.scala index c7071e0277..659363e2bf 100644 --- a/src/hre/hre/io/RWFile.scala +++ b/src/hre/hre/io/RWFile.scala @@ -7,7 +7,7 @@ import java.nio.file.{Files, Path} case class RWFile(file: Path, doWatch: Boolean = true) extends InMemoryCachedReadable with Writeable { override def underlyingPath: Option[Path] = Some(file) - override def fileName: String = file.toString + override def fileName: String = file.getFileName.toString override def isRereadable: Boolean = true override protected def getWriter: Writer = { diff --git a/src/main/vct/main/stages/Transformation.scala b/src/main/vct/main/stages/Transformation.scala index add6dde531..604a5e0c3d 100644 --- a/src/main/vct/main/stages/Transformation.scala +++ b/src/main/vct/main/stages/Transformation.scala @@ -34,7 +34,7 @@ import vct.rewrite.{ EncodeByValueClassUsage, EncodeRange, EncodeResourceValues, - EncodeAssertingAssuming, + EncodeAssuming, ExplicitResourceValues, GenerateSingleOwnerPermissions, HeapVariableToRef, @@ -414,7 +414,7 @@ case class SilverTransformation( RefuteToInvertedAssert, ExplicitResourceValues, EncodeResourceValues, - EncodeAssertingAssuming, + EncodeAssuming, // Encode parallel blocks EncodeSendRecv, diff --git a/src/main/vct/options/types/PathOrStd.scala b/src/main/vct/options/types/PathOrStd.scala index c5aa7d12c3..06df5330af 100644 --- a/src/main/vct/options/types/PathOrStd.scala +++ b/src/main/vct/options/types/PathOrStd.scala @@ -15,7 +15,7 @@ sealed trait PathOrStd extends InMemoryCachedReadable with Writeable { override def fileName: String = this match { - case PathOrStd.Path(path) => path.toString + case PathOrStd.Path(path) => path.getFileName.toString case PathOrStd.StdInOrOut => "" } diff --git a/src/rewrite/vct/rewrite/EncodeAssertingAssuming.scala b/src/rewrite/vct/rewrite/EncodeAssertingAssuming.scala deleted file mode 100644 index ae14cd81e9..0000000000 --- a/src/rewrite/vct/rewrite/EncodeAssertingAssuming.scala +++ /dev/null @@ -1,106 +0,0 @@ -package vct.rewrite - -import com.typesafe.scalalogging.LazyLogging -import vct.col.ast.{ - Asserting, - Assuming, - Expr, - Function, - Let, - TBool, - Type, - UnitAccountedPredicate, - Variable, -} -import vct.col.origin.{ - AssertFailed, - Blame, - DiagnosticOrigin, - InvocationFailure, - Origin, - PreconditionFailed, - UnsafeDontCare, -} -import vct.col.ref.Ref -import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} - -import scala.collection.mutable -import vct.col.util.AstBuildHelpers._ -import vct.rewrite.EncodeAssertingAssuming.InvocationFailureToAssertFailed - -case object EncodeAssertingAssuming extends RewriterBuilder { - override def key: String = "encodeAssertAssumeExpr" - override def desc: String = - "Encodes assert/assume exprs using plain pure functions" - - case class InvocationFailureToAssertFailed(assertExpr: Asserting[_]) - extends Blame[InvocationFailure] { - override def blame(error: InvocationFailure): Unit = - error match { - case PreconditionFailed(path, failure, node) => - assertExpr.blame.blame(AssertFailed(failure, assertExpr.assn)) - case _ => ??? - } - } -} - -case class EncodeAssertingAssuming[Pre <: Generation]() - extends Rewriter[Pre] with LazyLogging { - - lazy val assertingFunction: Function[Post] = { - implicit val o = DiagnosticOrigin - val assnVar = new Variable[Post](TBool())(o.where(name = "assn")) - globalDeclarations.declare( - function( - blame = UnsafeDontCare.Contract("assumption primitive"), - contractBlame = UnsafeDontCare.Satisfiability("assumption primitive"), - returnType = TBool(), - args = Seq(assnVar), - requires = UnitAccountedPredicate(assnVar.get), - )(o.where(name = "assert_")) - ) - } - - lazy val assumingFunction: Function[Post] = { - implicit val o = DiagnosticOrigin - val assnVar = new Variable[Post](TBool())(o.where(name = "assn")) - globalDeclarations.declare( - function( - blame = UnsafeDontCare.Contract("assumption primitive"), - contractBlame = UnsafeDontCare.Satisfiability("assumption primitive"), - returnType = TBool(), - args = Seq(assnVar), - ensures = UnitAccountedPredicate(assnVar.get), - )(o.where(name = "assume_")) - ) - } - - override def dispatch(expr: Expr[Pre]): Expr[Post] = - expr match { - case expr @ Asserting(assn, inner) => - implicit val o = expr.o - Let( - new Variable(TBool())(o.where(name = "_")), - functionInvocation( - ref = assertingFunction.ref, - args = Seq(dispatch(assn)), - blame = InvocationFailureToAssertFailed(expr), - ), - dispatch(inner), - ) - - case Assuming(assn, inner) => - implicit val o = expr.o - Let( - new Variable(TBool())(o.where(name = "_")), - functionInvocation( - ref = assumingFunction.ref, - args = Seq(dispatch(assn)), - blame = UnsafeDontCare.Invocation("assumption"), - ), - dispatch(inner), - ) - - case _ => expr.rewriteDefault() - } -} diff --git a/src/rewrite/vct/rewrite/EncodeAssuming.scala b/src/rewrite/vct/rewrite/EncodeAssuming.scala new file mode 100644 index 0000000000..3959d9eda1 --- /dev/null +++ b/src/rewrite/vct/rewrite/EncodeAssuming.scala @@ -0,0 +1,56 @@ +package vct.rewrite + +import com.typesafe.scalalogging.LazyLogging +import vct.col.ast.{ + Assuming, + Expr, + Function, + Let, + TBool, + UnitAccountedPredicate, + Variable, +} +import vct.col.origin.{DiagnosticOrigin, UnsafeDontCare} +import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} + +import vct.col.util.AstBuildHelpers._ + +case object EncodeAssuming extends RewriterBuilder { + override def key: String = "encodeAssumeExpr" + override def desc: String = "Encodes assume exprs using plain pure functions" +} + +case class EncodeAssuming[Pre <: Generation]() + extends Rewriter[Pre] with LazyLogging { + + lazy val assumingFunction: Function[Post] = { + implicit val o = DiagnosticOrigin + val assnVar = new Variable[Post](TBool())(o.where(name = "assn")) + globalDeclarations.declare( + function( + blame = UnsafeDontCare.Contract("assumption primitive"), + contractBlame = UnsafeDontCare.Satisfiability("assumption primitive"), + returnType = TBool(), + args = Seq(assnVar), + ensures = UnitAccountedPredicate(assnVar.get), + )(o.where(name = "assume_")) + ) + } + + override def dispatch(expr: Expr[Pre]): Expr[Post] = + expr match { + case Assuming(assn, inner) => + implicit val o = expr.o + Let( + new Variable(TBool())(o.where(name = "_")), + functionInvocation( + ref = assumingFunction.ref, + args = Seq(dispatch(assn)), + blame = UnsafeDontCare.Invocation("assumption"), + ), + dispatch(inner), + ) + + case _ => expr.rewriteDefault() + } +}