CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_is_cprover_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: March 2023
8
9\*******************************************************************/
10
11#include "dfcc_is_cprover_symbol.h"
12
13#include <util/cprover_prefix.h>
14#include <util/prefix.h>
15#include <util/suffix.h>
16
17#include <unordered_set>
18
19static void
20init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
21{
22 // the set of all CPROVER symbols that we know of
23 if(function_symbols.empty())
24 {
25 function_symbols.insert(CPROVER_PREFIX "_start");
26 function_symbols.insert(CPROVER_PREFIX "allocated_memory");
27 function_symbols.insert(CPROVER_PREFIX "array_copy");
28 function_symbols.insert(CPROVER_PREFIX "array_replace");
29 function_symbols.insert(CPROVER_PREFIX "array_set");
30 function_symbols.insert(CPROVER_PREFIX "assert");
31 function_symbols.insert(CPROVER_PREFIX "assignable");
32 function_symbols.insert(CPROVER_PREFIX "assume");
33 function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_init");
34 function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_reset");
35 function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
36 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
37 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
38 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert");
39 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove");
40 function_symbols.insert(
41 CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
42 function_symbols.insert(CPROVER_PREFIX "contracts_free");
43 function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable");
44 function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
45 function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
46 function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
47 function_symbols.insert(CPROVER_PREFIX "contracts_link_ptr_pred_ctx");
48 function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
49 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
50 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
51 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact");
52 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains");
53 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append");
54 function_symbols.insert(CPROVER_PREFIX
55 "contracts_obj_set_create_indexed_by_object_id");
56 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
57 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
58 function_symbols.insert(CPROVER_PREFIX "contracts_pointer_equals");
59 function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
60 function_symbols.insert(CPROVER_PREFIX "contracts_was_freed");
61 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated");
62 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl");
63 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable");
64 function_symbols.insert(
65 CPROVER_PREFIX
66 "contracts_write_set_check_allocated_deallocated_is_empty");
67 function_symbols.insert(CPROVER_PREFIX
68 "contracts_write_set_check_array_copy");
69 function_symbols.insert(CPROVER_PREFIX
70 "contracts_write_set_check_array_replace");
71 function_symbols.insert(CPROVER_PREFIX
72 "contracts_write_set_check_array_set");
73 function_symbols.insert(CPROVER_PREFIX
74 "contracts_write_set_check_assignment");
75 function_symbols.insert(
76 CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
77 function_symbols.insert(CPROVER_PREFIX
78 "contracts_write_set_check_deallocate");
79 function_symbols.insert(CPROVER_PREFIX
80 "contracts_write_set_check_frees_clause_inclusion");
81 function_symbols.insert(CPROVER_PREFIX
82 "contracts_write_set_check_havoc_object");
83 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create");
84 function_symbols.insert(CPROVER_PREFIX
85 "contracts_write_set_deallocate_freeable");
86 function_symbols.insert(CPROVER_PREFIX
87 "contracts_write_set_havoc_get_assignable_target");
88 function_symbols.insert(CPROVER_PREFIX
89 "contracts_write_set_havoc_object_whole");
90 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice");
91 function_symbols.insert(CPROVER_PREFIX
92 "contracts_write_set_insert_assignable");
93 function_symbols.insert(CPROVER_PREFIX
94 "contracts_write_set_insert_object_from");
95 function_symbols.insert(CPROVER_PREFIX
96 "contracts_write_set_insert_object_upto");
97 function_symbols.insert(CPROVER_PREFIX
98 "contracts_write_set_insert_object_whole");
99 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead");
100 function_symbols.insert(CPROVER_PREFIX
101 "contracts_write_set_record_deallocated");
102 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release");
103 function_symbols.insert(CPROVER_PREFIX "deallocate");
104 function_symbols.insert(CPROVER_PREFIX "freeable");
105 function_symbols.insert(CPROVER_PREFIX "havoc_object");
106 function_symbols.insert(CPROVER_PREFIX "havoc_slice");
107 function_symbols.insert(CPROVER_PREFIX "initialize");
108 function_symbols.insert(CPROVER_PREFIX "is_freeable");
109 function_symbols.insert(CPROVER_PREFIX "is_fresh");
110 function_symbols.insert(CPROVER_PREFIX "obeys_contract");
111 function_symbols.insert(CPROVER_PREFIX "object_from");
112 function_symbols.insert(CPROVER_PREFIX "object_upto");
113 function_symbols.insert(CPROVER_PREFIX "object_whole");
114 function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc");
115 function_symbols.insert(CPROVER_PREFIX "precondition");
116 function_symbols.insert(CPROVER_PREFIX "printf");
117 function_symbols.insert(CPROVER_PREFIX "was_freed");
118 }
119}
120
121static void init_static_symbols(std::unordered_set<irep_idt> &static_symbols)
122{
123 if(static_symbols.empty())
124 {
125 static_symbols.insert(CPROVER_PREFIX "dead_object");
126 static_symbols.insert(CPROVER_PREFIX "deallocated");
127 static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
128 static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
129 static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
130 static_symbols.insert(CPROVER_PREFIX
131 "malloc_failure_mode_assert_then_assume");
132 static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
133 static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
134 static_symbols.insert(CPROVER_PREFIX "memory_leak");
135 static_symbols.insert(CPROVER_PREFIX "pipe_offset");
136 static_symbols.insert(CPROVER_PREFIX "pipes");
137 static_symbols.insert(CPROVER_PREFIX "rounding_mode");
138 }
139}
140
141bool dfcc_is_cprover_function_symbol(const irep_idt &id)
142{
143 std::unordered_set<irep_idt> function_symbols;
144 init_function_symbols(function_symbols);
145 std::string str = id2string(id);
146 return function_symbols.find(id) != function_symbols.end() ||
147 // nondet functions
148 has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
149}
150
151bool dfcc_is_cprover_static_symbol(const irep_idt &id)
152{
153 std::unordered_set<irep_idt> static_symbols;
154 init_static_symbols(static_symbols);
155 return static_symbols.find(id) != static_symbols.end() ||
156 // auto objects from pointer derefs
157 has_suffix(id2string(id), "$object") ||
158 // going_to variables converted from goto statements
159 has_prefix(id2string(id), CPROVER_PREFIX "going_to");
160}
161
162bool dfcc_is_cprover_pointer_predicate(const irep_idt &id)
163{
164 return id == CPROVER_PREFIX "pointer_equals" ||
165 id == CPROVER_PREFIX "is_fresh" ||
166 id == CPROVER_PREFIX "pointer_in_range_dfcc" ||
167 id == CPROVER_PREFIX "obeys_contract";
168}
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
cprover_prefix.h
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition cprover_prefix.h:14
init_function_symbols
static void init_function_symbols(std::unordered_set< irep_idt > &function_symbols)
Definition dfcc_is_cprover_symbol.cpp:20
dfcc_is_cprover_function_symbol
bool dfcc_is_cprover_function_symbol(const irep_idt &id)
Returns true iff id is one of the known CPROVER functions or starts with __VERIFIER or nondet.
Definition dfcc_is_cprover_symbol.cpp:141
dfcc_is_cprover_pointer_predicate
bool dfcc_is_cprover_pointer_predicate(const irep_idt &id)
Returns true iff the symbol is one of the CPROVER pointer predicates.
Definition dfcc_is_cprover_symbol.cpp:162
dfcc_is_cprover_static_symbol
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
Returns true iff the symbol is one of the known CPROVER static instrumentation variables or ends with...
Definition dfcc_is_cprover_symbol.cpp:151
init_static_symbols
static void init_static_symbols(std::unordered_set< irep_idt > &static_symbols)
Definition dfcc_is_cprover_symbol.cpp:121
dfcc_is_cprover_symbol.h
id2string
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17