Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Defer CallStack computations by representing them as data constructors. #1202

Merged
merged 2 commits into from
May 27, 2021
Merged

Defer CallStack computations by representing them as data constructors. #1202

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
88fbbd3
Defer `CallStack` computations by representing them as data construct…
May 26, 2021
cbfc6c7
Add special cases to `combineCallStacks`.
May 26, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 40 additions & 7 deletions src/Cryptol/Backend/Monad.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,12 +63,33 @@ ready a = Ready a

-- | The type of dynamic call stacks for the interpreter.
-- New frames are pushed onto the right side of the sequence.
type CallStack = Seq (Name, Range)
data CallStack
= EmptyCallStack
| CombineCallStacks !CallStack !CallStack
| PushCallFrame !Name !Range !CallStack

instance Semigroup CallStack where
(<>) = CombineCallStacks

instance Monoid CallStack where
mempty = EmptyCallStack

type CallStack' = Seq (Name, Range)

evalCallStack :: CallStack -> CallStack'
evalCallStack stk =
case stk of
EmptyCallStack -> mempty
CombineCallStacks appstk fnstk -> combineCallStacks' (evalCallStack appstk) (evalCallStack fnstk)
PushCallFrame n r stk1 -> pushCallFrame' n r (evalCallStack stk1)

-- | Pretty print a call stack with each call frame on a separate
-- line, with most recent call frames at the top.
displayCallStack :: CallStack -> Doc
displayCallStack = vcat . map f . toList . Seq.reverse
displayCallStack = displayCallStack' . evalCallStack

displayCallStack' :: CallStack' -> Doc
displayCallStack' = vcat . map f . toList . Seq.reverse
where
f (nm,rng)
| rng == emptyRange = pp nm
Expand All @@ -92,7 +113,15 @@ combineCallStacks ::
CallStack {- ^ call stack of the application context -} ->
CallStack {- ^ call stack of the function being applied -} ->
CallStack
combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
combineCallStacks appstk EmptyCallStack = appstk
combineCallStacks EmptyCallStack fnstk = fnstk
combineCallStacks appstk fnstk = CombineCallStacks appstk fnstk
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure how common this is, but is it worth checking for the special cases where one of the arguments is the EmptyCallStack?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea. That would cost very little to check for, and it would strictly reduce the memory consumption whenever that rule matches.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added special cases for EmptyCallStack. Looking at +RTS -s, any performance differences (on my use case at least) are lost in the noise. But we might as well keep it in; it only reduces total allocation by 0.01% but it might be more on other examples.


combineCallStacks' ::
CallStack' {- ^ call stack of the application context -} ->
CallStack' {- ^ call stack of the function being applied -} ->
CallStack'
combineCallStacks' appstk fnstk = appstk <> dropCommonPrefix appstk fnstk
where
dropCommonPrefix _ Seq.Empty = Seq.Empty
dropCommonPrefix Seq.Empty fs = fs
Expand All @@ -102,9 +131,12 @@ combineCallStacks appstk fnstk = appstk <> dropCommonPrefix appstk fnstk

-- | Add a call frame to the top of a call stack
pushCallFrame :: Name -> Range -> CallStack -> CallStack
pushCallFrame nm rng stk@( _ Seq.:|> (nm',rng'))
pushCallFrame nm rng stk = PushCallFrame nm rng stk

pushCallFrame' :: Name -> Range -> CallStack' -> CallStack'
pushCallFrame' nm rng stk@( _ Seq.:|> (nm',rng'))
| nm == nm', rng == rng' = stk
pushCallFrame nm rng stk = stk Seq.:|> (nm,rng)
pushCallFrame' nm rng stk = stk Seq.:|> (nm,rng)


-- | The monad for Cryptol evaluation.
Expand Down Expand Up @@ -417,11 +449,12 @@ data EvalErrorEx =
deriving Typeable

instance PP EvalErrorEx where
ppPrec _ (EvalErrorEx stk ex) = vcat ([ pp ex ] ++ callStk)
ppPrec _ (EvalErrorEx stk0 ex) = vcat ([ pp ex ] ++ callStk)

where
stk = evalCallStack stk0
callStk | Seq.null stk = []
| otherwise = [ text "-- Backtrace --", displayCallStack stk ]
| otherwise = [ text "-- Backtrace --", displayCallStack' stk ]

instance Show EvalErrorEx where
show = show . pp
Expand Down