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

Fix examples after en tree #1827

Open
wants to merge 53 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
3a9c13b
add basic IDE logging, start error cleanup
Jun 28, 2021
bfd0566
clean up additional implication errors
Jun 28, 2021
49f72e4
add structure to stmt fail in line with impl fail
Jun 29, 2021
716a2e1
redesign error message types, pipe through to log
Jul 7, 2021
9283f0e
fix default heapster environments missing ioref
Jul 8, 2021
1e427a4
carry more information through on most common implication error
Jul 9, 2021
059ab7b
Merge branch 'heapster-ide-info' of github.com:GaloisInc/saw-script i…
Jul 9, 2021
6fef67a
remove Some from error constructor
Jul 9, 2021
f3b76bb
Merge branch 'master' into heapster-ide-info
glguy Jul 26, 2021
e2c9cd6
Export valueperms in full json detail
glguy Jul 28, 2021
b59adb9
Avoid generating orphan ToJSON instances and using Given
glguy Jul 28, 2021
65ae7dd
refine jsonexport instances
glguy Jul 28, 2021
931d802
Document JSONExport
glguy Jul 28, 2021
2ad2225
Remove need for passing undefined
glguy Jul 30, 2021
ce3313b
JSONExport support for PermImpls
glguy Jul 30, 2021
df114c1
export entrypoint and caller ID information
Aug 12, 2021
8875708
cleanup imports, 80 char columns
Aug 12, 2021
5f12cc4
heapster: export function name for IDE
Aug 12, 2021
cb7c57c
heapster-saw: LogEntry with names and structure
glguy Aug 19, 2021
e768f1f
Incorporate names from bindings in JsonExport
glguy Aug 20, 2021
f60affd
Merge remote-tracking branch 'origin/master' into heapster-ide-info
glguy Aug 20, 2021
51665d7
Update PPInfo while exporting
glguy Aug 23, 2021
dc70b93
checkpoint
glguy Aug 27, 2021
f0c7747
Use types to generate names for pretty permissions where possible
glguy Aug 27, 2021
45380a5
Merge branch 'master' into heapster-ide-info
scuellar Feb 3, 2023
6170858
WIP: fixing errors introduced by the merge.
scuellar Feb 3, 2023
7694e2f
got SAW to compile after the latest merge of master
Feb 6, 2023
009caf6
Merge branch 'master' into heapster-ide-info
Feb 7, 2023
8ac9eb5
Merge branch 'master' into heapster-ide-info
Feb 7, 2023
bb9c52d
Updtate deps
scuellar Feb 13, 2023
d0fe08e
Merge branch 'master' into heapster-ide-info
scuellar Feb 13, 2023
10aacd5
update proofs xor
scuellar Feb 16, 2023
1a6a03d
Fix xor proofs
scuellar Feb 16, 2023
b85f7b7
Add a file with generlalized tactics and definitions
scuellar Feb 16, 2023
c19c2ae
Quick fix.
scuellar Feb 16, 2023
4f04499
BROKEN: c_data_proofs.v is broken. pushing to get assitance.
scuellar Feb 17, 2023
2cadcbf
One more example fixed, more powerful automation to support it.
scuellar Feb 17, 2023
2cbf50d
Updating a couple more examples and some automation.
scuellar Feb 21, 2023
3d76821
Small clean
scuellar Feb 21, 2023
dd69d30
bumping the cryptol submodule to match master
Feb 28, 2023
dbc3ccf
moved nuMatching and Liftable instances to the top of the file in Nam…
Mar 1, 2023
1310346
GHC 9 fixes
Mar 1, 2023
599cf2a
renamed the Mb' datatype to the more accessible name NamedMb, and cha…
Mar 1, 2023
856e49b
Fix the tutorial proofs.
scuellar Mar 1, 2023
7d53a24
Update the tutorial text
scuellar Mar 1, 2023
defedde
Merge branch 'heapster-ide-info' into Fix-Examples-After-EnTree
scuellar Mar 1, 2023
013f9f9
Merge branch 'master' into Fix-Examples-After-EnTree
scuellar Mar 2, 2023
42981b1
Update heapster-saw/doc/tutorial/tutorial.md
scuellar Mar 7, 2023
b7ffbf3
Update heapster-saw/doc/tutorial/tutorial.md
scuellar Mar 7, 2023
45c6fcf
Update heapster-saw/doc/tutorial/tutorial.md
scuellar Mar 7, 2023
5615ae1
Update heapster-saw/doc/tutorial/tutorial.md
scuellar Mar 7, 2023
7a74d26
simple changes after review.
scuellar Mar 7, 2023
9e538c7
Merge branch 'Fix-Examples-After-EnTree' of https://github.com/Galois…
scuellar Mar 7, 2023
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
Prev Previous commit
Next Next commit
Use types to generate names for pretty permissions where possible
  • Loading branch information
glguy committed Aug 27, 2021
commit f0c77472c0e1fd0d7648723078c73b7e38982e67
14 changes: 12 additions & 2 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
Original file line number Diff line number Diff line change
@@ -349,6 +349,16 @@ permPrettyExprMb f mb =
do docs <- traverseRAssign (\n -> Constant <$> permPrettyM n) ns
f docs $ permPrettyM a

permPrettyExprMbTyped :: PermPretty a =>
CruCtx ctx ->
(RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
permPrettyExprMbTyped ctx f mb =
fmap mbLift $ strongMbM $ flip nuMultiWithElim1 mb $ \ns a ->
local (ppInfoAddTypedExprNames ctx ns) $
do docs <- traverseRAssign (\n -> Constant <$> permPrettyM n) ns
f docs $ permPrettyM a

instance (PermPretty a) => PermPretty (Mb (ctx :: RList CrucibleType) a) where
permPrettyM =
permPrettyExprMb $ \docs ppm ->
@@ -891,7 +901,7 @@ instance PermPretty (PermExpr a) where
pp2 <- permPrettyM sh2
return $ nest 2 $ sep [pp1 <+> pretty "orsh", pp2]
permPrettyM (PExpr_ExShape mb_sh) =
flip permPrettyExprMb mb_sh $ \(_ :>: Constant pp_n) ppm ->
flip (permPrettyExprMbTyped (CruCtxNil `CruCtxCons` knownRepr)) mb_sh $ \(_ :>: Constant pp_n) ppm ->
do pp <- ppm
return $ nest 2 $ sep [pretty "exsh" <+> pp_n <> dot, pp]
permPrettyM (PExpr_ValPerm p) = permPrettyM p
@@ -2592,7 +2602,7 @@ instance PermPretty (ValuePerm a) where
(\pp1 pp2 -> hang 2 (pp1 <> softline <> pretty "or" <+> pp2))
<$> permPrettyM p1 <*> permPrettyM p2
permPrettyM (ValPerm_Exists mb_p) =
flip permPrettyExprMb mb_p $ \(_ :>: Constant pp_n) ppm ->
flip (permPrettyExprMbTyped (CruCtxNil `CruCtxCons` knownRepr)) mb_p $ \(_ :>: Constant pp_n) ppm ->
(\pp -> hang 2 (pretty "exists" <+> pp_n <> dot <+> pp)) <$> ppm
permPrettyM (ValPerm_Named n args off) =
do n_pp <- permPrettyM n