CBMC
dfcc_is_cprover_symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 Date: 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 
19 static void
20 init_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(
62  CPROVER_PREFIX
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 
118 static 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 
138 bool dfcc_is_cprover_function_symbol(const irep_idt &id)
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 
148 bool dfcc_is_cprover_static_symbol(const irep_idt &id)
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 }
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:138
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:148
init_static_symbols
static void init_static_symbols(std::unordered_set< irep_idt > &static_symbols)
Definition: dfcc_is_cprover_symbol.cpp:118
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