Skip to content

Tighten up global extern detection in phi_function #3752

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

Merged
merged 2 commits into from
Jan 14, 2019
Merged

Tighten up global extern detection in phi_function #3752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
eca9b59
Narrowing the scope of the global extern phi merge check
JohnDumbell Jan 10, 2019
466ac7a
Loosening regex on phi merge zero generation regression tests
JohnDumbell Jan 10, 2019
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
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/phi-merge_uninitialized_values/dynamic.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+dynamic_object[0-9]+(@[0-9]+)?#0\)
^.*\?\s+dynamic_object[0-9]+(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/phi-merge_uninitialized_values/global.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+global(@[0-9]+)?#0\)
^.*\?\s+global(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/phi-merge_uninitialized_values/local.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+local(@[0-9]+)?#0\)
^.*\?\s+local(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc/phi-merge_uninitialized_values/static_local.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ activate-multi-line-match
^EXIT=0$
^SIGNAL=0$
--
^.*:\s+staticLocal(@[0-9]+)?#0\)
^.*\?\s+staticLocal(@[0-9]+)?#0\s+:
\([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\)
\([^\s]+guard[^\s]+ \? [^\s]+ : [^\s]+#0\)
--
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
statement:
Expand Down
6 changes: 4 additions & 2 deletions src/goto-symex/symex_goto.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -476,15 +476,17 @@ static void merge_names(
// 1. Either guard is false, so we can't follow that branch.
// 2. Either identifier is of generation zero, and so hasn't been
// initialized and therefore an invalid target.

// These rules only apply to dynamic objects and locals.
if(dest_state.guard.is_false())
rhs = goto_state_rhs;
else if(goto_state.guard.is_false())
rhs = dest_state_rhs;
else if(goto_count == 0 && symbol.value.is_not_nil())
else if(goto_count == 0 && !symbol.is_static_lifetime)
{
rhs = dest_state_rhs;
}
else if(dest_count == 0 && symbol.value.is_not_nil())
else if(dest_count == 0 && !symbol.is_static_lifetime)
{
rhs = goto_state_rhs;
}
Expand Down