-
Notifications
You must be signed in to change notification settings - Fork 275
L1 renaming at each declaration #3980
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
Merged
Merged
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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
This file contains hidden or 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
int g; | ||
|
||
int main() | ||
{ | ||
for(int i = 0; i < 4; ++i) | ||
{ | ||
int *x; | ||
*&x = &g; | ||
} | ||
} |
This file contains hidden or 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
main.c | ||
--pointer-check | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
^warning: ignoring |
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
This file contains hidden or 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include "goto_symex.h" | ||
|
||
#include <cassert> | ||
|
||
#include <util/std_expr.h> | ||
|
||
#include <pointer-analysis/add_failed_symbols.h> | ||
|
@@ -23,9 +21,6 @@ void goto_symext::symex_dead(statet &state) | |
|
||
const code_deadt &code = instruction.get_dead(); | ||
|
||
// We increase the L2 renaming to make these non-deterministic. | ||
// We also prevent propagation of old values. | ||
|
||
ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns); | ||
|
||
// in case of pointers, put something into the value set | ||
|
@@ -43,10 +38,13 @@ void goto_symext::symex_dead(statet &state) | |
|
||
const irep_idt &l1_identifier = ssa.get_identifier(); | ||
|
||
// prevent propagation | ||
// we cannot remove the object from the L1 renaming map, because L1 renaming | ||
// information is not local to a path, but removing it from the propagation | ||
// map is safe as 1) it is local to a path and 2) this instance can no longer | ||
// appear | ||
state.propagation.erase(l1_identifier); | ||
|
||
// L2 renaming | ||
// increment the L2 index to ensure a merge on join points will propagate the | ||
// value for branches that are still live | ||
auto level2_it = state.level2.current_names.find(l1_identifier); | ||
if(level2_it != state.level2.current_names.end()) | ||
symex_renaming_levelt::increase_counter(level2_it); | ||
|
This file contains hidden or 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
This file contains hidden or 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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected] | |
static void locality( | ||
const irep_idt &function_identifier, | ||
goto_symext::statet &state, | ||
path_storaget &path_storage, | ||
const goto_functionst::goto_functiont &goto_function, | ||
const namespacet &ns); | ||
|
||
|
@@ -307,7 +308,7 @@ void goto_symext::symex_function_call_code( | |
framet &frame = state.call_stack().new_frame(state.source); | ||
|
||
// preserve locality of local variables | ||
locality(identifier, state, goto_function, ns); | ||
locality(identifier, state, path_storage, goto_function, ns); | ||
|
||
// assign actuals to formal parameters | ||
parameter_assignments(identifier, goto_function, state, arguments); | ||
|
@@ -383,68 +384,27 @@ void goto_symext::symex_end_of_function(statet &state) | |
pop_frame(state); | ||
} | ||
|
||
/// preserves locality of local variables of a given function by applying L1 | ||
/// renaming to the local identifiers | ||
/// Preserves locality of parameters of a given function by applying L1 | ||
/// renaming to them. | ||
static void locality( | ||
const irep_idt &function_identifier, | ||
goto_symext::statet &state, | ||
path_storaget &path_storage, | ||
const goto_functionst::goto_functiont &goto_function, | ||
const namespacet &ns) | ||
{ | ||
unsigned &frame_nr= | ||
state.threads[state.source.thread_nr].function_frame[function_identifier]; | ||
frame_nr++; | ||
|
||
std::set<irep_idt> local_identifiers; | ||
|
||
get_local_identifiers(goto_function, local_identifiers); | ||
|
||
framet &frame = state.call_stack().top(); | ||
|
||
for(std::set<irep_idt>::const_iterator | ||
it=local_identifiers.begin(); | ||
it!=local_identifiers.end(); | ||
it++) | ||
for(const auto ¶m : goto_function.parameter_identifiers) | ||
{ | ||
// get L0 name | ||
ssa_exprt ssa = | ||
state.rename_ssa<L0>(ssa_exprt{ns.lookup(*it).symbol_expr()}, ns); | ||
const irep_idt l0_name=ssa.get_identifier(); | ||
|
||
// save old L1 name for popping the frame | ||
auto c_it = state.level1.current_names.find(l0_name); | ||
|
||
if(c_it != state.level1.current_names.end()) | ||
{ | ||
frame.old_level1.emplace(l0_name, c_it->second); | ||
c_it->second = std::make_pair(ssa, frame_nr); | ||
} | ||
else | ||
{ | ||
c_it = state.level1.current_names | ||
.emplace(l0_name, std::make_pair(ssa, frame_nr)) | ||
.first; | ||
} | ||
|
||
// do L1 renaming -- these need not be unique, as | ||
// identifiers may be shared among functions | ||
// (e.g., due to inlining or other code restructuring) | ||
|
||
ssa_exprt ssa_l1 = state.rename_ssa<L1>(std::move(ssa), ns); | ||
|
||
irep_idt l1_name = ssa_l1.get_identifier(); | ||
unsigned offset=0; | ||
|
||
while(state.l1_history.find(l1_name)!=state.l1_history.end()) | ||
{ | ||
symex_renaming_levelt::increase_counter(c_it); | ||
++offset; | ||
ssa_l1.set_level_1(frame_nr + offset); | ||
l1_name = ssa_l1.get_identifier(); | ||
} | ||
state.rename_ssa<L0>(ssa_exprt{ns.lookup(param).symbol_expr()}, ns); | ||
|
||
// now unique -- store | ||
frame.local_objects.insert(l1_name); | ||
state.l1_history.insert(l1_name); | ||
const std::size_t fresh_l1_index = | ||
path_storage.get_unique_index(ssa.get_identifier(), frame_nr); | ||
state.add_object(ssa, fresh_l1_index, ns); | ||
} | ||
} |
This file contains hidden or 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
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It looks like we could avoid the
if
condition if the function is always called with the same minimum index, I don't know if that's always the case.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, even right now we (intentionally) use
0
for L1 indices when setting up new threads, but elsewhere use1
. And also that facility is rather general, we could as well use it for non-det counters any maybe others.