35 const std::function<
void()> &havoc_code_impl)
75 const exprt &ptr_to_ptr,
110 if(expr.
id() == ID_pointer_object)
125 location, funcall.arguments().at(0), dest);
149 const auto &ptr = funcall.arguments().at(0);
150 const auto &size = funcall.arguments().at(1);
151 if(funcall.arguments().at(2).is_true())
176 if(
auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
184 for(
const auto &op : expr.
operands())
191 const std::vector<symbol_exprt> &lhs,
192 const std::vector<symbol_exprt> &rhs)
209 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
212 equality_conjunctions[i] =
213 and_exprt(equality_conjunctions[i - 1], component_i_equality);
223 lexicographic_individual_comparisons[0] =
225 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
228 lexicographic_individual_comparisons[i] =
229 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
231 return disjunction(lexicographic_individual_comparisons);
241 std::advance(target, offset);
249 const auto new_target = destination.
insert_before(target, i);
250 for(
auto it : target->incoming_edges)
253 it->set_target(new_target);
262 instruction.is_goto() &&
264 instruction.turn_into_skip();
280 "Instruction list vs CFG size mismatch.");
284 std::vector<idxt> node_to_scc(cfg.
size(), -1);
285 auto nof_sccs = cfg.
SCCs(node_to_scc);
288 std::vector<int> scc_size(nof_sccs, 0);
289 for(
auto scc : node_to_scc)
292 0 <= scc && scc < nof_sccs,
"Could not determine SCC for instruction");
297 for(
size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
299 auto size = scc_size[scc_id];
302 log.conditional_output(
305 mstream <<
"Found CFG SCC with size " << size << messaget::eom;
306 for(const auto &node_id : node_to_scc)
308 if(node_to_scc[node_id] == scc_id)
310 const auto &pc = cfg[node_id].PC;
312 mstream << messaget::eom;
324 " (assigned by the contract of ";
347 for(
const auto &e : assigns)
349 if(e.id() == ID_index || e.id() == ID_dereference)
372 if(expression.
id() == ID_not || expression.
id() == ID_typecast)
379 if(expression.
id() == ID_notequal || expression.
id() == ID_implies)
387 if(expression.
id() == ID_if)
396 if(expression.
id() == ID_and || expression.
id() == ID_or)
401 for(
auto &operand : multi_ary_expression.operands())
406 else if(expression.
id() == ID_exists || expression.
id() == ID_forall)
412 std::vector<symbol_exprt> fresh_variables;
413 fresh_variables.reserve(quantifier_expression.variables().size());
414 for(
const auto &quantified_variable : quantifier_expression.variables())
418 quantified_variable.type(),
419 id2string(quantified_variable.source_location().get_function()),
421 quantified_variable.source_location(),
426 fresh_variables.push_back(new_symbol.
symbol_expr());
430 exprt where = quantifier_expression.instantiate(fresh_variables);
436 quantifier_expression.variables() = fresh_variables;
437 quantifier_expression.where() = std::move(where);
444 std::unordered_map<exprt, symbol_exprt, irep_hash> ¶meter2history,
453 symbol_table, op, parameter2history, location, mode, history, history_id);
456 if(expr.
id() != ID_old && expr.
id() != ID_loop_entry)
460 const auto &
id = parameter.
id();
462 id == ID_dereference ||
id == ID_member ||
id == ID_symbol ||
463 id == ID_ptrmember ||
id == ID_constant ||
id == ID_typecast ||
466 " expressions is not supported yet.",
505 goto_instruction->complete_goto(label_instruction);
508 expr = entry.first->second;
558 clause.
swap(result.expression_after_replacement);
581 std::string var_name)
586 "var_name is not of instrumented variables.");
588 if(!target->is_assign())
594 return id2string(lhs.get_identifier()).find(
"::" + var_name) !=
604 auto first_index = str.find(prefix);
606 first_index != std::string::npos,
"Prefix not found in the given string");
607 first_index += prefix.length();
610 auto last_index = str.find_first_not_of(
"0123456789", first_index);
611 std::string result = str.substr(first_index, last_index - first_index);
612 return std::stol(result);
622 for(
const auto &t : loop)
627 t->is_goto() && t->get_target() == loop_head &&
628 t->location_number > loop_end->location_number)
632 loop_head != loop_end,
633 "Could not find end of the loop starting at: " +
634 loop_head->source_location().as_string());
645 for(
const auto &t : loop)
650 t->is_goto() && t->get_target() == loop_head &&
651 t->location_number > loop_end->location_number)
655 loop_head != loop_end,
656 "Could not find end of the loop starting at: " +
657 loop_head->source_location().as_string());
663 const unsigned int target_loop_number,
670 for(
const auto &loop_p : natural_loops.
loop_map)
676 if(loop_end->loop_number == target_loop_number)
704 for(
const auto &invariant_map_entry : invariant_map)
706 loop_idt loop_id = invariant_map_entry.first;
715 loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
716 invariant_map_entry.second;
721 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
724 for(
const auto &assigns_map_entry : assigns_map)
726 loop_idt loop_id = assigns_map_entry.first;
734 exprt &condition = loop_end->condition_nonconst();
735 auto assigns =
exprt(ID_target_list);
736 for(
const auto &e : assigns_map_entry.second)
737 assigns.add_to_operands(e);
738 condition.
add(ID_C_spec_assigns) = assigns;
743 const std::map<loop_idt, exprt> &assigns_map,
746 for(
const auto &assigns_map_entry : assigns_map)
748 loop_idt loop_id = assigns_map_entry.first;
756 exprt &condition = loop_end->condition_nonconst();
757 condition.
add(ID_C_spec_assigns) = assigns_map_entry.second;
762 const std::map<
loop_idt, std::vector<exprt>> &decreases_map,
765 for(
const auto &decreases_map_entry : decreases_map)
767 loop_idt loop_id = decreases_map_entry.first;
775 exprt &condition = loop_end->condition_nonconst();
776 auto decreases =
exprt(ID_target_list);
777 for(
const auto &e : decreases_map_entry.second)
778 decreases.add_to_operands(e);
779 condition.
add(ID_C_spec_decreases) = decreases;
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
Operator to return the address of an object.
A base class for relations, i.e., binary predicates whose two operands have the same type.
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
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.
std::vector< exprt > operandst
const source_locationt & source_location() const
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
The Boolean constant false.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_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())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
A class containing utility functions for havocing expressions.
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
const exprt & expression() const
const irep_idt & id() const
irept & add(const irep_idt &name)
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A predicate that indicates that an address range is ok to read.
const exprt & pointer() const
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_function() const
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
static exprt conditional_cast(const exprt &expr, const typet &type)
source_locationt & add_source_location()
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.
A Template Class for Graphs.
std::set< exprt > assignst
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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.
API to expression classes for Pointers.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#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_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
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 multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
A total order over targett and const_targett.
Loop id used to identify loops.
std::unordered_map< exprt, symbol_exprt, irep_hash > parameter_to_history
goto_programt history_construction
exprt expression_after_replacement
replace_history_parametert replace_history_old(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.
goto_programt::targett get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
Find and return the last instruction of the natural loop with loop_number in function.
static void append_safe_havoc_code_for_expr(const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
goto_programt::const_targett get_loop_end_from_loop_head_and_content(const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop)
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
goto_programt::targett get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
Find and return the first instruction of the natural loop with loop_number in function.
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
void annotate_decreases(const std::map< loop_idt, std::vector< exprt >> &decreases_map, goto_modelt &goto_model)
Annotate the decreases in decreases_map to their corresponding loops.
goto_programt::targett get_loop_head_or_end(const unsigned int target_loop_number, goto_functiont &function, bool finding_head)
Return loop head if finding_head is true, Otherwise return loop end.
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop)
Find the goto instruction of loop that jumps to loop_head
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
void annotate_assigns(const std::map< loop_idt, std::set< exprt >> &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
static void replace_history_parameter_rec(symbol_table_baset &symbol_table, exprt &expr, std::unordered_map< exprt, symbol_exprt, irep_hash > ¶meter2history, const source_locationt &location, const irep_idt &mode, goto_programt &history, const irep_idt &history_id)
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
std::map< loop_idt, exprt > invariant_mapt
#define IN_LOOP_HAVOC_BLOCK