25 exprt &dest,
bool write)
28 if(
build(
object, dest, write))
41 !(dest.
type().
id()==ID_array && a_t.
id()==ID_pointer &&
44 warning() <<
"warning: inconsistent abstract type for " 45 <<
object.pretty() <<
eom;
54 return type.
id()==ID_pointer &&
60 return type.
id()==ID_pointer;
95 arg_suffix(
"#strarg"),
96 sym_suffix(
"#str$fcn"),
140 abstract(it->second.body);
145 goto_functionst::function_mapt::iterator
179 for(code_typet::parameterst::iterator
180 it=parameters.begin();
181 it!=parameters.end();
185 if(abstract_type.
is_nil())
188 const irep_idt &identifier=it->get_identifier();
199 parameters.insert(parameters.end(), str_args.begin(), str_args.end());
202 symb_parameters.insert(
203 symb_parameters.end(), str_args.begin(), str_args.end());
217 str_args.back().add_source_location()=fct_symbol.
location;
218 str_args.back().set_base_name(base_name);
219 str_args.back().set_identifier(identifier);
222 new_symbol.
type=final_type;
224 new_symbol.
location=str_args.back().source_location();
225 new_symbol.
name=str_args.back().get_identifier();
227 new_symbol.
base_name=str_args.back().get_base_name();
229 new_symbol.
pretty_name=str_args.back().get_base_name();
239 it=
abstract(dest, it);
251 typedef std::unordered_map<irep_idt, goto_programt::targett> available_declst;
252 available_declst available_decls;
258 available_decls.insert(std::make_pair(
262 for(
const auto &l :
locals)
267 available_declst::const_iterator entry=available_decls.find(l.first);
269 if(available_declst::const_iterator(available_decls.end())!=entry)
271 ref_instr=entry->second;
294 decl1->source_location=ref_instr->source_location;
295 decl1->function=ref_instr->function;
297 decl1->code.add_source_location()=ref_instr->source_location;
311 assignment1->make_assignment();
312 assignment1->source_location=ref_instr->source_location;
313 assignment1->function=ref_instr->function;
315 assignment1->code.add_source_location()=ref_instr->source_location;
325 if(eff_type.
id()==ID_array || eff_type.
id()==ID_pointer)
330 dest, ref_instr, symbol,
irep_idt(),
331 eff_type.
subtype(), source_subt);
333 if(eff_type.
id()==ID_array)
338 else if(eff_type.
id()==ID_union ||
349 struct_union_typet::componentst::const_iterator it2=components.begin();
350 for(struct_union_typet::componentst::const_iterator
351 it=s_components.begin();
352 it!=s_components.end() && it2!=components.end();
355 if(it->get_name()!=it2->get_name())
359 if(eff_sub_type.
id()==ID_pointer ||
360 eff_sub_type.
id()==ID_array ||
361 eff_sub_type.
id()==ID_struct ||
362 eff_sub_type.
id()==ID_union)
365 dest, ref_instr, symbol, it2->get_name(),
371 assignment1->make_assignment();
372 assignment1->source_location=ref_instr->source_location;
373 assignment1->function=ref_instr->function;
375 assignment1->code.add_source_location()=ref_instr->source_location;
382 assert(components.size()==seen);
394 const typet &source_type)
396 std::string suffix=
"$strdummy";
397 if(!component_name.
empty())
398 suffix=
"#"+
id2string(component_name)+suffix;
403 new_symbol.
type=type;
405 new_symbol.
location=ref_instr->source_location;
406 new_symbol.
name=dummy_identifier;
418 decl->source_location=ref_instr->source_location;
419 decl->function=ref_instr->function;
421 decl->code.add_source_location()=ref_instr->source_location;
442 assignment1->make_assignment();
443 assignment1->source_location=ref_instr->source_location;
444 assignment1->function=ref_instr->function;
446 assignment1->code.add_source_location()=ref_instr->source_location;
522 if(type.
id()==ID_pointer || type.
id()==ID_array)
542 code_function_callt::argumentst::const_iterator it1=arguments.begin();
543 for(code_typet::parameterst::const_iterator it2=formal_params.begin();
544 it2!=formal_params.end();
548 if(abstract_type.
is_nil())
551 if(it1==arguments.end())
553 error() <<
"function call: not enough arguments" <<
eom;
557 str_args.push_back(
exprt());
563 if(str_args.back().type().id()==ID_array &&
564 abstract_type.
id()==ID_pointer)
566 assert(
type_eq(str_args.back().type().subtype(),
571 idx.
set(
"bounds_check",
false);
580 arguments.insert(arguments.end(), str_args.begin(), str_args.end());
585 if(expr.
id()==
"is_zero_string" ||
586 expr.
id()==
"zero_string_length" ||
587 expr.
id()==
"buffer_size")
602 if(expr.
id()==
"is_zero_string")
608 else if(expr.
id()==
"zero_string_length")
614 else if(expr.
id()==
"buffer_size")
626 const exprt &pointer,
632 if(pointer.
id()==ID_typecast)
635 assert(pointer.
operands().size()==1);
636 if(pointer.
op0().
type().
id()!=ID_pointer)
640 return build(pointer.
op0(), what, write, source_location);
662 abstraction_types_mapt::const_iterator map_entry=
665 return map_entry->second;
672 map_entry=tmp.find(eff_type);
673 assert(map_entry!=tmp.end());
675 std::make_pair(eff_type, map_entry->second)).first->second;
682 abstraction_types_mapt::const_iterator known_entry=known.
find(eff_type);
683 if(known_entry!=known.end())
684 return known_entry->second;
686 ::std::pair< abstraction_types_mapt::iterator, bool > map_entry(
689 if(!map_entry.second)
690 return map_entry.first->second;
692 if(eff_type.
id()==ID_array || eff_type.
id()==ID_pointer)
703 if(eff_type.
id()==ID_array)
704 map_entry.first->second=
711 else if(eff_type.
id()==ID_struct || eff_type.
id()==ID_union)
716 for(
const auto &comp : struct_union_type.
components())
718 if(comp.get_anonymous())
726 new_comp.back().set_name(comp.get_name());
727 new_comp.back().set_pretty_name(comp.get_pretty_name());
728 new_comp.back().type()=subt;
730 if(!new_comp.empty())
734 map_entry.first->second=t;
738 return map_entry.first->second;
744 if(abstract_type.
is_nil())
747 if(
object.
id()==ID_typecast)
753 (dest.
type().
id()==ID_array &&
754 abstract_type.
id()==ID_pointer &&
758 if(
object.
id()==ID_string_constant)
760 const std::string &str_value =
id2string(
object.
get(ID_value));
763 const std::size_t str_len =
764 std::min(str_value.size(), str_value.find(
'\0'));
768 if(
object.
id()==ID_array &&
is_char_type(
object.type().subtype()))
772 if(
object.is_constant())
775 if(
object.
id()==ID_symbol)
778 if(
object.
id()==ID_if)
781 if(
object.
id()==ID_member)
788 if(
object.
id()==ID_dereference)
795 if(
object.
id()==ID_index)
803 if(
object.type().id()==ID_pointer)
810 exprt &dest,
bool write)
817 if(op1_err && op2_err)
822 new_if.type()=new_if.false_case().type();
827 new_if.
type()=new_if.true_case().type();
831 new_if.
type()=new_if.true_case().type();
838 exprt &dest,
bool write)
851 assert(size==
object.operands().size());
853 exprt::operandst::const_iterator it=
object.operands().begin();
862 exprt &dest,
bool write)
864 assert(
object.type().
id()==ID_pointer);
898 return exprt(ID_null_object, type);
920 return exprt(ID_null_object, type);
928 locals[identifier]=identifier;
931 new_symbol.
type=type;
933 new_symbol.
name=identifier;
936 new_symbol.
mode=ID_C;
941 return ns.
lookup(identifier).symbol_expr();
949 assert(!abstract_type.
is_nil());
978 new_symbol.
type=type;
981 new_symbol.
name=identifier;
996 dummy_loc->source_location=symbol.
location;
1017 new_symbol.
name=identifier;
1019 new_symbol.
mode=ID_C;
1035 assignment1->make_assignment();
1049 if(lhs.
id()==ID_minus)
1069 while(rhsp->
id()==ID_typecast)
1070 rhsp=&(rhsp->
op0());
1073 if(abstract_type.
is_nil())
1076 exprt new_lhs, new_rhs;
1085 if(lhs.
type().
id()==ID_pointer && !unknown)
1090 assignment.
function=target->function;
1113 while(rhsp->
id()==ID_typecast)
1114 rhsp=&(rhsp->
op0());
1121 if(lhs.
id()==ID_index)
1137 return char_assign(dest, target, new_lhs, i2, min_expr);
1140 else if(lhs.
id()==ID_dereference)
1168 const exprt &new_lhs,
1178 assignment1->make_assignment();
1179 assignment1->source_location=target->source_location;
1180 assignment1->function=target->function;
1182 assignment1->code.add_source_location()=target->source_location;
1185 assignment2->make_assignment();
1186 assignment2->source_location=target->source_location;
1187 assignment2->function=target->function;
1189 assignment2->code.add_source_location()=target->source_location;
1192 assignment2->code.op0(),
1193 assignment2->code.op1());
1213 if(lhs.
type().
id()==ID_array)
1225 else if(lhs.
type().
id()==ID_pointer)
1231 else if(lhs.
type().
id()==ID_struct || lhs.
type().
id()==ID_union)
1236 for(
const auto &comp : struct_union_type.
components())
1238 assert(!comp.get_name().empty());
1261 goto_else->function=target->function;
1262 goto_else->source_location=target->source_location;
1263 goto_else->make_goto(else_target, rhs.
cond());
1264 goto_else->guard.make_not();
1266 goto_out->function=target->function;
1267 goto_out->source_location=target->source_location;
1268 goto_out->make_goto(out_target,
true_exprt());
1270 else_target->function=target->function;
1271 else_target->source_location=target->source_location;
1273 out_target->function=target->function;
1274 out_target->source_location=target->source_location;
1300 assignment->code.add_source_location()=target->source_location;
1301 assignment->function=target->function;
1302 assignment->source_location=target->source_location;
1310 assignment->code.add_source_location()=target->source_location;
1311 assignment->function=target->function;
1312 assignment->source_location=target->source_location;
1320 assignment->code.add_source_location()=target->source_location;
1321 assignment->function=target->function;
1322 assignment->source_location=target->source_location;
1342 a.
type().
id()==ID_pointer?
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
irep_idt function
The function this instruction belongs to.
goto_programt::targett abstract_pointer_assign(goto_programt &dest, goto_programt::targett it)
The type of an expression.
bool build_array(const array_exprt &object, exprt &dest, bool write)
irep_idt name
The unique identifier.
const std::string arg_suffix
const code_declt & to_code_decl(const codet &code)
void string_abstraction(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
const typet & build_abstraction_type_rec(const typet &type, const abstraction_types_mapt &known)
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
pointer_typet pointer_type(const typet &subtype)
const std::string integer2string(const mp_integer &n, unsigned base)
void make_type(exprt &dest, const typet &type)
exprt build_unknown(whatt what, bool write)
goto_programt::targett char_assign(goto_programt &dest, goto_programt::targett target, const exprt &new_lhs, const exprt &lhs, const exprt &rhs)
irep_idt mode
Language mode.
goto_programt initialization
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
goto_programt::targett abstract_char_assign(goto_programt &dest, goto_programt::targett it)
void move_lhs_arithmetic(exprt &lhs, exprt &rhs)
void declare_define_locals(goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
std::vector< componentt > componentst
std::vector< parametert > parameterst
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
exprt value
Initial value of symbol.
const componentst & components() const
bool build_wrap(const exprt &object, exprt &dest, bool write)
void build_new_symbol(const symbolt &symbol, const irep_idt &identifier, const typet &type)
The trinary if-then-else operator.
static typet build_type(whatt what)
irep_idt module
Name of module the symbol belongs to.
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
void add_str_arguments(const irep_idt &name, goto_functionst::goto_functiont &fct)
exprt::operandst argumentst
unsignedbv_typet size_type()
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Extract member of struct or union.
void add_argument(code_typet::parameterst &str_args, const symbolt &fct_symbol, const typet &type, const irep_idt &base_name, const irep_idt &identifier)
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
void clear()
Clear the goto program.
void make_decl_and_def(goto_programt &dest, goto_programt::targett ref_instr, const irep_idt &identifier, const irep_idt &source_sym)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
::std::set< irep_idt > current_args
void replace_string_macros(exprt &expr, bool lhs, const source_locationt &)
bool build_symbol(const symbol_exprt &sym, exprt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
bool build_symbol_constant(const mp_integer &zero_length, const mp_integer &buf_size, exprt &dest)
The boolean constant true.
bool is_char_type(const typet &type) const
static bool is_ptr_argument(const typet &type)
instructionst::iterator targett
A declaration of a local variable.
::std::map< typet, typet > abstraction_types_mapt
goto_programt::targett abstract_assign(goto_programt &dest, goto_programt::targett it)
Operator to dereference a pointer.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
exprt make_val_or_dummy_rec(goto_programt &dest, goto_programt::targett ref_instr, const symbolt &symbol, const typet &source_type)
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
::goto_functiont goto_functiont
symbol_tablet & symbol_table
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
exprt build(const exprt &pointer, whatt what, bool write, const source_locationt &)
const exprt & size() const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
array constructor from single element
const typet & follow(const typet &) const
bitvector_typet index_type()
goto_programt::targett abstract(goto_programt &dest, goto_programt::targett it)
goto_programt::targett value_assignments(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt &rhs)
Operator to return the address of an object.
Various predicates over pointers in programs.
goto_programt::targett value_assignments_string_struct(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt &rhs)
The boolean constant false.
const typet & build_abstraction_type(const typet &type)
void abstract_function_call(goto_programt &dest, goto_programt::targett it)
void swap(goto_programt &program)
Swap the goto program.
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
void operator()(goto_programt &dest)
source_locationt location
Source code location of definition of symbol.
string_abstractiont(symbol_tablet &_symbol_table, message_handlert &_message_handler)
static irep_idt entry_point()
Base type of C structs and unions, and C++ classes.
mstreamt & result() const
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const exprt & struct_op() const
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
exprt pointer_offset(const exprt &pointer)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
irep_idt get_component_name() const
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)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
unsigned temporary_counter
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
bool build_pointer(const exprt &object, exprt &dest, bool write)
bool build_if(const if_exprt &o_if, exprt &dest, bool write)
Expression to hold a symbol (variable)
bool is_ptr_string_struct(const typet &type) const
goto_programt::targett value_assignments_if(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const if_exprt &rhs)
goto_programt coverage_criteriont message_handlert & message_handler
const typet & subtype() const
static bool has_string_macros(const exprt &expr)
struct constructor from list of elements
exprt member(const exprt &a, whatt what)
abstraction_types_mapt abstraction_types_map
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
array constructor from list of elements
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
const code_function_callt & to_code_function_call(const codet &code)