mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-11 08:37:35 +03:00
Merge branch 'server-interrupts' into HEAD
This commit is contained in:
Adam C. Foltzer
commit
f87ea62646
@ -14,25 +14,31 @@
|
||||
{-# LANGUAGE ExtendedDefaultRules #-}
|
||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# OPTIONS_GHC -Wall -fno-warn-type-defaults #-}
|
||||
module Main where
|
||||
|
||||
import Control.Concurrent
|
||||
import Control.Monad
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Monad.Trans.Control
|
||||
import qualified Control.Exception as X
|
||||
import Data.Aeson
|
||||
import Data.Aeson.Encode.Pretty
|
||||
import qualified Data.ByteString.Char8 as BS
|
||||
import qualified Data.ByteString.Lazy.Char8 as BSL
|
||||
import Data.Char
|
||||
import Data.IORef
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import Data.Word
|
||||
import Options.Applicative
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
import System.FilePath
|
||||
import System.Posix.Signals
|
||||
import System.ZMQ4
|
||||
import Text.Read
|
||||
|
||||
@ -108,6 +114,7 @@ data RResult
|
||||
| RRUnknownCmd Text
|
||||
| RRBadMessage BS.ByteString String
|
||||
| RROk
|
||||
| RRInterrupted
|
||||
|
||||
instance ToJSON RResult where
|
||||
toJSON = \case
|
||||
@ -135,31 +142,48 @@ instance ToJSON RResult where
|
||||
[ "tag" .= "unknownCommand", "command" .= txt ]
|
||||
RRBadMessage msg err -> object
|
||||
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
|
||||
RROk -> object [ "tag" .= "ok" ]
|
||||
RROk -> object
|
||||
[ "tag" .= "ok" ]
|
||||
RRInterrupted -> object
|
||||
[ "tag" .= "interrupted" ]
|
||||
|
||||
data ControlMsg
|
||||
= CMConnect
|
||||
-- ^ Request a new Cryptol context and connection
|
||||
| CMInterrupt Word16
|
||||
-- ^ Request an interrupt of all current Cryptol contexts
|
||||
| CMExit
|
||||
-- ^ Request that the entire server shut down
|
||||
| CMUnknown Text
|
||||
-- ^ Unknown message
|
||||
|
||||
instance FromJSON ControlMsg where
|
||||
parseJSON = withObject "ControlMsg" $ \o -> do
|
||||
tag <- o .: "tag"
|
||||
flip (withText "tag") tag $ \case
|
||||
"connect" -> return CMConnect
|
||||
"interrupt" -> CMInterrupt <$> o .: "port"
|
||||
"exit" -> return CMExit
|
||||
other -> return $ CMUnknown other
|
||||
|
||||
data ControlReply
|
||||
= CRConnect Word16
|
||||
| CROk
|
||||
-- ^ Return the port for a new connection
|
||||
| CRInterrupted
|
||||
-- ^ Acknowledge receipt of an interrupt command
|
||||
| CRExiting
|
||||
-- ^ Acknowledge receipt of an exit command
|
||||
| CRBadMessage BS.ByteString String
|
||||
-- ^ Acknowledge receipt of an ill-formed control message
|
||||
|
||||
instance ToJSON ControlReply where
|
||||
toJSON = \case
|
||||
CRConnect port -> object
|
||||
[ "tag" .= "connect", "port" .= port ]
|
||||
CROk -> object [ "tag" .= "ok" ]
|
||||
CRInterrupted -> object
|
||||
[ "tag" .= "interrupted" ]
|
||||
CRExiting -> object
|
||||
[ "tag" .= "exiting" ]
|
||||
CRBadMessage msg err -> object
|
||||
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
|
||||
|
||||
@ -170,6 +194,7 @@ server port =
|
||||
let addr = "tcp://127.0.0.1:" ++ show port
|
||||
putStrLn ("[cryptol-server] coming online at " ++ addr)
|
||||
bind rep addr
|
||||
workers <- newIORef Map.empty
|
||||
let loop = do
|
||||
msg <- receive rep
|
||||
putStrLn "[cryptol-server] received message:"
|
||||
@ -184,12 +209,21 @@ server port =
|
||||
bind newRep "tcp://127.0.0.1:*"
|
||||
newAddr <- lastEndpoint newRep
|
||||
let portStr = reverse . takeWhile isDigit . reverse $ newAddr
|
||||
workerPort = read portStr
|
||||
putStrLn ("[cryptol-server] starting worker on interface " ++ newAddr)
|
||||
void . forkIO $ runRepl newRep
|
||||
reply rep $ CRConnect (read portStr)
|
||||
tid <- forkFinally (runRepl newRep) (removeWorker workers port)
|
||||
addNewWorker workers workerPort tid
|
||||
reply rep $ CRConnect workerPort
|
||||
Right (CMInterrupt port') -> do
|
||||
s <- readIORef workers
|
||||
case Map.lookup port' s of
|
||||
Nothing -> reply rep $ CRBadMessage msg "invalid worker port"
|
||||
Just tid -> do
|
||||
throwTo tid X.UserInterrupt
|
||||
reply rep $ CRInterrupted
|
||||
Right CMExit -> do
|
||||
putStrLn "[cryptol-server] shutting down"
|
||||
reply rep $ CROk
|
||||
reply rep $ CRExiting
|
||||
exitSuccess
|
||||
Right (CMUnknown cmd) -> do
|
||||
putStrLn ("[cryptol-server] unknown control command: " ++ T.unpack cmd)
|
||||
@ -204,6 +238,14 @@ reply rep msg = liftIO $ do
|
||||
BS.putStrLn bmsg
|
||||
send rep [] bmsg
|
||||
|
||||
addNewWorker :: IORef (Map Word16 ThreadId) -> Word16 -> ThreadId -> IO ()
|
||||
addNewWorker workers port tid =
|
||||
atomicModifyIORef workers $ \s -> (Map.insert port tid s, ())
|
||||
|
||||
removeWorker :: IORef (Map Word16 ThreadId) -> Word16 -> a -> IO ()
|
||||
removeWorker workers port _result =
|
||||
atomicModifyIORef workers $ \s -> (Map.delete port s, ())
|
||||
|
||||
runRepl :: Socket Rep -> IO ()
|
||||
runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
|
||||
@ -218,7 +260,9 @@ runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
#endif
|
||||
funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
|
||||
let handle err = reply rep (RRInteractiveError err (show (pp err)))
|
||||
loop = do
|
||||
handleAsync :: X.AsyncException -> IO ()
|
||||
handleAsync _int = reply rep RRInterrupted
|
||||
loop = liftBaseWith $ \run -> X.handle handleAsync $ run $ do
|
||||
msg <- io $ receive rep
|
||||
io $ putStrLn "[cryptol-worker] received message:"
|
||||
case decodeStrict msg of
|
||||
@ -313,13 +357,29 @@ withCapturedOutput m = do
|
||||
setPutStr old
|
||||
return (x, s)
|
||||
|
||||
data Server = Server { serverPort :: Word16
|
||||
, serverMaskSIGINT :: Bool }
|
||||
deriving Show
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
args <- getArgs
|
||||
case args of
|
||||
[] -> server 5555
|
||||
[portStr] ->
|
||||
case readMaybe portStr of
|
||||
Just port -> server port
|
||||
Nothing -> server 5555
|
||||
_ -> error "port is the only allowed argument"
|
||||
main = execParser opts >>= mainWith
|
||||
where
|
||||
opts =
|
||||
info (helper <*> serverOpts)
|
||||
( fullDesc
|
||||
<> progDesc "Run Cryptol as a server via ZeroMQ and JSON"
|
||||
<> header "cryptol-server" )
|
||||
serverOpts =
|
||||
Server
|
||||
<$> option auto
|
||||
( long "port"
|
||||
<> short 'p'
|
||||
<> metavar "PORT"
|
||||
<> value 5555
|
||||
<> help "TCP port to bind" )
|
||||
<*> switch
|
||||
( long "mask-interrupts"
|
||||
<> help "Suppress interrupt signals" )
|
||||
mainWith Server {..} = do
|
||||
when serverMaskSIGINT $ void $ installHandler sigINT Ignore Nothing
|
||||
server serverPort
|
||||
|
||||
@ -40,35 +40,37 @@ flag server
|
||||
library
|
||||
Default-language:
|
||||
Haskell98
|
||||
Build-depends: base >= 4.7 && < 5,
|
||||
base-compat >= 0.6,
|
||||
array >= 0.4,
|
||||
async >= 2.0,
|
||||
containers >= 0.5,
|
||||
deepseq >= 1.3,
|
||||
deepseq-generics >= 0.1,
|
||||
directory >= 1.2,
|
||||
filepath >= 1.3,
|
||||
gitrev >= 1.0,
|
||||
generic-trie >= 0.3.0.1,
|
||||
GraphSCC >= 1.0.4,
|
||||
heredoc >= 0.2,
|
||||
monadLib >= 3.7.2,
|
||||
old-time >= 1.1,
|
||||
presburger >= 1.3,
|
||||
pretty >= 1.1,
|
||||
process >= 1.2,
|
||||
QuickCheck >= 2.7,
|
||||
random >= 1.0.1,
|
||||
sbv >= 5.6,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.6.0,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
Build-depends: base >= 4.7 && < 5,
|
||||
base-compat >= 0.6,
|
||||
array >= 0.4,
|
||||
async >= 2.0,
|
||||
containers >= 0.5,
|
||||
deepseq >= 1.3,
|
||||
deepseq-generics >= 0.1,
|
||||
directory >= 1.2,
|
||||
filepath >= 1.3,
|
||||
gitrev >= 1.0,
|
||||
generic-trie >= 0.3.0.1,
|
||||
GraphSCC >= 1.0.4,
|
||||
heredoc >= 0.2,
|
||||
monad-control >= 1.0,
|
||||
monadLib >= 3.7.2,
|
||||
old-time >= 1.1,
|
||||
presburger >= 1.3,
|
||||
pretty >= 1.1,
|
||||
process >= 1.2,
|
||||
QuickCheck >= 2.7,
|
||||
random >= 1.0.1,
|
||||
sbv >= 5.6,
|
||||
smtLib >= 1.0.7,
|
||||
simple-smt >= 0.6.0,
|
||||
syb >= 0.4,
|
||||
text >= 1.1,
|
||||
template-haskell,
|
||||
tf-random >= 0.5,
|
||||
transformers >= 0.3,
|
||||
utf8-string >= 0.3
|
||||
tf-random >= 0.5,
|
||||
transformers >= 0.3,
|
||||
transformers-base >= 0.4,
|
||||
utf8-string >= 0.3
|
||||
|
||||
Build-tools: alex, happy
|
||||
hs-source-dirs: src
|
||||
@ -192,6 +194,7 @@ executable cryptol
|
||||
, filepath
|
||||
, haskeline
|
||||
, monadLib
|
||||
, monad-control
|
||||
, process
|
||||
, random
|
||||
, sbv
|
||||
@ -214,18 +217,21 @@ executable cryptol-server
|
||||
if os(linux) && flag(static)
|
||||
ld-options: -static -pthread
|
||||
if flag(server)
|
||||
build-depends: aeson >= 0.10
|
||||
, aeson-pretty >= 0.7
|
||||
, base
|
||||
, base-compat
|
||||
, bytestring >= 0.10
|
||||
, containers
|
||||
, cryptol
|
||||
, filepath
|
||||
, text
|
||||
, transformers
|
||||
, unordered-containers >= 0.2
|
||||
, zeromq4-haskell >= 0.6
|
||||
build-depends: aeson >= 0.10
|
||||
, aeson-pretty >= 0.7
|
||||
, base
|
||||
, base-compat
|
||||
, bytestring >= 0.10
|
||||
, containers
|
||||
, cryptol
|
||||
, filepath
|
||||
, monad-control
|
||||
, optparse-applicative
|
||||
, text
|
||||
, transformers
|
||||
, unix
|
||||
, unordered-containers >= 0.2
|
||||
, zeromq4-haskell >= 0.6
|
||||
else
|
||||
buildable: False
|
||||
|
||||
|
||||
@ -18,8 +18,9 @@ import Cryptol.REPL.Trie
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (guard, when)
|
||||
import Control.Monad (guard, join, when)
|
||||
import qualified Control.Monad.Trans.Class as MTL
|
||||
import Control.Monad.Trans.Control
|
||||
import Data.Char (isAlphaNum, isSpace)
|
||||
import Data.Function (on)
|
||||
import Data.List (isPrefixOf,nub,sortBy)
|
||||
@ -30,6 +31,9 @@ import System.Directory ( doesFileExist
|
||||
, getCurrentDirectory)
|
||||
import System.FilePath ((</>))
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
-- | Haskeline-specific repl implementation.
|
||||
repl :: Cryptolrc -> Maybe FilePath -> REPL () -> IO ()
|
||||
repl cryrc mbBatch begin =
|
||||
@ -133,11 +137,8 @@ data Cryptolrc =
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
instance MonadException REPL where
|
||||
controlIO branchIO = REPL $ \ ref -> do
|
||||
runBody <- branchIO $ RunIO $ \ m -> do
|
||||
a <- unREPL m ref
|
||||
return (return a)
|
||||
unREPL runBody ref
|
||||
controlIO f = join $ liftBaseWith $ \f' ->
|
||||
f $ RunIO $ \m -> restoreM <$> (f' m)
|
||||
|
||||
-- Titles ----------------------------------------------------------------------
|
||||
|
||||
|
||||
@ -6,10 +6,12 @@
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE DeriveDataTypeable #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
module Cryptol.REPL.Monad (
|
||||
@ -86,7 +88,9 @@ import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))
|
||||
|
||||
import Control.Monad (ap,unless,when)
|
||||
import Control.Monad.Base
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Monad.Trans.Control
|
||||
import Data.Char (isSpace)
|
||||
import Data.IORef
|
||||
(IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef)
|
||||
@ -176,12 +180,20 @@ instance Monad REPL where
|
||||
instance MonadIO REPL where
|
||||
liftIO = io
|
||||
|
||||
instance MonadBase IO REPL where
|
||||
liftBase = liftIO
|
||||
|
||||
instance MonadBaseControl IO REPL where
|
||||
type StM REPL a = a
|
||||
liftBaseWith f = REPL $ \ref ->
|
||||
f $ \m -> unREPL m ref
|
||||
restoreM x = return x
|
||||
|
||||
instance M.FreshM REPL where
|
||||
liftSupply f = modifyRW $ \ RW { .. } ->
|
||||
let (a,s') = f (M.meSupply eModuleEnv)
|
||||
in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a)
|
||||
|
||||
|
||||
-- Exceptions ------------------------------------------------------------------
|
||||
|
||||
-- | REPL exceptions.
|
||||
|
||||
@ -9,14 +9,14 @@
|
||||
{-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module Cryptol.Utils.PP where
|
||||
module Cryptol.Utils.PP (module Cryptol.Utils.PP, (<>)) where
|
||||
|
||||
import Cryptol.Utils.Ident
|
||||
|
||||
import Control.DeepSeq.Generics
|
||||
import Control.Monad (mplus)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import qualified Data.Monoid as M
|
||||
import Data.Monoid
|
||||
import Data.String (IsString(..))
|
||||
import qualified Data.Text as T
|
||||
import GHC.Generics (Generic)
|
||||
@ -36,7 +36,7 @@ instance NFData NameDisp where rnf = genericRnf
|
||||
instance Show NameDisp where
|
||||
show _ = "<NameDisp>"
|
||||
|
||||
instance M.Monoid NameDisp where
|
||||
instance Monoid NameDisp where
|
||||
mempty = EmptyNameDisp
|
||||
|
||||
mappend (NameDisp f) (NameDisp g) = NameDisp (\m n -> f m n `mplus` g m n)
|
||||
@ -70,7 +70,7 @@ fmtModName mn NotInScope = mn
|
||||
-- | Compose two naming environments, preferring names from the left
|
||||
-- environment.
|
||||
extend :: NameDisp -> NameDisp -> NameDisp
|
||||
extend = M.mappend
|
||||
extend = mappend
|
||||
|
||||
-- | Get the format for a name. When 'Nothing' is returned, the name is not
|
||||
-- currently in scope.
|
||||
@ -91,19 +91,23 @@ fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)
|
||||
|
||||
newtype Doc = Doc (NameDisp -> PJ.Doc) deriving (Generic)
|
||||
|
||||
instance Monoid Doc where
|
||||
mempty = liftPJ PJ.empty
|
||||
mappend = liftPJ2 (PJ.<>)
|
||||
|
||||
instance NFData Doc where rnf = genericRnf
|
||||
|
||||
runDoc :: NameDisp -> Doc -> PJ.Doc
|
||||
runDoc names (Doc f) = f names
|
||||
|
||||
instance Show Doc where
|
||||
show d = show (runDoc M.mempty d)
|
||||
show d = show (runDoc mempty d)
|
||||
|
||||
instance IsString Doc where
|
||||
fromString = text
|
||||
|
||||
render :: Doc -> String
|
||||
render d = PJ.render (runDoc M.mempty d)
|
||||
render d = PJ.render (runDoc mempty d)
|
||||
|
||||
class PP a where
|
||||
ppPrec :: Int -> a -> Doc
|
||||
@ -197,9 +201,6 @@ liftPJ2 f (Doc a) (Doc b) = Doc (\e -> f (a e) (b e))
|
||||
liftSep :: ([PJ.Doc] -> PJ.Doc) -> ([Doc] -> Doc)
|
||||
liftSep f ds = Doc (\e -> f [ d e | Doc d <- ds ])
|
||||
|
||||
(<>) :: Doc -> Doc -> Doc
|
||||
(<>) = liftPJ2 (PJ.<>)
|
||||
|
||||
(<+>) :: Doc -> Doc -> Doc
|
||||
(<+>) = liftPJ2 (PJ.<+>)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user