36 const std::function<
void()> &havoc_code_impl)
78 const exprt &ptr_to_ptr,
113 if(expr.
id() == ID_pointer_object)
128 location, funcall.arguments().at(0), dest);
152 const auto &ptr = funcall.arguments().at(0);
153 const auto &size = funcall.arguments().at(1);
154 if(funcall.arguments().at(2).is_true())
179 if(
auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
187 for(
const auto &op : expr.
operands())
194 const std::vector<symbol_exprt> &lhs,
195 const std::vector<symbol_exprt> &rhs)
212 for(
size_t i = 1; i < equality_conjunctions.size() - 1; i++)
215 equality_conjunctions[i] =
216 and_exprt(equality_conjunctions[i - 1], component_i_equality);
226 lexicographic_individual_comparisons[0] =
228 for(
size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
231 lexicographic_individual_comparisons[i] =
232 and_exprt(equality_conjunctions[i - 1], component_i_less_than);
234 return disjunction(lexicographic_individual_comparisons);
244 std::advance(target, offset);
252 const auto new_target = destination.
insert_before(target, i);
253 for(
auto it : target->incoming_edges)
255 if(it->is_goto() && it->get_target() == target)
256 it->set_target(new_target);
265 instruction.is_goto() &&
267 instruction.turn_into_skip();
283 "Instruction list vs CFG size mismatch.");
287 std::vector<idxt> node_to_scc(cfg.
size(), -1);
288 auto nof_sccs = cfg.
SCCs(node_to_scc);
291 std::vector<int> scc_size(nof_sccs, 0);
292 for(
auto scc : node_to_scc)
295 0 <= scc && scc < nof_sccs,
"Could not determine SCC for instruction");
300 for(
size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
302 auto size = scc_size[scc_id];
305 log.conditional_output(
308 mstream <<
"Found CFG SCC with size " << size << messaget::eom;
309 for(const auto &node_id : node_to_scc)
311 if(node_to_scc[node_id] == scc_id)
313 const auto &pc = cfg[node_id].PC;
315 mstream << messaget::eom;
327 " (assigned by the contract of ";
351 if(e.
id() == ID_symbol)
353 const auto &s = expr_try_dynamic_cast<symbol_exprt>(e);
354 return !has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX);
366 for(
const auto &e : assigns)
368 if(e.id() == ID_index || e.id() == ID_dereference)
389 std::unordered_map<exprt, symbol_exprt, irep_hash> ¶meter2history,
398 symbol_table, op, parameter2history, location, mode, history, history_id);
401 if(expr.
id() != ID_old && expr.
id() != ID_loop_entry)
405 const auto &
id = parameter.
id();
407 id == ID_dereference ||
id == ID_member ||
id == ID_symbol ||
408 id == ID_ptrmember ||
id == ID_constant ||
id == ID_typecast ||
411 " expressions is not supported yet.",
450 goto_instruction->complete_goto(label_instruction);
453 expr = entry.first->second;
503 clause.
swap(result.expression_after_replacement);
526 std::string var_name)
531 "var_name is not of instrumented variables.");
533 if(!target->is_assign())
539 return id2string(lhs.get_identifier()).find(
"::" + var_name) !=
549 auto first_index = str.find(prefix);
551 first_index != std::string::npos,
"Prefix not found in the given string");
552 first_index += prefix.length();
555 auto last_index = str.find_first_not_of(
"0123456789", first_index);
556 std::string result = str.substr(first_index, last_index - first_index);
557 return std::stol(result);
567 for(
const auto &t : loop)
572 t->is_goto() && t->get_target() == loop_head &&
573 t->location_number > loop_end->location_number)
577 loop_head != loop_end,
578 "Could not find end of the loop starting at: " +
579 loop_head->source_location().as_string());
590 for(
const auto &t : loop)
595 t->is_goto() && t->get_target() == loop_head &&
596 t->location_number > loop_end->location_number)
600 loop_head != loop_end,
601 "Could not find end of the loop starting at: " +
602 loop_head->source_location().as_string());
608 const unsigned int target_loop_number,
615 for(
const auto &loop_p : natural_loops.
loop_map)
621 if(loop_end->loop_number == target_loop_number)
649 return static_cast<const exprt &
>(
650 loop_end->condition().find(ID_C_spec_loop_invariant));
655 return static_cast<const exprt &
>(
656 loop_end->condition().find(ID_C_spec_assigns));
662 return static_cast<const exprt &
>(
663 loop_end->condition().find(ID_C_spec_decreases));
668 const bool check_side_effect)
671 if(!invariant.is_nil() && check_side_effect)
676 "Loop invariant is not side-effect free.",
677 loop_end->condition().find_source_location());
690 const bool check_side_effect)
693 if(!decreases_clause.is_nil() && check_side_effect)
698 "Decreases clause is not side-effect free.",
699 loop_end->condition().find_source_location());
702 return decreases_clause;
709 for(
const auto &invariant_map_entry : invariant_map)
711 loop_idt loop_id = invariant_map_entry.first;
720 loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
721 invariant_map_entry.second;
726 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
729 for(
const auto &assigns_map_entry : assigns_map)
731 loop_idt loop_id = assigns_map_entry.first;
739 exprt &condition = loop_end->condition_nonconst();
740 auto assigns =
exprt(ID_target_list);
741 for(
const auto &e : assigns_map_entry.second)
742 assigns.add_to_operands(e);
743 condition.
add(ID_C_spec_assigns) = assigns;
748 const std::map<loop_idt, exprt> &assigns_map,
751 for(
const auto &assigns_map_entry : assigns_map)
753 loop_idt loop_id = assigns_map_entry.first;
761 exprt &condition = loop_end->condition_nonconst();
762 condition.
add(ID_C_spec_assigns) = assigns_map_entry.second;
767 const std::map<
loop_idt, std::vector<exprt>> &decreases_map,
770 for(
const auto &decreases_map_entry : decreases_map)
772 loop_idt loop_id = decreases_map_entry.first;
780 exprt &condition = loop_end->condition_nonconst();
781 auto decreases =
exprt(ID_target_list);
782 for(
const auto &e : decreases_map_entry.second)
783 decreases.add_to_operands(e);
784 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
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'.
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()
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
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.
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
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 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, const 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)
Extract loop assigns from annotated 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.
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.
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.
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
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)
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 decreases 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