frame_enforcer.h

Go to the documentation of this file.

 
#ifndef GOTO_PROGRAMS_FRAME_ENFORCER_H
#define GOTO_PROGRAMS_FRAME_ENFORCER_H
 
#include <goto-programs/goto_program.h>
#include <util/symtab/context.h>
#include <irep2/irep2_expr.h>
#include <map>
#include <set>
#include <vector>

enum class frame_modet
{
  ASSUME,
  ASSERT
};
 
class frame_enforcert
{
public:
  struct snapshot_entryt
  {
    expr2tc original_expr; 
    expr2tc snapshot_sym;  
  };
 
  frame_enforcert(contextt &_context);

  void materialize_snapshots(
    const std::vector<expr2tc> &vars_to_snapshot,
    goto_programt &dest,
    const locationt &loc,
    const std::string &scope_prefix);

  void enforce_frame_rule(
    const std::vector<expr2tc> &explicit_assigns,
    goto_programt &dest,
    const locationt &loc,
    frame_modet mode = frame_modet::ASSUME);

  expr2tc replace_old_with_snapshots(const expr2tc &expr) const;

  expr2tc in_pre_state(const expr2tc &expr) const;

  void patch_old_snapshot_assigns(goto_programt &prog) const;

  const std::vector<snapshot_entryt> &get_active_snapshots() const
  {
    return active_snapshots;
  }

  static std::vector<expr2tc> collect_global_variables(const contextt &context);

  struct classified_assignst
  {
    std::vector<expr2tc>
      direct_targets; 
    std::vector<expr2tc>
      pointer_targets; 
    std::map<irep_idt, std::set<irep_idt>> struct_field_targets;
    std::map<irep_idt, std::set<irep_idt>> ptr_field_targets;
    std::map<irep_idt, std::vector<expr2tc>> array_elem_targets;
  };

  static classified_assignst
  classify_assigns_targets(const std::vector<expr2tc> &explicit_assigns);
 
private:
  contextt &context;

  std::vector<snapshot_entryt> active_snapshots;

  size_t snapshot_counter;

  expr2tc create_snapshot_symbol(
    const expr2tc &original,
    const std::string &prefix,
    size_t index);
};
 
#endif /* GOTO_PROGRAMS_FRAME_ENFORCER_H */