cprover
Loading...
Searching...
No Matches
cegis_verifier.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Verifier for Counterexample-Guided Synthesis
4
5Author: Qinheping Hu
6
7\*******************************************************************/
8
11
12#include "cegis_verifier.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/expr_iterator.h>
17#include <util/options.h>
20#include <util/simplify_expr.h>
21
26
32#include <cpp/cprover_library.h>
41#include <solvers/prop/prop.h>
42
43static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
44{
45 for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
46 {
47 if(
48 it->id() == ID_symbol &&
49 to_symbol_expr(*it).get_identifier().starts_with(prefix))
50 {
51 return true;
52 }
53 }
54 return false;
55}
56
57static const exprt &
59{
60 // A NULL-pointer check is the negation of an equation between the checked
61 // pointer and a NULL pointer.
62 // ! (POINTER_OBJECT(NULL) == POINTER_OBJECT(ptr))
63 const equal_exprt &equal_expr = to_equal_expr(to_not_expr(violation).op());
64
65 const pointer_object_exprt &lhs_pointer_object =
66 to_pointer_object_expr(equal_expr.lhs());
67 const pointer_object_exprt &rhs_pointer_object =
68 to_pointer_object_expr(equal_expr.rhs());
69
70 const exprt &lhs_pointer = lhs_pointer_object.operands()[0];
71 const exprt &rhs_pointer = rhs_pointer_object.operands()[0];
72
73 // NULL == ptr
74 if(
75 can_cast_expr<constant_exprt>(lhs_pointer) &&
77 {
78 return rhs_pointer;
79 }
80
81 // Not a equation with NULL on one side.
83}
84
86{
87 // Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
88 remove_asm(goto_model, log.get_message_handler());
90 goto_model, log.get_message_handler(), cprover_cpp_library_factory);
92 goto_model, log.get_message_handler(), cprover_c_library_factory);
93 // library functions may introduce inline assembler
94 while(has_asm(goto_model))
95 {
96 remove_asm(goto_model, log.get_message_handler());
98 goto_model, log.get_message_handler(), cprover_cpp_library_factory);
100 goto_model, log.get_message_handler(), cprover_c_library_factory);
101 }
103
104 add_failed_symbols(goto_model.symbol_table);
105
108}
109
111cegis_verifiert::extract_violation_type(const std::string &description)
112{
113 // The violation is a pointer OOB check.
114 if((description.find(
115 "dereference failure: pointer outside object bounds in") !=
116 std::string::npos))
117 {
119 }
120
121 // The violation is a null pointer check.
122 if(description.find("pointer NULL") != std::string::npos)
123 {
125 }
126
127 // The violation is a loop-invariant-preservation check.
128 if(description.find("preserved") != std::string::npos)
129 {
131 }
132
133 // The violation is a loop-invariant-preservation check.
134 if(description.find("invariant before entry") != std::string::npos)
135 {
137 }
138
139 // The violation is an assignable check.
140 if(description.find("assignable") != std::string::npos)
141 {
143 }
144
146}
147
148std::list<loop_idt>
150{
151 std::list<loop_idt> result;
152
153 // We say a loop is the cause loop of an assignable-violation if the inclusion
154 // check is in the loop.
155
156 // So we check what loops the last step of the trace is in.
157 // Transformed loop head:
158 // ASSIGN entered_loop = false
159 // Transformed loop end:
160 // ASSIGN entered_loop = true
161 for(const auto &step : goto_trace.steps)
162 {
163 // We are entering a loop.
164 if(is_transformed_loop_head(step.pc))
165 {
166 result.push_front(
167 loop_idt(step.function_id, original_loop_number_map[step.pc]));
168 }
169 // We are leaving a loop.
170 else if(is_transformed_loop_end(step.pc))
171 {
172 const loop_idt loop_id(
173 step.function_id, original_loop_number_map[step.pc]);
174 INVARIANT(
175 result.front() == loop_id, "Leaving a loop we haven't entered.");
176 result.pop_front();
177 }
178 }
179
180 INVARIANT(!result.empty(), "The assignable violation is not in a loop.");
181 return result;
182}
183
185 const goto_tracet &goto_trace,
186 const goto_programt::const_targett violation)
187{
188 std::list<loop_idt> result;
189
190 // build the dependence graph
191 dependence_grapht dependence_graph(ns, log.get_message_handler());
192 dependence_graph(goto_model);
193
194 // Checking if `to` is dependent on `from`.
195 // `from` : loop havocing
196 // `to` : violation
197
198 // Get `to`---the instruction where the violation happens
199 irep_idt to_fun_name = goto_trace.get_last_step().function_id;
200 const goto_functionst::goto_functiont &to_function =
201 goto_model.get_goto_function(to_fun_name);
202 goto_programt::const_targett to = to_function.body.instructions.end();
203 for(goto_programt::const_targett it = to_function.body.instructions.begin();
204 it != to_function.body.instructions.end();
205 ++it)
206 {
207 if(it->location_number == violation->location_number)
208 {
209 to = it;
210 }
211 }
212
213 INVARIANT(
214 to != to_function.body.instructions.end(),
215 "There must be a violation in a trace.");
216
217 // Compute the backward reachable set.
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());
222
223 // A loop is the cause loop if the violation is dependent on the write set of
224 // the loop.
225 for(const auto &step : goto_trace.steps)
226 {
227 // Being dependent on a write set is equivalent to being dependent on one
228 // of the loop havocing instruction.
229 if(loop_havoc_set.count(step.pc))
230 {
231 // Get `from`---a loop havoc instruction.
232 irep_idt from_fun_name = step.function_id;
233 const goto_functionst::goto_functiont &from_function =
234 goto_model.get_goto_function(from_fun_name);
235 goto_programt::const_targett from = from_function.body.instructions.end();
237 from_function.body.instructions.begin();
238 it != from_function.body.instructions.end();
239 ++it)
240 {
241 if(it->location_number == step.pc->location_number)
242 {
243 from = it;
244 }
245 }
246
247 INVARIANT(
248 from != from_function.body.instructions.end(),
249 "Failed to find the location number of the loop havoc.");
250
251 // The violation is caused by the loop havoc
252 // if it is dependent on the loop havoc.
253 if(reachable_set.count(dependence_graph[from].get_node_id()))
254 {
255 result.push_back(
256 loop_idt(step.function_id, original_loop_number_map[step.pc]));
257 return result;
258 }
259 }
260 }
261 return result;
262}
263
265 const loop_idt &loop_id,
266 const goto_functiont &function,
267 unsigned location_number_of_target)
268{
270 loop_id, function, location_number_of_target))
271 {
273 }
274
276 loop_id, function, location_number_of_target))
277 {
279 }
280
282}
283
285 const loop_idt &loop_id,
286 const goto_functiont &function,
287 unsigned location_number_of_target)
288{
289 // The transformed loop condition is a set of instructions from
290 // loop havocing instructions
291 // to
292 // if(!guard) GOTO EXIT
293 unsigned location_number_of_havocing = 0;
294 for(auto it = function.body.instructions.begin();
295 it != function.body.instructions.end();
296 ++it)
297 {
298 // Record the location number of the beginning of a transformed loop.
299 if(
300 loop_havoc_set.count(it) &&
302 {
303 location_number_of_havocing = it->location_number;
304 }
305
306 // Reach the end of the evaluation of the transformed loop condition.
307 if(location_number_of_havocing != 0 && it->is_goto())
308 {
309 if((location_number_of_havocing < location_number_of_target &&
310 location_number_of_target < it->location_number))
311 {
312 return true;
313 }
314 location_number_of_havocing = 0;
315 }
316 }
317 return false;
318}
319
321 const loop_idt &loop_id,
322 const goto_functiont &function,
323 unsigned location_number_of_target)
324{
325 // The loop body after transformation are instructions from
326 // loop havocing instructions
327 // to
328 // loop end of transformed code.
329 unsigned location_number_of_havocing = 0;
330
331 for(goto_programt::const_targett it = function.body.instructions.begin();
332 it != function.body.instructions.end();
333 ++it)
334 {
335 // Record the location number of the begin of a transformed loop.
336 if(
337 loop_havoc_set.count(it) &&
339 {
340 location_number_of_havocing = it->location_number;
341 }
342
343 // Reach the end of a transformed loop.
344 if(
347 {
348 INVARIANT(
349 location_number_of_havocing != 0,
350 "We must have entered the transformed loop before reaching the end");
351
352 // Check if `location_number_of_target` is between the begin and the end
353 // of the transformed loop.
354 if((location_number_of_havocing < location_number_of_target &&
355 location_number_of_target < it->location_number))
356 {
357 return true;
358 }
359 }
360 }
361
362 return false;
363}
364
366 const goto_tracet &goto_trace,
367 const source_locationt &loop_entry_loc)
368{
369 // Valuations of havoced variables right after havoc instructions.
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;
373
374 // Loop-entry valuations of havoced variables.
375 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
376 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
377
378 // Live variables upon the loop head.
379 std::set<exprt> live_variables;
380
381 bool entered_loop = false;
382
383 // Scan the trace step by step to store needed valuations.
384 for(const auto &step : goto_trace.steps)
385 {
386 switch(step.type)
387 {
390 {
391 if(!step.full_lhs_value.is_nil())
392 {
393 // Entered loop?
395 entered_loop = step.full_lhs_value == true_exprt();
396
397 // skip hidden steps
398 if(step.hidden)
399 break;
400
401 // Live variables
402 // 1. must be in the same function as the target loop;
403 // 2. alive before entering the target loop;
404 // 3. a pointer or a primitive-typed variable;
405 // TODO: add support for union pointer
406 if(
407 step.pc->source_location().get_function() ==
408 loop_entry_loc.get_function() &&
409 !entered_loop &&
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)
414 {
415 const auto &symbol =
417
418 // malloc_size is not-hidden tmp variable.
419 if(id2string(symbol->get_identifier()) != "malloc::malloc_size")
420 {
421 live_variables.emplace(step.full_lhs);
422 }
423 }
424
425 // Record valuation of primitive-typed variable.
426 if(
427 step.full_lhs.type().id() == ID_unsignedbv ||
428 step.full_lhs.type().id() == ID_signedbv)
429 {
430 bool is_signed = step.full_lhs.type().id() == ID_signedbv;
431 const auto &bv_type =
432 type_try_dynamic_cast<bitvector_typet>(step.full_lhs.type());
433 const auto width = bv_type->get_width();
434 // Store the value into the map for loop_entry value if we haven't
435 // entered the loop.
436 if(!entered_loop)
437 {
438 loop_entry_values[step.full_lhs] = bvrep2integer(
439 step.full_lhs_value.get_string(ID_value), width, is_signed);
440 }
441
442 // Store the value into the the map for havoced value if this step
443 // is a loop havocing instruction.
444 if(loop_havoc_set.count(step.pc))
445 {
446 havoced_values[step.full_lhs] = bvrep2integer(
447 step.full_lhs_value.get_string(ID_value), width, is_signed);
448 }
449 }
450
451 // Record object_size, pointer_offset, and loop_entry(pointer_offset).
452 if(
454 step.full_lhs_value) &&
456 step.full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
457 {
458 const auto &pointer_constant_expr =
460 step.full_lhs_value);
461
462 pointer_arithmetict pointer_arithmetic(
463 pointer_constant_expr->symbolic_pointer());
464 if(pointer_constant_expr->symbolic_pointer().id() == ID_typecast)
465 {
466 pointer_arithmetic = pointer_arithmetict(
467 pointer_constant_expr->symbolic_pointer().operands()[0]);
468 }
469
470 // Extract object size.
471 exprt &underlying_array = pointer_arithmetic.pointer;
472 // Object sizes are stored in the type of underlying arrays.
473 while(!can_cast_type<array_typet>(underlying_array.type()))
474 {
475 if(
476 underlying_array.id() == ID_address_of ||
477 underlying_array.id() == ID_index ||
478 underlying_array.id() == ID_typecast)
479 {
480 underlying_array = underlying_array.operands()[0];
481 continue;
482 }
484 }
486 pointer_offset_size(to_array_type(underlying_array.type()), ns)
487 .value();
488 object_sizes[step.full_lhs] = object_size;
489
490 // Extract offsets.
491 mp_integer offset = 0;
492 if(pointer_arithmetic.offset.is_not_nil())
493 {
494 constant_exprt offset_expr =
495 expr_dynamic_cast<constant_exprt>(pointer_arithmetic.offset);
496 offset = bvrep2integer(
497 offset_expr.get_value(), size_type().get_width(), false);
498 }
499
500 // Store the offset into the map for loop_entry if we haven't
501 // entered the loop.
502 if(!entered_loop)
503 {
504 loop_entry_offsets[step.full_lhs] = offset;
505 }
506
507 // Store the offset into the the map for havoced offset if this step
508 // is a loop havocing instruction.
509 if(loop_havoc_set.count(step.pc))
510 {
511 havoced_pointer_offsets[step.full_lhs] = offset;
512 }
513 }
514 }
515 }
516
533 break;
534
537 }
538 }
539
540 return cext(
541 object_sizes,
542 havoced_values,
543 havoced_pointer_offsets,
544 loop_entry_values,
545 loop_entry_offsets,
546 live_variables);
547}
548
550{
551 for(auto &[fun_name, orig_fun_body] : original_functions)
552 goto_model.goto_functions.function_map[fun_name].body.swap(orig_fun_body);
553}
554
555std::optional<cext> cegis_verifiert::verify()
556{
557 // This method does the following three things to verify the `goto_model` and
558 // return a formatted counterexample if there is any violated property.
559 //
560 // 1. annotate and apply the loop contracts stored in `invariant_candidates`.
561 //
562 // 2. run the CBMC API to verify the instrumented goto model. As the API is
563 // not merged yet, we preprocess the goto model and run the symex checker
564 // on it to simulate CBMC API.
565 // TODO: ^^^ replace the symex checker once the real API is merged.
566 //
567 // 3. construct the formatted counterexample from the violated property and
568 // its trace.
569
570 // Store the original functions when they have a body (library functions might
571 // not yet have one). We will restore them after the verification.
572 for(const auto &fun_entry : goto_model.goto_functions.function_map)
573 {
574 if(fun_entry.second.body_available())
575 original_functions[fun_entry.first].copy_from(fun_entry.second.body);
576 }
577
578 // Annotate the candidates to the goto_model for checking.
580
581 // Annotate assigns
583
584 // Control verbosity. We allow non-error output message only when verbosity
585 // is set to larger than messaget::M_DEBUG.
586 const unsigned original_verbosity = log.get_message_handler().get_verbosity();
587 if(original_verbosity < messaget::M_DEBUG)
588 log.get_message_handler().set_verbosity(messaget::M_ERROR);
589
590 // Apply loop contracts we annotated.
591 code_contractst cont(
592 goto_model, log, loop_contract_configt{true, false, true});
594 original_loop_number_map = cont.get_original_loop_number_map();
595 loop_havoc_set = cont.get_loop_havoc_set();
596
597 // Get the checker same as CBMC api without any flag.
598 // TODO: replace the checker with CBMC api once it is implemented.
599 ui_message_handlert ui_message_handler(log.get_message_handler());
601 std::unique_ptr<
603 checker = std::make_unique<
605 options, ui_message_handler, goto_model);
606
608 goto_model.symbol_table,
609 goto_model.goto_functions,
610 log.get_message_handler());
611
612 // Run the checker to get the result.
613 const resultt result = (*checker)();
614
615 if(original_verbosity >= messaget::M_DEBUG)
616 checker->report();
617
618 // Restore the verbosity.
619 log.get_message_handler().set_verbosity(original_verbosity);
620
621 //
622 // Start to construct the counterexample.
623 //
624
625 if(result == resultt::PASS)
626 {
628 return std::optional<cext>();
629 }
630
631 if(result == resultt::ERROR || result == resultt::UNKNOWN)
632 {
633 INVARIANT(false, "Verification failed during loop contract synthesis.");
634 }
635
636 properties = checker->get_properties();
637 auto target_violation = properties.end();
638
639 // Find target violation---the violation we want to fix next.
640 // A target violation is an assignable violation or the first violation that
641 // is not assignable violation.
642 for(auto it_property = properties.begin(); it_property != properties.end();
643 it_property++)
644 {
645 if(it_property->second.status != property_statust::FAIL)
646 continue;
647
648 // assignable violation found
649 if(it_property->second.description.find("assignable") != std::string::npos)
650 {
651 target_violation = it_property;
652 break;
653 }
654
655 // Store the violation that we want to fix with synthesized
656 // assigns/invariant.
657 // ignore ASSERT FALSE
658 if(
659 target_violation == properties.end() &&
660 simplify_expr(it_property->second.pc->condition(), ns) != false_exprt())
661 {
662 target_violation = it_property;
663 }
664 }
665
666 // All violations are
667 // ASSERT FALSE
668 if(target_violation == properties.end())
669 {
671 return std::optional<cext>();
672 }
673
674 target_violation_id = target_violation->first;
675
676 // Decide the violation type from the description of violation
677 cext::violation_typet violation_type =
678 extract_violation_type(target_violation->second.description);
679
680 // Compute the cause loop---the loop for which we synthesize loop contracts,
681 // and the counterexample.
682
683 // If the violation is an assignable check, we synthesize assigns targets.
684 // In the case, cause loops are all loops the violation is in. We keep
685 // adding the new assigns target to the most-inner loop that does not
686 // contain the new target until the assignable violation is resolved.
687
688 // For other cases, we synthesize loop invariant clauses. We synthesize
689 // invariants for one loop at a time. So we return only the first cause loop
690 // although there can be multiple ones.
691
692 log.debug() << "Start to compute cause loop ids." << messaget::eom;
693 log.debug() << "Violation description: "
694 << target_violation->second.description << messaget::eom;
695
696 const auto &trace = checker->get_traces()[target_violation->first];
697 // Doing assigns-synthesis or invariant-synthesis
698 if(violation_type == cext::violation_typet::cex_assignable)
699 {
700 cext result(violation_type);
702 result.checked_pointer = static_cast<const exprt &>(
703 target_violation->second.pc->condition().find(ID_checked_assigns));
705 return result;
706 }
707
708 // We construct the full counterexample only for violations other than
709 // assignable checks.
710
711 // Although there can be multiple cause loop ids. We only synthesize
712 // loop invariants for the first cause loop.
713 const std::list<loop_idt> cause_loop_ids =
714 get_cause_loop_id(trace, target_violation->second.pc);
715
716 if(cause_loop_ids.empty())
717 {
718 log.debug() << "No cause loop found!" << messaget::eom;
720
721 return cext(violation_type);
722 }
723
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
727 << messaget::eom;
728
729 auto violation_location = cext::violation_locationt::in_loop;
730 // We always strengthen in_clause if the violation is
731 // invariant-not-preserved.
732 if(violation_type != cext::violation_typet::cex_not_preserved)
733 {
734 // Get the location of the violation
735 violation_location = get_violation_location(
736 cause_loop_ids.front(),
737 goto_model.get_goto_function(cause_loop_ids.front().function_id),
738 target_violation->second.pc->location_number);
739 }
740
742
743 auto return_cex = build_cex(
744 trace,
746 cause_loop_ids.front().loop_number,
747 goto_model.goto_functions
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;
754
755 // The pointer checked in the null-pointer-check violation.
756 if(violation_type == cext::violation_typet::cex_null_pointer)
757 {
758 return_cex.checked_pointer = get_checked_pointer_from_null_pointer_check(
759 target_violation->second.pc->condition());
760 }
761
762 return return_cex;
763}
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....
Pointer Dereferencing.
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)
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
unsignedbv_typet size_type()
Definition c_types.cpp:50
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.
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
std::optional< cext > verify()
Verify goto_model.
const namespacet ns
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 optionst & options
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)
goto_modelt & goto_model
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.
exprt checked_pointer
std::list< loop_idt > cause_loop_ids
violation_locationt
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
A constant literal expression.
Definition std_expr.h:3122
const irep_idt & get_value() const
Definition std_expr.h:3130
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3204
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
irep_idt function_id
Definition goto_trace.h:111
Trace of a GOTO program.
Definition goto_trace.h:177
stepst steps
Definition goto_trace.h:180
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition goto_trace.h:205
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.
Definition graph.h:602
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
@ M_DEBUG
Definition message.h:170
@ M_ERROR
Definition message.h:169
static eomt eom
Definition message.h:289
A numerical identifier for the object a pointer points to.
const irep_idt & get_function() const
The Boolean constant true.
Definition std_expr.h:3195
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.
Definition expr_cast.h:135
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.
Definition expr_cast.h:81
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.
Definition expr_cast.h:207
Forward depth-first search iterators These iterators' copy operations are expensive,...
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)
Definition irep.h:44
Goto Checker using Multi-Path Symbolic Execution.
Options.
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.
Pointer Logic.
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.
Definition properties.h:36
resultt
The result of goto verifying.
Definition properties.h:45
@ UNKNOWN
No property was violated, neither was there an error.
Definition properties.h:47
@ PASS
No properties were violated.
Definition properties.h:49
@ ERROR
An error occurred during goto checking.
Definition properties.h:53
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
Program Transformation.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2484
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1407
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Loop contract configurations.
Loop id used to identify loops.
Definition loop_ids.h:28
unsigned int loop_number
Definition loop_ids.h:37
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
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.
Definition utils.cpp:524
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.
Definition utils.cpp:640
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition utils.cpp:508
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.
Definition utils.cpp:725
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition utils.cpp:516
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition utils.cpp:705
#define ENTERED_LOOP
Definition utils.h:26
dstringt irep_idt