From efffd2e404dae9171d1426228a7d5ac137a2a1c6 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Fri, 12 Feb 2021 10:52:57 -0800
Subject: [PATCH 01/19] crux-mir.cabal: move all module into exposed-modules

---
 crux-mir/crux-mir.cabal | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/crux-mir/crux-mir.cabal b/crux-mir/crux-mir.cabal
index 89e752f58..b7fc7d7fc 100644
--- a/crux-mir/crux-mir.cabal
+++ b/crux-mir/crux-mir.cabal
@@ -65,13 +65,12 @@ library
                    Mir.PP
                    Mir.Generate
                    Mir.DefId
-  other-modules:
-                 Mir.FancyMuxTree
-                 Mir.Intrinsics
-                 Mir.Overrides
-                 Mir.TransTy
-                 Mir.Trans
-                 Mir.TransCustom
+                   Mir.FancyMuxTree
+                   Mir.Intrinsics
+                   Mir.Overrides
+                   Mir.TransTy
+                   Mir.Trans
+                   Mir.TransCustom
 
 
 executable crux-mir

From bbc792c1e9e5b002a22a823a8839edd7c0abe893 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Fri, 12 Feb 2021 10:53:11 -0800
Subject: [PATCH 02/19] crux-mir: add mainWithExtraOverrides entry point

---
 crux-mir/src/Mir/Language.hs | 57 +++++++++++++++++++++++++++++-------
 1 file changed, 46 insertions(+), 11 deletions(-)

diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs
index 3d763f785..f021eb1a6 100644
--- a/crux-mir/src/Mir/Language.hs
+++ b/crux-mir/src/Mir/Language.hs
@@ -9,11 +9,22 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RankNTypes #-}
 
 {-# OPTIONS_GHC -Wall #-}
 
-module Mir.Language (main, mainWithOutputTo, mainWithOutputConfig, runTests,
-                     MIROptions(..), defaultMirOptions) where
+module Mir.Language (
+    main,
+    mainWithExtraOverrides,
+    mainWithOutputTo,
+    mainWithOutputConfig,
+    runTests,
+    runTestsWithExtraOverrides,
+    BindExtraOverridesFn,
+    noExtraOverrides,
+    MIROptions(..),
+    defaultMirOptions,
+) where
 
 import qualified Data.Aeson as Aeson
 import qualified Data.BitVector.Sized as BV
@@ -84,17 +95,38 @@ import           Mir.Trans (transStatics)
 import           Mir.TransTy
 
 main :: IO ()
-main = mainWithOutputConfig defaultOutputConfig >>= exitWith
+main = mainWithOutputConfig defaultOutputConfig noExtraOverrides >>= exitWith
+
+mainWithExtraOverrides :: BindExtraOverridesFn -> IO ()
+mainWithExtraOverrides bindExtra =
+    mainWithOutputConfig defaultOutputConfig bindExtra >>= exitWith
 
-mainWithOutputTo :: Handle -> IO ExitCode
-mainWithOutputTo h = mainWithOutputConfig (OutputConfig False h h False)
+mainWithOutputTo :: Handle -> BindExtraOverridesFn -> IO ExitCode
+mainWithOutputTo h bindExtra = mainWithOutputConfig (OutputConfig False h h False) bindExtra
 
-mainWithOutputConfig :: OutputConfig -> IO ExitCode
-mainWithOutputConfig outCfg =
-    Crux.loadOptions outCfg "crux-mir" "0.1" mirConfig $ runTests
+mainWithOutputConfig :: OutputConfig -> BindExtraOverridesFn -> IO ExitCode
+mainWithOutputConfig outCfg bindExtra =
+    Crux.loadOptions outCfg "crux-mir" "0.1" mirConfig $ runTestsWithExtraOverrides bindExtra
 
-runTests :: (Crux.Logs) => (Crux.CruxOptions, MIROptions) -> IO ExitCode
-runTests (cruxOpts, mirOpts) = do
+type BindExtraOverridesFn = forall args ret blocks sym rtp a r.
+    C.IsSymInterface sym =>
+    Maybe (Crux.SomeOnlineSolver sym) ->
+    Text ->
+    C.CFG MIR blocks args ret ->
+    Maybe (C.OverrideSim (Model sym) sym MIR rtp a r ())
+
+noExtraOverrides :: BindExtraOverridesFn
+noExtraOverrides _ _ _ = Nothing
+
+runTests :: (Crux.Logs) =>
+    (Crux.CruxOptions, MIROptions) -> IO ExitCode
+runTests opts = runTestsWithExtraOverrides noExtraOverrides opts
+
+runTestsWithExtraOverrides :: (Crux.Logs) =>
+    BindExtraOverridesFn ->
+    (Crux.CruxOptions, MIROptions) ->
+    IO ExitCode
+runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
     let ?debug              = Crux.simVerbose cruxOpts
     --let ?assertFalseOnError = assertFalse mirOpts
     let ?assertFalseOnError = True
@@ -152,7 +184,10 @@ runTests (cruxOpts, mirOpts) = do
     let linkOverrides :: C.IsSymInterface sym =>
             Maybe (Crux.SomeOnlineSolver sym) -> C.OverrideSim (Model sym) sym MIR rtp a r ()
         linkOverrides symOnline =
-            forM_ (Map.toList cfgMap) $ \(fn, C.AnyCFG cfg) -> bindFn symOnline fn cfg
+            forM_ (Map.toList cfgMap) $ \(fn, C.AnyCFG cfg) -> do
+                case bindExtra symOnline fn cfg of
+                    Just f -> f
+                    Nothing -> bindFn symOnline fn cfg
     let entry = W4.mkProgramLoc "<entry>" W4.InternalPos
     let testStartLoc fnName =
             W4.mkProgramLoc (W4.functionNameFromText $ idText fnName) (W4.OtherPos "<start>")

From a5ec4eb3c0cd1fd34298f0a3ae6b7865db97e1cb Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Fri, 12 Feb 2021 17:03:42 -0800
Subject: [PATCH 03/19] crux-mir: add MethodSpec and MethodSpecBuilder
 intrinsics

---
 crux-mir/lib/crucible/lib.rs             |   2 +
 crux-mir/lib/crucible/method_spec/mod.rs |  81 +++++++++++++++++
 crux-mir/lib/crucible/method_spec/raw.rs |  57 ++++++++++++
 crux-mir/src/Mir/Intrinsics.hs           | 110 +++++++++++++++++++++--
 crux-mir/src/Mir/TransTy.hs              |   9 ++
 5 files changed, 252 insertions(+), 7 deletions(-)
 create mode 100644 crux-mir/lib/crucible/method_spec/mod.rs
 create mode 100644 crux-mir/lib/crucible/method_spec/raw.rs

diff --git a/crux-mir/lib/crucible/lib.rs b/crux-mir/lib/crucible/lib.rs
index 93a669bfb..5d8419668 100644
--- a/crux-mir/lib/crucible/lib.rs
+++ b/crux-mir/lib/crucible/lib.rs
@@ -1,8 +1,10 @@
 #![no_std]
 #![feature(core_intrinsics)]
 #![feature(crucible_intrinsics)]
+#![feature(unboxed_closures)]
 
 pub mod bitvector;
+pub mod method_spec;
 pub mod sym_bytes;
 pub mod symbolic;
 
diff --git a/crux-mir/lib/crucible/method_spec/mod.rs b/crux-mir/lib/crucible/method_spec/mod.rs
new file mode 100644
index 000000000..2a88919d3
--- /dev/null
+++ b/crux-mir/lib/crucible/method_spec/mod.rs
@@ -0,0 +1,81 @@
+//! Provides the `MethodSpec` type, used for compositional reasoning.  Also provides
+//! `MethodSpecBuilder`, which is used internally by the compositional reasoning macros to
+//! construct a `MethodSpec` from a symbolic test.
+//!
+//! Note that these types work only when running under `crux-mir-comp`.  Trying to use them under
+//! ordinary `crux-mir` will produce an error.
+use core::fmt;
+
+mod raw;
+
+
+/// The specification of a function.  This can be used when verifying callers of the function to
+/// avoid simulating the entire function itself.
+#[derive(Clone, Copy)]
+pub struct MethodSpec {
+    raw: raw::MethodSpec,
+}
+
+impl MethodSpec {
+    /// Enable this `MethodSpec` to be used as an override for its subject function.
+    pub fn enable(&self) {
+        raw::spec_enable(self.raw);
+    }
+}
+
+impl fmt::Debug for MethodSpec {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        let s = raw::spec_pretty_print(self.raw);
+        fmt.write_str("MethodSpec {")?;
+        for (i, chunk) in s.split("\n").enumerate() {
+            if i > 0 {
+                fmt.write_str(", ")?;
+            }
+            fmt.write_str(chunk);
+        }
+        fmt.write_str("}")?;
+        Ok(())
+    }
+}
+
+
+/// Helper type used to incrementally construct a `MethodSpec` for a function.
+pub struct MethodSpecBuilder {
+    raw: raw::MethodSpecBuilder,
+}
+
+impl fmt::Debug for MethodSpecBuilder {
+    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
+        write!(fmt, "MethodSpecBuilder {{ .. }}")
+    }
+}
+
+impl MethodSpecBuilder {
+    pub fn new<Args, F: Fn<Args>>(f: F) -> MethodSpecBuilder {
+        MethodSpecBuilder {
+            raw: raw::builder_new::<F>(),
+        }
+    }
+
+    pub fn add_arg<T>(&mut self, x: &T) {
+        self.raw = raw::builder_add_arg(self.raw, x);
+    }
+
+    pub fn gather_assumes(&mut self) {
+        self.raw = raw::builder_gather_assumes(self.raw);
+    }
+
+    pub fn set_return<T>(&mut self, x: &T) {
+        self.raw = raw::builder_set_return(self.raw, x);
+    }
+
+    pub fn gather_asserts(&mut self) {
+        self.raw = raw::builder_gather_asserts(self.raw);
+    }
+
+    pub fn finish(self) -> MethodSpec {
+        MethodSpec {
+            raw: raw::builder_finish(self.raw),
+        }
+    }
+}
diff --git a/crux-mir/lib/crucible/method_spec/raw.rs b/crux-mir/lib/crucible/method_spec/raw.rs
new file mode 100644
index 000000000..e000004aa
--- /dev/null
+++ b/crux-mir/lib/crucible/method_spec/raw.rs
@@ -0,0 +1,57 @@
+/// Crucible `MethodSpecType`, exposed to Rust.
+///
+/// As usual for Crucible types, this implements `Copy`, since it's backed by a boxed,
+/// garbage-collected Haskell value.  It contains a dummy field to ensure the Rust compiler sees it
+/// as having non-zero size.  The representation is overridden within `crux-mir`, so the field
+/// should not be accessed when running symbolically.
+#[derive(Clone, Copy)]
+pub struct MethodSpec(u8);
+
+// We only have `libcore` available, so we can't return `String` here.  Instead, the override for
+// this function within `crux-mir` will construct and leak a `str`.
+pub fn spec_pretty_print(ms: MethodSpec) -> &'static str {
+    "(unknown MethodSpec)"
+}
+
+/// Enable using `ms` in place of calls to the actual function.  The function to override is
+/// determined by the `F` type parameter of `builder_new` during the construction of the
+/// `MethodSpec`.
+pub fn spec_enable(ms: MethodSpec) {
+}
+
+
+/// Crucible `MethodSpecBuilderType`, exposed to Rust.
+#[derive(Clone, Copy)]
+pub struct MethodSpecBuilder(u8);
+
+pub fn builder_new<F>() -> MethodSpecBuilder {
+    // If the program is running under ordinary `crux-mir` instead of `crux-mir-comp`, then the
+    // override for this function will be missing.  We could provide a dummy implementation for
+    // that case, but it's better to fail early.  Otherwise users will get cryptic errors when
+    // invoking their spec functions, as `builder_finish` won't have its usual effect of discarding
+    // any new goals added by the spec function.
+    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
+}
+
+pub fn builder_add_arg<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
+    let _ = x;
+    msb
+}
+
+pub fn builder_gather_assumes(msb: MethodSpecBuilder) -> MethodSpecBuilder {
+    msb
+}
+
+pub fn builder_set_return<T>(msb: MethodSpecBuilder, x: &T) -> MethodSpecBuilder {
+    let _ = x;
+    msb
+}
+
+pub fn builder_gather_asserts(msb: MethodSpecBuilder) -> MethodSpecBuilder {
+    msb
+}
+
+pub fn builder_finish(msb: MethodSpecBuilder) -> MethodSpec {
+    let _ = msb;
+    MethodSpec(0)
+}
diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index fdbccacfa..3860a968f 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -70,6 +70,7 @@ import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.String
 import qualified Data.Vector as V
