cprover
Loading...
Searching...
No Matches
statement_list_typecheck.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Statement List Language Type Checking
4
5Author: Matthias Weiss, matthias.weiss@diffblue.com
6
7\*******************************************************************/
8
11
14
16
17#include <util/cprover_prefix.h>
18#include <util/message.h>
19#include <util/namespace.h>
20#include <util/pointer_expr.h>
21#include <util/simplify_expr.h>
22#include <util/std_code.h>
23#include <util/symbol_table.h>
24
26#define STATEMENT_LIST_PTR_WIDTH 64
27// TODO: Replace with more specific exception throws.
28#define TYPECHECK_ERROR 0
30#define DATA_BLOCK_PARAMETER_NAME "data_block"
32#define DATA_BLOCK_TYPE_POSTFIX "_db"
34#define CPROVER_ASSERT CPROVER_PREFIX "assert"
36#define CPROVER_ASSUME CPROVER_PREFIX "assume"
38#define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
39
54
62
80
82 const statement_list_parse_treet &parse_tree,
83 symbol_tablet &symbol_table,
84 const std::string &module,
85 message_handlert &message_handler)
86{
88 parse_tree, symbol_table, module, message_handler);
89
90 return stl_typecheck.typecheck_main();
91}
92
94 exprt rlo_bit,
95 bool or_bit,
96 codet function_code)
97 : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
98{
99}
100
102 size_t nesting_depth,
103 bool jumps_permitted,
104 bool fc_false_required)
105 : nesting_depth(nesting_depth),
106 jumps_permitted(jumps_permitted),
107 fc_false_required(fc_false_required)
108{
109}
111 size_t nesting_depth,
112 bool sets_fc_false)
113 : nesting_depth(nesting_depth), sets_fc_false(sets_fc_false)
114{
115}
116
128
130{
131 // First fill the symbol table with function, tag and parameter declarations
132 // to be able to properly resolve block calls later.
139 // Temporary RLO symbol for certain operations.
140 add_temp_rlo();
141
142 // Iterate through all networks to generate the function bodies.
145 {
148 }
150 {
153 }
154}
155
158{
159 // Create FB symbol.
161 function_block_sym.module = module;
163 function_block_sym.base_name = function_block_sym.name;
164 function_block_sym.pretty_name = function_block_sym.name;
166
167 // When calling function blocks, the passed parameters are value-copied to a
168 // corresponding instance data block. This block contains all input, inout,
169 // output and static variables. The function block reads and writes only
170 // those fields and does not modify the actual parameters. To simulate this
171 // behaviour, all function blocks are modeled as functions with a single
172 // parameter: An instance of their data block, whose members they modify.
173
174 // Create and add DB type symbol.
178 data_block.name =
180 data_block.base_name = data_block.name;
183
184 // Create and add parameter symbol.
188 param_sym.module = module;
189 param_sym.type = param.type();
190 param_sym.name = param.get_identifier();
192 param_sym.pretty_name = param_sym.base_name;
195
196 // Setup FB symbol type and value.
198 params.push_back(param);
199 code_typet fb_type{params, empty_typet()};
203}
204
227
229{
230 for(const symbol_exprt &tag : parse_tree.tags)
231 {
233 tag_sym.is_static_lifetime = true;
234 tag_sym.module = module;
235 tag_sym.name = tag.get_identifier();
236 tag_sym.base_name = tag_sym.name;
237 tag_sym.pretty_name = tag_sym.name;
238 tag_sym.type = tag.type();
241 }
242}
243
245{
247 temp_rlo.is_static_lifetime = true;
248 temp_rlo.module = module;
250 temp_rlo.base_name = temp_rlo.name;
251 temp_rlo.pretty_name = temp_rlo.name;
252 temp_rlo.type = get_bool_type();
255}
256
272
288
292 const irep_idt &function_name,
293 const irep_idt &var_property)
294{
296 var_decls)
297 {
299 param_sym.module = module;
300 param_sym.type = declaration.variable.type();
301 param_sym.name = id2string(function_name) +
302 "::" + id2string(declaration.variable.get_identifier());
303 param_sym.base_name = declaration.variable.get_identifier();
304 param_sym.pretty_name = param_sym.base_name;
307
309 param.set_identifier(param_sym.name);
310 param.set_base_name(declaration.variable.get_identifier());
312 params.push_back(param);
313 }
314}
315
319{
321 tia_module.var_temp)
322 {
324 temp_sym.name = id2string(tia_symbol.name) +
325 "::" + id2string(declaration.variable.get_identifier());
326 temp_sym.base_name = declaration.variable.get_identifier();
327 temp_sym.pretty_name = temp_sym.base_name;
328 temp_sym.type = declaration.variable.type();
330 temp_sym.module = module;
332
333 const code_declt code_decl{temp_sym.symbol_expr()};
334 tia_symbol.value.add_to_operands(code_decl);
335 }
336}
337
341{
342 // Leave value empty if there are no networks to iterate through.
343 if(tia_module.networks.empty())
344 return;
345 if(tia_symbol.value.is_nil())
346 tia_symbol.value = code_blockt{};
347
350
351 for(const auto &network : tia_module.networks)
352 {
354 for(const auto &instruction : network.instructions)
356 }
358}
359
361{
362 if(!label_references.empty())
363 {
364 error() << "Unable to find the labels:";
365 for(auto pair : label_references)
366 {
367 error() << "\n";
368 error() << id2string(pair.first);
369 }
370 error() << eom;
371 throw TYPECHECK_ERROR;
372 }
373}
374
382
384 const codet &instruction,
386{
387 const irep_idt statement{instruction.get_statement()};
388
389 if(ID_label == statement)
390 typecheck_label(instruction, tia_element);
391 else if(ID_statement_list_load == statement)
393 else if(ID_statement_list_transfer == statement)
395 else if(ID_statement_list_accu_int_add == statement)
397 else if(ID_statement_list_accu_int_sub == statement)
399 else if(ID_statement_list_accu_int_mul == statement)
401 else if(ID_statement_list_accu_int_div == statement)
403 else if(ID_statement_list_accu_int_eq == statement)
405 else if(ID_statement_list_accu_int_neq == statement)
407 else if(ID_statement_list_accu_int_lt == statement)
409 else if(ID_statement_list_accu_int_gt == statement)
411 else if(ID_statement_list_accu_int_lte == statement)
413 else if(ID_statement_list_accu_int_gte == statement)
415 else if(ID_statement_list_accu_dint_add == statement)
417 else if(ID_statement_list_accu_dint_sub == statement)
419 else if(ID_statement_list_accu_dint_mul == statement)
421 else if(ID_statement_list_accu_dint_div == statement)
423 else if(ID_statement_list_accu_dint_eq == statement)
425 else if(ID_statement_list_accu_dint_neq == statement)
427 else if(ID_statement_list_accu_dint_lt == statement)
429 else if(ID_statement_list_accu_dint_gt == statement)
431 else if(ID_statement_list_accu_dint_lte == statement)
433 else if(ID_statement_list_accu_dint_gte == statement)
435 else if(ID_statement_list_accu_real_add == statement)
437 else if(ID_statement_list_accu_real_sub == statement)
439 else if(ID_statement_list_accu_real_mul == statement)
441 else if(ID_statement_list_accu_real_div == statement)
443 else if(ID_statement_list_accu_real_eq == statement)
445 else if(ID_statement_list_accu_real_neq == statement)
447 else if(ID_statement_list_accu_real_lt == statement)
449 else if(ID_statement_list_accu_real_gt == statement)
451 else if(ID_statement_list_accu_real_lte == statement)
453 else if(ID_statement_list_accu_real_gte == statement)
455 else if(ID_statement_list_not == statement)
456 typecheck_statement_list_not(instruction);
457 else if(ID_statement_list_and == statement)
459 else if(ID_statement_list_and_not == statement)
461 else if(ID_statement_list_or == statement)
463 else if(ID_statement_list_or_not == statement)
465 else if(ID_statement_list_xor == statement)
467 else if(ID_statement_list_xor_not == statement)
469 else if(ID_statement_list_and_nested == statement)
471 else if(ID_statement_list_and_not_nested == statement)
473 else if(ID_statement_list_or_nested == statement)
475 else if(ID_statement_list_or_not_nested == statement)
477 else if(ID_statement_list_xor_nested == statement)
479 else if(ID_statement_list_xor_not_nested == statement)
481 else if(ID_statement_list_nesting_closed == statement)
483 else if(ID_statement_list_assign == statement)
485 else if(ID_statement_list_set_rlo == statement)
487 else if(ID_statement_list_clr_rlo == statement)
489 else if(ID_statement_list_set == statement)
491 else if(ID_statement_list_reset == statement)
493 else if(ID_statement_list_jump_unconditional == statement)
495 else if(ID_statement_list_jump_conditional == statement)
497 else if(ID_statement_list_jump_conditional_not == statement)
499 else if(ID_statement_list_nop == statement)
500 return;
501 else if(ID_statement_list_call == statement)
503 else
504 {
505 error() << "OP code of instruction not found: "
506 << instruction.get_statement() << eom;
507 throw TYPECHECK_ERROR;
508 }
509}
510
512 const codet &instruction,
514{
515 const code_labelt &label = to_code_label(instruction);
516
517 // Check if label is duplicate (not allowed in STL).
518 if(stl_labels.find(label.get_label()) != end(stl_labels))
519 {
520 error() << "Multiple definitions of label " << id2string(label.get_label())
521 << eom;
522 throw TYPECHECK_ERROR;
523 }
524
525 // Determine the properties of this location in the code.
527
528 // Store the implicit RLO in order to correctly separate the different
529 // blocks of logic.
530 if(location.jumps_permitted)
532
533 // Now check if there are any jumps that referenced that label before and
534 // validate these.
535 typecheck_jump_locations(label, location);
536
537 // Only add the label to the code if jumps are permitted. Proceed as normal
538 // if they are not. An added label will always point at an empty code
539 // location due to the way how the typecheck works.
540 if(location.jumps_permitted)
541 tia_element.value.add_to_operands(
542 code_labelt{label.get_label(), code_skipt{}});
543
544 // Recursive call to check the label target.
546}
547
550{
551 // Jumps to a label are only allowed if one of the following conditions
552 // applies:
553 //
554 // a) The /FC bit is false when encountering the instruction (pointing at the
555 // beginning of a logic sequence or no sequence at all).
556 // b) The /FC bit is set to false after processing the instruction (pointing
557 // at the termination of a logic sequence). This excludes nesting-open
558 // operations since although they terminate the current sequence, it will
559 // be resumed later.
560 //
561 // Labels at locations where this does not hold true compile, but actual
562 // jumps to them do not.
563 //
564 // Additionally, jumps to instructions that mark the beginning of a logic
565 // sequence are only allowed if the jump instruction itself sets the /FC bit
566 // to false.
567
568 bool jumps_permitted = false;
569 bool fc_false_required = false;
570 if(!fc_bit)
571 {
572 jumps_permitted = true;
573 // Check if label points to new logic sequence.
575 if(op_code == label.code().get_statement())
576 {
577 fc_false_required = true;
578 break;
579 }
580 }
581 else // Check if the label's instruction terminates the logic sequence.
582 {
584 if(op_code == label.code().get_statement())
585 {
586 jumps_permitted = true;
587 break;
588 }
589 }
590
591 // Add the label to map.
592 stl_label_locationt location{
593 nesting_stack.size(), jumps_permitted, fc_false_required};
594 stl_labels.emplace(label.get_label(), location);
595 return location;
596}
597
599 const code_labelt &label,
601{
602 // Now check if there are any jumps that referenced that label before and
603 // validate these.
604 auto reference_it = label_references.find(label.get_label());
606 {
607 if(!location.jumps_permitted)
608 {
609 error() << "Not allowed to jump to label " << id2string(label.get_label())
610 << eom;
611 throw TYPECHECK_ERROR;
612 }
613 for(auto jump_location_it = begin(reference_it->second);
614 jump_location_it != end(reference_it->second);
616 {
617 if(location.fc_false_required && !jump_location_it->sets_fc_false)
618 {
619 error() << "Jump to label " << id2string(label.get_label())
620 << " can not be unconditional" << eom;
621 throw TYPECHECK_ERROR;
622 }
623 if(nesting_stack.size() != jump_location_it->nesting_depth)
624 {
625 error() << "Jump to label " << id2string(label.get_label())
626 << " violates brace scope" << eom;
627 throw TYPECHECK_ERROR;
628 }
629 }
630 // Remove entry after validation.
631 label_references.erase(label.get_label());
632 }
633}
634
636 const codet &op_code,
637 const symbolt &tia_element)
638{
639 const symbol_exprt *const symbol =
641 if(symbol)
642 {
643 const irep_idt &identifier{symbol->get_identifier()};
644 const exprt val{typecheck_identifier(tia_element, identifier)};
645 accumulator.push_back(val);
646 }
648 accumulator.push_back(op_code.op0());
649 else
650 {
651 error() << "Instruction is not followed by symbol or constant" << eom;
652 throw TYPECHECK_ERROR;
653 }
654}
655
657 const codet &op_code,
659{
661 const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
662 if(lhs.type() != accumulator.back().type())
663 {
664 error() << "Types of transfer assignment do not match" << eom;
665 throw TYPECHECK_ERROR;
666 }
667 const code_assignt assignment{lhs, accumulator.back()};
668 tia_element.value.add_to_operands(assignment);
669}
670
672 const codet &op_code)
673{
675
676 // Pop first operand, peek second.
677 const exprt accu1{accumulator.back()};
678 accumulator.pop_back();
679 const exprt &accu2{accumulator.back()};
680 const plus_exprt operation{accu2, accu1};
681 accumulator.push_back(operation);
682}
683
685 const codet &op_code)
686{
688
689 // Pop first operand, peek second.
690 const exprt accu1{accumulator.back()};
691 accumulator.pop_back();
692 const exprt &accu2{accumulator.back()};
693 const minus_exprt operation{accu2, accu1};
694 accumulator.push_back(operation);
695}
696
698 const codet &op_code)
699{
701
702 // Pop first operand, peek second.
703 const exprt accu1{accumulator.back()};
704 accumulator.pop_back();
705 const exprt &accu2{accumulator.back()};
706 const mult_exprt operation{accu2, accu1};
707 accumulator.push_back(operation);
708}
709
711 const codet &op_code)
712{
714
715 // Pop first operand, peek second.
716 const exprt accu1{accumulator.back()};
717 accumulator.pop_back();
718 const exprt &accu2{accumulator.back()};
719 const div_exprt operation{accu2, accu1};
720 accumulator.push_back(operation);
721}
722
729
736
743
750
757
764
766 const codet &op_code)
767{
769
770 // Pop first operand, peek second.
771 const exprt accu1{accumulator.back()};
772 accumulator.pop_back();
773 const exprt &accu2{accumulator.back()};
774 const plus_exprt operation{accu2, accu1};
775 accumulator.push_back(operation);
776}
777
779 const codet &op_code)
780{
782
783 // Pop first operand, peek second.
784 const exprt accu1{accumulator.back()};
785 accumulator.pop_back();
786 const exprt &accu2{accumulator.back()};
787 const minus_exprt operation{accu2, accu1};
788 accumulator.push_back(operation);
789}
790
792 const codet &op_code)
793{
795
796 // Pop first operand, peek second.
797 const exprt accu1{accumulator.back()};
798 accumulator.pop_back();
799 const exprt &accu2{accumulator.back()};
800 const mult_exprt operation{accu2, accu1};
801 accumulator.push_back(operation);
802}
803
805 const codet &op_code)
806{
808
809 // Pop first operand, peek second.
810 const exprt accu1{accumulator.back()};
811 accumulator.pop_back();
812 const exprt &accu2{accumulator.back()};
813 const div_exprt operation{accu2, accu1};
814 accumulator.push_back(operation);
815}
816
823
830
837
844
851
858
860 const codet &op_code)
861{
863
864 // Pop first operand, peek second.
865 const exprt accu1{accumulator.back()};
866 accumulator.pop_back();
867 const exprt &accu2{accumulator.back()};
868 const plus_exprt operation{accu2, accu1};
869 accumulator.push_back(operation);
870}
871
873 const codet &op_code)
874{
876
877 // Pop first operand, peek second.
878 const exprt accu1{accumulator.back()};
879 accumulator.pop_back();
880 const exprt &accu2{accumulator.back()};
881 const minus_exprt operation{accu2, accu1};
882 accumulator.push_back(operation);
883}
884
886 const codet &op_code)
887{
889
890 // Pop first operand, peek second.
891 const exprt accu1{accumulator.back()};
892 accumulator.pop_back();
893 const exprt &accu2{accumulator.back()};
894 const mult_exprt operation{accu2, accu1};
895 accumulator.push_back(operation);
896}
897
899 const codet &op_code)
900{
902
903 // Pop first operand, peek second.
904 const exprt accu1{accumulator.back()};
905 accumulator.pop_back();
906 const exprt &accu2{accumulator.back()};
907 const div_exprt operation{accu2, accu1};
908 accumulator.push_back(operation);
909}
910
917
924
931
938
945
952
960
962 const codet &op_code,
963 const symbolt &tia_element)
964{
965 exprt op{
967
968 // If inside of a bit string and if the OR bit is not set, create an 'and'
969 // expression with the operand and the current contents of the rlo bit. If
970 // the OR bit is set then this instruction is part of an 'and-before-or'
971 // block and needs to be added to the rlo in a special way.
972 if(fc_bit && or_bit)
974 else if(fc_bit)
975 {
976 const and_exprt unsimplified{rlo_bit, op};
978 }
979 else
981}
982
984 const codet &op_code,
985 const symbolt &tia_element)
986{
987 exprt op{
989
990 // If inside of a bit string and if the OR bit is not set, create an 'and'
991 // expression with the operand and the current contents of the rlo bit. If
992 // the OR bit is set then this instruction is part of an 'and-before-or'
993 // block and needs to be added to the rlo in a special way.
994 if(or_bit && fc_bit)
996 else if(fc_bit)
997 {
998 const and_exprt unsimplified{rlo_bit, op};
1000 }
1001 else
1003}
1004
1006 const codet &op_code,
1007 const symbolt &tia_element)
1008{
1009 if(op_code.operands().empty())
1010 {
1012 return;
1013 }
1014 const symbol_exprt &sym{
1016 const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1017
1018 // If inside of a bit string, create an 'or' expression with the operand and
1019 // the current contents of the rlo bit.
1020 if(fc_bit)
1021 {
1022 const or_exprt unsimplified{rlo_bit, op};
1024 or_bit = false;
1025 }
1026 else
1028}
1029
1031 const codet &op_code,
1032 const symbolt &tia_element)
1033{
1034 const symbol_exprt &sym{
1036 const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1037 const not_exprt not_op{op};
1038
1039 // If inside of a bit string, create an 'or' expression with the operand and
1040 // the current contents of the rlo bit.
1041 if(fc_bit)
1042 {
1045 or_bit = false;
1046 }
1047 else
1049}
1050
1052 const codet &op_code,
1053 const symbolt &tia_element)
1054{
1055 const symbol_exprt &sym{
1057 const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1058
1059 // If inside of a bit string, create an 'xor' expression with the operand and
1060 // the current contents of the rlo bit.
1061 if(fc_bit)
1062 {
1063 const xor_exprt unsimplified{rlo_bit, op};
1065 or_bit = false;
1066 }
1067 else
1069}
1070
1072 const codet &op_code,
1073 const symbolt &tia_element)
1074{
1075 const symbol_exprt &sym{
1077 const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1078 const not_exprt not_op{op};
1079
1080 // If inside of a bit string, create an 'xor not' expression with the
1081 // operand and the current contents of the rlo bit.
1082 if(fc_bit)
1083 {
1086 or_bit = false;
1087 }
1088 else
1090}
1091
1093{
1094 if(fc_bit)
1095 {
1097 or_bit = true;
1098 }
1099 else
1100 return; // Instruction has no semantic influence.
1101}
1102
1104 const codet &op_code)
1105{
1106 // Set the rlo to true implicitly so that the value of the AND instruction
1107 // is being loaded in case of a new bit string.
1109}
1110
1112 const codet &op_code)
1113{
1114 // Set the rlo to true implicitly so that the value of the AND instruction
1115 // is being loaded in case of a new bit string.
1117}
1118
1120 const codet &op_code)
1121{
1122 // Set the rlo to false implicitly so that the value of the OR instruction
1123 // is being loaded in case of a new bit string.
1125}
1126
1128 const codet &op_code)
1129{
1130 // Set the rlo to false implicitly so that the value of the OR instruction
1131 // is being loaded in case of a new bit string.
1133}
1134
1136 const codet &op_code)
1137{
1138 // Set the rlo to false implicitly so that the value of the XOR instruction
1139 // is being loaded in case of a new bit string.
1141}
1142
1144 const codet &op_code)
1145{
1146 // Set the rlo to false implicitly so that the value of the XOR instruction
1147 // is being loaded in case of a new bit string.
1149}
1150
1152 const codet &op_code)
1153{
1155 if(nesting_stack.empty())
1156 {
1157 error() << "Wrong order of brackets (Right parenthesis is not preceded by "
1158 "nesting)"
1159 << eom;
1160 throw TYPECHECK_ERROR;
1161 }
1162 or_bit = nesting_stack.back().or_bit;
1163 fc_bit = true;
1164 const irep_idt &statement{nesting_stack.back().function_code.get_statement()};
1165 if(ID_statement_list_and_nested == statement)
1166 {
1167 if(or_bit)
1168 {
1169 const exprt op{rlo_bit};
1170 rlo_bit = nesting_stack.back().rlo_bit;
1172 }
1173 else
1174 rlo_bit = and_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1175 }
1176 else if(ID_statement_list_and_not_nested == statement)
1177 {
1178 if(or_bit)
1179 {
1180 const not_exprt op{rlo_bit};
1181 rlo_bit = nesting_stack.back().rlo_bit;
1183 }
1184 else
1185 rlo_bit = and_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1186 }
1187 else if(ID_statement_list_or_nested == statement)
1188 {
1189 or_bit = false;
1190 rlo_bit = or_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1191 }
1192 else if(ID_statement_list_or_not_nested == statement)
1193 {
1194 or_bit = false;
1195 rlo_bit = or_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1196 }
1197 else if(ID_statement_list_xor_nested == statement)
1198 {
1199 or_bit = false;
1200 rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, rlo_bit};
1201 }
1202 else if(ID_statement_list_xor_not_nested == statement)
1203 {
1204 or_bit = false;
1205 rlo_bit = xor_exprt{nesting_stack.back().rlo_bit, not_exprt{rlo_bit}};
1206 }
1207 nesting_stack.pop_back();
1208}
1209
1211 const codet &op_code,
1213{
1215 const exprt lhs{typecheck_identifier(tia_element, op.get_identifier())};
1216
1217 if(lhs.type() != rlo_bit.type())
1218 {
1219 error() << "Types of assign do not match" << eom;
1220 throw TYPECHECK_ERROR;
1221 }
1222 const code_assignt assignment{lhs, rlo_bit};
1223 tia_element.value.add_to_operands(assignment);
1224 fc_bit = false;
1225 or_bit = false;
1226 // Set RLO to assigned operand in order to prevent false results if a symbol
1227 // that's implicitly part of the RLO was changed by the assignment.
1228 rlo_bit = lhs;
1229}
1230
1239
1248
1250 const codet &op_code,
1252{
1254 const irep_idt &identifier{op.get_identifier()};
1255
1257
1258 const exprt lhs{typecheck_identifier(tia_element, identifier)};
1259 const code_assignt assignment{lhs, true_exprt()};
1260 const code_ifthenelset ifthen{rlo_bit, assignment};
1261 tia_element.value.add_to_operands(ifthen);
1262 fc_bit = false;
1263 or_bit = false;
1264}
1265
1267 const codet &op_code,
1269{
1271 const irep_idt &identifier{op.get_identifier()};
1272
1274
1275 const exprt lhs{typecheck_identifier(tia_element, identifier)};
1276 const code_assignt assignment{lhs, false_exprt()};
1277 const code_ifthenelset ifthen{rlo_bit, assignment};
1278 tia_element.value.add_to_operands(ifthen);
1279 fc_bit = false;
1280 or_bit = false;
1281}
1282
1284 const codet &op_code,
1286{
1288 const irep_idt &identifier{op.get_identifier()};
1289 if(symbol_table.has_symbol(identifier))
1291 else if(identifier == CPROVER_ASSUME)
1293 else if(identifier == CPROVER_ASSERT)
1295 else
1296 {
1297 error() << "Called function could not be found" << eom;
1298 throw TYPECHECK_ERROR;
1299 }
1300 fc_bit = false;
1301 or_bit = false;
1302}
1303
1305 const codet &op_code,
1307{
1308 const symbol_exprt &label{
1310 typecheck_label_reference(label.get_identifier(), false);
1311
1313 code_gotot unconditional{label.get_identifier()};
1314 tia_element.value.add_to_operands(unconditional);
1315}
1316
1318 const codet &op_code,
1320{
1321 const symbol_exprt &label{
1323 typecheck_label_reference(label.get_identifier(), true);
1324
1326 code_gotot jump{label.get_identifier()};
1328 tia_element.value.add_to_operands(conditional);
1329
1330 fc_bit = false;
1331 or_bit = false;
1332 rlo_bit = true_exprt{};
1333}
1334
1336 const codet &op_code,
1338{
1339 const symbol_exprt &label{
1341 typecheck_label_reference(label.get_identifier(), true);
1342
1344 code_gotot jump{label.get_identifier()};
1346 tia_element.value.add_to_operands(not_conditional);
1347
1348 fc_bit = false;
1349 or_bit = false;
1350 rlo_bit = true_exprt{};
1351}
1352
1354 const codet &op_code)
1355{
1357 const exprt &accu1{accumulator.back()};
1358 const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1359
1360 // Are both operands integers?
1361 const signedbv_typet *const accu_type1 =
1363 const signedbv_typet *const accu_type2 =
1365 if(
1366 !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_INT_WIDTH ||
1367 accu_type2->get_width() != STL_INT_WIDTH)
1368 {
1369 error() << "Operands of integer addition are no integers" << eom;
1370 throw TYPECHECK_ERROR;
1371 }
1372}
1373
1375 const codet &op_code)
1376{
1378 const exprt &accu1{accumulator.back()};
1379 const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1380
1381 // Are both operands double integers?
1382 const signedbv_typet *const accu_type1 =
1384 const signedbv_typet *const accu_type2 =
1386 if(
1387 !accu_type1 || !accu_type2 || accu_type1->get_width() != STL_DINT_WIDTH ||
1388 accu_type2->get_width() != STL_DINT_WIDTH)
1389 {
1390 error() << "Operands of double integer addition are no double integers"
1391 << eom;
1392 throw TYPECHECK_ERROR;
1393 }
1394}
1395
1397 const codet &op_code)
1398{
1400 const exprt &accu1{accumulator.back()};
1401 const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1402
1403 // Are both operands real types?
1404 if(!(can_cast_type<floatbv_typet>(accu1.type()) &&
1406 {
1407 error() << "Operands of Real addition do not have the type Real" << eom;
1408 throw TYPECHECK_ERROR;
1409 }
1410}
1411
1413 const irep_idt &comparison)
1414{
1415 const exprt &accu1{accumulator.back()};
1416 const exprt &accu2{accumulator.at(accumulator.size() - 2)};
1417 // STL behaviour: ACCU2 is lhs, ACCU1 is rhs.
1418 const binary_relation_exprt operation{accu2, comparison, accu1};
1419 rlo_bit = operation;
1420}
1421
1423 const irep_idt &label,
1424 bool sets_fc_false)
1425{
1426 // If the label is already present in the list, check if it matches the
1427 // criteria.
1428 auto label_it = stl_labels.find(label);
1429 if(label_it != end(stl_labels))
1430 {
1431 if(!label_it->second.jumps_permitted)
1432 {
1433 error() << "Not allowed to jump to label " << id2string(label_it->first)
1434 << eom;
1435 throw TYPECHECK_ERROR;
1436 }
1437
1438 if(label_it->second.fc_false_required && !sets_fc_false)
1439 {
1440 error() << "Jump to label " << id2string(label_it->first)
1441 << " can not be unconditional" << eom;
1442 throw TYPECHECK_ERROR;
1443 }
1444
1445 if(label_it->second.nesting_depth != nesting_stack.size())
1446 {
1447 error() << "Jump to label " << id2string(label_it->first)
1448 << " violates brace scope" << eom;
1449 throw TYPECHECK_ERROR;
1450 }
1451 }
1452 else // If it was not encountered yet, create a new reference entry.
1453 {
1454 stl_jump_locationt location{nesting_stack.size(), sets_fc_false};
1455 auto reference_it = label_references.find(label);
1456 if(reference_it == end(label_references))
1457 {
1458 std::vector<stl_jump_locationt> locations;
1459 locations.push_back(location);
1460 label_references.emplace(label, locations);
1461 }
1462 else
1463 reference_it->second.push_back(location);
1464 }
1465}
1466
1467const symbol_exprt &
1469 const codet &op_code)
1470{
1471 const symbol_exprt *const symbol =
1473
1474 if(symbol)
1475 return *symbol;
1476
1477 error() << "Instruction is not followed by symbol" << eom;
1478 throw TYPECHECK_ERROR;
1479}
1480
1482 const codet &op_code)
1483{
1484 if(op_code.operands().size() > 0)
1485 {
1486 error() << "Instruction is followed by operand" << eom;
1487 throw TYPECHECK_ERROR;
1488 }
1489}
1490
1492 const codet &op_code)
1493{
1495 if(accumulator.size() < 2)
1496 {
1497 error() << "Not enough operands in the accumulator" << eom;
1498 throw TYPECHECK_ERROR;
1499 }
1500}
1501
1503 const codet &op_code,
1504 const exprt &rlo_value)
1505{
1507 // If inside of a bit string use the value of the rlo. If this is the first
1508 // expression of a bit string, load the value of the nested operation by
1509 // implicitly setting the rlo to the specified value.
1510 if(!fc_bit)
1513 nesting_stack.push_back(stack_entry);
1514 fc_bit = false;
1515 or_bit = false;
1516}
1517
1519 const codet &op_code,
1520 const symbolt &tia_element,
1521 bool negate)
1522{
1523 const symbol_exprt &sym{
1525 const exprt op{typecheck_identifier(tia_element, sym.get_identifier())};
1526 const not_exprt not_op{op};
1527 return negate ? not_op : op;
1528}
1529
1531 const symbolt &tia_element,
1532 const irep_idt &identifier)
1533{
1534 const code_typet &element_type{to_code_type(tia_element.type)};
1535
1536 // Check for temporary variables.
1538 id2string(tia_element.name) + "::" + id2string(identifier)))
1539 {
1541 id2string(tia_element.name) + "::" + id2string(identifier))};
1542 return sym.symbol_expr();
1543 }
1544
1545 // Check for global tags.
1546 if(symbol_table.has_symbol(identifier))
1547 return symbol_table.lookup_ref(identifier).symbol_expr();
1548
1549 if(
1550 element_type.get(ID_statement_list_type) ==
1552 {
1553 // Check for variables inside of the function block interface.
1556 const symbol_exprt db_expr = data_block.symbol_expr();
1559 if(!db_type)
1561 for(const struct_union_typet::componentt &member : db_type->components())
1562 {
1563 if(member.get_name() == identifier)
1564 {
1566 const member_exprt val{deref_db, member.get_name(), member.type()};
1567 return val;
1568 }
1569 }
1570 }
1571 else if(
1573 {
1574 // Check for variables inside of the function interface.
1575 for(const auto &member : element_type.parameters())
1576 {
1577 if(member.get_base_name() == identifier)
1578 {
1579 const symbolt &par{
1580 symbol_table.get_writeable_ref(member.get_identifier())};
1581 return par.symbol_expr();
1582 }
1583 }
1584 }
1585 else
1586 UNREACHABLE; // Variable declarations should only be checked for FCs or FBs
1587
1588 error() << "Identifier could not be found in project" << eom;
1589 throw TYPECHECK_ERROR;
1590}
1591
1593 const codet &op_code,
1595{
1596 const equal_exprt *const assignment =
1598 if(assignment)
1599 {
1600 const code_assertt assertion{
1602 tia_element.value.add_to_operands(assertion);
1603 }
1604 else
1605 {
1606 error() << "No assignment found for assertion" << eom;
1607 throw TYPECHECK_ERROR;
1608 }
1609}
1610
1612 const codet &op_code,
1614{
1615 const equal_exprt *const assignment =
1617 if(assignment)
1618 {
1619 const code_assumet assumption{
1621 tia_element.value.add_to_operands(assumption);
1622 }
1623 else
1624 {
1625 error() << "No assignment found for assumption" << eom;
1626 throw TYPECHECK_ERROR;
1627 }
1628}
1629
1631 const codet &op_code,
1633{
1635 const symbolt &called_function{
1636 symbol_table.lookup_ref(call_operand.get_identifier())};
1637 const code_typet &called_type{to_code_type(called_function.type)};
1638 // Is it a STL function or STL function block?
1639 if(
1644 else
1645 {
1646 error() << "Tried to call element that is no function or function block"
1647 << eom;
1648 throw TYPECHECK_ERROR;
1649 }
1650}
1651
1653 const codet &op_code,
1655{
1658 symbol_table.lookup_ref(call_operand.get_identifier())};
1661
1662 // Check if function name is followed by data block.
1664 {
1665 error() << "Function calls should not address instance data blocks" << eom;
1666 throw TYPECHECK_ERROR;
1667 }
1668
1669 // Check if function interface matches the call and fill argument list.
1670 const code_typet::parameterst &params{called_type.parameters()};
1672 std::vector<equal_exprt> assignments;
1673 for(const auto &expr : op_code.operands())
1674 {
1676 assignments.push_back(to_equal_expr(expr));
1677 }
1678
1679 for(const code_typet::parametert &param : params)
1680 args.emplace_back(
1682
1683 // Check the return value if present.
1684 if(called_type.return_type().is_nil())
1685 tia_element.value.add_to_operands(
1687 else
1688 {
1689 const exprt lhs{typecheck_return_value_assignment(
1690 assignments, called_type.return_type(), tia_element)};
1691 tia_element.value.add_to_operands(
1693 }
1694}
1695
1697 const codet &op_code,
1699{
1700 // TODO: Implement support for function block calls.
1701 // Needs code statements which assign the parameters to the instance data
1702 // block, call the function and write the result back to the parameters
1703 // afterwards.
1704 error() << "Calls to function blocks are not supported yet" << eom;
1705 throw TYPECHECK_ERROR;
1706}
1707
1709 const std::vector<equal_exprt> &assignments,
1711 const symbolt &tia_element)
1712{
1713 const irep_idt &param_name = param.get_base_name();
1714 const typet &param_type = param.type();
1715 for(const equal_exprt &assignment : assignments)
1716 {
1717 const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1718 if(param_name == lhs.get_identifier())
1719 {
1722
1723 if(param_type == assigned_variable.type())
1724 return assigned_variable;
1725 else
1726 {
1727 error() << "Types of parameter assignment do not match: "
1728 << param.type().id() << " != " << assigned_variable.type().id()
1729 << eom;
1730 throw TYPECHECK_ERROR;
1731 }
1732 }
1733 }
1734 error() << "No assignment found for function parameter "
1735 << param.get_identifier() << eom;
1736 throw TYPECHECK_ERROR;
1737}
1738
1740 const symbolt &tia_element,
1741 const exprt &rhs)
1742{
1744 const symbol_exprt *const symbol_rhs =
1746 if(symbol_rhs)
1748 typecheck_identifier(tia_element, symbol_rhs->get_identifier());
1749 else // constant_exprt.
1750 assigned_operand = rhs;
1751 return assigned_operand;
1752}
1753
1755 const std::vector<equal_exprt> &assignments,
1756 const typet &return_type,
1757 const symbolt &tia_element)
1758{
1759 for(const equal_exprt &assignment : assignments)
1760 {
1761 const symbol_exprt &lhs{to_symbol_expr(assignment.lhs())};
1762 if(ID_statement_list_return_value_id == lhs.get_identifier())
1763 {
1764 const symbol_exprt &rhs{to_symbol_expr(assignment.rhs())};
1766 typecheck_identifier(tia_element, rhs.get_identifier())};
1767 if(return_type == assigned_variable.type())
1768 return assigned_variable;
1769 else
1770 {
1771 error() << "Types of return value assignment do not match: "
1772 << return_type.id() << " != " << assigned_variable.type().id()
1773 << eom;
1774 throw TYPECHECK_ERROR;
1775 }
1776 }
1777 }
1778 error() << "No assignment found for function return value" << eom;
1779 throw TYPECHECK_ERROR;
1780}
1781
1783{
1785
1787 or_wrapper.op1();
1788 else if(can_cast_expr<and_exprt>(or_wrapper.op1()))
1789 {
1791 and_op.add_to_operands(op);
1792 or_wrapper.op1() = and_op;
1793 }
1794 else
1795 {
1796 and_exprt and_op{or_wrapper.op1(), op};
1797 or_wrapper.op1() = and_op;
1798 }
1800}
1801
1803{
1804 fc_bit = true;
1805 or_bit = false;
1806 rlo_bit = op;
1807}
1808
1810{
1811 rlo_bit = true_exprt{};
1812 fc_bit = false;
1813 or_bit = false;
1815}
1816
1823
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
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
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
A codet representing the declaration of a local variable.
codet representation of a function call statement.
codet representation of a goto statement.
Definition std_code.h:841
codet representation of an if-then-else statement.
Definition std_code.h:460
codet representation of a label for branch targets.
Definition std_code.h:959
const irep_idt & get_label() const
Definition std_code.h:967
codet & code()
Definition std_code.h:977
A codet representing a skip statement.
Definition std_code.h:322
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Operator to dereference a pointer.
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
size_t size() const
Definition dstring.h:104
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2667
message_handlert * message_handler
Definition message.h:439
mstreamt & error() const
Definition message.h:399
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
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:2181
Boolean OR.
Definition std_expr.h:2082
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 ...
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.
const irep_idt std::vector< exprt > accumulator
Name of the module this typecheck belongs to.
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.
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.
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
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.
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
The Boolean constant true.
Definition std_expr.h:2856
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition symbol.h:133
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
Boolean XOR.
Definition std_expr.h:2145
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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:1004
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition std_expr.h:2021
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition std_expr.h:2129
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1265
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.
Structure for a simple function in Statement List.
const typet return_type
FC-exclusive return type.
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.
var_declarationst var_inout
Inout variable declarations.
var_declarationst var_output
Output variable declarations.
Struct for a single variable declaration in Statement List.
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.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177