Merge pull request #1096 from GaloisInc/crux-mir-nightly-2023-01-23-m…

…erge

`crux-mir`: Support `nightly-2023-01-23`

.github/Dockerfile-crux-mir

@@ -2,8 +2,6 @@ FROM rust:1.46.0 AS mir_json
 
 ADD dependencies/mir-json /mir-json
 WORKDIR /mir-json
-# Work around https://github.com/rust-lang/cargo/issues/10303
-ENV CARGO_NET_GIT_FETCH_WITH_CLI=true
 RUN rustup toolchain install nightly-2020-03-22 --force
 RUN rustup component add --toolchain nightly-2020-03-22 rustc-dev
 RUN rustup default nightly-2020-03-22

.github/workflows/crux-mir-build.yml

@@ -20,8 +20,6 @@ env:
   # (symptom: "No suitable image found ... unknown file type, first
   # eight bytes: 0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00")
   CACHE_VERSION: 4
-  # Work around https://github.com/rust-lang/cargo/issues/10303
-  CARGO_NET_GIT_FETCH_WITH_CLI: true
 
 jobs:
   config:
@@ -65,13 +63,10 @@ jobs:
         os: [ubuntu-22.04]
         cabal: ["3.8.1.0"]
         ghc: ["8.10.7", "9.2.7", "9.4.4"]
-        # include:
-          # Disable the macOS build for now due to
-          # https://github.com/GaloisInc/crucible/issues/1050
-          #
-          # - os: macos-12
-          #   cabal: 3.8.1.0
-          #   ghc: 9.2.4
+        include:
+          - os: macos-12
+            cabal: 3.8.1.0
+            ghc: 9.2.7
 
           # We want Windows soon, but it doesn't need to be now
     name: crux-mir - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
@@ -106,7 +101,7 @@ jobs:
       - name: Install latest Rust nightly
         uses: actions-rs/toolchain@v1
         with:
-          toolchain: nightly-2020-03-22
+          toolchain: nightly-2023-01-23
           override: true
           components: rustc-dev
 

crucible-mir/src/Mir/DefId.hs

@@ -1,4 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DeriveGeneric, DeriveAnyClass, DefaultSignatures #-}
 
 {-# OPTIONS_GHC -Wincomplete-patterns -Wall #-}
@@ -8,20 +10,23 @@
 
 module Mir.DefId
 ( DefId
+, didCrate
+, didCrateDisambig
+, didPath
 , textId
 , idText
 
 , ExplodedDefId
 , idKey
+, explodedDefIdPat
+, textIdKey
 
 , getTraitName
 , cleanVariantName
 , parseFieldName
-
-, normDefId
-, normDefIdPat
 ) where
 
+import Control.Lens (makeLenses)
 import Data.Aeson
 
 import qualified Language.Haskell.TH.Syntax as TH
@@ -47,30 +52,26 @@ type Segment = (Text, Int)
 data DefId = DefId
     {
     -- | The name of the enclosing crate.
-      did_crate :: Text
+      _didCrate :: Text
     -- | The disambiguator of the enclosing crate.  These are strings, in a
     -- different format than the integer disambiguators used for normal path
     -- segments.
-    , did_crate_disambig :: Text
+    , _didCrateDisambig :: Text
     -- | The segments of the path.
-    , did_path :: [Segment]
+    , _didPath :: [Segment]
     }
   deriving (Eq, Ord, Generic)
 
--- | The crate disambiguator hash produced when the crate metadata string is
--- empty.  This is the disambiguator for all sysroot crates, which are the only
--- ones we override.
-defaultDisambiguator :: Text
-defaultDisambiguator = "3a1fbbbh"
+makeLenses ''DefId
 
 -- | Parse a string into a `DefId`.
 --
 -- For convenience when writing literal paths in the Haskell source, both types
 -- of disambiguators are optional.  If the crate disambiguator is omitted, then
--- it's assumed to be `defaultDisambiguator`, and if a segment disambiguator is
--- omitted elsewhere in the path, it's assumed to be zero.  So you can write,
--- for example, `core::option::Option`, and parsing will expand it to the
--- canonical form `core/3a1fbbbh::option[0]::Option[0]`.
+-- an exception is thrown. If a segment disambiguator is omitted elsewhere in
+-- the path, it's assumed to be zero.  So you can write, for example,
+-- `foo/3a1fbbbh::bar::Baz`, and parsing will expand it to the canonical form
+-- `foo/3a1fbbbh::bar[0]::Baz[0]`.
 textId :: Text -> DefId
 textId s = DefId crate disambig segs
   where
@@ -79,7 +80,7 @@ textId s = DefId crate disambig segs
         x:xs -> (x, xs)
 
     (crate, disambig) = case T.splitOn "/" crateStr of
-        [x] -> (x, defaultDisambiguator)
+        [x] -> error $ "textId: No crate disambiguator for: " ++ T.unpack x
         [x, y] -> (x, y)
         _ -> error $ "textId: malformed crate name " ++ show crateStr
 
@@ -109,11 +110,21 @@ instance FromJSON DefId where
 instance Pretty DefId where
     pretty = viaShow
 
-
+-- | The individual 'DefId' components of a 'DefId'. The first element is the
+-- crate name, and the subsequent elements are the path segments. By convention,
+-- 'ExplodedDefId's never contain disambiguators, which make them a useful way
+-- to refer to identifiers in a slightly more stable format that does not depend
+-- on the particulars of how a package is hashed.
 type ExplodedDefId = [Text]
+
 idKey :: DefId -> ExplodedDefId
-idKey did = did_crate did : map fst (did_path did)
+idKey did = _didCrate did : map fst (_didPath did)
 
+explodedDefIdPat :: ExplodedDefId -> TH.Q TH.Pat
+explodedDefIdPat edid = [p| ((\did -> idKey did == edid) -> True) |]
+
+textIdKey :: Text -> ExplodedDefId
+textIdKey = idKey . textId
 
 idInit :: DefId -> DefId
 idInit (DefId crate disambig segs) = DefId crate disambig (init segs)
@@ -133,13 +144,3 @@ cleanVariantName = idLast
 parseFieldName :: DefId -> Maybe Text
 parseFieldName (DefId _ _ []) = Nothing
 parseFieldName did = Just $ idLast did
-
--- | Normalize a DefId string.  This allows writing down path strings in a more
--- readable form.
-normDefId :: Text -> Text
-normDefId s = idText $ textId s
-
--- | Like `normDefId`, but produces a Template Haskell pattern.  Useful for
--- defining pattern synonyms that match a specific `TyAdt` type constructor.
-normDefIdPat :: Text -> TH.Q TH.Pat
-normDefIdPat s = return $ TH.LitP $ TH.StringL $ T.unpack $ normDefId s