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

Support building Heapster shapes from Rust type declarations #85

Merged
merged 35 commits into from
Apr 29, 2021
Merged

Support building Heapster shapes from Rust type declarations #85

Show file tree
Hide file tree
Changes from 33 commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
fd6dd79
Skeleton for Rust type decl parser
ChrisEPhifer Apr 14, 2021
b3ce37c
Some RsConvert instances to support top-level struct/enum definitions
ChrisEPhifer Apr 19, 2021
4db9aa5
Corrected return type on type shape entrypoint
ChrisEPhifer Apr 19, 2021
adf51da
Fix RsConvert Item instance target type, implement Generics -> RustCt…
ChrisEPhifer Apr 19, 2021
9970755
Fix some unused variable warnings
ChrisEPhifer Apr 19, 2021
2e12524
Implement basic/naive decider for recursive Rust types
ChrisEPhifer Apr 19, 2021
a8502f5
Support deciding recursive structs
ChrisEPhifer Apr 19, 2021
fdde147
Be consistent about the uses of `error` vs `fail`
ChrisEPhifer Apr 20, 2021
669b1ab
Add missing cases to recursive-decider helper
ChrisEPhifer Apr 20, 2021
75c17ec
Implement struct conversion
ChrisEPhifer Apr 20, 2021
bccb0c2
Better style for Item RsConvert instance
ChrisEPhifer Apr 20, 2021
bf3d899
First crack at parsing shapes from Rust
ChrisEPhifer Apr 20, 2021
527e6dc
'permission' -> 'shape' in new parser docs
ChrisEPhifer Apr 20, 2021
4b64361
Merge branch 'master' into feature/rust-type-decls
ChrisEPhifer Apr 20, 2021
eebf456
Add an exposed entry into the shape parser
ChrisEPhifer Apr 21, 2021
15da3f8
Add helper to augment permission environments with `SomeNamedShape`s
ChrisEPhifer Apr 21, 2021
d0bfc29
RsConvert instance for Variant
ChrisEPhifer Apr 22, 2021
7f9d56a
RsConvert instance for many variants
ChrisEPhifer Apr 22, 2021
675412a
Non-recursive enum translation
ChrisEPhifer Apr 22, 2021
71eb7bb
Merge branch 'master' into feature/rust-type-decls
ChrisEPhifer Apr 22, 2021
bafe2ed
Remove duplicate function definition
ChrisEPhifer Apr 22, 2021
f81eae6
Support type vars in Generics conversion
ChrisEPhifer Apr 22, 2021
3fb9931
Delete redundant equation for generics conversion
ChrisEPhifer Apr 22, 2021
fef3066
Inlined some definitions
ChrisEPhifer Apr 22, 2021
adeb367
Add helper for constructing bitvecs of known size
ChrisEPhifer Apr 22, 2021
fd0aca9
Support non-recursive enum variants
ChrisEPhifer Apr 22, 2021
53d300f
Point-free-ify a messy function
ChrisEPhifer Apr 22, 2021
4b0bf17
Helper function to build shape functions from named shapes, fixed con…
ChrisEPhifer Apr 23, 2021
e620cf5
Formatting update
ChrisEPhifer Apr 26, 2021
259c853
Improved failure mode for namedShapeShapeFun
ChrisEPhifer Apr 26, 2021
c5bab3f
Updated conversion of `PathTy` to use new instances
ChrisEPhifer Apr 26, 2021
6665202
Fix bug with uninhabited enums / extra empty disjunct
ChrisEPhifer Apr 27, 2021
1b9b072
Update rust_data examples to use new Rust type machinery
ChrisEPhifer Apr 27, 2021
8e24f71
Add Haddock for recursive type decider
ChrisEPhifer Apr 29, 2021
15c2226
Renamed/redocumented the Rust type declaration parser
ChrisEPhifer Apr 29, 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
18 changes: 9 additions & 9 deletions examples/rust_data.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,10 @@ heapster_define_llvmshape env "u32" 64 "" "fieldsh(32,int32<>)";
heapster_define_llvmshape env "bool" 64 "" "fieldsh(1,int1<>)";

// Result type
heapster_define_llvmshape env "Result" 64 "X:llvmshape 64, Y:llvmshape 64" "(fieldsh(eq(llvmword(0)));X) orsh (fieldsh(eq(llvmword(1)));Y)";
heapster_define_rust_type env "pub enum Result<X,Y> { Ok (X), Err (Y) }";

// Sum type
heapster_define_llvmshape env "Sum" 64 "X:llvmshape 64, Y:llvmshape 64" "(fieldsh(eq(llvmword(0)));X) orsh (fieldsh(eq(llvmword(1)));Y)";
heapster_define_rust_type env "pub enum Sum<X,Y> { Left (X), Right (Y) }";

// List type
heapster_define_llvmshape env "List" 64 "L:perm(llvmptr 64),X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;fieldsh(L))";
Expand All @@ -31,17 +31,17 @@ heapster_define_recursive_perm env "ListPerm" "X:llvmshape 64, Xlen:bv 64, rw:rw
heapster_define_llvmshape env "String" 64 "" "exsh cap:bv 64. ptrsh(arraysh(cap,1,[(8,int8<>)]));fieldsh(int64<>);fieldsh(eq(llvmword(cap)))";

// The TwoValues, ThreeValues, FourValues, and FiveValues types
heapster_define_llvmshape env "TwoValues" 64 "" "fieldsh(32,int32<>);fieldsh(32,int32<>)";
heapster_define_llvmshape env "ThreeValues" 64 "" "fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>)";
heapster_define_llvmshape env "FourValues" 64 "" "fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>)";
heapster_define_llvmshape env "FiveValues" 64 "" "fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>);fieldsh(32,int32<>)";
heapster_define_rust_type env "pub struct TwoValues(u32,u32);";
heapster_define_rust_type env "pub struct ThreeValues(u32,u32,u32);";
heapster_define_rust_type env "pub struct FourValues(u32,u32,u32,u32);";
heapster_define_rust_type env "pub struct FiveValues(u32,u32,u32,u32,u32);";

// MixedStruct type
heapster_define_llvmshape env "MixedStruct" 64 "" "String<>;fieldsh(64,int64<>);fieldsh(64,int64<>)";
// heapster_define_llvmshape env "MixedStruct" 64 "" "String<>;fieldsh(64,int64<>);fieldsh(64,int64<>)";
heapster_define_rust_type env "pub struct MixedStruct { pub s: String, pub i1: u64, pub i2: u64, }";

// TrueEnum type
heapster_define_llvmshape env "TrueEnum" 64 "" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)))) orsh (fieldsh(eq(llvmword(2))))";

heapster_define_rust_type env "pub enum TrueEnum { Foo, Bar, Baz }";

/***
*** Assumed Functions
Expand Down
Loading