Classify division-by-zero checks as distinct property type#514
Open
tautschnig wants to merge 6 commits intomainfrom
Open
Classify division-by-zero checks as distinct property type#514tautschnig wants to merge 6 commits intomainfrom
tautschnig wants to merge 6 commits intomainfrom
Conversation
Extend PropertyType with a divisionByZero variant so that verification results from safe division/modulo preconditions are distinguishable from regular assertions. PrecondElim attaches a propertyType metadata tag based on the function name (Int.SafeDiv*, Int.SafeMod*), which CmdEval reads when creating proof obligations. The classification propagates to both text output (Property: division by zero check) and SARIF output (kind: division-by-zero). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
tautschnig/classify-division-by-zero
branch
from
460165c to
ed5408c
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR extends Strata’s proof-obligation pipeline to distinguish division-by-zero precondition checks from ordinary assertions, and propagates that classification through verification and reporting (text + SARIF). It also introduces safe truncating division/mod operators and updates translation/parsing layers and tests accordingly.
Changes:
- Add
divisionByZeroas a distinctPropertyType, and tag generated precondition asserts via metadata inPrecondElim, then decode it inCmdEval. - Emit the property classification in SARIF output and update SARIF-related tests/fixtures.
- Add
Int.SafeDivT/Int.SafeModTsupport across factories/SMT encoder/grammar/translation, and update expected outputs and end-to-end tests.
Reviewed changes
Copilot reviewed 24 out of 24 changed files in this pull request and generated 4 comments.
Show a summary per file
| File | Description |
|---|---|
| StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected | Updates expected VC list to include SafeDiv precondition obligation. |
| StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean | New end-to-end Laurel test covering safe vs unsafe division. |
| StrataTest/Languages/Core/SarifOutputTests.lean | Updates expected SARIF JSON to include the new result classification field. |
| StrataTest/Languages/Core/ProgramTypeTests.lean | Updates expected Core prelude/program types to include Int.SafeDivT/Int.SafeModT. |
| StrataTest/Languages/Core/ProcedureEvalTests.lean | Updates expected procedure-eval environment/types for new safe truncating ops. |
| StrataTest/Languages/Core/Examples/NoFilterWFProc.lean | Updates expected “Property:” rendering for SafeDiv-generated obligations. |
| StrataTest/Languages/Core/Examples/Loops.lean | Updates expected property rendering for loop-related SafeDiv obligations. |
| StrataTest/Languages/Core/Examples/FunctionPreconditions.lean | Updates expected property rendering for SafeDiv obligations in multiple examples. |
| StrataTest/DL/Lambda/TestGenTests.lean | Updates expected operator factory list to include safe truncating ops. |
| Strata/Util/Sarif.lean | Extends SARIF Result structure with a classification field (serialized as kind). |
| Strata/Transform/PrecondElim.lean | Tags generated precondition asserts with propertyType metadata based on callee name. |
| Strata/Languages/Python/PythonToLaurel.lean | Improves source-location propagation into translated Laurel statements/expressions. |
| Strata/Languages/Laurel/LaurelToCoreTranslator.lean | Translates Laurel div/mod (incl. truncating) to Core safe operators. |
| Strata/Languages/Core/Verifier.lean | Treats divisionByZero similarly to assert in preprocessing shortcuts. |
| Strata/Languages/Core/SarifOutput.lean | Maps PropertyType to SARIF output classification string. |
| Strata/Languages/Core/SMTEncoder.lean | Encodes Int.SafeDivT/Int.SafeModT using the same SMT encoding as truncating ops. |
| Strata/Languages/Core/Factory.lean | Adds safe truncating ops to well-formedness factory and exposes operator expressions. |
| Strata/Languages/Core/DDMTransform/Translate.lean | Adds translation support for truncating and safe truncating ops in the DDM layer. |
| Strata/Languages/Core/DDMTransform/Grammar.lean | Extends grammar with /t, %t and explicit truncating operator forms. |
| Strata/Languages/Core/DDMTransform/ASTtoCST.lean | Adds CST construction for the new truncating/safe truncating operator names. |
| Strata/DL/Lambda/IntBoolFactory.lean | Defines Int.SafeDivT/Int.SafeModT with divisor-nonzero preconditions and registers them. |
| Strata/DL/Imperative/MetaData.lean | Introduces propertyType metadata field + accessor. |
| Strata/DL/Imperative/EvalContext.lean | Adds divisionByZero constructor to PropertyType and updates formatting. |
| Strata/DL/Imperative/CmdEval.lean | Decodes propertyType metadata to set ProofObligation.property accordingly. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Move the property classification from the non-standard 'kind' field to a SARIF-compliant 'properties' bag with a 'propertyType' entry. Rename propertyTypeToRuleKind to propertyTypeToClassification to reflect its updated purpose. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Use MetaData.getPropertyType in createUnreachableAssertObligations instead of hardcoding PropertyType.assert, so that unreachable division-by-zero checks retain their property classification. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
shigoel
reviewed
Mar 5, 2026
shigoel
reviewed
Mar 5, 2026
shigoel
reviewed
Mar 5, 2026
shigoel
reviewed
Mar 5, 2026
shigoel
reviewed
Mar 5, 2026
shigoel
requested changes
Mar 5, 2026
Contributor
shigoel
left a comment
shigoel
left a comment
There was a problem hiding this comment.
LGTM in general, but I'd like hard-coded/magic strings to go away.
Add MetaData.divisionByZero constant and use MetaData.getPropertyType accessor consistently across CmdEval, StatementEval, and PrecondElim, eliminating magic strings for property type classification. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.
Description of changes:
Extend PropertyType with a divisionByZero variant so that verification results from safe division/modulo preconditions are distinguishable from regular assertions. PrecondElim attaches a propertyType metadata tag based on the function name (Int.SafeDiv*, Int.SafeMod*), which CmdEval reads when creating proof obligations. The classification propagates to both text output (Property: division by zero check) and SARIF output (kind: division-by-zero).
Co-authored-by: Kiro kiro-agent@users.noreply.github.com
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.