From 0f79ab21f8e300c4a849572932df4482dbcc0020 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 26 Feb 2025 11:16:55 +0100 Subject: [PATCH 1/2] fixes type of old and labeled old to always be exclusive --- .../viper/gobra/ast/internal/PrettyPrinter.scala | 2 +- .../scala/viper/gobra/ast/internal/Program.scala | 6 ++++-- src/main/scala/viper/gobra/frontend/Desugar.scala | 2 +- .../encodings/typeless/AssertionEncoding.scala | 2 +- .../encodings/typeless/BuiltInEncoding.scala | 6 +++--- .../resources/regressions/issues/000620-1.gobra | 14 ++++++++++++++ .../resources/regressions/issues/000620-2.gobra | 15 +++++++++++++++ 7 files changed, 39 insertions(+), 8 deletions(-) create mode 100644 src/test/resources/regressions/issues/000620-1.gobra create mode 100644 src/test/resources/regressions/issues/000620-2.gobra diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala index 4b7950e42..f3d2de0c5 100644 --- a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala @@ -478,7 +478,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter case PureLet(left, right, exp) => "let" <+> showVar(left) <+> "==" <+> parens(showExpr(right)) <+> "in" <+> showExpr(exp) - case Old(op, _) => "old" <> parens(showExpr(op)) + case Old(op) => "old" <> parens(showExpr(op)) case LabeledOld(label, operand) => "old" <> brackets(showProxy(label)) <> parens(showExpr(operand)) diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala index 66e417efb..6ff413f24 100644 --- a/src/main/scala/viper/gobra/ast/internal/Program.scala +++ b/src/main/scala/viper/gobra/ast/internal/Program.scala @@ -563,10 +563,12 @@ case class PureLet(left: LocalVar, right: Expr, in: Expr)(val info: Source.Parse case class Let(left: LocalVar, right: Expr, in: Assertion)(val info: Source.Parser.Info) extends Assertion -case class Old(operand: Expr, typ: Type)(val info: Source.Parser.Info) extends Expr +case class Old(operand: Expr)(val info: Source.Parser.Info) extends Expr { + override def typ: Type = operand.typ.withAddressability(Addressability.rValue) +} case class LabeledOld(label: LabelProxy, operand: Expr)(val info: Source.Parser.Info) extends Expr { - override val typ: Type = operand.typ + override val typ: Type = operand.typ.withAddressability(Addressability.rValue) } case class Conditional(cond: Expr, thn: Expr, els: Expr, typ: Type)(val info: Source.Parser.Info) extends Expr diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 9b185a529..02bf27df1 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -4291,7 +4291,7 @@ object Desugar extends LazyLogging { val typ = typeD(info.typ(expr), info.addressability(expr))(src) expr match { - case POld(op) => for {o <- go(op)} yield in.Old(o, typ)(src) + case POld(op) => for {o <- go(op)} yield in.Old(o)(src) case PLabeledOld(l, op) => for {o <- go(op)} yield in.LabeledOld(labelProxy(l), o)(src) case PBefore(op) => for {o <- go(op)} yield in.LabeledOld(in.LabelProxy("before")(src), o)(src) case PConditional(cond, thn, els) => for { diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala index dbbdb4e2d..46ef471f4 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/AssertionEncoding.scala @@ -21,7 +21,7 @@ class AssertionEncoding extends Encoding { import viper.gobra.translator.util.ViperWriter.CodeLevel._ override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = { - case n@ in.Old(op, _) => for { o <- ctx.expression(op)} yield withSrc(vpr.Old(o), n) + case n@ in.Old(op) => for { o <- ctx.expression(op)} yield withSrc(vpr.Old(o), n) case n@ in.LabeledOld(l, op) => for {o <- ctx.expression(op)} yield withSrc(vpr.LabelledOld(o, l.name), n) case n@ in.Negation(op) => for{o <- ctx.expression(op)} yield withSrc(vpr.Not(o), n) diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala index 71aab6317..afd9bf6e8 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala @@ -483,7 +483,7 @@ class BuiltInEncoding extends Encoding { i => in.ExprAssertion( in.GhostEqCmp( in.IndexedExp(resultParam, i, sliceType)(src), - in.Old(in.IndexedExp(sliceParam, i, sliceType)(src), elemType)(src) + in.Old(in.IndexedExp(sliceParam, i, sliceType)(src))(src) )(src) )(src) } @@ -586,7 +586,7 @@ class BuiltInEncoding extends Encoding { in.ExprAssertion( in.GhostEqCmp( in.IndexedExp(dstParam, i, dstUnderlyingType)(src), - in.Old(in.IndexedExp(srcParam, i, srcUnderlyingType)(src), srcUnderlyingType.elems)(src) + in.Old(in.IndexedExp(srcParam, i, srcUnderlyingType)(src))(src) )(src) )(src) } @@ -598,7 +598,7 @@ class BuiltInEncoding extends Encoding { in.ExprAssertion( in.GhostEqCmp( in.IndexedExp(dstParam, i, dstUnderlyingType)(src), - in.Old(in.IndexedExp(dstParam, i, dstUnderlyingType)(src), dstUnderlyingType.elems)(src) + in.Old(in.IndexedExp(dstParam, i, dstUnderlyingType)(src))(src) )(src) )(src) } diff --git a/src/test/resources/regressions/issues/000620-1.gobra b/src/test/resources/regressions/issues/000620-1.gobra new file mode 100644 index 000000000..2d3dba070 --- /dev/null +++ b/src/test/resources/regressions/issues/000620-1.gobra @@ -0,0 +1,14 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +type MyType struct { + x int +} + +func main() { + mySlice := make([]MyType, 0) + snd := []MyType{MyType{1}} + mySlice = append(perm(1/2), mySlice, snd...) +} diff --git a/src/test/resources/regressions/issues/000620-2.gobra b/src/test/resources/regressions/issues/000620-2.gobra new file mode 100644 index 000000000..cd2ee09f9 --- /dev/null +++ b/src/test/resources/regressions/issues/000620-2.gobra @@ -0,0 +1,15 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +type MyStruct struct { + x int +} + + +func test() { + myStruct @ := MyStruct{42} + l: + assert myStruct == old[l](myStruct) +} From c66a7d666f51edc957ee2d3a57f706964cc6a590 Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Wed, 26 Feb 2025 11:27:42 +0100 Subject: [PATCH 2/2] adds another test case --- src/test/resources/regressions/issues/000620-2.gobra | 1 - src/test/resources/regressions/issues/000620-3.gobra | 10 ++++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/regressions/issues/000620-3.gobra diff --git a/src/test/resources/regressions/issues/000620-2.gobra b/src/test/resources/regressions/issues/000620-2.gobra index cd2ee09f9..52a472bd7 100644 --- a/src/test/resources/regressions/issues/000620-2.gobra +++ b/src/test/resources/regressions/issues/000620-2.gobra @@ -7,7 +7,6 @@ type MyStruct struct { x int } - func test() { myStruct @ := MyStruct{42} l: diff --git a/src/test/resources/regressions/issues/000620-3.gobra b/src/test/resources/regressions/issues/000620-3.gobra new file mode 100644 index 000000000..6fc4984ec --- /dev/null +++ b/src/test/resources/regressions/issues/000620-3.gobra @@ -0,0 +1,10 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package main + +func test() { + myInt @ := 42 + l: + assert myInt == old[l](myInt) +}