refactor(control_tree): split StepTree facts vs contract boxes
This commit is contained in:
@ -3,11 +3,20 @@
|
|||||||
//! Policy:
|
//! Policy:
|
||||||
//! - This module must NOT reference MIR/JoinIR values (`ValueId`, `BlockId`, `PHI`, ...).
|
//! - This module must NOT reference MIR/JoinIR values (`ValueId`, `BlockId`, `PHI`, ...).
|
||||||
//! - It only describes AST control structure and derived features/capabilities.
|
//! - It only describes AST control structure and derived features/capabilities.
|
||||||
|
//!
|
||||||
|
//! Phase 120: Facts→Decision→Emit architecture
|
||||||
|
//! - step_tree_facts: Raw data collection (exits/writes/caps/cond_sig)
|
||||||
|
//! - step_tree_contract_box: Facts → Contract transformation
|
||||||
|
//! - step_tree: Structure + integration
|
||||||
|
|
||||||
mod step_tree;
|
mod step_tree;
|
||||||
|
mod step_tree_contract_box;
|
||||||
|
mod step_tree_facts;
|
||||||
|
|
||||||
pub use step_tree::{
|
pub use step_tree::{
|
||||||
AstSummary, ExitKind, StepCapability, StepNode, StepStmtKind, StepTree, StepTreeBuilderBox,
|
AstSummary, ExitKind, StepCapability, StepNode, StepStmtKind, StepTree, StepTreeBuilderBox,
|
||||||
StepTreeContract, StepTreeFeatures, StepTreeSignature,
|
StepTreeFeatures, StepTreeSignature,
|
||||||
};
|
};
|
||||||
|
pub use step_tree_contract_box::{StepTreeContract, StepTreeContractBox};
|
||||||
|
pub use step_tree_facts::StepTreeFacts;
|
||||||
|
|
||||||
|
|||||||
@ -1,4 +1,8 @@
|
|||||||
use crate::ast::{ASTNode, BinaryOperator, LiteralValue, Span, UnaryOperator};
|
use crate::ast::{ASTNode, BinaryOperator, LiteralValue, Span, UnaryOperator};
|
||||||
|
use crate::mir::control_tree::step_tree_contract_box::{
|
||||||
|
StepTreeContract, StepTreeContractBox,
|
||||||
|
};
|
||||||
|
use crate::mir::control_tree::step_tree_facts::StepTreeFacts;
|
||||||
|
|
||||||
use std::collections::BTreeSet;
|
use std::collections::BTreeSet;
|
||||||
|
|
||||||
@ -115,56 +119,7 @@ pub enum StepCapability {
|
|||||||
Arrow,
|
Arrow,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone, PartialEq, Default)]
|
// StepTreeContract moved to step_tree_contract_box.rs (Phase 120)
|
||||||
pub struct StepTreeContract {
|
|
||||||
pub exits: BTreeSet<ExitKind>,
|
|
||||||
pub writes: BTreeSet<String>,
|
|
||||||
pub required_caps: BTreeSet<StepCapability>,
|
|
||||||
pub cond_sig: Vec<String>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl StepTreeContract {
|
|
||||||
pub fn signature_basis_string(&self, node_kinds: &str) -> String {
|
|
||||||
let exits = self
|
|
||||||
.exits
|
|
||||||
.iter()
|
|
||||||
.map(|e| match e {
|
|
||||||
ExitKind::Return => "return",
|
|
||||||
ExitKind::Break => "break",
|
|
||||||
ExitKind::Continue => "continue",
|
|
||||||
})
|
|
||||||
.collect::<Vec<_>>()
|
|
||||||
.join(",");
|
|
||||||
let writes = self.writes.iter().cloned().collect::<Vec<_>>().join(",");
|
|
||||||
let caps = self
|
|
||||||
.required_caps
|
|
||||||
.iter()
|
|
||||||
.map(|c| match c {
|
|
||||||
StepCapability::If => "If",
|
|
||||||
StepCapability::Loop => "Loop",
|
|
||||||
StepCapability::NestedIf => "NestedIf",
|
|
||||||
StepCapability::NestedLoop => "NestedLoop",
|
|
||||||
StepCapability::Return => "Return",
|
|
||||||
StepCapability::Break => "Break",
|
|
||||||
StepCapability::Continue => "Continue",
|
|
||||||
StepCapability::TryCatch => "TryCatch",
|
|
||||||
StepCapability::Throw => "Throw",
|
|
||||||
StepCapability::Lambda => "Lambda",
|
|
||||||
StepCapability::While => "While",
|
|
||||||
StepCapability::ForRange => "ForRange",
|
|
||||||
StepCapability::Match => "Match",
|
|
||||||
StepCapability::Arrow => "Arrow",
|
|
||||||
})
|
|
||||||
.collect::<Vec<_>>()
|
|
||||||
.join(",");
|
|
||||||
let cond_sig = self.cond_sig.join("|");
|
|
||||||
|
|
||||||
format!(
|
|
||||||
"kinds={};exits={};writes={};caps={};conds={}",
|
|
||||||
node_kinds, exits, writes, caps, cond_sig
|
|
||||||
)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||||
pub struct StepTreeSignature(pub u64);
|
pub struct StepTreeSignature(pub u64);
|
||||||
@ -457,7 +412,9 @@ impl StepTreeBuilderBox {
|
|||||||
}
|
}
|
||||||
|
|
||||||
fn build_step_tree(root: StepNode, features: StepTreeFeatures) -> StepTree {
|
fn build_step_tree(root: StepNode, features: StepTreeFeatures) -> StepTree {
|
||||||
let contract = StepTreeContractBox::compute(&root, &features);
|
// Phase 120: Facts → Contract → Signature (separated concerns)
|
||||||
|
let facts = extract_facts_from_tree(&root, &features);
|
||||||
|
let contract = StepTreeContractBox::from_facts(&facts);
|
||||||
let mut kinds = Vec::new();
|
let mut kinds = Vec::new();
|
||||||
collect_node_kinds(&root, &mut kinds);
|
collect_node_kinds(&root, &mut kinds);
|
||||||
let kinds = kinds.join(",");
|
let kinds = kinds.join(",");
|
||||||
@ -472,6 +429,112 @@ fn build_step_tree(root: StepNode, features: StepTreeFeatures) -> StepTree {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Extract raw facts from StepNode tree (Phase 120)
|
||||||
|
fn extract_facts_from_tree(root: &StepNode, features: &StepTreeFeatures) -> StepTreeFacts {
|
||||||
|
let mut facts = StepTreeFacts::new();
|
||||||
|
|
||||||
|
// Required caps from features (structural only)
|
||||||
|
if features.has_if {
|
||||||
|
facts.add_capability(StepCapability::If);
|
||||||
|
}
|
||||||
|
if features.max_if_depth > 1 {
|
||||||
|
facts.add_capability(StepCapability::NestedIf);
|
||||||
|
}
|
||||||
|
if features.has_loop {
|
||||||
|
facts.add_capability(StepCapability::Loop);
|
||||||
|
}
|
||||||
|
if features.max_loop_depth > 1 {
|
||||||
|
facts.add_capability(StepCapability::NestedLoop);
|
||||||
|
}
|
||||||
|
if features.has_return {
|
||||||
|
facts.add_capability(StepCapability::Return);
|
||||||
|
}
|
||||||
|
if features.has_break {
|
||||||
|
facts.add_capability(StepCapability::Break);
|
||||||
|
}
|
||||||
|
if features.has_continue {
|
||||||
|
facts.add_capability(StepCapability::Continue);
|
||||||
|
}
|
||||||
|
|
||||||
|
walk_for_facts(root, &mut facts);
|
||||||
|
facts
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Walk StepNode tree to collect facts (Phase 120)
|
||||||
|
fn walk_for_facts(node: &StepNode, facts: &mut StepTreeFacts) {
|
||||||
|
match node {
|
||||||
|
StepNode::Block(nodes) => {
|
||||||
|
for n in nodes {
|
||||||
|
walk_for_facts(n, facts);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepNode::If {
|
||||||
|
cond,
|
||||||
|
then_branch,
|
||||||
|
else_branch,
|
||||||
|
..
|
||||||
|
} => {
|
||||||
|
facts.add_cond_sig(cond.to_compact_string());
|
||||||
|
walk_for_facts(then_branch, facts);
|
||||||
|
if let Some(else_branch) = else_branch {
|
||||||
|
walk_for_facts(else_branch, facts);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepNode::Loop { cond, body, .. } => {
|
||||||
|
facts.add_cond_sig(cond.to_compact_string());
|
||||||
|
walk_for_facts(body, facts);
|
||||||
|
}
|
||||||
|
StepNode::Stmt { kind, .. } => {
|
||||||
|
match kind {
|
||||||
|
StepStmtKind::LocalDecl { vars } => {
|
||||||
|
for v in vars {
|
||||||
|
facts.add_write(v.clone());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepStmtKind::Assign { target } => {
|
||||||
|
if let Some(name) = target.as_ref() {
|
||||||
|
facts.add_write(name.clone());
|
||||||
|
}
|
||||||
|
}
|
||||||
|
StepStmtKind::Print => {}
|
||||||
|
StepStmtKind::Return => {
|
||||||
|
facts.add_exit(ExitKind::Return);
|
||||||
|
}
|
||||||
|
StepStmtKind::Break => {
|
||||||
|
facts.add_exit(ExitKind::Break);
|
||||||
|
}
|
||||||
|
StepStmtKind::Continue => {
|
||||||
|
facts.add_exit(ExitKind::Continue);
|
||||||
|
}
|
||||||
|
StepStmtKind::Other(name) => match *name {
|
||||||
|
"TryCatch" => {
|
||||||
|
facts.add_capability(StepCapability::TryCatch);
|
||||||
|
}
|
||||||
|
"Throw" => {
|
||||||
|
facts.add_capability(StepCapability::Throw);
|
||||||
|
}
|
||||||
|
"Lambda" => {
|
||||||
|
facts.add_capability(StepCapability::Lambda);
|
||||||
|
}
|
||||||
|
"While" => {
|
||||||
|
facts.add_capability(StepCapability::While);
|
||||||
|
}
|
||||||
|
"ForRange" => {
|
||||||
|
facts.add_capability(StepCapability::ForRange);
|
||||||
|
}
|
||||||
|
"MatchExpr" => {
|
||||||
|
facts.add_capability(StepCapability::Match);
|
||||||
|
}
|
||||||
|
"Arrow" => {
|
||||||
|
facts.add_capability(StepCapability::Arrow);
|
||||||
|
}
|
||||||
|
_ => {}
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn merge_features(mut a: StepTreeFeatures, b: StepTreeFeatures) -> StepTreeFeatures {
|
fn merge_features(mut a: StepTreeFeatures, b: StepTreeFeatures) -> StepTreeFeatures {
|
||||||
a.has_if |= b.has_if;
|
a.has_if |= b.has_if;
|
||||||
a.has_loop |= b.has_loop;
|
a.has_loop |= b.has_loop;
|
||||||
@ -483,113 +546,8 @@ fn merge_features(mut a: StepTreeFeatures, b: StepTreeFeatures) -> StepTreeFeatu
|
|||||||
a
|
a
|
||||||
}
|
}
|
||||||
|
|
||||||
struct StepTreeContractBox;
|
// StepTreeContractBox moved to step_tree_contract_box.rs (Phase 120)
|
||||||
|
// extract_facts_from_tree + walk_for_facts replace the old compute/walk pattern
|
||||||
impl StepTreeContractBox {
|
|
||||||
fn compute(root: &StepNode, features: &StepTreeFeatures) -> StepTreeContract {
|
|
||||||
let mut contract = StepTreeContract::default();
|
|
||||||
|
|
||||||
// Required caps from features (structural only).
|
|
||||||
if features.has_if {
|
|
||||||
contract.required_caps.insert(StepCapability::If);
|
|
||||||
}
|
|
||||||
if features.max_if_depth > 1 {
|
|
||||||
contract.required_caps.insert(StepCapability::NestedIf);
|
|
||||||
}
|
|
||||||
if features.has_loop {
|
|
||||||
contract.required_caps.insert(StepCapability::Loop);
|
|
||||||
}
|
|
||||||
if features.max_loop_depth > 1 {
|
|
||||||
contract.required_caps.insert(StepCapability::NestedLoop);
|
|
||||||
}
|
|
||||||
if features.has_return {
|
|
||||||
contract.required_caps.insert(StepCapability::Return);
|
|
||||||
}
|
|
||||||
if features.has_break {
|
|
||||||
contract.required_caps.insert(StepCapability::Break);
|
|
||||||
}
|
|
||||||
if features.has_continue {
|
|
||||||
contract.required_caps.insert(StepCapability::Continue);
|
|
||||||
}
|
|
||||||
|
|
||||||
Self::walk(root, &mut contract);
|
|
||||||
contract
|
|
||||||
}
|
|
||||||
|
|
||||||
fn walk(node: &StepNode, contract: &mut StepTreeContract) {
|
|
||||||
match node {
|
|
||||||
StepNode::Block(nodes) => {
|
|
||||||
for n in nodes {
|
|
||||||
Self::walk(n, contract);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
StepNode::If {
|
|
||||||
cond,
|
|
||||||
then_branch,
|
|
||||||
else_branch,
|
|
||||||
..
|
|
||||||
} => {
|
|
||||||
contract.cond_sig.push(cond.to_compact_string());
|
|
||||||
Self::walk(then_branch, contract);
|
|
||||||
if let Some(else_branch) = else_branch {
|
|
||||||
Self::walk(else_branch, contract);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
StepNode::Loop { cond, body, .. } => {
|
|
||||||
contract.cond_sig.push(cond.to_compact_string());
|
|
||||||
Self::walk(body, contract);
|
|
||||||
}
|
|
||||||
StepNode::Stmt { kind, .. } => {
|
|
||||||
match kind {
|
|
||||||
StepStmtKind::LocalDecl { vars } => {
|
|
||||||
for v in vars {
|
|
||||||
contract.writes.insert(v.clone());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
StepStmtKind::Assign { target } => {
|
|
||||||
if let Some(name) = target.as_ref() {
|
|
||||||
contract.writes.insert(name.clone());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
StepStmtKind::Print => {}
|
|
||||||
StepStmtKind::Return => {
|
|
||||||
contract.exits.insert(ExitKind::Return);
|
|
||||||
}
|
|
||||||
StepStmtKind::Break => {
|
|
||||||
contract.exits.insert(ExitKind::Break);
|
|
||||||
}
|
|
||||||
StepStmtKind::Continue => {
|
|
||||||
contract.exits.insert(ExitKind::Continue);
|
|
||||||
}
|
|
||||||
StepStmtKind::Other(name) => match *name {
|
|
||||||
"TryCatch" => {
|
|
||||||
contract.required_caps.insert(StepCapability::TryCatch);
|
|
||||||
}
|
|
||||||
"Throw" => {
|
|
||||||
contract.required_caps.insert(StepCapability::Throw);
|
|
||||||
}
|
|
||||||
"Lambda" => {
|
|
||||||
contract.required_caps.insert(StepCapability::Lambda);
|
|
||||||
}
|
|
||||||
"While" => {
|
|
||||||
contract.required_caps.insert(StepCapability::While);
|
|
||||||
}
|
|
||||||
"ForRange" => {
|
|
||||||
contract.required_caps.insert(StepCapability::ForRange);
|
|
||||||
}
|
|
||||||
"MatchExpr" => {
|
|
||||||
contract.required_caps.insert(StepCapability::Match);
|
|
||||||
}
|
|
||||||
"Arrow" => {
|
|
||||||
contract.required_caps.insert(StepCapability::Arrow);
|
|
||||||
}
|
|
||||||
_ => {}
|
|
||||||
},
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn collect_node_kinds(node: &StepNode, out: &mut Vec<String>) {
|
fn collect_node_kinds(node: &StepNode, out: &mut Vec<String>) {
|
||||||
match node {
|
match node {
|
||||||
|
|||||||
133
src/mir/control_tree/step_tree_contract_box.rs
Normal file
133
src/mir/control_tree/step_tree_contract_box.rs
Normal file
@ -0,0 +1,133 @@
|
|||||||
|
//! StepTreeContractBox - facts → contract transformation (Phase 120)
|
||||||
|
//!
|
||||||
|
//! Responsibility:
|
||||||
|
//! - Transform StepTreeFacts into StepTreeContract
|
||||||
|
//! - Format facts into contract structure
|
||||||
|
//! - NO decision-making - just data transformation
|
||||||
|
//! - Maintain determinism (BTreeSet/BTreeMap order)
|
||||||
|
//!
|
||||||
|
//! Design:
|
||||||
|
//! - Pure transformation: facts → contract (idempotent)
|
||||||
|
//! - No AST traversal, no interpretation
|
||||||
|
//! - Contract is the formatted representation of facts
|
||||||
|
|
||||||
|
use crate::mir::control_tree::step_tree_facts::StepTreeFacts;
|
||||||
|
use crate::mir::control_tree::{ExitKind, StepCapability};
|
||||||
|
use std::collections::BTreeSet;
|
||||||
|
|
||||||
|
/// Structured contract derived from facts (formatted, stable representation)
|
||||||
|
#[derive(Debug, Clone, PartialEq, Default)]
|
||||||
|
pub struct StepTreeContract {
|
||||||
|
pub exits: BTreeSet<ExitKind>,
|
||||||
|
pub writes: BTreeSet<String>,
|
||||||
|
pub required_caps: BTreeSet<StepCapability>,
|
||||||
|
pub cond_sig: Vec<String>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl StepTreeContract {
|
||||||
|
/// Generate signature basis string (stable representation for hashing)
|
||||||
|
///
|
||||||
|
/// This is used for StepTreeSignature computation.
|
||||||
|
/// Format: "kinds=...;exits=...;writes=...;caps=...;conds=..."
|
||||||
|
///
|
||||||
|
/// Invariants:
|
||||||
|
/// - Span is NOT included (determinism)
|
||||||
|
/// - BTreeSet iteration order is stable
|
||||||
|
/// - cond_sig order is preserved from traversal
|
||||||
|
pub fn signature_basis_string(&self, node_kinds: &str) -> String {
|
||||||
|
let exits = self
|
||||||
|
.exits
|
||||||
|
.iter()
|
||||||
|
.map(|e| match e {
|
||||||
|
ExitKind::Return => "return",
|
||||||
|
ExitKind::Break => "break",
|
||||||
|
ExitKind::Continue => "continue",
|
||||||
|
})
|
||||||
|
.collect::<Vec<_>>()
|
||||||
|
.join(",");
|
||||||
|
let writes = self.writes.iter().cloned().collect::<Vec<_>>().join(",");
|
||||||
|
let caps = self
|
||||||
|
.required_caps
|
||||||
|
.iter()
|
||||||
|
.map(|c| match c {
|
||||||
|
StepCapability::If => "If",
|
||||||
|
StepCapability::Loop => "Loop",
|
||||||
|
StepCapability::NestedIf => "NestedIf",
|
||||||
|
StepCapability::NestedLoop => "NestedLoop",
|
||||||
|
StepCapability::Return => "Return",
|
||||||
|
StepCapability::Break => "Break",
|
||||||
|
StepCapability::Continue => "Continue",
|
||||||
|
StepCapability::TryCatch => "TryCatch",
|
||||||
|
StepCapability::Throw => "Throw",
|
||||||
|
StepCapability::Lambda => "Lambda",
|
||||||
|
StepCapability::While => "While",
|
||||||
|
StepCapability::ForRange => "ForRange",
|
||||||
|
StepCapability::Match => "Match",
|
||||||
|
StepCapability::Arrow => "Arrow",
|
||||||
|
})
|
||||||
|
.collect::<Vec<_>>()
|
||||||
|
.join(",");
|
||||||
|
let cond_sig = self.cond_sig.join("|");
|
||||||
|
|
||||||
|
format!(
|
||||||
|
"kinds={};exits={};writes={};caps={};conds={}",
|
||||||
|
node_kinds, exits, writes, caps, cond_sig
|
||||||
|
)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// StepTreeContractBox - pure transformation from facts to contract
|
||||||
|
pub struct StepTreeContractBox;
|
||||||
|
|
||||||
|
impl StepTreeContractBox {
|
||||||
|
/// Transform facts into contract (idempotent, deterministic)
|
||||||
|
///
|
||||||
|
/// This is a pure transformation:
|
||||||
|
/// - No decision-making
|
||||||
|
/// - No AST traversal
|
||||||
|
/// - Same facts → same contract (idempotent)
|
||||||
|
pub fn from_facts(facts: &StepTreeFacts) -> StepTreeContract {
|
||||||
|
StepTreeContract {
|
||||||
|
exits: facts.exits.clone(),
|
||||||
|
writes: facts.writes.clone(),
|
||||||
|
required_caps: facts.required_caps.clone(),
|
||||||
|
cond_sig: facts.cond_sig.clone(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#[cfg(test)]
|
||||||
|
mod tests {
|
||||||
|
use super::*;
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn from_facts_is_idempotent() {
|
||||||
|
let mut facts = StepTreeFacts::new();
|
||||||
|
facts.add_exit(ExitKind::Return);
|
||||||
|
facts.add_write("x".to_string());
|
||||||
|
facts.add_capability(StepCapability::If);
|
||||||
|
facts.add_cond_sig("var:cond".to_string());
|
||||||
|
|
||||||
|
let contract1 = StepTreeContractBox::from_facts(&facts);
|
||||||
|
let contract2 = StepTreeContractBox::from_facts(&facts);
|
||||||
|
|
||||||
|
assert_eq!(contract1, contract2);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn signature_basis_string_is_deterministic() {
|
||||||
|
let mut facts = StepTreeFacts::new();
|
||||||
|
// Add in different order
|
||||||
|
facts.add_write("z".to_string());
|
||||||
|
facts.add_write("a".to_string());
|
||||||
|
facts.add_write("m".to_string());
|
||||||
|
|
||||||
|
let contract = StepTreeContractBox::from_facts(&facts);
|
||||||
|
let basis1 = contract.signature_basis_string("Block");
|
||||||
|
let basis2 = contract.signature_basis_string("Block");
|
||||||
|
|
||||||
|
assert_eq!(basis1, basis2);
|
||||||
|
// BTreeSet should give stable order: a, m, z
|
||||||
|
assert!(basis1.contains("writes=a,m,z"));
|
||||||
|
}
|
||||||
|
}
|
||||||
63
src/mir/control_tree/step_tree_facts.rs
Normal file
63
src/mir/control_tree/step_tree_facts.rs
Normal file
@ -0,0 +1,63 @@
|
|||||||
|
//! StepTreeFacts - raw structural facts extraction (Phase 120)
|
||||||
|
//!
|
||||||
|
//! Responsibility:
|
||||||
|
//! - Collect raw structural facts from StepNode tree (exits/writes/required_caps/cond_sig)
|
||||||
|
//! - NO formatting, NO decision-making, NO signature generation
|
||||||
|
//! - Pure "facts only" - data collection without interpretation
|
||||||
|
//!
|
||||||
|
//! Design:
|
||||||
|
//! - Facts are collected during tree traversal
|
||||||
|
//! - BTreeSet for deterministic iteration (order stability)
|
||||||
|
//! - No dependency on contract or signature logic
|
||||||
|
|
||||||
|
use crate::mir::control_tree::{ExitKind, StepCapability};
|
||||||
|
use std::collections::BTreeSet;
|
||||||
|
|
||||||
|
/// Raw structural facts extracted from StepTree (facts only, no interpretation)
|
||||||
|
#[derive(Debug, Clone, PartialEq, Default)]
|
||||||
|
pub struct StepTreeFacts {
|
||||||
|
/// Exit kinds found in the tree (return/break/continue)
|
||||||
|
pub exits: BTreeSet<ExitKind>,
|
||||||
|
/// Variable writes (Local declarations + Assignment targets)
|
||||||
|
pub writes: BTreeSet<String>,
|
||||||
|
/// Required capabilities (structural features like NestedLoop, TryCatch, etc.)
|
||||||
|
pub required_caps: BTreeSet<StepCapability>,
|
||||||
|
/// Condition signatures (compact string representations of if/loop conditions)
|
||||||
|
/// - Collected in traversal order for signature stability
|
||||||
|
pub cond_sig: Vec<String>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl StepTreeFacts {
|
||||||
|
/// Create empty facts
|
||||||
|
pub fn new() -> Self {
|
||||||
|
Self::default()
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Add an exit kind
|
||||||
|
pub fn add_exit(&mut self, kind: ExitKind) {
|
||||||
|
self.exits.insert(kind);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Add a variable write
|
||||||
|
pub fn add_write(&mut self, var: String) {
|
||||||
|
self.writes.insert(var);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Add a required capability
|
||||||
|
pub fn add_capability(&mut self, cap: StepCapability) {
|
||||||
|
self.required_caps.insert(cap);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Add a condition signature
|
||||||
|
pub fn add_cond_sig(&mut self, sig: String) {
|
||||||
|
self.cond_sig.push(sig);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Merge another facts into this one
|
||||||
|
pub fn merge(&mut self, other: StepTreeFacts) {
|
||||||
|
self.exits.extend(other.exits);
|
||||||
|
self.writes.extend(other.writes);
|
||||||
|
self.required_caps.extend(other.required_caps);
|
||||||
|
self.cond_sig.extend(other.cond_sig);
|
||||||
|
}
|
||||||
|
}
|
||||||
Reference in New Issue
Block a user