27#include <unordered_map>
31 if(expr.
id() == ID_symbol)
35 else if(expr.
id() == ID_member)
39 else if(expr.
id() == ID_index)
43 else if(expr.
id() == ID_dereference)
47 else if(expr.
id() == ID_typecast)
51 else if(expr.
id() == ID_address_of)
57 throw "unsupported expression type for finding base symbol";
75 natural_loops.
loop_map.size() == 0,
"quantifier must not contain loops");
77 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
96 declared_symbols.insert(it->decl_symbol());
102 "expression statements must contain a terminator expression");
106 last_expr.id() == ID_typecast &&
115 std::vector<goto_programt::const_targett> paths;
116 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
119 std::vector<goto_programt::const_targett> paths,
120 std::vector<std::pair<exprt, replace_mapt>>
121 path_conditions_and_value_maps)
123 path_conditions_and_value_maps(path_conditions_and_value_maps)
129 return paths.empty();
137 exprt &back_path_condition()
139 return path_conditions_and_value_maps.back().first;
144 return path_conditions_and_value_maps.back().second;
149 exprt path_condition,
152 paths.push_back(target);
153 path_conditions_and_value_maps.push_back(
154 std::make_pair(path_condition, value_map));
160 path_conditions_and_value_maps.pop_back();
171 while(!paths.empty())
173 auto ¤t_it = paths.back_it();
174 auto &path_condition = paths.back_path_condition();
175 auto &value_map = paths.back_value_map();
183 switch(current_it->type())
187 declared_symbols.insert(current_it->decl_symbol());
195 auto lhs = current_it->assign_lhs();
198 "quantifier must not contain side effects");
199 exprt rhs = current_it->assign_rhs();
201 value_map[lhs] = rhs;
217 exprt condition = current_it->condition();
219 if(condition !=
true)
221 auto next_it = current_it->targets.front();
222 exprt copy_path_condition = path_condition;
226 next_it,
and_exprt(copy_path_condition, condition), value_map);
230 current_it = current_it->targets.front();
240 if(current_it == last)
242 exprt copy_of_last_expr = last_expr;
294 new_symbol.
value = expr;
300 result.add_source_location() = source_location;
309 convert(code_assign, dest, mode);
315 targets.scope_stack.add(std::move(code_dead), {});
329 expr.
id() == ID_side_effect || expr.
id() == ID_compound_literal ||
330 expr.
id() == ID_comma)
349 if(expr.
id() == ID_forall || expr.
id() == ID_exists)
359 for(
const auto &op : expr.
operands())
372 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
378 "' must be Boolean, but got ",
387 std::move(implies->lhs()),
388 std::move(implies->rhs()),
399 if(expr.
id() == ID_and)
409 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
416 "boolean operators must have only boolean operands",
419 if(expr.
id() == ID_and)
427 if(expr.
id() == ID_or)
457 if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
463 return clean_expr(expr, mode, result_is_used);
465 else if(expr.
id() == ID_if)
484 "condition for an 'if' must be boolean",
585 else if(expr.
id() == ID_comma)
595 bool last = (it == --expr.
operands().end());
631 else if(expr.
id() == ID_typecast)
644 else if(expr.
id() == ID_side_effect)
649 if(statement == ID_gcc_conditional_expression)
654 else if(statement == ID_statement_expression)
661 else if(statement == ID_assign)
666 "side-effect assignment expressions must have two operands");
671 side_effect_assign.rhs().id() == ID_side_effect &&
677 exprt lhs = side_effect_assign.lhs();
691 side_effect_assign.rhs(), new_lhs.
type());
697 expr = must_use_rhs ? new_rhs : lhs;
705 else if(expr.
id() == ID_forall || expr.
id() == ID_exists)
711 (code.
operands()[0].id() == ID_side_effect &&
712 code.
operands()[0].get_named_sub()[ID_statement].id() ==
713 ID_statement_expression),
714 "quantifier must not contain side effects");
718 code.
operands()[0].id() == ID_side_effect &&
719 code.
operands()[0].get_named_sub()[ID_statement].id() ==
720 ID_statement_expression)
728 else if(expr.
id() == ID_address_of)
737 expr.
id() == ID_side_effect &&
751 if(expr.
id() == ID_side_effect)
756 else if(expr.
id() == ID_compound_literal)
760 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
775 if(expr.
id() == ID_compound_literal)
778 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
783 else if(expr.
id() == ID_string_constant)
788 else if(expr.
id() == ID_index)
794 else if(expr.
id() == ID_dereference)
799 else if(expr.
id() == ID_comma)
808 bool last = (it == --expr.
operands().end());
828 else if(expr.
id() == ID_side_effect)
884 config.ansi_c.argument_evaluation_order ==
887 for(
auto it = arguments.rbegin(); it != arguments.rend(); ++it)
892 for(
auto &argument : arguments)
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
Operator to return the address of an object.
Boolean AND All operands must be boolean, and the result is always boolean.
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)
clean_expr_resultt clean_function_call_operands(exprt &function, exprt::operandst &arguments, const irep_idt &mode)
Remove side effects from the function operand and the argument operands of a function call,...
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.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
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.