@@ -391,11 +391,15 @@ Definition Cond__WaitForⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContex
391391 ])] "done") in
392392 SelectStmt (SelectStmtClauses None [(CommClause (RecvCase (go.StructType [
393393
394- ]) "$ch0") (let : "$r0" := #true in
395- do: ("signaled" <-[go.bool] "$r0"))); (CommClause (RecvCase (go.StructType [
396-
397- ]) "$ch1") (let : "$r0" := #false in
398- do: ("signaled" <-[go.bool] "$r0")))]);;;
394+ ]) "$ch0") (λ: "$recvVal",
395+ let : "$r0" := #true in
396+ do: ("signaled" <-[go.bool] "$r0")
397+ )); (CommClause (RecvCase (go.StructType [
398+
399+ ]) "$ch1") (λ: "$recvVal",
400+ let : "$r0" := #false in
401+ do: ("signaled" <-[go.bool] "$r0")
402+ ))]);;;
399403 do: ((MethodResolve (go.PointerType Lock) "Lock"%go (![go.PointerType Lock] (StructFieldRef Cond "L"%go (![go.PointerType Cond] "c")))) #());;;
400404 (if : (⟨go.bool⟩! (![go.bool] "signaled"))
401405 then
@@ -404,7 +408,9 @@ Definition Cond__WaitForⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContex
404408 ])] "ch") in
405409 SelectStmt (SelectStmtClauses (Some (do: #())) [(CommClause (RecvCase (go.StructType [
406410
407- ]) "$ch0") (return : (#true)))]);;;
411+ ]) "$ch0") (λ: "$recvVal",
412+ return : (#true)
413+ ))]);;;
408414 let : "$range" := (![go.SliceType (go.ChannelType go.sendrecv (go.StructType [
409415
410416 ]))] (StructFieldRef Cond "waiters"%go (![go.PointerType Cond] "c"))) in
@@ -541,7 +547,9 @@ Definition EliminationStack__Pushⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlo
541547 let : "$ch0" := (![go.ChannelType go.sendrecv go.string] (StructFieldRef EliminationStack "exchanger"%go (![go.PointerType EliminationStack] "s"))) in
542548 let : "$ch1" := (let : "$a0" := timeout in
543549 (FuncResolve time.After [] #()) "$a0") in
544- SelectStmt (SelectStmtClauses None [(CommClause (SendCase go.string "$ch0" "$v0") (return : (#()))); (CommClause (RecvCase time.Time "$ch1") (do: #()))]);;;
550+ SelectStmt (SelectStmtClauses None [(CommClause (SendCase go.string "$ch0" "$v0") (return : (#()))); (CommClause (RecvCase time.Time "$ch1") (λ: "$recvVal",
551+ do: #()
552+ ))]);;;
545553 do: (let: "$a0" := (![go.string] "value") in
546554 (MethodResolve (go.PointerType LockedStack) "Push"%go (![go.PointerType LockedStack] (StructFieldRef EliminationStack "base"%go (![go.PointerType EliminationStack] "s")))) "$a0");;;
547555 return : #()).
@@ -555,10 +563,14 @@ Definition EliminationStack__Popⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlob
555563 let : "$ch0" := (![go.ChannelType go.sendrecv go.string] (StructFieldRef EliminationStack "exchanger"%go (![go.PointerType EliminationStack] "s"))) in
556564 let : "$ch1" := (let : "$a0" := timeout in
557565 (FuncResolve time.After [] #()) "$a0") in
558- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (let : "v" := (GoAlloc go.string (GoZeroVal go.string #())) in
559- let : "$r0" := (Fst "$recvVal") in
560- do: ("v" <-[go.string] "$r0");;;
561- return : (![go.string] "v", #true))); (CommClause (RecvCase time.Time "$ch1") (do: #()))]);;;
566+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (λ: "$recvVal",
567+ let : "v" := (GoAlloc go.string (GoZeroVal go.string #())) in
568+ let : "$r0" := (Fst "$recvVal") in
569+ do: ("v" <-[go.string] "$r0");;;
570+ return : (![go.string] "v", #true)
571+ )); (CommClause (RecvCase time.Time "$ch1") (λ: "$recvVal",
572+ do: #()
573+ ))]);;;
562574 let : ("$ret0", "$ret1") := (((MethodResolve (go.PointerType LockedStack) "Pop"%go (![go.PointerType LockedStack] (StructFieldRef EliminationStack "base"%go (![go.PointerType EliminationStack] "s")))) #())) in
563575 return : ("$ret0", "$ret1")).
564576
@@ -605,12 +617,16 @@ Definition HelloWorldCancellableⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlob
605617 let : "$ch1" := (![go.ChannelType go.sendrecv (go.StructType [
606618
607619 ])] "done") in
608- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (let : "resolved" := (GoAlloc go.string (GoZeroVal go.string #())) in
609- let : "$r0" := (Fst "$recvVal") in
610- do: ("resolved" <-[go.string] "$r0");;;
611- return : (![go.string] "resolved"))); (CommClause (RecvCase (go.StructType [
620+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (λ: "$recvVal",
621+ let : "resolved" := (GoAlloc go.string (GoZeroVal go.string #())) in
622+ let : "$r0" := (Fst "$recvVal") in
623+ do: ("resolved" <-[go.string] "$r0");;;
624+ return : (![go.string] "resolved")
625+ )); (CommClause (RecvCase (go.StructType [
612626
613- ]) "$ch1") (return : (![go.string] (![go.PointerType go.string] "err"))))])).
627+ ]) "$ch1") (λ: "$recvVal",
628+ return : (![go.string] (![go.PointerType go.string] "err"))
629+ ))])).
614630
615631(* Uses cancellation as a timeout mechanism.
616632
@@ -860,8 +876,10 @@ Definition select_nb_no_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalC
860876 ])] "ch") in
861877 SelectStmt (SelectStmtClauses (Some (do: #())) [(CommClause (RecvCase (go.StructType [
862878
863- ]) "$ch0") (do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"bad"%go) in
864- (FuncResolve go.panic [] #()) "$a0")))]);;;
879+ ]) "$ch0") (λ: "$recvVal",
880+ do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"bad"%go) in
881+ (FuncResolve go.panic [] #()) "$a0")
882+ ))]);;;
865883 return : #())
866884 ) in
867885 do: (Fork ("$go" #()));;;
@@ -887,7 +905,9 @@ Definition select_no_double_closeⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlo
887905 (FuncResolve go.close [go.ChannelType go.sendrecv go.int] #()) "$a0");;;
888906 let : "$ch0" := (![go.ChannelType go.sendrecv go.int] "x") in
889907 SelectStmt (SelectStmtClauses (Some (do: (let: "$a0" := (![go.ChannelType go.sendrecv go.int] "x") in
890- (FuncResolve go.close [go.ChannelType go.sendrecv go.int] #()) "$a0"))) [(CommClause (RecvCase go.int "$ch0") (do: #()))]);;;
908+ (FuncResolve go.close [go.ChannelType go.sendrecv go.int] #()) "$a0"))) [(CommClause (RecvCase go.int "$ch0") (λ: "$recvVal",
909+ do: #()
910+ ))]);;;
891911 return : #()).
892912
893913(* Show that a nonblocking select does not take a send case
@@ -1166,7 +1186,9 @@ Definition select_ready_case_no_panicⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : G
11661186 SelectStmt (SelectStmtClauses (Some (do: (let: "$a0" := (Convert go.string (go.InterfaceType []) #"Shouldn't be possible!"%go) in
11671187 (FuncResolve go.panic [] #()) "$a0"))) [(CommClause (RecvCase (go.StructType [
11681188
1169- ]) "$ch0") (do: #()))]);;;
1189+ ]) "$ch0") (λ: "$recvVal",
1190+ do: #()
1191+ ))]);;;
11701192 return : #()).
11711193
11721194(* Various tests that should panic when failing, which also means verifying { True } e { True } is
@@ -1327,35 +1349,45 @@ Definition CancellableHedgedRequestⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoG
13271349 let : "$ch2" := (![go.ChannelType go.recvonly (go.StructType [
13281350
13291351 ])] "done") in
1330- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase Result "$ch0") (let : "r" := (GoAlloc Result (GoZeroVal Result #())) in
1331- let : "$r0" := (Fst "$recvVal") in
1332- do: ("r" <-[Result] "$r0");;;
1333- return : (![Result] "r"))); (CommClause (RecvCase time.Time "$ch1") (let : "$go" := (λ: <>,
1334- exception_do (do: (let: "$chan" := (![go.ChannelType go.sendrecv Result] "c") in
1335- let : "$v" := (let: "$v0" := (let: "$a0" := (![go.string] "query") in
1336- (FuncResolve GetSecondary [] #()) "$a0") in
1337- let : "$v1" := #false in
1338- CompositeLiteral Result (LiteralValue [KeyedElement None (ElementExpression go.string "$v0"); KeyedElement None (ElementExpression go.bool "$v1")])) in
1339- chan.send Result "$chan" "$v");;;
1340- return : #())
1341- ) in
1342- do: (Fork ("$go" #())))); (CommClause (RecvCase (go.StructType [
1343-
1344- ]) "$ch2") (let : "$r0" := #"cancelled"%go in
1345- do: ((![go.PointerType go.string] "errStr") <-[go.string] "$r0");;;
1346- return : (CompositeLiteral Result (LiteralValue []))))]);;;
1352+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase Result "$ch0") (λ: "$recvVal",
1353+ let : "r" := (GoAlloc Result (GoZeroVal Result #())) in
1354+ let : "$r0" := (Fst "$recvVal") in
1355+ do: ("r" <-[Result] "$r0");;;
1356+ return : (![Result] "r")
1357+ )); (CommClause (RecvCase time.Time "$ch1") (λ: "$recvVal",
1358+ let : "$go" := (λ: <>,
1359+ exception_do (do: (let: "$chan" := (![go.ChannelType go.sendrecv Result] "c") in
1360+ let : "$v" := (let: "$v0" := (let: "$a0" := (![go.string] "query") in
1361+ (FuncResolve GetSecondary [] #()) "$a0") in
1362+ let : "$v1" := #false in
1363+ CompositeLiteral Result (LiteralValue [KeyedElement None (ElementExpression go.string "$v0"); KeyedElement None (ElementExpression go.bool "$v1")])) in
1364+ chan.send Result "$chan" "$v");;;
1365+ return : #())
1366+ ) in
1367+ do: (Fork ("$go" #()))
1368+ )); (CommClause (RecvCase (go.StructType [
1369+
1370+ ]) "$ch2") (λ: "$recvVal",
1371+ let : "$r0" := #"cancelled"%go in
1372+ do: ((![go.PointerType go.string] "errStr") <-[go.string] "$r0");;;
1373+ return : (CompositeLiteral Result (LiteralValue []))
1374+ ))]);;;
13471375 let : "$ch0" := (![go.ChannelType go.sendrecv Result] "c") in
13481376 let : "$ch1" := (![go.ChannelType go.recvonly (go.StructType [
13491377
13501378 ])] "done") in
1351- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase Result "$ch0") (let : "r" := (GoAlloc Result (GoZeroVal Result #())) in
1352- let : "$r0" := (Fst "$recvVal") in
1353- do: ("r" <-[Result] "$r0");;;
1354- return : (![Result] "r"))); (CommClause (RecvCase (go.StructType [
1355-
1356- ]) "$ch1") (let : "$r0" := #"cancelled"%go in
1357- do: ((![go.PointerType go.string] "errStr") <-[go.string] "$r0");;;
1358- return : (CompositeLiteral Result (LiteralValue []))))])).
1379+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase Result "$ch0") (λ: "$recvVal",
1380+ let : "r" := (GoAlloc Result (GoZeroVal Result #())) in
1381+ let : "$r0" := (Fst "$recvVal") in
1382+ do: ("r" <-[Result] "$r0");;;
1383+ return : (![Result] "r")
1384+ )); (CommClause (RecvCase (go.StructType [
1385+
1386+ ]) "$ch1") (λ: "$recvVal",
1387+ let : "$r0" := #"cancelled"%go in
1388+ do: ((![go.PointerType go.string] "errStr") <-[go.string] "$r0");;;
1389+ return : (CompositeLiteral Result (LiteralValue []))
1390+ ))])).
13591391
13601392(* go: higher_order.go:8:6 *)
13611393Definition mkRequestⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
@@ -1462,9 +1494,11 @@ Definition clientⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : va
14621494 let : "$ch0" := (![go.ChannelType go.sendrecv (go.SliceType go.byte)] "freeList") in
14631495 SelectStmt (SelectStmtClauses (Some (let : "$r0" := (let : "$v0" := #(W8 0) in
14641496 CompositeLiteral (go.SliceType go.byte) (LiteralValue [KeyedElement None (ElementExpression go.byte "$v0")])) in
1465- do: ("b" <-[go.SliceType go.byte] "$r0"))) [(CommClause (RecvCase (go.SliceType go.byte) "$ch0") (let : "$r0" := (Fst "$recvVal") in
1466- do: ("b" <-[go.SliceType go.byte] "$r0");;;
1467- do: #()))]);;;
1497+ do: ("b" <-[go.SliceType go.byte] "$r0"))) [(CommClause (RecvCase (go.SliceType go.byte) "$ch0") (λ: "$recvVal",
1498+ let : "$r0" := (Fst "$recvVal") in
1499+ do: ("b" <-[go.SliceType go.byte] "$r0");;;
1500+ do: #()
1501+ ))]);;;
14681502 do: (let : "$a0" := "b" in
14691503 let : "$a1" := (![go.string] "letter") in
14701504 (FuncResolve load [] #()) "$a0" "$a1");;;
@@ -1655,7 +1689,9 @@ Definition Lock__LockIfNotCancelledⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoG
16551689
16561690 ]) "$ch0" "$v0") (return : (#true))); (CommClause (RecvCase (go.StructType [
16571691
1658- ]) "$ch1") (return : (#false)))])).
1692+ ]) "$ch1") (λ: "$recvVal",
1693+ return : (#false)
1694+ ))])).
16591695
16601696(* LockWithTimeout attempts to acquire the lock, timing out after d.
16611697 Returns true if acquired, false if timed out.
@@ -1879,22 +1915,26 @@ Definition CancellableMapServerⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGloba
18791915 let : "$ch1" := (![go.ChannelType go.sendrecv (go.StructType [
18801916
18811917 ])] "done") in
1882- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (let : "ok" := (GoAlloc go.bool (GoZeroVal go.bool #())) in
1883- let : "in" := (GoAlloc go.string (GoZeroVal go.string #())) in
1884- let : ("$ret0", "$ret1") := "$recvVal" in
1885- let : "$r0" := "$ret0" in
1886- let : "$r1" := "$ret1" in
1887- do: ("in" <-[go.string] "$r0");;;
1888- do: ("ok" <-[go.bool] "$r1");;;
1889- (if : (⟨go.bool⟩! (![go.bool] "ok"))
1890- then return : (#())
1891- else do: #());;;
1892- do: (let: "$chan" := (![go.ChannelType go.sendrecv go.string] (StructFieldRef streamold "res"%go "s")) in
1893- let : "$v" := (let: "$a0" := (![go.string] "in ") in
1894- (![go.FunctionType (go.Signature [go.string] false [go.string])] (StructFieldRef streamold "f"%go "s")) "$a0") in
1895- chan.send go.string "$chan" "$v"))); (CommClause (RecvCase (go.StructType [
1896-
1897- ]) "$ch1") (return : (#())))]));;;
1918+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase go.string "$ch0") (λ: "$recvVal",
1919+ let : "ok" := (GoAlloc go.bool (GoZeroVal go.bool #())) in
1920+ let : "in" := (GoAlloc go.string (GoZeroVal go.string #())) in
1921+ let : ("$ret0", "$ret1") := "$recvVal" in
1922+ let : "$r0" := "$ret0" in
1923+ let : "$r1" := "$ret1" in
1924+ do: ("in" <-[go.string] "$r0");;;
1925+ do: ("ok" <-[go.bool] "$r1");;;
1926+ (if : (⟨go.bool⟩! (![go.bool] "ok"))
1927+ then return : (#())
1928+ else do: #());;;
1929+ do: (let: "$chan" := (![go.ChannelType go.sendrecv go.string] (StructFieldRef streamold "res"%go "s")) in
1930+ let : "$v" := (let: "$a0" := (![go.string] "in ") in
1931+ (![go.FunctionType (go.Signature [go.string] false [go.string])] (StructFieldRef streamold "f"%go "s")) "$a0") in
1932+ chan.send go.string "$chan" "$v")
1933+ )); (CommClause (RecvCase (go.StructType [
1934+
1935+ ]) "$ch1") (λ: "$recvVal",
1936+ return : (#())
1937+ ))]));;;
18981938 return : #()).
18991939
19001940(* 4. CancellableMuxer - muxer with cancellation
@@ -1912,24 +1952,28 @@ Definition CancellableMuxerⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalCon
19121952 let : "$ch1" := (![go.ChannelType go.sendrecv (go.StructType [
19131953
19141954 ])] "done") in
1915- SelectStmt (SelectStmtClauses None [(CommClause (RecvCase streamold "$ch0") (let : "ok" := (GoAlloc go.bool (GoZeroVal go.bool #())) in
1916- let : "s" := (GoAlloc streamold (GoZeroVal streamold #())) in
1917- let : ("$ret0", "$ret1") := "$recvVal" in
1918- let : "$r0" := "$ret0" in
1919- let : "$r1" := "$ret1" in
1920- do: ("s" <-[streamold] "$r0");;;
1921- do: ("ok" <-[go.bool] "$r1");;;
1922- (if : (⟨go.bool⟩! (![go.bool] "ok"))
1923- then return : (#"serviced all requests"%go)
1924- else do: #());;;
1925- let : "$a0" := (![streamold] "s") in
1926- let : "$a1" := (![go.ChannelType go.sendrecv (go.StructType [
1955+ SelectStmt (SelectStmtClauses None [(CommClause (RecvCase streamold "$ch0") (λ: "$recvVal",
1956+ let : "ok" := (GoAlloc go.bool (GoZeroVal go.bool #())) in
1957+ let : "s" := (GoAlloc streamold (GoZeroVal streamold #())) in
1958+ let : ("$ret0", "$ret1") := "$recvVal" in
1959+ let : "$r0" := "$ret0" in
1960+ let : "$r1" := "$ret1" in
1961+ do: ("s" <-[streamold] "$r0");;;
1962+ do: ("ok" <-[go.bool] "$r1");;;
1963+ (if : (⟨go.bool⟩! (![go.bool] "ok"))
1964+ then return : (#"serviced all requests"%go)
1965+ else do: #());;;
1966+ let : "$a0" := (![streamold] "s") in
1967+ let : "$a1" := (![go.ChannelType go.sendrecv (go.StructType [
19271968
1928- ])] "done") in
1929- let : "$go" := (FuncResolve CancellableMapServer [] #()) in
1930- do: (Fork ("$go" "$a0" "$a1")))); (CommClause (RecvCase (go.StructType [
1969+ ])] "done") in
1970+ let : "$go" := (FuncResolve CancellableMapServer [] #()) in
1971+ do: (Fork ("$go" "$a0" "$a1"))
1972+ )); (CommClause (RecvCase (go.StructType [
19311973
1932- ]) "$ch1") (return : (![go.string] (![go.PointerType go.string] "errMsg"))))]))).
1974+ ]) "$ch1") (λ: "$recvVal",
1975+ return : (![go.string] (![go.PointerType go.string] "errMsg"))
1976+ ))]))).
19331977
19341978(* go: parallel_search_replace.go:13:6 *)
19351979Definition workerⁱᵐᵖˡ {ext : ffi_syntax} {go_gctx : GoGlobalContext} : val :=
0 commit comments