Types for ebpf #1
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 16 commits
March 9, 2022 10:44
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Abstract transformers for assignment and memory instruction implemented; Join not implemented yet Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
created a testcase for type_domain; moved functionality from ebpf_proof to testcase/type_domain; edited CMakeLists to run new testcase Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
better error prints; refactoring; more refactoring and testing needed Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
fixed issues with join; refactored Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…ilds; attempting to fix Github Actions build Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
caballa
requested changes
Mar 23, 2022
src/crab/type_domain.hpp
Outdated
| ptr_no_off_t(region _r) : r(_r) {} | ||
| ptr_no_off_t(const ptr_no_off_t& p) : r(p.r) {} | ||
|
|
||
| friend bool operator==(const ptr_no_off_t& p1, const ptr_no_off_t& p2) { |
There was a problem hiding this comment.
This is required when I am comparing two ptr_t objects, where ptr_t = std::variant<ptr_no_off_t, ptr_with_off_t>. It does not allow operator== to be a member method for ptr_no_off_t (and ptr_with_off_t) but requires to pass both objects as arguments. May be I am mistaken and there's a way to resolve that. Please suggest if you know.
There was a problem hiding this comment.
You can specialize std::equals_to (similar to what you do with std::hash).
I assume that std::variant really calls to std::equals_to which in turn, it calls to operator== if there is no specialization.
There was a problem hiding this comment.
I am having issues with this, as std::equal_to is not being called even after specialization. Not sure what would be the actual fix because google doesn't provide much resources on it. I will commit the code so may be someone can comment on it
added 4 commits
March 25, 2022 04:38
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…into type-proofs
removed temporary tests Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
caballa
reviewed
Mar 28, 2022
caballa
reviewed
Mar 28, 2022
added 4 commits
March 28, 2022 22:39
implemented required features for type_domain_t to be used as an abstract_domain_t; printing types after each statement that is supported; Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Fixed printing of types; Refactoring Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
added 2 commits
March 29, 2022 21:22
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
this can be changed later to call each domain separately, but for now it was not feasible to have half implemented sub-domains; added functionality to forget registers when needed Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
without print_invariants option, print only initial types and for each bb, minimal types; with print_invariants option, print pre- and post-types for each bb in addition; refactoring Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
… joining two domains, only one was being joined with itself; fixed issue with adjusting of basic block labels for types -- location comparisons were done after updating values, which caused issues with reading correct types; reverting back printing of pre-types and post-types -- printing pre-types is tricky because we do not have basic block label yet while we start printing (we always adjusted types after we started to read basic blocks), hence printing pre-types is not feasible Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
refactored code Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
remove extra prints Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
handled operations in Bin other than add, subtract or move; added support for recording key_size and value_size for a map; added support for ValidMapKeyValue assertion -- a few assertions still need fixing because still haven't added support for recoding width of a stack store, and some other issues Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
… -- need the same for pointers; a little refactoring in offset_domain class; a small fix when handling Call in type_domain/interval_prop_domain Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
… printing; some refactoring in region_domain and interval_domain Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Fixed storing intervals and forgetting locations into stack, and fixed loading of intervals from stack Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…pport for packet access checks once meta pointers are supported; added extra checks when loading numbers Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
refactoring of code in Offset_domain Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
refactoring in region_domain.cpp and interval_prop_domain.cpp Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Added the check for packet access in the ValidMapKeyValue assertion; Refactored a bit Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
it is a conservative fix that allows us to assume that if we have a packet constraint like , where is a slack variable, then is at least far from (rather than being far from ); it is imprecise assumption but sound Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…egions; Added relevant checks for assertions and any required functionality; shared pointer is now a pointer with offset, not a pointer with no offsets Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
previously mapfd passed the check of a pointer, which should not happen Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…issing before Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
…is not known Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@my.fsu.edu>
This also resolves many map key value assertion fails that occurred due to misreading values from the stack Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Remove extra print statements Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
…ntegers; stack and context keys changed to uint64_t from int; respective valid_access checks and store and load operations updated; Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
it reported that cannot store a pointer into shared, although only number was being stored Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Since now we have offsets as intervals, we still have a ptr_with_off_t when we do not know the exact offset, hence we do not create a ptr_no_off_t anymore, we are simplifying a lot of checks; Refactoring some code based on changes done Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Limited support for handling intervals (assuming rhs is singleton) when 'assume' instruction encountered; Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Support for binary operations on pointers, of form 'num op ptr'; A much better handling of binary operations for all domains, with added multiple sanity checks; TODO: precise handling of subtraction for packet pointers (rest are precise) Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
…do not have a fixed offset; changed ctx indices from int to uint64_t; Signed-off-by: Ameer Hamza <ah18r@fsu.edu>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Signed-off-by: Ameer Hamza ah18r@my.fsu.edu