From ef98d4389795f56affe670d2dc7e4e496affd07e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 11:50:07 +0100 Subject: [PATCH 1/6] add test --- .../resources/regressions/issues/000796.gobra | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 src/test/resources/regressions/issues/000796.gobra diff --git a/src/test/resources/regressions/issues/000796.gobra b/src/test/resources/regressions/issues/000796.gobra new file mode 100644 index 000000000..d80945e9d --- /dev/null +++ b/src/test/resources/regressions/issues/000796.gobra @@ -0,0 +1,20 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue000796 + +func m1() { + //:: ExpectedOutput(type_error) + ghost for { + + } +} + +func m2() { + ghost { + //:: ExpectedOutput(type_error) + for { + + } + } +} \ No newline at end of file From d1f21a96dc72a873802c600e03af320ee5272188 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 11:50:49 +0100 Subject: [PATCH 2/6] add fix --- .../frontend/info/implementation/typing/StmtTyping.scala | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala index 70e0d7deb..09d996a4a 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info.implementation.typing -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message, noMessages} import viper.gobra.ast.frontend._ import viper.gobra.ast.frontend.{AstPattern => ap, _} import viper.gobra.frontend.info.base.{SymbolTable => st} @@ -105,7 +105,11 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => } if (firstChecks.isEmpty) latterChecks else firstChecks - case n@PForStmt(_, cond, _, _, _) => isExpr(cond).out ++ comparableTypes.errors(exprType(cond), BooleanT)(n) + case n@PForStmt(_, cond, _, spec, _) => + val isGhost = isEnclosingGhost(n) + isExpr(cond).out ++ + comparableTypes.errors(exprType(cond), BooleanT)(n) ++ + error(n, s"Loop occurring in ghost context does not have a termination measure", isGhost && spec.terminationMeasure.isEmpty) case PShortForRange(range, shorts, _, _, _) => underlyingType(exprType(range.exp)) match { From 443901d1a4fa1e896e7cb6d0ff2c5b397faa7281 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 11:54:29 +0100 Subject: [PATCH 3/6] cleanup --- .../frontend/info/implementation/typing/StmtTyping.scala | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala index 09d996a4a..c467ab0da 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/StmtTyping.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info.implementation.typing -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, message, noMessages} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} import viper.gobra.ast.frontend._ import viper.gobra.ast.frontend.{AstPattern => ap, _} import viper.gobra.frontend.info.base.{SymbolTable => st} @@ -107,9 +107,10 @@ trait StmtTyping extends BaseTyping { this: TypeInfoImpl => case n@PForStmt(_, cond, _, spec, _) => val isGhost = isEnclosingGhost(n) + val noTerminationMeasureMsg = "Loop occurring in ghost context does not have a termination measure" isExpr(cond).out ++ comparableTypes.errors(exprType(cond), BooleanT)(n) ++ - error(n, s"Loop occurring in ghost context does not have a termination measure", isGhost && spec.terminationMeasure.isEmpty) + error(n, noTerminationMeasureMsg, isGhost && spec.terminationMeasure.isEmpty) case PShortForRange(range, shorts, _, _, _) => underlyingType(exprType(range.exp)) match { From fe46108f340381be11a1bc126d7740266a63e22a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 13:31:05 +0100 Subject: [PATCH 4/6] fix tests --- .../examples/evaluation/impl_errors/parallel_sum.gobra | 1 + .../examples/evaluation/parallel_search_replace.gobra | 1 + .../regressions/examples/evaluation/parallel_sum.gobra | 1 + .../evaluation/spec_errors/parallel_search_replace.gobra | 1 + .../examples/evaluation/spec_errors/parallel_sum.gobra | 1 + .../examples/parallel_search_replace_shared.gobra | 1 + .../regressions/features/sequences/seq-index-fail10.gobra | 7 +++++-- .../regressions/features/sequences/seq-index-fail9.gobra | 5 ++++- .../regressions/features/sequences/seq-index-simple1.gobra | 5 ++++- 9 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra index 4e5cd982c..21b06c68d 100644 --- a/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra +++ b/src/test/resources/regressions/examples/evaluation/impl_errors/parallel_sum.gobra @@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) { invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2) invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!> invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j)) + decreases n - i for i:=0; i < n; i++ { unfold sync.InjEval(tokens[i], i) unfold locHasVal!<&seenSlice[i],s[i]!>() diff --git a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra index 9942e04ed..82f22ddcd 100644 --- a/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra +++ b/src/test/resources/regressions/examples/evaluation/parallel_search_replace.gobra @@ -127,6 +127,7 @@ func SearchReplace(s []int, x, y int) { invariant forall j int :: 0 <= j && j < (i == len(seqs) ? len(s) : i * workRange) ==> acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j]) + decreases len(pseqs) - i for i := 0; i != len(pseqs); i++ { unfold sync.InjEval(pseqs[i],i) low := i * workRange diff --git a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra index 90357b532..9bd88a507 100644 --- a/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra +++ b/src/test/resources/regressions/examples/evaluation/parallel_sum.gobra @@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) { invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2) invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!> invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j)) + decreases n - i for i:=0; i < n; i++ { unfold sync.InjEval(tokens[i], i) unfold locHasVal!<&seenSlice[i],s[i]!>() diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra index f1c345a53..509af763d 100644 --- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra +++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_search_replace.gobra @@ -128,6 +128,7 @@ func SearchReplace(s []int, x, y int) { invariant forall j int :: 0 <= j && j < (i == len(seqs) ? len(s) : i * workRange) ==> acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j]) + decreases len(pseqs) - i for i := 0; i != len(pseqs); i++ { unfold sync.InjEval(pseqs[i],i) low := i * workRange diff --git a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra index 8faf2c427..dcec71c89 100644 --- a/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra +++ b/src/test/resources/regressions/examples/evaluation/spec_errors/parallel_sum.gobra @@ -77,6 +77,7 @@ func ParallelSum(s []int) (res int) { invariant forall j int :: 0 <= j && j < n ==> acc(&s[j], 1/2) invariant forall j int :: 0 <= j && j < n ==> tokens[j] == locHasVal!<&seenSlice[j],s[j]!> invariant forall j int :: 0 <= j && j < n ==> (j < i ? acc(&seenSlice[j], 1/2) && seenSlice[j] == s[j] : sync.InjEval(tokens[j], j)) + decreases n - i for i:=0; i < n; i++ { unfold sync.InjEval(tokens[i], i) unfold locHasVal!<&seenSlice[i],s[i]!>() diff --git a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra index 6d9a3f4dd..6fb31c82b 100644 --- a/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra +++ b/src/test/resources/regressions/examples/parallel_search_replace_shared.gobra @@ -139,6 +139,7 @@ func SearchReplace(s []int, x, y int) { invariant forall j int :: 0 <= j && j < (i == len(seqs) ? len(s) : i * workRange) ==> acc(&s[j]) && s[j] == (s0[j] == x ? y : s0[j]) + decreases len(pseqs) - i for i := 0; i != len(pseqs); i++ { unfold sync.InjEval(pseqs[i],i) low := i * workRange diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra index cf49e78b3..0307062b6 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra @@ -5,6 +5,9 @@ package pkg requires 0 < len(xs) func foo(ghost xs seq[bool]) { - //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error) - ghost for ;xs[42]; { } + ghost { + //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error) + decreases _ + for ;xs[42]; { } + } } diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra index eb0c91472..da572ec2c 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra @@ -6,5 +6,8 @@ package pkg requires 0 < len(xs) func foo(ghost xs seq[bool]) { //:: ExpectedOutput(for_loop_error:seq_index_negative_error) - ghost for ;xs[-1]; { } + ghost { + decreases _ + for ;xs[-1]; { } + } } diff --git a/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra b/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra index aa358a761..d8922779e 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-simple1.gobra @@ -39,5 +39,8 @@ func example7(ghost xs seq[bool]) { requires 0 < len(xs) func example8(ghost xs seq[bool]) { - ghost for ;xs[0]; { } + ghost { + decreases + for ;xs[0]; { break } + } } From c6f1d8794b3fba9ebf73e0ed3d60eaca5c030188 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 13:31:53 +0100 Subject: [PATCH 5/6] fix tests --- .../regressions/features/sequences/seq-index-fail10.gobra | 4 ++-- .../regressions/features/sequences/seq-index-fail9.gobra | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra index 0307062b6..e0d32bd4d 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra @@ -7,7 +7,7 @@ requires 0 < len(xs) func foo(ghost xs seq[bool]) { ghost { //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error) - decreases _ - for ;xs[42]; { } + decreases + for ;xs[42]; { break } } } diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra index da572ec2c..d02b8d543 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra @@ -7,7 +7,7 @@ requires 0 < len(xs) func foo(ghost xs seq[bool]) { //:: ExpectedOutput(for_loop_error:seq_index_negative_error) ghost { - decreases _ - for ;xs[-1]; { } + decreases + for ;xs[-1]; { break } } } From 0a41811ada2c929e9908ae31e82b928956f18bbd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 27 Nov 2024 14:00:22 +0100 Subject: [PATCH 6/6] fix test annotations --- .../regressions/features/sequences/seq-index-fail10.gobra | 2 +- .../regressions/features/sequences/seq-index-fail9.gobra | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra index e0d32bd4d..0dba9f06e 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail10.gobra @@ -6,8 +6,8 @@ package pkg requires 0 < len(xs) func foo(ghost xs seq[bool]) { ghost { - //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error) decreases + //:: ExpectedOutput(for_loop_error:seq_index_exceeds_length_error) for ;xs[42]; { break } } } diff --git a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra index d02b8d543..dbd56f595 100644 --- a/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra +++ b/src/test/resources/regressions/features/sequences/seq-index-fail9.gobra @@ -5,9 +5,9 @@ package pkg requires 0 < len(xs) func foo(ghost xs seq[bool]) { - //:: ExpectedOutput(for_loop_error:seq_index_negative_error) ghost { decreases + //:: ExpectedOutput(for_loop_error:seq_index_negative_error) for ;xs[-1]; { break } } }