Skip to content

Commit a7855cf

Browse files
authored
Merge pull request #2689 from GaloisInc/T2687-fix-traverseMirAggregate-bug
`traverseMirAggregate`: Add a special case for empty `MirAggregate`s
2 parents 731c648 + fe303c4 commit a7855cf

File tree

3 files changed

+62
-3
lines changed

3 files changed

+62
-3
lines changed
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
test clobber_globals_closure/<DISAMB>::foo_equiv[0]: ok
2+
3+
[Crux] Overall status: Valid.
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// A regression test for #2687. rustc will promote the closure used in the body
2+
// of the mk_closure() function to a static item, which means that the value
3+
// of this static will be clobbered as part of proving foo_equiv(). Because
4+
// this closure does not capture any variables, it is represented as an empty
5+
// MirAggregate in crucible-mir. There was a subtle bug involving mistreatment
6+
// of empty MirAggregates that #2687 uncovered, and this test case aims to
7+
// ensure that this bug remains fixed.
8+
9+
extern crate crucible;
10+
extern crate crucible_proc_macros;
11+
use crucible::crucible_assert;
12+
use crucible_proc_macros::crux_spec_for;
13+
14+
// The closure must be promoted to get 'static lifetime
15+
fn mk_closure() -> &'static impl Fn() -> u32 {
16+
&|| 42u32
17+
}
18+
19+
pub fn foo() -> u32 {
20+
mk_closure()()
21+
}
22+
23+
#[crux_spec_for(foo)]
24+
pub fn foo_equiv() {
25+
let expected = 42u32;
26+
let actual = foo();
27+
crucible_assert!(expected == actual);
28+
}

saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs

Lines changed: 31 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -454,7 +454,7 @@ shapeToTerm' sc = go
454454
ty <- go sub shp
455455
liftIO (mkVec n ty)
456456
go (AdaptDerefSlice col n ada) (SliceShape _ elT M.Immut tpr) =
457-
do et <- go ada (tyToShapeEq col elT tpr)
457+
do et <- go ada (tyToShapeEq col elT tpr)
458458
liftIO (mkVec n et)
459459
go _ada shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp)
460460

@@ -568,6 +568,7 @@ buildMirAggregate sym elems xs f = do
568568
-- offset, size, type, and value of the entry, and its result is stored as the
569569
-- new value in the output.
570570
traverseMirAggregate ::
571+
forall sym m.
571572
(IsSymInterface sym, Monad m, MonadFail m, MonadIO m) =>
572573
sym ->
573574
[AgElemShape] ->
@@ -576,7 +577,35 @@ traverseMirAggregate ::
576577
m (MirAggregate sym)
577578
traverseMirAggregate sym elems (MirAggregate totalSize m) f = do
578579
agCheckKeysEq "traverseMirAggregate" elems m
579-
m' <- sequence $ IntMap.mergeWithKey
580+
m' <-
581+
-- Hack: we include a special case for when the list of AgElemShapes and
582+
-- the MirAggregate are both empty, skipping the call to mergeEntries
583+
-- entirely if this is the case. This is because mergeEntries calls
584+
-- IntMap.mergeWithKey under the hood, and prior to containers-0.8, the
585+
-- implementation of IntMap.mergeWithKey had a bug where merging two empty
586+
-- IntMaps would invoke the third callback argument instead of just
587+
-- returning an empty map. (See
588+
-- https://github.com/haskell/containers/issues/979.) Note that
589+
-- mergeEntries uses the third callback argument to panic, however, and we
590+
-- definitely don't want to panic if the IntMaps are both empty!
591+
--
592+
-- Because SAW still supports GHC versions that bundle versions of
593+
-- containers that are older than 0.8 (and therefore do not contain a fix
594+
-- for the issue above), we include this special case as a workaround. Once
595+
-- SAW drops support for pre-0.8 versions of containers, we can remove this
596+
-- special case.
597+
if null elems && IntMap.null m
598+
then pure IntMap.empty
599+
else mergeEntries
600+
return $ MirAggregate totalSize m'
601+
where
602+
-- Merge the existing MirAggregate's entries together with the new entries
603+
-- from the list of AgElemShapes.
604+
--
605+
-- Precondition: both the list of AgElemShapes and the MirAggregate are
606+
-- non-empty (see the comments above near mergeEntries' call site).
607+
mergeEntries :: m (IntMap (MirAggregateEntry sym))
608+
mergeEntries = sequence $ IntMap.mergeWithKey
580609
(\_off' (AgElemShape off _sz' shp) (MirAggregateEntry sz tpr rvPart) -> Just $ do
581610
Refl <- case testEquality tpr (shapeType shp) of
582611
Just pf -> return pf
@@ -590,7 +619,6 @@ traverseMirAggregate sym elems (MirAggregate totalSize m) f = do
590619
(\_ -> panic "traverseMirAggregate" ["mismatched keys in aggregate"])
591620
(IntMap.fromList [(fromIntegral off, e) | e@(AgElemShape off _ _) <- elems])
592621
m
593-
return $ MirAggregate totalSize m'
594622

595623
-- | Extract values from a `MirAggregate`, one for each entry. The callback
596624
-- gets the offset, size, type, and value of the entry. Callback results are

0 commit comments

Comments
 (0)