Skip to content

Commit a28bc65

Browse files
fabianhjrabaillygallaisRussoul
authored
Fix deadlocks [Rebased, Squashed] (#1536)
Co-authored-by: Arnaud Bailly <[email protected]> Co-authored-by: Guillaume Allais <[email protected]> Co-authored-by: Fabián Heredia Montiel <[email protected]> Co-authored-by: Ruslan Feizerakhmanov <[email protected]>
1 parent 7692de6 commit a28bc65

File tree

13 files changed

+225
-76
lines changed

13 files changed

+225
-76
lines changed

.github/workflows/ci-ubuntu-combined.yml

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,9 @@ jobs:
3131
uses: actions/checkout@v2
3232
- name: Install build dependencies
3333
run: |
34-
sudo apt-get install -y chezscheme
34+
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
35+
sudo apt-get update
36+
sudo apt-get install -y -t hirsute chezscheme
3537
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
3638
- name: Build from bootstrap
3739
run: make bootstrap && make install
@@ -71,14 +73,16 @@ jobs:
7173
uses: actions/checkout@v2
7274
- name: Install build dependencies
7375
run: |
74-
sudo apt-get install -y chezscheme
76+
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
77+
sudo apt-get update
78+
sudo apt-get install -y -t hirsute chezscheme
7579
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
7680
- name: Cache Chez Previous Version
7781
id: previous-version-cache
7882
uses: actions/cache@v2
7983
with:
8084
path: Idris2-${{ env.IDRIS2_VERSION }}
81-
key: ${{ runner.os }}-idris2-bootstrapped-${{ env.IDRIS2_VERSION }}
85+
key: ${{ runner.os }}-idris2-bootstrapped-hirsute-chez-${{ env.IDRIS2_VERSION }}
8286
- name : Build previous version
8387
if: steps.previous-version-cache.outputs.cache-hit != 'true'
8488
run: |
@@ -118,7 +122,9 @@ jobs:
118122
path: ~/.idris2/
119123
- name: Install build dependencies
120124
run: |
121-
sudo apt-get install -y chezscheme
125+
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
126+
sudo apt-get update
127+
sudo apt-get install -y -t hirsute chezscheme
122128
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
123129
chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
124130
- name: Build self-hosted
@@ -166,7 +172,9 @@ jobs:
166172
path: ~/.idris2/
167173
- name: Install build dependencies
168174
run: |
169-
sudo apt-get install -y chezscheme
175+
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
176+
sudo apt-get update
177+
sudo apt-get install -y -t hirsute chezscheme
170178
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
171179
chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
172180
- name: Build from previous version
@@ -197,7 +205,9 @@ jobs:
197205
path: ~/.idris2/
198206
- name: Install build dependencies
199207
run: |
200-
sudo apt-get install -y chezscheme
208+
echo "deb http://security.ubuntu.com/ubuntu hirsute universe" | sudo tee -a /etc/apt/sources.list
209+
sudo apt-get update
210+
sudo apt-get install -y -t hirsute chezscheme
201211
echo "$HOME/.idris2/bin" >> $GITHUB_PATH
202212
chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
203213
- name: Build API

idris2api.ipkg

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -132,6 +132,7 @@ modules =
132132
Libraries.Data.String.Iterator,
133133
Libraries.Data.StringMap,
134134
Libraries.Data.StringTrie,
135+
Libraries.Data.Version,
135136

136137
Libraries.System.Directory.Tree,
137138

libs/network/Network/FFI.idr

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,8 @@ prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int
5757
export
5858
prim__idrnet_create_sockaddr : PrimIO AnyPtr
5959

60-
%foreign "C:idrnet_accept, libidris2_support, idris_net.h"
60+
%foreign "C__collect_safe:idrnet_accept, libidris2_support, idris_net.h"
61+
"C:idrnet_accept, libidris2_support, idris_net.h"
6162
export
6263
prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int
6364

@@ -70,11 +71,13 @@ export
7071
prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int
7172

7273

73-
%foreign "C:idrnet_recv, libidris2_support, idris_net.h"
74+
%foreign "C__collect_safe:idrnet_recv, libidris2_support, idris_net.h"
75+
"C:idrnet_recv, libidris2_support, idris_net.h"
7476
export
7577
prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
7678

77-
%foreign "C:idrnet_recv_buf, libidris2_support, idris_net.h"
79+
%foreign "C__collect_safe:idrnet_recv_buf, libidris2_support, idris_net.h"
80+
"C:idrnet_recv_buf, libidris2_support, idris_net.h"
7881
export
7982
prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int
8083

@@ -89,11 +92,13 @@ prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
8992
(buf_len : Int) -> (host : String) -> (port : Port) ->
9093
(family : Int) -> PrimIO Int
9194

92-
%foreign "C:idrnet_recvfrom, libidris2_support, idris_net.h"
95+
%foreign "C__collect_safe:idrnet_recvfrom, libidris2_support, idris_net.h"
96+
"C:idrnet_recvfrom, libidris2_support, idris_net.h"
9397
export
9498
prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
9599

96-
%foreign "C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
100+
%foreign "C__collect_safe:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
101+
"C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
97102
export
98103
prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr
99104

src/Compiler/Scheme/Chez.idr

Lines changed: 60 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import Data.List
1818
import Data.List1
1919
import Data.Maybe
2020
import Libraries.Data.NameMap
21+
import Libraries.Data.Version
2122
import Data.Strings
2223
import Data.Vect
2324

@@ -38,6 +39,28 @@ findChez
3839
path <- pathLookup ["chez", "chezscheme9.5", "scheme"]
3940
pure $ fromMaybe "/usr/bin/env scheme" path
4041

42+
||| Returns the chez scheme version for given executable
43+
|||
44+
||| This uses `chez --version` which unfortunately writes the version
45+
||| on `stderr` thus requiring suffixing the command which shell redirection
46+
||| which does not seem very portable.
47+
export
48+
chezVersion : String -> IO (Maybe Version)
49+
chezVersion chez = do
50+
Right fh <- popen cmd Read
51+
| Left err => pure Nothing
52+
Right output <- fGetLine fh
53+
| Left err => pure Nothing
54+
pclose fh
55+
pure $ parseVersion output
56+
where
57+
cmd : String
58+
cmd = chez ++ " --version 2>&1"
59+
60+
unsupportedCallingConvention : Maybe Version -> Bool
61+
unsupportedCallingConvention Nothing = True
62+
unsupportedCallingConvention (Just version) = version < MkVersion (9,5,0) Nothing
63+
4164
-- Given the chez compiler directives, return a list of pairs of:
4265
-- - the library file name
4366
-- - the full absolute path of the library file name, if it's in one
@@ -197,19 +220,25 @@ cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
197220
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
198221
" to foreign function"))
199222

