slice.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_SYMEX_SLICE_H
#define CPROVER_GOTO_SYMEX_SLICE_H
 
#include <goto-symex/equation/symex_target_equation.h>
#include <util/base/time_stopping.h>
#include <goto-programs/property_verdict.h>
#include <goto-symex/equation/ssa_step_algorithm.h>
#include <util/config/options.h>
#include <boost/range/adaptor/reversed.hpp>
#include <langapi/language_util.h>
 
/* Base interface */
class slicer : public ssa_step_algorithm
{
public:
  slicer() : ssa_step_algorithm(true)
  {
  }
  BigInt ignored() const override
  {
    return sliced;
  }
 
protected:
  BigInt sliced = 0;
};

class simple_slice : public slicer
{
public:
  simple_slice() = default;
  bool run(symex_target_equationt::SSA_stepst &) override;
};

class claim_slicer : public slicer
{
public:
  explicit claim_slicer(
    const size_t claim_to_keep,
    bool show_slice_info,
    bool is_goto_cov,
    namespacet &ns)
    : claim_to_keep(claim_to_keep),
      show_slice_info(show_slice_info),
      is_goto_cov(is_goto_cov),
      ns(ns)
  {
    if (!claim_to_keep)
    {
      log_error("All the claims start from 1 (use --show-claims)");
      abort();
    }
  };
  bool run(symex_target_equationt::SSA_stepst &) override;
  size_t claim_to_keep;
  std::string claim_msg;
  std::string claim_loc;
  std::string claim_cstr;
  std::string claim_key;
  const goto_programt::instructiont *claim_instruction = nullptr;
  property_locationt claim_ploc;
  std::string claim_property;
  std::string claim_comment;
  locationt claim_location;
  bool claim_after_invariant_havoc = false;
  bool show_slice_info;
  bool is_goto_cov;
  namespacet ns;
};

class symex_slicet : public slicer
{
public:
  explicit symex_slicet(const optionst &options)
    : slice_assumes(options.get_bool_option("slice-assumes")),
      slice_nondet(
        !options.get_bool_option("generate-testcase") &&
        !options.get_bool_option("generate-ctest-testcase"))
  {
  }

  bool run(symex_target_equationt::SSA_stepst &eq) override
  {
    // The slicer object is reused across equations (e.g. incremental-bmc /
    // k-induction run it once per produced formula). Each formula must be
    // sliced independently, so clear all per-equation state up front.
    // (Previously only `sliced` was reset, leaking `depends` across equations.)
    sliced = 0;
    depends.clear();
    collected_cache.clear();
    index_reads.clear();
    array_disqualified.clear();
    scanned_cache.clear();
 
    fine_timet algorithm_start = current_time();
    for (auto &step : boost::adaptors::reverse(eq))
    {
      if (step.ignore)
        continue;
      run_on_step(step);
    }
    fine_timet algorithm_stop = current_time();
    log_status(
      "Slicing time: {}s (removed {} assignments)",
      time2string(algorithm_stop - algorithm_start),
      sliced);
    return true;
  }

  std::unordered_set<std::string> depends;

  std::unordered_set<const expr2t *> collected_cache;

  std::unordered_map<std::string, std::unordered_set<size_t>> index_reads;

  std::unordered_set<std::string> array_disqualified;

  std::unordered_set<const expr2t *> scanned_cache;
 
  static expr2tc get_nondet_symbol(const expr2tc &expr);
 
protected:
  const bool slice_assumes;
  const bool slice_nondet;

  void collect_dependencies(const expr2tc &expr);

  void scan_array_uses(const expr2tc &expr);

  bool depends_on_tracked(const expr2tc &expr);

  void run_on_assert(symex_target_equationt::SSA_stept &SSA_step) override;

  void run_on_assume(symex_target_equationt::SSA_stept &SSA_step) override;

  void run_on_assignment(symex_target_equationt::SSA_stept &SSA_step) override;

  void run_on_renumber(symex_target_equationt::SSA_stept &SSA_step) override;
};
 
#endif