cprover
Loading...
Searching...
No Matches
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
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_car_create");
34 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
35 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
36 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_insert");
37 function_symbols.insert(CPROVER_PREFIX "contracts_car_set_remove");
38 function_symbols.insert(
39 CPROVER_PREFIX "contracts_check_replace_ensures_was_freed_preconditions");
40 function_symbols.insert(CPROVER_PREFIX "contracts_free");
41 function_symbols.insert(CPROVER_PREFIX "contracts_is_freeable");
42 function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
43 function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
44 function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
45 function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
46 function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
47 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
48 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
49 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains_exact");
50 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_contains");
51 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_create_append");
52 function_symbols.insert(CPROVER_PREFIX
53 "contracts_obj_set_create_indexed_by_object_id");
54 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
55 function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
56 function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");
57 function_symbols.insert(CPROVER_PREFIX "contracts_was_freed");
58 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated");
59 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_decl");
60 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_freeable");
61 function_symbols.insert(
63 "contracts_write_set_check_allocated_deallocated_is_empty");
64 function_symbols.insert(CPROVER_PREFIX
65 "contracts_write_set_check_array_copy");
66 function_symbols.insert(CPROVER_PREFIX
67 "contracts_write_set_check_array_replace");
68 function_symbols.insert(CPROVER_PREFIX
69 "contracts_write_set_check_array_set");
70 function_symbols.insert(CPROVER_PREFIX
71 "contracts_write_set_check_assignment");
72 function_symbols.insert(
73 CPROVER_PREFIX "contracts_write_set_check_assigns_clause_inclusion");
74 function_symbols.insert(CPROVER_PREFIX
75 "contracts_write_set_check_deallocate");
76 function_symbols.insert(CPROVER_PREFIX
77 "contracts_write_set_check_frees_clause_inclusion");
78 function_symbols.insert(CPROVER_PREFIX
79 "contracts_write_set_check_havoc_object");
80 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_create");
81 function_symbols.insert(CPROVER_PREFIX
82 "contracts_write_set_deallocate_freeable");
83 function_symbols.insert(CPROVER_PREFIX
84 "contracts_write_set_havoc_get_assignable_target");
85 function_symbols.insert(CPROVER_PREFIX
86 "contracts_write_set_havoc_object_whole");
87 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_havoc_slice");
88 function_symbols.insert(CPROVER_PREFIX
89 "contracts_write_set_insert_assignable");
90 function_symbols.insert(CPROVER_PREFIX
91 "contracts_write_set_insert_object_from");
92 function_symbols.insert(CPROVER_PREFIX
93 "contracts_write_set_insert_object_upto");
94 function_symbols.insert(CPROVER_PREFIX
95 "contracts_write_set_insert_object_whole");
96 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_record_dead");
97 function_symbols.insert(CPROVER_PREFIX
98 "contracts_write_set_record_deallocated");
99 function_symbols.insert(CPROVER_PREFIX "contracts_write_set_release");
100 function_symbols.insert(CPROVER_PREFIX "deallocate");
101 function_symbols.insert(CPROVER_PREFIX "freeable");
102 function_symbols.insert(CPROVER_PREFIX "havoc_object");
103 function_symbols.insert(CPROVER_PREFIX "havoc_slice");
104 function_symbols.insert(CPROVER_PREFIX "initialize");
105 function_symbols.insert(CPROVER_PREFIX "is_freeable");
106 function_symbols.insert(CPROVER_PREFIX "is_fresh");
107 function_symbols.insert(CPROVER_PREFIX "obeys_contract");
108 function_symbols.insert(CPROVER_PREFIX "object_from");
109 function_symbols.insert(CPROVER_PREFIX "object_upto");
110 function_symbols.insert(CPROVER_PREFIX "object_whole");
111 function_symbols.insert(CPROVER_PREFIX "pointer_in_range_dfcc");
112 function_symbols.insert(CPROVER_PREFIX "precondition");
113 function_symbols.insert(CPROVER_PREFIX "printf");
114 function_symbols.insert(CPROVER_PREFIX "was_freed");
115 }
116}
117
118static void init_static_symbols(std::unordered_set<irep_idt> &static_symbols)
119{
120 if(static_symbols.empty())
121 {
122 static_symbols.insert(CPROVER_PREFIX "dead_object");
123 static_symbols.insert(CPROVER_PREFIX "deallocated");
124 static_symbols.insert(CPROVER_PREFIX "fpu_control_word");
125 static_symbols.insert(CPROVER_PREFIX "jsa_jump_buffer");
126 static_symbols.insert(CPROVER_PREFIX "malloc_failure_mode_return_null");
127 static_symbols.insert(CPROVER_PREFIX
128 "malloc_failure_mode_assert_then_assume");
129 static_symbols.insert(CPROVER_PREFIX "malloc_is_new_array");
130 static_symbols.insert(CPROVER_PREFIX "max_malloc_size");
131 static_symbols.insert(CPROVER_PREFIX "memory_leak");
132 static_symbols.insert(CPROVER_PREFIX "pipe_offset");
133 static_symbols.insert(CPROVER_PREFIX "pipes");
134 static_symbols.insert(CPROVER_PREFIX "rounding_mode");
135 }
136}
137
139{
140 std::unordered_set<irep_idt> function_symbols;
141 init_function_symbols(function_symbols);
142 std::string str = id2string(id);
143 return function_symbols.find(id) != function_symbols.end() ||
144 // nondet functions
145 has_prefix(str, "__VERIFIER") || has_prefix(str, "nondet");
146}
147
149{
150 std::unordered_set<irep_idt> static_symbols;
151 init_static_symbols(static_symbols);
152 return static_symbols.find(id) != static_symbols.end() ||
153 // auto objects from pointer derefs
154 has_suffix(id2string(id), "$object") ||
155 // going_to variables converted from goto statements
156 has_prefix(id2string(id), CPROVER_PREFIX "going_to");
157}
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
static void init_function_symbols(std::unordered_set< irep_idt > &function_symbols)
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.
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...
static void init_static_symbols(std::unordered_set< irep_idt > &static_symbols)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
dstringt irep_idt