Support for f-strings in Python->Laurel translation + bind variables introduced by exception handlers

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
 

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

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)

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
 
 

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()