Skip to content

Fix a bug in extraction for method calls with multiple list of arguments #1694

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
vkuncak merged 3 commits into from
Dec 23, 2025
Merged

Fix a bug in extraction for method calls with multiple list of arguments #1694

vkuncak merged 3 commits into from
Dec 23, 2025
+44 −0

Conversation

@samuelchassot
Copy link
Collaborator

@samuelchassot samuelchassot commented Dec 22, 2025 •
edited
Loading

Fixes a problem in the extraction of method calls with multiple lists of arguments. Previously, the receiver (i.e., probably this) was lost as it was extracted as a function call without receiver.

Fixes #1692

Was discovered while working on class tags, as they add implicitly a new list of parameters to methods.

Example:

trait Interface:
  def pred[C: ClassTag](l: List[C]): Boolean = true
  def f[C: ClassTag](l: List[C]): List[C]
end Interface

case object Impl extends Interface:
  override def f[C: ClassTag](l: List[C]): List[C] = {
    require(pred(l))
    l
  }
end Impl

Here, the call to pred in the require of f was extracted as:

@final
@method(Impl)
def f[C](l: List[C]): List[C] = {
  require(pred[C](l))
  l
}

instead of

@final
@method(Impl)
def f[C](l: List[C]): List[C] = {
  require(this.pred[C](l))
  l
}

See #1692 for more details.

Copilot AI review requested due to automatic review settings December 22, 2025 14:20
Copilot AI reviewed Dec 22, 2025
View reviewed changes
Copy link
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

This PR fixes a bug in AST extraction for method calls with multiple argument lists in the Dotty frontend. The fix adds pattern matching cases to handle nested Apply nodes, which represent curried method calls with multiple parameter lists.

Key Changes

  • Added support for nested Apply nodes in ExThisCall extractor to handle methods with multiple argument lists
  • Added support for nested Apply nodes on ExThisCall in ExCall extractor for proper recursion
  • Added test cases to validate extraction of methods with multiple argument lists and ClassTag context bounds

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File Description
frontends/dotty/src/main/scala/stainless/frontends/dotc/ASTExtractors.scala Adds pattern matching cases to handle nested Apply nodes for multiple argument lists in ExThisCall and ExCall extractors
frontends/benchmarks/extraction/valid/MethodCallsWithMultipleArgsLists.scala Test case for methods with multiple explicit argument lists (e.g., pred(l)(0)(0))
frontends/benchmarks/extraction/valid/ClassTagMethodCalls.scala Test case for methods with ClassTag context bounds that create implicit argument lists

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@samuelchassot samuelchassot requested a review from mbovel December 22, 2025 14:46
Copilot AI reviewed Dec 22, 2025
View reviewed changes
Copy link
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated no new comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

mbovel
mbovel reviewed Dec 23, 2025
View reviewed changes
Copy link
Member

@mbovel mbovel left a comment •
edited
Loading

Choose a reason for hiding this comment

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

This seems okay-ish as a quick fix.

However, I find it misleading that ExCall also matches ExThisCall. These extractors are mainly used here:

stainless/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala

Lines 1867 to 1878 in 2b3d9c0

case ExThisCall(tt, sym, tps, args) =>
extractCall(tr, Some(tpd.This(tt.cls)), sym, tps, args)
case ExCastCall(expr, from, to) =>
// Double check that we are dealing with regular integer types
val xt.BVType(true, size) = extractType(from)(using dctx, NoSourcePosition): @unchecked
val newType @ xt.BVType(true, newSize) = extractType(to)(using dctx, NoSourcePosition): @unchecked
if (size > newSize) xt.BVNarrowingCast(extractTree(expr), newType)
else xt.BVWideningCast(extractTree(expr), newType)
case c@ExCall(rec, sym, tps, args) =>
extractCall(c, rec, sym, tps, args)

where there is clearly a case for this.m(...) and a distinct case for m(...).

If I understand correctly, after this PR, this-calls with multiple argument lists will not be matched by ExThisCall but instead by ExCall, while this-calls with a single argument list will still be matched by ExThisCall.

That creates a semantic overlap where ExCall subsumes part of ExThisCall’s intended domain. This makes the extractor behavior arity-dependent, which I find confusing and harder to reason about.

I would find it more coherent to either:

  1. Extend ExThisCall to support multiple argument lists, or
  2. Let ExCall match this-calls as it currently does, but then completely remove ExThisCall, which should no longer be necessary.

On a separate note, ExThisCall also seems limited to paths of depth one: it matches this.m but not this.c.m, since it only recognizes a single top-level TermRef and does not recurse. We might want to test this and potentially address it separately.

@vkuncak vkuncak merged commit a860c9b into main Dec 23, 2025
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@mbovel mbovel mbovel left review comments

Copilot code review Copilot Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Trait's default implementations crash when using implicit ClassTag

4 participants

@samuelchassot @mbovel @vkuncak