Split out crucible-mir-comp from crux-mir-comp

For the most part, most code was moved wholesale from `crux-mir-comp` with only minor changes. This fixes #1839. This also adds basic `README` and `LICENSE` files for `crucible-mir-comp` and `crux-mir-comp`, thereby fixing #1616.
GaloisInc · Mar 14, 2023 · b2c4bb1 · b2c4bb1
1 parent 9bc0a22
commit b2c4bb1
Show file tree

Hide file tree

Showing 12 changed files with 119 additions and 18 deletions.
diff --git 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

diff --git a/crucible-mir-comp/LICENSE 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
@@ -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
@@ -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:          [email protected]
+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/...mir-comp/src/Mir/Compositional/Builder.hs → ...mir-comp/src/Mir/Compositional/Builder.hs b/...mir-comp/src/Mir/Compositional/Builder.hs → ...mir-comp/src/Mir/Compositional/Builder.hs
diff --git a/...mir-comp/src/Mir/Compositional/Clobber.hs → ...mir-comp/src/Mir/Compositional/Clobber.hs b/...mir-comp/src/Mir/Compositional/Clobber.hs → ...mir-comp/src/Mir/Compositional/Clobber.hs
diff --git a/...mir-comp/src/Mir/Compositional/Convert.hs → ...mir-comp/src/Mir/Compositional/Convert.hs b/...mir-comp/src/Mir/Compositional/Convert.hs → ...mir-comp/src/Mir/Compositional/Convert.hs
diff --git a/...-comp/src/Mir/Compositional/MethodSpec.hs → ...-comp/src/Mir/Compositional/MethodSpec.hs b/...-comp/src/Mir/Compositional/MethodSpec.hs → ...-comp/src/Mir/Compositional/MethodSpec.hs
diff --git a/...ir-comp/src/Mir/Compositional/Override.hs → ...ir-comp/src/Mir/Compositional/Override.hs b/...ir-comp/src/Mir/Compositional/Override.hs → ...ir-comp/src/Mir/Compositional/Override.hs
diff --git a/crux-mir-comp/LICENSE 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
@@ -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
@@ -11,7 +11,7 @@ author:              Joshua Gancher,
                      Stephanie Weirich,
                      Stuart Pernsteiner
 maintainer:          [email protected]
-copyright:           2017-2020 Galois, Inc.
+copyright:           2017-2023 Galois, Inc.
 category:            Web
 build-type:          Simple
 cabal-version:       >=1.10
@@ -21,38 +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