From ba90cd3c39e3caa618e6763ec6b91db3710e40d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Nov 2021 15:16:11 +0000 Subject: [PATCH] String abstraction: use tag types String abstraction would previously place expanded struct types in expressions. All other analyses, however, expect exclusive use of struct_tag_types. --- src/goto-programs/string_abstraction.cpp | 122 ++++++++++++++--------- 1 file changed, 74 insertions(+), 48 deletions(-) diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index f4cbf286136..27ca19d5ceb 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -100,7 +100,17 @@ string_abstractiont::string_abstractiont( s.components()[1].set_pretty_name("length"); s.components()[2].set_pretty_name("size"); - string_struct = std::move(s); + symbolt &struct_symbol = get_fresh_aux_symbol( + s, "tag-", "string_struct", source_locationt{}, ID_C, ns, symbol_table); + struct_symbol.is_type = true; + struct_symbol.is_lvalue = false; + struct_symbol.is_state_var = false; + struct_symbol.is_thread_local = true; + struct_symbol.is_file_local = true; + struct_symbol.is_auxiliary = false; + struct_symbol.is_macro = true; + + string_struct = struct_tag_typet{struct_symbol.name}; } typet string_abstractiont::build_type(whatt what) @@ -310,7 +320,7 @@ void string_abstractiont::make_decl_and_def(goto_programt &dest, if(val.is_nil()) { const symbolt &orig=ns.lookup(source_sym); - val=make_val_or_dummy_rec(dest, ref_instr, symbol, ns.follow(orig.type)); + val = make_val_or_dummy_rec(dest, ref_instr, symbol, orig.type); } // may still be nil (structs, then assignments have been done already) @@ -328,29 +338,28 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type) { - const typet &eff_type=ns.follow(symbol.type); - - if(eff_type.id()==ID_array || eff_type.id()==ID_pointer) + if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer) { - const typet &source_subt=is_ptr_string_struct(eff_type)? - source_type:ns.follow(source_type.subtype()); - symbol_exprt sym_expr=add_dummy_symbol_and_value( - dest, ref_instr, symbol, irep_idt(), - eff_type.subtype(), source_subt); - - if(eff_type.id()==ID_array) - return array_of_exprt(sym_expr, to_array_type(eff_type)); + const typet &source_subt = + is_ptr_string_struct(symbol.type) ? source_type : source_type.subtype(); + symbol_exprt sym_expr = add_dummy_symbol_and_value( + dest, ref_instr, symbol, irep_idt(), symbol.type.subtype(), source_subt); + + if(symbol.type.id() == ID_array) + return array_of_exprt(sym_expr, to_array_type(symbol.type)); else return address_of_exprt(sym_expr); } else if( - eff_type.id() == ID_union || - (eff_type.id() == ID_struct && eff_type != string_struct)) + symbol.type.id() == ID_union_tag || + (symbol.type.id() == ID_struct_tag && symbol.type != string_struct)) { - const struct_union_typet &su_source=to_struct_union_type(source_type); + const struct_union_typet &su_source = + to_struct_union_type(ns.follow(source_type)); const struct_union_typet::componentst &s_components= su_source.components(); - const struct_union_typet &struct_union_type=to_struct_union_type(eff_type); + const struct_union_typet &struct_union_type = + to_struct_union_type(ns.follow(symbol.type)); const struct_union_typet::componentst &components= struct_union_type.components(); unsigned seen=0; @@ -364,15 +373,12 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest, if(it->get_name()!=it2->get_name()) continue; - const typet &eff_sub_type=ns.follow(it2->type()); - if(eff_sub_type.id()==ID_pointer || - eff_sub_type.id()==ID_array || - eff_sub_type.id()==ID_struct || - eff_sub_type.id()==ID_union) + if( + it2->type().id() == ID_pointer || it2->type().id() == ID_array || + it2->type().id() == ID_struct_tag || it2->type().id() == ID_union_tag) { - symbol_exprt sym_expr=add_dummy_symbol_and_value( - dest, ref_instr, symbol, it2->get_name(), - it2->type(), ns.follow(it->type())); + symbol_exprt sym_expr = add_dummy_symbol_and_value( + dest, ref_instr, symbol, it2->get_name(), it2->type(), it->type()); member_exprt member(symbol.symbol_expr(), it2->get_name(), it2->type()); @@ -675,58 +681,56 @@ exprt string_abstractiont::build( const typet &string_abstractiont::build_abstraction_type(const typet &type) { - const typet &eff_type=ns.follow(type); - abstraction_types_mapt::const_iterator map_entry= - abstraction_types_map.find(eff_type); + abstraction_types_mapt::const_iterator map_entry = + abstraction_types_map.find(type); if(map_entry!=abstraction_types_map.end()) return map_entry->second; abstraction_types_mapt tmp; tmp.swap(abstraction_types_map); - build_abstraction_type_rec(eff_type, tmp); + build_abstraction_type_rec(type, tmp); abstraction_types_map.swap(tmp); - map_entry=tmp.find(eff_type); - CHECK_RETURN(map_entry != tmp.end()); - return abstraction_types_map.insert( - std::make_pair(eff_type, map_entry->second)).first->second; + abstraction_types_map.insert(tmp.begin(), tmp.end()); + map_entry = abstraction_types_map.find(type); + CHECK_RETURN(map_entry != abstraction_types_map.end()); + return map_entry->second; } const typet &string_abstractiont::build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known) { - const typet &eff_type=ns.follow(type); - abstraction_types_mapt::const_iterator known_entry=known.find(eff_type); + abstraction_types_mapt::const_iterator known_entry = known.find(type); if(known_entry!=known.end()) return known_entry->second; ::std::pair map_entry( - abstraction_types_map.insert(::std::make_pair(eff_type, typet{ID_nil}))); + abstraction_types_map.insert(::std::make_pair(type, typet{ID_nil}))); if(!map_entry.second) return map_entry.first->second; - if(eff_type.id()==ID_array || eff_type.id()==ID_pointer) + if(type.id() == ID_array || type.id() == ID_pointer) { // char* or void* or char[] - if(is_char_type(eff_type.subtype()) || - eff_type.subtype().id()==ID_empty) + if(is_char_type(type.subtype()) || type.subtype().id() == ID_empty) map_entry.first->second=pointer_type(string_struct); else { - const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known); + const typet &subt = build_abstraction_type_rec(type.subtype(), known); if(!subt.is_nil()) { - if(eff_type.id()==ID_array) - map_entry.first->second= - array_typet(subt, to_array_type(eff_type).size()); + if(type.id() == ID_array) + map_entry.first->second = + array_typet(subt, to_array_type(type).size()); else map_entry.first->second=pointer_type(subt); } } } - else if(eff_type.id()==ID_struct || eff_type.id()==ID_union) + else if(type.id() == ID_struct_tag || type.id() == ID_union_tag) { - const struct_union_typet &struct_union_type=to_struct_union_type(eff_type); + const struct_union_typet &struct_union_type = + to_struct_union_type(ns.follow(type)); struct_union_typet::componentst new_comp; for(const auto &comp : struct_union_type.components()) @@ -745,9 +749,31 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type, } if(!new_comp.empty()) { - struct_union_typet t(eff_type.id()); - t.components().swap(new_comp); - map_entry.first->second=t; + struct_union_typet abstracted_type = struct_union_type; + abstracted_type.components().swap(new_comp); + + const symbolt &existing_tag_symbol = + ns.lookup(to_tag_type(type).get_identifier()); + symbolt &abstracted_type_symbol = get_fresh_aux_symbol( + abstracted_type, + "", + id2string(existing_tag_symbol.name), + existing_tag_symbol.location, + existing_tag_symbol.mode, + ns, + symbol_table); + abstracted_type_symbol.is_type = true; + abstracted_type_symbol.is_lvalue = false; + abstracted_type_symbol.is_state_var = false; + abstracted_type_symbol.is_thread_local = true; + abstracted_type_symbol.is_file_local = true; + abstracted_type_symbol.is_auxiliary = false; + abstracted_type_symbol.is_macro = true; + + if(type.id() == ID_struct_tag) + map_entry.first->second = struct_tag_typet{abstracted_type_symbol.name}; + else + map_entry.first->second = union_tag_typet{abstracted_type_symbol.name}; } }