31 exprt &dest,
bool write)
34 if(
build(
object, dest, write))
48 !(dest.
type().
id() == ID_array && a_t.
id() == ID_pointer &&
52 log.warning() <<
"warning: inconsistent abstract type for "
67 return type.
id()==ID_pointer;
90 : sym_suffix(
"#str$fcn"),
91 symbol_table(_symbol_table),
94 message_handler(_message_handler)
100 s.components()[1].set_pretty_name(
"length");
101 s.components()[2].set_pretty_name(
"size");
145 if(type.
id() != ID_code)
150 goto_functionst::function_mapt::iterator fct_entry =
156 fct_entry->second.parameter_identifiers);
169 abstract(gf_entry.second.body);
173 goto_functionst::function_mapt::iterator
206 goto_functiont::parameter_identifierst::const_iterator param_id_it =
207 parameter_identifiers.begin();
208 for(
const auto ¶meter : fct_type.
parameters())
211 if(abstract_type.
is_nil())
214 str_args.push_back(
add_parameter(fct_symbol, abstract_type, *param_id_it));
218 for(
const auto &new_param : str_args)
219 parameter_identifiers.push_back(new_param.get_identifier());
221 fct_type.
parameters().end(), str_args.begin(), str_args.end());
237 :
ns.
lookup(identifier).base_name) +
247 str_parameter.set_base_name(param_symbol.
base_name);
248 str_parameter.set_identifier(param_symbol.
name);
250 if(!identifier.
empty())
253 return str_parameter;
261 it=
abstract(dest, it);
273 typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
274 available_declst available_decls;
280 available_decls.insert(
281 std::make_pair(it->decl_symbol().get_identifier(), it));
284 for(
const auto &l :
locals)
289 available_declst::const_iterator entry=available_decls.find(l.first);
291 if(available_declst::const_iterator(available_decls.end())!=entry)
293 ref_instr=entry->second;
316 decl1->code_nonconst().add_source_location() = ref_instr->source_location();
332 assignment1->code_nonconst().add_source_location() =
333 ref_instr->source_location();
341 if(symbol.
type.
id() == ID_array || symbol.
type.
id() == ID_pointer)
343 const typet &source_subt =
348 if(symbol.
type.
id() == ID_array)
354 symbol.
type.
id() == ID_union_tag ||
367 struct_union_typet::componentst::const_iterator it2=components.begin();
368 for(struct_union_typet::componentst::const_iterator
369 it=s_components.begin();
370 it!=s_components.end() && it2!=components.end();
373 if(it->get_name()!=it2->get_name())
377 it2->type().id() == ID_pointer || it2->type().id() == ID_array ||
378 it2->type().id() == ID_struct_tag || it2->type().id() == ID_union_tag)
381 dest, ref_instr, symbol, it2->get_name(), it2->
type(), it->type());
388 assignment1->code_nonconst().add_source_location() =
389 ref_instr->source_location();
397 components.size() == seen,
398 "some of the symbol's component names were not found in the source");
410 const typet &source_type)
412 std::string suffix=
"$strdummy";
413 if(!component_name.
empty())
414 suffix=
"#"+
id2string(component_name)+suffix;
419 new_symbol.
type=type;
421 new_symbol.
location = ref_instr->source_location();
422 new_symbol.
name=dummy_identifier;
434 decl->code_nonconst().add_source_location() = ref_instr->source_location();
461 assignment1->code_nonconst().add_source_location() =
462 ref_instr->source_location();
485 exprt tmp = it->get_condition();
487 it->set_condition(tmp);
528 exprt &lhs = target->assign_lhs_nonconst();
529 exprt &rhs = target->assign_rhs_nonconst();
541 const typet &type = target->assign_lhs().type();
543 if(type.
id() == ID_pointer || type.
id() == ID_array)
554 auto arguments =
as_const(*target).call_arguments();
557 for(
const auto &arg : arguments)
560 if(abstract_type.
is_nil())
563 str_args.push_back(
exprt());
569 if(str_args.back().type().id()==ID_array &&
570 abstract_type.
id()==ID_pointer)
573 str_args.back().type().subtype() == abstract_type.
subtype(),
574 "argument array type differs from formal parameter pointer type");
578 idx.
set(ID_C_bounds_check,
false);
587 if(!str_args.empty())
589 arguments.insert(arguments.end(), str_args.begin(), str_args.end());
593 for(
const auto &arg : str_args)
596 target->call_arguments() = std::move(arguments);
602 if(expr.
id()==
"is_zero_string" ||
603 expr.
id()==
"zero_string_length" ||
604 expr.
id()==
"buffer_size")
619 if(expr.
id()==
"is_zero_string")
626 else if(expr.
id()==
"zero_string_length")
633 else if(expr.
id()==
"buffer_size")
646 const exprt &pointer,
652 if(pointer.
id()==ID_typecast)
684 abstraction_types_mapt::const_iterator map_entry =
687 return map_entry->second;
697 return map_entry->second;
703 abstraction_types_mapt::const_iterator known_entry = known.
find(type);
704 if(known_entry!=known.end())
705 return known_entry->second;
707 ::std::pair<abstraction_types_mapt::iterator, bool> map_entry(
709 if(!map_entry.second)
710 return map_entry.first->second;
712 if(type.
id() == ID_array || type.
id() == ID_pointer)
722 if(type.
id() == ID_array)
723 map_entry.first->second =
730 else if(type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
736 for(
const auto &comp : struct_union_type.
components())
738 if(comp.get_anonymous())
746 new_comp.back().set_name(comp.get_name());
747 new_comp.back().set_pretty_name(comp.get_pretty_name());
748 new_comp.back().type()=subt;
750 if(!new_comp.empty())
755 const symbolt &existing_tag_symbol =
762 existing_tag_symbol.
mode,
765 abstracted_type_symbol.
is_type =
true;
766 abstracted_type_symbol.
is_lvalue =
false;
771 abstracted_type_symbol.
is_macro =
true;
773 if(type.
id() == ID_struct_tag)
780 return map_entry.first->second;
786 if(abstract_type.
is_nil())
789 if(
object.
id()==ID_typecast)
794 return dest.
type() != abstract_type ||
795 (dest.
type().
id() == ID_array && abstract_type.
id() == ID_pointer &&
799 if(
object.
id()==ID_string_constant)
801 const std::string &str_value =
805 const std::size_t str_len =
806 std::min(str_value.size(), str_value.find(
'\0'));
810 if(
object.
id()==ID_array &&
is_char_type(
object.type().subtype()))
817 if(
object.
id()==ID_symbol)
820 if(
object.
id()==ID_if)
823 if(
object.
id()==ID_member)
831 if(
object.
id()==ID_dereference)
839 if(
object.
id()==ID_index)
847 if(
object.type().
id()==ID_pointer)
854 exprt &dest,
bool write)
861 if(op1_err && op2_err)
882 exprt &dest,
bool write)
891 const auto size = numeric_cast<mp_integer>(a_size);
893 if(!size.has_value())
896 *size ==
object.operands().size(),
897 "wrong number of array object arguments");
899 exprt::operandst::const_iterator it=
object.operands().begin();
908 exprt &dest,
bool write)
944 return exprt(ID_null_object, type);
966 return exprt(ID_null_object, type);
974 locals[identifier]=identifier;
977 new_symbol.
type=type;
979 new_symbol.
name=identifier;
982 new_symbol.
mode=ID_C;
987 return ns.
lookup(identifier).symbol_expr();
1004 identifier = parameter_map_entry->second;
1037 new_symbol.
type=type;
1040 new_symbol.
name=identifier;
1056 dummy_loc->source_location_nonconst() = symbol.
location;
1077 new_symbol.
name=identifier;
1079 new_symbol.
mode=ID_C;
1107 while(lhs.
id() == ID_typecast)
1114 if(lhs.
id()==ID_minus)
1123 while(lhs.
id() == ID_typecast)
1135 const exprt &lhs = target->assign_lhs();
1136 const exprt rhs = target->assign_rhs();
1137 const exprt *rhsp = &(target->assign_rhs());
1139 while(rhsp->
id()==ID_typecast)
1143 if(abstract_type.
is_nil())
1146 exprt new_lhs, new_rhs;
1155 if(lhs.
type().
id()==ID_pointer && !unknown)
1161 target->source_location();
1164 return std::next(target);
1176 const exprt &lhs = target->assign_lhs();
1177 const exprt *rhsp = &(target->assign_rhs());
1179 while(rhsp->
id()==ID_typecast)
1187 if(lhs.
id()==ID_index)
1197 "failed to create length-component for the left-hand-side");
1205 return char_assign(dest, target, new_lhs, i2, min_expr);
1208 else if(lhs.
id()==ID_dereference)
1217 "failed to create length-component for the left-hand-side");
1238 const exprt &new_lhs,
1247 "failed to create is_zero-component for the left-hand-side");
1251 assignment1->code_nonconst().add_source_location() =
1252 target->source_location();
1256 assignment2->code_nonconst().add_source_location() =
1257 target->source_location();
1260 assignment2->code_nonconst().op0(), assignment2->code_nonconst().op1());
1280 if(lhs.
type().
id()==ID_array)
1283 const auto size = numeric_cast<mp_integer>(a_size);
1285 if(!size.has_value())
1292 else if(lhs.
type().
id() == ID_pointer)
1297 else if(lhs.
type().
id()==ID_struct || lhs.
type().
id()==ID_union)
1302 for(
const auto &comp : struct_union_type.
components())
1305 !comp.get_name().empty(),
"struct/union components must have a name");
1333 goto_else->complete_goto(else_target);
1334 goto_out->complete_goto(out_target);
1360 assignment->code_nonconst().add_source_location() =
1361 target->source_location();
1369 assignment->code_nonconst().add_source_location() =
1370 target->source_location();
1378 assignment->code_nonconst().add_source_location() =
1379 target->source_location();
1397 "either the expression is not a string or it is not a pointer to one");
1400 a.
type().
id()==ID_pointer?
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
Array constructor from list of elements.
Array constructor from single element.
const exprt & size() const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A codet representing an assignment in the program.
exprt::operandst argumentst
std::vector< parametert > parameterst
const parameterst & parameters() const
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
const source_locationt & source_location() const
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::vector< irep_idt > parameter_identifierst
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
codet & code_nonconst()
Set the code represented by this instruction.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
void swap(goto_programt &program)
Swap the goto program.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
const irept & find(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
Class that provides messages with a built-in verbosity 'level'.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The plus expression Associativity is not specified.
A side_effect_exprt that returns a non-deterministically chosen value.
Replace all uses of char * by a struct that carries that string, and also the underlying allocation a...
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
void declare_define_locals(goto_programt &dest)
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
static typet build_type(whatt what)
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
unsigned temporary_counter
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
exprt build_unknown(whatt what, bool write)
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
bool is_ptr_string_struct(const typet &type) const
message_handlert & message_handler
::std::map< typet, typet > abstraction_types_mapt
goto_programt initialization
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
symbol_exprt add_dummy_symbol_and_value(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const irep_idt &component_name, const typet &type, const typet &source_type)
bool build_wrap(const exprt &object, exprt &dest, bool write)
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
bool build_array(const array_exprt &object, exprt &dest, bool write)
void apply(goto_modelt &goto_model)
Apply string abstraction to goto_model.
bool build_symbol(const symbol_exprt &sym, exprt &dest)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void operator()(goto_programt &dest)
abstraction_types_mapt abstraction_types_map
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
code_typet::parametert add_parameter(const symbolt &fct_symbol, const typet &type, const irep_idt &identifier)
bool build_pointer(const exprt &object, exprt &dest, bool write)
void abstract_function_call(goto_programt::targett it)
exprt member(const exprt &a, whatt what)
static bool has_string_macros(const exprt &expr)
void make_type(exprt &dest, const typet &type)
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
void add_str_parameters(symbolt &fct_symbol, goto_functiont::parameter_identifierst ¶meter_identifiers)
bool is_char_type(const typet &type) const
symbol_tablet & symbol_table
const typet & build_abstraction_type(const typet &type)
Struct constructor from list of elements.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
source_locationt & add_source_location()
A union tag type, i.e., union_typet with an identifier.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
int main(int argc, char *argv[])
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
exprt pointer_offset(const exprt &pointer)
Various predicates over pointers in programs.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_functionst &dest)
static bool is_ptr_argument(const typet &type)
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.