cprover
Loading...
Searching...
No Matches
ensure_one_backedge_per_target.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Ensure one backedge per target
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
13
14#include "goto_model.h"
15
16#include <algorithm>
17
21{
22 return a->location_number < b->location_number;
23}
24
27 goto_programt &goto_program)
28{
29 auto &instruction = *it;
30 std::vector<goto_programt::targett> backedges;
31
32 // Check if this instruction has multiple incoming edges from (lexically)
33 // lower down the program. These aren't necessarily loop backedges (in fact
34 // the program might be acyclic), but that's the most common case.
35 for(auto predecessor : instruction.incoming_edges)
36 {
37 if(predecessor->location_number > instruction.location_number)
38 backedges.push_back(predecessor);
39 }
40
41 if(backedges.size() < 2)
42 return false;
43
44 std::sort(backedges.begin(), backedges.end(), location_number_less_than);
45
46 auto last_backedge = backedges.back();
47 backedges.pop_back();
48
49 // Can't transform if the bottom of the (probably) loop is of unexpected
50 // form:
51 if(!last_backedge->is_goto() || last_backedge->targets.size() > 1)
52 {
53 return false;
54 }
55
56 // If the last backedge is a conditional jump, add an extra unconditional
57 // backedge after it:
58 if(!last_backedge->guard.is_true())
59 {
60 auto new_goto =
61 goto_program.insert_after(last_backedge, goto_programt::make_goto(it));
62 // Turn the existing `if(x) goto head; succ: ...`
63 // into `if(!x) goto succ; goto head; succ: ...`
64 last_backedge->guard = not_exprt(last_backedge->guard);
65 last_backedge->set_target(std::next(new_goto));
66 // Use the new backedge as the one true way to the header:
67 last_backedge = new_goto;
68 }
69
70 // Redirect all but one of the backedges to the last one.
71 // For example, transform
72 // "a: if(x) goto a; if(y) goto a;" into
73 // "a: if(x) goto b; if(y) b: goto a;"
74 // In the common case where this is a natural loop this corresponds to
75 // branching to the bottom of the loop on a `continue` statement.
76 for(auto backedge : backedges)
77 {
78 if(backedge->is_goto() && backedge->targets.size() == 1)
79 {
80 backedge->set_target(last_backedge);
81 }
82 }
83
84 return true;
85}
86
88{
89 bool any_change = false;
90
91 for(auto it = goto_program.instructions.begin();
92 it != goto_program.instructions.end();
93 ++it)
94 {
95 any_change |= ensure_one_backedge_per_target(it, goto_program);
96 }
97
98 return any_change;
99}
100
102{
103 auto &goto_function = goto_model_function.get_goto_function();
104
105 if(ensure_one_backedge_per_target(goto_function.body))
106 {
107 goto_function.body.update();
108 goto_model_function.compute_location_numbers();
109 return true;
110 }
111
112 return false;
113}
114
116{
117 bool any_change = false;
118
119 for(auto &id_and_function : goto_model.goto_functions.function_map)
120 any_change |= ensure_one_backedge_per_target(id_and_function.second.body);
121
122 if(any_change)
123 goto_model.goto_functions.update();
124
125 return any_change;
126}
function_mapt function_map
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:183
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:225
void compute_location_numbers()
Re-number our goto_function.
Definition goto_model.h:209
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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
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())
Boolean negation.
Definition std_expr.h:2181
static bool location_number_less_than(const goto_programt::targett &a, const goto_programt::targett &b)
bool ensure_one_backedge_per_target(goto_programt::targett &it, goto_programt &goto_program)
Ensure one backedge per target.
Symbol Table + CFG.