Fix static lifetime pointer initialization dependency ordering

regression/cbmc/static_init_chain/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+// Test case for chained static initialization dependencies
+// Tests: A -> B -> C dependency chain
+//
+// According to C standard (C99/C11):
+// - Section 6.7.9 paragraph 4: All expressions in an initializer for an
+//   object that has static storage duration shall be constant expressions.
+// - Section 6.6 paragraph 9: An address constant is a pointer to an lvalue
+//   designating an object of static storage duration.
+//
+// This means c_int must be initialized before b_ptr (which points to it),
+// and b_ptr must be initialized before a_ptr_ptr (which points to it).
+
+static int c_int = 42;
+static int *b_ptr = &c_int;
+static int **a_ptr_ptr = &b_ptr;
+
+int main()
+{
+  // Verify the entire chain is correctly initialized
+  assert(a_ptr_ptr != 0);
+  assert(*a_ptr_ptr != 0);
+  assert(**a_ptr_ptr == 42);
+
+  // Verify pointer values are correct
+  assert(*a_ptr_ptr == b_ptr);
+  assert(**a_ptr_ptr == c_int);
+
+  return 0;
+}

regression/cbmc/static_init_chain/test.desc

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

regression/cbmc/static_pointer_init_order/main.c

@@ -0,0 +1,33 @@
+#include <assert.h>
+#include <stdint.h>
+#include <string.h>
+
+#define PACKETBUF_SIZE 128
+
+// Test case for GitHub issue #8593
+// When a pointer is initialized outside a function with a cast expression
+// pointing to another static storage duration object, CBMC should properly
+// handle the dependency and not mark the pointer as invalid.
+
+static uint32_t packetbuf_aligned[(PACKETBUF_SIZE + 3) / 4];
+// This pointer initialization depends on packetbuf_aligned being initialized first
+uint8_t *packetbuf = (uint8_t *)packetbuf_aligned;
+
+int main()
+{
+  uint16_t channelId = 0x1234;
+  uint8_t *data = packetbuf;
+
+  // This should not fail - data should point to valid memory
+  assert(data != 0);
+
+  // Write some data
+  memcpy(data, &channelId, 2);
+
+  // Verify the data was written correctly
+  uint16_t result;
+  memcpy(&result, data, 2);
+  assert(result == channelId);
+
+  return 0;
+}

regression/cbmc/static_pointer_init_order/test.desc

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

src/linking/static_lifetime_init.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/find_symbols.h>
 #include <util/namespace.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
@@ -22,6 +23,130 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <set>
 
+using dependency_mapt =
+  std::unordered_map<irep_idt, std::unordered_set<irep_idt>>;
+
+/// Build a dependency graph for static lifetime objects.
+/// Returns a map from symbol identifier to the set of identifiers it depends
+/// on.  According to C standard (C99/C11 Section 6.7.9 and 6.6 paragraph 9):
+/// - Objects with static storage duration can be initialized with constant
+///   expressions or string literals
+/// - An address constant is a pointer to an lvalue designating an object of
+///   static storage duration
+/// - When a static object's initializer references another static object,
+///   that referenced object must be initialized first to maintain proper
+///   initialization order
+static dependency_mapt build_static_initialization_dependencies(
+  const std::set<std::string> &symbols,
+  const namespacet &ns)
+{
+  dependency_mapt dependencies;
+
+  for(const std::string &id : symbols)
+  {
+    const symbolt &symbol = ns.lookup(id);
+
+    // Only track dependencies for objects with static lifetime that have
+    // initializers
+    if(
+      !symbol.is_static_lifetime || symbol.is_type || symbol.is_macro ||
+      symbol.type.id() == ID_code || symbol.type.id() == ID_empty)
+    {
+      continue;
+    }
+
+    // Skip if no initializer or nondet initializer
+    if(
+      symbol.value.is_nil() ||
+      (symbol.value.id() == ID_side_effect &&
+       to_side_effect_expr(symbol.value).get_statement() == ID_nondet))
+    {
+      continue;
+    }
+
+    // Find all symbols referenced in the initializer
+    find_symbols_sett referenced_symbols =
+      find_symbol_identifiers(symbol.value);
+
+    // Add dependencies on other static lifetime objects
+    for(const irep_idt &ref_id : referenced_symbols)
+    {
+      // Skip self-references
+      if(ref_id == symbol.name)
+        continue;
+
+      // Check if the referenced symbol is in our set of symbols to initialize
+      if(symbols.find(id2string(ref_id)) == symbols.end())
+        continue;
+
+      // Verify it's a static lifetime object
+      if(ns.lookup(ref_id).is_static_lifetime)
+        dependencies[symbol.name].insert(ref_id);
+    }
+  }
+
+  return dependencies;
+}
+
+/// Perform a topological sort on symbols considering their initialization
+/// dependencies. Returns a vector of symbol identifiers in initialization
+/// order. Uses alphabetical ordering as a tiebreaker for reproducibility.
+static std::vector<irep_idt> topological_sort_with_dependencies(
+  const std::set<std::string> &symbols,
+  const dependency_mapt &dependencies)
+{
+  std::vector<irep_idt> result;
+  std::unordered_set<irep_idt> visited;
+  std::unordered_set<irep_idt> in_progress; // For cycle detection
+
+  // Recursive helper function for depth-first search
+  std::function<void(const irep_idt &)> visit = [&](const irep_idt &id)
+  {
+    // If already visited, nothing to do
+    if(visited.find(id) != visited.end())
+      return;
+
+    // Check for cycles (should not happen in valid code)
+    if(!in_progress.insert(id).second)
+    {
+      // Cycle detected - this indicates an error in the source code
+      // For now, we'll just continue to avoid infinite recursion
+      return;
+    }
+
+    // Visit all dependencies first
+    auto dep_it = dependencies.find(id);
+    if(dep_it != dependencies.end())
+    {
+      // Sort dependencies alphabetically for reproducibility
+      std::set<std::string> sorted_deps;
+      for(const irep_idt &dep : dep_it->second)
+      {
+        sorted_deps.insert(id2string(dep));
+      }
+
+      for(const std::string &dep : sorted_deps)
+      {
+        // Only visit if it's in our symbol set
+        if(symbols.find(dep) != symbols.end())
+          visit(dep);
+      }
+    }
+
+    in_progress.erase(id);
+    visited.insert(id);
+    result.push_back(id);
+  };
+
+  // Process all symbols in alphabetical order for reproducibility
+  for(const std::string &id : symbols)
+  {
+    visit(id);
+  }
+
+  return result;
+}
+
 static std::optional<codet> static_lifetime_init(
   const irep_idt &identifier,
   symbol_table_baset &symbol_table)
