CBMC
goto_instruction_code.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing instructions in a GOTO program
4 
5 Author: 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 {
23 public:
25  {
26  operands().resize(2);
27  }
28 
30  : goto_instruction_codet(ID_assign, {std::move(lhs), std::move(rhs)})
31  {
32  }
33 
36  ID_assign,
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  {
66  DATA_CHECK(
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 
77  DATA_CHECK(
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 
96 protected:
101 };
102 
103 template <>
104 inline bool can_cast_expr<code_assignt>(const exprt &base)
105 {
106  return detail::can_cast_code_impl(base, ID_assign);
107 }
108 
109 inline void validate_expr(const code_assignt &x)
110 {
112 }
113 
115 {
116  PRECONDITION(code.get_statement() == ID_assign);
117  code_assignt::check(code);
118  return static_cast<const code_assignt &>(code);
119 }
120 
122 {
123  PRECONDITION(code.get_statement() == ID_assign);
124  code_assignt::check(code);
125  return static_cast<code_assignt &>(code);
126 }
127 
131 {
132 public:
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 
148  const irep_idt &get_identifier() const
149  {
150  return symbol().get_identifier();
151  }
152 
153  static void check(
154  const goto_instruction_codet &code,
156  {
157  DATA_CHECK(
158  vm,
159  code.operands().size() == 1,
160  "removal (code_deadt) must have one operand");
161  DATA_CHECK(
162  vm,
163  code.op0().id() == ID_symbol,
164  "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
165  }
166 
167 protected:
172 };
173 
174 template <>
175 inline bool can_cast_expr<code_deadt>(const exprt &base)
176 {
177  return detail::can_cast_code_impl(base, ID_dead);
178 }
179 
180 inline void validate_expr(const code_deadt &x)
181 {
183 }
184 
186 {
187  PRECONDITION(code.get_statement() == ID_dead);
188  code_deadt::check(code);
189  return static_cast<const code_deadt &>(code);
190 }
191 
193 {
194  PRECONDITION(code.get_statement() == ID_dead);
195  code_deadt::check(code);
196  return static_cast<code_deadt &>(code);
197 }
198 
204 {
205 public:
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 
221  const irep_idt &get_identifier() const
222  {
223  return symbol().get_identifier();
224  }
225 
226  static void check(
227  const goto_instruction_codet &code,
229  {
230  DATA_CHECK(
231  vm, code.operands().size() == 1, "declaration must have one operand");
232  DATA_CHECK(
233  vm,
234  code.op0().id() == ID_symbol,
235  "declaring a non-symbol: " +
237  }
238 };
239 
240 template <>
241 inline bool can_cast_expr<code_declt>(const exprt &base)
242 {
243  return detail::can_cast_code_impl(base, ID_decl);
244 }
245 
246 inline void validate_expr(const code_declt &x)
247 {
249 }
250 
252 {
253  PRECONDITION(code.get_statement() == ID_decl);
254  code_declt::check(code);
255  return static_cast<const code_declt &>(code);
256 }
257 
259 {
260  PRECONDITION(code.get_statement() == ID_decl);
261  code_declt::check(code);
262  return static_cast<code_declt &>(code);
263 }
264 
271 {
272 public:
273  explicit code_function_callt(exprt _function)
275  ID_function_call,
276  {nil_exprt(), std::move(_function), exprt(ID_arguments)})
277  {
278  }
279 
281 
282  code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
284  ID_function_call,
285  {std::move(_lhs), std::move(_function), exprt(ID_arguments)})
286  {
287  arguments() = std::move(_arguments);
288  }
289 
290  code_function_callt(exprt _function, argumentst _arguments)
291  : code_function_callt(std::move(_function))
292  {
293  arguments() = std::move(_arguments);
294  }
295 
297  {
298  return op0();
299  }
300 
301  const exprt &lhs() const
302  {
303  return op0();
304  }
305 
306  exprt &function()
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  {
330  DATA_CHECK(
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)
346  DATA_CHECK(
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 
365 protected:
370 };
371 
372 template <>
374 {
375  return detail::can_cast_code_impl(base, ID_function_call);
376 }
377 
378 inline void validate_expr(const code_function_callt &x)
379 {
381 }
382 
383 inline const code_function_callt &
385 {
386  PRECONDITION(code.get_statement() == ID_function_call);
388  return static_cast<const code_function_callt &>(code);
389 }
390 
392 {
393  PRECONDITION(code.get_statement() == ID_function_call);
395  return static_cast<code_function_callt &>(code);
396 }
397 
407 {
408 public:
412  explicit code_inputt(
413  std::vector<exprt> arguments,
414  std::optional<source_locationt> location = {});
415 
424  code_inputt(
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 
434 template <>
435 inline bool can_cast_expr<code_inputt>(const exprt &base)
436 {
437  return detail::can_cast_code_impl(base, ID_input);
438 }
439 
440 inline void validate_expr(const code_inputt &input)
441 {
442  code_inputt::check(input);
443 }
444 
454 {
455 public:
459  explicit code_outputt(
460  std::vector<exprt> arguments,
461  std::optional<source_locationt> location = {});
462 
470  code_outputt(
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 
480 template <>
481 inline bool can_cast_expr<code_outputt>(const exprt &base)
482 {
483  return detail::can_cast_code_impl(base, ID_output);
484 }
485 
486 inline void validate_expr(const code_outputt &output)
487 {
488  code_outputt::check(output);
489 }
490 
494 {
495 public:
496  explicit code_returnt(exprt _op)
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 
518 protected:
523 };
524 
525 template <>
526 inline bool can_cast_expr<code_returnt>(const exprt &base)
527 {
528  return detail::can_cast_code_impl(base, ID_return);
529 }
530 
531 inline void validate_expr(const code_returnt &x)
532 {
534 }
535 
537 {
538  PRECONDITION(code.get_statement() == ID_return);
539  code_returnt::check(code);
540  return static_cast<const code_returnt &>(code);
541 }
542 
544 {
545  PRECONDITION(code.get_statement() == ID_return);
546  code_returnt::check(code);
547  return static_cast<code_returnt &>(code);
548 }
549 
561 inline code_function_callt
562 havoc_slice_call(const exprt &p, const exprt &size, const namespacet &ns);
563 
564 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INSTRUCTION_CODE_H
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)
const exprt & lhs() const
static void validate_full(const goto_instruction_codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
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)
static void check(const goto_instruction_codet &code, const validation_modet vm=validation_modet::INVARIANT)
const irep_idt & get_identifier() const
const symbol_exprt & symbol() 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)
const irep_idt & get_identifier() const
symbol_exprt & symbol()
code_declt(symbol_exprt symbol)
const symbol_exprt & symbol() 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)
static void check(const goto_instruction_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
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)
code_inputt(std::vector< exprt > arguments, std::optional< source_locationt > location={})
This constructor is for support of calls to __CPROVER_input in user code.
A goto_instruction_codet representing the declaration that an output of a particular description has ...
code_outputt(std::vector< exprt > arguments, std::optional< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
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
const typet & return_type() const
Definition: std_types.h:689
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op3()
Definition: expr.h:142
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
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: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:94
The NIL expression.
Definition: std_expr.h:3081
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_returnt & to_code_return(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)
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const code_deadt & to_code_dead(const goto_instruction_codet &code)
bool can_cast_expr< code_returnt >(const exprt &base)
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
bool can_cast_expr< code_deadt >(const exprt &base)
const code_declt & to_code_decl(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 std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code_base.h:84
#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