cprover
Loading...
Searching...
No Matches
statement_list_typecheck.h
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
12#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
13#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
14
15#include <util/std_code_base.h>
16#include <util/typecheck.h>
17
19
21class code_labelt;
23class symbolt;
24
36 const statement_list_parse_treet &parse_tree,
37 symbol_table_baset &symbol_table,
38 const std::string &module,
39 message_handlert &message_handler);
40
43{
44public:
56 const std::string &module,
58
61 void typecheck() override;
62
63private:
66
69
72
73 // Internal state of the PLC program
74 // TODO: Implement complete status word representation.
75 // See the Siemens documentation for further details.
76
78 std::vector<exprt> accumulator;
79
84
89 bool fc_bit = false;
90
94 bool or_bit = false;
95
113 using nesting_stackt = std::vector<nesting_stack_entryt>;
114
118
122 {
125 const size_t nesting_depth;
126
129 const bool jumps_permitted;
130
134
142 size_t nesting_depth,
143 bool jumps_permitted,
144 bool fc_false_required);
145 };
146 using stl_labelst = std::unordered_map<irep_idt, stl_label_locationt>;
147
150
153 {
154 // TODO: Add source location to the structure.
155 // Requires the source location to be added to the parser in general.
156
159 const size_t nesting_depth;
160
162 const bool sets_fc_false;
163
169 };
171 std::unordered_map<irep_idt, std::vector<stl_jump_locationt>>;
172
178
179 // High level checks
180
186
191 const statement_list_parse_treet::function_blockt &function_block);
192
195 void typecheck_tag_list();
196
199 void add_temp_rlo();
200
207 const statement_list_parse_treet::function_blockt &function_block);
208
218 const irep_idt &var_property);
219
231 const irep_idt &function_name,
232 const irep_idt &var_property);
233
240 symbolt &tia_symbol);
241
248 symbolt &tia_symbol);
249
252
259 symbolt &tia_element);
260
264 void typecheck_code(const codet &instruction, symbolt &tia_element);
265
269 void typecheck_label(const codet &instruction, symbolt &tia_element);
270
271 // Load and Transfer instructions
272
277 const codet &op_code,
278 const symbolt &tia_element);
279
284 void
285 typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
286
287 // Arithmetic accumulator instructions (int)
288
292 void typecheck_statement_list_accu_int_add(const codet &op_code);
293
297 void typecheck_statement_list_accu_int_sub(const codet &op_code);
298
302 void typecheck_statement_list_accu_int_div(const codet &op_code);
303
307 void typecheck_statement_list_accu_int_mul(const codet &op_code);
308
312 void typecheck_statement_list_accu_int_eq(const codet &op_code);
313
317 void typecheck_statement_list_accu_int_neq(const codet &op_code);
318
322 void typecheck_statement_list_accu_int_gt(const codet &op_code);
323
327 void typecheck_statement_list_accu_int_lt(const codet &op_code);
328
332 void typecheck_statement_list_accu_int_gte(const codet &op_code);
333
337 void typecheck_statement_list_accu_int_lte(const codet &op_code);
338
339 // Arithmetic accumulator instructions (dint)
340
345
350
355
360
364 void typecheck_statement_list_accu_dint_eq(const codet &op_code);
365
370
374 void typecheck_statement_list_accu_dint_gt(const codet &op_code);
375
379 void typecheck_statement_list_accu_dint_lt(const codet &op_code);
380
385
390
391 // Arithmetic accumulator instructions (real)
392
397
402
407
412
416 void typecheck_statement_list_accu_real_eq(const codet &op_code);
417
422
426 void typecheck_statement_list_accu_real_gt(const codet &op_code);
427
431 void typecheck_statement_list_accu_real_lt(const codet &op_code);
432
437
442
443 // Bit Logic instructions
444
448 void typecheck_statement_list_not(const codet &op_code);
449
455 const codet &op_code,
456 const symbolt &tia_element);
457
462 void
463 typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
464
470 const codet &op_code,
471 const symbolt &tia_element);
472
478 const codet &op_code,
479 const symbolt &tia_element);
480
486 const codet &op_code,
487 const symbolt &tia_element);
488
494 const codet &op_code,
495 const symbolt &tia_element);
496
500
504 void typecheck_statement_list_nested_and(const codet &op_code);
505
509 void typecheck_statement_list_nested_or(const codet &op_code);
510
514 void typecheck_statement_list_nested_xor(const codet &op_code);
515
520
525
530
536
541 void
542 typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
543
547 void typecheck_statement_list_set_rlo(const codet &op_code);
548
552 void typecheck_statement_list_clr_rlo(const codet &op_code);
553
558 void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
559
564 void
565 typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
566
567 // Program Control instructions
568
573 void
574 typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
575
576 // Logic Control instructions
577
583 const codet &op_code,
584 symbolt &tia_element);
585
591 const codet &op_code,
592 symbolt &tia_element);
593
599 const codet &op_code,
600 symbolt &tia_element);
601
602 // Low level checks
603
609
614 const code_labelt &label,
615 const stl_label_locationt &location);
616
620
625
629
634 const symbol_exprt &
636
639 void typecheck_instruction_without_operand(const codet &op_code);
640
645
652 const codet &op_code,
653 const exprt &rlo_value);
654
663 const codet &op_code,
664 const symbolt &tia_element,
665 bool negate);
666
671
678 void typecheck_label_reference(const irep_idt &label, bool sets_fc_false);
679
684 exprt
685 typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
686
691 void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
692
697 void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
698
703 void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
704
709 void typecheck_called_function(const codet &op_code, symbolt &tia_element);
710
715 void
716 typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
717
725 const std::vector<code_frontend_assignt> &assignments,
726 const code_typet::parametert &param,
727 const symbolt &tia_element);
728
735 const symbolt &tia_element,
736 const exprt &rhs);
737
746 const std::vector<code_frontend_assignt> &assignments,
747 const typet &return_type,
748 const symbolt &tia_element);
749
750 // Helper functions
751
755 void add_to_or_rlo_wrapper(const exprt &op);
756
760 void initialize_bit_expression(const exprt &op);
761
765 void clear_module_state();
766
770 void clear_network_state();
771
775 void save_rlo_state(symbolt &tia_element);
776};
777
778#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a label for branch targets.
Definition std_code.h:959
std::vector< parametert > parameterst
Definition std_types.h:586
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
Definition expr.h:56
message_handlert * message_handler
Definition message.h:431
Intermediate representation of a parsed Statement List file before converting it into a goto program.
std::list< var_declarationt > var_declarationst
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.
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.
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.
statement_list_typecheckt(const statement_list_parse_treet &parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
Creates a new instance of statement_list_typecheckt.
symbol_table_baset & symbol_table
Reference to the symbol table that should be filled during the typecheck.
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_return_value_assignment(const std::vector< code_frontend_assignt > &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...
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.
std::unordered_map< irep_idt, stl_label_locationt > stl_labelst
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.
exprt typecheck_function_call_arguments(const std::vector< code_frontend_assignt > &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...
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...
std::vector< nesting_stack_entryt > nesting_stackt
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.
std::unordered_map< irep_idt, std::vector< stl_jump_locationt > > label_referencest
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.
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:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
The Boolean constant true.
Definition std_expr.h:3190
typecheckt(message_handlert &_message_handler)
Definition typecheck.h:18
The type of an expression, extends irept.
Definition type.h:29
Statement List Language Parse Tree.
bool statement_list_typecheck(const statement_list_parse_treet &parse_tree, symbol_table_baset &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.
Structure for a simple function block in Statement List.
Structure for a simple function in Statement List.
Represents a regular Statement List instruction which consists out of one or more codet tokens.
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
exprt rlo_bit
The rlo's value when the entry was generated.
codet function_code
OP code of the instruction that generated the stack entry.
bool or_bit
The OR bit's value when the entry was generated.
const size_t nesting_depth
The size of the nesting stack at the label location, used for checking scope violations.
stl_jump_locationt(size_t nesting_depth, bool sets_fc_false)
Constructs a new location with the specified properties.
const bool sets_fc_false
States if the jump instruction sets the /FC bit to false.
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.
const size_t nesting_depth
The size of the nesting stack at the label location, used for checking scope violations.
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.
dstringt irep_idt