add missing cryptol-server directory

This commit is contained in:
Adam C. Foltzer 2015-07-08 18:01:22 -07:00
parent d5aff31d64
commit 89b4567b93
3 changed files with 455 additions and 0 deletions

View File

@ -0,0 +1,181 @@
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wall -fno-warn-orphans -fno-warn-type-defaults #-}
-- | Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol
-- types. Since these are meant to be consumed over a wire, they are
-- mostly focused on base values and interfaces rather than a full
-- serialization of internal ASTs and such.
module Cryptol.Aeson where
import Control.Applicative
import Control.Exception
import Data.Aeson
import Data.Aeson.TH
import qualified Data.HashMap.Strict as HM
import Data.List
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Vector as V
import qualified Cryptol.Eval.Error as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Renamer as M
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name
import qualified Cryptol.Parser as P
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Parser.Lexer as P
import qualified Cryptol.Parser.NoInclude as P
import qualified Cryptol.Parser.NoPat as NoPat
import qualified Cryptol.Parser.Position as P
import Cryptol.REPL.Monad
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.Utils.PP hiding (empty)
instance FromJSON a => FromJSON (Map QName a) where
parseJSON = withObject "QName map" $ \o -> do
let (ks, vs) = unzip (HM.toList o)
ks' = map keyToQName ks
vs' <- mapM parseJSON vs
return (Map.fromList (zip ks' vs'))
instance ToJSON a => ToJSON (Map QName a) where
toJSON m = Object (HM.fromList (zip ks' vs'))
where (ks, vs) = unzip (Map.toList m)
ks' = map keyFromQName ks
vs' = map toJSON vs
-- | Assume that a 'QName' contains only an optional 'ModName' and a
-- 'Name', rather than a 'NewName'. This should be safe for the
-- purposes of this API where we're dealing with top-level names.
keyToQName :: Text -> QName
keyToQName str =
case map T.unpack (T.split (== '.') str) of
[] -> error "empty QName"
[""] -> error "empty QName"
[x] -> mkUnqual (Name x)
xs -> mkQual (ModName (init xs)) (Name (last xs))
keyFromQName :: QName -> Text
keyFromQName = \case
QName Nothing (Name x) -> T.pack x
QName (Just (ModName mn)) (Name x) ->
T.pack (intercalate "." (mn ++ [x]))
_ -> error "NewName unsupported in JSON"
instance ToJSON Doc where
toJSON = String . T.pack . render
instance ToJSON E.Value where
toJSON = \case
E.VRecord fs -> object
[ "record" .= fs ]
E.VTuple vs -> object
[ "tuple" .= vs ]
E.VBit b -> object
[ "bit" .= b ]
E.VSeq isWord xs -> object
[ "sequence" .= object [ "isWord" .= isWord, "elements" .= xs ] ]
E.VWord w -> object
[ "word" .= w ]
E.VStream _ -> object
[ "stream" .= object [ "@note" .= "streams not supported" ] ]
E.VFun _ -> object
[ "function" .= object [ "@note" .= "functions not supported" ] ]
E.VPoly _ -> object
[ "poly" .= object [ "@note" .= "polymorphic values not supported" ] ]
instance FromJSON E.Value where
parseJSON = withObject "Value" $ \o ->
E.VRecord <$> o .: "record"
<|> E.VTuple <$> o .: "tuple"
<|> E.VBit <$> o .: "bit"
<|> do s <- o .: "sequence"
E.VSeq <$> s .: "isWord" <*> s .: "elements"
<|> E.VWord <$> o .: "word"
<|> error ("unexpected JSON value: " ++ show o)
nth :: Alternative f => Int -> Value -> f Value
nth i = \case
Array v ->
case v V.!? i of
Nothing -> empty
Just x -> pure x
_ -> empty
instance ToJSON P.Token where
toJSON = toJSON . pp
instance ToJSON IOException where
toJSON exn = object
[ "IOException" .= show exn ]
instance ToJSON M.RenamerError where
toJSON err = object
[ "renamerError" .= pp err ]
instance ToJSON T.Error where
toJSON err = object
[ "inferError" .= pp err ]
instance ToJSON E.BV where
toJSON = \case
E.BV w v -> object
[ "bitvector" .= object [ "width" .= w, "value" .= v ] ]
instance FromJSON E.BV where
parseJSON = withObject "BV" $ \o -> do
bv <- o .: "bitvector"
E.BV <$> bv .: "width" <*> bv .: "value"
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''REPLException)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameEnv)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameInfo)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''E.EvalError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.ParseError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Position)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Range)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Located)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.IncludeError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Schema)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Type)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.TParam)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Prop)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Named)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Kind)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NoPat.Error)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ModuleError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ImportSource)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Import)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.ImportSpec)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Type)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TParam)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Kind)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TVar)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TCon)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.PC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.UserTC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Schema)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TFun)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Selector)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } { fieldLabelModifier = drop 1 } ''T.Fixity)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Pragma)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Assoc)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''QName)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''ModName)
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Name)
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Pass)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecl)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Newtype)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TySyn)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecls)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Iface)

