CBMC
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/std_code_base.h>
13#include <util/std_expr.h>
14
16
22{
23public:
25 {
26 operands().resize(2);
27 }
28
30 : goto_instruction_codet(ID_assign, {std::move(lhs), std::move(rhs)})
31 {
32 }
33
37 {std::move(lhs), std::move(rhs)},
38 std::move(loc))
39 {
40 }
41
43 {
44 return op0();
45 }
46
48 {
49 return op1();
50 }
51
52 const exprt &lhs() const
53 {
54 return op0();
55 }
56
57 const exprt &rhs() const
58 {
59 return op1();
60 }
61
62 static void check(
63 const goto_instruction_codet &code,
65 {
67 vm, code.operands().size() == 2, "assignment must have two operands");
68 }
69
70 static void validate(
71 const goto_instruction_codet &code,
72 const namespacet &,
74 {
75 check(code, vm);
76
78 vm,
79 code.op0().type() == code.op1().type(),
80 "lhs and rhs of assignment must have same type");
81 }
82
83 static void validate_full(
84 const goto_instruction_codet &code,
85 const namespacet &ns,
87 {
88 for(const exprt &op : code.operands())
89 {
90 validate_full_expr(op, ns, vm);
91 }
92
93 validate(code, ns, vm);
94 }
95
96protected:
101};
102
103template <>
104inline bool can_cast_expr<code_assignt>(const exprt &base)
105{
107}
108
109inline void validate_expr(const code_assignt &x)
110{
112}
113
115{
118 return static_cast<const code_assignt &>(code);
119}
120
122{
125 return static_cast<code_assignt &>(code);
126}
127
131{
132public:
134 : goto_instruction_codet(ID_dead, {std::move(symbol)})
135 {
136 }
137
139 {
140 return static_cast<symbol_exprt &>(op0());
141 }
142
143 const symbol_exprt &symbol() const
144 {
145 return static_cast<const symbol_exprt &>(op0());
146 }
147
149 {
150 return symbol().get_identifier();
151 }
152
153 static void check(
154 const goto_instruction_codet &code,
156 {
158 vm,
159 code.operands().size() == 1,
160 "removal (code_deadt) must have one operand");
162 vm,
163 code.op0().id() == ID_symbol,
164 "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
165 }
166
167protected:
172};
173
174template <>
175inline bool can_cast_expr<code_deadt>(const exprt &base)
176{
178}
179
180inline void validate_expr(const code_deadt &x)
181{
183}
184
186{
188 code_deadt::check(code);
189 return static_cast<const code_deadt &>(code);
190}
191
193{
195 code_deadt::check(code);
196 return static_cast<code_deadt &>(code);
197}
198
204{
205public:
207 : goto_instruction_codet(ID_decl, {std::move(symbol)})
208 {
209 }
210
212 {
213 return static_cast<symbol_exprt &>(op0());
214 }
215
216 const symbol_exprt &symbol() const
217 {
218 return static_cast<const symbol_exprt &>(op0());
219 }
220
222 {
223 return symbol().get_identifier();
224 }
225
226 static void check(
227 const goto_instruction_codet &code,
229 {
231 vm, code.operands().size() == 1, "declaration must have one operand");
233 vm,
234 code.op0().id() == ID_symbol,
235 "declaring a non-symbol: " +
236 id2string(to_symbol_expr(code.op0()).get_identifier()));
237 }
238};
239
240template <>
241inline bool can_cast_expr<code_declt>(const exprt &base)
242{
244}
245
246inline void validate_expr(const code_declt &x)
247{
249}
250
252{
254 code_declt::check(code);
255 return static_cast<const code_declt &>(code);
256}
257
259{
261 code_declt::check(code);
262 return static_cast<code_declt &>(code);
263}
264
271{
272public:
279
281
289
295
297 {
298 return op0();
299 }
300
301 const exprt &lhs() const
302 {
303 return op0();
304 }
305
307 {
308 return op1();
309 }
310
311 const exprt &function() const
312 {
313 return op1();
314 }
315
317 {
318 return op2().operands();
319 }
320
321 const argumentst &arguments() const
322 {
323 return op2().operands();
324 }
325
326 static void check(
327 const goto_instruction_codet &code,
329 {
331 vm,
332 code.operands().size() == 3,
333 "function calls must have three operands:\n1) expression to store the "
334 "returned values\n2) the function being called\n3) the vector of "
335 "arguments");
336 }
337
338 static void validate(
339 const goto_instruction_codet &code,
340 const namespacet &,
342 {
343 check(code, vm);
344
345 if(code.op0().id() != ID_nil)
347 vm,
348 code.op0().type() == to_code_type(code.op1().type()).return_type(),
349 "function returns expression of wrong type");
350 }
351
352 static void validate_full(
353 const goto_instruction_codet &code,
354 const namespacet &ns,
356 {
357 for(const exprt &op : code.operands())
358 {
359 validate_full_expr(op, ns, vm);
360 }
361
362 validate(code, ns, vm);
363 }
364
365protected:
370};
371
372template <>
374{
376}
377
382
383inline const code_function_callt &
385{
388 return static_cast<const code_function_callt &>(code);
389}
390
397
407{
408public:
412 explicit code_inputt(
413 std::vector<exprt> arguments,
414 std::optional<source_locationt> location = {});
415
425 const irep_idt &description,
426 exprt expression,
427 std::optional<source_locationt> location = {});
428
429 static void check(
430 const goto_instruction_codet &code,
432};
433
434template <>
435inline bool can_cast_expr<code_inputt>(const exprt &base)
436{
438}
439
440inline void validate_expr(const code_inputt &input)
441{
442 code_inputt::check(input);
443}
444
454{
455public:
459 explicit code_outputt(
460 std::vector<exprt> arguments,
461 std::optional<source_locationt> location = {});
462
471 const irep_idt &description,
472 exprt expression,
473 std::optional<source_locationt> location = {});
474
475 static void check(
476 const goto_instruction_codet &code,
478};
479
480template <>
481inline bool can_cast_expr<code_outputt>(const exprt &base)
482{
484}
485
486inline void validate_expr(const code_outputt &output)
487{
488 code_outputt::check(output);
489}
490
494{
495public:
497 : goto_instruction_codet(ID_return, {std::move(_op)})
498 {
499 }
500
501 const exprt &return_value() const
502 {
503 return op0();
504 }
505
507 {
508 return op0();
509 }
510
511 static void check(
512 const goto_instruction_codet &code,
514 {
515 DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
516 }
517
518protected:
523};
524
525template <>
526inline bool can_cast_expr<code_returnt>(const exprt &base)
527{
529}
530
531inline void validate_expr(const code_returnt &x)
532{
534}
535
537{
540 return static_cast<const code_returnt &>(code);
541}
542
544{
547 return static_cast<code_returnt &>(code);
548}
549
562havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns);
563
564#endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A goto_instruction_codet representing an assignment in the program.
const exprt & rhs() const
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
static void validate_full(const goto_instruction_codet &code, const namespacet &ns, 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(const goto_instruction_codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
A goto_instruction_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 goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get_identifier() const
A goto_instruction_codet representing the declaration of a local variable.
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
symbol_exprt & symbol()
const symbol_exprt & symbol() const
code_declt(symbol_exprt symbol)
const irep_idt & get_identifier() const
goto_instruction_codet representation of a function call statement.
const argumentst & arguments() const
static void validate(const goto_instruction_codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void validate_full(const goto_instruction_codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
code_function_callt(exprt _function)
const exprt & lhs() const
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_function_callt(exprt _function, argumentst _arguments)
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
const exprt & function() const
A goto_instruction_codet representing the declaration that an input of a particular description has a...
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
A goto_instruction_codet representing the declaration that an output of a particular description has ...
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
goto_instruction_codet representation of a "return from a function" statement.
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
const exprt & return_value() const
Data structure for representing an arbitrary statement in a program.
exprt & op3()
Definition expr.h:142
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
exprt & op2()
Definition expr.h:139
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
exprt()
Definition expr.h:61
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:388
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:3208
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
bool can_cast_expr< code_function_callt >(const exprt &base)
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_deadt & to_code_dead(const goto_instruction_codet &code)
bool can_cast_expr< code_inputt >(const exprt &base)
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)
bool can_cast_expr< code_deadt >(const exprt &base)
const code_assignt & to_code_assign(const goto_instruction_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 code_declt & to_code_decl(const goto_instruction_codet &code)
const code_returnt & to_code_return(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
STL namespace.
#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:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
#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