cprover
Loading...
Searching...
No Matches
dfcc_check_loop_normal_form.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for loop contracts
4
5Author: Qinheping Hu, qinhh@amazon.com
6Author: Remi Delmas, delmasrd@amazon.com
7
8\*******************************************************************/
9
11
14
16{
17 natural_loops_mutablet natural_loops(goto_program);
18
19 // instruction span for each loop
20 std::vector<std::pair<goto_programt::targett, goto_programt::targett>> spans;
21
22 for(auto &loop : natural_loops.loop_map)
23 {
24 auto head = loop.first;
25 auto &loop_instructions = loop.second;
26
27 if(loop_instructions.size() <= 1)
28 {
29 // Ignore single instruction loops of the form
30 // `LOOP: IF cond GOTO LOOP;`
31 continue;
32 }
33
34 auto latch = head;
35 bool latch_found = false;
36
37 // Find latch and check it is unique
38 for(const auto &t : loop_instructions)
39 {
40 if(t->is_goto() && t->get_target() == head)
41 {
42 if(latch_found)
43 {
44 log.error() << "Loop starting at:"
45 << "\n- head: " << head->source_location()
46 << "\nhas more than one latch instruction:"
47 << "\n- latch1: " << latch->source_location()
48 << "\n- latch2: " << t->source_location()
51 "Found loop with more than one latch instruction");
52 }
53 latch = t;
54 latch_found = true;
55 }
56 }
57
58 INVARIANT(latch_found, "Natural loop latch found");
59
60 // Check that instruction spans are not overlapping
61 for(const auto &span : spans)
62 {
63 bool head_in_span =
64 span.first->location_number <= head->location_number &&
65 head->location_number <= span.second->location_number;
66
67 bool latch_in_span =
68 span.first->location_number <= latch->location_number &&
69 latch->location_number <= span.second->location_number;
70
72 {
73 log.error() << "Loop spanning:"
74 << "\n- head: " << head->source_location()
75 << "\n- latch: " << latch->source_location()
76 << "\noverlaps loop spanning:"
77 << "\n- head: " << span.first->source_location()
78 << "\n- latch: " << span.second->source_location()
81 "Found loops with overlapping instruction spans");
82 }
83 }
84
85 spans.push_back({head, latch});
86
87 // Check that:
88 // 1. all loop instructions are in the range [head, latch]
89 // 2. except for the head instruction, no incoming edge from outside the
90 // loop
91 for(const auto &i : loop_instructions)
92 {
93 if(
94 i->location_number < head->location_number ||
95 i->location_number > latch->location_number)
96 {
97 log.error() << "Loop body instruction at:"
98 << "\n- " << i->source_location() << "\nis outside of"
99 << "\n- head: " << head->source_location()
100 << "\n- latch: " << latch->source_location()
101 << messaget::eom;
103 "Found loop body instruction outside of the [head, latch] "
104 "instruction span");
105 }
106
107 for(const auto &from : i->incoming_edges)
108 {
109 if(i != head && !loop_instructions.contains(from))
110 {
111 log.error() << "Loop body instruction at:"
112 << "\n- " << i->source_location()
113 << "\n has incoming edge from outside the loop at:"
114 << "\n- " << from->source_location() << messaget::eom;
115
117 "Found loop body instruction with incoming edge from outside the "
118 "loop");
119 }
120 }
121 }
122
123 // Check if a loop contains another loop's head (resp. latch) then
124 // it also contains the latch (resp. head)
125 for(auto &other_loop : natural_loops.loop_map)
126 {
127 auto &other_loop_instructions = other_loop.second;
128 bool contains_head = other_loop_instructions.contains(head);
129 bool contains_latch = other_loop_instructions.contains(latch);
130 INVARIANT(
132 "nested loop head and latch are in outer loop");
133 }
134
135 // all checks passed, now we perform some instruction rewriting
136
137 // Convert conditional latch into exiting + unconditional latch.
138 // ```
139 // IF g THEN GOTO HEAD
140 // --------------------------
141 // IF !g THEN GOTO EXIT
142 // GOTO HEAD
143 // EXIT: SKIP
144 // ```
145 if(latch->has_condition() && !latch->condition().is_true())
146 {
147 const source_locationt &loc = latch->source_location();
148 const auto &exit =
149 goto_program.insert_after(latch, goto_programt::make_skip(loc));
150
152 goto_program,
153 latch,
155 exit, not_exprt(latch->condition()), latch->source_location()));
156
157 // CAUTION: The condition expression needs to be updated in place because
158 // this is where loop contract clauses are stored as extra ireps.
159 // Overwriting this expression with a fresh expression will also lose the
160 // loop contract.
161 exprt latch_condition = latch->condition();
163 *latch = goto_programt::make_goto(head, latch_condition, loc);
164 }
165
166 // The latch node is now an unconditional jump.
167
168 // insert a SKIP pre-head node and reroute all incoming edges to that node,
169 // except for edge coming from the latch.
171 goto_program, head, goto_programt::make_skip(head->source_location()));
172 latch->set_target(head);
173 }
174 goto_program.update();
175}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:223
A generic container class for the GOTO intermediate representation of one function.
void update()
Update all indices.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
loop_mapt loop_map
source_locationt source_location
Definition message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
Boolean negation.
Definition std_expr.h:2278
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.
Compute natural loops in a goto_function.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
Definition utils.cpp:244