diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index d9c494a3a..26724bc2e 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -482,13 +482,37 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang | _ => throw (.unsupportedConstruct s!"Unary operator not yet supported: {repr op}" (toString (repr e))) return mkStmtExprMd (StmtExpr.StaticCall preludeOpnames [operandExpr]) - -- JoinedStr (f-strings) - return first part until we have string concat + -- FormattedValue (f-string interpolation {expr}) - convert to string-typed Any + | .FormattedValue _ value _ _ => + let ty ← inferExprType ctx value + let inner ← translateExpr ctx value + let asAny ← if ty ∈ ctx.compositeTypeNames then + let fields := (ctx.classFieldHighType[ty]?.getD {}).toList + let dict ← fields.foldlM (fun acc (fname, fty) => + return mkStmtExprMd (.StaticCall "DictStrAny_cons" + [mkStmtExprMd (.LiteralString fname), + ← wrapFieldInAny fty (mkStmtExprMd (.FieldSelect inner fname)), acc])) + (mkStmtExprMd (.StaticCall "DictStrAny_empty" [])) + pure <| mkStmtExprMd (.StaticCall "from_ClassInstance" + [mkStmtExprMd (.LiteralString ty), dict]) + else pure inner + return mkStmtExprMd (.StaticCall "to_string_any" [asAny]) + + -- JoinedStr (f-strings) - concatenate string parts via str.concat | .JoinedStr _ values => if values.val.isEmpty then - return mkStmtExprMd (StmtExpr.LiteralString "") + return strToAny "" else - let first ← translateExpr ctx values.val[0]! - return first + let parts ← values.val.toList.mapM (translateExpr ctx ·) + let unwrap (e : StmtExprMd) := mkStmtExprMd (.StaticCall "Any..as_string!" [e]) + let concat := parts.foldl (fun acc part => + mkStmtExprMd (.PrimitiveOp .StrConcat [acc, unwrap part])) + (mkStmtExprMd (.LiteralString "")) + return mkStmtExprMd (.StaticCall "from_string" [concat]) + + -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported + | .Interpolation .. => return mkStmtExprMd .Hole + | .TemplateStr .. => return mkStmtExprMd .Hole | .Call _ f args kwargs => translateCall ctx f args.val.toList kwargs.val.toList @@ -617,8 +641,10 @@ partial def inferExprType (ctx : TranslationContext) (e: Python.expr SourceRange -- Unary operations | .UnaryOp _ _ _ => return PyLauType.Any - -- JoinedStr (f-strings) - return first part until we have string concat - | .JoinedStr _ _ => return PyLauType.Any + -- JoinedStr (f-strings) produce strings + | .JoinedStr _ _ => return PyLauType.Str + -- FormattedValue produces string-typed Any + | .FormattedValue _ _ _ _ => return PyLauType.Str | .Call _ f args _ => getFunctionReturnType ctx f args.val diff --git a/StrataTest/Languages/Python/expected_laurel/test_fstrings.expected b/StrataTest/Languages/Python/expected_laurel/test_fstrings.expected new file mode 100644 index 000000000..8dafe3cfc --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_fstrings.expected @@ -0,0 +1,37 @@ + +==== Verification Results ==== +List_get_body_calls_List_get_0: ✅ pass +List_take_body_calls_List_take_0: ✅ pass +List_drop_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_take_1: ✅ pass +List_set_body_calls_List_set_0: ✅ pass +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_List_get_1: ✅ pass +Any_get_body_calls_List_slice_2: ✅ pass +Any_get_body_calls_List_drop_3: ✅ pass +Any_get!_body_calls_DictStrAny_get_0: ✅ pass +Any_get!_body_calls_List_get_1: ✅ pass +Any_set_body_calls_List_set_0: ✅ pass +Any_set!_body_calls_List_set_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass +PAnd_body_calls_Any_to_bool_0: ✅ pass +POr_body_calls_Any_to_bool_0: ✅ pass +ret_type: ✅ pass (in prelude file) +ret_type: ✅ pass (in prelude file) +ret_pos: ✅ pass (in prelude file) +assert_name_is_foo: ✅ pass (in prelude file) +assert_opt_name_none_or_str: ✅ pass (in prelude file) +assert_opt_name_none_or_bar: ✅ pass (in prelude file) +ensures_maybe_except_none: ✅ pass (in prelude file) +assert_assert(196)_calls_Any_to_bool_0: ✅ pass (at line 6, col 4) +assert(196): ❓ unknown (at line 6, col 4) +assert_assert(430)_calls_Any_to_bool_0: ✅ pass (at line 13, col 4) +assert(430): ✅ pass (at line 13, col 4) +assert_assert(511)_calls_Any_to_bool_0: ✅ pass (at line 15, col 4) +assert(511): ✅ pass (at line 15, col 4) +ite_cond_calls_Any_to_bool_0: ✅ pass diff --git a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected index 786f4dd6c..ddd81ccb1 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected @@ -28,6 +28,8 @@ assert_name_is_foo: ✅ pass (in prelude file) assert_opt_name_none_or_str: ✅ pass (in prelude file) assert_opt_name_none_or_bar: ✅ pass (in prelude file) ensures_maybe_except_none: ✅ pass (in prelude file) +call_print_arg_calls_Any_get_0: ❓ unknown (at line 8, col 4) +call_print_arg_calls_Any_get_1: ❓ unknown (at line 8, col 4) (Origin_test_helper_procedure_Requires)req_name_is_foo: ❓ unknown (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str: ✅ pass (in prelude file) (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar: ✅ pass (in prelude file) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index d943fce76..b7dec8a8c 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -21,7 +21,7 @@ BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"} SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement", "test_class_field_init", "test_break_continue", "test_try_except", "test_try_except_scoping", - "test_augmented_assign", "test_list_slice"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign + "test_augmented_assign", "test_list_slice", "test_fstrings"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign SKIP_TESTS_LAUREL = BOTH_SKIP diff --git a/StrataTest/Languages/Python/tests/test_fstrings.py b/StrataTest/Languages/Python/tests/test_fstrings.py new file mode 100644 index 000000000..d4379ce4e --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_fstrings.py @@ -0,0 +1,18 @@ +def main(): + # F-string basics: variable interpolation, multiple parts, surrounding literals + name: str = "world" + tag: str = "ok" + greeting: str = f"hello {name}, status=[{tag}]" + assert greeting == "hello world, status=[ok]", "f-string interpolation failed" + + # F-string edge cases: empty, no interpolation, integer expression + x: int = 3 + y: int = 4 + msg: str = f"{x} + {y}" + empty: str = f"" + assert empty == "", "empty f-string failed" + plain: str = f"literal only" + assert plain == "literal only", "f-string no interpolation failed" + +if __name__ == "__main__": + main()