Skip to content

Commit 52b6a19

Browse files
samcowgersamcowger
authored
Merge pull request #1837 from GaloisInc/feature/hashed-let-bindings
Expose term hashes in memoization
2 parents 2cf27a9 + f538ea7 commit 52b6a19

File tree

4 files changed

+199
-55
lines changed

4 files changed

+199
-55
lines changed

‎saw-core/src/Verifier/SAW/Term/Pretty.hs

+114-53
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ module Verifier.SAW.Term.Pretty
2222
, renderSawDoc
2323
, SawStyle(..)
2424
, PPOpts(..)
25+
, MemoStyle(..)
2526
, defaultPPOpts
2627
, depthPPOpts
2728
, ppNat
@@ -53,13 +54,14 @@ import Control.Monad.State.Strict (MonadState(..), State, execState)
5354
import Data.Foldable (Foldable)
5455
#endif
5556
import qualified Data.Foldable as Fold
57+
import Data.Hashable (hash)
5658
import qualified Data.Text as Text
5759
import qualified Data.Text.Lazy as Text.Lazy
5860
import qualified Data.Map as Map
5961
import Data.Set (Set)
6062
import qualified Data.Set as Set
6163
import qualified Data.Vector as V
62-
import Numeric (showIntAtBase)
64+
import Numeric (showIntAtBase, showHex)
6365
import Prettyprinter
6466
import Prettyprinter.Render.Terminal
6567
import Text.URI
@@ -109,15 +111,46 @@ data PPOpts = PPOpts { ppBase :: Int
109111
, ppColor :: Bool
110112
, ppShowLocalNames :: Bool
111113
, ppMaxDepth :: Maybe Int
112-
, ppNoInlineMemo :: [MemoVar]
114+
, ppNoInlineMemoFresh :: [Int]
115+
-- ^ The numeric identifiers, as seen in the 'memoFresh'
116+
-- field of 'MemoVar', of variables that shouldn't be
117+
-- inlined
113118
, ppNoInlineIdx :: Set TermIndex -- move to PPState?
119+
, ppMemoStyle :: MemoStyle
114120
, ppMinSharing :: Int }
115121

122+
-- | How should memoization variables be displayed?
123+
--
124+
-- Note: actual text stylization is the province of 'ppMemoVar', this just
125+
-- describes the semantic information 'ppMemoVar' should be prepared to display.
126+
data MemoStyle
127+
= Incremental
128+
-- ^ 'Incremental' says to display a term's memoization variable with the
129+
-- value of a counter that increments after a term is memoized. The first
130+
-- term to be memoized will be displayed with '1', the second with '2', etc.
131+
| Hash Int
132+
-- ^ 'Hash i' says to display a term's memoization variable with the first 'i'
133+
-- digits of the term's hash.
134+
| HashIncremental Int
135+
-- ^ 'HashIncremental i' says to display a term's memoization variable with
136+
-- _both_ the first 'i' digits of the term's hash _and_ the value of the
137+
-- counter described in 'Incremental'.
138+
116139
-- | Default options for pretty-printing
117140
defaultPPOpts :: PPOpts
118-
defaultPPOpts = PPOpts { ppBase = 10, ppColor = False,
119-
ppNoInlineMemo = mempty, ppNoInlineIdx = mempty,
120-
ppShowLocalNames = True, ppMaxDepth = Nothing, ppMinSharing = 2 }
141+
defaultPPOpts =
142+
PPOpts
143+
{ ppBase = 10
144+
, ppColor = False
145+
, ppNoInlineMemoFresh = mempty
146+
, ppNoInlineIdx = mempty
147+
, ppShowLocalNames = True
148+
, ppMaxDepth = Nothing
149+
, ppMinSharing = 2
150+
, ppMemoStyle = Incremental }
151+
-- If 'ppMemoStyle' changes its default, be sure to update the help text in
152+
-- the interpreter functions that control the memoization style to reflect
153+
-- this change to users.
121154

122155
-- | Options for printing with a maximum depth
123156
depthPPOpts :: Int -> PPOpts
@@ -211,9 +244,18 @@ consVarNaming (VarNaming names) name =
211244
-- * Pretty-printing monad
212245
--------------------------------------------------------------------------------
213246

