36 const std::function<
void()> &havoc_code_impl)
76 const exprt &ptr_to_ptr,
111 if(expr.
id() == ID_pointer_object)
126 location, funcall.arguments().at(0), dest);
150 const auto &ptr = funcall.arguments().at(0);
151 const auto &size = funcall.arguments().at(1);
152 if(funcall.arguments().at(2).is_true())
182 validity_checks.push_back(
r_ok_exprt{deref->pointer(), *size_of_expr_opt});
185 for(
const auto &op : expr.
operands())
192 const std::vector<symbol_exprt> &lhs,
193 const std::vector<symbol_exprt> &rhs)
210 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
213 equality_conjunctions[i] =
214 and_exprt(equality_conjunctions[i - 1], component_i_equality);
224 lexicographic_individual_comparisons[0] =
226 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
229 lexicographic_individual_comparisons[i] =
230 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
232 return disjunction(lexicographic_individual_comparisons);
242 std::advance(target, offset);
250 const auto new_target = destination.
insert_before(target, i);
251 for(
auto it : target->incoming_edges)
253 if(it->is_goto() && it->get_target() == target)
254 it->set_target(new_target);
263 instruction.is_goto() &&
265 instruction.turn_into_skip();
281 "Instruction list vs CFG size mismatch.");
285 std::vector<idxt> node_to_scc(cfg.
size(), -1);
286 auto nof_sccs = cfg.
SCCs(node_to_scc);
289 std::vector<int> scc_size(nof_sccs, 0);
290 for(
auto scc : node_to_scc)
293 0 <= scc && scc < nof_sccs,
"Could not determine SCC for instruction");
298 for(
size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
300 auto size = scc_size[scc_id];
306 mstream <<
"Found CFG SCC with size " << size << messaget::eom;
307 for(const auto &node_id : node_to_scc)
309 if(node_to_scc[node_id] == scc_id)
311 const auto &pc = cfg[node_id].PC;
313 mstream << messaget::eom;
325 " (assigned by the contract of ";
349 if(e.
id() == ID_symbol)
364 for(
const auto &e : assigns)
366 if(e.id() == ID_index || e.id() == ID_dereference)
389 auto visitor = [&symbol_table, &mode](
exprt &expr) {
390 if(expr.id() != ID_exists && expr.id() != ID_forall)
396 std::vector<symbol_exprt> fresh_variables;
397 fresh_variables.reserve(quantifier_expression.variables().size());
398 for(
const auto &quantified_variable : quantifier_expression.variables())
402 quantified_variable.type(),
403 id2string(quantified_variable.source_location().get_function()),
405 quantified_variable.source_location(),
410 fresh_variables.push_back(new_symbol.
symbol_expr());
414 exprt where = quantifier_expression.instantiate(fresh_variables);
420 quantifier_expression.variables() = fresh_variables;
421 quantifier_expression.where() = std::move(where);
429 std::unordered_map<exprt, symbol_exprt, irep_hash> ¶meter2history,
438 symbol_table, op, parameter2history, location, mode, history, history_id);
441 if(expr.
id() != ID_old && expr.
id() != ID_loop_entry)
445 const auto &
id = parameter.
id();
447 id == ID_dereference ||
id == ID_member ||
id == ID_symbol ||
448 id == ID_ptrmember ||
id == ID_constant ||
id == ID_typecast ||
451 " expressions is not supported yet.",
490 goto_instruction->complete_goto(label_instruction);
493 expr = entry.first->second;
543 clause.
swap(result.expression_after_replacement);
566 std::string var_name)
571 "var_name is not of instrumented variables.");
573 if(!target->is_assign())
579 return id2string(lhs.get_identifier()).find(
"::" + var_name) !=
589 auto first_index = str.find(prefix);
591 first_index != std::string::npos,
"Prefix not found in the given string");
592 first_index += prefix.length();
595 auto last_index = str.find_first_not_of(
"0123456789", first_index);
596 std::string result = str.substr(first_index, last_index - first_index);
597 return std::stol(result);
607 for(
const auto &t : loop)
612 t->is_goto() && t->get_target() == loop_head &&
613 t->location_number > loop_end->location_number)
617 loop_head != loop_end,
618 "Could not find end of the loop starting at: " +
619 loop_head->source_location().as_string());
630 for(
const auto &t : loop)
635 t->is_goto() && t->get_target() == loop_head &&
636 t->location_number > loop_end->location_number)
640 loop_head != loop_end,
641 "Could not find end of the loop starting at: " +
642 loop_head->source_location().as_string());
648 const unsigned int target_loop_number,
655 for(
const auto &loop_p : natural_loops.
loop_map)
661 if(loop_end->loop_number == target_loop_number)
689 return static_cast<const exprt &
>(
690 loop_end->condition().find(ID_C_spec_loop_invariant));
695 return static_cast<const exprt &
>(
696 loop_end->condition().find(ID_C_spec_assigns));
702 return static_cast<const exprt &
>(
703 loop_end->condition().find(ID_C_spec_decreases));
708 const bool check_side_effect)
711 if(!invariant.is_nil() && check_side_effect)
716 "Loop invariant is not side-effect free.",
717 loop_end->condition().find_source_location());
730 const bool check_side_effect)
733 if(!decreases_clause.is_nil() && check_side_effect)
738 "Decreases clause is not side-effect free.",
739 loop_end->condition().find_source_location());
742 return decreases_clause;
749 for(
const auto &invariant_map_entry : invariant_map)
751 loop_idt loop_id = invariant_map_entry.first;
760 loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
761 invariant_map_entry.second;
766 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
769 for(
const auto &assigns_map_entry : assigns_map)
771 loop_idt loop_id = assigns_map_entry.first;
779 exprt &condition = loop_end->condition_nonconst();
780 auto assigns =
exprt(ID_target_list);
781 for(
const auto &e : assigns_map_entry.second)
782 assigns.add_to_operands(e);
783 condition.
add(ID_C_spec_assigns) = assigns;
788 const std::map<loop_idt, exprt> &assigns_map,
791 for(
const auto &assigns_map_entry : assigns_map)
793 loop_idt loop_id = assigns_map_entry.first;
801 exprt &condition = loop_end->condition_nonconst();
802 condition.
add(ID_C_spec_assigns) = assigns_map_entry.second;
807 const std::map<
loop_idt, std::vector<exprt>> &decreases_map,
810 for(
const auto &decreases_map_entry : decreases_map)
812 loop_idt loop_id = decreases_map_entry.first;
820 exprt &condition = loop_end->condition_nonconst();
821 auto decreases =
exprt(ID_target_list);
822 for(
const auto &e : decreases_map_entry.second)
823 decreases.add_to_operands(e);
824 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)
unsignedbv_typet size_type()
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.
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
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
bool is_false() const
Return whether the expression is a constant representing false.
void visit_pre(std::function< void(exprt &)>)
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
source_locationt & add_source_location()
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".
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.
instructionst::iterator targett
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
instructionst::const_iterator const_targett
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
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
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'.
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
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.
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)
bool has_prefix(const std::string &s, const std::string &prefix)
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.
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
natural_loops_mutablet::natural_loopt loopt
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...
bool can_cast_expr< symbol_exprt >(const exprt &base)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_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.
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
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.
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.
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_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.
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.
static exprt extract_loop_assigns(const goto_programt::const_targett &loop_end)
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
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.
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.
static exprt extract_loop_decreases(const goto_programt::const_targett &loop_end)
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
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.
static exprt extract_loop_invariants(const goto_programt::const_targett &loop_end)
Extract loop invariants from loop end without any checks.
std::map< loop_idt, exprt > invariant_mapt
#define IN_LOOP_HAVOC_BLOCK