ld_converter.h

Go to the documentation of this file.

#pragma once
 
#include <ld-frontend/ir/ld_ir.h>
#include <util/symtab/context.h>
#include <util/irep/std_code.h>
#include <util/irep/std_expr.h>
#include <optional>
#include <string>
 
// ld_converter translates LdIR into ESBMC's GOTO IR (irep2 / contextt).
//
// Pattern mirrors python_converter: the caller (ld_languaget::typecheck) passes
// the context in; convert() adds all symbolt entries, the scan loop function,
// and the loop-free __ESBMC_main that calls it.  No C file is produced.
class ld_converter
{
public:
  ld_converter(contextt &context, const LdIR &ir);

  void convert();

  void prepend_static_init();

  void enable_fault_injection(bool enabled)
  {
    fault_injection_ = enabled;
  }
 
private:
  contextt &context_;
  const LdIR &ir_;
  bool fault_injection_ = false;
 
  // Edge contact evaluations so far; each keeps its own previous sample.
  unsigned edge_contacts_ = 0;
 
  typet bool_t() const;
  typet dint_type() const;
  typet type_of_kind(VarKind kind) const; // IEC 61131-3 type -> ESBMC typet
  exprt int_const(long long value, const typet &type) const;
 
  symbol_exprt declare_variable(const VarDecl &v);
  symbol_exprt declare_bool_shadow(const std::string &id);
  symbol_exprt declare_scoped(const std::string &id, const typet &t);
  symbol_exprt var_expr(const std::string &name) const;
  exprt bool_value_of(const symbol_exprt &var) const;
 
  code_blockt build_scan_body(const exprt &pf_in);
 
  exprt translate_contact(const LdIRNode &n, code_blockt &blk);
  codet translate_coil(const LdIRNode &n, const exprt &pf);
  codet translate_timer(const LdIRNode &n);
  codet translate_counter(const LdIRNode &n);
  codet translate_arith(const LdIRNode &n);
  codet translate_user_fb(const UserFBExec &ex);
  std::optional<code_blockt> translate_fb_body(const UserFBExec &ex);
  std::optional<exprt>
  wire_source(const std::string &source, const typet &type) const;
  exprt input_value(
    const UserFBExec &ex,
    const std::string &pin,
    const typet &type) const;
  void declare_user_fb_interfaces();
 
  void emit_scan_function(const code_blockt &scan_body);
  void emit_main_function();
};