26#include <unordered_map>
30 if(expr.
id() == ID_symbol)
34 else if(expr.
id() == ID_member)
38 else if(expr.
id() == ID_index)
42 else if(expr.
id() == ID_dereference)
46 else if(expr.
id() == ID_typecast)
50 else if(expr.
id() == ID_address_of)
56 throw "unsupported expression type for finding base symbol";
74 natural_loops.
loop_map.size() == 0,
"quantifier must not contain loops");
76 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
95 declared_symbols.insert(it->decl_symbol());
101 "expression statements must contain a terminator expression");
105 last_expr.id() == ID_typecast &&
114 std::vector<goto_programt::const_targett> paths;
115 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
118 std::vector<goto_programt::const_targett> paths,
119 std::vector<std::pair<exprt, replace_mapt>>
120 path_conditions_and_value_maps)
122 path_conditions_and_value_maps(path_conditions_and_value_maps)
128 return paths.empty();
136 exprt &back_path_condition()
138 return path_conditions_and_value_maps.back().first;
143 return path_conditions_and_value_maps.back().second;
148 exprt path_condition,
151 paths.push_back(target);
152 path_conditions_and_value_maps.push_back(
153 std::make_pair(path_condition, value_map));
159 path_conditions_and_value_maps.pop_back();
170 while(!paths.empty())
172 auto ¤t_it = paths.back_it();
173 auto &path_condition = paths.back_path_condition();
174 auto &value_map = paths.back_value_map();
182 switch(current_it->type())
186 declared_symbols.insert(current_it->decl_symbol());
194 auto lhs = current_it->assign_lhs();
197 "quantifier must not contain side effects");
198 exprt rhs = current_it->assign_rhs();
200 value_map[lhs] = rhs;
216 exprt condition = current_it->condition();
220 auto next_it = current_it->targets.front();
221 exprt copy_path_condition = path_condition;
225 next_it,
and_exprt(copy_path_condition, condition), value_map);
229 current_it = current_it->targets.front();
239 if(current_it == last)
241 exprt copy_of_last_expr = last_expr;
293 new_symbol.
value = expr;
299 result.add_source_location() = source_location;
308 convert(code_assign, dest, mode);
314 targets.scope_stack.add(std::move(code_dead), {});
328 expr.
id() == ID_side_effect || expr.
id() == ID_compound_literal ||
329 expr.
id() == ID_comma)
348 if(expr.
id() == ID_forall || expr.
id() == ID_exists)
358 for(
const auto &op : expr.
operands())
371 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
377 "' must be Boolean, but got ",
386 std::move(implies->lhs()),
387 std::move(implies->rhs()),
398 if(expr.
id() == ID_and)
408 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
415 "boolean operators must have only boolean operands",
418 if(expr.
id() == ID_and)
426 if(expr.
id() == ID_or)
456 if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
462 return clean_expr(expr, mode, result_is_used);
464 else if(expr.
id() == ID_if)
483 "condition for an 'if' must be boolean",
584 else if(expr.
id() == ID_comma)
594 bool last = (it == --expr.
operands().end());
630 else if(expr.
id() == ID_typecast)
643 else if(expr.
id() == ID_side_effect)
648 if(statement == ID_gcc_conditional_expression)
653 else if(statement == ID_statement_expression)
660 else if(statement == ID_assign)
665 "side-effect assignment expressions must have two operands");
670 side_effect_assign.rhs().id() == ID_side_effect &&
676 exprt lhs = side_effect_assign.lhs();
690 side_effect_assign.rhs(), new_lhs.
type());
696 expr = must_use_rhs ? new_rhs : lhs;
704 else if(expr.
id() == ID_forall || expr.
id() == ID_exists)
710 (code.
operands()[0].id() == ID_side_effect &&
711 code.
operands()[0].get_named_sub()[ID_statement].id() ==
712 ID_statement_expression),
713 "quantifier must not contain side effects");
717 code.
operands()[0].id() == ID_side_effect &&
718 code.
operands()[0].get_named_sub()[ID_statement].id() ==
719 ID_statement_expression)
727 else if(expr.
id() == ID_address_of)
740 if(expr.
id() == ID_side_effect)
745 else if(expr.
id() == ID_compound_literal)
749 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
764 if(expr.
id() == ID_compound_literal)
767 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
772 else if(expr.
id() == ID_string_constant)
777 else if(expr.
id() == ID_index)
783 else if(expr.
id() == ID_dereference)
788 else if(expr.
id() == ID_comma)
797 bool last = (it == --expr.
operands().end());
817 else if(expr.
id() == ID_side_effect)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the removal of a local variable going out of scope.
A goto_instruction_codet representing the declaration of a local variable.
codet representation of an expression statement.
const exprt & expression() const
Operator to dereference a pointer.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
The Boolean constant false.
clean_expr_resultt clean_expr_address_of(exprt &expr, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void generate_ifthenelse(const exprt &cond, const source_locationt &, goto_programt &true_case, const source_locationt &, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
std::string tmp_symbol_prefix
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
symbol_exprt make_compound_literal(const exprt &expr, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt remove_side_effect(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)
static bool needs_cleaning(const exprt &expr)
Returns 'true' for expressions that may change the program state.
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
clean_expr_resultt remove_function_call(side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt remove_statement_expression(side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
void rewrite_boolean(exprt &dest)
re-write boolean operators into ?:
static bool assignment_lhs_needs_temporary(const exprt &lhs)
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
void compute_location_numbers(unsigned &nr)
Compute location numbers.
The trinary if-then-else operator.
const irep_idt & id() const
message_handlert & get_message_handler()
mstreamt & result() const
A base class for quantifier expressions.
const irep_idt & get_statement() const
Expression to hold a symbol (variable)
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
exprt value
Initial value of symbol.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
#define Forall_operands(it, expr)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
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.
static symbol_exprt find_base_symbol(const exprt &expr)
static exprt convert_statement_expression(const quantifier_exprt &qex, const code_expressiont &code, const irep_idt &mode, symbol_table_baset &symbol_table, message_handlert &message_handler)
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Compute natural loops in a goto_function.
natural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > natural_loops_mutablet
std::list< patht > pathst
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
side_effect_exprt & to_side_effect_expr(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
code_expressiont & to_code_expression(codet &code)
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.