cprover
c_typecheck_gcc_polymorphic_builtins.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_types.h>
19 #include <util/string_constant.h>
20 
21 #include <atomic>
22 
24  const irep_idt &identifier,
25  const exprt::operandst &arguments,
26  const source_locationt &source_location,
27  message_handlert &message_handler)
28 {
29  messaget log(message_handler);
30 
31  // adjust return type of function to match pointer subtype
32  if(arguments.size() < 2)
33  {
34  log.error().source_location = source_location;
35  log.error() << identifier << " expects at least two arguments"
36  << messaget::eom;
37  throw 0;
38  }
39 
40  const exprt &ptr_arg = arguments.front();
41 
42  if(ptr_arg.type().id() != ID_pointer)
43  {
44  log.error().source_location = source_location;
45  log.error() << identifier << " takes a pointer as first argument"
46  << messaget::eom;
47  throw 0;
48  }
49 
51  code_typet::parametert(ptr_arg.type().subtype())},
52  ptr_arg.type().subtype()};
53  t.make_ellipsis();
54  symbol_exprt result{identifier, std::move(t)};
55  result.add_source_location() = source_location;
56 
57  return result;
58 }
59 
61  const irep_idt &identifier,
62  const exprt::operandst &arguments,
63  const source_locationt &source_location,
64  message_handlert &message_handler)
65 {
66  messaget log(message_handler);
67 
68  // adjust return type of function to match pointer subtype
69  if(arguments.size() < 3)
70  {
71  log.error().source_location = source_location;
72  log.error() << identifier << " expects at least three arguments"
73  << messaget::eom;
74  throw 0;
75  }
76 
77  const exprt &ptr_arg = arguments.front();
78 
79  if(ptr_arg.type().id() != ID_pointer)
80  {
81  log.error().source_location = source_location;
82  log.error() << identifier << " takes a pointer as first argument"
83  << messaget::eom;
84  throw 0;
85  }
86 
87  const typet &subtype = ptr_arg.type().subtype();
88  typet sync_return_type = subtype;
89  if(identifier == ID___sync_bool_compare_and_swap)
90  sync_return_type = c_bool_type();
91 
93  code_typet::parametert(subtype),
94  code_typet::parametert(subtype)},
95  sync_return_type};
96  t.make_ellipsis();
97  symbol_exprt result{identifier, std::move(t)};
98  result.add_source_location() = source_location;
99 
100  return result;
101 }
102 
104  const irep_idt &identifier,
105  const exprt::operandst &arguments,
106  const source_locationt &source_location,
107  message_handlert &message_handler)
108 {
109  messaget log(message_handler);
110 
111  // adjust return type of function to match pointer subtype
112  if(arguments.empty())
113  {
114  log.error().source_location = source_location;
115  log.error() << identifier << " expects at least one argument"
116  << messaget::eom;
117  throw 0;
118  }
119 
120  const exprt &ptr_arg = arguments.front();
121 
122  if(ptr_arg.type().id() != ID_pointer)
123  {
124  log.error().source_location = source_location;
125  log.error() << identifier << " takes a pointer as first argument"
126  << messaget::eom;
127  throw 0;
128  }
129 
130  code_typet t{{code_typet::parametert(ptr_arg.type())}, void_type()};
131  t.make_ellipsis();
132  symbol_exprt result{identifier, std::move(t)};
133  result.add_source_location() = source_location;
134 
135  return result;
136 }
137 
139  const irep_idt &identifier,
140  const exprt::operandst &arguments,
141  const source_locationt &source_location,
142  message_handlert &message_handler)
143 {
144  // type __atomic_load_n(type *ptr, int memorder)
145  messaget log(message_handler);
146 
147  if(arguments.size() != 2)
148  {
149  log.error().source_location = source_location;
150  log.error() << identifier << " expects two arguments" << messaget::eom;
151  throw 0;
152  }
153 
154  const exprt &ptr_arg = arguments.front();
155 
156  if(ptr_arg.type().id() != ID_pointer)
157  {
158  log.error().source_location = source_location;
159  log.error() << identifier << " takes a pointer as first argument"
160  << messaget::eom;
161  throw 0;
162  }
163 
164  const code_typet t(
165  {code_typet::parametert(ptr_arg.type()),
167  ptr_arg.type().subtype());
168  symbol_exprt result(identifier, t);
169  result.add_source_location() = source_location;
170  return result;
171 }
172 
174  const irep_idt &identifier,
175  const exprt::operandst &arguments,
176  const source_locationt &source_location,
177  message_handlert &message_handler)
178 {
179  // void __atomic_store_n(type *ptr, type val, int memorder)
180  messaget log(message_handler);
181 
182  if(arguments.size() != 3)
183  {
184  log.error().source_location = source_location;
185  log.error() << identifier << " expects three arguments" << messaget::eom;
186  throw 0;
187  }
188 
189  const exprt &ptr_arg = arguments.front();
190 
191  if(ptr_arg.type().id() != ID_pointer)
192  {
193  log.error().source_location = source_location;
194  log.error() << identifier << " takes a pointer as first argument"
195  << messaget::eom;
196  throw 0;
197  }
198 
199  const code_typet t(
200  {code_typet::parametert(ptr_arg.type()),
201  code_typet::parametert(ptr_arg.type().subtype()),
203  void_type());
204  symbol_exprt result(identifier, t);
205  result.add_source_location() = source_location;
206  return result;
207 }
208 
210  const irep_idt &identifier,
211  const exprt::operandst &arguments,
212  const source_locationt &source_location,
213  message_handlert &message_handler)
214 {
215  // type __atomic_exchange_n(type *ptr, type val, int memorder)
216  messaget log(message_handler);
217 
218  if(arguments.size() != 3)
219  {
220  log.error().source_location = source_location;
221  log.error() << identifier << " expects three arguments" << messaget::eom;
222  throw 0;
223  }
224 
225  const exprt &ptr_arg = arguments.front();
226 
227  if(ptr_arg.type().id() != ID_pointer)
228  {
229  log.error().source_location = source_location;
230  log.error() << identifier << " takes a pointer as first argument"
231  << messaget::eom;
232  throw 0;
233  }
234 
235  const code_typet t(
236  {code_typet::parametert(ptr_arg.type()),
237  code_typet::parametert(ptr_arg.type().subtype()),
239  ptr_arg.type().subtype());
240  symbol_exprt result(identifier, t);
241  result.add_source_location() = source_location;
242  return result;
243 }
244 
246  const irep_idt &identifier,
247  const exprt::operandst &arguments,
248  const source_locationt &source_location,
249  message_handlert &message_handler)
250 {
251  // void __atomic_load(type *ptr, type *ret, int memorder)
252  // void __atomic_store(type *ptr, type *val, int memorder)
253  messaget log(message_handler);
254 
255  if(arguments.size() != 3)
256  {
257  log.error().source_location = source_location;
258  log.error() << identifier << " expects three arguments" << messaget::eom;
259  throw 0;
260  }
261 
262  if(arguments[0].type().id() != ID_pointer)
263  {
264  log.error().source_location = source_location;
265  log.error() << identifier << " takes a pointer as first argument"
266  << messaget::eom;
267  throw 0;
268  }
269 
270  if(arguments[1].type().id() != ID_pointer)
271  {
272  log.error().source_location = source_location;
273  log.error() << identifier << " takes a pointer as second argument"
274  << messaget::eom;
275  throw 0;
276  }
277 
278  const exprt &ptr_arg = arguments.front();
279 
280  const code_typet t(
281  {code_typet::parametert(ptr_arg.type()),
282  code_typet::parametert(ptr_arg.type()),
284  void_type());
285  symbol_exprt result(identifier, t);
286  result.add_source_location() = source_location;
287  return result;
288 }
289 
291  const irep_idt &identifier,
292  const exprt::operandst &arguments,
293  const source_locationt &source_location,
294  message_handlert &message_handler)
295 {
296  // void __atomic_exchange(type *ptr, type *val, type *ret, int memorder)
297  messaget log(message_handler);
298 
299  if(arguments.size() != 4)
300  {
301  log.error().source_location = source_location;
302  log.error() << identifier << " expects four arguments" << messaget::eom;
303  throw 0;
304  }
305 
306  if(arguments[0].type().id() != ID_pointer)
307  {
308  log.error().source_location = source_location;
309  log.error() << identifier << " takes a pointer as first argument"
310  << messaget::eom;
311  throw 0;
312  }
313 
314  if(arguments[1].type().id() != ID_pointer)
315  {
316  log.error().source_location = source_location;
317  log.error() << identifier << " takes a pointer as second argument"
318  << messaget::eom;
319  throw 0;
320  }
321 
322  if(arguments[2].type().id() != ID_pointer)
323  {
324  log.error().source_location = source_location;
325  log.error() << identifier << " takes a pointer as third argument"
326  << messaget::eom;
327  throw 0;
328  }
329 
330  const exprt &ptr_arg = arguments.front();
331 
332  const code_typet t(
333  {code_typet::parametert(ptr_arg.type()),
334  code_typet::parametert(ptr_arg.type()),
335  code_typet::parametert(ptr_arg.type()),
337  void_type());
338  symbol_exprt result(identifier, t);
339  result.add_source_location() = source_location;
340  return result;
341 }
342 
344  const irep_idt &identifier,
345  const exprt::operandst &arguments,
346  const source_locationt &source_location,
347  message_handlert &message_handler)
348 {
349  // bool __atomic_compare_exchange_n(type *ptr, type *expected, type
350  // desired, bool weak, int success_memorder, int failure_memorder)
351  // bool __atomic_compare_exchange(type *ptr, type *expected, type
352  // *desired, bool weak, int success_memorder, int failure_memorder)
353  messaget log(message_handler);
354 
355  if(arguments.size() != 6)
356  {
357  log.error().source_location = source_location;
358  log.error() << identifier << " expects six arguments" << messaget::eom;
359  throw 0;
360  }
361 
362  if(arguments[0].type().id() != ID_pointer)
363  {
364  log.error().source_location = source_location;
365  log.error() << identifier << " takes a pointer as first argument"
366  << messaget::eom;
367  throw 0;
368  }
369 
370  if(arguments[1].type().id() != ID_pointer)
371  {
372  log.error().source_location = source_location;
373  log.error() << identifier << " takes a pointer as second argument"
374  << messaget::eom;
375  throw 0;
376  }
377 
378  if(
379  identifier == ID___atomic_compare_exchange &&
380  arguments[2].type().id() != ID_pointer)
381  {
382  log.error().source_location = source_location;
383  log.error() << identifier << " takes a pointer as third argument"
384  << messaget::eom;
385  throw 0;
386  }
387 
388  const exprt &ptr_arg = arguments.front();
389 
390  code_typet::parameterst parameters;
391  parameters.push_back(code_typet::parametert(ptr_arg.type()));
392  parameters.push_back(code_typet::parametert(ptr_arg.type()));
393 
394  if(identifier == ID___atomic_compare_exchange)
395  parameters.push_back(code_typet::parametert(ptr_arg.type()));
396  else
397  parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));
398 
399  parameters.push_back(code_typet::parametert(c_bool_type()));
400  parameters.push_back(code_typet::parametert(signed_int_type()));
401  parameters.push_back(code_typet::parametert(signed_int_type()));
402  code_typet t(std::move(parameters), c_bool_type());
403  symbol_exprt result(identifier, t);
404  result.add_source_location() = source_location;
405  return result;
406 }
407 
409  const irep_idt &identifier,
410  const exprt::operandst &arguments,
411  const source_locationt &source_location,
412  message_handlert &message_handler)
413 {
414  messaget log(message_handler);
415 
416  if(arguments.size() != 3)
417  {
418  log.error().source_location = source_location;
419  log.error() << "__atomic_*_fetch primitives take three arguments"
420  << messaget::eom;
421  throw 0;
422  }
423 
424  const exprt &ptr_arg = arguments.front();
425 
426  if(ptr_arg.type().id() != ID_pointer)
427  {
428  log.error().source_location = source_location;
429  log.error()
430  << "__atomic_*_fetch primitives take a pointer as first argument"
431  << messaget::eom;
432  throw 0;
433  }
434 
435  code_typet t(
436  {code_typet::parametert(ptr_arg.type()),
437  code_typet::parametert(ptr_arg.type().subtype()),
439  ptr_arg.type().subtype());
440  symbol_exprt result(identifier, std::move(t));
441  result.add_source_location() = source_location;
442  return result;
443 }
444 
446  const irep_idt &identifier,
447  const exprt::operandst &arguments,
448  const source_locationt &source_location,
449  message_handlert &message_handler)
450 {
451  messaget log(message_handler);
452 
453  if(arguments.size() != 3)
454  {
455  log.error().source_location = source_location;
456  log.error() << "__atomic_fetch_* primitives take three arguments"
457  << messaget::eom;
458  throw 0;
459  }
460 
461  const exprt &ptr_arg = arguments.front();
462 
463  if(ptr_arg.type().id() != ID_pointer)
464  {
465  log.error().source_location = source_location;
466  log.error()
467  << "__atomic_fetch_* primitives take a pointer as first argument"
468  << messaget::eom;
469  throw 0;
470  }
471 
472  code_typet t(
473  {code_typet::parametert(ptr_arg.type()),
474  code_typet::parametert(ptr_arg.type().subtype()),
476  ptr_arg.type().subtype());
477  symbol_exprt result(identifier, std::move(t));
478  result.add_source_location() = source_location;
479  return result;
480 }
481 
483  const irep_idt &identifier,
484  const exprt::operandst &arguments,
485  const source_locationt &source_location)
486 {
487  // the arguments need not be type checked just yet, thus do not make
488  // assumptions that would require type checking
489 
490  if(
491  identifier == ID___sync_fetch_and_add ||
492  identifier == ID___sync_fetch_and_sub ||
493  identifier == ID___sync_fetch_and_or ||
494  identifier == ID___sync_fetch_and_and ||
495  identifier == ID___sync_fetch_and_xor ||
496  identifier == ID___sync_fetch_and_nand ||
497  identifier == ID___sync_add_and_fetch ||
498  identifier == ID___sync_sub_and_fetch ||
499  identifier == ID___sync_or_and_fetch ||
500  identifier == ID___sync_and_and_fetch ||
501  identifier == ID___sync_xor_and_fetch ||
502  identifier == ID___sync_nand_and_fetch ||
503  identifier == ID___sync_lock_test_and_set)
504  {
505  // These are polymorphic, see
506  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
508  identifier, arguments, source_location, get_message_handler());
509  }
510  else if(
511  identifier == ID___sync_bool_compare_and_swap ||
512  identifier == ID___sync_val_compare_and_swap)
513  {
514  // These are polymorphic, see
515  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
517  identifier, arguments, source_location, get_message_handler());
518  }
519  else if(identifier == ID___sync_lock_release)
520  {
521  // This is polymorphic, see
522  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
524  identifier, arguments, source_location, get_message_handler());
525  }
526  else if(identifier == ID___atomic_load_n)
527  {
528  // These are polymorphic
529  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
531  identifier, arguments, source_location, get_message_handler());
532  }
533  else if(identifier == ID___atomic_store_n)
534  {
535  // These are polymorphic
536  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
538  identifier, arguments, source_location, get_message_handler());
539  }
540  else if(identifier == ID___atomic_exchange_n)
541  {
542  // These are polymorphic
543  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
545  identifier, arguments, source_location, get_message_handler());
546  }
547  else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
548  {
549  // These are polymorphic
550  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
552  identifier, arguments, source_location, get_message_handler());
553  }
554  else if(identifier == ID___atomic_exchange)
555  {
556  // These are polymorphic
557  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
559  identifier, arguments, source_location, get_message_handler());
560  }
561  else if(
562  identifier == ID___atomic_compare_exchange_n ||
563  identifier == ID___atomic_compare_exchange)
564  {
565  // These are polymorphic
566  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
568  identifier, arguments, source_location, get_message_handler());
569  }
570  else if(
571  identifier == ID___atomic_add_fetch ||
572  identifier == ID___atomic_sub_fetch ||
573  identifier == ID___atomic_and_fetch ||
574  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
575  identifier == ID___atomic_nand_fetch)
576  {
577  // These are polymorphic
578  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
580  identifier, arguments, source_location, get_message_handler());
581  }
582  else if(
583  identifier == ID___atomic_fetch_add ||
584  identifier == ID___atomic_fetch_sub ||
585  identifier == ID___atomic_fetch_and ||
586  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
587  identifier == ID___atomic_fetch_nand)
588  {
589  // These are polymorphic
590  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
592  identifier, arguments, source_location, get_message_handler());
593  }
594 
595  return {};
596 }
597 
599  const irep_idt &identifier,
600  const typet &type,
601  const source_locationt &source_location,
602  symbol_tablet &symbol_table)
603 {
604  symbolt symbol;
605  symbol.name = id2string(identifier) + "::1::result";
606  symbol.base_name = "result";
607  symbol.type = type;
608  symbol.mode = ID_C;
609  symbol.location = source_location;
610  symbol.is_file_local = true;
611  symbol.is_lvalue = true;
612  symbol.is_thread_local = true;
613 
614  symbol_table.add(symbol);
615 
616  return symbol;
617 }
618 
620  const irep_idt &identifier,
621  const irep_idt &identifier_with_type,
622  const code_typet &code_type,
623  const source_locationt &source_location,
624  const std::vector<symbol_exprt> &parameter_exprs,
625  symbol_tablet &symbol_table,
626  code_blockt &block)
627 {
628  // type __sync_fetch_and_OP(type *ptr, type value, ...)
629  // { type result; result = *ptr; *ptr = result OP value; return result; }
630  const typet &type = code_type.return_type();
631 
632  const symbol_exprt result =
633  result_symbol(identifier_with_type, type, source_location, symbol_table)
634  .symbol_expr();
635  block.add(codet{ID_decl_block, {code_declt{result}}});
636 
637  // place operations on *ptr in an atomic section
639  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
640  {},
641  code_typet{{}, void_type()},
642  source_location}});
643 
644  // build *ptr
645  const dereference_exprt deref_ptr{parameter_exprs[0]};
646 
647  block.add(code_assignt{result, deref_ptr});
648 
649  // build *ptr = result OP arguments[1];
650  irep_idt op_id = identifier == ID___atomic_fetch_add
651  ? ID_plus
652  : identifier == ID___atomic_fetch_sub
653  ? ID_minus
654  : identifier == ID___atomic_fetch_or
655  ? ID_bitor
656  : identifier == ID___atomic_fetch_and
657  ? ID_bitand
658  : identifier == ID___atomic_fetch_xor
659  ? ID_bitxor
660  : identifier == ID___atomic_fetch_nand
661  ? ID_bitnand
662  : ID_nil;
663  binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
664  block.add(code_assignt{deref_ptr, std::move(op_expr)});
665 
667  symbol_exprt::typeless("__atomic_thread_fence"),
668  {parameter_exprs[2]},
669  typet{},
670  source_location}});
671 
674  {},
675  code_typet{{}, void_type()},
676  source_location}});
677 
678  block.add(code_returnt{result});
679 }
680 
682  const irep_idt &identifier,
683  const irep_idt &identifier_with_type,
684  const code_typet &code_type,
685  const source_locationt &source_location,
686  const std::vector<symbol_exprt> &parameter_exprs,
687  symbol_tablet &symbol_table,
688  code_blockt &block)
689 {
690  // type __sync_OP_and_fetch(type *ptr, type value, ...)
691  // { type result; result = *ptr OP value; *ptr = result; return result; }
692  const typet &type = code_type.return_type();
693 
694  const symbol_exprt result =
695  result_symbol(identifier_with_type, type, source_location, symbol_table)
696  .symbol_expr();
697  block.add(codet{ID_decl_block, {code_declt{result}}});
698 
699  // place operations on *ptr in an atomic section
701  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
702  {},
703  code_typet{{}, void_type()},
704  source_location}});
705 
706  // build *ptr
707  const dereference_exprt deref_ptr{parameter_exprs[0]};
708 
709  // build result = *ptr OP arguments[1];
710  irep_idt op_id = identifier == ID___atomic_add_fetch
711  ? ID_plus
712  : identifier == ID___atomic_sub_fetch
713  ? ID_minus
714  : identifier == ID___atomic_or_fetch
715  ? ID_bitor
716  : identifier == ID___atomic_and_fetch
717  ? ID_bitand
718  : identifier == ID___atomic_xor_fetch
719  ? ID_bitxor
720  : identifier == ID___atomic_nand_fetch
721  ? ID_bitnand
722  : ID_nil;
723  binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
724  block.add(code_assignt{result, std::move(op_expr)});
725 
726  block.add(code_assignt{deref_ptr, result});
727 
728  // this instruction implies an mfence, i.e., WRfence
730  symbol_exprt::typeless("__atomic_thread_fence"),
731  {parameter_exprs[2]},
732  typet{},
733  source_location}});
734 
737  {},
738  code_typet{{}, void_type()},
739  source_location}});
740 
741  block.add(code_returnt{result});
742 }
743 
745  const irep_idt &identifier,
746  const irep_idt &identifier_with_type,
747  const code_typet &code_type,
748  const source_locationt &source_location,
749  const std::vector<symbol_exprt> &parameter_exprs,
750  code_blockt &block)
751 {
752  // implement by calling their __atomic_ counterparts with memorder SEQ_CST
753  std::string atomic_name = "__atomic_" + id2string(identifier).substr(7);
754  atomic_name.replace(atomic_name.find("_and_"), 5, "_");
755 
756  exprt::operandst arguments{
757  parameter_exprs[0],
758  parameter_exprs[1],
759  from_integer(std::memory_order_seq_cst, signed_int_type())};
760 
761  block.add(code_returnt{
763  std::move(arguments),
764  typet{},
765  source_location}});
766 }
767 
769  const irep_idt &identifier_with_type,
770  const code_typet &code_type,
771  const source_locationt &source_location,
772  const std::vector<symbol_exprt> &parameter_exprs,
773  code_blockt &block)
774 {
775  // These builtins perform an atomic compare and swap. That is, if the
776  // current value of *ptr is oldval, then write newval into *ptr. The
777  // "bool" version returns true if the comparison is successful and
778  // newval was written. The "val" version returns the contents of *ptr
779  // before the operation.
780 
781  // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
782 
784  symbol_exprt::typeless(ID___atomic_compare_exchange),
785  {parameter_exprs[0],
786  address_of_exprt{parameter_exprs[1]},
787  address_of_exprt{parameter_exprs[2]},
789  from_integer(std::memory_order_seq_cst, signed_int_type()),
790  from_integer(std::memory_order_seq_cst, signed_int_type())},
791  typet{},
792  source_location}});
793 }
794 
796  const irep_idt &identifier_with_type,
797  const code_typet &code_type,
798  const source_locationt &source_location,
799  const std::vector<symbol_exprt> &parameter_exprs,
800  symbol_tablet &symbol_table,
801  code_blockt &block)
802 {
803  // type __sync_val_compare_and_swap(type *ptr, type old, type new, ...)
804  // { type result = *ptr; if(result == old) *ptr = new; return result; }
805  const typet &type = code_type.return_type();
806 
807  const symbol_exprt result =
808  result_symbol(identifier_with_type, type, source_location, symbol_table)
809  .symbol_expr();
810  block.add(codet{ID_decl_block, {code_declt{result}}});
811 
812  // place operations on *ptr in an atomic section
814  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
815  {},
816  code_typet{{}, void_type()},
817  source_location}});
818 
819  // build *ptr
820  const dereference_exprt deref_ptr{parameter_exprs[0]};
821 
822  block.add(code_assignt{result, deref_ptr});
823 
824  code_assignt assign{deref_ptr, parameter_exprs[2]};
825  assign.add_source_location() = source_location;
826  block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]},
827  std::move(assign)});
828 
829  // this instruction implies an mfence, i.e., WRfence
832  {string_constantt{ID_WRfence}},
833  typet{},
834  source_location}});
835 
838  {},
839  code_typet{{}, void_type()},
840  source_location}});
841 
842  block.add(code_returnt{result});
843 }
844 
846  const irep_idt &identifier_with_type,
847  const code_typet &code_type,
848  const source_locationt &source_location,
849  const std::vector<symbol_exprt> &parameter_exprs,
850  symbol_tablet &symbol_table,
851  code_blockt &block)
852 {
853  // type __sync_lock_test_and_set (type *ptr, type value, ...)
854 
855  // This builtin, as described by Intel, is not a traditional
856  // test-and-set operation, but rather an atomic exchange operation.
857  // It writes value into *ptr, and returns the previous contents of
858  // *ptr. Many targets have only minimal support for such locks, and
859  // do not support a full exchange operation. In this case, a target
860  // may support reduced functionality here by which the only valid
861  // value to store is the immediate constant 1. The exact value
862  // actually stored in *ptr is implementation defined.
863  const typet &type = code_type.return_type();
864 
865  const symbol_exprt result =
866  result_symbol(identifier_with_type, type, source_location, symbol_table)
867  .symbol_expr();
868  block.add(codet{ID_decl_block, {code_declt{result}}});
869 
870  // place operations on *ptr in an atomic section
872  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
873  {},
874  code_typet{{}, void_type()},
875  source_location}});
876 
877  // build *ptr
878  const dereference_exprt deref_ptr{parameter_exprs[0]};
879 
880  block.add(code_assignt{result, deref_ptr});
881 
882  block.add(code_assignt{deref_ptr, parameter_exprs[1]});
883 
884  // This built-in function is not a full barrier, but rather an acquire
885  // barrier.
888  {string_constantt{ID_RRfence}, {string_constantt{ID_RRfence}}},
889  typet{},
890  source_location}});
891 
894  {},
895  code_typet{{}, void_type()},
896  source_location}});
897 
898  block.add(code_returnt{result});
899 }
900 
902  const irep_idt &identifier_with_type,
903  const code_typet &code_type,
904  const source_locationt &source_location,
905  const std::vector<symbol_exprt> &parameter_exprs,
906  code_blockt &block)
907 {
908  // void __sync_lock_release (type *ptr, ...)
909 
910  // This built-in function releases the lock acquired by
911  // __sync_lock_test_and_set. Normally this means writing the constant 0 to
912  // *ptr.
913  const typet &type = to_pointer_type(parameter_exprs[0].type()).subtype();
914 
915  // place operations on *ptr in an atomic section
917  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
918  {},
919  code_typet{{}, void_type()},
920  source_location}});
921 
922  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
924  from_integer(0, signed_int_type()), type)});
925 
926  // This built-in function is not a full barrier, but rather a release
927  // barrier.
930  {string_constantt{ID_WRfence}, {string_constantt{ID_WWfence}}},
931  typet{},
932  source_location}});
933 
936  {},
937  code_typet{{}, void_type()},
938  source_location}});
939 }
940 
942  const irep_idt &identifier_with_type,
943  const code_typet &code_type,
944  const source_locationt &source_location,
945  const std::vector<symbol_exprt> &parameter_exprs,
946  code_blockt &block)
947 {
948  // void __atomic_load (type *ptr, type *ret, int memorder)
949  // This is the generic version of an atomic load. It returns the contents of
950  // *ptr in *ret.
951 
953  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
954  {},
955  code_typet{{}, void_type()},
956  source_location}});
957 
958  block.add(code_assignt{dereference_exprt{parameter_exprs[1]},
959  dereference_exprt{parameter_exprs[0]}});
960 
962  symbol_exprt::typeless("__atomic_thread_fence"),
963  {parameter_exprs[2]},
964  typet{},
965  source_location}});
966 
969  {},
970  code_typet{{}, void_type()},
971  source_location}});
972 }
973 
975  const irep_idt &identifier_with_type,
976  const code_typet &code_type,
977  const source_locationt &source_location,
978  const std::vector<symbol_exprt> &parameter_exprs,
979  symbol_tablet &symbol_table,
980  code_blockt &block)
981 {
982  // type __atomic_load_n (type *ptr, int memorder)
983  // This built-in function implements an atomic load operation. It returns
984  // the contents of *ptr.
985  const typet &type = code_type.return_type();
986 
987  const symbol_exprt result =
988  result_symbol(identifier_with_type, type, source_location, symbol_table)
989  .symbol_expr();
990  block.add(codet{ID_decl_block, {code_declt{result}}});
991 
993  symbol_exprt::typeless(ID___atomic_load),
994  {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
995  typet{},
996  source_location}});
997 
998  block.add(code_returnt{result});
999 }
1000 
1002  const irep_idt &identifier_with_type,
1003  const code_typet &code_type,
1004  const source_locationt &source_location,
1005  const std::vector<symbol_exprt> &parameter_exprs,
1006  code_blockt &block)
1007 {
1008  // void __atomic_store (type *ptr, type *val, int memorder)
1009  // This is the generic version of an atomic store. It stores the value of
1010  // *val into *ptr.
1011 
1013  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1014  {},
1015  code_typet{{}, void_type()},
1016  source_location}});
1017 
1018  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1019  dereference_exprt{parameter_exprs[1]}});
1020 
1022  symbol_exprt::typeless("__atomic_thread_fence"),
1023  {parameter_exprs[2]},
1024  typet{},
1025  source_location}});
1026 
1028  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1029  {},
1030  code_typet{{}, void_type()},
1031  source_location}});
1032 }
1033 
1035  const irep_idt &identifier_with_type,
1036  const code_typet &code_type,
1037  const source_locationt &source_location,
1038  const std::vector<symbol_exprt> &parameter_exprs,
1039  code_blockt &block)
1040 {
1041  // void __atomic_store_n (type *ptr, type val, int memorder)
1042  // This built-in function implements an atomic store operation. It writes
1043  // val into *ptr.
1044 
1045  block.add(code_expressiont{
1047  {parameter_exprs[0],
1048  address_of_exprt{parameter_exprs[1]},
1049  parameter_exprs[2]},
1050  typet{},
1051  source_location}});
1052 }
1053 
1055  const irep_idt &identifier_with_type,
1056  const code_typet &code_type,
1057  const source_locationt &source_location,
1058  const std::vector<symbol_exprt> &parameter_exprs,
1059  code_blockt &block)
1060 {
1061  // void __atomic_exchange (type *ptr, type *val, type *ret, int memorder)
1062  // This is the generic version of an atomic exchange. It stores the contents
1063  // of *val into *ptr. The original value of *ptr is copied into *ret.
1064 
1066  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1067  {},
1068  code_typet{{}, void_type()},
1069  source_location}});
1070 
1071  block.add(code_assignt{dereference_exprt{parameter_exprs[2]},
1072  dereference_exprt{parameter_exprs[0]}});
1073  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1074  dereference_exprt{parameter_exprs[1]}});
1075 
1077  symbol_exprt::typeless("__atomic_thread_fence"),
1078  {parameter_exprs[3]},
1079  typet{},
1080  source_location}});
1081 
1083  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1084  {},
1085  code_typet{{}, void_type()},
1086  source_location}});
1087 }
1088 
1090  const irep_idt &identifier_with_type,
1091  const code_typet &code_type,
1092  const source_locationt &source_location,
1093  const std::vector<symbol_exprt> &parameter_exprs,
1094  symbol_tablet &symbol_table,
1095  code_blockt &block)
1096 {
1097  // type __atomic_exchange_n (type *ptr, type val, int memorder)
1098  // This built-in function implements an atomic exchange operation. It writes
1099  // val into *ptr, and returns the previous contents of *ptr.
1100  const typet &type = code_type.return_type();
1101 
1102  const symbol_exprt result =
1103  result_symbol(identifier_with_type, type, source_location, symbol_table)
1104  .symbol_expr();
1105  block.add(codet{ID_decl_block, {code_declt{result}}});
1106 
1108  symbol_exprt::typeless(ID___atomic_exchange),
1109  {parameter_exprs[0],
1110  address_of_exprt{parameter_exprs[1]},
1111  address_of_exprt{result},
1112  parameter_exprs[2]},
1113  typet{},
1114  source_location}});
1115 
1116  block.add(code_returnt{result});
1117 }
1118 
1120  const irep_idt &identifier_with_type,
1121  const code_typet &code_type,
1122  const source_locationt &source_location,
1123  const std::vector<symbol_exprt> &parameter_exprs,
1124  symbol_tablet &symbol_table,
1125  code_blockt &block)
1126 {
1127  // bool __atomic_compare_exchange (type *ptr, type *expected, type *desired,
1128  // bool weak, int success_memorder, int failure_memorder)
1129  // This built-in function implements an atomic compare and exchange
1130  // operation. This compares the contents of *ptr with the contents of
1131  // *expected. If equal, the operation is a read-modify-write operation that
1132  // writes *desired into *ptr. If they are not equal, the operation is a read
1133  // and the current contents of *ptr are written into *expected. weak is true
1134  // for weak compare_exchange, which may fail spuriously, and false for the
1135  // strong variation, which never fails spuriously. Many targets only offer
1136  // the strong variation and ignore the parameter.
1137 
1138  const symbol_exprt result =
1139  result_symbol(
1140  identifier_with_type, c_bool_type(), source_location, symbol_table)
1141  .symbol_expr();
1142  block.add(codet{ID_decl_block, {code_declt{result}}});
1143 
1144  // place operations on *ptr in an atomic section
1146  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1147  {},
1148  code_typet{{}, void_type()},
1149  source_location}});
1150 
1151  // build *ptr
1152  const dereference_exprt deref_ptr{parameter_exprs[0]};
1153 
1154  block.add(code_assignt{
1155  result,
1157  equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}},
1158  result.type())});
1159 
1160  // we never fail spuriously, and ignore parameter_exprs[3]
1161  code_assignt assign{deref_ptr, dereference_exprt{parameter_exprs[2]}};
1162  assign.add_source_location() = source_location;
1164  symbol_exprt::typeless("__atomic_thread_fence"),
1165  {parameter_exprs[4]},
1166  typet{},
1167  source_location}};
1168  success_fence.add_source_location() = source_location;
1169 
1170  code_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]},
1171  deref_ptr};
1172  assign_not_equal.add_source_location() = source_location;
1174  symbol_exprt::typeless("__atomic_thread_fence"),
1175  {parameter_exprs[5]},
1176  typet{},
1177  source_location}};
1178  failure_fence.add_source_location() = source_location;
1179 
1180  block.add(code_ifthenelset{
1181  result,
1182  code_blockt{{std::move(assign), std::move(success_fence)}},
1183  code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1184 
1186  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1187  {},
1188  code_typet{{}, void_type()},
1189  source_location}});
1190 
1191  block.add(code_returnt{result});
1192 }
1193 
1195  const irep_idt &identifier_with_type,
1196  const code_typet &code_type,
1197  const source_locationt &source_location,
1198  const std::vector<symbol_exprt> &parameter_exprs,
1199  code_blockt &block)
1200 {
1201  // bool __atomic_compare_exchange_n (type *ptr, type *expected, type
1202  // desired, bool weak, int success_memorder, int failure_memorder)
1203 
1205  symbol_exprt::typeless(ID___atomic_compare_exchange),
1206  {parameter_exprs[0],
1207  parameter_exprs[1],
1208  address_of_exprt{parameter_exprs[2]},
1209  parameter_exprs[3],
1210  parameter_exprs[4],
1211  parameter_exprs[5]},
1212  typet{},
1213  source_location}});
1214 }
1215 
1217  const irep_idt &identifier,
1218  const symbol_exprt &function_symbol)
1219 {
1220  const irep_idt &identifier_with_type = function_symbol.get_identifier();
1221  const code_typet &code_type = to_code_type(function_symbol.type());
1222  const source_locationt &source_location = function_symbol.source_location();
1223 
1224  std::vector<symbol_exprt> parameter_exprs;
1225  parameter_exprs.reserve(code_type.parameters().size());
1226  for(const auto &parameter : code_type.parameters())
1227  {
1228  parameter_exprs.push_back(lookup(parameter.get_identifier()).symbol_expr());
1229  }
1230 
1231  code_blockt block;
1232 
1233  if(
1234  identifier == ID___atomic_fetch_add ||
1235  identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1236  identifier == ID___atomic_fetch_and ||
1237  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1238  {
1240  identifier,
1241  identifier_with_type,
1242  code_type,
1243  source_location,
1244  parameter_exprs,
1245  symbol_table,
1246  block);
1247  }
1248  else if(
1249  identifier == ID___atomic_add_fetch ||
1250  identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1251  identifier == ID___atomic_and_fetch ||
1252  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1253  {
1255  identifier,
1256  identifier_with_type,
1257  code_type,
1258  source_location,
1259  parameter_exprs,
1260  symbol_table,
1261  block);
1262  }
1263  else if(
1264  identifier == ID___sync_fetch_and_add ||
1265  identifier == ID___sync_fetch_and_sub ||
1266  identifier == ID___sync_fetch_and_or ||
1267  identifier == ID___sync_fetch_and_and ||
1268  identifier == ID___sync_fetch_and_xor ||
1269  identifier == ID___sync_fetch_and_nand ||
1270  identifier == ID___sync_add_and_fetch ||
1271  identifier == ID___sync_sub_and_fetch ||
1272  identifier == ID___sync_or_and_fetch ||
1273  identifier == ID___sync_and_and_fetch ||
1274  identifier == ID___sync_xor_and_fetch ||
1275  identifier == ID___sync_nand_and_fetch)
1276  {
1278  identifier,
1279  identifier_with_type,
1280  code_type,
1281  source_location,
1282  parameter_exprs,
1283  block);
1284  }
1285  else if(identifier == ID___sync_bool_compare_and_swap)
1286  {
1288  identifier_with_type, code_type, source_location, parameter_exprs, block);
1289  }
1290  else if(identifier == ID___sync_val_compare_and_swap)
1291  {
1293  identifier_with_type,
1294  code_type,
1295  source_location,
1296  parameter_exprs,
1297  symbol_table,
1298  block);
1299  }
1300  else if(identifier == ID___sync_lock_test_and_set)
1301  {
1303  identifier_with_type,
1304  code_type,
1305  source_location,
1306  parameter_exprs,
1307  symbol_table,
1308  block);
1309  }
1310  else if(identifier == ID___sync_lock_release)
1311  {
1313  identifier_with_type, code_type, source_location, parameter_exprs, block);
1314  }
1315  else if(identifier == ID___atomic_load)
1316  {
1318  identifier_with_type, code_type, source_location, parameter_exprs, block);
1319  }
1320  else if(identifier == ID___atomic_load_n)
1321  {
1323  identifier_with_type,
1324  code_type,
1325  source_location,
1326  parameter_exprs,
1327  symbol_table,
1328  block);
1329  }
1330  else if(identifier == ID___atomic_store)
1331  {
1333  identifier_with_type, code_type, source_location, parameter_exprs, block);
1334  }
1335  else if(identifier == ID___atomic_store_n)
1336  {
1338  identifier_with_type, code_type, source_location, parameter_exprs, block);
1339  }
1340  else if(identifier == ID___atomic_exchange)
1341  {
1343  identifier_with_type, code_type, source_location, parameter_exprs, block);
1344  }
1345  else if(identifier == ID___atomic_exchange_n)
1346  {
1348  identifier_with_type,
1349  code_type,
1350  source_location,
1351  parameter_exprs,
1352  symbol_table,
1353  block);
1354  }
1355  else if(identifier == ID___atomic_compare_exchange)
1356  {
1358  identifier_with_type,
1359  code_type,
1360  source_location,
1361  parameter_exprs,
1362  symbol_table,
1363  block);
1364  }
1365  else if(identifier == ID___atomic_compare_exchange_n)
1366  {
1368  identifier_with_type, code_type, source_location, parameter_exprs, block);
1369  }
1370  else
1371  {
1372  UNREACHABLE;
1373  }
1374 
1375  for(auto &statement : block.statements())
1376  statement.add_source_location() = source_location;
1377 
1378  return block;
1379 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ANSI-C Language Type Checking.
static void instantiate_atomic_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_fetch_op(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_op_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static void instantiate_atomic_load(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_compare_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
static void instantiate_atomic_load_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static void instantiate_sync_val_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static symbol_exprt typecheck_sync_with_pointer_parameter(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_store(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static void instantiate_atomic_compare_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static symbol_exprt typecheck_atomic_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_lock_test_and_set(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static void instantiate_atomic_fetch_op(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static symbol_exprt typecheck_atomic_op_fetch(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_store_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_bool_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static symbol_exprt typecheck_sync_lock_release(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_load_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static symbol_exprt typecheck_atomic_exchange_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_sync_lock_release(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static void instantiate_atomic_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static void instantiate_sync_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static void instantiate_atomic_store_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
static symbol_exprt typecheck_sync_compare_swap(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
static void instantiate_atomic_compare_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
static symbol_exprt typecheck_atomic_load_store(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
empty_typet void_type()
Definition: c_types.cpp:253
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
typet c_bool_type()
Definition: c_types.cpp:108
Operator to return the address of an object.
Definition: pointer_expr.h:200
A base class for binary expressions.
Definition: std_expr.h:551
symbol_tablet & symbol_table
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
A codet representing an assignment in the program.
Definition: std_code.h:295
A codet representing sequential composition of program statements.
Definition: std_code.h:170
void add(const codet &code)
Definition: std_code.h:208
code_operandst & statements()
Definition: std_code.h:178
A codet representing the declaration of a local variable.
Definition: std_code.h:402
codet representation of an expression statement.
Definition: std_code.h:1842
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
Base type of functions.
Definition: std_types.h:744
std::vector< parametert > parameterst
Definition: std_types.h:746
const typet & return_type() const
Definition: std_types.h:850
const parameterst & parameters() const
Definition: std_types.h:860
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
Operator to dereference a pointer.
Definition: pointer_expr.h:256
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:239
const source_locationt & source_location() const
Definition: expr.h:234
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:407
source_locationt source_location
Definition: message.h:247
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
Expression to hold a symbol (variable)
Definition: std_expr.h:81
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:100
const irep_idt & get_identifier() const
Definition: std_expr.h:110
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
bool is_thread_local
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533