cprover
statement_list_typecheck.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Type Checking
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
14 
15 #include <iostream>
16 
17 #include <util/ieee_float.h>
18 #include <util/message.h>
19 #include <util/namespace.h>
20 #include <util/pointer_expr.h>
21 #include <util/simplify_expr.h>
22 #include <util/std_code.h>
23 #include <util/std_expr.h>
24 #include <util/std_types.h>
25 
27 #define STATEMENT_LIST_PTR_WIDTH 64
28 // TODO: Replace with more specific exception throws.
29 #define TYPECHECK_ERROR 0
30 #define DATA_BLOCK_PARAMETER_NAME "data_block"
32 #define DATA_BLOCK_TYPE_POSTFIX "_db"
34 #define CPROVER_ASSERT CPROVER_PREFIX "assert"
36 #define CPROVER_ASSUME CPROVER_PREFIX "assume"
38 #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
40 
48  const struct_typet &data_block_type,
49  const irep_idt &function_block_name)
50 {
51  const pointer_typet db_ptr{data_block_type, STATEMENT_LIST_PTR_WIDTH};
52  code_typet::parametert param{db_ptr};
53  param.set_identifier(
54  id2string(function_block_name) + "::" + DATA_BLOCK_PARAMETER_NAME);
55  param.set_base_name(DATA_BLOCK_PARAMETER_NAME);
56  return param;
57 }
58 
60  const statement_list_parse_treet &parse_tree,
61  symbol_tablet &symbol_table,
62  const std::string &module,
63  message_handlert &message_handler)
64 {
65  statement_list_typecheckt stl_typecheck(
66  parse_tree, symbol_table, module, message_handler);
67 
68  return stl_typecheck.typecheck_main();
69 }
70 
72  exprt rlo_bit,
73  bool or_bit,
74  codet function_code)
75  : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
76 {
77 }
78 
82  const std::string &module,
87  module(module)
88 {
89 }
90 
92 {
93  // First fill the symbol table with function, tag and parameter declarations
94  // to be able to properly resolve block calls later.
101  // Temporary RLO symbol for certain operations.
102  add_temp_rlo();
103 
104  // Iterate through all networks to generate the function bodies.
107  {
110  }
112  {
113  symbolt &function_sym{symbol_table.get_writeable_ref(fc.name)};
114  typecheck_statement_list_networks(fc, function_sym);
115  }
116 }
117 
119  const statement_list_parse_treet::function_blockt &function_block)
120 {
121  // Create FB symbol.
122  symbolt function_block_sym;
123  function_block_sym.module = module;
124  function_block_sym.name = function_block.name;
125  function_block_sym.base_name = function_block_sym.name;
126  function_block_sym.pretty_name = function_block_sym.name;
127  function_block_sym.mode = ID_statement_list;
128 
129  // When calling function blocks, the passed parameters are value-copied to a
130  // corresponding instance data block. This block contains all input, inout,
131  // output and static variables. The function block reads and writes only
132  // those fields and does not modify the actual parameters. To simulate this
133  // behaviour, all function blocks are modeled as functions with a single
134  // parameter: An instance of their data block, whose members they modify.
135 
136  // Create and add DB type symbol.
137  const struct_typet data_block_type{
138  create_instance_data_block_type(function_block)};
139  type_symbolt data_block{data_block_type};
140  data_block.name =
141  id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX;
142  data_block.base_name = data_block.name;
143  data_block.mode = ID_statement_list;
144  symbol_table.add(data_block);
145 
146  // Create and add parameter symbol.
148  create_data_block_parameter(data_block_type, function_block_sym.name)};
149  parameter_symbolt param_sym;
150  param_sym.module = module;
151  param_sym.type = param.type();
152  param_sym.name = param.get_identifier();
154  param_sym.pretty_name = param_sym.base_name;
155  param_sym.mode = ID_statement_list;
156  symbol_table.add(param_sym);
157 
158  // Setup FB symbol type and value.
160  params.push_back(param);
161  code_typet fb_type{params, empty_typet()};
162  fb_type.set(ID_statement_list_type, ID_statement_list_function_block);
163  function_block_sym.type = fb_type;
164  symbol_table.add(function_block_sym);
165 }
166 
169 {
170  symbolt function_sym;
171  function_sym.module = module;
172  function_sym.name = function.name;
173  function_sym.base_name = function_sym.name;
174  function_sym.pretty_name = function_sym.name;
175  function_sym.mode = ID_statement_list;
178  function.var_input, params, function.name, ID_statement_list_var_input);
180  function.var_inout, params, function.name, ID_statement_list_var_inout);
182  function.var_output, params, function.name, ID_statement_list_var_output);
183 
184  code_typet fc_type{params, function.return_type};
185  fc_type.set(ID_statement_list_type, ID_statement_list_function);
186  function_sym.type = fc_type;
187  symbol_table.add(function_sym);
188 }
189 
191 {
192  for(const symbol_exprt &tag : parse_tree.tags)
193  {
194  symbolt tag_sym;
195  tag_sym.is_static_lifetime = true;
196  tag_sym.module = module;
197  tag_sym.name = tag.get_identifier();
198  tag_sym.base_name = tag_sym.name;
199  tag_sym.pretty_name = tag_sym.name;
200  tag_sym.type = tag.type();
201  tag_sym.mode = ID_statement_list;
202  symbol_table.add(tag_sym);
203  }
204 }
205 
207 {
208  symbolt temp_rlo;
209  temp_rlo.is_static_lifetime = true;
210  temp_rlo.module = module;
211  temp_rlo.name = CPROVER_TEMP_RLO;
212  temp_rlo.base_name = temp_rlo.name;
213  temp_rlo.pretty_name = temp_rlo.name;
214  temp_rlo.type = get_bool_type();
215  temp_rlo.mode = ID_statement_list;
216  symbol_table.add(temp_rlo);
217 }
218 
220  const statement_list_parse_treet::function_blockt &function_block)
221 {
224  function_block.var_input, components, ID_statement_list_var_input);
226  function_block.var_inout, components, ID_statement_list_var_inout);
228  function_block.var_output, components, ID_statement_list_var_output);
230  function_block.var_static, components, ID_statement_list_var_static);
231 
232  return struct_typet{components};
233 }
234 
238  const irep_idt &var_property)
239 {
240  for(const statement_list_parse_treet::var_declarationt &declaration :
241  var_decls)
242  {
243  const irep_idt &var_name{declaration.variable.get_identifier()};
244  const typet &var_type{declaration.variable.type()};
245  struct_union_typet::componentt component{var_name, var_type};
246  component.set(ID_statement_list_type, var_property);
247  components.push_back(component);
248  }
249 }
250 
253  code_typet::parameterst &params,
254  const irep_idt &function_name,
255  const irep_idt &var_property)
256 {
257  for(const statement_list_parse_treet::var_declarationt &declaration :
258  var_decls)
259  {
260  parameter_symbolt param_sym;
261  param_sym.module = module;
262  param_sym.type = declaration.variable.type();
263  param_sym.name = id2string(function_name) +
264  "::" + id2string(declaration.variable.get_identifier());
265  param_sym.base_name = declaration.variable.get_identifier();
266  param_sym.pretty_name = param_sym.base_name;
267  param_sym.mode = ID_statement_list;
268  symbol_table.add(param_sym);
269 
270  code_typet::parametert param{declaration.variable.type()};
271  param.set_identifier(param_sym.name);
272  param.set_base_name(declaration.variable.get_identifier());
273  param.set(ID_statement_list_type, var_property);
274  params.push_back(param);
275  }
276 }
277 
279  const statement_list_parse_treet::tia_modulet &tia_module,
280  symbolt &tia_symbol)
281 {
282  for(const statement_list_parse_treet::var_declarationt &declaration :
283  tia_module.var_temp)
284  {
285  symbolt temp_sym;
286  temp_sym.name = id2string(tia_symbol.name) +
287  "::" + id2string(declaration.variable.get_identifier());
288  temp_sym.base_name = declaration.variable.get_identifier();
289  temp_sym.pretty_name = temp_sym.base_name;
290  temp_sym.type = declaration.variable.type();
291  temp_sym.mode = ID_statement_list;
292  temp_sym.module = module;
293  symbol_table.add(temp_sym);
294 
295  const code_declt code_decl{temp_sym.symbol_expr()};
296  tia_symbol.value.add_to_operands(code_decl);
297  }
298 }
299 
301  const statement_list_parse_treet::tia_modulet &tia_module,
302  symbolt &tia_symbol)
303 {
304  // Leave value empty if there are no networks to iterate through.
305  if(tia_module.networks.empty())
306  return;
307  if(tia_symbol.value.is_nil())
308  tia_symbol.value = code_blockt{};
309 
310  typecheck_temp_var_decls(tia_module, tia_symbol);
311 
312  for(const auto &network : tia_module.networks)
313  {
314  // Set RLO to true each time a new network is entered (TIA behaviour).
315  rlo_bit = true_exprt();
316  for(const auto &instruction : network.instructions)
317  typecheck_statement_list_instruction(instruction, tia_symbol);
318  }
319 }
320 
322  const statement_list_parse_treet::instructiont &instruction,
323  symbolt &tia_element)
324 {
325  const codet &op_code{instruction.tokens.back()};
326  const irep_idt statement{op_code.get_statement()};
327 
328  if(ID_statement_list_load == statement)
329  typecheck_statement_list_load(op_code, tia_element);
330  else if(ID_statement_list_transfer == statement)
331  typecheck_statement_list_transfer(op_code, tia_element);
332  else if(ID_statement_list_accu_int_add == statement)
334  else if(ID_statement_list_accu_int_sub == statement)
336  else if(ID_statement_list_accu_int_mul == statement)
338  else if(ID_statement_list_accu_int_div == statement)
340  else if(ID_statement_list_accu_int_eq == statement)
342  else if(ID_statement_list_accu_int_neq == statement)
344  else if(ID_statement_list_accu_int_lt == statement)
346  else if(ID_statement_list_accu_int_gt == statement)
348  else if(ID_statement_list_accu_int_lte == statement)
350  else if(ID_statement_list_accu_int_gte == statement)
352  else if(ID_statement_list_accu_dint_add == statement)
354  else if(ID_statement_list_accu_dint_sub == statement)
356  else if(ID_statement_list_accu_dint_mul == statement)
358  else if(ID_statement_list_accu_dint_div == statement)
360  else if(ID_statement_list_accu_dint_eq == statement)
362  else if(ID_statement_list_accu_dint_neq == statement)
364  else if(ID_statement_list_accu_dint_lt == statement)
366  else if(ID_statement_list_accu_dint_gt == statement)
368  else if(ID_statement_list_accu_dint_lte == statement)
370  else if(ID_statement_list_accu_dint_gte == statement)
372  else if(ID_statement_list_accu_real_add == statement)
374  else if(ID_statement_list_accu_real_sub == statement)
376  else if(ID_statement_list_accu_real_mul == statement)
378  else if(ID_statement_list_accu_real_div == statement)
380  else if(ID_statement_list_accu_real_eq == statement)
382  else if(ID_statement_list_accu_real_neq == statement)
384  else if(ID_statement_list_accu_real_lt == statement)
386  else if(ID_statement_list_accu_real_gt == statement)
388  else if(ID_statement_list_accu_real_lte == statement)
390  else if(ID_statement_list_accu_real_gte == statement)
392  else if(ID_statement_list_not == statement)
394  else if(ID_statement_list_and == statement)
395  typecheck_statement_list_and(op_code, tia_element);
396  else if(ID_statement_list_and_not == statement)
397  typecheck_statement_list_and_not(op_code, tia_element);
398  else if(ID_statement_list_or == statement)
399  typecheck_statement_list_or(op_code, tia_element);
400  else if(ID_statement_list_or_not == statement)
401  typecheck_statement_list_or_not(op_code, tia_element);
402  else if(ID_statement_list_xor == statement)
403  typecheck_statement_list_xor(op_code, tia_element);
404  else if(ID_statement_list_xor_not == statement)
405  typecheck_statement_list_xor_not(op_code, tia_element);
406  else if(ID_statement_list_and_nested == statement)
408  else if(ID_statement_list_and_not_nested == statement)
410  else if(ID_statement_list_or_nested == statement)
412  else if(ID_statement_list_or_not_nested == statement)
414  else if(ID_statement_list_xor_nested == statement)
416  else if(ID_statement_list_xor_not_nested == statement)
418  else if(ID_statement_list_nesting_closed == statement)
420  else if(ID_statement_list_assign == statement)
421  typecheck_statement_list_assign(op_code, tia_element);
422  else if(ID_statement_list_set_rlo == statement)
424  else if(ID_statement_list_clr_rlo == statement)
426  else if(ID_statement_list_set == statement)
427  typecheck_statement_list_set(op_code, tia_element);
428  else if(ID_statement_list_reset == statement)
429  typecheck_statement_list_reset(op_code, tia_element);
430  else if(ID_statement_list_nop == statement)
431  return;
432  else if(ID_statement_list_call == statement)
433  typecheck_statement_list_call(op_code, tia_element);
434  else
435  {
436  error() << "OP code of instruction not found: " << op_code.get_statement()
437  << eom;
438  throw TYPECHECK_ERROR;
439  }
440 }
441 
443  const codet &op_code,
444  const symbolt &tia_element)
445 {
446  const symbol_exprt *const symbol =
447  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
448  if(symbol)
449  {
450  const irep_idt &identifier{symbol->get_identifier()};
451  const exprt val{typecheck_identifier(tia_element, identifier)};
452  accumulator.push_back(val);
453  }
454  else if(can_cast_expr<constant_exprt>(op_code.op0()))
455  accumulator.push_back(op_code.op0());
456  else
457  {
458  error() << "Instruction is not followed by symbol or constant" << eom;
459  throw TYPECHECK_ERROR;
460  }
461 }
462 
464  const codet &op_code,
465  symbolt &tia_element)
466 {
468  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
469  if(lhs.type() != accumulator.back().type())
470  {
471  error() << "Types of transfer assignment do not match" << eom;
472  throw TYPECHECK_ERROR;
473  }
474  const code_assignt assignment{lhs, accumulator.back()};
475  tia_element.value.add_to_operands(assignment);
476 }
477 
479  const codet &op_code)
480 {
482 
483  // Pop first operand, peek second.
484  const exprt accu1{accumulator.back()};
485  accumulator.pop_back();
486  const exprt &accu2{accumulator.back()};
487  const plus_exprt operation{accu2, accu1};
488  accumulator.push_back(operation);
489 }
490 
492  const codet &op_code)
493 {
495 
496  // Pop first operand, peek second.
497  const exprt accu1{accumulator.back()};
498  accumulator.pop_back();
499  const exprt &accu2{accumulator.back()};
500  const minus_exprt operation{accu2, accu1};
501  accumulator.push_back(operation);
502 }
503 
505  const codet &op_code)
506 {
508 
509  // Pop first operand, peek second.
510  const exprt accu1{accumulator.back()};
511  accumulator.pop_back();
512  const exprt &accu2{accumulator.back()};
513  const mult_exprt operation{accu2, accu1};
514  accumulator.push_back(operation);
515 }
516 
518  const codet &op_code)
519 {
521 
522  // Pop first operand, peek second.
523  const exprt accu1{accumulator.back()};
524  accumulator.pop_back();
525  const exprt &accu2{accumulator.back()};
526  const div_exprt operation{accu2, accu1};
527  accumulator.push_back(operation);
528 }
529 
531  const codet &op_code)
532 {
535 }
536 
538  const codet &op_code)
539 {
542 }
543 
545  const codet &op_code)
546 {
549 }
550 
552  const codet &op_code)
553 {
556 }
557 
559  const codet &op_code)
560 {
563 }
564 
566  const codet &op_code)
567 {
570 }
571 
573  const codet &op_code)
574 {
576 
577  // Pop first operand, peek second.
578  const exprt accu1{accumulator.back()};
579  accumulator.pop_back();
580  const exprt &accu2{accumulator.back()};
581  const plus_exprt operation{accu2, accu1};
582  accumulator.push_back(operation);
583 }
584 
586  const codet &op_code)
587 {
589 
590  // Pop first operand, peek second.
591  const exprt accu1{accumulator.back()};
592  accumulator.pop_back();
593  const exprt &accu2{accumulator.back()};
594  const minus_exprt operation{accu2, accu1};
595  accumulator.push_back(operation);
596 }
597 
599  const codet &op_code)
600 {
602 
603  // Pop first operand, peek second.
604  const exprt accu1{accumulator.back()};
605  accumulator.pop_back();
606  const exprt &accu2{accumulator.back()};
607  const mult_exprt operation{accu2, accu1};
608  accumulator.push_back(operation);
609 }
610 
612  const codet &op_code)
613 {
615 
616  // Pop first operand, peek second.
617  const exprt accu1{accumulator.back()};
618  accumulator.pop_back();
619  const exprt &accu2{accumulator.back()};
620  const div_exprt operation{accu2, accu1};
621  accumulator.push_back(operation);
622 }
623 
625  const codet &op_code)
626 {
629 }
630 
632  const codet &op_code)
633 {
636 }
637 
639  const codet &op_code)
640 {
643 }
644 
646  const codet &op_code)
647 {
650 }
651 
653  const codet &op_code)
654 {
657 }
658 
660  const codet &op_code)
661 {
664 }
665 
667  const codet &op_code)
668 {
670 
671  // Pop first operand, peek second.
672  const exprt accu1{accumulator.back()};
673  accumulator.pop_back();
674  const exprt &accu2{accumulator.back()};
675  const plus_exprt operation{accu2, accu1};
676  accumulator.push_back(operation);
677 }
678 
680  const codet &op_code)
681 {
683 
684  // Pop first operand, peek second.
685  const exprt accu1{accumulator.back()};
686  accumulator.pop_back();
687  const exprt &accu2{accumulator.back()};
688  const minus_exprt operation{accu2, accu1};
689  accumulator.push_back(operation);
690 }
691 
693  const codet &op_code)
694 {
696 
697  // Pop first operand, peek second.
698  const exprt accu1{accumulator.back()};
699  accumulator.pop_back();
700  const exprt &accu2{accumulator.back()};
701  const mult_exprt operation{accu2, accu1};
702  accumulator.push_back(operation);
703 }
704 
706  const codet &op_code)
707 {
709 
710  // Pop first operand, peek second.
711  const exprt accu1{accumulator.back()};
712  accumulator.pop_back();
713  const exprt &accu2{accumulator.back()};
714  const div_exprt operation{accu2, accu1};
715  accumulator.push_back(operation);
716 }
717 
719  const codet &op_code)
720 {
723 }
724 
726  const codet &op_code)
727 {
730 }
731 
733  const codet &op_code)
734 {
737 }
738 
740  const codet &op_code)
741 {
744 }
745 
747  const codet &op_code)
748 {
751 }
752 
754  const codet &op_code)
755 {
758 }
759 
761  const codet &op_code)
762 {
764  if(fc_bit)
765  {
766  const not_exprt unsimplified{rlo_bit};
767  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
768  or_bit = false;
769  }
770  else
772 }
773 
775  const codet &op_code,
776  const symbolt &tia_element)
777 {
778  exprt op{
779  typecheck_simple_boolean_instruction_operand(op_code, tia_element, false)};
780 
781  // If inside of a bit string and if the OR bit is not set, create an 'and'
782  // expression with the operand and the current contents of the rlo bit. If
783  // the OR bit is set then this instruction is part of an 'and-before-or'
784  // block and needs to be added to the rlo in a special way.
785  if(fc_bit && or_bit)
787  else if(fc_bit)
788  {
789  const and_exprt unsimplified{rlo_bit, op};
790  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
791  }
792  else
794 }
795 
797  const codet &op_code,
798  const symbolt &tia_element)
799 {
800  exprt op{
801  typecheck_simple_boolean_instruction_operand(op_code, tia_element, true)};
802 
803  // If inside of a bit string and if the OR bit is not set, create an 'and'
804  // expression with the operand and the current contents of the rlo bit. If
805  // the OR bit is set then this instruction is part of an 'and-before-or'
806  // block and needs to be added to the rlo in a special way.
807  if(or_bit && fc_bit)
809  else if(fc_bit)
810  {
811  const and_exprt unsimplified{rlo_bit, op};
812  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
813  }
814  else
816 }
817 
819  const codet &op_code,
820  const symbolt &tia_element)
821 {
822  if(op_code.operands().empty())
823  {
825  return;
826  }
827  const symbol_exprt &sym{
829  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
830 
831  // If inside of a bit string, create an 'or' expression with the operand and
832  // the current contents of the rlo bit.
833  if(fc_bit)
834  {
835  const or_exprt unsimplified{rlo_bit, op};
836  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
837  or_bit = false;
838  }
839  else
841 }
842 
844  const codet &op_code,
845  const symbolt &tia_element)
846 {
847  const symbol_exprt &sym{
849  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
850  const not_exprt not_op{op};
851 
852  // If inside of a bit string, create an 'or' expression with the operand and
853  // the current contents of the rlo bit.
854  if(fc_bit)
855  {
856  const or_exprt unsimplified{rlo_bit, not_op};
857  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
858  or_bit = false;
859  }
860  else
862 }
863 
865  const codet &op_code,
866  const symbolt &tia_element)
867 {
868  const symbol_exprt &sym{
870  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
871 
872  // If inside of a bit string, create an 'xor' expression with the operand and
873  // the current contents of the rlo bit.
874  if(fc_bit)
875  {
876  const xor_exprt unsimplified{rlo_bit, op};
877  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
878  or_bit = false;
879  }
880  else
882 }
883 
885  const codet &op_code,
886  const symbolt &tia_element)
887 {
888  const symbol_exprt &sym{
890  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
891  const not_exprt not_op{op};
892 
893  // If inside of a bit string, create an 'xor not' expression with the
894  // operand and the current contents of the rlo bit.
895  if(fc_bit)
896  {
897  const xor_exprt unsimplified{rlo_bit, not_op};
898  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
899  or_bit = false;
900  }
901  else
903 }
904 
906 {
907  if(fc_bit)
908  {
910  or_bit = true;
911  }
912  else
913  return; // Instruction has no semantic influence.
914 }
915 
917  const codet &op_code)
918 {
919  // Set the rlo to true implicitly so that the value of the AND instruction
920  // is being loaded in case of a new bit string.
922 }
923 
925  const codet &op_code)
926 {
927  // Set the rlo to true implicitly so that the value of the AND instruction
928  // is being loaded in case of a new bit string.
930 }
931 
933  const codet &op_code)
934 {
935  // Set the rlo to false implicitly so that the value of the OR instruction
936  // is being loaded in case of a new bit string.
938 }
939 
941  const codet &op_code)
942 {
943  // Set the rlo to false implicitly so that the value of the OR instruction
944  // is being loaded in case of a new bit string.
946 }
947 
949  const codet &op_code)
950 {
951  // Set the rlo to false implicitly so that the value of the XOR instruction
952  // is being loaded in case of a new bit string.
954 }
955 
957  const codet &op_code)
958 {
959  // Set the rlo to false implicitly so that the value of the XOR instruction
960  // is being loaded in case of a new bit string.
962 }
963 
965  const codet &op_code)
966 {
968  if(nesting_stack.empty())
969  {
970  error() << "Wrong order of brackets (Right parenthesis is not preceded by "
971  "nesting)"
972  << eom;
973  throw TYPECHECK_ERROR;
974  }
975  or_bit = nesting_stack.back().or_bit;
976  fc_bit = true;
977  const irep_idt &statement{nesting_stack.back().function_code.get_statement()};
978  if(ID_statement_list_and_nested == statement)
979  {
980  if(or_bit)
981  {
982  const exprt op{rlo_bit};
983  rlo_bit = nesting_stack.back().rlo_bit;
985  }
986  else
987  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, rlo_bit};
988  }
989  else if(ID_statement_list_and_not_nested == statement)
990  {
991  if(or_bit)
992  {
993  const not_exprt op{rlo_bit};
994  rlo_bit = nesting_stack.back().rlo_bit;
996  }
997  else
998  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
999  }
1000  else if(ID_statement_list_or_nested == statement)
1001  {
1002  or_bit = false;
1003  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1004  }
1005  else if(ID_statement_list_or_not_nested == statement)
1006  {
1007  or_bit = false;
1008  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1009  }
1010  else if(ID_statement_list_xor_nested == statement)
1011  {
1012  or_bit = false;
1013  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1014  }
1015  else if(ID_statement_list_xor_not_nested == statement)
1016  {
1017  or_bit = false;
1018  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1019  }
1020  nesting_stack.pop_back();
1021 }
1022 
1024  const codet &op_code,
1025  symbolt &tia_element)
1026 {
1028  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
1029 
1030  if(lhs.type() != rlo_bit.type())
1031  {
1032  error() << "Types of assign do not match" << eom;
1033  throw TYPECHECK_ERROR;
1034  }
1035  const code_assignt assignment{lhs, rlo_bit};
1036  tia_element.value.add_to_operands(assignment);
1037  fc_bit = false;
1038  or_bit = false;
1039  // Set RLO to assigned operand in order to prevent false results if a symbol
1040  // that's implicitly part of the RLO was changed by the assignment.
1041  rlo_bit = lhs;
1042 }
1043 
1045  const codet &op_code)
1046 {
1048  fc_bit = false;
1049  or_bit = false;
1050  rlo_bit = true_exprt();
1051 }
1052 
1054  const codet &op_code)
1055 {
1057  fc_bit = false;
1058  or_bit = false;
1059  rlo_bit = false_exprt();
1060 }
1061 
1063  const codet &op_code,
1064  symbolt &tia_element)
1065 {
1067  const irep_idt &identifier{op.get_identifier()};
1068 
1069  save_rlo_state(tia_element);
1070 
1071  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1072  const code_assignt assignment{lhs, true_exprt()};
1073  const code_ifthenelset ifthen{rlo_bit, assignment};
1074  tia_element.value.add_to_operands(ifthen);
1075  fc_bit = false;
1076  or_bit = false;
1077 }
1078 
1080  const codet &op_code,
1081  symbolt &tia_element)
1082 {
1084  const irep_idt &identifier{op.get_identifier()};
1085 
1086  save_rlo_state(tia_element);
1087 
1088  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1089  const code_assignt assignment{lhs, false_exprt()};
1090  const code_ifthenelset ifthen{rlo_bit, assignment};
1091  tia_element.value.add_to_operands(ifthen);
1092  fc_bit = false;
1093  or_bit = false;
1094 }
1095 
1097  const codet &op_code,
1098  symbolt &tia_element)
1099 {
1101  const irep_idt &identifier{op.get_identifier()};
1102  if(symbol_table.has_symbol(identifier))
1103  typecheck_called_tia_element(op_code, tia_element);
1104  else if(identifier == CPROVER_ASSUME)
1105  typecheck_CPROVER_assume(op_code, tia_element);
1106  else if(identifier == CPROVER_ASSERT)
1107  typecheck_CPROVER_assert(op_code, tia_element);
1108  else
1109  {
1110  error() << "Called function could not be found" << eom;
1111  throw TYPECHECK_ERROR;
1112  }
1113  fc_bit = false;
1114  or_bit = false;
1115 }
1116 
1118  const codet &op_code)
1119 {
1121  const exprt &accu1{accumulator.back()};
1122  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1123 
1124  // Are both operands integers?
1125  const signedbv_typet *const accu_type1 =
1126  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1127  const signedbv_typet *const accu_type2 =
1128  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1129  if(
1130  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_INT_WIDTH ||
1131  accu_type2->get_width() != STL_INT_WIDTH)
1132  {
1133  error() << "Operands of integer addition are no integers" << eom;
1134  throw TYPECHECK_ERROR;
1135  }
1136 }
1137 
1139  const codet &op_code)
1140 {
1142  const exprt &accu1{accumulator.back()};
1143  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1144 
1145  // Are both operands double integers?
1146  const signedbv_typet *const accu_type1 =
1147  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1148  const signedbv_typet *const accu_type2 =
1149  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1150  if(
1151  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_DINT_WIDTH ||
1152  accu_type2->get_width() != STL_DINT_WIDTH)
1153  {
1154  error() << "Operands of double integer addition are no double integers"
1155  << eom;
1156  throw TYPECHECK_ERROR;
1157  }
1158 }
1159 
1161  const codet &op_code)
1162 {
1164  const exprt &accu1{accumulator.back()};
1165  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1166 
1167  // Are both operands real types?
1168  if(!(can_cast_type<floatbv_typet>(accu1.type()) &&
1169  can_cast_type<floatbv_typet>(accu2.type())))
1170  {
1171  error() << "Operands of Real addition do not have the type Real" << eom;
1172  throw TYPECHECK_ERROR;
1173  }
1174 }
1175 
1177  const irep_idt &comparison)
1178 {
1179  const exprt &accu1{accumulator.back()};
1180  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1181  // STL behaviour: ACCU2 is lhs, ACCU1 is rhs.
1182  const binary_relation_exprt operation{accu2, comparison, accu1};
1183  rlo_bit = operation;
1184 }
1185 
1186 const symbol_exprt &
1188  const codet &op_code)
1189 {
1190  const symbol_exprt *const symbol =
1191  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
1192 
1193  if(symbol)
1194  return *symbol;
1195 
1196  error() << "Instruction is not followed by symbol" << eom;
1197  throw TYPECHECK_ERROR;
1198 }
1199 
1201  const codet &op_code)
1202 {
1203  if(op_code.operands().size() > 0)
1204  {
1205  error() << "Instruction is followed by operand" << eom;
1206  throw TYPECHECK_ERROR;
1207  }
1208 }
1209 
1211  const codet &op_code)
1212 {
1214  if(accumulator.size() < 2)
1215  {
1216  error() << "Not enough operands in the accumulator" << eom;
1217  throw TYPECHECK_ERROR;
1218  }
1219 }
1220 
1222  const codet &op_code,
1223  const exprt &rlo_value)
1224 {
1226  // If inside of a bit string use the value of the rlo. If this is the first
1227  // expression of a bit string, load the value of the nested operation by
1228  // implicitly setting the rlo to the specified value.
1229  if(!fc_bit)
1230  rlo_bit = rlo_value;
1231  const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code};
1232  nesting_stack.push_back(stack_entry);
1233  fc_bit = false;
1234  or_bit = false;
1235 }
1236 
1238  const codet &op_code,
1239  const symbolt &tia_element,
1240  bool negate)
1241 {
1242  const symbol_exprt &sym{
1244  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1245  const not_exprt not_op{op};
1246  return negate ? not_op : op;
1247 }
1248 
1250  const symbolt &tia_element,
1251  const irep_idt &identifier)
1252 {
1253  const code_typet &element_type{to_code_type(tia_element.type)};
1254 
1255  // Check for temporary variables.
1257  id2string(tia_element.name) + "::" + id2string(identifier)))
1258  {
1259  const symbolt &sym{symbol_table.lookup_ref(
1260  id2string(tia_element.name) + "::" + id2string(identifier))};
1261  return sym.symbol_expr();
1262  }
1263 
1264  // Check for global tags.
1265  if(symbol_table.has_symbol(identifier))
1266  return symbol_table.lookup_ref(identifier).symbol_expr();
1267 
1268  if(
1269  element_type.get(ID_statement_list_type) ==
1270  ID_statement_list_function_block)
1271  {
1272  // Check for variables inside of the function block interface.
1273  const symbolt &data_block{symbol_table.get_writeable_ref(
1274  id2string(tia_element.name) + "::" + DATA_BLOCK_PARAMETER_NAME)};
1275  const symbol_exprt db_expr = data_block.symbol_expr();
1276  const struct_typet *const db_type =
1277  type_try_dynamic_cast<struct_typet>(db_expr.type().subtype());
1278  if(!db_type)
1279  UNREACHABLE;
1280  for(const struct_union_typet::componentt &member : db_type->components())
1281  {
1282  if(member.get_name() == identifier)
1283  {
1284  const dereference_exprt deref_db{db_expr};
1285  const member_exprt val{deref_db, member.get_name(), member.type()};
1286  return val;
1287  }
1288  }
1289  }
1290  else if(
1291  element_type.get(ID_statement_list_type) == ID_statement_list_function)
1292  {
1293  // Check for variables inside of the function interface.
1294  for(const auto &member : element_type.parameters())
1295  {
1296  if(member.get_base_name() == identifier)
1297  {
1298  const symbolt &par{
1299  symbol_table.get_writeable_ref(member.get_identifier())};
1300  return par.symbol_expr();
1301  }
1302  }
1303  }
1304  else
1305  UNREACHABLE; // Variable declarations should only be checked for FCs or FBs
1306 
1307  error() << "Identifier could not be found in project" << eom;
1308  throw TYPECHECK_ERROR;
1309 }
1310 
1312  const codet &op_code,
1313  symbolt &tia_element)
1314 {
1315  const equal_exprt *const assignment =
1316  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1317  if(assignment)
1318  {
1319  const code_assertt assertion{
1320  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1321  tia_element.value.add_to_operands(assertion);
1322  }
1323  else
1324  {
1325  error() << "No assignment found for assertion" << eom;
1326  throw TYPECHECK_ERROR;
1327  }
1328 }
1329 
1331  const codet &op_code,
1332  symbolt &tia_element)
1333 {
1334  const equal_exprt *const assignment =
1335  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1336  if(assignment)
1337  {
1338  const code_assumet assumption{
1339  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1340  tia_element.value.add_to_operands(assumption);
1341  }
1342  else
1343  {
1344  error() << "No assignment found for assumption" << eom;
1345  throw TYPECHECK_ERROR;
1346  }
1347 }
1348 
1350  const codet &op_code,
1351  symbolt &tia_element)
1352 {
1353  const symbol_exprt &call_operand{to_symbol_expr(op_code.op0())};
1354  const symbolt &called_function{
1355  symbol_table.lookup_ref(call_operand.get_identifier())};
1356  const code_typet &called_type{to_code_type(called_function.type)};
1357  // Is it a STL function or STL function block?
1358  if(
1359  called_type.get(ID_statement_list_type) == ID_statement_list_function_block)
1360  typecheck_called_function_block(op_code, tia_element);
1361  else if(called_type.get(ID_statement_list_type) == ID_statement_list_function)
1362  typecheck_called_function(op_code, tia_element);
1363  else
1364  {
1365  error() << "Tried to call element that is no function or function block"
1366  << eom;
1367  throw TYPECHECK_ERROR;
1368  }
1369 }
1370 
1372  const codet &op_code,
1373  symbolt &tia_element)
1374 {
1375  const symbol_exprt call_operand{to_symbol_expr(op_code.op0())};
1376  const symbolt &called_function_sym{
1377  symbol_table.lookup_ref(call_operand.get_identifier())};
1378  const symbol_exprt called_function_expr{called_function_sym.symbol_expr()};
1379  const code_typet &called_type{to_code_type(called_function_sym.type)};
1380 
1381  // Check if function name is followed by data block.
1382  if(!can_cast_expr<equal_exprt>(op_code.op1()))
1383  {
1384  error() << "Function calls should not address instance data blocks" << eom;
1385  throw TYPECHECK_ERROR;
1386  }
1387 
1388  // Check if function interface matches the call and fill argument list.
1389  const code_typet::parameterst &params{called_type.parameters()};
1391  std::vector<equal_exprt> assignments;
1392  for(const auto &expr : op_code.operands())
1393  {
1394  if(can_cast_expr<equal_exprt>(expr))
1395  assignments.push_back(to_equal_expr(expr));
1396  }
1397 
1398  for(const code_typet::parametert &param : params)
1399  args.emplace_back(
1400  typecheck_function_call_arguments(assignments, param, tia_element));
1401 
1402  // Check the return value if present.
1403  if(called_type.return_type().is_nil())
1404  tia_element.value.add_to_operands(
1405  code_function_callt{called_function_expr, args});
1406  else
1407  {
1409  assignments, called_type.return_type(), tia_element)};
1410  tia_element.value.add_to_operands(
1411  code_function_callt{lhs, called_function_expr, args});
1412  }
1413 }
1414 
1416  const codet &op_code,
1417  symbolt &tia_element)
1418 {
1419  // TODO: Implement support for function block calls.
1420  // Needs code statements which assign the parameters to the instance data
1421  // block, call the function and write the result back to the parameters
1422  // afterwards.
1423  error() << "Calls to function blocks are not supported yet" << eom;
1424  throw TYPECHECK_ERROR;
1425 }
1426 
1428  const std::vector<equal_exprt> &assignments,
1429  const code_typet::parametert &param,
1430  const symbolt &tia_element)
1431 {
1432  const irep_idt &param_name = param.get_base_name();
1433  const typet &param_type = param.type();
1434  for(const equal_exprt &assignment : assignments)
1435  {
1436  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1437  if(param_name == lhs.get_identifier())
1438  {
1439  exprt assigned_variable{
1440  typecheck_function_call_argument_rhs(tia_element, assignment.rhs())};
1441 
1442  if(param_type == assigned_variable.type())
1443  return assigned_variable;
1444  else
1445  {
1446  error() << "Types of parameter assignment do not match: "
1447  << param.type().id() << " != " << assigned_variable.type().id()
1448  << eom;
1449  throw TYPECHECK_ERROR;
1450  }
1451  }
1452  }
1453  error() << "No assignment found for function parameter "
1454  << param.get_identifier() << eom;
1455  throw TYPECHECK_ERROR;
1456 }
1457 
1459  const symbolt &tia_element,
1460  const exprt &rhs)
1461 {
1462  exprt assigned_operand;
1463  const symbol_exprt *const symbol_rhs =
1464  expr_try_dynamic_cast<symbol_exprt>(rhs);
1465  if(symbol_rhs)
1466  assigned_operand =
1467  typecheck_identifier(tia_element, symbol_rhs->get_identifier());
1468  else // constant_exprt.
1469  assigned_operand = rhs;
1470  return assigned_operand;
1471 }
1472 
1474  const std::vector<equal_exprt> &assignments,
1475  const typet &return_type,
1476  const symbolt &tia_element)
1477 {
1478  for(const equal_exprt &assignment : assignments)
1479  {
1480  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1481  if(ID_statement_list_return_value_id == lhs.get_identifier())
1482  {
1483  const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())};
1484  const exprt assigned_variable{
1485  typecheck_identifier(tia_element, rhs.get_identifier())};
1486  if(return_type == assigned_variable.type())
1487  return assigned_variable;
1488  else
1489  {
1490  error() << "Types of return value assignment do not match: "
1491  << return_type.id() << " != " << assigned_variable.type().id()
1492  << eom;
1493  throw TYPECHECK_ERROR;
1494  }
1495  }
1496  }
1497  error() << "No assignment found for function return value" << eom;
1498  throw TYPECHECK_ERROR;
1499 }
1500 
1502 {
1503  or_exprt or_wrapper{to_or_expr(rlo_bit)};
1504 
1505  if(can_cast_expr<constant_exprt>(or_wrapper.op1()))
1506  or_wrapper.op1();
1507  else if(can_cast_expr<and_exprt>(or_wrapper.op1()))
1508  {
1509  and_exprt &and_op{to_and_expr(or_wrapper.op1())};
1510  and_op.add_to_operands(op);
1511  or_wrapper.op1() = and_op;
1512  }
1513  else
1514  {
1515  and_exprt and_op{or_wrapper.op1(), op};
1516  or_wrapper.op1() = and_op;
1517  }
1518  rlo_bit = or_wrapper;
1519 }
1520 
1522 {
1523  fc_bit = true;
1524  or_bit = false;
1525  rlo_bit = op;
1526 }
1527 
1529 {
1530  symbol_exprt temp_rlo{
1532  const code_assignt rlo_assignment{temp_rlo, rlo_bit};
1533  tia_element.value.add_to_operands(rlo_assignment);
1534  rlo_bit = std::move(temp_rlo);
1535 }
statement_list_typecheckt::create_instance_data_block_type
struct_typet create_instance_data_block_type(const statement_list_parse_treet::function_blockt &function_block)
Creates a data block type for the given function block.
Definition: statement_list_typecheck.cpp:219
statement_list_typecheckt::typecheck_statement_list_nested_and_not
void typecheck_statement_list_nested_and_not(const codet &op_code)
Performs a typecheck on a nested And Not instruction.
Definition: statement_list_typecheck.cpp:924
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
statement_list_typecheckt::typecheck_statement_list_and_not
void typecheck_statement_list_and_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And Not instruction.
Definition: statement_list_typecheck.cpp:796
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
statement_list_typecheckt::typecheck_statement_list_reset
void typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL 'R' instruction and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1079
typet::subtype
const typet & subtype() const
Definition: type.h:47
statement_list_typecheckt::typecheck_statement_list_and_before_or
void typecheck_statement_list_and_before_or()
Performs a typecheck on a STL operand-less Or instruction.
Definition: statement_list_typecheck.cpp:905
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
statement_list_typecheckt::typecheck_statement_list_accu_int_arith
void typecheck_statement_list_accu_int_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for integers.
Definition: statement_list_typecheck.cpp:1117
statement_list_typecheckt::typecheck_statement_list_accu_int_gt
void typecheck_statement_list_accu_int_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for integers.
Definition: statement_list_typecheck.cpp:551
statement_list_typecheck.h
Statement List Language Type Checking.
STL_DINT_WIDTH
#define STL_DINT_WIDTH
Definition: statement_list_types.h:16
codet::op0
exprt & op0()
Definition: expr.h:103
statement_list_parse_treet::tia_modulet::networks
networkst networks
List of all networks of this module.
Definition: statement_list_parse_tree.h:99
statement_list_typecheckt::typecheck_statement_list_not
void typecheck_statement_list_not(const codet &op_code)
Performs a typecheck on a STL boolean NOT instruction.
Definition: statement_list_typecheck.cpp:760
statement_list_typecheckt::typecheck_CPROVER_assert
void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a call of __CPOVER_ASSERT and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1311
statement_list_typecheckt::module
const irep_idt module
Name of the module this typecheck belongs to.
Definition: statement_list_typecheck.h:66
statement_list_typecheckt::typecheck_statement_list_nested_or_not
void typecheck_statement_list_nested_or_not(const codet &op_code)
Performs a typecheck on a nested Or Not instruction.
Definition: statement_list_typecheck.cpp:940
statement_list_parse_treet::var_declarationst
std::list< var_declarationt > var_declarationst
Definition: statement_list_parse_tree.h:40
statement_list_typecheckt::typecheck_statement_list_call
void typecheck_statement_list_call(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL Call instruction and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1096
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
statement_list_parse_treet::tia_modulet::var_temp
var_declarationst var_temp
Temp variable declarations.
Definition: statement_list_parse_tree.h:94
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
statement_list_typecheckt::typecheck_statement_list_accu_real_eq
void typecheck_statement_list_accu_real_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:718
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:574
statement_list_typecheckt::typecheck_statement_list_accu_real_sub
void typecheck_statement_list_accu_real_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for reals.
Definition: statement_list_typecheck.cpp:679
statement_list_typecheckt::typecheck_statement_list_nested_and
void typecheck_statement_list_nested_and(const codet &op_code)
Performs a typecheck on a nested And instruction.
Definition: statement_list_typecheck.cpp:916
statement_list_typecheckt::typecheck_statement_list_accu_dint_sub
void typecheck_statement_list_accu_dint_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for double integers.
Definition: statement_list_typecheck.cpp:585
xor_exprt
Boolean XOR.
Definition: std_expr.h:2005
statement_list_typecheckt::typecheck_statement_list_assign
void typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL assign instruction and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1023
statement_list_typecheckt::typecheck_statement_list_accu_int_lte
void typecheck_statement_list_accu_int_lte(const codet &op_code)
Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers.
Definition: statement_list_typecheck.cpp:558
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
and_exprt
Boolean AND.
Definition: std_expr.h:1834
statement_list_parse_treet::var_declarationt
Struct for a single variable declaration in Statement List.
Definition: statement_list_parse_tree.h:30
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
statement_list_parse_treet::tia_modulet::var_input
var_declarationst var_input
Input variable declarations.
Definition: statement_list_parse_tree.h:88
statement_list_typecheckt::typecheck_statement_list_accu_real_add
void typecheck_statement_list_accu_real_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for reals.
Definition: statement_list_typecheck.cpp:666
CPROVER_TEMP_RLO
#define CPROVER_TEMP_RLO
Name of the RLO symbol used in some operations.
Definition: statement_list_typecheck.cpp:39
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
statement_list_typecheckt::symbol_table
symbol_tablet & symbol_table
Reference to the symbol table that should be filled during the typecheck.
Definition: statement_list_typecheck.h:63
statement_list_parse_treet::instructiont
Represents a regular Statement List instruction which consists out of one or more codet tokens.
Definition: statement_list_parse_tree.h:45
statement_list_parse_treet::tia_modulet
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
Definition: statement_list_parse_tree.h:81
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
statement_list_typecheckt::typecheck_statement_list_accu_dint_arith
void typecheck_statement_list_accu_dint_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for double integers.
Definition: statement_list_typecheck.cpp:1138
statement_list_typecheckt::save_rlo_state
void save_rlo_state(symbolt &tia_element)
Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean v...
Definition: statement_list_typecheck.cpp:1528
statement_list_parse_treet::var_declarationt::variable
symbol_exprt variable
Representation of the variable, including identifier and type.
Definition: statement_list_parse_tree.h:32
messaget::eom
static eomt eom
Definition: message.h:297
statement_list_typecheckt::rlo_bit
exprt rlo_bit
Result of Logic Operation (Part of the TIA status word).
Definition: statement_list_typecheck.h:78
statement_list_typecheckt::typecheck_statement_list_accu_int_neq
void typecheck_statement_list_accu_int_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for integers.
Definition: statement_list_typecheck.cpp:537
div_exprt
Division.
Definition: std_expr.h:980
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
statement_list_typecheckt::typecheck_statement_list_instruction
void typecheck_statement_list_instruction(const statement_list_parse_treet::instructiont &instruction, symbolt &tia_element)
Performs a typecheck on a single instruction and saves the result to the given symbol body if necessa...
Definition: statement_list_typecheck.cpp:321
statement_list_typecheckt::typecheck_statement_list_accu_int_add
void typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
Definition: statement_list_typecheck.cpp:478
namespace.h
CPROVER_ASSUME
#define CPROVER_ASSUME
Name of the CBMC assume function.
Definition: statement_list_typecheck.cpp:37
equal_exprt
Equality.
Definition: std_expr.h:1139
statement_list_typecheckt::typecheck_temp_var_decls
void typecheck_temp_var_decls(const statement_list_parse_treet::tia_modulet &tia_module, symbolt &tia_symbol)
Performs a typecheck on the temp variables of a TIA module and saves the result to the given symbol v...
Definition: statement_list_typecheck.cpp:278
statement_list_typecheckt::typecheck_statement_list_accu_real_div
void typecheck_statement_list_accu_real_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for reals.
Definition: statement_list_typecheck.cpp:705
statement_list_typecheckt::nesting_stack_entryt::nesting_stack_entryt
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
Definition: statement_list_typecheck.cpp:71
statement_list_typecheckt::typecheck_tag_list
void typecheck_tag_list()
Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents t...
Definition: statement_list_typecheck.cpp:190
statement_list_parse_treet::function_blockt
Structure for a simple function block in Statement List.
Definition: statement_list_parse_tree.h:148
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1163
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
statement_list_typecheckt::typecheck_statement_list_accu_dint_lte
void typecheck_statement_list_accu_dint_lte(const codet &op_code)
Performs a typecheck on a STL accumulator less than or equal comparison instruction for double intege...
Definition: statement_list_typecheck.cpp:652
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
statement_list_typecheckt::typecheck_statement_list_nested_xor_not
void typecheck_statement_list_nested_xor_not(const codet &op_code)
Performs a typecheck on a nested XOR Not instruction.
Definition: statement_list_typecheck.cpp:956
statement_list_typecheckt::typecheck_statement_list_or
void typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or instruction.
Definition: statement_list_typecheck.cpp:818
TYPECHECK_ERROR
#define TYPECHECK_ERROR
Definition: statement_list_typecheck.cpp:29
statement_list_typecheckt::typecheck_statement_list_accu_int_sub
void typecheck_statement_list_accu_int_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for integers.
Definition: statement_list_typecheck.cpp:491
statement_list_typecheckt::typecheck_CPROVER_assume
void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a call of __CPOVER_ASSUME and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1330
statement_list_typecheckt::typecheck_called_tia_element
void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a call of a TIA element and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1349
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
statement_list_typecheckt::typecheck_statement_list_networks
void typecheck_statement_list_networks(const statement_list_parse_treet::tia_modulet &tia_module, symbolt &tia_symbol)
Performs a typecheck on the networks of a TIA module and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:300
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
statement_list_typecheckt::typecheck_function_call_arguments
exprt typecheck_function_call_arguments(const std::vector< equal_exprt > &assignments, const code_typet::parametert &param, const symbolt &tia_element)
Checks if the given parameter is inside of the assignment list of a function call and returns the exp...
Definition: statement_list_typecheck.cpp:1427
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:1870
statement_list_typecheckt::typecheck_statement_list_accu_dint_eq
void typecheck_statement_list_accu_dint_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:624
statement_list_typecheckt::typecheck_statement_list_accu_int_gte
void typecheck_statement_list_accu_int_gte(const codet &op_code)
Performs a typecheck on a STL accumulator greater than or equal comparison instruction for integers.
Definition: statement_list_typecheck.cpp:565
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
statement_list_typecheckt::typecheck_statement_list_accu_real_gt
void typecheck_statement_list_accu_real_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:739
statement_list_typecheckt::nesting_stack
nesting_stackt nesting_stack
Representation of the nesting stack.
Definition: statement_list_typecheck.h:112
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:589
statement_list_typecheckt::typecheck_statement_list_accu_real_lt
void typecheck_statement_list_accu_real_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:732
empty_typet
The empty type.
Definition: std_types.h:45
or_exprt
Boolean OR.
Definition: std_expr.h:1942
statement_list_typecheckt::typecheck_statement_list_load
void typecheck_statement_list_load(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL load instruction.
Definition: statement_list_typecheck.cpp:442
statement_list_typecheckt::typecheck_binary_accumulator_instruction
void typecheck_binary_accumulator_instruction(const codet &op_code)
Performs a typecheck on a STL instruction that uses two accumulator entries.
Definition: statement_list_typecheck.cpp:1210
statement_list_typecheckt::add_temp_rlo
void add_temp_rlo()
Adds a symbol for the RLO to the symbol table.
Definition: statement_list_typecheck.cpp:206
statement_list_typecheckt::typecheck_statement_list_xor_not
void typecheck_statement_list_xor_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR Not instruction.
Definition: statement_list_typecheck.cpp:884
statement_list_typecheckt::typecheck_statement_list_or_not
void typecheck_statement_list_or_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or Not instruction.
Definition: statement_list_typecheck.cpp:843
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
statement_list_typecheckt::typecheck_statement_list_accu_int_eq
void typecheck_statement_list_accu_int_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for integers.
Definition: statement_list_typecheck.cpp:530
statement_list_typecheckt::typecheck_function_var_decls
void typecheck_function_var_decls(const statement_list_parse_treet::var_declarationst &var_decls, code_typet::parameterst &params, const irep_idt &function_name, const irep_idt &var_property)
Performs a typecheck on a variable declaration list and saves the result to the given component eleme...
Definition: statement_list_typecheck.cpp:251
statement_list_typecheckt::typecheck_statement_list_accu_real_neq
void typecheck_statement_list_accu_real_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:725
statement_list_typecheckt::typecheck_statement_list_accu_real_mul
void typecheck_statement_list_accu_real_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for reals.
Definition: statement_list_typecheck.cpp:692
statement_list_typecheckt::typecheck_statement_list_accu_dint_gt
void typecheck_statement_list_accu_dint_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:645
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:766
statement_list_typecheckt::typecheck_function_block_declaration
void typecheck_function_block_declaration(const statement_list_parse_treet::function_blockt &function_block)
Performs a typecheck on a function block declaration inside of the parse tree and adds symbols for it...
Definition: statement_list_typecheck.cpp:118
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
statement_list_parse_treet::function_blocks
function_blockst function_blocks
List of function blocks this parse tree includes.
Definition: statement_list_parse_tree.h:174
statement_list_parse_treet::tia_modulet::name
const irep_idt name
Name of the module.
Definition: statement_list_parse_tree.h:83
statement_list_typecheckt::typecheck_statement_list_accu_dint_gte
void typecheck_statement_list_accu_dint_gte(const codet &op_code)
Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double int...
Definition: statement_list_typecheck.cpp:659
statement_list_typecheck
bool statement_list_typecheck(const statement_list_parse_treet &parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Create a new statement_list_typecheckt object and perform a type check to fill the symbol table.
Definition: statement_list_typecheck.cpp:59
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
statement_list_typecheckt::typecheck_return_value_assignment
exprt typecheck_return_value_assignment(const std::vector< equal_exprt > &assignments, const typet &return_type, const symbolt &tia_element)
Checks if there is a return value assignment inside of the assignment list of a function call and ret...
Definition: statement_list_typecheck.cpp:1473
statement_list_typecheckt::typecheck_statement_list_set
void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL 'S' instruction and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1062
exprt::op1
exprt & op1()
Definition: expr.h:106
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
statement_list_typecheckt::typecheck_function_declaration
void typecheck_function_declaration(const statement_list_parse_treet::functiont &function)
Performs a typecheck on a function declaration inside of the parse tree and adds symbols for it and i...
Definition: statement_list_typecheck.cpp:167
statement_list_typecheckt::typecheck_statement_list_accu_real_arith
void typecheck_statement_list_accu_real_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for reals.
Definition: statement_list_typecheck.cpp:1160
statement_list_typecheckt::typecheck_instruction_without_operand
void typecheck_instruction_without_operand(const codet &op_code)
Performs a typecheck on an operand-less STL instruction.
Definition: statement_list_typecheck.cpp:1200
statement_list_typecheckt::typecheck_called_function_block
void typecheck_called_function_block(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a call of a TIA function block and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1415
statement_list_parse_treet::instructiont::tokens
std::vector< codet > tokens
Data structure for all tokens of the instruction.
Definition: statement_list_parse_tree.h:47
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:533
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
statement_list_typecheckt::typecheck_statement_list_accu_int_mul
void typecheck_statement_list_accu_int_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for integers.
Definition: statement_list_typecheck.cpp:504
std_code.h
statement_list_typecheckt::statement_list_typecheckt
statement_list_typecheckt(const statement_list_parse_treet &parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Creates a new instance of statement_list_typecheckt.
Definition: statement_list_typecheck.cpp:79
minus_exprt
Binary minus.
Definition: std_expr.h:889
statement_list_typecheckt::typecheck_statement_list_accu_dint_neq
void typecheck_statement_list_accu_dint_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:631
simplify_expr.h
statement_list_typecheckt::typecheck_statement_list_accu_int_lt
void typecheck_statement_list_accu_int_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for integers.
Definition: statement_list_typecheck.cpp:544
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:1989
statement_list_parse_treet::function_blockt::var_static
var_declarationst var_static
FB-exclusive static variable declarations.
Definition: statement_list_parse_tree.h:150
statement_list_typecheckt::typecheck
void typecheck() override
Performs the actual typecheck by using the parse tree with which the object was initialized and modif...
Definition: statement_list_typecheck.cpp:91
statement_list_typecheckt::typecheck_statement_list_nesting_closed
void typecheck_statement_list_nesting_closed(const codet &op_code)
Performs a typecheck on a Nesting Closed instruction.
Definition: statement_list_typecheck.cpp:964
STATEMENT_LIST_PTR_WIDTH
#define STATEMENT_LIST_PTR_WIDTH
Size of pointers in Siemens TIA.
Definition: statement_list_typecheck.cpp:27
statement_list_typecheckt::typecheck_statement_list_nested_or
void typecheck_statement_list_nested_or(const codet &op_code)
Performs a typecheck on a nested Or instruction.
Definition: statement_list_typecheck.cpp:932
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
struct_union_typet::componentt
Definition: std_types.h:63
statement_list_typecheckt::typecheck_instruction_with_non_const_operand
const symbol_exprt & typecheck_instruction_with_non_const_operand(const codet &op_code)
Performs a typecheck on a STL instruction with an additional operand that should be no constant.
Definition: statement_list_typecheck.cpp:1187
statement_list_parse_treet
Intermediate representation of a parsed Statement List file before converting it into a goto program.
Definition: statement_list_parse_tree.h:22
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
statement_list_typecheckt::typecheck_identifier
exprt typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier)
Performs a typecheck on the given identifier and returns its symbol.
Definition: statement_list_typecheck.cpp:1249
statement_list_typecheckt::typecheck_statement_list_set_rlo
void typecheck_statement_list_set_rlo(const codet &op_code)
Performs a typecheck on a STL 'SET' instruction and modifies the RLO, OR and FC bit.
Definition: statement_list_typecheck.cpp:1044
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
statement_list_typecheckt::typecheck_statement_list_transfer
void typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL transfer instruction and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:463
statement_list_typecheckt::typecheck_statement_list_accu_real_gte
void typecheck_statement_list_accu_real_gte(const codet &op_code)
Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double int...
Definition: statement_list_typecheck.cpp:753
statement_list_typecheckt::typecheck_accumulator_compare_instruction
void typecheck_accumulator_compare_instruction(const irep_idt &comparison)
Performs a typecheck on an STL comparison instruction.
Definition: statement_list_typecheck.cpp:1176
statement_list_typecheckt::parse_tree
const statement_list_parse_treet & parse_tree
Parse tree which is used to fill the symbol table.
Definition: statement_list_typecheck.h:60
statement_list_typecheckt::initialize_bit_expression
void initialize_bit_expression(const exprt &op)
Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.
Definition: statement_list_typecheck.cpp:1521
statement_list_parse_treet::tags
std::vector< symbol_exprt > tags
List of tags that were included in the source.
Definition: statement_list_parse_tree.h:178
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
ieee_float.h
statement_list_typecheckt::typecheck_statement_list_accu_dint_div
void typecheck_statement_list_accu_dint_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
Definition: statement_list_typecheck.cpp:611
statement_list_typecheckt::typecheck_statement_list_nested_xor
void typecheck_statement_list_nested_xor(const codet &op_code)
Performs a typecheck on a nested XOR instruction.
Definition: statement_list_typecheck.cpp:948
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:584
code_typet::parametert
Definition: std_types.h:550
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1179
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:144
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
create_data_block_parameter
static code_typet::parametert create_data_block_parameter(const struct_typet &data_block_type, const irep_idt &function_block_name)
Creates the artificial data block parameter with a generic name and the specified type.
Definition: statement_list_typecheck.cpp:47
type_symbolt
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:133
statement_list_typecheckt::typecheck_statement_list_accu_dint_mul
void typecheck_statement_list_accu_dint_mul(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
Definition: statement_list_typecheck.cpp:598
statement_list_typecheckt::typecheck_statement_list_accu_dint_lt
void typecheck_statement_list_accu_dint_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:638
statement_list_typecheckt::nesting_stack_entryt
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
Definition: statement_list_typecheck.h:96
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
statement_list_typecheckt::typecheck_statement_list_xor
void typecheck_statement_list_xor(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR instruction.
Definition: statement_list_typecheck.cpp:864
statement_list_typecheckt::typecheck_simple_boolean_instruction_operand
exprt typecheck_simple_boolean_instruction_operand(const codet &op_code, const symbolt &tia_element, bool negate)
Performs a typecheck on the operand of a not nested boolean instruction and returns the result.
Definition: statement_list_typecheck.cpp:1237
statement_list_typecheckt::typecheck_statement_list_accu_real_lte
void typecheck_statement_list_accu_real_lte(const codet &op_code)
Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers.
Definition: statement_list_typecheck.cpp:746
statement_list_typecheckt::typecheck_statement_list_and
void typecheck_statement_list_and(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And instruction.
Definition: statement_list_typecheck.cpp:774
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2689
exprt::operands
operandst & operands()
Definition: expr.h:96
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
codet::op1
exprt & op1()
Definition: expr.h:106
statement_list_typecheckt::typecheck_statement_list_accu_int_div
void typecheck_statement_list_accu_int_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for integers.
Definition: statement_list_typecheck.cpp:517
typecheckt
Definition: typecheck.h:17
STL_INT_WIDTH
#define STL_INT_WIDTH
Definition: statement_list_types.h:15
statement_list_parse_treet::tia_modulet::var_inout
var_declarationst var_inout
Inout variable declarations.
Definition: statement_list_parse_tree.h:90
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
statement_list_parse_treet::functiont
Structure for a simple function in Statement List.
Definition: statement_list_parse_tree.h:129
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
statement_list_parse_treet::tia_modulet::var_output
var_declarationst var_output
Output variable declarations.
Definition: statement_list_parse_tree.h:92
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
statement_list_typecheckt::accumulator
std::vector< exprt > accumulator
Representation of the accumulator of a TIA element.
Definition: statement_list_typecheck.h:73
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
typecheckt::typecheck_main
virtual bool typecheck_main()
Definition: typecheck.cpp:13
CPROVER_ASSERT
#define CPROVER_ASSERT
Name of the CBMC assert function.
Definition: statement_list_typecheck.cpp:35
std_expr.h
API to expression classes.
get_bool_type
bool_typet get_bool_type()
Creates a new type that resembles the 'Bool' type of the Siemens PLC languages.
Definition: statement_list_types.cpp:29
statement_list_typecheckt::typecheck_function_block_var_decls
void typecheck_function_block_var_decls(const statement_list_parse_treet::var_declarationst &var_decls, struct_union_typet::componentst &components, const irep_idt &var_property)
Performs a typecheck on a variable declaration list and saves the result to the given component eleme...
Definition: statement_list_typecheck.cpp:235
can_cast_type< floatbv_typet >
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
Definition: bitvector_types.h:354
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
statement_list_parse_treet::functions
functionst functions
List of functions this parse tree includes.
Definition: statement_list_parse_tree.h:176
statement_list_typecheckt::add_to_or_rlo_wrapper
void add_to_or_rlo_wrapper(const exprt &op)
Adds the given expression to the operands of the Or expression that is saved in the RLO.
Definition: statement_list_typecheck.cpp:1501
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:1881
statement_list_typecheckt::typecheck_nested_boolean_instruction
void typecheck_nested_boolean_instruction(const codet &op_code, const exprt &rlo_value)
Performs a typecheck on a STL instruction that initializes a new boolean nesting.
Definition: statement_list_typecheck.cpp:1221
statement_list_typecheckt::typecheck_statement_list_clr_rlo
void typecheck_statement_list_clr_rlo(const codet &op_code)
Performs a typecheck on a STL 'CLR' instruction and modifies the RLO, OR and FC bit.
Definition: statement_list_typecheck.cpp:1053
statement_list_typecheckt::typecheck_called_function
void typecheck_called_function(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a call of a TIA function and saves the result to the given symbol.
Definition: statement_list_typecheck.cpp:1371
DATA_BLOCK_TYPE_POSTFIX
#define DATA_BLOCK_TYPE_POSTFIX
Postfix for the type of a data block.
Definition: statement_list_typecheck.cpp:33
statement_list_typecheckt
Class for encapsulating the current state of the type check.
Definition: statement_list_typecheck.h:38
statement_list_typecheckt::fc_bit
bool fc_bit
First Check (Part of the TIA status word).
Definition: statement_list_typecheck.h:84
DATA_BLOCK_PARAMETER_NAME
#define DATA_BLOCK_PARAMETER_NAME
Artificial name for the data block interface of a function block.
Definition: statement_list_typecheck.cpp:31
statement_list_types.h
Statement List Type Helper.
statement_list_typecheckt::typecheck_function_call_argument_rhs
exprt typecheck_function_call_argument_rhs(const symbolt &tia_element, const exprt &rhs)
Checks if the given assigned expression is a variable or a constant and returns the typechecked versi...
Definition: statement_list_typecheck.cpp:1458
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
statement_list_typecheckt::or_bit
bool or_bit
Or (Part of the TIA status word).
Definition: statement_list_typecheck.h:89
not_exprt
Boolean negation.
Definition: std_expr.h:2041
statement_list_typecheckt::typecheck_statement_list_accu_dint_add
void typecheck_statement_list_accu_dint_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for double integers.
Definition: statement_list_typecheck.cpp:572