Skip to content

Commit 03fbce4

Browse files
brianhuffmanbrianhuffman
committed
saw-core: Rename function 'scInstantiateExt' to 'scInstantiate'.
The "Ext" suffix formerly referred to type "ExtCns" which has been removed (#2732).
1 parent d86bb79 commit 03fbce4

File tree

14 files changed

+52
-53
lines changed

14 files changed

+52
-53
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -588,7 +588,7 @@ buildSubstMap sc substs0 = go IntMap.empty substs0
588588
go sm ((vn, term) : substs) = do
589589
-- Rewrite the RHSs of previous substitutions using the current one.
590590
let sm1 = IntMap.singleton (SAW.vnIndex vn) term
591-
sm' <- mapM (SAW.scInstantiateExt sc sm1) sm
591+
sm' <- mapM (SAW.scInstantiate sc sm1) sm
592592
-- Add the current subst and continue.
593593
go (IntMap.insert (SAW.vnIndex vn) term sm') substs
594594

@@ -677,7 +677,7 @@ substMethodSpec sc sm ms = do
677677
term' <- goTerm $ SAW.ttTerm tt
678678
return $ tt { SAW.ttTerm = term' }
679679

680-
goTerm term = SAW.scInstantiateExt sc sm term
680+
goTerm term = SAW.scInstantiate sc sm term
681681

682682

683683

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -545,7 +545,7 @@ setupToReg sym termSub myRegMap allocMap shp0 sv0 = go shp0 sv0
545545
go (UnitShape _) (MS.SetupTuple _ []) = return ()
546546
go (PrimShape _ btpr) (MS.SetupTerm tt) = do
547547
let sc = mirSharedContext (sym ^. W4.userState)
548-
term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
548+
term <- liftIO $ SAW.scInstantiate sc termSub $ SAW.ttTerm tt
549549
Some expr <- termToExpr sym myRegMap term
550550
Refl <- case testEquality (W4.exprType expr) btpr of
551551
Just x -> return x
@@ -607,7 +607,7 @@ condTerm _sc (MS.SetupCond_Equal _loc _sv1 _sv2) = do
607607
error $ "learnCond: SetupCond_Equal NYI" -- TODO
608608
condTerm sc (MS.SetupCond_Pred md tt) = do
609609
sub <- use MS.termSub
610-
t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt
610+
t' <- liftIO $ SAW.scInstantiate sc sub $ SAW.ttTerm tt
611611
return (md, t')
612612
condTerm _ (MS.SetupCond_Ghost _ _ _) = do
613613
error $ "learnCond: SetupCond_Ghost is not supported"

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -226,8 +226,7 @@ buildCompositionSideCondition bc innerBt = do
226226
lhsTuple <- io $ scTuple sc [lhsOuterState, input] -- (f_lhs_s, in)
227227
rhsTuple <- io $ scTuple sc [rhsOuterState, input] -- (f_rhs_s, in)
228228
innerRel' <- io $
229-
scInstantiateExt sc
230-
(IntMap.fromList [ (vnIndex lhsInnerVar, lhsTuple)
229+
scInstantiate sc (IntMap.fromList [ (vnIndex lhsInnerVar, lhsTuple)
231230
, (vnIndex rhsInnerVar, rhsTuple)])
232231
innerRel
233232

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -689,7 +689,7 @@ executeGhost ::
689689
OverrideMatcher ext RW ()
690690
executeGhost sc _md var (TypedTerm (TypedTermSchema sch) tm) =
691691
do s <- OM (use termSub)
692-
tm' <- liftIO (scInstantiateExt sc s tm)
692+
tm' <- liftIO (scInstantiate sc s tm)
693693
writeGlobal var (sch,tm')
694694
executeGhost _sc _md _var (TypedTerm tp _) =
695695
fail $ unlines
@@ -708,7 +708,7 @@ instantiateExtMatchTerm ::
708708
OverrideMatcher ext md ()
709709
instantiateExtMatchTerm sc md prepost actual expected = do
710710
sub <- OM (use termSub)
711-
matchTerm sc md prepost actual =<< liftIO (scInstantiateExt sc sub expected)
711+
matchTerm sc md prepost actual =<< liftIO (scInstantiate sc sub expected)
712712

713713
matchTerm ::
714714
SharedContext {- ^ context for constructing SAW terms -} ->

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -730,7 +730,7 @@ learnPred ::
730730
OverrideMatcher CJ.JVM w ()
731731
learnPred sc cc md prepost t =
732732
do s <- OM (use termSub)
733-
u <- liftIO $ scInstantiateExt sc s t
733+
u <- liftIO $ scInstantiate sc s t
734734
p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) u
735735
let loc = MS.conditionLoc md
736736
addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))
@@ -742,7 +742,7 @@ instantiateExtResolveSAWPred ::
742742
OverrideMatcher CJ.JVM md (W4.Pred Sym)
743743
instantiateExtResolveSAWPred sc cc cond = do
744744
sub <- OM (use termSub)
745-
liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
745+
liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
746746

747747
------------------------------------------------------------------------
748748

@@ -918,7 +918,7 @@ executePred ::
918918
OverrideMatcher CJ.JVM w ()
919919
executePred sc cc md tt =
920920
do s <- OM (use termSub)
921-
t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
921+
t <- liftIO $ scInstantiate sc s (ttTerm tt)
922922
p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) t
923923
addAssume p md
924924

@@ -949,7 +949,7 @@ instantiateSetupValue sc s v =
949949
MS.SetupGlobalInitializer empty _ -> absurd empty
950950
MS.SetupMux empty _ _ _ -> absurd empty
951951
where
952-
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
952+
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
953953

954954
------------------------------------------------------------------------
955955

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -459,7 +459,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic =
459459
IntMap.fromList $
460460
zip (map (vnIndex . fst) output_parameters) (map ttTerm applied_extracted_func_selectors)
461461
let substitute_output_parameters =
462-
ttTermLens $ scInstantiateExt shared_context output_parameter_substitution
462+
ttTermLens $ scInstantiate shared_context output_parameter_substitution
463463
let setup_value_substitute_output_parameter setup_value
464464
| SetupTerm term <- setup_value = SetupTerm <$> substitute_output_parameters term
465465
| otherwise = return $ setup_value

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1483,7 +1483,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
14831483
zero_byte_tm <- scBvNat sc byte_width_tm =<< scNat sc 0
14841484
zero_arr_const_tm <- scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm
14851485

1486-
instantiated_expected_sz_tm <- scInstantiateExt sc sub $ ttTerm expected_sz_tm
1486+
instantiated_expected_sz_tm <- scInstantiate sc sub $ ttTerm expected_sz_tm
14871487
scArrayCopy sc ptr_width_tm byte_type_tm
14881488
zero_arr_const_tm -- dest array
14891489
zero_off_tm -- dest offset
@@ -1502,7 +1502,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
15021502

15031503
_ ->
15041504
do sub <- OM (use termSub)
1505-
instantiated_expected_sz_tm <- liftIO $ scInstantiateExt sc sub $ ttTerm expected_sz_tm
1505+
instantiated_expected_sz_tm <- liftIO $ scInstantiate sc sub $ ttTerm expected_sz_tm
15061506
normalized_expected_sz_tm <- liftIO $
15071507
scTypeCheckWHNF sc =<< scUnfoldConstantSet sc False mempty instantiated_expected_sz_tm
15081508
case asUnsignedConcreteBv normalized_expected_sz_tm of
@@ -1743,7 +1743,7 @@ instantiateExtResolveSAWPred ::
17431743
OverrideMatcher (LLVM arch) md (W4.Pred Sym)
17441744
instantiateExtResolveSAWPred sc cc cond = do
17451745
sub <- OM (use termSub)
1746-
liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
1746+
liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
17471747

17481748
instantiateExtResolveSAWSymBV ::
17491749
(?w4EvalTactic :: W4EvalTactic, 1 <= w) =>
@@ -1754,7 +1754,7 @@ instantiateExtResolveSAWSymBV ::
17541754
OverrideMatcher (LLVM arch) md (W4.SymBV Sym w)
17551755
instantiateExtResolveSAWSymBV sc cc w tm = do
17561756
sub <- OM (use termSub)
1757-
liftIO $ resolveSAWSymBV cc w =<< scInstantiateExt sc sub tm
1757+
liftIO $ resolveSAWSymBV cc w =<< scInstantiate sc sub tm
17581758

17591759
------------------------------------------------------------------------
17601760

@@ -1979,7 +1979,7 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v
19791979
val' <- liftIO $ case val of
19801980
ConcreteSizeValue val'' -> ConcreteSizeValue <$> instantiateSetupValue sc s val''
19811981
SymbolicSizeValue arr sz ->
1982-
SymbolicSizeValue <$> ttTermLens (scInstantiateExt sc s) arr <*> ttTermLens (scInstantiateExt sc s) sz
1982+
SymbolicSizeValue <$> ttTermLens (scInstantiate sc s) arr <*> ttTermLens (scInstantiate sc s) sz
19831983
cond' <- mapM (instantiateExtResolveSAWPred sc cc . ttTerm) cond
19841984
let Crucible.LLVMPointer blk _ = ptr'
19851985
let invalidate_msg = Map.lookup blk overwritten_allocs
@@ -2330,7 +2330,7 @@ instantiateSetupValue sc s v =
23302330
SetupTuple empty _ -> absurd empty
23312331
SetupSlice empty -> absurd empty
23322332
where
2333-
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
2333+
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
23342334

23352335
------------------------------------------------------------------------
23362336

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -660,7 +660,7 @@ executePred ::
660660
OverrideMatcher MIR w ()
661661
executePred sc cc md tt =
662662
do s <- OM (use termSub)
663-
t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
663+
t <- liftIO $ scInstantiate sc s (ttTerm tt)
664664
p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) t
665665
addAssume p md
666666

@@ -900,7 +900,7 @@ instantiateExtResolveSAWPred ::
900900
OverrideMatcher MIR md (W4.Pred Sym)
901901
instantiateExtResolveSAWPred sc cc cond = do
902902
sub <- OM (use termSub)
903-
liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond
903+
liftIO $ resolveSAWPred cc =<< scInstantiate sc sub cond
904904

905905
-- | Map the given substitution over all 'SetupTerm' constructors in
906906
-- the given 'MirPointsTo' value.
@@ -949,7 +949,7 @@ instantiateSetupValue sc s v =
949949
<*> instantiateSetupValue sc s t
950950
<*> instantiateSetupValue sc s f
951951
where
952-
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
952+
doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiate sc s t
953953

954954
instantiateSetupEnum :: MirSetupEnum -> IO MirSetupEnum
955955
instantiateSetupEnum (MirSetupEnumVariant adt variant variantIdx vs) =
@@ -1085,7 +1085,7 @@ learnPred ::
10851085
OverrideMatcher MIR w ()
10861086
learnPred sc cc md prepost t =
10871087
do s <- OM (use termSub)
1088-
u <- liftIO $ scInstantiateExt sc s t
1088+
u <- liftIO $ scInstantiate sc s t
10891089
p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) u
10901090
let loc = MS.conditionLoc md
10911091
addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1741,7 +1741,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do
17411741
, showTerm ty
17421742
]
17431743
x' <- scVariable sc x xty
1744-
body' <- scInstantiateExt sc (IntMap.singleton (vnIndex nm) x') body
1744+
body' <- scInstantiate sc (IntMap.singleton (vnIndex nm) x') body
17451745
check nenv e' (mkSqt (Prop body'))
17461746

