Conversation
…riginal location (#706) During procedure inlining, assertions in the callee body now carry the call site metadata as the primary file range, with the original assertion location stored as a related file range. This allows error reporting to show the procedure call location first, with the original assertion as a related position. Changes: - Add relatedFileRange metadata field and setCallSiteFileRange helper - Update ProcedureInlining to set call site metadata on inlined assertions - Display related positions in pyAnalyze and pyAnalyzeLaurel output - Add RelatedLocation to SARIF output for related positions - Update SARIF test expected outputs for new relatedLocations field
|
|
||
| /-- Metadata field for a related file range (e.g., the original assertion location | ||
| when the primary file range points to the call site after inlining). -/ | ||
| def MetaData.relatedFileRange : MetaDataElem.Field P := .label "relatedFileRange" |
There was a problem hiding this comment.
There might be more than one inlining, so related file ranges should be ordered. For every inlining, the related file ranges should shift as well.
There was a problem hiding this comment.
Updated setCallSiteFileRange to support multiple inlinings. It now collects existing related file ranges, clears them, prepends the current primary range as the first related range, then appends the previously existing related ranges. This preserves ordering: the most recent inlining's original location comes first, followed by earlier ones.
Strata/DL/Imperative/MetaData.lean
Outdated
| def MetaData.relatedFileRange : MetaDataElem.Field P := .label "relatedFileRange" | ||
|
|
||
| /-- Get the related file range from metadata, if present. -/ | ||
| def getRelatedFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option FileRange := do |
There was a problem hiding this comment.
There might be more than one related file range.
There was a problem hiding this comment.
Changed getRelatedFileRange (returning Option FileRange) to getRelatedFileRanges (returning Array FileRange), which collects all metadata elements with the relatedFileRange field. Updated all callers: SARIF output now emits all related locations with sequential IDs, and the CLI output formats all related positions.
| Strata.Sarif.toJsonString sarif | ||
|
|
||
| /-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/ | ||
| /-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"relatedLocations\":[],\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/ |
There was a problem hiding this comment.
Nice to update this but I would like to see a test that displays related locations. Look into the python specification tests, there is a place where we inline a procedure. Look at StrataTest/Languages/Python/AnalyzeLaurelTest.lean and messages like Storage_Storage_put_item_assert(0)_9: ✔️ always true if reached (Required parameter 'Bucket' is missing).
First you should update the messages to include line and column number and remove the assertion names that are not human-readable. Then verify that with your approach, it indicates the assertion's line and column number to be at the call site.
There was a problem hiding this comment.
Added a SARIF test that constructs metadata with setCallSiteFileRange (simulating inlining) and verifies the related location appears in the SARIF JSON output with the correct line/column.
Regarding the Python spec test updates (updating messages to include line/column, removing non-human-readable assertion names, and verifying call site location through the full pipeline) — this is a larger change that touches the Python pipeline output formatting. I can tackle that as a follow-up if you'd like, or address it in this PR with more guidance on the expected output format.
- Change getRelatedFileRange to getRelatedFileRanges returning Array FileRange - Add MetaData.eraseAllElems to remove all elements with a given field - Update setCallSiteFileRange to preserve existing related ranges on each inlining - Update extractRelatedLocations in SARIF output to emit all related locations - Update formatRelatedPositions in StrataMain to display all related locations - Add SARIF test with related locations from inlining
1 participant
Fixes #706
During procedure inlining, assertions in the callee body now carry the call site metadata as the primary file range, with the original assertion location stored as a related file range. This allows error reporting to show the procedure call location first, with the original assertion as a related position.
relatedFileRangemetadata field andsetCallSiteFileRangehelper to combine call site and original assertion metadataProcedureInlining.inlineCallCmdto set call site metadata on inlined assertions, assumes, and coverspyAnalyzeandpyAnalyzeLaureloutputRelatedLocationto SARIF output for related positionsrelatedLocationsfieldTested: existing tests pass, SARIF test outputs updated.