mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Add cryptol-remote-api
(#927)
This commit moves the `cryptol-remote-api` package from the `argo` repository to the `cryptol` repository.
This commit is contained in:
parent
72611f77bd
commit
f0b851ecf0
6
.github/ci.sh
vendored
6
.github/ci.sh
vendored
@ -77,7 +77,7 @@ install_cvc4() {
|
||||
esac
|
||||
# Temporary workaround
|
||||
if [[ "$RUNNER_OS" == "Linux" ]]; then
|
||||
curl -o cvc4$EXT -sL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-09-30-x86_64-linux-opt"
|
||||
curl -o cvc4$EXT -sL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-10-12-x86_64-linux-opt"
|
||||
else
|
||||
curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
|
||||
fi
|
||||
@ -136,6 +136,10 @@ test_dist() {
|
||||
$BIN/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol tests
|
||||
}
|
||||
|
||||
test_rpc() {
|
||||
cabal v2-test cryptol-remote-api
|
||||
}
|
||||
|
||||
bundle_files() {
|
||||
doc=dist/share/doc/cryptol
|
||||
mkdir -p $doc
|
||||
|
9
.github/workflows/build.yml
vendored
9
.github/workflows/build.yml
vendored
@ -47,6 +47,10 @@ jobs:
|
||||
with:
|
||||
submodules: true
|
||||
|
||||
- uses: actions/setup-python@v2
|
||||
with:
|
||||
python-version: '3.x'
|
||||
|
||||
- uses: actions/setup-haskell@v1
|
||||
id: setup-haskell
|
||||
with:
|
||||
@ -78,6 +82,11 @@ jobs:
|
||||
- shell: bash
|
||||
run: .github/ci.sh test_dist
|
||||
|
||||
# TODO: get Python client to work on Windows
|
||||
- shell: bash
|
||||
run: .github/ci.sh test_rpc
|
||||
if: runner.os != 'Windows'
|
||||
|
||||
- if: >-
|
||||
env.RELEASE && matrix.ghc == '8.8.4'
|
||||
uses: actions/upload-artifact@v2
|
||||
|
@ -32,7 +32,7 @@ RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux
|
||||
# Install CVC4 1.8
|
||||
# The latest CVC4 1.8 and the release version has a minor discrepency between it, causing sbv to fail
|
||||
# https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt
|
||||
RUN curl -L https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-09-30-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
|
||||
RUN curl -L https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-10-12-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4
|
||||
|
||||
# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license.
|
||||
# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz
|
||||
|
@ -1,5 +1,7 @@
|
||||
packages:
|
||||
cryptol.cabal
|
||||
cryptol-remote-api
|
||||
tests
|
||||
deps/argo/argo
|
||||
deps/argo/cryptol-remote-api
|
||||
deps/argo/python
|
||||
deps/argo/tasty-script-exitcode
|
||||
|
5
cryptol-remote-api/CHANGELOG.md
Normal file
5
cryptol-remote-api/CHANGELOG.md
Normal file
@ -0,0 +1,5 @@
|
||||
# Revision history for cryptol-server
|
||||
|
||||
## 0.1.0.0 -- YYYY-mm-dd
|
||||
|
||||
* First version. Released on an unsuspecting world.
|
29
cryptol-remote-api/LICENSE
Normal file
29
cryptol-remote-api/LICENSE
Normal file
@ -0,0 +1,29 @@
|
||||
BSD 3-Clause License
|
||||
|
||||
Copyright (c) 2019, Galois, Inc.
|
||||
All rights reserved.
|
||||
|
||||
Redistribution and use in source and binary forms, with or without
|
||||
modification, are permitted provided that the following conditions are met:
|
||||
|
||||
1. Redistributions of source code must retain the above copyright notice, this
|
||||
list of conditions and the following disclaimer.
|
||||
|
||||
2. Redistributions in binary form must reproduce the above copyright notice,
|
||||
this list of conditions and the following disclaimer in the documentation
|
||||
and/or other materials provided with the distribution.
|
||||
|
||||
3. Neither the name of the copyright holder nor the names of its
|
||||
contributors may be used to endorse or promote products derived from
|
||||
this software without specific prior written permission.
|
||||
|
||||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
2
cryptol-remote-api/Setup.hs
Normal file
2
cryptol-remote-api/Setup.hs
Normal file
@ -0,0 +1,2 @@
|
||||
import Distribution.Simple
|
||||
main = defaultMain
|
84
cryptol-remote-api/cryptol-remote-api.cabal
Normal file
84
cryptol-remote-api/cryptol-remote-api.cabal
Normal file
@ -0,0 +1,84 @@
|
||||
cabal-version: 2.4
|
||||
name: cryptol-remote-api
|
||||
version: 0.1.0.0
|
||||
license: BSD-3-Clause
|
||||
license-file: LICENSE
|
||||
author: David Thrane Christiansen
|
||||
maintainer: dtc@galois.com
|
||||
category: Language
|
||||
extra-source-files: CHANGELOG.md
|
||||
data-files: test-scripts/**/*.py
|
||||
test-scripts/**/*.cry
|
||||
|
||||
common warnings
|
||||
ghc-options:
|
||||
-Weverything
|
||||
-Wno-missing-exported-signatures
|
||||
-Wno-missing-import-lists
|
||||
-Wno-missed-specialisations
|
||||
-Wno-all-missed-specialisations
|
||||
-Wno-unsafe
|
||||
-Wno-safe
|
||||
-Wno-missing-local-signatures
|
||||
-Wno-monomorphism-restriction
|
||||
-Wno-implicit-prelude
|
||||
|
||||
common deps
|
||||
build-depends:
|
||||
base >=4.11.1.0 && <4.15,
|
||||
argo,
|
||||
aeson >= 1.4.2,
|
||||
base64-bytestring >= 1.0,
|
||||
bytestring ^>= 0.10.8,
|
||||
containers >=0.5.11 && <0.7,
|
||||
cryptol >= 2.9.0,
|
||||
directory ^>= 1.3.1,
|
||||
filepath ^>= 1.4,
|
||||
lens >= 4.17 && < 4.20,
|
||||
scientific ^>= 0.3,
|
||||
text ^>= 1.2.3,
|
||||
unordered-containers ^>= 0.2,
|
||||
vector ^>= 0.12,
|
||||
|
||||
default-language: Haskell2010
|
||||
|
||||
library
|
||||
import: deps, warnings
|
||||
hs-source-dirs: src
|
||||
|
||||
exposed-modules:
|
||||
CryptolServer
|
||||
CryptolServer.Call
|
||||
CryptolServer.ChangeDir
|
||||
CryptolServer.Data.Expression
|
||||
CryptolServer.Data.Type
|
||||
CryptolServer.EvalExpr
|
||||
CryptolServer.Exceptions
|
||||
CryptolServer.FocusedModule
|
||||
CryptolServer.LoadModule
|
||||
CryptolServer.Names
|
||||
CryptolServer.Sat
|
||||
CryptolServer.TypeCheck
|
||||
|
||||
executable cryptol-remote-api
|
||||
import: deps, warnings
|
||||
main-is: Main.hs
|
||||
hs-source-dirs: cryptol-remote-api
|
||||
|
||||
build-depends:
|
||||
cryptol-remote-api,
|
||||
sbv < 8.8
|
||||
|
||||
test-suite test-cryptol-remote-api
|
||||
import: deps, warnings
|
||||
type: exitcode-stdio-1.0
|
||||
hs-source-dirs: test
|
||||
main-is: Test.hs
|
||||
other-modules: Paths_cryptol_remote_api
|
||||
build-depends:
|
||||
argo-python,
|
||||
cryptol-remote-api,
|
||||
quickcheck-instances ^>= 0.3.19,
|
||||
tasty >= 1.2.1,
|
||||
tasty-quickcheck ^>= 0.10,
|
||||
tasty-script-exitcode
|
51
cryptol-remote-api/cryptol-remote-api/Main.hs
Normal file
51
cryptol-remote-api/cryptol-remote-api/Main.hs
Normal file
@ -0,0 +1,51 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PartialTypeSignatures #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Main (main) where
|
||||
|
||||
import qualified Data.Aeson as JSON
|
||||
import Data.Text (Text)
|
||||
import System.Environment (lookupEnv)
|
||||
import System.FilePath (splitSearchPath)
|
||||
|
||||
import Argo
|
||||
import Argo.DefaultMain
|
||||
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Call
|
||||
import CryptolServer.ChangeDir
|
||||
import CryptolServer.EvalExpr
|
||||
import CryptolServer.FocusedModule
|
||||
import CryptolServer.LoadModule
|
||||
import CryptolServer.Names
|
||||
import CryptolServer.Sat
|
||||
import CryptolServer.TypeCheck
|
||||
|
||||
main :: IO ()
|
||||
main =
|
||||
do paths <- getSearchPaths
|
||||
initSt <- setSearchPath paths <$> initialState
|
||||
theApp <- mkApp (const (pure initSt)) cryptolMethods
|
||||
defaultMain description theApp
|
||||
|
||||
description :: String
|
||||
description =
|
||||
"An RPC server for Cryptol that supports type checking and evaluation of Cryptol code."
|
||||
|
||||
getSearchPaths :: IO [FilePath]
|
||||
getSearchPaths =
|
||||
maybe [] splitSearchPath <$> lookupEnv "CRYPTOLPATH"
|
||||
|
||||
cryptolMethods :: [(Text, MethodType, JSON.Value -> Method ServerState JSON.Value)]
|
||||
cryptolMethods =
|
||||
[ ("change directory", Command, method cd)
|
||||
, ("load module", Command, method loadModule)
|
||||
, ("load file", Command, method loadFile)
|
||||
, ("focused module", Query, method focusedModule)
|
||||
, ("evaluate expression", Query, method evalExpression)
|
||||
, ("call", Query, method call)
|
||||
, ("visible names", Query, method visibleNames)
|
||||
, ("check type", Query, method checkType)
|
||||
, ("satisfy", Query, method sat)
|
||||
]
|
80
cryptol-remote-api/src/CryptolServer.hs
Normal file
80
cryptol-remote-api/src/CryptolServer.hs
Normal file
@ -0,0 +1,80 @@
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer (module CryptolServer) where
|
||||
|
||||
import Control.Lens
|
||||
import Control.Monad.IO.Class
|
||||
|
||||
import Cryptol.Eval.Monad (EvalOpts(..), PPOpts(..), PPFloatFormat(..), PPFloatExp(..))
|
||||
import Cryptol.ModuleSystem (ModuleCmd, ModuleEnv)
|
||||
import Cryptol.ModuleSystem.Env
|
||||
(getLoadedModules, lmFilePath, lmFingerprint, meLoadedModules,
|
||||
initialModuleEnv, meSearchPath, ModulePath(..))
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.Parser.AST (ModName)
|
||||
import Cryptol.Utils.Logger (quietLogger)
|
||||
|
||||
import Argo
|
||||
import CryptolServer.Exceptions
|
||||
|
||||
runModuleCmd :: ModuleCmd a -> Method ServerState a
|
||||
runModuleCmd cmd =
|
||||
do s <- getState
|
||||
reader <- getFileReader
|
||||
out <- liftIO $ cmd (theEvalOpts, reader, view moduleEnv s)
|
||||
case out of
|
||||
(Left x, warns) ->
|
||||
raise (cryptolError x warns)
|
||||
(Right (x, newEnv), _warns) ->
|
||||
-- TODO: What to do about warnings when a command completes
|
||||
-- successfully?
|
||||
do setState (set moduleEnv newEnv s)
|
||||
return x
|
||||
|
||||
data LoadedModule = LoadedModule
|
||||
{ _loadedName :: Maybe ModName -- ^ Working on this module.
|
||||
, _loadedPath :: FilePath -- ^ Working on this file.
|
||||
}
|
||||
|
||||
loadedName :: Lens' LoadedModule (Maybe ModName)
|
||||
loadedName = lens _loadedName (\v n -> v { _loadedName = n })
|
||||
|
||||
loadedPath :: Lens' LoadedModule FilePath
|
||||
loadedPath = lens _loadedPath (\v n -> v { _loadedPath = n })
|
||||
|
||||
|
||||
data ServerState =
|
||||
ServerState { _loadedModule :: Maybe LoadedModule
|
||||
, _moduleEnv :: ModuleEnv
|
||||
}
|
||||
|
||||
loadedModule :: Lens' ServerState (Maybe LoadedModule)
|
||||
loadedModule = lens _loadedModule (\v n -> v { _loadedModule = n })
|
||||
|
||||
moduleEnv :: Lens' ServerState ModuleEnv
|
||||
moduleEnv = lens _moduleEnv (\v n -> v { _moduleEnv = n })
|
||||
|
||||
initialState :: IO ServerState
|
||||
initialState = ServerState Nothing <$> initialModuleEnv
|
||||
|
||||
setSearchPath :: [FilePath] -> ServerState -> ServerState
|
||||
setSearchPath paths =
|
||||
over moduleEnv $ \me -> me { meSearchPath = paths ++ meSearchPath me }
|
||||
|
||||
theEvalOpts :: EvalOpts
|
||||
theEvalOpts = EvalOpts quietLogger (PPOpts False 10 25 10 (FloatFree AutoExponent))
|
||||
|
||||
-- | Check that all of the modules loaded in the Cryptol environment
|
||||
-- currently have fingerprints that match those when they were loaded.
|
||||
validateServerState :: ServerState -> IO Bool
|
||||
validateServerState =
|
||||
foldr check (return True) . getLoadedModules . meLoadedModules . view moduleEnv
|
||||
where
|
||||
check lm continue =
|
||||
case lmFilePath lm of
|
||||
InMem{} -> continue
|
||||
InFile file ->
|
||||
do fp <- fingerprintFile file
|
||||
if fp == Just (lmFingerprint lm)
|
||||
then continue
|
||||
else return False
|
90
cryptol-remote-api/src/CryptolServer/Call.hs
Normal file
90
cryptol-remote-api/src/CryptolServer/Call.hs
Normal file
@ -0,0 +1,90 @@
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
module CryptolServer.Call
|
||||
( Expression(..)
|
||||
, Encoding(..)
|
||||
, LetBinding(..)
|
||||
, call
|
||||
, CallParams(..)
|
||||
) where
|
||||
|
||||
import Control.Lens hiding ((.=))
|
||||
import Control.Monad (unless)
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Aeson as JSON hiding (Encoding, Value, decode)
|
||||
import qualified Data.Aeson as JSON
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
|
||||
import Cryptol.IR.FreeVars (freeVars, tyDeps, valDeps)
|
||||
import Cryptol.ModuleSystem (checkExpr, evalExpr, getPrimMap, meLoadedModules)
|
||||
import Cryptol.ModuleSystem.Env (isLoadedParamMod, meSolverConfig)
|
||||
import Cryptol.ModuleSystem.Name (NameInfo(Declared), nameInfo)
|
||||
import Cryptol.Parser.AST (Expr(..), PName(..))
|
||||
import Cryptol.TypeCheck.AST (sType)
|
||||
import Cryptol.TypeCheck.Solve (defaultReplExpr)
|
||||
import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.PP (pretty)
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
|
||||
import Argo
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions
|
||||
import CryptolServer.Data.Expression
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
call :: CallParams -> Method ServerState JSON.Value
|
||||
call (CallParams fun rawArgs) =
|
||||
do args <- traverse getExpr rawArgs
|
||||
let appExpr = mkEApp (EVar (UnQual (mkIdent fun))) args
|
||||
(_expr, ty, schema) <- runModuleCmd (checkExpr appExpr)
|
||||
evalAllowed ty
|
||||
evalAllowed schema
|
||||
me <- view moduleEnv <$> getState
|
||||
let cfg = meSolverConfig me
|
||||
perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema)
|
||||
case perhapsDef of
|
||||
Nothing -> error "TODO" -- TODO: What should happen here?
|
||||
Just (tys, checked) ->
|
||||
do noDefaults tys
|
||||
let su = listParamSubst tys
|
||||
let theType = apSubst su (sType schema)
|
||||
res <- runModuleCmd (evalExpr checked)
|
||||
prims <- runModuleCmd getPrimMap
|
||||
val <- observe $ readBack prims theType res
|
||||
return (JSON.object [ "value" .= val
|
||||
, "type string" .= pretty theType
|
||||
, "type" .= JSONType mempty theType
|
||||
])
|
||||
where
|
||||
noDefaults [] = return ()
|
||||
noDefaults xs@(_:_) =
|
||||
raise (unwantedDefaults xs)
|
||||
|
||||
evalAllowed x =
|
||||
do me <- view moduleEnv <$> getState
|
||||
let ds = freeVars x
|
||||
badVals = foldr badName Set.empty (valDeps ds)
|
||||
bad = foldr badName badVals (tyDeps ds)
|
||||
badName nm bs =
|
||||
case nameInfo nm of
|
||||
Declared m _
|
||||
| isLoadedParamMod m (meLoadedModules me) -> Set.insert nm bs
|
||||
_ -> bs
|
||||
unless (Set.null bad) $
|
||||
raise (evalInParamMod (Set.toList bad))
|
||||
|
||||
|
||||
data CallParams
|
||||
= CallParams Text [Expression]
|
||||
|
||||
instance FromJSON CallParams where
|
||||
parseJSON =
|
||||
withObject "params for \"call\"" $
|
||||
\o -> CallParams <$> o .: "function" <*> o .: "arguments"
|
25
cryptol-remote-api/src/CryptolServer/ChangeDir.hs
Normal file
25
cryptol-remote-api/src/CryptolServer/ChangeDir.hs
Normal file
@ -0,0 +1,25 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.ChangeDir (cd, ChangeDirectoryParams(..)) where
|
||||
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Aeson as JSON
|
||||
import System.Directory
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions
|
||||
import Argo
|
||||
|
||||
cd :: ChangeDirectoryParams -> Method ServerState ()
|
||||
cd (ChangeDirectoryParams newDir) =
|
||||
do exists <- liftIO $ doesDirectoryExist newDir
|
||||
if exists
|
||||
then liftIO $ setCurrentDirectory newDir
|
||||
else raise (dirNotFound newDir)
|
||||
|
||||
data ChangeDirectoryParams
|
||||
= ChangeDirectoryParams FilePath
|
||||
|
||||
instance FromJSON ChangeDirectoryParams where
|
||||
parseJSON =
|
||||
withObject "params for \"change directory\"" $
|
||||
\o -> ChangeDirectoryParams <$> o .: "directory"
|
373
cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Normal file
373
cryptol-remote-api/src/CryptolServer/Data/Expression.hs
Normal file
@ -0,0 +1,373 @@
|
||||
{-# OPTIONS_GHC -fno-warn-type-defaults #-}
|
||||
{-# LANGUAGE ImplicitParams #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
module CryptolServer.Data.Expression
|
||||
( module CryptolServer.Data.Expression
|
||||
) where
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Exception (throwIO)
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Aeson as JSON hiding (Encoding, Value, decode)
|
||||
import qualified Data.ByteString as BS
|
||||
import qualified Data.ByteString.Base64 as Base64
|
||||
import Data.HashMap.Strict (HashMap)
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import Data.List.NonEmpty (NonEmpty(..))
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Scientific as Sc
|
||||
import Data.Text (Text, pack)
|
||||
import qualified Data.Text as T
|
||||
import Data.Traversable
|
||||
import qualified Data.Vector as V
|
||||
import Data.Text.Encoding (encodeUtf8)
|
||||
import Numeric (showHex)
|
||||
|
||||
import Cryptol.Eval (evalSel)
|
||||
import Cryptol.Eval.Monad
|
||||
import Cryptol.Eval.Concrete (primTable)
|
||||
import Cryptol.Eval.Concrete.Value hiding (Concrete)
|
||||
import qualified Cryptol.Eval.Concrete.Value as C
|
||||
import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap)
|
||||
import Cryptol.Parser
|
||||
import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Type(..), PName(..), Literal(..), NumInfo(..))
|
||||
import Cryptol.Parser.Position (Located(..), emptyRange)
|
||||
import Cryptol.Parser.Selector
|
||||
-- import Cryptol.Prims.Syntax
|
||||
import Cryptol.TypeCheck.AST (PrimMap)
|
||||
import Cryptol.TypeCheck.SimpType (tRebuild)
|
||||
import qualified Cryptol.TypeCheck.Type as TC
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.RecordMap (recordFromFields, canonicalFields)
|
||||
|
||||
|
||||
import Argo
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions
|
||||
|
||||
data Encoding = Base64 | Hex
|
||||
deriving (Eq, Show, Ord)
|
||||
|
||||
instance JSON.FromJSON Encoding where
|
||||
parseJSON =
|
||||
withText "encoding" $
|
||||
\case
|
||||
"hex" -> pure Hex
|
||||
"base64" -> pure Base64
|
||||
_ -> empty
|
||||
|
||||
data LetBinding =
|
||||
LetBinding
|
||||
{ argDefName :: !Text
|
||||
, argDefVal :: !Expression
|
||||
}
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
instance JSON.FromJSON LetBinding where
|
||||
parseJSON =
|
||||
withObject "let binding" $ \o ->
|
||||
LetBinding <$> o .: "name" <*> o .: "definition"
|
||||
|
||||
instance JSON.ToJSON LetBinding where
|
||||
toJSON (LetBinding x def) =
|
||||
object [ "name" .= x
|
||||
, "definition" .= def
|
||||
]
|
||||
|
||||
data Expression =
|
||||
Bit !Bool
|
||||
| Unit
|
||||
| Num !Encoding !Text !Integer -- ^ data and bitwidth
|
||||
| Record !(HashMap Text Expression)
|
||||
| Sequence ![Expression]
|
||||
| Tuple ![Expression]
|
||||
| Integer !Integer
|
||||
| IntegerModulo !Integer !Integer -- ^ value, modulus
|
||||
| Concrete !Text
|
||||
| Let ![LetBinding] !Expression
|
||||
| Application !Expression !(NonEmpty Expression)
|
||||
deriving (Eq, Ord, Show)
|
||||
|
||||
data ExpressionTag =
|
||||
TagNum | TagRecord | TagSequence | TagTuple | TagUnit | TagLet | TagApp | TagIntMod
|
||||
|
||||
instance JSON.FromJSON ExpressionTag where
|
||||
parseJSON =
|
||||
withText "tag" $
|
||||
\case
|
||||
"bits" -> pure TagNum
|
||||
"unit" -> pure TagUnit
|
||||
"record" -> pure TagRecord
|
||||
"sequence" -> pure TagSequence
|
||||
"tuple" -> pure TagTuple
|
||||
"let" -> pure TagLet
|
||||
"call" -> pure TagApp
|
||||
"integer modulo" -> pure TagIntMod
|
||||
_ -> empty
|
||||
|
||||
instance JSON.ToJSON ExpressionTag where
|
||||
toJSON TagNum = "bits"
|
||||
toJSON TagRecord = "record"
|
||||
toJSON TagSequence = "sequence"
|
||||
toJSON TagTuple = "tuple"
|
||||
toJSON TagUnit = "unit"
|
||||
toJSON TagLet = "let"
|
||||
toJSON TagApp = "call"
|
||||
toJSON TagIntMod = "integer modulo"
|
||||
|
||||
instance JSON.FromJSON Expression where
|
||||
parseJSON v = bool v <|> integer v <|> concrete v <|> obj v
|
||||
where
|
||||
bool =
|
||||
withBool "boolean" $ pure . Bit
|
||||
integer =
|
||||
-- Note: this means that we should not expose this API to the
|
||||
-- public, but only to systems that will validate input
|
||||
-- integers. Otherwise, they can use this to allocate a
|
||||
-- gigantic integer that fills up all memory.
|
||||
withScientific "integer" $ \s ->
|
||||
case Sc.floatingOrInteger s of
|
||||
Left _fl -> empty
|
||||
Right i -> pure (Integer i)
|
||||
concrete =
|
||||
withText "concrete syntax" $ pure . Concrete
|
||||
|
||||
obj =
|
||||
withObject "argument" $
|
||||
\o -> o .: "expression" >>=
|
||||
\case
|
||||
TagUnit -> pure Unit
|
||||
TagNum ->
|
||||
do enc <- o .: "encoding"
|
||||
Num enc <$> o .: "data" <*> o .: "width"
|
||||
TagRecord ->
|
||||
do fields <- o .: "data"
|
||||
flip (withObject "record data") fields $
|
||||
\fs -> Record <$> traverse parseJSON fs
|
||||
TagSequence ->
|
||||
do contents <- o .: "data"
|
||||
flip (withArray "sequence") contents $
|
||||
\s -> Sequence . V.toList <$> traverse parseJSON s
|
||||
TagTuple ->
|
||||
do contents <- o .: "data"
|
||||
flip (withArray "tuple") contents $
|
||||
\s -> Tuple . V.toList <$> traverse parseJSON s
|
||||
TagLet ->
|
||||
Let <$> o .: "binders" <*> o .: "body"
|
||||
TagApp ->
|
||||
Application <$> o .: "function" <*> o .: "arguments"
|
||||
TagIntMod ->
|
||||
IntegerModulo <$> o .: "integer" <*> o .: "modulus"
|
||||
|
||||
instance ToJSON Encoding where
|
||||
toJSON Hex = String "hex"
|
||||
toJSON Base64 = String "base64"
|
||||
|
||||
instance JSON.ToJSON Expression where
|
||||
toJSON Unit = object [ "expression" .= TagUnit ]
|
||||
toJSON (Bit b) = JSON.Bool b
|
||||
toJSON (Integer i) = JSON.Number (fromInteger i)
|
||||
toJSON (IntegerModulo i n) =
|
||||
object [ "expression" .= TagIntMod
|
||||
, "integer" .= JSON.Number (fromInteger i)
|
||||
, "modulus" .= JSON.Number (fromInteger n)
|
||||
]
|
||||
toJSON (Concrete expr) = toJSON expr
|
||||
toJSON (Num enc dat w) =
|
||||
object [ "expression" .= TagNum
|
||||
, "data" .= String dat
|
||||
, "encoding" .= enc
|
||||
, "width" .= w
|
||||
]
|
||||
toJSON (Record fields) =
|
||||
object [ "expression" .= TagRecord
|
||||
, "data" .= object [ fieldName .= toJSON val
|
||||
| (fieldName, val) <- HM.toList fields
|
||||
]
|
||||
]
|
||||
toJSON (Sequence elts) =
|
||||
object [ "expression" .= TagSequence
|
||||
, "data" .= Array (V.fromList (map toJSON elts))
|
||||
]
|
||||
toJSON (Tuple projs) =
|
||||
object [ "expression" .= TagTuple
|
||||
, "data" .= Array (V.fromList (map toJSON projs))
|
||||
]
|
||||
toJSON (Let binds body) =
|
||||
object [ "expression" .= TagLet
|
||||
, "binders" .= Array (V.fromList (map toJSON binds))
|
||||
, "body" .= toJSON body
|
||||
]
|
||||
toJSON (Application fun args) =
|
||||
object [ "expression" .= TagApp
|
||||
, "function" .= fun
|
||||
, "arguments" .= args
|
||||
]
|
||||
|
||||
|
||||
decode :: Encoding -> Text -> Method s Integer
|
||||
decode Base64 txt =
|
||||
let bytes = encodeUtf8 txt
|
||||
in
|
||||
case Base64.decode bytes of
|
||||
Left err ->
|
||||
raise (invalidBase64 bytes err)
|
||||
Right decoded -> return $ bytesToInt decoded
|
||||
decode Hex txt =
|
||||
squish <$> traverse hexDigit (T.unpack txt)
|
||||
where
|
||||
squish = foldl (\acc i -> (acc * 16) + i) 0
|
||||
|
||||
hexDigit :: Num a => Char -> Method s a
|
||||
hexDigit '0' = pure 0
|
||||
hexDigit '1' = pure 1
|
||||
hexDigit '2' = pure 2
|
||||
hexDigit '3' = pure 3
|
||||
hexDigit '4' = pure 4
|
||||
hexDigit '5' = pure 5
|
||||
hexDigit '6' = pure 6
|
||||
hexDigit '7' = pure 7
|
||||
hexDigit '8' = pure 8
|
||||
hexDigit '9' = pure 9
|
||||
hexDigit 'a' = pure 10
|
||||
hexDigit 'A' = pure 10
|
||||
hexDigit 'b' = pure 11
|
||||
hexDigit 'B' = pure 11
|
||||
hexDigit 'c' = pure 12
|
||||
hexDigit 'C' = pure 12
|
||||
hexDigit 'd' = pure 13
|
||||
hexDigit 'D' = pure 13
|
||||
hexDigit 'e' = pure 14
|
||||
hexDigit 'E' = pure 14
|
||||
hexDigit 'f' = pure 15
|
||||
hexDigit 'F' = pure 15
|
||||
hexDigit c = raise (invalidHex c)
|
||||
|
||||
|
||||
getExpr :: Expression -> Method s (Expr PName)
|
||||
getExpr Unit =
|
||||
return $
|
||||
ETyped
|
||||
(ETuple [])
|
||||
(TTuple [])
|
||||
getExpr (Bit b) =
|
||||
return $
|
||||
ETyped
|
||||
(EVar (UnQual (mkIdent $ if b then "True" else "False")))
|
||||
TBit
|
||||
getExpr (Integer i) =
|
||||
return $
|
||||
ETyped
|
||||
(ELit (ECNum i (DecLit (pack (show i)))))
|
||||
(TUser (UnQual (mkIdent "Integer")) [])
|
||||
getExpr (IntegerModulo i n) =
|
||||
return $
|
||||
ETyped
|
||||
(ELit (ECNum i (DecLit (pack (show i)))))
|
||||
(TUser (UnQual (mkIdent "Z")) [TNum n])
|
||||
getExpr (Num enc txt w) =
|
||||
do d <- decode enc txt
|
||||
return $ ETyped
|
||||
(ELit (ECNum d (DecLit txt)))
|
||||
(TSeq (TNum w) TBit)
|
||||
getExpr (Record fields) =
|
||||
fmap (ERecord . recordFromFields) $ for (HM.toList fields) $
|
||||
\(recName, spec) ->
|
||||
(mkIdent recName,) . (emptyRange,) <$> getExpr spec
|
||||
getExpr (Sequence elts) =
|
||||
EList <$> traverse getExpr elts
|
||||
getExpr (Tuple projs) =
|
||||
ETuple <$> traverse getExpr projs
|
||||
getExpr (Concrete syntax) =
|
||||
case parseExpr syntax of
|
||||
Left err ->
|
||||
raise (cryptolParseErr syntax err)
|
||||
Right e -> pure e
|
||||
getExpr (Let binds body) =
|
||||
EWhere <$> getExpr body <*> traverse mkBind binds
|
||||
where
|
||||
mkBind (LetBinding x rhs) =
|
||||
DBind .
|
||||
(\bindBody ->
|
||||
Bind (fakeLoc (UnQual (mkIdent x))) [] bindBody Nothing False Nothing [] True Nothing) .
|
||||
fakeLoc .
|
||||
DExpr <$>
|
||||
getExpr rhs
|
||||
|
||||
fakeLoc = Located emptyRange
|
||||
getExpr (Application fun (arg :| [])) =
|
||||
EApp <$> getExpr fun <*> getExpr arg
|
||||
getExpr (Application fun (arg1 :| (arg : args))) =
|
||||
getExpr (Application (Application fun (arg1 :| [])) (arg :| args))
|
||||
|
||||
-- TODO add tests that this is big-endian
|
||||
-- | Interpret a ByteString as an Integer
|
||||
bytesToInt :: BS.ByteString -> Integer
|
||||
bytesToInt bs =
|
||||
BS.foldl' (\acc w -> (acc * 256) + toInteger w) 0 bs
|
||||
|
||||
typeNum :: (Alternative f, Integral a) => TC.Type -> f a
|
||||
typeNum (tRebuild -> (TC.TCon (TC.TC (TC.TCNum n)) [])) =
|
||||
pure $ fromIntegral n
|
||||
typeNum _ = empty
|
||||
|
||||
readBack :: PrimMap -> TC.Type -> Value -> Eval Expression
|
||||
readBack prims ty val =
|
||||
let tbl = primTable theEvalOpts in
|
||||
let ?evalPrim = \i -> Map.lookup i tbl in
|
||||
case TC.tNoUser ty of
|
||||
TC.TRec tfs ->
|
||||
Record . HM.fromList <$>
|
||||
sequence [ do fv <- evalSel C.Concrete val (RecordSel f Nothing)
|
||||
fa <- readBack prims t fv
|
||||
return (identText f, fa)
|
||||
| (f, t) <- canonicalFields tfs
|
||||
]
|
||||
TC.TCon (TC.TC (TC.TCTuple _)) [] ->
|
||||
pure Unit
|
||||
TC.TCon (TC.TC (TC.TCTuple _)) ts ->
|
||||
Tuple <$> sequence [ do v <- evalSel C.Concrete val (TupleSel n Nothing)
|
||||
a <- readBack prims t v
|
||||
return a
|
||||
| (n, t) <- zip [0..] ts
|
||||
]
|
||||
TC.TCon (TC.TC TC.TCBit) [] ->
|
||||
case val of
|
||||
VBit b -> pure (Bit b)
|
||||
_ -> mismatchPanic
|
||||
TC.TCon (TC.TC TC.TCInteger) [] ->
|
||||
case val of
|
||||
VInteger i -> pure (Integer i)
|
||||
_ -> mismatchPanic
|
||||
TC.TCon (TC.TC TC.TCIntMod) [typeNum -> Just n] ->
|
||||
case val of
|
||||
VInteger i -> pure (IntegerModulo i n)
|
||||
_ -> mismatchPanic
|
||||
TC.TCon (TC.TC TC.TCSeq) [TC.tNoUser -> len, TC.tNoUser -> contents]
|
||||
| len == TC.tZero ->
|
||||
return Unit
|
||||
| contents == TC.TCon (TC.TC TC.TCBit) []
|
||||
, VWord _ wv <- val ->
|
||||
do BV w v <- wv >>= asWordVal C.Concrete
|
||||
return $ Num Hex (T.pack $ showHex v "") w
|
||||
| TC.TCon (TC.TC (TC.TCNum k)) [] <- len
|
||||
, VSeq _l (enumerateSeqMap k -> vs) <- val ->
|
||||
Sequence <$> mapM (>>= readBack prims contents) vs
|
||||
other -> liftIO $ throwIO (invalidType other)
|
||||
where
|
||||
mismatchPanic =
|
||||
error $ "Internal error: readBack: value '" <>
|
||||
show val <>
|
||||
"' didn't match type '" <>
|
||||
show ty <>
|
||||
"'"
|
||||
|
||||
|
||||
observe :: Eval a -> Method ServerState a
|
||||
observe e = liftIO (runEval e)
|
||||
|
||||
mkEApp :: Expr PName -> [Expr PName] -> Expr PName
|
||||
mkEApp f args = foldl EApp f args
|
206
cryptol-remote-api/src/CryptolServer/Data/Type.hs
Normal file
206
cryptol-remote-api/src/CryptolServer/Data/Type.hs
Normal file
@ -0,0 +1,206 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.Data.Type
|
||||
( JSONSchema(..)
|
||||
, JSONType(..)
|
||||
) where
|
||||
|
||||
import qualified Data.Aeson as JSON
|
||||
import Data.Aeson ((.=))
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Cryptol.Parser.Selector (ppSelector)
|
||||
import Cryptol.TypeCheck.PP (NameMap, emptyNameMap, ppWithNames)
|
||||
import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf)
|
||||
import Cryptol.Utils.PP (pp)
|
||||
import Cryptol.Utils.RecordMap (canonicalFields)
|
||||
|
||||
|
||||
newtype JSONSchema = JSONSchema Schema
|
||||
|
||||
data JSONType = JSONType NameMap Type
|
||||
|
||||
newtype JSONKind = JSONKind Kind
|
||||
|
||||
instance JSON.ToJSON JSONSchema where
|
||||
toJSON (JSONSchema (Forall vars props ty)) =
|
||||
let ns = addTNames vars emptyNameMap
|
||||
in JSON.object [ "forall" .=
|
||||
[JSON.object
|
||||
[ "name" .= show (ppWithNames ns v)
|
||||
, "kind" .= JSONKind (kindOf v)
|
||||
]
|
||||
| v@(TParam _uniq _k _flav _info) <- vars
|
||||
]
|
||||
, "propositions" .= map (JSON.toJSON . JSONType ns) props
|
||||
, "type" .= JSONType ns ty
|
||||
]
|
||||
|
||||
instance JSON.ToJSON JSONKind where
|
||||
toJSON (JSONKind k) = convert k
|
||||
where
|
||||
convert KType = "Type"
|
||||
convert KNum = "Num"
|
||||
convert KProp = "Prop"
|
||||
convert (k1 :-> k2) =
|
||||
JSON.object [ "kind" .= T.pack "arrow"
|
||||
, "from" .= convert k1
|
||||
, "to" .= convert k2
|
||||
]
|
||||
|
||||
instance JSON.ToJSON JSONType where
|
||||
toJSON (JSONType ns t) = convert t
|
||||
where
|
||||
convert (TCon (TError _ _) _) =
|
||||
-- TODO: figure out what to do in this situation
|
||||
error "JSON conversion of errors is not yet supported"
|
||||
convert (TCon (TC tc) args) =
|
||||
JSON.object $
|
||||
case (tc, args) of
|
||||
(TCNum n, []) ->
|
||||
[ "type" .= T.pack "number" , "value" .= n ]
|
||||
(TCInf, []) -> ["type" .= T.pack "inf"]
|
||||
(TCBit, []) -> ["type" .= T.pack "Bit"]
|
||||
(TCInteger, []) -> ["type" .= T.pack "Integer"]
|
||||
(TCIntMod, [n]) -> [ "type" .= T.pack "Z"
|
||||
, "modulus" .= JSONType ns n
|
||||
]
|
||||
(TCSeq, [t1, TCon (TC TCBit) []]) ->
|
||||
[ "type" .= T.pack "bitvector"
|
||||
, "width" .= JSONType ns t1
|
||||
]
|
||||
(TCSeq, [t1, t2]) ->
|
||||
[ "type" .= T.pack "sequence"
|
||||
, "length" .= JSONType ns t1
|
||||
, "contents" .= JSONType ns t2
|
||||
]
|
||||
(TCFun, [t1, t2]) ->
|
||||
[ "type" .= T.pack "function"
|
||||
, "domain" .= JSONType ns t1
|
||||
, "range" .= JSONType ns t2
|
||||
]
|
||||
(TCTuple _ , []) ->
|
||||
[ "type" .= T.pack "unit" ]
|
||||
(TCTuple _, fs) ->
|
||||
[ "type" .= T.pack "tuple"
|
||||
, "contents" .= map (JSONType ns) fs
|
||||
]
|
||||
(TCRational, []) ->
|
||||
[ "type" .= T.pack "Rational"]
|
||||
(other, otherArgs) ->
|
||||
[ "type" .= T.pack "unknown"
|
||||
, "constructor" .= show other
|
||||
, "arguments" .= show otherArgs
|
||||
]
|
||||
convert (TCon (TF tf) args) =
|
||||
JSON.object
|
||||
[ "type" .= T.pack t'
|
||||
, "arguments" .= map (JSONType ns) args
|
||||
]
|
||||
where
|
||||
t' =
|
||||
case tf of
|
||||
TCAdd -> "+"
|
||||
TCSub -> "-"
|
||||
TCMul -> "*"
|
||||
TCDiv -> "/"
|
||||
TCMod -> "%"
|
||||
TCExp -> "^^"
|
||||
TCWidth -> "width"
|
||||
TCMin -> "min"
|
||||
TCMax -> "max"
|
||||
TCCeilDiv -> "/^"
|
||||
TCCeilMod -> "%^"
|
||||
TCLenFromThenTo -> "lengthFromThenTo"
|
||||
convert (TCon (PC pc) args) =
|
||||
JSON.object $
|
||||
case (pc, args) of
|
||||
(PEqual, [t1, t2]) ->
|
||||
[ "prop" .= T.pack "=="
|
||||
, "left" .= JSONType ns t1
|
||||
, "right" .= JSONType ns t2
|
||||
]
|
||||
(PNeq, [t1, t2]) ->
|
||||
[ "prop" .= T.pack "!="
|
||||
, "left" .= JSONType ns t1
|
||||
, "right" .= JSONType ns t2
|
||||
]
|
||||
(PGeq, [t1, t2]) ->
|
||||
[ "prop" .= T.pack ">="
|
||||
, "greater" .= JSONType ns t1
|
||||
, "less" .= JSONType ns t2
|
||||
]
|
||||
(PFin, [t']) ->
|
||||
[ "prop" .= T.pack "fin"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PHas x, [t1, t2]) ->
|
||||
[ "prop" .= T.pack "has"
|
||||
, "selector" .= show (ppSelector x)
|
||||
, "type" .= JSONType ns t1
|
||||
, "is" .= JSONType ns t2
|
||||
]
|
||||
(PRing, [t']) ->
|
||||
[ "prop" .= T.pack "Ring"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PField, [t']) ->
|
||||
[ "prop" .= T.pack "Field"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PRound, [t']) ->
|
||||
[ "prop" .= T.pack "Round"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PIntegral, [t']) ->
|
||||
[ "prop" .= T.pack "Integral"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PCmp, [t']) ->
|
||||
[ "prop" .= T.pack "Cmp"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PSignedCmp, [t']) ->
|
||||
[ "prop" .= T.pack "SignedCmp"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PLiteral, [t1, t2]) ->
|
||||
[ "prop" .= T.pack "Literal"
|
||||
, "size" .= JSONType ns t1
|
||||
, "subject" .= JSONType ns t2
|
||||
]
|
||||
(PZero, [t']) ->
|
||||
[ "prop" .= T.pack "Zero"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PLogic, [t']) ->
|
||||
[ "prop" .= T.pack "Logic"
|
||||
, "subject" .= JSONType ns t'
|
||||
]
|
||||
(PTrue, []) ->
|
||||
[ "prop" .= T.pack "True"
|
||||
]
|
||||
(PAnd, [t1, t2]) ->
|
||||
[ "prop" .= T.pack "And"
|
||||
, "left" .= JSONType ns t1
|
||||
, "right" .= JSONType ns t2
|
||||
]
|
||||
(pc', args') ->
|
||||
[ "prop" .= T.pack "unknown"
|
||||
, "constructor" .= show pc'
|
||||
, "arguments" .= show args'
|
||||
]
|
||||
convert (TVar v) =
|
||||
JSON.object
|
||||
[ "type" .= T.pack "variable"
|
||||
, "kind" .= JSONKind (kindOf v)
|
||||
, "name" .= show (ppWithNames ns v)
|
||||
]
|
||||
convert (TUser _n _args def) = convert def
|
||||
convert (TRec fields) =
|
||||
JSON.object
|
||||
[ "type" .= T.pack "record"
|
||||
, "fields" .=
|
||||
JSON.object [ T.pack (show (pp f)) .= JSONType ns t'
|
||||
| (f, t') <- canonicalFields fields
|
||||
]
|
||||
]
|
55
cryptol-remote-api/src/CryptolServer/EvalExpr.hs
Normal file
55
cryptol-remote-api/src/CryptolServer/EvalExpr.hs
Normal file
@ -0,0 +1,55 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.EvalExpr (evalExpression, EvalExprParams(..)) where
|
||||
|
||||
import Control.Lens hiding ((.=))
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Aeson as JSON
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem (checkExpr, evalExpr, getPrimMap)
|
||||
import Cryptol.ModuleSystem.Env (meSolverConfig)
|
||||
import Cryptol.TypeCheck.AST (sType)
|
||||
import Cryptol.TypeCheck.Solve (defaultReplExpr)
|
||||
import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
|
||||
import Cryptol.TypeCheck.Type (Schema(..))
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
import Cryptol.Utils.PP (pretty)
|
||||
|
||||
import Argo
|
||||
import CryptolServer
|
||||
import CryptolServer.Data.Expression
|
||||
import CryptolServer.Data.Type
|
||||
import CryptolServer.Exceptions
|
||||
|
||||
evalExpression :: EvalExprParams -> Method ServerState JSON.Value
|
||||
evalExpression (EvalExprParams jsonExpr) =
|
||||
do e <- getExpr jsonExpr
|
||||
(_expr, ty, schema) <- runModuleCmd (checkExpr e)
|
||||
-- TODO: see Cryptol REPL for how to check whether we
|
||||
-- can actually evaluate things, which we can't do in
|
||||
-- a parameterized module
|
||||
me <- view moduleEnv <$> getState
|
||||
let cfg = meSolverConfig me
|
||||
perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema)
|
||||
case perhapsDef of
|
||||
Nothing ->
|
||||
raise (evalPolyErr schema)
|
||||
Just (tys, checked) ->
|
||||
do -- TODO: warnDefaults here
|
||||
let su = listParamSubst tys
|
||||
let theType = apSubst su (sType schema)
|
||||
res <- runModuleCmd (evalExpr checked)
|
||||
prims <- runModuleCmd getPrimMap
|
||||
val <- observe $ readBack prims theType res
|
||||
return (JSON.object [ "value" .= val
|
||||
, "type string" .= pretty theType
|
||||
, "type" .= JSONSchema (Forall [] [] theType)
|
||||
])
|
||||
|
||||
newtype EvalExprParams =
|
||||
EvalExprParams Expression
|
||||
|
||||
instance JSON.FromJSON EvalExprParams where
|
||||
parseJSON =
|
||||
JSON.withObject "params for \"evaluate expression\"" $
|
||||
\o -> EvalExprParams <$> o .: "expression"
|
209
cryptol-remote-api/src/CryptolServer/Exceptions.hs
Normal file
209
cryptol-remote-api/src/CryptolServer/Exceptions.hs
Normal file
@ -0,0 +1,209 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.Exceptions
|
||||
( dirNotFound
|
||||
, invalidBase64
|
||||
, invalidHex
|
||||
, invalidType
|
||||
, unwantedDefaults
|
||||
, evalInParamMod
|
||||
, evalPolyErr
|
||||
, proverError
|
||||
, cryptolParseErr
|
||||
, cryptolError
|
||||
) where
|
||||
|
||||
import qualified Data.Aeson as JSON
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Vector as Vector
|
||||
|
||||
import Cryptol.ModuleSystem (ModuleError(..), ModuleWarning(..))
|
||||
import Cryptol.Utils.PP (pretty, PP)
|
||||
|
||||
import Data.Aeson hiding (Encoding, Value, decode)
|
||||
import Data.ByteString (ByteString)
|
||||
import qualified Data.ByteString.Char8 as B8
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.HashMap.Strict as HashMap
|
||||
|
||||
import Cryptol.ModuleSystem.Name (Name)
|
||||
import Cryptol.Parser
|
||||
import qualified Cryptol.TypeCheck.Type as TC
|
||||
|
||||
import Argo
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
cryptolError :: ModuleError -> [ModuleWarning] -> JSONRPCException
|
||||
cryptolError modErr warns =
|
||||
makeJSONRPCException
|
||||
errorNum
|
||||
(Text.pack $ (pretty modErr) <> foldMap (\w -> "\n" <> pretty w) warns)
|
||||
(Just . JSON.object $ errorData ++ [("warnings", moduleWarnings warns)])
|
||||
where
|
||||
-- TODO: make sub-errors (parse, typecheck, etc.) into structured data so
|
||||
-- that another client can parse them and make use of them (possible
|
||||
-- locations noted below)
|
||||
|
||||
(errorNum, errorData) = moduleError modErr
|
||||
|
||||
moduleError err = case err of
|
||||
ModuleNotFound src path ->
|
||||
(20500, [ ("source", jsonPretty src)
|
||||
, ("path", jsonList (map jsonString path))
|
||||
])
|
||||
CantFindFile path ->
|
||||
(20050, [ ("path", jsonString path)
|
||||
])
|
||||
BadUtf8 path ue ->
|
||||
(20010, [ ("path", jsonShow path)
|
||||
, ("error", jsonShow ue)
|
||||
])
|
||||
OtherIOError path exn ->
|
||||
(20060, [ ("path", jsonString path)
|
||||
, ("error", jsonShow exn)
|
||||
])
|
||||
ModuleParseError source message ->
|
||||
(20540, [ ("source", jsonShow source)
|
||||
, ("error", jsonShow message)
|
||||
])
|
||||
RecursiveModules mods ->
|
||||
(20550, [ ("modules", jsonList (reverse (map jsonPretty mods)))
|
||||
])
|
||||
RenamerErrors src errs ->
|
||||
-- TODO: structured error here
|
||||
(20700, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonList (map jsonPretty errs))
|
||||
])
|
||||
NoPatErrors src errs ->
|
||||
-- TODO: structured error here
|
||||
(20710, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonList (map jsonPretty errs))
|
||||
])
|
||||
NoIncludeErrors src errs ->
|
||||
-- TODO: structured error here
|
||||
(20720, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonList (map jsonShow errs))
|
||||
])
|
||||
TypeCheckingFailed src errs ->
|
||||
-- TODO: structured error here
|
||||
(20730, [ ("source", jsonPretty src)
|
||||
, ("errors", jsonList (map jsonShow errs))
|
||||
])
|
||||
ModuleNameMismatch expected found ->
|
||||
(20600, [ ("expected", jsonPretty expected)
|
||||
, ("found", jsonPretty found)
|
||||
])
|
||||
DuplicateModuleName name path1 path2 ->
|
||||
(20610, [ ("name", jsonPretty name)
|
||||
, ("paths", jsonList [jsonString path1, jsonString path2])
|
||||
])
|
||||
ImportedParamModule x ->
|
||||
(20630, [ ("module", jsonPretty x)
|
||||
])
|
||||
FailedToParameterizeModDefs x xs ->
|
||||
(20640, [ ("module", jsonPretty x)
|
||||
, ("parameters", jsonList (map (jsonString . pretty) xs))
|
||||
])
|
||||
NotAParameterizedModule x ->
|
||||
(20650, [ ("module", jsonPretty x)
|
||||
])
|
||||
OtherFailure x ->
|
||||
(29999, [ ("error", jsonString x)
|
||||
])
|
||||
ErrorInFile x y ->
|
||||
(n, ("path", jsonShow x) : e)
|
||||
where (n, e) = moduleError y
|
||||
|
||||
moduleWarnings :: [ModuleWarning] -> JSON.Value
|
||||
moduleWarnings =
|
||||
-- TODO: structured error here
|
||||
jsonList . concatMap
|
||||
(\w -> case w of
|
||||
TypeCheckWarnings tcwarns ->
|
||||
map (jsonPretty . snd) tcwarns
|
||||
RenamerWarnings rnwarns ->
|
||||
map jsonPretty rnwarns)
|
||||
|
||||
-- Some little helpers for common ways of building JSON values in the above:
|
||||
|
||||
jsonString :: String -> JSON.Value
|
||||
jsonString = JSON.String . Text.pack
|
||||
|
||||
jsonPretty :: PP a => a -> JSON.Value
|
||||
jsonPretty = jsonString . pretty
|
||||
|
||||
jsonShow :: Show a => a -> JSON.Value
|
||||
jsonShow = jsonString . show
|
||||
|
||||
jsonList :: [JSON.Value] -> JSON.Value
|
||||
jsonList = JSON.Array . Vector.fromList
|
||||
|
||||
dirNotFound :: FilePath -> JSONRPCException
|
||||
dirNotFound dir =
|
||||
makeJSONRPCException
|
||||
20051 (T.pack ("Directory doesn't exist: " <> dir))
|
||||
(Just (JSON.object ["path" .= dir]))
|
||||
|
||||
invalidBase64 :: ByteString -> String -> JSONRPCException
|
||||
invalidBase64 invalidData msg =
|
||||
makeJSONRPCException
|
||||
20020 (T.pack msg)
|
||||
(Just (JSON.object ["input" .= B8.unpack invalidData]))
|
||||
|
||||
invalidHex :: Char -> JSONRPCException
|
||||
invalidHex invalidData =
|
||||
makeJSONRPCException
|
||||
20030 "Not a hex digit"
|
||||
(Just (JSON.object ["input" .= T.singleton invalidData]))
|
||||
|
||||
invalidType :: TC.Type -> JSONRPCException
|
||||
invalidType ty =
|
||||
makeJSONRPCException
|
||||
20040 "Can't convert Cryptol data from this type to JSON"
|
||||
(Just (jsonTypeAndString ty))
|
||||
|
||||
unwantedDefaults :: [(TC.TParam, TC.Type)] -> JSONRPCException
|
||||
unwantedDefaults defs =
|
||||
makeJSONRPCException
|
||||
20210 "Execution would have required these defaults"
|
||||
(Just (JSON.object ["defaults" .=
|
||||
[ jsonTypeAndString ty <> HashMap.fromList ["parameter" .= pretty param]
|
||||
| (param, ty) <- defs ] ]))
|
||||
|
||||
evalInParamMod :: [Cryptol.ModuleSystem.Name.Name] -> JSONRPCException
|
||||
evalInParamMod mods =
|
||||
makeJSONRPCException
|
||||
20220 "Can't evaluate Cryptol in a parameterized module."
|
||||
(Just (JSON.object ["modules" .= map pretty mods]))
|
||||
|
||||
evalPolyErr ::
|
||||
TC.Schema {- ^ the type that was too polymorphic -} ->
|
||||
JSONRPCException
|
||||
evalPolyErr schema =
|
||||
makeJSONRPCException
|
||||
20200 "Can't evaluate at polymorphic type"
|
||||
(Just (JSON.object [ "type" .= JSONSchema schema
|
||||
, "type string" .= pretty schema ]))
|
||||
|
||||
proverError :: String -> JSONRPCException
|
||||
proverError msg =
|
||||
makeJSONRPCException
|
||||
20230 "Prover error"
|
||||
(Just (JSON.object ["error" .= msg]))
|
||||
|
||||
cryptolParseErr ::
|
||||
Text {- ^ the input that couldn't be parsed -} ->
|
||||
ParseError {- ^ the parse error from Cryptol -} ->
|
||||
JSONRPCException
|
||||
cryptolParseErr expr err =
|
||||
makeJSONRPCException
|
||||
20000 "Cryptol parse error"
|
||||
(Just $ JSON.object ["input" .= expr, "error" .= show err])
|
||||
|
||||
-- The standard way of presenting a type: a structured type, plus a
|
||||
-- human-readable string
|
||||
jsonTypeAndString :: TC.Type -> JSON.Object
|
||||
jsonTypeAndString ty =
|
||||
HashMap.fromList
|
||||
[ "type" .= JSONSchema (TC.Forall [] [] ty)
|
||||
, "type string" .= pretty ty ]
|
30
cryptol-remote-api/src/CryptolServer/FocusedModule.hs
Normal file
30
cryptol-remote-api/src/CryptolServer/FocusedModule.hs
Normal file
@ -0,0 +1,30 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.FocusedModule (focusedModule, FocusedModParams(..)) where
|
||||
|
||||
import Control.Lens hiding ((.=))
|
||||
import Data.Aeson as JSON
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem (meFocusedModule, meLoadedModules)
|
||||
import Cryptol.ModuleSystem.Env (isLoadedParamMod)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
import Argo
|
||||
import CryptolServer
|
||||
|
||||
focusedModule :: FocusedModParams -> Method ServerState JSON.Value
|
||||
focusedModule _ =
|
||||
do me <- view moduleEnv <$> getState
|
||||
case meFocusedModule me of
|
||||
Nothing ->
|
||||
return $ JSON.object [ "module" .= JSON.Null ]
|
||||
Just name ->
|
||||
do let parameterized = isLoadedParamMod name (meLoadedModules me)
|
||||
return $ JSON.object [ "module" .= pretty name
|
||||
, "parameterized" .= parameterized
|
||||
]
|
||||
|
||||
data FocusedModParams = FocusedModParams
|
||||
|
||||
instance JSON.FromJSON FocusedModParams where
|
||||
parseJSON _ = pure FocusedModParams
|
55
cryptol-remote-api/src/CryptolServer/LoadModule.hs
Normal file
55
cryptol-remote-api/src/CryptolServer/LoadModule.hs
Normal file
@ -0,0 +1,55 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.LoadModule
|
||||
( loadFile
|
||||
, loadModule
|
||||
, LoadFileParams(..)
|
||||
, LoadModuleParams(..)
|
||||
) where
|
||||
|
||||
import Control.Applicative
|
||||
import Data.Aeson as JSON
|
||||
import qualified Data.Text as T
|
||||
import Data.Functor
|
||||
|
||||
import Cryptol.ModuleSystem (loadModuleByPath, loadModuleByName)
|
||||
import Cryptol.Parser (parseModName)
|
||||
import Cryptol.Parser.AST (ModName)
|
||||
|
||||
import CryptolServer
|
||||
import Argo
|
||||
|
||||
|
||||
loadFile :: LoadFileParams -> Method ServerState ()
|
||||
loadFile (LoadFileParams fn) =
|
||||
void $ runModuleCmd (loadModuleByPath fn)
|
||||
|
||||
newtype LoadFileParams
|
||||
= LoadFileParams FilePath
|
||||
|
||||
instance JSON.FromJSON LoadFileParams where
|
||||
parseJSON =
|
||||
JSON.withObject "params for \"load module\"" $
|
||||
\o -> LoadFileParams <$> o .: "file"
|
||||
|
||||
loadModule :: LoadModuleParams -> Method ServerState ()
|
||||
loadModule (LoadModuleParams mn) =
|
||||
void $ runModuleCmd (loadModuleByName mn)
|
||||
|
||||
newtype JSONModuleName
|
||||
= JSONModuleName { unJSONModName :: ModName }
|
||||
|
||||
instance JSON.FromJSON JSONModuleName where
|
||||
parseJSON =
|
||||
JSON.withText "module name" $
|
||||
\txt ->
|
||||
case parseModName (T.unpack txt) of
|
||||
Nothing -> empty
|
||||
Just n -> return (JSONModuleName n)
|
||||
|
||||
newtype LoadModuleParams
|
||||
= LoadModuleParams ModName
|
||||
|
||||
instance JSON.FromJSON LoadModuleParams where
|
||||
parseJSON =
|
||||
JSON.withObject "params for \"load module\"" $
|
||||
\o -> LoadModuleParams . unJSONModName <$> o .: "module name"
|
61
cryptol-remote-api/src/CryptolServer/Names.hs
Normal file
61
cryptol-remote-api/src/CryptolServer/Names.hs
Normal file
@ -0,0 +1,61 @@
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.Names (visibleNames) where
|
||||
|
||||
import Control.Lens hiding ((.=))
|
||||
import qualified Data.Aeson as JSON
|
||||
import Data.Aeson ((.=))
|
||||
import qualified Data.Map as Map
|
||||
import Data.Map (Map)
|
||||
import Data.Text (unpack)
|
||||
|
||||
import Cryptol.Parser.Name (PName(..))
|
||||
import Cryptol.ModuleSystem.Env (ModContext(..), ModuleEnv(..), DynamicEnv(..), focusedEnv)
|
||||
import Cryptol.ModuleSystem.Interface (IfaceDecl(..), IfaceDecls(..))
|
||||
import Cryptol.ModuleSystem.Name (Name)
|
||||
import Cryptol.ModuleSystem.NamingEnv (NamingEnv(..), lookupValNames, shadowing)
|
||||
import Cryptol.TypeCheck.Type (Schema(..))
|
||||
import Cryptol.Utils.PP (pp)
|
||||
|
||||
import Argo
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
|
||||
visibleNames :: JSON.Value -> Method ServerState [NameInfo]
|
||||
visibleNames _ =
|
||||
do me <- view moduleEnv <$> getState
|
||||
let DEnv { deNames = dyNames } = meDynEnv me
|
||||
let ModContext { mctxDecls = fDecls, mctxNames = fNames} = focusedEnv me
|
||||
let inScope = Map.keys (neExprs $ dyNames `shadowing` fNames)
|
||||
return $ concatMap (getInfo fNames (ifDecls fDecls)) inScope
|
||||
|
||||
getInfo :: NamingEnv -> Map Name IfaceDecl -> PName -> [NameInfo]
|
||||
getInfo rnEnv info n' =
|
||||
[ case Map.lookup n info of
|
||||
Nothing -> error $ "Name not found, but should have been: " ++ show n
|
||||
Just i ->
|
||||
let ty = ifDeclSig i
|
||||
nameDocs = ifDeclDoc i
|
||||
in NameInfo (show (pp n')) (show (pp ty)) ty (unpack <$> nameDocs)
|
||||
| n <- lookupValNames n' rnEnv
|
||||
]
|
||||
|
||||
data NameInfo =
|
||||
NameInfo
|
||||
{ name :: String
|
||||
, typeSig :: String
|
||||
, schema :: Schema
|
||||
, nameDocs :: Maybe String
|
||||
}
|
||||
|
||||
instance JSON.ToJSON NameInfo where
|
||||
toJSON (NameInfo{name, typeSig, schema, nameDocs}) =
|
||||
JSON.object $
|
||||
[ "name" .= name
|
||||
, "type string" .= typeSig
|
||||
, "type" .= JSON.toJSON (JSONSchema schema)
|
||||
] ++
|
||||
maybe [] (\d -> ["documentation" .= d]) nameDocs
|
132
cryptol-remote-api/src/CryptolServer/Sat.hs
Normal file
132
cryptol-remote-api/src/CryptolServer/Sat.hs
Normal file
@ -0,0 +1,132 @@
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.Sat (sat, ProveSatParams(..)) where
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Lens hiding ((.=))
|
||||
import Control.Monad.IO.Class
|
||||
import Data.Aeson ((.=), (.:), FromJSON, ToJSON)
|
||||
import qualified Data.Aeson as JSON
|
||||
import Data.IORef
|
||||
import Data.Scientific (floatingOrInteger)
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
|
||||
import Cryptol.Eval.Concrete.Value (Value)
|
||||
import Cryptol.ModuleSystem (checkExpr, getPrimMap)
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), meDynEnv, meSolverConfig)
|
||||
import Cryptol.Symbolic (ProverCommand(..), ProverResult(..), QueryType(..), SatNum(..))
|
||||
import Cryptol.Symbolic.SBV (proverNames, satProve, setupProver)
|
||||
import Cryptol.TypeCheck.AST (Expr, Type)
|
||||
import Cryptol.TypeCheck.Solve (defaultReplExpr)
|
||||
import qualified Cryptol.TypeCheck.Solver.SMT as SMT
|
||||
|
||||
import Argo
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions (evalPolyErr, proverError)
|
||||
import CryptolServer.Data.Expression
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
sat :: ProveSatParams -> Method ServerState SatResult
|
||||
sat (ProveSatParams (Prover name) jsonExpr num) =
|
||||
do e <- getExpr jsonExpr
|
||||
(_expr, ty, schema) <- runModuleCmd (checkExpr e)
|
||||
-- TODO validEvalContext expr, ty, schema
|
||||
me <- view moduleEnv <$> getState
|
||||
let decls = deDecls (meDynEnv me)
|
||||
let cfg = meSolverConfig me
|
||||
perhapsDef <- liftIO $ SMT.withSolver cfg (\s -> defaultReplExpr s ty schema)
|
||||
case perhapsDef of
|
||||
Nothing ->
|
||||
raise (evalPolyErr schema)
|
||||
Just (_tys, checked) ->
|
||||
do timing <- liftIO $ newIORef 0
|
||||
let cmd =
|
||||
ProverCommand
|
||||
{ pcQueryType = SatQuery num
|
||||
, pcProverName = name
|
||||
, pcVerbose = True -- verbose
|
||||
, pcProverStats = timing
|
||||
, pcExtraDecls = decls
|
||||
, pcSmtFile = Nothing -- mfile
|
||||
, pcExpr = checked
|
||||
, pcSchema = schema
|
||||
, pcValidate = False
|
||||
, pcIgnoreSafety = False
|
||||
}
|
||||
sbvCfg <- liftIO (setupProver name) >>= \case
|
||||
Left msg -> error msg
|
||||
Right (_ws, sbvCfg) -> return sbvCfg
|
||||
(_firstProver, res) <- runModuleCmd $ satProve sbvCfg cmd
|
||||
_stats <- liftIO (readIORef timing)
|
||||
case res of
|
||||
ProverError msg -> raise (proverError msg)
|
||||
EmptyResult -> error "got empty result for online prover!"
|
||||
ThmResult _ts -> pure Unsatisfiable
|
||||
AllSatResult results ->
|
||||
Satisfied <$> traverse satResult results
|
||||
|
||||
where
|
||||
satResult :: [(Type, Expr, Value)] -> Method ServerState [(JSONType, Expression)]
|
||||
satResult es = traverse result es
|
||||
|
||||
result (t, _, v) =
|
||||
do prims <- runModuleCmd getPrimMap
|
||||
e <- observe $ readBack prims t v
|
||||
return (JSONType mempty t, e)
|
||||
|
||||
data SatResult = Unsatisfiable | Satisfied [[(JSONType, Expression)]]
|
||||
|
||||
instance ToJSON SatResult where
|
||||
toJSON Unsatisfiable = JSON.object ["result" .= ("unsatisfiable" :: Text)]
|
||||
toJSON (Satisfied xs) =
|
||||
JSON.object [ "result" .= ("satisfied" :: Text)
|
||||
, "model" .=
|
||||
[ [ JSON.object [ "type" .= t
|
||||
, "expr" .= e
|
||||
]
|
||||
| (t, e) <- res
|
||||
]
|
||||
| res <- xs
|
||||
]
|
||||
]
|
||||
|
||||
|
||||
newtype Prover = Prover String
|
||||
|
||||
instance FromJSON Prover where
|
||||
parseJSON =
|
||||
JSON.withText "prover name" $
|
||||
\txt ->
|
||||
let str = T.unpack txt
|
||||
in if str `elem` proverNames
|
||||
then return (Prover str)
|
||||
else empty
|
||||
|
||||
|
||||
data ProveSatParams =
|
||||
ProveSatParams
|
||||
{ prover :: Prover
|
||||
, expression :: Expression
|
||||
, numResults :: SatNum
|
||||
}
|
||||
|
||||
instance FromJSON ProveSatParams where
|
||||
parseJSON =
|
||||
JSON.withObject "sat or prove parameters" $
|
||||
\o ->
|
||||
do prover <- o .: "prover"
|
||||
expression <- o .: "expression"
|
||||
numResults <- (o .: "result count" >>= num)
|
||||
pure ProveSatParams{prover, expression, numResults}
|
||||
where
|
||||
num v = ((JSON.withText "all" $
|
||||
\t -> if t == "all" then pure AllSat else empty) v) <|>
|
||||
((JSON.withScientific "count" $
|
||||
\s ->
|
||||
case floatingOrInteger s of
|
||||
Left (_float :: Double) -> empty
|
||||
Right int -> pure (SomeSat int)) v)
|
36
cryptol-remote-api/src/CryptolServer/TypeCheck.hs
Normal file
36
cryptol-remote-api/src/CryptolServer/TypeCheck.hs
Normal file
@ -0,0 +1,36 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
module CryptolServer.TypeCheck (checkType, TypeCheckParams(..)) where
|
||||
|
||||
import Control.Lens hiding ((.=))
|
||||
import Data.Aeson as JSON
|
||||
|
||||
|
||||
import Cryptol.ModuleSystem (checkExpr)
|
||||
import Cryptol.ModuleSystem.Env (meSolverConfig)
|
||||
|
||||
import Argo
|
||||
|
||||
import CryptolServer
|
||||
import CryptolServer.Exceptions
|
||||
import CryptolServer.Data.Expression
|
||||
import CryptolServer.Data.Type
|
||||
|
||||
checkType :: TypeCheckParams -> Method ServerState JSON.Value
|
||||
checkType (TypeCheckParams e) =
|
||||
do e' <- getExpr e
|
||||
(_expr, _ty, schema) <- runModuleCmd (checkExpr e')
|
||||
-- FIXME: why are we running this command if the result isn't used?
|
||||
_cfg <- meSolverConfig . view moduleEnv <$> getState
|
||||
return (JSON.object [ "type schema" .= JSONSchema schema ])
|
||||
where
|
||||
-- FIXME: Why is this check not being used?
|
||||
_noDefaults [] = return ()
|
||||
_noDefaults xs@(_:_) = raise (unwantedDefaults xs)
|
||||
|
||||
newtype TypeCheckParams =
|
||||
TypeCheckParams Expression
|
||||
|
||||
instance JSON.FromJSON TypeCheckParams where
|
||||
parseJSON =
|
||||
JSON.withObject "params for \"check type\"" $
|
||||
\o -> TypeCheckParams <$> o .: "expression"
|
17
cryptol-remote-api/test-scripts/Foo.cry
Normal file
17
cryptol-remote-api/test-scripts/Foo.cry
Normal file
@ -0,0 +1,17 @@
|
||||
module Foo where
|
||||
|
||||
id : {a} a -> a
|
||||
id x = x
|
||||
|
||||
x : [8]
|
||||
x = 255
|
||||
|
||||
add : {a} (fin a) => [a] -> [a] -> [a]
|
||||
add = (+)
|
||||
|
||||
foo : {foo : [32], bar : [32]}
|
||||
foo = {foo = 23, bar = 99}
|
||||
|
||||
getFoo : {foo : [32], bar : [32]} -> [32]
|
||||
getFoo x = x.foo
|
||||
|
4
cryptol-remote-api/test-scripts/Inst.cry
Normal file
4
cryptol-remote-api/test-scripts/Inst.cry
Normal file
@ -0,0 +1,4 @@
|
||||
module Inst =
|
||||
Param where
|
||||
type w = 8
|
||||
|
8
cryptol-remote-api/test-scripts/Param.cry
Normal file
8
cryptol-remote-api/test-scripts/Param.cry
Normal file
@ -0,0 +1,8 @@
|
||||
module Param where
|
||||
parameter
|
||||
type w : #
|
||||
type constraint (fin w)
|
||||
|
||||
foo : [w] -> [2 * w]
|
||||
foo x = x # x
|
||||
|
23
cryptol-remote-api/test-scripts/cryptol-api_test.py
Normal file
23
cryptol-remote-api/test-scripts/cryptol-api_test.py
Normal file
@ -0,0 +1,23 @@
|
||||
import os
|
||||
|
||||
from cryptol import CryptolConnection, CryptolContext, cry
|
||||
import cryptol
|
||||
import cryptol.cryptoltypes
|
||||
|
||||
dir_path = os.path.dirname(os.path.realpath(__file__))
|
||||
|
||||
c = cryptol.connect("cabal new-exec --verbose=0 cryptol-remote-api")
|
||||
|
||||
c.change_directory(dir_path)
|
||||
|
||||
c.load_file("Foo.cry")
|
||||
|
||||
val = c.evaluate_expression("x").result()
|
||||
|
||||
assert c.call('add', b'\0', b'\1').result() == b'\x01'
|
||||
assert c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result() == bytes.fromhex('02')
|
||||
|
||||
|
||||
cryptol.add_cryptol_module('Foo', c)
|
||||
from Foo import *
|
||||
assert add(b'\2', 2) == b'\4'
|
175
cryptol-remote-api/test-scripts/cryptol-tests.py
Normal file
175
cryptol-remote-api/test-scripts/cryptol-tests.py
Normal file
@ -0,0 +1,175 @@
|
||||
import os
|
||||
from pathlib import Path
|
||||
import signal
|
||||
import subprocess
|
||||
import sys
|
||||
import time
|
||||
|
||||
import argo.connection as argo
|
||||
import cryptol
|
||||
from cryptol import CryptolConnection, CryptolContext, cry
|
||||
|
||||
dir_path = Path(os.path.dirname(os.path.realpath(__file__)))
|
||||
|
||||
cryptol_path = dir_path.joinpath('test-data')
|
||||
|
||||
|
||||
|
||||
def low_level_api_test(c):
|
||||
|
||||
id_1 = c.send_message("load module", {"module name": "M", "state": None})
|
||||
reply_1 = c.wait_for_reply_to(id_1)
|
||||
assert('result' in reply_1)
|
||||
assert('state' in reply_1['result'])
|
||||
assert('answer' in reply_1['result'])
|
||||
state_1 = reply_1['result']['state']
|
||||
|
||||
id_2 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
|
||||
reply_2 = c.wait_for_reply_to(id_2)
|
||||
assert('result' in reply_2)
|
||||
assert('answer' in reply_2['result'])
|
||||
assert('value' in reply_2['result']['answer'])
|
||||
assert(reply_2['result']['answer']['value'] ==
|
||||
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
|
||||
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
|
||||
'expression': 'sequence'})
|
||||
|
||||
id_3 = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1})
|
||||
reply_3 = c.wait_for_reply_to(id_3)
|
||||
assert('result' in reply_3)
|
||||
assert('answer' in reply_3['result'])
|
||||
assert('value' in reply_3['result']['answer'])
|
||||
assert(reply_3['result']['answer']['value'] ==
|
||||
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
|
||||
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
|
||||
'expression': 'sequence'})
|
||||
|
||||
id_4 = c.send_message("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1})
|
||||
reply_4 = c.wait_for_reply_to(id_4)
|
||||
assert('result' in reply_4)
|
||||
assert('answer' in reply_4['result'])
|
||||
assert('value' in reply_4['result']['answer'])
|
||||
assert(reply_4['result']['answer']['value'] ==
|
||||
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
|
||||
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
|
||||
'expression': 'sequence'})
|
||||
|
||||
a_record = {"expression": "record",
|
||||
"data": {"unit": "()",
|
||||
"fifteen": {"expression": "bits",
|
||||
"encoding": "hex",
|
||||
"width": 4,
|
||||
"data": "f"}}}
|
||||
|
||||
id_5 = c.send_message("evaluate expression", {"state": state_1, "expression": a_record})
|
||||
reply_5 = c.wait_for_reply_to(id_5)
|
||||
assert('result' in reply_5)
|
||||
assert('answer' in reply_5['result'])
|
||||
assert('value' in reply_5['result']['answer'])
|
||||
assert(reply_5['result']['answer']['value'] ==
|
||||
{'expression': 'record',
|
||||
'data': {'fifteen':
|
||||
{'data': 'f',
|
||||
'width': 4,
|
||||
'expression': 'bits',
|
||||
'encoding': 'hex'},
|
||||
'unit':
|
||||
{'expression': 'unit'}}})
|
||||
|
||||
id_6 = c.send_message("evaluate expression",
|
||||
{"state": state_1,
|
||||
"expression": {"expression": "let",
|
||||
"binders": [{"name": "theRecord", "definition": a_record}],
|
||||
"body": {"expression": "tuple",
|
||||
"data": [a_record, "theRecord"]}}})
|
||||
reply_6 = c.wait_for_reply_to(id_6)
|
||||
assert('result' in reply_6)
|
||||
assert('answer' in reply_6['result'])
|
||||
assert('value' in reply_6['result']['answer'])
|
||||
assert(reply_6['result']['answer']['value'] ==
|
||||
{'expression': 'tuple',
|
||||
'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
|
||||
'unit': {'expression': 'unit'}},
|
||||
'expression': 'record'},
|
||||
{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
|
||||
'unit': {'expression': 'unit'}},
|
||||
'expression': 'record'}]})
|
||||
|
||||
id_7 = c.send_message("evaluate expression",
|
||||
{"state": state_1,
|
||||
"expression": {"expression": "sequence",
|
||||
"data": [a_record, a_record]}})
|
||||
reply_7 = c.wait_for_reply_to(id_7)
|
||||
assert('result' in reply_7)
|
||||
assert('answer' in reply_7['result'])
|
||||
assert('value' in reply_7['result']['answer'])
|
||||
assert(reply_7['result']['answer']['value'] ==
|
||||
{'expression': 'sequence',
|
||||
'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
|
||||
'unit': {'expression': 'unit'}},
|
||||
'expression': 'record'},
|
||||
{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
|
||||
'unit': {'expression': 'unit'}},
|
||||
'expression': 'record'}]})
|
||||
|
||||
id_8 = c.send_message("evaluate expression",
|
||||
{"state": state_1,
|
||||
"expression": {"expression": "integer modulo",
|
||||
"integer": 14,
|
||||
"modulus": 42}})
|
||||
reply_8 = c.wait_for_reply_to(id_8)
|
||||
assert('result' in reply_8)
|
||||
assert('answer' in reply_8['result'])
|
||||
assert('value' in reply_8['result']['answer'])
|
||||
assert(reply_8['result']['answer']['value'] ==
|
||||
{"expression": "integer modulo",
|
||||
"integer": 14,
|
||||
"modulus": 42})
|
||||
|
||||
id_9 = c.send_message("evaluate expression",
|
||||
{"state": state_1,
|
||||
"expression": "m `{a=60}"})
|
||||
reply_9 = c.wait_for_reply_to(id_9)
|
||||
assert('result' in reply_9)
|
||||
assert('answer' in reply_9['result'])
|
||||
assert('value' in reply_9['result']['answer'])
|
||||
assert(reply_9['result']['answer']['value'] ==
|
||||
{"expression": "integer modulo",
|
||||
"integer": 42,
|
||||
"modulus": 60})
|
||||
|
||||
# Test with both sockets and stdio
|
||||
|
||||
c1 = argo.ServerConnection(
|
||||
cryptol.CryptolDynamicSocketProcess(
|
||||
"cabal v2-exec cryptol-remote-api --verbose=0",
|
||||
cryptol_path=cryptol_path))
|
||||
c2 = argo.ServerConnection(
|
||||
cryptol.CryptolStdIOProcess(
|
||||
"cabal v2-exec cryptol-remote-api --verbose=0 -- --stdio",
|
||||
cryptol_path=cryptol_path))
|
||||
|
||||
low_level_api_test(c1)
|
||||
low_level_api_test(c2)
|
||||
|
||||
env = os.environ.copy()
|
||||
env['CRYPTOLPATH'] = cryptol_path
|
||||
|
||||
p = subprocess.Popen(
|
||||
["cabal", "v2-exec", "cryptol-remote-api", "--verbose=0", "--", "--port", "50005"],
|
||||
stdout=subprocess.DEVNULL,
|
||||
stdin=subprocess.DEVNULL,
|
||||
stderr=subprocess.DEVNULL,
|
||||
start_new_session=True,
|
||||
env=env)
|
||||
|
||||
time.sleep(5)
|
||||
assert(p is not None)
|
||||
assert(p.poll() is None)
|
||||
|
||||
c3 = argo.ServerConnection(
|
||||
argo.RemoteSocketProcess('localhost', 50005, ipv6=True))
|
||||
|
||||
low_level_api_test(c3)
|
||||
|
||||
os.killpg(os.getpgid(p.pid), signal.SIGKILL)
|
12
cryptol-remote-api/test-scripts/test-data/M.cry
Normal file
12
cryptol-remote-api/test-scripts/test-data/M.cry
Normal file
@ -0,0 +1,12 @@
|
||||
module M where
|
||||
f : [8] -> [2][8]
|
||||
f x = repeat x
|
||||
|
||||
g : [8] -> [2][8]
|
||||
g x = [x, x]
|
||||
|
||||
h : [2][8] -> [2][8]
|
||||
h x = x
|
||||
|
||||
m : {a} (fin a, a > 42) => Z a
|
||||
m = 42
|
83
cryptol-remote-api/test/Test.hs
Normal file
83
cryptol-remote-api/test/Test.hs
Normal file
@ -0,0 +1,83 @@
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
module Main where
|
||||
|
||||
import Data.Aeson as JSON (fromJSON, toJSON, Result(..))
|
||||
|
||||
import Data.ByteString.Lazy (ByteString)
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import Data.List.NonEmpty(NonEmpty(..))
|
||||
|
||||
import Test.QuickCheck.Instances.ByteString
|
||||
import Test.QuickCheck.Instances.Scientific
|
||||
import Test.QuickCheck.Instances.Text
|
||||
import Test.Tasty
|
||||
import Test.Tasty.HUnit.ScriptExit
|
||||
import Test.Tasty.QuickCheck
|
||||
|
||||
import CryptolServer.Call
|
||||
|
||||
import Debug.Trace
|
||||
|
||||
import Argo.PythonBindings
|
||||
import Paths_cryptol_remote_api
|
||||
|
||||
main :: IO ()
|
||||
main =
|
||||
do reqs <- getArgoPythonFile "requirements.txt"
|
||||
withPython3venv (Just reqs) $ \pip python ->
|
||||
do pySrc <- getArgoPythonFile "."
|
||||
testScriptsDir <- getDataFileName "test-scripts/"
|
||||
pip ["install", pySrc]
|
||||
putStrLn "pipped"
|
||||
|
||||
scriptTests <- makeScriptTests testScriptsDir [python]
|
||||
|
||||
defaultMain $
|
||||
testGroup "Tests for saw-remote-api"
|
||||
[ testGroup "Scripting API tests" scriptTests
|
||||
, callMsgProps
|
||||
]
|
||||
|
||||
instance Arbitrary Encoding where
|
||||
arbitrary = oneof [pure Hex, pure Base64]
|
||||
|
||||
instance Arbitrary Expression where
|
||||
arbitrary = sized spec
|
||||
where
|
||||
spec n
|
||||
| n <= 0 =
|
||||
oneof [ Bit <$> arbitrary
|
||||
, pure Unit
|
||||
, Num <$> arbitrary <*> arbitrary <*> arbitrary
|
||||
, Integer <$> arbitrary
|
||||
-- NB: The following case will not generate
|
||||
-- syntactically valid Cryptol. But for testing
|
||||
-- round-tripping of the JSON, and coverage of various
|
||||
-- functions, it's better than nothing.
|
||||
, Concrete <$> arbitrary
|
||||
]
|
||||
| otherwise =
|
||||
choose (2, n) >>=
|
||||
\len ->
|
||||
let sub = n `div` len
|
||||
in
|
||||
oneof [ Record . HM.fromList <$> vectorOf len ((,) <$> arbitrary <*> spec sub)
|
||||
, Sequence <$> vectorOf len (spec sub)
|
||||
, Tuple <$> vectorOf len (spec sub)
|
||||
-- NB: Will not make valid identifiers, so if we
|
||||
-- ever insert validation, then this will need to
|
||||
-- change.
|
||||
, Let <$> vectorOf len (LetBinding <$> arbitrary <*> spec sub) <*> spec sub
|
||||
, Application <$> spec sub <*> ((:|) <$> spec sub <*> vectorOf len (spec sub))
|
||||
]
|
||||
|
||||
callMsgProps :: TestTree
|
||||
callMsgProps =
|
||||
testGroup "QuickCheck properties for the \"call\" message"
|
||||
[ testProperty "encoding and decoding arg specs is the identity" $
|
||||
\(spec :: Expression) ->
|
||||
case fromJSON (toJSON spec) of
|
||||
JSON.Success v -> spec == v
|
||||
JSON.Error err -> False
|
||||
]
|
2
deps/argo
vendored
2
deps/argo
vendored
@ -1 +1 @@
|
||||
Subproject commit 8b8c84ae0c3e61f39a6e8609b02d887ac47003f8
|
||||
Subproject commit 023a3c458668e88940e8efa675062864eefb5a67
|
Loading…
Reference in New Issue
Block a user