Skip to content
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.

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

Problem Function References and Name Mangling #554

Closed
DavePearce opened this issue Dec 23, 2015 · 12 comments
Closed

Problem Function References and Name Mangling #554

DavePearce opened this issue Dec 23, 2015 · 12 comments
Assignees
Labels
Milestone

Comments

@DavePearce
Copy link
Member

The following test case was show by @utting to fail at runtime:

import whiley.lang.*

type SizeGetter is function(Sized) -> int

type Sized is {
    int size,
    SizeGetter getSize,
    ...
    }

type MultiSized is {
    int size,
    int count,
    SizeGetter getSize,
    ...
    }

public function getSized(Sized s) -> int:
    return s.size

constant DATA is [
      {size:3, getSize: &getSized},
      {size:5, count:4, getSize: &getSized},  // TODO: use getMultiSized
      {size:7, getSize: &getSized}
    ]

method sum(Sized[] values) -> int:
    int i = 0
    int total = 0
    while i < |values|:
    Sized ob = values[i]
    SizeGetter sg = ob.getSize
    // int size = ob.size       // this works
    // int size = getSized(ob)  // this works
    int size = sg(ob)           // this gives a run-time type error
    total = total + size
    i = i + 1
    return total
    
method main(System.Console sys):
    sys.out.println(sum(DATA))

The error message reported is:

Exception in thread "main" java.lang.NoSuchMethodError: sum1.getSized$Z9bFaA$WE9FJD$D2Vm$VD$a1Vo$FE$9Y$ND$H2$x$cgz(Lwyjc/runtime/WyRecord;)Ljava/math/BigInteger;
    at sum1$0.call(Unknown Source)
    at sum1.sum$4AbFaA$0D5ZL13$n0FS$o5$lJ$B4$d0VT$J5$ZC(./sum1.whiley)
    at sum1.main$2Ab737oHF4$i2$o$7C$N2Vm$7E$T0$q$7B$R2Vn$s4$a1Vw$ND$c2Vm$ch2VW$sC$R2Vt$sC$N2Vm1(./sum1.whiley)
    at sum1.main(./sum1.whiley)

In essence, this looks like a problem with name mangling...

@DavePearce DavePearce self-assigned this Dec 23, 2015
@DavePearce DavePearce added this to the ChangeList Pre v0.4.0 milestone Dec 23, 2015
@DavePearce
Copy link
Member Author

So, if we display the mangles as generated by Whiley2JavaBuilder.nameMangle() we get this:

GOT: function(sum1:Sized) -> int
MANGLE: getSized$Z9bFaA$WL13$n0FS$o5$lJ$B4$d0VT$J5$Zx
...
GOT: X<function({X getSize,int size,...}) -> int>
MANGLE: getSized$Z9bFaA$WE9FJD$D2Vm$VD$a1Vo$FE$9Y$ND$H2$x$cgz
...

We can see clearly that it's not generated the same name mangles. In fact, the interesting thing here is that the problem is arising because one type is "raw" and the other contains a "nominal". Interesting...

@DavePearce
Copy link
Member Author

UPDATE: so the first mangle is occurring at the definition site.

@DavePearce
Copy link
Member Author

So, thinking about this there are two options:

  1. Make all declarations use raw types. This means we convert the function or method declaration types to raw at the point of constructing the Jvm method.
  2. Ensure Lambda's keep nominal types. This means we copy over the nominal type for a lambda from the function in question.

Seems like I prefer option (2) above because this retains as we generally prefer to retain as much nominal information as possible. I suppose I should add a test case or two.

DavePearce added a commit that referenced this issue Dec 23, 2015
This test case was designed to illustrate the problem highlighted in
this issue, however it is not actually achieving that.  Rather, the
problem does not show on the JVM but does show on the WyIL intepreter.
@DavePearce
Copy link
Member Author

Have added test case FunctionRef_Valid_10, which operates on a linked list. However, this does not illustrate the problem on the JVM, although it does on the WyIL intepreter.

The essential difference appears to be that the lambda is stored in a constant definition in the original example, where as in my new test case it's not.

DavePearce added a commit that referenced this issue Dec 23, 2015
This illustrates the problem as identified in issue 554.  Unlike
FunctionRef_Valid_10, this illustrates the issue on the JVM as well.
@utting
Copy link
Contributor

