cprover
statement_list_typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Type Checking
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
13 #define CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
14 
15 #include <util/symbol_table.h>
16 #include <util/typecheck.h>
17 
19 
31  const statement_list_parse_treet &parse_tree,
32  symbol_tablet &symbol_table,
33  const std::string &module,
34  message_handlert &message_handler);
35 
38 {
39 public:
51  const std::string &module,
53 
56  void typecheck() override;
57 
58 private:
61 
64 
67 
68  // Internal state of the PLC program
69  // TODO: Implement complete status word representation.
70  // See the Siemens documentation for further details.
71 
73  std::vector<exprt> accumulator;
74 
79 
84  bool fc_bit = false;
85 
89  bool or_bit = false;
90 
96  {
99 
101  bool or_bit = false;
102 
105 
107  };
108  using nesting_stackt = std::vector<nesting_stack_entryt>;
109 
113 
114  // High level checks
115 
120  const statement_list_parse_treet::functiont &function);
121 
126  const statement_list_parse_treet::function_blockt &function_block);
127 
130  void typecheck_tag_list();
131 
134  void add_temp_rlo();
135 
142  const statement_list_parse_treet::function_blockt &function_block);
143 
153  const irep_idt &var_property);
154 
165  code_typet::parameterst &params,
166  const irep_idt &function_name,
167  const irep_idt &var_property);
168 
174  const statement_list_parse_treet::tia_modulet &tia_module,
175  symbolt &tia_symbol);
176 
182  const statement_list_parse_treet::tia_modulet &tia_module,
183  symbolt &tia_symbol);
184 
190  const statement_list_parse_treet::instructiont &instruction,
191  symbolt &tia_element);
192 
193  // Load and Transfer instructions
194 
199  const codet &op_code,
200  const symbolt &tia_element);
201 
206  void
207  typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
208 
209  // Arithmetic accumulator instructions (int)
210 
214  void typecheck_statement_list_accu_int_add(const codet &op_code);
215 
219  void typecheck_statement_list_accu_int_sub(const codet &op_code);
220 
224  void typecheck_statement_list_accu_int_div(const codet &op_code);
225 
229  void typecheck_statement_list_accu_int_mul(const codet &op_code);
230 
234  void typecheck_statement_list_accu_int_eq(const codet &op_code);
235 
239  void typecheck_statement_list_accu_int_neq(const codet &op_code);
240 
244  void typecheck_statement_list_accu_int_gt(const codet &op_code);
245 
249  void typecheck_statement_list_accu_int_lt(const codet &op_code);
250 
254  void typecheck_statement_list_accu_int_gte(const codet &op_code);
255 
259  void typecheck_statement_list_accu_int_lte(const codet &op_code);
260 
261  // Arithmetic accumulator instructions (dint)
262 
266  void typecheck_statement_list_accu_dint_add(const codet &op_code);
267 
271  void typecheck_statement_list_accu_dint_sub(const codet &op_code);
272 
276  void typecheck_statement_list_accu_dint_div(const codet &op_code);
277 
281  void typecheck_statement_list_accu_dint_mul(const codet &op_code);
282 
286  void typecheck_statement_list_accu_dint_eq(const codet &op_code);
287 
291  void typecheck_statement_list_accu_dint_neq(const codet &op_code);
292 
296  void typecheck_statement_list_accu_dint_gt(const codet &op_code);
297 
301  void typecheck_statement_list_accu_dint_lt(const codet &op_code);
302 
306  void typecheck_statement_list_accu_dint_gte(const codet &op_code);
307 
311  void typecheck_statement_list_accu_dint_lte(const codet &op_code);
312 
313  // Arithmetic accumulator instructions (real)
314 
318  void typecheck_statement_list_accu_real_add(const codet &op_code);
319 
323  void typecheck_statement_list_accu_real_sub(const codet &op_code);
324 
328  void typecheck_statement_list_accu_real_div(const codet &op_code);
329 
333  void typecheck_statement_list_accu_real_mul(const codet &op_code);
334 
338  void typecheck_statement_list_accu_real_eq(const codet &op_code);
339 
343  void typecheck_statement_list_accu_real_neq(const codet &op_code);
344 
348  void typecheck_statement_list_accu_real_gt(const codet &op_code);
349 
353  void typecheck_statement_list_accu_real_lt(const codet &op_code);
354 
358  void typecheck_statement_list_accu_real_gte(const codet &op_code);
359 
363  void typecheck_statement_list_accu_real_lte(const codet &op_code);
364 
365  // Bit Logic instructions
366 
370  void typecheck_statement_list_not(const codet &op_code);
371 
377  const codet &op_code,
378  const symbolt &tia_element);
379 
384  void
385  typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
386 
392  const codet &op_code,
393  const symbolt &tia_element);
394 
400  const codet &op_code,
401  const symbolt &tia_element);
402 
408  const codet &op_code,
409  const symbolt &tia_element);
410 
416  const codet &op_code,
417  const symbolt &tia_element);
418 
422 
426  void typecheck_statement_list_nested_and(const codet &op_code);
427 
431  void typecheck_statement_list_nested_or(const codet &op_code);
432 
436  void typecheck_statement_list_nested_xor(const codet &op_code);
437 
441  void typecheck_statement_list_nested_and_not(const codet &op_code);
442 
446  void typecheck_statement_list_nested_or_not(const codet &op_code);
447 
451  void typecheck_statement_list_nested_xor_not(const codet &op_code);
452 
457  void typecheck_statement_list_nesting_closed(const codet &op_code);
458 
463  void
464  typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
465 
469  void typecheck_statement_list_set_rlo(const codet &op_code);
470 
474  void typecheck_statement_list_clr_rlo(const codet &op_code);
475 
480  void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
481 
486  void
487  typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
488 
489  // Control instructions
490 
495  void
496  typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
497 
498  // Low level checks
499 
502  void typecheck_statement_list_accu_int_arith(const codet &op_code);
503 
507  void typecheck_statement_list_accu_dint_arith(const codet &op_code);
508 
511  void typecheck_statement_list_accu_real_arith(const codet &op_code);
512 
517  const symbol_exprt &
519 
522  void typecheck_instruction_without_operand(const codet &op_code);
523 
527  void typecheck_binary_accumulator_instruction(const codet &op_code);
528 
535  const codet &op_code,
536  const exprt &rlo_value);
537 
546  const codet &op_code,
547  const symbolt &tia_element,
548  bool negate);
549 
553  void typecheck_accumulator_compare_instruction(const irep_idt &comparison);
554 
559  exprt
560  typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
561 
566  void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
567 
572  void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
573 
578  void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
579 
584  void typecheck_called_function(const codet &op_code, symbolt &tia_element);
585 
590  void
591  typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
592 
600  const std::vector<equal_exprt> &assignments,
601  const code_typet::parametert &param,
602  const symbolt &tia_element);
603 
610  const symbolt &tia_element,
611  const exprt &rhs);
612 
621  const std::vector<equal_exprt> &assignments,
622  const typet &return_type,
623  const symbolt &tia_element);
624 
625  // Helper functions
626 
630  void add_to_or_rlo_wrapper(const exprt &op);
631 
635  void initialize_bit_expression(const exprt &op);
636 
640  void save_rlo_state(symbolt &tia_element);
641 };
642 
643 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
std::vector< parametert > parameterst
Definition: std_types.h:746
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
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.
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 typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
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 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_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.
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.
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.
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.
bool fc_bit
First Check (Part of the TIA status word).
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_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:226
std::vector< componentt > componentst
Definition: std_types.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The Boolean constant true.
Definition: std_expr.h:2717
The type of an expression, extends irept.
Definition: type.h:28
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...
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.
Author: Diffblue Ltd.