diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala index 14cdf66bb..6bed59099 100644 --- a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala @@ -310,6 +310,9 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter showVar(resTarget) <> "," <+> showVar(successTarget) <+> "=" <+> showExpr(expr) <> "." <> parens(showType(typ)) case Initialization(left) => "init" <+> showVar(left) + + case Allocation(left) => "allocate" <+> showVar(left) + case SingleAss(left, right) => showAssignee(left) <+> "=" <+> showExpr(right) case FunctionCall(targets, func, args) => @@ -741,6 +744,9 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter { showVar(resTarget) <> "," <+> showVar(successTarget) <+> "=" <+> showExpr(expr) case Initialization(left) => "init" <+> showVar(left) + + case Allocation(left) => "allocate" <+> showVar(left) + case SingleAss(left, right) => showAssignee(left) <+> "=" <+> showExpr(right) case _: FunctionCall | _: MethodCall | _: ClosureCall => super.showStmt(s) diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index 00818fc75..926e506a1 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/src/main/scala/viper/gobra/ast/internal/Program.scala @@ -365,6 +365,8 @@ case class While(cond: Expr, invs: Vector[Assertion], terminationMeasure: Option case class Initialization(left: AssignableVar)(val info: Source.Parser.Info) extends Stmt +case class Allocation(left: AssignableVar)(val info: Source.Parser.Info) extends Stmt + sealed trait Assignment extends Stmt case class SingleAss(left: Assignee, right: Expr)(val info: Source.Parser.Info) extends Assignment diff --git a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala index 883d861b6..ec44293de 100644 --- a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala +++ b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala @@ -8,7 +8,7 @@ package viper.gobra.ast.internal.transform import viper.gobra.ast.internal._ import viper.gobra.reporting.Source -import viper.gobra.reporting.Source.OverflowCheckAnnotation +import viper.gobra.reporting.Source.{AnnotatedOrigin, InhaleInsteadOfAssignmentAnnotation, OverflowCheckAnnotation} import viper.gobra.reporting.Source.Parser.Single import viper.gobra.util.TypeBounds.BoundedIntegerKind import viper.gobra.util.Violation.violation @@ -134,10 +134,20 @@ object OverflowChecksTransform extends InternalTransform { case m@SafeMapLookup(_, _, IndexedExp(base, idx, _)) => Seqn(genOverflowChecksExprs(Vector(base, idx)) :+ m)(m.info) + case i@Inhale(a) => + i.info.origin match { + case Some(o: AnnotatedOrigin) if o.annotation == InhaleInsteadOfAssignmentAnnotation => + a match { + case ExprAssertion(e) => Seqn(genOverflowChecksExprs(Vector(e)) :+ i)(i.info) + case a => violation(s"unexpected assertion $a.") + } + case _ => i + } + // explicitly matches remaining statements to detect non-exhaustive pattern matching if a new statement is added - case x@(_: Inhale | _: Exhale | _: Assert | _: Assume + case x@(_: Exhale | _: Assert | _: Assume | _: Return | _: Fold | _: Unfold | _: PredExprFold | _: PredExprUnfold | _: Outline - | _: SafeTypeAssertion | _: SafeReceive | _: Label | _: Initialization | _: PatternMatchStmt) => x + | _: SafeTypeAssertion | _: SafeReceive | _: Label | _: Initialization | _: Allocation | _: PatternMatchStmt) => x case _ => violation("Unexpected case reached.") } diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index f56fd3004..c039fb81d 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -15,7 +15,7 @@ import viper.gobra.frontend.info.base.Type._ import viper.gobra.frontend.info.base.{BuiltInMemberTag, Type, SymbolTable => st} import viper.gobra.frontend.info.implementation.resolution.MemberPath import viper.gobra.frontend.info.{ExternalTypeInfo, TypeInfo} -import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstablished, MainPreNotEstablished} +import viper.gobra.reporting.Source.{AutoImplProofAnnotation, ImportPreNotEstablished, InhaleInsteadOfAssignmentAnnotation, MainPreNotEstablished} import viper.gobra.reporting.{DesugaredMessage, Source} import viper.gobra.theory.Addressability import viper.gobra.translator.Names @@ -963,17 +963,29 @@ object Desugar { val src: Meta = meta(stmt, info) - /** - * Desugars the left side of an assignment, short variable declaration, and normal variable declaration. - * If the left side is an identifier definition, a variable declaration and initialization is written, as well. - */ - def leftOfAssignmentD(idn: PIdnNode, info: TypeInfo)(t: in.Type): Writer[in.Assignee] = { - val isDef = idn match { + trait InitMode + + object InitMode { + // TODO(suggestion): we could remove `leftOfAssignmentNoInit` altogether by introducing the following mode + // case object SkipAllocAndInit extends InitMode + case object OnlyAlloc extends InitMode + case object AllocAndInit extends InitMode + } + + def isDef(idn: PIdnNode, info: TypeInfo): Boolean = { + idn match { case _: PIdnDef => true case unk: PIdnUnk if info.isDef(unk) => true case _ => false } + } + /** + * Desugars the left side of an assignment, short variable declaration, and normal variable declaration. + * If the left side is an identifier definition, a variable declaration and allocation/initialization are also + * written, depending on the value of `initMode`. + */ + def leftOfAssignmentD(idn: PIdnNode, info: TypeInfo, initMode: InitMode)(t: in.Type): Writer[in.Assignee] = { idn match { case _: PWildcard => freshDeclaredExclusiveVar(t.withAddressability(Addressability.Exclusive), idn, info)(src).map(in.Assignee.Var) @@ -982,11 +994,15 @@ object Desugar { case Left(v) => v case Right(v) => violation(s"Expected an assignable variable, but got $v instead") } - if (isDef) { + if (isDef(idn, info)) { val v = x.asInstanceOf[in.LocalVar] for { _ <- declare(v) - _ <- write(in.Initialization(v)(src)) + allocOrInit = initMode match { + case InitMode.OnlyAlloc => in.Allocation(v)(src) + case InitMode.AllocAndInit => in.Initialization(v)(src) + } + _ <- write(allocOrInit) } yield in.Assignee(v) } else unit(in.Assignee(x)) } @@ -1348,7 +1364,7 @@ object Desugar { domain = in.MapKeys(c, underlyingType(exp.typ))(src) - visited <- leftOfAssignmentD(range.enumerated, info)(in.SetT(keyType, Addressability.exclusiveVariable)) + visited <- leftOfAssignmentD(range.enumerated, info, InitMode.AllocAndInit)(in.SetT(keyType, Addressability.exclusiveVariable)) perm <- freshDeclaredExclusiveVar(in.PermissionT(Addressability.exclusiveVariable), n, info)(src) @@ -1430,7 +1446,7 @@ object Desugar { domain = in.MapKeys(c, underlyingType(exp.typ))(src) - visited <- leftOfAssignmentD(range.enumerated, info)(in.SetT(keyType, Addressability.exclusiveVariable)) + visited <- leftOfAssignmentD(range.enumerated, info, InitMode.AllocAndInit)(in.SetT(keyType, Addressability.exclusiveVariable)) perm <- freshDeclaredExclusiveVar(in.PermissionT(Addressability.exclusiveVariable), n, info)(src) @@ -1644,18 +1660,16 @@ object Desugar { seqn(sequence((left zip right).map{ case (l, r) => for { re <- goE(r) - le <- leftOfAssignmentD(l, info)(re.typ) - } yield singleAss(le, re)(src) + le <- leftOfAssignmentD(l, info, InitMode.OnlyAlloc)(re.typ) + } yield singleAss(le, re, isInitExpr = isDef(l, info))(src) }).map(in.Seqn(_)(src))) } else if (right.size == 1) { seqn(for { re <- goE(right.head) les <- sequence(left.map{ l => - for { - dL <- leftOfAssignmentD(l, info)(typeD(info.typ(l), Addressability.exclusiveVariable)(src)) - } yield dL + leftOfAssignmentD(l, info, InitMode.OnlyAlloc)(typeD(info.typ(l), Addressability.exclusiveVariable)(src)) }) - } yield multiassD(les, re, stmt)(src)) + } yield multiassD(les, re, stmt, isInitExpr = left.forall(l => isDef(l, info)))(src)) } else { violation("invalid assignment") } case PVarDecl(typOpt, right, left, _) => @@ -1665,32 +1679,19 @@ object Desugar { for { re <- goE(r) typ = typOpt.map(x => typeD(info.symbType(x), Addressability.exclusiveVariable)(src)).getOrElse(re.typ) - dL <- leftOfAssignmentD(l, info)(typ) + dL <- leftOfAssignmentD(l, info, InitMode.OnlyAlloc)(typ) le <- unit(dL) - } yield singleAss(le, re)(src) + } yield singleAss(le, re, isInitExpr = isDef(l, info))(src) }).map(in.Seqn(_)(src))) } else if (right.size == 1) { seqn(for { re <- goE(right.head) - les <- sequence(left.map{l => - for { - dL <- leftOfAssignmentD(l, info)(re.typ) - } yield dL - }) - } yield multiassD(les, re, stmt)(src)) + les <- sequence(left.map{leftOfAssignmentD(_, info, InitMode.OnlyAlloc)(re.typ)}) + } yield multiassD(les, re, stmt, isInitExpr = left.forall(l => isDef(l, info)))(src)) } else if (right.isEmpty && typOpt.nonEmpty) { val typ = typeD(info.symbType(typOpt.get), Addressability.exclusiveVariable)(src) - val lelems = sequence(left.map{ l => - for { - dL <- leftOfAssignmentD(l, info)(typ) - } yield dL - }) - val relems = left.map{ l => in.DfltVal(typeD(info.symbType(typOpt.get), Addressability.defaultValue)(meta(l, info)))(meta(l, info)) } - seqn(lelems.map{ lelemsV => - in.Seqn((lelemsV zip relems).map{ - case (l, r) => singleAss(l, r)(src) - })(src) - }) + val lelems = sequence(left.map{ leftOfAssignmentD(_, info, InitMode.AllocAndInit)(typ) }) + for {_ <- lelems} yield in.Seqn(Vector())(src) } else { violation("invalid declaration") } case PReturn(exps) => @@ -1925,11 +1926,11 @@ object Desugar { } yield (acceptCond, stmt) } - def multiassD(lefts: Vector[in.Assignee], right: in.Expr, astCtx: PNode)(src: Source.Parser.Info): in.Stmt = { + def multiassD(lefts: Vector[in.Assignee], right: in.Expr, astCtx: PNode, isInitExpr: Boolean = false)(src: Source.Parser.Info): in.Stmt = { right match { case in.Tuple(args) if args.size == lefts.size => - in.Seqn(lefts.zip(args) map { case (l, r) => singleAss(l, r)(src)})(src) + in.Seqn(lefts.zip(args) map { case (l, r) => singleAss(l, r, isInitExpr)(src)})(src) case n: in.TypeAssertion if lefts.size == 2 => val resTarget = freshExclusiveVar(lefts(0).op.typ.withAddressability(Addressability.exclusiveVariable), astCtx, info)(src) @@ -1938,8 +1939,8 @@ object Desugar { Vector(resTarget, successTarget), Vector( // declare for the fresh variables is not necessary because they are put into a block in.SafeTypeAssertion(resTarget, successTarget, n.exp, n.arg)(n.info), - singleAss(lefts(0), resTarget)(src), - singleAss(lefts(1), successTarget)(src) + singleAss(lefts(0), resTarget, isInitExpr)(src), + singleAss(lefts(1), successTarget, isInitExpr)(src) ) )(src) @@ -1954,8 +1955,8 @@ object Desugar { Vector(resTarget, successTarget), Vector( // declare for the fresh variables is not necessary because they are put into a block in.SafeReceive(resTarget, successTarget, n.channel, recvChannelProxy, recvGivenPermProxy, recvGotPermProxy, closedProxy)(n.info), - singleAss(lefts(0), resTarget)(src), - singleAss(lefts(1), successTarget)(src) + singleAss(lefts(0), resTarget, isInitExpr)(src), + singleAss(lefts(1), successTarget, isInitExpr)(src) ) )(src) @@ -1966,8 +1967,8 @@ object Desugar { Vector(resTarget, successTarget), Vector( in.SafeMapLookup(resTarget, successTarget, l)(l.info), - singleAss(lefts(0), resTarget)(src), - singleAss(lefts(1), successTarget)(src) + singleAss(lefts(0), resTarget, isInitExpr)(src), + singleAss(lefts(1), successTarget, isInitExpr)(src) ) )(src) @@ -2337,8 +2338,20 @@ object Desugar { } } - def singleAss(left: in.Assignee, right: in.Expr)(info: Source.Parser.Info): in.SingleAss = { - in.SingleAss(left, implicitConversion(right.typ, left.op.typ, right))(info) + def singleAss(left: in.Assignee, right: in.Expr, isInitExpr: Boolean = false)(info: Source.Parser.Info): in.Stmt = { + if (isInitExpr) { + val newInfo = info match { + case s: Source.Parser.Single => s.createAnnotatedInfo(InhaleInsteadOfAssignmentAnnotation) + case i => violation(s"l.op.info ($i) is expected to be a Single") + } + // Optimization: if we know that right is the expr passed to the declaration of left, then there is no need to + // assign to left (which implies exhaling and inhaling the footprint). Instead, we can just assume directly the + // equality between left and right. + val eq = in.ExprAssertion(in.GhostEqCmp(left.op, implicitConversion(right.typ, left.op.typ, right))(newInfo))(newInfo) + in.Inhale(eq)(newInfo) + } else { + in.SingleAss(left, implicitConversion(right.typ, left.op.typ, right))(info) + } } def arguments(symb: st.WithArguments, args: Vector[in.Expr]): Vector[in.Expr] = { diff --git a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala index 2cc79ddc3..d6971f8e3 100644 --- a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala +++ b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala @@ -6,8 +6,7 @@ package viper.gobra.reporting -import viper.gobra.reporting.Source.{AutoImplProofAnnotation, CertainSource, CertainSynthesized, ImportPreNotEstablished, MainPreNotEstablished, OverflowCheckAnnotation, ReceiverNotNilCheckAnnotation, InsufficientPermissionToRangeExpressionAnnotation, LoopInvariantNotEstablishedAnnotation} - +import viper.gobra.reporting.Source.{AutoImplProofAnnotation, CertainSource, CertainSynthesized, ImportPreNotEstablished, InhaleInsteadOfAssignmentAnnotation, InsufficientPermissionToRangeExpressionAnnotation, LoopInvariantNotEstablishedAnnotation, MainPreNotEstablished, OverflowCheckAnnotation, ReceiverNotNilCheckAnnotation} import viper.gobra.reporting.Source.Verifier./ import viper.silver import viper.silver.ast.Not @@ -185,6 +184,11 @@ class DefaultErrorBackTranslator( case _ / LoopInvariantNotEstablishedAnnotation => x.reasons.foldLeft(LoopInvariantEstablishmentError(x.info): VerificationError) { case (err, reason) => err dueTo reason } + case _ / InhaleInsteadOfAssignmentAnnotation => + x.reasons.foldLeft(AssignmentError(x.info): VerificationError){ + case (err, reason) => err dueTo reason + } + case _ => x } diff --git a/src/main/scala/viper/gobra/reporting/Source.scala b/src/main/scala/viper/gobra/reporting/Source.scala index 6204aa50d..0fd901dc6 100644 --- a/src/main/scala/viper/gobra/reporting/Source.scala +++ b/src/main/scala/viper/gobra/reporting/Source.scala @@ -30,6 +30,7 @@ object Source { case object ImportPreNotEstablished extends Annotation case object MainPreNotEstablished extends Annotation case object LoopInvariantNotEstablishedAnnotation extends Annotation + case object InhaleInsteadOfAssignmentAnnotation extends Annotation case class NoPermissionToRangeExpressionAnnotation() extends Annotation case class InsufficientPermissionToRangeExpressionAnnotation() extends Annotation case class AutoImplProofAnnotation(subT: String, superT: String) extends Annotation diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala index a64938693..727587f48 100644 --- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala @@ -110,19 +110,13 @@ trait TypeEncoding extends Generator { * Initialize[loc: T@] -> inhale Footprint[loc]; assume [loc == dflt(T°)] && [&loc != nil(*T)] */ def initialization(ctx: Context): in.Location ==> CodeWriter[vpr.Stmt] = { - case loc :: t / Exclusive if typ(ctx).isDefinedAt(t) => + case loc :: t if typ(ctx).isDefinedAt(t) => val (pos, info, errT) = loc.vprMeta for { + alloc <- ctx.allocation(loc) + _ <- write(alloc) eq <- ctx.equal(loc, in.DfltVal(t.withAddressability(Exclusive))(loc.info))(loc) } yield vpr.Inhale(eq)(pos, info, errT): vpr.Stmt - - case loc :: t / Shared if typ(ctx).isDefinedAt(t) => - val (pos, info, errT) = loc.vprMeta - for { - footprint <- addressFootprint(ctx)(loc, in.FullPerm(loc.info)) - eq1 <- ctx.equal(loc, in.DfltVal(t.withAddressability(Exclusive))(loc.info))(loc) - eq2 <- ctx.equal(in.Ref(loc)(loc.info), in.NilLit(in.PointerT(t, Exclusive))(loc.info))(loc) - } yield vpr.Inhale(vpr.And(footprint, vpr.And(eq1, vpr.Not(eq2)(pos, info, errT))(pos, info, errT))(pos, info, errT))(pos, info, errT) } /** diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala index b5149518a..d5e38937a 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala @@ -32,6 +32,7 @@ class MemoryEncoding extends Encoding { } override def statement(ctx: Context): in.Stmt ==> CodeWriter[vpr.Stmt] = { + case in.Allocation(left) => ctx.allocation(left) case in.Initialization(left) => ctx.initialization(left) case ass: in.SingleAss => ctx.assignment(ass.left, ass.right)(ass) } diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/visitor_pattern.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/visitor_pattern.gobra index 7c808b42d..f00a6cb74 100644 --- a/src/test/resources/regressions/examples/evaluation/impl_errors/visitor_pattern.gobra +++ b/src/test/resources/regressions/examples/evaluation/impl_errors/visitor_pattern.gobra @@ -168,4 +168,4 @@ func isAstNode(n node) (res bool) { } else { return false } -} \ No newline at end of file +}