47 expr.
id() == ID_symbol &&
84void cegis_verifiert::preprocess_goto_model()
101cegis_verifiert::extract_violation_type(
const std::string &description)
104 if((description.find(
105 "dereference failure: pointer outside object bounds in") !=
112 if(description.find(
"pointer NULL") != std::string::npos)
118 if(description.find(
"preserved") != std::string::npos)
124 if(description.find(
"invariant before entry") != std::string::npos)
130 if(description.find(
"assignable") != std::string::npos)
139cegis_verifiert::get_cause_loop_id_for_assigns(
const goto_tracet &goto_trace)
141 std::list<loop_idt> result;
151 for(
const auto &step : goto_trace.steps)
165 result.front() == loop_id,
"Leaving a loop we haven't entered.");
170 INVARIANT(!result.empty(),
"The assignable violation is not in a loop.");
174std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
178 std::list<loop_idt> result;
182 dependence_graph(goto_model);
191 goto_model.get_goto_function(to_fun_name);
194 it != to_function.body.instructions.end();
197 if(it->location_number == violation->location_number)
204 to != to_function.body.instructions.end(),
205 "There must be a violation in a trace.");
208 const auto reachable_vector =
209 dependence_graph.get_reachable(dependence_graph[to].get_node_id(),
false);
210 const std::set<size_t> reachable_set =
211 std::set<size_t>(reachable_vector.begin(), reachable_vector.end());
215 for(
const auto &step : goto_trace.steps)
222 irep_idt from_fun_name = step.function_id;
224 goto_model.get_goto_function(from_fun_name);
227 from_function.body.instructions.begin();
228 it != from_function.body.instructions.end();
231 if(it->location_number == step.pc->location_number)
238 from != from_function.body.instructions.end(),
239 "Failed to find the location number of the loop havoc.");
243 if(reachable_set.count(dependence_graph[from].get_node_id()))
257 unsigned location_number_of_target)
259 if(is_instruction_in_transformed_loop_condition(
260 loop_id, function, location_number_of_target))
265 if(is_instruction_in_transformed_loop(
266 loop_id, function, location_number_of_target))
274bool cegis_verifiert::is_instruction_in_transformed_loop_condition(
277 unsigned location_number_of_target)
283 unsigned location_number_of_havocing = 0;
293 location_number_of_havocing = it->location_number;
297 if(location_number_of_havocing != 0 && it->is_goto())
299 if((location_number_of_havocing < location_number_of_target &&
300 location_number_of_target < it->location_number))
304 location_number_of_havocing = 0;
310bool cegis_verifiert::is_instruction_in_transformed_loop(
313 unsigned location_number_of_target)
319 unsigned location_number_of_havocing = 0;
330 location_number_of_havocing = it->location_number;
339 location_number_of_havocing != 0,
340 "We must have entered the transformed loop before reaching the end");
344 if((location_number_of_havocing < location_number_of_target &&
345 location_number_of_target < it->location_number))
355cext cegis_verifiert::build_cex(
360 std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
361 std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
362 std::unordered_map<exprt, mp_integer, irep_hash> havoced_pointer_offsets;
365 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
366 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
369 std::set<exprt> live_variables;
371 bool entered_loop =
false;
374 for(
const auto &step : goto_trace.steps)
381 if(!step.full_lhs_value.is_nil())
385 entered_loop = step.full_lhs_value ==
true_exprt();
397 step.pc->source_location().get_function() ==
400 (step.full_lhs.type().id() == ID_unsignedbv ||
401 step.full_lhs.type().id() == ID_signedbv ||
402 step.full_lhs.type().id() == ID_pointer) &&
403 step.full_lhs.id() == ID_symbol)
409 if(
id2string(symbol->get_identifier()) !=
"malloc::malloc_size")
411 live_variables.emplace(step.full_lhs);
417 step.full_lhs.type().id() == ID_unsignedbv ||
418 step.full_lhs.type().id() == ID_signedbv)
420 bool is_signed = step.full_lhs.type().id() == ID_signedbv;
421 const auto &bv_type =
423 const auto width = bv_type->get_width();
429 step.full_lhs_value.get_string(ID_value), width,
is_signed);
437 step.full_lhs_value.get_string(ID_value), width,
is_signed);
444 step.full_lhs_value) &&
448 const auto &pointer_constant_expr =
450 step.full_lhs_value);
453 pointer_constant_expr->symbolic_pointer());
454 if(pointer_constant_expr->symbolic_pointer().id() == ID_typecast)
457 pointer_constant_expr->symbolic_pointer().operands()[0]);
461 exprt &underlying_array = pointer_arithmetic.pointer;
466 underlying_array.
id() == ID_address_of ||
467 underlying_array.
id() == ID_index)
469 underlying_array = underlying_array.
operands()[0];
481 if(pointer_arithmetic.offset.is_not_nil())
493 loop_entry_offsets[step.full_lhs] = offset;
500 havoced_pointer_offsets[step.full_lhs] = offset;
532 havoced_pointer_offsets,
538void cegis_verifiert::restore_functions()
540 for(
const auto &fun_entry : goto_model.goto_functions.function_map)
542 irep_idt fun_name = fun_entry.first;
543 goto_model.goto_functions.function_map[fun_name].body.
swap(
544 original_functions[fun_name]);
564 for(
const auto &fun_entry : goto_model.goto_functions.function_map)
566 original_functions[fun_entry.first].copy_from(fun_entry.second.body);
577 const unsigned original_verbosity = log.get_message_handler().get_verbosity();
583 cont.unwind_transformed_loops =
false;
584 cont.apply_loop_contracts();
591 preprocess_goto_model();
596 options, ui_message_handler, goto_model);
599 goto_model.symbol_table,
600 goto_model.goto_functions,
601 log.get_message_handler());
604 const resultt result = (*checker)();
610 log.get_message_handler().set_verbosity(original_verbosity);
624 INVARIANT(
false,
"Verification failed during loop contract synthesis.");
627 properties = checker->get_properties();
628 auto target_violation = properties.end();
633 for(
auto it_property = properties.begin(); it_property != properties.end();
640 if(it_property->second.description.find(
"assignable") != std::string::npos)
642 target_violation = it_property;
650 target_violation == properties.end() &&
653 target_violation = it_property;
659 if(target_violation == properties.end())
665 target_violation_id = target_violation->first;
669 extract_violation_type(target_violation->second.description);
683 log.debug() <<
"Start to compute cause loop ids." <<
messaget::eom;
684 log.debug() <<
"Violation description: "
687 const auto &trace = checker->get_traces()[target_violation->first];
691 cext result(violation_type);
692 result.cause_loop_ids = get_cause_loop_id_for_assigns(trace);
693 result.checked_pointer =
static_cast<const exprt &
>(
694 target_violation->second.pc->condition().find(ID_checked_assigns));
704 const std::list<loop_idt> cause_loop_ids =
705 get_cause_loop_id(trace, target_violation->second.pc);
707 if(cause_loop_ids.empty())
712 return cext(violation_type);
715 log.debug() <<
"Found cause loop with function id: "
716 << cause_loop_ids.front().function_id
717 <<
", and loop number: " << cause_loop_ids.front().loop_number
726 violation_location = get_violation_location(
727 cause_loop_ids.front(),
728 goto_model.get_goto_function(cause_loop_ids.front().function_id),
729 target_violation->second.pc->location_number);
734 auto return_cex = build_cex(
737 cause_loop_ids.front().loop_number,
738 goto_model.goto_functions
739 .function_map[cause_loop_ids.front().function_id])
740 ->source_location());
741 return_cex.violated_predicate = target_violation->second.pc->condition();
742 return_cex.cause_loop_ids = cause_loop_ids;
743 return_cex.violation_location = violation_location;
744 return_cex.violation_type = violation_type;
750 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::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Verify goto_model.
Formatted counterexample.
@ cex_not_hold_upon_entry
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string::const_iterator end() 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,...
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.
bool has_prefix(const std::string &s, const std::string &prefix)
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.
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.
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.
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
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.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Goto Checker using Multi-Path Symbolic Execution.
nonstd::optional< T > optionalt
bool can_cast_expr< annotated_pointer_constant_exprt >(const exprt &base)
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
optionalt< 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)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
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'.
bool can_cast_expr< constant_exprt >(const exprt &base)
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.
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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.