Fix global variable initialisation

External globals (static fields in Java) should have been annotated with the
static_lifetime attribute and consequently initialised with either null, or
an actual instance of the right type. Instead they were given nondet pointers
which could lead to odd results, such as apparently being neither null nor
pointing to something of the expected type. This restores proper initialisation,
and excludes global void* fields (currently only the #exception_value special
returns match this definition)

Author: smowton

regression/cbmc-java/external_getstatic1/test.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/external_getstatic1/test.desc

@@ -0,0 +1,16 @@
+class A
+{
+  public static A external_global;
+  public int i;
+};
+
+public class test
+{
+  public static void main()
+  {
+    if(A.external_global == null)
+      return;
+    A local = A.external_global;
+    assert(local instanceof A);
+  }
+}

regression/cbmc-java/external_getstatic1/test.java

@@ -2014,6 +2014,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const bool is_assertions_disabled_field=
         field_name.find("$assertionsDisabled")!=std::string::npos;
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+
+      // If external, create a symbol table entry for this static field:
+      check_static_field_stub(symbol_expr, field_name);
+
       if(lazy_methods)
       {
         if(arg0.type().id()==ID_symbol)
@@ -2056,6 +2060,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
+
+      // If external, create a symbol table entry for this static field:
+      check_static_field_stub(symbol_expr, field_name);
+
       if(lazy_methods && arg0.type().id()==ID_symbol)
       {
         lazy_methods->add_needed_class(

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -473,6 +473,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
     alloc_type,
     update_in_placet::NO_UPDATE_IN_PLACE);
 
+  auto set_null_inst=get_null_assignment(expr, pointer_type);
+
   // Determine whether the pointer can be null.
   // In particular the array field of a String should not be null.
   bool not_null=
@@ -483,7 +485,18 @@ void java_object_factoryt::gen_nondet_pointer_init(
       class_identifier=="java.lang.CharSequence") &&
      subtype.id()==ID_array);
 
-  if(not_null)
+  // Alternatively, if this is a void* we *must* initialise with null:
+  // (This can currently happen for some cases of #exception_value)
+  bool must_be_null=
+    subtype==empty_typet();
+
+  if(must_be_null)
+  {
+    // Add the following code to assignments:
+    // <expr> = nullptr;
+    new_object_assignments.add(set_null_inst);
+  }
+  else if(not_null)
   {
     // Add the following code to assignments:
     // <expr> = <aoe>;
@@ -500,8 +513,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
     //    <code from recursive call to gen_nondet_init() with
     //             tmp$<temporary_counter>>
     // }
-    auto set_null_inst=get_null_assignment(expr, pointer_type);
-
     code_ifthenelset null_check;
     null_check.cond()=side_effect_expr_nondett(bool_typet());
     null_check.then_case()=set_null_inst;
@@ -900,6 +911,29 @@ void java_object_factoryt::gen_nondet_array_init(
   assignments.move_to_operands(init_done_label);
 }
 
+/// Add code_declt instructions to `init_code` for every non-static symbol
+/// in `symbols_created`
+/// \param symbols_created: list of symbols
+/// \param loc: source location for new code_declt instances
+/// \param [out] init_code: gets code_declt for each symbol
+static void declare_created_symbols(
+  const std::vector<const symbolt *> &symbols_created,
+  const source_locationt &loc,
+  code_blockt &init_code)
+{
+  // Add the following code to init_code for each symbol that's been created:
+  //   <type> <identifier>;
+  for(const symbolt * const symbol_ptr : symbols_created)
+  {
+    if(!symbol_ptr->is_static_lifetime)
+    {
+      code_declt decl(symbol_ptr->symbol_expr());
+      decl.add_source_location()=loc;
+      init_code.add(decl);
+    }
+  }
+}
+
 /// Similar to `gen_nondet_init`, but returns an object expression
 /// rather than assigning to one.
 /// \param type: type of new object to create
@@ -960,17 +994,7 @@ exprt object_factory(
     typet(),
     update_in_placet::NO_UPDATE_IN_PLACE);
 
-  // Add the following code to init_code for each symbol that's been created:
-  //   <type> <identifier>;
-  for(const symbolt * const symbol_ptr : symbols_created)
-  {
-    if(!symbol_ptr->is_static_lifetime)
-    {
-      code_declt decl(symbol_ptr->symbol_expr());
-      decl.add_source_location()=loc;
-      init_code.add(decl);
-    }
-  }
+  declare_created_symbols(symbols_created, loc, init_code);
 
   init_code.append(assignments);
   return object;
@@ -1026,17 +1050,7 @@ void gen_nondet_init(
     typet(),
     update_in_place);
 
-  // Add the following code to init_code for each symbol that's been created:
-  //   <type> <identifier>;
-  for(const symbolt * const symbol_ptr : symbols_created)
-  {
-    if(!symbol_ptr->is_static_lifetime)
-    {
-      code_declt decl(symbol_ptr->symbol_expr());
-      decl.add_source_location()=loc;
-      init_code.add(decl);
-    }
-  }
+  declare_created_symbols(symbols_created, loc, init_code);
 
   init_code.append(assignments);
 }