0 | ||| Signal raising and handling.
  1 | |||
  2 | ||| NOTE that there are important differences between
  3 | ||| what can be done out-of-box in Windows and POSIX based
  4 | ||| operating systems. This module tries to honor both
  5 | ||| by putting things only available in POSIX environments
  6 | ||| into appropriately named namespaces or data types.
  7 | module System.Signal
  8 |
  9 | import Data.Fuel
 10 | import Data.List
 11 | import System.Errno
 12 |
 13 | %default total
 14 |
 15 | signalFFI : String -> String
 16 | signalFFI fn = "C:" ++ fn ++ ", libidris2_support, idris_signal.h"
 17 |
 18 | signalFFINode : String -> String
 19 | signalFFINode fn = "node:support:" ++ fn ++ ",support_system_signal"
 20 |
 21 | --
 22 | -- Signals
 23 | --
 24 | %foreign signalFFI "sighup"
 25 |          signalFFINode "sighup"
 26 | prim__sighup : Int
 27 |
 28 | %foreign signalFFI "sigint"
 29 |          signalFFINode "sigint"
 30 | prim__sigint : Int
 31 |
 32 | %foreign signalFFI "sigabrt"
 33 |          signalFFINode "sigabrt"
 34 | prim__sigabrt : Int
 35 |
 36 | %foreign signalFFI "sigquit"
 37 |          signalFFINode "sigquit"
 38 | prim__sigquit : Int
 39 |
 40 | %foreign signalFFI "sigill"
 41 |          signalFFINode "sigill"
 42 | prim__sigill : Int
 43 |
 44 | %foreign signalFFI "sigsegv"
 45 |          signalFFINode "sigsegv"
 46 | prim__sigsegv : Int
 47 |
 48 | %foreign signalFFI "sigtrap"
 49 |          signalFFINode "sigtrap"
 50 | prim__sigtrap : Int
 51 |
 52 | %foreign signalFFI "sigfpe"
 53 |          signalFFINode "sigfpe"
 54 | prim__sigfpe : Int
 55 |
 56 | %foreign signalFFI "sigusr1"
 57 |          signalFFINode "sigusr1"
 58 | prim__sigusr1 : Int
 59 |
 60 | %foreign signalFFI "sigusr2"
 61 |          signalFFINode "sigusr2"
 62 | prim__sigusr2 : Int
 63 |
 64 | public export
 65 | data PosixSignal = ||| Hangup (i.e. controlling terminal closed)
 66 |                    SigHUP
 67 |                  | ||| Quit
 68 |                    SigQUIT
 69 |                  | ||| Trap (as used by debuggers)
 70 |                    SigTRAP
 71 |                  | SigUser1
 72 |                  | SigUser2
 73 |
 74 | export
 75 | Eq PosixSignal where
 76 |   SigHUP   == SigHUP   = True
 77 |   SigQUIT  == SigQUIT  = True
 78 |   SigTRAP  == SigTRAP  = True
 79 |   SigUser1 == SigUser1 = True
 80 |   SigUser2 == SigUser2 = True
 81 |   _ == _ = False
 82 |
 83 | public export
 84 | data Signal = ||| Interrupt (e.g. ctrl+c pressed)
 85 |               SigINT
 86 |             | ||| Abnormal termination
 87 |               SigABRT
 88 |             | ||| Ill-formed instruction
 89 |               SigILL
 90 |             | ||| Segmentation fault
 91 |               SigSEGV
 92 |             | ||| Floating-point error
 93 |               SigFPE
 94 |             | ||| Signals only available on POSIX operating systems
 95 |               SigPosix PosixSignal
 96 |
 97 | export
 98 | Eq Signal where
 99 |   SigINT   == SigINT   = True
