From b951ab2763347d4b2bfaf704109f255575675066 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 6 Aug 2020 15:19:54 -0700 Subject: [PATCH] Rename and move `cryptol-verifier` package into `saw-core` repo. Package `cryptol-verifier` is now called `cryptol-saw-core`, and it has moved into a subdirectory within the `saw-core` repository. Update cabal.project and stack.yaml files with new package locations. Remove redundant `cryptol-verifier` submodule. --- .gitmodules | 3 --- README.md | 1 - cabal.project | 2 +- cabal.project.ci | 2 +- cabal.project.freeze | 2 +- deps/cryptol-verifier | 1 - deps/jvm-verifier | 2 +- deps/saw-core | 2 +- deps/saw-core-coq | 2 +- saw-script.cabal | 4 ++-- src/SAWScript/Builtins.hs | 2 +- src/SAWScript/Crucible/JVM/Builtins.hs | 2 +- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 2 +- src/SAWScript/Crucible/LLVM/Builtins.hs | 2 +- src/SAWScript/Interpreter.hs | 2 +- stack.ghc-8.6.yaml | 2 +- stack.ghc-8.8.yaml | 2 +- 17 files changed, 15 insertions(+), 20 deletions(-) delete mode 160000 deps/cryptol-verifier diff --git a/.gitmodules b/.gitmodules index 6c056b6475..316bddb18f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,9 +7,6 @@ [submodule "deps/crucible"] path = deps/crucible url = https://github.com/GaloisInc/crucible.git -[submodule "deps/cryptol-verifier"] - path = deps/cryptol-verifier - url = https://github.com/GaloisInc/cryptol-verifier.git [submodule "deps/cryptol"] path = deps/cryptol url = https://github.com/GaloisInc/cryptol.git diff --git a/README.md b/README.md index 806f7791f8..38502af095 100644 --- a/README.md +++ b/README.md @@ -124,7 +124,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/cryptol-verifier/`: [Cryptol Symbolic Simulator (CSS)](https://github.com/GaloisInc/cryptol-verifier) * `deps/jvm-verifier/`: [Java Symbolic Simulator (JSS)](https://github.com/GaloisInc/jvm-verifier) * `deps/saw-core/`: [SAWCore intermediate language](https://github.com/GaloisInc/saw-core), used by CSS, JSS, and SAWScript diff --git a/cabal.project b/cabal.project index 13adedc9d6..83108c6a80 100644 --- a/cabal.project +++ b/cabal.project @@ -6,12 +6,12 @@ packages: deps/aig deps/abcBridge deps/cryptol + deps/saw-core/cryptol-saw-core 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-coq - deps/cryptol-verifier deps/jvm-verifier deps/what4/what4 deps/what4/what4-abc diff --git a/cabal.project.ci b/cabal.project.ci index 59f81efdf9..31785e5371 100644 --- a/cabal.project.ci +++ b/cabal.project.ci @@ -6,12 +6,12 @@ packages: deps/aig deps/abcBridge deps/cryptol + deps/saw-core/cryptol-saw-core 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-coq - deps/cryptol-verifier deps/jvm-verifier deps/what4/what4 deps/what4/what4-abc diff --git a/cabal.project.freeze b/cabal.project.freeze index d515097322..5182da1c7a 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -80,7 +80,7 @@ constraints: any.Cabal ==2.4.0.1, crucible +unsafe-operations, any.cryptohash-sha1 ==0.11.100.1, cryptol +relocatable -static, - cryptol-verifier +build-css, + cryptol-saw-core +build-css, any.data-accessor ==0.2.3, data-accessor +category -monadfail +splitbase, any.data-binary-ieee754 ==0.4.4, diff --git a/deps/cryptol-verifier b/deps/cryptol-verifier deleted file mode 160000 index 5fed6dcac7..0000000000 --- a/deps/cryptol-verifier +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 5fed6dcac7bad275ee1980ffb7b500c1d17d67ca diff --git a/deps/jvm-verifier b/deps/jvm-verifier index 4484e38526..7cc6504350 160000 --- a/deps/jvm-verifier +++ b/deps/jvm-verifier @@ -1 +1 @@ -Subproject commit 4484e38526c7a1937d85863ac42248aa459474e0 +Subproject commit 7cc650435015186d47711bf32e52e7a51209e19e diff --git a/deps/saw-core b/deps/saw-core index 702dbfcb89..3ec1be28ae 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 702dbfcb89ef97cc2f2f58be0de5995d0da468c1 +Subproject commit 3ec1be28aeec1497643873246757a76f548c5cfe diff --git a/deps/saw-core-coq b/deps/saw-core-coq index 704e6b1781..296b0c399b 160000 --- a/deps/saw-core-coq +++ b/deps/saw-core-coq @@ -1 +1 @@ -Subproject commit 704e6b1781c79c8d24eeef6657b1878602661f12 +Subproject commit 296b0c399b347d4f5c4d169f4d38659d1dd8d31d diff --git a/saw-script.cabal b/saw-script.cabal index f0b4398204..8de7218ebe 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -33,7 +33,7 @@ library , containers , constraints >= 0.6 , cryptol - , cryptol-verifier + , cryptol-saw-core , crucible >= 0.4 , crucible-jvm , crucible-llvm >= 0.2 @@ -213,4 +213,4 @@ executable saw , transformers , saw-script , saw-core - , cryptol-verifier + , cryptol-saw-core diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index a231fed248..8e659bc388 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -76,7 +76,7 @@ import Verifier.SAW.TypedAST import SAWScript.Position --- cryptol-verifier +-- cryptol-saw-core import qualified Verifier.SAW.CryptolEnv as CEnv -- saw-core-aig diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 8f0790644f..3d6124851b 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -65,7 +65,7 @@ import qualified Verifier.Java.Codebase as CB -- cryptol import qualified Cryptol.TypeCheck.Type as Cryptol --- cryptol-verifier +-- cryptol-saw-core import Verifier.SAW.Cryptol (importType, emptyEnv) -- what4 diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 66de17aa9e..c7ab9d5255 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -66,7 +66,7 @@ import qualified What4.Solver.Yices as Yices -- saw-core import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies, scAbstractExts) --- cryptol-verifier +-- cryptol-saw-core import Verifier.SAW.TypedTerm(TypedTerm(..)) -- saw-script diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index af1f4cf190..4e35e29673 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -157,7 +157,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST import Verifier.SAW.Recognizer --- cryptol-verifier +-- cryptol-saw-core import Verifier.SAW.TypedTerm -- saw-script diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 00ecbc1069..91125c4215 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1005,7 +1005,7 @@ primitives = Map.fromList , prim "write_coq_cryptol_primitives_for_sawcore" "String -> [(String, String)] -> [String] -> TopLevel ()" (pureVal writeCoqCryptolPrimitivesForSAWCore) Experimental - [ "Write out a representation of cryptol-verifier's Cryptol.sawcore in" + [ "Write out a representation of cryptol-saw-core's Cryptol.sawcore in" , "Gallina syntax for Coq." , "The first argument is the name of the file to output into," , "use an empty string to output to standard output." diff --git a/stack.ghc-8.6.yaml b/stack.ghc-8.6.yaml index 1b372f64e0..6d5a0f85c3 100644 --- a/stack.ghc-8.6.yaml +++ b/stack.ghc-8.6.yaml @@ -6,12 +6,12 @@ packages: - deps/aig/ - deps/abcBridge/ - deps/cryptol/ + - deps/saw-core/cryptol-saw-core/ - 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-coq/ - - deps/cryptol-verifier/ - deps/jvm-verifier/ - deps/what4/what4/ - deps/what4/what4-abc/ diff --git a/stack.ghc-8.8.yaml b/stack.ghc-8.8.yaml index b82d38fb8a..fc0737f1ca 100644 --- a/stack.ghc-8.8.yaml +++ b/stack.ghc-8.8.yaml @@ -6,12 +6,12 @@ packages: - deps/aig/ - deps/abcBridge/ - deps/cryptol/ + - deps/saw-core/cryptol-saw-core/ - 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-coq/ - - deps/cryptol-verifier/ - deps/jvm-verifier/ - deps/what4/what4/ - deps/what4/what4-abc/