Tolerate stub static fields defined on non-stub types

Normally this situation (a reference to static field A.x, when neither A
nor any of its ancestors either define a field x or are opaque stubs) would
be an error, probably indicating a class version mismatch, but at present some
of our library models intentionally exploit this behaviour to obtain a nondet-
initialised field. Therefore for the time being we tolerate the situation,
initialising such fields in __CPROVER_initialize, as we cannot attach a synthetic
clinit method to a non-stub type.

Author: smowton

src/java_bytecode/java_bytecode_language.cpp

@@ -390,12 +390,17 @@ static void generate_constant_global_variables(
 /// \param symbol_basename: new symbol basename
 /// \param symbol_type: new symbol type
 /// \param class_id: class id that directly encloses this static field
+/// \param force_nondet_init: if true, always leave the symbol's value nil so it
+///   gets nondet initialised during __CPROVER_initialize. Otherwise, pointer-
+///   typed globals are initialised null and we expect a synthetic clinit method
+///   to be created later.
 static void create_stub_global_symbol(
   symbol_table_baset &symbol_table,
   const irep_idt &symbol_id,
   const irep_idt &symbol_basename,
   const typet &symbol_type,
-  const irep_idt &class_id)
+  const irep_idt &class_id,
+  bool force_nondet_init)
 {
   symbolt new_symbol;
   new_symbol.is_static_lifetime = true;
@@ -415,7 +420,7 @@ static void create_stub_global_symbol(
   // If pointer-typed, initialise to null and a static initialiser will be
   // created to initialise on first reference. If primitive-typed, specify
   // nondeterministic initialisation by setting a nil value.
-  if(symbol_type.id() == ID_pointer)
+  if(symbol_type.id() == ID_pointer && !force_nondet_init)
     new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type));
   else
     new_symbol.value.make_nil();
@@ -454,7 +459,7 @@ static irep_idt get_any_incomplete_ancestor(
       classes_to_check.end(), parents.begin(), parents.end());
   }
 
-  INVARIANT(false, "input class id should have some incomplete ancestor");
+  return irep_idt();
 }
 
 /// Search for getstatic and putstatic instructions in a class' bytecode and
@@ -464,10 +469,13 @@ static irep_idt get_any_incomplete_ancestor(
 /// \param parse_tree: class bytecode
 /// \param symbol_table: symbol table; may gain new symbols
 /// \param class_hierarchy: global class hierarchy
+/// \param log: message handler used to log warnings when stub static fields are
+///   found belonging to non-stub classes.
 static void create_stub_global_symbols(
   const java_bytecode_parse_treet &parse_tree,
   symbol_table_baset &symbol_table,
-  const class_hierarchyt &class_hierarchy)
+  const class_hierarchyt &class_hierarchy,
+  messaget &log)
 {
   namespacet ns(symbol_table);
   for(const auto &method : parse_tree.parsed_class.methods)
@@ -507,6 +515,28 @@ static void create_stub_global_symbols(
             get_any_incomplete_ancestor(
               class_id, symbol_table, class_hierarchy);
 
+          // If there are no incomplete ancestors to ascribe the missing field
+          // to, we must have an incomplete model of a class or simply a
+          // version mismatch of some kind. Normally this would be an error, but
+          // our models library currently triggers this error in some cases
+          // (notably java.lang.System, which is missing System.in/out/err).
+          // Therefore for this case we ascribe the missing field to the class
+          // it was directly referenced from, and fall back to initialising the
+          // field in __CPROVER_initialize, rather than try to create or augment
+          // a clinit method for a non-stub class.
+
+          bool no_incomplete_ancestors = add_to_class_id.empty();
+          if(no_incomplete_ancestors)
+          {
+            add_to_class_id = class_id;
+
+            // TODO forbid this again once the models library has been checked
+            // for missing static fields.
+            log.warning() << "Stub static field " << component << " found for "
+                          << "non-stub type " << class_id << ". In future this "
+                          << "will be a fatal error." << messaget::eom;
+          }
+
           irep_idt identifier =
             id2string(add_to_class_id) + "." + id2string(component);
 
@@ -515,7 +545,8 @@ static void create_stub_global_symbols(
             identifier,
             component,
             instruction.args[0].type(),
-            add_to_class_id);
+            add_to_class_id,
+            no_incomplete_ancestors);
         }
       }
     }