+import           Data.Word
 
 import           Prettyprinter
 import qualified Text.Regex as Regex
@@ -97,6 +98,8 @@ import           Lang.Crucible.Simulator.RegValue
 import           Lang.Crucible.Simulator.RegMap
 import           Lang.Crucible.Simulator.SimError
 
+import           Crux.Types (Model)
+
 import           What4.Concrete (ConcreteVal(..), concreteType)
 import           What4.Interface
 import           What4.Partial
@@ -114,13 +117,6 @@ import           Debug.Trace
 import           Unsafe.Coerce
 
 
-mirIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
-mirIntrinsicTypes =
-   MapF.insert (knownSymbol @MirReferenceSymbol) IntrinsicMuxFn $
-   MapF.insert (knownSymbol @MirVectorSymbol) IntrinsicMuxFn $
-   MapF.empty
-
-
 
 -- Rust enum representation
 
@@ -1709,3 +1705,103 @@ getSlicePtr e = getStruct i1of2 e
 
 getSliceLen :: Expr MIR s (MirSlice tp) -> Expr MIR s UsizeType
 getSliceLen e = getStruct i2of2 e
+
+
+--------------------------------------------------------------------------------
+-- ** MethodSpec and MethodSpecBuilder
+--
+-- We define the intrinsics here so they can be used in `TransTy.tyToRepr`, and
+-- also define their interfaces (as typeclasses), but the concrete
+-- implementations of these types are in `saw-script/crux-mir-comp`, since they
+-- depend on some SAW components (notably SAW's `MethodSpec` and `Term` types).
+
+class MethodSpecImpl sym ms where
+    -- | Pretty-print the MethodSpec, returning the result as a Rust string
+    -- (`&str`).
+    msPrettyPrint ::
+        forall rtp args ret.
+        ms ->
+        OverrideSim (Model sym) sym MIR rtp args ret (RegValue sym (MirSlice (BVType 8)))
+
+    -- | Enable the MethodSpec for use as an override for the remainder of the
+    -- current test.
+    msEnable ::
+        forall rtp args ret.
+        ms ->
+        OverrideSim (Model sym) sym MIR rtp args ret ()
+
+data MethodSpec sym = forall ms. MethodSpecImpl sym ms => MethodSpec {
+    msData :: ms,
+    msNonce :: Word64
+}
+
+type MethodSpecSymbol = "MethodSpec"
+type MethodSpecType = IntrinsicType MethodSpecSymbol EmptyCtx
+
+pattern MethodSpecRepr :: () => tp' ~ MethodSpecType => TypeRepr tp'
+pattern MethodSpecRepr <-
+     IntrinsicRepr (testEquality (knownSymbol @MethodSpecSymbol) -> Just Refl) Empty
+ where MethodSpecRepr = IntrinsicRepr (knownSymbol @MethodSpecSymbol) Empty
+
+type family MethodSpecFam (sym :: Type) (ctx :: Ctx CrucibleType) :: Type where
+  MethodSpecFam sym EmptyCtx = MethodSpec sym
+  MethodSpecFam sym ctx = TypeError
+    ('Text "MethodSpecType expects no arguments, but was given" ':<>: 'ShowType ctx)
+instance IsSymInterface sym => IntrinsicClass sym MethodSpecSymbol where
+  type Intrinsic sym MethodSpecSymbol ctx = MethodSpecFam sym ctx
+
+  muxIntrinsic _sym _iTypes _nm Empty _p ms1 ms2
+    | msNonce ms1 == msNonce ms2 = return ms1
+    | otherwise = fail "can't mux MethodSpecs"
+  muxIntrinsic _sym _tys nm ctx _ _ _ = typeError nm ctx
+
+
+class MethodSpecBuilderImpl sym msb where
+    msbAddArg :: forall rtp args ret tp.
+        TypeRepr tp -> MirReferenceMux sym tp -> msb ->
+        OverrideSim (Model sym) sym MIR rtp args ret msb
+    msbSetReturn :: forall rtp args ret tp.
+        TypeRepr tp -> MirReferenceMux sym tp -> msb ->
+        OverrideSim (Model sym) sym MIR rtp args ret msb
+    msbGatherAssumes :: forall rtp args ret.
+        msb ->
+        OverrideSim (Model sym) sym MIR rtp args ret msb
+    msbGatherAsserts :: forall rtp args ret.
+        msb ->
+        OverrideSim (Model sym) sym MIR rtp args ret msb
+    msbFinish :: forall rtp args ret.
+        msb ->
+        OverrideSim (Model sym) sym MIR rtp args ret (MethodSpec sym)
+
+data MethodSpecBuilder sym = forall msb. MethodSpecBuilderImpl sym msb => MethodSpecBuilder msb
+
+type MethodSpecBuilderSymbol = "MethodSpecBuilder"
+type MethodSpecBuilderType = IntrinsicType MethodSpecBuilderSymbol EmptyCtx
+
+pattern MethodSpecBuilderRepr :: () => tp' ~ MethodSpecBuilderType => TypeRepr tp'
+pattern MethodSpecBuilderRepr <-
+     IntrinsicRepr (testEquality (knownSymbol @MethodSpecBuilderSymbol) -> Just Refl) Empty
+ where MethodSpecBuilderRepr = IntrinsicRepr (knownSymbol @MethodSpecBuilderSymbol) Empty
+
+type family MethodSpecBuilderFam (sym :: Type) (ctx :: Ctx CrucibleType) :: Type where
+  MethodSpecBuilderFam sym EmptyCtx = MethodSpecBuilder sym
+  MethodSpecBuilderFam sym ctx = TypeError
+    ('Text "MethodSpecBuilderType expects no arguments, but was given" ':<>: 'ShowType ctx)
+instance IsSymInterface sym => IntrinsicClass sym MethodSpecBuilderSymbol where
+  type Intrinsic sym MethodSpecBuilderSymbol ctx = MethodSpecBuilderFam sym ctx
+
+  muxIntrinsic _sym _iTypes _nm Empty _ _ _ =
+    fail "can't mux MethodSpecBuilders"
+  muxIntrinsic _sym _tys nm ctx _ _ _ = typeError nm ctx
+
+
+-- Table of all MIR-specific intrinsic types.  Must be at the end so it can see
+-- past all previous TH calls.
+
+mirIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
+mirIntrinsicTypes =
+   MapF.insert (knownSymbol @MirReferenceSymbol) IntrinsicMuxFn $
+   MapF.insert (knownSymbol @MirVectorSymbol) IntrinsicMuxFn $
+   MapF.insert (knownSymbol @MethodSpecSymbol) IntrinsicMuxFn $
+   MapF.insert (knownSymbol @MethodSpecBuilderSymbol) IntrinsicMuxFn $
+   MapF.empty
diff --git a/crux-mir/src/Mir/TransTy.hs b/crux-mir/src/Mir/TransTy.hs
index 2cc498112..300229cef 100644
--- a/crux-mir/src/Mir/TransTy.hs
+++ b/crux-mir/src/Mir/TransTy.hs
@@ -65,6 +65,7 @@ import           Mir.Intrinsics
     , SizeBits, pattern UsizeRepr, pattern IsizeRepr
     , isizeLit
     , RustEnumType, pattern RustEnumRepr, mkRustEnum, rustEnumVariant, rustEnumDiscriminant
+    , pattern MethodSpecRepr, pattern MethodSpecBuilderRepr
     , DynRefType)
 
 
@@ -123,6 +124,12 @@ pattern CTyBv512 = CTyBv CTyBvSize512
 pattern CTyAny <- M.TyAdt _ $(M.normDefIdPat "core::crucible::any::Any") (M.Substs [])
   where CTyAny = M.TyAdt (M.textId "type::adt") (M.textId "core::crucible::any::Any") (M.Substs [])
 
+pattern CTyMethodSpec <- M.TyAdt _ $(M.normDefIdPat "crucible::method_spec::raw::MethodSpec") (M.Substs [])
+  where CTyMethodSpec = M.TyAdt (M.textId "type::adt") (M.textId "crucible::method_spec::raw::MethodSpec") (M.Substs [])
+
+pattern CTyMethodSpecBuilder <- M.TyAdt _ $(M.normDefIdPat "crucible::method_spec::raw::MethodSpecBuilder") (M.Substs [])
+  where CTyMethodSpecBuilder = M.TyAdt (M.textId "type::adt") (M.textId "crucible::method_spec::raw::MethodSpecBuilder") (M.Substs [])
+
 
 -- These don't have custom representation, but are referenced in various
 -- places.
@@ -150,6 +157,8 @@ tyToRepr t0 = case t0 of
       Some (C.SymbolicArrayRepr (Ctx.Empty Ctx.:> C.BaseBVRepr (knownNat @SizeBits)) btr)
     | otherwise -> error $ "unsupported: crucible arrays of non-base type"
   CTyAny -> Some C.AnyRepr
+  CTyMethodSpec -> Some MethodSpecRepr
+  CTyMethodSpecBuilder -> Some MethodSpecBuilderRepr
 
   -- Defined as `union MaybeUninit<T> { uninit: (), value: ManuallyDrop<T> }`.
   -- We skip the outer union, leaving only `ManuallyDrop<T>`, which is a

From 57dcde9313111b0fb6fc2ea253b917d496d81cf9 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Tue, 16 Feb 2021 14:29:05 -0800
Subject: [PATCH 04/19] crux-mir: TransTy: add isUnsized

---
 crux-mir/src/Mir/TransTy.hs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/crux-mir/src/Mir/TransTy.hs b/crux-mir/src/Mir/TransTy.hs
index 300229cef..10930ed60 100644
--- a/crux-mir/src/Mir/TransTy.hs
+++ b/crux-mir/src/Mir/TransTy.hs
@@ -258,6 +258,14 @@ canInitialize ty = case ty of
     --M.TyRef ty' _ -> canInitialize ty'
     _ -> False
 
+isUnsized :: M.Ty -> Bool
+isUnsized ty = case ty of
+    M.TyStr -> True
+    M.TySlice _ -> True
+    M.TyDynamic _ -> True
+    -- TODO: struct types whose last field is unsized ("custom DSTs")
+    _ -> False
+
 
 variantFields :: TransTyConstraint => M.Variant -> Some C.CtxRepr
 variantFields (M.Variant _vn _vd vfs _vct) =

From ccc62d927195acacad48eb33b5f79dc15c59552d Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 14 Jan 2021 09:28:06 -0800
Subject: [PATCH 05/19] crux-mir: add functions for manipulating MirRefs within
 IO/OverrideSim monad

---
 crux-mir/src/Mir/Intrinsics.hs | 39 +++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index 3860a968f..d8dcaf494 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1504,6 +1504,17 @@ execMirStmt stmt s =
 -- MirReferenceType manipulation within the OverrideSim monad.  These are
 -- useful for implementing overrides that work with MirReferences.
 
+newMirRefSim :: IsSymInterface sym =>
+    TypeRepr tp ->
+    OverrideSim m sym MIR rtp args ret (MirReferenceMux sym tp)
+newMirRefSim tpr = do
+    sym <- getSymInterface
+    s <- get
+    let halloc = simHandleAllocator $ s ^. stateContext
+    rc <- liftIO $ freshRefCell halloc tpr
+    let ref = MirReference (RefCell_RefRoot rc) Empty_RefPath
+    return $ MirReferenceMux $ toFancyMuxTree sym ref
+
 readRefMuxSim :: IsSymInterface sym =>
     TypeRepr tp' ->
     (MirReference sym tp -> MuxLeafT sym IO (RegValue sym tp')) ->
@@ -1515,6 +1526,17 @@ readRefMuxSim tpr' f (MirReferenceMux ref) = do
     let iTypes = ctxIntrinsicTypes ctx
     liftIO $ readFancyMuxTree' sym f (muxRegForType sym iTypes tpr') ref
 
+readRefMuxIO :: IsSymInterface sym =>
+    sym -> SimState p sym ext rtp f a ->
+    TypeRepr tp' ->
+    (MirReference sym tp -> MuxLeafT sym IO (RegValue sym tp')) ->
+    MirReferenceMux sym tp ->
+    IO (RegValue sym tp')
+readRefMuxIO sym s tpr' f (MirReferenceMux ref) = do
+    let ctx = s ^. stateContext
+    let iTypes = ctxIntrinsicTypes ctx
+    readFancyMuxTree' sym f (muxRegForType sym iTypes tpr') ref
+
 modifyRefMuxSim :: IsSymInterface sym =>
     (MirReference sym tp -> MuxLeafT sym IO (MirReference sym tp')) ->
     MirReferenceMux sym tp ->
@@ -1531,7 +1553,22 @@ readMirRefSim :: IsSymInterface sym =>
 readMirRefSim tpr ref = do
     sym <- getSymInterface
     s <- get
-    readRefMuxSim tpr (readMirRefLeaf s sym) ref
+    liftIO $ readMirRefIO sym s tpr ref
+
+readMirRefIO :: IsSymInterface sym =>
+    sym -> SimState p sym ext rtp f a ->
+    TypeRepr tp -> MirReferenceMux sym tp ->
+    IO (RegValue sym tp)
+readMirRefIO sym s tpr ref = readRefMuxIO sym s tpr (readMirRefLeaf s sym) ref
+
+writeMirRefSim :: IsSymInterface sym =>
+    TypeRepr tp -> MirReferenceMux sym tp -> RegValue sym tp ->
+    OverrideSim m sym MIR rtp args ret ()
+writeMirRefSim tpr (MirReferenceMux ref) x = do
+    sym <- getSymInterface
+    s <- get
+    s' <- liftIO $ foldFancyMuxTree sym (\s' ref' -> writeMirRefLeaf s' sym ref' x) s ref
+    put s'
 
 subindexMirRefSim :: IsSymInterface sym =>
     TypeRepr tp -> MirReferenceMux sym (MirVectorType tp) -> RegValue sym UsizeType ->

From 8b10cfcafd245f80035bfc68a9c8094a6c93838e Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Wed, 13 Jan 2021 15:27:04 -0800
Subject: [PATCH 06/19] crux-mir: add mirRef_eqIO

---
 crux-mir/src/Mir/Intrinsics.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index d8dcaf494..615bcc832 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1300,6 +1300,11 @@ mirRef_eqLeaf sym _ _ =
     -- All valid references are disjoint from all integer references.
     return $ falsePred sym
 
+mirRef_eqIO :: IsSymInterface sym => sym ->
+    MirReferenceMux sym tp -> MirReferenceMux sym tp -> IO (RegValue sym BoolType)
+mirRef_eqIO sym (MirReferenceMux r1) (MirReferenceMux r2) =
+    zipFancyMuxTrees' sym (mirRef_eqLeaf sym) (itePred sym) r1 r2
+
 mirRef_offsetLeaf :: IsSymInterface sym => sym ->
     TypeRepr tp -> MirReference sym tp -> RegValue sym IsizeType ->
     MuxLeafT sym IO (MirReference sym tp)

From 259e08697cd1a8a2c45022103ecc627d7a85a96e Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Wed, 17 Feb 2021 10:15:09 -0800
Subject: [PATCH 07/19] crux-mir: pass MIR CollectionState to overrides

---
 crux-mir/src/Mir/Language.hs  |  7 ++++---
 crux-mir/src/Mir/Overrides.hs | 10 +++++++---
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs
index f021eb1a6..35407331f 100644
--- a/crux-mir/src/Mir/Language.hs
+++ b/crux-mir/src/Mir/Language.hs
@@ -111,12 +111,13 @@ mainWithOutputConfig outCfg bindExtra =
 type BindExtraOverridesFn = forall args ret blocks sym rtp a r.
     C.IsSymInterface sym =>
     Maybe (Crux.SomeOnlineSolver sym) ->
+    CollectionState ->
     Text ->
     C.CFG MIR blocks args ret ->
     Maybe (C.OverrideSim (Model sym) sym MIR rtp a r ())
 
 noExtraOverrides :: BindExtraOverridesFn
-noExtraOverrides _ _ _ = Nothing
+noExtraOverrides _ _ _ _ = Nothing
 
 runTests :: (Crux.Logs) =>
     (Crux.CruxOptions, MIROptions) -> IO ExitCode
@@ -185,9 +186,9 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
             Maybe (Crux.SomeOnlineSolver sym) -> C.OverrideSim (Model sym) sym MIR rtp a r ()
         linkOverrides symOnline =
             forM_ (Map.toList cfgMap) $ \(fn, C.AnyCFG cfg) -> do
-                case bindExtra symOnline fn cfg of
+                case bindExtra symOnline (mir ^. rmCS) fn cfg of
                     Just f -> f
-                    Nothing -> bindFn symOnline fn cfg
+                    Nothing -> bindFn symOnline (mir ^. rmCS) fn cfg
     let entry = W4.mkProgramLoc "<entry>" W4.InternalPos
     let testStartLoc fnName =
             W4.mkProgramLoc (W4.functionNameFromText $ idText fnName) (W4.OtherPos "<start>")
diff --git a/crux-mir/src/Mir/Overrides.hs b/crux-mir/src/Mir/Overrides.hs
index f773b9580..c9d30a755 100644
--- a/crux-mir/src/Mir/Overrides.hs
+++ b/crux-mir/src/Mir/Overrides.hs
@@ -85,6 +85,7 @@ import Crux.Types (Model(..), Vars(..), Vals(..), Entry(..))
 
 import Mir.DefId
 import Mir.FancyMuxTree
+import Mir.Generator (CollectionState)
 import Mir.Intrinsics
 
 
@@ -370,9 +371,12 @@ regEval sym baseEval tpr v = go tpr v
 bindFn ::
   forall args ret blocks sym rtp a r .
   (IsSymInterface sym) =>
-  Maybe (SomeOnlineSolver sym) -> Text -> CFG MIR blocks args ret ->
+  Maybe (SomeOnlineSolver sym) ->
+  CollectionState ->
+  Text ->
+  CFG MIR blocks args ret ->
   OverrideSim (Model sym) sym MIR rtp a r ()
-bindFn symOnline name cfg
+bindFn symOnline _cs name cfg
   | (normDefId "crucible::array::symbolic" <> "::_inst") `Text.isPrefixOf` name
   , Empty :> MirSliceRepr (BVRepr w) <- cfgArgTypes cfg
   , UsizeArrayRepr btpr <- cfgReturnType cfg
@@ -383,7 +387,7 @@ bindFn symOnline name cfg
   , Empty :> tpr <- cfgArgTypes cfg
   , Just Refl <- testEquality tpr (cfgReturnType cfg)
   = bindFnHandle (cfgHandle cfg) $ UseOverride $ mkOverride' "concretize" tpr $ concretize symOnline
-bindFn _symOnline fn cfg =
+bindFn _symOnline _cs fn cfg =
   getSymInterface >>= \s ->
   case Map.lookup fn (overrides s) of
     Nothing ->

From 25bab3f00fee0bd03e18c5115d7272edec23d292 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Wed, 17 Feb 2021 11:29:52 -0800
Subject: [PATCH 08/19] crux-mir: add _Wrapped lens for Substs

---
 crux-mir/src/Mir/Mir.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/crux-mir/src/Mir/Mir.hs b/crux-mir/src/Mir/Mir.hs
index 34d8e5efa..3bb42d829 100644
--- a/crux-mir/src/Mir/Mir.hs
+++ b/crux-mir/src/Mir/Mir.hs
@@ -19,6 +19,7 @@ License          : BSD3
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TypeFamilies #-}
 
 {-# LANGUAGE OverloadedStrings #-}
 
@@ -34,9 +35,7 @@ import qualified Data.ByteString as B
 import Data.Map.Strict (Map)
 import Data.Text (Text)
 
-import Data.Semigroup (Semigroup(..))
-
-import Control.Lens (makeLenses)
+import Control.Lens (makeLenses, makeWrapped)
 
 import GHC.Generics 
 
@@ -540,6 +539,7 @@ makeLenses ''Vtable
 makeLenses ''Intrinsic
 makeLenses ''Instance
 makeLenses ''NamedTy
+makeWrapped ''Substs
 
 --------------------------------------------------------------------------------------
 -- Other instances for ADT types

From 619b36505757d487babf48b29738c0a20edae6eb Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Wed, 17 Feb 2021 11:30:15 -0800
Subject: [PATCH 09/19] crux-mir: expose `sym ~ W4.ExprBuilder ...` constraint
 in BindExtraOverridesFn

---
 crux-mir/src/Mir/Language.hs | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs
index 35407331f..39a59342e 100644
--- a/crux-mir/src/Mir/Language.hs
+++ b/crux-mir/src/Mir/Language.hs
@@ -66,6 +66,7 @@ import qualified Lang.Crucible.FunctionHandle          as C
 import qualified Lang.Crucible.Backend                 as C
 
 -- what4
+import qualified What4.Expr.Builder                    as W4
 import qualified What4.Interface                       as W4
 import qualified What4.Config                          as W4
 import qualified What4.Partial                         as W4
@@ -108,8 +109,8 @@ mainWithOutputConfig :: OutputConfig -> BindExtraOverridesFn -> IO ExitCode
 mainWithOutputConfig outCfg bindExtra =
     Crux.loadOptions outCfg "crux-mir" "0.1" mirConfig $ runTestsWithExtraOverrides bindExtra
 
-type BindExtraOverridesFn = forall args ret blocks sym rtp a r.
-    C.IsSymInterface sym =>
+type BindExtraOverridesFn = forall sym t st fs args ret blocks rtp a r.
+    (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
     Maybe (Crux.SomeOnlineSolver sym) ->
     CollectionState ->
     Text ->
@@ -182,7 +183,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
     let cfgMap = mir^.rmCFGs
 
     -- Simulate each test case
-    let linkOverrides :: C.IsSymInterface sym =>
+    let linkOverrides :: (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs) =>
             Maybe (Crux.SomeOnlineSolver sym) -> C.OverrideSim (Model sym) sym MIR rtp a r ()
         linkOverrides symOnline =
             forM_ (Map.toList cfgMap) $ \(fn, C.AnyCFG cfg) -> do
@@ -207,7 +208,8 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
     -- that calls `simTest`.  Counterexamples are printed separately, and only
     -- for tests that failed.
 
-    let simTest :: forall sym. (C.IsSymInterface sym, Crux.Logs) =>
+    let simTest :: forall sym t st fs.
+            (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, Crux.Logs) =>
             Maybe (Crux.SomeOnlineSolver sym) -> DefId -> Fun Model sym MIR Ctx.EmptyCtx C.UnitType
         simTest symOnline fnName = do
             when (not $ printResultOnly mirOpts) $

From 4f429457ec2994703a6be26efcbbb23c10dc9528 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 5 Nov 2020 13:42:48 -0800
Subject: [PATCH 10/19] add mirFail stubs for construction of
 MethodSpec{,Builder}

---
 crux-mir/src/Mir/Trans.hs   | 19 +++++++++++++++++++
 crux-mir/src/Mir/TransTy.hs |  4 ++++
 2 files changed, 23 insertions(+)

diff --git a/crux-mir/src/Mir/Trans.hs b/crux-mir/src/Mir/Trans.hs
index 0b30c4217..93db44cac 100644
--- a/crux-mir/src/Mir/Trans.hs
+++ b/crux-mir/src/Mir/Trans.hs
@@ -131,6 +131,8 @@ u8ToBV8 _ = error $ "BUG: array literals should only contain bytes (u8)"
 --
 
 transConstVal :: HasCallStack => M.Ty -> Some C.TypeRepr -> M.ConstVal -> MirGenerator h s ret (MirExp s)
+
+-- Custom types
 transConstVal (CTyBv _) (Some (C.BVRepr w)) (M.ConstStruct [M.ConstInt i, M.ConstStruct []]) = do
     val <- case M.fromIntegerLit i of
         0 -> return 0   -- Bv::ZERO
@@ -138,6 +140,11 @@ transConstVal (CTyBv _) (Some (C.BVRepr w)) (M.ConstStruct [M.ConstInt i, M.Cons
         2 -> return $ (1 `shift` fromIntegral (intValue w)) - 1    -- Bv::MAX
         i' -> mirFail $ "unknown bitvector constant " ++ show i'
     return $ MirExp (C.BVRepr w) (S.app $ eBVLit w val)
+transConstVal CTyMethodSpec _ _ = do
+    mirFail "transConstVal: can't construct MethodSpec without an override"
+transConstVal CTyMethodSpecBuilder _ _ = do
+    mirFail "transConstVal: can't construct MethodSpecBuilder without an override"
+
 transConstVal _ty (Some (C.BVRepr w)) (M.ConstInt i) =
     return $ MirExp (C.BVRepr w) (S.app $ eBVLit w (fromInteger (M.fromIntegerLit i)))
 transConstVal _ty (Some (C.BoolRepr)) (M.ConstBool b) = return $ MirExp (C.BoolRepr) (S.litExpr b)
@@ -936,6 +943,15 @@ evalRval (M.Aggregate ak ops) = case ak of
                                        return $ buildTuple args
 evalRval rv@(M.RAdtAg (M.AdtAg adt agv ops ty)) = do
     case ty of
+      -- It's not legal to construct a MethodSpec using a Rust struct
+      -- constructor, so we translate as "assert(false)" instead.  Only
+      -- functions in the `method_spec::raw` should be creating MethodSpecs
+      -- directly, and those functions will be overridden, so the code we
+      -- generate here never runs.
+      CTyMethodSpec ->
+        mirFail $ "evalRval: can't construct MethodSpec without an override"
+      CTyMethodSpecBuilder ->
+        mirFail $ "evalRval: can't construct MethodSpecBuilder without an override"
       TyAdt _ _ _ -> do
         es <- mapM evalOperand ops
         case adt^.adtkind of
@@ -1499,6 +1515,9 @@ initialValue ty@(CTyBv _sz)
   | Some (C.BVRepr w) <- tyToRepr ty
   = return $ Just $ MirExp (C.BVRepr w) $ S.app $ eBVLit w 0
   | otherwise = mirFail $ "Bv type " ++ show ty ++ " does not have BVRepr"
+initialValue CTyMethodSpec = return Nothing
+initialValue CTyMethodSpecBuilder = return Nothing
+
 initialValue M.TyBool       = return $ Just $ MirExp C.BoolRepr (S.false)
 initialValue (M.TyTuple []) = return $ Just $ MirExp C.UnitRepr (R.App E.EmptyApp)
 initialValue (M.TyTuple tys) = do
diff --git a/crux-mir/src/Mir/TransTy.hs b/crux-mir/src/Mir/TransTy.hs
index 10930ed60..24d81dda3 100644
--- a/crux-mir/src/Mir/TransTy.hs
+++ b/crux-mir/src/Mir/TransTy.hs
@@ -243,6 +243,10 @@ dynRefRepr = C.StructRepr dynRefCtx
 -- fields are wrapped in `Maybe` to support field-by-field initialization.
 canInitialize :: M.Ty -> Bool
 canInitialize ty = case ty of
+    -- Custom types
+    CTyMethodSpec -> False
+    CTyMethodSpecBuilder -> False
+
     -- Primitives
     M.TyBool -> True
     M.TyChar -> True

From 46aa87f2341fc98cd7bf6b57c5ef61fbadce4541 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 18 Feb 2021 11:12:52 -0800
Subject: [PATCH 11/19] let test suites override the default mir-json -L search
 path

---
 crux-mir/src/Mir/Generate.hs | 10 +++++-----
 crux-mir/src/Mir/Language.hs |  7 +++++++
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/crux-mir/src/Mir/Generate.hs b/crux-mir/src/Mir/Generate.hs
index b6c20afde..d196a0a61 100644
--- a/crux-mir/src/Mir/Generate.hs
+++ b/crux-mir/src/Mir/Generate.hs
@@ -77,10 +77,10 @@ needsRebuild output inputs = do
 mirJsonOutFile :: FilePath -> FilePath
 mirJsonOutFile rustFile = rustFile -<.> "mir"
 
-getRlibsDir :: IO FilePath
-getRlibsDir = maybe "rlibs" id <$> lookupEnv "CRUX_RUST_LIBRARY_PATH"
+getRlibsDir :: (?defaultRlibsDir :: FilePath) => IO FilePath
+getRlibsDir = maybe ?defaultRlibsDir id <$> lookupEnv "CRUX_RUST_LIBRARY_PATH"
 
-compileMirJson :: Bool -> Bool -> FilePath -> IO ()
+compileMirJson :: (?defaultRlibsDir :: FilePath) => Bool -> Bool -> FilePath -> IO ()
 compileMirJson keepRlib quiet rustFile = do
     let outFile = rustFile -<.> "bin"
 
@@ -103,7 +103,7 @@ compileMirJson keepRlib quiet rustFile = do
             True  -> removeFile outFile
             False -> return ()
 
-maybeCompileMirJson :: Bool -> Bool -> FilePath -> IO ()
+maybeCompileMirJson :: (?defaultRlibsDir :: FilePath) => Bool -> Bool -> FilePath -> IO ()
 maybeCompileMirJson keepRlib quiet rustFile = do
     build <- needsRebuild (mirJsonOutFile rustFile) [rustFile]
     when build $ compileMirJson keepRlib quiet rustFile
@@ -159,7 +159,7 @@ libJsonFiles =
 -- NOTE: If the rust file has not been modified since the
 -- last .mir file was created, this function does nothing
 -- This function uses 'failIO' if any error occurs
-generateMIR :: (HasCallStack, ?debug::Int) =>
+generateMIR :: (HasCallStack, ?debug::Int, ?defaultRlibsDir :: FilePath) =>
                FilePath          -- ^ location of input file
             -> Bool              -- ^ `True` to keep the generated .rlib
             -> IO Collection
diff --git a/crux-mir/src/Mir/Language.hs b/crux-mir/src/Mir/Language.hs
index 39a59342e..335f93463 100644
--- a/crux-mir/src/Mir/Language.hs
+++ b/crux-mir/src/Mir/Language.hs
@@ -133,6 +133,7 @@ runTestsWithExtraOverrides bindExtra (cruxOpts, mirOpts) = do
     --let ?assertFalseOnError = assertFalse mirOpts
     let ?assertFalseOnError = True
     let ?printCrucible      = printCrucible mirOpts
+    let ?defaultRlibsDir    = defaultRlibsDir mirOpts
 
     let (filename, nameFilter) = case cargoTestFile mirOpts of
             -- This case is terrible a hack.  The goal is to mimic the behavior
@@ -346,6 +347,11 @@ data MIROptions = MIROptions
     , printResultOnly :: Bool
     , testFilter   :: Maybe Text
     , cargoTestFile :: Maybe FilePath
+    , defaultRlibsDir :: FilePath
+    -- ^ Directory to search for builds of `crux-mir`'s custom standard
+    -- library, if `$CRUX_RUST_LIBRARY_PATH` is unset.  This option exists for
+    -- the purposes of the `crux-mir-comp` test suite; there's no user-facing
+    -- flag to set it.
     }
 
 defaultMirOptions :: MIROptions
@@ -357,6 +363,7 @@ defaultMirOptions = MIROptions
     , printResultOnly = False
     , testFilter = Nothing
     , cargoTestFile = Nothing
+    , defaultRlibsDir = "rlibs"
     }
 
 mirConfig :: Crux.Config MIROptions

From 607c33c0cfa873b3550acbfe527c5010a3cd4dfc Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 18 Feb 2021 16:01:03 -0800
Subject: [PATCH 12/19] crux-mir: add CTyUnsafeCell pattern

---
 crux-mir/src/Mir/TransTy.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/crux-mir/src/Mir/TransTy.hs b/crux-mir/src/Mir/TransTy.hs
index 24d81dda3..55a9a34fe 100644
--- a/crux-mir/src/Mir/TransTy.hs
+++ b/crux-mir/src/Mir/TransTy.hs
@@ -104,6 +104,10 @@ pattern CTyBox t <- M.TyAdt _ $(M.normDefIdPat "alloc::boxed::Box") (M.Substs [t
   where CTyBox t = M.TyAdt (M.textId "type::adt") (M.textId "alloc::boxed::Box") (M.Substs [t])
 pattern CTyMaybeUninit t <- M.TyAdt _ $(M.normDefIdPat "core::mem::maybe_uninit::MaybeUninit") (M.Substs [t])
   where CTyMaybeUninit t = M.TyAdt (M.textId "type::adt") (M.textId "core::mem::maybe_uninit::MaybeUninit") (M.Substs [t])
+-- `UnsafeCell` isn't handled specially inside baseline `crux-mir`, but
+-- `crux-mir-comp` looks for it (using this pattern synonym).
+pattern CTyUnsafeCell t <- M.TyAdt _ $(M.normDefIdPat "core::cell::UnsafeCell") (M.Substs [t])
+  where CTyUnsafeCell t = M.TyAdt (M.textId "type::adt") (M.textId "core::cell::UnsafeCell") (M.Substs [t])
 pattern CTyVector t <- M.TyAdt _ $(M.normDefIdPat "crucible::vector::Vector") (M.Substs [t])
   where CTyVector t = M.TyAdt (M.textId "type::adt") (M.textId "crucible::vector::Vector") (M.Substs [t])
 pattern CTyArray t <- M.TyAdt _ $(M.normDefIdPat "crucible::array::Array") (M.Substs [t])

From f23e1413b2b3c0c27fd85e6047ab620ce95b6b85 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 18 Feb 2021 17:01:40 -0800
Subject: [PATCH 13/19] update golden test files for line number change

---
 crux-mir/test/symb_eval/concretize/assert.good   |  2 +-
 crux-mir/test/symb_eval/crux/early_fail.good     |  2 +-
 crux-mir/test/symb_eval/crux/fail_return.good    |  4 ++--
 crux-mir/test/symb_eval/crux/mixed_fail.good     |  4 ++--
 crux-mir/test/symb_eval/crux/multi.good          |  4 ++--
 crux-mir/test/symb_eval/crypto/bytes.good        | 10 +++++-----
 crux-mir/test/symb_eval/overrides/override2.good |  2 +-
 crux-mir/test/symb_eval/overrides/override5.good |  2 +-
 crux-mir/test/symb_eval/sym_bytes/construct.good |  2 +-
 9 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/crux-mir/test/symb_eval/concretize/assert.good b/crux-mir/test/symb_eval/concretize/assert.good
index 80a99d497..90708d9a8 100644
--- a/crux-mir/test/symb_eval/concretize/assert.good
+++ b/crux-mir/test/symb_eval/concretize/assert.good
@@ -3,7 +3,7 @@ test assert/3a1fbbbh::crux_test[0]: returned 1, FAILED
 failures:
 
 ---- assert/3a1fbbbh::crux_test[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:44:17: 44:82 !test/symb_eval/concretize/assert.rs:10:5: 10:82: error: in assert/3a1fbbbh::crux_test[0]
+Failure for ./lib/crucible/lib.rs:46:17: 46:82 !test/symb_eval/concretize/assert.rs:10:5: 10:82: error: in assert/3a1fbbbh::crux_test[0]
 MIR assertion at test/symb_eval/concretize/assert.rs:10:5:
 	100 + 157 == 1
 Failure for test/symb_eval/concretize/assert.rs:11:16: 11:17: error: in assert/3a1fbbbh::crux_test[0]
diff --git a/crux-mir/test/symb_eval/crux/early_fail.good b/crux-mir/test/symb_eval/crux/early_fail.good
index 50d9ccaeb..fc02ecf71 100644
--- a/crux-mir/test/symb_eval/crux/early_fail.good
+++ b/crux-mir/test/symb_eval/crux/early_fail.good
@@ -8,7 +8,7 @@ Failure for internal: error: in early_fail/3a1fbbbh::fail1[0]
 panicking::begin_panic, called from early_fail/3a1fbbbh::fail1[0]
 
 ---- early_fail/3a1fbbbh::fail2[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:30: error: in early_fail/3a1fbbbh::fail2[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/early_fail.rs:17:5: 17:30: error: in early_fail/3a1fbbbh::fail2[0]
 MIR assertion at test/symb_eval/crux/early_fail.rs:17:5:
 	x == 0
 
diff --git a/crux-mir/test/symb_eval/crux/fail_return.good b/crux-mir/test/symb_eval/crux/fail_return.good
index a8fe186a4..7a7336bce 100644
--- a/crux-mir/test/symb_eval/crux/fail_return.good
+++ b/crux-mir/test/symb_eval/crux/fail_return.good
@@ -6,14 +6,14 @@ failures:
 ---- fail_return/3a1fbbbh::fail1[0] counterexamples ----
 Failure for test/symb_eval/crux/fail_return.rs:8:22: 8:27: error: in fail_return/3a1fbbbh::fail1[0]
 attempt to add with overflow
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:33: error: in fail_return/3a1fbbbh::fail1[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:8:5: 8:33: error: in fail_return/3a1fbbbh::fail1[0]
 MIR assertion at test/symb_eval/crux/fail_return.rs:8:5:
 	x + 1 > x
 
 ---- fail_return/3a1fbbbh::fail2[0] counterexamples ----
 Failure for test/symb_eval/crux/fail_return.rs:15:22: 15:27: error: in fail_return/3a1fbbbh::fail2[0]
 attempt to add with overflow
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:33: error: in fail_return/3a1fbbbh::fail2[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/fail_return.rs:15:5: 15:33: error: in fail_return/3a1fbbbh::fail2[0]
 MIR assertion at test/symb_eval/crux/fail_return.rs:15:5:
 	x + 1 > x
 
diff --git a/crux-mir/test/symb_eval/crux/mixed_fail.good b/crux-mir/test/symb_eval/crux/mixed_fail.good
index e26fa3c5c..426c9780d 100644
--- a/crux-mir/test/symb_eval/crux/mixed_fail.good
+++ b/crux-mir/test/symb_eval/crux/mixed_fail.good
@@ -8,14 +8,14 @@ failures:
 ---- mixed_fail/3a1fbbbh::fail1[0] counterexamples ----
 Failure for test/symb_eval/crux/mixed_fail.rs:8:22: 8:27: error: in mixed_fail/3a1fbbbh::fail1[0]
 attempt to add with overflow
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:33: error: in mixed_fail/3a1fbbbh::fail1[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:8:5: 8:33: error: in mixed_fail/3a1fbbbh::fail1[0]
 MIR assertion at test/symb_eval/crux/mixed_fail.rs:8:5:
 	x + 1 > x
 
 ---- mixed_fail/3a1fbbbh::fail2[0] counterexamples ----
 Failure for test/symb_eval/crux/mixed_fail.rs:14:22: 14:27: error: in mixed_fail/3a1fbbbh::fail2[0]
 attempt to add with overflow
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:33: error: in mixed_fail/3a1fbbbh::fail2[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/mixed_fail.rs:14:5: 14:33: error: in mixed_fail/3a1fbbbh::fail2[0]
 MIR assertion at test/symb_eval/crux/mixed_fail.rs:14:5:
 	x + 2 > x
 
diff --git a/crux-mir/test/symb_eval/crux/multi.good b/crux-mir/test/symb_eval/crux/multi.good
index 87eab8ce7..9eee3ce47 100644
--- a/crux-mir/test/symb_eval/crux/multi.good
+++ b/crux-mir/test/symb_eval/crux/multi.good
@@ -7,7 +7,7 @@ failures:
 ---- multi/3a1fbbbh::fail1[0] counterexamples ----
 Failure for test/symb_eval/crux/multi.rs:8:22: 8:27: error: in multi/3a1fbbbh::fail1[0]
 attempt to add with overflow
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/multi.rs:8:5: 8:33: error: in multi/3a1fbbbh::fail1[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:8:5: 8:33: error: in multi/3a1fbbbh::fail1[0]
 MIR assertion at test/symb_eval/crux/multi.rs:8:5:
 	x + 1 > x
 
@@ -16,7 +16,7 @@ Failure for internal: error: in multi/3a1fbbbh::fail2[0]
 panicking::begin_panic, called from multi/3a1fbbbh::fail2[0]
 
 ---- multi/3a1fbbbh::fail3[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crux/multi.rs:20:5: 20:30: error: in multi/3a1fbbbh::assert_zero[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crux/multi.rs:20:5: 20:30: error: in multi/3a1fbbbh::assert_zero[0]
 MIR assertion at test/symb_eval/crux/multi.rs:20:5:
 	x == 0
 
diff --git a/crux-mir/test/symb_eval/crypto/bytes.good b/crux-mir/test/symb_eval/crypto/bytes.good
index 859994a22..910370bf1 100644
--- a/crux-mir/test/symb_eval/crypto/bytes.good
+++ b/crux-mir/test/symb_eval/crypto/bytes.good
@@ -3,19 +3,19 @@ test bytes/3a1fbbbh::f[0]: FAILED
 failures:
 
 ---- bytes/3a1fbbbh::f[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 	a[i] == b[i]
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 	a[i] == b[i]
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 	a[i] == b[i]
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 	a[i] == b[i]
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/crypto/bytes.rs:85:7: 85:38: error: in bytes/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/crypto/bytes.rs:85:7:
 	a[i] == b[i]
 
diff --git a/crux-mir/test/symb_eval/overrides/override2.good b/crux-mir/test/symb_eval/overrides/override2.good
index 67c99d966..ad6905592 100644
--- a/crux-mir/test/symb_eval/overrides/override2.good
+++ b/crux-mir/test/symb_eval/overrides/override2.good
@@ -3,7 +3,7 @@ test override2/3a1fbbbh::f[0]: FAILED
 failures:
 
 ---- override2/3a1fbbbh::f[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/overrides/override2.rs:9:5: 9:50: error: in override2/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override2.rs:9:5: 9:50: error: in override2/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/overrides/override2.rs:9:5:
 	foo.wrapping_add(1) == foo
 
diff --git a/crux-mir/test/symb_eval/overrides/override5.good b/crux-mir/test/symb_eval/overrides/override5.good
index 25c1b8c3b..387bcec72 100644
--- a/crux-mir/test/symb_eval/overrides/override5.good
+++ b/crux-mir/test/symb_eval/overrides/override5.good
@@ -3,7 +3,7 @@ test override5/3a1fbbbh::f[0]: FAILED
 failures:
 
 ---- override5/3a1fbbbh::f[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/overrides/override5.rs:10:5: 10:48: error: in override5/3a1fbbbh::f[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/overrides/override5.rs:10:5: 10:48: error: in override5/3a1fbbbh::f[0]
 MIR assertion at test/symb_eval/overrides/override5.rs:10:5:
 	foo.wrapping_add(1) != 0
 
diff --git a/crux-mir/test/symb_eval/sym_bytes/construct.good b/crux-mir/test/symb_eval/sym_bytes/construct.good
index 9e79b415c..9fcf0660d 100644
--- a/crux-mir/test/symb_eval/sym_bytes/construct.good
+++ b/crux-mir/test/symb_eval/sym_bytes/construct.good
@@ -3,7 +3,7 @@ test construct/3a1fbbbh::crux_test[0]: returned Symbolic BV, FAILED
 failures:
 
 ---- construct/3a1fbbbh::crux_test[0] counterexamples ----
-Failure for ./lib/crucible/lib.rs:34:41: 34:58 !test/symb_eval/sym_bytes/construct.rs:13:5: 13:36: error: in construct/3a1fbbbh::crux_test[0]
+Failure for ./lib/crucible/lib.rs:36:41: 36:58 !test/symb_eval/sym_bytes/construct.rs:13:5: 13:36: error: in construct/3a1fbbbh::crux_test[0]
 MIR assertion at test/symb_eval/sym_bytes/construct.rs:13:5:
 	sym2[0] == 0
 

From 529f038b3c762d9739699325ba806c29be76541a Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Mon, 22 Feb 2021 16:27:12 -0800
Subject: [PATCH 14/19] crux-mir: add crucible::method_spec::clobber_globals
 function

---
 crux-mir/lib/crucible/method_spec/mod.rs | 2 ++
 crux-mir/lib/crucible/method_spec/raw.rs | 7 +++++++
 2 files changed, 9 insertions(+)

diff --git a/crux-mir/lib/crucible/method_spec/mod.rs b/crux-mir/lib/crucible/method_spec/mod.rs
index 2a88919d3..7518af18b 100644
--- a/crux-mir/lib/crucible/method_spec/mod.rs
+++ b/crux-mir/lib/crucible/method_spec/mod.rs
@@ -8,6 +8,8 @@ use core::fmt;
 
 mod raw;
 
+pub use self::raw::clobber_globals;
+
 
 /// The specification of a function.  This can be used when verifying callers of the function to
 /// avoid simulating the entire function itself.
diff --git a/crux-mir/lib/crucible/method_spec/raw.rs b/crux-mir/lib/crucible/method_spec/raw.rs
index e000004aa..29b36a5dd 100644
--- a/crux-mir/lib/crucible/method_spec/raw.rs
+++ b/crux-mir/lib/crucible/method_spec/raw.rs
@@ -55,3 +55,10 @@ pub fn builder_finish(msb: MethodSpecBuilder) -> MethodSpec {
     let _ = msb;
     MethodSpec(0)
 }
+
+
+/// Replace all mutable global data with arbitrary values.  This is used at the start of tests to
+/// ensure that the property holds in any context.
+pub fn clobber_globals() {
+    unimplemented!("MethodSpecBuilder is not supported on this version of crux-mir")
+}

From 42f151e7e40f0f87139c54f7234a145b480c5af2 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Tue, 23 Feb 2021 13:53:23 -0800
Subject: [PATCH 15/19] Mir.Intrinsics: add mirRef_overlaps

---
 crux-mir/src/Mir/Intrinsics.hs | 129 +++++++++++++++++++++++++++++++++
 1 file changed, 129 insertions(+)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index 615bcc832..894a1e2c6 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1252,6 +1252,7 @@ mirRef_arrayAsMirVectorLeaf sym _ (MirReference_Integer _ _) =
     leafAbort sym $ GenericSimError $
         "attempted Array->MirVector conversion on the result of an integer-to-pointer cast"
 
+
 refRootEq :: IsSymInterface sym => sym ->
     MirReferenceRoot sym tp1 -> MirReferenceRoot sym tp2 ->
     MuxLeafT sym IO (RegValue sym BoolType)
@@ -1305,6 +1306,134 @@ mirRef_eqIO :: IsSymInterface sym => sym ->
 mirRef_eqIO sym (MirReferenceMux r1) (MirReferenceMux r2) =
     zipFancyMuxTrees' sym (mirRef_eqLeaf sym) (itePred sym) r1 r2
 
+
+-- | An ordinary `MirReferencePath sym tp tp''` is represented "inside-out": to
+-- turn `tp` into `tp''`, we first use a subsidiary `MirReferencePath` to turn
+-- `tp` into `tp'`, then perform one last step to turn `tp'` into `tp''`.
+-- `ReversedRefPath` is represented "outside-in", so the first/outermost
+-- element is the first step of the conversion, not the last.
+data ReversedRefPath sym :: CrucibleType -> CrucibleType -> Type where
+  RrpNil :: forall sym tp. ReversedRefPath sym tp tp
+  RrpCons :: forall sym tp tp' tp''.
+    -- | The first step of the path.  For all cases but Empty_RefPath, the
+    -- nested initial MirReferencePath is always Empty_RefPath.
+    MirReferencePath sym tp tp' ->
+    ReversedRefPath sym tp' tp'' ->
+    ReversedRefPath sym tp tp''
+
+reverseRefPath :: forall sym tp tp'.
+    MirReferencePath sym tp tp' ->
+    ReversedRefPath sym tp tp'
+reverseRefPath rp = go RrpNil rp
+  where
+    go :: forall sym tp tp' tp''.
+        ReversedRefPath sym tp' tp'' ->
+        MirReferencePath sym tp tp' ->
+        ReversedRefPath sym tp tp''
+    go acc Empty_RefPath = acc
+    go acc (Field_RefPath ctx rp idx) =
+        go (Field_RefPath ctx Empty_RefPath idx `RrpCons` acc) rp
+    go acc (Variant_RefPath ctx rp idx) =
+        go (Variant_RefPath ctx Empty_RefPath idx `RrpCons` acc) rp
+    go acc (Index_RefPath tpr rp idx) =
+        go (Index_RefPath tpr Empty_RefPath idx `RrpCons` acc) rp
+    go acc (Just_RefPath tpr rp) =
+        go (Just_RefPath tpr Empty_RefPath `RrpCons` acc) rp
+    go acc (VectorAsMirVector_RefPath tpr rp) =
+        go (VectorAsMirVector_RefPath tpr Empty_RefPath `RrpCons` acc) rp
+    go acc (ArrayAsMirVector_RefPath tpr rp) =
+        go (ArrayAsMirVector_RefPath tpr Empty_RefPath `RrpCons` acc) rp
+
+-- | If the final step of `path` is an `Index_RefPath`, remove it.  Otherwise,
+-- return `path` unchanged.
+popIndex :: MirReferencePath sym tp tp' -> Some (MirReferencePath sym tp)
+popIndex (Index_RefPath _ p _) = Some p
+popIndex p = Some p
+
+
+refRootOverlaps :: IsSymInterface sym => sym ->
+    MirReferenceRoot sym tp1 -> MirReferenceRoot sym tp2 ->
+    MuxLeafT sym IO (RegValue sym BoolType)
+refRootOverlaps sym (RefCell_RefRoot rc1) (RefCell_RefRoot rc2)
+  | Just Refl <- testEquality rc1 rc2 = return $ truePred sym
+refRootOverlaps sym (GlobalVar_RefRoot gv1) (GlobalVar_RefRoot gv2)
+  | Just Refl <- testEquality gv1 gv2 = return $ truePred sym
+refRootOverlaps sym (Const_RefRoot _ _) (Const_RefRoot _ _) =
+    leafAbort sym $ Unsupported $ "Cannot compare Const_RefRoots"
+refRootOverlaps sym _ _ = return $ falsePred sym
+
+-- | Check whether two `MirReferencePath`s might reference overlapping memory
+-- regions, when starting from the same `MirReferenceRoot`.
+refPathOverlaps :: forall sym tp_base1 tp1 tp_base2 tp2. IsSymInterface sym =>
+    sym ->
+    MirReferencePath sym tp_base1 tp1 ->
+    MirReferencePath sym tp_base2 tp2 ->
+    MuxLeafT sym IO (RegValue sym BoolType)
+refPathOverlaps sym path1 path2 = do
+    -- We remove the outermost `Index` before comparing, since `offset` allows
+    -- modifying the index value arbitrarily, giving access to all elements of
+    -- the containing vector.
+    Some path1' <- return $ popIndex path1
+    Some path2' <- return $ popIndex path2
+    -- Essentially, this checks whether `rrp1` is a prefix of `rrp2` or vice
+    -- versa.
+    go (reverseRefPath path1') (reverseRefPath path2')
+  where
+    go :: forall tp1 tp1' tp2 tp2'.
+        ReversedRefPath sym tp1 tp1' ->
+        ReversedRefPath sym tp2 tp2' ->
+        MuxLeafT sym IO (RegValue sym BoolType)
+    -- An empty RefPath (`RrpNil`) covers the whole object, so it overlaps with
+    -- all other paths into the same object.
+    go RrpNil _ = return $ truePred sym
+    go _ RrpNil = return $ truePred sym
+    go (Empty_RefPath `RrpCons` rrp1) rrp2 = go rrp1 rrp2
+    go rrp1 (Empty_RefPath `RrpCons` rrp2) = go rrp1 rrp2
+    -- If two `Any_RefPath`s have different `tpr`s, then we assume they don't
+    -- overlap, since applying both to the same root will cause at least one to
+    -- give a type mismatch error.
+    go (Any_RefPath tpr1 _ `RrpCons` rrp1) (Any_RefPath tpr2 _ `RrpCons` rrp2)
+      | Just Refl <- testEquality tpr1 tpr2 = go rrp1 rrp2
+    go (Field_RefPath ctx1 _ idx1 `RrpCons` rrp1) (Field_RefPath ctx2 _ idx2 `RrpCons` rrp2)
+      | Just Refl <- testEquality ctx1 ctx2
+      , Just Refl <- testEquality idx1 idx2 = go rrp1 rrp2
+    go (Variant_RefPath ctx1 _ idx1 `RrpCons` rrp1) (Variant_RefPath ctx2 _ idx2 `RrpCons` rrp2)
+      | Just Refl <- testEquality ctx1 ctx2
+      , Just Refl <- testEquality idx1 idx2 = go rrp1 rrp2
+    go (Index_RefPath tpr1 _ idx1 `RrpCons` rrp1) (Index_RefPath tpr2 _ idx2 `RrpCons` rrp2)
+      | Just Refl <- testEquality tpr1 tpr2 = do
+        rrpEq <- go rrp1 rrp2
+        idxEq <- liftIO $ bvEq sym idx1 idx2
+        liftIO $ andPred sym rrpEq idxEq
+    go (Just_RefPath tpr1 _ `RrpCons` rrp1) (Just_RefPath tpr2 _ `RrpCons` rrp2)
+      | Just Refl <- testEquality tpr1 tpr2 = go rrp1 rrp2
+    go (VectorAsMirVector_RefPath tpr1 _ `RrpCons` rrp1)
+        (VectorAsMirVector_RefPath tpr2 _ `RrpCons` rrp2)
+      | Just Refl <- testEquality tpr1 tpr2 = go rrp1 rrp2
+    go (ArrayAsMirVector_RefPath tpr1 _ `RrpCons` rrp1)
+        (ArrayAsMirVector_RefPath tpr2 _ `RrpCons` rrp2)
+      | Just Refl <- testEquality tpr1 tpr2 = go rrp1 rrp2
+    go _ _ = return $ falsePred sym
+
+-- | Check whether the memory accessible through `ref1` overlaps the memory
+-- accessible through `ref2`.
+mirRef_overlapsLeaf :: IsSymInterface sym => sym ->
+    MirReference sym tp -> MirReference sym tp -> MuxLeafT sym IO (RegValue sym BoolType)
+mirRef_overlapsLeaf sym (MirReference root1 path1) (MirReference root2 path2) = do
+    rootOverlaps <- refRootOverlaps sym root1 root2
+    pathOverlaps <- refPathOverlaps sym path1 path2
+    liftIO $ andPred sym rootOverlaps pathOverlaps
+-- No memory is accessible through an integer reference, so they can't overlap
+-- with anything.
+mirRef_overlapsLeaf sym (MirReference_Integer _ _) _ = return $ falsePred sym
+mirRef_overlapsLeaf sym _ (MirReference_Integer _ _) = return $ falsePred sym
+
+mirRef_overlapsIO :: IsSymInterface sym => sym ->
+    MirReferenceMux sym tp -> MirReferenceMux sym tp -> IO (RegValue sym BoolType)
+mirRef_overlapsIO sym (MirReferenceMux r1) (MirReferenceMux r2) =
+    zipFancyMuxTrees' sym (mirRef_overlapsLeaf sym) (itePred sym) r1 r2
+
+
 mirRef_offsetLeaf :: IsSymInterface sym => sym ->
     TypeRepr tp -> MirReference sym tp -> RegValue sym IsizeType ->
     MuxLeafT sym IO (MirReference sym tp)

From d29d5aa30988cadd52961286e7268f277bea5050 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Wed, 24 Feb 2021 09:52:27 -0800
Subject: [PATCH 16/19] minor improvements to mirRef_overlaps

---
 crux-mir/src/Mir/Intrinsics.hs | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index 894a1e2c6..a55874d9a 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1418,18 +1418,21 @@ refPathOverlaps sym path1 path2 = do
 -- | Check whether the memory accessible through `ref1` overlaps the memory
 -- accessible through `ref2`.
 mirRef_overlapsLeaf :: IsSymInterface sym => sym ->
-    MirReference sym tp -> MirReference sym tp -> MuxLeafT sym IO (RegValue sym BoolType)
+    MirReference sym tp -> MirReference sym tp' -> MuxLeafT sym IO (RegValue sym BoolType)
 mirRef_overlapsLeaf sym (MirReference root1 path1) (MirReference root2 path2) = do
     rootOverlaps <- refRootOverlaps sym root1 root2
-    pathOverlaps <- refPathOverlaps sym path1 path2
-    liftIO $ andPred sym rootOverlaps pathOverlaps
+    case asConstantPred rootOverlaps of
+        Just False -> return $ falsePred sym
+        _ -> do
+            pathOverlaps <- refPathOverlaps sym path1 path2
+            liftIO $ andPred sym rootOverlaps pathOverlaps
 -- No memory is accessible through an integer reference, so they can't overlap
 -- with anything.
 mirRef_overlapsLeaf sym (MirReference_Integer _ _) _ = return $ falsePred sym
 mirRef_overlapsLeaf sym _ (MirReference_Integer _ _) = return $ falsePred sym
 
 mirRef_overlapsIO :: IsSymInterface sym => sym ->
-    MirReferenceMux sym tp -> MirReferenceMux sym tp -> IO (RegValue sym BoolType)
+    MirReferenceMux sym tp -> MirReferenceMux sym tp' -> IO (RegValue sym BoolType)
 mirRef_overlapsIO sym (MirReferenceMux r1) (MirReferenceMux r2) =
     zipFancyMuxTrees' sym (mirRef_overlapsLeaf sym) (itePred sym) r1 r2
 

From 155fa0fa971f0c414708ea74037ecc1b60001f24 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 25 Feb 2021 15:53:34 -0800
Subject: [PATCH 17/19] more doc comments explaining the crux-mir/crux-mir-comp
 split

---
 crux-mir/lib/crucible/method_spec/raw.rs | 9 +++++++++
 crux-mir/src/Mir/Intrinsics.hs           | 7 ++++---
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/crux-mir/lib/crucible/method_spec/raw.rs b/crux-mir/lib/crucible/method_spec/raw.rs
index 29b36a5dd..eb29435b5 100644
--- a/crux-mir/lib/crucible/method_spec/raw.rs
+++ b/crux-mir/lib/crucible/method_spec/raw.rs
@@ -1,3 +1,12 @@
+//! Bindings for low-level MethodSpec APIs.
+//!
+//! Like most functions in the `crucible` crate, these functions are left unimplemented in Rust
+//! and are replaced by a real implementation via the Crucible override mechanism.  However, unlike
+//! most other functions, the necessary overrides are not provided by `crux-mir`; instead, they are
+//! provided by the `crux-mir-comp` package in the `saw-script` repository, which extends ordinary
+//! `crux-mir` with additional overrides using `crux-mir`'s new `mainWithExtraOverrides` entry
+//! point.  Trying to use these APIs under ordinary `crux-mir` will produce an error.
+
 /// Crucible `MethodSpecType`, exposed to Rust.
 ///
 /// As usual for Crucible types, this implements `Copy`, since it's backed by a boxed,
diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index a55874d9a..a7c1bb18e 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1885,9 +1885,10 @@ getSliceLen e = getStruct i2of2 e
 -- ** MethodSpec and MethodSpecBuilder
 --
 -- We define the intrinsics here so they can be used in `TransTy.tyToRepr`, and
--- also define their interfaces (as typeclasses), but the concrete
--- implementations of these types are in `saw-script/crux-mir-comp`, since they
--- depend on some SAW components (notably SAW's `MethodSpec` and `Term` types).
+-- also define their interfaces (as typeclasses), but we don't provide any
+-- concrete implementations in `crux-mir`.  Instead, implementations of these
+-- types are in `saw-script/crux-mir-comp`, since they depend on some SAW
+-- components, such as `saw-script`'s `MethodSpec`.
 
 class MethodSpecImpl sym ms where
     -- | Pretty-print the MethodSpec, returning the result as a Rust string

From 44c8aeb29adafb9112a54e43224422721aeede56 Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Thu, 25 Feb 2021 15:53:41 -0800
Subject: [PATCH 18/19] add mirRef_indexAndLenSim

---
 crux-mir/src/Mir/Intrinsics.hs | 53 ++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index a7c1bb18e..1a6e74347 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1505,6 +1505,59 @@ mirRef_peelIndexIO sym _ _ = do
     leafAbort sym $ Unsupported $
         "cannot perform peelIndex on invalid pointer"
 
+-- | Compute the index of `ref` within its containing allocation, along with
+-- the length of that allocation.  This is useful for determining the amount of
+-- memory accessible through all valid offsets of `ref`.
+--
+-- Unlike `peelIndex`, this operation is valid on non-`Index_RefPath`
+-- references (on which it returns `(0, 1)`) and also on `MirReference_Integer`
+-- (returning `(0, 0)`).
+mirRef_indexAndLenLeaf :: IsSymInterface sym =>
+    sym -> SimState p sym ext rtp f a ->
+    MirReference sym tp ->
+    MuxLeafT sym IO (RegValue sym UsizeType, RegValue sym UsizeType)
+mirRef_indexAndLenLeaf sym s (MirReference root (Index_RefPath _tpr' path idx)) = do
+    let parent = MirReference root path
+    parentVec <- readMirRefLeaf s sym parent
+    lenInt <- case parentVec of
+        MirVector_Vector v -> return $ V.length v
+        MirVector_PartialVector pv -> return $ V.length pv
+        MirVector_Array _ -> leafAbort sym $ Unsupported $
+            "can't compute allocation length for MirVector_Array, which is unbounded"
+    len <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral lenInt
+    return (idx, len)
+mirRef_indexAndLenLeaf sym _ (MirReference _ _) = do
+    idx <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat 0
+    len <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat 1
+    return (idx, len)
+mirRef_indexAndLenLeaf sym _ (MirReference_Integer _ _) = do
+    -- No offset of `MirReference_Integer` is dereferenceable, so `len` is
+    -- zero.
+    zero <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat 0
+    return (zero, zero)
+
+mirRef_indexAndLenIO :: IsSymInterface sym =>
+    sym -> SimState p sym ext rtp f a ->
+    MirReferenceMux sym tp ->
+    IO (PartExpr (Pred sym) (RegValue sym UsizeType, RegValue sym UsizeType))
+mirRef_indexAndLenIO sym s (MirReferenceMux ref) = do
+    readPartialFancyMuxTree sym
+        (mirRef_indexAndLenLeaf sym s)
+        (\c (tIdx, tLen) (eIdx, eLen) -> do
+            idx <- baseTypeIte sym c tIdx eIdx
+            len <- baseTypeIte sym c tLen eLen
+            return (idx, len))
+        ref
+
+mirRef_indexAndLenSim :: IsSymInterface sym =>
+    MirReferenceMux sym tp ->
+    OverrideSim (Model sym) sym MIR rtp args ret
+        (PartExpr (Pred sym) (RegValue sym UsizeType, RegValue sym UsizeType))
+mirRef_indexAndLenSim ref = do
+    sym <- getSymInterface
+    s <- get
+    liftIO $ mirRef_indexAndLenIO sym s ref
+
 
 execMirStmt :: forall p sym. IsSymInterface sym => EvalStmtFunc p sym MIR
 execMirStmt stmt s =

From c6b5472d33dc2f5f7c8dc449a0ea13113943fd2d Mon Sep 17 00:00:00 2001
From: Stuart Pernsteiner <spernsteiner@galois.com>
Date: Fri, 26 Feb 2021 13:18:34 -0800
Subject: [PATCH 19/19] don't require Crux.Model personality for
 mirRef_indexAndLenSim

---
 crux-mir/src/Mir/Intrinsics.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crux-mir/src/Mir/Intrinsics.hs b/crux-mir/src/Mir/Intrinsics.hs
index 1a6e74347..6f6b17487 100644
--- a/crux-mir/src/Mir/Intrinsics.hs
+++ b/crux-mir/src/Mir/Intrinsics.hs
@@ -1551,7 +1551,7 @@ mirRef_indexAndLenIO sym s (MirReferenceMux ref) = do
 
 mirRef_indexAndLenSim :: IsSymInterface sym =>
     MirReferenceMux sym tp ->
-    OverrideSim (Model sym) sym MIR rtp args ret
+    OverrideSim p sym MIR rtp args ret
         (PartExpr (Pred sym) (RegValue sym UsizeType, RegValue sym UsizeType))
 mirRef_indexAndLenSim ref = do
     sym <- getSymInterface