@@ -116,31 +241,65 @@ void static_lifetime_init(
 
   // do assignments based on "value"
 
-  // sort alphabetically for reproducible results
+  // Build dependency graph for static lifetime initialization.
+  // According to the C standard (C99/C11):
+  // - Section 6.7.9 paragraph 4: All expressions in an initializer for an
+  //   object that has static storage duration shall be constant expressions
+  //   or string literals.
+  // - Section 6.6 paragraph 9: An address constant is a null pointer, a pointer
+  //   to an lvalue designating an object of static storage duration, or a
+  //   pointer to a function designator.
+  // - Section 6.2.4: Objects with static storage duration are initialized
+  //   before program startup.
+  //
+  // When one static object's initializer takes the address of another static
+  // object, the referenced object must be initialized first to ensure the
+  // address constant is properly available.
+
+  // First, collect all symbols and sort alphabetically for reproducible results
   std::set<std::string> symbols;
 
   for(const auto &symbol_pair : symbol_table.symbols)
   {
     symbols.insert(id2string(symbol_pair.first));
   }
 
-  // first do framework variables
+  // Build dependency graph
+  auto dependencies = build_static_initialization_dependencies(symbols, ns);
+
+  // Separate CPROVER framework variables from user variables
+  std::set<std::string> cprover_symbols;
+  std::set<std::string> user_symbols;
+
   for(const std::string &id : symbols)
+  {
     if(has_prefix(id, CPROVER_PREFIX))
-    {
-      auto code = static_lifetime_init(id, symbol_table);
-      if(code.has_value())
-        dest.add(std::move(*code));
-    }
+      cprover_symbols.insert(id);
+    else
+      user_symbols.insert(id);
+  }
 
-  // now all other variables
-  for(const std::string &id : symbols)
-    if(!has_prefix(id, CPROVER_PREFIX))
-    {
-      auto code = static_lifetime_init(id, symbol_table);
-      if(code.has_value())
-        dest.add(std::move(*code));
-    }
+  // First initialize framework variables with topological sort
+  std::vector<irep_idt> sorted_cprover =
+    topological_sort_with_dependencies(cprover_symbols, dependencies);
+
+  for(const auto &id : sorted_cprover)
+  {
+    auto code = static_lifetime_init(id, symbol_table);
+    if(code.has_value())
+      dest.add(std::move(*code));
+  }
+
+  // Now initialize all other variables with topological sort
+  std::vector<irep_idt> sorted_user =
+    topological_sort_with_dependencies(user_symbols, dependencies);
+
+  for(const auto &id : sorted_user)
+  {
+    auto code = static_lifetime_init(id, symbol_table);
+    if(code.has_value())
+      dest.add(std::move(*code));
+  }
 
   // now call designated "initialization" functions