diff --git a/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/main.c b/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/main.c new file mode 100644 index 00000000000..55d6b8b47af --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/main.c @@ -0,0 +1,40 @@ +#include + +struct s +{ + int x; + int y; +}; + +struct s global; +int alsoGlobal; + +void f00(void) +{ + global.x = 0; +} + +int main(int argc, char **argv) +{ + global.x = 1; + global.y = 1; + alsoGlobal = 1; + + f00(); + + assert(global.x == 0); + assert(global.y == 1); + assert(alsoGlobal == 1); + + global.x = 2; + global.y = 2; + alsoGlobal = 2; + + f00(); + + assert(global.x == 0); + assert(global.y == 2); + assert(alsoGlobal == 2); + + return 0; +} diff --git a/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/test.desc b/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/test.desc new file mode 100644 index 00000000000..33b84fb42e0 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-assign-aware-merge-struct-02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--verify --vsd --three-way-merge --vsd-structs every-field +^\[main.assertion.1\] line \d+ assertion global.x == 0: SUCCESS$ +^\[main.assertion.2\] line \d+ assertion global.y == 1: SUCCESS$ +^\[main.assertion.3\] line \d+ assertion alsoGlobal == 1: SUCCESS$ +^\[main.assertion.4\] line \d+ assertion global.x == 0: SUCCESS$ +^\[main.assertion.5\] line \d+ assertion global.y == 2: SUCCESS$ +^\[main.assertion.6\] line \d+ assertion alsoGlobal == 2: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index b348096522c..e37aa41f7ca 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -13,6 +13,7 @@ Date: April 2016 #include #include #include +#include #include #include @@ -416,6 +417,90 @@ bool variable_sensitivity_domaint::ignore_function_call_transform( ignored_internal_function.cend(); } +// Helper function to recursively collect all modified sub-paths within an +// object +static void collect_modified_paths( + const abstract_object_pointert &start_value, + const abstract_object_pointert &end_value, + const exprt &base_expr, + std::vector &modified_paths, + const abstract_environmentt &env, + const namespacet &ns) +{ + // If the objects themselves are different at this level + if(start_value->has_been_modified(end_value)) + { + // Check if this is a struct or array that we should descend into + const typet &obj_type = start_value->type(); + + if(obj_type.id() == ID_struct || obj_type.id() == ID_struct_tag) + { + // Get the struct type + const struct_typet &struct_type = + obj_type.id() == ID_struct + ? to_struct_type(obj_type) + : ns.follow_tag(to_struct_tag_type(obj_type)); + + // Track if any field was modified + bool any_field_modified = false; + + // Check each field + for(const auto &component : struct_type.components()) + { + member_exprt member_expr( + base_expr, component.get_name(), component.type()); + + abstract_object_pointert start_field = + start_value->expression_transform( + member_expr, {start_value}, env, ns); + abstract_object_pointert end_field = + end_value->expression_transform(member_expr, {end_value}, env, ns); + + // Recursively check if this field was modified + if(start_field->has_been_modified(end_field)) + { + any_field_modified = true; + + // Check if this field is also a struct/array - if so, descend + // recursively + const typet &field_type = start_field->type(); + if( + field_type.id() == ID_struct || field_type.id() == ID_struct_tag || + field_type.id() == ID_array) + { + // Recursively descend + collect_modified_paths( + start_field, end_field, member_expr, modified_paths, env, ns); + } + else + { + // It's a leaf field (not struct/array), add it + modified_paths.push_back(member_expr); + } + } + } + + // If no field-specific modifications were found but the struct was marked + // as modified, fall back to updating the whole struct + if(!any_field_modified) + { + modified_paths.push_back(base_expr); + } + } + else if(obj_type.id() == ID_array) + { + // For arrays, we can't enumerate all possible indices + // So we fall back to marking the entire array as modified + modified_paths.push_back(base_expr); + } + else + { + // It's a simple value type that was modified + modified_paths.push_back(base_expr); + } + } +} + void variable_sensitivity_domaint::merge_three_way_function_return( const ai_domain_baset &function_start, const ai_domain_baset &function_end, @@ -431,19 +516,42 @@ void variable_sensitivity_domaint::merge_three_way_function_return( abstract_environmentt::modified_symbols( cast_function_start.abstract_state, cast_function_end.abstract_state); - std::vector modified_symbols; - modified_symbols.reserve(modified_symbol_names.size()); - std::transform( - modified_symbol_names.begin(), - modified_symbol_names.end(), - std::back_inserter(modified_symbols), - [&ns](const irep_idt &id) { return ns.lookup(id).symbol_expr(); }); - - for(const auto &symbol : modified_symbols) + for(const auto &symbol_name : modified_symbol_names) { - abstract_object_pointert value = + symbol_exprt symbol = ns.lookup(symbol_name).symbol_expr(); + + abstract_object_pointert function_start_value = + cast_function_start.abstract_state.eval(symbol, ns); + abstract_object_pointert function_end_value = cast_function_end.abstract_state.eval(symbol, ns); - abstract_state.assign(symbol, value, ns); + + // Collect all modified sub-paths (fields/elements) within this symbol + std::vector modified_paths; + collect_modified_paths( + function_start_value, + function_end_value, + symbol, + modified_paths, + cast_function_start.abstract_state, + ns); + + // Apply updates only for the modified paths + if(modified_paths.empty()) + { + // No specific sub-paths found, update the whole symbol + // This happens for non-struct/non-array types + abstract_state.assign(symbol, function_end_value, ns); + } + else + { + // Update only the modified sub-paths + for(const auto &path : modified_paths) + { + abstract_object_pointert value = + cast_function_end.abstract_state.eval(path, ns); + abstract_state.assign(path, value, ns); + } + } } return;