interval_domain.h

Go to the documentation of this file.

 
#ifndef CPROVER_ANALYSES_INTERVAL_DOMAIN_H
#define CPROVER_ANALYSES_INTERVAL_DOMAIN_H
 
#include <goto-programs/abstract-interpretation/ai.h>
#include <goto-programs/abstract-interpretation/interval_template.h>
#include <goto-programs/abstract-interpretation/wrapped_interval.h>
#include <boost/serialization/nvp.hpp>
#include <util/arith/ieee_float.h>
#include <irep2/irep2_utils.h>
#include <util/arith/mp_arith.h>
#include <util/base/threeval.h>
#include <boost/multiprecision/cpp_bin_float.hpp>
#include <variant>

class interval_domaint : public ai_domain_baset
{
public:
  using integer_intervalt = interval_templatet<BigInt>;
  using real_intervalt =
    interval_templatet<boost::multiprecision::cpp_bin_float_100>;
 
  using interval = std::variant<
    std::shared_ptr<integer_intervalt>,
    std::shared_ptr<real_intervalt>,
    std::shared_ptr<wrapped_interval>>;
 
  // Map of variables into intervals.
  // If a key does not exist then imply the TOP interval.
  // If a key exists then the shared_ptr must point to a valid place
  using interval_map = std::unordered_map<irep_idt, interval, irep_id_hash>;
 
  interval_domaint() : bottom(true)
  {
  }
 
  void transform(
    goto_programt::const_targett from,
    goto_programt::const_targett to,
    ai_baset &ai,
    const namespacet &ns) final override;
 
  void output(std::ostream &out) const override;
 
  static void set_options(const optionst &options);
 
  void dump() const;
 
  // TODO: Add options for ai.h
  // Extensions
  static bool enable_interval_arithmetic;         
  static bool enable_interval_bitwise_arithmetic; 
  static bool enable_modular_intervals; 
  static bool enable_assertion_simplification; 
  static bool
    enable_contraction_for_abstract_states; 
  static bool
    enable_wrapped_intervals; 
  static bool enable_real_intervals; 
  static bool enable_assume_asserts; 
  static bool enable_eval_assumptions; 
  static bool enable_ibex_contractor;  

  static thread_local bool skip_inductive_step_instructions;
  // Widening options
  static unsigned
    fixpoint_limit; 
  static bool widening_under_approximate_bound; 
  static bool widening_extrapolate; 
  static bool widening_narrowing;   

  static tvt
  eval_boolean_expression(const expr2tc &cond, const interval_domaint &id);
 
protected:
  bool join(const interval_domaint &b, const goto_programt::const_targett &to);
 
public:
  bool merge(
    const interval_domaint &b,
    goto_programt::const_targett,
    goto_programt::const_targett to)
  {
    const bool result = join(b, to);
    copied = false;
    return result;
  }
 
  void clear_state()
  {
    intervals = get_empty();
    // get_empty() is shared: the next write must copy it first.
    copied = false;
  }
 
  // no states
  void make_bottom() final override
  {
    clear_state();
    bottom = true;
  }
 
  // all states
  void make_top() final override
  {
    clear_state();
    bottom = false;
  }
 
  void make_entry() final override
  {
    make_top();
  }
 
  bool is_bottom() const override final
  {
    return bottom;
  }
 
  bool is_top() const override final
  {
    return !bottom && intervals->empty();
  }

  expr2tc make_expression(const expr2tc &symbol) const;

  void assume(const expr2tc &);

  void assume_assertion(const expr2tc &guard, const ai_baset &ai);

  void process_instruction(goto_programt::const_targett from);

  void join_snapshot(const std::shared_ptr<interval_map> &snapshot);

  void havoc_rec(const expr2tc &expr);

  void havoc_written_arguments(const code_function_call2t &call);

  bool havoc_pointee(const expr2tc &arg, bool any_type);

  virtual bool
  ai_simplify(expr2tc &condition, const namespacet &ns) const override;
 
  std::shared_ptr<interval_map> intervals;
  bool copied = false;
 
  static std::shared_ptr<interval_map> get_empty()
  {
    static std::shared_ptr<interval_map> map = std::make_shared<interval_map>();
    return map;
  }
  void copy_if_needed()
  {
    if (copied)
      return;
    std::shared_ptr<interval_map> cpy = std::make_shared<interval_map>();
    *cpy = *intervals;
    intervals = cpy;
    copied = true;
  }
 
protected:
  // Abstract state information
  bool bottom;

  void assume_rec(const expr2tc &expr, bool negation = false);

  void assume_rec(const expr2tc &lhs, expr2t::expr_ids id, const expr2tc &rhs);

  void assign(const expr2tc &assignment, const bool recursive = false);

  template <class Interval>
  void apply_assignment(const expr2tc &lhs, const expr2tc &rhs, bool recursive);

  template <class Interval>
  Interval
  extrapolate_intervals(const Interval &before, const Interval &after) const;

  template <class Interval>
  Interval interpolate_intervals(const Interval &before, const Interval &after);

  template <class Interval>
  void apply_assume_less(const expr2tc &lhs, const expr2tc &rhs);

  template <class Interval>
  void apply_assume_symbol_truth(const symbol2t &sym, bool is_false);

  template <class Interval>
  Interval generate_modular_interval(const type2tc &t) const;

  template <class Interval>
  Interval wrap_to_type(const Interval &i, const type2tc &t) const;
 
public:
  template <class Interval>
  Interval get_interval(const expr2tc &e) const;

  template <class Interval>
  Interval get_interval_from_symbol(const symbol2t &sym) const;
 
  template <size_t Index, class Interval>
  Interval get_interval_from_variant(const symbol2t &sym) const;
 
  template <class Interval>
  bool join_intervals(
    const std::shared_ptr<Interval> &after,
    std::shared_ptr<Interval> &dst,
    bool can_extrapolate) const;

  template <class Interval>
  Interval get_interval_from_const(const expr2tc &sym) const;
 
  template <class Interval>
  Interval
  get_interval_from_typecast(const typecast2t &cast, Interval result) const;
 
  template <class Interval>
  Interval get_top_interval_from_expr(const expr2tc &sym) const;
 
  template <class Interval>
  bool is_mapped(const symbol2t &sym) const;
 
  template <class Interval>
  expr2tc make_expression_helper(const expr2tc &symbol) const;
 
  template <class Interval>
  expr2tc make_expression_value(
    const Interval &interval,
    const type2tc &type,
    bool upper) const;
 
protected:
  template <class IntervalMap>
  bool join(
    IntervalMap &new_map,
    const IntervalMap &previous_map,
    const bool is_guard_instruction = true);

  template <class Interval>
  void update_symbol_interval(const symbol2t &sym, const Interval &value);
 
  template <size_t Index, class Interval>
  void update_symbol_from_variant(const symbol2t &sym, const Interval &value);
};
 
#endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H