100 |   SigABRT  == SigABRT  = True
101 |   SigILL   == SigILL   = True
102 |   SigSEGV  == SigSEGV  = True
103 |   SigFPE   == SigFPE   = True
104 |   SigPosix x == SigPosix y = x == y
105 |   _ == _ = False
106 |
107 | ||| Converts a `Signal` to its integer representation to be used
108 | ||| in FFI calls.
109 | export
110 | signalCode : Signal -> Int
111 | signalCode SigINT   = prim__sigint
112 | signalCode SigABRT  = prim__sigabrt
113 | signalCode SigILL   = prim__sigill
114 | signalCode SigSEGV  = prim__sigsegv
115 | signalCode SigFPE   = prim__sigfpe
116 | signalCode (SigPosix SigHUP  ) = prim__sighup
117 | signalCode (SigPosix SigQUIT ) = prim__sigquit
118 | signalCode (SigPosix SigTRAP ) = prim__sigtrap
119 | signalCode (SigPosix SigUser1) = prim__sigusr1
120 | signalCode (SigPosix SigUser2) = prim__sigusr2
121 |
122 | ||| Tries to convert an integer to the corresponding `Signal`.
123 | export
124 | toSignal : Int -> Maybe Signal
125 | toSignal (-1) = Nothing
126 | toSignal x    = lookup x codes
127 |   where
128 |     codes : List (Int, Signal)
129 |     codes = [
130 |               (prim__sigint , SigINT)
131 |             , (prim__sigabrt, SigABRT)
132 |             , (prim__sigill , SigILL)
133 |             , (prim__sigsegv, SigSEGV)
134 |             , (prim__sigfpe , SigFPE)
135 |             , (prim__sighup , SigPosix SigHUP)
136 |             , (prim__sigquit, SigPosix SigQUIT)
137 |             , (prim__sigtrap, SigPosix SigTRAP)
138 |             , (prim__sigusr1, SigPosix SigUser1)
139 |             , (prim__sigusr2, SigPosix SigUser2)
140 |             ]
141 |
142 | --
143 | -- Signal Handling
144 | --
145 | %foreign signalFFI "ignore_signal"
146 |          signalFFINode "ignoreSignal"
147 | prim__ignoreSignal : Int -> PrimIO Int
148 |
149 | %foreign signalFFI "default_signal"
150 |          signalFFINode "defaultSignal"
151 | prim__defaultSignal : Int -> PrimIO Int
152 |
153 | %foreign signalFFI "collect_signal"
154 |          signalFFINode "collectSignal"
155 | prim__collectSignal : Int -> PrimIO Int
156 |
157 | %foreign signalFFI "handle_next_collected_signal"
158 |          signalFFINode "handleNextCollectedSignal"
159 | prim__handleNextCollectedSignal : PrimIO Int
160 |
161 | %foreign signalFFI "send_signal"
162 |          signalFFINode "sendSignal"
163 | prim__sendSignal : Int -> Int -> PrimIO Int
164 |
165 | %foreign signalFFI "raise_signal"
166 |          signalFFINode "raiseSignal"
167 | prim__raiseSignal : Int -> PrimIO Int
168 |
169 | ||| An Error represented by a code. See
170 | ||| relevant `errno` documentation.
171 | ||| https://man7.org/linux/man-pages/man3/errno.3.html
172 | public export
173 | data SignalError = Error Int
174 |
175 | getError : HasIO io => io SignalError
176 | getError = Error <$> getErrno
177 |
178 | isError : Int -> Bool
179 | isError (-1) = True
180 | isError _    = False
181 |
182 | ||| Ignore the given signal.
183 | ||| Be careful doing this, as most signals have useful
184 | ||| default behavior -- you might want to set the signal
185 | ||| to its default behavior instead with `defaultSignal`.
186 | export
187 | ignoreSignal : HasIO io => Signal -> io (Either SignalError ())
188 | ignoreSignal sig = do
189 |   res <- primIO $ prim__ignoreSignal (signalCode sig)
190 |   case isError res of
191 |        False => pure $ Right ()
192 |        True  => Left <$> getError
193 |
194 | ||| Use the default handler for the given signal.
195 | ||| You can use this function to unset custom
196 | ||| handling of a signal.
197 | export
198 | defaultSignal : HasIO io => Signal -> io (Either SignalError ())
199 | defaultSignal sig = do
200 |   res <- primIO $ prim__defaultSignal (signalCode sig)
201 |   case isError res of
202 |        False => pure $ Right ()
203 |        True  => Left <$> getError
204 |
205 | ||| Collect the given signal.
206 | |||
207 | ||| This replaces the existing handling of the given signal
208 | ||| and instead results in Idris collecting occurrences of
209 | ||| the signal until you call `handleNextCollectedSignal`.
210 | |||
211 | ||| First, call `collectSignal` for any number of signals.
212 | ||| Then, call `handleNextCollectedSignal` in each main loop
213 | ||| of your program to retrieve (and mark as handled) the next
214 | ||| signal that was collected, if any.
215 | |||
216 | ||| Signals are not queued, so the return order of signals is
217 | ||| not specified and signals may be deduplicated.
218 | export
219 | collectSignal : HasIO io => Signal -> io (Either SignalError ())
220 | collectSignal sig = do
221 |   res <- primIO $ prim__collectSignal (signalCode sig)
222 |   case isError res of
223 |        False => pure $ Right ()
224 |        True  => Left <$> getError
225 |
226 | ||| Get next collected signal under the pretense of handling it.
227 | |||
228 | ||| Calling this "marks" the signal as handled so the next time
229 | ||| this function is called you will retrieve the next unhandled
230 | ||| signal instead of the same signal again.
231 | |||
232 | ||| You get back Nothing if there are no pending signals.
233 | export
234 | handleNextCollectedSignal : HasIO io => io (Maybe Signal)
235 | handleNextCollectedSignal =
236 |   toSignal <$> primIO prim__handleNextCollectedSignal
237 |
238 | ||| Get many collected signals and mark them as handled.
239 | |||
240 | ||| Use `forever` as your fuel if you don't want or need to
241 | ||| retain totality. Alternatively, pick a max number to
242 | ||| retrieve and use `limit/1` as your fuel.
243 | export
244 | handleManyCollectedSignals : HasIO io => Fuel -> io (List Signal)
245 | handleManyCollectedSignals Dry = pure []
246 | handleManyCollectedSignals (More fuel) = do
247 |   Just next <- handleNextCollectedSignal
248 |     | Nothing => pure []
249 |   pure $ next :: !(handleManyCollectedSignals fuel)
250 |
251 | ||| Send a signal to the current process.
252 | export
253 | raiseSignal : HasIO io => Signal -> io (Either SignalError ())
254 | raiseSignal sig = do
255 |   res <- primIO $ prim__raiseSignal (signalCode sig)
256 |   case isError res of
257 |        False => pure $ Right ()
258 |        True  => Left <$> getError
259 |
260 | namespace Posix
261 |   ||| Send a signal to a POSIX process using a PID to identify the process.
262 |   export
263 |   sendSignal : HasIO io => Signal -> (pid : Int) -> io (Either SignalError ())
264 |   sendSignal sig pid = do
265 |     res <- primIO $ prim__sendSignal pid (signalCode sig)
266 |     case isError res of
267 |          False => pure $ Right ()
268 |          True  => Left <$> getError
269 |