CBMC
Loading...
Searching...
No Matches
dfcc_instrument_loop.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for loop contracts
4
5Author: Qinheping Hu, qinhh@amazon.com
6
7Author: Remi Delmas, delmasrd@amazon.com
8
9Date: April 2023
10
11\*******************************************************************/
12
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/expr_util.h>
19
21
22#include "dfcc_cfg_info.h"
24#include "dfcc_library.h"
25#include "dfcc_loop_tags.h"
26#include "dfcc_spec_functions.h"
27#include "dfcc_utils.h"
28
30 goto_modelt &goto_model,
31 message_handlert &message_handler,
32 dfcc_libraryt &library,
33 dfcc_spec_functionst &spec_functions,
34 dfcc_contract_clauses_codegent &contract_clauses_codegen)
35 : goto_model(goto_model),
36 log(message_handler),
37 library(library),
38 spec_functions(spec_functions),
39 contract_clauses_codegen(contract_clauses_codegen),
40 ns(goto_model.symbol_table)
41{
42}
43
45 const std::size_t loop_id,
46 const irep_idt &function_id,
47 goto_functiont &goto_function,
48 dfcc_cfg_infot &cfg_info,
49 const std::set<symbol_exprt> &local_statics,
50 std::set<irep_idt> &function_pointer_contracts)
51{
52 const dfcc_loop_infot &loop = cfg_info.get_loop_info(loop_id);
53 const std::size_t cbmc_loop_id = loop.cbmc_loop_id;
54 const exprt &outer_write_set = cfg_info.get_outer_write_set(loop_id);
55 goto_programt::targett head = loop.find_head(goto_function.body).value();
56 auto head_location(head->source_location());
57
58 auto &symbol_table = goto_model.symbol_table;
59
60 // Temporary variables:
61 // Create a temporary to track if we entered the loop,
62 // i.e., the loop guard was satisfied.
64 symbol_table,
65 bool_typet(),
66 function_id,
67 std::string(ENTERED_LOOP) + "__" + std::to_string(cbmc_loop_id),
69
70 // Create a snapshot of the invariant so that we can check the base case,
71 // if the loop is not vacuous and must be abstracted with contracts.
73 symbol_table, bool_typet(), function_id, INIT_INVARIANT, head_location);
74
75 // Create a temporary variable to track base case vs inductive case
76 // instrumentation of the loop.
78 symbol_table, bool_typet(), function_id, IN_BASE_CASE, head_location);
79
80 // Temporary variables for storing the multidimensional decreases clause
81 // at the start of and end of a loop body.
82 exprt::operandst decreases_clauses = loop.decreases;
83 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
84 for(const auto &clause : decreases_clauses)
85 {
86 // old
88 symbol_table, clause.type(), function_id, "tmp_cc", head_location);
90 // new
92 symbol_table, clause.type(), function_id, "tmp_cc", head_location);
94 }
95
96 // Convert the assigns clause to the required type.
97 exprt::operandst assigns(loop.assigns.begin(), loop.assigns.end());
98
99 // Add local statics to the assigns clause.
100 for(auto &local_static : local_statics)
101 {
102 assigns.push_back(local_static);
103 }
104
105 auto nof_targets = assigns.size();
107
108 // populate(w_loop, <loop_assigns>);
109 // Construct the write set from loop assigns target. That is, contract_assigns
110 // in the result __CPROVER_contracts_write_set_t should be the set of CAR
111 // of the loop assign targets.
113 const irep_idt &language_mode =
114 dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
116 language_mode, assigns, write_set_populate_instrs);
117
118 // havoc(w_loop);
119 // The generated GOTO instructions havoc the write set of the loop.
121
123 function_id,
131 language_mode,
134
135 // ---------- Add instrumented instructions ----------
137 loop.find_latch(goto_function.body).value();
138 exprt invariant(loop.invariant);
140 loop_id,
141 goto_function,
142 symbol_table,
143 head,
146 invariant,
147 assigns,
148 loop.write_set_var,
153 language_mode);
154
156 loop_id,
157 cbmc_loop_id,
158 function_id,
159 goto_function,
160 symbol_table,
161 head,
164 invariant,
165 decreases_clauses,
171
173 loop_id,
174 cbmc_loop_id,
175 goto_function,
176 symbol_table,
177 head,
179 invariant,
180 decreases_clauses,
186 language_mode);
187
189 loop_id,
190 cbmc_loop_id,
191 goto_function,
192 head,
193 loop.write_set_var,
201
202 goto_function.body.update();
203}
204
205std::unordered_map<exprt, symbol_exprt, irep_hash>
207 const std::size_t loop_id,
208 goto_functionst::goto_functiont &goto_function,
209 symbol_table_baset &symbol_table,
213 exprt &invariant,
214 const exprt::operandst &assigns,
220 const irep_idt &language_mode)
221{
222 auto loop_head_location(loop_head->source_location());
224
225 // ```
226 // ... preamble ...
227 //
228 // // Prehead block: Declare & initialize instrumentation variables
229 // snapshot loop_entry history vars;
230 // entered_loop = false
231 // initial_invariant = loop_invariant;
232 // in_base_case = true;
233 // __ws_loop;
234 // ws_loop := address_of(__ws_loop);
235 // __write_set_create(ws_loop);
236 // __write_set_add(ws_loop, loop_assigns);
237 // __write_set_add(ws_loop, local_statics);
238 // GOTO HEAD;
239 // ```
240
241 // initialize loop_entry history vars;
243 symbol_table, invariant, loop_head_location, language_mode);
244 invariant.swap(replace_history_result.expression_after_replacement);
246 replace_history_result.history_construction;
247
248 // entered_loop = false
249 {
254 }
255
256 // initial_invariant = <loop_invariant>;
257 {
258 // Create a snapshot of the invariant so that we can check the base case,
259 // if the loop is not vacuous and must be abstracted with contracts.
262
263 // Although the invariant at this point will not have side effects,
264 // it is still a C expression, and needs to be "goto_convert"ed.
265 // Note that this conversion may emit many GOTO instructions.
268 goto_convertt converter(symbol_table, log.get_message_handler());
269 converter.goto_convert(
271 }
272
273 {
274 // Create a temporary variable to track base case vs inductive case
275 // instrumentation of the loop.
276 // in_base_case = true;
281 }
282
283 {
284 // Create and populate the write set.
285 // DECL loop_write_set
286 // DECL addr_of_loop_write_set
287 // ASSIGN write_set_ptr := address_of(write_set)
288 // CALL __CPROVER_contracts_write_set_create(write_set_ptr,
289 // contracts_assigns_size, contracts_assigns_frees_size,
290 // assume_require_ctx, assert_require_ctx, assume_ensures_ctx,
291 // assert_ensures_ctx, allow_allocate, allow_deallocate);
300
303 from_integer(assigns.size(), size_type()),
307
308 pre_loop_head_instrs.destructive_append(assigns_instrs);
309 }
310
311 // goto HEAD;
314
315 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
316 return replace_history_result.parameter_to_history;
317}
318
321 const std::size_t loop_id,
322 const std::size_t cbmc_loop_id,
323 const irep_idt &function_id,
324 goto_functionst::goto_functiont &goto_function,
325 symbol_table_baset &symbol_table,
329 exprt &invariant,
330 const exprt::operandst &decreases_clauses,
332 const exprt &outer_write_set,
335 const std::vector<symbol_exprt> &old_decreases_vars)
336{
337 auto loop_head_location(loop_head->source_location());
339
340 // ```
341 // STEP: // Loop step block: havoc the loop state
342 // ASSERT(initial_invariant);
343 // __write_set_check_inclusion(ws_loop, ws_parent);
344 // in_base_case = false;
345 // in_loop_havoc_block = true;
346 // havoc(assigns_clause_targets);
347 // in_loop_havoc_block = false;
348 // ASSUME(loop_invariant);
349 // old_variant = loop_decreases;
350 // ```
351
353
354 // We skip past it initially, because of the unconditional jump above,
355 // but jump back here if we get past the loop guard while in_base_case.
356 // `in_base_case = false;`
360
361 {
362 // If we jump here, then the loop runs at least once,
363 // so add the base case assertion: `assert(initial_invariant)`.
365 check_location.set_property_class("loop_invariant_base");
366 check_location.set_comment(
367 "Check invariant before entry for loop " +
368 id2string(check_location.get_function()) + "." +
369 std::to_string(cbmc_loop_id));
370 step_instrs.add(
372 }
373
374 {
375 // Check assigns clause inclusion with parent write set
376 // skip the check when if w_parent is NULL.
377 auto goto_instruction = step_instrs.add(goto_programt::make_incomplete_goto(
382
384 symbol_table,
385 bool_typet(),
386 function_id,
387 "__check_assigns_clause_incl_loop_" + std::to_string(cbmc_loop_id),
389
395
397 check_location.set_property_class("loop_assigns");
398 check_location.set_comment(
399 "Check assigns clause inclusion for loop " +
400 id2string(check_location.get_function()) + "." +
401 std::to_string(cbmc_loop_id));
404
405 auto label_instruction =
407 goto_instruction->complete_goto(label_instruction);
408 }
409
410 {
411 // Generate havocing code for assigns targets.
413 symbol_table,
414 bool_typet(),
415 function_id,
416 std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(cbmc_loop_id),
418 step_instrs.add(
422 step_instrs.destructive_append(havoc_instrs);
425 }
426
427 goto_convertt converter(symbol_table, log.get_message_handler());
428 const irep_idt &language_mode =
429 dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
430 {
431 // Assume the loop invariant after havocing the state; produce one
432 // assumption per conjunct to ease analysis of counterexamples, and possibly
433 // also improve solver performance (observed with Bitwuzla)
434 if(invariant.id() == ID_and)
435 {
436 for(const auto &op : invariant.operands())
437 {
438 code_assumet assumption{op};
440 converter.goto_convert(assumption, step_instrs, language_mode);
441 }
442 }
443 else
444 {
445 code_assumet assumption{invariant};
447 converter.goto_convert(assumption, step_instrs, language_mode);
448 }
449 }
450
451 {
452 // Generate assignments to store the multidimensional decreases clause's
453 // value just before the loop_head.
454 for(size_t i = 0; i < old_decreases_vars.size(); i++)
455 {
457 old_decreases_vars[i], decreases_clauses[i], loop_head_location};
458 converter.goto_convert(
459 old_decreases_assignment, step_instrs, language_mode);
460 }
461 }
462
463 goto_function.body.destructive_insert(loop_head, step_instrs);
464
465 return step_case_target;
466}
467
469 const std::size_t loop_id,
470 const std::size_t cbmc_loop_id,
471 goto_functionst::goto_functiont &goto_function,
472 symbol_table_baset &symbol_table,
475 exprt &invariant,
476 const exprt::operandst &decreases_clauses,
479 const std::vector<symbol_exprt> &old_decreases_vars,
480 const std::vector<symbol_exprt> &new_decreases_vars,
482 const irep_idt &language_mode)
483{
484 auto loop_head_location(loop_head->source_location());
486
487 // HEAD: // Loop body block
488 // ... eval guard ...
489 // IF (!guard) GOTO EXIT;
490 // ... loop body ...
491 // // instrumentation
492 // entered_loop = true
493 // // Jump back to the step case if the loop can run at least once
494 // IF (in_base_case) GOTO STEP;
495 // ASSERT(<loop_invariant>);
496 // new_variant = <loop_decreases>;
497 // ASSERT(new_variant < old_variant);
498 // ASSUME(false);
499
501
502 {
503 // Record that we entered the loop with `entered_loop = true`.
506 }
507
508 {
509 // Jump back to the step case to havoc the write set, assume the invariant,
510 // and execute an arbitrary iteration.
513 }
514
515 goto_convertt converter(symbol_table, log.get_message_handler());
516 {
517 // Because of the unconditional jump above the following code is only
518 // reachable in the step case. Generate the inductive invariant check
519 // `ASSERT(invariant)`.
521 check_location.set_property_class("loop_invariant_step");
522 check_location.set_comment(
523 "Check invariant after step for loop " +
524 id2string(check_location.get_function()) + "." +
525 std::to_string(cbmc_loop_id));
526 // Assert the loop invariant after havocing the state; produce one assertion
527 // per conjunct to ease analysis of counterexamples, and possibly also
528 // improve solver performance (observed with Bitwuzla)
529 if(invariant.id() == ID_and)
530 {
531 for(const auto &op : invariant.operands())
532 {
533 code_assertt assertion{op};
535 converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
536 }
537 }
538 else
539 {
540 code_assertt assertion{invariant};
542 converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
543 }
544 }
545
546 {
547 // Generate assignments to store the multidimensional decreases clause's
548 // value after one iteration of the loop.
549 if(!decreases_clauses.empty())
550 {
551 for(size_t i = 0; i < new_decreases_vars.size(); i++)
552 {
554 new_decreases_vars[i], decreases_clauses[i], loop_head_location};
555 converter.goto_convert(
557 }
558
559 // Generate assertion that the multidimensional decreases clause's value
560 // after the loop is lexicographically smaller than its initial value.
562 check_location.set_property_class("loop_decreases");
563 check_location.set_comment(
564 "Check variant decreases after step for loop " +
565 id2string(check_location.get_function()) + "." +
566 std::to_string(cbmc_loop_id));
571
572 // Discard the temporary variables that store decreases clause's value.
573 for(size_t i = 0; i < old_decreases_vars.size(); i++)
574 {
579 }
580 }
581 }
582
584 goto_function.body, loop_latch, pre_loop_latch_instrs);
585
586 {
587 // Change the back edge into assume(false) or assume(!guard).
588 loop_latch->turn_into_assume();
589 loop_latch->condition_nonconst() = boolean_negate(loop_latch->condition());
590 }
591}
592
594 const std::size_t loop_id,
595 const std::size_t cbmc_loop_id,
596 goto_functionst::goto_functiont &goto_function,
600 const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
604 const std::vector<symbol_exprt> &old_decreases_vars,
605 const std::vector<symbol_exprt> &new_decreases_vars)
606{
607 // Collect all exit targets of the loop.
608 std::set<goto_programt::targett, goto_programt::target_less_than>
610
612 goto_function.body.instructions.begin();
613 target != goto_function.body.instructions.end();
614 target++)
615 {
616 if(!dfcc_is_loop_exiting(target) || !dfcc_has_loop_id(target, loop_id))
617 continue;
618 INVARIANT(target->is_goto(), "Exiting instructions must be GOTOs");
619 auto exit_target = target->get_target();
621 INVARIANT(
622 exit_loop_id_opt.has_value() && exit_loop_id_opt.value() != loop_id,
623 "Exiting instructions must jump out of the loop");
625 }
626
627 // For each exit target of the loop, insert a code block:
628 // ```
629 // EXIT:
630 // // check that step case was checked if loop can run once
631 // ASSUME (entered_loop ==> !in_base_case);
632 // DEAD loop_entry history vars, in_base_case;
633 // DEAD initial_invariant, entered_loop;
634 // DEAD old_variant, in_loop_havoc_block;
635 // __write_set_release(w_loop);
636 // DEAD __ws_loop, ws_loop;
637 // ```
638
639 for(auto exit_target : exit_targets)
640 {
642
643 // Use the head location for this check as well so that all checks related
644 // to a given loop are presented as coming from the loop head.
645 source_locationt check_location = loop_head->source_location();
646 check_location.set_property_class("loop_step_unwinding");
647 check_location.set_comment(
648 "Check step was unwound for loop " +
649 id2string(check_location.get_function()) + "." +
650 std::to_string(cbmc_loop_id));
654
655 // Mark instrumentation variables as going out of scope.
656 const source_locationt &exit_location = exit_target->source_location();
663
664 // Release the write set resources.
668
669 // Mark write set as going out of scope.
674
675 // Mark history variables as going out of scope.
676 for(const auto &v : history_var_map)
678
679 // Mark decreases clause snapshots as gong out of scope.
680 for(size_t i = 0; i < old_decreases_vars.size(); i++)
681 {
686 }
687
688 // Insert the exit block, preserving the loop end target.
690 goto_function.body, exit_target, loop_exit_program);
691 }
692}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_codet representation of a function call statement.
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
const exprt & get_outer_write_set(std::size_t loop_id) const
Returns the write set of the outer loop of that loop or the top level write set if that loop has no o...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void add_exit_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const std::unordered_map< exprt, symbol_exprt, irep_hash > &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars)
Adds instructions of the exit block.
dfcc_spec_functionst & spec_functions
dfcc_instrument_loopt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
Constructor for the loop contract instrumentation class.
void add_body_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars, const goto_programt::instructiont::targett &step_case_target, const irep_idt &symbol_mode)
Adds instructions of the body block.
std::unordered_map< exprt, symbol_exprt, irep_hash > add_prehead_instructions(const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, exprt &invariant, const exprt::operandst &assigns, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const irep_idt &symbol_mode)
Adds instructions of prehead block, and return history variables.
void operator()(const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Replaces a loop by a base + step abstraction generated from its contract.
goto_programt::instructiont::targett add_step_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars)
Adds instructions of the step block, and returns the STEP jump target so that it can be used to jump ...
dfcc_contract_clauses_codegent & contract_clauses_codegen
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
Describes a single loop for the purpose of DFCC loop contract instrumentation.
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
const exprt::operandst decreases
Decreases clause expression.
const std::set< exprt > assigns
Set of targets assigned by the loop, either user-provided or inferred.
const std::size_t cbmc_loop_id
Loop identifier assigned to this loop by traditional CBMC loop numbering.
std::optional< goto_programt::targett > find_latch(goto_programt &goto_program) const
const exprt invariant
Loop invariant expression.
std::optional< goto_programt::targett > find_head(goto_programt &goto_program) const
Finds the first instruction tagged as loop head and having the same loop identifier as this struct in...
const symbol_exprt write_set_var
Symbol representing the stack-allocated write set object for this loop.
This class rewrites GOTO functions that use the built-ins:
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3200
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
message_handlert & get_message_handler()
Definition message.h:183
Boolean negation.
Definition std_expr.h:2459
The null pointer constant.
Boolean OR.
Definition std_expr.h:2275
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
The Boolean constant true.
Definition std_expr.h:3191
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
This class applies the loop contract transformation to a loop in a goto function.
Dynamic frame condition checking library loading.
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
void dfcc_remove_loop_tags(source_locationt &source_location)
std::optional< std::size_t > dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_exiting(const goto_programt::instructiont::const_targett &target)
Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head,...
Translate functions that specify assignable and freeable targets declaratively into active functions ...
@ NONDET
havocs the pointer to an nondet pointer
Dynamic frame condition checking utility functions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition expr_util.cpp:98
Deprecated expression utility functions.
Program Transformation.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
double log(double x)
Definition math.c:2449
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
#define size_type
Definition unistd.c:186
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
Definition utils.cpp:475
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition utils.cpp:237
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition utils.cpp:193
#define ENTERED_LOOP
Definition utils.h:24
#define INIT_INVARIANT
Definition utils.h:26
#define IN_BASE_CASE
Definition utils.h:23
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:25