Merge saw-core repo

.github/workflows/saw-core-coq-check-coq-files.yml

@@ -0,0 +1,61 @@
+name: Type-check handwritten and generated Coq files
+on:
+  push:
+    branches: [master]
+  pull_request:
+    branches: [master]
+  workflow_dispatch:
+    branches: [master]
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        # coq-bits does not support coq >= 8.13 yet
+        coq: [8.12.2, 8.11.2, 8.10.2]
+        os: [ubuntu-latest]
+    runs-on: ${{ matrix.os }}
+    name: saw-core-coq - ${{ matrix.os }} - coq-${{ matrix.coq }}
+    env:
+      COQ_VERSION: ${{ matrix.coq }}
+      # coq-bits claims to support < 4.10 only
+      OCAML_VERSION: 4.09.1
+      COQBITS_VERSION: 1.0.0
+    steps:
+
+      - uses: actions/checkout@v2
+
+      - name: Cache ~/.opam
+        uses: actions/cache@v2
+        with:
+          path: ~/.opam
+          key: opam-${{ runner.os }}-${{ env.OCAML_VERSION }}-${{ env.COQ_VERSION }}-${{ env.COQBITS_VERSION }}
+
+      # NOTE: this action is marked as experimental by their author, but it is
+      # much faster than avsm@setup-ocaml@v1.  However, if this one ever becomes
+      # problematic, it should suffice to switch back to that version.
+      - name: Set up ocaml and opam
+        uses: actions-ml/setup-ocaml@df8c831c6c1e49804621d6e09c4ab9235da31fb5
+        with:
+          ocaml-version: ${{ env.OCAML_VERSION }}
+
+      - name: Install coq
+        shell: bash
+        run: |
+          opam pin add coq ${{ env.COQ_VERSION }}
+          opam install --unlock-base -y coq
+
+      - name: Install coq-bits
+        shell: bash
+        run: |
+          opam repo add coq-released https://coq.inria.fr/opam/released
+          opam install --unlock-base -y "coq-bits=$COQBITS_VERSION"
+
+      - name: Build saw-core-coq/coq
+        shell: bash
+        working-directory: saw-core-coq/coq
+        run: |
+          eval $(opam env)
+          coq_makefile -f _CoqProject -o Makefile.coq
+          make -j2

.gitmodules

@@ -22,9 +22,6 @@
 [submodule "deps/parameterized-utils"]
 	path = deps/parameterized-utils
 	url = https://github.com/GaloisInc/parameterized-utils.git
-[submodule "deps/saw-core"]
-	path = deps/saw-core
-	url = https://github.com/GaloisInc/saw-core.git
 [submodule "deps/flexdis86"]
 	path = deps/flexdis86
 	url = https://github.com/GaloisInc/flexdis86.git

README.md

