Refactor basic block detection into standalone utility module

src/analyses/basic_blocks.h

@@ -0,0 +1,267 @@
+/*******************************************************************\
+
+Module: Basic Blocks Detection for Goto Programs
+
+Author: Refactored from cover_basic_blocks.h
+
+\*******************************************************************/
+
+/// \file
+/// Generic basic block detection for goto programs
+///
+/// This module provides a generic basic block detection utility that can
+/// be used across different parts of the codebase. It supports pluggable
+/// strategies for language-specific behavior and configurable options for
+/// how basic blocks are detected (e.g., whether assume statements delimit
+/// blocks).
+
+#ifndef CPROVER_ANALYSES_BASIC_BLOCKS_H
+#define CPROVER_ANALYSES_BASIC_BLOCKS_H
+
+#include <util/irep.h>
+
+#include <goto-programs/goto_program.h>
+
+#include <map>
+#include <memory>
+#include <optional>
+#include <set>
+#include <vector>
+
+class source_locationt;
+
+/// Configuration options for basic block detection
+struct basic_block_configt
+{
+  /// If true, assume statements delimit basic blocks
+  /// (i.e., assumptions terminate blocks as subsequent instructions may be
+  /// unreachable). However, multiple consecutive assumes with the same source
+  /// location are treated as part of the same block.
+  bool assume_delimit_blocks = true;
+
+  basic_block_configt() = default;
+  explicit basic_block_configt(bool _assume_delimit_blocks)
+    : assume_delimit_blocks(_assume_delimit_blocks)
+  {
+  }
+};
+
+/// Abstract policy interface for language-specific basic block detection
+/// behavior. This enables different detection strategies for different
+/// languages (e.g., Java bytecode uses java_bytecode_index for blocks)
+template <class P, class T>
+class basic_block_policy_baset
+{
+public:
+  virtual ~basic_block_policy_baset() = default;
+
+  /// Information about a basic block
+  struct block_infot
+  {
+    /// Program location representative of this block (for instrumentation)
+    std::optional<T> representative_inst;
+    /// Source location representative of this block
+    source_locationt source_location;
+    /// Additional policy-specific data can be stored in derived classes
+  };
+
+  /// Compute basic blocks for the given program
+  /// \param program: The goto program to analyze
+  /// \param config: Configuration options for block detection
+  virtual void
+  compute_blocks(const P &program, const basic_block_configt &config) = 0;
+
+  /// Get the block number for a given instruction
+  /// \param t: An instruction in the program
+  /// \return The block number containing this instruction
+  virtual std::size_t block_of(T t) const = 0;
+
+  /// Get the representative instruction for a block
+  /// \param block_nr: Block number
+  /// \return The representative instruction, or empty if none
+  virtual std::optional<T> instruction_of(std::size_t block_nr) const = 0;
+
+  /// Get the source location for a block
+  /// \param block_nr: Block number
+  /// \return Reference to the source location
+  virtual const source_locationt &
+  source_location_of(std::size_t block_nr) const = 0;
+
+  /// Get the number of blocks detected
+  virtual std::size_t size() const = 0;
+};
+
+/// Default basic block detection policy for C/C++
+/// This implements standard control-flow-based basic block detection
+template <class P, class T, typename C>
+class default_basic_block_policyt : public basic_block_policy_baset<P, T>
+{
+public:
+  using block_infot = typename basic_block_policy_baset<P, T>::block_infot;
+
+  void
+  compute_blocks(const P &program, const basic_block_configt &config) override;
+  std::size_t block_of(T t) const override;
+  std::optional<T> instruction_of(std::size_t block_nr) const override;
+  const source_locationt &
+  source_location_of(std::size_t block_nr) const override;
+  std::size_t size() const override
+  {
+    return block_infos.size();
+  }
+
+protected:
+  using block_mapt = std::map<T, std::size_t, C>;
+
+  /// Map program locations to block numbers
+  block_mapt block_map;
+  /// Information about each block
+  std::vector<block_infot> block_infos;
+
+  /// Check if instruction is a continuation of a previous block through
+  /// unconditional forward gotos
+  static std::optional<std::size_t>
+  continuation_of_block(T instruction, block_mapt &block_map);
+};
+
+/// Java-specific basic block detection policy
+/// Uses Java bytecode index to determine blocks
+template <class P, class T, typename C>
+class java_basic_block_policyt : public basic_block_policy_baset<P, T>
+{
+public:
+  using block_infot = typename basic_block_policy_baset<P, T>::block_infot;
+
+  void
+  compute_blocks(const P &program, const basic_block_configt &config) override;
+  std::size_t block_of(T t) const override;
+  std::optional<T> instruction_of(std::size_t block_nr) const override;
+  const source_locationt &
+  source_location_of(std::size_t block_nr) const override;
+  std::size_t size() const override
+  {
+    return block_infos.size();
+  }
+
+protected:
+  /// Information about each block (indexed by block number)
+  std::vector<block_infot> block_infos;
+  /// Map Java bytecode index to block number
+  std::unordered_map<irep_idt, std::size_t> index_to_block;
+};
+
+/// Main template for basic block detection
+/// Similar to natural_loops_templatet, this provides a generic interface
+/// for detecting basic blocks in goto programs with pluggable policies.
+///
+/// \tparam P: Program type (e.g., goto_programt)
+/// \tparam T: Iterator type (e.g., goto_programt::const_targett)
+/// \tparam C: Comparison functor for iterators
+template <class P, class T, typename C>
+class basic_blocks_templatet
+{
+public:
+  /// Create a basic block detector with default policy
+  basic_blocks_templatet()
+    : policy(std::make_unique<default_basic_block_policyt<P, T, C>>()), config()
+  {
+  }
+
+  /// Create with a specific configuration
+  explicit basic_blocks_templatet(const basic_block_configt &_config)
+    : policy(std::make_unique<default_basic_block_policyt<P, T, C>>()),
+      config(_config)
+  {
+  }
+
+  /// Create with a custom policy
+  explicit basic_blocks_templatet(
+    std::unique_ptr<basic_block_policy_baset<P, T>> _policy)
+    : policy(std::move(_policy)), config()
+  {
+  }
+
+  /// Create with custom policy and configuration
+  basic_blocks_templatet(
+    std::unique_ptr<basic_block_policy_baset<P, T>> _policy,
+    const basic_block_configt &_config)
+    : policy(std::move(_policy)), config(_config)
+  {
+  }
+
+  /// Compute basic blocks for a program
+  /// \param program: The goto program to analyze
+  void operator()(const P &program)
+  {
+    compute(program);
+  }
+
+  /// Compute basic blocks for a program
+  /// \param program: The goto program to analyze
+  void compute(const P &program)
+  {
+    PRECONDITION(policy);
+    policy->compute_blocks(program, config);
+  }
+
+  /// Get the block number for a given instruction
+  std::size_t block_of(T t) const
+  {
+    PRECONDITION(policy);
+    return policy->block_of(t);
+  }
+
+  /// Get the representative instruction for a block
+  std::optional<T> instruction_of(std::size_t block_nr) const
+  {
+    PRECONDITION(policy);
+    return policy->instruction_of(block_nr);
+  }
+
+  /// Get the source location for a block
+  const source_locationt &source_location_of(std::size_t block_nr) const
+  {
+    PRECONDITION(policy);
+    return policy->source_location_of(block_nr);
+  }
+
+  /// Get the number of blocks detected
+  std::size_t size() const
+  {
+    PRECONDITION(policy);
+    return policy->size();
+  }
+
+  /// Get the configuration
+  const basic_block_configt &get_config() const
+  {
+    return config;
+  }
+
+  /// Set the configuration
+  void set_config(const basic_block_configt &_config)
+  {
+    config = _config;
+  }
+
+protected:
+  std::unique_ptr<basic_block_policy_baset<P, T>> policy;
+  basic_block_configt config;
+};
+
+/// Concrete type for basic block detection on const goto programs
+using basic_blockst = basic_blocks_templatet<
+  const goto_programt,
+  goto_programt::const_targett,
+  goto_programt::target_less_than>;
+
+/// Concrete type for basic block detection on mutable goto programs
+using basic_blocks_mutablet = basic_blocks_templatet<
+  goto_programt,
+  goto_programt::targett,
+  goto_programt::target_less_than>;
+
+// Include template implementations
+#include "basic_blocks_impl.h"
+
+#endif // CPROVER_ANALYSES_BASIC_BLOCKS_H