cprover
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/cprover_prefix.h>
13 #include <util/std_code_base.h>
14 #include <util/std_expr.h>
15 
20 class code_assignt : public codet
21 {
22 public:
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,
61  {
62  DATA_CHECK(
63  vm, code.operands().size() == 2, "assignment must have two operands");
64  }
65 
66  static void validate(
67  const codet &code,
68  const namespacet &,
70  {
71  check(code, vm);
72 
73  DATA_CHECK(
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,
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 
92 protected:
93  using codet::op0;
94  using codet::op1;
95  using codet::op2;
96  using codet::op3;
97 };
98 
99 template <>
100 inline bool can_cast_expr<code_assignt>(const exprt &base)
101 {
102  return detail::can_cast_code_impl(base, ID_assign);
103 }
104 
105 inline void validate_expr(const code_assignt &x)
106 {
108 }
109 
110 inline const code_assignt &to_code_assign(const codet &code)
111 {
112  PRECONDITION(code.get_statement() == ID_assign);
113  code_assignt::check(code);
114  return static_cast<const code_assignt &>(code);
115 }
116 
118 {
119  PRECONDITION(code.get_statement() == ID_assign);
120  code_assignt::check(code);
121  return static_cast<code_assignt &>(code);
122 }
123 
126 class code_deadt : public codet
127 {
128 public:
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 
143  const irep_idt &get_identifier() const
144  {
145  return symbol().get_identifier();
146  }
147 
148  static void check(
149  const codet &code,
151  {
152  DATA_CHECK(
153  vm,
154  code.operands().size() == 1,
155  "removal (code_deadt) must have one operand");
156  DATA_CHECK(
157  vm,
158  code.op0().id() == ID_symbol,
159  "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
160  }
161 
162 protected:
163  using codet::op0;
164  using codet::op1;
165  using codet::op2;
166  using codet::op3;
167 };
168 
169 template <>
170 inline bool can_cast_expr<code_deadt>(const exprt &base)
171 {
172  return detail::can_cast_code_impl(base, ID_dead);
173 }
174 
175 inline void validate_expr(const code_deadt &x)
176 {
178 }
179 
180 inline 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 
198 class code_declt : public codet
199 {
200 public:
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 
215  const irep_idt &get_identifier() const
216  {
217  return symbol().get_identifier();
218  }
219 
220  static void check(
221  const codet &code,
223  {
224  DATA_CHECK(
225  vm, code.operands().size() == 1, "declaration must have one operand");
226  DATA_CHECK(
227  vm,
228  code.op0().id() == ID_symbol,
229  "declaring a non-symbol: " +
231  }
232 };
233 
234 template <>
235 inline bool can_cast_expr<code_declt>(const exprt &base)
236 {
237  return detail::can_cast_code_impl(base, ID_decl);
238 }
239 
240 inline void validate_expr(const code_declt &x)
241 {
243 }
244 
245 inline 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 {
266 public:
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 
300  exprt &function()
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,
323  {
324  DATA_CHECK(
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 &,
336  {
337  check(code, vm);
338 
339  if(code.op0().id() != ID_nil)
340  DATA_CHECK(
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,
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 
359 protected:
360  using codet::op0;
361  using codet::op1;
362  using codet::op2;
363  using codet::op3;
364 };
365 
366 template <>
368 {
369  return detail::can_cast_code_impl(base, ID_function_call);
370 }
371 
372 inline void validate_expr(const code_function_callt &x)
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 
399 class code_inputt : public codet
400 {
401 public:
405  explicit code_inputt(
406  std::vector<exprt> arguments,
407  optionalt<source_locationt> location = {});
408 
417  code_inputt(
418  const irep_idt &description,
419  exprt expression,
420  optionalt<source_locationt> location = {});
421 
422  static void check(
423  const codet &code,
425 };
426 
427 template <>
428 inline bool can_cast_expr<code_inputt>(const exprt &base)
429 {
430  return detail::can_cast_code_impl(base, ID_input);
431 }
432 
433 inline void validate_expr(const code_inputt &input)
434 {
435  code_inputt::check(input);
436 }
437 
446 class code_outputt : public codet
447 {
448 public:
452  explicit code_outputt(
453  std::vector<exprt> arguments,
454  optionalt<source_locationt> location = {});
455 
463  code_outputt(
464  const irep_idt &description,
465  exprt expression,
466  optionalt<source_locationt> location = {});
467 
468  static void check(
469  const codet &code,
471 };
472 
473 template <>
474 inline bool can_cast_expr<code_outputt>(const exprt &base)
475 {
476  return detail::can_cast_code_impl(base, ID_output);
477 }
478 
479 inline void validate_expr(const code_outputt &output)
480 {
481  code_outputt::check(output);
482 }
483 
485 class code_returnt : public codet
486 {
487 public:
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,
505  {
506  DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
507  }
508 
509 protected:
510  using codet::op0;
511  using codet::op1;
512  using codet::op2;
513  using codet::op3;
514 };
515 
516 template <>
517 inline bool can_cast_expr<code_returnt>(const exprt &base)
518 {
519  return detail::can_cast_code_impl(base, ID_return);
520 }
521 
522 inline void validate_expr(const code_returnt &x)
523 {
525 }
526 
527 inline const code_returnt &to_code_return(const codet &code)
528 {
529  PRECONDITION(code.get_statement() == ID_return);
530  code_returnt::check(code);
531  return static_cast<const code_returnt &>(code);
532 }
533 
535 {
536  PRECONDITION(code.get_statement() == ID_return);
537  code_returnt::check(code);
538  return static_cast<code_returnt &>(code);
539 }
540 
552 inline code_function_callt
553 havoc_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 irep_idt & get_identifier() const
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
const symbol_exprt & symbol() const
A codet representing the declaration of a local variable.
const irep_idt & get_identifier() const
symbol_exprt & symbol()
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
code_declt(symbol_exprt symbol)
const symbol_exprt & symbol() 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
A codet representing the declaration that an input of a particular description has a value which corr...
code_inputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_input in user code.
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)
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
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 & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
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
const code_returnt & to_code_return(const codet &code)
bool can_cast_expr< code_function_callt >(const exprt &base)
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_declt & to_code_decl(const codet &code)
bool can_cast_expr< code_returnt >(const exprt &base)
const code_deadt & to_code_dead(const codet &code)
bool can_cast_expr< code_deadt >(const exprt &base)
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_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
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
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