@@ -52,20 +52,6 @@ Definition exchangePointer {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_s
5252
5353Definition BroadcastExample {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.BroadcastExample"%go.
5454
55- Definition select_ready_case_no_panic {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_ready_case_no_panic"%go.
56-
57- Definition TestHelloWorldSync {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldSync"%go.
58-
59- Definition TestHelloWorldWithTimeout {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldWithTimeout"%go.
60-
61- Definition TestDSPExample {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestDSPExample"%go.
62-
63- Definition TestFibConsumer {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestFibConsumer"%go.
64-
65- Definition TestSelectNbNotReady {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectNbNotReady"%go.
66-
67- Definition TestSelectReadyCaseNoPanic {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectReadyCaseNoPanic"%go.
68-
6955Definition fibonacci {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fibonacci"%go.
7056
7157Definition fib_consumer {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fib_consumer"%go.
@@ -126,11 +112,7 @@ Definition select_nb_not_ready {ext : ffi_syntax} {go_gctx : GoGlobalContext} :
126112
127113Definition select_nb_guaranteed_ready {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_guaranteed_ready"%go.
128114
129- Definition select_nb_full_buffer_no_panic {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_full_buffer_no_panic"%go.
130-
131- Definition select_nb_buffer_space_panic {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_buffer_space_panic"%go.
132-
133- Definition select_nb_buffer_space_deadlock {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_buffer_space_deadlock"%go.
115+ Definition select_nb_full_buffer_not_ready {ext : ffi_syntax} {go_gctx : GoGlobalContext} : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_full_buffer_not_ready"%go.
134116
135117(* prog3 from Actris 2.0 intro: https://arxiv.org/pdf/2010.15030
136118
@@ -811,146 +793,6 @@ Definition BroadcastExampleⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalCon
811793 else do: #());;;
812794 return : #()).
813795
814- (* Show that a guaranteed to be ready case makes default impossible
815-
816- go: examples_unverified.go:6:6 *)
817- Definition select_ready_case_no_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
818- λ: <>,
819- exception_do (let : "ch" := (GoAlloc (go.ChannelType go.sendrecv (go.StructType [
820-
821- ])) (GoZeroVal (go.ChannelType go.sendrecv (go.StructType [
822-
823- ])) #())) in
824- let : "$r0" := ((FuncResolve go.make1 [go.ChannelType go.sendrecv (go.StructType [
825-
826- ])] #()) #()) in
827- do: ("ch" <-[go.ChannelType go.sendrecv (go.StructType [
828-
829- ])] "$r0");;;
830- do: (let: "$a0" := (![go.ChannelType go.sendrecv (go.StructType [
831-
832- ])] "ch") in
833- (FuncResolve go.close [go.ChannelType go.sendrecv (go.StructType [
834-
835- ])] #()) "$a0");;;
836- let : "$ch0" := (![go.ChannelType go.sendrecv (go.StructType [
837-
838- ])] "ch") in
839- SelectStmt (SelectStmtClauses (Some (do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"Shouldn't be possible!"%go) in
840- (FuncResolve go.panic [] #()) "$a0"))) [(CommClause (RecvCase (go.StructType [
841-
842- ]) "$ch0") (λ: "$recvVal",
843- do: #()
844- ))]);;;
845- return : #()).
846-
847- (* Various tests that should panic when failing, which also means verifying { True } e { True } is
848- sufficient since panic can't be verified.
849-
850- go: examples_unverified.go:20:6 *)
851- Definition TestHelloWorldSyncⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
852- λ: <>,
853- exception_do (let : "result" := (GoAlloc go.string (GoZeroVal go.string #())) in
854- let : "$r0" := ((FuncResolve HelloWorldSync [] #()) #()) in
855- do: ("result" <-[go.string] "$r0");;;
856- (if : Convert go.untyped_bool go.bool ((![go.string] "result") ≠⟨go.string⟩ #"Hello, World!"%go)
857- then
858- do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"incorrect output"%go) in
859- (FuncResolve go.panic [] #()) "$a0")
860- else do: #());;;
861- return : #()).
862-
863- (* go: examples_unverified.go:27:6 *)
864- Definition TestHelloWorldWithTimeoutⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
865- λ: <>,
866- exception_do (let : "result" := (GoAlloc go.string (GoZeroVal go.string #())) in
867- let : "$r0" := ((FuncResolve HelloWorldWithTimeout [] #()) #()) in
868- do: ("result" <-[go.string] "$r0");;;
869- (if : Convert go.untyped_bool go.bool (((![go.string] "result") ≠⟨go.string⟩ #"operation timed out"%go) && ((![go.string] "result") ≠⟨go.string⟩ #"Hello, World!"%go))
870- then
871- do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"incorrect output"%go) in
872- (FuncResolve go.panic [] #()) "$a0")
873- else do: #());;;
874- return : #()).
875-
876- (* go: examples_unverified.go:34:6 *)
877- Definition TestDSPExampleⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
878- λ: <>,
879- exception_do (let : "result" := (GoAlloc go.int (GoZeroVal go.int #())) in
880- let : "$r0" := ((FuncResolve DSPExample [] #()) #()) in
881- do: ("result" <-[go.int] "$r0");;;
882- (if : Convert go.untyped_bool go.bool ((![go.int] "result") ≠⟨go.int⟩ #(W64 42))
883- then
884- do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"incorrect output"%go) in
885- (FuncResolve go.panic [] #()) "$a0")
886- else do: #());;;
887- return : #()).
888-
889- (* go: examples_unverified.go:41:6 *)
890- Definition TestFibConsumerⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
891- λ: <>,
892- exception_do (let : "result" := (GoAlloc (go.SliceType go.int) (GoZeroVal (go.SliceType go.int) #())) in
893- let : "$r0" := ((FuncResolve fib_consumer [] #()) #()) in
894- do: ("result" <-[go.SliceType go.int] "$r0");;;
895- let : "expected" := (GoAlloc (go.SliceType go.int) (GoZeroVal (go.SliceType go.int) #())) in
896- let : "$r0" := (let : "$v0" := #(W64 0) in
897- let : "$v1" := #(W64 1) in
898- let : "$v2" := #(W64 1) in
899- let : "$v3" := #(W64 2) in
900- let : "$v4" := #(W64 3) in
901- let : "$v5" := #(W64 5) in
902- let : "$v6" := #(W64 8) in
903- let : "$v7" := #(W64 13) in
904- let : "$v8" := #(W64 21) in
905- let : "$v9" := #(W64 34) in
906- CompositeLiteral (go.SliceType go.int) (LiteralValue [KeyedElement None (ElementExpression go.int "$v0"); KeyedElement None (ElementExpression go.int "$v1"); KeyedElement None (ElementExpression go.int "$v2"); KeyedElement None (ElementExpression go.int "$v3"); KeyedElement None (ElementExpression go.int "$v4"); KeyedElement None (ElementExpression go.int "$v5"); KeyedElement None (ElementExpression go.int "$v6"); KeyedElement None (ElementExpression go.int "$v7"); KeyedElement None (ElementExpression go.int "$v8"); KeyedElement None (ElementExpression go.int "$v9")])) in
907- do: ("expected" <-[go.SliceType go.int] "$r0");;;
908- (if : Convert go.untyped_bool go.bool ((let : "$a0" := (![go.SliceType go.int] "result") in
909- (FuncResolve go.len [go.SliceType go.int] #()) "$a0") ≠⟨go.int⟩ (let : "$a0" := (![go.SliceType go.int] "expected") in
910- (FuncResolve go.len [go.SliceType go.int] #()) "$a0"))
911- then
912- do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"incorrect output"%go) in
913- (FuncResolve go.panic [] #()) "$a0")
914- else do: #());;;
915- let : "$range" := (![go.SliceType go.int] "expected") in
916- (let : "i" := (GoAlloc go.int (GoZeroVal go.int #())) in
917- slice.for_range go.int "$range" (λ: "$key" "$value",
918- do: ("i" <-[go.int] "$key");;;
919- (if : Convert go.untyped_bool go.bool ((![go.int] (IndexRef (go.SliceType go.int) (![go.SliceType go.int] "result", ![go.int] "i"))) ≠⟨go.int⟩ (![go.int] (IndexRef (go.SliceType go.int) (![go.SliceType go.int] "expected", ![go.int] "i"))))
920- then
921- do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"incorrect output"%go) in
922- (FuncResolve go.panic [] #()) "$a0")
923- else do: #())));;;
924- return : #()).
925-
926- (* go: examples_unverified.go:56:6 *)
927- Definition TestSelectNbNotReadyⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
928- λ: <>,
929- exception_do (let : "iterations" := (GoAlloc go.int (GoZeroVal go.int #())) in
930- let : "$r0" := #(W64 10000) in
931- do: ("iterations" <-[go.int] "$r0");;;
932- (let : "i" := (GoAlloc go.int (GoZeroVal go.int #())) in
933- let : "$r0" := #(W64 0) in
934- do: ("i" <-[go.int] "$r0");;;
935- (for : (λ: <>, (![go.int] "i") <⟨go.int⟩ (![go.int] "iterations")); (λ: <>, do: ("i" <-[go.int] ((![go.int] "i") +⟨go.int⟩ #(W64 1)))) := λ: <>,
936- do: ((FuncResolve select_nb_not_ready [] #()) #());;;
937- do: (let: "$a0" := (#(W64 1) *⟨time.Duration⟩ time.Microsecond) in
938- (FuncResolve time.Sleep [] #()) "$a0")));;;
939- return : #()).
940-
941- (* go: examples_unverified.go:65:6 *)
942- Definition TestSelectReadyCaseNoPanicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
943- λ: <>,
944- exception_do (let : "iterations" := (GoAlloc go.int (GoZeroVal go.int #())) in
945- let : "$r0" := #(W64 10000) in
946- do: ("iterations" <-[go.int] "$r0");;;
947- (let : "i" := (GoAlloc go.int (GoZeroVal go.int #())) in
948- let : "$r0" := #(W64 0) in
949- do: ("i" <-[go.int] "$r0");;;
950- (for : (λ: <>, (![go.int] "i") <⟨go.int⟩ (![go.int] "iterations")); (λ: <>, do: ("i" <-[go.int] ((![go.int] "i") +⟨go.int⟩ #(W64 1)))) := λ: <>,
951- do: ((FuncResolve select_ready_case_no_panic [] #()) #())));;;
952- return : #()).
953-
954796(* https://go.dev/tour/concurrency/4
955797
956798 go: fibonacci.go:4:6 *)
@@ -1610,7 +1452,7 @@ Definition CancellableMuxerⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalCon
16101452 return : (![go.string] (![go.PointerType go.string] "errMsg"))
16111453 ))]))).
16121454
1613- (* Show that it isn't possible to have 2 nonblocking ops that match.
1455+ (* Example with 2 nonblocking ops that should not match.
16141456
16151457 go: select_tricky_examples.go:4:6 *)
16161458Definition select_nb_not_readyⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
@@ -1666,11 +1508,10 @@ Definition select_nb_guaranteed_readyⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : G
16661508 ))]);;;
16671509 return : #()).
16681510
1669- (* Show that a nonblocking select does not take a send case
1670- when the buffered channel is already full.
1511+ (* Non-blocking send cannot send on a full buffer
16711512
1672- go: select_tricky_examples.go:33 :6 *)
1673- Definition select_nb_full_buffer_no_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
1513+ go: select_tricky_examples.go:34 :6 *)
1514+ Definition select_nb_full_buffer_not_readyⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
16741515 λ: <>,
16751516 exception_do (let : "ch" := (GoAlloc (go.ChannelType go.sendrecv go.int) (GoZeroVal (go.ChannelType go.sendrecv go.int) #())) in
16761517 let : "$r0" := ((FuncResolve go.make2 [go.ChannelType go.sendrecv go.int] #()) #(W64 1)) in
@@ -1684,37 +1525,6 @@ Definition select_nb_full_buffer_no_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx
16841525 (FuncResolve go.panic [] #()) "$a0")))]);;;
16851526 return : #()).
16861527
1687- (* Unverifiable: Panic is irreducible
1688-
1689- go: select_tricky_examples.go:52:6 *)
1690- Definition select_nb_buffer_space_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
1691- λ: <>,
1692- exception_do (let : "ch" := (GoAlloc (go.ChannelType go.sendrecv go.int) (GoZeroVal (go.ChannelType go.sendrecv go.int) #())) in
1693- let : "$r0" := ((FuncResolve go.make2 [go.ChannelType go.sendrecv go.int] #()) #(W64 1)) in
1694- do: ("ch" <-[go.ChannelType go.sendrecv go.int] "$r0");;;
1695- let : "$v0" := #(W64 0) in
1696- let : "$ch0" := (![go.ChannelType go.sendrecv go.int] "ch") in
1697- SelectStmt (SelectStmtClauses (Some (do: #())) [(CommClause (SendCase go.int "$ch0" "$v0") (do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"bad"%go) in
1698- (FuncResolve go.panic [] #()) "$a0")))]);;;
1699- return : #()).
1700-
1701- (* Blocking select: vacuously verifiable due to deadlock
1702-
1703- go: select_tricky_examples.go:67:6 *)
1704- Definition select_nb_buffer_space_deadlockⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
1705- λ: <>,
1706- exception_do (let : "ch" := (GoAlloc (go.ChannelType go.sendrecv go.int) (GoZeroVal (go.ChannelType go.sendrecv go.int) #())) in
1707- let : "$r0" := ((FuncResolve go.make2 [go.ChannelType go.sendrecv go.int] #()) #(W64 1)) in
1708- do: ("ch" <-[go.ChannelType go.sendrecv go.int] "$r0");;;
1709- do: (let: "$chan" := (![go.ChannelType go.sendrecv go.int] "ch") in
1710- let : "$v" := #(W64 0) in
1711- chan.send go.int "$chan" "$v");;;
1712- let : "$v0" := #(W64 0) in
1713- let : "$ch0" := (![go.ChannelType go.sendrecv go.int] "ch") in
1714- SelectStmt (SelectStmtClauses None [(CommClause (SendCase go.int "$ch0" "$v0") (do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"unreachable"%go) in
1715- (FuncResolve go.panic [] #()) "$a0")))]);;;
1716- return : #()).
1717-
17181528#[global] Instance info' : PkgInfo pkg_id.channel_examples :=
17191529{|
17201530 pkg_imported_pkgs := [code.time.pkg_id.time; code.github_com.goose_lang.goose.testdata.examples.channel.lock.pkg_id.lock; code.strings.pkg_id.strings]
@@ -1932,13 +1742,6 @@ Class Assumptions {ext : ffi_syntax} `{!GoGlobalContext} `{!GoLocalContext} `{!G
19321742 #[global] simple_multi_join_unfold :: FuncUnfold simple_multi_join [] (simple_multi_joinⁱᵐᵖˡ);
19331743 #[global] exchangePointer_unfold :: FuncUnfold exchangePointer [] (exchangePointerⁱᵐᵖˡ);
19341744 #[global] BroadcastExample_unfold :: FuncUnfold BroadcastExample [] (BroadcastExampleⁱᵐᵖˡ);
1935- #[global] select_ready_case_no_panic_unfold :: FuncUnfold select_ready_case_no_panic [] (select_ready_case_no_panicⁱᵐᵖˡ);
1936- #[global] TestHelloWorldSync_unfold :: FuncUnfold TestHelloWorldSync [] (TestHelloWorldSyncⁱᵐᵖˡ);
1937- #[global] TestHelloWorldWithTimeout_unfold :: FuncUnfold TestHelloWorldWithTimeout [] (TestHelloWorldWithTimeoutⁱᵐᵖˡ);
1938- #[global] TestDSPExample_unfold :: FuncUnfold TestDSPExample [] (TestDSPExampleⁱᵐᵖˡ);
1939- #[global] TestFibConsumer_unfold :: FuncUnfold TestFibConsumer [] (TestFibConsumerⁱᵐᵖˡ);
1940- #[global] TestSelectNbNotReady_unfold :: FuncUnfold TestSelectNbNotReady [] (TestSelectNbNotReadyⁱᵐᵖˡ);
1941- #[global] TestSelectReadyCaseNoPanic_unfold :: FuncUnfold TestSelectReadyCaseNoPanic [] (TestSelectReadyCaseNoPanicⁱᵐᵖˡ);
19421745 #[global] fibonacci_unfold :: FuncUnfold fibonacci [] (fibonacciⁱᵐᵖˡ);
19431746 #[global] fib_consumer_unfold :: FuncUnfold fib_consumer [] (fib_consumerⁱᵐᵖˡ);
19441747 #[global] Web_unfold :: FuncUnfold Web [] (Webⁱᵐᵖˡ);
@@ -1969,9 +1772,7 @@ Class Assumptions {ext : ffi_syntax} `{!GoGlobalContext} `{!GoLocalContext} `{!G
19691772 #[global] CancellableMuxer_unfold :: FuncUnfold CancellableMuxer [] (CancellableMuxerⁱᵐᵖˡ);
19701773 #[global] select_nb_not_ready_unfold :: FuncUnfold select_nb_not_ready [] (select_nb_not_readyⁱᵐᵖˡ);
19711774 #[global] select_nb_guaranteed_ready_unfold :: FuncUnfold select_nb_guaranteed_ready [] (select_nb_guaranteed_readyⁱᵐᵖˡ);
1972- #[global] select_nb_full_buffer_no_panic_unfold :: FuncUnfold select_nb_full_buffer_no_panic [] (select_nb_full_buffer_no_panicⁱᵐᵖˡ);
1973- #[global] select_nb_buffer_space_panic_unfold :: FuncUnfold select_nb_buffer_space_panic [] (select_nb_buffer_space_panicⁱᵐᵖˡ);
1974- #[global] select_nb_buffer_space_deadlock_unfold :: FuncUnfold select_nb_buffer_space_deadlock [] (select_nb_buffer_space_deadlockⁱᵐᵖˡ);
1775+ #[global] select_nb_full_buffer_not_ready_unfold :: FuncUnfold select_nb_full_buffer_not_ready [] (select_nb_full_buffer_not_readyⁱᵐᵖˡ);
19751776 #[global] import_time_Assumption :: time.Assumptions ;
19761777 #[global] import_lock_Assumption :: lock.Assumptions ;
19771778 #[global] import_strings_Assumption :: strings.Assumptions ;
0 commit comments