Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 15 additions & 10 deletions crucible-mir/src/Mir/ParseTranslate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ import Prettyprinter (Pretty(..))
import qualified Lang.Crucible.FunctionHandle as C


import Mir.Mir (Collection(..), namedTys, tiTy, tiNeedsDrop, tiLayout)
import Mir.Mir (Collection(..), namedTys, tiTy, tiNeedsDrop, tiLayout, version)
import Mir.JSON ()
import Mir.GenericOps (uninternTys)
import Mir.Pass(rewriteCollection)
Expand Down Expand Up @@ -62,13 +62,26 @@ parseMIR path f = do
case J.eitherDecode @Collection f of
Left msg -> fallback msg
Right col -> pure col
checkSchemaVersion (col ^. version)
when (?debug > 5) $ do
traceM "--------------------------------------------------------------"
traceM $ "Loaded module: " ++ path
traceM $ show (pretty col)
traceM "--------------------------------------------------------------"
return $ uninternMir col
where
checkSchemaVersion :: Word64 -> IO ()
checkSchemaVersion actualSchemaVersion =
unless (actualSchemaVersion == supportedSchemaVersion) $
fail $ unlines
[ path ++ " uses an unsupported mir-json schema version: "
++ show actualSchemaVersion
, "This release only supports schema version "
++ show supportedSchemaVersion ++ "."
, "(See https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md"
, "for more details on what the schema version means.)"
]

-- If parsing fails, try to interpret the file as a raw JSON J.Value and
-- see if the schema version number (if one exists) matches. If they are
-- mismatched, then report this, as this is a pretty significant clue that
Expand Down Expand Up @@ -109,15 +122,7 @@ parseMIR path f = do
J.Success actualSchemaVersion -> pure actualSchemaVersion
-- As a sanity-check, ensure that the number which "version" maps to is a
-- supported JSON schema version. If not, error out early.
unless (actualSchemaVersion == supportedSchemaVersion) $
fail $ unlines
[ path ++ " uses an unsupported mir-json schema version: "
++ show actualSchemaVersion
, "This release only supports schema version "
++ show supportedSchemaVersion ++ "."
, "(See https://github.com/GaloisInc/mir-json/blob/master/SCHEMA_CHANGELOG.md"
, "for more details on what the schema version means.)"
]
checkSchemaVersion actualSchemaVersion
-- If we have reached this point, then we know that the JSON file failed
-- to parse as a Collection despite the schema versions matching, so
-- something has gone awry. Report a generic JSON parse error to the user
Expand Down
Loading