[semdiff] Python migration checker: fix conversion crashes and false positives - #2063
Merged
Merged
Conversation
Summary: Textual encodes converging values via SSA block parameters + jump arguments (e.g. `v = a if c else b` lowers to a merge block `#b3(n4)` fed by `jmp b3(arg)` from each predecessor). The StructuredPeg conversion dropped both the jump arguments and the block parameters, so the parameter ident was never bound and conversion died with "unknown ident". This made the b007 migration checker crash on most real Python files (any conditional value followed by more code). We now desugar each `jmp target(args)` into per-edge `param_i := arg_i` assignments in StructuredIR.of_cfg, and merge_envs reconverges idents bound on different branches into a @phi (exactly like named locals). This gives the standard phi semantics with no dedicated phi node. Test Plan: - make -C infer/src check - New expect test in TextualToPegTest.ml: "if branch with ssa block parameter (phi via jump args)" (previously crashed with "unknown ident n4", now produces the expected @phi PEG). - dune runtest src/semdiff/unit (green) - Integration suites unchanged: make -C infer/tests/codetoanalyze/python/semdiff test make -C infer/tests/codetoanalyze/python/semdiff-b006 test make -C infer/tests/codetoanalyze/python/semdiff-b007 test
Summary: A short-circuit condition (`if a and b:`) produces two merge blocks in a row where the earlier one jumps to the later one (b3 -> b4, both merges dominated by the same node). of_cfg's node_within nested merge children in ascending rpo, making the earlier merge the OUTER block; the b3 -> b4 edge then could not find its target in context and conversion died with "br target not found in context". Forward edges between merges always go from smaller to larger rpo, so the larger-rpo merge must be the outer block to stay reachable from the inner one. Nest merge children in descending rpo order, which handles merge chains of any length. Builds on the SSA block-parameter support, which added the @phi merge of idents this relies on. On the 60-commit replay of the python_b007_unused_loop_variables codemod this brings conversion crashes down from 13 (before the SSA block-parameter fix) to 4. Test Plan: - make -C infer/src check - New expect test in TextualToPegTest.ml: "chained merge blocks (if a and b)" (previously crashed with "br target b4 not found in context"). - dune runtest src/semdiff/unit (green) - Soundness spot-checks on `if a and b` chained merges: DIFFERENT for `and` vs `or` and for differing branch values, EQUAL for identical programs and for a real B007 enumerate-removal transform. - Integration suites unchanged (semdiff, semdiff-b006, semdiff-b007).
Summary:
The Python frontend embeds the module name (derived from the source file path)
in the qualified names of nested procedures — comprehensions, generator
expressions and lambdas (e.g. `...::prev.f::_$genexpr`). semdiff compiles the
two sides from different files ("previous/x.py" vs "current/x.py"), so these
nested names always differed between the two modules. Any function containing a
comprehension/generator/lambda therefore never compared equal — a pervasive
false positive: even a function compared to itself was reported "different".
Compile both sides under a fixed filename so the module component is identical,
making nested-proc names stable across the two sides.
On a replay of 59 real python_b007_unused_loop_variables codemod commits this
drops the flagged (false-positive) count from ~43 to 6.
Test Plan:
- make -C infer/src check
- dune runtest src/semdiff/unit (green)
- semdiff / semdiff-b006 / semdiff-b007 integration suites unchanged
- Replay: generator/comprehension functions (e.g. `sum(x for x in xs)`) now
compare equal to themselves; a real avg->_avg rename in a comprehension-heavy
file is correctly EQUAL.
Summary: The b006/b007 migration checks run a PEG conversion + bisimulation for every procedure of the file, even the ones the codemod did not touch. On real files this is the dominant cost: most functions are unchanged, yet each pays the full (sometimes >60s) bisimulation, causing timeouts. A procedure that is byte-for-byte unchanged between the two sides is trivially equivalent, so add a fast-path: if proc_old and proc_new are structurally equal (location-free pretty-print), accept immediately without converting to a PEG. Locations are not semantic, so this is sound. On a replay of 59 real python_b007_unused_loop_variables codemod commits this takes EQUAL from 30 to 44 and timeouts from 15 to 5 (the remaining timeouts are files whose *changed* function is itself large). Test Plan: - make -C infer/src check - dune runtest src/semdiff/unit (green) - semdiff / semdiff-b006 / semdiff-b007 integration suites unchanged - Replay wall-clock drops from minutes to seconds; no verdict regressions.
Summary: The b007 migration check failed to recognise items()->values()/keys() and enumerate-removal transforms whenever the loop body contained a nested loop (or any heap write that keeps the loop's state alive). The outer loop's has_next(get_iter(dict_items D)) then sits under the matching get_iter/has_next wrappers of the inner loop, so the bisimulation recurses straight down to the bare dict_items vs dict_values/keys mismatch — a leaf no accept rule covers — instead of bridging at the has_next level. Result: a pervasive false positive on real comprehension/loop-heavy code. Fix: apply the has_next length-bridges (enumerate L ~ L, and items/keys/values all canonicalised to keys()) as rewrites in check_b007_migration's full_rewrite, so the outer loop's has_next is merged in the congruence closure even under wrappers. The value projection stays handled by the existing directional accept rules, so the check remains directional — a reverse migration (whose value access does not match a forward accept rule) is still rejected (see the existing "reverse … is rejected" unit tests, which still pass unchanged). Soundness: the has_next bridges are true equalities (length only); the enumerate index (subscript[0]) and value/key projections are never rewritten, so index- used, value/key-swap and body-change transforms still diverge. Canonicalising has_next to a SINGLE target (keys) is required: two targets would leave keys()/values() e-nodes in one class and the structural bisimulation could pick different ones per side and wrongly diverge. On a replay of 59 real python_b007_unused_loop_variables codemod commits the flagged false-positive count drops from 6 to 2 (the two remaining are items() wrapped in tqdm() and an enumerate->range(len) rewrite, neither modelled). Test Plan: - make -C infer/src check ; dune runtest src/semdiff/unit (green, reverse- rejection tests unchanged) - semdiff / semdiff-b006 / semdiff-b007 integration suites pass. - Added equal_items_to_values_nested and equal_items_to_keys_nested regression tests (forward, nested body). - Soundness spot-checks: reverse migration, value/key swap, body change and enumerate-index-used (incl. nested) all still report DIFFERENT.
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.
This PR improves the Python b006/b007 migration equivalence checker
(
infer semdiff --semdiff-b00{6,7}-migration): it fixes several conversioncrashes and a large class of false positives found by replaying real codemod
commits.
Commits
arguments (the phi mechanism); previously any function with a conditional
value (
a if c else b) crashed with "unknown ident".children in descending rpo so
if a and b:(two chained merges) no longerdies with "br target not found in context".
embedded in nested-proc qualified names (comprehensions/generators/lambdas),
so any such function never compared equal across the two files. Pervasive FP.
procedures are accepted without the (sometimes >60s) bisimulation, removing
most timeouts.
items()->keys()/values() and enumerate-removal bridge when the loop body has
a nested loop; kept directional (reverse migrations still rejected).
Impact
On a replay of 59 real
python_b007_unused_loop_variablescodemod commits:conversion crashes 13 → 4, false positives 37 → 2, EQUAL 12 → 48.
Test Plan
make -C infer/src check(no warnings)make ocaml_unit_test(new regression tests inTextualToPegTest.ml)semdiff,semdiff-b006,semdiff-b007integration suites passequal_items_to_{values,keys}_nestedtests; soundness spot-checks(reverse migration, value/key swap, body change, enumerate-index-used) stay
DIFFERENT.