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";
72 natural_loops.
loop_map.size() == 0,
"quantifier must not contain loops");
74 std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
93 declared_symbols.insert(it->decl_symbol());
99 "expression statements must contain a terminator expression");
103 last_expr.id() == ID_typecast &&
112 std::vector<goto_programt::const_targett> paths;
113 std::vector<std::pair<exprt, replace_mapt>> path_conditions_and_value_maps;
116 std::vector<goto_programt::const_targett> paths,
117 std::vector<std::pair<exprt, replace_mapt>>
118 path_conditions_and_value_maps)
120 path_conditions_and_value_maps(path_conditions_and_value_maps)
126 return paths.empty();
134 exprt &back_path_condition()
136 return path_conditions_and_value_maps.back().first;
141 return path_conditions_and_value_maps.back().second;
146 exprt path_condition,
149 paths.push_back(target);
150 path_conditions_and_value_maps.push_back(
151 std::make_pair(path_condition, value_map));
157 path_conditions_and_value_maps.pop_back();
168 while(!paths.empty())
170 auto ¤t_it = paths.back_it();
171 auto &path_condition = paths.back_path_condition();
172 auto &value_map = paths.back_value_map();
180 switch(current_it->type())
184 declared_symbols.insert(current_it->decl_symbol());
192 auto lhs = current_it->assign_lhs();
195 "quantifier must not contain side effects");
196 exprt rhs = current_it->assign_rhs();
198 value_map[lhs] = rhs;
214 exprt condition = current_it->condition();
218 auto next_it = current_it->targets.front();
219 exprt copy_path_condition = path_condition;
223 next_it,
and_exprt(copy_path_condition, condition), value_map);
227 current_it = current_it->targets.front();
237 if(current_it == last)
239 exprt copy_of_last_expr = last_expr;
291 new_symbol.
value = expr;
297 result.add_source_location() = source_location;
306 convert(code_assign, dest, mode);
312 targets.scope_stack.add(std::move(code_dead), {});
326 expr.
id() == ID_side_effect || expr.
id() == ID_compound_literal ||
327 expr.
id() == ID_comma)
346 if(expr.
id() == ID_forall || expr.
id() == ID_exists)
356 for(
const auto &op : expr.
operands())
369 expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies);
375 "' must be Boolean, but got ",
384 std::move(implies->lhs()),
385 std::move(implies->rhs()),
396 if(expr.
id() == ID_and)
406 for(exprt::operandst::reverse_iterator it = ops.rbegin(); it != ops.rend();
413 "boolean operators must have only boolean operands",
416 if(expr.
id() == ID_and)
424 if(expr.
id() == ID_or)
454 if(expr.
id() == ID_and || expr.
id() == ID_or || expr.
id() == ID_implies)
460 return clean_expr(expr, mode, result_is_used);
462 else if(expr.
id() == ID_if)
481 "condition for an 'if' must be boolean",
582 else if(expr.
id() == ID_comma)
592 bool last = (it == --expr.
operands().end());
628 else if(expr.
id() == ID_typecast)
641 else if(expr.
id() == ID_side_effect)
646 if(statement == ID_gcc_conditional_expression)
651 else if(statement == ID_statement_expression)
658 else if(statement == ID_assign)
663 "side-effect assignment expressions must have two operands");
668 side_effect_assign.rhs().id() == ID_side_effect &&
674 exprt lhs = side_effect_assign.lhs();
688 side_effect_assign.rhs(), new_lhs.
type());
694 expr = must_use_rhs ? new_rhs : lhs;
702 else if(expr.
id() == ID_forall || expr.
id() == ID_exists)
708 (code.operands()[0].id() == ID_side_effect &&
709 code.operands()[0].get_named_sub()[ID_statement].id() ==
710 ID_statement_expression),
711 "quantifier must not contain side effects");
715 code.operands()[0].id() == ID_side_effect &&
716 code.operands()[0].get_named_sub()[ID_statement].id() ==
717 ID_statement_expression)
724 else if(expr.
id() == ID_address_of)
737 if(expr.
id() == ID_side_effect)
742 else if(expr.
id() == ID_compound_literal)
746 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
761 if(expr.
id() == ID_compound_literal)
764 expr.
operands().size() == 1,
"ID_compound_literal has a single operand");
769 else if(expr.
id() == ID_string_constant)
774 else if(expr.
id() == ID_index)
780 else if(expr.
id() == ID_dereference)
785 else if(expr.
id() == ID_comma)
794 bool last = (it == --expr.
operands().end());
814 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
mstreamt & result() const
A base class for quantifier expressions.
const irep_idt & get_statement() const
Expression to hold a symbol (variable)
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, goto_convertt &converter)
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.