Skip to content
Open
22 changes: 20 additions & 2 deletions Strata/Languages/Python/PythonToLaurel.lean
Original file line number Diff line number Diff line change
Expand Up @@ -991,6 +991,22 @@ partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRan
pure <| mkStmtExprMd (.Hole)
else pure translated

/-- Coerce each argument whose corresponding parameter type is Any.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I will reiterate what I said in the other PRs. In the current modeling, we assume that values of type Any are never composite since toString is a function that does not depend on the heap. Whereas by construction it was not possible to hit this soundness issue before, this PR would concretize the soundness issue by making it possible to cast a composite into an Any.

The solution is obviously to make toString a bodiless procedure and not a bodiless function and declare that this procedure modifies the heap.

Arguments aligned with non-Any parameters are kept unchanged.
When `fd` is `none` or the argument index exceeds the parameter list,
the argument is left unchanged (we cannot determine the target type). -/
partial def coerceArgsToAny (ctx : TranslationContext)
(args : List (Python.expr SourceRange))
(rawTransArgs : List StmtExprMd)
(fd : Option PythonFunctionDecl) : Except TranslationError (List StmtExprMd) := do
let paramTypeNames : Array String := match fd with
| some fd => (fd.args.map fun a => highTypeToPyLauType a.laurelType.val).toArray
| none => #[]
(args.zip rawTransArgs).zipIdx.mapM fun ((orig, trans), i) =>
match paramTypeNames[i]? with
| some ty => if ty == PyLauType.Any then coerceToAny ctx orig trans else pure trans
| none => pure trans

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Design trade-off introduced in d8d233de: the none arm leaves unknown-parameter-type arguments uncoerced. Walked the reasoning with the commit message:

  • test_class_field_use has process_buffer(my_buf) called before process_buffer's signature is registered, so funcDecl = none. With the previous "coerce on unknown" behaviour, my_buf (a typed-Composite CircularBuffer) would become a Hole, and buf.buffer inside the function body would fail to dispatch. The new "leave on unknown" behaviour fixes that.
  • The symmetric case is unknown_func(composite_val) where unknown_func happens to have an Any parameter. Under the old behaviour this worked (coerced to Hole). Under the new behaviour, the original Internal error when accessing a field from a Any typed composite #875 Impossible to unify Any with Composite is back for this specific shape.

The test_class_field_use evidence says the new behaviour is right for real code. But the #875 hazard-in-this-shape is now undocumented and unguarded.

Suggestion: add a fixture under dispatch_test/ that exercises the unknown-function-with-Any-parameter path — even as .failPrefix expecting the unification error if that's what the current behaviour produces. Pins the trade-off so a future "let's coerce unknown" refactor silently flipping the direction is caught. Two minutes of work; turns an implicit decision into an explicit regression test.

Alternative if the trade-off is judged clean: a one-line doc-comment on the none arm (-- See #875: we may get a unification error here if the unknown function's param is Any, but coercing on unknown broke test_class_field_use where a typed-Composite forward reference was being turned into Hole). No code change, just surfaces the decision for future readers.


partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
Except TranslationError (String × Option (Python.expr SourceRange) × Bool) := do
match func with
Expand Down Expand Up @@ -1271,7 +1287,8 @@ partial def translateCall (ctx : TranslationContext)
if args.length > funcDecl.args.length then
throwUserError callRange
s!"'{name}' called with too many positional arguments: expected at most {funcDecl.args.length}, got {args.length}"
let trans_posArgs ← args.mapM (translateExpr ctx)
let rawPosArgs ← args.mapM (translateExpr ctx)
let trans_posArgs ← coerceArgsToAny ctx args rawPosArgs (some funcDecl)
let trans_dict ← translateVarKwargs ctx kwords
let remainingParams := funcDecl.args.drop args.length
let trans_dictArgs := remainingParams.map fun arg =>
Expand Down Expand Up @@ -1302,7 +1319,8 @@ partial def translateCall (ctx : TranslationContext)
else
let (args, kwords, funcdecl_hasKwargs) ←
combinePositionalAndKeywordArgs args kwords funcDecl methodName callRange
let trans_args ← args.mapM (translateExpr ctx)
let rawTransArgs ← args.mapM (translateExpr ctx)
let trans_args ← coerceArgsToAny ctx args rawTransArgs funcDecl
let trans_kwords ← translateKwargs ctx kwords
let trans_kwords_exprs :=
if kwords.length == 0 then
Expand Down
6 changes: 6 additions & 0 deletions StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,12 @@ private meta def testCases : List (String × Expected) := [
.mk "test_annotation_dispatch.py" .success,
.mk "test_constructor_dispatch.py" .success,
.mk "test_reassign_dispatch.py" .success,
-- Composite argument passed to untyped (Any) parameter: coercion must prevent type error
Comment thread
olivier-aws marked this conversation as resolved.
.mk "test_composite_arg_to_any_param.py" .success,
-- Composite argument passed via **kwargs to untyped parameter (exercises isVarKwargs branch)
.mk "test_composite_arg_to_any_param_kwargs.py" .success,
-- Composite argument passed to explicitly typed Composite parameter: must NOT be coerced
.mk "test_composite_arg_typed_param.py" .success,
-- Known failing tests:
-- With @ separator, Storage_put_item is no longer a known symbol, so it
-- falls through to the default Any type. These should produce an
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# Test: passing a dispatch-created Composite value to a function with untyped parameter.
# Before the fix, this caused "Impossible to unify Any with Composite" because
# the factory dispatch produces a Composite-typed value but the function parameter
# defaults to Any.
import servicelib


def use_storage(client):
client.put_item(Bucket="test", Key="k", Data="v")


use_storage(servicelib.connect("storage"))
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Test: passing a dispatch-created Composite value as a positional argument
# alongside **kwargs expansion. This exercises the first coerceArgsToAny call
# site (the isVarKwargs branch) where positional args precede the dict expansion.
import servicelib


def use_client(client, Bucket, Key, Data):
client.put_item(Bucket=Bucket, Key=Key, Data=Data)


def call_with_kwargs():
extra = {"Bucket": "b", "Key": "k", "Data": "v"}
use_client(servicelib.connect("storage"), **extra)
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Test: a Composite-typed field (self.client: Storage) is passed to a function
# with an untyped parameter. The Composite is coerced to Any at the call site,
# but inside the class method where the field is used directly, dispatch still
# works because the field retains its Composite type.
import servicelib


class StorageUser:
def __init__(self):
self.client: Storage = servicelib.connect("storage")

def do_put(self):
self.client.put_item(Bucket="b", Key="k", Data="d")
Loading