Dfa work - #185
Merged
Merged
Conversation
…ches now says what it holds 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.
`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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.