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 <util/cprover_prefix.h>
16 #include <util/message.h>
17 #include <util/namespace.h>
18 #include <util/pointer_expr.h>
19 #include <util/simplify_expr.h>
20 #include <util/std_code.h>
21 #include <util/symbol_table.h>
22 
24 #define STATEMENT_LIST_PTR_WIDTH 64
25 // TODO: Replace with more specific exception throws.
26 #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"
37 
38 static const std::vector<irep_idt> logic_sequence_initializers = {
39  ID_statement_list_and,
40  ID_statement_list_and_not,
41  ID_statement_list_or,
42  ID_statement_list_or_not,
43  ID_statement_list_xor,
44  ID_statement_list_xor_not,
45  ID_statement_list_and_nested,
46  ID_statement_list_and_not_nested,
47  ID_statement_list_or_nested,
48  ID_statement_list_or_not_nested,
49  ID_statement_list_xor_nested,
50  ID_statement_list_xor_not_nested,
51 };
52 
53 static const std::vector<irep_idt> logic_sequence_terminators = {
54  ID_statement_list_set_rlo,
55  ID_statement_list_clr_rlo,
56  ID_statement_list_set,
57  ID_statement_list_reset,
58  ID_statement_list_assign,
59 };
60 
68  const struct_typet &data_block_type,
69  const irep_idt &function_block_name)
70 {
71  const pointer_typet db_ptr{data_block_type, STATEMENT_LIST_PTR_WIDTH};
72  code_typet::parametert param{db_ptr};
73  param.set_identifier(
74  id2string(function_block_name) + "::" + DATA_BLOCK_PARAMETER_NAME);
75  param.set_base_name(DATA_BLOCK_PARAMETER_NAME);
76  return param;
77 }
78 
80  const statement_list_parse_treet &parse_tree,
81  symbol_tablet &symbol_table,
82  const std::string &module,
83  message_handlert &message_handler)
84 {
85  statement_list_typecheckt stl_typecheck(
86  parse_tree, symbol_table, module, message_handler);
87 
88  return stl_typecheck.typecheck_main();
89 }
90 
92  exprt rlo_bit,
93  bool or_bit,
94  codet function_code)
95  : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
96 {
97 }
98 
100  size_t nesting_depth,
101  bool jumps_permitted,
102  bool fc_false_required)
103  : nesting_depth(nesting_depth),
104  jumps_permitted(jumps_permitted),
105  fc_false_required(fc_false_required)
106 {
107 }
109  size_t nesting_depth,
110  bool sets_fc_false)
111  : nesting_depth(nesting_depth), sets_fc_false(sets_fc_false)
112 {
113 }
114 
118  const std::string &module,
123  module(module)
124 {
125 }
126 
128 {
129  // First fill the symbol table with function, tag and parameter declarations
130  // to be able to properly resolve block calls later.
137  // Temporary RLO symbol for certain operations.
138  add_temp_rlo();
139 
140  // Iterate through all networks to generate the function bodies.
143  {
146  }
148  {
149  symbolt &function_sym{symbol_table.get_writeable_ref(fc.name)};
150  typecheck_statement_list_networks(fc, function_sym);
151  }
152 }
153 
155  const statement_list_parse_treet::function_blockt &function_block)
156 {
157  // Create FB symbol.
158  symbolt function_block_sym;
159  function_block_sym.module = module;
160  function_block_sym.name = function_block.name;
161  function_block_sym.base_name = function_block_sym.name;
162  function_block_sym.pretty_name = function_block_sym.name;
163  function_block_sym.mode = ID_statement_list;
164 
165  // When calling function blocks, the passed parameters are value-copied to a
166  // corresponding instance data block. This block contains all input, inout,
167  // output and static variables. The function block reads and writes only
168  // those fields and does not modify the actual parameters. To simulate this
169  // behaviour, all function blocks are modeled as functions with a single
170  // parameter: An instance of their data block, whose members they modify.
171 
172  // Create and add DB type symbol.
173  const struct_typet data_block_type{
174  create_instance_data_block_type(function_block)};
175  type_symbolt data_block{data_block_type};
176  data_block.name =
177  id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX;
178  data_block.base_name = data_block.name;
179  data_block.mode = ID_statement_list;
180  symbol_table.add(data_block);
181 
182  // Create and add parameter symbol.
184  create_data_block_parameter(data_block_type, function_block_sym.name)};
185  parameter_symbolt param_sym;
186  param_sym.module = module;
187  param_sym.type = param.type();
188  param_sym.name = param.get_identifier();
190  param_sym.pretty_name = param_sym.base_name;
191  param_sym.mode = ID_statement_list;
192  symbol_table.add(param_sym);
193 
194  // Setup FB symbol type and value.
196  params.push_back(param);
197  code_typet fb_type{params, empty_typet()};
198  fb_type.set(ID_statement_list_type, ID_statement_list_function_block);
199  function_block_sym.type = fb_type;
200  symbol_table.add(function_block_sym);
201 }
202 
205 {
206  symbolt function_sym;
207  function_sym.module = module;
208  function_sym.name = function.name;
209  function_sym.base_name = function_sym.name;
210  function_sym.pretty_name = function_sym.name;
211  function_sym.mode = ID_statement_list;
214  function.var_input, params, function.name, ID_statement_list_var_input);
216  function.var_inout, params, function.name, ID_statement_list_var_inout);
218  function.var_output, params, function.name, ID_statement_list_var_output);
219 
220  code_typet fc_type{params, function.return_type};
221  fc_type.set(ID_statement_list_type, ID_statement_list_function);
222  function_sym.type = fc_type;
223  symbol_table.add(function_sym);
224 }
225 
227 {
228  for(const symbol_exprt &tag : parse_tree.tags)
229  {
230  symbolt tag_sym;
231  tag_sym.is_static_lifetime = true;
232  tag_sym.module = module;
233  tag_sym.name = tag.get_identifier();
234  tag_sym.base_name = tag_sym.name;
235  tag_sym.pretty_name = tag_sym.name;
236  tag_sym.type = tag.type();
237  tag_sym.mode = ID_statement_list;
238  symbol_table.add(tag_sym);
239  }
240 }
241 
243 {
244  symbolt temp_rlo;
245  temp_rlo.is_static_lifetime = true;
246  temp_rlo.module = module;
247  temp_rlo.name = CPROVER_TEMP_RLO;
248  temp_rlo.base_name = temp_rlo.name;
249  temp_rlo.pretty_name = temp_rlo.name;
250  temp_rlo.type = get_bool_type();
251  temp_rlo.mode = ID_statement_list;
252  symbol_table.add(temp_rlo);
253 }
254 
256  const statement_list_parse_treet::function_blockt &function_block)
257 {
260  function_block.var_input, components, ID_statement_list_var_input);
262  function_block.var_inout, components, ID_statement_list_var_inout);
264  function_block.var_output, components, ID_statement_list_var_output);
266  function_block.var_static, components, ID_statement_list_var_static);
267 
268  return struct_typet{components};
269 }
270 
274  const irep_idt &var_property)
275 {
276  for(const statement_list_parse_treet::var_declarationt &declaration :
277  var_decls)
278  {
279  const irep_idt &var_name{declaration.variable.get_identifier()};
280  const typet &var_type{declaration.variable.type()};
281  struct_union_typet::componentt component{var_name, var_type};
282  component.set(ID_statement_list_type, var_property);
283  components.push_back(component);
284  }
285 }
286 
289  code_typet::parameterst &params,
290  const irep_idt &function_name,
291  const irep_idt &var_property)
292 {
293  for(const statement_list_parse_treet::var_declarationt &declaration :
294  var_decls)
295  {
296  parameter_symbolt param_sym;
297  param_sym.module = module;
298  param_sym.type = declaration.variable.type();
299  param_sym.name = id2string(function_name) +
300  "::" + id2string(declaration.variable.get_identifier());
301  param_sym.base_name = declaration.variable.get_identifier();
302  param_sym.pretty_name = param_sym.base_name;
303  param_sym.mode = ID_statement_list;
304  symbol_table.add(param_sym);
305 
306  code_typet::parametert param{declaration.variable.type()};
307  param.set_identifier(param_sym.name);
308  param.set_base_name(declaration.variable.get_identifier());
309  param.set(ID_statement_list_type, var_property);
310  params.push_back(param);
311  }
312 }
313 
315  const statement_list_parse_treet::tia_modulet &tia_module,
316  symbolt &tia_symbol)
317 {
318  for(const statement_list_parse_treet::var_declarationt &declaration :
319  tia_module.var_temp)
320  {
321  symbolt temp_sym;
322  temp_sym.name = id2string(tia_symbol.name) +
323  "::" + id2string(declaration.variable.get_identifier());
324  temp_sym.base_name = declaration.variable.get_identifier();
325  temp_sym.pretty_name = temp_sym.base_name;
326  temp_sym.type = declaration.variable.type();
327  temp_sym.mode = ID_statement_list;
328  temp_sym.module = module;
329  symbol_table.add(temp_sym);
330 
331  const code_declt code_decl{temp_sym.symbol_expr()};
332  tia_symbol.value.add_to_operands(code_decl);
333  }
334 }
335 
337  const statement_list_parse_treet::tia_modulet &tia_module,
338  symbolt &tia_symbol)
339 {
340  // Leave value empty if there are no networks to iterate through.
341  if(tia_module.networks.empty())
342  return;
343  if(tia_symbol.value.is_nil())
344  tia_symbol.value = code_blockt{};
345 
347  typecheck_temp_var_decls(tia_module, tia_symbol);
348 
349  for(const auto &network : tia_module.networks)
350  {
352  for(const auto &instruction : network.instructions)
353  typecheck_statement_list_instruction(instruction, tia_symbol);
354  }
356 }
357 
359 {
360  if(!label_references.empty())
361  {
362  error() << "Unable to find the labels:";
363  for(auto pair : label_references)
364  {
365  error() << "\n";
366  error() << id2string(pair.first);
367  }
368  error() << eom;
369  throw TYPECHECK_ERROR;
370  }
371 }
372 
374  const statement_list_parse_treet::instructiont &instruction,
375  symbolt &tia_element)
376 {
377  const codet &op_code{instruction.tokens.back()};
378  typecheck_code(op_code, tia_element);
379 }
380 
382  const codet &instruction,
383  symbolt &tia_element)
384 {
385  const irep_idt statement{instruction.get_statement()};
386 
387  if(ID_label == statement)
388  typecheck_label(instruction, tia_element);
389  else if(ID_statement_list_load == statement)
390  typecheck_statement_list_load(instruction, tia_element);
391  else if(ID_statement_list_transfer == statement)
392  typecheck_statement_list_transfer(instruction, tia_element);
393  else if(ID_statement_list_accu_int_add == statement)
395  else if(ID_statement_list_accu_int_sub == statement)
397  else if(ID_statement_list_accu_int_mul == statement)
399  else if(ID_statement_list_accu_int_div == statement)
401  else if(ID_statement_list_accu_int_eq == statement)
403  else if(ID_statement_list_accu_int_neq == statement)
405  else if(ID_statement_list_accu_int_lt == statement)
407  else if(ID_statement_list_accu_int_gt == statement)
409  else if(ID_statement_list_accu_int_lte == statement)
411  else if(ID_statement_list_accu_int_gte == statement)
413  else if(ID_statement_list_accu_dint_add == statement)
415  else if(ID_statement_list_accu_dint_sub == statement)
417  else if(ID_statement_list_accu_dint_mul == statement)
419  else if(ID_statement_list_accu_dint_div == statement)
421  else if(ID_statement_list_accu_dint_eq == statement)
423  else if(ID_statement_list_accu_dint_neq == statement)
425  else if(ID_statement_list_accu_dint_lt == statement)
427  else if(ID_statement_list_accu_dint_gt == statement)
429  else if(ID_statement_list_accu_dint_lte == statement)
431  else if(ID_statement_list_accu_dint_gte == statement)
433  else if(ID_statement_list_accu_real_add == statement)
435  else if(ID_statement_list_accu_real_sub == statement)
437  else if(ID_statement_list_accu_real_mul == statement)
439  else if(ID_statement_list_accu_real_div == statement)
441  else if(ID_statement_list_accu_real_eq == statement)
443  else if(ID_statement_list_accu_real_neq == statement)
445  else if(ID_statement_list_accu_real_lt == statement)
447  else if(ID_statement_list_accu_real_gt == statement)
449  else if(ID_statement_list_accu_real_lte == statement)
451  else if(ID_statement_list_accu_real_gte == statement)
453  else if(ID_statement_list_not == statement)
454  typecheck_statement_list_not(instruction);
455  else if(ID_statement_list_and == statement)
456  typecheck_statement_list_and(instruction, tia_element);
457  else if(ID_statement_list_and_not == statement)
458  typecheck_statement_list_and_not(instruction, tia_element);
459  else if(ID_statement_list_or == statement)
460  typecheck_statement_list_or(instruction, tia_element);
461  else if(ID_statement_list_or_not == statement)
462  typecheck_statement_list_or_not(instruction, tia_element);
463  else if(ID_statement_list_xor == statement)
464  typecheck_statement_list_xor(instruction, tia_element);
465  else if(ID_statement_list_xor_not == statement)
466  typecheck_statement_list_xor_not(instruction, tia_element);
467  else if(ID_statement_list_and_nested == statement)
469  else if(ID_statement_list_and_not_nested == statement)
471  else if(ID_statement_list_or_nested == statement)
473  else if(ID_statement_list_or_not_nested == statement)
475  else if(ID_statement_list_xor_nested == statement)
477  else if(ID_statement_list_xor_not_nested == statement)
479  else if(ID_statement_list_nesting_closed == statement)
481  else if(ID_statement_list_assign == statement)
482  typecheck_statement_list_assign(instruction, tia_element);
483  else if(ID_statement_list_set_rlo == statement)
485  else if(ID_statement_list_clr_rlo == statement)
487  else if(ID_statement_list_set == statement)
488  typecheck_statement_list_set(instruction, tia_element);
489  else if(ID_statement_list_reset == statement)
490  typecheck_statement_list_reset(instruction, tia_element);
491  else if(ID_statement_list_jump_unconditional == statement)
492  typecheck_statement_list_jump_unconditional(instruction, tia_element);
493  else if(ID_statement_list_jump_conditional == statement)
494  typecheck_statement_list_jump_conditional(instruction, tia_element);
495  else if(ID_statement_list_jump_conditional_not == statement)
496  typecheck_statement_list_jump_conditional_not(instruction, tia_element);
497  else if(ID_statement_list_nop == statement)
498  return;
499  else if(ID_statement_list_call == statement)
500  typecheck_statement_list_call(instruction, tia_element);
501  else
502  {
503  error() << "OP code of instruction not found: "
504  << instruction.get_statement() << eom;
505  throw TYPECHECK_ERROR;
506  }
507 }
508 
510  const codet &instruction,
511  symbolt &tia_element)
512 {
513  const code_labelt &label = to_code_label(instruction);
514 
515  // Check if label is duplicate (not allowed in STL).
516  if(stl_labels.find(label.get_label()) != end(stl_labels))
517  {
518  error() << "Multiple definitions of label " << id2string(label.get_label())
519  << eom;
520  throw TYPECHECK_ERROR;
521  }
522 
523  // Determine the properties of this location in the code.
525 
526  // Store the implicit RLO in order to correctly separate the different
527  // blocks of logic.
528  if(location.jumps_permitted)
529  save_rlo_state(tia_element);
530 
531  // Now check if there are any jumps that referenced that label before and
532  // validate these.
533  typecheck_jump_locations(label, location);
534 
535  // Only add the label to the code if jumps are permitted. Proceed as normal
536  // if they are not. An added label will always point at an empty code
537  // location due to the way how the typecheck works.
538  if(location.jumps_permitted)
539  tia_element.value.add_to_operands(
540  code_labelt{label.get_label(), code_skipt{}});
541 
542  // Recursive call to check the label target.
543  typecheck_code(label.code(), tia_element);
544 }
545 
548 {
549  // Jumps to a label are only allowed if one of the following conditions
550  // applies:
551  //
552  // a) The /FC bit is false when encountering the instruction (pointing at the
553  // beginning of a logic sequence or no sequence at all).
554  // b) The /FC bit is set to false after processing the instruction (pointing
555  // at the termination of a logic sequence). This excludes nesting-open
556  // operations since although they terminate the current sequence, it will
557  // be resumed later.
558  //
559  // Labels at locations where this does not hold true compile, but actual
560  // jumps to them do not.
561  //
562  // Additionally, jumps to instructions that mark the beginning of a logic
563  // sequence are only allowed if the jump instruction itself sets the /FC bit
564  // to false.
565 
566  bool jumps_permitted = false;
567  bool fc_false_required = false;
568  if(!fc_bit)
569  {
570  jumps_permitted = true;
571  // Check if label points to new logic sequence.
572  for(const irep_idt &op_code : logic_sequence_initializers)
573  if(op_code == label.code().get_statement())
574  {
575  fc_false_required = true;
576  break;
577  }
578  }
579  else // Check if the label's instruction terminates the logic sequence.
580  {
581  for(const irep_idt &op_code : logic_sequence_terminators)
582  if(op_code == label.code().get_statement())
583  {
584  jumps_permitted = true;
585  break;
586  }
587  }
588 
589  // Add the label to map.
590  stl_label_locationt location{
591  nesting_stack.size(), jumps_permitted, fc_false_required};
592  stl_labels.emplace(label.get_label(), location);
593  return location;
594 }
595 
597  const code_labelt &label,
599 {
600  // Now check if there are any jumps that referenced that label before and
601  // validate these.
602  auto reference_it = label_references.find(label.get_label());
603  if(reference_it != end(label_references))
604  {
605  if(!location.jumps_permitted)
606  {
607  error() << "Not allowed to jump to label " << id2string(label.get_label())
608  << eom;
609  throw TYPECHECK_ERROR;
610  }
611  for(auto jump_location_it = begin(reference_it->second);
612  jump_location_it != end(reference_it->second);
613  ++jump_location_it)
614  {
615  if(location.fc_false_required && !jump_location_it->sets_fc_false)
616  {
617  error() << "Jump to label " << id2string(label.get_label())
618  << " can not be unconditional" << eom;
619  throw TYPECHECK_ERROR;
620  }
621  if(nesting_stack.size() != jump_location_it->nesting_depth)
622  {
623  error() << "Jump to label " << id2string(label.get_label())
624  << " violates brace scope" << eom;
625  throw TYPECHECK_ERROR;
626  }
627  }
628  // Remove entry after validation.
629  label_references.erase(label.get_label());
630  }
631 }
632 
634  const codet &op_code,
635  const symbolt &tia_element)
636 {
637  const symbol_exprt *const symbol =
638  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
639  if(symbol)
640  {
641  const irep_idt &identifier{symbol->get_identifier()};
642  const exprt val{typecheck_identifier(tia_element, identifier)};
643  accumulator.push_back(val);
644  }
645  else if(can_cast_expr<constant_exprt>(op_code.op0()))
646  accumulator.push_back(op_code.op0());
647  else
648  {
649  error() << "Instruction is not followed by symbol or constant" << eom;
650  throw TYPECHECK_ERROR;
651  }
652 }
653 
655  const codet &op_code,
656  symbolt &tia_element)
657 {
659  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
660  if(lhs.type() != accumulator.back().type())
661  {
662  error() << "Types of transfer assignment do not match" << eom;
663  throw TYPECHECK_ERROR;
664  }
665  const code_assignt assignment{lhs, accumulator.back()};
666  tia_element.value.add_to_operands(assignment);
667 }
668 
670  const codet &op_code)
671 {
673 
674  // Pop first operand, peek second.
675  const exprt accu1{accumulator.back()};
676  accumulator.pop_back();
677  const exprt &accu2{accumulator.back()};
678  const plus_exprt operation{accu2, accu1};
679  accumulator.push_back(operation);
680 }
681 
683  const codet &op_code)
684 {
686 
687  // Pop first operand, peek second.
688  const exprt accu1{accumulator.back()};
689  accumulator.pop_back();
690  const exprt &accu2{accumulator.back()};
691  const minus_exprt operation{accu2, accu1};
692  accumulator.push_back(operation);
693 }
694 
696  const codet &op_code)
697 {
699 
700  // Pop first operand, peek second.
701  const exprt accu1{accumulator.back()};
702  accumulator.pop_back();
703  const exprt &accu2{accumulator.back()};
704  const mult_exprt operation{accu2, accu1};
705  accumulator.push_back(operation);
706 }
707 
709  const codet &op_code)
710 {
712 
713  // Pop first operand, peek second.
714  const exprt accu1{accumulator.back()};
715  accumulator.pop_back();
716  const exprt &accu2{accumulator.back()};
717  const div_exprt operation{accu2, accu1};
718  accumulator.push_back(operation);
719 }
720 
722  const codet &op_code)
723 {
726 }
727 
729  const codet &op_code)
730 {
733 }
734 
736  const codet &op_code)
737 {
740 }
741 
743  const codet &op_code)
744 {
747 }
748 
750  const codet &op_code)
751 {
754 }
755 
757  const codet &op_code)
758 {
761 }
762 
764  const codet &op_code)
765 {
767 
768  // Pop first operand, peek second.
769  const exprt accu1{accumulator.back()};
770  accumulator.pop_back();
771  const exprt &accu2{accumulator.back()};
772  const plus_exprt operation{accu2, accu1};
773  accumulator.push_back(operation);
774 }
775 
777  const codet &op_code)
778 {
780 
781  // Pop first operand, peek second.
782  const exprt accu1{accumulator.back()};
783  accumulator.pop_back();
784  const exprt &accu2{accumulator.back()};
785  const minus_exprt operation{accu2, accu1};
786  accumulator.push_back(operation);
787 }
788 
790  const codet &op_code)
791 {
793 
794  // Pop first operand, peek second.
795  const exprt accu1{accumulator.back()};
796  accumulator.pop_back();
797  const exprt &accu2{accumulator.back()};
798  const mult_exprt operation{accu2, accu1};
799  accumulator.push_back(operation);
800 }
801 
803  const codet &op_code)
804 {
806 
807  // Pop first operand, peek second.
808  const exprt accu1{accumulator.back()};
809  accumulator.pop_back();
810  const exprt &accu2{accumulator.back()};
811  const div_exprt operation{accu2, accu1};
812  accumulator.push_back(operation);
813 }
814 
816  const codet &op_code)
817 {
820 }
821 
823  const codet &op_code)
824 {
827 }
828 
830  const codet &op_code)
831 {
834 }
835 
837  const codet &op_code)
838 {
841 }
842 
844  const codet &op_code)
845 {
848 }
849 
851  const codet &op_code)
852 {
855 }
856 
858  const codet &op_code)
859 {
861 
862  // Pop first operand, peek second.
863  const exprt accu1{accumulator.back()};
864  accumulator.pop_back();
865  const exprt &accu2{accumulator.back()};
866  const plus_exprt operation{accu2, accu1};
867  accumulator.push_back(operation);
868 }
869 
871  const codet &op_code)
872 {
874 
875  // Pop first operand, peek second.
876  const exprt accu1{accumulator.back()};
877  accumulator.pop_back();
878  const exprt &accu2{accumulator.back()};
879  const minus_exprt operation{accu2, accu1};
880  accumulator.push_back(operation);
881 }
882 
884  const codet &op_code)
885 {
887 
888  // Pop first operand, peek second.
889  const exprt accu1{accumulator.back()};
890  accumulator.pop_back();
891  const exprt &accu2{accumulator.back()};
892  const mult_exprt operation{accu2, accu1};
893  accumulator.push_back(operation);
894 }
895 
897  const codet &op_code)
898 {
900 
901  // Pop first operand, peek second.
902  const exprt accu1{accumulator.back()};
903  accumulator.pop_back();
904  const exprt &accu2{accumulator.back()};
905  const div_exprt operation{accu2, accu1};
906  accumulator.push_back(operation);
907 }
908 
910  const codet &op_code)
911 {
914 }
915 
917  const codet &op_code)
918 {
921 }
922 
924  const codet &op_code)
925 {
928 }
929 
931  const codet &op_code)
932 {
935 }
936 
938  const codet &op_code)
939 {
942 }
943 
945  const codet &op_code)
946 {
949 }
950 
952  const codet &op_code)
953 {
955  const not_exprt unsimplified{rlo_bit};
956  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
957 }
958 
960  const codet &op_code,
961  const symbolt &tia_element)
962 {
963  exprt op{
964  typecheck_simple_boolean_instruction_operand(op_code, tia_element, false)};
965 
966  // If inside of a bit string and if the OR bit is not set, create an 'and'
967  // expression with the operand and the current contents of the rlo bit. If
968  // the OR bit is set then this instruction is part of an 'and-before-or'
969  // block and needs to be added to the rlo in a special way.
970  if(fc_bit && or_bit)
972  else if(fc_bit)
973  {
974  const and_exprt unsimplified{rlo_bit, op};
975  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
976  }
977  else
979 }
980 
982  const codet &op_code,
983  const symbolt &tia_element)
984 {
985  exprt op{
986  typecheck_simple_boolean_instruction_operand(op_code, tia_element, true)};
987 
988  // If inside of a bit string and if the OR bit is not set, create an 'and'
989  // expression with the operand and the current contents of the rlo bit. If
990  // the OR bit is set then this instruction is part of an 'and-before-or'
991  // block and needs to be added to the rlo in a special way.
992  if(or_bit && fc_bit)
994  else if(fc_bit)
995  {
996  const and_exprt unsimplified{rlo_bit, op};
997  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
998  }
999  else
1001 }
1002 
1004  const codet &op_code,
1005  const symbolt &tia_element)
1006 {
1007  if(op_code.operands().empty())
1008  {
1010  return;
1011  }
1012  const symbol_exprt &sym{
1014  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1015 
1016  // If inside of a bit string, create an 'or' expression with the operand and
1017  // the current contents of the rlo bit.
1018  if(fc_bit)
1019  {
1020  const or_exprt unsimplified{rlo_bit, op};
1021  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
1022  or_bit = false;
1023  }
1024  else
1026 }
1027 
1029  const codet &op_code,
1030  const symbolt &tia_element)
1031 {
1032  const symbol_exprt &sym{
1034  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1035  const not_exprt not_op{op};
1036 
1037  // If inside of a bit string, create an 'or' expression with the operand and
1038  // the current contents of the rlo bit.
1039  if(fc_bit)
1040  {
1041  const or_exprt unsimplified{rlo_bit, not_op};
1042  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
1043  or_bit = false;
1044  }
1045  else
1046  initialize_bit_expression(not_op);
1047 }
1048 
1050  const codet &op_code,
1051  const symbolt &tia_element)
1052 {
1053  const symbol_exprt &sym{
1055  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1056 
1057  // If inside of a bit string, create an 'xor' expression with the operand and
1058  // the current contents of the rlo bit.
1059  if(fc_bit)
1060  {
1061  const xor_exprt unsimplified{rlo_bit, op};
1062  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
1063  or_bit = false;
1064  }
1065  else
1067 }
1068 
1070  const codet &op_code,
1071  const symbolt &tia_element)
1072 {
1073  const symbol_exprt &sym{
1075  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1076  const not_exprt not_op{op};
1077 
1078  // If inside of a bit string, create an 'xor not' expression with the
1079  // operand and the current contents of the rlo bit.
1080  if(fc_bit)
1081  {
1082  const xor_exprt unsimplified{rlo_bit, not_op};
1083  rlo_bit = simplify_expr(unsimplified, namespacet(symbol_table));
1084  or_bit = false;
1085  }
1086  else
1087  initialize_bit_expression(not_op);
1088 }
1089 
1091 {
1092  if(fc_bit)
1093  {
1095  or_bit = true;
1096  }
1097  else
1098  return; // Instruction has no semantic influence.
1099 }
1100 
1102  const codet &op_code)
1103 {
1104  // Set the rlo to true implicitly so that the value of the AND instruction
1105  // is being loaded in case of a new bit string.
1107 }
1108 
1110  const codet &op_code)
1111 {
1112  // Set the rlo to true implicitly so that the value of the AND instruction
1113  // is being loaded in case of a new bit string.
1115 }
1116 
1118  const codet &op_code)
1119 {
1120  // Set the rlo to false implicitly so that the value of the OR instruction
1121  // is being loaded in case of a new bit string.
1123 }
1124 
1126  const codet &op_code)
1127 {
1128  // Set the rlo to false implicitly so that the value of the OR instruction
1129  // is being loaded in case of a new bit string.
1131 }
1132 
1134  const codet &op_code)
1135 {
1136  // Set the rlo to false implicitly so that the value of the XOR instruction
1137  // is being loaded in case of a new bit string.
1139 }
1140 
1142  const codet &op_code)
1143 {
1144  // Set the rlo to false implicitly so that the value of the XOR instruction
1145  // is being loaded in case of a new bit string.
1147 }
1148 
1150  const codet &op_code)
1151 {
1153  if(nesting_stack.empty())
1154  {
1155  error() << "Wrong order of brackets (Right parenthesis is not preceded by "
1156  "nesting)"
1157  << eom;
1158  throw TYPECHECK_ERROR;
1159  }
1160  or_bit = nesting_stack.back().or_bit;
1161  fc_bit = true;
1162  const irep_idt &statement{nesting_stack.back().function_code.get_statement()};
1163  if(ID_statement_list_and_nested == statement)
1164  {
1165  if(or_bit)
1166  {
1167  const exprt op{rlo_bit};
1168  rlo_bit = nesting_stack.back().rlo_bit;
1170  }
1171  else
1172  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1173  }
1174  else if(ID_statement_list_and_not_nested == statement)
1175  {
1176  if(or_bit)
1177  {
1178  const not_exprt op{rlo_bit};
1179  rlo_bit = nesting_stack.back().rlo_bit;
1181  }
1182  else
1183  rlo_bit = and_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1184  }
1185  else if(ID_statement_list_or_nested == statement)
1186  {
1187  or_bit = false;
1188  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1189  }
1190  else if(ID_statement_list_or_not_nested == statement)
1191  {
1192  or_bit = false;
1193  rlo_bit = or_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1194  }
1195  else if(ID_statement_list_xor_nested == statement)
1196  {
1197  or_bit = false;
1198  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1199  }
1200  else if(ID_statement_list_xor_not_nested == statement)
1201  {
1202  or_bit = false;
1203  rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1204  }
1205  nesting_stack.pop_back();
1206 }
1207 
1209  const codet &op_code,
1210  symbolt &tia_element)
1211 {
1213  const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
1214 
1215  if(lhs.type() != rlo_bit.type())
1216  {
1217  error() << "Types of assign do not match" << eom;
1218  throw TYPECHECK_ERROR;
1219  }
1220  const code_assignt assignment{lhs, rlo_bit};
1221  tia_element.value.add_to_operands(assignment);
1222  fc_bit = false;
1223  or_bit = false;
1224  // Set RLO to assigned operand in order to prevent false results if a symbol
1225  // that's implicitly part of the RLO was changed by the assignment.
1226  rlo_bit = lhs;
1227 }
1228 
1230  const codet &op_code)
1231 {
1233  fc_bit = false;
1234  or_bit = false;
1235  rlo_bit = true_exprt();
1236 }
1237 
1239  const codet &op_code)
1240 {
1242  fc_bit = false;
1243  or_bit = false;
1244  rlo_bit = false_exprt();
1245 }
1246 
1248  const codet &op_code,
1249  symbolt &tia_element)
1250 {
1252  const irep_idt &identifier{op.get_identifier()};
1253 
1254  save_rlo_state(tia_element);
1255 
1256  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1257  const code_assignt assignment{lhs, true_exprt()};
1258  const code_ifthenelset ifthen{rlo_bit, assignment};
1259  tia_element.value.add_to_operands(ifthen);
1260  fc_bit = false;
1261  or_bit = false;
1262 }
1263 
1265  const codet &op_code,
1266  symbolt &tia_element)
1267 {
1269  const irep_idt &identifier{op.get_identifier()};
1270 
1271  save_rlo_state(tia_element);
1272 
1273  const exprt lhs{typecheck_identifier(tia_element, identifier)};
1274  const code_assignt assignment{lhs, false_exprt()};
1275  const code_ifthenelset ifthen{rlo_bit, assignment};
1276  tia_element.value.add_to_operands(ifthen);
1277  fc_bit = false;
1278  or_bit = false;
1279 }
1280 
1282  const codet &op_code,
1283  symbolt &tia_element)
1284 {
1286  const irep_idt &identifier{op.get_identifier()};
1287  if(symbol_table.has_symbol(identifier))
1288  typecheck_called_tia_element(op_code, tia_element);
1289  else if(identifier == CPROVER_ASSUME)
1290  typecheck_CPROVER_assume(op_code, tia_element);
1291  else if(identifier == CPROVER_ASSERT)
1292  typecheck_CPROVER_assert(op_code, tia_element);
1293  else
1294  {
1295  error() << "Called function could not be found" << eom;
1296  throw TYPECHECK_ERROR;
1297  }
1298  fc_bit = false;
1299  or_bit = false;
1300 }
1301 
1303  const codet &op_code,
1304  symbolt &tia_element)
1305 {
1306  const symbol_exprt &label{
1308  typecheck_label_reference(label.get_identifier(), false);
1309 
1310  save_rlo_state(tia_element);
1311  code_gotot unconditional{label.get_identifier()};
1312  tia_element.value.add_to_operands(unconditional);
1313 }
1314 
1316  const codet &op_code,
1317  symbolt &tia_element)
1318 {
1319  const symbol_exprt &label{
1321  typecheck_label_reference(label.get_identifier(), true);
1322 
1323  save_rlo_state(tia_element);
1324  code_gotot jump{label.get_identifier()};
1325  code_ifthenelset conditional{rlo_bit, jump};
1326  tia_element.value.add_to_operands(conditional);
1327 
1328  fc_bit = false;
1329  or_bit = false;
1330  rlo_bit = true_exprt{};
1331 }
1332 
1334  const codet &op_code,
1335  symbolt &tia_element)
1336 {
1337  const symbol_exprt &label{
1339  typecheck_label_reference(label.get_identifier(), true);
1340 
1341  save_rlo_state(tia_element);
1342  code_gotot jump{label.get_identifier()};
1343  code_ifthenelset not_conditional{not_exprt{rlo_bit}, jump};
1344  tia_element.value.add_to_operands(not_conditional);
1345 
1346  fc_bit = false;
1347  or_bit = false;
1348  rlo_bit = true_exprt{};
1349 }
1350 
1352  const codet &op_code)
1353 {
1355  const exprt &accu1{accumulator.back()};
1356  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1357 
1358  // Are both operands integers?
1359  const signedbv_typet *const accu_type1 =
1360  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1361  const signedbv_typet *const accu_type2 =
1362  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1363  if(
1364  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_INT_WIDTH ||
1365  accu_type2->get_width() != STL_INT_WIDTH)
1366  {
1367  error() << "Operands of integer addition are no integers" << eom;
1368  throw TYPECHECK_ERROR;
1369  }
1370 }
1371 
1373  const codet &op_code)
1374 {
1376  const exprt &accu1{accumulator.back()};
1377  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1378 
1379  // Are both operands double integers?
1380  const signedbv_typet *const accu_type1 =
1381  type_try_dynamic_cast<signedbv_typet>(accu1.type());
1382  const signedbv_typet *const accu_type2 =
1383  type_try_dynamic_cast<signedbv_typet>(accu2.type());
1384  if(
1385  !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_DINT_WIDTH ||
1386  accu_type2->get_width() != STL_DINT_WIDTH)
1387  {
1388  error() << "Operands of double integer addition are no double integers"
1389  << eom;
1390  throw TYPECHECK_ERROR;
1391  }
1392 }
1393 
1395  const codet &op_code)
1396 {
1398  const exprt &accu1{accumulator.back()};
1399  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1400 
1401  // Are both operands real types?
1402  if(!(can_cast_type<floatbv_typet>(accu1.type()) &&
1403  can_cast_type<floatbv_typet>(accu2.type())))
1404  {
1405  error() << "Operands of Real addition do not have the type Real" << eom;
1406  throw TYPECHECK_ERROR;
1407  }
1408 }
1409 
1411  const irep_idt &comparison)
1412 {
1413  const exprt &accu1{accumulator.back()};
1414  const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1415  // STL behaviour: ACCU2 is lhs, ACCU1 is rhs.
1416  const binary_relation_exprt operation{accu2, comparison, accu1};
1417  rlo_bit = operation;
1418 }
1419 
1421  const irep_idt &label,
1422  bool sets_fc_false)
1423 {
1424  // If the label is already present in the list, check if it matches the
1425  // criteria.
1426  auto label_it = stl_labels.find(label);
1427  if(label_it != end(stl_labels))
1428  {
1429  if(!label_it->second.jumps_permitted)
1430  {
1431  error() << "Not allowed to jump to label " << id2string(label_it->first)
1432  << eom;
1433  throw TYPECHECK_ERROR;
1434  }
1435 
1436  if(label_it->second.fc_false_required && !sets_fc_false)
1437  {
1438  error() << "Jump to label " << id2string(label_it->first)
1439  << " can not be unconditional" << eom;
1440  throw TYPECHECK_ERROR;
1441  }
1442 
1443  if(label_it->second.nesting_depth != nesting_stack.size())
1444  {
1445  error() << "Jump to label " << id2string(label_it->first)
1446  << " violates brace scope" << eom;
1447  throw TYPECHECK_ERROR;
1448  }
1449  }
1450  else // If it was not encountered yet, create a new reference entry.
1451  {
1452  stl_jump_locationt location{nesting_stack.size(), sets_fc_false};
1453  auto reference_it = label_references.find(label);
1454  if(reference_it == end(label_references))
1455  {
1456  std::vector<stl_jump_locationt> locations;
1457  locations.push_back(location);
1458  label_references.emplace(label, locations);
1459  }
1460  else
1461  reference_it->second.push_back(location);
1462  }
1463 }
1464 
1465 const symbol_exprt &
1467  const codet &op_code)
1468 {
1469  const symbol_exprt *const symbol =
1470  expr_try_dynamic_cast<symbol_exprt>(op_code.op0());
1471 
1472  if(symbol)
1473  return *symbol;
1474 
1475  error() << "Instruction is not followed by symbol" << eom;
1476  throw TYPECHECK_ERROR;
1477 }
1478 
1480  const codet &op_code)
1481 {
1482  if(op_code.operands().size() > 0)
1483  {
1484  error() << "Instruction is followed by operand" << eom;
1485  throw TYPECHECK_ERROR;
1486  }
1487 }
1488 
1490  const codet &op_code)
1491 {
1493  if(accumulator.size() < 2)
1494  {
1495  error() << "Not enough operands in the accumulator" << eom;
1496  throw TYPECHECK_ERROR;
1497  }
1498 }
1499 
1501  const codet &op_code,
1502  const exprt &rlo_value)
1503 {
1505  // If inside of a bit string use the value of the rlo. If this is the first
1506  // expression of a bit string, load the value of the nested operation by
1507  // implicitly setting the rlo to the specified value.
1508  if(!fc_bit)
1509  rlo_bit = rlo_value;
1510  const nesting_stack_entryt stack_entry{rlo_bit, or_bit, op_code};
1511  nesting_stack.push_back(stack_entry);
1512  fc_bit = false;
1513  or_bit = false;
1514 }
1515 
1517  const codet &op_code,
1518  const symbolt &tia_element,
1519  bool negate)
1520 {
1521  const symbol_exprt &sym{
1523  const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1524  const not_exprt not_op{op};
1525  return negate ? not_op : op;
1526 }
1527 
1529  const symbolt &tia_element,
1530  const irep_idt &identifier)
1531 {
1532  const code_typet &element_type{to_code_type(tia_element.type)};
1533 
1534  // Check for temporary variables.
1536  id2string(tia_element.name) + "::" + id2string(identifier)))
1537  {
1538  const symbolt &sym{symbol_table.lookup_ref(
1539  id2string(tia_element.name) + "::" + id2string(identifier))};
1540  return sym.symbol_expr();
1541  }
1542 
1543  // Check for global tags.
1544  if(symbol_table.has_symbol(identifier))
1545  return symbol_table.lookup_ref(identifier).symbol_expr();
1546 
1547  if(
1548  element_type.get(ID_statement_list_type) ==
1549  ID_statement_list_function_block)
1550  {
1551  // Check for variables inside of the function block interface.
1552  const symbolt &data_block{symbol_table.get_writeable_ref(
1553  id2string(tia_element.name) + "::" + DATA_BLOCK_PARAMETER_NAME)};
1554  const symbol_exprt db_expr = data_block.symbol_expr();
1555  const struct_typet *const db_type =
1556  type_try_dynamic_cast<struct_typet>(db_expr.type().subtype());
1557  if(!db_type)
1558  UNREACHABLE;
1559  for(const struct_union_typet::componentt &member : db_type->components())
1560  {
1561  if(member.get_name() == identifier)
1562  {
1563  const dereference_exprt deref_db{db_expr};
1564  const member_exprt val{deref_db, member.get_name(), member.type()};
1565  return val;
1566  }
1567  }
1568  }
1569  else if(
1570  element_type.get(ID_statement_list_type) == ID_statement_list_function)
1571  {
1572  // Check for variables inside of the function interface.
1573  for(const auto &member : element_type.parameters())
1574  {
1575  if(member.get_base_name() == identifier)
1576  {
1577  const symbolt &par{
1578  symbol_table.get_writeable_ref(member.get_identifier())};
1579  return par.symbol_expr();
1580  }
1581  }
1582  }
1583  else
1584  UNREACHABLE; // Variable declarations should only be checked for FCs or FBs
1585 
1586  error() << "Identifier could not be found in project" << eom;
1587  throw TYPECHECK_ERROR;
1588 }
1589 
1591  const codet &op_code,
1592  symbolt &tia_element)
1593 {
1594  const equal_exprt *const assignment =
1595  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1596  if(assignment)
1597  {
1598  const code_assertt assertion{
1599  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1600  tia_element.value.add_to_operands(assertion);
1601  }
1602  else
1603  {
1604  error() << "No assignment found for assertion" << eom;
1605  throw TYPECHECK_ERROR;
1606  }
1607 }
1608 
1610  const codet &op_code,
1611  symbolt &tia_element)
1612 {
1613  const equal_exprt *const assignment =
1614  expr_try_dynamic_cast<equal_exprt>(op_code.op1());
1615  if(assignment)
1616  {
1617  const code_assumet assumption{
1618  typecheck_function_call_argument_rhs(tia_element, assignment->rhs())};
1619  tia_element.value.add_to_operands(assumption);
1620  }
1621  else
1622  {
1623  error() << "No assignment found for assumption" << eom;
1624  throw TYPECHECK_ERROR;
1625  }
1626 }
1627 
1629  const codet &op_code,
1630  symbolt &tia_element)
1631 {
1632  const symbol_exprt &call_operand{to_symbol_expr(op_code.op0())};
1633  const symbolt &called_function{
1634  symbol_table.lookup_ref(call_operand.get_identifier())};
1635  const code_typet &called_type{to_code_type(called_function.type)};
1636  // Is it a STL function or STL function block?
1637  if(
1638  called_type.get(ID_statement_list_type) == ID_statement_list_function_block)
1639  typecheck_called_function_block(op_code, tia_element);
1640  else if(called_type.get(ID_statement_list_type) == ID_statement_list_function)
1641  typecheck_called_function(op_code, tia_element);
1642  else
1643  {
1644  error() << "Tried to call element that is no function or function block"
1645  << eom;
1646  throw TYPECHECK_ERROR;
1647  }
1648 }
1649 
1651  const codet &op_code,
1652  symbolt &tia_element)
1653 {
1654  const symbol_exprt call_operand{to_symbol_expr(op_code.op0())};
1655  const symbolt &called_function_sym{
1656  symbol_table.lookup_ref(call_operand.get_identifier())};
1657  const symbol_exprt called_function_expr{called_function_sym.symbol_expr()};
1658  const code_typet &called_type{to_code_type(called_function_sym.type)};
1659 
1660  // Check if function name is followed by data block.
1661  if(!can_cast_expr<equal_exprt>(op_code.op1()))
1662  {
1663  error() << "Function calls should not address instance data blocks" << eom;
1664  throw TYPECHECK_ERROR;
1665  }
1666 
1667  // Check if function interface matches the call and fill argument list.
1668  const code_typet::parameterst &params{called_type.parameters()};
1670  std::vector<equal_exprt> assignments;
1671  for(const auto &expr : op_code.operands())
1672  {
1673  if(can_cast_expr<equal_exprt>(expr))
1674  assignments.push_back(to_equal_expr(expr));
1675  }
1676 
1677  for(const code_typet::parametert &param : params)
1678  args.emplace_back(
1679  typecheck_function_call_arguments(assignments, param, tia_element));
1680 
1681  // Check the return value if present.
1682  if(called_type.return_type().is_nil())
1683  tia_element.value.add_to_operands(
1684  code_function_callt{called_function_expr, args});
1685  else
1686  {
1688  assignments, called_type.return_type(), tia_element)};
1689  tia_element.value.add_to_operands(
1690  code_function_callt{lhs, called_function_expr, args});
1691  }
1692 }
1693 
1695  const codet &op_code,
1696  symbolt &tia_element)
1697 {
1698  // TODO: Implement support for function block calls.
1699  // Needs code statements which assign the parameters to the instance data
1700  // block, call the function and write the result back to the parameters
1701  // afterwards.
1702  error() << "Calls to function blocks are not supported yet" << eom;
1703  throw TYPECHECK_ERROR;
1704 }
1705 
1707  const std::vector<equal_exprt> &assignments,
1708  const code_typet::parametert &param,
1709  const symbolt &tia_element)
1710 {
1711  const irep_idt &param_name = param.get_base_name();
1712  const typet &param_type = param.type();
1713  for(const equal_exprt &assignment : assignments)
1714  {
1715  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1716  if(param_name == lhs.get_identifier())
1717  {
1718  exprt assigned_variable{
1719  typecheck_function_call_argument_rhs(tia_element, assignment.rhs())};
1720 
1721  if(param_type == assigned_variable.type())
1722  return assigned_variable;
1723  else
1724  {
1725  error() << "Types of parameter assignment do not match: "
1726  << param.type().id() << " != " << assigned_variable.type().id()
1727  << eom;
1728  throw TYPECHECK_ERROR;
1729  }
1730  }
1731  }
1732  error() << "No assignment found for function parameter "
1733  << param.get_identifier() << eom;
1734  throw TYPECHECK_ERROR;
1735 }
1736 
1738  const symbolt &tia_element,
1739  const exprt &rhs)
1740 {
1741  exprt assigned_operand;
1742  const symbol_exprt *const symbol_rhs =
1743  expr_try_dynamic_cast<symbol_exprt>(rhs);
1744  if(symbol_rhs)
1745  assigned_operand =
1746  typecheck_identifier(tia_element, symbol_rhs->get_identifier());
1747  else // constant_exprt.
1748  assigned_operand = rhs;
1749  return assigned_operand;
1750 }
1751 
1753  const std::vector<equal_exprt> &assignments,
1754  const typet &return_type,
1755  const symbolt &tia_element)
1756 {
1757  for(const equal_exprt &assignment : assignments)
1758  {
1759  const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1760  if(ID_statement_list_return_value_id == lhs.get_identifier())
1761  {
1762  const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())};
1763  const exprt assigned_variable{
1764  typecheck_identifier(tia_element, rhs.get_identifier())};
1765  if(return_type == assigned_variable.type())
1766  return assigned_variable;
1767  else
1768  {
1769  error() << "Types of return value assignment do not match: "
1770  << return_type.id() << " != " << assigned_variable.type().id()
1771  << eom;
1772  throw TYPECHECK_ERROR;
1773  }
1774  }
1775  }
1776  error() << "No assignment found for function return value" << eom;
1777  throw TYPECHECK_ERROR;
1778 }
1779 
1781 {
1782  or_exprt or_wrapper{to_or_expr(rlo_bit)};
1783 
1784  if(can_cast_expr<constant_exprt>(or_wrapper.op1()))
1785  or_wrapper.op1();
1786  else if(can_cast_expr<and_exprt>(or_wrapper.op1()))
1787  {
1788  and_exprt &and_op{to_and_expr(or_wrapper.op1())};
1789  and_op.add_to_operands(op);
1790  or_wrapper.op1() = and_op;
1791  }
1792  else
1793  {
1794  and_exprt and_op{or_wrapper.op1(), op};
1795  or_wrapper.op1() = and_op;
1796  }
1797  rlo_bit = or_wrapper;
1798 }
1799 
1801 {
1802  fc_bit = true;
1803  or_bit = false;
1804  rlo_bit = op;
1805 }
1806 
1808 {
1809  rlo_bit = true_exprt{};
1810  fc_bit = false;
1811  or_bit = false;
1812  nesting_stack.clear();
1813 }
1814 
1816 {
1818  label_references.clear();
1819  stl_labels.clear();
1820 }
1821 
1823 {
1824  symbol_exprt temp_rlo{
1826  const code_assignt rlo_assignment{temp_rlo, rlo_bit};
1827  tia_element.value.add_to_operands(rlo_assignment);
1828  rlo_bit = std::move(temp_rlo);
1829 }
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
Boolean AND.
Definition: std_expr.h:1920
exprt & rhs()
Definition: std_expr.h:590
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
std::size_t get_width() const
Definition: std_types.h:843
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
A codet representing an assignment in the program.
Definition: std_code.h:293
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
A codet representing sequential composition of program statements.
Definition: std_code.h:168
A codet representing the declaration of a local variable.
Definition: std_code.h:400
codet representation of a function call statement.
Definition: std_code.h:1213
exprt::operandst argumentst
Definition: std_code.h:1222
codet representation of a goto statement.
Definition: std_code.h:1157
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a label for branch targets.
Definition: std_code.h:1405
const irep_idt & get_label() const
Definition: std_code.h:1413
codet & code()
Definition: std_code.h:1423
A codet representing a skip statement.
Definition: std_code.h:268
const irep_idt & get_base_name() const
Definition: std_types.h:595
const irep_idt & get_identifier() const
Definition: std_types.h:590
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:580
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
Operator to dereference a pointer.
Definition: pointer_expr.h:628
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
exprt & op1()
Definition: expr.h:102
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2811
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2613
mstreamt & error() const
Definition: message.h:399
message_handlert * message_handler
Definition: message.h:439
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:973
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
exprt & op1()
Definition: std_expr.h:850
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean negation.
Definition: std_expr.h:2127
Boolean OR.
Definition: std_expr.h:2028
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
Fixed-width bit-vector with two's complement interpretation.
Intermediate representation of a parsed Statement List file before converting it into a goto program.
std::list< var_declarationt > var_declarationst
functionst functions
List of functions this parse tree includes.
function_blockst function_blocks
List of function blocks this parse tree includes.
std::vector< symbol_exprt > tags
List of tags that were included in the source.
Class for encapsulating the current state of the type check.
void typecheck_accumulator_compare_instruction(const irep_idt &comparison)
Performs a typecheck on an STL comparison instruction.
void typecheck_statement_list_accu_real_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for reals.
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.
symbol_tablet & symbol_table
Reference to the symbol table that should be filled during the typecheck.
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...
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.
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.
const statement_list_parse_treet & parse_tree
Parse tree which is used to fill the symbol table.
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.
void typecheck_statement_list_nesting_closed(const codet &op_code)
Performs a typecheck on a Nesting Closed instruction.
void typecheck_statement_list_accu_real_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for reals.
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.
void clear_module_state()
Modifies the state of the typecheck to resemble the beginning of a new module.
void typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
void typecheck_jump_locations(const code_labelt &label, const stl_label_locationt &location)
Performs a typecheck on all references for the given label.
void typecheck_label_reference(const irep_idt &label, bool sets_fc_false)
Checks if the given label is already present and compares the current state with it.
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.
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.
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...
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...
void typecheck_statement_list_and_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And Not instruction.
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.
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...
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...
void typecheck() override
Performs the actual typecheck by using the parse tree with which the object was initialized and modif...
void typecheck_statement_list_accu_dint_mul(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
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.
void typecheck_statement_list_nested_xor(const codet &op_code)
Performs a typecheck on a nested XOR instruction.
void typecheck_statement_list_accu_int_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for integers.
const irep_idt module
Name of the module this typecheck belongs to.
void typecheck_statement_list_accu_int_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for integers.
void typecheck_statement_list_nested_or_not(const codet &op_code)
Performs a typecheck on a nested Or Not instruction.
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.
void typecheck_statement_list_accu_dint_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for double integers.
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.
std::vector< exprt > accumulator
Representation of the accumulator of a TIA element.
void typecheck_statement_list_nested_xor_not(const codet &op_code)
Performs a typecheck on a nested XOR Not instruction.
void clear_network_state()
Modifies the state of the typecheck to resemble the beginning of a new network.
void typecheck_statement_list_accu_real_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
void typecheck_statement_list_xor(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR instruction.
exprt typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier)
Performs a typecheck on the given identifier and returns its symbol.
void typecheck_tag_list()
Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents t...
void typecheck_statement_list_xor_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR Not instruction.
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.
void typecheck_statement_list_jump_unconditional(const codet &op_code, symbolt &tia_element)
Performs a typecheck on an unconditional jump instruction (JU) and adds the jump to the given symbol.
void typecheck_code(const codet &instruction, symbolt &tia_element)
Performs a typecheck for the specified instruction in code form.
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.
void typecheck_statement_list_accu_real_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for reals.
label_referencest label_references
Holds associations between labels and jumps that are referencing it.
exprt rlo_bit
Result of Logic Operation (Part of the TIA status word).
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.
bool or_bit
Or (Part of the TIA status word).
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.
stl_labelst stl_labels
Data structure that contains data about the labels of the current module.
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...
void typecheck_statement_list_load(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL load instruction.
void typecheck_statement_list_accu_int_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for integers.
stl_label_locationt typecheck_label_location(const code_labelt &label)
Converts the properties of the current typecheck state to a label location.
void typecheck_statement_list_accu_int_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for integers.
void typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or instruction.
void typecheck_statement_list_accu_int_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for integers.
void typecheck_statement_list_and(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And instruction.
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.
void typecheck_instruction_without_operand(const codet &op_code)
Performs a typecheck on an operand-less STL instruction.
void typecheck_label(const codet &instruction, symbolt &tia_element)
Performs a typecheck for the given label in code form.
bool fc_bit
First Check (Part of the TIA status word).
void typecheck_statement_list_jump_conditional(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a conditional jump instruction (JC) and adds it to the given symbol.
void typecheck_statement_list_jump_conditional_not(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a inverted conditional jump instruction (JCN) and adds it to the given symbol...
void typecheck_statement_list_or_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or Not instruction.
void typecheck_label_references()
Checks if all jumps reference labels that exist.
void typecheck_binary_accumulator_instruction(const codet &op_code)
Performs a typecheck on a STL instruction that uses two accumulator entries.
void initialize_bit_expression(const exprt &op)
Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.
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.
void typecheck_statement_list_nested_or(const codet &op_code)
Performs a typecheck on a nested Or instruction.
void typecheck_statement_list_accu_dint_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
void typecheck_statement_list_accu_real_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for reals.
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...
void typecheck_statement_list_accu_dint_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for double integers.
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.
void typecheck_statement_list_nested_and_not(const codet &op_code)
Performs a typecheck on a nested And Not instruction.
void typecheck_statement_list_accu_int_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for integers.
void typecheck_statement_list_accu_int_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for integers.
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...
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...
void typecheck_statement_list_accu_dint_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
void typecheck_statement_list_accu_real_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for reals.
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...
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.
void typecheck_statement_list_accu_real_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
nesting_stackt nesting_stack
Representation of the nesting stack.
void typecheck_statement_list_not(const codet &op_code)
Performs a typecheck on a STL boolean NOT instruction.
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...
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.
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.
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.
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.
void typecheck_statement_list_accu_int_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for integers.
void typecheck_statement_list_accu_dint_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for double integers.
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.
void typecheck_statement_list_accu_dint_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
void add_temp_rlo()
Adds a symbol for the RLO to the symbol table.
void typecheck_statement_list_nested_and(const codet &op_code)
Performs a typecheck on a nested And instruction.
void save_rlo_state(symbolt &tia_element)
Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean v...
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.
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.
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...
void typecheck_statement_list_and_before_or()
Performs a typecheck on a STL operand-less Or instruction.
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2802
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:133
virtual bool typecheck_main()
Definition: typecheck.cpp:13
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Boolean XOR.
Definition: std_expr.h:2091
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
exprt simplify_expr(exprt src, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define CPROVER_ASSERT
Name of the CBMC assert function.
#define CPROVER_TEMP_RLO
Name of the RLO symbol used in some operations.
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.
#define DATA_BLOCK_PARAMETER_NAME
Artificial name for the data block interface of a function block.
#define DATA_BLOCK_TYPE_POSTFIX
Postfix for the type of a data block.
#define STATEMENT_LIST_PTR_WIDTH
Size of pointers in Siemens TIA.
static const std::vector< irep_idt > logic_sequence_terminators
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.
#define TYPECHECK_ERROR
#define CPROVER_ASSUME
Name of the CBMC assume function.
static const std::vector< irep_idt > logic_sequence_initializers
Statement List Language Type Checking.
bool_typet get_bool_type()
Creates a new type that resembles the 'Bool' type of the Siemens PLC languages.
Statement List Type Helper.
#define STL_INT_WIDTH
#define STL_DINT_WIDTH
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1249
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2075
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:1967
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2775
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:1956
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Structure for a simple function block in Statement List.
var_declarationst var_static
FB-exclusive static variable declarations.
Structure for a simple function in Statement List.
Represents a regular Statement List instruction which consists out of one or more codet tokens.
std::vector< codet > tokens
Data structure for all tokens of the instruction.
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
var_declarationst var_input
Input variable declarations.
const irep_idt name
Name of the module.
var_declarationst var_inout
Inout variable declarations.
networkst networks
List of all networks of this module.
var_declarationst var_temp
Temp variable declarations.
var_declarationst var_output
Output variable declarations.
Struct for a single variable declaration in Statement List.
symbol_exprt variable
Representation of the variable, including identifier and type.
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
Holds information about the properties of a jump instruction.
stl_jump_locationt(size_t nesting_depth, bool sets_fc_false)
Constructs a new location with the specified properties.
Holds information about the instruction and the nesting depth to which a label points.
const bool jumps_permitted
States if jumps to this location are permitted or if the location is invalid.
stl_label_locationt(size_t nesting_depth, bool jumps_permitted, bool fc_false_required)
Constructs a new location with the specified properties.
const bool fc_false_required
States if jump instructions to this location need to set the /FC bit to false.
Author: Diffblue Ltd.