From 196d227988c4e72315066e7f052f91f9ec4b4615 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 12 Oct 2020 14:44:05 -0700 Subject: [PATCH] Move `saw-remote-api` to the SAW repo (#93) The `saw-remote-api` package will shortly be in the `saw-script` repository. --- cabal.project | 1 - saw-remote-api/CHANGELOG.md | 5 - saw-remote-api/LICENSE | 29 -- saw-remote-api/Setup.hs | 2 - saw-remote-api/saw-remote-api.cabal | 112 ----- saw-remote-api/saw-remote-api/Main.hs | 49 --- saw-remote-api/src/Main.hs | 0 saw-remote-api/src/SAWServer.hs | 384 ------------------ .../src/SAWServer/CryptolExpression.hs | 99 ----- saw-remote-api/src/SAWServer/CryptolSetup.hs | 72 ---- saw-remote-api/src/SAWServer/Data/Contract.hs | 93 ----- saw-remote-api/src/SAWServer/Data/JVMType.hs | 76 ---- saw-remote-api/src/SAWServer/Data/LLVMType.hs | 115 ------ .../src/SAWServer/Data/SetupValue.hs | 48 --- saw-remote-api/src/SAWServer/Exceptions.hs | 178 -------- .../src/SAWServer/JVMCrucibleSetup.hs | 196 --------- saw-remote-api/src/SAWServer/JVMVerify.hs | 60 --- .../src/SAWServer/LLVMCrucibleSetup.hs | 210 ---------- saw-remote-api/src/SAWServer/LLVMVerify.hs | 78 ---- saw-remote-api/src/SAWServer/NoParams.hs | 11 - saw-remote-api/src/SAWServer/OK.hs | 12 - saw-remote-api/src/SAWServer/ProofScript.hs | 155 ------- saw-remote-api/src/SAWServer/SaveTerm.hs | 25 -- saw-remote-api/src/SAWServer/SetOption.hs | 46 --- saw-remote-api/src/SAWServer/Term.hs | 26 -- saw-remote-api/src/SAWServer/TopLevel.hs | 26 -- saw-remote-api/src/SAWServer/TrackFile.hs | 24 -- saw-remote-api/src/SAWServer/VerifyCommon.hs | 94 ----- saw-remote-api/test-scripts/Foo.cry | 17 - saw-remote-api/test-scripts/Salsa20.cry | 182 --------- saw-remote-api/test-scripts/assume.bc | Bin 3232 -> 0 bytes saw-remote-api/test-scripts/assume.c | 5 - saw-remote-api/test-scripts/assume.py | 42 -- saw-remote-api/test-scripts/null.bc | Bin 2000 -> 0 bytes saw-remote-api/test-scripts/null.c | 3 - saw-remote-api/test-scripts/salsa20.bc | Bin 11968 -> 0 bytes saw-remote-api/test-scripts/salsa20.c | 191 --------- saw-remote-api/test-scripts/salsa20.h | 72 ---- saw-remote-api/test-scripts/salsa20.py | 235 ----------- saw-remote-api/test-scripts/salsa20_easy.py | 184 --------- saw-remote-api/test-scripts/saw-test.py | 37 -- saw-remote-api/test-scripts/seven.bc | Bin 1996 -> 0 bytes saw-remote-api/test-scripts/seven.c | 4 - saw-remote-api/test-scripts/seven.py | 28 -- saw-remote-api/test-scripts/swap.bc | Bin 2236 -> 0 bytes saw-remote-api/test-scripts/swap.c | 13 - saw-remote-api/test-scripts/swap.py | 54 --- saw-remote-api/test-scripts/swap_easy.py | 35 -- saw-remote-api/test-scripts/swap_fancy.py | 39 -- saw-remote-api/test/Test.hs | 25 -- 50 files changed, 3392 deletions(-) delete mode 100644 saw-remote-api/CHANGELOG.md delete mode 100644 saw-remote-api/LICENSE delete mode 100644 saw-remote-api/Setup.hs delete mode 100644 saw-remote-api/saw-remote-api.cabal delete mode 100644 saw-remote-api/saw-remote-api/Main.hs delete mode 100644 saw-remote-api/src/Main.hs delete mode 100644 saw-remote-api/src/SAWServer.hs delete mode 100644 saw-remote-api/src/SAWServer/CryptolExpression.hs delete mode 100644 saw-remote-api/src/SAWServer/CryptolSetup.hs delete mode 100644 saw-remote-api/src/SAWServer/Data/Contract.hs delete mode 100644 saw-remote-api/src/SAWServer/Data/JVMType.hs delete mode 100644 saw-remote-api/src/SAWServer/Data/LLVMType.hs delete mode 100644 saw-remote-api/src/SAWServer/Data/SetupValue.hs delete mode 100644 saw-remote-api/src/SAWServer/Exceptions.hs delete mode 100644 saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs delete mode 100644 saw-remote-api/src/SAWServer/JVMVerify.hs delete mode 100644 saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs delete mode 100644 saw-remote-api/src/SAWServer/LLVMVerify.hs delete mode 100644 saw-remote-api/src/SAWServer/NoParams.hs delete mode 100644 saw-remote-api/src/SAWServer/OK.hs delete mode 100644 saw-remote-api/src/SAWServer/ProofScript.hs delete mode 100644 saw-remote-api/src/SAWServer/SaveTerm.hs delete mode 100644 saw-remote-api/src/SAWServer/SetOption.hs delete mode 100644 saw-remote-api/src/SAWServer/Term.hs delete mode 100644 saw-remote-api/src/SAWServer/TopLevel.hs delete mode 100644 saw-remote-api/src/SAWServer/TrackFile.hs delete mode 100644 saw-remote-api/src/SAWServer/VerifyCommon.hs delete mode 100644 saw-remote-api/test-scripts/Foo.cry delete mode 100644 saw-remote-api/test-scripts/Salsa20.cry delete mode 100644 saw-remote-api/test-scripts/assume.bc delete mode 100644 saw-remote-api/test-scripts/assume.c delete mode 100644 saw-remote-api/test-scripts/assume.py delete mode 100644 saw-remote-api/test-scripts/null.bc delete mode 100644 saw-remote-api/test-scripts/null.c delete mode 100644 saw-remote-api/test-scripts/salsa20.bc delete mode 100644 saw-remote-api/test-scripts/salsa20.c delete mode 100644 saw-remote-api/test-scripts/salsa20.h delete mode 100755 saw-remote-api/test-scripts/salsa20.py delete mode 100644 saw-remote-api/test-scripts/salsa20_easy.py delete mode 100644 saw-remote-api/test-scripts/saw-test.py delete mode 100644 saw-remote-api/test-scripts/seven.bc delete mode 100644 saw-remote-api/test-scripts/seven.c delete mode 100644 saw-remote-api/test-scripts/seven.py delete mode 100644 saw-remote-api/test-scripts/swap.bc delete mode 100644 saw-remote-api/test-scripts/swap.c delete mode 100644 saw-remote-api/test-scripts/swap.py delete mode 100644 saw-remote-api/test-scripts/swap_easy.py delete mode 100644 saw-remote-api/test-scripts/swap_fancy.py delete mode 100644 saw-remote-api/test/Test.hs diff --git a/cabal.project b/cabal.project index 9c9044d..35a129a 100644 --- a/cabal.project +++ b/cabal.project @@ -2,7 +2,6 @@ packages: argo/ python/ cryptol-remote-api/ - saw-remote-api/ tasty-script-exitcode/ optional-packages: diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md deleted file mode 100644 index 48ff3f1..0000000 --- a/saw-remote-api/CHANGELOG.md +++ /dev/null @@ -1,5 +0,0 @@ -# Revision history for saw-remote-api - -## 0.1.0.0 -- YYYY-mm-dd - -* First version. Released on an unsuspecting world. diff --git a/saw-remote-api/LICENSE b/saw-remote-api/LICENSE deleted file mode 100644 index 76ed25f..0000000 --- a/saw-remote-api/LICENSE +++ /dev/null @@ -1,29 +0,0 @@ -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. diff --git a/saw-remote-api/Setup.hs b/saw-remote-api/Setup.hs deleted file mode 100644 index 9a994af..0000000 --- a/saw-remote-api/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal deleted file mode 100644 index c04068b..0000000 --- a/saw-remote-api/saw-remote-api.cabal +++ /dev/null @@ -1,112 +0,0 @@ -cabal-version: 2.4 --- Initial package description 'saw-remote-api.cabal' generated by 'cabal --- init'. For further documentation, see --- http://haskell.org/cabal/users-guide/ - -name: saw-remote-api -version: 0.1.0.0 --- synopsis: --- description: --- bug-reports: -license: BSD-3-Clause -license-file: LICENSE -author: Kenny Foner -maintainer: kwf@galois.com --- copyright: -category: Network -extra-source-files: CHANGELOG.md -data-files: test-scripts/*.py - test-scripts/*.cry - test-scripts/*.bc - test-scripts/*.c - -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, - abcBridge, - aeson, - argo, - bytestring, - containers >= 0.6 && < 0.7, - cryptol >= 2.8.1, - cryptol-saw-core, - crucible, - crucible-jvm, - cryptonite, - cryptonite-conduit, - directory, - jvm-parser, - jvm-verifier, - lens, - llvm-pretty, - llvm-pretty-bc-parser, - mtl, - parameterized-utils, - saw-core, - saw-script, - silently, - text, - vector >= 0.12 && < 0.13, - cryptol-remote-api - default-language: Haskell2010 - -library - import: deps, warnings - hs-source-dirs: src - exposed-modules: SAWServer, - SAWServer.CryptolExpression, - SAWServer.CryptolSetup, - SAWServer.Data.Contract, - SAWServer.Data.JVMType, - SAWServer.Data.LLVMType, - SAWServer.Data.SetupValue, - SAWServer.Exceptions, - SAWServer.JVMCrucibleSetup, - SAWServer.JVMVerify, - SAWServer.LLVMCrucibleSetup, - SAWServer.LLVMVerify, - SAWServer.NoParams, - SAWServer.OK, - SAWServer.ProofScript, - SAWServer.SaveTerm, - SAWServer.SetOption, - SAWServer.Term, - SAWServer.TopLevel, - SAWServer.TrackFile, - SAWServer.VerifyCommon - -executable saw-remote-api - import: deps, warnings - main-is: Main.hs - build-depends: saw-remote-api - -- other-modules: - -- other-extensions: - hs-source-dirs: saw-remote-api - -test-suite test-saw-remote-api - import: deps, warnings - type: exitcode-stdio-1.0 - hs-source-dirs: test - main-is: Test.hs - other-modules: Paths_saw_remote_api - build-depends: argo-python, - cryptol-remote-api, - filepath, - process, - quickcheck-instances, - tasty, - tasty-hunit, - tasty-quickcheck, - tasty-script-exitcode diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs deleted file mode 100644 index 3bcafcd..0000000 --- a/saw-remote-api/saw-remote-api/Main.hs +++ /dev/null @@ -1,49 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Main (main) where - -import qualified Data.Aeson as JSON -import Data.Text (Text) - -import Argo -import Argo.DefaultMain - -import SAWServer -import SAWServer.CryptolSetup -import SAWServer.JVMCrucibleSetup -import SAWServer.JVMVerify -import SAWServer.LLVMCrucibleSetup -import SAWServer.LLVMVerify -import SAWServer.ProofScript -import SAWServer.SaveTerm -import SAWServer.SetOption - - -main :: IO () -main = - do theApp <- mkApp initialState sawMethods - defaultMain description theApp - -description :: String -description = - "An RPC server for SAW." - -sawMethods :: [(Text, MethodType, JSON.Value -> Method SAWState JSON.Value)] -sawMethods = - -- Cryptol - [ ("SAW/Cryptol/load module", Command, method cryptolLoadModule) - , ("SAW/Cryptol/load file", Command, method cryptolLoadFile) - , ("SAW/Cryptol/save term", Command, method saveTerm) - -- JVM - , ("SAW/JVM/load class", Command, method jvmLoadClass) - , ("SAW/JVM/verify", Command, method jvmVerify) - , ("SAW/JVM/assume", Command, method jvmAssume) - -- LLVM - , ("SAW/LLVM/load module", Command, method llvmLoadModule) - , ("SAW/LLVM/verify", Command, method llvmVerify) - , ("SAW/LLVM/verify x86", Command, method llvmVerifyX86) - , ("SAW/LLVM/assume", Command, method llvmAssume) - -- General - , ("SAW/make simpset", Command, method makeSimpset) - , ("SAW/prove", Command, method prove) - , ("SAW/set option", Command, method setOption) - ] diff --git a/saw-remote-api/src/Main.hs b/saw-remote-api/src/Main.hs deleted file mode 100644 index e69de29..0000000 diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs deleted file mode 100644 index 25a5c3a..0000000 --- a/saw-remote-api/src/SAWServer.hs +++ /dev/null @@ -1,384 +0,0 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE OverloadedStrings #-} -module SAWServer - ( module SAWServer - ) where - -import Prelude hiding (mod) -import Control.Lens -import Control.Monad.ST -import Data.Aeson (FromJSON(..), ToJSON(..), fromJSON, withText, (.:), withObject) -import qualified Data.Aeson as JSON -import Data.ByteString (ByteString) -import Data.Map.Strict (Map) -import qualified Data.Map.Strict as M -import Data.Parameterized.Pair -import Data.Parameterized.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 System.IO.Silently (silence) - -import qualified Cryptol.Parser.AST as P -import qualified Cryptol.TypeCheck.AST as Cryptol (Schema) -import qualified Data.ABC.GIA as GIA -import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator) -import qualified Lang.Crucible.JVM as CJ -import qualified Lang.Crucible.JVM.Types as CJ -import qualified Text.LLVM.AST as LLVM -import qualified Verifier.Java.Codebase as JSS -import Verifier.SAW.CryptolEnv (CryptolEnv) -import qualified Verifier.SAW.CryptolEnv as CryptolEnv -import Verifier.SAW.Module (emptyModule) -import Verifier.SAW.SharedTerm (mkSharedContext, scLoadModule, Term) -import Verifier.SAW.Term.Functor (mkModuleName) -import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule) - - -import qualified SAWScript.Crucible.Common.MethodSpec as CMS (CrucibleMethodSpecIR) -import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (AllLLVM, SomeLLVM, LLVMModule(..)) -import SAWScript.JavaExpr (JavaType(..)) -import SAWScript.Options (defaultOptions) -import SAWScript.Position (Pos(..)) -import SAWScript.Prover.Rewrite (basic_ss) -import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts) -import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW -import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm) -import Verifier.SAW.Rewriter (Simpset) -import qualified Verifier.Java.SAWBackend as JavaSAW -import qualified Cryptol.Utils.Ident as Cryptol - -import Argo -import CryptolServer.Data.Expression -import qualified CryptolServer (validateServerState, ServerState(..)) -import SAWServer.Exceptions - -type SAWCont = (SAWEnv, SAWTask) - -type CryptolAST = P.Expr P.PName - -data SAWTask - = ProofScriptTask - | LLVMCrucibleSetup ServerName [SetupStep LLVM.Type] - | JVMSetup ServerName [SetupStep JavaType] - -instance Show SAWTask where - show ProofScriptTask = "ProofScript" - show (LLVMCrucibleSetup n steps) = "(LLVMCrucibleSetup" ++ show n ++ " " ++ show steps ++ ")" - show (JVMSetup n steps) = "(JVMSetup" ++ show n ++ " " ++ show steps ++ ")" - - -data CrucibleSetupVal e - = NullValue - | ArrayValue [CrucibleSetupVal e] - -- | TupleValue [CrucibleSetupVal e] - -- | RecordValue [(String, CrucibleSetupVal e)] - | FieldLValue (CrucibleSetupVal e) String - | ElementLValue (CrucibleSetupVal e) Int - | GlobalInitializer String - | GlobalLValue String - | ServerValue ServerName - | CryptolExpr e - deriving (Foldable, Functor, Traversable) - -data SetupStep ty - = SetupReturn (CrucibleSetupVal CryptolAST) -- ^ The return value - | SetupFresh ServerName Text ty -- ^ Server name to save in, debug name, fresh variable type - | SetupAlloc ServerName ty Bool (Maybe Int) -- ^ Server name to save in, type of allocation, mutability, alignment - | SetupPointsTo (CrucibleSetupVal CryptolAST) (CrucibleSetupVal CryptolAST) -- ^ Source, target - | SetupExecuteFunction [CrucibleSetupVal CryptolAST] -- ^ Function's arguments - | SetupPrecond CryptolAST -- ^ Function's precondition - | SetupPostcond CryptolAST -- ^ Function's postcondition - -instance Show (SetupStep ty) where - show _ = "⟨SetupStep⟩" -- TODO - -instance ToJSON SAWTask where - toJSON = toJSON . show - -data SAWState = - SAWState - { _sawEnv :: SAWEnv - , _sawBIC :: BuiltinContext - , _sawTask :: [(SAWTask, SAWEnv)] - , _sawTopLevelRO :: TopLevelRO - , _sawTopLevelRW :: TopLevelRW - , _trackedFiles :: Map FilePath (Hash.Digest Hash.SHA256) - } - -instance Show SAWState where - show (SAWState e _ t _ _ tf) = "(SAWState " ++ show e ++ " _sc_ " ++ show t ++ " _ro_ _rw" ++ show tf ++ ")" - -sawEnv :: Lens' SAWState SAWEnv -sawEnv = lens _sawEnv (\v e -> v { _sawEnv = e }) - -sawBIC :: Lens' SAWState BuiltinContext -sawBIC = lens _sawBIC (\v bic -> v { _sawBIC = bic }) - -sawTask :: Lens' SAWState [(SAWTask, SAWEnv)] -sawTask = lens _sawTask (\v t -> v { _sawTask = t }) - -sawTopLevelRO :: Lens' SAWState TopLevelRO -sawTopLevelRO = lens _sawTopLevelRO (\v ro -> v { _sawTopLevelRO = ro }) - -sawTopLevelRW :: Lens' SAWState TopLevelRW -sawTopLevelRW = lens _sawTopLevelRW (\v rw -> v { _sawTopLevelRW = rw }) - -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 - where mod (SAWState env bic stack ro rw tf) = - SAWState env bic ((t, env) : stack) ro rw tf - -dropTask :: Method SAWState () -dropTask = 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 - -initialState :: (FilePath -> IO ByteString) -> IO SAWState -initialState readFile = - let ?fileReader = readFile in - -- silence prevents output on stdout, which suppresses defaulting - -- warnings from the Cryptol type checker - silence $ - do sc <- mkSharedContext - CryptolSAW.scLoadPreludeModule sc - JavaSAW.scLoadJavaModule sc - CryptolSAW.scLoadCryptolModule sc - let mn = mkModuleName ["SAWScript"] - scLoadModule sc (emptyModule mn) - ss <- basic_ss sc - let jarFiles = [] - classPaths = [] - jcb <- JSS.loadCodebase jarFiles classPaths - let bic = BuiltinContext { biSharedContext = sc - , biJavaCodebase = jcb - , biBasicSS = ss - } - cenv <- initCryptolEnv sc - halloc <- Crucible.newHandleAllocator - jvmTrans <- CJ.mkInitialJVMContext halloc - let ro = TopLevelRO - { roSharedContext = sc - , roJavaCodebase = jcb - , roOptions = defaultOptions - , roHandleAlloc = halloc - , roPosition = PosInternal "SAWServer" - , roProxy = AIGProxy GIA.proxy - } - rw = TopLevelRW - { rwValues = mempty - , rwTypes = mempty - , rwTypedef = mempty - , rwDocs = mempty - , rwCryptol = cenv - , rwPPOpts = defaultPPOpts - , rwJVMTrans = jvmTrans - , rwPrimsAvail = mempty - , rwSMTArrayMemoryModel = False - , rwProfilingFile = Nothing - , rwCrucibleAssertThenAssume = False - , rwLaxArith = False - , rwWhat4HashConsing = False - } - return (SAWState emptyEnv bic [] ro rw M.empty) - --- NOTE: KWF: 2020-04-22: This function could introduce a race condition: if a --- file changes on disk after its hash is computed by validateSAWState, but --- before the function returns and its result is used to inform whether to --- 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) - - -newtype SAWEnv = - SAWEnv { sawEnvBindings :: Map ServerName ServerVal } - deriving Show - -emptyEnv :: SAWEnv -emptyEnv = SAWEnv M.empty - -newtype ServerName = ServerName Text - deriving (Eq, Show, Ord) - -instance ToJSON ServerName where - toJSON (ServerName n) = toJSON n - -instance FromJSON ServerName where - parseJSON = withText "name" (pure . ServerName) - -data CrucibleSetupTypeRepr :: * -> * where - UnitRepr :: CrucibleSetupTypeRepr () - TypedTermRepr :: CrucibleSetupTypeRepr TypedTerm - -data ServerVal - = VTerm TypedTerm - | VSimpset Simpset - | VType Cryptol.Schema - | VCryptolModule CryptolModule -- from SAW, includes Term mappings - | VJVMClass JSS.Class - | VJVMCrucibleSetup (Pair CrucibleSetupTypeRepr JVMSetupM) - | VLLVMCrucibleSetup (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM) - | VLLVMModule (Some CMS.LLVMModule) - | VJVMMethodSpecIR (CMS.CrucibleMethodSpecIR CJ.JVM) - | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) - -instance Show ServerVal where - show (VTerm t) = "(VTerm " ++ show t ++ ")" - show (VSimpset ss) = "(VSimpset " ++ show ss ++ ")" - show (VType t) = "(VType " ++ show t ++ ")" - show (VCryptolModule _) = "VCryptolModule" - show (VJVMClass _) = "VJVMClass" - show (VJVMCrucibleSetup _) = "VJVMCrucibleSetup" - show (VLLVMCrucibleSetup _) = "VLLVMCrucibleSetup" - show (VLLVMModule (Some _)) = "VLLVMModule" - show (VLLVMMethodSpecIR _) = "VLLVMMethodSpecIR" - show (VJVMMethodSpecIR _) = "VJVMMethodSpecIR" - -class IsServerVal a where - toServerVal :: a -> ServerVal - -instance IsServerVal TypedTerm where - toServerVal = VTerm - -instance IsServerVal Simpset where - toServerVal = VSimpset - -instance IsServerVal Cryptol.Schema where - toServerVal = VType - -instance IsServerVal CryptolModule where - toServerVal = VCryptolModule - -instance IsServerVal (CMS.CrucibleMethodSpecIR CJ.JVM) where - toServerVal = VJVMMethodSpecIR - -instance IsServerVal (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) where - toServerVal = VLLVMMethodSpecIR - -instance IsServerVal JSS.Class where - toServerVal = VJVMClass - -class KnownCrucibleSetupType a where - knownCrucibleSetupRepr :: CrucibleSetupTypeRepr a - -instance KnownCrucibleSetupType () where - knownCrucibleSetupRepr = UnitRepr - -instance KnownCrucibleSetupType TypedTerm where - knownCrucibleSetupRepr = TypedTermRepr - -instance KnownCrucibleSetupType a => IsServerVal (LLVMCrucibleSetupM a) where - toServerVal x = VLLVMCrucibleSetup (Pair knownCrucibleSetupRepr x) - -instance IsServerVal (Some CMS.LLVMModule) where - toServerVal = VLLVMModule - -setServerVal :: IsServerVal val => ServerName -> val -> Method SAWState () -setServerVal name val = - do debugLog $ "Saving " <> (T.pack (show name)) - 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) - - -getServerVal :: ServerName -> Method SAWState ServerVal -getServerVal n = - do SAWEnv serverEnv <- view sawEnv <$> getState - st <- getState - debugLog $ "Looking up " <> T.pack (show n) <> " in " <> T.pack (show st) - case M.lookup n serverEnv of - Nothing -> raise (serverValNotFound n) - Just val -> return val - -bindCryptolVar :: Text -> TypedTerm -> Method SAWState () -bindCryptolVar x t = - do modifyState $ over sawTopLevelRW $ \rw -> - rw { rwCryptol = bindTypedTerm (Cryptol.mkIdent x, t) (rwCryptol rw) } - -getJVMClass :: ServerName -> Method SAWState JSS.Class -getJVMClass n = - do v <- getServerVal n - case v of - VJVMClass c -> return c - _other -> raise (notAJVMClass n) - -getJVMMethodSpecIR :: ServerName -> Method SAWState (CMS.CrucibleMethodSpecIR CJ.JVM) -getJVMMethodSpecIR n = - do v <- getServerVal n - case v of - VJVMMethodSpecIR ir -> return ir - _other -> raise (notAJVMMethodSpecIR n) - -getLLVMModule :: ServerName -> Method SAWState (Some CMS.LLVMModule) -getLLVMModule n = - do v <- getServerVal n - case v of - VLLVMModule m -> return m - _other -> raise (notAnLLVMModule n) - -getLLVMSetup :: ServerName -> Method SAWState (Pair CrucibleSetupTypeRepr LLVMCrucibleSetupM) -getLLVMSetup n = - do v <- getServerVal n - case v of - VLLVMCrucibleSetup setup -> return setup - _other -> raise (notAnLLVMSetup n) - -getLLVMMethodSpecIR :: ServerName -> Method SAWState (CMS.SomeLLVM CMS.CrucibleMethodSpecIR) -getLLVMMethodSpecIR n = - do v <- getServerVal n - case v of - VLLVMMethodSpecIR ir -> return ir - _other -> raise (notAnLLVMMethodSpecIR n) - -getSimpset :: ServerName -> Method SAWState Simpset -getSimpset n = - do v <- getServerVal n - case v of - VSimpset ss -> return ss - _other -> raise (notASimpset n) - -getTerm :: ServerName -> Method SAWState TypedTerm -getTerm n = - do v <- getServerVal n - case v of - VTerm t -> return t - _other -> raise (notATerm n) diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs deleted file mode 100644 index f313c68..0000000 --- a/saw-remote-api/src/SAWServer/CryptolExpression.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE PartialTypeSignatures #-} -module SAWServer.CryptolExpression (getTypedTerm, getTypedTermOfCExp) where - -import Control.Lens hiding (re) -import Control.Monad.IO.Class -import qualified Data.ByteString as B -import qualified Data.Map as Map -import Data.Maybe (fromMaybe) - -import Cryptol.Eval (EvalOpts(..), defaultPPOpts) -import Cryptol.ModuleSystem (ModuleRes) -import Cryptol.ModuleSystem.Base (genInferInput, getPrimMap, noPat, rename) -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 -import Cryptol.Parser.AST -import Cryptol.Parser.Position (emptyRange, getLoc) -import Cryptol.TypeCheck (tcExpr) -import Cryptol.TypeCheck.Monad (InferOutput(..), inpVars, inpTSyns) -import Cryptol.Utils.Ident (interactiveName) -import Cryptol.Utils.Logger (quietLogger) -import Cryptol.Utils.PP -import SAWScript.Value (biSharedContext, TopLevelRW(..)) -import Verifier.SAW.CryptolEnv -import Verifier.SAW.SharedTerm (SharedContext) -import Verifier.SAW.TypedTerm(TypedTerm(..)) - -import Argo -import CryptolServer.Data.Expression -import SAWServer -import CryptolServer.Exceptions (cryptolError) - -getTypedTerm :: Expression -> Method SAWState TypedTerm -getTypedTerm inputExpr = - do cenv <- rwCryptol . view sawTopLevelRW <$> getState - fileReader <- getFileReader - expr <- getExpr inputExpr - sc <- biSharedContext . view sawBIC <$> getState - (t, _) <- moduleCmdResult =<< (liftIO $ getTypedTermOfCExp fileReader sc cenv expr) - return t - -getTypedTermOfCExp :: - (FilePath -> IO B.ByteString) -> - SharedContext -> CryptolEnv -> Expr PName -> IO (ModuleRes TypedTerm) -getTypedTermOfCExp fileReader sc cenv expr = - do let ?fileReader = fileReader - let env = eModuleEnv cenv - mres <- runModuleM (defaultEvalOpts, B.readFile, env) $ - do npe <- interactive (noPat expr) -- eliminate patterns - - -- resolve names - let nameEnv = getNamingEnv cenv - re <- interactive (rename interactiveName nameEnv (MR.rename npe)) - - -- infer types - let ifDecls = getAllIfaceDecls env - let range = fromMaybe emptyRange (getLoc re) - prims <- getPrimMap - tcEnv <- genInferInput range prims noIfaceParams ifDecls - let tcEnv' = tcEnv { inpVars = Map.union (eExtraTypes cenv) (inpVars tcEnv) - , inpTSyns = Map.union (eExtraTSyns cenv) (inpTSyns tcEnv) - } - - out <- liftIO (tcExpr re tcEnv') - interactive (runInferOutput out) - case mres of - (Right ((checkedExpr, schema), modEnv'), ws) -> - do let env' = cenv { eModuleEnv = modEnv' } - trm <- liftIO $ translateExpr sc env' checkedExpr - return (Right (TypedTerm schema trm, modEnv'), ws) - (Left err, ws) -> return (Left err, ws) - -liftModuleM :: ModuleEnv -> ModuleM a -> Method SAWState (a, ModuleEnv) -liftModuleM env m = liftIO (runModuleM (defaultEvalOpts, B.readFile, env) m) >>= moduleCmdResult - -moduleCmdResult :: ModuleRes a -> Method SAWState (a, ModuleEnv) -moduleCmdResult (result, warnings) = - do mapM_ (liftIO . print . pp) warnings - case result of - Right (a, me) -> return (a, me) - Left err -> raise $ cryptolError err warnings - -defaultEvalOpts :: EvalOpts -defaultEvalOpts = EvalOpts quietLogger defaultPPOpts - -runInferOutput :: InferOutput a -> ModuleM a -runInferOutput out = - case out of - InferOK warns seeds supply o -> - do setNameSeeds seeds - setSupply supply - typeCheckWarnings warns - return o - - InferFailed warns errs -> - do typeCheckWarnings warns - typeCheckingFailed errs diff --git a/saw-remote-api/src/SAWServer/CryptolSetup.hs b/saw-remote-api/src/SAWServer/CryptolSetup.hs deleted file mode 100644 index e0bbacb..0000000 --- a/saw-remote-api/src/SAWServer/CryptolSetup.hs +++ /dev/null @@ -1,72 +0,0 @@ -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -module SAWServer.CryptolSetup - ( cryptolLoadFile - , cryptolLoadModule - ) where - -import Control.Exception (SomeException, try) -import Control.Monad.IO.Class -import Control.Lens -import Data.Aeson (FromJSON(..), withObject, (.:)) -import qualified Data.Text as T - -import qualified Cryptol.Parser.AST as P -import Cryptol.Utils.Ident (textToModName) -import SAWScript.Value (biSharedContext, rwCryptol) -import qualified Verifier.SAW.CryptolEnv as CEnv -import Verifier.SAW.CryptolEnv (CryptolEnv) - -import Argo -import SAWServer -import SAWServer.Exceptions -import SAWServer.NoParams -import SAWServer.OK - -cryptolLoadModule :: CryptolLoadModuleParams -> Method SAWState OK -cryptolLoadModule (CryptolLoadModuleParams modName) = - do sc <- biSharedContext . view sawBIC <$> getState - cenv <- rwCryptol . view sawTopLevelRW <$> getState - let qual = Nothing -- TODO add field to params - let importSpec = Nothing -- TODO add field to params - fileReader <- getFileReader - let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Right modName) qual importSpec - case cenv' of - Left (ex :: SomeException) -> raise $ cryptolError (show ex) - Right cenv'' -> - do modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } - ok - -data CryptolLoadModuleParams = - CryptolLoadModuleParams P.ModName - -instance FromJSON CryptolLoadModuleParams where - parseJSON = - withObject "params for \"SAW/Cryptol setup/load module\"" $ \o -> - CryptolLoadModuleParams . textToModName <$> o .: "module name" - -cryptolLoadFile :: CryptolLoadFileParams -> Method SAWState OK -cryptolLoadFile (CryptolLoadFileParams fileName) = - do sc <- biSharedContext . view sawBIC <$> getState - cenv <- rwCryptol . view sawTopLevelRW <$> getState - let qual = Nothing -- TODO add field to params - let importSpec = Nothing -- TODO add field to params - fileReader <- getFileReader - let ?fileReader = fileReader - cenv' <- liftIO $ try $ CEnv.importModule sc cenv (Left fileName) qual importSpec - case cenv' of - Left (ex :: SomeException) -> raise $ cryptolError (show ex) - Right cenv'' -> - do modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } - ok - -data CryptolLoadFileParams = - CryptolLoadFileParams FilePath - -instance FromJSON CryptolLoadFileParams where - parseJSON = - withObject "params for \"SAW/Cryptol setup/load file\"" $ \o -> - CryptolLoadFileParams . T.unpack <$> o .: "file" diff --git a/saw-remote-api/src/SAWServer/Data/Contract.hs b/saw-remote-api/src/SAWServer/Data/Contract.hs deleted file mode 100644 index 356d4b5..0000000 --- a/saw-remote-api/src/SAWServer/Data/Contract.hs +++ /dev/null @@ -1,93 +0,0 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.Data.Contract - ( ContractMode(..) - , Contract(..) - , ContractVar(..) - , Allocated(..) - , PointsTo(..) - ) where - -import Data.Aeson (FromJSON(..), withObject, (.:)) -import Data.Text - -import SAWServer -import SAWServer.Data.SetupValue () - --- | How to use a contract: as a verification goal or an assumption. -data ContractMode - = VerifyContract - | AssumeContract - -data Contract ty cryptolExpr = - Contract - { preVars :: [ContractVar ty] - , preConds :: [cryptolExpr] - , preAllocated :: [Allocated ty] - , prePointsTos :: [PointsTo cryptolExpr] - , argumentVals :: [CrucibleSetupVal cryptolExpr] - , postVars :: [ContractVar ty] - , postConds :: [cryptolExpr] - , postAllocated :: [Allocated ty] - , postPointsTos :: [PointsTo cryptolExpr] - , returnVal :: Maybe (CrucibleSetupVal cryptolExpr) - } - deriving (Functor, Foldable, Traversable) - -data ContractVar ty = - ContractVar - { contractVarServerName :: ServerName - , contractVarName :: Text - , contractVarType :: ty - } - -data Allocated ty = - Allocated - { allocatedServerName :: ServerName - , allocatedType :: ty - , allocatedMutable :: Bool - , allocatedAlignment :: Maybe Int - } - -data PointsTo cryptolExpr = - PointsTo - { pointer :: CrucibleSetupVal cryptolExpr - , pointsTo :: CrucibleSetupVal cryptolExpr - } deriving (Functor, Foldable, Traversable) - -instance FromJSON cryptolExpr => FromJSON (PointsTo cryptolExpr) where - parseJSON = - withObject "Points-to relationship" $ \o -> - PointsTo <$> o .: "pointer" - <*> o .: "points to" - -instance FromJSON ty => FromJSON (Allocated ty) where - parseJSON = - withObject "allocated thing" $ \o -> - Allocated <$> o .: "server name" - <*> o .: "type" - <*> o .: "mutable" - <*> o .: "alignment" - -instance FromJSON ty => FromJSON (ContractVar ty) where - parseJSON = - withObject "contract variable" $ \o -> - ContractVar <$> o .: "server name" - <*> o .: "name" - <*> o .: "type" - -instance (FromJSON ty, FromJSON e) => FromJSON (Contract ty e) where - parseJSON = - withObject "contract" $ \o -> - Contract <$> o .: "pre vars" - <*> o .: "pre conds" - <*> o .: "pre allocated" - <*> o .: "pre points tos" - <*> o .: "argument vals" - <*> o .: "post vars" - <*> o .: "post conds" - <*> o .: "post allocated" - <*> o .: "post points tos" - <*> o .: "return val" diff --git a/saw-remote-api/src/SAWServer/Data/JVMType.hs b/saw-remote-api/src/SAWServer/Data/JVMType.hs deleted file mode 100644 index 1f417e7..0000000 --- a/saw-remote-api/src/SAWServer/Data/JVMType.hs +++ /dev/null @@ -1,76 +0,0 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -module SAWServer.Data.JVMType () where - -import Control.Applicative -import qualified Data.Aeson as JSON -import Data.Aeson (withObject, withText, (.:)) - {- -import Data.Int (Int32, Int64) -import Data.Text (Text) -import qualified Data.Text as T --} - -import SAWScript.JavaExpr - -data JVMTypeTag - = TagPrimType - | TagArrayType - | TagClassType - -instance JSON.FromJSON JVMTypeTag where - parseJSON = - withText "JVM type tag" $ - \case - "primitive type" -> pure TagPrimType - "array type" -> pure TagArrayType - "class type" -> pure TagClassType - _ -> empty - -data PrimTypeTag - = TagBoolean - | TagByte - | TagChar - | TagDouble - | TagFloat - | TagInt - | TagLong - | TagShort - -instance JSON.FromJSON PrimTypeTag where - parseJSON = - withText "JVM primitive type tag" $ - \case - "boolean" -> pure TagBoolean - "byte" -> pure TagByte - "char" -> pure TagChar - "double" -> pure TagDouble - "float" -> pure TagFloat - "int" -> pure TagInt - "long" -> pure TagLong - "short" -> pure TagShort - _ -> empty - -instance JSON.FromJSON JavaType where - parseJSON = - primType - - where - primType = - withObject "JVM type" $ \o -> - o .: "type" >>= - \case - TagPrimType -> - o .: "primitive" >>= - \case - TagBoolean -> pure JavaBoolean - TagByte -> pure JavaByte - TagChar -> pure JavaChar - TagDouble -> pure JavaDouble - TagFloat -> pure JavaFloat - TagInt -> pure JavaInt - TagLong -> pure JavaLong - TagShort -> pure JavaShort - TagArrayType -> JavaArray <$> o .: "size" <*> o .: "element type" - TagClassType -> JavaClass <$> o .: "class name" diff --git a/saw-remote-api/src/SAWServer/Data/LLVMType.hs b/saw-remote-api/src/SAWServer/Data/LLVMType.hs deleted file mode 100644 index b8ac57d..0000000 --- a/saw-remote-api/src/SAWServer/Data/LLVMType.hs +++ /dev/null @@ -1,115 +0,0 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -module SAWServer.Data.LLVMType (JSONLLVMType, llvmType) where - -import Control.Applicative -import qualified Data.Aeson as JSON -import Data.Aeson (withObject, withText, (.:)) -import Data.Int (Int32, Int64) -import Data.Text (Text) -import qualified Data.Text as T - - -import Text.LLVM.AST (FloatType(..), Type'(..), Type, Ident(..), PrimType(..)) - -newtype JSONLLVMIdent = JSONLLVMIdent { getIdent :: Ident } - -instance JSON.FromJSON JSONLLVMIdent where - parseJSON = - withText "LLVM identifier" $ pure . JSONLLVMIdent . Ident . T.unpack - -newtype JSONLLVMType = JSONLLVMType { getLLVMType :: Type' JSONLLVMIdent } - - -data LLVMTypeTag - = TagPrimType - | TagAlias - | TagArray - | TagFunTy - | TagPtrTo - | TagStruct - | TagPackedStruct - | TagVector - | TagOpaque - -instance JSON.FromJSON LLVMTypeTag where - parseJSON = - withText "LLVM type tag" $ - \case - "primitive type" -> pure TagPrimType - "type alias" -> pure TagAlias - "array"-> pure TagArray - "function" -> pure TagFunTy - "pointer" -> pure TagPtrTo - "struct" -> pure TagStruct - "packed struct" -> pure TagPackedStruct - "vector" -> pure TagVector - "opaque" -> pure TagOpaque - _ -> empty - -data PrimTypeTag - = TagLabel - | TagVoid - | TagInteger - | TagFloatType - | TagX86mmx - | TagMetadata - -instance JSON.FromJSON PrimTypeTag where - parseJSON = - withText "LLVM primitive type tag" $ - \case - "label" -> pure TagLabel - "void" -> pure TagVoid - "integer" -> pure TagInteger - "float" -> pure TagFloatType - "X86mmx" -> pure TagX86mmx - "metadata" -> pure TagMetadata - _ -> empty - -newtype JSONFloatType = JSONFloatType { getFloatType :: FloatType } - -instance JSON.FromJSON JSONFloatType where - parseJSON = - withText "LLVM float type" $ \t -> fmap JSONFloatType $ - case t of - "half" -> pure Half - "float" -> pure Float - "double" -> pure Double - "fp128" -> pure Fp128 - "x86_fp80" -> pure X86_fp80 - "PPC_fp128" -> pure PPC_fp128 - - -instance JSON.FromJSON JSONLLVMType where - parseJSON = - primType - - where - primType = - withObject "LLVM type" $ \o -> fmap JSONLLVMType $ - o .: "type" >>= - \case - TagPrimType -> - fmap PrimType $ - o .: "primitive" >>= - \case - TagLabel -> pure Label - TagVoid -> pure Void - TagInteger -> Integer <$> o .: "size" - TagFloatType -> - FloatType . getFloatType <$> o .: "float type" - TagX86mmx -> pure X86mmx - TagMetadata -> pure Metadata - TagAlias -> Alias <$> o .: "alias of" - TagArray -> Array <$> o .: "size" <*> (getLLVMType <$> o .: "element type") - TagFunTy -> FunTy <$> (getLLVMType <$> o .: "return type") <*> (fmap getLLVMType <$> o .: "argument types") <*> o .: "varargs" - TagPtrTo -> PtrTo <$> (getLLVMType <$> o .: "to type") - TagStruct -> Struct <$> (fmap getLLVMType <$> o .: "fields") - TagPackedStruct -> PackedStruct <$> (fmap getLLVMType <$> o .: "fields") - TagVector -> Vector <$> o .: "size" <*> (getLLVMType <$> o .: "element type") - TagOpaque -> pure Opaque - -llvmType :: JSONLLVMType -> Type -llvmType = fmap getIdent . getLLVMType diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs deleted file mode 100644 index 7047a83..0000000 --- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs +++ /dev/null @@ -1,48 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.Data.SetupValue (CrucibleSetupVal) where - -import Control.Applicative -import Data.Aeson (FromJSON(..), withObject, withText, (.:)) - -import SAWServer - -data SetupValTag - = TagServerValue - | TagNullValue - | TagCryptol - | TagArrayValue - | TagFieldLValue - | TagElemLValue - | TagGlobalInit - | TagGlobalLValue - -instance FromJSON SetupValTag where - parseJSON = - withText "tag for setup value"$ - \case - "saved" -> pure TagServerValue - "null value" -> pure TagNullValue - "Cryptol" -> pure TagCryptol - "array value" -> pure TagArrayValue - "field lvalue" -> pure TagFieldLValue - "element lvalue" -> pure TagElemLValue - "global initializer" -> pure TagGlobalInit - "global lvalue" -> pure TagGlobalLValue - _ -> empty - -instance FromJSON cryptolExpr => FromJSON (CrucibleSetupVal cryptolExpr) where - parseJSON v = fromObject v - where - fromObject = withObject "saved value or Cryptol expression" $ \o -> - o .: "setup value" >>= - \case - TagServerValue -> ServerValue <$> o .: "name" - TagNullValue -> pure NullValue - TagCryptol -> CryptolExpr <$> o .: "expression" - TagArrayValue -> ArrayValue <$> o .: "elements" - TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field" - TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index" - TagGlobalInit -> GlobalInitializer <$> o .: "name" - TagGlobalLValue -> GlobalLValue <$> o .: "name" diff --git a/saw-remote-api/src/SAWServer/Exceptions.hs b/saw-remote-api/src/SAWServer/Exceptions.hs deleted file mode 100644 index 60567ce..0000000 --- a/saw-remote-api/src/SAWServer/Exceptions.hs +++ /dev/null @@ -1,178 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.Exceptions ( - -- * Environment errors - serverValNotFound - , notACryptolEnv - , notAnLLVMModule - , notAnLLVMSetup - , notACrucibleSetupVal - , notAJVMMethodSpecIR - , notAnLLVMMethodSpecIR - , notASimpset - , notATerm - , notAJVMClass - -- * Wrong monad errors - , notSettingUpCryptol - , notSettingUpLLVMCrucible - , notAtTopLevel - -- * Cryptol errors - , cryptolError - -- * LLVM errors - , cantLoadLLVMModule - -- * Verification - , verificationException - ) where - -import Control.Exception -import Data.Aeson as JSON -import qualified Data.Text as T - -import Argo - --------------------------------------------------------------------------------- --- NOTE: IF YOU MODIFY EXCEPTION CODES OR ADD NEW ONES, THESE CHANGES MUST BE --- SYNCHRONIZED WITH ANY CLIENTS (such as argo/python/saw/exceptions.py) --------------------------------------------------------------------------------- - -serverValNotFound :: - (ToJSON name, Show name) => - name {- ^ the name that was not found -}-> - JSONRPCException -serverValNotFound name = - makeJSONRPCException 10000 ("No server value with name " <> T.pack (show name)) - (Just $ object ["name" .= name]) - -notACryptolEnv :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a Cryptol environment -}-> - JSONRPCException -notACryptolEnv name = - makeJSONRPCException 10010 - ("The server value with name " <> - T.pack (show name) <> - " is not a Cryptol environment") - (Just $ object ["name" .= name]) - -notAnLLVMModule :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to an LLVM module -}-> - JSONRPCException -notAnLLVMModule name = - makeJSONRPCException 10020 - ("The server value with name " <> - T.pack (show name) <> - " is not an LLVM module") - (Just $ object ["name" .= name]) - -notAnLLVMSetup :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to an LLVM setup script -}-> - JSONRPCException -notAnLLVMSetup name = - makeJSONRPCException 10030 - ("The server value with name " <> - T.pack (show name) <> - " is not an LLVM setup script") - (Just $ object ["name" .= name]) - -notACrucibleSetupVal :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a Crucible setup value -}-> - JSONRPCException -notACrucibleSetupVal name = - makeJSONRPCException 10040 - ("The server value with name " <> - T.pack (show name) <> - " is not a Crucible setup value") - (Just $ object ["name" .= name]) - -notAnLLVMMethodSpecIR :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a method specification IR -}-> - JSONRPCException -notAnLLVMMethodSpecIR name = - makeJSONRPCException 10050 - ("The server value with name " <> - T.pack (show name) <> - " is not an LLVM method specification") - (Just $ object ["name" .= name]) - -notASimpset :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a simpset -}-> - JSONRPCException -notASimpset name = - makeJSONRPCException 10060 - ("The server value with name " <> - T.pack (show name) <> - " is not a simpset") - (Just $ object ["name" .= name]) - -notATerm :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a term -}-> - JSONRPCException -notATerm name = - makeJSONRPCException 10070 - ("The server value with name " <> - T.pack (show name) <> - " is not a term") - (Just $ object ["name" .= name]) - -notAJVMClass :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a JVM class -}-> - JSONRPCException -notAJVMClass name = - makeJSONRPCException 10080 - ("The server value with name " <> - T.pack (show name) <> - " is not a JVM class") - (Just $ object ["name" .= name]) - -notAJVMMethodSpecIR :: - (ToJSON name, Show name) => - name {- ^ the name that should have been mapped to a method specification IR -}-> - JSONRPCException -notAJVMMethodSpecIR name = - makeJSONRPCException 10090 - ("The server value with name " <> - T.pack (show name) <> - " is not a JVM method specification") - (Just $ object ["name" .= name]) - -notSettingUpCryptol :: JSONRPCException -notSettingUpCryptol = - makeJSONRPCException 10100 "Not currently setting up Cryptol" noData - -notSettingUpLLVMCrucible :: JSONRPCException -notSettingUpLLVMCrucible = - makeJSONRPCException - 10110 "Not currently setting up Crucible/LLVM" noData - -notAtTopLevel :: ToJSON a => [a] -> JSONRPCException -notAtTopLevel tasks = - makeJSONRPCException - 10120 "Not at top level" - (Just (JSON.object ["tasks" .= tasks])) - -cantLoadLLVMModule :: String -> JSONRPCException -cantLoadLLVMModule err = - makeJSONRPCException - 10200 "Can't load LLVM module" - (Just (JSON.object ["error" .= err])) - -verificationException :: Exception e => e -> JSONRPCException -verificationException e = - makeJSONRPCException - 10300 "Verification exception" - (Just (JSON.object ["error" .= displayException e])) - -cryptolError :: String -> JSONRPCException -cryptolError message = - makeJSONRPCException - 11000 "Cryptol exception" - (Just (JSON.object ["error" .= message])) - -noData :: Maybe () -noData = Nothing diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs deleted file mode 100644 index c67afed..0000000 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ /dev/null @@ -1,196 +0,0 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE PartialTypeSignatures #-} -module SAWServer.JVMCrucibleSetup - ( startJVMSetup - , jvmLoadClass - , compileJVMContract - ) where - -import Control.Lens -import Control.Monad.IO.Class -import Control.Monad.State -import Data.Aeson (FromJSON(..), withObject, (.:)) -import Data.ByteString (ByteString) -import Data.Foldable -import Data.Map (Map) -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Text as T - -import qualified Cryptol.Parser.AST as P -import Cryptol.Utils.Ident (mkIdent) -import qualified Lang.Crucible.JVM as CJ -import qualified Language.JVM.Common as JVM -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) -import SAWScript.Crucible.JVM.Builtins -import SAWScript.Crucible.JVM.BuiltinsJVM -import qualified SAWScript.Crucible.JVM.MethodSpecIR as CMS -import SAWScript.JavaExpr (JavaType(..)) -import SAWScript.Options (defaultOptions) -import SAWScript.Value (BuiltinContext, JVMSetupM(..), biSharedContext) -import qualified Verifier.SAW.CryptolEnv as CEnv -import Verifier.SAW.CryptolEnv (CryptolEnv) -import Verifier.SAW.TypedTerm (TypedTerm) - -import Argo -import SAWServer -import SAWServer.Data.Contract -import SAWServer.Data.JVMType -import SAWServer.Data.SetupValue () -import SAWServer.CryptolExpression (getTypedTermOfCExp) -import SAWServer.Exceptions -import SAWServer.OK -import SAWServer.TopLevel -import SAWServer.TrackFile - -startJVMSetup :: StartJVMSetupParams -> Method SAWState OK -startJVMSetup (StartJVMSetupParams n) = - do pushTask (JVMSetup n []) - ok - -data StartJVMSetupParams - = StartJVMSetupParams ServerName - -instance FromJSON StartJVMSetupParams where - parseJSON = - withObject "params for \"SAW/Crucible setup\"" $ \o -> - StartJVMSetupParams <$> o .: "name" - -data ServerSetupVal = Val (SetupValue CJ.JVM) - --- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now. -compileJVMContract :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - Contract JavaType (P.Expr P.PName) -> - JVMSetupM () -compileJVMContract fileReader bic cenv c = interpretJVMSetup fileReader bic cenv steps - where - setupFresh (ContractVar n dn ty) = SetupFresh n dn ty - setupAlloc (Allocated n ty mut align) = SetupAlloc n ty mut align - steps = - map setupFresh (preVars c) ++ - map SetupPrecond (preConds c) ++ - map setupAlloc (preAllocated c) ++ - map (\(PointsTo p v) -> SetupPointsTo p v) (prePointsTos c) ++ - [ SetupExecuteFunction (argumentVals c) ] ++ - map setupFresh (postVars c) ++ - map SetupPostcond (postConds c) ++ - map setupAlloc (postAllocated c) ++ - map (\(PointsTo p v) -> SetupPointsTo p v) (postPointsTos c) ++ - [ SetupReturn v | v <- maybeToList (returnVal c) ] - -interpretJVMSetup :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - [SetupStep JavaType] -> - JVMSetupM () -interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, cenv0) *> pure () - where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return bic opts - -- TODO: do we really want two names here? - go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ jvm_fresh_var bic opts (T.unpack debugName) ty - (env, cenv) <- get - put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) - save name (Val (MS.SetupTerm t)) - go (SetupAlloc name ty _ (Just _)) = - error "attempted to allocate a Java object with alignment information" - go (SetupAlloc name (JavaArray n ty) True Nothing) = - lift (jvm_alloc_array bic opts n ty) >>= save name . Val - go (SetupAlloc name (JavaClass c) True Nothing) = - lift (jvm_alloc_object bic opts c) >>= save name . Val - go (SetupAlloc name ty False Nothing) = - error $ "cannot allocate type: " ++ show ty - go (SetupPointsTo src tgt) = get >>= \env -> lift $ - do ptr <- getSetupVal env src - tgt' <- getSetupVal env tgt - error "nyi: points-to" - go (SetupExecuteFunction args) = - get >>= \env -> - lift $ traverse (getSetupVal env) args >>= jvm_execute_func bic opts - go (SetupPrecond p) = get >>= \env -> lift $ - getTypedTerm env p >>= jvm_precond - go (SetupPostcond p) = get >>= \env -> lift $ - getTypedTerm env p >>= jvm_postcond - - opts = defaultOptions - save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv)) - - getSetupVal :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - CrucibleSetupVal (P.Expr P.PName) -> - JVMSetupM (MS.SetupValue CJ.JVM) - getSetupVal _ NullValue = JVMSetupM $ return $ MS.SetupNull () - {- - getSetupVal env (ArrayValue elts) = - do elts' <- mapM (getSetupVal env) elts - JVMSetupM $ return $ MS.SetupArray () elts' - getSetupVal env (FieldLValue base fld) = - do base' <- getSetupVal env base - JVMSetupM $ return $ MS.SetupField () base' fld - getSetupVal env (ElementLValue base idx) = - do base' <- getSetupVal env base - JVMSetupM $ return $ MS.SetupElem () base' idx - getSetupVal _ (GlobalInitializer name) = - JVMSetupM $ return $ MS.SetupGlobalInitializer () name - getSetupVal _ (GlobalLValue name) = - JVMSetupM $ return $ MS.SetupGlobal () name - -} - getSetupVal (env, _) (ServerValue n) = JVMSetupM $ - resolve env n >>= - \case - Val x -> return x -- TODO add cases for the server values that - -- are not coming from the setup monad - -- (e.g. surrounding context) - getSetupVal (_, cenv) (CryptolExpr expr) = JVMSetupM $ - do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr - -- TODO: add warnings (snd res) - case fst res of - Right (t, _) -> return (MS.SetupTerm t) - Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly - getSetupVal _ _sv = error $ "unrecognized setup value" -- ++ show sv - - getTypedTerm :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - P.Expr P.PName -> - JVMSetupM TypedTerm - getTypedTerm (_, cenv) expr = JVMSetupM $ - do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr - -- TODO: add warnings (snd res) - case fst res of - Right (t, _) -> return t - Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly - - resolve env name = - case Map.lookup name env of - Just v -> return v - Nothing -> error "Server value not found - impossible!" -- rule out elsewhere - -data JVMLoadClassParams - = JVMLoadClassParams ServerName String - -instance FromJSON JVMLoadClassParams where - parseJSON = - withObject "params for \"SAW/JVM/load class\"" $ \o -> - JVMLoadClassParams <$> o .: "name" <*> o .: "class" - -jvmLoadClass :: JVMLoadClassParams -> Method SAWState OK -jvmLoadClass (JVMLoadClassParams serverName cname) = - do tasks <- view sawTask <$> getState - case tasks of - (_:_) -> raise $ notAtTopLevel $ map fst tasks - [] -> - do bic <- view sawBIC <$> getState - c <- tl $ loadJavaClass bic cname - setServerVal serverName c - ok diff --git a/saw-remote-api/src/SAWServer/JVMVerify.hs b/saw-remote-api/src/SAWServer/JVMVerify.hs deleted file mode 100644 index 6304080..0000000 --- a/saw-remote-api/src/SAWServer/JVMVerify.hs +++ /dev/null @@ -1,60 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module SAWServer.JVMVerify - ( jvmVerify - , jvmAssume - ) where - -import Prelude hiding (mod) -import Control.Lens - -import qualified Language.JVM.Common as JVM - -import SAWScript.Crucible.JVM.Builtins -import SAWScript.JavaExpr (JavaType(..)) -import SAWScript.Options (defaultOptions) -import SAWScript.Value (rwCryptol) - -import Argo -import CryptolServer.Data.Expression -import SAWServer -import SAWServer.Data.Contract -import SAWServer.Data.JVMType -import SAWServer.Exceptions -import SAWServer.JVMCrucibleSetup -import SAWServer.OK -import SAWServer.ProofScript -import SAWServer.TopLevel -import SAWServer.VerifyCommon - -jvmVerifyAssume :: ContractMode -> VerifyParams JavaType -> Method SAWState OK -jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract script lemmaName) = - do tasks <- view sawTask <$> getState - case tasks of - (_:_) -> raise $ notAtTopLevel $ map fst tasks - [] -> - do pushTask (JVMSetup lemmaName []) - state <- getState - cls <- getJVMClass className - let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) - fileReader <- getFileReader - setup <- compileJVMContract fileReader bic cenv <$> traverse getExpr contract - res <- case mode of - VerifyContract -> do - lemmas <- mapM getJVMMethodSpecIR lemmaNames - proofScript <- interpretProofScript script - tl $ crucible_jvm_verify bic defaultOptions cls fun lemmas checkSat setup proofScript - AssumeContract -> - tl $ crucible_jvm_unsafe_assume_spec bic defaultOptions cls fun setup - dropTask - setServerVal lemmaName res - ok - -jvmVerify :: VerifyParams JavaType -> Method SAWState OK -jvmVerify = jvmVerifyAssume VerifyContract - - -jvmAssume :: AssumeParams JavaType -> Method SAWState OK -jvmAssume (AssumeParams className fun contract lemmaName) = - jvmVerifyAssume AssumeContract (VerifyParams className fun [] False contract (ProofScript []) lemmaName) diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs deleted file mode 100644 index fc8af24..0000000 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ /dev/null @@ -1,210 +0,0 @@ -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE PartialTypeSignatures #-} -module SAWServer.LLVMCrucibleSetup - ( startLLVMCrucibleSetup - , llvmLoadModule - , Contract(..) - , ContractVar(..) - , Allocated(..) - , PointsTo(..) - , compileLLVMContract - ) where - -import Control.Lens -import Control.Monad.IO.Class -import Control.Monad.State -import Data.Aeson (FromJSON(..), withObject, (.:)) -import Data.ByteString (ByteString) -import Data.Foldable -import Data.Map (Map) -import qualified Data.Map as Map -import Data.Maybe -import qualified Data.Text as T - -import qualified Cryptol.Parser.AST as P -import Cryptol.Utils.Ident (mkIdent) -import qualified Text.LLVM.AST as LLVM -import qualified Data.LLVM.BitCode as LLVM -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) -import SAWScript.Crucible.LLVM.Builtins - ( crucible_alloc - , crucible_alloc_aligned - , crucible_alloc_readonly - , crucible_alloc_readonly_aligned - , crucible_execute_func - , crucible_fresh_var - , crucible_points_to - , crucible_return - , crucible_precond - , crucible_postcond ) -import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS -import SAWScript.Options (defaultOptions) -import SAWScript.Value (BuiltinContext, LLVMCrucibleSetupM(..), biSharedContext) -import qualified Verifier.SAW.CryptolEnv as CEnv -import Verifier.SAW.CryptolEnv (CryptolEnv) -import Verifier.SAW.TypedTerm (TypedTerm) - -import Argo -import SAWServer -import SAWServer.Data.Contract -import SAWServer.Data.LLVMType (JSONLLVMType, llvmType) -import SAWServer.Data.SetupValue () -import SAWServer.CryptolExpression (getTypedTermOfCExp) -import SAWServer.Exceptions -import SAWServer.OK -import SAWServer.TrackFile - -startLLVMCrucibleSetup :: StartLLVMCrucibleSetupParams -> Method SAWState OK -startLLVMCrucibleSetup (StartLLVMCrucibleSetupParams n) = - do pushTask (LLVMCrucibleSetup n []) - ok - -data StartLLVMCrucibleSetupParams - = StartLLVMCrucibleSetupParams ServerName - -instance FromJSON StartLLVMCrucibleSetupParams where - parseJSON = - withObject "params for \"SAW/Crucible setup\"" $ \o -> - StartLLVMCrucibleSetupParams <$> o .: "name" - -data ServerSetupVal = Val (CMS.AllLLVM SetupValue) - --- TODO: this is an extra layer of indirection that could be collapsed, but is easy to implement for now. -compileLLVMContract :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - Contract JSONLLVMType (P.Expr P.PName) -> - LLVMCrucibleSetupM () -compileLLVMContract fileReader bic cenv c = - interpretLLVMSetup fileReader bic cenv steps - where - setupFresh (ContractVar n dn ty) = SetupFresh n dn (llvmType ty) - setupAlloc (Allocated n ty mut align) = SetupAlloc n (llvmType ty) mut align - steps = - map setupFresh (preVars c) ++ - map SetupPrecond (preConds c) ++ - map setupAlloc (preAllocated c) ++ - map (\(PointsTo p v) -> SetupPointsTo p v) (prePointsTos c) ++ - [ SetupExecuteFunction (argumentVals c) ] ++ - map setupFresh (postVars c) ++ - map SetupPostcond (postConds c) ++ - map setupAlloc (postAllocated c) ++ - map (\(PointsTo p v) -> SetupPointsTo p v) (postPointsTos c) ++ - [ SetupReturn v | v <- maybeToList (returnVal c) ] - -interpretLLVMSetup :: - (FilePath -> IO ByteString) -> - BuiltinContext -> - CryptolEnv -> - [SetupStep LLVM.Type] -> - LLVMCrucibleSetupM () -interpretLLVMSetup fileReader bic cenv0 ss = - runStateT (traverse_ go ss) (mempty, cenv0) *> pure () - where - go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= crucible_return bic defaultOptions - -- TODO: do we really want two names here? - go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ crucible_fresh_var bic defaultOptions (T.unpack debugName) ty - (env, cenv) <- get - put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) - save name (Val (CMS.anySetupTerm t)) - go (SetupAlloc name ty True Nothing) = - lift (crucible_alloc bic defaultOptions ty) >>= save name . Val - go (SetupAlloc name ty False Nothing) = - lift (crucible_alloc_readonly bic defaultOptions ty) >>= save name . Val - go (SetupAlloc name ty True (Just align)) = - lift (crucible_alloc_aligned bic defaultOptions align ty) >>= save name . Val - go (SetupAlloc name ty False (Just align)) = - lift (crucible_alloc_readonly_aligned bic defaultOptions align ty) >>= save name . Val - go (SetupPointsTo src tgt) = get >>= \env -> lift $ - do ptr <- getSetupVal env src - tgt' <- getSetupVal env tgt - crucible_points_to True bic defaultOptions ptr tgt' - go (SetupExecuteFunction args) = - get >>= \env -> - lift $ traverse (getSetupVal env) args >>= crucible_execute_func bic defaultOptions - go (SetupPrecond p) = get >>= \env -> lift $ - getTypedTerm env p >>= crucible_precond - go (SetupPostcond p) = get >>= \env -> lift $ - getTypedTerm env p >>= crucible_postcond - - save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv)) - - getSetupVal :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - CrucibleSetupVal (P.Expr P.PName) -> - LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue) - getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull - getSetupVal env (ArrayValue elts) = - do elts' <- mapM (getSetupVal env) elts - LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts' - getSetupVal env (FieldLValue base fld) = - do base' <- getSetupVal env base - LLVMCrucibleSetupM $ return $ CMS.anySetupField base' fld - getSetupVal env (ElementLValue base idx) = - do base' <- getSetupVal env base - LLVMCrucibleSetupM $ return $ CMS.anySetupElem base' idx - getSetupVal _ (GlobalInitializer name) = - LLVMCrucibleSetupM $ return $ CMS.anySetupGlobalInitializer name - getSetupVal _ (GlobalLValue name) = - LLVMCrucibleSetupM $ return $ CMS.anySetupGlobal name - getSetupVal (env, _) (ServerValue n) = LLVMCrucibleSetupM $ - resolve env n >>= - \case - Val x -> return x -- TODO add cases for the server values that - -- are not coming from the setup monad - -- (e.g. surrounding context) - getSetupVal (_, cenv) (CryptolExpr expr) = LLVMCrucibleSetupM $ - do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr - -- TODO: add warnings (snd res) - case fst res of - Right (t, _) -> return (CMS.anySetupTerm t) - Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly - - getTypedTerm :: - (Map ServerName ServerSetupVal, CryptolEnv) -> - P.Expr P.PName -> - LLVMCrucibleSetupM TypedTerm - getTypedTerm (_, cenv) expr = LLVMCrucibleSetupM $ - do res <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr - -- TODO: add warnings (snd res) - case fst res of - Right (t, _) -> return t - Left err -> error $ "Cryptol error: " ++ show err -- TODO: report properly - - resolve env name = - case Map.lookup name env of - Just v -> return v - Nothing -> error "Server value not found - impossible!" -- rule out elsewhere - -data LLVMLoadModuleParams - = LLVMLoadModuleParams ServerName FilePath - -instance FromJSON LLVMLoadModuleParams where - parseJSON = - withObject "params for \"SAW/LLVM/load module\"" $ \o -> - LLVMLoadModuleParams <$> o .: "name" <*> o .: "bitcode file" - -llvmLoadModule :: LLVMLoadModuleParams -> Method SAWState OK -llvmLoadModule (LLVMLoadModuleParams serverName fileName) = - do tasks <- view sawTask <$> getState - case tasks of - (_:_) -> raise $ notAtTopLevel $ map fst tasks - [] -> - do let ?laxArith = False -- TODO read from config - halloc <- getHandleAlloc - loaded <- liftIO (CMS.loadLLVMModule fileName halloc) - case loaded of - Left err -> raise (cantLoadLLVMModule (LLVM.formatError err)) - Right llvmMod -> - do setServerVal serverName llvmMod - trackFile fileName - ok diff --git a/saw-remote-api/src/SAWServer/LLVMVerify.hs b/saw-remote-api/src/SAWServer/LLVMVerify.hs deleted file mode 100644 index 6de1ad2..0000000 --- a/saw-remote-api/src/SAWServer/LLVMVerify.hs +++ /dev/null @@ -1,78 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module SAWServer.LLVMVerify - ( llvmVerify - , llvmVerifyX86 - , llvmAssume - ) where - -import Prelude hiding (mod) -import Control.Lens - -import SAWScript.Crucible.LLVM.Builtins -import SAWScript.Crucible.LLVM.X86 -import SAWScript.Options (defaultOptions) -import SAWScript.Value (rwCryptol) - -import Argo -import CryptolServer.Data.Expression -import SAWServer -import SAWServer.Data.Contract -import SAWServer.Data.LLVMType -import SAWServer.Exceptions -import SAWServer.LLVMCrucibleSetup -import SAWServer.OK -import SAWServer.ProofScript -import SAWServer.TopLevel -import SAWServer.VerifyCommon - -llvmVerifyAssume :: ContractMode -> VerifyParams JSONLLVMType -> Method SAWState OK -llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract script lemmaName) = - do tasks <- view sawTask <$> getState - case tasks of - (_:_) -> raise $ notAtTopLevel $ map fst tasks - [] -> - do pushTask (LLVMCrucibleSetup lemmaName []) - state <- getState - mod <- getLLVMModule modName - let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) - fileReader <- getFileReader - setup <- compileLLVMContract fileReader bic cenv <$> traverse getExpr contract - res <- case mode of - VerifyContract -> do - lemmas <- mapM getLLVMMethodSpecIR lemmaNames - proofScript <- interpretProofScript script - tl $ crucible_llvm_verify bic defaultOptions mod fun lemmas checkSat setup proofScript - AssumeContract -> - tl $ crucible_llvm_unsafe_assume_spec bic defaultOptions mod fun setup - dropTask - setServerVal lemmaName res - ok - -llvmVerify :: VerifyParams JSONLLVMType -> Method SAWState OK -llvmVerify = llvmVerifyAssume VerifyContract - -llvmAssume :: AssumeParams JSONLLVMType -> Method SAWState OK -llvmAssume (AssumeParams modName fun contract lemmaName) = - llvmVerifyAssume AssumeContract (VerifyParams modName fun [] False contract (ProofScript []) lemmaName) - -llvmVerifyX86 :: X86VerifyParams JSONLLVMType -> Method SAWState OK -llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat contract script lemmaName) = - do tasks <- view sawTask <$> getState - case tasks of - (_:_) -> raise $ notAtTopLevel $ map fst tasks - [] -> - do pushTask (LLVMCrucibleSetup lemmaName []) - state <- getState - mod <- getLLVMModule modName - let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) - allocs = map (\(X86Alloc name size) -> (name, size)) globals - proofScript <- interpretProofScript script - fileReader <- getFileReader - setup <- compileLLVMContract fileReader bic cenv <$> traverse getExpr contract - res <- tl $ crucible_llvm_verify_x86 bic defaultOptions mod objName fun allocs checkSat setup proofScript - dropTask - setServerVal lemmaName res - ok diff --git a/saw-remote-api/src/SAWServer/NoParams.hs b/saw-remote-api/src/SAWServer/NoParams.hs deleted file mode 100644 index dcd1376..0000000 --- a/saw-remote-api/src/SAWServer/NoParams.hs +++ /dev/null @@ -1,11 +0,0 @@ -module SAWServer.NoParams (NoParams(..)) where - -import Data.Aeson - -data NoParams = NoParams - -instance ToJSON NoParams where - toJSON NoParams = object [] - -instance FromJSON NoParams where - parseJSON = withObject "no parameters" (const (pure NoParams)) diff --git a/saw-remote-api/src/SAWServer/OK.hs b/saw-remote-api/src/SAWServer/OK.hs deleted file mode 100644 index eed8ea1..0000000 --- a/saw-remote-api/src/SAWServer/OK.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.OK (OK(..), ok) where - -import Data.Aeson - -data OK = OK - -ok :: Applicative f => f OK -ok = pure OK - -instance ToJSON OK where - toJSON OK = "ok" diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs deleted file mode 100644 index b9da520..0000000 --- a/saw-remote-api/src/SAWServer/ProofScript.hs +++ /dev/null @@ -1,155 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -module SAWServer.ProofScript - ( ProofScript(..) - , interpretProofScript - , makeSimpset - , prove - ) where - -import Control.Applicative -import Control.Monad (foldM) -import Data.Aeson -import Data.Text (Text) - -import Argo -import qualified SAWScript.Builtins as SB -import qualified SAWScript.Value as SV -import SAWServer -import SAWServer.Exceptions -import SAWServer.OK -import SAWServer.TopLevel -import Verifier.SAW.Rewriter (addSimp, emptySimpset) -import Verifier.SAW.TermNet (merge) -import Verifier.SAW.TypedTerm (TypedTerm(..)) - -data Prover - = ABC - | CVC4 [String] - | RME - | Yices [String] - | Z3 [String] - -data ProofTactic - = UseProver Prover - | Unfold [String] - | BetaReduceGoal - | EvaluateGoal [String] - | Simplify ServerName - | AssumeUnsat - | Trivial - -newtype ProofScript = ProofScript [ProofTactic] - -instance FromJSON Prover where - parseJSON = - withObject "prover" $ \o -> do - (name :: String) <- o .: "name" - case name of - "abc" -> pure ABC - "cvc4" -> CVC4 <$> o .: "uninterpreted functions" - "rme" -> pure RME - "yices" -> Yices <$> o .: "uninterpreted functions" - "z3" -> Z3 <$> o .: "uninterpreted functions" - _ -> empty - -instance FromJSON ProofTactic where - parseJSON = - withObject "proof tactic" $ \o -> do - (tac :: String) <- o .: "tactic" - case tac of - "use prover" -> UseProver <$> o .: "prover" - "unfold" -> Unfold <$> o .: "names" - "beta reduce goal" -> pure BetaReduceGoal - "evalute goal" -> EvaluateGoal <$> o .: "uninterpreted functions" - "simplify" -> Simplify <$> o .: "rules" - "assume unsat" -> pure AssumeUnsat - "trivial" -> pure Trivial - _ -> empty - -instance FromJSON ProofScript where - parseJSON = - withObject "proof script" $ \o -> ProofScript <$> o .: "tactics" - -data MakeSimpsetParams = - MakeSimpsetParams - { ssElements :: [ServerName] - , ssResult :: ServerName - } - -instance FromJSON MakeSimpsetParams where - parseJSON = - withObject "SAW/make simpset params" $ \o -> - MakeSimpsetParams <$> o .: "elements" - <*> o .: "result" - -makeSimpset :: MakeSimpsetParams -> Method SAWState OK -makeSimpset params = do - let add ss n = do - v <- getServerVal n - case v of - VSimpset ss' -> return (merge ss ss') - VTerm t -> return (addSimp (ttTerm t) ss) - _ -> raise (notASimpset n) - ss <- foldM add emptySimpset (ssElements params) - setServerVal (ssResult params) ss - ok - -data ProveParams = - ProveParams - { ppScript :: ProofScript - , ppTermName :: ServerName - } - -instance FromJSON ProveParams where - parseJSON = - withObject "SAW/prove params" $ \o -> - ProveParams <$> o .: "script" - <*> o .: "term" - ---data CexValue = CexValue String TypedTerm - -data ProveResult - = ProofValid - | ProofInvalid -- [CexValue] - ---instance ToJSON CexValue where --- toJSON (CexValue n t) = object [ "name" .= n, "value" .= t ] - -instance ToJSON ProveResult where - toJSON ProofValid = object [ "status" .= ("valid" :: Text)] - toJSON ProofInvalid {-cex-} = - object [ "status" .= ("invalid" :: Text) ] -- , "counterexample" .= cex] - -prove :: ProveParams -> Method SAWState ProveResult -prove params = do - t <- getTerm (ppTermName params) - proofScript <- interpretProofScript (ppScript params) - res <- tl $ SB.provePrim proofScript t - case res of - SV.Valid _ -> return ProofValid - SV.InvalidMulti _ _ -> return ProofInvalid - -interpretProofScript :: ProofScript -> Method SAWState (SV.ProofScript SV.SatResult) -interpretProofScript (ProofScript ts) = go ts - where go [UseProver ABC] = return $ SB.proveABC - go [UseProver (CVC4 unints)] = return $ SB.proveUnintCVC4 unints - go [UseProver RME] = return $ SB.proveRME - go [UseProver (Yices unints)] = return $ SB.proveUnintYices unints - go [UseProver (Z3 unints)] = return $ SB.proveUnintZ3 unints - go [Trivial] = return $ SB.trivial - go [AssumeUnsat] = return $ SB.assumeUnsat - go (BetaReduceGoal : rest) = do - m <- go rest - return (SB.beta_reduce_goal >> m) - go (EvaluateGoal fns : rest) = do - m <- go rest - return (SB.goal_eval fns >> m) - go (Unfold fns : rest) = do - m <- go rest - return (SB.unfoldGoal fns >> m) - go (Simplify sn : rest) = do - ss <- getSimpset sn - m <- go rest - return (SB.simplifyGoal ss >> m) - go _ = error "malformed proof script" diff --git a/saw-remote-api/src/SAWServer/SaveTerm.hs b/saw-remote-api/src/SAWServer/SaveTerm.hs deleted file mode 100644 index fbcef3d..0000000 --- a/saw-remote-api/src/SAWServer/SaveTerm.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.SaveTerm (saveTerm) where - -import Data.Aeson (FromJSON(..), withObject, (.:)) - -import Argo - -import CryptolServer.Data.Expression -import SAWServer -import SAWServer.CryptolExpression -import SAWServer.OK - -saveTerm :: SaveTermParams -> Method SAWState OK -saveTerm (SaveTermParams name e) = - do setServerVal name =<< getTypedTerm e - ok - -data SaveTermParams - = SaveTermParams ServerName Expression - -instance FromJSON SaveTermParams where - parseJSON = - withObject "parameters for saving a term" $ \o -> - SaveTermParams <$> o .: "name" - <*> o .: "expression" diff --git a/saw-remote-api/src/SAWServer/SetOption.hs b/saw-remote-api/src/SAWServer/SetOption.hs deleted file mode 100644 index 0df1a8a..0000000 --- a/saw-remote-api/src/SAWServer/SetOption.hs +++ /dev/null @@ -1,46 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE LambdaCase #-} -module SAWServer.SetOption (setOption) where - -import Control.Applicative -import Control.Lens (view, set) -import Data.Aeson (FromJSON(..), Object, withObject, (.:)) -import Data.Aeson.Types (Parser) - -import SAWScript.Value - -import Argo - -import SAWServer -import SAWServer.OK - -setOption :: SetOptionParams -> Method SAWState OK -setOption opt = - do rw <- view sawTopLevelRW <$> getState - let updateRW = modifyState . set sawTopLevelRW - case opt of - EnableLaxArithmetic enabled -> - updateRW rw { rwLaxArith = enabled } - EnableSMTArrayMemoryModel enabled -> undefined - updateRW rw { rwSMTArrayMemoryModel = enabled } - EnableWhat4HashConsing enabled -> undefined - updateRW rw { rwWhat4HashConsing = enabled } - ok - -data SetOptionParams - = EnableLaxArithmetic Bool - | EnableSMTArrayMemoryModel Bool - | EnableWhat4HashConsing Bool - -parseOption :: Object -> String -> Parser SetOptionParams -parseOption o name = - case name of - "lax arithmetic" -> EnableLaxArithmetic <$> o .: "value" - "SMT array memory model" -> EnableSMTArrayMemoryModel <$> o .: "value" - "What4 hash consing" -> EnableWhat4HashConsing <$> o .: "value" - _ -> empty - -instance FromJSON SetOptionParams where - parseJSON = - withObject "parameters for setting options" $ \o -> o .: "option" >>= parseOption o - diff --git a/saw-remote-api/src/SAWServer/Term.hs b/saw-remote-api/src/SAWServer/Term.hs deleted file mode 100644 index 0e4aea7..0000000 --- a/saw-remote-api/src/SAWServer/Term.hs +++ /dev/null @@ -1,26 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module SAWServer.Term (JSONModuleName(..)) where - -import Control.Applicative -import Data.Aeson (FromJSON(..), ToJSON(..)) -import Data.Aeson as JSON -import qualified Data.Text as T -import qualified Data.Vector as V - -import Verifier.SAW.Term.Functor - -newtype JSONModuleName = JSONModuleName ModuleName - -instance FromJSON JSONModuleName where - parseJSON val = literal val <|> structured val - where - literal = - withText "module name as string" $ - pure . JSONModuleName . mkModuleName . map T.unpack . T.splitOn "." - structured = - withArray "module name as list of parts" $ \v -> - do parts <- traverse parseJSON (V.toList v) - pure $ JSONModuleName $ mkModuleName $ map T.unpack parts - -instance ToJSON JSONModuleName where - toJSON (JSONModuleName n) = toJSON (show n) diff --git a/saw-remote-api/src/SAWServer/TopLevel.hs b/saw-remote-api/src/SAWServer/TopLevel.hs deleted file mode 100644 index b3c632c..0000000 --- a/saw-remote-api/src/SAWServer/TopLevel.hs +++ /dev/null @@ -1,26 +0,0 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} -module SAWServer.TopLevel (tl) where - -import Control.Exception -import Control.Lens -import Control.Monad.State - -import SAWScript.Value - -import Argo -import SAWServer -import SAWServer.Exceptions - -tl :: TopLevel a -> Method SAWState a -tl act = - do st <- getState - let ro = view sawTopLevelRO st - rw = view sawTopLevelRW st - liftIO (try (runTopLevel act ro rw)) >>= - \case - Left (e :: SomeException) -> - raise (verificationException e) - Right (res, rw') -> - do modifyState $ set sawTopLevelRW rw' - return res diff --git a/saw-remote-api/src/SAWServer/TrackFile.hs b/saw-remote-api/src/SAWServer/TrackFile.hs deleted file mode 100644 index 5bec3b5..0000000 --- a/saw-remote-api/src/SAWServer/TrackFile.hs +++ /dev/null @@ -1,24 +0,0 @@ -module SAWServer.TrackFile (trackFile, forgetFile) where - -import Control.Lens -import qualified Data.Map as M -import qualified Crypto.Hash.Conduit as Hash - -import Argo -import SAWServer - --- | Add a filepath to the list of filepaths tracked by the server. Any change --- to the SHA256 hash of this file will invalidate any cached state which is --- causally descended from the moment this method is invoked, unless --- @forgetFile@ is used to remove tracking of this file. -trackFile :: FilePath -> Method SAWState () -trackFile path = - do hash <- Hash.hashFile path - modifyState $ over trackedFiles (M.insert path hash) - --- | Stop tracking a given file. Any state that causally descends from the --- moment this method is invoked will not be invalidated by changes to the file --- on disk, even if this file was previously tracked via @trackFile@. -forgetFile :: FilePath -> Method SAWState () -forgetFile path = - modifyState $ over trackedFiles (M.delete path) diff --git a/saw-remote-api/src/SAWServer/VerifyCommon.hs b/saw-remote-api/src/SAWServer/VerifyCommon.hs deleted file mode 100644 index 950cf00..0000000 --- a/saw-remote-api/src/SAWServer/VerifyCommon.hs +++ /dev/null @@ -1,94 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module SAWServer.VerifyCommon - ( VerifyParams(..) - , X86Alloc(..) - , X86VerifyParams(..) - , AssumeParams(..) - ) where - -import Prelude hiding (mod) -import Data.Aeson (FromJSON(..), withObject, (.:)) - -import CryptolServer.Data.Expression -import SAWServer -import SAWServer.Data.Contract -import SAWServer.ProofScript - -data VerifyParams ty = - VerifyParams - { verifyModule :: ServerName - , verifyFunctionName :: String - , verifyLemmas :: [ServerName] - , verifyCheckSat :: Bool - -- TODO: might want to be able to save contracts and refer to them by name? - , verifyContract :: Contract ty Expression -- ServerName - -- TODO: might want to be able to save proof scripts and refer to them by name? - , verifyScript :: ProofScript - , verifyLemmaName :: ServerName - } - --- | A global allocation from the x86 machine code perspective. The --- first argument is the symbol name of the global, and the second --- argument is how many bytes it should be allocated to point to. -data X86Alloc = X86Alloc String Integer - -data X86VerifyParams ty = - X86VerifyParams - { x86VerifyModule :: ServerName - , x86VerifyObjectFile :: String - , x86VerifyFunctionName :: String - , x86VerifyGlobals :: [X86Alloc] - , x86VerifyLemmas :: [ServerName] - , x86VerifyCheckSat :: Bool - , x86VerifyContract :: Contract ty Expression -- ServerName - , x86VerifyScript :: ProofScript - , x86VerifyLemmaName :: ServerName - } - -instance (FromJSON ty) => FromJSON (VerifyParams ty) where - parseJSON = - withObject "SAW/verify params" $ \o -> - VerifyParams <$> o .: "module" - <*> o .: "function" - <*> o .: "lemmas" - <*> o .: "check sat" - <*> o .: "contract" - <*> o .: "script" - <*> o .: "lemma name" - -instance FromJSON X86Alloc where - parseJSON = - withObject "SAW/x86 allocation" $ \o -> - X86Alloc <$> o .: "global name" - <*> o .: "global size" - -instance (FromJSON ty) => FromJSON (X86VerifyParams ty) where - parseJSON = - withObject "SAW/x86 verify params" $ \o -> - X86VerifyParams <$> o .: "module" - <*> o .: "object file" - <*> o .: "function" - <*> o .: "globals" - <*> o .: "lemmas" - <*> o .: "check sat" - <*> o .: "contract" - <*> o .: "script" - <*> o .: "lemma name" - -data AssumeParams ty = - AssumeParams - { assumeModule :: ServerName - , assumeFunctionName :: String - -- TODO: might want to be able to save contracts and refer to them by name? - , assumeContract :: Contract ty Expression -- ServerName - , assumeLemmaName :: ServerName - } - -instance (FromJSON ty) => FromJSON (AssumeParams ty) where - parseJSON = - withObject "SAW/assume params" $ \o -> - AssumeParams <$> o .: "module" - <*> o .: "function" - <*> o .: "contract" - <*> o .: "lemma name" diff --git a/saw-remote-api/test-scripts/Foo.cry b/saw-remote-api/test-scripts/Foo.cry deleted file mode 100644 index 4a3dd15..0000000 --- a/saw-remote-api/test-scripts/Foo.cry +++ /dev/null @@ -1,17 +0,0 @@ -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 - diff --git a/saw-remote-api/test-scripts/Salsa20.cry b/saw-remote-api/test-scripts/Salsa20.cry deleted file mode 100644 index 782d5d9..0000000 --- a/saw-remote-api/test-scripts/Salsa20.cry +++ /dev/null @@ -1,182 +0,0 @@ -/* - * Copyright (c) 2013-2016 Galois, Inc. - * Distributed under the terms of the BSD3 license (see LICENSE file) - */ - -// see http://cr.yp.to/snuffle/spec.pdf - -module Salsa20 where - -quarterround : [4][32] -> [4][32] -quarterround [y0, y1, y2, y3] = [z0, z1, z2, z3] - where - z1 = y1 ^ ((y0 + y3) <<< 0x7) - z2 = y2 ^ ((z1 + y0) <<< 0x9) - z3 = y3 ^ ((z2 + z1) <<< 0xd) - z0 = y0 ^ ((z3 + z2) <<< 0x12) - -property quarterround_passes_tests = - (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000000] == [0x00000000, 0x00000000, 0x00000000, 0x00000000]) /\ - (quarterround [0x00000001, 0x00000000, 0x00000000, 0x00000000] == [0x08008145, 0x00000080, 0x00010200, 0x20500000]) /\ - (quarterround [0x00000000, 0x00000001, 0x00000000, 0x00000000] == [0x88000100, 0x00000001, 0x00000200, 0x00402000]) /\ - (quarterround [0x00000000, 0x00000000, 0x00000001, 0x00000000] == [0x80040000, 0x00000000, 0x00000001, 0x00002000]) /\ - (quarterround [0x00000000, 0x00000000, 0x00000000, 0x00000001] == [0x00048044, 0x00000080, 0x00010000, 0x20100001]) /\ - (quarterround [0xe7e8c006, 0xc4f9417d, 0x6479b4b2, 0x68c67137] == [0xe876d72b, 0x9361dfd5, 0xf1460244, 0x948541a3]) /\ - (quarterround [0xd3917c5b, 0x55f1c407, 0x52a58a7a, 0x8f887a3b] == [0x3e2f308c, 0xd90a8f36, 0x6ab2a923, 0x2883524c]) - -rowround : [16][32] -> [16][32] -rowround [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] = - [z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15] - where - [ z0, z1, z2, z3] = quarterround [ y0, y1, y2, y3] - [ z5, z6, z7, z4] = quarterround [ y5, y6, y7, y4] - [z10, z11, z8, z9] = quarterround [y10, y11, y8, y9] - [z15, z12, z13, z14] = quarterround [y15, y12, y13, y14] - -property rowround_passes_tests = - (rowround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000] == - [0x08008145, 0x00000080, 0x00010200, 0x20500000, - 0x20100001, 0x00048044, 0x00000080, 0x00010000, - 0x00000001, 0x00002000, 0x80040000, 0x00000000, - 0x00000001, 0x00000200, 0x00402000, 0x88000100]) /\ - (rowround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, - 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, - 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, - 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == - [0xa890d39d, 0x65d71596, 0xe9487daa, 0xc8ca6a86, - 0x949d2192, 0x764b7754, 0xe408d9b9, 0x7a41b4d1, - 0x3402e183, 0x3c3af432, 0x50669f96, 0xd89ef0a8, - 0x0040ede5, 0xb545fbce, 0xd257ed4f, 0x1818882d]) - - -rowround_opt : [16][32] -> [16][32] -rowround_opt ys = join [ (quarterround (yi<<>>i | yi <- split ys | i <- [0 .. 3] ] - -property rowround_opt_is_rowround ys = rowround ys == rowround_opt ys - -columnround : [16][32] -> [16][32] -columnround [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15] = - [y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15] - where - [ y0, y4, y8, y12] = quarterround [ x0, x4, x8, x12] - [ y5, y9, y13, y1] = quarterround [ x5, x9, x13, x1] - [y10, y14, y2, y6] = quarterround [x10, x14, x2, x6] - [y15, y3, y7, y11] = quarterround [x15, x3, x7, x11] - -property columnround_passes_tests = - (columnround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000001, 0x00000000, 0x00000000, 0x00000000] == - [0x10090288, 0x00000000, 0x00000000, 0x00000000, - 0x00000101, 0x00000000, 0x00000000, 0x00000000, - 0x00020401, 0x00000000, 0x00000000, 0x00000000, - 0x40a04001, 0x00000000, 0x00000000, 0x00000000]) /\ - (columnround [0x08521bd6, 0x1fe88837, 0xbb2aa576, 0x3aa26365, - 0xc54c6a5b, 0x2fc74c2f, 0x6dd39cc3, 0xda0a64f6, - 0x90a2f23d, 0x067f95a6, 0x06b35f61, 0x41e4732e, - 0xe859c100, 0xea4d84b7, 0x0f619bff, 0xbc6e965a] == - [0x8c9d190a, 0xce8e4c90, 0x1ef8e9d3, 0x1326a71a, - 0x90a20123, 0xead3c4f3, 0x63a091a0, 0xf0708d69, - 0x789b010c, 0xd195a681, 0xeb7d5504, 0xa774135c, - 0x481c2027, 0x53a8e4b5, 0x4c1f89c5, 0x3f78c9c8]) - - -columnround_opt : [16][32] -> [16][32] -columnround_opt xs = join (transpose [ (quarterround (xi<<>>i | xi <- transpose(split xs) | i <- [0 .. 3] ]) - -columnround_opt_is_columnround xs = columnround xs == columnround_opt xs - -property columnround_is_transpose_of_rowround ys = - rowround ys == join(transpose(split`{4}(columnround xs))) - where xs = join(transpose(split`{4} ys)) - -doubleround : [16][32] -> [16][32] -doubleround(xs) = rowround(columnround(xs)) - -property doubleround_passes_tests = - (doubleround [0x00000001, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000, - 0x00000000, 0x00000000, 0x00000000, 0x00000000] == - [0x8186a22d, 0x0040a284, 0x82479210, 0x06929051, - 0x08000090, 0x02402200, 0x00004000, 0x00800000, - 0x00010200, 0x20400000, 0x08008104, 0x00000000, - 0x20500000, 0xa0000040, 0x0008180a, 0x612a8020]) /\ - (doubleround [0xde501066, 0x6f9eb8f7, 0xe4fbbd9b, 0x454e3f57, - 0xb75540d3, 0x43e93a4c, 0x3a6f2aa0, 0x726d6b36, - 0x9243f484, 0x9145d1e8, 0x4fa9d247, 0xdc8dee11, - 0x054bf545, 0x254dd653, 0xd9421b6d, 0x67b276c1] == - [0xccaaf672, 0x23d960f7, 0x9153e63a, 0xcd9a60d0, - 0x50440492, 0xf07cad19, 0xae344aa0, 0xdf4cfdfc, - 0xca531c29, 0x8e7943db, 0xac1680cd, 0xd503ca00, - 0xa74b2ad6, 0xbc331c5c, 0x1dda24c7, 0xee928277]) - -littleendian : [4][8] -> [32] -littleendian b = join(reverse b) - -property littleendian_passes_tests = - (littleendian [ 0, 0, 0, 0] == 0x00000000) /\ - (littleendian [ 86, 75, 30, 9] == 0x091e4b56) /\ - (littleendian [255, 255, 255, 250] == 0xfaffffff) - -littleendian_inverse : [32] -> [4][8] -littleendian_inverse b = reverse(split b) - -property littleendian_is_invertable b = littleendian_inverse(littleendian b) == b - -Salsa20 : [64][8] -> [64][8] -Salsa20 xs = join ar - where - ar = [ littleendian_inverse words | words <- xw + zs@10 ] - xw = [ littleendian xi | xi <- split xs ] - zs = [xw] # [ doubleround zi | zi <- zs ] - -property Salsa20_passes_tests = - (Salsa20 [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] == - [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) /\ - (Salsa20 [211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, 191, 187, 234, 136, - 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, 86, 16, 179, 207, - 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113, 238, 55, 204, 36, - 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, 88, 118, 104, 54] == - [109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, 26, 110, 170, 154, - 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, 69, 144, 51, 57, - 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35, 27, 111, 114, 114, - 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, 179, 19, 48, 202]) /\ - (Salsa20 [ 88, 118, 104, 54, 79, 201, 235, 79, 3, 81, 156, 47, 203, 26, 244, 243, - 191, 187, 234, 136, 211, 159, 13, 115, 76, 55, 82, 183, 3, 117, 222, 37, - 86, 16, 179, 207, 49, 237, 179, 48, 1, 106, 178, 219, 175, 199, 166, 48, - 238, 55, 204, 36, 31, 240, 32, 63, 15, 83, 93, 161, 116, 147, 48, 113] == - [179, 19, 48, 202, 219, 236, 232, 135, 111, 155, 110, 18, 24, 232, 95, 158, - 26, 110, 170, 154, 109, 42, 178, 168, 156, 240, 248, 238, 168, 196, 190, 203, - 69, 144, 51, 57, 29, 29, 150, 26, 150, 30, 235, 249, 190, 163, 251, 48, - 27, 111, 114, 114, 118, 40, 152, 157, 180, 57, 27, 94, 107, 42, 236, 35]) - -property Salsa20_has_no_collisions x1 x2 = - if(x1 != x2) then (doubleround x1) != (doubleround x2) else True - -// Salsa 20 supports two key sizes, [16][8] and [32][8] -Salsa20_expansion : {a} (a >= 1, 2 >= a) => ([16*a][8], [16][8]) -> [64][8] -Salsa20_expansion(k, n) = z - where - [s0, s1, s2, s3] = split "expand 32-byte k" : [4][4][8] - [t0, t1, t2, t3] = split "expand 16-byte k" : [4][4][8] - x = if(`a == 2) then s0 # k0 # s1 # n # s2 # k1 # s3 - else t0 # k0 # t1 # n # t2 # k0 # t3 - z = Salsa20(x) - [k0, k1] = (split(k#zero)):[2][16][8] - -Salsa20_encrypt : {a, l} (a >= 1, 2 >= a, l <= 2^^70) => ([16*a][8], [8][8], [l][8]) -> [l][8] -Salsa20_encrypt(k, v, m) = c - where - salsa = take (join [ Salsa20_expansion(k, v#(reverse (split i))) | i <- [0, 1 ... ] ]) - c = m ^ salsa diff --git a/saw-remote-api/test-scripts/assume.bc b/saw-remote-api/test-scripts/assume.bc deleted file mode 100644 index 606bd7170f311c4c7de97c77e1964d1d93f0eb8d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 3232 zcmZ`*ZA@F&89wF`A15)_PJ$XJ_ugHXY;w8=E~cS2wl~bBDN!@kS=uSmQpHYi0&M_e zyZ)e2cg=NosfH#eLzO4xhrMQ1ru7HW_>mv^;SWYVW<@TmQiKq)$46id6-=V4J zs(*Dx(mr3+d3kqdkKR;k*3`YY%VZku_D&fZyY?z$ddKCep1kIIEiWD!<^Q5GnPPQM z8=sE1T%0&{iO=PM@9{c>{BUQ(l=0DjpsBoQr;+NQvQnKAisOh;8A{?{UTKRfp=&tA zD?VOnWex0Hs%F~2%mEXXpm<$M#E2!A;!7xz zUMd_{e05470asIgNr4-Er~sSY+>DB!uiOQEZox{b=5C6aj&h3*Zob6LMwvAgi_Az9 z3KMA~8YO5{+9V~^jYCPr7gyShIM}TO5r}sOgwL>xshWa=%cj_wR86VO&Su!P6tkSF znTfKqDRw^1f)?`W}{s38~MFTsF!-!bmt0#zUZf z0uO7Hp_90@|E===X%&0h&8@lFx4w3qiU-GK-OO#U0C+9R&A6GhG7CnSN^yk@GXu7D zakGx^&8X6p1bW34zY!1j%0rSej7lkH!NJ|nfQ!Mu+^rO|2HK?{Jh(d!V8uy?>+r=< z%IcC23;1FJM}X*6f@$1#QjTbFK&TMlYgh;G8?j}JP__x&?v>4(i?A(0wVk9cre!M{ z9rh}~!4EoqM`WVkaS)#%`C_IbQj}dZKzM8in~VCFhNQxe^-JsYeO|XB&>Ly`pGEck zb^2k6UUt&UMfGx={xVMJenIySUbj(HuOeN4kuG=W)=)w;PvmUlln@uq`JDZ#Y@N*5 zin;bNs{I48p+MR5IqQv_Wm08@Ums8%ak0H1n!ys|Vnb0hU!`EbIYwE530l?DcLm)F z(%*H`4+LF5(%pB`OL6)ET+AGqC3?e2-!H0H()4FVx*s-_=>9alqNi7p{@yy> zAE)oR=m+1aX2*@3buwy=$sj{Rg0f9ItTD=-q+E14P2@yna@~VC{b`9_>7e_Qx)omc z1?WQLSAVXjH>7W=Py`hyTUu-zO5hFjYvczQD z0-U8fz|^sv8El@GZ8s_Vc+OnRS-~2kqCFv7#$_A$<*NLnaZ19-p)2#cPn|TlatY}k zqO@qaA={QAnyT%<@QP?Df_5U9+WxU@8wc0CF3^u4lhf+gUGyVCcOQr%{kf#OFrj{+ zr`KFGA;5RAF6h7xzHP$4O$18np-mdL2^jW2l5hy=AXwVYZK5ta_!=a?DOW_I z!0G1VH`Yc+0nmt(tQJ;(HQ z{%V)A%BimUDQbkh`<}g+rmT;4Sd(&_28SgASZ%$E7pg*nB&`_|?;7=-B-eOA$|5~n z36Wq29(LgXM2UpGNj${ka8Z3v!oy&uB=+-LfB&S%J_$c*(7uB%ceTWtwZA2If|OgW z&Q$+As+P89@aMWCdF=*59ZzU9uxR2E`uaV`;$u61@WOPp*ttjl;ofn@sqr|gR>+y_ zp#PgNwrV71s?40LRoO>Hb1XO3SwTL3Vn_?gx*2z^+D;B|7r^P9u%og~t|X{vAEWGr z@L0f$-_&4$UauDqd#PYp@$yQ2VGn&bPL~DUfS?1ASa;H``YD1UP}8z*?ws(B^=2jW zCMoa|#Im)pUK@1bH+%7Oy->UGa}ohduM5nIgO7Fq+mNK31~9Ix6uLz88OXVNCHi3+ zvY$GWCzXc*?1b-vn}M1$6=i4K>f3RW+!lyR_}<8w$2UWw|N7E|Z1 zkI&yXIM5Yx`_6qm@tk?%Jb!fH+~D>~=xndsciP`K z>~S6y`D31-=Yresf1}^ibhh~wKd@+a2L}7kG@o~080>?I@BCo1-yJ&S^Yjk}Jcr!g zzUF|(A2{Sc>+ACd{0^`8f`>nQ!98%E4{i#;x3n|~O#*MMtR8A<5n$HT+S=4&I@qX@ zgpm$yqXxB%pjw#0z=%IloiKpH(H-zXDt$pX5H;oEn!jpAlhCTIxn2;=&zqd8I*baa zpyy3{6Uni;xx4eH<`?sK=4MV6=CZd|j~wKTm)}2CScP=6DXCo5;;0#KO3*+F^s|E~247^+G;=d{-AW4Ya$bXK=vNHxK~&k5}Kz zO0TV{kqTh?88qidJ@Kf@i5f=w_Zbj_8r9Wk#HD9i)jKl1NXnoppd5W@A~WW2)IN!- zr@%nK=jYWt1p^x55h8?%);|?PxrzbFx(5US9721kah~iao#;*U=-Qe)VI+-=1Y;%W zr0s$JB=jFbCm7WMeY=r;q_sjPZ-3GVPx8n>2M}uCnv*pm3|ZH}I%%(hO#5I2nUZ9_ xX%|04;J{|Ygw1WI+n$9GgOEDZ?>;-|54Q+SEr*+g?Fc=+dFFKG5aB`Ee*xBZcY*)_ diff --git a/saw-remote-api/test-scripts/assume.c b/saw-remote-api/test-scripts/assume.c deleted file mode 100644 index ec74e04..0000000 --- a/saw-remote-api/test-scripts/assume.c +++ /dev/null @@ -1,5 +0,0 @@ -extern int seven(void); - -int addone() { - return seven() + 1; -} diff --git a/saw-remote-api/test-scripts/assume.py b/saw-remote-api/test-scripts/assume.py deleted file mode 100644 index 08764af..0000000 --- a/saw-remote-api/test-scripts/assume.py +++ /dev/null @@ -1,42 +0,0 @@ -import os -import os.path -import saw.connection as saw -from saw.proofscript import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -assume_bc = os.path.join(dir_path, 'assume.bc') - -c.llvm_load_module('m', assume_bc).result() - -seven_contract = { - "pre vars": [], - "pre conds": [], - "pre allocated": [], - "pre points tos": [], - "argument vals": [], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [], - "return val": {"setup value": "Cryptol", "expression": "7 : [32]"} -} - -addone_contract = { - "pre vars": [], - "pre conds": [], - "pre allocated": [], - "pre points tos": [], - "argument vals": [], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [], - "return val": {"setup value": "Cryptol", "expression": "8 : [32]"} -} - -prover = ProofScript([abc]).to_json() -c.llvm_assume('m', 'seven', seven_contract, 'seven_ov').result() -c.llvm_verify('m', 'addone', ['seven_ov'], False, addone_contract, prover, 'addone_ov').result() diff --git a/saw-remote-api/test-scripts/null.bc b/saw-remote-api/test-scripts/null.bc deleted file mode 100644 index bcf62757e03bc477d2e6bedfe7dfb6e397427e57..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2000 zcmaJ?Uu;uV7(dtS{eIs$L-PFc3mpixAcT(U%)9o#`PEZDefM(rUX6uLAxVeOml}k&Hc6-n#*e^< zV_oMQh35UO220<0O+xo%i?&l}{@`d-_e#^y`K?2v21|!cYkYl+#gcUTZb)5wx095? zalUD^puOB7%KMVyw;GEjVSLu~th(pq+~IR#z5sR)7!mpe+MUBs-~R)O#)sNWjHpXa zDLAYWzY#}VeiQb47{3$GI-yUjX`-k&;$Z?&V)YPT22Z1s#FgDbQ6m;4 zzAkY$Vtg^HUz50{7+-O5xflE?Qt zL!ap-`Ih0dm?eFKU27AWr}2=9MIEExgbJ@K%D0~yM7P@%HNJ5D2XR)idY zzU7I6RvbOk{E>7q0oC0^R_)k6{C;X{VszMG3^cn2O%5lc>4L3jhnaeEzr~)3TQA|z zAq))7`iK=o;3JWFVue^=BKolr_T5D`0=3Ep2SMX_da<=0#eii>#L8mpMifU3IGDi! z@!{&{2JDaG$0Xgv^LMV?&Pno%P?>9JaLR^Rl>DF&e{gN?kl2x)ESwqZ5Z_SCC4 zo8_UljwW;&e4B;Mz1k>uqsEPQXa1{g=anZMVdJH#VBRp=fXh~4&HA8v!N(C zq9s#C&;X=rZ1=_{yRpLlHqWk`nWKd)x02e^{NZ@OC#o{8H^dHb9^00H?u*S{*;lQ7JuzTQGFr4ZoJ(mTYTjvc;h zVAto_A4b?;%v}ph4q>(SXt~BO0{~~IeJ(z5HNG>Ex25F1QojG%LSG>dKK4^#ghhm& zgw`)OMLDVKZ1Y>3VplA6?%eIY8G~uGe~)G8Lsk0JWC)?x9z!T}%;WYS2~0%Bj!n9~ z$Hm~7KQM8^E82R@J!a9gZ*260-~C|Jy{BjVSg-jR)TJFXpGMkVojh1FXf4~*nN+#F zUO8M@F5D{@50}chTlIZy$%Bo_r9!c~wy$jqVEPR7Nb_s!7P!kpAoxSRv^)TG&B=X> z`O|goCfwW(D#NlPopYde}9yJ2f1 zmoIFC_XYY>um%}|EUe*)1p0z@8)XdMJ05!5nG0)lg4&_D=wrC|;dlgET4+nxJ#+wt zo&jzk6MPg`4}5+-?a@M8`p%(UjUjpq&TfY;ob9DE?#Yll95~{gnVf8dT(Mb? fSfB5n@xJ3d5%P9VPIzaO?&IDWx}oRT0~>z=Fh8B} diff --git a/saw-remote-api/test-scripts/null.c b/saw-remote-api/test-scripts/null.c deleted file mode 100644 index 38a8c07..0000000 --- a/saw-remote-api/test-scripts/null.c +++ /dev/null @@ -1,3 +0,0 @@ -int *always_null () { - return 0; -} diff --git a/saw-remote-api/test-scripts/salsa20.bc b/saw-remote-api/test-scripts/salsa20.bc deleted file mode 100644 index 808474461be045342e3a2a861484595acf0b0ce0..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 11968 zcmch7eOwb)*8iPMm;{)F0fGeZWdL7LQ6~xVQndyWC~CAQNNKg}L|#M}Fo;sDeHjQK zD!S3K7OQmwRTta3ixn-pcAG%7tQ%WYT5)SzsFr2-@v&HKS9jg+bM8!h>F)E#^ZEVp zOJs5`ZAhE=pZ}^tYMK1o`t}lqB?eG zYL9###pqLZ5w-LLKV`&N`L>mUHeHssD=^K&=rzeo?YscJd37 zGz70~bG8}Jju0Scu@<4_@ENt$sJw`-*rK}r1+O4MUToAdH?q{Xxu8-M^j((vnnQg% zOI^yVM|#zRMzxSqOV09|Qc&%z)266q`|MiNtR_>Gt9#Y~`>bA5N{=b3iJW!7Gz;Bf zgTBvFy9U(X_EJM^&|t6nn_g;UME#cm^_?vBcfHg%F7;n})uqs3Kwaumf5WJU5OZ@x zUFuNZa!|_v|Lp*x5a+qk2}Y9dw9lCTDk~&Z;HnI7wbT=)!s; zUChF2=kT~ychx+f(b1X8?>Fl0eYfl0F|2I*KgRtRT z(6_w$4k+VNf6J)vJk+G!t^E-^_9_}L{K?1=?IrA1?7?wpwaKbXjWkAW%?HP7615E| z-gvwvvxZd}!SVCJ?-ckwwAR?n(4q3yW=0uGU1KKF@+B4~gxJC&6a&xoF%AA~L7hA_ z_CPIMuGO|UG$EG8#=u&Sg?ZOKn%E^bhRDZzg9U;(!)~pKQ|dDiB@3t?KQHavXd=!V zEI(rm5TYa3of9tVR`#$qb1`Q&*_Z$o{v!0IDfHK zF3Yqig`UYMAf$$EO2B$1yyPNh-SwO0v?nSRRf3{2ZgXPsW}9~N3(bm`8pvduJ=sAf z33gQ>IICCvqPTvQM#YP~Vm)|GP}rP`a#m5*OWhO{FEWZsr=o)OJw3)K)(MIyg3Ot0 ztT{s%<7F)K2xLUa#rzo|@PzoPPYz^6{KFmR*(e}zA$|$bi{yv|pW+u?J`rgHq&DA> zO%S})My7p%sGgK=v|kq>j*;3fW-}=a`a0Dok47|XJN)82gNRR-+CuaW#bZ;rVD0cm zgjbJ@Kq~muk8RdO1X~=9{u7@%D>uc=cPisD(+;J_&+tE`cgzfNI72f6cG+UdJ@Z=W zpy{xq5!wg_d1-YmEX!%YewIy)Y z-c38Fteg_?#+1LmadhWK-GYk1`~`$SAo$l{)rX%=44+6|)1UqJ;F{l9%5F|*ym@5d zjl!D;=^5{;b{r|WSvbA1bh?Eqva|Gkexw);74W|w8txkY>(K9q(Mlc_72tn7es^}B z_SPLeU-t)Br?Zr4tPY{~(`r`}?Y*4yX>ZnrJ`M8LqZYY+lAYuxkhcppO`ejLO1+q`drnpJu?U@r_S3H#zOFrI4 zjLAeIl7T-&vf25#ZF8Ax`hJS2+JX-{jTgi{Ggry};uctY5NyNK^sW^AZfH)C~K ze#wS{!Wk>pZ?qLw%viBub=i7@e#QFf#ZmIL0}A^j6Pfkr#Mdi_axSsM+mj6GX0PXV8W#)*Qi|e=9oA=I){)~*znMOOY0TkLm7#Z z{~q2TCe#4#`-uZX^N&@doJfovM zCE;NMmP;$ZTeNdeWE6bvZC1%#rN$`;U4{MU-?gD6^G|~FOC*qpBZmljza_%8kM@RN zS@x!O*`BM*-i-Q>d*rgHjI@zP@D?oFRfu*qo~OPhkglIa745`fh=C+R6P3%~i{44r zyiK~)$VDeBxGH@is?c*Q)~$VE-P#Rh1wXw(x)h{?HwSP1%tUe2K9R~D1+Hz|W=@#%brDMp&{dk2Mff+*OTyf%f zr!ngQYLcO5;x?k5K1B12sG*7|M9)EWT2!YFv|} zc4f0|PoOLU@U!V5e$MR9c(V?G4|hJWHcO0Wymse34z*yXf2Gs zz|Xq>z7Sv)gL`&aEwnnmc+cHKY6kv>3x-b+Vz@g7Dl<*Kj$K& z%--{S#OL+a@GAGH9xA`YTDFRNydTkkNn4UOY&&I8{uBw=^B;Aspnw`GFkf@(g zw7Se%GC4}Ng7ve9lc8jL?rsH>Ur|wE$R|kz8*Q_}nLLWC(sBAIS-Df{H1NYvVlKrQ zva?Ou6&1J}i@Pnt-E^p8HJZs847#M01jI!tE0W3ibSChc%Yzy|-9z+W^|-FPJV0$F zZ0{f)w8SxBp|wBV=@^quHOZAxPW#% zef`*gJ79orKxUsrG1;$?HgJV?K=C!*=^EHVc>2A_i##RT`_;+hbgpV8(j^*@0qLVC z2m51nAiZB}Y*eXTDwnrDb$o+?C9#-%JIRKU#$#62f8}^d&ef|Rr>{h7sd*qLDGB5x zMo~@dq8d>St)`7&MTB;?PH5g6B}7CBdsW@@naM}3S^hN>dPIE&T&U+dx?ZAPUQ_Hp zUs^1zR8mrsJ~0WeRdci7*0+S37?duhNQ&OXf+Yu=ZdG6USN58rJ*}N#D%Imdwx1XnBsB97pedJNk zRqWCAFlsSRf(|6|<(Zdk%fuFtg)$z(i$;GjDk|UYWV^%J(HC}QJ_@xhddP=mtHOYZ`ajo#L_d5M?l6QQ60=w!qeDU<$0d*Nb`vkf*;yJ5W;!jXGHZ}IK8L@I61q1S&!e(+QfdlG9Zd2O&Ia><<@%mG$@79p25*Y8e&d^DY>@0F-=fx ztWs1om(x&I{x?)|g4#f*jqP%e`M70t5$7j%vqyQ!IX$L1jpQ6}RpWY_Vv|y_F>|xc zrg+gtR#t7cv6~~j!Ri|h^&l5i#sys)QIBM)4UA{Zm(ip9qsMev#};v0W}OyG;SO^4 zX{e8(TprO>@`_ExilpMr>)>ODJ+oTX5zs?N$a2%}wa~N6_|> zCtI&gMEFY+f0vAoH=6rpu~+VlOUb>Sb)H8%3NFnppJOy!J@IW`7kocAIj5c3X_{#t z!-7}^J0{nanfTAp%Va`#X%sO51_ponA$zHVF&kJTY&&EH8$3AglrM?L)fWYS@4vMF0>{1V=gq9sx^7d#kB^nxse#u7=jCp$!9FJ8Ohzed|j}s zp_)KzM*a%*I{9C433?kYbG=%ItEN^VI%D)GqEV|wPU<&M;?H&BI^X$sxO6uX!J&mV z%Ei|%R!Ks7u@L)T;POz2-YN>wXnaE6#X=m93(fVkX`zP_dT=_2!77Ssrw(IL zUM#BJXOBD78-bb}5#-mCcD#b>qhu64krtk%yU-c z)zfJ(&3#Wfg(erA74B{^3@iA~Xu-vIq2@wu1CPJEMhk9b8;#%wZEGDTJX=%Tg|v;v zcA{Cwo|WBG@VlMO98yLYC{Nz(Xo60XkBYEp(J`6|feG_<_etY9=-QJO;6EUnSVSw| zuoHm#tu(lziLn$;b z|E!=5oH||z7(ig2TRBB5_>))#P-dmlUw99OJJ0AsjD7`Kp_I#J;wh_W>-hO#tMg1b z<*Fhpsa0^(R+kI2q;V9;-3W5Cw*405UgSY;uw91CR`8tic-(v$t78q6d|BoMqA_WG ziHpKF%kj-irM==!G28&mi~)8AOfFg6BOujh0cqGK=PvBlUY6g+xR2cG&eRbN?a&Bc7a>Z-hxYI`qP=W#=(jNHN3BoNZ zY1sZG=yfAzlRtl&P~Ue2fv0{q@H3fK$06q^DjGlhy2_v5?b@SbZ?;zX3&U9b7h8_X zjW*Cg`N7>hSzNRbL8i?}*o~$r>)z0@cVhB=2>GBYPo`blPA*XbGy=M62^(xz3Vnf{ zaVN(5pjTX;%=sh>t6Y`Ff?GAU{^Wox29_^Cy`MwV5x`j67*~UuIaK7oKZ0C2gW8RT zgG8S%n~%co$Y7K`xP_rzfU^bdpkcZ00Ib-~fTKW2lz9cc3UFtJsSnCv>iaRtBybtY zjs||K2F^N>%Wk(_dtG4b=8iFUM~x!Q!Gfw5@h3{3rI~b;$jF2%?{5eTcK4s!IHAWj zXJ>c+@3#9IA3Uqseo5&G)@BZdp0_dc2F*`ipkH_;K)K|u+0b|V&4`*yIWN3Sod4SV z-zh@5Ed=_7j`GM{?6x;S|yJ%7;r$^f0W{a3=V}D-TU4)y?)gMW=t^O+w*0lq=**sJadn~hYA(^oOXC(` z#jr|6OXHWeTJazZ${CeTdBU* zHT(SwjO_NnWrsK_``b|&VBND!H229XLD)GLm47Rp?GIk9r(ZAAnv7xLR<>9+dG?=&5ReDj)x-?m48zBLY)}NYTFqx z2z}Xxg8+wvz+KGku#>&+NUsbyFplI_@<^B@2ADtMZm-~O0NDzg;uy-p+xm&DBBB#c zb4Wp{hfVC}0%2!3M2x!`1Sk#zmTM;qM+pI=_xU!6vlc{Daxlk!CIPk*Z|3B%8$`;! zY24%Il=)Ahg+RQAdZK~i$I!=6<0Sb7k(g;r%)JKK&$D6bHdhzkfWXV>jh;rLTG1U3 z6rVcN3V~Q|LZC--zVUi07idgo5Q+d_{9w&{lB0JXW-bPQksB=kAuaQ%1D`9U1uL9b zH;}NjbShlK%Eo34;3fG3J7%X_0~_NXgvM-0Z?0pYT@;*GzsrZM&wPzpX z)`u7KmWAT_!1hJvMx@D%*32g;O|Co3ATwI3vve9gl4tO8oY&y>!UxH)UJOoK8r||} zx(BkAUrLEgmyLp)<*{_-u}nowSLoVoIzt;OMh2dG2M6rl`>IIYgy1ZwNO%N|2jjoDwG$$2BKF})UEje) zN^yYP=ERkV$plXw!n!p-F19)-FbaihX5n;$MI1%!GM>XLo@yomlY)H7C|7(ctUaTH zwRco~EYp@LM<-yOjgXHArZldM3*@=hW(u+frT>I!kTqDlkaHzqEjsv!A7mhz#W38f zXEH!ut$F7tGzPHA`0Mim2V@x_bZ75pGPV%<$GDI9Wu>MAH2oU!Z3_(lvb`8*246BI zX8@|HFt0MwK-FfNe@-w7cyQZiGAGdae&viaZCv5e-4f6Bp~Jp?uMySUcrMgX{~vI{O$p0nOo_LGPVTNV9Ve1kJYD1WccSS$gk)|@%ycw` z)WcFul0&EjuF&Fb>4<2ATyXq*ohZJUWI&qeg?*l|aCDT|!=baGGQ1=>aC#_EAlZNN zbo7oL$zhYvn_W&UcflSm4@qB+Ni~$8? z6ApADZ;%YS&!Tu#H8v=zNaJn#|`~z@u zyyWCzI}gkPKmwcNwhT@~-;uDY@5;LY{se(e;~A#v+6e*VFOZj@TKGW;&dJbcO>Fn~ zW_A9h#9vB{uPS|wKY!+H-2TX+S#%wu@aKp0N^kyjg&6fF+9e8!$ifloS2aNX;K2J@nVp@+EM6xdZH{g;~J3Y6^k^{FZV8z8pnTyB-4sG zh>0%OLsP>_x7Jh5WD3&wrIBo(WZj%EouBk zO)#pEL!^eJqW@(gQ?%4x7nT`&btWu>__DGHg+Io_xTf^+FfRE;&czMj++K*0iK&@n zS&f4lgP%PXFD>RsW|1y*Cxsc7@fXR_RVOmsO<*|kE4Ty!48~QJiwx(g#?PFOKdT)# z+V||A_uv`-_%qKq&iCvderA09nLG}j(HV3P&gc&ccl@{ocyA>D)LS+CKg4yHT!mpu zRpYvAiT3X@)(%|{8L3wZ2WHFcD*K1X;%|n{-`o{>U)mA1lO66Au;0zFZyL1>>h%LU zn{0WN=+)yPwjX7k!cN%rn&uDD*{D&Ifo`Z+*-9L0*8z1|13p?I?eFHaTj7xSXZwkv z+$JTq9B8P4nxj?on-5X^T_a3FXIR`gA|I3E{63(21?0h@iMX(s!nP3J5DjDt3xO4k zb*mDD!FpF3q`mxZw-HlZSbZ-jF>&Eu*sCp(D&8X?lz^?xiOV3HCnSSX?}1X)0hf!> zD2K$S%J@fhT9#F-;yKxW;oy+xcOU`p=`JMF>N_L*C15m z$h?+$D*m)J(2kji2P<$vRTH+OPhv#AE@mbaDZiy_fOuVzNEAon~oKmA=aY|s7^FGB^PT?j0<@F5k% zDWy!?9p_7oizZ2|SoE66qS>GOh{Cz-3>)kymG?}>}G>yEd%uQ3e-fLduBdA}cO7yiGvx$`JJqMrv$6S0EkCC{AH#?*>e7Ts0 zci^mO#FvJ*xg$GeMgkVL-&pPkVT%J~JgQ8?ASe~v&x8rLYS}#;ii7_N;_@>CGQ*5X zR@59U0MvQ%Oc;6&g6bf(Z7PoKaF~P7K7_yqz|fSovM$8M;+(}zZJmlVu-(5_jd}*+ zbj@mCoDOF&n4MqL5_|?u0%}y6XOJFX*U#Jha8ViswoEi-espnJI@7OskVo6s$LB7A zV(Lnz9ts~Rp&lb9)K@G7ZCbd@5}my8%s69eLU!$yOlj28WlH$6aI#czT`ryBYm~*; zu8%)?oN;lY<6u53i_m!Z1b@%Q|0zPOapW`Gp$UFn1IKy1nU(zd%l(*`#Z0)*=hw#S zh^vI?*K_vE_e zE=UEzQh7L@7r(45{6-F+4{(5Uc@O0LX{nlw$xY_fO~%EVr-C)6jZLX3O(5uDeI}pD zVI)1&T}saj#q`|t8*ITrxZuibZ^Qu!6Q`!&l{dl}#uHP*P$aDJh4RBVAG-vt(!(e# z71*(iUP3_b*#JEg_s+z@!zg2SCl(eqPIrdp!WsWjFym$716IVEZTa znSR1_(BP#K5LlJg3*EkoJRsv%+K_AX=rcG4`wD*aEremnF8ag;!(0L=o(RK)R8jf} z4C7q~WyUeEom_(C78mRgWY@t2PvV|#EOtLr3!WgT2kLK<)EC?^2f)C}9FU1HK$Bs; zidJGA>}>I!eVlzjIvw{gg~4gahEk)CQ%a?ykm&BEkCM602p^el@TGB6B*Z^c8t*%F zD4qUbGlaPdIjJ39ruTI#OYn6oOZ0UsOZN3y`-HDg5U45QvK2o64VO*E;HK2c8dHiU zZE;h2YLj`RCS$b*K>L5fW%rTCad}BQEbXbc=Lh+4Ic0v3h|9(0FZyt~xb#H{muu)d zxF*853?b)8xI9RS-2j)14_1$T9G8n#Fbw1Jor^eo$GF^fkrZ*6w{NTumw9`~O1O*! zff6p;J;oprm)64|P{L*2YA0;&N4U(hkCkxwwx|)tW$PUz;_{haD}1;N|FuHIW#>5~ zHV)%*y1thbak;z%1WLHP961c7?;~7Zb}B?%x~7O4tvxHa;^v@YT#bD87XqO6612|# zg%Cm64g$eAWQS}g7W+i(Ci%n)8;HmAV8wligUwC{7#xSDj z{|S%3dkl}5zs*gic}*ERALZlnnZpy6YX%lFeFJ;hHUfT{_3@*nHd6elM*NkgjTmI? z!En@rf6;j90FIxhappbpH@Lu0E=Qg2agb+rr%4^&!W}w((xG4MP~+>+iaWgflMaq9 zEFsm`p#^t1@RJTb&>;b5c#D68+z<$9;dcrYfy49Lb5R^rt!C3d38Nn{&l~?8gaU8| zSo|vLV_eY4dKHpy4QluM1a4--x4|RO82>8#UpC0H|%D&a2{4oO1KuNntz?S@P%OkOqo_t_we+HhkXQ)$$|K>f(@-#%yidKNtN~ zSp|(VhIg%aRFgPVAraF2os;@)w+e#-vCV4g+lD+Fv z()d|9-+}ARv5MS(K;isDIe!A*vWiN4Ta*JmM=H(B7xgVWXG__62C|gCdYmivs|lJc zo8$S$`~=J@aj+3SA8;^~q;Ou#JjS)Ey=-v=U|jr75-#@OG@XcA{$-3g0b@?^!P@%L zA*iS19_cndKBpVgj%R3*rv&7f; -#include -#include "salsa20.h" - -// Implements DJB's definition of '<<<' -static uint32_t rotl(uint32_t value, int shift) -{ - return (value << shift) | (value >> (32 - shift)); -} - -static void s20_quarterround(uint32_t *y0, uint32_t *y1, uint32_t *y2, uint32_t *y3) -{ - *y1 = *y1 ^ rotl(*y0 + *y3, 7); - *y2 = *y2 ^ rotl(*y1 + *y0, 9); - *y3 = *y3 ^ rotl(*y2 + *y1, 13); - *y0 = *y0 ^ rotl(*y3 + *y2, 18); -} - -static void s20_rowround(uint32_t y[static 16]) -{ - s20_quarterround(&y[0], &y[1], &y[2], &y[3]); - s20_quarterround(&y[5], &y[6], &y[7], &y[4]); - s20_quarterround(&y[10], &y[11], &y[8], &y[9]); - s20_quarterround(&y[15], &y[12], &y[13], &y[14]); -} - -static void s20_columnround(uint32_t x[static 16]) -{ - s20_quarterround(&x[0], &x[4], &x[8], &x[12]); - s20_quarterround(&x[5], &x[9], &x[13], &x[1]); - s20_quarterround(&x[10], &x[14], &x[2], &x[6]); - s20_quarterround(&x[15], &x[3], &x[7], &x[11]); -} - -static void s20_doubleround(uint32_t x[static 16]) -{ - s20_columnround(x); - s20_rowround(x); -} - -// Creates a little-endian word from 4 bytes pointed to by b -static uint32_t s20_littleendian(uint8_t *b) -{ - return b[0] + - (b[1] << 8) + - (b[2] << 16) + - (b[3] << 24); -} - -// Moves the little-endian word into the 4 bytes pointed to by b -static void s20_rev_littleendian(uint8_t *b, uint32_t w) -{ - b[0] = w; - b[1] = w >> 8; - b[2] = w >> 16; - b[3] = w >> 24; -} - -// The core function of Salsa20 -static void s20_hash(uint8_t seq[static 64]) -{ - int i; - uint32_t x[16]; - uint32_t z[16]; - - // Create two copies of the state in little-endian format - // First copy is hashed together - // Second copy is added to first, word-by-word - for (i = 0; i < 16; ++i) - x[i] = z[i] = s20_littleendian(seq + (4 * i)); - - for (i = 0; i < 10; ++i) - s20_doubleround(z); - - for (i = 0; i < 16; ++i) { - z[i] += x[i]; - s20_rev_littleendian(seq + (4 * i), z[i]); - } -} - -// The 16-byte (128-bit) key expansion function -static void s20_expand16(uint8_t *k, - uint8_t n[static 16], - uint8_t keystream[static 64]) -{ - int i, j; - // The constants specified by the Salsa20 specification, 'tau' - // "expand 16-byte k" - uint8_t t[4][4] = { - { 'e', 'x', 'p', 'a' }, - { 'n', 'd', ' ', '1' }, - { '6', '-', 'b', 'y' }, - { 't', 'e', ' ', 'k' } - }; - - // Copy all of 'tau' into the correct spots in our keystream block - for (i = 0; i < 64; i += 20) - for (j = 0; j < 4; ++j) - keystream[i + j] = t[i / 20][j]; - - // Copy the key and the nonce into the keystream block - for (i = 0; i < 16; ++i) { - keystream[4+i] = k[i]; - keystream[44+i] = k[i]; - keystream[24+i] = n[i]; - } - - s20_hash(keystream); -} - - -// The 32-byte (256-bit) key expansion function -static void s20_expand32(uint8_t *k, - uint8_t n[static 16], - uint8_t keystream[static 64]) -{ - int i, j; - // The constants specified by the Salsa20 specification, 'sigma' - // "expand 32-byte k" - uint8_t o[4][4] = { - { 'e', 'x', 'p', 'a' }, - { 'n', 'd', ' ', '3' }, - { '2', '-', 'b', 'y' }, - { 't', 'e', ' ', 'k' } - }; - - // Copy all of 'sigma' into the correct spots in our keystream block - for (i = 0; i < 64; i += 20) - for (j = 0; j < 4; ++j) - keystream[i + j] = o[i / 20][j]; - - // Copy the key and the nonce into the keystream block - for (i = 0; i < 16; ++i) { - keystream[4+i] = k[i]; - keystream[44+i] = k[i+16]; - keystream[24+i] = n[i]; - } - - s20_hash(keystream); -} - -// Performs up to 2^32-1 bytes of encryption or decryption under a -// 128- or 256-bit key. -enum s20_status_t s20_crypt32(uint8_t *key, - uint8_t nonce[static 8], - uint32_t si, - uint8_t *buf, - uint32_t buflen) -{ - uint8_t keystream[64]; - // 'n' is the 8-byte nonce (unique message number) concatenated - // with the per-block 'counter' value (4 bytes in our case, 8 bytes - // in the standard). We leave the high 4 bytes set to zero because - // we permit only a 32-bit integer for stream index and length. - uint8_t n[16] = { 0 }; - uint32_t i; - - // If any of the parameters we received are invalid - if (key == NULL || nonce == NULL || buf == NULL) - return S20_FAILURE; - - // Set up the low 8 bytes of n with the unique message number - for (i = 0; i < 8; ++i) - n[i] = nonce[i]; - - // If we're not on a block boundary, compute the first keystream - // block. This will make the primary loop (below) cleaner - if (si % 64 != 0) { - // Set the second-to-highest 4 bytes of n to the block number - s20_rev_littleendian(n+8, si / 64); - // Expand the key with n and hash to produce a keystream block - s20_expand32(key, n, keystream); - } - - // Walk over the plaintext byte-by-byte, xoring the keystream with - // the plaintext and producing new keystream blocks as needed - for (i = 0; i < buflen; ++i) { - // If we've used up our entire keystream block (or have just begun - // and happen to be on a block boundary), produce keystream block - if ((si + i) % 64 == 0) { - s20_rev_littleendian(n+8, ((si + i) / 64)); - s20_expand32(key, n, keystream); - } - - // xor one byte of plaintext with one byte of keystream - buf[i] ^= keystream[(si + i) % 64]; - } - - return S20_SUCCESS; -} - diff --git a/saw-remote-api/test-scripts/salsa20.h b/saw-remote-api/test-scripts/salsa20.h deleted file mode 100644 index df94eed..0000000 --- a/saw-remote-api/test-scripts/salsa20.h +++ /dev/null @@ -1,72 +0,0 @@ -#ifndef _SALSA20_H_ -#define _SALSA20_H_ - -#include -#include - -/** - * Return codes for s20_crypt - */ -enum s20_status_t -{ - S20_SUCCESS, - S20_FAILURE -}; - -/** - * Key size - * Salsa20 only permits a 128-bit key or a 256-bit key, so these are - * the only two options made available by this library. - */ -enum s20_keylen_t -{ - S20_KEYLEN_256, - S20_KEYLEN_128 -}; - -/** - * Performs up to 2^32-1 bytes of encryption or decryption under a - * 128- or 256-bit key in blocks of arbitrary size. Permits seeking - * to any point within a stream. - * - * key Pointer to either a 128-bit or 256-bit key. - * No key-derivation function is applied to this key, and no - * entropy is gathered. It is expected that this key is already - * appropriate for direct use by the Salsa20 algorithm. - * - * keylen Length of the key. - * Must be S20_KEYLEN_256 or S20_KEYLEN_128. - * - * nonce Pointer to an 8-byte nonce. - * Does not have to be random, but must be unique for every - * message under a single key. Nonce reuse destroys message - * confidentiality. - * - * si Stream index. - * The position within the stream. When encrypting/decrypting - * a message sequentially from beginning to end in fixed-size - * chunks of length L, this value is increased by L on every - * call. Care must be taken not to select values that cause - * overlap. Example: encrypting 1000 bytes at index 100, and - * then encrypting 1000 bytes at index 500. Doing so will - * result in keystream reuse, which destroys message - * confidentiality. - * - * buf The data to encrypt or decrypt. - * - * buflen Length of the data in buf. - * - * This function returns either S20_SUCCESS or S20_FAILURE. - * A return of S20_SUCCESS indicates that basic sanity checking on - * parameters succeeded and encryption/decryption was performed. - * A return of S20_FAILURE indicates that basic sanity checking on - * parameters failed and encryption/decryption was not performed. - */ -enum s20_status_t s20_crypt(uint8_t *key, - enum s20_keylen_t keylen, - uint8_t nonce[static 8], - uint32_t si, - uint8_t *buf, - uint32_t buflen); - -#endif diff --git a/saw-remote-api/test-scripts/salsa20.py b/saw-remote-api/test-scripts/salsa20.py deleted file mode 100755 index f98f3a1..0000000 --- a/saw-remote-api/test-scripts/salsa20.py +++ /dev/null @@ -1,235 +0,0 @@ -#!/usr/bin/env python3 -import os -import os.path -import saw.connection as saw -from saw.llvm import * -from saw.proofscript import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -print("Starting server") -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -bcname = os.path.join(dir_path, 'salsa20.bc') -cryname = os.path.join(dir_path, 'Salsa20.cry') - -print("Loading Cryptol spec") -c.cryptol_load_file(cryname).result() - -print("Loading LLVM module") -c.llvm_load_module('m', bcname).result() - -# SetupVals -value = {"setup value": "Cryptol", "expression": "value" } -shift = {"setup value": "Cryptol", "expression": "shift" } -res = {"setup value": "Cryptol", "expression": "value <<< shift" } - -y0p = {"setup value": "saved", "name" : "y0p" } -y1p = {"setup value": "saved", "name" : "y1p" } -y2p = {"setup value": "saved", "name" : "y2p" } -y3p = {"setup value": "saved", "name" : "y3p" } - -y0 = {"setup value": "Cryptol", "expression" : "y0" } -y1 = {"setup value": "Cryptol", "expression" : "y1" } -y2 = {"setup value": "Cryptol", "expression" : "y2" } -y3 = {"setup value": "Cryptol", "expression" : "y3" } - -y0f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 0" } -y1f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 1" } -y2f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 2" } -y3f = {"setup value": "Cryptol", "expression" : "(quarterround [y0, y1, y2, y3]) @ 3" } - -yp = {"setup value": "saved", "name" : "yp" } -y = {"setup value": "Cryptol", "expression" : "y" } - -rr_res = {"setup value": "Cryptol", "expression" : "rowround y" } -cr_res = {"setup value": "Cryptol", "expression" : "columnround y" } -dr_res = {"setup value": "Cryptol", "expression" : "doubleround y" } -hash_res = {"setup value": "Cryptol", "expression" : "Salsa20 y" } -expand_res = {"setup value": "Cryptol", "expression" : "Salsa20_expansion`{a=2}(k, n)" } -crypt_res = {"setup value": "Cryptol", "expression" : "Salsa20_encrypt (k, v, m)" } - -rotl_contract = { - "pre vars": [ - {"server name": "value", "name": "value", "type": uint32_t.to_json()}, - {"server name": "shift", "name": "shift", "type": uint32_t.to_json()} - ], - "pre conds": ["0 < shift /\\ shift < 32"], - "pre allocated": [], - "pre points tos": [], - "argument vals": [value, shift], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [], - "return val": res -} - -qr_contract = { - "pre vars": [ - {"server name": "y0", "name": "y0", "type": uint32_t.to_json()}, - {"server name": "y1", "name": "y1", "type": uint32_t.to_json()}, - {"server name": "y2", "name": "y2", "type": uint32_t.to_json()}, - {"server name": "y3", "name": "y3", "type": uint32_t.to_json()} - ], - "pre conds": [], - "pre allocated": [ - {"server name": "y0p", - "type": uint32_t.to_json(), - "mutable": True, - "alignment": None}, - {"server name": "y1p", - "type": uint32_t.to_json(), - "mutable": True, - "alignment": None}, - {"server name": "y2p", - "type": uint32_t.to_json(), - "mutable": True, - "alignment": None}, - {"server name": "y3p", - "type": uint32_t.to_json(), - "mutable": True, - "alignment": None} - ], - "pre points tos": [ {"pointer": y0p, "points to": y0}, - {"pointer": y1p, "points to": y1}, - {"pointer": y2p, "points to": y2}, - {"pointer": y3p, "points to": y3} ], - "argument vals": [y0p, y1p, y2p, y3p], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [ {"pointer": y0p, "points to": y0f}, - {"pointer": y1p, "points to": y1f}, - {"pointer": y2p, "points to": y2f}, - {"pointer": y3p, "points to": y3f} ], - "return val": None -} - -def oneptr_update_contract(ty, res): - return { - "pre vars": [ - {"server name": "y", "name": "y", "type": ty.to_json()} - ], - "pre conds": [], - "pre allocated": [ - {"server name": "yp", - "type": ty.to_json(), - "mutable": True, - "alignment": None} - ], - "pre points tos": [ {"pointer": yp, "points to": y} ], - "argument vals": [yp], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [ {"pointer": yp, "points to": res} ], - "return val": None - } - -rr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), rr_res) -cr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), cr_res) -dr_contract = oneptr_update_contract(LLVMArrayType(uint32_t, 16), dr_res) -hash_contract = oneptr_update_contract(LLVMArrayType(uint8_t, 64), hash_res) - -kp = {"setup value": "saved", "name" : "kp" } -np = {"setup value": "saved", "name" : "np" } -ksp = {"setup value": "saved", "name" : "ksp" } -k = {"setup value": "Cryptol", "expression" : "k" } -n = {"setup value": "Cryptol", "expression" : "n" } -zero = {"setup value": "Cryptol", "expression" : "0 : [32]" } - -expand_contract = { - "pre vars": [ - {"server name": "k", "name": "k", "type": LLVMArrayType(uint8_t, 32).to_json()}, - {"server name": "n", "name": "n", "type": LLVMArrayType(uint8_t, 16).to_json()} - ], - "pre conds": [], - "pre allocated": [ - {"server name": "kp", - "type": LLVMArrayType(uint8_t, 32).to_json(), - "mutable": True, - "alignment": None}, - {"server name": "np", - "type": LLVMArrayType(uint8_t, 16).to_json(), - "mutable": True, - "alignment": None}, - {"server name": "ksp", - "type": LLVMArrayType(uint8_t, 64).to_json(), - "mutable": True, - "alignment": None} - ], - "pre points tos": [ {"pointer": kp, "points to": k}, - {"pointer": np, "points to": n} ], - "argument vals": [kp, np, ksp], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [ {"pointer": ksp, "points to": expand_res} ], - "return val": None -} - -vp = {"setup value": "saved", "name" : "vp" } -mp = {"setup value": "saved", "name" : "mp" } -v = {"setup value": "Cryptol", "expression" : "v" } -m = {"setup value": "Cryptol", "expression" : "m" } -def crypt_contract(size : int): - return { - "pre vars": [ - {"server name": "k", "name": "k", "type": LLVMArrayType(uint8_t, 32).to_json()}, - {"server name": "v", "name": "v", "type": LLVMArrayType(uint8_t, 8).to_json()}, - {"server name": "m", "name": "m", "type": LLVMArrayType(uint8_t, size).to_json()} - ], - "pre conds": [], - "pre allocated": [ - {"server name": "kp", - "type": LLVMArrayType(uint8_t, 32).to_json(), - "mutable": True, - "alignment": None}, - {"server name": "vp", - "type": LLVMArrayType(uint8_t, 8).to_json(), - "mutable": True, - "alignment": None}, - {"server name": "mp", - "type": LLVMArrayType(uint8_t, size).to_json(), - "mutable": True, - "alignment": None} - ], - "pre points tos": [ {"pointer": kp, "points to": k}, - {"pointer": vp, "points to": v}, - {"pointer": mp, "points to": m} ], - "argument vals": [kp, vp, zero, mp, {"setup value": "Cryptol", "expression": (str(size) + " : [32]")}], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [ {"pointer": mp, "points to": crypt_res} ], - "return val": zero - } - -prover = ProofScript([abc]).to_json() - -print("Verifying rotl") -c.llvm_verify('m', 'rotl', [], False, rotl_contract, prover, 'rotl_ov').result() - -print("Verifying s20_quarterround") -c.llvm_verify('m', 's20_quarterround', ['rotl_ov'], False, qr_contract, prover, 'qr_ov').result() - -print("Verifying s20_rowround") -c.llvm_verify('m', 's20_rowround', ['qr_ov'], False, rr_contract, prover, 'rr_ov').result() - -print("Verifying s20_columnround") -c.llvm_verify('m', 's20_columnround', ['rr_ov'], False, cr_contract, prover, 'cr_ov').result() - -print("Verifying s20_doubleround") -c.llvm_verify('m', 's20_doubleround', ['cr_ov', 'rr_ov'], False, dr_contract, prover, 'dr_ov').result() - -print("Verifying s20_hash") -c.llvm_verify('m', 's20_hash', ['dr_ov'], False, hash_contract, prover, 'hash_ov').result() - -print("Verifying s20_expand32") -c.llvm_verify('m', 's20_expand32', ['hash_ov'], False, expand_contract, prover, 'expand_ov').result() - -print("Verifying s20_crypt32") -c.llvm_verify('m', 's20_crypt32', ['expand_ov'], False, crypt_contract(63), prover, 'crypt_ov').result() - -print("Done") diff --git a/saw-remote-api/test-scripts/salsa20_easy.py b/saw-remote-api/test-scripts/salsa20_easy.py deleted file mode 100644 index ebdacb2..0000000 --- a/saw-remote-api/test-scripts/salsa20_easy.py +++ /dev/null @@ -1,184 +0,0 @@ -import os -import os.path -from cryptol.cryptoltypes import to_cryptol -from saw import * -from saw.llvm import Contract, LLVMArrayType, uint8_t, uint32_t, void - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -connect("cabal new-exec --verbose=0 saw-remote-api") -view(LogResults()) - -bcname = os.path.join(dir_path, 'salsa20.bc') -cryname = os.path.join(dir_path, 'Salsa20.cry') - -cryptol_load_file(cryname) - -mod = llvm_load_module(bcname) - -class RotlContract(Contract): - def pre(self): - self.value = self.declare(uint32_t) - self.shift = self.declare(uint32_t) - self.proclaim(self.shift > self.cryptol("0")) - self.proclaim(self.shift < self.cryptol("32")) - def call(self): - self.arguments(self.value, self.shift) - def post(self): - self.returns(self.cryptol("(<<<)")(self.value, self.shift)) - - -rotl_result = llvm_verify(mod, 'rotl', RotlContract()) - -class TrivialContract(Contract): - def post(self): self.returns(void) - -class QuarterRoundContract(Contract): - def pre(self): - self.y0 = self.declare(uint32_t) - self.y1 = self.declare(uint32_t) - self.y2 = self.declare(uint32_t) - self.y3 = self.declare(uint32_t) - - self.y0_p = self.declare_pointer(uint32_t) - self.y1_p = self.declare_pointer(uint32_t) - self.y2_p = self.declare_pointer(uint32_t) - self.y3_p = self.declare_pointer(uint32_t) - - self.points_to(self.y0_p, self.y0) - self.points_to(self.y1_p, self.y1) - self.points_to(self.y2_p, self.y2) - self.points_to(self.y3_p, self.y3) - - def call(self): - self.arguments(self.y0_p, self.y1_p, self.y2_p, self.y3_p) - - def post(self): - self.points_to(self.y0_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("0"))) - self.points_to(self.y1_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("1"))) - self.points_to(self.y2_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("2"))) - self.points_to(self.y3_p, - self.cryptol("(@)")(self.cryptol("quarterround")([self.y0, self.y1, self.y2, self.y3]), - self.cryptol("3"))) - self.returns(void) - - -qr_result = llvm_verify(mod, 's20_quarterround', QuarterRoundContract(), lemmas=[rotl_result]) - - -class OnePointerUpdateContract(Contract): - def __init__(self, the_type): - super().__init__() - self.t = the_type - - - def pre(self): - self.y = self.declare(self.t) - self.y_p = self.declare_pointer(self.t) - self.points_to(self.y_p, self.y) - - def call(self): - self.arguments(self.y_p) - - def post(self): - - self.returns(void) - - -class RowRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("rowround")(self.y)) - -rr_result = llvm_verify(mod, 's20_rowround', RowRoundContract(), lemmas=[qr_result]) - - -class ColumnRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("columnround")(self.y)) - -cr_result = llvm_verify(mod, 's20_columnround', ColumnRoundContract(), lemmas=[rr_result]) - - -class DoubleRoundContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint32_t, 16)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("doubleround")(self.y)) - -dr_result = llvm_verify(mod, 's20_doubleround', DoubleRoundContract(), lemmas=[cr_result, rr_result]) - - -class HashContract(OnePointerUpdateContract): - def __init__(self): - super().__init__(LLVMArrayType(uint8_t, 64)) - - def post(self): - super().post() - self.points_to(self.y_p, self.cryptol("Salsa20")(self.y)) - -hash_result = llvm_verify(mod, 's20_hash', HashContract(), lemmas=[dr_result]) - - -class ExpandContract(Contract): - def pre(self): - self.k = self.declare(LLVMArrayType(uint8_t, 32)) - self.n = self.declare(LLVMArrayType(uint8_t, 16)) - - self.k_p = self.declare_pointer(LLVMArrayType(uint8_t, 32)) - self.n_p = self.declare_pointer(LLVMArrayType(uint8_t, 16)) - self.ks_p = self.declare_pointer(LLVMArrayType(uint8_t, 64)) - - self.points_to(self.k_p, self.k) - self.points_to(self.n_p, self.n) - - def call(self): - self.arguments(self.k_p, self.n_p, self.ks_p) - - def post(self): - self.returns(void) - self.points_to(self.ks_p, self.cryptol("Salsa20_expansion`{a=2}")((self.k, self.n))) - -expand_result = llvm_verify(mod, 's20_expand32', ExpandContract(), lemmas=[hash_result]) - - -class Salsa20CryptContract(Contract): - def __init__(self, size): - super().__init__() - self.size = size - self.zero = self.cryptol("0 : [32]") - - def val_and_pointer(self, t): - v = self.declare(t) - p = self.declare_pointer(t) - self.points_to(p, v) - return (v, p) - - def pre(self): - (self.k, self.k_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 32)) - (self.v, self.v_p) = self.val_and_pointer(LLVMArrayType(uint8_t, 8)) - (self.m, self.m_p) = self.val_and_pointer(LLVMArrayType(uint8_t, self.size)) - - def call(self): - self.arguments(self.k_p, self.v_p, self.zero, self.m_p, self.cryptol(str(self.size) + " : [32]")) - - def post(self): - self.returns(self.zero) - self.points_to(self.m_p, self.cryptol("Salsa20_encrypt")((self.k, self.v, self.m))) - -crypt_result = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(63), lemmas=[expand_result]) diff --git a/saw-remote-api/test-scripts/saw-test.py b/saw-remote-api/test-scripts/saw-test.py deleted file mode 100644 index f42e9aa..0000000 --- a/saw-remote-api/test-scripts/saw-test.py +++ /dev/null @@ -1,37 +0,0 @@ -print("Starting") -import os -import os.path -import saw.connection as saw -from saw.proofscript import * - -print("Imported") - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -print("This is " + dir_path) - -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -cry_file = os.path.join(dir_path, 'Foo.cry') -c.cryptol_load_file(cry_file) - - -null_bc = os.path.join(dir_path, 'null.bc') - -c.llvm_load_module('m', null_bc).result() - -contract = { - "pre vars": [], - "pre conds": [], - "pre allocated": [], - "pre points tos": [], - "argument vals": [], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [], - "return val": {"setup value": "null value"} -} - -prover = ProofScript([abc]).to_json() -print(c.llvm_verify('m', 'always_null', [], False, contract, prover, 'ok').result()) diff --git a/saw-remote-api/test-scripts/seven.bc b/saw-remote-api/test-scripts/seven.bc deleted file mode 100644 index 4d1d393a860033d93e75d5d83c53c50e44e580a8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 1996 zcmaJ?Uu;@c7(Z~^9=gFT+Zv_r-s`>VoXo6~(TP-AQ+m6~v=1!qVJ0(!t*z8Qj9xmp z&}m?x2bCB$_rSv*VEQoMYBbRpv$SPSBxLETF@%s>vPznz*2X`{9!&H*Z0duHCpmw< z^XEI?_x*m~IYaW?@)Mm1wIYO0>Mgquzi@TW&)+`XGpw=FDJ1C;`a*-yR;`4zAU^;V z$Gguvi!F!SjMlyjnxy`bR$Z6S^6tr){*ZR)!q%ZNqqWnnGd;J(YE8KU*QD;@?Idk< zUeJyebsu+%@<>YjMq{-mO^=x$%N#g6d;GjuD1zQ2CWJ0SzjO4_JAXpa1W>z~5%sAl z6-P2eG2y6(ob@pgl|%zrF=NHYC@wtXf-$jWiJHMt9}|obn~wx?cp8-@uHqF+8nGzx z4T-xJ=Sz9Rn#3)|`KpIoi1VU;D!bbmKq9q#`*IFp)Fheuji|P3!lO+2$1L;u|ce_5W~2eeQlAALYrYjgTQe-z1Y@>VX$RN#Oh+(Mhr)dIF!Rd z@!skuMy$l}Ly|t?8a{OJs%1?34nnc!rO;>xPbLPB`~Wlij5LX@LRQzcZ8Vc^-}B7% z7I~<>Q;R+Z-)3N~R~O^1)wzjI%|J@FCkyEz;6DT;JEd=+j-QO|Z!xx4KO`(rl(`8@ zYjay-XPFr&$^&U;psc2W-ZMHJaghMMbxVie(s65(-E_0P#%ugC zq@=_zc!dee+m0_2jzzieQ>OpRM1PWTls7v=9z5g2PtwG}PsS+v0S^wDap+Dfs13)+ z2_2a-0S6#eg!brG%sG-hIyz4+*PS%^n&3Ez?0GAiUgs zF(iI@o_|9F?*Lbp_)Txy(Ki$Ja=|ex4?sZvSm94lXM=1>U=;#}wWaGzg z8QJwY_D47StEGE>$tkSXAFR~*WiY_i<(N$je45yqEZEa>U%Al#`Fvlo06z8u)F>h% z^a%8d;1cDOzN=lay2S2y`uzEu!#SgQtp9*@=)H{ef!P>F&pw1u_>|A9oCr=v$4|ZL z^}i&B#+BgYX}@USZ`p4V%_HMurxovAspr7{iBr9ny{KC^XgP;;y?S}DY}8q|XLIRF zWxaa5x?H?nDIG6Y7H%{~+EYiHlS{=?ZEd7|3)u7#@R8=%)-CXshk@|N0$F(g;F^{D z77OPZ+;w=los@ujc0*4K?diIY3Q(vY z;0D?S6+_(%_3uLW{avUoT4+!IIkdYeq8H(A7KU*5B%KM4hsOQQV5@f93ERP*GyYfn Zr^Ei9S10{v)Sj38XPP_qpSpV-{RII@o6P_K diff --git a/saw-remote-api/test-scripts/seven.c b/saw-remote-api/test-scripts/seven.c deleted file mode 100644 index 43a2add..0000000 --- a/saw-remote-api/test-scripts/seven.c +++ /dev/null @@ -1,4 +0,0 @@ - -int seven() { - return 7; -} diff --git a/saw-remote-api/test-scripts/seven.py b/saw-remote-api/test-scripts/seven.py deleted file mode 100644 index d57995c..0000000 --- a/saw-remote-api/test-scripts/seven.py +++ /dev/null @@ -1,28 +0,0 @@ -import os -import os.path -import saw.connection as saw -from saw.proofscript import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -seven_bc = os.path.join(dir_path, 'seven.bc') - -c.llvm_load_module('m', seven_bc).result() - -contract = { - "pre vars": [], - "pre conds": [], - "pre allocated": [], - "pre points tos": [], - "argument vals": [], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [], - "return val": {"setup value": "Cryptol", "expression": "7 : [32]"} -} - -prover = ProofScript([abc]).to_json() -print(c.llvm_verify('m', 'seven', [], False, contract, prover, 'ok').result()) diff --git a/saw-remote-api/test-scripts/swap.bc b/saw-remote-api/test-scripts/swap.bc deleted file mode 100644 index e6293c8daa14749d27295f90c3c3be622aabd31d..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 2236 zcmZ`)Z%kX)6~B*Xd`&RVF9c;cy!ZNCSmd-Ld6>*KHB2^-F{g_(qUHnBm|`bDVI$^Y z9REu>R)=BwLX*bU%y<~{$>k8^$4NsMycb{_dh!O*{9#?9H4BP3R#Q@eMTYF zSZ6_Xus;nG$J-a&W!)t`YwNj3C5>ONH<$(8&#$Y-Z`bwTYwRCoZ7mK%>vvDsZ1Wyv z+0s7HOj4}-UfpQf@NSDJ56+8!q-?fi>r2*`(p_)nM;63V8T?*pMd;Tc+g8s$`8Nzo zrCoJJwUva^IBF#`SsW@8dzyq7aabe)k=R8N%#$FjClb+l9L*BDgd-D)kO9YBxWE?v-r$jw9jL;?En#Si-cU`bT=q(W;pgOX>ST=~GcXYqB zypx2-!(=Yq(tP=DsxdiwndREitj_B?M|W(x3LIqx`%}`J1={(f-kD97ysbbc3ir4jH-;8C1)uIK-=iwU!2pn%i_gTf+#A#u3;dn~*V@PhL)^ z8qR)aMJK=3&{7xGjNgT9Z-eYMsNC`{H{L?^&C8BtDb-)Ybv83&+()Lrv&`oz({1dB zTJr$pxKv*=OSDz!zOvkxqWdb5R8YaU0ZtE56dY6NP=qKVF;`A9hiPV4GWjLb!z1Qs zi0NjR`E6(z3t#jJ(T0&lYdjh{Q0bPe*QHhdeD|+%RObe zCsTWVP;%Ut9rLvFe(3^y^ou#?Uub8(Wc+xND8nS6B!Uw-0+>PPXNh_3b<<;H`o|En zmu4QiOuHg;2w8|$=v9r`8y0RWE^O^^d%OH2N*Hgw;>gRdzMXJZhB}@m0?doxNao7r z&(kKY0>Y1kRUda?;kTFgpHhMru!TSJ>95{NI4UJ)Uhac}d{OM(lb!RhEv5c&f<%GG z5DzfeiUXPW$U~MnEHHl?V*V+$FKxJmz1^=>clm7yz+-mi6MgR|+L9$lO75wYdOuj| zDVHF}UVs`!MT9Pb39#1VSd@_(_t)snNw*FtFEx#QWKSHmaF@8_u zN%+QuFK}&kGB$Q&%IAMW42=b5C#U_QM->D;70IDOMU zsZ0mQ{6SGW|N7)jWok^6FUT*yEMDz*yAf(P#HBgb*ly5wmAtx-jd4jHsz_|3tt3fh zqx`98YtCd-)#~Bq$mVwWQFV2sQZ26S4>qK))|4CN)vbfUhGqy6{SLU?2(s}+zzQ6} zv0)`6_W{&-xo5pJx6iE{-)V3|TKMDIqfb~=>knM%eJA038wf%7WfQ$Xj&wA|B~XWuu@-VYGVf_6g*Zg=;$ofg$!W(-2Ywh&${0m zljg?%r0D+qD@(%}c>m?M=3OXNe@8-YEpmir#N!xj4EtgdEz_-PUrj#-7eza)n(6zZ zW~oi>uG4ZEc)EWUuqL$&MTM!2lQ6Xl@*GUoO`;^EuFb-smV-bh_n*CzuE&q@G(_w$-)TIAbr1K5`EzRKk I4ebc}4@B9_1^@s6 diff --git a/saw-remote-api/test-scripts/swap.c b/saw-remote-api/test-scripts/swap.c deleted file mode 100644 index 3780446..0000000 --- a/saw-remote-api/test-scripts/swap.c +++ /dev/null @@ -1,13 +0,0 @@ -#include - -void swap(uint32_t *a, uint32_t *b) { - uint32_t tmp = *a; - *a = *b; - *b = tmp; -} - -void xor_swap(uint32_t *a, uint32_t *b) { - *a ^= *b; - *b ^= *a; - *a ^= *b; -} diff --git a/saw-remote-api/test-scripts/swap.py b/saw-remote-api/test-scripts/swap.py deleted file mode 100644 index f8df5e6..0000000 --- a/saw-remote-api/test-scripts/swap.py +++ /dev/null @@ -1,54 +0,0 @@ -import os -import os.path -import saw.connection as saw -from saw.proofscript import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -swap_bc = os.path.join(dir_path, 'swap.bc') - -c.llvm_load_module('m', swap_bc).result() - -uint32_t = {"type": "primitive type", "primitive": "integer", "size": 32} - -# ServerNames -xp_name = {"name": "xp"} -yp_name = {"name": "yp"} - -# SetupVals -xp = {"setup value": "saved", "name": "xp"} -yp = {"setup value": "saved", "name": "yp"} -x = {"setup value": "Cryptol", "expression": "x" } -y = {"setup value": "Cryptol", "expression": "x" } - -contract = { - "pre vars": [ - {"server name": "x", "name": "x", "type": uint32_t}, - {"server name": "y", "name": "y", "type": uint32_t} - ], - "pre conds": [], - "pre allocated": [ - {"server name": "xp", - "type": uint32_t, - "mutable": True, - "alignment": None}, - {"server name": "yp", - "type": uint32_t, - "mutable": True, - "alignment": None} - ], - "pre points tos": [{"pointer": xp, "points to": x}, - {"pointer": yp, "points to": y}], - "argument vals": [xp, yp], - "post vars": [], - "post conds": [], - "post allocated": [], - "post points tos": [{"pointer": xp, "points to": y}, - {"pointer": yp, "points to": x}], - "return val": None -} - -prover = ProofScript([abc]).to_json() -print(c.llvm_verify('m', 'swap', [], False, contract, prover, 'ok').result()) diff --git a/saw-remote-api/test-scripts/swap_easy.py b/saw-remote-api/test-scripts/swap_easy.py deleted file mode 100644 index 983602d..0000000 --- a/saw-remote-api/test-scripts/swap_easy.py +++ /dev/null @@ -1,35 +0,0 @@ -from saw import * -from saw.llvm import uint32_t, Contract, void - -import os -import os.path - -dir_path = os.path.dirname(os.path.realpath(__file__)) -swap_bc = os.path.join(dir_path, 'swap.bc') - -class Swap(Contract): - def __init__(self) -> None: - super().__init__() - self.t = uint32_t - - def pre(self) -> None: - self.x = self.declare(self.t) - self.y = self.declare(self.t) - self.x_pointer = self.declare_pointer(self.t) - self.y_pointer = self.declare_pointer(self.t) - self.points_to(self.x_pointer, self.x) - self.points_to(self.y_pointer, self.y) - - def call(self) -> None: - self.arguments(self.x_pointer, self.y_pointer) - - def post(self) -> None: - self.points_to(self.x_pointer, self.y) - self.points_to(self.y_pointer, self.x) - self.returns(void) - -connect("cabal new-exec --verbose=0 saw-remote-api") - -mod = llvm_load_module(swap_bc) - -result = llvm_verify(mod, 'swap', Swap()) diff --git a/saw-remote-api/test-scripts/swap_fancy.py b/saw-remote-api/test-scripts/swap_fancy.py deleted file mode 100644 index fc11938..0000000 --- a/saw-remote-api/test-scripts/swap_fancy.py +++ /dev/null @@ -1,39 +0,0 @@ -import os -import os.path -import saw.connection as saw -from saw.llvm import uint32_t, Contract, void -from saw.proofscript import * - -dir_path = os.path.dirname(os.path.realpath(__file__)) - -c = saw.connect("cabal new-exec --verbose=0 saw-remote-api") - -swap_bc = os.path.join(dir_path, 'swap.bc') - -c.llvm_load_module('m', swap_bc).result() - -class Swap(Contract): - def __init__(self) -> None: - super().__init__() - self.t = uint32_t - - def pre(self) -> None: - self.x = self.declare(self.t) - self.y = self.declare(self.t) - self.x_pointer = self.declare_pointer(self.t) - self.y_pointer = self.declare_pointer(self.t) - self.points_to(self.x_pointer, self.x) - self.points_to(self.y_pointer, self.y) - - def call(self) -> None: - self.arguments(self.x_pointer, self.y_pointer) - - def post(self) -> None: - self.points_to(self.x_pointer, self.y) - self.points_to(self.y_pointer, self.x) - self.returns(void) - -contract = Swap() - -prover = ProofScript([abc]).to_json() -print(c.llvm_verify('m', 'swap', [], False, contract.to_json(), prover, 'ok').result()) diff --git a/saw-remote-api/test/Test.hs b/saw-remote-api/test/Test.hs deleted file mode 100644 index 8fdffd4..0000000 --- a/saw-remote-api/test/Test.hs +++ /dev/null @@ -1,25 +0,0 @@ -{-# LANGUAGE NamedFieldPuns #-} - -module Main where - -import System.FilePath (()) - -import Test.Tasty -import Test.Tasty.HUnit -import Test.Tasty.HUnit.ScriptExit - -import Paths_saw_remote_api -import Argo.PythonBindings - -main :: IO () -main = - do reqs <- getArgoPythonFile "requirements.txt" - withPython3venv (Just reqs) $ \pip python -> - do pySrc <- getArgoPythonFile "." - testScriptsDir <- getDataFileName "test-scripts/" - pip ["install", pySrc] - - scriptTests <- makeScriptTests testScriptsDir [python] - - defaultMain $ - testGroup "Tests for saw-remote-api" scriptTests