diff --git a/regression/cbmc/static_init_chain/main.c b/regression/cbmc/static_init_chain/main.c new file mode 100644 index 00000000000..ed4c2bdee81 --- /dev/null +++ b/regression/cbmc/static_init_chain/main.c @@ -0,0 +1,31 @@ +#include + +// 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; +} diff --git a/regression/cbmc/static_init_chain/test.desc b/regression/cbmc/static_init_chain/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/static_init_chain/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/static_pointer_init_order/main.c b/regression/cbmc/static_pointer_init_order/main.c new file mode 100644 index 00000000000..a672a8614cc --- /dev/null +++ b/regression/cbmc/static_pointer_init_order/main.c @@ -0,0 +1,33 @@ +#include +#include +#include + +#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; +} diff --git a/regression/cbmc/static_pointer_init_order/test.desc b/regression/cbmc/static_pointer_init_order/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/static_pointer_init_order/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 336c848d7dd..b4fbe5644ee 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -22,6 +23,130 @@ Author: Daniel Kroening, kroening@kroening.com #include +using dependency_mapt = + std::unordered_map>; + +/// 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 &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 topological_sort_with_dependencies( + const std::set &symbols, + const dependency_mapt &dependencies) +{ + std::vector result; + std::unordered_set visited; + std::unordered_set in_progress; // For cycle detection + + // Recursive helper function for depth-first search + std::function 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 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 static_lifetime_init( const irep_idt &identifier, symbol_table_baset &symbol_table) @@ -116,7 +241,22 @@ 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 symbols; for(const auto &symbol_pair : symbol_table.symbols) @@ -124,23 +264,42 @@ void static_lifetime_init( 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 cprover_symbols; + std::set 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 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 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