Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions crates/perry-codegen/src/collectors/hir_facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,13 @@ pub(crate) struct RepresentationFacts {
/// proof as `loop_bounded_i32_locals`, weaker conclusion — it changes no
/// storage decision, only an FMF flag. See `collectors/loop_bounded_i32.rs`.
pub reassociable_f64_accumulators: HashSet<u32>,
/// The intervals and integer constants behind `loop_bounded_i32_locals`,
/// for a consumer that needs the numbers rather than the verdict:
/// `concat_site_cache.rs` gives a `"literal" + value` site a per-site
/// table only when the value is proven small. Runs independently of the
/// canonical-i32 gate for the same reason as
/// `reassociable_f64_accumulators`: it is not a storage decision.
pub loop_induction: super::loop_bounded_i32::LoopInductionFacts,
/// Locals whose canonical-i32 promotion is PROVABLE but not PROFITABLE
/// (#7128): written after declaration, no i32-consuming read anywhere in
/// the body, and at least one double-consuming read inside a loop — so the
Expand Down Expand Up @@ -234,6 +241,10 @@ impl TypeFacts {
&self.representation.reassociable_f64_accumulators
}

pub(crate) fn loop_induction(&self) -> &super::loop_bounded_i32::LoopInductionFacts {
&self.representation.loop_induction
}

pub(crate) fn unprofitable_canonical_i32_locals(&self) -> &HashSet<u32> {
&self.representation.unprofitable_canonical_i32_locals
}
Expand Down Expand Up @@ -559,6 +570,8 @@ pub(crate) fn collect_type_facts(
stmts,
compile_time_constants,
);
let loop_induction =
super::loop_bounded_i32::collect_loop_induction_facts(stmts, compile_time_constants);
// #7123: this set now includes accumulators whose integer-ness and full
// range were proved together (for example `sum += i % 1000`). The older
// integer provenance collector deliberately does not accept bare `%`, so
Expand Down Expand Up @@ -735,6 +748,7 @@ pub(crate) fn collect_type_facts(
int_valued_ta_locals,
loop_bounded_i32_locals,
reassociable_f64_accumulators,
loop_induction,
unprofitable_canonical_i32_locals,
number_by_construction_locals,
},
Expand Down
65 changes: 52 additions & 13 deletions crates/perry-codegen/src/collectors/loop_bounded_i32.rs
Original file line number Diff line number Diff line change
Expand Up @@ -105,10 +105,11 @@ struct GuardedLevel {
extreme: i64,
}

/// A closed integer interval a local is proven never to leave.
#[derive(Clone, Copy, Debug)]
struct IntInterval {
lo: i64,
hi: i64,
pub(crate) struct IntInterval {
pub(crate) lo: i64,
pub(crate) hi: i64,
}

/// Analysis state, accumulated over one whole function body.
Expand Down Expand Up @@ -216,6 +217,48 @@ pub fn collect_reassociable_f64_accumulators(
stmts: &[Stmt],
compile_time_constants: &HashMap<u32, f64>,
) -> HashSet<u32> {
let st = analysed_state(stmts, compile_time_constants);
let induction_intervals = induction_intervals(&st);
collect_bounded_accumulator_locals(
stmts,
&st,
&induction_intervals,
AccumulatorMode::ReassocF64,
)
}

/// What the induction proof knows about integer values, for a consumer that
/// needs the numbers rather than the i32 verdict: `concat_site_cache.rs`
/// gives a `"literal" + value` site a per-site table only when the value is
/// proven small, because the table's inline gate is pure cost on a value
/// that sweeps past it.
#[derive(Clone, Debug, Default)]
pub(crate) struct LoopInductionFacts {
/// Every admissible counter's closed interval, both endpoints in i32.
pub(crate) intervals: HashMap<u32, IntInterval>,
/// Locals that are integer constants: module-level compile-time
/// constants plus this body's never-written `const`/`let` bindings with
/// an integer-literal initialiser — the same set the loop guard `v < B`
/// accepts as `B`.
pub(crate) integer_constants: HashMap<u32, i64>,
}

pub fn collect_loop_induction_facts(
stmts: &[Stmt],
compile_time_constants: &HashMap<u32, f64>,
) -> LoopInductionFacts {
let st = analysed_state(stmts, compile_time_constants);
let intervals = induction_intervals(&st);
let mut integer_constants = st.module_consts.clone();
integer_constants.extend(st.const_ints.iter().map(|(&id, &v)| (id, v)));
LoopInductionFacts {
intervals,
integer_constants,
}
}

/// Run the whole-function walk once; both interval consumers start here.
fn analysed_state(stmts: &[Stmt], compile_time_constants: &HashMap<u32, f64>) -> State {
let mut st = State::default();
st.module_consts = compile_time_constants
.iter()
Expand All @@ -228,9 +271,12 @@ pub fn collect_reassociable_f64_accumulators(
collect_const_ints(stmts, &mut st);
let empty: HashMap<u32, GuardedLevel> = HashMap::new();
walk_stmts(stmts, &empty, &mut st);
st
}

let induction_intervals: HashMap<u32, IntInterval> = st
.bounds
/// Every admissible local's closed interval, both endpoints inside i32.
fn induction_intervals(st: &State) -> HashMap<u32, IntInterval> {
st.bounds
.iter()
.filter_map(|(&id, bound)| {
if st.disqualified.contains(&id) || st.bad_decl.contains(&id) {
Expand All @@ -249,14 +295,7 @@ pub fn collect_reassociable_f64_accumulators(
};
(fits_i32(interval.lo) && fits_i32(interval.hi)).then_some((id, interval))
})
.collect();

collect_bounded_accumulator_locals(
stmts,
&st,
&induction_intervals,
AccumulatorMode::ReassocF64,
)
.collect()
}

fn fits_i32(n: i64) -> bool {
Expand Down
Loading
Loading