214-
-- | Memoization variables, which are like deBruijn index variables but for
215-
-- terms that we are memoizing during printing
216-
type MemoVar = Int
247+
-- | Memoization variables contain several pieces of information about the term
248+
-- they bind. What subset is displayed when they're printed is governed by the
249+
-- 'ppMemoStyle' field of 'PPOpts', in tandem with 'ppMemoVar'.
250+
data MemoVar =
251+
MemoVar
252+
{
253+
-- | A unique value - like a deBruijn index, but evinced only during
254+
-- printing when a term is to be memoized.
255+
memoFresh :: Int,
256+
-- | A likely-unique value - the hash of the term this 'MemoVar'
257+
-- represents.
258+
memoHash :: Int }
217259

218260
-- | The local state used by pretty-printing computations
219261
data PPState =
@@ -227,8 +269,8 @@ data PPState =
227269
ppNaming :: VarNaming,
228270
-- | The top-level naming environment
229271
ppNamingEnv :: SAWNamingEnv,
230-
-- | The next "memoization variable" to generate
231-
ppNextMemoVar :: MemoVar,
272+
-- | A source of freshness for memoization variables
273+
ppMemoFresh :: Int,
232274
-- | Memoization table for the global, closed terms, mapping term indices to
233275
-- "memoization variables" that are in scope
234276
ppGlobalMemoTable :: IntMap MemoVar,
@@ -239,9 +281,12 @@ data PPState =
239281

240282
emptyPPState :: PPOpts -> SAWNamingEnv -> PPState
241283
emptyPPState opts ne =
242-
PPState { ppOpts = opts, ppDepth = 0, ppNaming = emptyVarNaming,
284+
PPState { ppOpts = opts,
285+
ppDepth = 0,
286+
ppNaming = emptyVarNaming,
243287
ppNamingEnv = ne,
244-
ppNextMemoVar = 1, ppGlobalMemoTable = IntMap.empty,
288+
ppMemoFresh = 1,
289+
ppGlobalMemoTable = IntMap.empty,
245290
ppLocalMemoTable = IntMap.empty }
246291

247292
-- | The pretty-printing monad
@@ -295,45 +340,47 @@ withBoundVarM basename m =
295340
ppLocalMemoTable = IntMap.empty }) m
296341
return (var, ret)
297342

298-
-- | Attempt to memoize the given term (index) 'idx' and run a computation in
299-
-- the context that the attempt produces. If memoization succeeds, the context
300-
-- will contain a binding (global in scope if 'global_p' is set, local if not)
301-
-- of a fresh memoization variable to the term, and the fresh variable will be
302-
-- supplied to the computation. If memoization fails, the context will not
303-
-- contain such a binding, and no fresh variable will be supplied.
304-
withMemoVar :: Bool -> TermIndex -> (Maybe MemoVar -> PPM a) -> PPM a
305-
withMemoVar global_p idx f =
343+
-- | Attempt to memoize the given term (index) 'termIdx' and run a computation
344+
-- in the context that the attempt produces. If memoization succeeds, the
345+
-- context will contain a binding (global in scope if 'global_p' is set, local
346+
-- if not) of a fresh memoization variable to the term, and the fresh variable
347+
-- will be supplied to the computation. If memoization fails, the context will
348+
-- not contain such a binding, and no fresh variable will be supplied.
349+
withMemoVar :: Bool -> TermIndex -> Int -> (Maybe MemoVar -> PPM a) -> PPM a
350+
withMemoVar global_p termIdx termHash f =
306351
do
307-
memoVar <- asks ppNextMemoVar
308-
memoSkips <- asks (ppNoInlineMemo . ppOpts)
309-
idxSkips <- asks (ppNoInlineIdx . ppOpts)
310-
case memoSkips of
352+
memoFresh <- asks ppMemoFresh
353+
let memoVar = MemoVar { memoFresh = memoFresh, memoHash = termHash }
354+
memoFreshSkips <- asks (ppNoInlineMemoFresh . ppOpts)
355+
termIdxSkips <- asks (ppNoInlineIdx . ppOpts)
356+
case memoFreshSkips of
311357
-- Even if we must skip this memoization variable, we still want to
312-
-- "pretend" we memoized by calling `updateMemoVar`, so that non-inlined
358+
-- "pretend" we memoized by calling `freshen`, so that non-inlined
313359
-- memoization identifiers are kept constant between two
314360
-- otherwise-identical terms with differing inline strategies.
315361
(skip:skips)
316-
| skip == memoVar -> local (updateMemoVar . addIdxSkip . setMemoSkips skips) (f Nothing)
362+
| skip == memoFresh ->
363+
local (freshen . addIdxSkip . setMemoFreshSkips skips) (f Nothing)
317364
_
318-
| idx `Set.member` idxSkips -> f Nothing
319-
| otherwise -> local (updateMemoVar . bind memoVar) (f (Just memoVar))
365+
| termIdx `Set.member` termIdxSkips -> f Nothing
366+
| otherwise -> local (freshen . bind memoVar) (f (Just memoVar))
320367
where
321368
bind = if global_p then bindGlobal else bindLocal
322369

