Skip to content

Commit 7b1a0bd

Browse files
ana-pantiliegithub-actionsMirceaSrv-jenkins
authored
kore-repl: improve exception handling (#2514)
* Handle WithConfiguration in kore-repl * Remove outdated UserInterrupt case * Handle exceptions at the top level as well * Clean-up: factor out handlers in kore-repl * Revert "Clean-up: factor out handlers in kore-repl" This reverts commit dc6867a. * Format with fourmolu * Reorder functions Co-authored-by: Octavian Mircea Sebe <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: Octavian Mircea Sebe <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 47bfdc7 commit 7b1a0bd

File tree

3 files changed

+113
-70
lines changed

3 files changed

+113
-70
lines changed

‎kore/app/repl/Main.hs

Lines changed: 91 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,12 @@
55
module Main (main) where
66

77
import Control.Concurrent.MVar
8+
import Control.Monad.Catch (
9+
SomeException,
10+
fromException,
11+
handle,
12+
throwM,
13+
)
814
import Data.Reflection
915
import GlobalMain
1016
import Kore.BugReport
@@ -16,21 +22,30 @@ import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools (
1622
)
1723
import Kore.Log (
1824
KoreLogOptions (..),
25+
SomeEntry (..),
26+
logEntry,
1927
runLoggerT,
2028
swappableLogger,
2129
withLogger,
2230
)
31+
import Kore.Log.ErrorException (
32+
errorException,
33+
)
2334
import Kore.Log.KoreLogOptions (
2435
parseKoreLogOptions,
2536
)
2637
import Kore.Log.WarnIfLowProductivity (
2738
warnIfLowProductivity,
2839
)
40+
import qualified Kore.Reachability.Claim as Claim
2941
import Kore.Repl.Data
3042
import Kore.Step.SMT.Lemma
3143
import Kore.Syntax.Module (
3244
ModuleName (..),
3345
)
46+
import Kore.Unparser (
47+
unparseToString,
48+
)
3449
import Options.Applicative (
3550
InfoMod,
3651
Parser,
@@ -198,62 +213,89 @@ mainWithOptions
198213
withLogger tempDirectory koreLogOptions $ \actualLogAction -> do
199214
mvarLogAction <- newMVar actualLogAction
200215
let swapLogAction = swappableLogger mvarLogAction
201-
flip runLoggerT swapLogAction $ do
202-
definition <- loadDefinitions [definitionFileName, specFile]
203-
indexedModule <- loadModule mainModuleName definition
204-
specDefIndexedModule <- loadModule specModule definition
216+
flip runLoggerT swapLogAction $
217+
runExceptionHandlers $ do
218+
definition <- loadDefinitions [definitionFileName, specFile]
219+
indexedModule <- loadModule mainModuleName definition
220+
specDefIndexedModule <- loadModule specModule definition
205221

206-
let smtConfig =
207-
SMT.defaultConfig
208-
{ SMT.timeOut = smtTimeOut
209-
, SMT.resetInterval = smtResetInterval
210-
, SMT.prelude = smtPrelude
211-
}
222+
let smtConfig =
223+
SMT.defaultConfig
224+
{ SMT.timeOut = smtTimeOut
225+
, SMT.resetInterval = smtResetInterval
226+
, SMT.prelude = smtPrelude
227+
}
212228

213-
when
214-
( replMode == RunScript
215-
&& isNothing (unReplScript replScript)
216-
)
217-
$ lift $ do
218-
hPutStrLn
219-
stderr
220-
"You must supply the path to the repl script\
221-
\ in order to run the repl in run-script mode."
222-
exitFailure
229+
when
230+
( replMode == RunScript
231+
&& isNothing (unReplScript replScript)
232+
)
233+
$ lift $ do
234+
hPutStrLn
235+
stderr
236+
"You must supply the path to the repl script\
237+
\ in order to run the repl in run-script mode."
238+
exitFailure
223239

224-
when
225-
( replMode == Interactive
226-
&& scriptModeOutput == EnableOutput
227-
)
228-
$ lift $ do
229-
hPutStrLn
230-
stderr
231-
"The --save-run-output flag is only available\
232-
\ when running the repl in run-script mode."
233-
exitFailure
240+
when
241+
( replMode == Interactive
242+
&& scriptModeOutput == EnableOutput
243+
)
244+
$ lift $ do
245+
hPutStrLn
246+
stderr
247+
"The --save-run-output flag is only available\
248+
\ when running the repl in run-script mode."
249+
exitFailure
234250

235-
SMT.runSMT
236-
smtConfig
237-
( give
238-
(MetadataTools.build indexedModule)
239-
(declareSMTLemmas indexedModule)
240-
)
241-
$ proveWithRepl
242-
indexedModule
243-
specDefIndexedModule
244-
Nothing
245-
mvarLogAction
246-
replScript
247-
replMode
248-
scriptModeOutput
249-
outputFile
250-
mainModuleName
251-
koreLogOptions
251+
SMT.runSMT
252+
smtConfig
253+
( give
254+
(MetadataTools.build indexedModule)
255+
(declareSMTLemmas indexedModule)
256+
)
257+
$ proveWithRepl
258+
indexedModule
259+
specDefIndexedModule
260+
Nothing
261+
mvarLogAction
262+
replScript
263+
replMode
264+
scriptModeOutput
265+
outputFile
266+
mainModuleName
267+
koreLogOptions
252268

253-
warnIfLowProductivity
254-
pure ExitSuccess
269+
warnIfLowProductivity
270+
pure ExitSuccess
255271
exitWith exitCode
256272
where
273+
runExceptionHandlers action =
274+
action
275+
& handle exitReplHandler
276+
& handle withConfigurationHandler
277+
& handle someExceptionHandler
278+
279+
exitReplHandler :: ExitCode -> Main ExitCode
280+
exitReplHandler = pure
281+
282+
withConfigurationHandler :: Claim.WithConfiguration -> Main ExitCode
283+
withConfigurationHandler
284+
(Claim.WithConfiguration lastConfiguration someException) =
285+
do
286+
liftIO $
287+
hPutStrLn
288+
stderr
289+
("// Last configuration:\n" <> unparseToString lastConfiguration)
290+
throwM someException
291+
292+
someExceptionHandler :: SomeException -> Main ExitCode
293+
someExceptionHandler someException = do
294+
case fromException someException of
295+
Just (SomeEntry entry) -> logEntry entry
296+
Nothing -> errorException someException
297+
throwM someException
298+
257299
mainModuleName :: ModuleName
258300
mainModuleName = moduleName definitionModule
259301

‎kore/src/Kore/Repl.hs

Lines changed: 21 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,6 @@ module Kore.Repl (
1212
) where
1313

1414
import Control.Concurrent.MVar
15-
import Control.Exception (
16-
AsyncException (UserInterrupt),
17-
fromException,
18-
)
1915
import qualified Control.Lens as Lens
2016
import Control.Monad (
2117
forever,
@@ -64,6 +60,7 @@ import Kore.Reachability (
6460
lensClaimPattern,
6561
)
6662
import Kore.Reachability.Claim
63+
import qualified Kore.Reachability.Claim as Claim
6764
import Kore.Reachability.Prove
6865
import Kore.Repl.Data
6966
import Kore.Repl.Interpreter
@@ -263,25 +260,29 @@ runRepl
263260
if Graph.outdeg (Strategy.graph graph) node == 0
264261
then
265262
proveClaimStep claims axioms graph node
266-
& catchInterruptWithDefault graph
267-
& catchEverything graph
263+
& Exception.handle (withConfigurationHandler graph)
264+
& Exception.handle (someExceptionHandler graph)
268265
else pure graph
269266

270-
catchInterruptWithDefault :: a -> m a -> m a
271-
catchInterruptWithDefault a =
272-
Exception.handle $ \case
273-
UserInterrupt -> do
274-
liftIO $ hPutStrLn stderr "Step evaluation interrupted."
275-
pure a
276-
e -> Exception.throwM e
267+
withConfigurationHandler :: a -> Claim.WithConfiguration -> m a
268+
withConfigurationHandler
269+
_
270+
(Claim.WithConfiguration lastConfiguration someException) =
271+
do
272+
liftIO $
273+
hPutStrLn
274+
stderr
275+
("// Last configuration:\n" <> unparseToString lastConfiguration)
276+
Exception.throwM someException
277277

278-
catchEverything :: a -> m a -> m a
279-
catchEverything a =
280-
Exception.handleAll $ \e -> do
281-
case fromException e of
282-
Just (Log.SomeEntry entry) -> Log.logEntry entry
283-
Nothing -> errorException e
284-
pure a
278+
someExceptionHandler :: a -> Exception.SomeException -> m a
279+
someExceptionHandler a someException = do
280+
case Exception.fromException someException of
281+
Just (Log.SomeEntry entry) ->
282+
Log.logEntry entry
283+
Nothing ->
284+
errorException someException
285+
pure a
285286

286287
replGreeting :: m ()
287288
replGreeting =

‎kore/src/Kore/Repl/Parser.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
{- |
44
Module : Kore.Repl.Parser
55
Description : REPL parser.
6-
Copyright : (c) Runtime Verification, 219
6+
Copyright : (c) Runtime Verification, 2019
77
License : NCSA
88
Maintainer : [email protected]
99
-}

0 commit comments

Comments
 (0)