crucible-mir: Explicitly check mir-json schema version

crucible-mir/CHANGELOG.md

@@ -1,5 +1,9 @@
 # next -- TBA
 
+This release supports [version
+1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
+`mir-json`'s schema.
+
 * The calling sequence of ```translateMIR``` has changed: the first argument,
   which should always have been passed as ```mempty```, has been removed.
   This will require adjustments in any downstream callers.

crucible-mir/src/Mir/GenericOps.hs

@@ -29,6 +29,7 @@ import qualified Data.Map.Strict as Map
 import Data.Text (Text)
 import Data.Vector(Vector)
 import qualified Data.Vector as V
+import Data.Word (Word64)
 
 import Control.Lens((^.))
 
@@ -43,11 +44,11 @@ import GHC.Stack
 -- Generic operations over MIR AST
 --
 
--- 
+--
 -- These syntax-directed operations are defined via GHC.Generics so
 -- that they can automatically adapt to changes in the Mir AST.
 --
--- 
+--
 class GenericOps a where
 
   -- | Replace `TyInterned` with real types by applying a function.  The types
@@ -78,9 +79,9 @@ adtIndices (Adt _aname _kind vars _ _ _ _) col = go 0 vars
         Just fn -> case fn^.fbody.mblocks of
             ( BasicBlock _info (BasicBlockData [Assign _lhs (Use (OpConstant (Constant _ty (ConstInt i)))) _loc] _term) ):_ ->
                 fromIntegerLit i
-            
+
             _ -> error ("enum discriminant constant should only have one basic block [variant id:" ++ show _aname ++ " discr index:" ++ show name ++ "]")
-          
+
         Nothing -> error $ "cannot find discriminant constant " ++ show did ++
             " for variant " ++ show name
     getDiscr lastExplicit (Variant _vname (Relative i) _fields _kind _ _) =
@@ -160,12 +161,12 @@ instance GenericOps NamedTy
 instance GenericOps NonDivergingIntrinsic
 
 -- instances for newtypes
--- we need the deriving strategy 'anyclass' to disambiguate 
+-- we need the deriving strategy 'anyclass' to disambiguate
 -- from generalized newtype deriving
 -- either version would work, but GHC doesn't know that and gives a warning
 instance GenericOps Substs
 
--- *** Instances for Prelude types                 
+-- *** Instances for Prelude types
 
 instance GenericOps Int     where
    uninternTys = const id
@@ -175,29 +176,31 @@ instance GenericOps Char    where
    uninternTys = const id
 instance GenericOps Bool    where
    uninternTys = const id
-
+instance GenericOps Word64  where
+   uninternTys = const id
+
 instance GenericOps Text    where
    uninternTys = const id
-   
+
 instance GenericOps B.ByteString where
    uninternTys = const id
-   
+
 instance GenericOps b => GenericOps (Map.Map a b) where
    uninternTys f     = Map.map (uninternTys f)
-   
+
 instance GenericOps a => GenericOps [a]
 instance GenericOps a => GenericOps (Maybe a)
 instance (GenericOps a, GenericOps b) => GenericOps (a,b)
 instance GenericOps a => GenericOps (Vector a) where
    uninternTys f     = V.map (uninternTys f)
-  
-   
+
+
 --------------------------------------------------------------------------------------
 -- ** Generic programming plumbing
 
 class GenericOps' f where
   uninternTys'   :: (Text -> Ty) -> f p -> f p
-  
+
 instance GenericOps' V1 where
   uninternTys' _  = error "impossible: this is a void type"
 
@@ -213,6 +216,6 @@ instance (GenericOps c) => GenericOps' (K1 i c) where
 
 instance (GenericOps' f) => GenericOps' (M1 i t f) where
   uninternTys' s (M1 x) = M1 (uninternTys' s x)
-  
+
 instance (GenericOps' U1) where
   uninternTys' _s U1 = U1

crucible-mir/src/Mir/JSON.hs

@@ -22,6 +22,7 @@ import Data.Text (Text,  unpack)
 import qualified Data.Text as T
 import qualified Data.Text.Read  as T
 import qualified Data.Vector as V
+import Data.Word (Word64)
 import Control.Lens((^.))
 
 #if MIN_VERSION_aeson(2,0,0)
@@ -198,6 +199,7 @@ instance FromJSON Var where
 
 instance FromJSON Collection where
     parseJSON = withObject "Collection" $ \v -> do
+      (version :: Word64)     <- v .: "version"
       (fns    :: [Fn])        <- v .: "fns"
       (adts   :: [Adt])       <- v .: "adts"
       (traits :: [Trait])     <- v .: "traits"
@@ -207,6 +209,7 @@ instance FromJSON Collection where
       (tys    :: [NamedTy])   <- v .: "tys"
       (roots :: [MethName])   <- v .: "roots"
       return $ Collection
+        version
         (foldr (\ x m -> Map.insert (x^.fname) x m)     Map.empty fns)
         (foldr (\ x m -> Map.insert (x^.adtname) x m)   Map.empty adts)
         (foldr (\ x m -> Map.insertWith (++) (x^.adtOrigDefId) [x] m) Map.empty adts)

crucible-mir/src/Mir/Mir.hs

@@ -34,6 +34,7 @@ module Mir.Mir where
 import qualified Data.ByteString as B
 import Data.Map.Strict (Map)
 import Data.Text (Text)
+import Data.Word (Word64)
 
 import Control.Lens (makeLenses, makePrisms, makeWrapped)
 
@@ -235,6 +236,7 @@ instance Ord Var where
     compare (Var n _ _ _) (Var m _ _ _) = compare n m
 
 data Collection = Collection {
+    _version   :: !Word64,
     _functions :: !(Map MethName Fn),
     _adts      :: !(Map AdtName Adt),
     -- ADTs, indexed by original (pre-monomorphization) DefId

crucible-mir/src/Mir/ParseTranslate.hs

@@ -15,7 +15,7 @@
 module Mir.ParseTranslate (parseMIR, translateMIR) where
 
 import Control.Lens hiding((<.>))
-import Control.Monad (when)
+import Control.Monad (unless, when)
 
 import qualified Data.Aeson as J
 import qualified Data.ByteString.Lazy as B
@@ -28,7 +28,7 @@ import Prettyprinter (Pretty(..))
 import qualified Lang.Crucible.FunctionHandle as C
 
 
-import Mir.Mir (Collection(..), namedTys)
+import Mir.Mir (Collection(..), namedTys, version)
 import Mir.JSON ()
 import Mir.GenericOps (uninternTys)
 import Mir.Pass(rewriteCollection)
@@ -48,6 +48,16 @@ parseMIR path f = do
   case c of
       Left msg -> fail $ "JSON Decoding of " ++ path ++ " failed: " ++ msg
       Right col -> do
+        -- If you update the supported mir-json schema version below, make sure
+        -- to also update the crux-mir README accordingly.
+        unless (col^.version == 1) $
+          fail $ unlines
+            [ path ++ " uses an unsupported mir-json schema version: "
+                   ++ show (col^. version)
+            , "This crux-mir release only supports schema version 1."
+            , "(See https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md"
+            , "for more details on what the schema version means.)"
+            ]
         when (?debug > 5) $ do
           traceM "--------------------------------------------------------------"
           traceM $ "Loaded module: " ++ path

crucible-mir/src/Mir/Trans.hs

@@ -2225,7 +2225,8 @@ mkDiscrMap col = mconcat
 -- the comments below), which ranges over 'M.DefId's.
 mkCrateHashesMap :: M.Collection -> Map Text (NonEmpty Text)
 mkCrateHashesMap
-    (Collection functionsM adtsM adtsOrigM traitsM
+    (Collection _version
+                functionsM adtsM adtsOrigM traitsM
                 staticsM vtablesM intrinsicsM
                 -- namedTys ranges over type names, which aren't full DefIds.
                 _namedTysM

crux-mir/CHANGELOG.md

@@ -1,5 +1,15 @@
 # next -- TBA
 
+This release supports [version
+1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
+`mir-json`'s schema.
+
+* Add a `_version` field to `Collection`, which represents the `mir-json` schema
+  version of the MIR JSON file.
+* Explicitly check that the `mir-json` schema version is supported when parsing
+  a MIR JSON file. If the version is not supported, it will be rejected. This
+  helps ensure that unsupported `mir-json` files do not cause unintended
+  results.
 * Add `--debug` option for starting the Crucible debugger.
 
 # 0.9 -- 2024-08-30

crux-mir/README.md

@@ -19,6 +19,22 @@ Next, navigate to the `crucible/dependencies/mir-json` directory and install
 `mir-json` according to the instructions in [the `mir-json`
 README][mir-json-readme].
 
+Currently, `crux-mir` supports [version
+1](https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md#1) of
+`mir-json`'s schema. Note that the schema versions produced by `mir-json` can
+change over time as dictated by internal requirements and upstream changes. To
+help smooth this over, we intend that once:
+
+* `crux-mir` introduces support for any given schema version, it will retain
+  that support across at least two releases.
+* An exception to this rule is when `mir-json` updates to support a new Rust
+  toolchain version. In general, we cannot promise backwards compatibility
+  across Rust toolchains, as the changes are often significant enough to impeded
+  any ability to reasonably provide backwards-compatibility guarantees.
+
+As a general policy, `crux-mir` strives to support the `mir-json` schema
+versions corresponding to the last two `crux-mir` releases.
+
 [mir-json-readme]: https://github.com/GaloisInc/mir-json#readme
 
 

crux-mir/src/Mir/Language.hs

@@ -114,7 +114,7 @@ import           Mir.Trans (transStatics)
 import qualified Mir.TransCustom as TransCustom
 import           Mir.TransTy
 import           Mir.Concurrency
-import           Paths_crux_mir (version)
+import qualified Paths_crux_mir (version)
 
 defaultOutputConfig :: IO (Maybe Crux.OutputOptions -> OutputConfig MirLogging)
 defaultOutputConfig = Crux.defaultOutputConfig mirLoggingToSayWhat
@@ -159,7 +159,7 @@ mainWithOutputConfig :: (Maybe Crux.OutputOptions -> OutputConfig MirLogging)
                      -> BindExtraOverridesFn -> IO ExitCode
 mainWithOutputConfig mkOutCfg bindExtra =
     withMirLogging $
-    Crux.loadOptions mkOutCfg "crux-mir" version mirConfig
+    Crux.loadOptions mkOutCfg "crux-mir" Paths_crux_mir.version mirConfig
         $ runTestsWithExtraOverrides bindExtra
 
 type BindExtraOverridesFn = forall sym bak p t st fs args ret blocks rtp a r.