Fix symex of functions that may throw

jbmc/regression/jbmc/throwing-function-return-value/Test.java

@@ -0,0 +1,49 @@
+public class Test {
+
+  public static Test f(boolean unknown) throws Exception {
+
+    if(unknown)
+      throw new Exception();
+    else
+      return new Test();
+
+  }
+
+  public static void main(boolean unknown) {
+
+    Sub s = new Sub(); // Make sure Sub is loaded
+    int x = 0;
+
+    // The routine below is repeated twice because historically symex could
+    // behave differently the first and second times a may-throw function was
+    // called.
+
+    try {
+      Test t1 = f(unknown);
+      t1.f();
+      x += t1.g();
+    }
+    catch(Exception e) { }
+
+    try {
+      Test t2 = f(unknown);
+      t2.f();
+      x += t2.g();
+    }
+    catch(Exception e) { }
+
+    assert x == 10;
+
+  }
+
+  public void f() { }
+  public int g() { return 5; }
+
+}
+
+class Sub extends Test {
+
+  public void f() { }
+  public int g() { return 0; }
+
+}

jbmc/regression/jbmc/throwing-function-return-value/test.desc

@@ -0,0 +1,18 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
+java::Test\.main:\(Z\)V::9::x!0@1#\d+ = 5 \+ java::Test\.main:\(Z\)V::9::x!0@1#\d+
+^EXIT=0$
+^SIGNAL=0$
+--
+return_value!0#0
+java::Sub\.g:\(\)
+--
+This checks that when a function may throw, we can nonetheless constant-propagate
+and populate the value-set for the normal-return path. In particular we don't
+expect to see any reference to a zero-generation return value (indicating
+reading the return-value when not defined), nor do we expect to see any code
+from the Sub class, which is not accessible and can only be reached when
+constant propagation has lost information to the point we're not sure which type
+virtual calls against Test may find.

src/goto-symex/symex_dead.cpp

@@ -22,26 +22,13 @@ void goto_symext::symex_dead(statet &state)
   const code_deadt &code = instruction.get_dead();
 
   ssa_exprt ssa = state.rename_ssa<L1>(ssa_exprt{code.symbol()}, ns);
-
-  // in case of pointers, put something into the value set
-  if(code.symbol().type().id() == ID_pointer)
-  {
-    exprt rhs;
-    if(auto failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns))
-      rhs = address_of_exprt(*failed, to_pointer_type(code.symbol().type()));
-    else
-      rhs=exprt(ID_invalid);
-
-    const exprt l1_rhs = state.rename<L1>(std::move(rhs), ns);
-    state.value_set.assign(ssa, l1_rhs, ns, true, false);
-  }
-
   const irep_idt &l1_identifier = ssa.get_identifier();
 
   // 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
+  // map and value-set is safe as 1) it is local to a path and 2) this instance
+  // can no longer appear
+  state.value_set.values.erase(l1_identifier);
   state.propagation.erase(l1_identifier);
   // increment the L2 index to ensure a merge on join points will propagate the
   // value for branches that are still live

src/goto-symex/symex_goto.cpp

@@ -520,14 +520,10 @@ static void merge_names(
     rhs = goto_state_rhs;
   else if(goto_state.guard.is_false())
     rhs = dest_state_rhs;
-  else if(goto_count == 0 && !symbol.is_static_lifetime)
-  {
+  else if(goto_count == 0)
     rhs = dest_state_rhs;
-  }
-  else if(dest_count == 0 && !symbol.is_static_lifetime)
-  {
+  else if(dest_count == 0)
     rhs = goto_state_rhs;
-  }
   else
   {
     rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);

src/linking/static_lifetime_init.cpp

@@ -53,14 +53,6 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
   if(type.id() == ID_code || type.id() == ID_empty)
     return {};
 
-  // We won't try to initialize any symbols that have
-  // remained incomplete.
-
-  if(symbol.value.is_nil() && symbol.is_extern)
-    // Compilers would usually complain about these
-    // symbols being undefined.
-    return {};
-
   if(type.id() == ID_array && to_array_type(type).size().is_nil())
   {
     // C standard 6.9.2, paragraph 5
@@ -77,14 +69,18 @@ static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
     return {}; // do not initialize
   }
 
-  if(symbol.value.id() == ID_nondet)
-  {
-    return {}; // do not initialize
-  }
-
   exprt rhs;
 
-  if(symbol.value.is_nil())
+  if((symbol.value.is_nil() && symbol.is_extern) ||
+     symbol.value.id() == ID_nondet)
+  {
+    // Nondet initialise if not linked, or if explicitly requested.
+    // Compilers would usually complain about the unlinked symbol case.
+    const auto nondet = nondet_initializer(symbol.type, symbol.location, ns);
+    CHECK_RETURN(nondet.has_value());
+    rhs = *nondet;
+  }
+  else if(symbol.value.is_nil())
   {
     const auto zero = zero_initializer(symbol.type, symbol.location, ns);
     CHECK_RETURN(zero.has_value());