|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Basic Blocks Detection for Goto Programs |
| 4 | +
|
| 5 | +Author: Refactored from cover_basic_blocks.h |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +/// \file |
| 10 | +/// Generic basic block detection for goto programs |
| 11 | +/// |
| 12 | +/// This module provides a generic basic block detection utility that can |
| 13 | +/// be used across different parts of the codebase. It supports pluggable |
| 14 | +/// strategies for language-specific behavior and configurable options for |
| 15 | +/// how basic blocks are detected (e.g., whether assume statements delimit |
| 16 | +/// blocks). |
| 17 | + |
| 18 | +#ifndef CPROVER_ANALYSES_BASIC_BLOCKS_H |
| 19 | +#define CPROVER_ANALYSES_BASIC_BLOCKS_H |
| 20 | + |
| 21 | +#include <util/irep.h> |
| 22 | + |
| 23 | +#include <goto-programs/goto_program.h> |
| 24 | + |
| 25 | +#include <map> |
| 26 | +#include <memory> |
| 27 | +#include <optional> |
| 28 | +#include <set> |
| 29 | +#include <vector> |
| 30 | + |
| 31 | +class source_locationt; |
| 32 | + |
| 33 | +/// Configuration options for basic block detection |
| 34 | +struct basic_block_configt |
| 35 | +{ |
| 36 | + /// If true, assume statements delimit basic blocks |
| 37 | + /// (i.e., assumptions terminate blocks as subsequent instructions may be |
| 38 | + /// unreachable). However, multiple consecutive assumes with the same source |
| 39 | + /// location are treated as part of the same block. |
| 40 | + bool assume_delimit_blocks = true; |
| 41 | + |
| 42 | + basic_block_configt() = default; |
| 43 | + explicit basic_block_configt(bool _assume_delimit_blocks) |
| 44 | + : assume_delimit_blocks(_assume_delimit_blocks) |
| 45 | + { |
| 46 | + } |
| 47 | +}; |
| 48 | + |
| 49 | +/// Abstract policy interface for language-specific basic block detection |
| 50 | +/// behavior. This enables different detection strategies for different |
| 51 | +/// languages (e.g., Java bytecode uses java_bytecode_index for blocks) |
| 52 | +template <class P, class T> |
| 53 | +class basic_block_policy_baset |
| 54 | +{ |
| 55 | +public: |
| 56 | + virtual ~basic_block_policy_baset() = default; |
| 57 | + |
| 58 | + /// Information about a basic block |
| 59 | + struct block_infot |
| 60 | + { |
| 61 | + /// Program location representative of this block (for instrumentation) |
| 62 | + std::optional<T> representative_inst; |
| 63 | + /// Source location representative of this block |
| 64 | + source_locationt source_location; |
| 65 | + /// Additional policy-specific data can be stored in derived classes |
| 66 | + }; |
| 67 | + |
| 68 | + /// Compute basic blocks for the given program |
| 69 | + /// \param program: The goto program to analyze |
| 70 | + /// \param config: Configuration options for block detection |
| 71 | + virtual void |
| 72 | + compute_blocks(const P &program, const basic_block_configt &config) = 0; |
| 73 | + |
| 74 | + /// Get the block number for a given instruction |
| 75 | + /// \param t: An instruction in the program |
| 76 | + /// \return The block number containing this instruction |
| 77 | + virtual std::size_t block_of(T t) const = 0; |
| 78 | + |
| 79 | + /// Get the representative instruction for a block |
| 80 | + /// \param block_nr: Block number |
| 81 | + /// \return The representative instruction, or empty if none |
| 82 | + virtual std::optional<T> instruction_of(std::size_t block_nr) const = 0; |
| 83 | + |
| 84 | + /// Get the source location for a block |
| 85 | + /// \param block_nr: Block number |
| 86 | + /// \return Reference to the source location |
| 87 | + virtual const source_locationt & |
| 88 | + source_location_of(std::size_t block_nr) const = 0; |
| 89 | + |
| 90 | + /// Get the number of blocks detected |
| 91 | + virtual std::size_t size() const = 0; |
| 92 | +}; |
| 93 | + |
| 94 | +/// Default basic block detection policy for C/C++ |
| 95 | +/// This implements standard control-flow-based basic block detection |
| 96 | +template <class P, class T, typename C> |
| 97 | +class default_basic_block_policyt : public basic_block_policy_baset<P, T> |
| 98 | +{ |
| 99 | +public: |
| 100 | + using block_infot = typename basic_block_policy_baset<P, T>::block_infot; |
| 101 | + |
| 102 | + void |
| 103 | + compute_blocks(const P &program, const basic_block_configt &config) override; |
| 104 | + std::size_t block_of(T t) const override; |
| 105 | + std::optional<T> instruction_of(std::size_t block_nr) const override; |
| 106 | + const source_locationt & |
| 107 | + source_location_of(std::size_t block_nr) const override; |
| 108 | + std::size_t size() const override |
| 109 | + { |
| 110 | + return block_infos.size(); |
| 111 | + } |
| 112 | + |
| 113 | +protected: |
| 114 | + using block_mapt = std::map<T, std::size_t, C>; |
| 115 | + |
| 116 | + /// Map program locations to block numbers |
| 117 | + block_mapt block_map; |
| 118 | + /// Information about each block |
| 119 | + std::vector<block_infot> block_infos; |
| 120 | + |
| 121 | + /// Check if instruction is a continuation of a previous block through |
| 122 | + /// unconditional forward gotos |
| 123 | + static std::optional<std::size_t> |
| 124 | + continuation_of_block(T instruction, block_mapt &block_map); |
| 125 | +}; |
| 126 | + |
| 127 | +/// Java-specific basic block detection policy |
| 128 | +/// Uses Java bytecode index to determine blocks |
| 129 | +template <class P, class T, typename C> |
| 130 | +class java_basic_block_policyt : public basic_block_policy_baset<P, T> |
| 131 | +{ |
| 132 | +public: |
| 133 | + using block_infot = typename basic_block_policy_baset<P, T>::block_infot; |
| 134 | + |
| 135 | + void |
| 136 | + compute_blocks(const P &program, const basic_block_configt &config) override; |
| 137 | + std::size_t block_of(T t) const override; |
| 138 | + std::optional<T> instruction_of(std::size_t block_nr) const override; |
| 139 | + const source_locationt & |
| 140 | + source_location_of(std::size_t block_nr) const override; |
| 141 | + std::size_t size() const override |
| 142 | + { |
| 143 | + return block_infos.size(); |
| 144 | + } |
| 145 | + |
| 146 | +protected: |
| 147 | + /// Information about each block (indexed by block number) |
| 148 | + std::vector<block_infot> block_infos; |
| 149 | + /// Map Java bytecode index to block number |
| 150 | + std::unordered_map<irep_idt, std::size_t> index_to_block; |
| 151 | +}; |
| 152 | + |
| 153 | +/// Main template for basic block detection |
| 154 | +/// Similar to natural_loops_templatet, this provides a generic interface |
| 155 | +/// for detecting basic blocks in goto programs with pluggable policies. |
| 156 | +/// |
| 157 | +/// \tparam P: Program type (e.g., goto_programt) |
| 158 | +/// \tparam T: Iterator type (e.g., goto_programt::const_targett) |
| 159 | +/// \tparam C: Comparison functor for iterators |
| 160 | +template <class P, class T, typename C> |
| 161 | +class basic_blocks_templatet |
| 162 | +{ |
| 163 | +public: |
| 164 | + /// Create a basic block detector with default policy |
| 165 | + basic_blocks_templatet() |
| 166 | + : policy(std::make_unique<default_basic_block_policyt<P, T, C>>()), config() |
| 167 | + { |
| 168 | + } |
| 169 | + |
| 170 | + /// Create with a specific configuration |
| 171 | + explicit basic_blocks_templatet(const basic_block_configt &_config) |
| 172 | + : policy(std::make_unique<default_basic_block_policyt<P, T, C>>()), |
| 173 | + config(_config) |
| 174 | + { |
| 175 | + } |
| 176 | + |
| 177 | + /// Create with a custom policy |
| 178 | + explicit basic_blocks_templatet( |
| 179 | + std::unique_ptr<basic_block_policy_baset<P, T>> _policy) |
| 180 | + : policy(std::move(_policy)), config() |
| 181 | + { |
| 182 | + } |
| 183 | + |
| 184 | + /// Create with custom policy and configuration |
| 185 | + basic_blocks_templatet( |
| 186 | + std::unique_ptr<basic_block_policy_baset<P, T>> _policy, |
| 187 | + const basic_block_configt &_config) |
| 188 | + : policy(std::move(_policy)), config(_config) |
| 189 | + { |
| 190 | + } |
| 191 | + |
| 192 | + /// Compute basic blocks for a program |
| 193 | + /// \param program: The goto program to analyze |
| 194 | + void operator()(const P &program) |
| 195 | + { |
| 196 | + compute(program); |
| 197 | + } |
| 198 | + |
| 199 | + /// Compute basic blocks for a program |
| 200 | + /// \param program: The goto program to analyze |
| 201 | + void compute(const P &program) |
| 202 | + { |
| 203 | + PRECONDITION(policy); |
| 204 | + policy->compute_blocks(program, config); |
| 205 | + } |
| 206 | + |
| 207 | + /// Get the block number for a given instruction |
| 208 | + std::size_t block_of(T t) const |
| 209 | + { |
| 210 | + PRECONDITION(policy); |
| 211 | + return policy->block_of(t); |
| 212 | + } |
| 213 | + |
| 214 | + /// Get the representative instruction for a block |
| 215 | + std::optional<T> instruction_of(std::size_t block_nr) const |
| 216 | + { |
| 217 | + PRECONDITION(policy); |
| 218 | + return policy->instruction_of(block_nr); |
| 219 | + } |
| 220 | + |
| 221 | + /// Get the source location for a block |
| 222 | + const source_locationt &source_location_of(std::size_t block_nr) const |
| 223 | + { |
| 224 | + PRECONDITION(policy); |
| 225 | + return policy->source_location_of(block_nr); |
| 226 | + } |
| 227 | + |
| 228 | + /// Get the number of blocks detected |
| 229 | + std::size_t size() const |
| 230 | + { |
| 231 | + PRECONDITION(policy); |
| 232 | + return policy->size(); |
| 233 | + } |
| 234 | + |
| 235 | + /// Get the configuration |
| 236 | + const basic_block_configt &get_config() const |
| 237 | + { |
| 238 | + return config; |
| 239 | + } |
| 240 | + |
| 241 | + /// Set the configuration |
| 242 | + void set_config(const basic_block_configt &_config) |
| 243 | + { |
| 244 | + config = _config; |
| 245 | + } |
| 246 | + |
| 247 | +protected: |
| 248 | + std::unique_ptr<basic_block_policy_baset<P, T>> policy; |
| 249 | + basic_block_configt config; |
| 250 | +}; |
| 251 | + |
| 252 | +/// Concrete type for basic block detection on const goto programs |
| 253 | +using basic_blockst = basic_blocks_templatet< |
| 254 | + const goto_programt, |
| 255 | + goto_programt::const_targett, |
| 256 | + goto_programt::target_less_than>; |
| 257 | + |
| 258 | +/// Concrete type for basic block detection on mutable goto programs |
| 259 | +using basic_blocks_mutablet = basic_blocks_templatet< |
| 260 | + goto_programt, |
| 261 | + goto_programt::targett, |
| 262 | + goto_programt::target_less_than>; |
| 263 | + |
| 264 | +// Include template implementations |
| 265 | +#include "basic_blocks_impl.h" |
| 266 | + |
| 267 | +#endif // CPROVER_ANALYSES_BASIC_BLOCKS_H |
0 commit comments