200-
cCall : {auto c : Ref Ctxt Defs} ->
201-
{auto l : Ref Loaded (List String)} ->
202-
String -> FC -> (cfn : String) -> (clib : String) ->
203-
List (Name, CFType) -> CFType -> Core (String, String)
204-
cCall appdir fc cfn clib args (CFIORes CFGCPtr)
223+
cCall : {auto c : Ref Ctxt Defs}
224+
-> {auto l : Ref Loaded (List String)}
225+
-> String
226+
-> FC
227+
-> (cfn : String)
228+
-> (clib : String)
229+
-> List (Name, CFType)
230+
-> CFType
231+
-> (collectSafe : Bool)
232+
-> Core (String, String)
233+
cCall appdir fc cfn clib args (CFIORes CFGCPtr) _
205234
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
206-
cCall appdir fc cfn clib args CFGCPtr
235+
cCall appdir fc cfn clib args CFGCPtr _
207236
= throw (GenericMsg fc "Can't return GCPtr from a foreign function")
208-
cCall appdir fc cfn clib args (CFIORes CFBuffer)
237+
cCall appdir fc cfn clib args (CFIORes CFBuffer) _
209238
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
210-
cCall appdir fc cfn clib args CFBuffer
239+
cCall appdir fc cfn clib args CFBuffer _
211240
= throw (GenericMsg fc "Can't return Buffer from a foreign function")
212-
cCall appdir fc cfn clib args ret
241+
cCall appdir fc cfn clib args ret collectSafe
213242
= do loaded <- get Loaded
214243
lib <- if clib `elem` loaded
215244
then pure ""
@@ -221,7 +250,8 @@ cCall appdir fc cfn clib args ret
221250
++ "\")\n"
222251
argTypes <- traverse (\a => cftySpec fc (snd a)) args
223252
retType <- cftySpec fc ret
224-
let call = "((foreign-procedure #f " ++ show cfn ++ " ("
253+
let callConv = if collectSafe then " __collect_safe" else ""
254+
let call = "((foreign-procedure" ++ callConv ++ " " ++ show cfn ++ " ("
225255
++ showSep " " argTypes ++ ") " ++ retType ++ ") "
226256
++ showSep " " !(traverse buildArg args) ++ ")"
227257

