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/options.h>
19#include <util/prefix.h>
20
27
31#include <cpp/cprover_library.h>
40#include <solvers/prop/prop.h>
41
42static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
43{
44 for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
45 {
46 if(
47 expr.id() == ID_symbol &&
48 has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix))
49 {
50 return true;
51 }
52 }
53 return false;
54}
55
56static const exprt &
58{
59 // A NULL-pointer check is the negation of an equation between the checked
60 // pointer and a NULL pointer.
61 // ! (POINTER_OBJECT(NULL) == POINTER_OBJECT(ptr))
62 const equal_exprt &equal_expr = to_equal_expr(to_not_expr(violation).op());
63
64 const pointer_object_exprt &lhs_pointer_object =
65 to_pointer_object_expr(equal_expr.lhs());
66 const pointer_object_exprt &rhs_pointer_object =
67 to_pointer_object_expr(equal_expr.rhs());
68
69 const exprt &lhs_pointer = lhs_pointer_object.operands()[0];
70 const exprt &rhs_pointer = rhs_pointer_object.operands()[0];
71
72 // NULL == ptr
73 if(
74 can_cast_expr<constant_exprt>(lhs_pointer) &&
76 {
77 return rhs_pointer;
78 }
79
80 // Not a equation with NULL on one side.
82}
83
84void cegis_verifiert::preprocess_goto_model()
85{
86 // Preprocess `goto_model`. Copied from `cbmc_parse_options.cpp`.
87 remove_asm(goto_model);
89 goto_model, log.get_message_handler(), cprover_cpp_library_factory);
91 goto_model, log.get_message_handler(), cprover_c_library_factory);
92 process_goto_program(goto_model, options, log);
93
94 add_failed_symbols(goto_model.symbol_table);
95
96 remove_skip(goto_model);
97 label_properties(goto_model);
98}
99
101cegis_verifiert::extract_violation_type(const std::string &description)
102{
103 // The violation is a pointer OOB check.
104 if((description.find(
105 "dereference failure: pointer outside object bounds in") !=
106 std::string::npos))
107 {
109 }
110
111 // The violation is a null pointer check.
112 if(description.find("pointer NULL") != std::string::npos)
113 {
115 }
116
117 // The violation is a loop-invariant-preservation check.
118 if(description.find("preserved") != std::string::npos)
119 {
121 }
122
123 // The violation is a loop-invariant-preservation check.
124 if(description.find("invariant before entry") != std::string::npos)
125 {
127 }
128
129 // The violation is an assignable check.
130 if(description.find("assignable") != std::string::npos)
131 {
133 }
134
136}
137
138std::list<loop_idt>
139cegis_verifiert::get_cause_loop_id_for_assigns(const goto_tracet &goto_trace)
140{
141 std::list<loop_idt> result;
142
143 // We say a loop is the cause loop of an assignable-violation if the inclusion
144 // check is in the loop.
145
146 // So we check what loops the last step of the trace is in.
147 // Transformed loop head:
148 // ASSIGN entered_loop = false
149 // Transformed loop end:
150 // ASSIGN entered_loop = true
151 for(const auto &step : goto_trace.steps)
152 {
153 // We are entering a loop.
154 if(is_transformed_loop_head(step.pc))
155 {
156 result.push_front(
157 loop_idt(step.function_id, original_loop_number_map[step.pc]));
158 }
159 // We are leaving a loop.
160 else if(is_transformed_loop_end(step.pc))
161 {
162 const loop_idt loop_id(
163 step.function_id, original_loop_number_map[step.pc]);
164 INVARIANT(
165 result.front() == loop_id, "Leaving a loop we haven't entered.");
166 result.pop_front();
167 }
168 }
169
170 INVARIANT(!result.empty(), "The assignable violation is not in a loop.");
171 return result;
172}
173
174std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
175 const goto_tracet &goto_trace,
176 const goto_programt::const_targett violation)
177{
178 std::list<loop_idt> result;
179
180 // build the dependence graph
181 dependence_grapht dependence_graph(ns);
182 dependence_graph(goto_model);
183
184 // Checking if `to` is dependent on `from`.
185 // `from` : loop havocing
186 // `to` : violation
187
188 // Get `to`---the instruction where the violation happens
189 irep_idt to_fun_name = goto_trace.get_last_step().function_id;
190 const goto_functionst::goto_functiont &to_function =
191 goto_model.get_goto_function(to_fun_name);
192 goto_programt::const_targett to = to_function.body.instructions.end();
193 for(goto_programt::const_targett it = to_function.body.instructions.begin();
194 it != to_function.body.instructions.end();
195 ++it)
196 {
197 if(it->location_number == violation->location_number)
198 {
199 to = it;
200 }
201 }
202
203 INVARIANT(
204 to != to_function.body.instructions.end(),
205 "There must be a violation in a trace.");
206
207 // Compute the backward reachable set.
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());
212
213 // A loop is the cause loop if the violation is dependent on the write set of
214 // the loop.
215 for(const auto &step : goto_trace.steps)
216 {
217 // Being dependent on a write set is equivalent to being dependent on one
218 // of the loop havocing instruction.
219 if(loop_havoc_set.count(step.pc))
220 {
221 // Get `from`---a loop havoc instruction.
222 irep_idt from_fun_name = step.function_id;
223 const goto_functionst::goto_functiont &from_function =
224 goto_model.get_goto_function(from_fun_name);
225 goto_programt::const_targett from = from_function.body.instructions.end();
227 from_function.body.instructions.begin();
228 it != from_function.body.instructions.end();
229 ++it)
230 {
231 if(it->location_number == step.pc->location_number)
232 {
233 from = it;
234 }
235 }
236
237 INVARIANT(
238 from != from_function.body.instructions.end(),
239 "Failed to find the location number of the loop havoc.");
240
241 // The violation is caused by the loop havoc
242 // if it is dependent on the loop havoc.
243 if(reachable_set.count(dependence_graph[from].get_node_id()))
244 {
245 result.push_back(
246 loop_idt(step.function_id, original_loop_number_map[step.pc]));
247 return result;
248 }
249 }
250 }
251 return result;
252}
253
254cext::violation_locationt cegis_verifiert::get_violation_location(
255 const loop_idt &loop_id,
256 const goto_functiont &function,
257 unsigned location_number_of_target)
258{
259 if(is_instruction_in_transformed_loop_condition(
260 loop_id, function, location_number_of_target))
261 {
263 }
264
265 if(is_instruction_in_transformed_loop(
266 loop_id, function, location_number_of_target))
267 {
269 }
270
272}
273
274bool cegis_verifiert::is_instruction_in_transformed_loop_condition(
275 const loop_idt &loop_id,
276 const goto_functiont &function,
277 unsigned location_number_of_target)
278{
279 // The transformed loop condition is a set of instructions from
280 // loop havocing instructions
281 // to
282 // if(!guard) GOTO EXIT
283 unsigned location_number_of_havocing = 0;
284 for(auto it = function.body.instructions.begin();
285 it != function.body.instructions.end();
286 ++it)
287 {
288 // Record the location number of the beginning of a transformed loop.
289 if(
290 loop_havoc_set.count(it) &&
292 {
293 location_number_of_havocing = it->location_number;
294 }
295
296 // Reach the end of the evaluation of the transformed loop condition.
297 if(location_number_of_havocing != 0 && it->is_goto())
298 {
299 if((location_number_of_havocing < location_number_of_target &&
300 location_number_of_target < it->location_number))
301 {
302 return true;
303 }
304 location_number_of_havocing = 0;
305 }
306 }
307 return false;
308}
309
310bool cegis_verifiert::is_instruction_in_transformed_loop(
311 const loop_idt &loop_id,
312 const goto_functiont &function,
313 unsigned location_number_of_target)
314{
315 // The loop body after transformation are instructions from
316 // loop havocing instructions
317 // to
318 // loop end of transformed code.
319 unsigned location_number_of_havocing = 0;
320
321 for(goto_programt::const_targett it = function.body.instructions.begin();
322 it != function.body.instructions.end();
323 ++it)
324 {
325 // Record the location number of the begin of a transformed loop.
326 if(
327 loop_havoc_set.count(it) &&
329 {
330 location_number_of_havocing = it->location_number;
331 }
332
333 // Reach the end of a transformed loop.
334 if(
337 {
338 INVARIANT(
339 location_number_of_havocing != 0,
340 "We must have entered the transformed loop before reaching the end");
341
342 // Check if `location_number_of_target` is between the begin and the end
343 // of the transformed loop.
344 if((location_number_of_havocing < location_number_of_target &&
345 location_number_of_target < it->location_number))
346 {
347 return true;
348 }
349 }
350 }
351
352 return false;
353}
354
355cext cegis_verifiert::build_cex(
356 const goto_tracet &goto_trace,
357 const source_locationt &loop_entry_loc)
358{
359 // Valuations of havoced variables right after havoc instructions.
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;
363
364 // Loop-entry valuations of havoced variables.
365 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
366 std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
367
368 // Live variables upon the loop head.
369 std::set<exprt> live_variables;
370
371 bool entered_loop = false;
372
373 // Scan the trace step by step to store needed valuations.
374 for(const auto &step : goto_trace.steps)
375 {
376 switch(step.type)
377 {
380 {
381 if(!step.full_lhs_value.is_nil())
382 {
383 // Entered loop?
385 entered_loop = step.full_lhs_value == true_exprt();
386
387 // skip hidden steps
388 if(step.hidden)
389 break;
390
391 // Live variables
392 // 1. must be in the same function as the target loop;
393 // 2. alive before entering the target loop;
394 // 3. a pointer or a primitive-typed variable;
395 // TODO: add support for union pointer
396 if(
397 step.pc->source_location().get_function() ==
398 loop_entry_loc.get_function() &&
399 !entered_loop &&
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)
404 {
405 const auto &symbol =
407
408 // malloc_size is not-hidden tmp variable.
409 if(id2string(symbol->get_identifier()) != "malloc::malloc_size")
410 {
411 live_variables.emplace(step.full_lhs);
412 }
413 }
414
415 // Record valuation of primitive-typed variable.
416 if(
417 step.full_lhs.type().id() == ID_unsignedbv ||
418 step.full_lhs.type().id() == ID_signedbv)
419 {
420 bool is_signed = step.full_lhs.type().id() == ID_signedbv;
421 const auto &bv_type =
422 type_try_dynamic_cast<bitvector_typet>(step.full_lhs.type());
423 const auto width = bv_type->get_width();
424 // Store the value into the map for loop_entry value if we haven't
425 // entered the loop.
426 if(!entered_loop)
427 {
428 loop_entry_values[step.full_lhs] = bvrep2integer(
429 step.full_lhs_value.get_string(ID_value), width, is_signed);
430 }
431
432 // Store the value into the the map for havoced value if this step
433 // is a loop havocing instruction.
434 if(loop_havoc_set.count(step.pc))
435 {
436 havoced_values[step.full_lhs] = bvrep2integer(
437 step.full_lhs_value.get_string(ID_value), width, is_signed);
438 }
439 }
440
441 // Record object_size, pointer_offset, and loop_entry(pointer_offset).
442 if(
444 step.full_lhs_value) &&
446 step.full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
447 {
448 const auto &pointer_constant_expr =
450 step.full_lhs_value);
451
452 pointer_arithmetict pointer_arithmetic(
453 pointer_constant_expr->symbolic_pointer());
454 if(pointer_constant_expr->symbolic_pointer().id() == ID_typecast)
455 {
456 pointer_arithmetic = pointer_arithmetict(
457 pointer_constant_expr->symbolic_pointer().operands()[0]);
458 }
459
460 // Extract object size.
461 exprt &underlying_array = pointer_arithmetic.pointer;
462 // Object sizes are stored in the type of underlying arrays.
463 while(!can_cast_type<array_typet>(underlying_array.type()))
464 {
465 if(
466 underlying_array.id() == ID_address_of ||
467 underlying_array.id() == ID_index)
468 {
469 underlying_array = underlying_array.operands()[0];
470 continue;
471 }
473 }
475 pointer_offset_size(to_array_type(underlying_array.type()), ns)
476 .value();
477 object_sizes[step.full_lhs] = object_size;
478
479 // Extract offsets.
480 mp_integer offset = 0;
481 if(pointer_arithmetic.offset.is_not_nil())
482 {
483 constant_exprt offset_expr =
484 expr_dynamic_cast<constant_exprt>(pointer_arithmetic.offset);
485 offset = bvrep2integer(
486 offset_expr.get_value(), size_type().get_width(), false);
487 }
488
489 // Store the offset into the map for loop_entry if we haven't
490 // entered the loop.
491 if(!entered_loop)
492 {
493 loop_entry_offsets[step.full_lhs] = offset;
494 }
495
496 // Store the offset into the the map for havoced offset if this step
497 // is a loop havocing instruction.
498 if(loop_havoc_set.count(step.pc))
499 {
500 havoced_pointer_offsets[step.full_lhs] = offset;
501 }
502 }
503 }
504 }
505
522 break;
523
526 }
527 }
528
529 return cext(
530 object_sizes,
531 havoced_values,
532 havoced_pointer_offsets,
533 loop_entry_values,
534 loop_entry_offsets,
535 live_variables);
536}
537
538void cegis_verifiert::restore_functions()
539{
540 for(const auto &fun_entry : goto_model.goto_functions.function_map)
541 {
542 irep_idt fun_name = fun_entry.first;
543 goto_model.goto_functions.function_map[fun_name].body.swap(
544 original_functions[fun_name]);
545 }
546}
547
548optionalt<cext> cegis_verifiert::verify()
549{
550 // This method does the following three things to verify the `goto_model` and
551 // return a formatted counterexample if there is any violated property.
552 //
553 // 1. annotate and apply the loop contracts stored in `invariant_candidates`.
554 //
555 // 2. run the CBMC API to verify the instrumented goto model. As the API is
556 // not merged yet, we preprocess the goto model and run the symex checker
557 // on it to simulate CBMC API.
558 // TODO: ^^^ replace the symex checker once the real API is merged.
559 //
560 // 3. construct the formatted counterexample from the violated property and
561 // its trace.
562
563 // Store the original functions. We will restore them after the verification.
564 for(const auto &fun_entry : goto_model.goto_functions.function_map)
565 {
566 original_functions[fun_entry.first].copy_from(fun_entry.second.body);
567 }
568
569 // Annotate the candidates to the goto_model for checking.
570 annotate_invariants(invariant_candidates, goto_model);
571
572 // Annotate assigns
573 annotate_assigns(assigns_map, goto_model);
574
575 // Control verbosity. We allow non-error output message only when verbosity
576 // is set to larger than messaget::M_DEBUG.
577 const unsigned original_verbosity = log.get_message_handler().get_verbosity();
578 if(original_verbosity < messaget::M_DEBUG)
579 log.get_message_handler().set_verbosity(messaget::M_ERROR);
580
581 // Apply loop contracts we annotated.
582 code_contractst cont(goto_model, log);
583 cont.unwind_transformed_loops = false;
584 cont.apply_loop_contracts();
585 original_loop_number_map = cont.get_original_loop_number_map();
586 loop_havoc_set = cont.get_loop_havoc_set();
587
588 // Get the checker same as CBMC api without any flag.
589 // TODO: replace the checker with CBMC api once it is implemented.
590 ui_message_handlert ui_message_handler(log.get_message_handler());
591 preprocess_goto_model();
592 std::unique_ptr<
594 checker = util_make_unique<
596 options, ui_message_handler, goto_model);
597
599 goto_model.symbol_table,
600 goto_model.goto_functions,
601 log.get_message_handler());
602
603 // Run the checker to get the result.
604 const resultt result = (*checker)();
605
606 if(original_verbosity >= messaget::M_DEBUG)
607 checker->report();
608
609 // Restore the verbosity.
610 log.get_message_handler().set_verbosity(original_verbosity);
611
612 //
613 // Start to construct the counterexample.
614 //
615
616 if(result == resultt::PASS)
617 {
618 restore_functions();
619 return optionalt<cext>();
620 }
621
622 if(result == resultt::ERROR || result == resultt::UNKNOWN)
623 {
624 INVARIANT(false, "Verification failed during loop contract synthesis.");
625 }
626
627 properties = checker->get_properties();
628 auto target_violation = properties.end();
629
630 // Find target violation---the violation we want to fix next.
631 // A target violation is an assignable violation or the first violation that
632 // is not assignable violation.
633 for(auto it_property = properties.begin(); it_property != properties.end();
634 it_property++)
635 {
636 if(it_property->second.status != property_statust::FAIL)
637 continue;
638
639 // assignable violation found
640 if(it_property->second.description.find("assignable") != std::string::npos)
641 {
642 target_violation = it_property;
643 break;
644 }
645
646 // Store the violation that we want to fix with synthesized
647 // assigns/invariant.
648 // ignore ASSERT FALSE
649 if(
650 target_violation == properties.end() &&
651 simplify_expr(it_property->second.pc->condition(), ns) != false_exprt())
652 {
653 target_violation = it_property;
654 }
655 }
656
657 // All violations are
658 // ASSERT FALSE
659 if(target_violation == properties.end())
660 {
661 restore_functions();
662 return optionalt<cext>();
663 }
664
665 target_violation_id = target_violation->first;
666
667 // Decide the violation type from the description of violation
668 cext::violation_typet violation_type =
669 extract_violation_type(target_violation->second.description);
670
671 // Compute the cause loop---the loop for which we synthesize loop contracts,
672 // and the counterexample.
673
674 // If the violation is an assignable check, we synthesize assigns targets.
675 // In the case, cause loops are all loops the violation is in. We keep
676 // adding the new assigns target to the most-inner loop that does not
677 // contain the new target until the assignable violation is resolved.
678
679 // For other cases, we synthesize loop invariant clauses. We synthesize
680 // invariants for one loop at a time. So we return only the first cause loop
681 // although there can be multiple ones.
682
683 log.debug() << "Start to compute cause loop ids." << messaget::eom;
684 log.debug() << "Violation description: "
685 << target_violation->second.description << messaget::eom;
686
687 const auto &trace = checker->get_traces()[target_violation->first];
688 // Doing assigns-synthesis or invariant-synthesis
689 if(violation_type == cext::violation_typet::cex_assignable)
690 {
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));
695 restore_functions();
696 return result;
697 }
698
699 // We construct the full counterexample only for violations other than
700 // assignable checks.
701
702 // Although there can be multiple cause loop ids. We only synthesize
703 // loop invariants for the first cause loop.
704 const std::list<loop_idt> cause_loop_ids =
705 get_cause_loop_id(trace, target_violation->second.pc);
706
707 if(cause_loop_ids.empty())
708 {
709 log.debug() << "No cause loop found!" << messaget::eom;
710 restore_functions();
711
712 return cext(violation_type);
713 }
714
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
718 << messaget::eom;
719
720 auto violation_location = cext::violation_locationt::in_loop;
721 // We always strengthen in_clause if the violation is
722 // invariant-not-preserved.
723 if(violation_type != cext::violation_typet::cex_not_preserved)
724 {
725 // Get the location of the violation
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);
730 }
731
732 restore_functions();
733
734 auto return_cex = build_cex(
735 trace,
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;
745
746 // The pointer checked in the null-pointer-check violation.
747 if(violation_type == cext::violation_typet::cex_null_pointer)
748 {
749 return_cex.checked_pointer = get_checked_pointer_from_null_pointer_check(
750 target_violation->second.pc->condition());
751 }
752
753 return return_cex;
754}
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:55
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:613
exprt & rhs()
Definition std_expr.h:623
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.
violation_locationt
A constant literal expression.
Definition std_expr.h:2942
const irep_idt & get_value() const
Definition std_expr.h:2950
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
void swap(dstringt &b)
Definition dstring.h:163
std::string::const_iterator end() const
Definition dstring.h:199
Equality.
Definition std_expr.h:1306
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:3017
::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
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
const irep_idt & id() const
Definition irep.h:396
@ M_DEBUG
Definition message.h:171
@ M_ERROR
Definition message.h:170
static eomt eom
Definition message.h:297
A numerical identifier for the object a pointer points to.
const irep_idt & get_function() const
The Boolean constant true.
Definition std_expr.h:3008
Verify and use annotated invariants and pre/post-conditions.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
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.
Definition expr_cast.h:135
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
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:47
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
Goto Checker using Multi-Path Symbolic Execution.
nonstd::optional< T > optionalt
Definition optional.h:35
Options.
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.
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.
resultt
The result of goto verifying.
Definition properties.h:45
@ 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
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:18
#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
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition std_expr.h:2976
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2303
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1347
bool can_cast_type< array_typet >(const typet &type)
Check whether a reference to a typet is a array_typet.
Definition std_types.h:831
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
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:579
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:695
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:563
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:720
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:571
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:700
#define ENTERED_LOOP
Definition utils.h:24