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
34static bool has_contract(
35 const goto_programt::const_targett &latch_target,
36 const bool check_side_effect)
37{
38 return get_loop_assigns(latch_target).is_not_nil() ||
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
43void 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
130static std::optional<goto_programt::targett> check_has_contract_rec(
131 const dfcc_loop_nesting_grapht &loop_nesting_graph,
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(
143 loop_nesting_graph,
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
156static std::optional<goto_programt::targett> check_inner_loops_have_contracts(
157 const dfcc_loop_nesting_grapht &loop_nesting_graph,
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,
178 dfcc_loop_nesting_grapht &loop_nesting_graph)
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
190 for(goto_programt::targett t : instruction_iterators)
191 {
192 // Skip instructions that are already tagged and belong to inner loops.
193 auto loop_id_opt = dfcc_get_loop_id(t);
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
227static 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)->get_identifier() ==
239 ident)
240 {
241 return true;
242 }
243 // If `root_object` is not a symbol, then it contains a combination of
244 // address-of and dereference operators that cannot be statically
245 // resolved to a symbol.
246 // Since we know `ident` is not dirty, we know that dereference
247 // operations cannot land on that `ident`. So the root_object cannot
248 // describe a memory location within the object backing that ident.
249 // We conclude that ident is not assigned by this target and move on to
250 // the next target.
251 }
252 }
253 return false;
254}
255
258static std::unordered_set<irep_idt> gen_loop_locals_set(
259 const dfcc_loop_nesting_grapht &loop_nesting_graph,
260 const std::size_t loop_id)
261{
262 std::unordered_set<irep_idt> loop_locals;
263 for(const auto &target : loop_nesting_graph[loop_id].instructions)
264 {
265 auto loop_id_opt = dfcc_get_loop_id(target);
266 if(
267 target->is_decl() && loop_id_opt.has_value() &&
268 loop_id_opt.value() == loop_id)
269 {
270 loop_locals.insert(target->decl_symbol().get_identifier());
271 }
272 }
273 return loop_locals;
274}
275
289static std::unordered_set<irep_idt> gen_tracked_set(
290 const std::vector<std::size_t> &inner_loops_ids,
291 const std::unordered_set<irep_idt> &locals,
292 dirtyt &dirty,
293 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
294{
295 std::unordered_set<irep_idt> tracked;
296 for(const auto &ident : locals)
297 {
298 if(dirty(ident))
299 {
300 tracked.insert(ident);
301 }
302 else
303 {
304 // Check if this ident is touched by one of the inner loops
305 for(const auto inner_loop_id : inner_loops_ids)
306 {
307 if(is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
308 tracked.insert(ident);
309 }
310 }
311 }
312 return tracked;
313}
314
325
329 const dfcc_loop_nesting_grapht &loop_nesting_graph,
330 const std::size_t loop_id,
331 const irep_idt &function_id,
332 local_may_aliast &local_may_alias,
333 const bool check_side_effect,
334 message_handlert &message_handler,
335 const namespacet &ns)
336{
337 messaget log(message_handler);
338 const auto &loop = loop_nesting_graph[loop_id];
339
340 // Process loop contract clauses
341 exprt::operandst invariant_clauses =
342 get_loop_invariants(loop.latch, check_side_effect).operands();
343 exprt::operandst assigns_clauses = get_loop_assigns(loop.latch).operands();
344
345 // Initialise defaults
346 struct contract_clausest result(
347 get_loop_decreases(loop.latch, check_side_effect).operands());
348
349 // Generate defaults for all clauses if at least one type of clause is defined
350 if(
351 !invariant_clauses.empty() || !result.decreases_clauses.empty() ||
352 !assigns_clauses.empty())
353 {
354 if(invariant_clauses.empty())
355 {
356 // use a default invariant if none given.
357 result.invariant_expr = true_exprt{};
358 // assigns clause is missing; we will try to automatic inference
359 log.warning() << "No invariant provided for loop " << function_id << "."
360 << loop.latch->loop_number << " at "
361 << loop.head->source_location()
362 << ". Using 'true' as a sound default invariant. Please "
363 "provide an invariant the default is too weak."
364 << messaget::eom;
365 }
366 else
367 {
368 // conjoin all invariant clauses
369 result.invariant_expr = conjunction(invariant_clauses);
370 }
371
372 // unpack assigns clause targets
373 if(!assigns_clauses.empty())
374 {
375 for(auto &operand : assigns_clauses)
376 {
377 result.assigns.insert(operand);
378 }
379 }
380 else
381 {
382 // infer assigns clause targets if none given
383 auto inferred = dfcc_infer_loop_assigns(
384 local_may_alias, loop.instructions, loop.head->source_location(), ns);
385 log.warning() << "No assigns clause provided for loop " << function_id
386 << "." << loop.latch->loop_number << " at "
387 << loop.head->source_location() << ". The inferred set {";
388 bool first = true;
389 for(const auto &expr : inferred)
390 {
391 if(!first)
392 {
393 log.warning() << ", ";
394 }
395 first = false;
396 log.warning() << format(expr);
397 }
398 log.warning() << "} might be incomplete or imprecise, please provide an "
399 "assigns clause if the analysis fails."
400 << messaget::eom;
401 result.assigns.swap(inferred);
402 }
403
404 if(result.decreases_clauses.empty())
405 {
406 log.warning() << "No decrease clause provided for loop " << function_id
407 << "." << loop.latch->loop_number << " at "
408 << loop.head->source_location()
409 << ". Termination will not be checked." << messaget::eom;
410 }
411 }
412 return result;
413}
414
416 const dfcc_loop_nesting_grapht &loop_nesting_graph,
417 const std::size_t loop_id,
418 const irep_idt &function_id,
419 const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
420 dirtyt &dirty,
421 local_may_aliast &local_may_alias,
422 const bool check_side_effect,
423 message_handlert &message_handler,
424 dfcc_libraryt &library,
425 symbol_table_baset &symbol_table)
426{
427 std::unordered_set<irep_idt> loop_locals =
428 gen_loop_locals_set(loop_nesting_graph, loop_id);
429
430 std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
431 loop_nesting_graph.get_predecessors(loop_id),
432 loop_locals,
433 dirty,
434 loop_info_map);
435
436 const namespacet ns(symbol_table);
437 struct contract_clausest contract_clauses = default_loop_contract_clauses(
438 loop_nesting_graph,
439 loop_id,
440 function_id,
441 local_may_alias,
442 check_side_effect,
443 message_handler,
444 ns);
445
446 std::set<std::size_t> inner_loops;
447 for(auto pred_idx : loop_nesting_graph.get_predecessors(loop_id))
448 {
449 inner_loops.insert(pred_idx);
450 }
451
452 std::set<std::size_t> outer_loops;
453 for(auto succ_idx : loop_nesting_graph.get_successors(loop_id))
454 {
455 outer_loops.insert(succ_idx);
456 }
457
458 auto &loop = loop_nesting_graph[loop_id];
459 const auto cbmc_loop_number = loop.latch->loop_number;
460
461 // Generate "write set" variable
462 const auto write_set_var = dfcc_utilst::create_symbol(
463 symbol_table,
465 function_id,
466 "__write_set_loop_" + std::to_string(cbmc_loop_number),
467 loop.head->source_location());
468
469 // Generate "address of write set" variable
470 const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
471 symbol_table,
473 function_id,
474 "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
475 loop.head->source_location());
476
477 return {
478 loop_id,
479 cbmc_loop_number,
480 contract_clauses.assigns,
481 contract_clauses.invariant_expr,
482 contract_clauses.decreases_clauses,
483 loop_locals,
484 loop_tracked,
485 inner_loops,
486 outer_loops,
487 write_set_var,
488 addr_of_write_set_var};
489}
490
492 const irep_idt &function_id,
493 goto_functiont &goto_function,
494 const exprt &top_level_write_set,
495 const loop_contract_configt &loop_contract_config,
496 symbol_table_baset &symbol_table,
497 message_handlert &message_handler,
498 dfcc_libraryt &library)
499 : function_id(function_id),
500 goto_function(goto_function),
501 top_level_write_set(top_level_write_set),
502 ns(symbol_table)
503{
504 dfcc_loop_nesting_grapht loop_nesting_graph;
505 goto_programt &goto_program = goto_function.body;
506 if(loop_contract_config.apply_loop_contracts)
507 {
508 messaget log(message_handler);
509 dfcc_check_loop_normal_form(goto_program, log);
510 loop_nesting_graph = build_loop_nesting_graph(goto_program);
511
512 const auto head = check_inner_loops_have_contracts(
513 loop_nesting_graph, loop_contract_config.check_side_effect);
514 if(head.has_value())
515 {
516 throw invalid_source_file_exceptiont(
517 "Found loop without contract nested in a loop with a "
518 "contract.\nPlease "
519 "provide a contract or unwind this loop before applying loop "
520 "contracts.",
521 head.value()->source_location());
522 }
523
524 auto topsorted = loop_nesting_graph.topsort();
525
526 for(const auto idx : topsorted)
527 {
528 topsorted_loops.push_back(idx);
529 }
530 }
531
532 // At this point, either loop contracts were activated and the loop nesting
533 // graph describes the loop structure of the function,
534 // or loop contracts were not activated and the loop nesting graph is empty
535 // (i.e. there might be some loops in the function but we won't consider them
536 // for the instrumentation).
537 // In both cases, we tag program instructions and generate the dfcc_cfg_infot
538 // instance from that graph's contents. The tags will decide against which
539 // write set the instructions are going to be instrumented (either the
540 // function's write set, or the write set of a loop), and each dfcc_loop_infot
541 // contained in the loop_info_map describes a loop to be abstracted by a
542 // contract.
543
544 tag_loop_instructions(goto_program, loop_nesting_graph);
545
546 // generate dfcc_cfg_loop_info for loops and add to loop_info_map
547 dirtyt dirty(goto_function);
548 local_may_aliast local_may_alias(goto_function);
549
550 for(const auto &loop_id : topsorted_loops)
551 {
552 loop_info_map.insert(
553 {loop_id,
555 loop_nesting_graph,
556 loop_id,
557 function_id,
558 loop_info_map,
559 dirty,
560 local_may_alias,
561 loop_contract_config.check_side_effect,
562 message_handler,
563 library,
564 symbol_table)});
565
566 if(loop_nesting_graph.get_successors(loop_id).empty())
567 top_level_loops.push_back(loop_id);
568 }
569
570 // generate set of top level of locals
571 top_level_local.insert(
572 goto_function.parameter_identifiers.begin(),
573 goto_function.parameter_identifiers.end());
574
575 for(auto target = goto_function.body.instructions.begin();
576 target != goto_function.body.instructions.end();
577 target++)
578 {
579 if(target->is_decl() && dfcc_is_loop_top_level(target))
580 top_level_local.insert(target->decl_symbol().get_identifier());
581 }
582
583 top_level_tracked =
584 gen_tracked_set(top_level_loops, top_level_local, dirty, loop_info_map);
585}
586
587void dfcc_cfg_infot::output(std::ostream &out) const
588{
589 out << "// dfcc_cfg_infot for: " << function_id << "\n";
590 out << "// top_level_local: {";
591 for(auto &id : top_level_local)
592 {
593 out << id << ", ";
594 }
595 out << "}\n";
596
597 out << "// top_level_tracked: {";
598 for(auto &id : top_level_tracked)
599 {
600 out << id << ", ";
601 }
602 out << "}\n";
603
604 out << "// loop:\n";
605 for(auto &loop : loop_info_map)
606 {
607 out << "// dfcc-loop_id:" << loop.first << "\n";
608 auto head = loop.second.find_head(goto_function.body);
609 auto latch = loop.second.find_latch(goto_function.body);
610 out << "// head:\n";
611 head.value()->output(out);
612 out << "// latch:\n";
613 latch.value()->output(out);
614 loop.second.output(out);
615 }
616 out << "// program:\n";
618 {
619 out << "// dfcc-loop-id:" << dfcc_get_loop_id(target).value();
620 out << " cbmc-loop-number:" << target->loop_number;
621 out << " top-level:" << dfcc_is_loop_top_level(target);
622 out << " head:" << dfcc_is_loop_head(target);
623 out << " body:" << dfcc_is_loop_body(target);
624 out << " exiting:" << dfcc_is_loop_exiting(target);
625 out << " latch:" << dfcc_is_loop_latch(target);
626 out << "\n";
627 target->output(out);
628 }
629}
630
632 const std::size_t loop_id) const
633{
634 if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip())
635 {
636 return loop_id;
637 }
639 get_outer_loop_identifier(loop_id).value_or(top_level_id()));
640}
641
642const exprt &
644{
645 auto loop_id_opt = dfcc_get_loop_id(target);
647 loop_id_opt.has_value() &&
648 is_valid_loop_or_top_level_id(loop_id_opt.value()));
649 auto loop_id = get_first_id_not_skipped_or_top_level_id(loop_id_opt.value());
650 if(is_top_level_id(loop_id))
651 {
652 return top_level_write_set;
653 }
654 else
655 {
656 return loop_info_map.at(loop_id).addr_of_write_set_var;
657 }
658}
659
660const std::unordered_set<irep_idt> &
662{
663 auto loop_id_opt = dfcc_get_loop_id(target);
665 loop_id_opt.has_value() &&
666 is_valid_loop_or_top_level_id(loop_id_opt.value()));
667 auto loop_id = loop_id_opt.value();
668 if(is_top_level_id(loop_id))
669 {
670 return top_level_tracked;
671 }
672 else
673 {
674 return loop_info_map.at(loop_id).tracked;
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() &&
684 is_valid_loop_or_top_level_id(loop_id_opt.value()));
685 auto loop_id = loop_id_opt.value();
686 if(is_top_level_id(loop_id))
687 {
688 return top_level_local;
689 }
690 else
691 {
692 return loop_info_map.at(loop_id).local;
693 }
694}
695
696const exprt &dfcc_cfg_infot::get_outer_write_set(std::size_t loop_id) const
697{
699 auto outer_loop_opt = get_outer_loop_identifier(loop_id);
700 return outer_loop_opt.has_value()
701 ? get_loop_info(outer_loop_opt.value()).addr_of_write_set_var
703}
704
705const dfcc_loop_infot &
706dfcc_cfg_infot::get_loop_info(const std::size_t loop_id) const
707{
708 return loop_info_map.at(loop_id);
709}
710
711// find the identifier or the immediately enclosing loop in topological order
712const std::optional<std::size_t>
713dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const
714{
716 auto outer_loops = get_loop_info(loop_id).outer_loops;
717
718 // find the first loop in the topological order that is connected
719 // to our node.
720 for(const auto &idx : get_loops_toposorted())
721 {
722 if(
723 std::find(outer_loops.begin(), outer_loops.end(), idx) !=
724 outer_loops.end())
725 {
726 return idx;
727 }
728 }
729 // return nullopt for loops that are not nested in other loops
730 return std::nullopt;
731}
732
733bool dfcc_cfg_infot::is_valid_loop_or_top_level_id(const std::size_t id) const
734{
735 return id <= loop_info_map.size();
736}
737
738bool dfcc_cfg_infot::is_valid_loop_id(const std::size_t id) const
739{
740 return id < loop_info_map.size();
741}
742
743bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
744{
745 return id == loop_info_map.size();
746}
747
749{
750 return loop_info_map.size();
751}
752
754 goto_programt::const_targett target) const
755{
756 PRECONDITION(target->is_decl() || target->is_dead());
757 auto &ident = target->is_decl() ? target->decl_symbol().get_identifier()
758 : target->dead_symbol().get_identifier();
759 auto &tracked = get_tracked_set(target);
760 return tracked.find(ident) != tracked.end();
761}
762
768 const exprt &lhs,
769 const std::unordered_set<irep_idt> &local,
770 const std::unordered_set<irep_idt> &tracked)
771{
772 auto root_objects = dfcc_root_objects(lhs);
773
774 // Check wether all root_objects can be resolved to actual identifiers.
775 std::unordered_set<irep_idt> root_idents;
776 for(const auto &expr : root_objects)
777 {
778 if(expr.id() != ID_symbol)
779 {
780 // This means that lhs contains either an address-of operation or a
781 // dereference operation, and we cannot really know statically which
782 // object it refers to without using the may_alias analysis.
783 // Since the may_alias analysis is also used to infer targets, for
784 // soundness reasons we cannot also use it to skip checks, so we check
785 // the assignment. If happens to assign to a mix of tracked and
786 // non-tracked identifiers the check will fail but this is sound anyway.
787 return true;
788 }
789 const auto &id = to_symbol_expr(expr).get_identifier();
791 {
792 // Skip the check if we have a single cprover symbol as root object
793 // cprover symbols are used for generic checks instrumentation and are
794 // de-facto ghost code. We implicitly allow assignments to these symbols.
795 // To make this really sound we should use a white list of known
796 // CPROVER symbols, because right now simply naming a symbol with the
797 // CPROVER prefix bypasses the checks.
798 if(root_objects.size() == 1)
799 {
800 return false;
801 }
802 else
803 {
804 // error out if we have a cprover symbol and something else in the set
806 "LHS expression `" + format_to_string(lhs) +
807 "` in assignment refers to a cprover symbol and something else.");
808 }
809 }
810 root_idents.insert(id);
811 }
812
813 // The root idents set is Non-empty.
814 // true iff root_idents contains non-local idents
815 bool some_non_local = false;
816 // true iff root_idents contains some local that is not tracked
817 bool some_local_not_tracked = false;
818 // true iff root_idents contains only local that are not tracked
819 bool all_local_not_tracked = true;
820 // true iff root_idents contains only local that are tracked
821 bool all_local_tracked = true;
822 for(const auto &root_ident : root_idents)
823 {
824 bool loc = local.find(root_ident) != local.end();
825 bool tra = tracked.find(root_ident) != tracked.end();
826 bool local_tracked = loc && tra;
827 bool local_not_tracked = loc && !tra;
828 some_non_local |= !loc;
829 some_local_not_tracked |= local_not_tracked;
830 all_local_not_tracked &= local_not_tracked;
831 all_local_tracked &= local_tracked;
832 }
833
834 // some root identifier is not local, the lhs must be checked
835 if(some_non_local)
836 {
837 // if we also have a local that is not tracked, we know the check will
838 // fail with the current algorithm, error out.
839 if(some_local_not_tracked)
840 {
842 "LHS expression `" + format_to_string(lhs) +
843 "` in assignment mentions both explicitly and implicitly tracked "
844 "memory locations. DFCC does not yet handle that case, please "
845 "reformulate the assignment into separate assignments to either "
846 "memory locations.");
847 }
848 return true;
849 }
850 else
851 {
852 // all root identifiers are local
853 // if they are all not tracked, we *have* to skip the check
854 // (and it is sound to do so, because we know that the identifiers that
855 // are not tracked explicitly are not dirty and not assigned to outside of
856 // their scope).
857 // if they are all tracked, we *can* skip the check, because they are all
858 // local to that scope anyway and implicitly allowed.
859 if(all_local_not_tracked || all_local_tracked)
860 {
861 return false;
862 }
863 else
864 {
865 // we have a combination of tracked and not-tracked locals, we know
866 // the check will fail with the current algorithm, error out.
868 "LHS expression `" + format_to_string(lhs) +
869 "` in assignment mentions both explicitly and implicitly tracked "
870 "memory locations. DFCC does not yet handle that case, please "
871 "reformulate the assignment into separate assignments to either "
872 "memory locations.");
873 }
874 }
875}
876
878{
879 PRECONDITION(target->is_assign() || target->is_function_call());
880 const exprt &lhs =
881 target->is_assign() ? target->assign_lhs() : target->call_lhs();
882 if(lhs.is_nil())
883 return false;
885 lhs, get_local_set(target), get_tracked_set(target));
886}
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.
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
dfcc_cfg_infot(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)
const std::vector< std::size_t > & get_loops_toposorted() const
goto_functiont & goto_function
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.
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.
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.
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:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
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
bool is_not_nil() const
Definition irep.h:372
bool is_nil() const
Definition irep.h:368
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:94
The NIL expression.
Definition std_expr.h:3073
const irep_idt & get_identifier() const
Definition std_expr.h:160
The symbol table base class interface.
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
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, 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 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 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 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 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, 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...
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
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.
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.
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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...
Loop contract configurations.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Definition utils.cpp:723
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Definition utils.cpp:706
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:728