323370
bindGlobal memoVar PPState{ .. } =
324-
PPState { ppGlobalMemoTable = IntMap.insert idx memoVar ppGlobalMemoTable, .. }
371+
PPState { ppGlobalMemoTable = IntMap.insert termIdx memoVar ppGlobalMemoTable, .. }
325372

326373
bindLocal memoVar PPState{ .. } =
327-
PPState { ppLocalMemoTable = IntMap.insert idx memoVar ppLocalMemoTable, .. }
374+
PPState { ppLocalMemoTable = IntMap.insert termIdx memoVar ppLocalMemoTable, .. }
328375

329-
setMemoSkips memoSkips PPState{ ppOpts = PPOpts{ .. }, .. } =
330-
PPState { ppOpts = PPOpts { ppNoInlineMemo = memoSkips, ..}, ..}
376+
setMemoFreshSkips memoSkips PPState{ ppOpts = PPOpts{ .. }, .. } =
377+
PPState { ppOpts = PPOpts { ppNoInlineMemoFresh = memoSkips, ..}, ..}
331378

332379
addIdxSkip PPState{ ppOpts = PPOpts{ .. }, .. } =
333-
PPState { ppOpts = PPOpts { ppNoInlineIdx = Set.insert idx ppNoInlineIdx, .. }, .. }
380+
PPState { ppOpts = PPOpts { ppNoInlineIdx = Set.insert termIdx ppNoInlineIdx, .. }, .. }
334381

335-
updateMemoVar PPState{ .. } =
336-
PPState { ppNextMemoVar = ppNextMemoVar + 1, .. }
382+
freshen PPState{ .. } =
383+
PPState { ppMemoFresh = ppMemoFresh + 1, .. }
337384

338385
--------------------------------------------------------------------------------
339386
-- * The Pretty-Printing of Specific Constructs
@@ -359,9 +406,17 @@ ppNat (PPOpts{..}) i
359406
value = showIntAtBase (toInteger ppBase) (digits !!) i ""
360407
digits = "0123456789abcdefghijklmnopqrstuvwxyz"
361408

362-
-- | Pretty-print a memoization variable
363-
ppMemoVar :: MemoVar -> SawDoc
364-
ppMemoVar mv = "x@" <> pretty mv
409+
-- | Pretty-print a memoization variable, according to 'ppMemoStyle'
410+
ppMemoVar :: MemoVar -> PPM SawDoc
411+
ppMemoVar MemoVar{..} = asks (ppMemoStyle . ppOpts) >>= \case
412+
Incremental ->
413+
pure ("x@" <> pretty memoFresh)
414+
Hash prefixLen ->
415+
pure ("x@" <> pretty (take prefixLen hashStr))
416+
HashIncremental prefixLen ->
417+
pure ("x" <> pretty memoFresh <> "@" <> pretty (take prefixLen hashStr))
418+
where
419+
hashStr = showHex (abs memoHash) ""
365420

366421
-- | Pretty-print a type constraint (also known as an ascription) @x : tp@
367422
ppTypeConstraint :: SawDoc -> SawDoc -> SawDoc
@@ -373,16 +428,22 @@ ppAppList :: Prec -> SawDoc -> [SawDoc] -> SawDoc
373428
ppAppList _ f [] = f
374429
ppAppList p f args = ppParensPrec p PrecApp $ group $ hang 2 $ vsep (f : args)
375430