17471747
passthroughEvidence :: [Evidence] -> IO Evidence
@@ -2017,7 +2017,7 @@ propApply sc rule goal = applyFirst (asPiLists (unProp rule))
20172017
case IntMap.lookup (vnIndex vn) inst of
20182018
Nothing ->
20192019
-- this argument not solved by unification, so make it a goal
2020-
do c0 <- scInstantiateExt sc inst tp
2020+
do c0 <- scInstantiate sc inst tp
20212021
mp <- termToMaybeProp sc c0
20222022
let nm = vnName vn
20232023
case mp of
@@ -2052,7 +2052,7 @@ tacticIntro sc usernm = Tactic \goal ->
20522052
vn' <- liftIO $ scFreshVarName sc name
20532053
x <- liftIO $ scVariable sc vn' tp
20542054
tt <- liftIO $ mkTypedTerm sc x
2055-
body' <- liftIO $ scInstantiateExt sc (IntMap.singleton (vnIndex vn) x) body
2055+
body' <- liftIO $ scInstantiate sc (IntMap.singleton (vnIndex vn) x) body
20562056
let goal' = goal { goalSequent = mkSqt (Prop body') }
20572057
return (tt, mempty, [goal'], introEvidence vn' tp)
20582058

‎saw-core/src/SAWCore/Rewriter.hs‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,7 @@ scMatch sc ctxt pat term =
242242
check inst (t, n) = do
243243
--lift $ putStrLn $ "checking: " ++ show (t, n)
244244
-- apply substitution to the term
245-
t' <- lift $ scInstantiateExt sc inst t
245+
t' <- lift $ scInstantiate sc inst t
246246
--lift $ putStrLn $ "t': " ++ show t'
247247
-- constant-fold nat operations
248248
-- ensure that it evaluates to the same number
@@ -482,7 +482,7 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
482482
-- Define function to substitute the constructor @c@
483483
-- in for the old local variable @x@.
484484
let subst = IntMap.singleton (vnIndex x) c
485-
let adjust t = scInstantiateExt sc subst t
485+
let adjust t = scInstantiate sc subst t
486486
-- Build the list of types of the new context.
487487
ctxt2' <- traverse (traverse adjust) ctxt2
488488
let ctxt' = ctxt1 ++ argCtx ++ ctxt2'
@@ -525,7 +525,7 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
525525
case R.asLambda f' of
526526
Nothing -> scApply sc f' arg
527527
Just (vn, _, body) ->
528-
scInstantiateExt sc (IntMap.singleton (vnIndex vn) arg) body
528+
scInstantiate sc (IntMap.singleton (vnIndex vn) arg) body
529529

530530
-- | Like 'R.asPiList', but freshen all variables in the context.
531531
asFreshPiList :: SharedContext -> Term -> IO ([(VarName, Term)], Term)
@@ -537,7 +537,7 @@ asFreshPiList sc t =
537537
let basename = if vnName x == "_" then "_x" else vnName x
538538
x' <- scFreshVarName sc basename
539539
var <- scVariable sc x' t1
540-
t2' <- scInstantiateExt sc (IntMap.singleton (vnIndex x) var) t2
540+
t2' <- scInstantiate sc (IntMap.singleton (vnIndex x) var) t2
541541
(ctx, body) <- asFreshPiList sc t2'
542542
pure ((x', t1) : ctx, body)
543543

@@ -694,7 +694,7 @@ termWeightLt t t' =
694694
-- level, if possible.
695695
reduceSharedTerm :: SharedContext -> Term -> IO (Maybe Term)
696696
reduceSharedTerm sc (asBetaRedex -> Just (vn, _, body, arg)) =
697-
Just <$> scInstantiateExt sc (IntMap.singleton (vnIndex vn) arg) body
697+
Just <$> scInstantiate sc (IntMap.singleton (vnIndex vn) arg) body
698698
reduceSharedTerm _ (asPairRedex -> Just t) = pure (Just t)
699699
reduceSharedTerm _ (asRecordRedex -> Just t) = pure (Just t)
700700
reduceSharedTerm sc (asNatIotaRedex -> Just (f1, f2, n)) =
@@ -769,19 +769,19 @@ rewriteSharedTerm sc ss t0 =
769769
apply rules t
770770
| permutative ->
771771
do
772-
t' <- scInstantiateExt sc inst rhs
772+
t' <- scInstantiate sc inst rhs
773773
case termWeightLt t' t of
774774
True -> recordAnn annotation >> rewriteAll t' -- keep the result only if it is "smaller"
775775
False -> apply rules t
776776
| shallow ->
777777
-- do not to further rewriting to the result of a "shallow" rule
778778
do recordAnn annotation
779-
scInstantiateExt sc inst rhs
779+
scInstantiate sc inst rhs
780780
| otherwise ->
781781
do -- putStrLn "REWRITING:"
782782
-- print lhs
783783
recordAnn annotation
784-
rewriteAll =<< scInstantiateExt sc inst rhs
784+
rewriteAll =<< scInstantiate sc inst rhs
785785
apply (Right conv : rules) t =
786786
do -- putStrLn "REWRITING:"
787787
-- print (Net.toPat conv)
@@ -870,7 +870,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
870870
Nothing -> apply rules t
871871
Just inst ->
872872
do recordAnn (annotation rule)
873-
rewriteAll =<< scInstantiateExt sc inst (rhs rule)
873+
rewriteAll =<< scInstantiate sc inst (rhs rule)
874874
apply (Right conv : rules) t =
875875
case runConversion conv t of
876876
Nothing -> apply rules t
@@ -904,7 +904,7 @@ rewritingSharedContext sc ss = sc'
904904
| l == r ->
905905
do putStrLn $ "rewritingSharedContext: skipping reflexive rule: " ++ scPrettyTerm PPS.defaultOpts l
906906
apply rules t
907-
| otherwise -> scInstantiateExt sc' inst r
907+
| otherwise -> scInstantiate sc' inst r
908908
apply (Right conv : rules) t =
909909
case runConversion conv t of
910910
Nothing -> apply rules t

0 commit comments

Comments
 (0)