0 | module System.Linux.SignalFD
  1 |
  2 | import Data.Bits
  3 | import Derive.Finite
  4 | import Derive.Prelude
  5 | import System.FFI
  6 | import System.Linux.Error
  7 | import System.Linux.File
  8 | import public System.Signal
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- FFI
 15 | --------------------------------------------------------------------------------
 16 |
 17 | %foreign "C:ep_sfd_cloexec,epoll-idris"
 18 | ep_sfd_cloexec : Bits32
 19 |
 20 | %foreign "C:ep_sfd_nonblock,epoll-idris"
 21 | ep_sfd_nonblock : Bits32
 22 |
 23 | %foreign "C:ep_allocSignalset,epoll-idris"
 24 | prim__allocSignalset : PrimIO AnyPtr
 25 |
 26 | %foreign "C:signalfd,epoll-idris"
 27 | prim__signalfd : Int32 -> AnyPtr -> Bits32 -> PrimIO Bits32
 28 |
 29 | %foreign "C:ep_readSignal,epoll-idris"
 30 | prim__ep_readSignal : Bits32 -> PrimIO Bits32
 31 |
 32 | %foreign "C:raise,epoll-idris"
 33 | prim__raise : Bits32 -> PrimIO ()
 34 |
 35 | %foreign "C:ep_sigblock,epoll-idris"
 36 | prim__sigblock : AnyPtr -> PrimIO ()
 37 |
 38 | %foreign "C:sigaddset,epoll-idris"
 39 | prim__sigaddset : AnyPtr -> Bits32 -> PrimIO ()
 40 |
 41 | --------------------------------------------------------------------------------
 42 | -- API
 43 | --------------------------------------------------------------------------------
 44 |
 45 | %runElab derive "PosixSignal" [Show,Finite]
 46 |
 47 | %runElab derive "Signal" [Show,Finite]
 48 |
 49 | ||| Flags describing the behavior of an signal file descriptor.
 50 | |||
 51 | ||| Several flags can be combined using `(<+>)`.
 52 | export
 53 | record Flags where
 54 |   constructor F
 55 |   value : Bits32
 56 |
 57 | %runElab derive "Flags" [Show,Eq,Ord]
 58 |
 59 | export %inline
 60 | flagCode : Flags -> Bits32
 61 | flagCode = value
 62 |
 63 | export %inline
 64 | Semigroup Flags where
 65 |   F x <+> F y = F (x .|. y)
 66 |
 67 | export %inline
 68 | Monoid Flags where neutral = F 0
 69 |
 70 | export %inline
 71 | SFD_CLOEXEC : Flags
 72 | SFD_CLOEXEC = F ep_sfd_cloexec
 73 |
 74 | ||| Sets the file descriptor to non-blocking: Reading from
 75 | ||| a `SignalFD` via `readSignal` will usually block the calling thread
 76 | ||| unless the file descriptor's signal has been caught.
 77 | |||
 78 | ||| With this flag being set, `readSignal` will never block but will return
 79 | ||| `Left EAGAIN` in case of a still running signal.
 80 | export %inline
 81 | SFD_NONBLOCK : Flags
 82 | SFD_NONBLOCK = F ep_sfd_nonblock
 83 |
 84 | ||| A signal file descriptor that can be monitored via `epoll`.
 85 | public export
 86 | record SignalFD where
 87 |   constructor SFD
 88 |   file : Bits32
 89 |
 90 | export %inline
 91 | FileDesc SignalFD where fileDesc = file
 92 |
 93 | addSignals : List Signal -> AnyPtr -> PrimIO ()
 94 | addSignals []        ptr w = MkIORes () w
 95 | addSignals (x :: xs) ptr w =
 96 |   let MkIORes _ w := prim__sigaddset ptr (cast $ signalCode x) w
 97 |    in addSignals xs ptr w
 98 |
 99 | ||| Creates a new `SignalFD`, observing the given signals
100 | ||| with the given flags set.
101 | |||
102 | ||| Note: Make sure to block the given list of signals to prevent their
103 | |||       default behavior. The easiest way to do so is by using
104 | |||       `blockSignals` at the beginning of your application.
105 | export
106 | signalCreate : List Signal -> Flags -> PrimIO SignalFD
107 | signalCreate ss (F f) w =
108 |  let MkIORes ptr  w := prim__allocSignalset w
109 |      MkIORes _    w := addSignals ss ptr w
110 |      MkIORes file w := prim__signalfd (-1) ptr f w
111 |      MkIORes _    w := toPrim (free ptr) w
112 |   in MkIORes (SFD file) w
113 |
114 | ||| Block default handling for the given list of signals.
115 | export
116 | blockSignals : List Signal -> PrimIO ()
117 | blockSignals ss w =
118 |  let MkIORes ptr  w := prim__allocSignalset w
119 |      MkIORes _    w := addSignals ss ptr w
120 |      MkIORes _    w := prim__sigblock ptr w
121 |   in toPrim (free ptr) w
122 |
123 | ||| Reads the next caught signal from a signal file descriptor.
124 | export
125 | readSignal : SignalFD -> PrimIO (Either EpollErr Bits32)
126 | readSignal (SFD f) w =
127 |   let MkIORes v w := prim__ep_readSignal f w
128 |    in case v of
129 |         0 => getErr w
130 |         n => MkIORes (Right n) w
131 |
132 | ||| Creates and finally closes and event file descriptor.
133 | export
134 | withSignal : List Signal -> Flags -> (SignalFD -> PrimIO a) -> PrimIO a
135 | withSignal ss fs f w =
136 |   let MkIORes tf  w := signalCreate ss fs w
137 |       MkIORes res w := f tf w
138 |       MkIORes _   w := close tf w
139 |    in MkIORes res w
140 |
141 | export %inline
142 | raise : Signal -> PrimIO ()
143 | raise s = prim__raise (cast $ signalCode s)
144 |