Merge pull request #1109 from GaloisInc/server-tweaks-bump

Server tweaks bump

cabal.project

@@ -31,5 +31,4 @@ packages:
     deps/dwarf
     deps/argo/argo
     deps/argo/tasty-script-exitcode
-    deps/argo/python
     deps/cryptol/cryptol-remote-api

saw-remote-api/saw-remote-api/Main.hs

@@ -1,25 +1,43 @@
 {-# LANGUAGE OverloadedStrings #-}
 module Main (main) where
 
-import Argo
-import Argo.DefaultMain
+import qualified Argo
+import qualified Argo.DefaultMain as Argo (defaultMain)
 import qualified Argo.Doc as Doc
 
-import SAWServer
+import SAWServer ( SAWState, initialState )
 import SAWServer.CryptolSetup
+    ( cryptolLoadModuleDescr,
+      cryptolLoadModule,
+      cryptolLoadFileDescr,
+      cryptolLoadFile )
 --import SAWServer.JVMCrucibleSetup
 --import SAWServer.JVMVerify
 import SAWServer.LLVMCrucibleSetup
+    ( llvmLoadModuleDescr, llvmLoadModule )
 import SAWServer.LLVMVerify
+    ( llvmVerifyDescr,
+      llvmVerify,
+      llvmAssumeDescr,
+      llvmAssume,
+      llvmVerifyX86Descr,
+      llvmVerifyX86 )
 import SAWServer.ProofScript
-import SAWServer.SaveTerm
-import SAWServer.SetOption
+    ( makeSimpsetDescr, makeSimpset, proveDescr, prove )
+import SAWServer.SaveTerm ( saveTermDescr, saveTerm )
+import SAWServer.SetOption ( setOptionDescr, setOption )
 
 
 main :: IO ()
-main =
-  do theApp <- mkDefaultApp "SAW RPC Server" serverDocs initialState sawMethods
-     defaultMain description theApp
+main = do
+  theApp <- Argo.mkApp
+               "SAW RPC Server"
+               serverDocs
+               (Argo.defaultAppOpts
+               Argo.MutableState)
+               initialState
+               sawMethods
+  Argo.defaultMain description theApp
 
 serverDocs :: [Doc.Block]
 serverDocs =
@@ -32,65 +50,55 @@ description :: String
 description =
   "An RPC server for SAW."
 
-sawMethods :: [AppMethod SAWState]
+sawMethods :: [Argo.AppMethod SAWState]
 sawMethods =
   -- Cryptol
-  [ method
+  [ Argo.command
      "SAW/Cryptol/load module"
-     Command
      cryptolLoadModuleDescr
      cryptolLoadModule
-  , method
+  , Argo.command
      "SAW/Cryptol/load file"
-     Command
      cryptolLoadFileDescr
      cryptolLoadFile
-  , method
+  , Argo.command
      "SAW/Cryptol/save term"
-     Command
      saveTermDescr
      saveTerm
   -- JVM
   {-
-  , method "SAW/JVM/load class" Command (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass
-  , method "SAW/JVM/verify"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify
-  , method "SAW/JVM/assume"     Command (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume
+  , Argo.command "SAW/JVM/load class" (Doc.Paragraph [Doc.Text "TODO"]) jvmLoadClass
+  , Argo.command "SAW/JVM/verify"     (Doc.Paragraph [Doc.Text "TODO"]) jvmVerify
+  , Argo.command "SAW/JVM/assume"     (Doc.Paragraph [Doc.Text "TODO"]) jvmAssume
   -}
   -- LLVM
-  , method
+  , Argo.command
      "SAW/LLVM/load module"
-     Command
      llvmLoadModuleDescr
      llvmLoadModule
-  , method
+  , Argo.command
      "SAW/LLVM/verify"
-     Command
      llvmVerifyDescr
      llvmVerify
-  , method
+  , Argo.command
      "SAW/LLVM/verify x86"
-     Command
      llvmVerifyX86Descr
      llvmVerifyX86
-  , method
+  , Argo.command
      "SAW/LLVM/assume"
-     Command
      llvmAssumeDescr
      llvmAssume
   -- General
-  , method
+  , Argo.command
      "SAW/make simpset"
-     Command
      makeSimpsetDescr
      makeSimpset
-  , method
+  , Argo.command
      "SAW/prove"
-     Command
      proveDescr
      prove
-  , method
+  , Argo.command
      "SAW/set option"
-     Command
      setOptionDescr
      setOption
   ]

saw-remote-api/src/SAWServer.hs

@@ -7,19 +7,20 @@
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 module SAWServer
   ( module SAWServer
   ) where
 
 import Prelude hiding (mod)
-import Control.Lens
+import Control.Lens ( Lens', view, lens, over )
 import Data.Aeson (FromJSON(..), ToJSON(..), withText)
 import Data.ByteString (ByteString)
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as M
-import Data.Parameterized.Pair
-import Data.Parameterized.Some
+import Data.Parameterized.Pair ( Pair(..) )
+import Data.Parameterized.Some ( Some(..) )
 import Data.Text (Text)
 import qualified Data.Text as T
 import qualified Crypto.Hash as Hash
@@ -58,9 +59,17 @@ import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import Verifier.SAW.Rewriter (Simpset)
 import qualified Cryptol.Utils.Ident as Cryptol
 
-import Argo
+import qualified Argo
 import qualified CryptolServer (validateServerState, ServerState(..))
 import SAWServer.Exceptions
+    ( serverValNotFound,
+      notAnLLVMModule,
+      notAnLLVMSetup,
+      notAnLLVMMethodSpecIR,
+      notASimpset,
+      notATerm,
+      notAJVMClass,
+      notAJVMMethodSpecIR )
 
 type SAWCont = (SAWEnv, SAWTask)
 
@@ -144,19 +153,19 @@ trackedFiles :: Lens' SAWState (Map FilePath (Hash.Digest Hash.SHA256))
 trackedFiles = lens _trackedFiles (\v tf -> v { _trackedFiles = tf })
 
 
-pushTask :: SAWTask -> Method SAWState ()
-pushTask t = modifyState mod
+pushTask :: SAWTask -> Argo.Command SAWState ()
+pushTask t = Argo.modifyState mod
   where mod (SAWState env bic stack ro rw tf) =
           SAWState env bic ((t, env) : stack) ro rw tf
 
-dropTask :: Method SAWState ()
-dropTask = modifyState mod
+dropTask :: Argo.Command SAWState ()
+dropTask = Argo.modifyState mod
   where mod (SAWState _ _ [] _ _ _) = error "Internal error - stack underflow"
         mod (SAWState _ sc ((_t, env):stack) ro rw tf) =
           SAWState env sc stack ro rw tf
 
-getHandleAlloc :: Method SAWState Crucible.HandleAllocator
-getHandleAlloc = roHandleAlloc . view sawTopLevelRO <$> getState
+getHandleAlloc :: Argo.Command SAWState Crucible.HandleAllocator
+getHandleAlloc = roHandleAlloc . view sawTopLevelRO <$> Argo.getState
 
 initialState :: (FilePath -> IO ByteString) -> IO SAWState
 initialState readFileFn =
@@ -326,77 +335,77 @@ instance KnownCrucibleSetupType a => IsServerVal (LLVMCrucibleSetupM a) where
 instance IsServerVal (Some CMS.LLVMModule) where
   toServerVal = VLLVMModule
 
-setServerVal :: IsServerVal val => ServerName -> val -> Method SAWState ()
+setServerVal :: IsServerVal val => ServerName -> val -> Argo.Command SAWState ()
 setServerVal name val =
-  do debugLog $ "Saving " <> (T.pack (show name))
-     modifyState $
+  do Argo.debugLog $ "Saving " <> (T.pack (show name))
+     Argo.modifyState $
        over sawEnv $
        \(SAWEnv env) ->
          SAWEnv (M.insert name (toServerVal val) env)
-     debugLog $ "Saved " <> (T.pack (show name))
-     st <- getState
-     debugLog $ "State is " <> T.pack (show st)
+     Argo.debugLog $ "Saved " <> (T.pack (show name))
+     st <- Argo.getState @SAWState
+     Argo.debugLog $ "State is " <> T.pack (show st)
 
 
-getServerVal :: ServerName -> Method SAWState ServerVal
+getServerVal :: ServerName -> Argo.Command SAWState ServerVal
 getServerVal n =
-  do SAWEnv serverEnv <- view sawEnv <$> getState
-     st <- getState
-     debugLog $ "Looking up " <> T.pack (show n) <> " in " <> T.pack (show st)
+  do SAWEnv serverEnv <- view sawEnv <$> Argo.getState
+     st <- Argo.getState @SAWState
+     Argo.debugLog $ "Looking up " <> T.pack (show n) <> " in " <> T.pack (show st)
      case M.lookup n serverEnv of
-       Nothing -> raise (serverValNotFound n)
+       Nothing -> Argo.raise (serverValNotFound n)
        Just val -> return val
 
-bindCryptolVar :: Text -> TypedTerm -> Method SAWState ()
+bindCryptolVar :: Text -> TypedTerm -> Argo.Command SAWState ()
 bindCryptolVar x t =
-  do modifyState $ over sawTopLevelRW $ \rw ->
+  do Argo.modifyState $ over sawTopLevelRW $ \rw ->
        rw { rwCryptol = bindTypedTerm (Cryptol.mkIdent x, t) (rwCryptol rw) }
 
-getJVMClass :: ServerName -> Method SAWState JSS.Class
+getJVMClass :: ServerName -> Argo.Command SAWState JSS.Class
 getJVMClass n =
   do v <- getServerVal n
      case v of
        VJVMClass c -> return c
-       _other -> raise (notAJVMClass n)
+       _other -> Argo.raise (notAJVMClass n)
 
-getJVMMethodSpecIR :: ServerName -> Method SAWState (CMS.CrucibleMethodSpecIR CJ.JVM)
+getJVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.CrucibleMethodSpecIR CJ.JVM)
 getJVMMethodSpecIR n =
   do v <- getServerVal n
      case v of
        VJVMMethodSpecIR ir -> return ir
-       _other -> raise (notAJVMMethodSpecIR n)
+       _other -> Argo.raise (notAJVMMethodSpecIR n)
 
-getLLVMModule :: ServerName -> Method SAWState (Some CMS.LLVMModule)
+getLLVMModule :: ServerName -> Argo.Command SAWState (Some CMS.LLVMModule)
 getLLVMModule n =
   do v <- getServerVal n
      case v of
        VLLVMModule m -> return m
-       _other -> raise (notAnLLVMModule n)
+       _other -> Argo.raise (notAnLLVMModule n)
 
-getLLVMSetup :: ServerName -> Method SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
+getLLVMSetup :: ServerName -> Argo.Command SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM)
 getLLVMSetup n =
   do v <- getServerVal n
      case v of
        VLLVMCrucibleSetup setup -> return setup
-       _other -> raise (notAnLLVMSetup n)
+       _other -> Argo.raise (notAnLLVMSetup n)
 
-getLLVMMethodSpecIR :: ServerName -> Method SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR)
+getLLVMMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR)
 getLLVMMethodSpecIR n =
   do v <- getServerVal n
      case v of
        VLLVMMethodSpecIR ir -> return ir
-       _other -> raise (notAnLLVMMethodSpecIR n)
+       _other -> Argo.raise (notAnLLVMMethodSpecIR n)
 
-getSimpset :: ServerName -> Method SAWState Simpset
+getSimpset :: ServerName -> Argo.Command SAWState Simpset
 getSimpset n =
   do v <- getServerVal n
      case v of
        VSimpset ss -> return ss
-       _other -> raise (notASimpset n)
+       _other -> Argo.raise (notASimpset n)
 
-getTerm :: ServerName -> Method SAWState TypedTerm
+getTerm :: ServerName -> Argo.Command SAWState TypedTerm
 getTerm n =
   do v <- getServerVal n
      case v of
        VTerm t -> return t
-       _other -> raise (notATerm n)
+       _other -> Argo.raise (notATerm n)