@@ -282,19 +312,23 @@ schemeCall fc sfn argns ret
282312
-- function call.
283313
useCC : {auto c : Ref Ctxt Defs} ->
284314
{auto l : Ref Loaded (List String)} ->
285-
String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
286-
useCC appdir fc ccs args ret
287-
= case parseCC ["scheme,chez", "scheme", "C"] ccs of
288-
Nothing => throw (NoForeignCC fc)
315+
String -> FC -> List String -> List (Name, CFType) -> CFType ->
316+
Maybe Version -> Core (String, String)
317+
useCC appdir fc ccs args ret version
318+
= case parseCC ["scheme,chez", "scheme", "C__collect_safe", "C"] ccs of
289319
Just ("scheme,chez", [sfn]) =>
290320
do body <- schemeCall fc sfn (map fst args) ret
291321
pure ("", body)
292322
Just ("scheme", [sfn]) =>
293323
do body <- schemeCall fc sfn (map fst args) ret
294324
pure ("", body)
295-
Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret
296-
Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret
297-
_ => throw (NoForeignCC fc)
325+
Just ("C__collect_safe", (cfn :: clib :: _)) => do
326+
if unsupportedCallingConvention version
327+
then cCall appdir fc cfn clib args ret False
328+
else cCall appdir fc cfn clib args ret True
329+
Just ("C", (cfn :: clib :: _)) =>
330+
cCall appdir fc cfn clib args ret False
331+
_ => throw (NoForeignCC fc ccs)
298332

