Skip to content

Conversation

@sharkdp
Copy link
Contributor

@sharkdp sharkdp commented Apr 30, 2025

Summary

We were previously recording wrong reachability constraints for negative branches. Instead of [cond] AND (NOT [True]) below, we were recording [cond] AND (NOT ([cond] AND [True])), i.e. we were negating not just the last predicate, but the AND-ed reachability constraint from last clause. With this fix, we now record the correct constraints for the example from #17723:

def _(cond: bool):
    if cond:
        # reachability: [cond]
        if True:
            # reachability: [cond] AND [True]
            pass
        else:
            # reachability: [cond] AND (NOT [True])
            x

closes #17723

Test Plan

  • Regression test.
  • Verified the ecosystem changes

@sharkdp sharkdp added the ty Multi-file analysis & type inference label Apr 30, 2025
@github-actions
Copy link
Contributor

mypy_primer results

Changes were detected when running on open source projects
kornia (https://github.com/kornia/kornia)
- warning[lint:unresolved-reference] kornia/utils/helpers.py:302:35: Name `A_LU` used when not defined
- warning[lint:unresolved-reference] kornia/utils/helpers.py:302:41: Name `pivots` used when not defined
- warning[lint:unresolved-reference] kornia/utils/helpers.py:305:41: Name `A_LU` used when not defined
- warning[lint:unresolved-reference] kornia/utils/helpers.py:305:47: Name `pivots` used when not defined
- Found 1014 diagnostics
+ Found 1010 diagnostics

flake8-pyi (https://github.com/PyCQA/flake8-pyi)
- error[lint:unresolved-attribute] pyi.py:2043:31: Type `<module 'ast'>` has no attribute `TypeVar`
- Found 33 diagnostics
+ Found 32 diagnostics

aiortc (https://github.com/aiortc/aiortc)
- warning[lint:unresolved-reference] src/aiortc/rtcsctptransport.py:530:31: Name `expected_tsn` used when not defined
- warning[lint:unresolved-reference] src/aiortc/rtcsctptransport.py:531:20: Name `ordered` used when not defined
- Found 131 diagnostics
+ Found 129 diagnostics

pip (https://github.com/pypa/pip)
- error[lint:unresolved-attribute] src/pip/_vendor/typing_extensions.py:4527:20: Type `<module 'typing'>` has no attribute `_eval_type`
- error[lint:unresolved-attribute] src/pip/_vendor/typing_extensions.py:4534:16: Type `<module 'typing'>` has no attribute `_eval_type`
- Found 1244 diagnostics
+ Found 1242 diagnostics

pyodide (https://github.com/pyodide/pyodide)
- warning[lint:unresolved-reference] pyodide-build/pyodide_build/pywasmcross.py:332:9: Name `symbol_lines` used when not defined
- warning[lint:unresolved-reference] pyodide-build/pyodide_build/pywasmcross.py:342:68: Name `symbol_lines` used when not defined
- Found 1258 diagnostics
+ Found 1256 diagnostics

pycryptodome (https://github.com/Legrandin/pycryptodome)
- warning[lint:unresolved-reference] lib/Crypto/SelfTest/Hash/test_BLAKE2.py:293:42: Name `input_data` used when not defined
- warning[lint:unresolved-reference] lib/Crypto/SelfTest/Hash/test_BLAKE2.py:293:54: Name `key` used when not defined
- Found 2184 diagnostics
+ Found 2182 diagnostics

static-frame (https://github.com/static-frame/static-frame)
- warning[lint:possibly-unresolved-reference] static_frame/core/util.py:1269:32: Name `rows` used when possibly not defined
- Found 4764 diagnostics
+ Found 4763 diagnostics

jax (https://github.com/google/jax)
- error[lint:unresolved-attribute] jax/_src/export/_export.py:763:41: Type `None` has no attribute `_aval`
- warning[lint:unresolved-reference] jax/_src/interpreters/ad.py:284:67: Name `aux` used when not defined
- Found 6082 diagnostics
+ Found 6080 diagnostics

@sharkdp sharkdp marked this pull request as ready for review April 30, 2025 07:30
@sharkdp
Copy link
Contributor Author

sharkdp commented Apr 30, 2025

Merging this without review, as the fix is relatively obvious in hindsight (after two hours of debugging 😢).

@sharkdp sharkdp merged commit 4a621c2 into main Apr 30, 2025
35 checks passed
@sharkdp sharkdp deleted the david/fix-negative-reachability-constraints branch April 30, 2025 07:32
Copy link
Member

@dcreager dcreager left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 post-merge review looks good!

dcreager added a commit that referenced this pull request Apr 30, 2025
* main:
  [red-knot] Use 'full' salsa backtrace output that includes durability and revisions (#17735)
  [red-knot] Initial support for protocol types (#17682)
  [red-knot] Computing a type ordering for two non-normalized types is meaningless (#17734)
  [red-knot] Include salsa backtrace in check and mdtest panic messages (#17732)
  [red-knot] Fix control flow for `assert` statements (#17702)
  [red-knot] Fix recording of negative visibility constraints (#17731)
  [red-knot] Update salsa (#17730)
  [red-knot] Support overloads for callable equivalence (#17698)
  [red-knot] Run py-fuzzer in CI to check for new panics (#17719)
  Upload red-knot binaries in CI on completion of linux tests (#17720)
  [`flake8-use-pathlib`] Fix `PTH123` false positive when `open` is passed a file descriptor from a function call (#17705)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ty Multi-file analysis & type inference

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[red-knot] Bug in reachability constraint merging

2 participants