Shadow memory initialization functions #7836
Merged
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
esteffin
force-pushed
the
esteffin/shadow-memory-init
branch
2 times, most recently
from
5dd8480
to
3bf8f24
Compare
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7836 +/- ##
=========================================
Coverage 78.79% 78.80%
=========================================
Files 1698 1698
Lines 194641 194745 +104
=========================================
+ Hits 153374 153467 +93
- Misses 41267 41278 +11
☔ View full report in Codecov by Sentry. |
| symbol.is_auxiliary) || | ||
| !symbol.is_static_lifetime) | ||
| return; | ||
| if(id2string(symbol.name).find("__cs_") != std::string::npos) |
There was a problem hiding this comment.
This case needs to be handled by some future filter option. I'd remove it for now.
There was a problem hiding this comment.
We added a TODO comment saying that the filtering will be done when the last functionalities are added, so we will have more confidence that we are not adding regressions.
| { | ||
| return; | ||
| } | ||
| if(symbol_name.find("__cs_") != std::string::npos) |
There was a problem hiding this comment.
Same here (filter option).
| symbol_name.find("::return_value") == std::string::npos) | ||
| return; | ||
| if( | ||
| symbol_name.find("malloc::") != std::string::npos && |
There was a problem hiding this comment.
These filters should be made more precise.
esteffin
force-pushed
the
esteffin/shadow-memory-init
branch
from
3bf8f24
to
8f57405
Compare
Clean the given pointer expression so that it has the right shape for being used for identifying shadow memory. This handles some quirks regarding array sizes containing L2 symbols and string constants not having char-pointer type.
Allocates shadows for a given original memory for each declared field. The shadows are registered in the shadow_memory_state (part of goto_symex_statet to consider scoping of local shadows). In the next step this functionality is used to allocate shadow memory for the original memory allocations encountered when symexing a goto model.
This commit adds the implementation to the 4 shadow memory user-facing initialization functions. Namely: - shadow_memoryt::symex_field_static_init - shadow_memoryt::symex_field_static_init_string_constant - shadow_memoryt::symex_field_local_init - shadow_memoryt::symex_field_dynamic_init
esteffin
force-pushed
the
esteffin/shadow-memory-init
branch
from
8f57405
to
4f5df20
Compare
peterschrammel
approved these changes
Aug 7, 2023
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.
PR adding implementation for the Shadow memory initialization functions.
Unit tests will be added when the remaining components will be added.