Skip to content

Commit

Permalink
Fixups to saw-remote-api
Browse files Browse the repository at this point in the history
This mostly consists of commenting-out the `validateSAWState` function.
It doesn't apper to have any call sites, so I'm not sure what it
is intended to be used for.
  • Loading branch information
robdockins committed May 18, 2021
1 parent 2ff337c commit 8615fc0
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 25 deletions.
49 changes: 25 additions & 24 deletions saw-remote-api/src/SAWServer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import Data.Parameterized.Some ( Some(..) )
import Data.Text (Text)
import qualified Data.Text as T
import qualified Crypto.Hash as Hash
import qualified Crypto.Hash.Conduit as Hash
--import qualified Crypto.Hash.Conduit as Hash
import System.Directory (getCurrentDirectory)
import System.IO.Silently (silence)

Expand All @@ -38,7 +38,7 @@ import qualified Data.AIG as AIG
import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator)
import qualified Lang.Crucible.JVM as CJ
import qualified Lang.JVM.Codebase as JSS
import qualified Verifier.SAW.CryptolEnv as CryptolEnv
--import qualified Verifier.SAW.CryptolEnv as CryptolEnv
import Verifier.SAW.Module (emptyModule)
import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule)
import Verifier.SAW.Term.Functor (mkModuleName)
Expand All @@ -59,7 +59,7 @@ import Verifier.SAW.Rewriter (Simpset)
import qualified Cryptol.Utils.Ident as Cryptol

import qualified Argo
import qualified CryptolServer (validateServerState, ServerState(..))
--import qualified CryptolServer (validateServerState, ServerState(..))
import SAWServer.Exceptions
( serverValNotFound,
notAnLLVMModule,
Expand Down Expand Up @@ -230,27 +230,28 @@ initialState readFileFn =
-- recompute a cached result, the cached result may be used even if it is
-- associated with stale filesystem state. See the discussion of this issue at:
-- https://github.com/GaloisInc/argo/pull/70#discussion_r412462908
validateSAWState :: SAWState -> IO Bool
validateSAWState sawState =
checkAll
[ CryptolServer.validateServerState cryptolState
, checkAll $ map (uncurry checkHash) (M.assocs (view trackedFiles sawState))
]
where
checkAll [] = pure True
checkAll (c : cs) =
do result <- c
if result
then checkAll cs
else pure False

checkHash path hash =
do currentHash <- Hash.hashFile path
pure (currentHash == hash)

cryptolState =
CryptolServer.ServerState Nothing
(CryptolEnv.eModuleEnv . rwCryptol . view sawTopLevelRW $ sawState)

-- validateSAWState :: SAWState -> IO Bool
-- validateSAWState sawState =
-- checkAll
-- [ CryptolServer.validateServerState cryptolState
-- , checkAll $ map (uncurry checkHash) (M.assocs (view trackedFiles sawState))
-- ]
-- where
-- checkAll [] = pure True
-- checkAll (c : cs) =
-- do result <- c
-- if result
-- then checkAll cs
-- else pure False

-- checkHash path hash =
-- do currentHash <- Hash.hashFile path
-- pure (currentHash == hash)

-- cryptolState =
-- CryptolServer.ServerState Nothing
-- (CryptolEnv.eModuleEnv . rwCryptol . view sawTopLevelRW $ sawState)


newtype SAWEnv =
Expand Down
3 changes: 2 additions & 1 deletion saw-remote-api/src/SAWServer/CryptolExpression.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ import Data.Maybe (fromMaybe)
import Cryptol.Eval (EvalOpts(..))
import Cryptol.ModuleSystem (ModuleError, ModuleInput(..), ModuleRes, ModuleWarning)
import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename)
import Cryptol.ModuleSystem.Env (ModuleEnv, meSolverConfig)
import Cryptol.ModuleSystem.Env (ModuleEnv)
import Cryptol.ModuleSystem.Interface (noIfaceParams)
import Cryptol.ModuleSystem.Monad (ModuleM, interactive, runModuleM, setNameSeeds, setSupply, typeCheckWarnings, typeCheckingFailed)
import qualified Cryptol.ModuleSystem.Renamer as MR
Expand All @@ -35,6 +35,7 @@ import SAWScript.Value (biSharedContext, TopLevelRW(..))
import Verifier.SAW.CryptolEnv
( getAllIfaceDecls,
getNamingEnv,
meSolverConfig,
translateExpr,
CryptolEnv(eExtraTypes, eExtraTSyns, eModuleEnv) )
import Verifier.SAW.SharedTerm (SharedContext)
Expand Down

0 comments on commit 8615fc0

Please sign in to comment.