Skip to content

Commit 44a112f

Browse files
author
Remi Delmas
committed
CONTRACTS: dfcc_libraryt remove global objects
1 parent c24b008 commit 44a112f

File tree

2 files changed

+162
-151
lines changed

2 files changed

+162
-151
lines changed

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

Lines changed: 140 additions & 151 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,140 @@ Author: Remi Delmas, [email protected]
3030

3131
#include "dfcc_utils.h"
3232

33+
/// Swaps keys and values in a map
34+
template <typename K, typename V>
35+
std::map<V, K> swap_map(std::map<K, V> const &map)
36+
{
37+
std::map<V, K> result;
38+
for(auto const &pair : map)
39+
result.insert({pair.second, pair.first});
40+
return result;
41+
}
42+
3343
// NOLINTNEXTLINE(build/deprecated)
3444
#define CONTRACTS_PREFIX CPROVER_PREFIX "contracts_"
3545

46+
/// Creates the enum to type name mapping
47+
const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name()
48+
{
49+
return std::map<dfcc_typet, irep_idt>{
50+
{dfcc_typet::CAR, CONTRACTS_PREFIX "car_t"},
51+
{dfcc_typet::CAR_SET, CONTRACTS_PREFIX "car_set_t"},
52+
{dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"},
53+
{dfcc_typet::OBJ_SET, CONTRACTS_PREFIX "obj_set_t"},
54+
{dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"},
55+
{dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"},
56+
{dfcc_typet::WRITE_SET_PTR, CONTRACTS_PREFIX "write_set_ptr_t"}};
57+
}
58+
59+
const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
60+
{
61+
return {
62+
{dfcc_funt::CAR_CREATE, CONTRACTS_PREFIX "car_create"},
63+
{dfcc_funt::CAR_SET_CREATE, CONTRACTS_PREFIX "car_set_create"},
64+
{dfcc_funt::CAR_SET_INSERT, CONTRACTS_PREFIX "car_set_insert"},
65+
{dfcc_funt::CAR_SET_REMOVE, CONTRACTS_PREFIX "car_set_remove"},
66+
{dfcc_funt::CAR_SET_CONTAINS, CONTRACTS_PREFIX "car_set_contains"},
67+
{dfcc_funt::OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID,
68+
CONTRACTS_PREFIX "obj_set_create_indexed_by_object_id"},
69+
{dfcc_funt::OBJ_SET_CREATE_APPEND,
70+
CONTRACTS_PREFIX "obj_set_create_append"},
71+
{dfcc_funt::OBJ_SET_RELEASE, CONTRACTS_PREFIX "obj_set_release"},
72+
{dfcc_funt::OBJ_SET_ADD, CONTRACTS_PREFIX "obj_set_add"},
73+
{dfcc_funt::OBJ_SET_APPEND, CONTRACTS_PREFIX "obj_set_append"},
74+
{dfcc_funt::OBJ_SET_REMOVE, CONTRACTS_PREFIX "obj_set_remove"},
75+
{dfcc_funt::OBJ_SET_CONTAINS, CONTRACTS_PREFIX "obj_set_contains"},
76+
{dfcc_funt::OBJ_SET_CONTAINS_EXACT,
77+
CONTRACTS_PREFIX "obj_set_contains_exact"},
78+
{dfcc_funt::WRITE_SET_CREATE, CONTRACTS_PREFIX "write_set_create"},
79+
{dfcc_funt::WRITE_SET_RELEASE, CONTRACTS_PREFIX "write_set_release"},
80+
{dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE,
81+
CONTRACTS_PREFIX "write_set_insert_assignable"},
82+
{dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE,
83+
CONTRACTS_PREFIX "write_set_insert_object_whole"},
84+
{dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM,
85+
CONTRACTS_PREFIX "write_set_insert_object_from"},
86+
{dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO,
87+
CONTRACTS_PREFIX "write_set_insert_object_upto"},
88+
{dfcc_funt::WRITE_SET_ADD_FREEABLE,
89+
CONTRACTS_PREFIX "write_set_add_freeable"},
90+
{dfcc_funt::WRITE_SET_ADD_ALLOCATED,
91+
CONTRACTS_PREFIX "write_set_add_allocated"},
92+
{dfcc_funt::WRITE_SET_RECORD_DEAD,
93+
CONTRACTS_PREFIX "write_set_record_dead"},
94+
{dfcc_funt::WRITE_SET_RECORD_DEALLOCATED,
95+
CONTRACTS_PREFIX "write_set_record_deallocated"},
96+
{dfcc_funt::WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY,
97+
CONTRACTS_PREFIX "write_set_check_allocated_deallocated_is_empty"},
98+
{dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT,
99+
CONTRACTS_PREFIX "write_set_check_assignment"},
100+
{dfcc_funt::WRITE_SET_CHECK_ARRAY_SET,
101+
CONTRACTS_PREFIX "write_set_check_array_set"},
102+
{dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY,
103+
CONTRACTS_PREFIX "write_set_check_array_copy"},
104+
{dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE,
105+
CONTRACTS_PREFIX "write_set_check_array_replace"},
106+
{dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT,
107+
CONTRACTS_PREFIX "write_set_check_havoc_object"},
108+
{dfcc_funt::WRITE_SET_CHECK_DEALLOCATE,
109+
CONTRACTS_PREFIX "write_set_check_deallocate"},
110+
{dfcc_funt::WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION,
111+
CONTRACTS_PREFIX "write_set_check_assigns_clause_inclusion"},
112+
{dfcc_funt::WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION,
113+
CONTRACTS_PREFIX "write_set_check_frees_clause_inclusion"},
114+
{dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE,
115+
CONTRACTS_PREFIX "write_set_deallocate_freeable"},
116+
{dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET,
117+
CONTRACTS_PREFIX "write_set_havoc_get_assignable_target"},
118+
{dfcc_funt::WRITE_SET_HAVOC_OBJECT_WHOLE,
119+
CONTRACTS_PREFIX "write_set_havoc_object_whole"},
120+
{dfcc_funt::WRITE_SET_HAVOC_SLICE,
121+
CONTRACTS_PREFIX "write_set_havoc_slice"},
122+
{dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"},
123+
{dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"},
124+
{dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"},
125+
{dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"},
126+
{dfcc_funt::IS_FREEABLE, CONTRACTS_PREFIX "is_freeable"},
127+
{dfcc_funt::WAS_FREED, CONTRACTS_PREFIX "was_freed"},
128+
{dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS,
129+
CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"}};
130+
}
131+
132+
const std::map<irep_idt, dfcc_funt> create_dfcc_hook()
133+
{
134+
return {
135+
{CPROVER_PREFIX "assignable", dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE},
136+
{CPROVER_PREFIX "object_whole", dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE},
137+
{CPROVER_PREFIX "object_from", dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM},
138+
{CPROVER_PREFIX "object_upto", dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO},
139+
{CPROVER_PREFIX "freeable", dfcc_funt::WRITE_SET_ADD_FREEABLE}};
140+
}
141+
142+
const std::map<irep_idt, dfcc_funt> create_havoc_hook()
143+
{
144+
return {
145+
{CPROVER_PREFIX "assignable",
146+
dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET},
147+
{CPROVER_PREFIX "object_whole", dfcc_funt::WRITE_SET_HAVOC_OBJECT_WHOLE},
148+
{CPROVER_PREFIX "object_from", dfcc_funt::WRITE_SET_HAVOC_SLICE},
149+
{CPROVER_PREFIX "object_upto", dfcc_funt::WRITE_SET_HAVOC_SLICE}};
150+
}
151+
152+
const std::set<irep_idt> create_assignable_builtin_names()
153+
{
154+
return {
155+
CPROVER_PREFIX "assignable",
156+
CPROVER_PREFIX "assignable_set_insert_assignable",
157+
CPROVER_PREFIX "object_whole",
158+
CPROVER_PREFIX "assignable_set_insert_object_whole",
159+
CPROVER_PREFIX "object_from",
160+
CPROVER_PREFIX "assignable_set_insert_object_from",
161+
CPROVER_PREFIX "object_upto",
162+
CPROVER_PREFIX "assignable_set_insert_object_upto",
163+
CPROVER_PREFIX "freeable",
164+
CPROVER_PREFIX "assignable_set_add_freeable"};
165+
}
166+
36167
/// Class constructor
37168
dfcc_libraryt::dfcc_libraryt(
38169
goto_modelt &goto_model,
@@ -41,138 +172,17 @@ dfcc_libraryt::dfcc_libraryt(
41172
: goto_model(goto_model),
42173
utils(utils),
43174
log(log),
44-
message_handler(log.get_message_handler())
175+
message_handler(log.get_message_handler()),
176+
dfcc_type_to_name(create_dfcc_type_to_name()),
177+
dfcc_name_to_type(swap_map<dfcc_typet, irep_idt>(dfcc_type_to_name)),
178+
dfcc_fun_to_name(create_dfcc_fun_to_name()),
179+
dfcc_name_to_fun(swap_map<dfcc_funt, irep_idt>(dfcc_fun_to_name)),
180+
dfcc_hook(create_dfcc_hook()),
181+
havoc_hook(create_havoc_hook()),
182+
assignable_builtin_names(create_assignable_builtin_names())
45183
{
46184
}
47185

48-
/// Swaps keys and values in a map
49-
template <typename K, typename V>
50-
std::map<V, K> swap_map(std::map<K, V> const &map)
51-
{
52-
std::map<V, K> result;
53-
for(auto const &pair : map)
54-
result.insert({pair.second, pair.first});
55-
return result;
56-
}
57-
58-
/// enum to type name mapping
59-
static const std::map<dfcc_typet, irep_idt> dfcc_type_to_name = {
60-
{dfcc_typet::CAR, CONTRACTS_PREFIX "car_t"},
61-
{dfcc_typet::CAR_SET, CONTRACTS_PREFIX "car_set_t"},
62-
{dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"},
63-
{dfcc_typet::OBJ_SET, CONTRACTS_PREFIX "obj_set_t"},
64-
{dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"},
65-
{dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"},
66-
{dfcc_typet::WRITE_SET_PTR, CONTRACTS_PREFIX "write_set_ptr_t"}};
67-
68-
/// Swapped dfcc_type_to_name
69-
static const std::map<irep_idt, dfcc_typet>
70-
dfcc_name_to_type(swap_map<dfcc_typet, irep_idt>(dfcc_type_to_name));
71-
72-
/// enum to function name mapping
73-
static const std::map<dfcc_funt, irep_idt> dfcc_fun_to_name = {
74-
// clang-format off
75-
{dfcc_funt::CAR_CREATE,
76-
CONTRACTS_PREFIX "car_create"},
77-
{dfcc_funt::CAR_SET_CREATE,
78-
CONTRACTS_PREFIX "car_set_create"},
79-
{dfcc_funt::CAR_SET_INSERT,
80-
CONTRACTS_PREFIX "car_set_insert"},
81-
{dfcc_funt::CAR_SET_REMOVE,
82-
CONTRACTS_PREFIX "car_set_remove"},
83-
{dfcc_funt::CAR_SET_CONTAINS,
84-
CONTRACTS_PREFIX "car_set_contains"},
85-
{dfcc_funt::OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID,
86-
CONTRACTS_PREFIX "obj_set_create_indexed_by_object_id"},
87-
{dfcc_funt::OBJ_SET_CREATE_APPEND,
88-
CONTRACTS_PREFIX "obj_set_create_append"},
89-
{dfcc_funt::OBJ_SET_RELEASE,
90-
CONTRACTS_PREFIX "obj_set_release"},
91-
{dfcc_funt::OBJ_SET_ADD,
92-
CONTRACTS_PREFIX "obj_set_add"},
93-
{dfcc_funt::OBJ_SET_APPEND,
94-
CONTRACTS_PREFIX "obj_set_append"},
95-
{dfcc_funt::OBJ_SET_REMOVE,
96-
CONTRACTS_PREFIX "obj_set_remove"},
97-
{dfcc_funt::OBJ_SET_CONTAINS,
98-
CONTRACTS_PREFIX "obj_set_contains"},
99-
{dfcc_funt::OBJ_SET_CONTAINS_EXACT,
100-
CONTRACTS_PREFIX "obj_set_contains_exact"},
101-
{dfcc_funt::WRITE_SET_CREATE,
102-
CONTRACTS_PREFIX "write_set_create"},
103-
{dfcc_funt::WRITE_SET_RELEASE,
104-
CONTRACTS_PREFIX "write_set_release"},
105-
{dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE,
106-
CONTRACTS_PREFIX "write_set_insert_assignable"},
107-
{dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE,
108-
CONTRACTS_PREFIX "write_set_insert_object_whole"},
109-
{dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM,
110-
CONTRACTS_PREFIX "write_set_insert_object_from"},
111-
{dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO,
112-
CONTRACTS_PREFIX "write_set_insert_object_upto"},
113-
{dfcc_funt::WRITE_SET_ADD_FREEABLE,
114-
CONTRACTS_PREFIX "write_set_add_freeable"},
115-
{dfcc_funt::WRITE_SET_ADD_ALLOCATED,
116-
CONTRACTS_PREFIX "write_set_add_allocated"},
117-
{dfcc_funt::WRITE_SET_RECORD_DEAD,
118-
CONTRACTS_PREFIX "write_set_record_dead"},
119-
{dfcc_funt::WRITE_SET_RECORD_DEALLOCATED,
120-
CONTRACTS_PREFIX "write_set_record_deallocated"},
121-
{dfcc_funt::WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY,
122-
CONTRACTS_PREFIX "write_set_check_allocated_deallocated_is_empty"},
123-
{dfcc_funt::WRITE_SET_CHECK_ASSIGNMENT,
124-
CONTRACTS_PREFIX "write_set_check_assignment"},
125-
{dfcc_funt::WRITE_SET_CHECK_ARRAY_SET,
126-
CONTRACTS_PREFIX "write_set_check_array_set"},
127-
{dfcc_funt::WRITE_SET_CHECK_ARRAY_COPY,
128-
CONTRACTS_PREFIX "write_set_check_array_copy"},
129-
{dfcc_funt::WRITE_SET_CHECK_ARRAY_REPLACE,
130-
CONTRACTS_PREFIX "write_set_check_array_replace"},
131-
{dfcc_funt::WRITE_SET_CHECK_HAVOC_OBJECT,
132-
CONTRACTS_PREFIX "write_set_check_havoc_object"},
133-
{dfcc_funt::WRITE_SET_CHECK_DEALLOCATE,
134-
CONTRACTS_PREFIX "write_set_check_deallocate"},
135-
{dfcc_funt::WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION,
136-
CONTRACTS_PREFIX "write_set_check_assigns_clause_inclusion"},
137-
{dfcc_funt::WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION,
138-
CONTRACTS_PREFIX "write_set_check_frees_clause_inclusion"},
139-
{dfcc_funt::WRITE_SET_DEALLOCATE_FREEABLE,
140-
CONTRACTS_PREFIX "write_set_deallocate_freeable"},
141-
{dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET,
142-
CONTRACTS_PREFIX "write_set_havoc_get_assignable_target"},
143-
{dfcc_funt::WRITE_SET_HAVOC_OBJECT_WHOLE,
144-
CONTRACTS_PREFIX "write_set_havoc_object_whole"},
145-
{dfcc_funt::WRITE_SET_HAVOC_SLICE,
146-
CONTRACTS_PREFIX "write_set_havoc_slice"},
147-
{dfcc_funt::LINK_IS_FRESH,
148-
CONTRACTS_PREFIX "link_is_fresh"},
149-
{dfcc_funt::LINK_ALLOCATED,
150-
CONTRACTS_PREFIX "link_allocated"},
151-
{dfcc_funt::LINK_DEALLOCATED,
152-
CONTRACTS_PREFIX "link_deallocated"},
153-
{dfcc_funt::IS_FRESH,
154-
CONTRACTS_PREFIX "is_fresh"},
155-
{dfcc_funt::IS_FREEABLE,
156-
CONTRACTS_PREFIX "is_freeable"},
157-
{dfcc_funt::WAS_FREED,
158-
CONTRACTS_PREFIX "was_freed"},
159-
{dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS,
160-
CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"}
161-
// clang-format on
162-
};
163-
164-
// Swapped dfcc_fun_to_name
165-
static const std::map<irep_idt, dfcc_funt>
166-
dfcc_name_to_fun(swap_map<dfcc_funt, irep_idt>(dfcc_fun_to_name));
167-
168-
/// Maps built-in function names to enums to use for instrumentation
169-
static const std::map<irep_idt, dfcc_funt> dfcc_hook = {
170-
{CPROVER_PREFIX "assignable", dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE},
171-
{CPROVER_PREFIX "object_whole", dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE},
172-
{CPROVER_PREFIX "object_from", dfcc_funt::WRITE_SET_INSERT_OBJECT_FROM},
173-
{CPROVER_PREFIX "object_upto", dfcc_funt::WRITE_SET_INSERT_OBJECT_UPTO},
174-
{CPROVER_PREFIX "freeable", dfcc_funt::WRITE_SET_ADD_FREEABLE}};
175-
176186
/// Returns the instrumentation function to use for a given front-end function
177187
optionalt<dfcc_funt> dfcc_libraryt::get_hook(const irep_idt &function_id) const
178188
{
@@ -183,15 +193,7 @@ optionalt<dfcc_funt> dfcc_libraryt::get_hook(const irep_idt &function_id) const
183193
return {};
184194
}
185195

186-
/// Maps front-end functions to library functions giving their havoc semantics
187-
static const std::map<irep_idt, dfcc_funt> havoc_hook = {
188-
{CPROVER_PREFIX "assignable",
189-
dfcc_funt::WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET},
190-
{CPROVER_PREFIX "object_whole", dfcc_funt::WRITE_SET_HAVOC_OBJECT_WHOLE},
191-
{CPROVER_PREFIX "object_from", dfcc_funt::WRITE_SET_HAVOC_SLICE},
192-
{CPROVER_PREFIX "object_upto", dfcc_funt::WRITE_SET_HAVOC_SLICE}};
193-
194-
/// Returns the havoc function to use for a given front-end function
196+
// Returns the havoc function to use for a given front-end function
195197
optionalt<dfcc_funt>
196198
dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
197199
{
@@ -202,19 +204,6 @@ dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
202204
return {};
203205
}
204206

205-
/// All built-in function names (front-end and instrumentation hooks)
206-
static const std::set<irep_idt> assignable_builtin_names = {
207-
CPROVER_PREFIX "assignable",
208-
CPROVER_PREFIX "assignable_set_insert_assignable",
209-
CPROVER_PREFIX "object_whole",
210-
CPROVER_PREFIX "assignable_set_insert_object_whole",
211-
CPROVER_PREFIX "object_from",
212-
CPROVER_PREFIX "assignable_set_insert_object_from",
213-
CPROVER_PREFIX "object_upto",
214-
CPROVER_PREFIX "assignable_set_insert_object_upto",
215-
CPROVER_PREFIX "freeable",
216-
CPROVER_PREFIX "assignable_set_add_freeable"};
217-
218207
void dfcc_libraryt::get_missing_funs(std::set<irep_idt> &missing)
219208
{
220209
missing.clear();

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,28 @@ class dfcc_libraryt
180180
/// Change calls to `__CPROVER_contracts_free` into calls to `free`
181181
void fix_malloc_free_calls();
182182

183+
private:
184+
/// Enum to type name mapping
185+
const std::map<dfcc_typet, irep_idt> dfcc_type_to_name;
186+
187+
/// Swapped dfcc_type_to_name
188+
const std::map<irep_idt, dfcc_typet> dfcc_name_to_type;
189+
190+
/// enum to function name mapping
191+
const std::map<dfcc_funt, irep_idt> dfcc_fun_to_name;
192+
193+
// Swapped dfcc_fun_to_name
194+
const std::map<irep_idt, dfcc_funt> dfcc_name_to_fun;
195+
196+
/// Maps built-in function names to enums to use for instrumentation
197+
const std::map<irep_idt, dfcc_funt> dfcc_hook;
198+
199+
/// Maps front-end functions to library functions giving their havoc semantics
200+
const std::map<irep_idt, dfcc_funt> havoc_hook;
201+
202+
/// All built-in function names (front-end and instrumentation hooks)
203+
const std::set<irep_idt> assignable_builtin_names;
204+
183205
public:
184206
/// Maps enum values to the actual types (dynamically loaded)
185207
std::map<dfcc_typet, typet> dfcc_type;

0 commit comments

Comments
 (0)