cprover
Loading...
Searching...
No Matches
goto_instruction_code.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data structures representing instructions in a GOTO program
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
10#define CPROVER_UTIL_GOTO_INSTRUCTION_CODE_H
11
12#include <util/cprover_prefix.h>
13#include <util/std_code_base.h>
14#include <util/std_expr.h>
15
20class code_assignt : public codet
21{
22public:
23 code_assignt() : codet(ID_assign)
24 {
25 operands().resize(2);
26 }
27
29 : codet(ID_assign, {std::move(lhs), std::move(rhs)})
30 {
31 }
32
34 : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc))
35 {
36 }
37
39 {
40 return op0();
41 }
42
44 {
45 return op1();
46 }
47
48 const exprt &lhs() const
49 {
50 return op0();
51 }
52
53 const exprt &rhs() const
54 {
55 return op1();
56 }
57
58 static void check(
59 const codet &code,
60 const validation_modet vm = validation_modet::INVARIANT)
61 {
63 vm, code.operands().size() == 2, "assignment must have two operands");
64 }
65
66 static void validate(
67 const codet &code,
68 const namespacet &,
69 const validation_modet vm = validation_modet::INVARIANT)
70 {
71 check(code, vm);
72
74 vm,
75 code.op0().type() == code.op1().type(),
76 "lhs and rhs of assignment must have same type");
77 }
78
79 static void validate_full(
80 const codet &code,
81 const namespacet &ns,
82 const validation_modet vm = validation_modet::INVARIANT)
83 {
84 for(const exprt &op : code.operands())
85 {
86 validate_full_expr(op, ns, vm);
87 }
88
89 validate(code, ns, vm);
90 }
91
92protected:
93 using codet::op0;
94 using codet::op1;
95 using codet::op2;
96 using codet::op3;
97};
98
99template <>
100inline bool can_cast_expr<code_assignt>(const exprt &base)
101{
102 return detail::can_cast_code_impl(base, ID_assign);
103}
104
105inline void validate_expr(const code_assignt &x)
106{
108}
109
110inline const code_assignt &to_code_assign(const codet &code)
111{
112 PRECONDITION(code.get_statement() == ID_assign);
114 return static_cast<const code_assignt &>(code);
115}
116
118{
119 PRECONDITION(code.get_statement() == ID_assign);
121 return static_cast<code_assignt &>(code);
122}
123
126class code_deadt : public codet
127{
128public:
129 explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)})
130 {
131 }
132
134 {
135 return static_cast<symbol_exprt &>(op0());
136 }
137
138 const symbol_exprt &symbol() const
139 {
140 return static_cast<const symbol_exprt &>(op0());
141 }
142
144 {
145 return symbol().get_identifier();
146 }
147
148 static void check(
149 const codet &code,
150 const validation_modet vm = validation_modet::INVARIANT)
151 {
153 vm,
154 code.operands().size() == 1,
155 "removal (code_deadt) must have one operand");
157 vm,
158 code.op0().id() == ID_symbol,
159 "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
160 }
161
162protected:
163 using codet::op0;
164 using codet::op1;
165 using codet::op2;
166 using codet::op3;
167};
168
169template <>
170inline bool can_cast_expr<code_deadt>(const exprt &base)
171{
172 return detail::can_cast_code_impl(base, ID_dead);
173}
174
175inline void validate_expr(const code_deadt &x)
176{
178}
179
180inline const code_deadt &to_code_dead(const codet &code)
181{
182 PRECONDITION(code.get_statement() == ID_dead);
183 code_deadt::check(code);
184 return static_cast<const code_deadt &>(code);
185}
186
188{
189 PRECONDITION(code.get_statement() == ID_dead);
190 code_deadt::check(code);
191 return static_cast<code_deadt &>(code);
192}
193
198class code_declt : public codet
199{
200public:
201 explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
202 {
203 }
204
206 {
207 return static_cast<symbol_exprt &>(op0());
208 }
209
210 const symbol_exprt &symbol() const
211 {
212 return static_cast<const symbol_exprt &>(op0());
213 }
214
216 {
217 return symbol().get_identifier();
218 }
219
220 static void check(
221 const codet &code,
222 const validation_modet vm = validation_modet::INVARIANT)
223 {
225 vm, code.operands().size() == 1, "declaration must have one operand");
227 vm,
228 code.op0().id() == ID_symbol,
229 "declaring a non-symbol: " +
231 }
232};
233
234template <>
235inline bool can_cast_expr<code_declt>(const exprt &base)
236{
237 return detail::can_cast_code_impl(base, ID_decl);
238}
239
240inline void validate_expr(const code_declt &x)
241{
243}
244
245inline const code_declt &to_code_decl(const codet &code)
246{
247 PRECONDITION(code.get_statement() == ID_decl);
248 code_declt::check(code);
249 return static_cast<const code_declt &>(code);
250}
251
253{
254 PRECONDITION(code.get_statement() == ID_decl);
255 code_declt::check(code);
256 return static_cast<code_declt &>(code);
257}
258
265{
266public:
267 explicit code_function_callt(exprt _function)
268 : codet(
269 ID_function_call,
270 {nil_exprt(), std::move(_function), exprt(ID_arguments)})
271 {
272 }
273
275
276 code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
277 : codet(
278 ID_function_call,
279 {std::move(_lhs), std::move(_function), exprt(ID_arguments)})
280 {
281 arguments() = std::move(_arguments);
282 }
283
284 code_function_callt(exprt _function, argumentst _arguments)
285 : code_function_callt(std::move(_function))
286 {
287 arguments() = std::move(_arguments);
288 }
289
291 {
292 return op0();
293 }
294
295 const exprt &lhs() const
296 {
297 return op0();
298 }
299
301 {
302 return op1();
303 }
304
305 const exprt &function() const
306 {
307 return op1();
308 }
309
311 {
312 return op2().operands();
313 }
314
315 const argumentst &arguments() const
316 {
317 return op2().operands();
318 }
319
320 static void check(
321 const codet &code,
322 const validation_modet vm = validation_modet::INVARIANT)
323 {
325 vm,
326 code.operands().size() == 3,
327 "function calls must have three operands:\n1) expression to store the "
328 "returned values\n2) the function being called\n3) the vector of "
329 "arguments");
330 }
331
332 static void validate(
333 const codet &code,
334 const namespacet &,
335 const validation_modet vm = validation_modet::INVARIANT)
336 {
337 check(code, vm);
338
339 if(code.op0().id() != ID_nil)
341 vm,
342 code.op0().type() == to_code_type(code.op1().type()).return_type(),
343 "function returns expression of wrong type");
344 }
345
346 static void validate_full(
347 const codet &code,
348 const namespacet &ns,
349 const validation_modet vm = validation_modet::INVARIANT)
350 {
351 for(const exprt &op : code.operands())
352 {
353 validate_full_expr(op, ns, vm);
354 }
355
356 validate(code, ns, vm);
357 }
358
359protected:
360 using codet::op0;
361 using codet::op1;
362 using codet::op2;
363 using codet::op3;
364};
365
366template <>
368{
369 return detail::can_cast_code_impl(base, ID_function_call);
370}
371
373{
375}
376
378{
379 PRECONDITION(code.get_statement() == ID_function_call);
381 return static_cast<const code_function_callt &>(code);
382}
383
385{
386 PRECONDITION(code.get_statement() == ID_function_call);
388 return static_cast<code_function_callt &>(code);
389}
390
399class code_inputt : public codet
400{
401public:
405 explicit code_inputt(
406 std::vector<exprt> arguments,
407 optionalt<source_locationt> location = {});
408
418 const irep_idt &description,
419 exprt expression,
420 optionalt<source_locationt> location = {});
421
422 static void check(
423 const codet &code,
424 const validation_modet vm = validation_modet::INVARIANT);
425};
426
427template <>
428inline bool can_cast_expr<code_inputt>(const exprt &base)
429{
430 return detail::can_cast_code_impl(base, ID_input);
431}
432
433inline void validate_expr(const code_inputt &input)
434{
435 code_inputt::check(input);
436}
437
446class code_outputt : public codet
447{
448public:
452 explicit code_outputt(
453 std::vector<exprt> arguments,
454 optionalt<source_locationt> location = {});
455
464 const irep_idt &description,
465 exprt expression,
466 optionalt<source_locationt> location = {});
467
468 static void check(
469 const codet &code,
470 const validation_modet vm = validation_modet::INVARIANT);
471};
472
473template <>
474inline bool can_cast_expr<code_outputt>(const exprt &base)
475{
476 return detail::can_cast_code_impl(base, ID_output);
477}
478
479inline void validate_expr(const code_outputt &output)
480{
481 code_outputt::check(output);
482}
483
485class code_returnt : public codet
486{
487public:
488 explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
489 {
490 }
491
492 const exprt &return_value() const
493 {
494 return op0();
495 }
496
498 {
499 return op0();
500 }
501
502 static void check(
503 const codet &code,
504 const validation_modet vm = validation_modet::INVARIANT)
505 {
506 DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
507 }
508
509protected:
510 using codet::op0;
511 using codet::op1;
512 using codet::op2;
513 using codet::op3;
514};
515
516template <>
517inline bool can_cast_expr<code_returnt>(const exprt &base)
518{
519 return detail::can_cast_code_impl(base, ID_return);
520}
521
522inline void validate_expr(const code_returnt &x)
523{
525}
526
527inline const code_returnt &to_code_return(const codet &code)
528{
529 PRECONDITION(code.get_statement() == ID_return);
531 return static_cast<const code_returnt &>(code);
532}
533
535{
536 PRECONDITION(code.get_statement() == ID_return);
538 return static_cast<code_returnt &>(code);
539}
540
553havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns);
554
555#endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H
A codet representing an assignment in the program.
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const exprt & rhs() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & lhs() const
code_assignt(exprt lhs, exprt rhs, source_locationt loc)
code_assignt(exprt lhs, exprt rhs)
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
A codet representing the removal of a local variable going out of scope.
symbol_exprt & symbol()
code_deadt(symbol_exprt symbol)
const symbol_exprt & symbol() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get_identifier() const
A codet representing the declaration of a local variable.
symbol_exprt & symbol()
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const symbol_exprt & symbol() const
code_declt(symbol_exprt symbol)
const irep_idt & get_identifier() const
codet representation of a function call statement.
const argumentst & arguments() const
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
code_function_callt(exprt _function)
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & lhs() const
code_function_callt(exprt _function, argumentst _arguments)
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
exprt::operandst argumentst
const exprt & function() const
A codet representing the declaration that an input of a particular description has a value which corr...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
A codet representing the declaration that an output of a particular description has a value which cor...
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
codet representation of a "return from a function" statement.
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & return_value() const
const typet & return_type() const
Definition: std_types.h:645
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op3()
Definition: expr.h:108
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt()
Definition: expr.h:59
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bool can_cast_expr< code_function_callt >(const exprt &base)
bool can_cast_expr< code_inputt >(const exprt &base)
const code_function_callt & to_code_function_call(const codet &code)
bool can_cast_expr< code_outputt >(const exprt &base)
bool can_cast_expr< code_assignt >(const exprt &base)
bool can_cast_expr< code_declt >(const exprt &base)
void validate_expr(const code_assignt &x)
bool can_cast_expr< code_returnt >(const exprt &base)
const code_assignt & to_code_assign(const codet &code)
const code_declt & to_code_decl(const codet &code)
const code_returnt & to_code_return(const codet &code)
bool can_cast_expr< code_deadt >(const exprt &base)
const code_deadt & to_code_dead(const codet &code)
code_function_callt havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns)
Builds a code_function_callt to __CPROVER_havoc_slice(p, size).
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code_base.h:84
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet