From 9a15e1a5535bbc906cbfc2dd76e1d0d0002ff852 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 6 Feb 2023 14:05:55 +0100 Subject: [PATCH 01/11] Added section on debugging to README. --- README.md | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c0c6760ae..30e6dc3c2 100644 --- a/README.md +++ b/README.md @@ -36,21 +36,41 @@ Gobra can be run either from sbt or from a compiled jar: - running from sbt: 1. change directory to the `gobra` directory obtained from cloning this repository. 2. run `sbt`. - 3. inside the sbt shell, run `run - i path/to/file` (e.g., `run -i src/test/resources/regressions/examples/swap.gobra`) + 3. inside the sbt shell, run `run - i path/to/file` ( + e.g., `run -i src/test/resources/regressions/examples/swap.gobra`) - running from a compiled jar: 1. run `java -jar -Xss128m path/to/gobra.jar -i path/to/file`. -More information about the available options in Gobra can be found by running `run --help` in an sbt shell or `java -jar path/to/gobra.jar --help` if you assembled Gobra. +More information about the available options in Gobra can be found by running `run --help` in an sbt shell +or `java -jar path/to/gobra.jar --help` if you assembled Gobra. ### Running the Tests + In the `gobra` directory, run the command `sbt test`. +### Debugging + +By default, Gobra runs in sbt on a forked VM. This means that simply attaching a debugger to sbt will not work. There +are two workarounds: + +- Run Gobra in a non-forked VM by first running `set fork := false` in sbt. This will allow you to attach a debugger to + sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually + only the parsing can really be debugged. +- Attach the debugger to the forked VM. By + running `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` in sbt, the forked + VM can be debugged. However, this will require starting the debugger for each run after the VM has started and is + ready for connection. In particular, it may be more difficult to debug early stages. + ## Licensing + Most Gobra sources are licensed under the Mozilla Public License Version 2.0. The [LICENSE](./LICENSE) lists the exceptions to this rule. Note that source files (whenever possible) should list their license in a short header. Continuous integration checks these file headers. -The same checks can be performed locally by running `npx github:viperproject/check-license-header#v1 check --config .github/license-check/config.json --strict` in this repository's root directory. +The same checks can be performed locally by +running `npx github:viperproject/check-license-header#v1 check --config .github/license-check/config.json --strict` in +this repository's root directory. ## Get in touch + Do you still have questions? Open an issue or contact us on [Zulip](https://gobra.zulipchat.com). From 5647db533c8fab15ee28c063e4f0f6454b0edbdc Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 6 Feb 2023 17:29:56 +0100 Subject: [PATCH 02/11] Clarified some stuff --- README.md | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 30e6dc3c2..b789ea611 100644 --- a/README.md +++ b/README.md @@ -50,16 +50,18 @@ In the `gobra` directory, run the command `sbt test`. ### Debugging -By default, Gobra runs in sbt on a forked VM. This means that simply attaching a debugger to sbt will not work. There +By default, Gobra runs in sbt on a forked JVM. This means that simply attaching a debugger to sbt will not work. There are two workarounds: -- Run Gobra in a non-forked VM by first running `set fork := false` in sbt. This will allow you to attach a debugger to +- Run Gobra in a non-forked JVM by first running `set fork := false` in sbt. This will allow you to attach a debugger to sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually only the parsing can really be debugged. -- Attach the debugger to the forked VM. By - running `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` in sbt, the forked - VM can be debugged. However, this will require starting the debugger for each run after the VM has started and is - ready for connection. In particular, it may be more difficult to debug early stages. +- Attach the debugger to the forked JVM. + Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` + in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be + debugged + instead of the sbt JVM. This requires starting the debugger again every time a new VM is created, e.g. for + every `run`. ## Licensing From cc21298266cd73d6301b2a292fd8e5705de985ab Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Mon, 6 Feb 2023 17:32:57 +0100 Subject: [PATCH 03/11] Reverted accidental formatting. --- README.md | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index b789ea611..45e1c5298 100644 --- a/README.md +++ b/README.md @@ -36,20 +36,16 @@ Gobra can be run either from sbt or from a compiled jar: - running from sbt: 1. change directory to the `gobra` directory obtained from cloning this repository. 2. run `sbt`. - 3. inside the sbt shell, run `run - i path/to/file` ( - e.g., `run -i src/test/resources/regressions/examples/swap.gobra`) + 3. inside the sbt shell, run `run - i path/to/file` (e.g., `run -i src/test/resources/regressions/examples/swap.gobra`) - running from a compiled jar: 1. run `java -jar -Xss128m path/to/gobra.jar -i path/to/file`. -More information about the available options in Gobra can be found by running `run --help` in an sbt shell -or `java -jar path/to/gobra.jar --help` if you assembled Gobra. +More information about the available options in Gobra can be found by running `run --help` in an sbt shell or `java -jar path/to/gobra.jar --help` if you assembled Gobra. ### Running the Tests - In the `gobra` directory, run the command `sbt test`. ### Debugging - By default, Gobra runs in sbt on a forked JVM. This means that simply attaching a debugger to sbt will not work. There are two workarounds: @@ -64,15 +60,11 @@ are two workarounds: every `run`. ## Licensing - Most Gobra sources are licensed under the Mozilla Public License Version 2.0. The [LICENSE](./LICENSE) lists the exceptions to this rule. Note that source files (whenever possible) should list their license in a short header. Continuous integration checks these file headers. -The same checks can be performed locally by -running `npx github:viperproject/check-license-header#v1 check --config .github/license-check/config.json --strict` in -this repository's root directory. +The same checks can be performed locally by running `npx github:viperproject/check-license-header#v1 check --config .github/license-check/config.json --strict` in this repository's root directory. ## Get in touch - Do you still have questions? Open an issue or contact us on [Zulip](https://gobra.zulipchat.com). From e0b4844d2c1f3f98c89885d15901054f9bd623cc Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Thu, 6 Apr 2023 13:09:50 +0200 Subject: [PATCH 04/11] Update README.md Co-authored-by: Linard Arquint --- README.md | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 45e1c5298..2d7f4ce32 100644 --- a/README.md +++ b/README.md @@ -53,11 +53,19 @@ are two workarounds: sbt normally. However, for unknown reasons, this causes issues with class resolution in the Viper backend, so actually only the parsing can really be debugged. - Attach the debugger to the forked JVM. - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` - in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be - debugged - instead of the sbt JVM. This requires starting the debugger again every time a new VM is created, e.g. for - every `run`. + - Create a debug configuration in IntelliJ and specify to `Attach to remote JVM`, set `localhost` as host, and + a port (e.g. 5005). + - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=5005"` + in sbt (use any port you like, just make sure to use the same one in the debugger). Now, the forked JVM can be + debugged instead of the sbt JVM. This requires starting the debugger again every time a new VM is created, + e.g. for every `run`. +- Let the debugger listen to the forked JVM. + - Create a debug configuration in IntelliJ and specify to `Listen to remote JVM`, enable auto restart, set + `localhost` as host, and a port (e.g. 5005). + - Run `set javaOptions += "-agentlib:jdwp=transport=dt_socket,server=n,address=localhost:5005,suspend=y"` in sbt. + Thanks to auto restart, the debugger keeps listening even when the JVM is restarted, e.g. for every `run`. + Note however that the debugger must be running/listening as otherwise the JVM will emit a connection + refused error. ## Licensing Most Gobra sources are licensed under the Mozilla Public License Version 2.0. From ce668a9721075d7a3676c8c415c7feabb8534865 Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Wed, 12 Apr 2023 18:54:40 +0200 Subject: [PATCH 05/11] Updates submodules (#644) Co-authored-by: jcp19 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 8ab7defa2..382dcb9f5 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 8ab7defa210e8df3aab962e7849966ab728a4863 +Subproject commit 382dcb9f5589b986ea8af392385aad809c9f74e1 From 9d15151c3aa2c001be158aa3c64666ed56e0de9c Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Wed, 19 Apr 2023 15:07:54 +0200 Subject: [PATCH 06/11] Updates submodules (#647) Co-authored-by: jcp19 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 382dcb9f5..2091da1b6 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 382dcb9f5589b986ea8af392385aad809c9f74e1 +Subproject commit 2091da1b66e0ede0692493ccb49f08d619622586 From f4babde357501183d6417130d80b26c02dd0b5a4 Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Fri, 5 May 2023 18:38:26 +0200 Subject: [PATCH 07/11] Updates submodules (#648) Co-authored-by: jcp19 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 2091da1b6..830c5fb98 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 2091da1b66e0ede0692493ccb49f08d619622586 +Subproject commit 830c5fb986992b5bae718acec1fe2209fc9e7090 From c0e1c408b582105153460f776aa67f038b33e9a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 11 May 2023 19:50:47 +0200 Subject: [PATCH 08/11] Update tutorial.md (#603) --- docs/tutorial.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/tutorial.md b/docs/tutorial.md index cace56515..d09f6bcf5 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -401,7 +401,7 @@ pure func toSeq(s []int) (res seq[int]) { Gobra supports many of Go's native types, namely integers (`int`, `int8`, `int16`, `int32`, `int64`, `byte`, `uint8`, `rune`, `uint16`, `uint32`, `uint64`, `uintptr`), strings, structs, pointers, arrays, slices, interfaces, and channels. Note that currently the support for strings and specific types of integers such as `rune` is very limited. -In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`|set1|`). +In addition, Gobra introduces additional ghost types for specification purposes. These are sequences (`seq[T]`), sets (`set[T]`), multisets (`mset[T]`), and permission amounts (`perm`). Gobra supports their common operations: sequence concatenation (`seq1 ++ seq2`), set union (`set1 union set2`), membership (`x in set1`), multiplicity (`x # set1`), sequence length (`len(seq1)`), and set cardinality (`len(set1)`). ## Interfaces @@ -680,4 +680,4 @@ java -Xss128m -jar gobra.jar -i [FILES_TO_VERIFY] To check the full list of flags available in Gobra, run the command ```bash java -jar gobra.jar -h -``` \ No newline at end of file +``` From 3ce34f3d02a84a227561e24b5909350aa8a3aac5 Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Fri, 12 May 2023 16:59:46 +0200 Subject: [PATCH 09/11] Updates submodules (#650) Co-authored-by: jcp19 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 830c5fb98..83881c346 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 830c5fb986992b5bae718acec1fe2209fc9e7090 +Subproject commit 83881c346240e8eab6d43d9794d774aace8db062 From 178f9852bb9f42bd0d3fefbd819cc06f50aee9d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 14 May 2023 17:35:44 +0200 Subject: [PATCH 10/11] Fix issue 651 (#652) * Add bug witness * Add fix * Reflect that the order of fields matter in the signature of AdtClauseT * use more general type --- .../viper/gobra/frontend/info/base/Type.scala | 4 +-- .../implementation/typing/ExprTyping.scala | 4 ++- .../info/implementation/typing/IdTyping.scala | 4 ++- .../implementation/typing/TypeTyping.scala | 2 +- .../typing/ghost/GhostIdTyping.scala | 3 ++- .../resources/regressions/issues/000651.gobra | 25 +++++++++++++++++++ 6 files changed, 36 insertions(+), 6 deletions(-) create mode 100644 src/test/resources/regressions/issues/000651.gobra diff --git a/src/main/scala/viper/gobra/frontend/info/base/Type.scala b/src/main/scala/viper/gobra/frontend/info/base/Type.scala index c0eb1bdf1..4e600a0fd 100644 --- a/src/main/scala/viper/gobra/frontend/info/base/Type.scala +++ b/src/main/scala/viper/gobra/frontend/info/base/Type.scala @@ -13,7 +13,7 @@ import viper.gobra.frontend.info.ExternalTypeInfo import viper.gobra.util.TypeBounds import scala.annotation.tailrec -import scala.collection.immutable.ListMap +import scala.collection.immutable.{ListMap, SeqMap} object Type { @@ -58,7 +58,7 @@ object Type { case class AdtT(decl: PAdtType, context: ExternalTypeInfo) extends Type - case class AdtClauseT(fields: Map[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type + case class AdtClauseT(fields: SeqMap[String, Type], decl: PAdtClause, adtT: PAdtType, context: ExternalTypeInfo) extends Type case class MapT(key: Type, elem: Type) extends PrettyType(s"map[$key]$elem") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 979af8e2e..902d34a80 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -14,6 +14,8 @@ import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.util.TypeBounds.{BoundedIntegerKind, UnboundedInteger} import viper.gobra.util.{Constants, TypeBounds, Violation} +import scala.collection.immutable.ListMap + trait ExprTyping extends BaseTyping { this: TypeInfoImpl => import viper.gobra.util.Violation._ @@ -145,7 +147,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => case Some(p: ap.DomainFunction) => FunctionT(p.symb.args map p.symb.context.typ, p.symb.context.typ(p.symb.result)) case Some(p: ap.AdtClause) => - val fields = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap + val fields = ListMap.from(p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ))) AdtClauseT(fields, p.symb.decl, p.symb.adtDecl, this) case Some(p: ap.AdtField) => p.symb match { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala index 0f1b234fd..492d515f8 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala @@ -14,6 +14,8 @@ import viper.gobra.frontend.info.base.Type._ import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.property.{AssignMode, StrictAssignMode} +import scala.collection.immutable.ListMap + trait IdTyping extends BaseTyping { this: TypeInfoImpl => import viper.gobra.util.Violation._ @@ -157,7 +159,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl => // ADT clause is special since it is a type with a name that is not a named type case a: AdtClause => - val types = a.fields.map(f => f.id.name -> a.context.symbType(f.typ)).toMap + val types = ListMap.from(a.fields.map(f => f.id.name -> a.context.symbType(f.typ))) AdtClauseT(types, a.decl, a.adtDecl, this) case BuiltInType(tag, _, _) => tag.typ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 15f131f3c..b5eeb6518 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -155,7 +155,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => // ADT clause is special since it is a type with a name that is not a named type case Some(p: ap.AdtClause) => - val types = p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ)).toMap + val types = ListMap.from(p.symb.fields.map(f => f.id.name -> p.symb.context.symbType(f.typ))) AdtClauseT(types, p.symb.decl, p.symb.adtDecl, p.symb.context) case _ => violation(s"expected type, but got $n") diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala index 5e2d996ac..b2688de4d 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostIdTyping.scala @@ -14,6 +14,7 @@ import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.util.Violation.violation import scala.annotation.unused +import scala.collection.immutable.ListMap trait GhostIdTyping { this: TypeInfoImpl => @@ -42,7 +43,7 @@ trait GhostIdTyping { this: TypeInfoImpl => case AdtClause(decl, adtDecl, context) => AdtClauseT( - decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ)).toMap, + ListMap.from(decl.args.flatMap(_.fields).map(f => f.id.name -> context.symbType(f.typ))), decl, adtDecl, context diff --git a/src/test/resources/regressions/issues/000651.gobra b/src/test/resources/regressions/issues/000651.gobra new file mode 100644 index 000000000..d199f9546 --- /dev/null +++ b/src/test/resources/regressions/issues/000651.gobra @@ -0,0 +1,25 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package test + +type A adt { + A_ { + a uint + b set[int] + c bool + d bool + e seq[int] + } +} + +ghost +decreases +pure func f(x A) A { + return A_ { + a: x.a, + b: x.b, + c: x.c, + d: x.d, + e: x.e} +} \ No newline at end of file From 5aeb8bf72e5618cc6dadfdd08aefd6f42d0f6c8c Mon Sep 17 00:00:00 2001 From: viper-admin <59963956+viper-admin@users.noreply.github.com> Date: Tue, 16 May 2023 12:02:56 +0200 Subject: [PATCH 11/11] Updates submodules (#653) Co-authored-by: jcp19 --- viperserver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/viperserver b/viperserver index 83881c346..bccf9e5f5 160000 --- a/viperserver +++ b/viperserver @@ -1 +1 @@ -Subproject commit 83881c346240e8eab6d43d9794d774aace8db062 +Subproject commit bccf9e5f5006ab1120da304917f24d6ae4b9f893