Skip to content

Commit b5879b9

Browse files
keyboardDrummer-botkeyboardDrummer-bot
authored
Fix missing source locations in Python → Laurel translation (#843)
## Summary Fixes #842 — Adds missing source location metadata in `PythonToLaurel.lean` so that diagnostics in the `expected_laurel` tests no longer report "unknown location". ## Root Cause Three places in `PythonToLaurel.lean` were producing nodes with `defaultMetadata` (which has `FileRange.unknown`) instead of passing through the source location from the Python AST: 1. **Return type constraint ensures** — `pyFuncDefToPythonFunctionDecl` used `returns.ann` (the `Ann` wrapper's annotation, which is `{0,0}` for DDM-generated optional fields) instead of `retTy.ann` (the actual return type expression's source range). 2. **For-loop assume statements** — The `PIn`, `Any_to_bool`, and range-check `Assume` nodes in the `For` case of `translateStmt` used `mkStmtExprMd` (unknown location) instead of `mkStmtExprMdWithLoc` with the for-statement's `md`. 3. **Return statement** — The `LaurelResult` assignment and `Exit "$body"` in the `Return` case used `mkStmtExprMd` instead of `mkStmtExprMdWithLoc` with the return-statement's `md`. ## Changes - `Strata/Languages/Python/PythonToLaurel.lean` — 3 targeted fixes (described above) - `StrataTest/Languages/Python/expected_laurel/*.expected` — 15 test expectation files updated (all `unknown location:` prefixes replaced with actual `file(line, col):` locations) ## Verification - `lake build` succeeds - `run_py_analyze.sh` passes all tests - `grep "^unknown location:" expected_laurel/*.expected` returns zero matches --------- Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
1 parent 5096a68 commit b5879b9

18 files changed

Lines changed: 68 additions & 66 deletions

‎Strata/Languages/Python/PythonToLaurel.lean‎

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1332,9 +1332,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
13321332
let exceptionCheck := getExceptionAssertions ctx e
13331333
-- Coerce Composite return values to Any for LaurelResult : Any
13341334
let e ← coerceToAny ctx expr e
1335-
let assign := mkStmtExprMd (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] e)
1336-
.ok $ exceptionCheck ++ [assign, mkStmtExprMd (StmtExpr.Exit "$body")]
1337-
| none => .ok [mkStmtExprMd (StmtExpr.Exit "$body")]
1335+
let assign := mkStmtExprMdWithLoc (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] e) md
1336+
.ok $ exceptionCheck ++ [assign, mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md]
1337+
| none => .ok [mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md]
13381338
return (ctx, stmts)
13391339

