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)
141 std::list<loop_idt> result;
165 result.front() == loop_id,
"Leaving a loop we haven't entered.");
170 INVARIANT(!result.empty(),
"The assignable violation is not in a loop.");
178 std::list<loop_idt> result;
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.");
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.");
340 "We must have entered the transformed loop before reaching the end");
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;
381 if(!step.full_lhs_value.is_nil())
397 step.pc->source_location().get_function() ==
409 if(
id2string(symbol->get_identifier()) !=
"malloc::malloc_size")
411 live_variables.emplace(step.full_lhs);
423 const auto width =
bv_type->get_width();
444 step.full_lhs_value) &&
450 step.full_lhs_value);
493 loop_entry_offsets[step.full_lhs] = offset;
500 havoced_pointer_offsets[step.full_lhs] = offset;
532 havoced_pointer_offsets,
583 cont.unwind_transformed_loops =
false;
584 cont.apply_loop_contracts();
604 const resultt result = (*checker)();
624 INVARIANT(
false,
"Verification failed during loop contract synthesis.");
640 if(
it_property->second.description.find(
"assignable") != std::string::npos)
684 log.
debug() <<
"Violation description: "
691 cext result(violation_type);
704 const std::list<loop_idt> cause_loop_ids =
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
727 cause_loop_ids.front(),
737 cause_loop_ids.front().loop_number,
740 ->source_location());
743 return_cex.violation_location = violation_location;
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
irep_idt target_violation_id
void restore_functions()
Restore transformed functions to original functions.
optionalt< cext > verify()
Verify goto_model.
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
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
The Boolean constant false.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
goto_functionst goto_functions
GOTO functions.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
const irep_idt & id() const
void set_verbosity(unsigned _verbosity)
unsigned get_verbosity() const
message_handlert & get_message_handler()
A numerical identifier for the object a pointer points to.
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.
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.
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'.
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 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.