diff --git a/cabal.project b/cabal.project index 8a20405818..7ed7119a69 100644 --- a/cabal.project +++ b/cabal.project @@ -1,6 +1,7 @@ packages: saw-script.cabal saw-remote-api + crucible-mir-comp crux-mir-comp cryptol-saw-core rme @@ -23,6 +24,7 @@ packages: deps/crucible/crucible-concurrency deps/crucible/crucible-jvm deps/crucible/crucible-llvm + deps/crucible/crucible-mir deps/crucible/crucible-symio deps/crucible/crucible-syntax deps/crucible/crux diff --git a/crucible-mir-comp/LICENSE b/crucible-mir-comp/LICENSE new file mode 100644 index 0000000000..e8f247d2ce --- /dev/null +++ b/crucible-mir-comp/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017-2023 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 name 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. diff --git a/crucible-mir-comp/README.md b/crucible-mir-comp/README.md new file mode 100644 index 0000000000..299ab18dd0 --- /dev/null +++ b/crucible-mir-comp/README.md @@ -0,0 +1,4 @@ +# crucible-mir-comp + +This package implements support for compositional verification in +[`crucible-mir`](https://github.com/GaloisInc/crucible/blob/master/crucible-mir). diff --git a/crucible-mir-comp/crucible-mir-comp.cabal b/crucible-mir-comp/crucible-mir-comp.cabal new file mode 100644 index 0000000000..6e4220cce1 --- /dev/null +++ b/crucible-mir-comp/crucible-mir-comp.cabal @@ -0,0 +1,47 @@ +name: crucible-mir-comp +version: 0.1 +-- synopsis: +-- description: +homepage: https://github.com/GaloisInc/saw-script/blob/master/crucible-mir-comp/README.md +license: BSD3 +license-file: LICENSE +author: Joshua Gancher, + Rob Dockins, + Andrey Chudnov, + Stephanie Weirich, + Stuart Pernsteiner +maintainer: spernsteiner@galois.com +copyright: 2017-2023 Galois, Inc. +category: Web +build-type: Simple +cabal-version: >=1.10 +extra-source-files: README.md + +library + default-language: Haskell2010 + build-depends: base >= 4.9 && < 5, + text, + prettyprinter >= 1.7.0, + crucible, + parameterized-utils >= 1.0.8, + containers, + lens, + vector, + mtl, + what4, + bv-sized, + bytestring, + crucible-mir, + saw-core, + saw-core-what4, + cryptol-saw-core, + saw-script + + hs-source-dirs: src + exposed-modules: Mir.Compositional.Builder + Mir.Compositional.Clobber + Mir.Compositional.Convert + Mir.Compositional.MethodSpec + Mir.Compositional.Override + + ghc-options: -Wall -Wno-name-shadowing diff --git a/crux-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs similarity index 100% rename from crux-mir-comp/src/Mir/Compositional/Builder.hs rename to crucible-mir-comp/src/Mir/Compositional/Builder.hs diff --git a/crux-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs similarity index 100% rename from crux-mir-comp/src/Mir/Compositional/Clobber.hs rename to crucible-mir-comp/src/Mir/Compositional/Clobber.hs diff --git a/crux-mir-comp/src/Mir/Compositional/Convert.hs b/crucible-mir-comp/src/Mir/Compositional/Convert.hs similarity index 100% rename from crux-mir-comp/src/Mir/Compositional/Convert.hs rename to crucible-mir-comp/src/Mir/Compositional/Convert.hs diff --git a/crux-mir-comp/src/Mir/Compositional/MethodSpec.hs b/crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs similarity index 100% rename from crux-mir-comp/src/Mir/Compositional/MethodSpec.hs rename to crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs similarity index 100% rename from crux-mir-comp/src/Mir/Compositional/Override.hs rename to crucible-mir-comp/src/Mir/Compositional/Override.hs diff --git a/crux-mir-comp/LICENSE b/crux-mir-comp/LICENSE new file mode 100644 index 0000000000..e8f247d2ce --- /dev/null +++ b/crux-mir-comp/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017-2023 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 name 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. diff --git a/crux-mir-comp/README.md b/crux-mir-comp/README.md new file mode 100644 index 0000000000..80533c947b --- /dev/null +++ b/crux-mir-comp/README.md @@ -0,0 +1,4 @@ +# crux-mir-comp + +This package implements a Crux frontend for +[`crucible-mir-comp`](https://github.com/GaloisInc/saw-script/blob/master/crux-mir-comp). diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal index fbb95ec9f9..ce6056da60 100644 --- a/crux-mir-comp/crux-mir-comp.cabal +++ b/crux-mir-comp/crux-mir-comp.cabal @@ -11,7 +11,7 @@ author: Joshua Gancher, Stephanie Weirich, Stuart Pernsteiner maintainer: spernsteiner@galois.com -copyright: 2017-2020 Galois, Inc. +copyright: 2017-2023 Galois, Inc. category: Web build-type: Simple cabal-version: >=1.10 @@ -21,37 +21,23 @@ library default-language: Haskell2010 build-depends: base >= 4.9 && < 5, text, - prettyprinter >= 1.7.0, crucible, parameterized-utils >= 1.0.8, containers, lens, - vector, - mtl, - transformers, what4, - tasty >= 0.10, - tasty-hunit >= 0.10, - tasty-quickcheck >= 0.8, - tasty-golden >= 2.3, - bv-sized, bytestring, crux, + crucible-mir, + crucible-mir-comp, crux-mir, - template-haskell, saw-core, saw-core-what4, cryptol, - cryptol-saw-core, - saw-script + cryptol-saw-core hs-source-dirs: src exposed-modules: Mir.Compositional - Mir.Compositional.Builder - Mir.Compositional.Clobber - Mir.Compositional.Convert - Mir.Compositional.MethodSpec - Mir.Compositional.Override Mir.Cryptol ghc-options: -Wall -Wno-name-shadowing diff --git a/deps/crucible b/deps/crucible index 7501d6b62b..4b8e481f98 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 7501d6b62be53fec0a1da4d92749c300c19da23a +Subproject commit 4b8e481f986e2ba2125032edf05dda407dbb57b8 diff --git a/deps/language-sally b/deps/language-sally index de4f979032..a217a9f661 160000 --- a/deps/language-sally +++ b/deps/language-sally @@ -1 +1 @@ -Subproject commit de4f979032396b2c8fa1b5d05603c47dd96874e2 +Subproject commit a217a9f661caabd7858a17c2b556217fc39a946e diff --git a/deps/what4 b/deps/what4 index 4af08d1762..6f5e0fe9be 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 4af08d1762a60ff4d36adf6a98481fe5910a72d6 +Subproject commit 6f5e0fe9bef58234603ccf6914c32ea1ba2f9766