cprover
Loading...
Searching...
No Matches
c_typecheck_shadow_memory_builtin.cpp
Go to the documentation of this file.
1//
2// Author: Enrico Steffinlongo for Diffblue Ltd
3//
4
5#include <util/c_types.h>
6#include <util/config.h>
8#include <util/expr.h>
10
11#include "c_typecheck_base.h"
12#include "expr2c.h"
13
19 const irep_idt &identifier,
20 const namespacet &ns)
21{
22 // Check correct number of arguments
23 if(expr.arguments().size() != 2)
24 {
25 std::ostringstream error_message;
26 error_message << identifier << " takes exactly 2 arguments, but "
27 << expr.arguments().size() << " were provided";
29 error_message.str(), expr.source_location()};
30 }
31
32 const auto &arg1 = expr.arguments()[0];
34 {
35 // Can't declare a shadow memory field that has a name that is not a
36 // constant string
37 std::ostringstream error_message;
38 error_message << identifier
39 << " argument 1 must be string constant (literal), but ("
40 << expr2c(arg1, ns) << ") has type `"
41 << type2c(arg1.type(), ns) << '`';
43 error_message.str(), expr.source_location()};
44 }
45
46 // The second argument type must be either a boolean or a bitvector of size
47 // less or equal to the size of a char.
48 const auto &arg2 = expr.arguments()[1];
49 const auto &arg2_type = arg2.type();
50 const auto arg2_type_as_bv =
52 if(
53 (!arg2_type_as_bv ||
54 arg2_type_as_bv->get_width() > config.ansi_c.char_width) &&
55 !can_cast_type<bool_typet>(arg2_type))
56 {
57 // Can't declare a shadow memory field with a non-boolean and non bitvector
58 // type or with a bitvector type greater than 8 bit.
59 std::ostringstream error_message;
60 error_message << identifier
61 << " argument 2 must be a byte-sized integer, but ("
62 << expr2c(arg2, ns) << ") has type `" << type2c(arg2_type, ns)
63 << '`';
65 error_message.str(), expr.source_location()};
66 }
67
68 // The function type is just an ellipsis, otherwise the non-ellipsis arguments
69 // will be typechecked and implicitly casted.
70 code_typet t({}, void_type());
71 t.make_ellipsis();
72
73 // Create the symbol with the right type.
74 symbol_exprt result(identifier, std::move(t));
75 result.add_source_location() = expr.source_location();
76 return result;
77}
78
84 const irep_idt &identifier,
85 const namespacet &ns)
86{
87 // Check correct number of arguments
88 if(expr.arguments().size() != 2)
89 {
90 std::ostringstream error_message;
91 error_message << identifier << " takes exactly 2 arguments, but "
92 << expr.arguments().size() << " were provided";
94 error_message.str(), expr.source_location()};
95 }
96
97 const auto &arg1 = expr.arguments()[0];
98 const auto arg1_type_as_ptr =
100 if(
101 !arg1_type_as_ptr || !arg1_type_as_ptr->has_subtype() ||
102 to_type_with_subtype(*arg1_type_as_ptr).subtype() == empty_typet{})
103 {
104 // Can't get the shadow memory value of anything other than a non-void
105 // pointer
106 std::ostringstream error_message;
107 error_message << identifier
108 << " argument 1 must be a non-void pointer, but ("
109 << expr2c(arg1, ns) << ") has type `"
110 << type2c(arg1.type(), ns)
111 << "`. Insert a cast to the type that you want to access.";
113 error_message.str(), expr.source_location()};
114 }
115
116 const auto &arg2 = expr.arguments()[1];
118 {
119 // Can't get value from a shadow memory field that has a name that is
120 // not a constant string
121 std::ostringstream error_message;
122 error_message << identifier
123 << " argument 2 must be string constant (literal), but ("
124 << expr2c(arg2, ns) << ") has type `"
125 << type2c(arg2.type(), ns) << '`';
127 error_message.str(), expr.source_location()};
128 }
129
130 // The function type is just an ellipsis, otherwise the non-ellipsis arguments
131 // will be typechecked and implicitly casted.
132 // Setting the return type to `signed_int_type` otherwise it was creating
133 // problem with signed-unsigned char comparison. Having `signed_int_type`
134 // seems to fix the issue as it contains more bits for the conversion.
136 t.make_ellipsis();
137
138 // Create the symbol with the right type.
139 symbol_exprt result(identifier, std::move(t));
140 result.add_source_location() = expr.source_location();
141 return result;
142}
143
149 const irep_idt &identifier,
150 const namespacet &ns)
151{
152 // Check correct number of arguments
153 if(expr.arguments().size() != 3)
154 {
155 std::ostringstream error_message;
156 error_message << identifier << " takes exactly 3 arguments, but "
157 << expr.arguments().size() << " were provided";
159 error_message.str(), expr.source_location()};
160 }
161
162 const auto &arg1 = expr.arguments()[0];
163 const auto arg1_type_as_ptr =
165 if(
166 !arg1_type_as_ptr || !arg1_type_as_ptr->has_subtype() ||
167 to_type_with_subtype(*arg1_type_as_ptr).subtype() == empty_typet{})
168 {
169 // Can't set the shadow memory value of anything other than a non-void
170 // pointer
171 std::ostringstream error_message;
172 error_message << identifier
173 << " argument 1 must be a non-void pointer, but ("
174 << expr2c(arg1, ns) << ") has type `"
175 << type2c(arg1.type(), ns)
176 << "`. Insert a cast to the type that you want to access.";
178 error_message.str(), expr.source_location()};
179 }
180
181 const auto &arg2 = expr.arguments()[1];
183 {
184 // Can't set value from a shadow memory field that has a name that is
185 // not a constant string
186 std::ostringstream error_message;
187 error_message << identifier
188 << " argument 2 must be string constant (literal), but ("
189 << expr2c(arg2, ns) << ") has type `"
190 << type2c(arg2.type(), ns) << '`';
192 error_message.str(), expr.source_location()};
193 }
194
195 // The third argument type must be either a boolean or a bitvector.
196 const auto &arg3 = expr.arguments()[2];
197 const auto &arg3_type = arg3.type();
198 if(
199 !can_cast_type<bitvector_typet>(arg3_type) &&
200 !can_cast_type<bool_typet>(arg3_type))
201 {
202 // Can't set the shadow memory value with a non-boolean and non-bitvector
203 // value.
204 std::ostringstream error_message;
205 error_message << identifier
206 << " argument 3 must be a boolean or of integer value, but ("
207 << expr2c(arg3, ns) << ") has type `" << type2c(arg3_type, ns)
208 << '`';
210 error_message.str(), expr.source_location()};
211 }
212
213 // The function type is just an ellipsis, otherwise the non-ellipsis arguments
214 // will be typechecked and implicitly casted.
215 code_typet t({}, void_type());
216 t.make_ellipsis();
217
218 // Create the symbol with the right type.
219 symbol_exprt result(identifier, std::move(t));
220 result.add_source_location() = expr.source_location();
221 return result;
222}
223
228{
229 const exprt &f_op = expr.function();
230 INVARIANT(
232 "expr.function() has to be a symbol_expr");
233 const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
234
235 if(
236 identifier == CPROVER_PREFIX "field_decl_global" ||
237 identifier == CPROVER_PREFIX "field_decl_local")
238 {
239 return typecheck_field_decl(expr, identifier, *this);
240 }
241 else if(identifier == CPROVER_PREFIX "get_field")
242 {
243 return typecheck_get_field(expr, identifier, *this);
244 }
245 else if(identifier == CPROVER_PREFIX "set_field")
246 {
247 return typecheck_set_field(expr, identifier, *this);
248 }
249 // The function is not a shadow memory builtin, so we return <empty>.
250 return {};
251}
configt config
Definition config.cpp:25
ANSI-C Language Type Checking.
static symbol_exprt typecheck_get_field(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory get_field function.
static symbol_exprt typecheck_set_field(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory set_field function.
static symbol_exprt typecheck_field_decl(const side_effect_expr_function_callt &expr, const irep_idt &identifier, const namespacet &ns)
Function to typecheck a shadow memory field_declaration function.
empty_typet void_type()
Definition c_types.cpp:245
signedbv_typet signed_int_type()
Definition c_types.cpp:22
virtual std::optional< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
Base type of functions.
Definition std_types.h:583
void make_ellipsis()
Definition std_types.h:679
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
Thrown when we can't handle something in an input source file.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
exprt::operandst & arguments()
Definition std_code.h:1718
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4184
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4200
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
dstringt irep_idt