goto_loop_invariant.h

Go to the documentation of this file.

#ifndef GOTO_PROGRAMS_GOTO_LOOP_INVARIANT_H_
#define GOTO_PROGRAMS_GOTO_LOOP_INVARIANT_H_
 
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_loops.h>
#include <irep2/irep2_guard.h>
#include <util/symtab/context.h>
#include <irep2/irep2_expr.h>
#include <set>
#include <unordered_set>
#include <vector>

extern const char *const kSynthesisedInvariantProperty;
 
namespace loop_invariant
{
bool is_inert_scan_instruction(goto_programt::const_targett t);
} // namespace loop_invariant
 
// Forward declaration: full definition is in frame_enforcer.h (included in
// .cpp)
class frame_enforcert;

void goto_loop_invariant(
  goto_functionst &goto_functions,
  contextt &context,
  bool use_frame_rule);

void goto_loop_invariant_combined(goto_functionst &goto_functions);
 
class goto_loop_invariantt : public goto_loopst
{
public:
  static constexpr size_t kMaxInvariantSearchBack = 10;
 
  goto_loop_invariantt(
    const irep_idt &_function_name,
    goto_functionst &_goto_functions,
    goto_functiont &_goto_function,
    contextt &_context,
    bool _use_frame_rule)
    : goto_loopst(_function_name, _goto_functions, _goto_function),
      context(_context),
      use_frame_rule(_use_frame_rule)
  {
    if (function_loops.size())
      goto_loop_invariant();
  }
 
protected:
  contextt &context;
  bool use_frame_rule;

  frame_enforcert *active_frame_enforcer = nullptr;
  std::vector<expr2tc> active_loop_assigns;
  static constexpr unsigned kMaxHavocPointeeBits = 1024;
 
  void goto_loop_invariant();
 
  void convert_loop_with_invariant(loopst &loop);
 
  // Extract loop invariants from LOOP_INVARIANT instructions
  std::vector<expr2tc> extract_loop_invariants(const loopst &loop);
 
  // Extract loop assigns targets from LOOP_INVARIANT instructions
  std::vector<expr2tc> extract_loop_assigns(const loopst &loop);

  static void collect_symbols(const expr2tc &expr, std::set<irep_idt> &symbols);

  void extract_and_remove_side_effects(
    goto_programt::targett loop_head,
    const loopst &loop,
    const std::vector<expr2tc> &invariants,
    goto_programt &side_effects_out);
 
  // Insert ASSERT invariant before loop (prepends side_effects if non-empty)
  void insert_assert_before_loop(
    goto_programt::targett &loop_head,
    const std::vector<expr2tc> &invariants,
    const goto_programt &side_effects);
 
  static type2tc havoc_pointee_type(const expr2tc &ptr, const namespacet &ns);

  bool pointees_havocable(const loopst &loop) const;
 
  // Insert HAVOC and ASSUME at \p loop_head, which must be the loop head's own
  // instruction, so that everything the guard evaluates runs after the havoc
  // (inserts side_effects between the HAVOC block and the ASSUME).
  // side_effects is non-const: if frame rule is active, old_snapshot assigns
  // are patched in-place so insert_inductive_step_and_termination (called
  // after this) sees the patched version too.
  void havoc_pointees(
    const loopst &loop,
    const locationt &loc,
    goto_programt &dest) const;
 
  void insert_havoc_and_assume_before_condition(
    goto_programt::targett loop_head,
    const loopst &loop,
    const std::vector<expr2tc> &invariants,
    const std::vector<expr2tc> &loop_assigns,
    goto_programt &side_effects);
 
  // Insert inductive step verification and loop termination
  // (prepends side_effects before the ASSERT)
  void insert_inductive_step_and_termination(
    const loopst &loop,
    const std::vector<expr2tc> &invariants,
    const goto_programt &side_effects);
};
 
// ---------------------------------------------------------------------------
// Combined mode: Branch 1 invariant verification pass
// ---------------------------------------------------------------------------

class goto_loop_invariant_combinedt : public goto_loopst
{
public:
  goto_loop_invariant_combinedt(
    const irep_idt &_function_name,
    goto_functionst &_goto_functions,
    goto_functiont &_goto_function)
    : goto_loopst(_function_name, _goto_functions, _goto_function)
  {
    if (!function_loops.empty())
      process_loops_combined();
  }
 
private:
  void process_loops_combined();

  void insert_invariant_verification_branch(loopst &loop);

  void copy_loop_body(
    goto_programt::targett body_begin,
    goto_programt::targett loop_exit,
    goto_programt &out) const;
};
 
#endif /* GOTO_PROGRAMS_GOTO_LOOP_INVARIANT_H_ */