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.

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

[Heapster] Reduce catchpoints and add more Mbox proofs #1413

Merged
merged 6 commits into from
Aug 9, 2021
Prev Previous commit
Merge remote-tracking branch 'origin/master' into heapster-reduce-cat…
…chpoints
Eddy Westbrook committed Aug 9, 2021
commit f0765aff9b7ffd065ceec820e6e067a2a5269e35
6 changes: 3 additions & 3 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
Original file line number Diff line number Diff line change
@@ -3119,7 +3119,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
-- A failure translates to a call to the catch handler, which is the most recent
-- Impl1_Catch, if one exists, or the SAW errorM function otherwise
([nuMP| Impl1_Fail str |], _) -> pitmFail $ mbLift str

([nuMP| Impl1_Catch |],
[nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) ->
pitmCatching (translatePermImpl prx $
@@ -3139,7 +3139,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
(Just trans, _, Nothing, _) -> return trans
(Nothing, _, Just trans, _) -> return trans
(Nothing, _, Nothing, _) -> mzero

-- A push moves the given permission from x to the top of the perm stack
([nuMP| Impl1_Push x p |], _) ->
translatePermImplUnary mb_impls $ \m ->
@@ -3293,7 +3293,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
([nuMP| Impl1_TryProveBVProp _ (BVProp_Eq e1 e2) prop_str |], _)
| not $ mbLift (mbMap2 bvCouldEqual e1 e2) ->
pitmFail (mbLift prop_str)

-- Otherwise, insert an equality test with proof construction. Note that, as
-- with all TryProveBVProps, if the test fails and there is no failure
-- continuation, we insert just the proposition failure string using
You are viewing a condensed version of this merge commit. You can view the full changes here.