@@ -637,7 +668,7 @@ bool java_bytecode_languaget::typecheck(
     for(const auto &c : java_class_loader.class_map)
     {
       create_stub_global_symbols(
-        c.second, symbol_table_journal, class_hierarchy);
+        c.second, symbol_table_journal, class_hierarchy, *this);
     }
 
     stub_global_initializer_factory.create_stub_global_initializer_symbols(

src/java_bytecode/java_entry_point.cpp

@@ -118,6 +118,8 @@ static void java_static_lifetime_init(
             allow_null=false;
           if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
+          if(allow_null && is_non_null_library_global(nameid))
+            allow_null = false;
         }
         gen_nondet_init(
           sym.symbol_expr(),

src/java_bytecode/java_static_initializers.cpp

@@ -8,6 +8,7 @@ Author: Chris Smowton, [email protected]
 
 #include "java_static_initializers.h"
 #include "java_object_factory.h"
+#include "java_utils.h"
 #include <goto-programs/class_hierarchy.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
@@ -266,8 +267,20 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
   // Populate map from class id -> stub globals:
   for(const irep_idt &stub_global : stub_globals_set)
   {
+    const symbolt &global_symbol = symbol_table.lookup_ref(stub_global);
+    if(global_symbol.value.is_nil())
+    {
+      // This symbol is already nondet-initialised during __CPROVER_initialize
+      // (generated in java_static_lifetime_init). In future this will only
+      // be the case for primitive-typed fields, but for now reference-typed
+      // fields can also be treated this way in the exceptional case that they
+      // belong to a non-stub class. Skip the field, as it does not need a
+      // synthetic static initializer.
+      continue;
+    }
+
     const irep_idt class_id =
-      symbol_table.lookup_ref(stub_global).type.get(ID_C_class);
+      global_symbol.type.get(ID_C_class);
     INVARIANT(
       !class_id.empty(),
       "static field should be annotated with its defining class");
@@ -283,6 +296,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
   {
     const irep_idt static_init_name = clinit_function_name(it->first);
 
+    INVARIANT(
+      symbol_table.lookup_ref(it->first).type.get_bool(ID_incomplete_class),
+      "only incomplete classes should be given synthetic static initialisers");
     INVARIANT(
       !symbol_table.has_symbol(static_init_name),
       "a class cannot be both incomplete, and so have stub static fields, and "
@@ -315,20 +331,6 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
   }
 }
 
-/// Check if a symbol is a well-known non-null global
-/// \param symbolid: symbol id to check
-/// \return true if this static field is known never to be null
-static bool is_non_null_library_global(const irep_idt &symbolid)
-{
-  static const std::unordered_set<irep_idt, irep_id_hash> non_null_globals =
-  {
-    "java::java.lang.System.out",
-    "java::java.lang.System.err",
-    "java::java.lang.System.in"
-  };
-  return non_null_globals.count(symbolid);
-}
-
 /// Create the body of a synthetic static initializer (clinit method),
 /// which initialise stub globals in the same manner as
 /// java_static_lifetime_init, only delayed until first reference by virtue of

src/java_bytecode/java_static_initializers.h

@@ -31,8 +31,9 @@ codet get_clinit_wrapper_body(
 class stub_global_initializer_factoryt
 {
   /// Maps class symbols onto the stub globals that belong to them
-  std::unordered_multimap<irep_idt, irep_idt, irep_id_hash>
-    stub_globals_by_class;
+  typedef std::unordered_multimap<irep_idt, irep_idt, irep_id_hash>
+    stub_globals_by_classt;
+  stub_globals_by_classt stub_globals_by_class;
 
 public:
   void create_stub_global_initializer_symbols(

src/java_bytecode/java_utils.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_utils.h>
 
 #include <set>
+#include <unordered_set>
 
 bool java_is_array_type(const typet &type)
 {
@@ -413,3 +414,17 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
     return resolve_inherited_componentt::inherited_componentt();
   }
 }
+
+/// Check if a symbol is a well-known non-null global
+/// \param symbolid: symbol id to check
+/// \return true if this static field is known never to be null
+bool is_non_null_library_global(const irep_idt &symbolid)
+{
+  static const std::unordered_set<irep_idt, irep_id_hash> non_null_globals =
+  {
+    "java::java.lang.System.out",
+    "java::java.lang.System.err",
+    "java::java.lang.System.in"
+  };
+  return non_null_globals.count(symbolid);
+}

src/java_bytecode/java_utils.h

@@ -106,4 +106,6 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
   const class_hierarchyt &class_hierarchy,
   bool include_interfaces);
 
+bool is_non_null_library_global(const irep_idt &);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H