13401340
-- Assert statement
@@ -1495,20 +1495,20 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
14951495
if ¬ (isAnyNone stopExpr && isAnyNone stepExpr) then
14961496
throw (.unsupportedConstruct "Unsupport range function with more than 1 input" (toString (repr iter)))
14971497
let asIntStart := mkStmtExprMd $ .StaticCall "Any..as_int!" [startExpr]
1498-
let emptyRangeExit := mkStmtExprMd $ .IfThenElse
1498+
let emptyRangeExit := mkStmtExprMdWithLoc (.IfThenElse
14991499
(mkStmtExprMd $ .PrimitiveOp .Leq [asIntStart, mkStmtExprMd $ .LiteralInt 0])
15001500
(mkStmtExprMd $ .Exit breakLabel)
1501-
none
1502-
let assumeTypeInt := mkStmtExprMd (.Assume $ mkStmtExprMd (.StaticCall "Any..isfrom_int" [targetVar]))
1501+
none) md
1502+
let assumeTypeInt := mkStmtExprMdWithLoc (.Assume $ mkStmtExprMd (.StaticCall "Any..isfrom_int" [targetVar])) md
15031503
let asIntTarget := mkStmtExprMd $ .StaticCall "Any..as_int!" [targetVar]
15041504
let inRangeExpr := mkStmtExprMd $ .PrimitiveOp .And [
15051505
(mkStmtExprMd $ .PrimitiveOp .Geq [asIntTarget, mkStmtExprMd $ .LiteralInt 0]),
15061506
(mkStmtExprMd $ .PrimitiveOp .Lt [asIntTarget, asIntStart]) ]
1507-
let assumeInRange := mkStmtExprMd (.Assume inRangeExpr)
1507+
let assumeInRange := mkStmtExprMdWithLoc (.Assume inRangeExpr) md
15081508
pure [emptyRangeExit, assumeTypeInt, assumeInRange]
15091509
| _ =>
15101510
let targetInIter := mkStmtExprMd (.StaticCall "PIn" [targetVar, iterExpr])
1511-
let assumeInStmt := mkStmtExprMd (.Assume (Any_to_bool targetInIter))
1511+
let assumeInStmt := mkStmtExprMdWithLoc (.Assume (Any_to_bool targetInIter)) md
15121512
pure [assumeInStmt]
15131513
| _ => pure []
15141514
let bodyStmts := assumeStmts ++ bodyStmts
@@ -1653,11 +1653,13 @@ def pyFuncDefToPythonFunctionDecl (ctx : TranslationContext) (f : Python.stmt S
16531653
let name := match ctx.currentClassName with | none => name.val | some classname => manglePythonMethod classname name.val
16541654
let args_trans ← unpackPyArguments ctx args
16551655
let args := if ctx.currentClassName.isSome then args_trans.fst.tail else args_trans.fst
1656-
let retMd := sourceRangeToMetaData ctx.filePath returns.ann
1657-
let ret ← if name.endsWith "@__init__" then pure $ some ([(name.dropEnd "@__init__".length).toString], retMd)
1656+
let ret ← if name.endsWith "@__init__" then
1657+
let retMd := sourceRangeToMetaData ctx.filePath f.ann
1658+
pure $ some ([(name.dropEnd "@__init__".length).toString], retMd)
16581659
else
16591660
match returns.val with
16601661
| some retTy =>
1662+
let retMd := sourceRangeToMetaData ctx.filePath retTy.ann
16611663
match checkValidInputTypeList ctx (← getArgumentTypes retTy) with
16621664
| .ok tys => pure (tys, retMd)
16631665
| _ => pure none

‎StrataTest/Languages/Python/expected_laurel/test_break_continue.expected‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
test_break_continue.py(3, 10): ✅ pass - Check PNot exception
22
test_break_continue.py(3, 4): ✅ pass - loop_guard_calls_Any_to_bool_0
3-
unknown location: ✅ pass - (test_while_break ensures) Return type constraint
3+
test_break_continue.py(1, 26): ✅ pass - (test_while_break ensures) Return type constraint
44
test_break_continue.py(8, 10): ✅ pass - Check PNot exception
55
test_break_continue.py(8, 4): ✅ pass - loop_guard_calls_Any_to_bool_0
66
test_break_continue.py(8, 4): ✅ pass - loop_guard_end_calls_Any_to_bool_0
7-
unknown location: ✅ pass - (test_while_continue ensures) Return type constraint
8-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
9-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
10-
unknown location: ✅ pass - (test_for_break ensures) Return type constraint
11-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
12-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
13-
unknown location: ✅ pass - (test_for_continue ensures) Return type constraint
7+
test_break_continue.py(6, 29): ✅ pass - (test_while_continue ensures) Return type constraint
8+
test_break_continue.py(14, 4): ✅ pass - assume_assume(267)_calls_PIn_0
9+
test_break_continue.py(14, 4): ✅ pass - assume_assume(267)_calls_Any_to_bool_1
10+
test_break_continue.py(12, 24): ✅ pass - (test_for_break ensures) Return type constraint
11+
test_break_continue.py(19, 4): ✅ pass - assume_assume(362)_calls_PIn_0
12+
test_break_continue.py(19, 4): ✅ pass - assume_assume(362)_calls_Any_to_bool_1
13+
test_break_continue.py(17, 27): ✅ pass - (test_for_continue ensures) Return type constraint
1414
DETAIL: 13 passed, 0 failed, 0 inconclusive
1515
RESULT: Analysis success

‎StrataTest/Languages/Python/expected_laurel/test_bug_finding_unreachable.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ test_bug_finding_unreachable.py(5, 11): ✔️ always true if reached - Check PL
66
test_bug_finding_unreachable.py(5, 8): ✔️ always true if reached - ite_cond_calls_Any_to_bool_0
77
test_bug_finding_unreachable.py(6, 12): ❌ fail (❗path unreachable) - dead code
88
test_bug_finding_unreachable.py(6, 12): ❌ fail (❗path unreachable) - dead code
9-
unknown location: ✔️ always true if reached - (test_bug_finding_unreachable ensures) Return type constraint
9+
test_bug_finding_unreachable.py(2, 44): ✔️ always true if reached - (test_bug_finding_unreachable ensures) Return type constraint
1010
DETAIL: 6 passed, 3 failed, 0 inconclusive, 2 unreachable
1111
RESULT: Failures found

‎StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
test_class_field_use.py(19, 11): ❓ unknown - Check PMul exception
2-
unknown location: ❓ unknown - (process_buffer ensures) Return type constraint
2+
test_class_field_use.py(18, 43): ❓ unknown - (process_buffer ensures) Return type constraint
33
test_class_field_use.py(14, 4): ✔️ always true if reached - Check PMul exception
44
test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work
55
test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work

‎StrataTest/Languages/Python/expected_laurel/test_deep_inline.expected‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
test_deep_inline.py(3, 11): ✔️ always true if reached - Check PAdd exception
2-
unknown location: ✔️ always true if reached - (inc ensures) Return type constraint
2+
test_deep_inline.py(2, 19): ✔️ always true if reached - (inc ensures) Return type constraint
33
test_deep_inline.py(6, 4): ✔️ always true if reached - Check PAdd exception
44
test_deep_inline.py(7, 11): ✔️ always true if reached - Check PMul exception
5-
unknown location: ✔️ always true if reached - (double_inc ensures) Return type constraint
5+
test_deep_inline.py(5, 26): ✔️ always true if reached - (double_inc ensures) Return type constraint
66
test_deep_inline.py(6, 4): ✔️ always true if reached - Check PAdd exception
77
test_deep_inline.py(10, 4): ✔️ always true if reached - Check PMul exception
88
test_deep_inline.py(11, 4): ✔️ always true if reached - Check PAdd exception
9-
unknown location: ✔️ always true if reached - (triple_apply ensures) Return type constraint
9+
test_deep_inline.py(9, 28): ✔️ always true if reached - (triple_apply ensures) Return type constraint
1010
test_deep_inline.py(10, 4): ✔️ always true if reached - Check PAdd exception
1111
test_deep_inline.py(10, 4): ✔️ always true if reached - Check PMul exception
1212
test_deep_inline.py(11, 4): ✔️ always true if reached - Check PAdd exception

‎StrataTest/Languages/Python/expected_laurel/test_default_params.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
test_default_params.py(2, 18): ✅ pass - Check PAdd exception
2-
unknown location: ✅ pass - (greet ensures) Return type constraint
2+
test_default_params.py(1, 49): ✅ pass - (greet ensures) Return type constraint
33
test_default_params.py(8, 10): ✅ pass - Check PLt exception
44
test_default_params.py(8, 4): ✅ pass - loop_guard_calls_Any_to_bool_0
55
test_default_params.py(9, 17): ❓ unknown - Check PMul exception
66
test_default_params.py(10, 12): ✅ pass - Check PAdd exception
77
test_default_params.py(8, 4): ✅ pass - loop_guard_end_calls_Any_to_bool_0
8-
unknown location: ❓ unknown - (power ensures) Return type constraint
8+
test_default_params.py(5, 38): ❓ unknown - (power ensures) Return type constraint
99
test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of name
1010
test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of greeting
1111
test_default_params.py(15, 4): ✅ pass - default greeting failed

‎StrataTest/Languages/Python/expected_laurel/test_for_else_break.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
2-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
1+
test_for_else_break.py(3, 4): ✅ pass - assume_assume(46)_calls_PIn_0
2+
test_for_else_break.py(3, 4): ✅ pass - assume_assume(46)_calls_Any_to_bool_1
33
test_for_else_break.py(4, 8): ✅ pass - ite_cond_calls_Any_to_bool_0
44
test_for_else_break.py(8, 4): ✅ pass - for else skipped on break
55
test_for_else_break.py(8, 4): ✅ pass - for else skipped on break

‎StrataTest/Languages/Python/expected_laurel/test_for_loop.expected‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
1-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
2-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
1+
test_for_loop.py(4, 4): ✅ pass - assume_assume(83)_calls_PIn_0
2+
test_for_loop.py(4, 4): ✅ pass - assume_assume(83)_calls_Any_to_bool_1
33
test_for_loop.py(5, 16): ✅ pass - Check PAdd exception
44
test_for_loop.py(6, 4): ✅ pass - sum of list should be 15
55
test_for_loop.py(6, 4): ❓ unknown - sum of list should be 15
6-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
7-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
6+
test_for_loop.py(12, 4): ✅ pass - assume_assume(293)_calls_PIn_0
7+
test_for_loop.py(12, 4): ✅ pass - assume_assume(293)_calls_Any_to_bool_1
88
test_for_loop.py(13, 11): ✅ pass - Check PGt exception
99
test_for_loop.py(13, 8): ✅ pass - ite_cond_calls_Any_to_bool_0
1010
test_for_loop.py(14, 20): ✅ pass - Check PAdd exception
1111
test_for_loop.py(15, 4): ✅ pass - should count 3 items greater than 3
1212
test_for_loop.py(15, 4): ❓ unknown - should count 3 items greater than 3
13-
unknown location: ✅ pass - assume_assume(0)_calls_PIn_0
14-
unknown location: ✅ pass - assume_assume(0)_calls_Any_to_bool_1
13+
test_for_loop.py(21, 4): ✅ pass - assume_assume(531)_calls_PIn_0
14+
test_for_loop.py(21, 4): ✅ pass - assume_assume(531)_calls_Any_to_bool_1
1515
test_for_loop.py(22, 8): ✅ pass - ite_cond_calls_Any_to_bool_0
1616
test_for_loop.py(25, 4): ✅ pass - should have found 30
1717
test_for_loop.py(25, 4): ✅ pass - should have found 30

‎StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
test_func_input_type_constraints.py(4, 11): ✅ pass - Check PMul exception
2-
unknown location: ✅ pass - (Mul ensures) Return type constraint
2+
test_func_input_type_constraints.py(3, 48): ✅ pass - (Mul ensures) Return type constraint
33
test_func_input_type_constraints.py(7, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
4-
unknown location: ✅ pass - (Sum ensures) Return type constraint
4+
test_func_input_type_constraints.py(6, 62): ✅ pass - (Sum ensures) Return type constraint
55
test_func_input_type_constraints.py(9, 11): ✅ pass - Check PAdd exception
6-
unknown location: ✅ pass - (Sum ensures) Return type constraint
7-
unknown location: ❓ unknown - set_LaurelResult_calls_Any_get_0
8-
unknown location: ❓ unknown - set_LaurelResult_calls_Any_get_1
9-
unknown location: ❓ unknown - (List_Dict_index ensures) Return type constraint
6+
test_func_input_type_constraints.py(6, 62): ✅ pass - (Sum ensures) Return type constraint
7+
test_func_input_type_constraints.py(12, 4): ❓ unknown - set_LaurelResult_calls_Any_get_0
8+
test_func_input_type_constraints.py(12, 4): ❓ unknown - set_LaurelResult_calls_Any_get_1
9+
test_func_input_type_constraints.py(11, 65): ❓ unknown - (List_Dict_index ensures) Return type constraint
1010
test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of x
1111
test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of y
1212
test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of x

‎StrataTest/Languages/Python/expected_laurel/test_if_elif.expected‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
test_if_elif.py(2, 7): ✅ pass - Check PLt exception
22
test_if_elif.py(2, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
3-
unknown location: ✅ pass - (classify ensures) Return type constraint
3+
test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint
44
test_if_elif.py(4, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
5-
unknown location: ✅ pass - (classify ensures) Return type constraint
5+
test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint
66
test_if_elif.py(6, 9): ✅ pass - Check PLt exception
77
test_if_elif.py(6, 4): ✅ pass - ite_cond_calls_Any_to_bool_0
8-
unknown location: ✅ pass - (classify ensures) Return type constraint
9-
unknown location: ✅ pass - (classify ensures) Return type constraint
8+
test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint
9+
test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint
1010
test_if_elif.py(12, 23): ✅ pass - Check PNeg exception
1111
test_if_elif.py(12, 4): ✅ pass - (classify requires) Type constraint of x
1212
test_if_elif.py(13, 4): ✅ pass - should be negative

0 commit comments

Comments
 (0)