273
cryptol-server/Main.hs Normal file
View File

@ -0,0 +1,273 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wall -fdefer-typed-holes -fno-warn-type-defaults #-}
module Main where
import Control.Concurrent
import Control.Monad
import Control.Monad.IO.Class
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 qualified Data.Map as Map
import Data.Text (Text)
import qualified Data.Text as T
import Data.Word
import System.Environment
import System.Exit
import System.FilePath
import System.ZMQ4
import Text.Read
import qualified Cryptol.Eval.Value as E
import Cryptol.REPL.Command
import Cryptol.REPL.Monad
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.ModuleSystem as M
import Cryptol.Aeson ()
data RCommand
= RCEvalExpr Text
| RCApplyFun FunHandle E.Value
| RCTypeOf Text
| RCSetOpt Text Text
| RCCheck Text
| RCExhaust Text
| RCProve Text
| RCSat Text
| RCLoadModule FilePath
| RCDecls
| RCUnknownCmd Text
| RCExit
instance FromJSON RCommand where
parseJSON = withObject "RCommand" $ \o -> do
tag <- o .: "tag"
flip (withText "tag") tag $ \case
"evalExpr" -> RCEvalExpr <$> o .: "expr"
"applyFun" -> RCApplyFun <$> o .: "handle" <*> o .: "arg"
"typeOf" -> RCTypeOf <$> o .: "expr"
"setOpt" -> RCSetOpt <$> o .: "key" <*> o .: "value"
"check" -> RCCheck <$> o .: "expr"
"exhaust" -> RCExhaust <$> o .: "expr"
"prove" -> RCProve <$> o .: "expr"
"sat" -> RCSat <$> o .: "expr"
"loadModule" -> RCLoadModule . T.unpack <$> o .: "filePath"
"browse" -> return RCDecls
"exit" -> return RCExit
unknown -> return (RCUnknownCmd unknown)
newtype FunHandle = FH Int
deriving (Eq, Ord, Enum, Bounded, Show)
instance ToJSON FunHandle where
toJSON (FH i) = toJSON i
instance FromJSON FunHandle where
parseJSON v = FH <$> parseJSON v
data RResult
= RRValue E.Value
| RRFunValue FunHandle T.Type
| RRType T.Schema
| RRDecls M.IfaceDecls
| RRCheck String
| RRExhaust String
| RRSat String
| RRProve String
| RRInteractiveError REPLException
| RRUnknownCmd Text
| RRBadMessage BS.ByteString String
| RROk
instance ToJSON RResult where
toJSON = \case
RRValue v -> object
[ "tag" .= "value", "value" .= v ]
RRFunValue fh t -> object
[ "tag" .= "funValue", "handle" .= fh, "type" .= t ]
RRType s -> object
[ "tag" .= "type", "value" .= s ]
RRDecls ifds -> object
[ "tag" .= "decls", "decls" .= ifds ]
RRCheck out -> object
[ "tag" .= "check", "out" .= out ]
RRExhaust out -> object
[ "tag" .= "exhaust", "out" .= out ]
RRSat out -> object
[ "tag" .= "sat", "out" .= out ]
RRProve out -> object
[ "tag" .= "prove", "out" .= out ]
RRInteractiveError err -> object
[ "tag" .= "interactiveError", "error" .= err ]
RRUnknownCmd txt -> object
[ "tag" .= "unknownCommand", "command" .= txt ]
RRBadMessage msg err -> object
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
RROk -> object [ "tag" .= "ok" ]
data ControlMsg
= CMConnect
| CMExit
| CMUnknown Text
instance FromJSON ControlMsg where
parseJSON = withObject "ControlMsg" $ \o -> do
tag <- o .: "tag"
flip (withText "tag") tag $ \case
"connect" -> return CMConnect
"exit" -> return CMExit
other -> return $ CMUnknown other
data ControlReply
= CRConnect Word16
| CROk
| CRBadMessage BS.ByteString String
instance ToJSON ControlReply where
toJSON = \case
CRConnect port -> object
[ "tag" .= "connect", "port" .= port ]
CROk -> object [ "tag" .= "ok" ]
CRBadMessage msg err -> object
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
server :: Word16 -> IO ()
server port =
withContext $ \ctx ->
withSocket ctx Rep $ \rep -> do
let addr = "tcp://127.0.0.1:" ++ show port
putStrLn ("[cryptol-server] coming online at " ++ addr)
bind rep addr
let loop = do
msg <- receive rep
putStrLn "[cryptol-server] received message:"
case decodeStrict msg of
Nothing -> BS.putStrLn msg
Just js -> BSL.putStrLn (encodePretty (js :: Value))
case eitherDecodeStrict msg of
Left err -> reply rep $ CRBadMessage msg err
Right CMConnect -> do
putStrLn "[cryptol-server] handling new incoming connection"
newRep <- socket ctx Rep
bind newRep "tcp://127.0.0.1:*"
newAddr <- lastEndpoint newRep
let portStr = reverse . takeWhile isDigit . reverse $ newAddr
putStrLn ("[cryptol-server] starting worker on interface " ++ newAddr)
void . forkIO $ runRepl newRep
reply rep $ CRConnect (read portStr)
Right CMExit -> do
putStrLn "[cryptol-server] shutting down"
reply rep $ CROk
exitSuccess
Right (CMUnknown cmd) -> do
putStrLn ("[cryptol-server] unknown control command: " ++ T.unpack cmd)
reply rep $ CRBadMessage msg "unknown control command"
loop
loop
reply :: (ToJSON a, MonadIO m) => Socket Rep -> a -> m ()
reply rep msg = liftIO $ do
let bmsg = BS.concat . BSL.toChunks . encodePretty $ msg
putStrLn "[cryptol-server] sending response:"
BS.putStrLn bmsg
send rep [] bmsg
runRepl :: Socket Rep -> IO ()
runRepl rep = runREPL False $ do -- TODO: batch mode?
mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
case mCryptolPath of
Nothing -> return ()
Just path -> prependSearchPath path'
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-- Windows paths search from end to beginning
where path' = reverse (splitSearchPath path)
#else
where path' = splitSearchPath path
#endif
loadPrelude
funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
let handle err = reply rep (RRInteractiveError err)
loop = do
msg <- io $ receive rep
io $ putStrLn "[cryptol-worker] received message:"
case decodeStrict msg of
Nothing -> io $ BS.putStrLn msg
Just js -> io $ BSL.putStrLn (encodePretty (js :: Value))
flip catch handle $ case eitherDecodeStrict msg of
Left cmdErr -> reply rep (RRBadMessage msg cmdErr)
Right rc -> case rc of
RCEvalExpr txt -> do
expr <- replParseExpr (T.unpack txt)
(val, ty) <- replEvalExpr expr
case val of
E.VFun f -> do
fh <- io $ atomicModifyIORef' funHandles $ \(m, fh) ->
let m' = Map.insert fh f m
fh' = succ fh
in ((m', fh'), fh)
reply rep (RRFunValue fh ty)
_ -> reply rep (RRValue val)
RCApplyFun fh arg -> do
(m, _) <- io $ readIORef funHandles
case Map.lookup fh m of
Nothing -> reply rep (RRBadMessage "invalid function handle" (show fh))
Just f -> reply rep (RRValue (f arg))
RCTypeOf txt -> do
expr <- replParseExpr (T.unpack txt)
(_expr, _def, sch) <- replCheckExpr expr
reply rep (RRType sch)
RCSetOpt key val -> do
setOptionCmd (T.unpack key ++ "=" ++ T.unpack val)
reply rep RROk
RCCheck expr -> do
(_, out) <- withCapturedOutput (qcCmd QCRandom (T.unpack expr))
reply rep (RRCheck out)
RCExhaust expr -> do
(_, out) <- withCapturedOutput (qcCmd QCExhaust (T.unpack expr))
reply rep (RRExhaust out)
RCProve expr -> do
(_, out) <- withCapturedOutput (proveCmd (T.unpack expr))
reply rep (RRProve out)
RCSat expr -> do
(_, out) <- withCapturedOutput (satCmd (T.unpack expr))
reply rep (RRSat out)
RCLoadModule fp -> do
loadCmd fp
reply rep RROk
RCDecls -> do
(decls, _names) <- getFocusedEnv
reply rep (RRDecls decls)
RCUnknownCmd cmd -> reply rep (RRUnknownCmd cmd)
RCExit -> do
reply rep RROk
io $ close rep
io $ putStrLn "[cryptol-worker] shutting down"
void $ forever loop
withCapturedOutput :: REPL a -> REPL (a, String)
withCapturedOutput m = do
old <- getPutStr
buf <- io $ newIORef ""
setPutStr $ \s -> modifyIORef' buf (++ s)
x <- m
s <- io $ readIORef buf
setPutStr old
return (x, s)
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"

View File

@ -214,6 +214,7 @@ executable cryptol-server
, bytestring >= 0.10
, containers >= 0.5
, cryptol
, filepath
, text >= 1.2
, transformers >= 0.4
, unordered-containers >= 0.2