CBMC
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 std::map<
27
28 for(auto &loop : natural_loops.loop_map)
29 {
30 auto head = loop.first;
31 auto &loop_instructions = loop.second;
32
33 if(loop_instructions.size() <= 1)
34 {
35 // Ignore single instruction loops of the form
36 // `LOOP: IF cond GOTO LOOP;`
37 continue;
38 }
39
40 auto latch = head;
41 bool latch_found = false;
42
43 // Find latch and check it is unique
44 for(const auto &t : loop_instructions)
45 {
46 if(t->is_goto() && t->get_target() == head)
47 {
48 if(latch_found)
49 {
50 log.error() << "Loop starting at:"
51 << "\n- head: " << head->source_location()
52 << "\nhas more than one latch instruction:"
53 << "\n- latch1: " << latch->source_location()
54 << "\n- latch2: " << t->source_location()
57 "Found loop with more than one latch instruction");
58 }
59 latch = t;
60 latch_found = true;
61 }
62 }
63
64 INVARIANT(latch_found, "Natural loop latch found");
65
66 // Check that instruction spans are not overlapping
67 for(const auto &span : spans)
68 {
69 bool head_in_span =
70 span.first->location_number <= head->location_number &&
71 head->location_number <= span.second->location_number;
72
73 bool latch_in_span =
74 span.first->location_number <= latch->location_number &&
75 latch->location_number <= span.second->location_number;
76
78 {
79 log.error() << "Loop spanning:"
80 << "\n- head: " << head->source_location()
81 << "\n- latch: " << latch->source_location()
82 << "\noverlaps loop spanning:"
83 << "\n- head: " << span.first->source_location()
84 << "\n- latch: " << span.second->source_location()
87 "Found loops with overlapping instruction spans");
88 }
89 }
90
91 spans.push_back({head, latch});
92
93 // Check that:
94 // 1. all loop instructions are in the range [head, latch]
95 // 2. except for the head instruction, no incoming edge from outside the
96 // loop
97 for(const auto &i : loop_instructions)
98 {
99 if(
100 i->location_number < head->location_number ||
101 i->location_number > latch->location_number)
102 {
103 log.error() << "Loop body instruction at:"
104 << "\n- " << i->source_location() << "\nis outside of"
105 << "\n- head: " << head->source_location()
106 << "\n- latch: " << latch->source_location()
107 << messaget::eom;
109 "Found loop body instruction outside of the [head, latch] "
110 "instruction span");
111 }
112
113 for(const auto &from : i->incoming_edges)
114 {
115 if(i != head && !loop_instructions.contains(from))
116 {
117 log.error() << "Loop body instruction at:"
118 << "\n- " << i->source_location()
119 << "\n has incoming edge from outside the loop at:"
120 << "\n- " << from->source_location() << messaget::eom;
121
123 "Found loop body instruction with incoming edge from outside the "
124 "loop");
125 }
126 }
127 }
128
129 // Check if a loop contains another loop's head (resp. latch) then
130 // it also contains the latch (resp. head)
131 for(auto &other_loop : natural_loops.loop_map)
132 {
133 auto &other_loop_instructions = other_loop.second;
134 bool contains_head = other_loop_instructions.contains(head);
135 bool contains_latch = other_loop_instructions.contains(latch);
136 INVARIANT(
138 "nested loop head and latch are in outer loop");
139 }
140
141 if(!latch_head_pairs.emplace(latch, head).second)
143 }
144
145 // all checks passed, now we perform some instruction rewriting
146 for(auto &entry_pair : latch_head_pairs)
147 {
148 auto latch = entry_pair.first;
149 auto head = entry_pair.second;
150
151 // Convert conditional latch into exiting + unconditional latch.
152 // ```
153 // IF g THEN GOTO HEAD
154 // --------------------------
155 // IF !g THEN GOTO EXIT
156 // IF TRUE GOTO HEAD
157 // EXIT: SKIP
158 // ```
159 if(latch->has_condition() && !latch->condition().is_true())
160 {
161 const source_locationt &loc = latch->source_location();
162 const auto &exit =
163 goto_program.insert_after(latch, goto_programt::make_skip(loc));
164
165 // Insert the loop exit jump `F !g THEN GOTO EXIT`
167 goto_program,
168 latch,
170 exit, not_exprt(latch->condition()), latch->source_location()));
171
172 // Rewrite the latch node `IF g THEN GOTO HEAD`
173 // into `IF true THEN GOTO HEAD`
174 // and transplanting contract clauses
176
177 // Extract the contract clauses from the existing latch condition,
178 const exprt &latch_condition = latch->condition();
180 if(latch_assigns.is_not_nil())
182
185 if(latch_loop_invariant.is_not_nil())
187
189 if(latch_decreases.is_not_nil())
191
192 latch->condition_nonconst() = new_condition;
193 // The latch node is now an unconditional jump with contract clauses
194 }
195
196 // Insert a SKIP pre-head node and reroute all incoming edges to that node,
197 // except for edge coming from the latch.
199 goto_program, head, goto_programt::make_skip(head->source_location()));
200 latch->set_target(head);
201 }
202 goto_program.update();
203}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:231
A generic container class for the GOTO intermediate representation of one function.
void update()
Update all indices.
instructionst::iterator targett
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())
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
loop_mapt loop_map
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
Boolean negation.
Definition std_expr.h:2454
The Boolean constant true.
Definition std_expr.h:3190
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.
double log(double x)
Definition math.c:2449
Compute natural loops in a goto_function.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
void exit(int status)
Definition stdlib.c:102
A total order over targett and const_targett.
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:247