diff --git a/.github/ci.sh b/.github/ci.sh index c5e4fc0337..8707e34e38 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -10,7 +10,7 @@ mkdir -p "$BIN" is_exe() { [[ -x "$1/$2$EXT" ]] || command -v "$2" > /dev/null 2>&1; } extract_exe() { - exe="$(cabal v2-exec which "$1$EXT")" + exe="$(find dist-newstyle -type f -name "$1$EXT")" name="$(basename "$exe")" echo "Copying $name to $2" mkdir -p "$2" @@ -38,9 +38,10 @@ retry() { } setup_dist_bins() { - is_exe "dist/bin" "saw" && is_exe "dist/bin" "jss" && return + is_exe "dist/bin" "saw" && is_exe "dist/bin" "jss" && is_exe "dist/bin" "saw-remote-api" && return extract_exe "saw" "dist/bin" extract_exe "jss" "dist/bin" + extract_exe "saw-remote-api" "dist/bin" export PATH=$PWD/dist/bin:$PATH echo "::add-path::$PWD/dist/bin" strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error" @@ -117,12 +118,12 @@ build() { ghc_ver="$(ghc --numeric-version)" cp cabal.GHC-"$ghc_ver".config cabal.project.freeze cabal v2-update - cabal v2-configure -j2 --minimize-conflict-set + echo "allow-newer: all" >> cabal.project.local tee -a cabal.project > /dev/null < cabal.project.ci - if ! retry cabal v2-build "$@" saw jss && [[ "$RUNNER_OS" == "macOS" ]]; then + if ! retry cabal v2-build "$@" jss saw saw-remote-api && [[ "$RUNNER_OS" == "macOS" ]]; then echo "Working around a dylib issue on macos by removing the cache and trying again" cabal v2-clean - retry cabal v2-build "$@" saw jss + retry cabal v2-build "$@" jss saw saw-remote-api fi } @@ -150,7 +151,6 @@ install_system_deps() { } test_dist() { - setup_dist_bins find_java pushd intTests for t in test0001 test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_examples test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done @@ -171,7 +171,6 @@ bundle_files() { cp deps/abcBridge/abc-build/copyright.txt dist/ABC_LICENSE cp LICENSE README.md dist/ $IS_WIN || chmod +x dist/bin/* - rm -f "dist/bin/jss" cp doc/extcore.md dist/doc cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 607ca33ea5..5e8440486c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -53,11 +53,17 @@ jobs: git submodule update --init git -C deps/abcBridge submodule update --init + - uses: actions/setup-python@v2 + with: + python-version: '3.x' + + - shell: bash + run: pip3 install virtualenv + - uses: actions/setup-haskell@v1 id: setup-haskell with: ghc-version: ${{ matrix.ghc }} - enable-stack: true - uses: actions/cache@v2 name: Cache cabal store @@ -82,6 +88,16 @@ jobs: CVC4_VERSION: "4.1.8" YICES_VERSION: "2.6.2" + - shell: bash + run: .github/ci.sh setup_dist_bins + + - shell: bash + # TODO: change this once we can get these tests working in CI + continue-on-error: true + run: cabal v2-test saw-remote-api + env: + SAW_SERVER: ${GITHUB_WORKSPACE}/dist/bin/saw-remote-api + - uses: actions/setup-java@v1 with: java-version: "8" @@ -93,8 +109,6 @@ jobs: continue-on-error: ${{ matrix.continue-on-error }} name: Integration Tests run: | - mkdir -p ~/.stack - echo "system-ghc: true" >> ~/.stack/config.yaml .github/ci.sh test_dist - if: >- diff --git a/.gitmodules b/.gitmodules index 316bddb18f..f417eb4edb 100644 --- a/.gitmodules +++ b/.gitmodules @@ -49,3 +49,6 @@ [submodule "deps/saw-core-coq"] path = deps/saw-core-coq url = https://github.com/GaloisInc/saw-core-coq.git +[submodule "deps/argo"] + path = deps/argo + url = https://github.com/galoisinc/argo diff --git a/cabal.project b/cabal.project index 83108c6a80..99ef3766f6 100644 --- a/cabal.project +++ b/cabal.project @@ -1,5 +1,6 @@ packages: saw-script.cabal + saw-remote-api deps/llvm-pretty deps/llvm-pretty-bc-parser deps/jvm-parser @@ -29,3 +30,7 @@ packages: deps/macaw/x86_symbolic deps/elf-edit deps/dwarf + deps/argo/argo + deps/argo/tasty-script-exitcode + deps/argo/python + deps/cryptol/cryptol-remote-api diff --git a/deps/argo b/deps/argo new file mode 160000 index 0000000000..196d227988 --- /dev/null +++ b/deps/argo @@ -0,0 +1 @@ +Subproject commit 196d227988c4e72315066e7f052f91f9ec4b4615 diff --git a/deps/cryptol b/deps/cryptol index 72611f77bd..f0b851ecf0 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 72611f77bd2fa27e3fb497197dd4cac4bbe3fef7 +Subproject commit f0b851ecf0a470c893ef4d98e9b199dafe64f1bf diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md new file mode 100644 index 0000000000..48ff3f1520 --- /dev/null +++ b/saw-remote-api/CHANGELOG.md @@ -0,0 +1,5 @@ +# 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 new file mode 100644 index 0000000000..76ed25f831 --- /dev/null +++ b/saw-remote-api/LICENSE @@ -0,0 +1,29 @@ +BSD 3-Clause License + +Copyright (c) 2019, Galois, Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +3. Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/saw-remote-api/Setup.hs b/saw-remote-api/Setup.hs new file mode 100644 index 0000000000..9a994af677 --- /dev/null +++ b/saw-remote-api/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal new file mode 100644 index 0000000000..c04068bbab --- /dev/null +++ b/saw-remote-api/saw-remote-api.cabal @@ -0,0 +1,112 @@ +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 new file mode 100644 index 0000000000..3bcafcd1da --- /dev/null +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -0,0 +1,49 @@ +{-# 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 new file mode 100644 index 0000000000..e69de29bb2 diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs new file mode 100644 index 0000000000..25a5c3a8d0 --- /dev/null +++ b/saw-remote-api/src/SAWServer.hs @@ -0,0 +1,384 @@ +{-# 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 new file mode 100644 index 0000000000..f313c68670 --- /dev/null +++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs @@ -0,0 +1,99 @@ +{-# 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 new file mode 100644 index 0000000000..e0bbacbc05 --- /dev/null +++ b/saw-remote-api/src/SAWServer/CryptolSetup.hs @@ -0,0 +1,72 @@ +{-# 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 new file mode 100644 index 0000000000..356d4b52c5 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Data/Contract.hs @@ -0,0 +1,93 @@ +{-# 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 new file mode 100644 index 0000000000..1f417e732b --- /dev/null +++ b/saw-remote-api/src/SAWServer/Data/JVMType.hs @@ -0,0 +1,76 @@ +{-# 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 new file mode 100644 index 0000000000..b8ac57d216 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Data/LLVMType.hs @@ -0,0 +1,115 @@ +{-# 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 new file mode 100644 index 0000000000..7047a83f39 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs @@ -0,0 +1,48 @@ +{-# 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 new file mode 100644 index 0000000000..60567ceb08 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Exceptions.hs @@ -0,0 +1,178 @@ +{-# 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 new file mode 100644 index 0000000000..c67afed0c1 --- /dev/null +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -0,0 +1,196 @@ +{-# 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 new file mode 100644 index 0000000000..630408030c --- /dev/null +++ b/saw-remote-api/src/SAWServer/JVMVerify.hs @@ -0,0 +1,60 @@ +{-# 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 new file mode 100644 index 0000000000..fc8af24ba1 --- /dev/null +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -0,0 +1,210 @@ +{-# 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 new file mode 100644 index 0000000000..6de1ad2d58 --- /dev/null +++ b/saw-remote-api/src/SAWServer/LLVMVerify.hs @@ -0,0 +1,78 @@ +{-# 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 new file mode 100644 index 0000000000..dcd137698f --- /dev/null +++ b/saw-remote-api/src/SAWServer/NoParams.hs @@ -0,0 +1,11 @@ +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 new file mode 100644 index 0000000000..eed8ea1e84 --- /dev/null +++ b/saw-remote-api/src/SAWServer/OK.hs @@ -0,0 +1,12 @@ +{-# 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 new file mode 100644 index 0000000000..b9da5205a0 --- /dev/null +++ b/saw-remote-api/src/SAWServer/ProofScript.hs @@ -0,0 +1,155 @@ +{-# 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 new file mode 100644 index 0000000000..fbcef3d5d6 --- /dev/null +++ b/saw-remote-api/src/SAWServer/SaveTerm.hs @@ -0,0 +1,25 @@ +{-# 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 new file mode 100644 index 0000000000..0df1a8a5ae --- /dev/null +++ b/saw-remote-api/src/SAWServer/SetOption.hs @@ -0,0 +1,46 @@ +{-# 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 new file mode 100644 index 0000000000..0e4aea779e --- /dev/null +++ b/saw-remote-api/src/SAWServer/Term.hs @@ -0,0 +1,26 @@ +{-# 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 new file mode 100644 index 0000000000..b3c632c1ea --- /dev/null +++ b/saw-remote-api/src/SAWServer/TopLevel.hs @@ -0,0 +1,26 @@ +{-# 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 new file mode 100644 index 0000000000..5bec3b5cd5 --- /dev/null +++ b/saw-remote-api/src/SAWServer/TrackFile.hs @@ -0,0 +1,24 @@ +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 new file mode 100644 index 0000000000..950cf002d1 --- /dev/null +++ b/saw-remote-api/src/SAWServer/VerifyCommon.hs @@ -0,0 +1,94 @@ +{-# 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 new file mode 100644 index 0000000000..4a3dd15152 --- /dev/null +++ b/saw-remote-api/test-scripts/Foo.cry @@ -0,0 +1,17 @@ +module Foo where + +id : {a} a -> a +id x = x + +x : [8] +x = 255 + +add : {a} (fin a) => [a] -> [a] -> [a] +add = (+) + +foo : {foo : [32], bar : [32]} +foo = {foo = 23, bar = 99} + +getFoo : {foo : [32], bar : [32]} -> [32] +getFoo x = x.foo + diff --git a/saw-remote-api/test-scripts/Salsa20.cry b/saw-remote-api/test-scripts/Salsa20.cry new file mode 100644 index 0000000000..782d5d96be --- /dev/null +++ b/saw-remote-api/test-scripts/Salsa20.cry @@ -0,0 +1,182 @@ +/* + * 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 new file mode 100644 index 0000000000..606bd7170f Binary files /dev/null and b/saw-remote-api/test-scripts/assume.bc differ diff --git a/saw-remote-api/test-scripts/assume.c b/saw-remote-api/test-scripts/assume.c new file mode 100644 index 0000000000..ec74e0409d --- /dev/null +++ b/saw-remote-api/test-scripts/assume.c @@ -0,0 +1,5 @@ +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 new file mode 100644 index 0000000000..37bba4d107 --- /dev/null +++ b/saw-remote-api/test-scripts/assume.py @@ -0,0 +1,42 @@ +import os +import os.path +import saw.connection as saw +from saw.proofscript import * +from env_server import * + +c = env_connect() + +dir_path = os.path.dirname(os.path.realpath(__file__)) +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/env_server.py b/saw-remote-api/test-scripts/env_server.py new file mode 100644 index 0000000000..131764f613 --- /dev/null +++ b/saw-remote-api/test-scripts/env_server.py @@ -0,0 +1,17 @@ +import os +import saw as saw +import saw.connection as conn + +def env_connect(): + server = os.environ.get('SAW_SERVER') + if not server: + server = "cabal new-exec --verbose=0 saw-remote-api" + print("Running: " + server) + return conn.connect(server) + +def env_connect_global(): + server = os.environ.get('SAW_SERVER') + if not server: + server = "cabal new-exec --verbose=0 saw-remote-api" + print("Running: " + server) + saw.connect(server) diff --git a/saw-remote-api/test-scripts/null.bc b/saw-remote-api/test-scripts/null.bc new file mode 100644 index 0000000000..bcf62757e0 Binary files /dev/null and b/saw-remote-api/test-scripts/null.bc differ diff --git a/saw-remote-api/test-scripts/null.c b/saw-remote-api/test-scripts/null.c new file mode 100644 index 0000000000..38a8c0728d --- /dev/null +++ b/saw-remote-api/test-scripts/null.c @@ -0,0 +1,3 @@ +int *always_null () { + return 0; +} diff --git a/saw-remote-api/test-scripts/salsa20.bc b/saw-remote-api/test-scripts/salsa20.bc new file mode 100644 index 0000000000..808474461b Binary files /dev/null and b/saw-remote-api/test-scripts/salsa20.bc differ diff --git a/saw-remote-api/test-scripts/salsa20.c b/saw-remote-api/test-scripts/salsa20.c new file mode 100644 index 0000000000..fd951639d5 --- /dev/null +++ b/saw-remote-api/test-scripts/salsa20.c @@ -0,0 +1,191 @@ +#include +#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 new file mode 100644 index 0000000000..df94eed6b1 --- /dev/null +++ b/saw-remote-api/test-scripts/salsa20.h @@ -0,0 +1,72 @@ +#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 new file mode 100755 index 0000000000..d01ddcaf9d --- /dev/null +++ b/saw-remote-api/test-scripts/salsa20.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +import os +import os.path +import saw.connection as saw +from saw.llvm import * +from saw.proofscript import * +from env_server import * + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +print("Starting server") +c = env_connect() + +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 new file mode 100644 index 0000000000..6b2d807b4e --- /dev/null +++ b/saw-remote-api/test-scripts/salsa20_easy.py @@ -0,0 +1,185 @@ +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 +from env_server import * + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +env_connect_global() +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 new file mode 100644 index 0000000000..53c6e1c93a --- /dev/null +++ b/saw-remote-api/test-scripts/saw-test.py @@ -0,0 +1,38 @@ +print("Starting") +import os +import os.path +import saw.connection as saw +from saw.proofscript import * +from env_server import * + +print("Imported") + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +print("This is " + dir_path) + +c = env_connect() + +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 new file mode 100644 index 0000000000..4d1d393a86 Binary files /dev/null and b/saw-remote-api/test-scripts/seven.bc differ diff --git a/saw-remote-api/test-scripts/seven.c b/saw-remote-api/test-scripts/seven.c new file mode 100644 index 0000000000..43a2add6af --- /dev/null +++ b/saw-remote-api/test-scripts/seven.c @@ -0,0 +1,4 @@ + +int seven() { + return 7; +} diff --git a/saw-remote-api/test-scripts/seven.py b/saw-remote-api/test-scripts/seven.py new file mode 100644 index 0000000000..25c077d4d4 --- /dev/null +++ b/saw-remote-api/test-scripts/seven.py @@ -0,0 +1,29 @@ +import os +import os.path +import saw.connection as saw +from saw.proofscript import * +from env_server import * + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +c = env_connect() + +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 new file mode 100644 index 0000000000..e6293c8daa Binary files /dev/null and b/saw-remote-api/test-scripts/swap.bc differ diff --git a/saw-remote-api/test-scripts/swap.c b/saw-remote-api/test-scripts/swap.c new file mode 100644 index 0000000000..37804462ba --- /dev/null +++ b/saw-remote-api/test-scripts/swap.c @@ -0,0 +1,13 @@ +#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 new file mode 100644 index 0000000000..272da1ec0c --- /dev/null +++ b/saw-remote-api/test-scripts/swap.py @@ -0,0 +1,55 @@ +import os +import os.path +import saw.connection as saw +from saw.proofscript import * +from env_server import * + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +c = env_connect() + +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 new file mode 100644 index 0000000000..8f95ad6d24 --- /dev/null +++ b/saw-remote-api/test-scripts/swap_easy.py @@ -0,0 +1,36 @@ +from saw import * +from saw.llvm import uint32_t, Contract, void + +import os +import os.path +from env_server import * + +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) + +env_connect_global() + +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 new file mode 100644 index 0000000000..1be18c8fb5 --- /dev/null +++ b/saw-remote-api/test-scripts/swap_fancy.py @@ -0,0 +1,40 @@ +import os +import os.path +import saw.connection as saw +from saw.llvm import uint32_t, Contract, void +from saw.proofscript import * +from env_server import * + +dir_path = os.path.dirname(os.path.realpath(__file__)) + +c = env_connect() + +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 new file mode 100644 index 0000000000..8fdffd4185 --- /dev/null +++ b/saw-remote-api/test/Test.hs @@ -0,0 +1,25 @@ +{-# 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 diff --git a/stack.ghc-8.6.yaml b/stack.ghc-8.6.yaml index 6d5a0f85c3..4a5698430b 100644 --- a/stack.ghc-8.6.yaml +++ b/stack.ghc-8.6.yaml @@ -30,6 +30,7 @@ packages: - deps/macaw/x86 - deps/macaw/x86_symbolic - . + - saw-remote-api extra-deps: - zenc-0.1.1@sha256:e4be3e5e9fe1a1ade05910909c6e5b5a8eff72e697868b03955c9781b0443947 - IfElse-0.85 diff --git a/stack.ghc-8.8.yaml b/stack.ghc-8.8.yaml index fc0737f1ca..832fce4ddb 100644 --- a/stack.ghc-8.8.yaml +++ b/stack.ghc-8.8.yaml @@ -30,6 +30,7 @@ packages: - deps/macaw/x86 - deps/macaw/x86_symbolic - . + - saw-remote-api extra-deps: - zenc-0.1.1@sha256:e4be3e5e9fe1a1ade05910909c6e5b5a8eff72e697868b03955c9781b0443947 - IfElse-0.85 @@ -50,5 +51,5 @@ extra-deps: - bitwise-1.0.0.1 - constraints-0.11.2 - libBF-0.5.1 -resolver: lts-16.1 +resolver: lts-16.2 allow-newer: false