goto_loops.h

Go to the documentation of this file.

#ifndef GOTO_PROGRAMS_GOTO_LOOPS_H_
#define GOTO_PROGRAMS_GOTO_LOOPS_H_
 
#include <goto-programs/goto_functions.h>
#include <goto-programs/loopst.h>
#include <util/irep/std_types.h>
#include <unordered_map>

bool check_var_name(const expr2tc &expr);
 
class goto_loopst
{
protected:
  irep_idt function_name;
  goto_functionst &goto_functions;
  goto_functiont &goto_function;
 
  typedef std::list<loopst> function_loopst;
  function_loopst function_loops;

  struct function_summaryt
  {
    loopst::loop_varst modified;
    loopst::loop_varst unmodified;
    bool modifies_pointer_array = false;
    bool writes_through_pointer = false;
    bool pointer_write_unresolvable = false;
    loopst::loop_varst written_pointers;
    bool unnamed_write = false;
    std::unordered_set<irep_idt, irep_id_hash> address_taken;
 
    void record_write(const expr2tc &lhs);
    void bind_arguments(
      const goto_functiont &callee,
      const std::vector<expr2tc> &arguments);
  };
  std::unordered_map<irep_idt, function_summaryt, irep_id_hash>
    function_summary_cache;
 
  void create_function_loop(
    goto_programt::instructionst::iterator loop_head,
    goto_programt::instructionst::iterator loop_exit);
 
  void get_modified_variables(
    goto_programt::instructionst::iterator instruction,
    function_loopst::iterator loop,
    std::vector<irep_idt> &function_name);

  bool compute_function_summary(
    const irep_idt &fname,
    std::vector<irep_idt> &in_progress,
    function_summaryt &out);
 
  static void
  merge_summary(const function_summaryt &from, function_summaryt &out);
 
  static void note_pointer_write(
    const expr2tc &target,
    function_summaryt &local,
    std::vector<expr2tc> &written_ptrs);

  bool summarise_call(
    const code_function_call2t &call,
    std::vector<irep_idt> &in_progress,
    function_summaryt &local,
    std::vector<expr2tc> &written_ptrs);
 
  static void apply_callee_summary(
    loopst &loop,
    const function_summaryt &summary,
    const code_function_call2t &call);
 
  void collect_address_taken(const expr2tc &expr, function_summaryt &out) const;

  void collect_loop_symbols(const expr2tc &expr, loopst::loop_varst &out) const;

  void collect_lhs_symbols(const expr2tc &expr, function_summaryt &out) const;
 
  void add_modified_var(loopst &loop, const expr2tc &expr);
  void add_unmodified_var(loopst &loop, const expr2tc &expr);
 
  void add_loop_var(loopst &loop, const expr2tc &expr, bool is_modified);
 
public:
  goto_loopst(
    const irep_idt &_function_name,
    goto_functionst &_goto_functions,
    goto_functiont &_goto_function)
    : function_name(_function_name),
      goto_functions(_goto_functions),
      goto_function(_goto_function)
  {
    find_function_loops();
  }
 
  void find_function_loops();
  void dump() const;
 
  const function_loopst &get_loops() const
  {
    return function_loops;
  }
 
  function_loopst &get_loops()
  {
    return function_loops;
  }
};
 
#endif /* GOTO_PROGRAMS_GOTO_LOOPS_H_ */