complexity_limiter.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: John Dumbell
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
#define CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
 
#include <util/message.h>
 
#include "complexity_violation.h"
#include "symex_complexity_limit_exceeded_action.h"
 
class optionst;

class complexity_limitert
{
public:
  complexity_limitert(message_handlert &logger, const optionst &options);

  inline bool complexity_limits_active()
  {
    return this->complexity_active;
  }

  complexity_violationt check_complexity(goto_symex_statet &state);

  void run_transformations(
    complexity_violationt complexity_violation,
    goto_symex_statet &current_state);

  static std::size_t bounded_expr_size(const exprt &expr, std::size_t limit);
 
protected:
  mutable messaget log;

  bool complexity_active = false;

  std::vector<symex_complexity_limit_exceeded_actiont>
    violation_transformations;

  symex_complexity_limit_exceeded_actiont default_transformation;

  std::size_t max_complexity = 0;

  std::size_t max_loops_complexity = 0;

  bool are_loop_children_too_complicated(call_stackt &current_call_stack);

  static bool in_blacklisted_loop(
    const call_stackt &current_call_stack,
    const goto_programt::const_targett &instr);

  static framet::active_loop_infot *
  get_current_active_loop(call_stackt &current_call_stack);
};
 
#endif // CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H