CBMC
dfcc_loop_tags.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 Author: Remi Delmas, delmasrd@amazon.com
7 
8 \*******************************************************************/
9 
10 #include "dfcc_loop_tags.h"
11 
12 const irep_idt ID_loop_id = "loop-id";
13 const irep_idt ID_loop_head = "loop-head";
14 const irep_idt ID_loop_body = "loop-body";
15 const irep_idt ID_loop_latch = "loop-latch";
16 const irep_idt ID_loop_exiting = "loop-exiting";
17 const irep_idt ID_loop_top_level = "loop-top-level";
18 
21  const std::size_t loop_id)
22 {
23  target->source_location_nonconst().set(ID_loop_id, loop_id);
24 }
25 
26 std::optional<std::size_t>
28 {
29  if(target->source_location().get(ID_loop_id).empty())
30  return {};
31 
32  return target->source_location().get_size_t(ID_loop_id);
33 }
34 
37  std::size_t loop_id)
38 {
39  auto loop_id_opt = dfcc_get_loop_id(target);
40  return loop_id_opt.has_value() && loop_id_opt.value() == loop_id;
41 }
42 
43 static void dfcc_set_loop_tag(
45  const irep_idt &tag)
46 {
47  target->source_location_nonconst().set(tag, true);
48 }
49 
50 static bool has_loop_tag(
52  const irep_idt &tag)
53 {
54  return target->source_location().get_bool(tag);
55 }
56 
58 {
60 }
61 
63 {
64  return has_loop_tag(target, ID_loop_head);
65 }
66 
68 {
70 }
71 
73 {
74  return has_loop_tag(target, ID_loop_body);
75 }
76 
78 {
80 }
81 
84 {
85  return has_loop_tag(target, ID_loop_exiting);
86 }
87 
89 {
91 }
92 
95 {
96  return has_loop_tag(target, ID_loop_latch);
97 }
98 
100 {
102 }
103 
106 {
107  return has_loop_tag(target, ID_loop_top_level);
108 }
109 
111 {
112  source_location.remove(ID_loop_id);
113  source_location.remove(ID_loop_head);
114  source_location.remove(ID_loop_body);
115  source_location.remove(ID_loop_exiting);
116  source_location.remove(ID_loop_latch);
117  source_location.remove(ID_loop_top_level);
118 }
119 
121 {
122  dfcc_remove_loop_tags(target->source_location_nonconst());
123 }
124 
126 {
127  for(auto target = goto_program.instructions.begin();
128  target != goto_program.instructions.end();
129  target++)
130  {
131  dfcc_remove_loop_tags(target);
132  }
133 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:382
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:381
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::iterator targett
Definition: goto_program.h:614
void remove(const irep_idt &name)
Definition: irep.cpp:87
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
const irep_idt ID_loop_top_level
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)
static void dfcc_set_loop_tag(goto_programt::instructiont::targett &target, const irep_idt &tag)
const irep_idt ID_loop_id
const irep_idt ID_loop_latch
bool dfcc_is_loop_latch(const goto_programt::instructiont::const_targett &target)
const irep_idt ID_loop_body
void dfcc_remove_loop_tags(source_locationt &source_location)
const irep_idt ID_loop_exiting
bool dfcc_is_loop_top_level(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
static bool has_loop_tag(const goto_programt::instructiont::const_targett &target, const irep_idt &tag)
void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
std::optional< std::size_t > dfcc_get_loop_id(const goto_programt::instructiont::const_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)
const irep_idt ID_loop_head
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,...