299333
-- For every foreign arg type, return a name, and whether to pass it to the
300334
-- foreign call (we don't pass '%World')
@@ -323,28 +357,28 @@ mkStruct _ = pure ""
323357
schFgnDef : {auto c : Ref Ctxt Defs} ->
324358
{auto l : Ref Loaded (List String)} ->
325359
{auto s : Ref Structs (List String)} ->
326-
String -> FC -> Name -> NamedDef -> Core (String, String)
327-
schFgnDef appdir fc n (MkNmForeign cs args ret)
360+
String -> FC -> Name -> NamedDef -> Maybe Version -> Core (String, String)
361+
schFgnDef appdir fc n (MkNmForeign cs args ret) version
328362
= do let argns = mkArgs 0 args
329363
let allargns = map fst argns
330364
let useargns = map fst (filter snd argns)
331365
argStrs <- traverse mkStruct args
332366
retStr <- mkStruct ret
333-
(load, body) <- useCC appdir fc cs (zip useargns args) ret
367+
(load, body) <- useCC appdir fc cs (zip useargns args) ret version
334368
defs <- get Ctxt
335369
pure (load,
336370
concat argStrs ++ retStr ++
337371
"(define " ++ schName !(full (gamma defs) n) ++
338372
" (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
339373
body ++ "))\n")
340-
schFgnDef _ _ _ _ = pure ("", "")
374+
schFgnDef _ _ _ _ _ = pure ("", "")
341375

342376
export
343377
getFgnCall : {auto c : Ref Ctxt Defs} ->
344378
{auto l : Ref Loaded (List String)} ->
345379
{auto s : Ref Structs (List String)} ->
346-
String -> (Name, FC, NamedDef) -> Core (String, String)
347-
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d
380+
String -> Maybe Version -> (Name, FC, NamedDef) -> Core (String, String)
381+
getFgnCall appdir version (n, fc, d) = schFgnDef appdir fc n d version
348382

349383
export
350384
startChezPreamble : String
@@ -401,11 +435,12 @@ compileToSS c prof appdir tm outfile
401435
defs <- get Ctxt
402436
l <- newRef {t = List String} Loaded ["libc", "libc 6"]
403437
s <- newRef {t = List String} Structs []
404-
fgndefs <- traverse (getFgnCall appdir) ndefs
438+
chez <- coreLift findChez
439+
version <- coreLift $ chezVersion chez
440+
fgndefs <- traverse (getFgnCall appdir version) ndefs
405441
compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
406442
let code = fastAppend (map snd fgndefs ++ compdefs)
407443
main <- schExp chezExtPrim chezString 0 ctm
408-
chez <- coreLift findChez
409444
support <- readDataFile "chez/support.ss"
410445
extraRuntime <- getExtraRuntime ds
411446
let scm = schHeader chez (map snd libs) ++

src/Compiler/Scheme/ChezSep.idr

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ import Data.List
2222
import Data.List1
2323
import Data.Maybe
2424
import Libraries.Data.NameMap
25+
import Libraries.Data.Version
2526
import Data.Strings
2627
import Data.Vect
2728

@@ -150,6 +151,7 @@ compileToSS c chez appdir tm = do
150151
ds <- getDirectives Chez
151152
libs <- findLibs ds
152153
traverse_ copyLib libs
154+
version <- coreLift $ chezVersion chez
153155

154156
-- get the material for compilation
155157
cdata <- getCompileData False Cases tm
@@ -213,7 +215,7 @@ compileToSS c chez appdir tm = do
213215
++ " (import (chezscheme) (support) " ++ imports ++ ")\n\n"
214216
let footer = ")"
215217

216-
fgndefs <- traverse (Chez.getFgnCall appdir) cu.definitions
218+
fgndefs <- traverse (Chez.getFgnCall appdir version) cu.definitions
217219
compdefs <- traverse (getScheme Chez.chezExtPrim Chez.chezString) cu.definitions
218220

219221
-- write the files

src/Compiler/Scheme/Gambit.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -307,12 +307,12 @@ useCC : {auto c : Ref Ctxt Defs} ->
307307
FC -> List String -> List (Name, CFType) -> CFType -> Core (Maybe String, (String, String))
308308
useCC fc ccs args ret
309309
= case parseCC ["scheme,gambit", "scheme", "C"] ccs of
310-
Nothing => throw (NoForeignCC fc)
310+
Nothing => throw (NoForeignCC fc ccs)
311311
Just ("scheme,gambit", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
312312
Just ("scheme", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
313313
Just ("C", [cfn, clib]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
314314
Just ("C", [cfn, clib, chdr]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
315-
_ => throw (NoForeignCC fc)
315+
_ => throw (NoForeignCC fc ccs)
316316
where
317317
fnWrapName : String -> String -> String
318318
fnWrapName cfn schemeArgName = schemeArgName ++ "-" ++ cfn ++ "-cFunWrap"

src/Compiler/Scheme/Racket.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -267,7 +267,7 @@ useCC : {auto f : Ref Done (List String) } ->
267267
String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
268268
useCC appdir fc ccs args ret
269269
= case parseCC ["scheme,racket", "scheme", "C"] ccs of
270-
Nothing => throw (NoForeignCC fc)
270+
Nothing => throw (NoForeignCC fc ccs)
271271
Just ("scheme,racket", [sfn]) =>
272272
do body <- schemeCall fc sfn (map fst args) ret
273273
pure ("", body)
@@ -276,7 +276,7 @@ useCC appdir fc ccs args ret
276276
pure ("", body)
277277
Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret
278278
Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret
279-
_ => throw (NoForeignCC fc)
279+
_ => throw (NoForeignCC fc ccs)
280280

281281
-- For every foreign arg type, return a name, and whether to pass it to the
282282
-- foreign call (we don't pass '%World')

src/Core/Core.idr

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,8 @@ data Error : Type where
154154
ForceNeeded : Error
155155
InternalError : String -> Error
156156
UserError : String -> Error
157-
NoForeignCC : FC -> Error
157+
||| Contains list of specifiers for which foreign call cannot be resolved
158+
NoForeignCC : FC -> List String -> Error
158159
BadMultiline : FC -> String -> Error
159160

160161
InType : FC -> Name -> Error -> Error
@@ -328,8 +329,8 @@ Show Error where
328329
show ForceNeeded = "Internal error when resolving implicit laziness"
329330
show (InternalError str) = "INTERNAL ERROR: " ++ str
330331
show (UserError str) = "Error: " ++ str
331-
show (NoForeignCC fc) = show fc ++
332-
":The given specifier was not accepted by any available backend."
332+
show (NoForeignCC fc specs) = show fc ++
333+
":The given specifier " ++ show specs ++ " was not accepted by any available backend."
333334
show (BadMultiline fc str) = "Invalid multiline string: " ++ str
334335

335336
show (InType fc n err)
@@ -420,7 +421,7 @@ getErrorLoc (CyclicImports _) = Nothing
420421
getErrorLoc ForceNeeded = Nothing
421422
getErrorLoc (InternalError _) = Nothing
422423
getErrorLoc (UserError _) = Nothing
423-
getErrorLoc (NoForeignCC loc) = Just loc
424+
getErrorLoc (NoForeignCC loc _) = Just loc
424425
getErrorLoc (BadMultiline loc _) = Just loc
425426
getErrorLoc (InType _ _ err) = getErrorLoc err
426427
getErrorLoc (InCon _ _ err) = getErrorLoc err

src/Idris/CommandLine.idr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -358,7 +358,7 @@ envsUsage = makeTextFromOptionsOrEnvs $ map (\e => (e.name, Just e.help)) envs
358358

359359
export
360360
versionMsg : String
361-
versionMsg = "Idris 2, version " ++ showVersion True version
361+
versionMsg = "Idris 2, version " ++ show version
362362

363363
export
364364
usage : String

src/Idris/Error.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -459,9 +459,9 @@ perror (CyclicImports ns)
459459
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
460460
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
461461
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str
462-
perror (NoForeignCC fc) = do
462+
perror (NoForeignCC fc specs) = do
463463
let cgs = fst <$> availableCGs (options !(get Ctxt))
464-
let res = vsep [ errorDesc (reflow "The given specifier was not accepted by any backend. Available backends" <+> colon)
464+
let res = vsep [ errorDesc (reflow ("The given specifier '" ++ show specs ++ "' was not accepted by any backend. Available backends") <+> colon)
465465
, indent 2 (concatWith (\ x, y => x <+> ", " <+> y) (map reflow cgs))
466466
, reflow "Some backends have additional specifier rules, refer to their documentation."
467467
] <+> line <+> !(ploc fc)

0 commit comments

Comments
 (0)