376-
-- | Pretty-print "let x1 = t1 ... xn = tn in body"
377-
ppLetBlock :: [(MemoVar, SawDoc)] -> SawDoc -> SawDoc
431+
-- | Pretty-print "let x = t ... x' = t' in body"
432+
ppLetBlock :: [(MemoVar, SawDoc)] -> SawDoc -> PPM SawDoc
378433
ppLetBlock defs body =
379-
vcat
380-
[ "let" <+> lbrace <+> align (vcat (map ppEqn defs))
381-
, indent 4 rbrace
382-
, " in" <+> body
383-
]
434+
do
435+
lets <- align . vcat <$> mapM ppEqn defs
436+
pure $
437+
vcat
438+
[ "let" <+> lbrace <+> lets
439+
, indent 4 rbrace
440+
, " in" <+> body
441+
]
384442
where
385-
ppEqn (var,d) = ppMemoVar var <+> pretty '=' <+> d
443+
ppEqn (var,d) =
444+
do
445+
mv <- ppMemoVar var
446+
pure $ mv <+> pretty '=' <+> d
386447

387448

388449
-- | Pretty-print pairs as "(x, y)"
@@ -573,7 +634,7 @@ ppTerm' prec = atNextDepthM "..." . ppTerm'' where
573634
ppTerm'' (STApp {stAppIndex = idx, stAppTermF = tf}) =
574635
do maybe_memo_var <- memoLookupM idx
575636
case maybe_memo_var of
576-
Just memo_var -> return $ ppMemoVar memo_var
637+
Just memo_var -> ppMemoVar memo_var
577638
Nothing -> ppTermF prec tf
578639

579640

@@ -685,17 +746,17 @@ ppLets _ [] [] baseDoc = baseDoc
685746

686747
-- When we have run out of (idx,term) pairs, pretty-print a let binding for
687748
-- all the accumulated bindings around the term
688-
ppLets _ [] bindings baseDoc = ppLetBlock (reverse bindings) <$> baseDoc
749+
ppLets _ [] bindings baseDoc = ppLetBlock (reverse bindings) =<< baseDoc
689750

690751
-- To add an (idx,term) pair, first check if idx is already bound, and, if
691752
-- not, add a new MemoVar bind it to idx
692-
ppLets global_p ((idx, (t_rhs,_)):idxs) bindings baseDoc =
693-
do isBound <- isJust <$> memoLookupM idx
753+
ppLets global_p ((termIdx, (term,_)):idxs) bindings baseDoc =
754+
do isBound <- isJust <$> memoLookupM termIdx
694755
if isBound then ppLets global_p idxs bindings baseDoc else
695-
do doc_rhs <- ppTerm' PrecTerm t_rhs
696-
withMemoVar global_p idx $ \memoVarM ->
756+
do termDoc <- ppTerm' PrecTerm term
757+
withMemoVar global_p termIdx (hash term) $ \memoVarM ->
697758
let bindings' = case memoVarM of
698-
Just memoVar -> (memoVar, doc_rhs):bindings
759+
Just memoVar -> (memoVar, termDoc):bindings
699760
Nothing -> bindings
700761
in ppLets global_p idxs bindings' baseDoc
701762

‎src/SAWScript/Builtins.hs

+13-1
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,7 @@ import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
8080
import Verifier.SAW.Recognizer
8181
import Verifier.SAW.Prelude (scEq)
8282
import Verifier.SAW.SharedTerm
83+
import Verifier.SAW.Term.Pretty (MemoStyle(..))
8384
import Verifier.SAW.TypedTerm
8485
import qualified Verifier.SAW.Simulator.Concrete as Concrete
8586
import Verifier.SAW.Prim (rethrowEvalError)
@@ -478,11 +479,22 @@ print_goal_inline noInline =
478479
execTactic $ tacticId $ \goal ->
479480
do
480481
opts <- getTopLevelPPOpts
481-
let opts' = opts { ppNoInlineMemo = sort noInline }
482+
opts' <-
483+
case ppMemoStyle opts of
484+
Incremental -> pure opts { ppNoInlineMemoFresh = sort noInline }
485+
HashIncremental _ -> pure opts { ppNoInlineMemoFresh = sort noInline }
486+
Hash _ -> warnIncremental >> pure opts
482487
sc <- getSharedContext
483488
nenv <- io (scGetNamingEnv sc)
484489
let output = prettySequent opts' nenv (goalSequent goal)
485490
printOutLnTop Info (unlines [goalSummary goal, output])
491+
where
492+
warnIncremental =
493+
printOutLnTop Warn $
494+
unlines
495+
[ "`print_goal_inline` is incompatible with non-incremental"
496+
, "memoization strategies. Printing goal without inlining..."
497+
]
486498

487499
print_goal_summary :: ProofScript ()
488500
print_goal_summary =

0 commit comments

Comments
 (0)