48 it->id() == ID_symbol &&
114 if((description.find(
115 "dereference failure: pointer outside object bounds in") !=
122 if(description.find(
"pointer NULL") != std::string::npos)
128 if(description.find(
"preserved") != std::string::npos)
134 if(description.find(
"invariant before entry") != std::string::npos)
140 if(description.find(
"assignable") != std::string::npos)
151 std::list<loop_idt> result;
161 for(
const auto &step : goto_trace.
steps)
175 result.front() == loop_id,
"Leaving a loop we haven't entered.");
180 INVARIANT(!result.empty(),
"The assignable violation is not in a loop.");
188 std::list<loop_idt> result;
204 it != to_function.body.instructions.end();
207 if(it->location_number == violation->location_number)
214 to != to_function.body.instructions.end(),
215 "There must be a violation in a trace.");
218 const auto reachable_vector =
219 dependence_graph.
get_reachable(dependence_graph[to].get_node_id(),
false);
220 const std::set<size_t> reachable_set =
221 std::set<size_t>(reachable_vector.begin(), reachable_vector.end());
225 for(
const auto &step : goto_trace.
steps)
232 irep_idt from_fun_name = step.function_id;
237 from_function.body.instructions.begin();
238 it != from_function.body.instructions.end();
241 if(it->location_number == step.pc->location_number)
248 from != from_function.body.instructions.end(),
249 "Failed to find the location number of the loop havoc.");
253 if(reachable_set.count(dependence_graph[from].get_node_id()))
267 unsigned location_number_of_target)
270 loop_id, function, location_number_of_target))
276 loop_id, function, location_number_of_target))
287 unsigned location_number_of_target)
293 unsigned location_number_of_havocing = 0;
303 location_number_of_havocing = it->location_number;
307 if(location_number_of_havocing != 0 && it->is_goto())
309 if((location_number_of_havocing < location_number_of_target &&
310 location_number_of_target < it->location_number))
314 location_number_of_havocing = 0;
323 unsigned location_number_of_target)
329 unsigned location_number_of_havocing = 0;
340 location_number_of_havocing = it->location_number;
349 location_number_of_havocing != 0,
350 "We must have entered the transformed loop before reaching the end");
354 if((location_number_of_havocing < location_number_of_target &&
355 location_number_of_target < it->location_number))
370 std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
371 std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
372 std::unordered_map<exprt, mp_integer, irep_hash> havoced_pointer_offsets;
375 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
376 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
379 std::set<exprt> live_variables;
381 bool entered_loop =
false;
384 for(
const auto &step : goto_trace.
steps)
391 if(!step.full_lhs_value.is_nil())
395 entered_loop = step.full_lhs_value ==
true_exprt();
407 step.pc->source_location().get_function() ==
410 (step.full_lhs.type().id() == ID_unsignedbv ||
411 step.full_lhs.type().id() == ID_signedbv ||
412 step.full_lhs.type().id() == ID_pointer) &&
413 step.full_lhs.id() == ID_symbol)
419 if(
id2string(symbol->get_identifier()) !=
"malloc::malloc_size")
421 live_variables.emplace(step.full_lhs);
427 step.full_lhs.type().id() == ID_unsignedbv ||
428 step.full_lhs.type().id() == ID_signedbv)
430 bool is_signed = step.full_lhs.type().id() == ID_signedbv;
431 const auto &bv_type =
433 const auto width = bv_type->get_width();
439 step.full_lhs_value.get_string(ID_value), width,
is_signed);
447 step.full_lhs_value.get_string(ID_value), width,
is_signed);
454 step.full_lhs_value) &&
458 const auto &pointer_constant_expr =
460 step.full_lhs_value);
463 pointer_constant_expr->symbolic_pointer());
464 if(pointer_constant_expr->symbolic_pointer().id() == ID_typecast)
467 pointer_constant_expr->symbolic_pointer().operands()[0]);
476 underlying_array.
id() == ID_address_of ||
477 underlying_array.
id() == ID_index ||
478 underlying_array.
id() == ID_typecast)
480 underlying_array = underlying_array.
operands()[0];
504 loop_entry_offsets[step.full_lhs] = offset;
511 havoced_pointer_offsets[step.full_lhs] = offset;
543 havoced_pointer_offsets,
552 goto_model.goto_functions.function_map[fun_name].body.swap(orig_fun_body);
572 for(
const auto &fun_entry :
goto_model.goto_functions.function_map)
574 if(fun_entry.second.body_available())
586 const unsigned original_verbosity =
log.get_message_handler().get_verbosity();
603 checker = std::make_unique<
610 log.get_message_handler());
613 const resultt result = (*checker)();
619 log.get_message_handler().set_verbosity(original_verbosity);
628 return std::optional<cext>();
633 INVARIANT(
false,
"Verification failed during loop contract synthesis.");
649 if(it_property->second.description.find(
"assignable") != std::string::npos)
651 target_violation = it_property;
662 target_violation = it_property;
671 return std::optional<cext>();
693 log.debug() <<
"Violation description: "
696 const auto &trace = checker->get_traces()[target_violation->first];
700 cext result(violation_type);
703 target_violation->second.pc->condition().find(ID_checked_assigns));
713 const std::list<loop_idt> cause_loop_ids =
716 if(cause_loop_ids.empty())
721 return cext(violation_type);
724 log.debug() <<
"Found cause loop with function id: "
725 << cause_loop_ids.front().function_id
726 <<
", and loop number: " << cause_loop_ids.front().loop_number
736 cause_loop_ids.front(),
737 goto_model.get_goto_function(cause_loop_ids.front().function_id),
738 target_violation->second.pc->location_number);
746 cause_loop_ids.front().loop_number,
748 .function_map[cause_loop_ids.front().function_id])
749 ->source_location());
750 return_cex.violated_predicate = target_violation->second.pc->condition();
751 return_cex.cause_loop_ids = cause_loop_ids;
752 return_cex.violation_location = violation_location;
753 return_cex.violation_type = violation_type;
759 target_violation->second.pc->condition());
void add_failed_symbols(symbol_table_baset &symbol_table)
Create a failed-dereference symbol for all symbols in the given table that need one (i....
Goto verifier for verifying all properties that stores traces.
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
unsignedbv_typet size_type()
static const exprt & get_checked_pointer_from_null_pointer_check(const exprt &violation)
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
Verifier for Counterexample-Guided Synthesis.
std::optional< cext > verify()
Verify goto_model.
irep_idt target_violation_id
void restore_functions()
Restore transformed functions to original functions.
const std::map< loop_idt, std::set< exprt > > & assigns_map
cext build_cex(const goto_tracet &goto_trace, const source_locationt &loop_entry_loc)
cext::violation_locationt get_violation_location(const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target)
std::list< loop_idt > get_cause_loop_id(const goto_tracet &goto_trace, const goto_programt::const_targett violation)
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
bool is_instruction_in_transformed_loop(const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target)
Decide whether the target instruction is in the body of the transformed loop specified by loop_id.
const invariant_mapt & invariant_candidates
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Map from instrumented instructions for loop contracts to their original loop numbers.
cext::violation_typet extract_violation_type(const std::string &description)
std::unordered_map< irep_idt, goto_programt > original_functions
Map from function names to original functions.
void preprocess_goto_model()
Preprocess the goto model to prepare for verification.
propertiest properties
Result counterexample.
std::list< loop_idt > get_cause_loop_id_for_assigns(const goto_tracet &goto_trace)
bool is_instruction_in_transformed_loop_condition(const loop_idt &loop_id, const goto_functiont &function, unsigned location_number_of_target)
Decide whether the target instruction is between the loop-havoc and the evaluation of the loop guard.
Formatted counterexample.
std::list< loop_idt > cause_loop_ids
@ cex_not_hold_upon_entry
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
A constant literal expression.
const irep_idt & get_value() const
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
typet & type()
Return the type of the expression.
The Boolean constant false.
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
std::vector< node_indext > get_reachable(node_indext src, bool forwards) const
Run depth-first search on the graph, starting from a single source node.
const irep_idt & id() const
A numerical identifier for the object a pointer points to.
const irep_idt & get_function() const
The Boolean constant true.
Verify and use annotated invariants and pre/post-conditions.
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
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.
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Forward depth-first search iterators These iterators' copy operations are expensive,...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
Utilities for building havoc code for expressions.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
Goto Checker using Multi-Path Symbolic Execution.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
exprt object_size(const exprt &pointer)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
bool process_goto_program(goto_modelt &goto_model, const optionst &options, messaget &log)
Common processing and simplification of goto_programts.
@ FAIL
The property was violated.
resultt
The result of goto verifying.
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void label_properties(goto_modelt &goto_model)
Set the properties to check.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Loop contract configurations.
Loop id used to identify loops.
bool is_signed(const typet &t)
Convenience function – is the type signed?
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.
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.
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.
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.