@@ -89,7 +89,6 @@ downloaded dependencies include:
 * `deps/abcBridge/`:        [Haskell bindings for ABC](https://github.com/GaloisInc/abcBridge)
 * `deps/crucible/`:         [Crucible symbolic execution engine](https://github.com/GaloisInc/crucible)
 * `deps/cryptol/`:          [Cryptol](https://github.com/GaloisInc/cryptol)
-* `deps/saw-core/`:         [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, and SAWScript
 
 ## For SAW developers
 

cabal.project

@@ -2,19 +2,19 @@ packages:
     saw-script.cabal
     saw-remote-api
     crux-mir-comp
+    cryptol-saw-core
+    rme
+    saw-core
+    saw-core-aig
+    saw-core-sbv
+    saw-core-what4
+    saw-core-coq
     deps/llvm-pretty
     deps/llvm-pretty-bc-parser
     deps/jvm-parser
     deps/aig
     deps/abcBridge
     deps/cryptol
-    deps/saw-core/cryptol-saw-core
-    deps/saw-core/rme
-    deps/saw-core/saw-core
-    deps/saw-core/saw-core-aig
-    deps/saw-core/saw-core-sbv
-    deps/saw-core/saw-core-what4
-    deps/saw-core/saw-core-coq
     deps/what4/what4
     deps/crucible/crucible
     deps/crucible/crucible-jvm

cryptol-saw-core/LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2014, 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:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the names of the authors nor the names of other
+      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
+OWNER 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.

cryptol-saw-core/README.md

@@ -0,0 +1,5 @@
+This repository contains the code for the Cryptol Symbolic Simulator
+(CSS). It is currently used primarily as a library from SAWScript, but
+also produces a stand-alone executable, `css`. This executable has
+only limited functionality: it can translate a single Cryptol function
+to an And-Inverter Graph (AIG).

cryptol-saw-core/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

cryptol-saw-core/cryptol-saw-core.cabal

@@ -0,0 +1,94 @@
+Name:              cryptol-saw-core
+Version:           0.1
+Author:            Galois, Inc.
+License:           BSD3
+License-file:      LICENSE
+Maintainer:        [email protected]
+Copyright:         (c) 2014 Galois Inc.
+Build-type:        Simple
+cabal-version:     >= 1.10
+Category:          Formal Methods
+Synopsis:          Representing Cryptol in SAWCore
+Description:
+  Translate Cryptol syntax into SAWCore terms, which can then
+  be analysed by various backend proof systems.
+
+extra-source-files:
+    saw/Cryptol.sawcore
+
+flag build-css
+  description: Build the css executable
+  default: True
+
+library
+  build-depends:
+    aig,
+    array,
+    base,
+    base-compat,
+    bytestring,
+    containers,
+    cryptol >= 2.3.0,
+    data-inttrie >= 0.1.4,
+    integer-gmp,
+    modern-uri,
+    panic,
+    saw-core,
+    saw-core-aig,
+    saw-core-sbv,
+    saw-core-what4,
+    what4,
+    sbv,
+    vector,
+    text,
+    executable-path,
+    filepath
+  hs-source-dirs: src
+  exposed-modules:
+     Verifier.SAW.Cryptol
+     Verifier.SAW.Cryptol.Panic
+     Verifier.SAW.Cryptol.Prelude
+     Verifier.SAW.Cryptol.Simpset
+     Verifier.SAW.CryptolEnv
+     Verifier.SAW.TypedTerm
+  GHC-options: -Wall -Werror
+
+executable css
+  if !flag(build-css)
+     buildable: False
+
+  other-modules:
+    Paths_cryptol_saw_core
+
+  build-depends:
+    array,
+    abcBridge,
+    base,
+    bytestring,
+    containers,
+    cryptol,
+    saw-core,
+    saw-core-aig,
+    text,
+    cryptol-saw-core
+
+  hs-source-dirs : css
+  main-is : Main.hs
+  GHC-options: -Wall -O2 -rtsopts -pgmlc++
+  extra-libraries:      stdc++
+
+test-suite cryptol-saw-core-tc-test
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+
+  hs-source-dirs: test
+  main-is: CryptolVerifierTC.hs
+
+  build-depends:
+    base,
+    bytestring,
+    containers,
+    cryptol,
+    cryptol-saw-core,
+    heredoc >= 0.2,
+    saw-core

cryptol-saw-core/css/Main.hs

@@ -0,0 +1,145 @@
+{-# LANGUAGE RankNTypes #-}
+
+module Main where
+
+import           System.Environment( getArgs )
+import           System.Exit( exitFailure )
+import           System.Console.GetOpt
+import           System.IO
+import qualified Data.ByteString as BS
+import           Data.Text ( pack )
+import           Data.Version
+
+import qualified Cryptol.Eval as E
+import qualified Cryptol.TypeCheck.AST as T
+import qualified Cryptol.ModuleSystem as CM
+import qualified Cryptol.ModuleSystem.Env as CME
+import qualified Cryptol.Parser as P
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
+import           Cryptol.Utils.PP
+import           Cryptol.Utils.Logger (quietLogger)
+
+import qualified Verifier.SAW.Cryptol as C
+import           Verifier.SAW.SharedTerm
+import qualified Verifier.SAW.Cryptol.Prelude as C
+import           Verifier.SAW.CryptolEnv (schemaNoUser)
+
+
+import qualified Data.ABC as ABC
+import qualified Verifier.SAW.Simulator.BitBlast as BBSim
+
+import qualified Paths_cryptol_saw_core as Paths
+
+data CSS = CSS
+  { output :: FilePath
+  , cssMode :: CmdMode
+  } deriving (Show)
+
+data CmdMode
+  = NormalMode
+  | HelpMode
+  | VersionMode
+ deriving (Show, Eq)
+
+emptyCSS :: CSS
+emptyCSS =
+  CSS
+  { output = ""
+  , cssMode = NormalMode
+  }
+
+options :: [OptDescr (CSS -> CSS)]
+options =
+  [ Option ['o'] ["output"]
+     (ReqArg (\x css -> css{ output = x }) "FILE")
+     "output file"
+  , Option ['h'] ["help"]
+     (NoArg (\css -> css{ cssMode = HelpMode }))
+     "display help"
+  , Option ['v'] ["version"]
+     (NoArg (\css -> css{ cssMode = VersionMode }))
+     "version"
+  ]
+
+version_string :: String
+version_string = unlines
+  [ "Cryptol Symbolic Simulator (css) version "++showVersion Paths.version
+  , "Copyright 2014 Galois, Inc.  All rights reserved."
+  ]
+
+header :: String
+header = "css [options] <input module> <function to simulate>"
+
+main :: IO ()
+main = do
+  args <- getArgs
+  case getOpt RequireOrder options args of
+    (flags,optArgs,[]) -> cssMain (foldr ($) emptyCSS flags) optArgs
+
+    (_,_,errs) -> do
+       hPutStr stderr (concat errs ++ usageInfo header options)
+       exitFailure
+
+defaultEvalOpts :: E.EvalOpts
+defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts
+
+cssMain :: CSS -> [String] -> IO ()
+cssMain css [inputModule,name] | cssMode css == NormalMode = do
+    let out = if null (output css)
+                 then name++".aig"
+                 else (output css)
+
+    modEnv <- CM.initialModuleEnv
+    let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
+    (e,warn) <-
+      SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+      CM.loadModuleByPath inputModule (minp s)
+    mapM_ (print . pp) warn
+    case e of
+       Left msg -> print msg >> exitFailure
+       Right (_,menv) -> processModule menv out name
+
+cssMain css _ | cssMode css == VersionMode = do
+    hPutStr stdout version_string
+
+cssMain css _ | cssMode css == HelpMode = do
+    hPutStr stdout (usageInfo header options)
+
+cssMain _ _ = do
+    hPutStr stdout (usageInfo header options)
+    exitFailure
+
+
+processModule :: CM.ModuleEnv -> FilePath -> String -> IO ()
+processModule menv fout funcName = do
+   sc <- mkSharedContext
+   C.scLoadPreludeModule sc
+   C.scLoadCryptolModule sc
+   tm <- extractCryptol sc menv funcName
+   writeAIG sc fout tm
+
+writeAIG :: SharedContext -> FilePath -> Term -> IO ()
+writeAIG sc f t = do
+  BBSim.withBitBlastedTerm ABC.giaNetwork sc mempty t $ \be ls -> do
+  ABC.writeAiger f (ABC.Network be (ABC.bvToList ls))
+
+extractCryptol :: SharedContext -> CM.ModuleEnv -> String -> IO Term
+extractCryptol sc modEnv input = do
+  let declGroups = concatMap T.mDecls (CME.loadedModules modEnv)
+  env <- C.importDeclGroups sc C.emptyEnv declGroups
+  pexpr <-
+    case P.parseExpr (pack input) of
+      Left err -> fail (show (P.ppError err))
+      Right x -> return x
+  let minp = CM.ModuleInput True (pure defaultEvalOpts) BS.readFile modEnv
+  (exprResult, exprWarnings) <-
+    SMT.withSolver (CME.meSolverConfig modEnv) $ \s ->
+    CM.checkExpr pexpr (minp s)
+  mapM_ (print . pp) exprWarnings
+  ((_, expr, schema), _modEnv') <-
+    case exprResult of
+      Left err -> fail (show (pp err))
+      Right x -> return x
+  putStrLn $ "Extracting expression of type " ++ show (pp (schemaNoUser schema))
+  C.importExpr sc env expr
+