Split out crucible-mir from crux-mir

For the most part, most code was moved wholesale from `crux-mir` with only
minor changes (I removed redundant imports to more easily determine which
library dependencies could be dropped in `crucible-mir`). The most unusual
change was creating a new `Mir.ParseTranslate` module in `crucible-mir`, which
contains the `parseMIR` and `translateMIR` functions previously defined in
`Mir.Generate` (now a `crux-mir` module that only exports `generateMIR`).

Fixes #1065.

Author: RyanGlScott

cabal.project

@@ -9,6 +9,7 @@ packages:
   crucible-go/
   crucible-jvm/
   crucible-llvm/
+  crucible-mir/
   crucible-wasm/
   crucible-syntax/
   crucible-concurrency/

crucible-mir/CHANGELOG.md

@@ -0,0 +1,3 @@
+# 0.1
+
+* TODO: Describe API changes here

crucible-mir/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.

crucible-mir/README.md

@@ -0,0 +1,6 @@
+# crucible-mir
+
+This package implements a MIR frontend for Crucible. This exports all of the
+code that is useful across multiple projects that make use of MIR, such as
+[`crux-mir`](https://github.com/GaloisInc/crucible/blob/master/crux-mir) and
+[`crux-mir-comp`](https://github.com/GaloisInc/saw-script/blob/master/crux-mir-comp).

crucible-mir/crucible-mir.cabal

@@ -0,0 +1,56 @@
+name:                crucible-mir
+version:             0.1
+-- synopsis:
+-- description:
+homepage:            https://github.com/GaloisInc/crucible/blob/master/crucible-mir/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:       2.0
+extra-source-files:  README.md
+
+library
+  default-language: Haskell2010
+  build-depends: base >= 4.11 && < 5,
+                 aeson < 2.1,
+                 bv-sized,
+                 bytestring,
+                 prettyprinter >= 1.7.0,
+                 text,
+                 unordered-containers,
+                 crucible,
+                 parameterized-utils >= 1.0.8,
+                 containers,
+                 lens,
+                 vector,
+                 mtl,
+                 regex-compat,
+                 regex-base,
+                 transformers,
+                 what4,
+                 scientific       >= 0.3,
+                 template-haskell
+
+  hs-source-dirs: src
+  exposed-modules: Mir.JSON
+                   Mir.Generator
+                   Mir.Mir
+                   Mir.GenericOps
+                   Mir.ParseTranslate
+                   Mir.Pass
+                   Mir.Pass.AllocateEnum
+                   Mir.PP
+                   Mir.DefId
+                   Mir.FancyMuxTree
+                   Mir.Intrinsics
+                   Mir.TransTy
+                   Mir.Trans
+                   Mir.TransCustom

crux-mir/src/Mir/DefId.hs renamed to crucible-mir/src/Mir/DefId.hs

@@ -15,19 +15,17 @@ import qualified Data.Aeson.Types  as Aeson
 import qualified Data.Map.Strict   as Map
 import qualified Data.Scientific   as Scientific
 
-import Data.Word (Word64, Word8)
-import Data.Bits
+import Data.Word (Word8)
 import qualified Data.ByteString as BS
 import qualified Data.Char as Char
 import Data.Text (Text,  unpack)
 import qualified Data.Text as T
 import qualified Data.Text.Read  as T
-import Data.List
 import qualified Data.Vector as V
-import Control.Lens((^.),(&),(.~))
+import Control.Lens((^.))
 
 #if MIN_VERSION_aeson(2,0,0)
-import Data.Aeson.Key (Key)
+import qualified Data.Aeson.Key as K (Key)
 import qualified Data.Aeson.KeyMap as KM
 #else
 import qualified Data.HashMap.Lazy as HML
@@ -36,8 +34,6 @@ import qualified Data.HashMap.Lazy as HML
 import Mir.DefId
 import Mir.Mir
 
-import Debug.Trace
-
 --------------------------------------------------------------------------------------
 -- | FromJSON instances
 
@@ -550,7 +546,7 @@ instance FromJSON Static where
 
 -- TODO: When the ecosystem widely uses aeson-2.0.0.0 or later, remove this CPP.
 #if MIN_VERSION_aeson(2,0,0)
-lookupKM :: Key -> KM.KeyMap Value -> Maybe Value
+lookupKM :: K.Key -> KM.KeyMap Value -> Maybe Value
 lookupKM = KM.lookup
 #else
 lookupKM :: Text -> HML.HashMap Text Value -> Maybe Value

crux-mir/src/Mir/FancyMuxTree.hs renamed to crucible-mir/src/Mir/FancyMuxTree.hs

@@ -143,7 +143,7 @@ instance Pretty MirBody where
     pretty (MirBody mvs mbs _) =
       vcat (map pretty_temp mvs ++
             map pretty      mbs)
-    
+
 instance Pretty BasicBlock where
     pretty (BasicBlock info dat) =
       vcat [
@@ -296,7 +296,7 @@ instance Pretty FloatLit where
 
 instance Pretty Substs where
   pretty (Substs b) = langle <> hcat (punctuate comma (map pretty b)) <> rangle
-  
+
 instance Pretty ConstVal where
     pretty (ConstFloat i)   = pretty i
     pretty (ConstInt i)     = pretty i

crux-mir/src/Mir/Generator.hs renamed to crucible-mir/src/Mir/Generator.hs

@@ -0,0 +1,76 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+-----------------------------------------------------------------------
+-- |
+-- Module           : Mir.ParseTranslate
+-- Description      : Produce MIR AST and translate to Crucible
+-- Copyright        : (c) Galois, Inc 2018
+-- License          : BSD3
+-- Stability        : provisional
+--
+-- Entry points for parsing and translating the MIR AST into Crucible.
+-----------------------------------------------------------------------
+
+
+module Mir.ParseTranslate (parseMIR, translateMIR) where
+
+import Control.Lens hiding((<.>))
+import Control.Monad (when)
+
+import qualified Data.Aeson as J
+import qualified Data.ByteString.Lazy as B
+import qualified Data.Map as M
+
+import GHC.Stack
+
+import Prettyprinter (Pretty(..))
+
+import qualified Lang.Crucible.FunctionHandle as C
+
+
+import Mir.Mir (Collection(..), namedTys)
+import Mir.JSON ()
+import Mir.GenericOps (uninternTys)
+import Mir.Pass(rewriteCollection)
+import Mir.Generator(RustModule(..),CollectionState(..), collection)
+import Mir.Trans(transCollection)
+import qualified Mir.TransCustom as Mir (customOps)
+
+import Debug.Trace
+
+
+parseMIR :: (HasCallStack, ?debug::Int) =>
+            FilePath
+         -> B.ByteString
+         -> IO Collection
+parseMIR path f = do
+  let c = (J.eitherDecode f) :: Either String Collection
+  case c of
+      Left msg -> fail $ "JSON Decoding of " ++ path ++ " failed: " ++ msg
+      Right col -> do
+        when (?debug > 5) $ do
+          traceM "--------------------------------------------------------------"
+          traceM $ "Loaded module: " ++ path
+          traceM $ show (pretty col)
+          traceM "--------------------------------------------------------------"
+        return $ uninternMir col
+
+uninternMir :: Collection -> Collection
+uninternMir col = uninternTys unintern (col { _namedTys = mempty })
+  where
+    -- NB: knot-tying is happening here.  Some values in `tyMap` depend on
+    -- other values.  This should be okay: the original `rustc::ty::Ty`s are
+    -- acyclic, so the entries in `tyMap` should be too.
+    tyMap = fmap (uninternTys unintern) (col^.namedTys)
+    unintern name = case M.lookup name tyMap of
+        Nothing -> error $ "missing " ++ show name ++ " in type map"
+        Just ty -> ty
+
+
+-- | Translate a MIR collection to Crucible
+translateMIR :: (HasCallStack, ?debug::Int, ?assertFalseOnError::Bool, ?printCrucible::Bool)
+   => CollectionState -> Collection -> C.HandleAllocator -> IO RustModule
+translateMIR lib col halloc =
+  let ?customOps = Mir.customOps in
+  let col0 = let ?mirLib  = lib^.collection in rewriteCollection col
+  in let ?libCS = lib in transCollection col0 halloc

crux-mir/src/Mir/GenericOps.hs renamed to crucible-mir/src/Mir/GenericOps.hs

@@ -10,25 +10,18 @@ module Mir.Pass (
 ) where
 
 
-import Control.Monad.State.Lazy
-import Data.List
 import Control.Lens hiding (op,(|>))
-import qualified Data.Text as T
-import Data.Map(Map)
 import qualified Data.Map.Strict as Map
-import qualified Data.Maybe as Maybe
 
 import GHC.Stack
 
 import Mir.Mir
 import Mir.DefId
 import Mir.PP(fmt)
-import Mir.GenericOps
 
 import Mir.Pass.AllocateEnum ( passAllocateEnum )
 
 import Debug.Trace
-import GHC.Stack
 
 type Pass = (?debug::Int, ?mirLib::Collection, HasCallStack) => Collection -> Collection
 
@@ -41,7 +34,7 @@ x |> f = f x
 rewriteCollection :: Pass
 rewriteCollection col =
   col
-    |> passAllocateEnum 
+    |> passAllocateEnum
 
 --------------------------------------------------------------------------------------
 
@@ -52,7 +45,7 @@ passId = id
 
 passTrace :: String -> Pass
 passTrace str col =
-  if (?debug > 5) then 
+  if (?debug > 5) then
       ((trace $ "*********MIR collection " ++ str ++ "*******\n"
                 ++ fmt col ++ "\n****************************")
        col)
@@ -65,6 +58,6 @@ toCollectionPass f col = col { _functions = (fromList (f (Map.elems (col^.functi
     fromList :: [Fn] -> Map.Map DefId Fn
     fromList = foldr (\fn m -> Map.insert (fn^.fname) fn m) Map.empty
 
---------------------------------------------------------------------------------------  
+--------------------------------------------------------------------------------------
 
 

crux-mir/src/Mir/Intrinsics.hs renamed to crucible-mir/src/Mir/Intrinsics.hs

@@ -15,21 +15,16 @@
 module Mir.Pass.AllocateEnum
 ( passAllocateEnum
 ) where
- 
+
 import Control.Lens hiding (op)
-import Control.Monad.State.Lazy
 import qualified Data.Text as T
-import qualified Data.Map.Strict as Map
 import Data.List
 
 import Mir.DefId
 import Mir.Mir
-import Mir.GenericOps
 
 import GHC.Stack
 
-import Debug.Trace
-
 {-
 
 Look for sequences of statements of the form
@@ -63,7 +58,7 @@ data FieldUpdate = FieldUpdate { adtLvalue :: Lvalue,
 
 lookupAdt :: (?col :: Collection) => DefId -> Maybe Adt
 lookupAdt defid = find (\adt -> _adtname adt == defid) (?col^.adts)
-  
+
 
 isAdtFieldUpdate :: Statement -> Maybe FieldUpdate
 isAdtFieldUpdate (Assign (LProj (LProj lv (Downcast j)) (PField i ty)) (Use rhs) pos) =
@@ -91,7 +86,7 @@ makeAggregate updates (lv, k, adt) =
   pos = case updates of
           u:_ -> upos u
           []  -> "internal"
-    
+
 
 findAllocEnum :: (?col :: Collection) => [Statement] -> Maybe ( Statement, [Statement] )
 findAllocEnum ss = f ss [] where