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/typecheck.h>
16
18
19class symbol_tablet;
20class symbolt;
21
33 const statement_list_parse_treet &parse_tree,
34 symbol_tablet &symbol_table,
35 const std::string &module,
36 message_handlert &message_handler);
37
40{
41public:
53 const std::string &module,
55
58 void typecheck() override;
59
60private:
63
66
69
70 // Internal state of the PLC program
71 // TODO: Implement complete status word representation.
72 // See the Siemens documentation for further details.
73
75 std::vector<exprt> accumulator;
76
81
86 bool fc_bit = false;
87
91 bool or_bit = false;
92
98 {
101
103 bool or_bit = false;
104
107
109 };
110 using nesting_stackt = std::vector<nesting_stack_entryt>;
111
115
119 {
122 const size_t nesting_depth;
123
126 const bool jumps_permitted;
127
131
139 size_t nesting_depth,
140 bool jumps_permitted,
141 bool fc_false_required);
142 };
143 using stl_labelst = std::unordered_map<irep_idt, stl_label_locationt>;
144
147
150 {
151 // TODO: Add source location to the structure.
152 // Requires the source location to be added to the parser in general.
153
156 const size_t nesting_depth;
157
159 const bool sets_fc_false;
160
166 };
168 std::unordered_map<irep_idt, std::vector<stl_jump_locationt>>;
169
175
176 // High level checks
177
183
188 const statement_list_parse_treet::function_blockt &function_block);
189
192 void typecheck_tag_list();
193
196 void add_temp_rlo();
197
204 const statement_list_parse_treet::function_blockt &function_block);
205
215 const irep_idt &var_property);
216
228 const irep_idt &function_name,
229 const irep_idt &var_property);
230
237 symbolt &tia_symbol);
238
245 symbolt &tia_symbol);
246
249
256 symbolt &tia_element);
257
261 void typecheck_code(const codet &instruction, symbolt &tia_element);
262
266 void typecheck_label(const codet &instruction, symbolt &tia_element);
267
268 // Load and Transfer instructions
269
274 const codet &op_code,
275 const symbolt &tia_element);
276
281 void
282 typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
283
284 // Arithmetic accumulator instructions (int)
285
289 void typecheck_statement_list_accu_int_add(const codet &op_code);
290
294 void typecheck_statement_list_accu_int_sub(const codet &op_code);
295
299 void typecheck_statement_list_accu_int_div(const codet &op_code);
300
304 void typecheck_statement_list_accu_int_mul(const codet &op_code);
305
309 void typecheck_statement_list_accu_int_eq(const codet &op_code);
310
314 void typecheck_statement_list_accu_int_neq(const codet &op_code);
315
319 void typecheck_statement_list_accu_int_gt(const codet &op_code);
320
324 void typecheck_statement_list_accu_int_lt(const codet &op_code);
325
329 void typecheck_statement_list_accu_int_gte(const codet &op_code);
330
334 void typecheck_statement_list_accu_int_lte(const codet &op_code);
335
336 // Arithmetic accumulator instructions (dint)
337
342
347
352
357
361 void typecheck_statement_list_accu_dint_eq(const codet &op_code);
362
367
371 void typecheck_statement_list_accu_dint_gt(const codet &op_code);
372
376 void typecheck_statement_list_accu_dint_lt(const codet &op_code);
377
382
387
388 // Arithmetic accumulator instructions (real)
389
394
399
404
409
413 void typecheck_statement_list_accu_real_eq(const codet &op_code);
414
419
423 void typecheck_statement_list_accu_real_gt(const codet &op_code);
424
428 void typecheck_statement_list_accu_real_lt(const codet &op_code);
429
434
439
440 // Bit Logic instructions
441
445 void typecheck_statement_list_not(const codet &op_code);
446
452 const codet &op_code,
453 const symbolt &tia_element);
454
459 void
460 typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
461
467 const codet &op_code,
468 const symbolt &tia_element);
469
475 const codet &op_code,
476 const symbolt &tia_element);
477
483 const codet &op_code,
484 const symbolt &tia_element);
485
491 const codet &op_code,
492 const symbolt &tia_element);
493
497
501 void typecheck_statement_list_nested_and(const codet &op_code);
502
506 void typecheck_statement_list_nested_or(const codet &op_code);
507
511 void typecheck_statement_list_nested_xor(const codet &op_code);
512
517
522
527
533
538 void
539 typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
540
544 void typecheck_statement_list_set_rlo(const codet &op_code);
545
549 void typecheck_statement_list_clr_rlo(const codet &op_code);
550
555 void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
556
561 void
562 typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
563
564 // Program Control instructions
565
570 void
571 typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
572
573 // Logic Control instructions
574
580 const codet &op_code,
581 symbolt &tia_element);
582
588 const codet &op_code,
589 symbolt &tia_element);
590
596 const codet &op_code,
597 symbolt &tia_element);
598
599 // Low level checks
600
606
611 const code_labelt &label,
612 const stl_label_locationt &location);
613
617
622
626
631 const symbol_exprt &
633
636 void typecheck_instruction_without_operand(const codet &op_code);
637
642
649 const codet &op_code,
650 const exprt &rlo_value);
651
660 const codet &op_code,
661 const symbolt &tia_element,
662 bool negate);
663
668
675 void typecheck_label_reference(const irep_idt &label, bool sets_fc_false);
676
681 exprt
682 typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
683
688 void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
689
694 void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
695
700 void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
701
706 void typecheck_called_function(const codet &op_code, symbolt &tia_element);
707
712 void
713 typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
714
722 const std::vector<equal_exprt> &assignments,
723 const code_typet::parametert &param,
724 const symbolt &tia_element);
725
732 const symbolt &tia_element,
733 const exprt &rhs);
734
743 const std::vector<equal_exprt> &assignments,
744 const typet &return_type,
745 const symbolt &tia_element);
746
747 // Helper functions
748
752 void add_to_or_rlo_wrapper(const exprt &op);
753
757 void initialize_bit_expression(const exprt &op);
758
762 void clear_module_state();
763
767 void clear_network_state();
768
772 void save_rlo_state(symbolt &tia_element);
773};
774
775#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
codet representation of a label for branch targets.
Definition: std_code.h:959
std::vector< parametert > parameterst
Definition: std_types.h:542
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
message_handlert * message_handler
Definition: message.h:439
Intermediate representation of a parsed Statement List file before converting it into a goto program.
std::list< var_declarationt > var_declarationst
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.
std::unordered_map< irep_idt, std::vector< stl_jump_locationt > > label_referencest
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.
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.
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.
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.
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
The symbol table.
Definition: symbol_table.h:14
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:2856
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_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.
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.
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
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.
Holds information about the properties of a jump instruction.
const size_t nesting_depth
The size of the nesting stack at the label location, used for checking scope violations.
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.
const bool fc_false_required
States if jump instructions to this location need to set the /FC bit to false.