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 #include <util/ieee_float.h>
17 #include <util/message.h>
18 #include <util/namespace.h>
19 #include <util/simplify_expr.h>
20 #include <util/std_code.h>
21 #include <util/std_expr.h>
22 #include <util/std_types.h>
23 
25 #define STATEMENT_LIST_PTR_WIDTH 64
26 // TODO: Replace with more specific exception throws.
27 #define TYPECHECK_ERROR 0
28 #define DATA_BLOCK_PARAMETER_NAME "data_block"
30 #define DATA_BLOCK_TYPE_POSTFIX "_db"
32 #define CPROVER_ASSERT CPROVER_PREFIX "assert"
34 #define CPROVER_ASSUME CPROVER_PREFIX "assume"
36 #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
38 
46  const struct_typet &data_block_type,
47  const irep_idt &function_block_name)
48 {
49  const pointer_typet db_ptr{data_block_type, STATEMENT_LIST_PTR_WIDTH};
50  code_typet::parametert param{db_ptr};
51  param.set_identifier(
52  id2string(function_block_name) + "::" + DATA_BLOCK_PARAMETER_NAME);
53  param.set_base_name(DATA_BLOCK_PARAMETER_NAME);
54  return param;
55 }
56 
58  const statement_list_parse_treet &parse_tree,
59  symbol_tablet &symbol_table,
60  const std::string &module,
61  message_handlert &message_handler)
62 {
63  statement_list_typecheckt stl_typecheck(
64  parse_tree, symbol_table, module, message_handler);
65 
66  return stl_typecheck.typecheck_main();
67 }
68 
70  exprt rlo_bit,
71  bool or_bit,
72  codet function_code)
73  : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
74 {
75 }
76 
80  const std::string &module,
85  module(module)
86 {
87 }
88 
90 {
91  // First fill the symbol table with function, tag and parameter declarations
92  // to be able to properly resolve block calls later.
99  // Temporary RLO symbol for certain operations.
100  add_temp_rlo();
101 
102  // Iterate through all networks to generate the function bodies.
105  {
108  }
110  {
111  symbolt &function_sym{symbol_table.get_writeable_ref(fc.name)};
112  typecheck_statement_list_networks(fc, function_sym);
113  }
114 }
115 
117  const statement_list_parse_treet::function_blockt &function_block)
118 {
119  // Create FB symbol.
120  symbolt function_block_sym;
121  function_block_sym.module = module;
122  function_block_sym.name = function_block.name;
123  function_block_sym.base_name = function_block_sym.name;
124  function_block_sym.pretty_name = function_block_sym.name;
125  function_block_sym.mode = ID_statement_list;
126 
127  // When calling function blocks, the passed parameters are value-copied to a
128  // corresponding instance data block. This block contains all input, inout,
129  // output and static variables. The function block reads and writes only
130  // those fields and does not modify the actual parameters. To simulate this
131  // behaviour, all function blocks are modeled as functions with a single
132  // parameter: An instance of their data block, whose members they modify.
133 
134  // Create and add DB type symbol.
135  const struct_typet data_block_type{
136  create_instance_data_block_type(function_block)};
137  type_symbolt data_block{data_block_type};
138  data_block.name =
139  id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX;
140  data_block.base_name = data_block.name;
141  data_block.mode = ID_statement_list;
142  symbol_table.add(data_block);
143 
144  // Create and add parameter symbol.
146  create_data_block_parameter(data_block_type, function_block_sym.name)};
147  parameter_symbolt param_sym;
148  param_sym.module = module;
149  param_sym.type = param.type();
150  param_sym.name = param.get_identifier();
152  param_sym.pretty_name = param_sym.base_name;
153  param_sym.mode = ID_statement_list;
154  symbol_table.add(param_sym);
155 
156  // Setup FB symbol type and value.
158  params.push_back(param);
159  code_typet fb_type{params, empty_typet()};
160  fb_type.set(ID_statement_list_type, ID_statement_list_function_block);
161  function_block_sym.type = fb_type;
162  symbol_table.add(function_block_sym);
163 }
164 
167 {
168  symbolt function_sym;
169  function_sym.module = module;
170  function_sym.name = function.name;
171  function_sym.base_name = function_sym.name;
172  function_sym.pretty_name = function_sym.name;
173  function_sym.mode = ID_statement_list;
176  function.var_input, params, function.name, ID_statement_list_var_input);
178  function.var_inout, params, function.name, ID_statement_list_var_inout);
180  function.var_output, params, function.name, ID_statement_list_var_output);
181 
182  code_typet fc_type{params, function.return_type};
183  fc_type.set(ID_statement_list_type, ID_statement_list_function);
184  function_sym.type = fc_type;
185  symbol_table.add(function_sym);
186 }
187 
189 {
190  for(const symbol_exprt &tag : parse_tree.tags)
191  {
192  symbolt tag_sym;
193  tag_sym.is_static_lifetime = true;
194  tag_sym.module = module;
195  tag_sym.name = tag.get_identifier();
196  tag_sym.base_name = tag_sym.name;
197  tag_sym.pretty_name = tag_sym.name;
198  tag_sym.type = tag.type();
199  tag_sym.mode = ID_statement_list;
200  symbol_table.add(tag_sym);
201  }
202 }
203 
205 {
206  symbolt temp_rlo;
207  temp_rlo.is_static_lifetime = true;
208  temp_rlo.module = module;
209  temp_rlo.name = CPROVER_TEMP_RLO;
210  temp_rlo.base_name = temp_rlo.name;
211  temp_rlo.pretty_name = temp_rlo.name;
212  temp_rlo.type = get_bool_type();
213  temp_rlo.mode = ID_statement_list;
214  symbol_table.add(temp_rlo);
215 }
216 
218  const statement_list_parse_treet::function_blockt &function_block)
219 {
222  function_block.var_input, components, ID_statement_list_var_input);
224  function_block.var_inout, components, ID_statement_list_var_inout);
226  function_block.var_output, components, ID_statement_list_var_output);
228  function_block.var_static, components, ID_statement_list_var_static);
229 
230  return struct_typet{components};
231 }
232 
236  const irep_idt &var_property)
237 {
238  for(const statement_list_parse_treet::var_declarationt &declaration :
239  var_decls)
240  {
241  const irep_idt &var_name{declaration.variable.get_identifier()};
242  const typet &var_type{declaration.variable.type()};
243  struct_union_typet::componentt component{var_name, var_type};
244  component.set(ID_statement_list_type, var_property);
245  components.push_back(component);
246  }
247 }
248 
251  code_typet::parameterst &params,
252  const irep_idt &function_name,
253  const irep_idt &var_property)
254 {
255  for(const statement_list_parse_treet::var_declarationt &declaration :
256  var_decls)
257  {
258  parameter_symbolt param_sym;
259  param_sym.module = module;
260  param_sym.type = declaration.variable.type();
261  param_sym.name = id2string(function_name) +
262  "::" + id2string(declaration.variable.get_identifier());
263  param_sym.base_name = declaration.variable.get_identifier();
264  param_sym.pretty_name = param_sym.base_name;
265  param_sym.mode = ID_statement_list;
266  symbol_table.add(param_sym);
267 
268  code_typet::parametert param{declaration.variable.type()};
269  param.set_identifier(param_sym.name);
270  param.set_base_name(declaration.variable.get_identifier());
271  param.set(ID_statement_list_type, var_property);
272  params.push_back(param);
273  }
274 }
275 
277  const statement_list_parse_treet::tia_modulet &tia_module,
278  symbolt &tia_symbol)
279 {
280  for(const statement_list_parse_treet::var_declarationt &declaration :
281  tia_module.var_temp)
282  {
283  symbolt temp_sym;
284  temp_sym.name = id2string(tia_symbol.name) +
285  "::" + id2string(declaration.variable.get_identifier());
286  temp_sym.base_name = declaration.variable.get_identifier();
287  temp_sym.pretty_name = temp_sym.base_name;
288  temp_sym.type = declaration.variable.type();
289  temp_sym.mode = ID_statement_list;
290  temp_sym.module = module;
291  symbol_table.add(temp_sym);
292 
293  const code_declt code_decl{temp_sym.symbol_expr()};
294  tia_symbol.value.add_to_operands(code_decl);
295  }
296 }
297 
299  const statement_list_parse_treet::tia_modulet &tia_module,
300  symbolt &tia_symbol)
301 {
302  // Leave value empty if there are no networks to iterate through.
303  if(tia_module.networks.empty())
304  return;
305  if(tia_symbol.value.is_nil())
306  tia_symbol.value = code_blockt{};
307 
308  typecheck_temp_var_decls(tia_module, tia_symbol);
309 
310  for(const auto &network : tia_module.networks)
311  {
312  // Set RLO to true each time a new network is entered (TIA behaviour).
313  rlo_bit = true_exprt();
314  for(const auto &instruction : network.instructions)
315  typecheck_statement_list_instruction(instruction, tia_symbol);
316  }
317 }
318 
320  const statement_list_parse_treet::instructiont &instruction,
321  symbolt &tia_element)
322 {
323  const codet &op_code{instruction.tokens.back()};
324  const irep_idt statement{op_code.get_statement()};
325 
326  if(ID_statement_list_load == statement)
327  typecheck_statement_list_load(op_code, tia_element);
328  else if(ID_statement_list_transfer == statement)
329  typecheck_statement_list_transfer(op_code, tia_element);
330  else if(ID_statement_list_accu_int_add == statement)
332  else if(ID_statement_list_accu_int_sub == statement)
334  else if(ID_statement_list_accu_int_mul == statement)
336  else if(ID_statement_list_accu_int_div == statement)
338  else if(ID_statement_list_accu_int_eq == statement)
340  else if(ID_statement_list_accu_int_neq == statement)
342  else if(ID_statement_list_accu_int_lt == statement)
344  else if(ID_statement_list_accu_int_gt == statement)
346  else if(ID_statement_list_accu_int_lte == statement)
348  else if(ID_statement_list_accu_int_gte == statement)
350  else if(ID_statement_list_accu_dint_add == statement)
352  else if(ID_statement_list_accu_dint_sub == statement)
354  else if(ID_statement_list_accu_dint_mul == statement)
356  else if(ID_statement_list_accu_dint_div == statement)
358  else if(ID_statement_list_accu_dint_eq == statement)
360  else if(ID_statement_list_accu_dint_neq == statement)
362  else if(ID_statement_list_accu_dint_lt == statement)
364  else if(ID_statement_list_accu_dint_gt == statement)
366  else if(ID_statement_list_accu_dint_lte == statement)
368  else if(ID_statement_list_accu_dint_gte == statement)
370  else if(ID_statement_list_accu_real_add == statement)
372  else if(ID_statement_list_accu_real_sub == statement)
374  else if(ID_statement_list_accu_real_mul == statement)
376  else if(ID_statement_list_accu_real_div == statement)
378  else if(ID_statement_list_accu_real_eq == statement)
380  else if(ID_statement_list_accu_real_neq == statement)
382  else if(ID_statement_list_accu_real_lt == statement)
384  else if(ID_statement_list_accu_real_gt == statement)
386  else if(ID_statement_list_accu_real_lte == statement)
388  else if(ID_statement_list_accu_real_gte == statement)
390  else if(ID_statement_list_not == statement)
392  else if(ID_statement_list_and == statement)
393  typecheck_statement_list_and(op_code, tia_element);
394  else if(ID_statement_list_and_not == statement)
395  typecheck_statement_list_and_not(op_code, tia_element);
396  else if(ID_statement_list_or == statement)
397  typecheck_statement_list_or(op_code, tia_element);
398  else if(ID_statement_list_or_not == statement)
399  typecheck_statement_list_or_not(op_code, tia_element);
400  else if(ID_statement_list_xor == statement)
401  typecheck_statement_list_xor(op_code, tia_element);
402  else if(ID_statement_list_xor_not == statement)
403  typecheck_statement_list_xor_not(op_code, tia_element);
404  else if(ID_statement_list_and_nested == statement)
406  else if(ID_statement_list_and_not_nested == statement)
408  else if(ID_statement_list_or_nested == statement)
410  else if(ID_statement_list_or_not_nested == statement)
412  else if(ID_statement_list_xor_nested == statement)
414  else if(ID_statement_list_xor_not_nested == statement)
416  else if(ID_statement_list_nesting_closed == statement)
418  else if(ID_statement_list_assign == statement)
419  typecheck_statement_list_assign(op_code, tia_element);
420  else if(ID_statement_list_set_rlo == statement)
422  else if(ID_statement_list_clr_rlo == statement)
424  else if(ID_statement_list_set == statement)
425  typecheck_statement_list_set(op_code, tia_element);
426  else if(ID_statement_list_reset == statement)
427  typecheck_statement_list_reset(op_code, tia_element);
428  else if(ID_statement_list_nop == statement)
429  return;
430  else if(ID_statement_list_call == statement)
431  typecheck_statement_list_call(op_code, tia_element);
432  else
433  {
434  error() << "OP code of instruction not found: " << op_code.get_statement()
435  << eom;
436  throw TYPECHECK_ERROR;
437  }
438 }
439 
441  const codet &op_code,
442  const symbolt &tia_element)
443 {
444  const symbol_exprt *const symbol =
445  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
446  if(symbol)
447  {
448  const irep_idt &identifier{symbol->get_identifier()};
449  const exprt val{typecheck_identifier(tia_element, identifier)};
450  accumulator.push_back(val);
451  }
452  else if(can_cast_expr<constant_exprt>(op_code.op0()))
453  accumulator.push_back(op_code.op0());
454  else
455  {
456  error() << "Instruction is not followed by symbol or constant" << eom;
457  throw TYPECHECK_ERROR;
458  }
459 }
460 
462  const codet &op_code,
463  symbolt &tia_element)
464 {
466  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
467  if(lhs.type() != accumulator.back().type())
468  {
469  error() << "Types of transfer assignment do not match" << eom;
470  throw TYPECHECK_ERROR;
471  }
472  const code_assignt assignment{lhs, accumulator.back()};
473  tia_element.value.add_to_operands(assignment);
474 }
475 
477  const codet &op_code)
478 {
480 
481  // Pop first operand, peek second.
482  const exprt accu1{accumulator.back()};
483  accumulator.pop_back();
484  const exprt &accu2{accumulator.back()};
485  const plus_exprt operation{accu2, accu1};
486  accumulator.push_back(operation);
487 }
488 
490  const codet &op_code)
491 {
493 
494  // Pop first operand, peek second.
495  const exprt accu1{accumulator.back()};
496  accumulator.pop_back();
497  const exprt &accu2{accumulator.back()};
498  const minus_exprt operation{accu2, accu1};
499  accumulator.push_back(operation);
500 }
501 
503  const codet &op_code)
504 {
506 
507  // Pop first operand, peek second.
508  const exprt accu1{accumulator.back()};
509  accumulator.pop_back();
510  const exprt &accu2{accumulator.back()};
511  const mult_exprt operation{accu2, accu1};
512  accumulator.push_back(operation);
513 }
514 
516  const codet &op_code)
517 {
519 
520  // Pop first operand, peek second.
521  const exprt accu1{accumulator.back()};
522  accumulator.pop_back();
523  const exprt &accu2{accumulator.back()};
524  const div_exprt operation{accu2, accu1};
525  accumulator.push_back(operation);
526 }
527 
529  const codet &op_code)
530 {
533 }
534 
536  const codet &op_code)
537 {
540 }
541 
543  const codet &op_code)
544 {
547 }
548 
550  const codet &op_code)
551 {
554 }
555 
557  const codet &op_code)
558 {
561 }
562 
564  const codet &op_code)
565 {
568 }
569 
571  const codet &op_code)
572 {
574 
575  // Pop first operand, peek second.
576  const exprt accu1{accumulator.back()};
577  accumulator.pop_back();
578  const exprt &accu2{accumulator.back()};
579  const plus_exprt operation{accu2, accu1};
580  accumulator.push_back(operation);
581 }
582 
584  const codet &op_code)
585 {
587 
588  // Pop first operand, peek second.
589  const exprt accu1{accumulator.back()};
590  accumulator.pop_back();
591  const exprt &accu2{accumulator.back()};
592  const minus_exprt operation{accu2, accu1};
593  accumulator.push_back(operation);
594 }
595 
597  const codet &op_code)
598 {
600 
601  // Pop first operand, peek second.
602  const exprt accu1{accumulator.back()};
603  accumulator.pop_back();
604  const exprt &accu2{accumulator.back()};
605  const mult_exprt operation{accu2, accu1};
606  accumulator.push_back(operation);
607 }
608 
610  const codet &op_code)
611 {
613 
614  // Pop first operand, peek second.
615  const exprt accu1{accumulator.back()};
616  accumulator.pop_back();
617  const exprt &accu2{accumulator.back()};
618  const div_exprt operation{accu2, accu1};
619  accumulator.push_back(operation);
620 }
621 
623  const codet &op_code)
624 {
627 }
628 
630  const codet &op_code)
631 {
634 }
635 
637  const codet &op_code)
638 {
641 }
642 
644  const codet &op_code)
645 {
648 }
649 
651  const codet &op_code)
652 {
655 }
656 
658  const codet &op_code)
659 {
662 }
663 
665  const codet &op_code)
666 {
668 
669  // Pop first operand, peek second.
670  const exprt accu1{accumulator.back()};
671  accumulator.pop_back();
672  const exprt &accu2{accumulator.back()};
673  const plus_exprt operation{accu2, accu1};
674  accumulator.push_back(operation);
675 }
676 
678  const codet &op_code)
679 {
681 
682  // Pop first operand, peek second.
683  const exprt accu1{accumulator.back()};
684  accumulator.pop_back();
685  const exprt &accu2{accumulator.back()};
686  const minus_exprt operation{accu2, accu1};
687  accumulator.push_back(operation);
688 }
689 
691  const codet &op_code)
692 {
694 
695  // Pop first operand, peek second.
696  const exprt accu1{accumulator.back()};
697  accumulator.pop_back();
698  const exprt &accu2{accumulator.back()};
699  const mult_exprt operation{accu2, accu1};
700  accumulator.push_back(operation);
701 }
702 
704  const codet &op_code)
705 {
707 
708  // Pop first operand, peek second.
709  const exprt accu1{accumulator.back()};
710  accumulator.pop_back();
711  const exprt &accu2{accumulator.back()};
712  const div_exprt operation{accu2, accu1};
713  accumulator.push_back(operation);
714 }
715 
717  const codet &op_code)
718 {
721 }
722 
724  const codet &op_code)
725 {
728 }
729 
731  const codet &op_code)
732 {
735 }
736 
738  const codet &op_code)
739 {
742 }
743 
745  const codet &op_code)
746 {
749 }
750 
752  const codet &op_code)
753 {
756 }
757 
759  const codet &op_code)
760 {
762  if(fc_bit)
763  {
764  const not_exprt unsimplified{rlo_bit};
765  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
766  or_bit = false;
767  }
768  else
770 }
771 
773  const codet &op_code,
774  const symbolt &tia_element)
775 {
776  exprt op{
777  typecheck_simple_boolean_instruction_operand(op_code, tia_element, false)};
778 
779  // If inside of a bit string and if the OR bit is not set, create an 'and'
780  // expression with the operand and the current contents of the rlo bit. If
781  // the OR bit is set then this instruction is part of an 'and-before-or'
782  // block and needs to be added to the rlo in a special way.
783  if(fc_bit && or_bit)
785  else if(fc_bit)
786  {
787  const and_exprt unsimplified{rlo_bit, op};
788  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
789  }
790  else
792 }
793 
795  const codet &op_code,
796  const symbolt &tia_element)
797 {
798  exprt op{
799  typecheck_simple_boolean_instruction_operand(op_code, tia_element, true)};
800 
801  // If inside of a bit string and if the OR bit is not set, create an 'and'
802  // expression with the operand and the current contents of the rlo bit. If
803  // the OR bit is set then this instruction is part of an 'and-before-or'
804  // block and needs to be added to the rlo in a special way.
805  if(or_bit && fc_bit)
807  else if(fc_bit)
808  {
809  const and_exprt unsimplified{rlo_bit, op};
810  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
811  }
812  else
814 }
815 
817  const codet &op_code,
818  const symbolt &tia_element)
819 {
820  if(op_code.operands().empty())
821  {
823  return;
824  }
825  const symbol_exprt &sym{
827  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
828 
829  // If inside of a bit string, create an 'or' expression with the operand and
830  // the current contents of the rlo bit.
831  if(fc_bit)
832  {
833  const or_exprt unsimplified{rlo_bit, op};
834  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
835  or_bit = false;
836  }
837  else
839 }
840 
842  const codet &op_code,
843  const symbolt &tia_element)
844 {
845  const symbol_exprt &sym{
847  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
848  const not_exprt not_op{op};
849 
850  // If inside of a bit string, create an 'or' expression with the operand and
851  // the current contents of the rlo bit.
852  if(fc_bit)
853  {
854  const or_exprt unsimplified{rlo_bit, not_op};
855  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
856  or_bit = false;
857  }
858  else
860 }
861 
863  const codet &op_code,
864  const symbolt &tia_element)
865 {
866  const symbol_exprt &sym{
868  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
869 
870  // If inside of a bit string, create an 'xor' expression with the operand and
871  // the current contents of the rlo bit.
872  if(fc_bit)
873  {
874  const xor_exprt unsimplified{rlo_bit, op};
875  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
876  or_bit = false;
877  }
878  else
880 }
881 
883  const codet &op_code,
884  const symbolt &tia_element)
885 {
886  const symbol_exprt &sym{
888  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
889  const not_exprt not_op{op};
890 
891  // If inside of a bit string, create an 'xor not' expression with the
892  // operand and the current contents of the rlo bit.
893  if(fc_bit)
894  {
895  const xor_exprt unsimplified{rlo_bit, not_op};
896  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
897  or_bit = false;
898  }
899  else
901 }
902 
904 {
905  if(fc_bit)
906  {
908  or_bit = true;
909  }
910  else
911  return; // Instruction has no semantic influence.
912 }
913 
915  const codet &op_code)
916 {
917  // Set the rlo to true implicitly so that the value of the AND instruction
918  // is being loaded in case of a new bit string.
920 }
921 
923  const codet &op_code)
924 {
925  // Set the rlo to true implicitly so that the value of the AND instruction
926  // is being loaded in case of a new bit string.
928 }
929 
931  const codet &op_code)
932 {
933  // Set the rlo to false implicitly so that the value of the OR instruction
934  // is being loaded in case of a new bit string.
936 }
937 
939  const codet &op_code)
940 {
941  // Set the rlo to false implicitly so that the value of the OR instruction
942  // is being loaded in case of a new bit string.
944 }
945 
947  const codet &op_code)
948 {
949  // Set the rlo to false implicitly so that the value of the XOR instruction
950  // is being loaded in case of a new bit string.
952 }
953 
955  const codet &op_code)
956 {
957  // Set the rlo to false implicitly so that the value of the XOR instruction
958  // is being loaded in case of a new bit string.
960 }
961 
963  const codet &op_code)
964 {
966  if(nesting_stack.empty())
967  {
968  error() << "Wrong order of brackets (Right parenthesis is not preceded by "
969  "nesting)"
970  << eom;
971  throw TYPECHECK_ERROR;
972  }
973  or_bit = nesting_stack.back().or_bit;
974  fc_bit = true;
975  const irep_idt &statement{nesting_stack.back().function_code.get_statement()};
976  if(ID_statement_list_and_nested == statement)
977  {
978  if(or_bit)
979  {
980  const exprt op{rlo_bit};
981  rlo_bit = nesting_stack.back().rlo_bit;
983  }
984  else
985  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, rlo_bit};
986  }
987  else if(ID_statement_list_and_not_nested == statement)
988  {
989  if(or_bit)
990  {
991  const not_exprt op{rlo_bit};
992  rlo_bit = nesting_stack.back().rlo_bit;
994  }
995  else
996  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
997  }
998  else if(ID_statement_list_or_nested == statement)
999  {
1000  or_bit = false;
1001  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1002  }
1003  else if(ID_statement_list_or_not_nested == statement)
1004  {
1005  or_bit = false;
1006  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1007  }
1008  else if(ID_statement_list_xor_nested == statement)
1009  {
1010  or_bit = false;
1011  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1012  }
1013  else if(ID_statement_list_xor_not_nested == statement)
1014  {
1015  or_bit = false;
1016  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1017  }
1018  nesting_stack.pop_back();
1019 }
1020 
1022  const codet &op_code,
1023  symbolt &tia_element)
1024 {
1026  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
1027 
1028  if(lhs.type() != rlo_bit.type())
1029  {
1030  error() << "Types of assign do not match" << eom;
1031  throw TYPECHECK_ERROR;
1032  }
1033  const code_assignt assignment{lhs, rlo_bit};
1034  tia_element.value.add_to_operands(assignment);
1035  fc_bit = false;
1036  or_bit = false;
1037  // Set RLO to assigned operand in order to prevent false results if a symbol
1038  // that's implicitly part of the RLO was changed by the assignment.
1039  rlo_bit = lhs;
1040 }
1041 
1043  const codet &op_code)
1044 {
1046  fc_bit = false;
1047  or_bit = false;
1048  rlo_bit = true_exprt();
1049 }
1050 
1052  const codet &op_code)
1053 {
1055  fc_bit = false;
1056  or_bit = false;
1057  rlo_bit = false_exprt();
1058 }
1059 
1061  const codet &op_code,
1062  symbolt &tia_element)
1063 {
1065  const irep_idt &identifier{op.get_identifier()};
1066 
1067  save_rlo_state(tia_element);
1068 
1069  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1070  const code_assignt assignment{lhs, true_exprt()};
1071  const code_ifthenelset ifthen{rlo_bit, assignment};
1072  tia_element.value.add_to_operands(ifthen);
1073  fc_bit = false;
1074  or_bit = false;
1075 }
1076 
1078  const codet &op_code,
1079  symbolt &tia_element)
1080 {
1082  const irep_idt &identifier{op.get_identifier()};
1083 
1084  save_rlo_state(tia_element);
1085 
1086  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1087  const code_assignt assignment{lhs, false_exprt()};
1088  const code_ifthenelset ifthen{rlo_bit, assignment};
1089  tia_element.value.add_to_operands(ifthen);
1090  fc_bit = false;
1091  or_bit = false;
1092 }
1093 
1095  const codet &op_code,
1096  symbolt &tia_element)
1097 {
1099  const irep_idt &identifier{op.get_identifier()};
1100  if(symbol_table.has_symbol(identifier))
1101  typecheck_called_tia_element(op_code, tia_element);
1102  else if(identifier == CPROVER_ASSUME)
1103  typecheck_CPROVER_assume(op_code, tia_element);
1104  else if(identifier == CPROVER_ASSERT)
1105  typecheck_CPROVER_assert(op_code, tia_element);
1106  else
1107  {
1108  error() << "Called function could not be found" << eom;
1109  throw TYPECHECK_ERROR;
1110  }
1111  fc_bit = false;
1112  or_bit = false;
1113 }
1114 
1116  const codet &op_code)
1117 {
1119  const exprt &accu1{accumulator.back()};
1120  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1121 
1122  // Are both operands integers?
1123  const signedbv_typet *const accu_type1 =
1124  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1125  const signedbv_typet *const accu_type2 =
1126  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1127  if(
1128  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_INT_WIDTH ||
1129  accu_type2->get_width() != STL_INT_WIDTH)
1130  {
1131  error() << "Operands of integer addition are no integers" << eom;
1132  throw TYPECHECK_ERROR;
1133  }
1134 }
1135 
1137  const codet &op_code)
1138 {
1140  const exprt &accu1{accumulator.back()};
1141  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1142 
1143  // Are both operands double integers?
1144  const signedbv_typet *const accu_type1 =
1145  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1146  const signedbv_typet *const accu_type2 =
1147  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1148  if(
1149  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_DINT_WIDTH ||
1150  accu_type2->get_width() != STL_DINT_WIDTH)
1151  {
1152  error() << "Operands of double integer addition are no double integers"
1153  << eom;
1154  throw TYPECHECK_ERROR;
1155  }
1156 }
1157 
1159  const codet &op_code)
1160 {
1162  const exprt &accu1{accumulator.back()};
1163  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1164 
1165  // Are both operands real types?
1166  if(!(can_cast_type<floatbv_typet>(accu1.type()) &&
1167  can_cast_type<floatbv_typet>(accu2.type())))
1168  {
1169  error() << "Operands of Real addition do not have the type Real" << eom;
1170  throw TYPECHECK_ERROR;
1171  }
1172 }
1173 
1175  const irep_idt &comparison)
1176 {
1177  const exprt &accu1{accumulator.back()};
1178  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1179  // STL behaviour: ACCU2 is lhs, ACCU1 is rhs.
1180  const binary_relation_exprt operation{accu2, comparison, accu1};
1181  rlo_bit = operation;
1182 }
1183 
1184 const symbol_exprt &
1186  const codet &op_code)
1187 {
1188  const symbol_exprt *const symbol =
1189  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
1190 
1191  if(symbol)
1192  return *symbol;
1193 
1194  error() << "Instruction is not followed by symbol" << eom;
1195  throw TYPECHECK_ERROR;
1196 }
1197 
1199  const codet &op_code)
1200 {
1201  if(op_code.operands().size() > 0)
1202  {
1203  error() << "Instruction is followed by operand" << eom;
1204  throw TYPECHECK_ERROR;
1205  }
1206 }
1207 
1209  const codet &op_code)
1210 {
1212  if(accumulator.size() < 2)
1213  {
1214  error() << "Not enough operands in the accumulator" << eom;
1215  throw TYPECHECK_ERROR;
1216  }
1217 }
1218 
1220  const codet &op_code,
1221  const exprt &rlo_value)
1222 {
1224  // If inside of a bit string use the value of the rlo. If this is the first
1225  // expression of a bit string, load the value of the nested operation by
1226  // implicitly setting the rlo to the specified value.
1227  if(!fc_bit)
1228  rlo_bit = rlo_value;
1229  const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code};
1230  nesting_stack.push_back(stack_entry);
1231  fc_bit = false;
1232  or_bit = false;
1233 }
1234 
1236  const codet &op_code,
1237  const symbolt &tia_element,
1238  bool negate)
1239 {
1240  const symbol_exprt &sym{
1242  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1243  const not_exprt not_op{op};
1244  return negate ? not_op : op;
1245 }
1246 
1248  const symbolt &tia_element,
1249  const irep_idt &identifier)
1250 {
1251  const code_typet &element_type{to_code_type(tia_element.type)};
1252 
1253  // Check for temporary variables.
1255  id2string(tia_element.name) + "::" + id2string(identifier)))
1256  {
1257  const symbolt &sym{symbol_table.lookup_ref(
1258  id2string(tia_element.name) + "::" + id2string(identifier))};
1259  return sym.symbol_expr();
1260  }
1261 
1262  // Check for global tags.
1263  if(symbol_table.has_symbol(identifier))
1264  return symbol_table.lookup_ref(identifier).symbol_expr();
1265 
1266  if(
1267  element_type.get(ID_statement_list_type) ==
1268  ID_statement_list_function_block)
1269  {
1270  // Check for variables inside of the function block interface.
1271  const symbolt &data_block{symbol_table.get_writeable_ref(
1272  id2string(tia_element.name) + "::" + DATA_BLOCK_PARAMETER_NAME)};
1273  const symbol_exprt db_expr = data_block.symbol_expr();
1274  const struct_typet *const db_type =
1275  type_try_dynamic_cast<struct_typet>(db_expr.type().subtype());
1276  if(!db_type)
1277  UNREACHABLE;
1278  for(const struct_union_typet::componentt &member : db_type->components())
1279  {
1280  if(member.get_name() == identifier)
1281  {
1282  const dereference_exprt deref_db{db_expr};
1283  const member_exprt val{deref_db, member.get_name(), member.type()};
1284  return val;
1285  }
1286  }
1287  }
1288  else if(
1289  element_type.get(ID_statement_list_type) == ID_statement_list_function)
1290  {
1291  // Check for variables inside of the function interface.
1292  for(const auto &member : element_type.parameters())
1293  {
1294  if(member.get_base_name() == identifier)
1295  {
1296  const symbolt &par{
1297  symbol_table.get_writeable_ref(member.get_identifier())};
1298  return par.symbol_expr();
1299  }
1300  }
1301  }
1302  else
1303  UNREACHABLE; // Variable declarations should only be checked for FCs or FBs
1304 
1305  error() << "Identifier could not be found in project" << eom;
1306  throw TYPECHECK_ERROR;
1307 }
1308 
1310  const codet &op_code,
1311  symbolt &tia_element)
1312 {
1313  const equal_exprt *const assignment =
1314  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1315  if(assignment)
1316  {
1317  const code_assertt assertion{
1318  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1319  tia_element.value.add_to_operands(assertion);
1320  }
1321  else
1322  {
1323  error() << "No assignment found for assertion" << eom;
1324  throw TYPECHECK_ERROR;
1325  }
1326 }
1327 
1329  const codet &op_code,
1330  symbolt &tia_element)
1331 {
1332  const equal_exprt *const assignment =
1333  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1334  if(assignment)
1335  {
1336  const code_assumet assumption{
1337  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1338  tia_element.value.add_to_operands(assumption);
1339  }
1340  else
1341  {
1342  error() << "No assignment found for assumption" << eom;
1343  throw TYPECHECK_ERROR;
1344  }
1345 }
1346 
1348  const codet &op_code,
1349  symbolt &tia_element)
1350 {
1351  const symbol_exprt &call_operand{to_symbol_expr(op_code.op0())};
1352  const symbolt &called_function{
1353  symbol_table.lookup_ref(call_operand.get_identifier())};
1354  const code_typet &called_type{to_code_type(called_function.type)};
1355  // Is it a STL function or STL function block?
1356  if(
1357  called_type.get(ID_statement_list_type) == ID_statement_list_function_block)
1358  typecheck_called_function_block(op_code, tia_element);
1359  else if(called_type.get(ID_statement_list_type) == ID_statement_list_function)
1360  typecheck_called_function(op_code, tia_element);
1361  else
1362  {
1363  error() << "Tried to call element that is no function or function block"
1364  << eom;
1365  throw TYPECHECK_ERROR;
1366  }
1367 }
1368 
1370  const codet &op_code,
1371  symbolt &tia_element)
1372 {
1373  const symbol_exprt call_operand{to_symbol_expr(op_code.op0())};
1374  const symbolt &called_function_sym{
1375  symbol_table.lookup_ref(call_operand.get_identifier())};
1376  const symbol_exprt called_function_expr{called_function_sym.symbol_expr()};
1377  const code_typet &called_type{to_code_type(called_function_sym.type)};
1378 
1379  // Check if function name is followed by data block.
1380  if(!can_cast_expr<equal_exprt>(op_code.op1()))
1381  {
1382  error() << "Function calls should not address instance data blocks" << eom;
1383  throw TYPECHECK_ERROR;
1384  }
1385 
1386  // Check if function interface matches the call and fill argument list.
1387  const code_typet::parameterst &params{called_type.parameters()};
1389  std::vector<equal_exprt> assignments;
1390  for(const auto &expr : op_code.operands())
1391  {
1392  if(can_cast_expr<equal_exprt>(expr))
1393  assignments.push_back(to_equal_expr(expr));
1394  }
1395 
1396  for(const code_typet::parametert &param : params)
1397  args.emplace_back(
1398  typecheck_function_call_arguments(assignments, param, tia_element));
1399 
1400  // Check the return value if present.
1401  if(called_type.return_type().is_nil())
1402  tia_element.value.add_to_operands(
1403  code_function_callt{called_function_expr, args});
1404  else
1405  {
1407  assignments, called_type.return_type(), tia_element)};
1408  tia_element.value.add_to_operands(
1409  code_function_callt{lhs, called_function_expr, args});
1410  }
1411 }
1412 
1414  const codet &op_code,
1415  symbolt &tia_element)
1416 {
1417  // TODO: Implement support for function block calls.
1418  // Needs code statements which assign the parameters to the instance data
1419  // block, call the function and write the result back to the parameters
1420  // afterwards.
1421  error() << "Calls to function blocks are not supported yet" << eom;
1422  throw TYPECHECK_ERROR;
1423 }
1424 
1426  const std::vector<equal_exprt> &assignments,
1427  const code_typet::parametert &param,
1428  const symbolt &tia_element)
1429 {
1430  const irep_idt &param_name = param.get_base_name();
1431  const typet &param_type = param.type();
1432  for(const equal_exprt &assignment : assignments)
1433  {
1434  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1435  if(param_name == lhs.get_identifier())
1436  {
1437  exprt assigned_variable{
1438  typecheck_function_call_argument_rhs(tia_element, assignment.rhs())};
1439 
1440  if(param_type == assigned_variable.type())
1441  return assigned_variable;
1442  else
1443  {
1444  error() << "Types of parameter assignment do not match: "
1445  << param.type().id() << " != " << assigned_variable.type().id()
1446  << eom;
1447  throw TYPECHECK_ERROR;
1448  }
1449  }
1450  }
1451  error() << "No assignment found for function parameter "
1452  << param.get_identifier() << eom;
1453  throw TYPECHECK_ERROR;
1454 }
1455 
1457  const symbolt &tia_element,
1458  const exprt &rhs)
1459 {
1460  exprt assigned_operand;
1461  const symbol_exprt *const symbol_rhs =
1462  expr_try_dynamic_cast<symbol_exprt>(rhs);
1463  if(symbol_rhs)
1464  assigned_operand =
1465  typecheck_identifier(tia_element, symbol_rhs->get_identifier());
1466  else // constant_exprt.
1467  assigned_operand = rhs;
1468  return assigned_operand;
1469 }
1470 
1472  const std::vector<equal_exprt> &assignments,
1473  const typet &return_type,
1474  const symbolt &tia_element)
1475 {
1476  for(const equal_exprt &assignment : assignments)
1477  {
1478  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1479  if(ID_statement_list_return_value_id == lhs.get_identifier())
1480  {
1481  const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())};
1482  const exprt assigned_variable{
1483  typecheck_identifier(tia_element, rhs.get_identifier())};
1484  if(return_type == assigned_variable.type())
1485  return assigned_variable;
1486  else
1487  {
1488  error() << "Types of return value assignment do not match: "
1489  << return_type.id() << " != " << assigned_variable.type().id()
1490  << eom;
1491  throw TYPECHECK_ERROR;
1492  }
1493  }
1494  }
1495  error() << "No assignment found for function return value" << eom;
1496  throw TYPECHECK_ERROR;
1497 }
1498 
1500 {
1501  or_exprt or_wrapper{to_or_expr(rlo_bit)};
1502 
1503  if(can_cast_expr<constant_exprt>(or_wrapper.op1()))
1504  or_wrapper.op1();
1505  else if(can_cast_expr<and_exprt>(or_wrapper.op1()))
1506  {
1507  and_exprt &and_op{to_and_expr(or_wrapper.op1())};
1508  and_op.add_to_operands(op);
1509  or_wrapper.op1() = and_op;
1510  }
1511  else
1512  {
1513  and_exprt and_op{or_wrapper.op1(), op};
1514  or_wrapper.op1() = and_op;
1515  }
1516  rlo_bit = or_wrapper;
1517 }
1518 
1520 {
1521  fc_bit = true;
1522  or_bit = false;
1523  rlo_bit = op;
1524 }
1525 
1527 {
1528  symbol_exprt temp_rlo{
1530  const code_assignt rlo_assignment{temp_rlo, rlo_bit};
1531  tia_element.value.add_to_operands(rlo_assignment);
1532  rlo_bit = std::move(temp_rlo);
1533 }
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:217
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:922
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:142
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:794
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:1077
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:903
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
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:1115
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:549
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:102
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:758
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:1309
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:938
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:1094
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
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: std_expr.h:2888
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:716
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:782
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:677
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:914
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:583
xor_exprt
Boolean XOR.
Definition: std_expr.h:2308
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:1021
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:556
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:587
and_exprt
Boolean AND.
Definition: std_expr.h:2137
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:881
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:664
CPROVER_TEMP_RLO
#define CPROVER_TEMP_RLO
Name of the RLO symbol used in some operations.
Definition: statement_list_typecheck.cpp:37
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
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:192
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:1136
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:1526
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:535
div_exprt
Division.
Definition: std_expr.h:1031
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:319
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:476
namespace.h
CPROVER_ASSUME
#define CPROVER_ASSUME
Name of the CBMC assume function.
Definition: statement_list_typecheck.cpp:35
equal_exprt
Equality.
Definition: std_expr.h:1190
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:276
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:703
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:69
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:188
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:1214
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
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:650
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:954
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:816
TYPECHECK_ERROR
#define TYPECHECK_ERROR
Definition: statement_list_typecheck.cpp:27
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:489
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:1328
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:1347
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:298
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:1425
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2173
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:622
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:563
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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:737
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:797
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:730
empty_typet
The empty type.
Definition: std_types.h:46
or_exprt
Boolean OR.
Definition: std_expr.h:2245
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:440
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:1208
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:204
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:882
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:841
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:44
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:528
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:249
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:723
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:690
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:643
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:817
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:116
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:657
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:57
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
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
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:1471
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:1060
exprt::op1
exprt & op1()
Definition: expr.h:105
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
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:165
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:1158
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:1198
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:1413
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:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
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:502
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:77
minus_exprt
Binary minus.
Definition: std_expr.h:940
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:629
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:542
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2292
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:89
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:962
STATEMENT_LIST_PTR_WIDTH
#define STATEMENT_LIST_PTR_WIDTH
Size of pointers in Siemens TIA.
Definition: statement_list_typecheck.cpp:25
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:930
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:3405
struct_union_typet::componentt
Definition: std_types.h:64
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:1185
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:1247
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:1042
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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:461
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:751
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:1174
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:1519
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:442
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:609
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:946
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:792
code_typet::parametert
Definition: std_types.h:753
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1230
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:157
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:45
type_symbolt
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:146
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:596
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:636
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:847
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:862
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:1235
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:744
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:772
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:3928
exprt::operands
operandst & operands()
Definition: expr.h:95
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
codet::op1
exprt & op1()
Definition: expr.h:105
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:515
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: std_types.h:1488
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:3955
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:33
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:28
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:233
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:1499
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: std_types.h:1411
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2184
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:1219
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:1051
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:1369
DATA_BLOCK_TYPE_POSTFIX
#define DATA_BLOCK_TYPE_POSTFIX
Postfix for the type of a data block.
Definition: statement_list_typecheck.cpp:31
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:29
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:1456
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:2843
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:570