Skip to content

Remove deprecated string abstraction methods #6673

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 15, 2022
Merged

Remove deprecated string abstraction methods #6673

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 24 additions & 31 deletions src/goto-programs/string_abstraction.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,29 +67,19 @@ static inline bool is_ptr_argument(const typet &type)
return type.id()==ID_pointer;
}

void string_abstraction(
symbol_tablet &symbol_table,
message_handlert &message_handler,
goto_functionst &dest)
{
string_abstractiont string_abstraction(symbol_table, message_handler);
string_abstraction(dest);
}

void string_abstraction(
goto_modelt &goto_model,
message_handlert &message_handler)
{
string_abstractiont{goto_model.symbol_table, message_handler}.apply(
goto_model);
string_abstractiont{goto_model, message_handler}.apply();
}

string_abstractiont::string_abstractiont(
symbol_tablet &_symbol_table,
goto_modelt &goto_model,
message_handlert &_message_handler)
: sym_suffix("#str$fcn"),
symbol_table(_symbol_table),
ns(_symbol_table),
goto_model(goto_model),
ns(goto_model.symbol_table),
temporary_counter(0),
message_handler(_message_handler)
{
Expand All @@ -101,7 +91,13 @@ string_abstractiont::string_abstractiont(
s.components()[2].set_pretty_name("size");

symbolt &struct_symbol = get_fresh_aux_symbol(
s, "tag-", "string_struct", source_locationt{}, ID_C, ns, symbol_table);
s,
"tag-",
"string_struct",
source_locationt{},
ID_C,
ns,
goto_model.symbol_table);
struct_symbol.is_type = true;
struct_symbol.is_lvalue = false;
struct_symbol.is_state_var = false;
Expand Down Expand Up @@ -129,13 +125,11 @@ typet string_abstractiont::build_type(whatt what)
return type;
}

void string_abstractiont::apply(goto_modelt &goto_model)
void string_abstractiont::apply()
{
operator()(goto_model.goto_functions);
}
goto_functionst &dest = goto_model.goto_functions;
symbol_tablet &symbol_table = goto_model.symbol_table;

void string_abstractiont::operator()(goto_functionst &dest)
{
// iterate over all previously known symbols as the body of the loop modifies
// the symbol table and can thus invalidate iterators
for(auto &sym_name : symbol_table.sorted_symbol_names())
Expand Down Expand Up @@ -184,7 +178,7 @@ void string_abstractiont::operator()(goto_functionst &dest)
}
}

void string_abstractiont::operator()(goto_programt &dest)
void string_abstractiont::apply(goto_programt &dest)
{
abstract(dest);

Expand Down Expand Up @@ -238,7 +232,7 @@ code_typet::parametert string_abstractiont::add_parameter(
"#str",
fct_symbol.location,
fct_symbol.mode,
symbol_table);
goto_model.symbol_table);
param_symbol.is_parameter = true;
param_symbol.value.make_nil();

Expand Down Expand Up @@ -462,7 +456,7 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
ref_instr->source_location();
}

symbol_table.insert(std::move(new_symbol));
goto_model.symbol_table.insert(std::move(new_symbol));

return sym_expr;
}
Expand Down Expand Up @@ -767,7 +761,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
existing_tag_symbol.location,
existing_tag_symbol.mode,
ns,
symbol_table);
goto_model.symbol_table);
abstracted_type_symbol.is_type = true;
abstracted_type_symbol.is_lvalue = false;
abstracted_type_symbol.is_state_var = false;
Expand Down Expand Up @@ -988,7 +982,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write)
new_symbol.mode=ID_C;
new_symbol.pretty_name=identifier;

symbol_table.insert(std::move(new_symbol));
goto_model.symbol_table.insert(std::move(new_symbol));

return ns.lookup(identifier).symbol_expr();
}
Expand All @@ -1014,14 +1008,14 @@ bool string_abstractiont::build_symbol(const symbol_exprt &sym, exprt &dest)
std::string sym_suffix_before = sym_suffix;
sym_suffix = "#str";
identifier = id2string(symbol.name) + sym_suffix;
if(symbol_table.symbols.find(identifier) == symbol_table.symbols.end())
if(!goto_model.symbol_table.has_symbol(identifier))
build_new_symbol(symbol, identifier, abstract_type);
sym_suffix = sym_suffix_before;
}
else
{
identifier=id2string(symbol.name)+sym_suffix;
if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
if(!goto_model.symbol_table.has_symbol(identifier))
build_new_symbol(symbol, identifier, abstract_type);
}

Expand Down Expand Up @@ -1053,7 +1047,7 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol,
new_symbol.is_static_lifetime=symbol.is_static_lifetime;
new_symbol.is_thread_local=symbol.is_thread_local;

symbol_table.insert(std::move(new_symbol));
goto_model.symbol_table.insert(std::move(new_symbol));

if(symbol.is_static_lifetime)
{
Expand All @@ -1074,8 +1068,7 @@ bool string_abstractiont::build_symbol_constant(
+"_"+integer2string(buf_size);
irep_idt identifier="string_abstraction::"+id2string(base);

if(symbol_table.symbols.find(identifier)==
symbol_table.symbols.end())
if(!goto_model.symbol_table.has_symbol(identifier))
{
auxiliary_symbolt new_symbol;
new_symbol.type=string_struct;
Expand All @@ -1100,7 +1093,7 @@ bool string_abstractiont::build_symbol_constant(
code_assignt(new_symbol.symbol_expr(), value)));
}

symbol_table.insert(std::move(new_symbol));
goto_model.symbol_table.insert(std::move(new_symbol));
}

dest=address_of_exprt(symbol_exprt(identifier, string_struct));
Expand Down
30 changes: 8 additions & 22 deletions src/goto-programs/string_abstraction.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]

#include <util/bitvector_types.h>
#include <util/config.h>
#include <util/deprecate.h>
#include <util/namespace.h>
#include <util/std_expr.h>

Expand All @@ -34,33 +33,27 @@ class message_handlert;
class string_abstractiont
{
public:
// To be deprecated once the operator() methods have been removed, at which
// point a new constructor that only takes a message_handler should be
// introduced.
string_abstractiont(
symbol_tablet &_symbol_table,
message_handlert &_message_handler);

DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
void operator()(goto_programt &dest);
DEPRECATED(SINCE(2020, 12, 14, "Use apply(goto_modelt &)"))
void operator()(goto_functionst &dest);

/// Apply string abstraction to \p goto_model. If any abstractions are to be
/// applied, the affected goto_functions and any affected symbols will be
/// modified.
void apply(goto_modelt &goto_model);
string_abstractiont(
goto_modelt &goto_model,
message_handlert &_message_handler);

void apply();

protected:
std::string sym_suffix;
symbol_tablet &symbol_table;
goto_modelt &goto_model;
namespacet ns;
unsigned temporary_counter;
message_handlert &message_handler;

typedef ::std::map< typet, typet > abstraction_types_mapt;
abstraction_types_mapt abstraction_types_map;

void apply(goto_programt &dest);

static bool has_string_macros(const exprt &expr);

void replace_string_macros(
Expand Down Expand Up @@ -190,11 +183,4 @@ void string_abstraction(
goto_modelt &,
message_handlert &);

DEPRECATED(
SINCE(2020, 12, 14, "Use string_abstraction(goto_model, message_handler)"))
void string_abstraction(
symbol_tablet &,
message_handlert &,
goto_functionst &);

#endif // CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H