Merge pull request #3752 from JohnDumbell/jd/enhancement/phi_merge_explicit_exclude_extern

Tighten up global extern detection in phi_function

Author: tautschnig

jbmc/regression/jbmc/phi-merge_uninitialized_values/field.desc

@@ -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:

jbmc/regression/jbmc/phi-merge_uninitialized_values/local.desc

@@ -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:

jbmc/regression/jbmc/phi-merge_uninitialized_values/static_field.desc

@@ -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:

regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

@@ -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:

regression/cbmc/phi-merge_uninitialized_values/global.desc

@@ -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:

regression/cbmc/phi-merge_uninitialized_values/local.desc

@@ -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:

regression/cbmc/phi-merge_uninitialized_values/static_local.desc

@@ -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:

src/goto-symex/symex_goto.cpp

@@ -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;
   }