Skip to content

Commit c2ad086

Browse files
brianhuffmanbrianhuffman
authored
Merge pull request #2470 from GaloisInc/bh/intmap
Use IntMap instead of Map VarIndex for term substitution maps.
2 parents e7af9a6 + 89e66d0 commit c2ad086

File tree

16 files changed

+84
-69
lines changed

16 files changed

+84
-69
lines changed

‎crucible-mir-comp/src/Mir/Compositional/Builder.hs‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,9 @@ import Control.Monad.State
2020
import qualified Data.BitVector.Sized as BV
2121
import Data.Foldable
2222
import Data.Functor.Const
23+
import Data.IntMap (IntMap)
24+
import qualified Data.IntMap as IntMap
2325
import Data.IORef
24-
import Data.Map (Map)
2526
import qualified Data.Map as Map
2627
import Data.Parameterized.Context (pattern Empty, pattern (:>), Assignment)
2728
import Data.Parameterized.Nonce
@@ -576,20 +577,20 @@ finish msb =
576577
buildSubstMap ::
577578
SAW.SharedContext ->
578579
[(SAW.ExtCns SAW.Term, SAW.Term)] ->
579-
IO (Map SAW.VarIndex SAW.Term)
580-
buildSubstMap sc substs0 = go Map.empty substs0
580+
IO (IntMap SAW.Term)
581+
buildSubstMap sc substs0 = go IntMap.empty substs0
581582
where
582583
go sm [] = return sm
583584
go sm ((ec, term) : substs) = do
584585
-- Rewrite the RHSs of previous substitutions using the current one.
585-
let sm1 = Map.singleton (SAW.ecVarIndex ec) term
586+
let sm1 = IntMap.singleton (SAW.ecVarIndex ec) term
586587
sm' <- mapM (SAW.scInstantiateExt sc sm1) sm
587588
-- Add the current subst and continue.
588-
go (Map.insert (SAW.ecVarIndex ec) term sm') substs
589+
go (IntMap.insert (SAW.ecVarIndex ec) term sm') substs
589590

590591
substMethodSpec ::
591592
SAW.SharedContext ->
592-
Map SAW.VarIndex SAW.Term ->
593+
IntMap SAW.Term ->
593594
MIRMethodSpec ->
594595
IO MIRMethodSpec
595596
substMethodSpec sc sm ms = do
@@ -608,7 +609,7 @@ substMethodSpec sc sm ms = do
608609
pointsTos' <- mapM goPointsTo $ ss ^. MS.csPointsTos
609610
conditions' <- mapM goSetupCondition $ ss ^. MS.csConditions
610611
let freshVars' =
611-
filter (\tec -> not $ Map.member (SAW.ecVarIndex $ SAW.tecExt tec) sm) $
612+
filter (\tec -> not $ IntMap.member (SAW.ecVarIndex $ SAW.tecExt tec) sm) $
612613
ss ^. MS.csFreshVars
613614
return $ ss
614615
& MS.csPointsTos .~ pointsTos'

‎crucible-mir-comp/src/Mir/Compositional/Override.hs‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ import Control.Monad.State
2222
import qualified Data.BitVector.Sized as BV
2323
import qualified Data.ByteString as BS
2424
import Data.Foldable
25+
import Data.IntMap (IntMap)
26+
import qualified Data.IntMap as IntMap
2527
import Data.IORef
2628
import Data.Map (Map)
2729
import qualified Data.Map as Map
@@ -162,7 +164,7 @@ runSpec myCS mh ms = ovrWithBackend $ \bak ->
162164
-- so we don't need to split up our `runOverrideMatcher` call into multiple
163165
-- blocks.
164166
let postFresh = ms ^. MS.csPostState . MS.csFreshVars
165-
postFreshTermSub <- liftM Map.fromList $ forM postFresh $ \tec -> do
167+
postFreshTermSub <- liftM IntMap.fromList $ forM postFresh $ \tec -> do
166168
let ec = SAW.tecExt tec
167169
let nameStr = Text.unpack $ SAW.toShortName $ SAW.ecName ec
168170
let nameSymbol = W4.safeSymbol nameStr
@@ -234,7 +236,7 @@ runSpec myCS mh ms = ovrWithBackend $ \bak ->
234236
ms ^. MS.csPostState . MS.csFreshVars
235237
forM_ allFresh $ \tec -> do
236238
let var = SAW.ecVarIndex $ SAW.tecExt tec
237-
when (not $ Map.member var termSub) $ do
239+
when (not $ IntMap.member var termSub) $ do
238240
error $ "argument matching failed to produce a binding for " ++
239241
show (SAW.ppTypedExtCns tec)
240242

@@ -367,9 +369,9 @@ matchArg sym sc eval allocSpecs md shp0 rv0 sv0 = go shp0 rv0 sv0
367369
Just ec -> do
368370
let var = SAW.ecVarIndex ec
369371
sub <- use MS.termSub
370-
when (Map.member var sub) $
372+
when (IntMap.member var sub) $
371373
MS.failure loc MS.NonlinearPatternNotSupported
372-
MS.termSub %= Map.insert var exprTerm
374+
MS.termSub %= IntMap.insert var exprTerm
373375
Nothing -> do
374376
-- If the `TypedTerm` is a constant, we want to assert that the
375377
-- argument `expr` matches the constant.
@@ -504,7 +506,7 @@ setupToReg :: forall sym t st fs tp0.
504506
SAW.SharedContext ->
505507
-- | `termSub`: maps `VarIndex`es in the MethodSpec's namespace to `Term`s
506508
-- in the context's namespace.
507-
Map SAW.VarIndex SAW.Term ->
509+
IntMap SAW.Term ->
508510
-- | `myRegMap`: maps `VarIndex`es in the context's namespace to the
509511
-- corresponding W4 variables in the context's namespace.
510512
Map SAW.VarIndex (Some (W4.Expr t)) ->

‎saw-central/src/SAWCentral/Bisimulation.hs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ import Control.Monad.IO.Class (MonadIO(..))
7979
import qualified Control.Monad.State.Strict as State
8080
import Control.Monad.Trans.Class (MonadTrans(..))
8181
import Data.Foldable (foldl')
82+
import qualified Data.IntMap as IntMap
8283
import qualified Data.IntSet as IntSet
8384
import qualified Data.Map.Strict as Map
8485
import Data.Maybe (mapMaybe)
@@ -222,8 +223,8 @@ buildCompositionSideCondition bc innerBt = do
222223
rhsTuple <- io $ scTuple sc [rhsOuterState, input] -- (f_rhs_s, in)
223224
innerRel' <- io $
224225
scInstantiateExt sc
225-
(Map.fromList [ (ecVarIndex lhsInnerEc, lhsTuple)
226-
, (ecVarIndex rhsInnerEc, rhsTuple)])
226+
(IntMap.fromList [ (ecVarIndex lhsInnerEc, lhsTuple)
227+
, (ecVarIndex rhsInnerEc, rhsTuple)])
227228
innerRel
228229

229230
-- outer state relation implies inner state relation

‎saw-central/src/SAWCentral/Builtins.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1752,7 +1752,7 @@ cexEvalFn sc args tm = do
17521752
let exts = map fst args
17531753
args' <- mapM (scFirstOrderValue sc . snd) args
17541754
let is = map ecVarIndex exts
1755-
argMap = Map.fromList (zip is args')
1755+
argMap = IntMap.fromList (zip is args')
17561756

17571757
-- TODO, instead of instantiating and then evaluating, we should
17581758
-- evaluate in the context of an EC map instead. argMap is almost

‎saw-central/src/SAWCentral/Crucible/Common/Override.hs‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,8 @@ import qualified Control.Monad.Fail as Fail
8989
import Control.Monad.Trans.Except
9090
import Control.Monad.Trans.Class
9191
import Control.Monad.IO.Class
92+
import qualified Data.IntMap as IntMap
93+
import Data.IntMap (IntMap)
9294
import qualified Data.Map as Map
9395
import Data.Map (Map)
9496
import Data.Maybe (fromMaybe)
@@ -147,8 +149,8 @@ data OverrideState' sym ext = OverrideState
147149
{ -- | Substitution for memory allocations
148150
_setupValueSub :: Map AllocIndex (MS.Pointer' ext sym)
149151

150-
-- | Substitution for SAW Core external constants
151-
, _termSub :: Map VarIndex Term
152+
-- | Substitution for SAW Core external constants, keyed by 'VarIndex'
153+
, _termSub :: IntMap Term
152154

153155
-- | Equalities of SAW Core terms. The four elements of each tuple are:
154156
--
@@ -193,7 +195,7 @@ initialState ::
193195
sym {- ^ simulator -} ->
194196
Crucible.SymGlobalState sym {- ^ initial global variables -} ->
195197
Map AllocIndex (Pointer' ext sym) {- ^ initial allocation substituion -} ->
196-
Map VarIndex Term {- ^ initial term substituion -} ->
198+
IntMap Term {- ^ initial term substitution -} ->
197199
Set VarIndex {- ^ initial free terms -} ->
198200
W4.ProgramLoc {- ^ location information for the override -} ->
199201
OverrideState' sym ext
@@ -433,7 +435,7 @@ runOverrideMatcher ::
433435
sym {- ^ simulator -} ->
434436
Crucible.SymGlobalState sym {- ^ initial global variables -} ->
435437
Map AllocIndex (Pointer' ext sym) {- ^ initial allocation substitution -} ->
436-
Map VarIndex Term {- ^ initial term substitution -} ->
438+
IntMap Term {- ^ initial term substitution -} ->
437439
Set VarIndex {- ^ initial free variables -} ->
438440
W4.ProgramLoc {- ^ override location information -} ->
439441
OverrideMatcher' sym ext md m a {- ^ matching action -} ->
@@ -531,7 +533,7 @@ enforceCompleteSubstitution loc ss =
531533

532534
let -- predicate matches terms that are not covered by the computed
533535
-- term substitution
534-
isMissing tt = ecVarIndex (tecExt tt) `Map.notMember` sub
536+
isMissing tt = ecVarIndex (tecExt tt) `IntMap.notMember` sub
535537

536538
-- list of all terms not covered by substitution
537539
missing = filter isMissing (view MS.csFreshVars ss)
@@ -545,8 +547,8 @@ refreshTerms ::
545547
MS.StateSpec ext {- ^ current phase spec -} ->
546548
OverrideMatcher ext w ()
547549
refreshTerms sc ss =
548-
do extension <- Map.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
549-
OM (termSub %= Map.union extension)
550+
do extension <- IntMap.fromList <$> traverse freshenTerm (view MS.csFreshVars ss)
551+
OM (termSub %= IntMap.union extension)
550552
where
551553
freshenTerm (TypedExtCns _cty ec) =
552554
do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec)

‎saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ import Control.Monad.Trans.Except (runExceptT)
6161
import qualified Data.BitVector.Sized as BV
6262
import Data.Foldable (for_)
6363
import Data.Function
64+
import qualified Data.IntMap as IntMap
6465
import Data.IORef
6566
import Data.List (isPrefixOf, sortBy)
6667
import Data.List.NonEmpty (NonEmpty)
@@ -785,7 +786,7 @@ verifyPoststate cc mspec env0 globals ret mdMap =
785786
skipSafetyProofs <- gets rwSkipSafetyProofs
786787
when skipSafetyProofs (io (Crucible.clearProofObligations bak))
787788

788-
let ecs0 = Map.fromList
789+
let ecs0 = IntMap.fromList
789790
[ (ecVarIndex ec, ec)
790791
| tt <- mspec ^. MS.csPreState . MS.csFreshVars
791792
, let ec = tecExt tt ]

‎saw-central/src/SAWCentral/Crucible/JVM/Override.hs‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,11 +58,12 @@ import Control.Monad.IO.Class (liftIO)
5858
import Control.Monad
5959
import Data.Either (partitionEithers)
6060
import Data.Foldable (for_, traverse_)
61+
import Data.IntMap (IntMap)
62+
import qualified Data.IntMap as IntMap
6163
import Data.IORef
6264
import Data.List (tails)
6365
import Data.List.NonEmpty (NonEmpty)
6466
import qualified Data.List.NonEmpty as NE
65-
import Data.Map (Map)
6667
import qualified Data.Map as Map
6768
import qualified Data.Set as Set
6869
import qualified Data.Text as Text
@@ -204,7 +205,7 @@ methodSpecHandler opts sc cc top_loc _mdMap css h =
204205
forM css $ \cs -> liftIO $
205206
let initialFree =
206207
Set.fromList (cs ^.. MS.csPreState. MS.csFreshVars . each . to tecExt . to ecVarIndex)
207-
in runOverrideMatcher sym g0 Map.empty Map.empty initialFree (view MS.csLoc cs)
208+
in runOverrideMatcher sym g0 Map.empty IntMap.empty initialFree (view MS.csLoc cs)
208209
(do methodSpecHandler_prestate opts sc cc args cs
209210
return cs)
210211

@@ -925,9 +926,9 @@ executePred sc cc md tt =
925926
-- | Map the given substitution over all 'SetupTerm' constructors in
926927
-- the given 'SetupValue'.
927928
instantiateSetupValue ::
928-
SharedContext ->
929-
Map VarIndex Term ->
930-
SetupValue ->
929+
SharedContext ->
930+
IntMap Term ->
931+
SetupValue ->
931932
IO SetupValue
932933
instantiateSetupValue sc s v =
933934
case v of

‎saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,7 @@ import qualified Data.Bimap as Bimap
104104
import Data.Char (isDigit)
105105
import Data.Foldable (for_, toList, fold)
106106
import Data.Functor (void)
107+
import qualified Data.IntMap as IntMap
107108
import Data.IORef
108109
import Data.List (find, nub, partition)
109110
import Data.List.Extra (nubOrd)
@@ -444,7 +445,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
444445
shared_context <- getSharedContext
445446

446447
let output_values =
447-
map (((Map.!) $ post_override_state ^. termSub) . ecVarIndex) output_parameters
448+
map (((IntMap.!) $ post_override_state ^. termSub) . ecVarIndex) output_parameters
448449

449450
extracted_func <-
450451
io $ scAbstractExts shared_context input_parameters
@@ -464,7 +465,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
464465
mkTypedTerm shared_context
465466
=<< scTupleSelector shared_context applied_extracted_func i (length output_parameters)
466467
let output_parameter_substitution =
467-
Map.fromList $
468+
IntMap.fromList $
468469
zip (map ecVarIndex output_parameters) (map ttTerm applied_extracted_func_selectors)
469470
let substitute_output_parameters =
470471
ttTermLens $ scInstantiateExt shared_context output_parameter_substitution
@@ -1594,7 +1595,7 @@ verifyPoststate cc mspec env0 globals ret mdMap invSubst =
15941595
skipSafetyProofs <- gets rwSkipSafetyProofs
15951596
when skipSafetyProofs (io (Crucible.clearProofObligations bak))
15961597

1597-
let ecs0 = Map.fromList
1598+
let ecs0 = IntMap.fromList
15981599
[ (ecVarIndex ec, ec)
15991600
| tt <- mspec ^. MS.csPreState . MS.csFreshVars
16001601
, let ec = tecExt tt ]

‎saw-central/src/SAWCentral/Crucible/LLVM/Override.hs‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,8 @@ import Control.Monad.IO.Class (MonadIO(..))
7171
import qualified Data.ByteString as BS
7272
import Data.Either (partitionEithers)
7373
import Data.Foldable (for_, traverse_, toList)
74+
import Data.IntMap (IntMap)
75+
import qualified Data.IntMap as IntMap
7476
import Data.List (partition, tails)
7577
import qualified Data.List.NonEmpty as NE
7678
import Data.IORef (IORef, modifyIORef)
@@ -334,7 +336,7 @@ methodSpecHandler opts sc cc mdMap css h =
334336
forM css $ \cs -> liftIO $
335337
let initialFree = Set.fromList (map (ecVarIndex . tecExt)
336338
(view (MS.csPreState . MS.csFreshVars) cs))
337-
in runOverrideMatcher sym g0 Map.empty Map.empty initialFree (view MS.csLoc cs)
339+
in runOverrideMatcher sym g0 Map.empty IntMap.empty initialFree (view MS.csLoc cs)
338340
(do methodSpecHandler_prestate opts sc cc args cs
339341
return cs)
340342

@@ -2306,9 +2308,9 @@ executeFreshPointer cc (AllocIndex i) =
23062308
-- | Map the given substitution over all 'SetupTerm' constructors in
23072309
-- the given 'SetupValue'.
23082310
instantiateSetupValue ::
2309-
SharedContext ->
2310-
Map VarIndex Term ->
2311-
SetupValue (LLVM arch) ->
2311+
SharedContext ->
2312+
IntMap Term ->
2313+
SetupValue (LLVM arch) ->
23122314
IO (SetupValue (LLVM arch))
23132315
instantiateSetupValue sc s v =
23142316
case v of

‎saw-central/src/SAWCentral/Crucible/LLVM/X86.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ import Control.Monad.State (MonadState, StateT(..), execStateT, gets)
4646
import qualified Data.BitVector.Sized as BV
4747
import Data.Foldable (foldlM)
4848
import Data.Functor (void)
49+
import qualified Data.IntMap as IntMap
4950
import Data.IORef
5051
import qualified Data.List.NonEmpty as NE
5152
import qualified Data.Vector as Vector
@@ -1493,7 +1494,7 @@ assertPost path func env premem preregs mdMap = do
14931494
$ ms ^. MS.csPostState . MS.csConditions
14941495

14951496
let
1496-
initialECs = Map.fromList
1497+
initialECs = IntMap.fromList
14971498
[ (ecVarIndex ec, ec)
14981499
| tt <- ms ^. MS.csPreState . MS.csFreshVars
14991500
, let ec = tecExt tt

0 commit comments

Comments
 (0)