Skip to content

Commit 2185dfd

Browse files
author
Remi Delmas
committed
CONTRACTS: loop info tagging utility functions
Utility functions for loop contracts instrumentation, allowing to tag GOTO instructions with loop identifiers and loop instruction type.
1 parent b34e991 commit 2185dfd

File tree

3 files changed

+185
-0
lines changed

3 files changed

+185
-0
lines changed

‎src/goto-instrument/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \
1818
call_sequences.cpp \
1919
contracts/contracts.cpp \
2020
contracts/dynamic-frames/dfcc_utils.cpp \
21+
contracts/dynamic-frames/dfcc_loop_tags.cpp \
2122
contracts/dynamic-frames/dfcc_library.cpp \
2223
contracts/dynamic-frames/dfcc_is_fresh.cpp \
2324
contracts/dynamic-frames/dfcc_pointer_in_range.cpp \

‎src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking
4+
5+
Author: Qinheping Hu, [email protected]
6+
7+
Author: Remi Delmas, [email protected]
8+
9+
Date: March 2023
10+
11+
\*******************************************************************/
12+
13+
#include "dfcc_loop_tags.h"
14+
15+
const irep_idt ID_loop_id = "loop-id";
16+
const irep_idt ID_loop_head = "loop-head";
17+
const irep_idt ID_loop_body = "loop-body";
18+
const irep_idt ID_loop_latch = "loop-latch";
19+
const irep_idt ID_loop_exiting = "loop-exiting";
20+
const irep_idt ID_loop_top_level = "loop-top-level";
21+
22+
void dfcc_set_loop_id(
23+
goto_programt::instructiont::targett &target,
24+
const std::size_t loop_id)
25+
{
26+
target->source_location_nonconst().set(ID_loop_id, loop_id);
27+
}
28+
29+
optionalt<std::size_t>
30+
dfcc_get_loop_id(const goto_programt::instructiont::targett &target)
31+
{
32+
if(target->source_location_nonconst().get(ID_loop_id).empty())
33+
return {};
34+
35+
return target->source_location_nonconst().get_size_t(ID_loop_id);
36+
}
37+
38+
bool dfcc_has_loop_id(
39+
const goto_programt::instructiont::targett &target,
40+
std::size_t loop_id)
41+
{
42+
auto loop_id_opt = dfcc_get_loop_id(target);
43+
return loop_id_opt.has_value() && loop_id_opt.value() == loop_id;
44+
}
45+
46+
static void dfcc_set_loop_tag(
47+
goto_programt::instructiont::targett &target,
48+
const irep_idt &tag)
49+
{
50+
target->source_location_nonconst().set(tag, true);
51+
}
52+
53+
static bool has_loop_tag(
54+
const goto_programt::instructiont::targett &target,
55+
const irep_idt &tag)
56+
{
57+
return target->source_location().get_bool(tag);
58+
}
59+
60+
void dfcc_set_loop_head(goto_programt::instructiont::targett &target)
61+
{
62+
dfcc_set_loop_tag(target, ID_loop_head);
63+
}
64+
65+
bool dfcc_is_loop_head(const goto_programt::instructiont::targett &target)
66+
{
67+
return has_loop_tag(target, ID_loop_head);
68+
}
69+
70+
void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
71+
{
72+
dfcc_set_loop_tag(target, ID_loop_body);
73+
}
74+
75+
bool dfcc_is_loop_body(const goto_programt::instructiont::targett &target)
76+
{
77+
return has_loop_tag(target, ID_loop_body);
78+
}
79+
80+
void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target)
81+
{
82+
dfcc_set_loop_tag(target, ID_loop_exiting);
83+
}
84+
85+
bool dfcc_is_loop_exiting(const goto_programt::instructiont::targett &target)
86+
{
87+
return has_loop_tag(target, ID_loop_exiting);
88+
}
89+
90+
void dfcc_set_loop_latch(goto_programt::instructiont::targett &target)
91+
{
92+
dfcc_set_loop_tag(target, ID_loop_latch);
93+
}
94+
95+
bool dfcc_is_loop_latch(const goto_programt::instructiont::targett &target)
96+
{
97+
return has_loop_tag(target, ID_loop_latch);
98+
}
99+
100+
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
101+
{
102+
dfcc_set_loop_tag(target, ID_loop_top_level);
103+
}
104+
105+
bool dfcc_is_loop_top_level(const goto_programt::instructiont::targett &target)
106+
{
107+
return has_loop_tag(target, ID_loop_top_level);
108+
}
109+
110+
void dfcc_remove_loop_tags(source_locationt &source_location)
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+
120+
void dfcc_remove_loop_tags(goto_programt::targett &target)
121+
{
122+
dfcc_remove_loop_tags(target->source_location_nonconst());
123+
}
124+
125+
void dfcc_remove_loop_tags(goto_programt &goto_program)
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+
}

‎src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
/*******************************************************************\
2+
3+
Module: Dynamic frame condition checking
4+
5+
Author: Qinheping Hu, [email protected]
6+
7+
Author: Remi Delmas, [email protected]
8+
9+
Date: March 2023
10+
11+
\*******************************************************************/
12+
13+
/// \file
14+
/// Functions that allow to tag GOTO instructions with loop identifiers and
15+
/// loop instruction type: head, body, exiting, latch.
16+
17+
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
18+
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
19+
20+
#include <goto-programs/goto_program.h>
21+
22+
void dfcc_set_loop_id(
23+
goto_programt::instructiont::targett &target,
24+
std::size_t loop_id);
25+
26+
bool dfcc_has_loop_id(
27+
const goto_programt::instructiont::targett &target,
28+
std::size_t loop_id);
29+
30+
optionalt<std::size_t>
31+
dfcc_get_loop_id(const goto_programt::instructiont::targett &target);
32+
33+
void dfcc_set_loop_head(goto_programt::instructiont::targett &target);
34+
bool dfcc_is_loop_head(const goto_programt::instructiont::targett &target);
35+
36+
void dfcc_set_loop_body(goto_programt::instructiont::targett &target);
37+
bool dfcc_is_loop_body(const goto_programt::instructiont::targett &target);
38+
39+
void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target);
40+
bool dfcc_is_loop_exiting(const goto_programt::instructiont::targett &target);
41+
42+
void dfcc_set_loop_latch(goto_programt::instructiont::targett &target);
43+
bool dfcc_is_loop_latch(const goto_programt::instructiont::targett &target);
44+
45+
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target);
46+
bool dfcc_is_loop_top_level(const goto_programt::instructiont::targett &target);
47+
48+
void dfcc_remove_loop_tags(source_locationt &source_location);
49+
void dfcc_remove_loop_tags(goto_programt &goto_program);
50+
void dfcc_remove_loop_tags(goto_programt::targett &target);
51+
#endif

0 commit comments

Comments
 (0)