CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp Source File

CBMC
Loading...
Searching...
No Matches
dfcc_cfg_info.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function and loop contracts.
4
5Author: Qinheping Hu, qinhh@amazon.com
6Author: Remi Delmas delmasrd@amazon.com
7
8Date: March 2023
9
10\*******************************************************************/
11
12#include "dfcc_cfg_info.h"
13
14#include <util/c_types.h>
15#include <util/format_expr.h>
16#include <util/fresh_symbol.h>
17#include <util/pointer_expr.h>
18
19#include <analyses/local_may_alias.h>
20#include <analyses/natural_loops.h>
21#include <goto-instrument/contracts/utils.h>
22
23#include "dfcc_check_loop_normal_form.h"
24#include "dfcc_infer_loop_assigns.h"
25#include "dfcc_is_cprover_symbol.h"
26#include "dfcc_library.h"
27#include "dfcc_loop_nesting_graph.h"
28#include "dfcc_loop_tags.h"
29#include "dfcc_root_object.h"
30#include "dfcc_utils.h"
31
34 static bool has_contract(
36 const bool check_side_effect)
37{
39 get_loop_invariants(latch_target, check_side_effect).is_not_nil() ||
40 get_loop_decreases(latch_target, check_side_effect).is_not_nil();
41}
42
43 void dfcc_loop_infot::output(std::ostream &out) const
44{
45 out << "dfcc_loop_id: " << loop_id << "\n";
46 out << "cbmc_loop_id: " << cbmc_loop_id << "\n";
47 out << "local: {";
48 for(auto &id : local)
49 {
50 out << id << ", ";
51 }
52 out << "}\n";
53
54 out << "tracked: {";
55 for(auto &id : tracked)
56 {
57 out << id << ", ";
58 }
59 out << "}\n";
60
61 out << "write_set: " << format(write_set_var) << "\n";
62
63 out << "addr_of_write_set: " << format(addr_of_write_set_var) << "\n";
64
65 out << "assigns: {";
66 for(auto &expr : assigns)
67 {
68 out << format(expr) << ", ";
69 }
70 out << "}\n";
71
72 out << "invariant: " << format(invariant) << "\n";
73
74 out << "decreases: {";
75 for(auto &expr : decreases)
76 {
77 out << format(expr) << ", ";
78 }
79 out << "}\n";
80
81 out << "inner loops: {"
82 << "\n";
83 for(auto &id : inner_loops)
84 {
85 out << id << ", ";
86 }
87 out << "}\n";
88
89 out << "outer loops: {"
90 << "\n";
91 for(auto &id : outer_loops)
92 {
93 out << id << ", ";
94 }
95 out << "}\n";
96}
97
98std::optional<goto_programt::targett>
100{
101 for(auto target = goto_program.instructions.begin();
102 target != goto_program.instructions.end();
103 target++)
104 {
105 if(dfcc_is_loop_head(target) && dfcc_has_loop_id(target, loop_id))
106 {
107 return target;
108 }
109 }
110 return {};
111}
112
113std::optional<goto_programt::targett>
115{
116 std::optional<goto_programt::targett> result = std::nullopt;
117 for(auto target = goto_program.instructions.begin();
118 target != goto_program.instructions.end();
119 target++)
120 {
121 // go until the end because we want to find the very last occurrence
122 if(dfcc_is_loop_latch(target) && dfcc_has_loop_id(target, loop_id))
123 {
124 result = target;
125 }
126 }
127 return result;
128}
129
130 static std::optional<goto_programt::targett> check_has_contract_rec(
132 const std::size_t loop_idx,
133 const bool must_have_contract,
134 const bool check_side_effect)
135{
136 const auto &node = loop_nesting_graph[loop_idx];
137 if(must_have_contract && !has_contract(node.latch, check_side_effect))
138 return node.head;
139
140 for(const auto pred_idx : loop_nesting_graph.get_predecessors(loop_idx))
141 {
142 auto result = check_has_contract_rec(
144 pred_idx,
145 has_contract(node.latch, check_side_effect),
146 check_side_effect);
147 if(result.has_value())
148 return result;
149 }
150 return {};
151}
152
156 static std::optional<goto_programt::targett> check_inner_loops_have_contracts(
158 const bool check_side_effect)
159{
160 for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++)
161 {
162 if(loop_nesting_graph.get_successors(idx).empty())
163 {
164 auto result = check_has_contract_rec(
165 loop_nesting_graph, idx, false, check_side_effect);
166 if(result.has_value())
167 return result;
168 }
169 }
170 return {};
171}
172
177 goto_programt &goto_program,
179{
180 for(const auto &idx : loop_nesting_graph.topsort())
181 {
182 auto &node = loop_nesting_graph[idx];
183 auto &head = node.head;
184 auto &latch = node.latch;
185 auto &instruction_iterators = node.instructions;
186
187 dfcc_set_loop_head(head);
188 dfcc_set_loop_latch(latch);
189
191 {
192 // Skip instructions that are already tagged and belong to inner loops.
194 if(loop_id_opt.has_value())
195 continue;
196
197 dfcc_set_loop_id(t, idx);
198
199 if(t != head && t != latch)
201
202 if(t->is_goto() && !instruction_iterators.contains(t->get_target()))
203 {
205 }
206 }
207 }
208
209 auto top_level_id = loop_nesting_graph.size();
210
211 // tag remaining instructions as top level
212 for(auto target = goto_program.instructions.begin();
213 target != goto_program.instructions.end();
214 target++)
215 {
216 // Skip instructions that are already tagged (belong to loops).
217 auto loop_id_opt = dfcc_get_loop_id(target);
218 if(loop_id_opt.has_value())
219 {
220 continue;
221 }
222 dfcc_set_loop_id(target, top_level_id);
224 }
225}
226
227 static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
228{
229 PRECONDITION(!dirty(ident));
230 // For each assigns clause target
231 for(const auto &expr : assigns)
232 {
233 auto root_objects = dfcc_root_objects(expr);
234 for(const auto &root_object : root_objects)
235 {
236 if(
237 root_object.id() == ID_symbol &&
238 expr_try_dynamic_cast<symbol_exprt>(root_object)->identifier() == ident)
239 {
240 return true;
241 }
242 // If `root_object` is not a symbol, then it contains a combination of
243 // address-of and dereference operators that cannot be statically
244 // resolved to a symbol.
245 // Since we know `ident` is not dirty, we know that dereference
246 // operations cannot land on that `ident`. So the root_object cannot
247 // describe a memory location within the object backing that ident.
248 // We conclude that ident is not assigned by this target and move on to
249 // the next target.
250 }
251 }
252 return false;
253}
254
268 static std::unordered_set<irep_idt> gen_tracked_set(
269 const std::vector<std::size_t> &inner_loops_ids,
270 const std::unordered_set<irep_idt> &locals,
271 dirtyt &dirty,
272 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
273{
274 std::unordered_set<irep_idt> tracked;
275 for(const auto &ident : locals)
276 {
277 if(dirty(ident))
278 {
279 tracked.insert(ident);
280 }
281 else
282 {
283 // Check if this ident is touched by one of the inner loops
284 for(const auto inner_loop_id : inner_loops_ids)
285 {
286 if(is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
287 tracked.insert(ident);
288 }
289 }
290 }
291 return tracked;
292}
293
304
309 const std::size_t loop_id,
310 const irep_idt &function_id,
312 const bool check_side_effect,
313 message_handlert &message_handler,
314 const namespacet &ns)
315{
316 messaget log(message_handler);
317 const auto &loop = loop_nesting_graph[loop_id];
318
319 // Process loop contract clauses
321 get_loop_invariants(loop.latch, check_side_effect).operands();
323
324 // Initialise defaults
325 struct contract_clausest result(
326 get_loop_decreases(loop.latch, check_side_effect).operands());
327
328 // Generate defaults for all clauses if at least one type of clause is defined
329 if(
330 !invariant_clauses.empty() || !result.decreases_clauses.empty() ||
331 !assigns_clauses.empty())
332 {
333 if(invariant_clauses.empty())
334 {
335 // use a default invariant if none given.
336 result.invariant_expr = true_exprt{};
337 // assigns clause is missing; we will try to automatic inference
338 log.warning() << "No invariant provided for loop " << function_id << "."
339 << loop.latch->loop_number << " at "
340 << loop.head->source_location()
341 << ". Using 'true' as a sound default invariant. Please "
342 "provide an invariant the default is too weak."
343 << messaget::eom;
344 }
345 else
346 {
347 // conjoin all invariant clauses
349 }
350
351 // unpack assigns clause targets
352 if(!assigns_clauses.empty())
353 {
354 for(auto &operand : assigns_clauses)
355 {
356 result.assigns.insert(operand);
357 }
358 }
359 else
360 {
361 // infer assigns clause targets if none given
362 log.debug() << "No assigns clause provided for loop " << function_id
363 << "." << loop.latch->loop_number << " at "
364 << loop.head->source_location() << ". The inferred set {";
365 bool first = true;
366 for(const auto &expr : inferred_assigns)
367 {
368 if(!first)
369 {
370 log.debug() << ", ";
371 }
372 first = false;
373 log.debug() << format(expr);
374 }
375 log.debug() << "} might be incomplete or imprecise, please provide an "
376 "assigns clause if the analysis fails."
377 << messaget::eom;
378 result.assigns = inferred_assigns;
379 }
380
381 if(result.decreases_clauses.empty())
382 {
383 log.debug() << "No decrease clause provided for loop " << function_id
384 << "." << loop.latch->loop_number << " at "
385 << loop.head->source_location()
386 << ". Termination will not be checked." << messaget::eom;
387 }
388 }
389 return result;
390}
391
394 const std::size_t loop_id,
395 const irep_idt &function_id,
396 goto_functiont &goto_function,
397 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
398 dirtyt &dirty,
400 const bool check_side_effect,
401 message_handlert &message_handler,
402 dfcc_libraryt &library,
403 symbol_table_baset &symbol_table)
404{
405 const namespacet ns(symbol_table);
406 std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
407 function_id,
408 goto_function,
409 loop_nesting_graph[loop_id],
410 message_handler,
411 ns);
412
413 // Exclude locals of inner nested loops.
414 for(const auto &inner_loop : loop_nesting_graph.get_predecessors(loop_id))
415 {
416 INVARIANT(
417 loop_info_map.find(inner_loop) != loop_info_map.end(),
418 "DFCC should gen_dfcc_loop_info for inner loops first.");
419 for(const auto &inner_local : loop_info_map.at(inner_loop).local)
420 {
422 }
423 }
424
425 std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
426 loop_nesting_graph.get_predecessors(loop_id),
428 dirty,
429 loop_info_map);
430
433 loop_id,
434 function_id,
436 check_side_effect,
437 message_handler,
438 ns);
439
440 std::set<std::size_t> inner_loops;
441 for(auto pred_idx : loop_nesting_graph.get_predecessors(loop_id))
442 {
443 inner_loops.insert(pred_idx);
444 }
445
446 std::set<std::size_t> outer_loops;
447 for(auto succ_idx : loop_nesting_graph.get_successors(loop_id))
448 {
449 outer_loops.insert(succ_idx);
450 }
451
452 auto &loop = loop_nesting_graph[loop_id];
453 const auto cbmc_loop_number = loop.latch->loop_number;
454
455 // Generate "write set" variable
456 const auto write_set_var = dfcc_utilst::create_symbol(
457 symbol_table,
459 function_id,
460 "__write_set_loop_" + std::to_string(cbmc_loop_number),
461 loop.head->source_location());
462
463 // Generate "address of write set" variable
464 const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
465 symbol_table,
467 function_id,
468 "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
469 loop.head->source_location());
470
471 return {
472 loop_id,
474 contract_clauses.assigns,
475 contract_clauses.invariant_expr,
476 contract_clauses.decreases_clauses,
479 inner_loops,
480 outer_loops,
481 write_set_var,
482 addr_of_write_set_var};
483}
484
486 goto_modelt &goto_model,
487 const irep_idt &function_id,
488 goto_functiont &goto_function,
489 const exprt &top_level_write_set,
490 const loop_contract_configt &loop_contract_config,
491 symbol_table_baset &symbol_table,
492 message_handlert &message_handler,
493 dfcc_libraryt &library)
494 : function_id(function_id),
495 goto_function(goto_function),
496 top_level_write_set(top_level_write_set),
497 ns(symbol_table)
498{
500 goto_programt &goto_program = goto_function.body;
501
502 // Clean up possible fake loops that are due to do { ... } while(0);
503 simplify_gotos(goto_program, ns);
504
505 // From loop number to the inferred loop assigns.
506 std::map<std::size_t, assignst> inferred_loop_assigns_map;
507
508 if(loop_contract_config.apply_loop_contracts)
509 {
510 messaget log(message_handler);
511 dfcc_check_loop_normal_form(goto_program, log);
513
514 const auto head = check_inner_loops_have_contracts(
515 loop_nesting_graph, loop_contract_config.check_side_effect);
516 if(head.has_value())
517 {
519 "Found loop without contract nested in a loop with a "
520 "contract.\nPlease "
521 "provide a contract or unwind this loop before applying loop "
522 "contracts.",
523 head.value()->source_location());
524 }
525
526 auto topsorted = loop_nesting_graph.topsort();
527
528 bool has_loops_with_contracts = false;
529 for(const auto idx : topsorted)
530 {
531 topsorted_loops.push_back(idx);
533 loop_nesting_graph[idx].latch, loop_contract_config.check_side_effect);
534 }
535
536 // We infer loop assigns for all loops in the function.
538 {
541 goto_model.goto_functions,
543 message_handler,
544 ns);
545 }
546 }
547
548 // At this point, either loop contracts were activated and the loop nesting
549 // graph describes the loop structure of the function,
550 // or loop contracts were not activated and the loop nesting graph is empty
551 // (i.e. there might be some loops in the function but we won't consider them
552 // for the instrumentation).
553 // In both cases, we tag program instructions and generate the dfcc_cfg_infot
554 // instance from that graph's contents. The tags will decide against which
555 // write set the instructions are going to be instrumented (either the
556 // function's write set, or the write set of a loop), and each dfcc_loop_infot
557 // contained in the loop_info_map describes a loop to be abstracted by a
558 // contract.
559
561
562 // generate dfcc_cfg_loop_info for loops and add to loop_info_map
563 dirtyt dirty(goto_function);
564
565 for(const auto &loop_id : topsorted_loops)
566 {
568 inferred_loop_assigns_map[loop_nesting_graph[loop_id].latch->loop_number];
569 loop_info_map.insert(
570 {loop_id,
573 loop_id,
577 dirty,
579 loop_contract_config.check_side_effect,
580 message_handler,
581 library,
582 symbol_table)});
583
584 if(loop_nesting_graph.get_successors(loop_id).empty())
585 top_level_loops.push_back(loop_id);
586 }
587
588 // generate set of top level of locals
589 top_level_local.insert(
592
593 for(auto target = goto_function.body.instructions.begin();
594 target != goto_function.body.instructions.end();
595 target++)
596 {
597 if(target->is_decl() && dfcc_is_loop_top_level(target))
598 top_level_local.insert(target->decl_symbol().identifier());
599 }
600
603}
604
605 void dfcc_cfg_infot::output(std::ostream &out) const
606{
607 out << "// dfcc_cfg_infot for: " << function_id << "\n";
608 out << "// top_level_local: {";
609 for(auto &id : top_level_local)
610 {
611 out << id << ", ";
612 }
613 out << "}\n";
614
615 out << "// top_level_tracked: {";
616 for(auto &id : top_level_tracked)
617 {
618 out << id << ", ";
619 }
620 out << "}\n";
621
622 out << "// loop:\n";
623 for(auto &loop : loop_info_map)
624 {
625 out << "// dfcc-loop_id:" << loop.first << "\n";
626 auto head = loop.second.find_head(goto_function.body);
627 auto latch = loop.second.find_latch(goto_function.body);
628 out << "// head:\n";
629 head.value()->output(out);
630 out << "// latch:\n";
631 latch.value()->output(out);
632 loop.second.output(out);
633 }
634 out << "// program:\n";
636 {
637 out << "// dfcc-loop-id:" << dfcc_get_loop_id(target).value();
638 out << " cbmc-loop-number:" << target->loop_number;
639 out << " top-level:" << dfcc_is_loop_top_level(target);
640 out << " head:" << dfcc_is_loop_head(target);
641 out << " body:" << dfcc_is_loop_body(target);
642 out << " exiting:" << dfcc_is_loop_exiting(target);
643 out << " latch:" << dfcc_is_loop_latch(target);
644 out << "\n";
645 target->output(out);
646 }
647}
648
650 const std::size_t loop_id) const
651{
652 if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip())
653 {
654 return loop_id;
655 }
658}
659
660const exprt &
662{
663 auto loop_id_opt = dfcc_get_loop_id(target);
665 loop_id_opt.has_value() &&
668 if(is_top_level_id(loop_id))
669 {
670 return top_level_write_set;
671 }
672 else
673 {
674 return loop_info_map.at(loop_id).addr_of_write_set_var;
675 }
676}
677
678const std::unordered_set<irep_idt> &
680{
681 auto loop_id_opt = dfcc_get_loop_id(target);
683 loop_id_opt.has_value() &&
685 auto loop_id = loop_id_opt.value();
686 if(is_top_level_id(loop_id))
687 {
688 return top_level_tracked;
689 }
690 else
691 {
692 return loop_info_map.at(loop_id).tracked;
693 }
694}
695
696const std::unordered_set<irep_idt> &
698{
699 auto loop_id_opt = dfcc_get_loop_id(target);
701 loop_id_opt.has_value() &&
703 auto loop_id = loop_id_opt.value();
704 if(is_top_level_id(loop_id))
705 {
706 return top_level_local;
707 }
708 else
709 {
710 return loop_info_map.at(loop_id).local;
711 }
712}
713
714 const exprt &dfcc_cfg_infot::get_outer_write_set(std::size_t loop_id) const
715{
718 return outer_loop_opt.has_value()
719 ? get_loop_info(outer_loop_opt.value()).addr_of_write_set_var
721}
722
723const dfcc_loop_infot &
724 dfcc_cfg_infot::get_loop_info(const std::size_t loop_id) const
725{
726 return loop_info_map.at(loop_id);
727}
728
729// find the identifier or the immediately enclosing loop in topological order
730const std::optional<std::size_t>
731 dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const
732{
734 auto outer_loops = get_loop_info(loop_id).outer_loops;
735
736 // find the first loop in the topological order that is connected
737 // to our node.
738 for(const auto &idx : get_loops_toposorted())
739 {
740 if(
741 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
742 outer_loops.end())
743 {
744 return idx;
745 }
746 }
747 // return nullopt for loops that are not nested in other loops
748 return std::nullopt;
749}
750
751 bool dfcc_cfg_infot::is_valid_loop_or_top_level_id(const std::size_t id) const
752{
753 return id <= loop_info_map.size();
754}
755
756 bool dfcc_cfg_infot::is_valid_loop_id(const std::size_t id) const
757{
758 return id < loop_info_map.size();
759}
760
761 bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
762{
763 return id == loop_info_map.size();
764}
765
767{
768 return loop_info_map.size();
769}
770
772 goto_programt::const_targett target) const
773{
774 PRECONDITION(target->is_decl() || target->is_dead());
775 auto &ident = target->is_decl() ? target->decl_symbol().identifier()
776 : target->dead_symbol().identifier();
777 auto &tracked = get_tracked_set(target);
778 return tracked.find(ident) != tracked.end();
779}
780
786 const exprt &lhs,
787 const std::unordered_set<irep_idt> &local,
788 const std::unordered_set<irep_idt> &tracked)
789{
791
792 // Check wether all root_objects can be resolved to actual identifiers.
793 std::unordered_set<irep_idt> root_idents;
794 for(const auto &expr : root_objects)
795 {
796 if(expr.id() != ID_symbol)
797 {
798 // This means that lhs contains either an address-of operation or a
799 // dereference operation, and we cannot really know statically which
800 // object it refers to without using the may_alias analysis.
801 // Since the may_alias analysis is also used to infer targets, for
802 // soundness reasons we cannot also use it to skip checks, so we check
803 // the assignment. If happens to assign to a mix of tracked and
804 // non-tracked identifiers the check will fail but this is sound anyway.
805 return true;
806 }
807 const auto &id = to_symbol_expr(expr).identifier();
809 {
810 // Skip the check if we have a single cprover symbol as root object
811 // cprover symbols are used for generic checks instrumentation and are
812 // de-facto ghost code. We implicitly allow assignments to these symbols.
813 // To make this really sound we should use a white list of known
814 // CPROVER symbols, because right now simply naming a symbol with the
815 // CPROVER prefix bypasses the checks.
816 if(root_objects.size() == 1)
817 {
818 return false;
819 }
820 else
821 {
822 // error out if we have a cprover symbol and something else in the set
824 "LHS expression `" + format_to_string(lhs) +
825 "` in assignment refers to a cprover symbol and something else.");
826 }
827 }
828 root_idents.insert(id);
829 }
830
831 // The root idents set is Non-empty.
832 // true iff root_idents contains non-local idents
833 bool some_non_local = false;
834 // true iff root_idents contains some local that is not tracked
835 bool some_local_not_tracked = false;
836 // true iff root_idents contains only local that are not tracked
837 bool all_local_not_tracked = true;
838 // true iff root_idents contains only local that are tracked
839 bool all_local_tracked = true;
840 for(const auto &root_ident : root_idents)
841 {
842 bool loc = local.find(root_ident) != local.end();
843 bool tra = tracked.find(root_ident) != tracked.end();
844 bool local_tracked = loc && tra;
845 bool local_not_tracked = loc && !tra;
846 some_non_local |= !loc;
850 }
851
852 // some root identifier is not local, the lhs must be checked
854 {
855 // if we also have a local that is not tracked, we know the check will
856 // fail with the current algorithm, error out.
858 {
860 "LHS expression `" + format_to_string(lhs) +
861 "` in assignment mentions both explicitly and implicitly tracked "
862 "memory locations. DFCC does not yet handle that case, please "
863 "reformulate the assignment into separate assignments to either "
864 "memory locations.");
865 }
866 return true;
867 }
868 else
869 {
870 // all root identifiers are local
871 // if they are all not tracked, we *have* to skip the check
872 // (and it is sound to do so, because we know that the identifiers that
873 // are not tracked explicitly are not dirty and not assigned to outside of
874 // their scope).
875 // if they are all tracked, we *can* skip the check, because they are all
876 // local to that scope anyway and implicitly allowed.
878 {
879 return false;
880 }
881 else
882 {
883 // we have a combination of tracked and not-tracked locals, we know
884 // the check will fail with the current algorithm, error out.
886 "LHS expression `" + format_to_string(lhs) +
887 "` in assignment mentions both explicitly and implicitly tracked "
888 "memory locations. DFCC does not yet handle that case, please "
889 "reformulate the assignment into separate assignments to either "
890 "memory locations.");
891 }
892 }
893}
894
896{
897 PRECONDITION(target->is_assign() || target->is_function_call());
898 const exprt &lhs =
899 target->is_assign() ? target->assign_lhs() : target->call_lhs();
900 if(lhs.is_nil())
901 return false;
903 lhs, get_local_set(target), get_tracked_set(target));
904}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const std::optional< std::size_t > get_outer_loop_identifier(const std::size_t loop_id) const
Finds the DFCC id of the loop that contains the given loop, returns nullopt when the loop has no oute...
std::unordered_set< irep_idt > top_level_local
Set of identifiers DECL at top level.
const exprt & top_level_write_set
std::size_t get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const
Returns the id of the first outer loop (including this one) that is not skipped, or the top level id.
const namespacet ns
std::vector< std::size_t > topsorted_loops
Loop identifiers sorted from most deeply nested to less deeply nested.
std::unordered_set< irep_idt > top_level_tracked
Set of identifiers DECL at top level.
bool is_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
void output(std::ostream &out) const
const std::vector< std::size_t > & get_loops_toposorted() const
goto_functiont & goto_function
std::vector< std::size_t > top_level_loops
Loop identifiers for top level loops (ie for loops that are not nested in in another loop).
const std::unordered_set< irep_idt > & get_tracked_set(goto_programt::const_targett target) const
Returns the subset of local variable that are explicitly tracked in the write set for the scope where...
dfcc_cfg_infot(goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
const std::unordered_set< irep_idt > & get_local_set(goto_programt::const_targett target) const
Returns the set of local variable for the scope where that target instruction is found.
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...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
size_t top_level_id() const
Returns the top level ID.
bool is_valid_loop_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const irep_idt & function_id
std::map< std::size_t, dfcc_loop_infot > loop_info_map
Map from loop identifier to loop info struct.
bool is_valid_loop_or_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id or is equal to the top level id for this function.
Class interface to library types and functions defined in cprover_contracts.c.
Definition dfcc_library.h:163
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition dfcc_library.h:221
Describes a single loop for the purpose of DFCC loop contract instrumentation.
Definition dfcc_cfg_info.h:40
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
void output(std::ostream &out) const
Prints a textual representation of the struct to out.
const exprt::operandst decreases
Decreases clause expression.
const std::unordered_set< irep_idt > local
Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested ...
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 std::unordered_set< irep_idt > tracked
Subset of locals that must be tracked in the loop's write set.
const std::size_t loop_id
Loop identifier assigned by DFCC to this loop.
const exprt invariant
Loop invariant expression.
const std::set< std::size_t > outer_loops
Integer identifier of the outer loop(s) if they exists.
const std::set< std::size_t > inner_loops
Integer identifiers of inner loops of that loop.
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.
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition dirty.h:28
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
operandst & operands()
Definition expr.h:95
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition goto_function.h:24
goto_programt body
Definition goto_function.h:26
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition goto_function.h:33
Definition goto_model.h:27
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
instructionst::iterator targett
Definition goto_program.h:613
instructionst::const_iterator const_targett
Definition goto_program.h:614
Thrown when we can't handle something in an input source file.
bool is_not_nil() const
Definition irep.h:372
bool is_nil() const
Definition irep.h:368
Definition message.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3144
The symbol table base class interface.
The Boolean constant true.
Definition std_expr.h:3126
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
static bool has_contract(const goto_programt::const_targett &latch_target, const bool check_side_effect)
Returns true iff some contract clause expression is attached to the latch condition of this loop.
static void tag_loop_instructions(goto_programt &goto_program, dfcc_loop_nesting_grapht &loop_nesting_graph)
Tags instructions of loops found in loop_nesting_graph with the loop identifier of the innermost loop...
static std::optional< goto_programt::targett > check_inner_loops_have_contracts(const dfcc_loop_nesting_grapht &loop_nesting_graph, const bool check_side_effect)
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that ha...
static bool must_check_lhs_from_local_and_tracked(const exprt &lhs, const std::unordered_set< irep_idt > &local, const std::unordered_set< irep_idt > &tracked)
Returns true if the lhs to an assignment must be checked against its write set.
static struct contract_clausest default_loop_contract_clauses(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, const namespacet &ns)
Generate defaults for all contract clauses of the loop with ID loop_id if at least one type of clause...
static dfcc_loop_infot gen_dfcc_loop_info(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map, dirtyt &dirty, const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table)
static std::optional< goto_programt::targett > check_has_contract_rec(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_idx, const bool must_have_contract, const bool check_side_effect)
static std::unordered_set< irep_idt > gen_tracked_set(const std::vector< std::size_t > &inner_loops_ids, const std::unordered_set< irep_idt > &locals, dirtyt &dirty, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map)
Compute subset of locals that must be tracked in the loop's write set.
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
Checks and enforces normal form properties for natural loops of the given goto_program.
Checks normal form properties of natural loops in a GOTO program.
std::unordered_set< irep_idt > gen_loop_locals_set(const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop_node, message_handlert &message_handler, const namespacet &ns)
Collect identifiers that are local to this loop.
void dfcc_infer_loop_assigns_for_function(std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)
Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis...
Infer a set of assigns clause targets for a natural loop.
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
Returns true iff the symbol is one of the known CPROVER static instrumentation variables or ends with...
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Builds a graph describing how loops are nested in a GOTO program.
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target)
void dfcc_set_loop_latch(goto_programt::instructiont::targett &target)
bool dfcc_is_loop_head(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_latch(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_top_level(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
void dfcc_set_loop_id(goto_programt::instructiont::targett &target, const std::size_t loop_id)
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)
bool dfcc_is_loop_body(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_head(goto_programt::instructiont::targett &target)
Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head,...
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
Dynamic frame condition checking utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
std::string format_to_string(const T &o)
Definition format.h:43
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
std::set< exprt > assignst
Definition havoc_utils.h:24
bool has_contract(const irep_idt &function_identifier, const namespacet &ns)
Field-insensitive, location-sensitive may-alias analysis.
double log(double x)
Definition math.c:2416
Compute natural loops in a goto_function.
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:252
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
exprt::operandst decreases_clauses
contract_clausest(const exprt::operandst &decreases)
assignst assigns
exprt invariant_expr
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...
Definition dfcc_utils.cpp:81
Loop contract configurations.
bool apply_loop_contracts
bool check_side_effect
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition utils.cpp:683
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:260
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:666
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
Definition utils.cpp:688

AltStyle によって変換されたページ (->オリジナル) /