Fix multi-output procedure handling: Unknown fallback and prelude withException detection#726
Merged
Fix multi-output procedure handling: Unknown fallback and prelude withException detection#726
Conversation
…edures computeExprType returned TVoid for procedures with multiple outputs (e.g., timedelta_func returning (delta : Any, maybe_except : Error)). TVoid is translated to bool in Core, causing "Impossible to unify bool with Any" when the lifted call result variable is used in an Any context. Fix: match on firstOutput :: _ instead of [singleOutput], returning the first output type for any non-empty output list. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Fixes Laurel type computation for static calls to multi-output procedures by returning the first output type (instead of defaulting to TVoid), preventing downstream Core unification failures (e.g., bool vs Any) when the lifted call result is used as a value.
Changes:
- Update
computeExprTypeto return the first output type for any non-emptyproc.outputslist. - Add a Python regression test covering
datetime - timedeltausage. - Register the new Python test expectation in the CBMC pipeline expected-results list.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| Strata/Languages/Laurel/LaurelTypes.lean | Fixes static procedure call expression typing by using the first declared output type. |
| StrataTest/Languages/Python/tests/test_timedelta_expr.py | Adds a regression test exercising datetime/timedelta expression typing/translation. |
| StrataTest/Languages/Python/tests/cbmc_expected.txt | Marks the new test as expected PASS in the Python CBMC pipeline. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
The comment said we don't track return types and fall back to TVoid, but the implementation now returns the first declared output type when available. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Exercise datetime/timedelta arithmetic through the full Python → Laurel → Core → SMT pipeline, verifying that multi-output procedures return the correct first output type instead of TVoid. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
shigoel
previously approved these changes
Apr 1, 2026
keyboardDrummer
requested changes
Apr 2, 2026
Per keyboardDrummer's review: multi-output procedures used as expressions don't have a meaningful single type. Return Unknown instead of picking the first output or falling back to TVoid. Unknown translates to Any in Core, which avoids the original 'Impossible to unify bool with Any' error (TVoid→bool was the cause). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…eption withException only checked importedSymbols for multi-output procedures, missing prelude procedures like timedelta_func. Add preludeProcedures field to TranslationContext and check it in withException so that calls to multi-output prelude procedures correctly generate 2-target assignments (result + maybe_except). This is the root cause fix for the timedelta type mismatch: the translator now generates 'call [delta, maybe_except] := timedelta_func()' instead of 'call [delta] := timedelta_func()'. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
changed the title
MikaelMayer
reviewed
Apr 3, 2026
- Deduplicate the output-check expression into hasErrorOutput helper - Update test comment to make explicit that timedelta_func exercises the multi-output prelude procedure path (withException + computeExprType) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
MikaelMayer
previously approved these changes
Apr 3, 2026
keyboardDrummer
previously approved these changes
Apr 4, 2026
Contributor
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Thanks, this is great. Ideally we would also add error reporting to Laurel to detect the incorrect Laurel that was generated before, but it would be a bonus :)
github-merge-queue
bot
removed this pull request from the merge queue due to a conflict with the base branch
shigoel
previously approved these changes
Apr 6, 2026
Contributor
shigoel
left a comment
shigoel
left a comment
There was a problem hiding this comment.
Happy to approve again when the merge conflicts are resolved.
# Conflicts: # StrataTest/Languages/Python/VerifyPythonTest.lean # StrataTest/Languages/Python/tests/cbmc_expected.txt
tautschnig
dismissed stale reviews from shigoel, keyboardDrummer, and MikaelMayer
via
4cab005
shigoel
approved these changes
Apr 6, 2026
MikaelMayer
approved these changes
Apr 6, 2026
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
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.
Problem
timedelta(days=7)caused a Core type checking error "Impossible to unify bool with Any" because:computeExprTypereturnedTVoidfor multi-output procedures (e.g.,timedelta_funcreturning(delta: Any, maybe_except: Error)).TVoidtranslates toboolin Core, causing the confusing error.withExceptionin PythonToLaurel only checkedimportedSymbolsfor multi-output procedures, missing prelude procedures liketimedelta_func. This caused the translator to generate a single-target assignment instead of the required 2-target assignmentcall [delta, maybe_except] := timedelta_func(...).Fix
computeExprType (LaurelTypes.lean): Return
Unknowninstead ofTVoidfor zero-output and multi-output procedures.Unknowntranslates toAnyin Core, which avoids the type mismatch. Single-output procedures continue to return their declared output type.withException (PythonToLaurel.lean): Add
preludeProceduresfield toTranslationContextand extendwithExceptionto check prelude procedure signatures. This ensures multi-output prelude procedureslike
timedelta_funccorrectly generate 2-target assignments.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.