fix: Add Dict and List to Any_to_bool precondition by MikaelMayer · Pull Request #675 · strata-org/Strata

MikaelMayer · 2026-03-26T17:31:23Z

Problem

Any_to_bool only accepted bool, none, string, and int in its precondition and body (returning false for everything else). This caused a soundness issue:

After if results:, the solver knows results must satisfy Any_to_bool's precondition and its body must return true. Since Dict and List were not handled, the solver could prove that results is never a Dict or List. Then PIn's precondition (requires isfrom_Dict || isfrom_ListAny) was provably unsatisfiable:

❌ always false and is reachable from declaration entry

This is a false positive — in Python, non-empty dicts and lists are truthy.

Fix

Add isfrom_Dict and isfrom_ListAny to Any_to_bool's precondition and body: empty dict/list → false, non-empty → true.

Additional changes

Add # strata-args: directive for per-file flags in test Python files
Deprecate pyAnalyze (non-Laurel) in CI — default to pyAnalyzeLaurel

Test

test_pin_any.py: def test_in_on_any(results: Any): if results: assert 'key' in results

Before: assert_assert(124)_calls_PIn_0: ❌ always false and is reachable
After: assert_assert(124)_calls_PIn_0: ❓ unknown

Any_to_bool only accepted bool, none, string, and int in its precondition and body (returning false for everything else). This caused a soundness issue: after `if results:`, the solver knew results must satisfy Any_to_bool's precondition (bool/none/ string/int) and its body must return true. Since Dict and List were not in the precondition, the solver could prove that results is never Dict or List. Then PIn's precondition (requires Dict or List) was provably unsatisfiable — reported as: ❌ always false and is reachable from declaration entry In Python, non-empty dicts and lists are truthy. Add isfrom_Dict and isfrom_ListAny to Any_to_bool's precondition and body (empty → false, non-empty → true). Test: test_pin_any.py — `if results: assert 'key' in results` Before: PIn precondition is ❌ always false and is reachable After: PIn precondition is ❓ unknown

StrataTest/Languages/Python/AnalyzeLaurelTest.lean

…deResult helper

test_variable_reassign and test_while_loop had assertions that were previously provably false (❌) because Any_to_bool excluded Dict/List. With the fix, these become unknown (❓) — the solver can no longer rule out Dict/List values after a truthiness check.

…st change

…l affected assertions

StrataTest/Languages/Python/AnalyzeLaurelTest.lean

StrataTest/Languages/Python/Specs/dispatch_test/test_pin_any.py

Remove Lean #eval test (requires fake fixture). Use run_py_analyze.sh framework instead: test_pin_any.py in tests/ with expected output in expected_laurel/. Empty expected file — CI will show the correct output.

… output Add '# strata-args:' comment directive to Python test files for passing extra flags to strata (e.g. --check-mode bugFinding). The shell script parses this and appends the args to the strata invocation. test_pin_any.py uses bugFinding mode to verify that PIn precondition is not provably false after a truthiness check on an opaque Any.

…n_any

…use git add -A)

pyAnalyze is deprecated in favor of pyAnalyzeLaurel. The shell script now defaults to laurel mode. CI no longer runs the non-Laurel pipeline.

joscoh

I think the CI change should be a separate PR, but I am fine to merge if others are.

aqjune-aws

Approving based on the fact that Thanh approved in the past

## Problem `Any_to_bool` only accepted `bool`, `none`, `string`, and `int` in its precondition and body (returning `false` for everything else). This caused a soundness issue: After `if results:`, the solver knows `results` must satisfy `Any_to_bool`'s precondition and its body must return `true`. Since Dict and List were not handled, the solver could prove that `results` is never a Dict or List. Then `PIn`'s precondition (`requires isfrom_Dict || isfrom_ListAny`) was provably unsatisfiable: ``` ❌ always false and is reachable from declaration entry ``` This is a false positive — in Python, non-empty dicts and lists are truthy. ## Fix Add `isfrom_Dict` and `isfrom_ListAny` to `Any_to_bool`'s precondition and body: empty dict/list → `false`, non-empty → `true`. ## Additional changes - Add `# strata-args:` directive for per-file flags in test Python files - Deprecate `pyAnalyze` (non-Laurel) in CI — default to `pyAnalyzeLaurel` ## Test `test_pin_any.py`: `def test_in_on_any(results: Any): if results: assert 'key' in results` - **Before**: `assert_assert(124)_calls_PIn_0: ❌ always false and is reachable` - **After**: `assert_assert(124)_calls_PIn_0: ❓ unknown`

MikaelMayer force-pushed the fix/pin-any-precondition branch from e3d708d to 8b71992 Compare March 26, 2026 17:39

MikaelMayer changed the title ~~fix: Handle 'in' operator on opaque Any values without false positive~~ fix: Add Dict and List to Any_to_bool precondition Mar 26, 2026

This comment was marked as outdated.

Sign in to view

MikaelMayer closed this Mar 26, 2026

This comment was marked as outdated.

Sign in to view

MikaelMayer reopened this Mar 26, 2026

MikaelMayer force-pushed the fix/pin-any-precondition branch from 8b71992 to 496d5e1 Compare March 26, 2026 18:44