utting commented Dec 23, 2015

Options 1 and 2 are interesting tradeoffs. I assume that raw type means base type, while nominal means the full subtype information.

Z uses option 1 for typechecking (it just checks base types), but one must still use the richer type for reasoning.

Keeping nominal types (full subtype information) might make it easier to support F-bounded quantification in the future, so that methods within subtypes can know that one of their inputs is the subtype rather than the supertype? This would be one step closer to supporting OOP.

@DavePearce
Copy link
Member Author

Hey Mark,

Yeah, raw type means that we extract all nominal type information just leaving the "base" type. For example:

type Point is { int x, int y }
function f(Point p) -> int:
    ...

The nominal type of function f is function(Point)->int, where as its raw type would be function({int x,int y})->int.

Yes, effectively, I use option (1) for type checking. Option (2) is retained for providing better debugging output, and also potentially to allow overloading of constrained types (though this is not really implemented yet).

DavePearce added a commit that referenced this issue Dec 23, 2015
This illustrates the problem as identified in issue 554.  Unlike
FunctionRef_Valid_10, this illustrates the issue on the JVM as well.
@DavePearce
Copy link
Member Author

The problem is an interesting one. Essentially, when a Constant.V_LAMBDA is created it is supplied with the type of the function in question. However, since Constant is a WyIL class it does not support Nominal types, only single instances of Type. At this point, a choice is made which originally was to use Nominal.raw().

Later this single instance is turned back into an instance of Nominal with both positions populated from the single Type instance. This occurs in Expr.ConstantAccess.result(), where a useful comment can be found:

// FIXME: loss of nominal information here, since the type of the
// constant in question is always fully expanded.
return Nominal.construct(value.type(), value.type());

Late the Nominal instance constructed is passed into FlowTypeChecker.resolveAsFunctionOrMethod() as part of the effort to type check a separate invocation. Unfortunately, resolveAsFunctionOrMethod() expects the rawType() to have a proper raw type, otherwise it doesn't work. Hence, changing the original choice to use Nominal.nominal() instead of Nominal.raw() still fails. Phew!

@DavePearce
Copy link
Member Author

So, what are the options? Here are some:

  1. Construct a wyc.lang.Constant hierarchy which shadows wyil.lang.Constant. This can then include proper Nominal type information, so there is no loss of information.

  2. Update resolveAsFunctionOrMethod() to not make any assumptions about the type actually being raw or not. This seems like a hack to me though.

Based on that, option (1) seems like the sensible though rather laborious approach. I wonder if there are other ways in which option (1) would benefit us?

For example, it seems possible that there are other situations where the loss of nominal information could be a problem...

@DavePearce
Copy link
Member Author

Other options include:

  1. Update the way that Nominal versus Raw type information is managed in the front end. This would mean moving away from maintaining both Nominal and Raw types alongside each other and, instead, recalculating the Raw types on demand. The performance hit from this could be offset by using a caching scheme for example.

@DavePearce
Copy link
Member Author

it seems possible that there are other situations where the loss of nominal information could be a problem...

Right, I'm not sure about this now. Basically it requires there to be a difference between the nominal and raw type for a constant. There aren't many situations where this could arise, since constants are generally by their very nature "raw" in some sense. It's only Lambda's that seem to bring in a non-raw type.

If casts were allowed in constant expressions, then something like this might do it:

type TRec is {int x, int y}
constant CRec is (TRec) { x: 1, y: 2 }
function f(TRec p) -> (int r):
    return p.x + p.y
function g(int x) -> (int r):
    return f(CRec)

Currently, this does not compile though.

@DavePearce
Copy link
Member Author

So, of course, the solution presents itself! The easiest thing is to have a proxy object to interface between the front-end AST and the WyIL which holds both types. And, we already have such an object: Expr.ConstantAccess ...

DavePearce added a commit that referenced this issue Dec 28, 2015
This fix resolves a problem related to the nominal typing of lambda
constants.  The problem occurred because lambda constants were encoded
as instances of wyil.lang.Constant which contained only one type slot.
This contrasts with the expectation in FlowTypeChecker where we need
both nominal and raw information.  Previously, just raw information was
used but this caused problems.  Instead, we now propagate full Nominal
information which resolves the issue.
@DavePearce
Copy link
Member Author

Right, fixed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants