From ddc9ad5dc802f88cdfd24ae040d272746c128c6d Mon Sep 17 00:00:00 2001 From: KotlinIsland <65446343+kotlinisland@users.noreply.github.com> Date: Tue, 18 Aug 2026 10:42:07 +1000 Subject: [PATCH 1/2] The stop is where the code is, and a name that survives two dead branches now says what it holds MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two things a user found by running the debugger-seeded data flow against a seven-line function. ## nothing was decided until the stop reached the `if` Stopped on the first statement of a function body, the analysis answered nothing at all; one line lower it decided both branches. Driven live — `by run` with bpd, breakpoint on line 2 — bpd proved `qty` is 3 and `member` is False, the plugin sent both, and `by` returned `[]`. So the wire was fine and the fault was here. The stop offset was the first byte of the stop line, which is in the indentation. A statement's range begins at its first token, so `body_contains` — first statement's start to last statement's end — did not contain it, `stopped_scope` answered with the module instead of the function, and every seed was refused as being about another frame. Only a stop on a body's *first* statement can land in that gap, which is why one line further down worked and why this survived a suite. `stop_offset` is now the first non-indentation character of the line, and all three places that wanted the offset ask for it rather than each computing one. Widening the body to swallow its first line's indentation was the alternative and it loses on `def f(): return 1`, where the body's first statement shares the header's line and a stop there would stop being read as on the header. ## it did not say what a name would hold The other half of the same report: with both branches dead, `discount` is still the `0.0` line 2 assigned, and nothing said so. A read below the stop line now gets a `discount = 0.0` beside its line when the seeded reading pins it to one value and the unseeded reading does not. The value is the read's inferred type through `display_value`, the same rendering the enum inlay hint uses — not a second analysis, the same one asked a different question. That is what makes "only what follows from decided branches plus observed seeds" true by construction: anything unobserved is a union or an instance type, which is not one value, so it answers nothing and there is no "probably" available to invent. A container is excluded by the same fact rather than by a rule — `list[int]` is not a value, so a length that would go stale has nothing to report with. Note what does not carry it: bpd proves `discount` is a float `0.0` at the stop and the plugin drops it, because `by` has no float observation. The `0.0` comes from the file's own assignment surviving branches the seeds proved dead. The value is derived, not echoed. A read inside a condition this pass already decided gets nothing of its own — `qty >= 10` carries the `= false`, and `qty = 3` beside it is the working rather than the answer. It is also the one place two of these labels would compete for the same margin. --- crates/ty_ide/src/data_flow.rs | 237 +++++++++++++++++- crates/ty_python_semantic/src/assumed.rs | 102 +++++++- crates/ty_python_semantic/src/lib.rs | 1 + .../src/types/ide_support.rs | 2 +- .../src/types/ide_support/data_flow.rs | 110 +++++++- .../src/server/api/requests/data_flow.rs | 31 ++- crates/ty_server/tests/e2e/data_flow.rs | 64 +++++ 7 files changed, 519 insertions(+), 28 deletions(-) diff --git a/crates/ty_ide/src/data_flow.rs b/crates/ty_ide/src/data_flow.rs index 2bfc8a3d95..3d0b3bb2cc 100644 --- a/crates/ty_ide/src/data_flow.rs +++ b/crates/ty_ide/src/data_flow.rs @@ -13,6 +13,7 @@ use ruff_source_file::OneIndexed; use ruff_text_size::TextRange; use ty_python_core::assumptions::{Assumptions, Observation}; use ty_python_core::{ProgramFile, Truthiness}; +use ty_python_semantic::stop_offset; use ty_python_semantic::types::ide_support::{UnreachableRange, data_flow}; use crate::Db; @@ -27,7 +28,7 @@ pub struct Finding { } /// what kind of thing was settled -#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[derive(Debug, Clone, PartialEq, Eq)] pub enum FindingKind { /// this condition will go this way Condition { @@ -36,6 +37,13 @@ pub enum FindingKind { }, /// this code will not run Unreachable, + /// this read will find this value + Value { + /// the name being read, as the source spells it + name: String, + /// what it will hold, written the way a source writes it + value: String, + }, } impl Finding { @@ -43,11 +51,20 @@ impl Finding { /// /// short on purpose: it is drawn inline, in the editor font, beside code somebody is reading /// while stopped in a debugger - pub fn label(&self) -> &'static str { - match self.kind { - FindingKind::Condition { taken: true } => "= true", - FindingKind::Condition { taken: false } => "= false", - FindingKind::Unreachable => "will not run", + /// + /// a value's label names the name it is about — `discount = 0.0` — where a condition's does + /// not. that is not a style difference, it is where the label goes: a client draws these in the + /// margin past the end of the line, not against the expression, because an inlay there reflows + /// the code it is annotating. a `= false` in that margin is unambiguous when the line holds one + /// condition; a bare `= 0.0` past `total = base + discount` would be read as being about + /// `total`. the `a: 1` an IDE's own debugger draws was the alternative, and it loses for the + /// same reason — that hint is drawn *at* the variable, where the subject needs no naming + pub fn label(&self) -> String { + match &self.kind { + FindingKind::Condition { taken: true } => "= true".to_string(), + FindingKind::Condition { taken: false } => "= false".to_string(), + FindingKind::Unreachable => "will not run".to_string(), + FindingKind::Value { name, value } => format!("{name} = {value}"), } } } @@ -80,7 +97,11 @@ pub fn data_flow_at( }; let source = ruff_db::source::source_text(db, source_file); - let below = ruff_db::source::line_index(db, source_file).line_start(line, &source); + // asked for rather than computed here, so that the boundary deciding which findings are below + // the stop and the one deciding which seeds survive it are the one offset. they were computed + // separately once, agreed on every file anybody tried, and disagreed about a stop on the first + // statement of a function body — see [`ty_python_semantic::stop_offset`] + let below = stop_offset(db, source_file, line); let assumptions = Assumptions::new(db, source_file, stop_line, observations.into_boxed_slice()); let seeded = file.program(db).seeded(db, assumptions); @@ -105,13 +126,34 @@ pub fn data_flow_at( kind: FindingKind::Unreachable, }); - conditions.chain(unreachable).collect() + let values = flow.values.iter().filter_map(|read| { + let name = &source[read.range]; + // a read written across lines — `obj.\n attr` — has no one-line spelling, and a label + // with a newline in it cannot be drawn in a margin. dropping it loses a fact; drawing it + // would break the line the reader is looking at + if name.contains('\n') { + return None; + } + Some(Finding { + range: read.range, + kind: FindingKind::Value { + name: name.to_string(), + value: read.value.clone(), + }, + }) + }); + + let mut findings: Vec = conditions.chain(unreachable).chain(values).collect(); + // in source order, because a client stacks the labels for one line in the order it is given + // them and a margin that reads back-to-front is one the reader has to sort out + findings.sort_by_key(|finding| finding.range.start()); + findings } #[cfg(test)] mod tests { use super::*; - use crate::tests::cursor_test; + use crate::tests::CursorTest; use ruff_python_ast::name::Name; use ty_python_core::assumptions::{ClassName, Observed}; @@ -123,8 +165,13 @@ mod tests { /// /// `` marks the line the program is stopped on, which is what the test is really /// about: everything below it is the question and everything above it has already run + /// + /// the fixture is a `.by` file because that is the only kind this feature is ever asked about: + /// the plugin fires on a basedpython file type and on nothing else. it is not a formality — + /// basedpython infers a literal type for a float and python does not, so `discount = 0.0` is + /// `float` in a `.py` fixture and `0.0` in the file a user is actually stopped in fn at(source: &str, observations: Vec<(&str, Observed)>) -> Vec { - let test = cursor_test(source); + let test = CursorTest::builder().source("main.by", source).build(); let file = test.cursor.file; let text = ruff_db::source::source_text(&test.db, file); let line = text[..usize::from(test.cursor.offset)] @@ -537,4 +584,174 @@ if isinstance(thing, Runner): "found {found:?}" ); } + + /// the function a user reported both of this module's bugs against, called with `qty=3` and + /// `member=False` + /// + /// worth keeping verbatim: the first defect only appeared because line 2 is the *first* + /// statement of the body, and the second only appeared because `discount` is a float + const PRICE: &str = "\ +def price(qty: int, member: bool): + discount = 0.0 + if qty >= 10: + discount = 0.1 + if member: + discount += 0.05 + return discount +"; + + /// what the two parameters were, at whichever line the program stopped on + fn priced() -> Vec<(&'static str, Observed)> { + vec![ + ("qty", Observed::IsInt("3".to_string())), + ("member", Observed::IsBool(false)), + ] + } + + #[test] + fn a_stop_on_the_first_statement_of_a_function_body_is_still_inside_that_function() { + // reported as "nothing is shown until the stop reaches the `if`". a statement's range + // begins at its first token, so the indentation in front of the first statement of a body + // belonged to no statement — and a stop offset taken at the start of the line landed just + // before the body, which made `stopped_scope` answer with the module and every seed get + // refused as being about another frame. one line further down the same file decided + // everything, which is what made it look like the analysis rather than the offset + let found = at( + &PRICE.replacen(" discount = 0.0", " discount = 0.0", 1), + priced(), + ); + assert!( + found.iter().any(|f| f == "qty >= 10: = false") + && found.iter().any(|f| f == "member: = false"), + "both branches are below this stop and both parameters were observed, and found {found:?}" + ); + } + + #[test] + fn a_stop_one_line_lower_reaches_exactly_the_same_answer() { + // the control for the test above. these two stops differ only in which line the program is + // held on, and nothing between them binds or reads anything — so an answer that differed + // would be the offset showing through again + let first = at( + &PRICE.replacen(" discount = 0.0", " discount = 0.0", 1), + priced(), + ); + let second = at( + &PRICE.replacen(" if qty >= 10:", " if qty >= 10:", 1), + priced(), + ); + assert_eq!(first, second, "the two stops disagree"); + } + + #[test] + fn the_value_a_name_still_holds_below_two_dead_branches_is_reported() { + // the whole point of the feature past reachability: neither `if` runs, so neither + // assignment to `discount` runs, so the `0.0` from line 2 is what `return discount` finds. + // no observation of `discount` is involved — a float is not an observation this can carry, + // and it does not need to be. the source says what it was assigned and the seeds say which + // of the later assignments are dead + let found = at( + &PRICE.replacen(" if qty >= 10:", " if qty >= 10:", 1), + priced(), + ); + assert!( + found.iter().any(|f| f == "discount: discount = 0.0"), + "found {found:?}" + ); + } + + #[test] + fn a_read_inside_a_decided_condition_gets_no_value_of_its_own() { + // `qty >= 10` already carries a `= false`, and it is drawn in the same margin. `qty = 3` + // beside it is the working rather than the answer + let found = at( + &PRICE.replacen(" if qty >= 10:", " if qty >= 10:", 1), + priced(), + ); + assert!( + !found.iter().any(|f| f.starts_with("qty: ")), + "found {found:?}" + ); + } + + #[test] + fn a_value_that_depends_on_something_unobserved_is_not_guessed_at() { + // the control for the value half. `qty` decides one branch and nothing decides the other, + // so `discount` at the return is `0.0` or `0.15` and the honest answer is neither. a + // feature that picked the likelier one would be worth less than one that says nothing, + // because the reason to trust it at all is that it only reports what follows + let found = at( + "\ +def price(qty: int, member: bool): + discount = 0.0 + if qty >= 10: + discount = 0.1 + if member: + discount += 0.05 + return discount +", + vec![("qty", Observed::IsInt("3".to_string()))], + ); + assert!( + !found.iter().any(|f| f.starts_with("discount: ")), + "found {found:?}" + ); + } + + #[test] + fn a_value_the_source_alone_already_fixes_is_not_reported_as_the_debuggers_doing() { + // `rate` is 0.2 whether or not anything is being debugged, and the editor is not being + // told that by a debugger. reporting it would credit ordinary inference to the stop + let found = at( + "\ +def price(qty: int): + rate = 0.2 + if qty >= 10: + big = 1 + return rate +", + vec![("qty", Observed::IsInt("3".to_string()))], + ); + assert!( + !found.iter().any(|f| f.starts_with("rate: ")), + "found {found:?}" + ); + } + + #[test] + fn a_container_whose_length_a_dead_branch_would_have_changed_reports_no_value() { + // the rule that a fact only travels to code that has not run when it will still be true + // there. this needs no guard of its own: a list is a `list[int]` and a `list[int]` is not + // one value, so there is nothing for the value half to report. the test is here because + // that is a property of the design rather than of anything written down, and a future + // change that started reporting a container would break it silently + let found = at( + "\ +def collect(flag: bool): + items = [] + if flag: + items.append(1) + return items +", + vec![("flag", Observed::IsBool(false))], + ); + assert!( + !found.iter().any(|f| f.starts_with("items: ")), + "found {found:?}" + ); + } + + #[test] + fn a_store_is_not_annotated_with_the_value_it_is_storing() { + // `discount = 0.1` says `0.1` on its own line. the value half is for reads, where somebody + // has to work out what arrived + let found = at( + &PRICE.replacen(" if qty >= 10:", " if qty >= 10:", 1), + priced(), + ); + assert!( + found.iter().all(|f| f != "discount: discount = 0.1"), + "found {found:?}" + ); + } } diff --git a/crates/ty_python_semantic/src/assumed.rs b/crates/ty_python_semantic/src/assumed.rs index 3a11cf8c38..28f9ac6894 100644 --- a/crates/ty_python_semantic/src/assumed.rs +++ b/crates/ty_python_semantic/src/assumed.rs @@ -191,11 +191,10 @@ pub(crate) fn seeds<'db>( return seeds; } - let source = source_text(db, source_file); let Some(line) = OneIndexed::new(assumptions.line(db) as usize) else { return seeds; }; - let stop = line_index(db, source_file).line_start(line, &source); + let stop = stop_offset(db, source_file, line); let file_scope = scope.file_scope_id(db); if *stopped_scope(db, file, stop) != Some(file_scope) { @@ -228,12 +227,50 @@ pub(crate) fn seeds<'db>( seeds } +/// where in the source a program stopped on `line` actually is +/// +/// the first character of the line that is not indentation, rather than the line's first byte. a +/// debugger reports a line, and everything downstream of that wants an offset — which scope the +/// stop is in, which bindings are behind it, which code is below it. +/// +/// the line's first byte was the obvious offset and it was wrong, in a way that only showed on one +/// shape of source. every statement's range starts at its first token, so the indentation in front +/// of it belongs to no statement at all — and [`body_contains`] asks whether the stop falls between +/// the first statement's start and the last one's end. a stop on the *first* statement of a +/// function body therefore landed just before that body, [`stopped_scope`] answered with the +/// enclosing scope instead, and every seed was refused for being about another frame: +/// +/// ```py +/// def price(qty: int, member: bool): +/// discount = 0.0 # ← stopped here: line_start is in the indent, before `discount` +/// if qty >= 10: ... # nothing decided. one line further down, everything decided +/// ``` +/// +/// widening the *body* to include its first line's indentation was the alternative. it loses on a +/// compound statement written on one line — `def f(): return 1`, where the body's first statement +/// shares the header's line, and a stop there would then be read as inside the body rather than on +/// the header. narrowing the stop instead leaves that distinction exactly where it was +/// +/// a blank or all-whitespace line has no such character, and answers with the line start. nothing +/// is written there for the answer to be wrong about +pub fn stop_offset(db: &dyn Db, file: ruff_db::files::File, line: OneIndexed) -> TextSize { + let source = source_text(db, file); + let start = line_index(db, file).line_start(line, &source); + let indent = source[usize::from(start)..] + .find(|character: char| !matches!(character, ' ' | '\t' | '\x0c')) + .unwrap_or(0); + start + TextSize::try_from(indent).unwrap_or_default() +} + /// the innermost scope the stop line falls inside /// /// walked over the syntax rather than asked of the scope tree because the question is "which frame /// is this", and a frame is a function body or the module body. the scopes that have no statements /// to stop on — a lambda, a comprehension, a type-parameter list — are not candidates, so a stop /// inside one of them answers with the function or module that contains it +/// +/// `stop` is a [`stop_offset`], not a line start: this walk compares it against statement ranges, +/// which begin at a statement's first token #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] pub(crate) fn stopped_scope<'db>( db: &'db dyn Db, @@ -448,11 +485,10 @@ pub(crate) fn is_at_or_below_stop_line<'db>( if source_file != assumptions.file(db) { return false; } - let source = source_text(db, source_file); let Some(line) = OneIndexed::new(assumptions.line(db) as usize) else { return false; }; - range.start() >= line_index(db, source_file).line_start(line, &source) + range.start() >= stop_offset(db, source_file, line) } /// module-level names basedpython renames on the way out, generated name first @@ -718,4 +754,62 @@ def f(): inventing a type that is nearly it would be worse than staying quiet" ); } + + /// which scope a stop on each line of an indented body is read as being in + fn scope_stopped_in(db: &TestDb, line: u32) -> Option { + let file = system_path_to_file(db, "/src/stopped.py").expect("the fixture was written"); + let stop = stop_offset( + db, + file, + OneIndexed::new(line as usize).expect("a one-based line"), + ); + *stopped_scope(db, db.program().program_file(db, file), stop) + } + + #[test] + fn a_stop_on_the_first_statement_of_a_body_is_read_as_inside_that_body() { + // the offset a stop is taken at used to be the first byte of the line, which is in the + // indentation — and a body's extent is measured from its first statement's first *token*. + // so a stop on line 2 fell just outside `f`, the scope came back as the module, and every + // seed was refused for being about another frame. a stop on line 3 was fine, which is what + // made it look like a fault in the analysis rather than in the offset + let db = db_with( + "\ +def f(): + limit = compute() + if limit > 100: + over = 1 +", + ); + let inside = scope_stopped_in(&db, 3); + assert_ne!( + inside, + Some(FileScopeId::global()), + "the fixture is wrong: line 3 was supposed to be inside `f`" + ); + assert_eq!( + scope_stopped_in(&db, 2), + inside, + "a stop on the first statement of `f` is in `f`, the same as one on the second" + ); + } + + #[test] + fn a_stop_on_a_function_header_is_read_as_outside_it() { + // the other edge of the same offset. a `def` line is written in the scope that contains + // the function, not in the function — nothing of the body has been entered yet, and a + // frame for it does not exist. narrowing the stop to the line's first token rather than + // widening the body to its first line is what keeps this true + let db = db_with( + "\ +def f(): + limit = compute() +", + ); + assert_eq!( + scope_stopped_in(&db, 1), + Some(FileScopeId::global()), + "a stop on `def f():` is in the module, not in `f`" + ); + } } diff --git a/crates/ty_python_semantic/src/lib.rs b/crates/ty_python_semantic/src/lib.rs index af76443e19..f5d7af247e 100644 --- a/crates/ty_python_semantic/src/lib.rs +++ b/crates/ty_python_semantic/src/lib.rs @@ -67,6 +67,7 @@ pub use types::{DisplaySettings, ProgramEnvironment, TypeQualifiers}; pub mod api_lockfile; mod assumed; +pub use assumed::stop_offset; mod db; pub mod dependencies; pub mod django_settings; diff --git a/crates/ty_python_semantic/src/types/ide_support.rs b/crates/ty_python_semantic/src/types/ide_support.rs index 829c3f953d..aace9056ae 100644 --- a/crates/ty_python_semantic/src/types/ide_support.rs +++ b/crates/ty_python_semantic/src/types/ide_support.rs @@ -50,7 +50,7 @@ mod unreachable_code; #[path = "ide_support/unused_bindings.rs"] mod unused_binding_support; -pub use data_flow::{ConditionVerdict, DataFlow, data_flow}; +pub use data_flow::{ConditionVerdict, DataFlow, ValueVerdict, data_flow}; pub use resolve_definition::{ImportAliasResolution, ResolvedDefinition, map_stub_definition}; use resolve_definition::{find_symbol_in_scope, resolve_definition}; pub use unreachable_code::{UnreachableKind, UnreachableRange, unreachable_ranges}; diff --git a/crates/ty_python_semantic/src/types/ide_support/data_flow.rs b/crates/ty_python_semantic/src/types/ide_support/data_flow.rs index df9b862800..7267e9c726 100644 --- a/crates/ty_python_semantic/src/types/ide_support/data_flow.rs +++ b/crates/ty_python_semantic/src/types/ide_support/data_flow.rs @@ -37,6 +37,15 @@ pub struct ConditionVerdict { pub verdict: Truthiness, } +/// what one read of a name will find when the program reaches it +#[derive(Debug, Clone, PartialEq, Eq, get_size2::GetSize)] +pub struct ValueVerdict { + /// the read itself — the `discount` in `return discount`, not the statement around it + pub range: TextRange, + /// the value, written the way a source writes it: `0.0`, `3`, `False`, `"hi"` + pub value: String, +} + /// what the runtime state settles that the source alone does not #[derive(Debug, Clone, PartialEq, Eq)] pub struct DataFlow { @@ -44,6 +53,8 @@ pub struct DataFlow { pub conditions: Box<[ConditionVerdict]>, /// the code below the stop line that is now known not to run pub unreachable: Box<[UnreachableRange]>, + /// the reads below the stop line that will find exactly one value + pub values: Box<[ValueVerdict]>, } /// what a seeded reading of `file` decides that the unseeded reading of `unseeded` does not @@ -59,7 +70,7 @@ pub fn data_flow<'db>( ) -> DataFlow { let without = verdicts(db, unseeded); - let conditions = verdicts(db, seeded) + let conditions: Box<[ConditionVerdict]> = verdicts(db, seeded) .iter() .copied() .filter(|decided| decided.range.start() >= below) @@ -78,9 +89,31 @@ pub fn data_flow<'db>( .copied() .collect(); + let already_known = values(db, unseeded); + let values = values(db, seeded) + .iter() + .filter(|read| read.range.start() >= below) + // the same comparison the conditions get, and for the same reason: a value the source + // alone already fixes is not the debugger's doing, and comparing the *value* rather than + // only the range means a disagreement between the two readings is reported instead of + // quietly dropped here + .filter(|read| !already_known.contains(read)) + // a read inside a condition this pass has already decided is that same finding written + // twice. `qty >= 10` gets a `= false`; adding `qty = 3` beside it is the working rather + // than the answer, and both labels land in the one margin, so it is also the only place + // two of this feature's labels would compete for the same space + .filter(|read| { + !conditions + .iter() + .any(|decided: &ConditionVerdict| decided.range.contains_range(read.range)) + }) + .cloned() + .collect(); + DataFlow { conditions, unreachable, + values, } } @@ -115,6 +148,81 @@ fn verdicts<'db>(db: &'db dyn Db, file: ProgramFile<'db>) -> Box<[ConditionVerdi .collect() } +/// every read in the file that this reading pins to one value +/// +/// the whole file and cached per program, for the same reason [`verdicts`] is: the unseeded half of +/// the comparison is computed once and answered from salsa for the rest of the debug session +/// +/// ## the value is the type, and that is the whole check +/// +/// a read is decided when its inferred type stands for exactly one value — `Literal[3]`, `0.0`, +/// `Literal[False]`. that is not a second analysis bolted on beside the reachability one, it is the +/// same one asked a different question, and it is what makes "only what follows from decided +/// branches plus observed seeds" true by construction rather than by a rule written here: +/// +/// * a value that depends on anything unobserved is a union or an instance type, not one value, so +/// it answers nothing. there is no "probably" to invent — the type system has no way to spell one +/// * a name rebound below the stop line by a branch that will not run has that binding dropped by +/// the reachability the seed decided, so the one live binding is what is left. this is the case +/// the feature is for: `discount = 0.0` still holds at `return discount` because the two `if`s +/// that would have touched it are dead +/// * a fact that goes stale is not expressible as one value in the first place. a list's length is +/// a property of a `list[int]`, and `list[int]` is not a value — so the rule that a fact only +/// travels to code that has not run when it will still be true there needs no separate guard +/// +/// [`Type::display_value`] is the same rendering the enum-value inlay hint uses, so a value has one +/// spelling in the editor however it got there. it answers nothing for a `LiteralString`, a +/// template or an enum member, which are a *set* of values, a shape, and a name rather than a +/// value — leaving those out is that helper's own rule, and giving them a second spelling here +/// would be this feature disagreeing with the rest of the editor about what a value looks like +#[salsa::tracked(returns(ref), heap_size=ruff_memory_usage::heap_size)] +fn values<'db>(db: &'db dyn Db, file: ProgramFile<'db>) -> Box<[ValueVerdict]> { + let parsed = ruff_db::parsed::parsed_module(db, file.python_file(db)).load(db); + let mut collector = Reads { found: Vec::new() }; + source_order::walk_body(&mut collector, parsed.suite()); + + let model = SemanticModel::new(db, file); + let env = ProgramEnvironment::from_file(file); + + collector + .found + .into_iter() + .filter_map(|read| { + let value = read.inferred_type(&model)?.display_value(db, &env)?; + Some(ValueVerdict { + range: read.range(), + value: value.to_string(), + }) + }) + .collect() +} + +/// collects the places a value is read out of +/// +/// loads only. a store's value is spelled on the line the store is written on, so annotating it +/// would be repeating the source back at the reader — a load is where somebody has to work out +/// what arrived +/// +/// attributes as well as bare names, because the observations are a vocabulary of "a name or a +/// dotted path": a `self.limit` a debugger saw can decide a branch, and a feature that then refused +/// to say what `self.limit` itself holds would be inconsistent for no reason. nothing else — a +/// subscript or a call is a place where deciding the value means deciding what the call did, which +/// is precisely what a seeded reading does not claim to know +struct Reads<'ast> { + found: Vec<&'ast ast::Expr>, +} + +impl<'ast> SourceOrderVisitor<'ast> for Reads<'ast> { + fn visit_expr(&mut self, expr: &'ast ast::Expr) { + match expr { + ast::Expr::Name(node) if node.ctx.is_load() => self.found.push(expr), + ast::Expr::Attribute(node) if node.ctx.is_load() => self.found.push(expr), + _ => {} + } + source_order::walk_expr(self, expr); + } +} + /// collects the expressions that decide which way control flows /// /// not every expression, and not every `bool` — the point is what a reader would draw a `=true` diff --git a/crates/ty_server/src/server/api/requests/data_flow.rs b/crates/ty_server/src/server/api/requests/data_flow.rs index 3db932c949..cd486c9c9c 100644 --- a/crates/ty_server/src/server/api/requests/data_flow.rs +++ b/crates/ty_server/src/server/api/requests/data_flow.rs @@ -139,11 +139,18 @@ impl WireObservation { pub(crate) struct DataFlowFinding { /// where in the document pub(crate) range: lsp_types::Range, - /// what kind of finding: `condition` or `unreachable` + /// what kind of finding: `condition`, `unreachable` or `value` pub(crate) kind: String, - /// which way a condition goes. absent for an unreachable range + /// which way a condition goes. absent for anything else #[serde(skip_serializing_if = "Option::is_none")] pub(crate) taken: Option, + /// what a decided read will find, written the way a source writes it. absent for anything else + /// + /// carried beside [`label`](Self::label), which already spells it, because a client that wants + /// to do anything but draw the label — colour by value, offer it for a copy — should not have + /// to take a string written for a human back apart + #[serde(skip_serializing_if = "Option::is_none")] + pub(crate) value: Option, /// what to draw beside the source pub(crate) label: String, } @@ -202,18 +209,18 @@ impl BackgroundDocumentRequestHandler for DataFlowRequestHandler { if &location.uri != document { return None; } + let label = finding.label(); + let (kind, taken, value) = match finding.kind { + FindingKind::Condition { taken } => ("condition", Some(taken), None), + FindingKind::Unreachable => ("unreachable", None, None), + FindingKind::Value { value, .. } => ("value", None, Some(value)), + }; Some(DataFlowFinding { range: location.range, - kind: match finding.kind { - FindingKind::Condition { .. } => "condition", - FindingKind::Unreachable => "unreachable", - } - .to_string(), - taken: match finding.kind { - FindingKind::Condition { taken } => Some(taken), - FindingKind::Unreachable => None, - }, - label: finding.label().to_string(), + kind: kind.to_string(), + taken, + value, + label, }) }) .collect(); diff --git a/crates/ty_server/tests/e2e/data_flow.rs b/crates/ty_server/tests/e2e/data_flow.rs index f29e66f2c1..b2f348e8ac 100644 --- a/crates/ty_server/tests/e2e/data_flow.rs +++ b/crates/ty_server/tests/e2e/data_flow.rs @@ -108,3 +108,67 @@ fn the_same_request_with_nothing_observed_settles_nothing() -> Result<()> { Ok(()) } + +/// the function a user reported the value half missing from +/// +/// a `.by` file rather than a `.py` one, because that is the only kind a debug session asks about +/// and it is load-bearing here: basedpython gives a float literal a literal type and python does +/// not, so `discount` at the return is `float` in a `.py` file and `0.0` in this one +const PRICE: &str = "\ +def price(qty: int, member: bool): + discount = 0.0 + if qty >= 10: + discount = 0.1 + if member: + discount += 0.05 + return discount +"; + +#[test] +fn the_value_a_name_will_hold_crosses_the_wire_with_its_own_kind() -> Result<()> { + // the value finding carries a string where a condition carries a bool, so it is the one shape + // in the reply that nothing else exercises. the client reads `kind` to decide how to draw it, + // which is exactly the field a serde attribute can break with no test inside the crate noticing + let workspace_root = SystemPath::new("src"); + let foo = SystemPath::new("src/foo.by"); + + let mut server = TestServerBuilder::new()? + .with_initialization_options(ClientOptions::default()) + .with_workspace(workspace_root, None)? + .with_file(foo, PRICE)? + .build() + .wait_until_workspaces_are_initialized(); + + server.open_text_document(foo, PRICE, 1); + + let findings = server + .send_request_await::(serde_json::json!({ + "textDocument": { "uri": server.file_uri(foo) }, + // the first statement of the body — the stop that used to answer nothing at all + "line": 2, + "observations": [ + { "name": "qty", "observed": "isInt", "text": "3" }, + { "name": "member", "observed": "isBool", "value": false }, + ], + })) + .expect("the server answers a file it is checking"); + + let value = findings + .iter() + .find(|finding| finding["kind"] == "value") + .unwrap_or_else(|| { + panic!("neither `if` runs, so `return discount` finds line 2's 0.0: {findings:?}") + }); + + assert_eq!(value["value"], "0.0", "the whole finding was {value:?}"); + assert_eq!( + value["label"], "discount = 0.0", + "the label names the name, because a client draws it in the margin and not at the read" + ); + assert!( + value["taken"].is_null(), + "a value is not a branch, and a client keying off `taken` must see nothing: {value:?}" + ); + + Ok(()) +} From 655ea2ee3ab39e2d4ce946bce7486e644ac76687 Mon Sep 17 00:00:00 2001 From: KotlinIsland <65446343+kotlinisland@users.noreply.github.com> Date: Tue, 18 Aug 2026 11:14:20 +1000 Subject: [PATCH 2/2] a float read off a running program is a value the checker can hold MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `bpd` proves a float and nothing could spend it: `Observed` had no variant for one, so the plugin dropped the fact and the reading fell back to whatever the source alone could say. that is `float` for anything out of a call, which is the case the observation is worth having for — a literal in the source needs no debugger to be known. so `Observed::IsFloat`, carried as `float.__repr__`'s own text rather than as a json number. json has no spelling for `inf` or `nan`, and a reader that went through a number would lose them; text is what `IsInt` already does, for the neighbouring reason that a python int has no width. every value crosses, including the two source cannot write. a reading is a statement about a value, and `nan` really is what the name holds — dropping it would trade a fact for a defence against something that does not exist. what they are dangerous for is *comparison folding*, which is a rule about types rather than a statement about a value: `nan` is not equal to itself and `-0.0` is equal to `0.0` while being a distinct literal, so an arm deciding `==` from literal identity would answer both the wrong way. `by` folds `Int`, `Bool`, `String` and `Bytes` and not `Float`, so nothing decides them today — and the warning is in the doc comment on `fold_literal_rich_comparison`, where such an arm would be written, rather than left to be rediscovered there. the boundary is pinned by a test rather than described: a float seed narrows and displays and decides no branch, and if that test ever starts finding something, the `Float` arm has been added and the two cases above it have to have been handled. measured live, `by run` + bpd + a real `by server`, on a float that comes out of a call: proved: ratio is_exactly float, ratio is_float "0.25" sent to by: [{"name":"ratio","observed":"isFloat","text":"0.25"}] line 6 value 'ratio' -> 'ratio = 0.25' line 7 value 'scaled' -> 'scaled = 0.25' the exact reading beat the class bpd proves beside it, which is the pairing it really sends. --- crates/ty_ide/src/data_flow.rs | 61 +++++++++++++++++++ crates/ty_python_core/src/assumptions.rs | 8 +++ crates/ty_python_semantic/src/assumed.rs | 23 ++++++- .../src/types/infer/comparisons.rs | 12 ++++ .../src/server/api/requests/data_flow.rs | 24 ++++++++ 5 files changed, 126 insertions(+), 2 deletions(-) diff --git a/crates/ty_ide/src/data_flow.rs b/crates/ty_ide/src/data_flow.rs index 3d0b3bb2cc..274ec7bb56 100644 --- a/crates/ty_ide/src/data_flow.rs +++ b/crates/ty_ide/src/data_flow.rs @@ -216,6 +216,67 @@ if limit > 100: ); } + /// the case the float observation exists for: the value came out of a call, so the file alone + /// says `float` and cannot say which one. this is what reaches the reader beside the code + #[test] + fn a_float_read_off_the_program_is_shown_as_the_value_it_holds() { + let found = at( + "\ +ratio = measure() + +scaled = ratio +", + vec![("ratio", Observed::IsFloat("0.25".to_string()))], + ); + assert!( + found.iter().any(|f| f == "ratio: ratio = 0.25"), + "the read below the stop should say what it holds, and found {found:?}" + ); + } + + /// every float, including the two source cannot write. a reading is a statement about the + /// value, and `nan` really is what the name holds — replacing it with `float` would drop a + /// fact to defend against a comparison nothing folds. see the note on + /// `fold_literal_rich_comparison`, which is where that defence belongs + #[test] + fn the_floats_source_cannot_write_are_still_shown() { + for text in ["nan", "-0.0", "inf"] { + let found = at( + "\ +ratio = measure() + +scaled = ratio +", + vec![("ratio", Observed::IsFloat(text.to_string()))], + ); + assert!( + found.iter().any(|f| f.starts_with("ratio: ratio = ")), + "{text} is a value the debugger really read, and found {found:?}" + ); + } + } + + /// the boundary, pinned deliberately rather than left to be discovered: `by` folds `Int`, + /// `Bool`, `String` and `Bytes` literal comparisons and not `Float`, so a float seed narrows + /// and displays but decides no branch. if this ever starts finding something, the `Float` arm + /// has been added and the `nan` / `-0.0` cases above it have to have been handled + #[test] + fn a_float_does_not_yet_decide_a_comparison() { + let found = at( + "\ +ratio = measure() + +if ratio > 0.5: + high = 1 +", + vec![("ratio", Observed::IsFloat("0.25".to_string()))], + ); + assert!( + !found.iter().any(|f| f.contains("ratio > 0.5")), + "float comparisons are not folded, and found {found:?}" + ); + } + #[test] fn without_the_observation_the_same_file_settles_nothing() { // the control for the test above. if this ever finds something, the feature is reporting diff --git a/crates/ty_python_core/src/assumptions.rs b/crates/ty_python_core/src/assumptions.rs index 28d4fd7903..d86c999abe 100644 --- a/crates/ty_python_core/src/assumptions.rs +++ b/crates/ty_python_core/src/assumptions.rs @@ -105,6 +105,14 @@ pub enum Observed { /// as a literal falls back to `int`, which is still narrower than nothing IsInt(String), + /// the value is exactly this float, as `float.__repr__` writes it + /// + /// python's own text, so `inf`, `-inf`, `nan` and `-0.0` all survive the crossing. two of them + /// cannot become a literal type on the other side and are not this module's business to filter + /// — the vocabulary records what was read, and `ty_python_semantic::assumed` decides what can + /// be said with it + IsFloat(String), + /// the value is exactly this string IsStr(String), diff --git a/crates/ty_python_semantic/src/assumed.rs b/crates/ty_python_semantic/src/assumed.rs index 28f9ac6894..aa0c81d1c7 100644 --- a/crates/ty_python_semantic/src/assumed.rs +++ b/crates/ty_python_semantic/src/assumed.rs @@ -53,6 +53,25 @@ pub(crate) fn seeded_type<'db>( Type::int_literal, )), + // the float as it was read, every value of it — `inf`, `-inf`, `nan` and `-0.0` included. + // + // a literal for those is a *true* statement about the value, and the reading is what gets + // displayed beside the code, so filtering them here would replace a fact with `float` for + // no gain. what they are dangerous for is comparison folding, which is a rule about types + // rather than a statement about a value: `nan` is not equal to itself and `-0.0` *is* equal + // to `0.0`, so an arm that decided `==` from literal identity would answer both the wrong + // way. `by` folds `Int`, `Bool`, `String` and `Bytes` and not `Float`, so nothing decides + // them today — and a seed is neither where that would be decided nor the only way one + // arrives: basedpython already writes `float.nan` and `±float.inf` as literal types. the + // warning belongs where such an arm would be written, and is in `types::infer::comparisons` + // + // text that will not parse falls back to the class, which is the trade `IsInt` makes for an + // integer too wide to hold: still narrows a `str | float`, still says less than nothing did + Observed::IsFloat(text) => Some(text.parse::().map_or_else( + |_| crate::types::KnownClass::Float.to_instance(db, env), + Type::float_literal, + )), + Observed::IsStr(text) => Some(Type::string_literal(db, text.as_str())), Observed::IsBytes(bytes) => Some(Type::bytes_literal(db, bytes)), @@ -235,9 +254,9 @@ pub(crate) fn seeds<'db>( /// /// the line's first byte was the obvious offset and it was wrong, in a way that only showed on one /// shape of source. every statement's range starts at its first token, so the indentation in front -/// of it belongs to no statement at all — and [`body_contains`] asks whether the stop falls between +/// of it belongs to no statement at all — and `body_contains` asks whether the stop falls between /// the first statement's start and the last one's end. a stop on the *first* statement of a -/// function body therefore landed just before that body, [`stopped_scope`] answered with the +/// function body therefore landed just before that body, `stopped_scope` answered with the /// enclosing scope instead, and every seed was refused for being about another frame: /// /// ```py diff --git a/crates/ty_python_semantic/src/types/infer/comparisons.rs b/crates/ty_python_semantic/src/types/infer/comparisons.rs index 0148426d50..f0c12bf3a0 100644 --- a/crates/ty_python_semantic/src/types/infer/comparisons.rs +++ b/crates/ty_python_semantic/src/types/infer/comparisons.rs @@ -339,6 +339,18 @@ pub(crate) fn deferred_comparison<'db>( /// same numeric/string/bytes ordering the value-level literal comparison uses. `bool` /// operands are treated as `0`/`1`. Returns `None` for operand pairs that don't fold /// to a definite result (e.g. mixed numeric/string ordering). +/// +/// **A `Float` arm here needs two special cases, and neither can be read off the type.** +/// `nan` is not equal to itself, so identical literals must fold `==` to `false` and `!=` to +/// `true`; and `-0.0 == 0.0` is true while the two are distinct literals, so distinct ones must +/// not fold `==` to `false`. +/// +/// Both are already reachable, which is why this is a warning rather than a hypothetical: +/// basedpython writes `float.nan` and `±float.inf` as literal types in type positions (see +/// `docs/basedpython/features/float-literals.md`), and an ordinary `-0.0` in a value position +/// infers as one. `assumed::seeded_type` adds a third route — a float read off a running program, +/// where every one of these is unremarkable — but it did not create the hazard, and removing it +/// would not close it. fn fold_literal_rich_comparison<'db>( db: &'db dyn Db, left: LiteralValueType<'db>, diff --git a/crates/ty_server/src/server/api/requests/data_flow.rs b/crates/ty_server/src/server/api/requests/data_flow.rs index cd486c9c9c..49c7e00718 100644 --- a/crates/ty_server/src/server/api/requests/data_flow.rs +++ b/crates/ty_server/src/server/api/requests/data_flow.rs @@ -88,6 +88,11 @@ pub(crate) enum WireObserved { IsBool { value: bool }, /// the value is exactly this integer, in decimal IsInt { text: String }, + /// the value is exactly this float, as `float.__repr__` writes it + /// + /// text rather than a json number, for the reason an integer is text: a reader that went + /// through json's number would lose `inf` and `nan`, which have no json spelling at all + IsFloat { text: String }, /// the value is exactly this string IsStr { text: String }, /// the value is exactly these bytes @@ -112,6 +117,7 @@ impl WireObservation { WireObserved::IsNone => Observed::IsNone, WireObserved::IsBool { value } => Observed::IsBool(value), WireObserved::IsInt { text } => Observed::IsInt(text), + WireObserved::IsFloat { text } => Observed::IsFloat(text), WireObserved::IsStr { text } => Observed::IsStr(text), WireObserved::IsBytes { bytes } => Observed::IsBytes(bytes.into_boxed_slice()), WireObserved::IsExactly { module, qualname } => { @@ -273,6 +279,24 @@ mod tests { assert!(params(r#"{"name":"x","observed":"isImaginary","value":1}"#).is_err()); } + /// `float.__repr__`'s text, and the two spellings json has no number for + #[test] + fn a_float_observation_survives_the_crossing_including_its_infinities() { + for text in ["0.25", "-0.0", "inf", "-inf", "nan"] { + let parsed = params(&format!( + r#"{{"name":"ratio","observed":"isFloat","text":"{text}"}}"# + )) + .expect("a float observation is one of the wire forms"); + let observation = parsed + .observations + .into_iter() + .next() + .expect("one observation was sent") + .into_observation(); + assert_eq!(observation.observed, Observed::IsFloat(text.to_string())); + } + } + #[test] fn a_bytes_observation_survives_the_crossing_to_an_observed() { let parsed = params(r#"{"name":"raw","observed":"isBytes","bytes":[104,105]}"#)