MikaelMayer commented Mar 26, 2026

View reviewed changes

StrataTest/Languages/Python/AnalyzeLaurelTest.lean Outdated Show resolved Hide resolved

MikaelMayer commented Mar 26, 2026

View reviewed changes

StrataTest/Languages/Python/AnalyzeLaurelTest.lean Outdated Show resolved Hide resolved

MikaelMayer added 20 commits March 26, 2026 18:48

fix: Address review comments — stateless doc comment, extract isPrelu…

4bb8e91

…deResult helper

fix: Use setupFixture for proper Python env in CI, fix assertion IDs

1611d04

fix: Use #eval with throw instead of #guard_msgs for CI compatibility

a180645

Merge branch 'main' into fix/pin-any-precondition

061762e

fix: Use line comment instead of doc comment before #eval

94ebbc5

fix: Compile test directly without setupFixture dependency

2a0ab20

Merge branch 'main' into fix/pin-any-precondition

8972203

fix: Use runAnalyzeAndVerify which handles the full pipeline

d4c7885

fix: Use splitOn for substring check (String.isInfixOf not available)

fe43181

fix: Inline pipeline without dispatch dependency for standalone test

1403def

fix: Correct Core.verify call signature

b93b977

fix: Update all expected test outputs affected by Any_to_bool Dict/Li…

04a6381

…st change

fix: Update expected test outputs — ❌ fail → ❓ unknown for Any_to_boo…

026e3ff

…l affected assertions

Merge main, resolve expected file conflicts

dd6fc5b

fix: Properly resolve expected file conflicts from main merge

3188afe

revert: Use main expected files as baseline for CI comparison

6978be3

fix: Apply exact expected output changes from CI diff

8bd6978

Merge main, resolve expected file conflicts

c34491b

fix: Update expected outputs with correct pass counts from latest main

543ffed

MikaelMayer added 2 commits March 26, 2026 20:47

Merge branch 'main' into fix/pin-any-precondition

f4e543a

Merge branch 'main' into fix/pin-any-precondition

4d06b2e

MikaelMayer commented Mar 26, 2026

View reviewed changes

StrataTest/Languages/Python/AnalyzeLaurelTest.lean Outdated Show resolved Hide resolved

MikaelMayer commented Mar 26, 2026

View reviewed changes

StrataTest/Languages/Python/Specs/dispatch_test/test_pin_any.py Outdated Show resolved Hide resolved

MikaelMayer added 3 commits March 26, 2026 21:14

simplify: Remove unnecessary class, use parameter directly

46fe14e

test: Move test to shell-based framework with expected file

2e17999

Remove Lean #eval test (requires fake fixture). Use run_py_analyze.sh framework instead: test_pin_any.py in tests/ with expected output in expected_laurel/. Empty expected file — CI will show the correct output.

thanhnguyen-aws previously approved these changes Mar 26, 2026

View reviewed changes

test: Add strata-args directive, generate expected output for test_pi…

d99e146

…n_any

MikaelMayer dismissed thanhnguyen-aws’s stale review via d99e146 March 26, 2026 22:00

MikaelMayer added 5 commits March 26, 2026 22:08

fix: Correct line numbers in expected output to match CI

7a2843c

cleanup: Remove accidentally added files (violated AGENTS.md — never …

23a39eb

…use git add -A)

deprecate: Remove pyAnalyze (non-Laurel) from CI, default to laurel mode

46ca6ac

pyAnalyze is deprecated in favor of pyAnalyzeLaurel. The shell script now defaults to laurel mode. CI no longer runs the non-Laurel pipeline.

Merge branch 'main' into fix/pin-any-precondition

c789011

Merge branch 'main' into fix/pin-any-precondition

d552914

MikaelMayer marked this pull request as ready for review March 27, 2026 01:41

MikaelMayer requested a review from a team March 27, 2026 01:41

MikaelMayer enabled auto-merge March 27, 2026 01:41

joscoh approved these changes Mar 27, 2026

View reviewed changes

Merge branch 'main' into fix/pin-any-precondition

e72c3f7

aqjune-aws approved these changes Mar 27, 2026

View reviewed changes

MikaelMayer added this pull request to the merge queue Mar 27, 2026

Merged via the queue into main with commit 41ae0c1 Mar 27, 2026
15 checks passed

MikaelMayer deleted the fix/pin-any-precondition branch March 27, 2026 03:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

fix: Add Dict and List to Any_to_bool precondition#675

fix: Add Dict and List to Any_to_bool precondition#675
MikaelMayer merged 33 commits intomainfrom
fix/pin-any-precondition

MikaelMayer commented Mar 26, 2026 •

edited

Loading

Uh oh!

This comment was marked as outdated.

This comment was marked as outdated.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joscoh left a comment

Uh oh!

aqjune-aws left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

MikaelMayer commented Mar 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem

Fix

Additional changes

Test

Uh oh!

This comment was marked as outdated.

This comment was marked as outdated.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

joscoh left a comment

Choose a reason for hiding this comment

Uh oh!

aqjune-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

MikaelMayer commented Mar 26, 2026 •

edited

Loading