statement_list_typecheck.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Statement List Language Type Checking
 
Author: Matthias Weiss, matthias.weiss@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
#define CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
 
#include <util/typecheck.h>
 
#include "statement_list_parse_tree.h"
 
class symbol_tablet;
class symbolt;
 
bool statement_list_typecheck(
  const statement_list_parse_treet &parse_tree,
  symbol_tablet &symbol_table,
  const std::string &module,
  message_handlert &message_handler);
 
class statement_list_typecheckt : public typecheckt
{
public:
  statement_list_typecheckt(
    const statement_list_parse_treet &parse_tree,
    symbol_tablet &symbol_table,
    const std::string &module,
    message_handlert &message_handler);
 
  void typecheck() override;
 
private:
  const statement_list_parse_treet &parse_tree;
 
  symbol_tablet &symbol_table;
 
  const irep_idt module;
 
  // Internal state of the PLC program
  // TODO: Implement complete status word representation.
  // See the Siemens documentation for further details.
 
  std::vector<exprt> accumulator;
 
  exprt rlo_bit = true_exprt();
 
  bool fc_bit = false;
 
  bool or_bit = false;
 
  struct nesting_stack_entryt
  {
    exprt rlo_bit;
 
    bool or_bit = false;
 
    codet function_code;
 
    nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code);
  };
  using nesting_stackt = std::vector<nesting_stack_entryt>;
 
  nesting_stackt nesting_stack;
 
  struct stl_label_locationt
  {
    const size_t nesting_depth;
 
    const bool jumps_permitted;
 
    const bool fc_false_required;
 
    stl_label_locationt(
      size_t nesting_depth,
      bool jumps_permitted,
      bool fc_false_required);
  };
  using stl_labelst = std::unordered_map<irep_idt, stl_label_locationt>;
 
  stl_labelst stl_labels;
 
  struct stl_jump_locationt
  {
    // TODO: Add source location to the structure.
    // Requires the source location to be added to the parser in general.
 
    const size_t nesting_depth;
 
    const bool sets_fc_false;
 
    stl_jump_locationt(size_t nesting_depth, bool sets_fc_false);
  };
  using label_referencest =
    std::unordered_map<irep_idt, std::vector<stl_jump_locationt>>;
 
  label_referencest label_references;
 
  // High level checks
 
  void typecheck_function_declaration(
    const statement_list_parse_treet::functiont &function);
 
  void typecheck_function_block_declaration(
    const statement_list_parse_treet::function_blockt &function_block);
 
  void typecheck_tag_list();
 
  void add_temp_rlo();
 
  struct_typet create_instance_data_block_type(
    const statement_list_parse_treet::function_blockt &function_block);
 
  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);
 
  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);
 
  void typecheck_temp_var_decls(
    const statement_list_parse_treet::tia_modulet &tia_module,
    symbolt &tia_symbol);
 
  void typecheck_statement_list_networks(
    const statement_list_parse_treet::tia_modulet &tia_module,
    symbolt &tia_symbol);
 
  void typecheck_label_references();
 
  void typecheck_statement_list_instruction(
    const statement_list_parse_treet::instructiont &instruction,
    symbolt &tia_element);
 
  void typecheck_code(const codet &instruction, symbolt &tia_element);
 
  void typecheck_label(const codet &instruction, symbolt &tia_element);
 
  // Load and Transfer instructions
 
  void typecheck_statement_list_load(
    const codet &op_code,
    const symbolt &tia_element);
 
  void
  typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
 
  // Arithmetic accumulator instructions (int)
 
  void typecheck_statement_list_accu_int_add(const codet &op_code);
 
  void typecheck_statement_list_accu_int_sub(const codet &op_code);
 
  void typecheck_statement_list_accu_int_div(const codet &op_code);
 
  void typecheck_statement_list_accu_int_mul(const codet &op_code);
 
  void typecheck_statement_list_accu_int_eq(const codet &op_code);
 
  void typecheck_statement_list_accu_int_neq(const codet &op_code);
 
  void typecheck_statement_list_accu_int_gt(const codet &op_code);
 
  void typecheck_statement_list_accu_int_lt(const codet &op_code);
 
  void typecheck_statement_list_accu_int_gte(const codet &op_code);
 
  void typecheck_statement_list_accu_int_lte(const codet &op_code);
 
  // Arithmetic accumulator instructions (dint)
 
  void typecheck_statement_list_accu_dint_add(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_sub(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_div(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_mul(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_eq(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_neq(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_gt(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_lt(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_gte(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_lte(const codet &op_code);
 
  // Arithmetic accumulator instructions (real)
 
  void typecheck_statement_list_accu_real_add(const codet &op_code);
 
  void typecheck_statement_list_accu_real_sub(const codet &op_code);
 
  void typecheck_statement_list_accu_real_div(const codet &op_code);
 
  void typecheck_statement_list_accu_real_mul(const codet &op_code);
 
  void typecheck_statement_list_accu_real_eq(const codet &op_code);
 
  void typecheck_statement_list_accu_real_neq(const codet &op_code);
 
  void typecheck_statement_list_accu_real_gt(const codet &op_code);
 
  void typecheck_statement_list_accu_real_lt(const codet &op_code);
 
  void typecheck_statement_list_accu_real_gte(const codet &op_code);
 
  void typecheck_statement_list_accu_real_lte(const codet &op_code);
 
  // Bit Logic instructions
 
  void typecheck_statement_list_not(const codet &op_code);
 
  void typecheck_statement_list_and(
    const codet &op_code,
    const symbolt &tia_element);
 
  void
  typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
 
  void typecheck_statement_list_xor(
    const codet &op_code,
    const symbolt &tia_element);
 
  void typecheck_statement_list_and_not(
    const codet &op_code,
    const symbolt &tia_element);
 
  void typecheck_statement_list_or_not(
    const codet &op_code,
    const symbolt &tia_element);
 
  void typecheck_statement_list_xor_not(
    const codet &op_code,
    const symbolt &tia_element);
 
  void typecheck_statement_list_and_before_or();
 
  void typecheck_statement_list_nested_and(const codet &op_code);
 
  void typecheck_statement_list_nested_or(const codet &op_code);
 
  void typecheck_statement_list_nested_xor(const codet &op_code);
 
  void typecheck_statement_list_nested_and_not(const codet &op_code);
 
  void typecheck_statement_list_nested_or_not(const codet &op_code);
 
  void typecheck_statement_list_nested_xor_not(const codet &op_code);
 
  void typecheck_statement_list_nesting_closed(const codet &op_code);
 
  void
  typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
 
  void typecheck_statement_list_set_rlo(const codet &op_code);
 
  void typecheck_statement_list_clr_rlo(const codet &op_code);
 
  void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
 
  void
  typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
 
  // Program Control instructions
 
  void
  typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
 
  // Logic Control instructions
 
  void typecheck_statement_list_jump_unconditional(
    const codet &op_code,
    symbolt &tia_element);
 
  void typecheck_statement_list_jump_conditional(
    const codet &op_code,
    symbolt &tia_element);
 
  void typecheck_statement_list_jump_conditional_not(
    const codet &op_code,
    symbolt &tia_element);
 
  // Low level checks
 
  stl_label_locationt typecheck_label_location(const code_labelt &label);
 
  void typecheck_jump_locations(
    const code_labelt &label,
    const stl_label_locationt &location);
 
  void typecheck_statement_list_accu_int_arith(const codet &op_code);
 
  void typecheck_statement_list_accu_dint_arith(const codet &op_code);
 
  void typecheck_statement_list_accu_real_arith(const codet &op_code);
 
  const symbol_exprt &
  typecheck_instruction_with_non_const_operand(const codet &op_code);
 
  void typecheck_instruction_without_operand(const codet &op_code);
 
  void typecheck_binary_accumulator_instruction(const codet &op_code);
 
  void typecheck_nested_boolean_instruction(
    const codet &op_code,
    const exprt &rlo_value);
 
  exprt typecheck_simple_boolean_instruction_operand(
    const codet &op_code,
    const symbolt &tia_element,
    bool negate);
 
  void typecheck_accumulator_compare_instruction(const irep_idt &comparison);
 
  void typecheck_label_reference(const irep_idt &label, bool sets_fc_false);
 
  exprt
  typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
 
  void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
 
  void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
 
  void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
 
  void typecheck_called_function(const codet &op_code, symbolt &tia_element);
 
  void
  typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
 
  exprt typecheck_function_call_arguments(
    const std::vector<code_frontend_assignt> &assignments,
    const code_typet::parametert &param,
    const symbolt &tia_element);
 
  exprt typecheck_function_call_argument_rhs(
    const symbolt &tia_element,
    const exprt &rhs);
 
  exprt typecheck_return_value_assignment(
    const std::vector<code_frontend_assignt> &assignments,
    const typet &return_type,
    const symbolt &tia_element);
 
  // Helper functions
 
  void add_to_or_rlo_wrapper(const exprt &op);
 
  void initialize_bit_expression(const exprt &op);
 
  void clear_module_state();
 
  void clear_network_state();
 
  void save_rlo_state(symbolt &tia_element);
};
 
#endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H