cprover
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
22
26#include "dfcc_library.h"
28#include "dfcc_loop_tags.h"
29#include "dfcc_root_object.h"
30#include "dfcc_utils.h"
31
33static const exprt::operandst &
35{
36 return static_cast<const exprt &>(
37 latch_target->condition().find(ID_C_spec_assigns))
38 .operands();
39}
40
42static const exprt::operandst &
44{
45 return static_cast<const exprt &>(
46 latch_target->condition().find(ID_C_spec_loop_invariant))
47 .operands();
48}
49
51static const exprt::operandst &
53{
54 return static_cast<const exprt &>(
55 latch_target->condition().find(ID_C_spec_decreases))
56 .operands();
57}
58
61static bool has_contract(const goto_programt::const_targett &latch_target)
62{
63 return !get_assigns(latch_target).empty() ||
64 !get_invariants(latch_target).empty() ||
65 !get_decreases(latch_target).empty();
66}
67
68void dfcc_loop_infot::output(std::ostream &out) const
69{
70 out << "dfcc_loop_id: " << loop_id << "\n";
71 out << "cbmc_loop_id: " << cbmc_loop_id << "\n";
72 out << "local: {";
73 for(auto &id : local)
74 {
75 out << id << ", ";
76 }
77 out << "}\n";
78
79 out << "tracked: {";
80 for(auto &id : tracked)
81 {
82 out << id << ", ";
83 }
84 out << "}\n";
85
86 out << "write_set: " << format(write_set_var) << "\n";
87
88 out << "addr_of_write_set: " << format(addr_of_write_set_var) << "\n";
89
90 out << "assigns: {";
91 for(auto &expr : assigns)
92 {
93 out << format(expr) << ", ";
94 }
95 out << "}\n";
96
97 out << "invariant: " << format(invariant) << "\n";
98
99 out << "decreases: {";
100 for(auto &expr : decreases)
101 {
102 out << format(expr) << ", ";
103 }
104 out << "}\n";
105
106 out << "inner loops: {"
107 << "\n";
108 for(auto &id : inner_loops)
109 {
110 out << id << ", ";
111 }
112 out << "}\n";
113
114 out << "outer loops: {"
115 << "\n";
116 for(auto &id : outer_loops)
117 {
118 out << id << ", ";
119 }
120 out << "}\n";
121}
122
125{
126 for(auto target = goto_program.instructions.begin();
127 target != goto_program.instructions.end();
128 target++)
129 {
130 if(dfcc_is_loop_head(target) && dfcc_has_loop_id(target, loop_id))
131 {
132 return target;
133 }
134 }
135 return {};
136}
137
140{
141 optionalt<goto_programt::targett> result = nullopt;
142 for(auto target = goto_program.instructions.begin();
143 target != goto_program.instructions.end();
144 target++)
145 {
146 // go until the end because we want to find the very last occurrence
147 if(dfcc_is_loop_latch(target) && dfcc_has_loop_id(target, loop_id))
148 {
149 result = target;
150 }
151 }
152 return result;
153}
154
156 const dfcc_loop_nesting_grapht &loop_nesting_graph,
157 const std::size_t loop_idx,
158 const bool must_have_contract)
159{
160 const auto &node = loop_nesting_graph[loop_idx];
161 if(must_have_contract && !has_contract(node.latch))
162 return node.head;
163
164 for(const auto pred_idx : loop_nesting_graph.get_predecessors(loop_idx))
165 {
166 auto result = check_has_contract_rec(
167 loop_nesting_graph, pred_idx, has_contract(node.latch));
168 if(result.has_value())
169 return result;
170 }
171 return {};
172}
173
178 const dfcc_loop_nesting_grapht &loop_nesting_graph)
179{
180 for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++)
181 {
182 if(loop_nesting_graph.get_successors(idx).empty())
183 {
184 auto result = check_has_contract_rec(loop_nesting_graph, idx, false);
185 if(result.has_value())
186 return result;
187 }
188 }
189 return {};
190}
191
196 goto_programt &goto_program,
197 dfcc_loop_nesting_grapht &loop_nesting_graph)
198{
199 for(const auto &idx : loop_nesting_graph.topsort())
200 {
201 auto &node = loop_nesting_graph[idx];
202 auto &head = node.head;
203 auto &latch = node.latch;
204 auto &instruction_iterators = node.instructions;
205
206 dfcc_set_loop_head(head);
207 dfcc_set_loop_latch(latch);
208
209 for(goto_programt::targett t : instruction_iterators)
210 {
211 // Skip instructions that are already tagged and belong to inner loops.
212 auto loop_id_opt = dfcc_get_loop_id(t);
213 if(loop_id_opt.has_value())
214 continue;
215
216 dfcc_set_loop_id(t, idx);
217
218 if(t != head && t != latch)
220
221 if(t->is_goto() && !instruction_iterators.contains(t->get_target()))
222 {
224 }
225 }
226 }
227
228 auto top_level_id = loop_nesting_graph.size();
229
230 // tag remaining instructions as top level
231 for(auto target = goto_program.instructions.begin();
232 target != goto_program.instructions.end();
233 target++)
234 {
235 // Skip instructions that are already tagged (belong to loops).
236 auto loop_id_opt = dfcc_get_loop_id(target);
237 if(loop_id_opt.has_value())
238 {
239 continue;
240 }
241 dfcc_set_loop_id(target, top_level_id);
243 }
244}
245
246static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
247{
248 PRECONDITION(!dirty(ident));
249 // For each assigns clause target
250 for(const auto &expr : assigns)
251 {
252 auto root_objects = dfcc_root_objects(expr);
253 for(const auto &root_object : root_objects)
254 {
255 if(
256 root_object.id() == ID_symbol &&
257 expr_try_dynamic_cast<symbol_exprt>(root_object)->get_identifier() ==
258 ident)
259 {
260 return true;
261 }
262 // If `root_object` is not a symbol, then it contains a combination of
263 // address-of and dereference operators that cannot be statically
264 // resolved to a symbol.
265 // Since we know `ident` is not dirty, we know that dereference
266 // operations cannot land on that `ident`. So the root_object cannot
267 // describe a memory location within the object backing that ident.
268 // We conclude that ident is not assigned by this target and move on to
269 // the next target.
270 }
271 }
272 return false;
273}
274
277static std::unordered_set<irep_idt> gen_loop_locals_set(
278 const dfcc_loop_nesting_grapht &loop_nesting_graph,
279 const std::size_t loop_id)
280{
281 std::unordered_set<irep_idt> loop_locals;
282 for(const auto &target : loop_nesting_graph[loop_id].instructions)
283 {
284 auto loop_id_opt = dfcc_get_loop_id(target);
285 if(
286 target->is_decl() && loop_id_opt.has_value() &&
287 loop_id_opt.value() == loop_id)
288 {
289 loop_locals.insert(target->decl_symbol().get_identifier());
290 }
291 }
292 return loop_locals;
293}
294
308static std::unordered_set<irep_idt> gen_tracked_set(
309 const std::vector<std::size_t> &inner_loops_ids,
310 const std::unordered_set<irep_idt> &locals,
311 dirtyt &dirty,
312 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
313{
314 std::unordered_set<irep_idt> tracked;
315 for(const auto &ident : locals)
316 {
317 if(dirty(ident))
318 {
319 tracked.insert(ident);
320 }
321 else
322 {
323 // Check if this ident is touched by one of the inner loops
324 for(const auto inner_loop_id : inner_loops_ids)
325 {
326 if(is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
327 tracked.insert(ident);
328 }
329 }
330 }
331 return tracked;
332}
333
344
348 const dfcc_loop_nesting_grapht &loop_nesting_graph,
349 const std::size_t loop_id,
350 const irep_idt &function_id,
351 local_may_aliast &local_may_alias,
352 message_handlert &message_handler,
353 const namespacet &ns)
354{
355 messaget log(message_handler);
356 const auto &loop = loop_nesting_graph[loop_id];
357
358 // Process loop contract clauses
359 exprt::operandst invariant_clauses = get_invariants(loop.latch);
360 exprt::operandst assigns_clauses = get_assigns(loop.latch);
361
362 // Initialise defaults
363 struct contract_clausest result(get_decreases(loop.latch));
364
365 // Generate defaults for all clauses if at least one type of clause is defined
366 if(
367 !invariant_clauses.empty() || !result.decreases_clauses.empty() ||
368 !assigns_clauses.empty())
369 {
370 if(invariant_clauses.empty())
371 {
372 // use a default invariant if none given.
373 result.invariant_expr = true_exprt{};
374 // assigns clause is missing; we will try to automatic inference
375 log.warning() << "No invariant provided for loop " << function_id << "."
376 << loop.latch->loop_number << " at "
377 << loop.head->source_location()
378 << ". Using 'true' as a sound default invariant. Please "
379 "provide an invariant the default is too weak."
380 << messaget::eom;
381 }
382 else
383 {
384 // conjoin all invariant clauses
385 result.invariant_expr = conjunction(invariant_clauses);
386 }
387
388 // unpack assigns clause targets
389 if(!assigns_clauses.empty())
390 {
391 for(auto &operand : assigns_clauses)
392 {
393 result.assigns.insert(operand);
394 }
395 }
396 else
397 {
398 // infer assigns clause targets if none given
399 auto inferred = dfcc_infer_loop_assigns(
400 local_may_alias, loop.instructions, loop.head->source_location(), ns);
401 log.warning() << "No assigns clause provided for loop " << function_id
402 << "." << loop.latch->loop_number << " at "
403 << loop.head->source_location() << ". The inferred set {";
404 bool first = true;
405 for(const auto &expr : inferred)
406 {
407 if(!first)
408 {
409 log.warning() << ", ";
410 }
411 first = false;
412 log.warning() << format(expr);
413 }
414 log.warning() << "} might be incomplete or imprecise, please provide an "
415 "assigns clause if the analysis fails."
416 << messaget::eom;
417 result.assigns.swap(inferred);
418 }
419
420 if(result.decreases_clauses.empty())
421 {
422 log.warning() << "No decrease clause provided for loop " << function_id
423 << "." << loop.latch->loop_number << " at "
424 << loop.head->source_location()
425 << ". Termination will not be checked." << messaget::eom;
426 }
427 }
428 return result;
429}
430
432 const dfcc_loop_nesting_grapht &loop_nesting_graph,
433 const std::size_t loop_id,
434 const irep_idt &function_id,
435 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
436 dirtyt &dirty,
437 local_may_aliast &local_may_alias,
438 message_handlert &message_handler,
439 dfcc_libraryt &library,
440 symbol_table_baset &symbol_table)
441{
442 std::unordered_set<irep_idt> loop_locals =
443 gen_loop_locals_set(loop_nesting_graph, loop_id);
444
445 std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
446 loop_nesting_graph.get_predecessors(loop_id),
447 loop_locals,
448 dirty,
449 loop_info_map);
450
451 const namespacet ns(symbol_table);
452 struct contract_clausest contract_clauses = default_loop_contract_clauses(
453 loop_nesting_graph,
454 loop_id,
455 function_id,
456 local_may_alias,
457 message_handler,
458 ns);
459
460 std::set<std::size_t> inner_loops;
461 for(auto pred_idx : loop_nesting_graph.get_predecessors(loop_id))
462 {
463 inner_loops.insert(pred_idx);
464 }
465
466 std::set<std::size_t> outer_loops;
467 for(auto succ_idx : loop_nesting_graph.get_successors(loop_id))
468 {
469 outer_loops.insert(succ_idx);
470 }
471
472 auto &loop = loop_nesting_graph[loop_id];
473 const auto cbmc_loop_number = loop.latch->loop_number;
474
475 // Generate "write set" variable
476 const auto write_set_var = dfcc_utilst::create_symbol(
477 symbol_table,
479 function_id,
480 "__write_set_loop_" + std::to_string(cbmc_loop_number),
481 loop.head->source_location());
482
483 // Generate "address of write set" variable
484 const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
485 symbol_table,
487 function_id,
488 "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
489 loop.head->source_location());
490
491 return {
492 loop_id,
493 cbmc_loop_number,
494 contract_clauses.assigns,
495 contract_clauses.invariant_expr,
496 contract_clauses.decreases_clauses,
497 loop_locals,
498 loop_tracked,
499 inner_loops,
500 outer_loops,
501 write_set_var,
502 addr_of_write_set_var};
503}
504
506 const irep_idt &function_id,
507 goto_functiont &goto_function,
508 const exprt &top_level_write_set,
509 const dfcc_loop_contract_modet loop_contract_mode,
510 symbol_table_baset &symbol_table,
511 message_handlert &message_handler,
512 dfcc_libraryt &library)
513 : function_id(function_id),
514 goto_function(goto_function),
515 top_level_write_set(top_level_write_set),
516 ns(symbol_table)
517{
518 dfcc_loop_nesting_grapht loop_nesting_graph;
519 goto_programt &goto_program = goto_function.body;
520 if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
521 {
522 messaget log(message_handler);
523 dfcc_check_loop_normal_form(goto_program, log);
524 loop_nesting_graph = build_loop_nesting_graph(goto_program);
525
526 const auto head = check_inner_loops_have_contracts(loop_nesting_graph);
527 if(head.has_value())
528 {
530 "Found loop without contract nested in a loop with a "
531 "contract.\nPlease "
532 "provide a contract or unwind this loop before applying loop "
533 "contracts.",
534 head.value()->source_location());
535 }
536
537 auto topsorted = loop_nesting_graph.topsort();
538
539 for(const auto idx : topsorted)
540 {
541 topsorted_loops.push_back(idx);
542 }
543 }
544
545 // At this point, either loop contracts were activated and the loop nesting
546 // graph describes the loop structure of the function,
547 // or loop contracts were not activated and the loop nesting graph is empty
548 // (i.e. there might be some loops in the function but we won't consider them
549 // for the instrumentation).
550 // In both cases, we tag program instructions and generate the dfcc_cfg_infot
551 // instance from that graph's contents. The tags will decide against which
552 // write set the instructions are going to be instrumented (either the
553 // function's write set, or the write set of a loop), and each dfcc_loop_infot
554 // contained in the loop_info_map describes a loop to be abstracted by a
555 // contract.
556
557 tag_loop_instructions(goto_program, loop_nesting_graph);
558
559 // generate dfcc_cfg_loop_info for loops and add to loop_info_map
560 dirtyt dirty(goto_function);
561 local_may_aliast local_may_alias(goto_function);
562
563 for(const auto &loop_id : topsorted_loops)
564 {
565 loop_info_map.insert(
566 {loop_id,
568 loop_nesting_graph,
569 loop_id,
572 dirty,
573 local_may_alias,
574 message_handler,
575 library,
576 symbol_table)});
577
578 if(loop_nesting_graph.get_successors(loop_id).empty())
579 top_level_loops.push_back(loop_id);
580 }
581
582 // generate set of top level of locals
583 top_level_local.insert(
586
587 for(auto target = goto_function.body.instructions.begin();
588 target != goto_function.body.instructions.end();
589 target++)
590 {
591 if(target->is_decl() && dfcc_is_loop_top_level(target))
592 top_level_local.insert(target->decl_symbol().get_identifier());
593 }
594
597}
598
599void dfcc_cfg_infot::output(std::ostream &out) const
600{
601 out << "// dfcc_cfg_infot for: " << function_id << "\n";
602 out << "// top_level_local: {";
603 for(auto &id : top_level_local)
604 {
605 out << id << ", ";
606 }
607 out << "}\n";
608
609 out << "// top_level_tracked: {";
610 for(auto &id : top_level_tracked)
611 {
612 out << id << ", ";
613 }
614 out << "}\n";
615
616 out << "// loop:\n";
617 for(auto &loop : loop_info_map)
618 {
619 out << "// dfcc-loop_id:" << loop.first << "\n";
620 auto head = loop.second.find_head(goto_function.body);
621 auto latch = loop.second.find_latch(goto_function.body);
622 out << "// head:\n";
623 head.value()->output(out);
624 out << "// latch:\n";
625 latch.value()->output(out);
626 loop.second.output(out);
627 }
628 out << "// program:\n";
630 {
631 out << "// dfcc-loop-id:" << dfcc_get_loop_id(target).value();
632 out << " cbmc-loop-number:" << target->loop_number;
633 out << " top-level:" << dfcc_is_loop_top_level(target);
634 out << " head:" << dfcc_is_loop_head(target);
635 out << " body:" << dfcc_is_loop_body(target);
636 out << " exiting:" << dfcc_is_loop_exiting(target);
637 out << " latch:" << dfcc_is_loop_latch(target);
638 out << "\n";
639 target->output(out);
640 }
641}
642
643const exprt &
645{
646 auto loop_id_opt = dfcc_get_loop_id(target);
648 loop_id_opt.has_value() &&
649 is_valid_loop_or_top_level_id(loop_id_opt.value()));
650 auto loop_id = loop_id_opt.value();
651 if(is_top_level_id(loop_id))
652 {
653 return top_level_write_set;
654 }
655 else
656 {
657 return loop_info_map.at(loop_id).addr_of_write_set_var;
658 }
659}
660
661const std::unordered_set<irep_idt> &
663{
664 auto loop_id_opt = dfcc_get_loop_id(target);
666 loop_id_opt.has_value() &&
667 is_valid_loop_or_top_level_id(loop_id_opt.value()));
668 auto loop_id = loop_id_opt.value();
669 if(is_top_level_id(loop_id))
670 {
671 return top_level_tracked;
672 }
673 else
674 {
675 return loop_info_map.at(loop_id).tracked;
676 }
677}
678
679const std::unordered_set<irep_idt> &
681{
682 auto loop_id_opt = dfcc_get_loop_id(target);
684 loop_id_opt.has_value() &&
685 is_valid_loop_or_top_level_id(loop_id_opt.value()));
686 auto loop_id = loop_id_opt.value();
687 if(is_top_level_id(loop_id))
688 {
689 return top_level_local;
690 }
691 else
692 {
693 return loop_info_map.at(loop_id).local;
694 }
695}
696
697const exprt &dfcc_cfg_infot::get_outer_write_set(std::size_t loop_id) const
698{
700 auto outer_loop_opt = get_outer_loop_identifier(loop_id);
701 return outer_loop_opt.has_value()
702 ? get_loop_info(outer_loop_opt.value()).addr_of_write_set_var
704}
705
706const dfcc_loop_infot &
707dfcc_cfg_infot::get_loop_info(const std::size_t loop_id) const
708{
709 return loop_info_map.at(loop_id);
710}
711
712// find the identifier or the immediately enclosing loop in topological order
714dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const
715{
717 auto outer_loops = get_loop_info(loop_id).outer_loops;
718
719 // find the first loop in the topological order that is connected
720 // to our node.
721 for(const auto &idx : get_loops_toposorted())
722 {
723 if(
724 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
725 outer_loops.end())
726 {
727 return idx;
728 }
729 }
730 // return nullopt for loops that are not nested in other loops
731 return nullopt;
732}
733
734bool dfcc_cfg_infot::is_valid_loop_or_top_level_id(const std::size_t id) const
735{
736 return id <= loop_info_map.size();
737}
738
739bool dfcc_cfg_infot::is_valid_loop_id(const std::size_t id) const
740{
741 return id < loop_info_map.size();
742}
743
744bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
745{
746 return id == loop_info_map.size();
747}
748
750 goto_programt::const_targett target) const
751{
752 PRECONDITION(target->is_decl() || target->is_dead());
753 auto &ident = target->is_decl() ? target->decl_symbol().get_identifier()
754 : target->dead_symbol().get_identifier();
755 auto &tracked = get_tracked_set(target);
756 return tracked.find(ident) != tracked.end();
757}
758#include <iostream>
759
765 const exprt &lhs,
766 const std::unordered_set<irep_idt> &local,
767 const std::unordered_set<irep_idt> &tracked)
768{
769 auto root_objects = dfcc_root_objects(lhs);
770
771 // Check wether all root_objects can be resolved to actual identifiers.
772 std::unordered_set<irep_idt> root_idents;
773 for(const auto &expr : root_objects)
774 {
775 if(expr.id() != ID_symbol)
776 {
777 // This means that lhs contains either an address-of operation or a
778 // dereference operation, and we cannot really know statically which
779 // object it refers to without using the may_alias analysis.
780 // Since the may_alias analysis is also used to infer targets, for
781 // soundness reasons we cannot also use it to skip checks, so we check
782 // the assignment. If happens to assign to a mix of tracked and
783 // non-tracked identifiers the check will fail but this is sound anyway.
784 return true;
785 }
786 const auto &id = to_symbol_expr(expr).get_identifier();
788 {
789 // Skip the check if we have a single cprover symbol as root object
790 // cprover symbols are used for generic checks instrumentation and are
791 // de-facto ghost code. We implicitly allow assignments to these symbols.
792 // To make this really sound we should use a white list of known
793 // CPROVER symbols, because right now simply naming a symbol with the
794 // CPROVER prefix bypasses the checks.
795 if(root_objects.size() == 1)
796 {
797 return false;
798 }
799 else
800 {
801 // error out if we have a cprover symbol and something else in the set
803 "LHS expression `" + format_to_string(lhs) +
804 "` in assignment refers to a cprover symbol and something else.");
805 }
806 }
807 root_idents.insert(id);
808 }
809
810 // The root idents set is Non-empty.
811 // true iff root_idents contains non-local idents
812 bool some_non_local = false;
813 // true iff root_idents contains some local that is not tracked
814 bool some_local_not_tracked = false;
815 // true iff root_idents contains only local that are not tracked
816 bool all_local_not_tracked = true;
817 // true iff root_idents contains only local that are tracked
818 bool all_local_tracked = true;
819 for(const auto &root_ident : root_idents)
820 {
821 bool loc = local.find(root_ident) != local.end();
822 bool tra = tracked.find(root_ident) != tracked.end();
823 bool local_tracked = loc && tra;
824 bool local_not_tracked = loc && !tra;
825 some_non_local |= !loc;
826 some_local_not_tracked |= local_not_tracked;
827 all_local_not_tracked &= local_not_tracked;
828 all_local_tracked &= local_tracked;
829 }
830
831 // some root identifier is not local, the lhs must be checked
832 if(some_non_local)
833 {
834 // if we also have a local that is not tracked, we know the check will
835 // fail with the current algorithm, error out.
836 if(some_local_not_tracked)
837 {
839 "LHS expression `" + format_to_string(lhs) +
840 "` in assignment mentions both explicitly and implicitly tracked "
841 "memory locations. DFCC does not yet handle that case, please "
842 "reformulate the assignment into separate assignments to either "
843 "memory locations.");
844 }
845 return true;
846 }
847 else
848 {
849 // all root identifiers are local
850 // if they are all not tracked, we *have* to skip the check
851 // (and it is sound to do so, because we know that the identifiers that
852 // are not tracked explicitly are not dirty and not assigned to outside of
853 // their scope).
854 // if they are all tracked, we *can* skip the check, because they are all
855 // local to that scope anyway and implicitly allowed.
856 if(all_local_not_tracked || all_local_tracked)
857 {
858 return false;
859 }
860 else
861 {
862 // we have a combination of tracked and not-tracked locals, we know
863 // the check will fail with the current algorithm, error out.
865 "LHS expression `" + format_to_string(lhs) +
866 "` in assignment mentions both explicitly and implicitly tracked "
867 "memory locations. DFCC does not yet handle that case, please "
868 "reformulate the assignment into separate assignments to either "
869 "memory locations.");
870 }
871 }
872}
873
875{
876 PRECONDITION(target->is_assign() || target->is_function_call());
877 const exprt &lhs =
878 target->is_assign() ? target->assign_lhs() : target->call_lhs();
879 if(lhs.is_nil())
880 return false;
882 lhs, get_local_set(target), get_tracked_set(target));
883}
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
std::unordered_set< irep_idt > top_level_local
Set of identifiers DECL at top level.
const exprt & top_level_write_set
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
const optionalt< 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...
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...
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.
dfcc_cfg_infot(const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
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 for that instruction.
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.
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.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
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.
optionalt< 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...
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.
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.
optionalt< goto_programt::targett > find_latch(goto_programt &goto_program) const
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:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
instructionst::const_iterator const_targett
A generic directed graph with a parametric node type.
Definition graph.h:167
std::vector< node_indext > get_predecessors(const node_indext &n) const
Definition graph.h:943
std::size_t size() const
Definition graph.h:212
std::vector< node_indext > get_successors(const node_indext &n) const
Definition graph.h:956
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Definition graph.h:879
Thrown when we can't handle something in an input source file.
bool is_nil() const
Definition irep.h:376
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
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:3026
const irep_idt & get_identifier() const
Definition std_expr.h:142
The symbol table base class interface.
The Boolean constant true.
Definition std_expr.h:3008
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
static std::unordered_set< irep_idt > gen_loop_locals_set(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id)
Collect identifiers that are local to this loop only (excluding nested 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 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 optionalt< 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)
static bool has_contract(const goto_programt::const_targett &latch_target)
Returns true iff some contract clause expression is attached to the latch condition of this loop.
static const exprt::operandst & get_invariants(const goto_programt::const_targett &latch_target)
Extracts the invariant clause expression from the latch condition.
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, local_may_aliast &local_may_alias, 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 optionalt< goto_programt::targett > check_inner_loops_have_contracts(const dfcc_loop_nesting_grapht &loop_nesting_graph)
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that ha...
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, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map, dirtyt &dirty, local_may_aliast &local_may_alias, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table)
static const exprt::operandst & get_assigns(const goto_programt::const_targett &latch_target)
Extracts the assigns clause expression from the latch condition.
static const exprt::operandst & get_decreases(const goto_programt::const_targett &latch_target)
Extracts the decreases clause expression from the latch condition.
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.
assignst dfcc_infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)
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_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
@ NONE
Do not apply loop contracts.
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)
bool dfcc_is_loop_exiting(const goto_programt::instructiont::const_targett &target)
optionalt< std::size_t > dfcc_get_loop_id(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.
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
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
Field-insensitive, location-sensitive may-alias analysis.
Compute natural loops in a goto_function.
nonstd::optional< T > optionalt
Definition optional.h:35
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
exprt::operandst decreases_clauses
contract_clausest(const exprt::operandst &decreases)
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...