Incorrect aliasing of iso when using match

[scwunch]

I don't think a field should be consumable, but this code compiles and gives rise to arbitrarily many copies of an iso reference to one object, breaking the isolation guarantees.

The particular function that should be caught by the function is this one:

fun ref take(): Foo iso^ =>
    // consume _foo  // <- compiler error
    match _foo
    | let b: Foo => consume b   // ... no compiler error?
    end

$ ponyc -v
0.58.9-cabe71e [release]
Compiled with: LLVM 15.0.7 -- Clang-18.1.3-x86_64
Defaults: pic=true

[SeanTAllen]

Code in question from the playground:

actor Main
  new create(env: Env) =>
    var fbox = FooBox(recover iso Foo("original") end)
    let one_foo = fbox.take()
    let same_foo = fbox.take()
    let w1 = WantFoo(consume one_foo)
    w1(env)
    same_foo.data = "changed"
    let w2 = WantFoo(consume same_foo)
    w2(env)

class iso Foo
  var data: String
  new create(data': String) =>
    data = data'

class iso FooBox
  var _foo: Foo iso

  new iso create(foo: Foo iso) =>
    _foo = consume foo

  fun ref take(): Foo iso^ =>
    // consume _foo  // <- compiler error
    match _foo
    | let b: Foo => consume b   // ... no compiler error?
    end

actor WantFoo
  var foo: Foo

  new create(foo': Foo iso) =>
    foo = consume foo'

  be apply(env: Env) =>
    env.out.print(foo.data)

[SeanTAllen]

Minimal reproduction:

class Bad
  let _s: String iso

  new iso create(s: String iso) =>
    _s = consume s

  fun ref take(): String iso^ =>
    match _s
    | let s': String iso => consume s'
    end

[SeanTAllen]

A variation to also test based on the consume code:

class Bad
  var _s: String iso

  new iso create(s: String iso) =>
    _s = consume s

  fun ref take(): String iso^ =>
    match _s
    | let s': String iso => consume s'
    end

[SeanTAllen]

If we had:

  fun ref take(): String iso^ =>
    consume _s

this would get caught. Because we would have this in the ast:

(consume x (. this (id _s))) which would fall through into the TK_DOT code in refer_consume, but we don't have that ast, we have (consume x (letref (id s')))

The code that handles TK_VARREF, TK_LETREF, and TK_PARAMREF needs to handle for varref and letref the possibility that have a field and do a check like TK_DOT has:

      if(ast_id(left) == TK_THIS)
      {
        def = (ast_t*)ast_data(term);
        name = ast_name(right);

        // check it's not a let or embed if it's a this variable
        if((ast_id(def) == TK_FLET) || (ast_id(def) == TK_EMBED))
        {
          ast_error(opt->check.errors, ast,
            "can't consume a let or embed field");
          return false;
        }

It is important to note that var fields aren't handled by the above code. but instead this code later in the TK_DOT case:

      if(!check_assigned_same_expression(opt, ast, name, &assign_ast))
      {
        ast_error(opt->check.errors, ast,
          "consuming a field is only allowed if it is reassigned in the same"
          " expression");
        return false;
      }

Thus we need two test both minimal cases, with let and with var. Additionally we need to test embed as well.

[SeanTAllen]

@jemc do you agree with this as a "general approach" or do you think there is an alternate approach we should be taking?

[dipinhora]

not sure if it's helpful, but the minimal reproduction from #4579 (comment) used to fail to compile through pony 0.40.0.. error details can be seen on godbolt: https://godbolt.org/z/W8brMzr8d

selecting pony 0.41.2 on godbolt allows it to compile successfully..

[SeanTAllen]

Thanks @dipinhora. I was already really confident this was broken in #3643 which went in with 0.41.0

[redvers]

I hesitate to stumble into areas of the theory or compiler that I don't fully understand, but it looks to me more like match on an iso breaks iso's guarantees as opposed to having anything to do with a class field:

For example:

actor Main
  new create(env: Env) =>
    let a: (String iso | None) = recover iso "Hello World".clone() end
    var b: String iso = recover iso String end
    
    match a
    | let dup: String iso => b = consume dup
    | let no: None => None
    end
    
    if (a is b) then env.out.print("Identity Equality") end

If that's the case, I guess we should ensure that we don't allow match on isos and force consumption?

[redvers]

Even more minimal example:

actor Main
  new create(env: Env) =>
    let a: String iso = recover iso "Hello World".clone() end
    var b: String iso = recover iso String end
    
    match a
    | let x: String iso => b = consume x
    end
    
    if (a is b) then env.out.print("Identity match of two isos") end

[SeanTAllen]

@redvers

If that's the case, I guess we should ensure that we don't allow match on isos and force consumption?

No, there's nothing wrong with matching on an iso. There's nothing wrong with consuming it, but we need to properly track aliasing and get the refcaps correct.

It makes sense that @redvers found what he did. Match and aliasing appears to have been broken when we moved to our current implementation of the type system when we switched to the Stead model.

[SeanTAllen]

Here's the correct error for red's minimal example.

Building builtin -> /opt/compiler-explorer/ponyc-0.40.0/packages/builtin
Building /app -> /app
Error:
<source>:7:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let x: String iso => b = consume x
      ^
    Info:
    <source>:3:12: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: String iso!
        let a: String iso = recover iso "Hello World".clone() end
               ^
    <source>:7:7: pattern type: String iso
        | let x: String iso => b = consume x
          ^
    <source>:7:14: matching String iso! with String iso could violate capabilities: iso! isn't a subcap of iso
        | let x: String iso => b = consume x

We appear to have lost some proper aliasing.

[SeanTAllen]

My minimal example should have:

Building builtin -> /opt/compiler-explorer/ponyc-0.40.0/packages/builtin
Building /app -> /app
Error:
<source>:9:7: this capture violates capabilities, because the match would need to differentiate by capability at runtime instead of matching on type alone
    | let s': String iso => consume s'
      ^
    Info:
    <source>:2:11: the match type allows for more than one possibility with the same type as pattern type, but different capabilities. match type: String iso!
      let _s: String iso
              ^
    <source>:9:7: pattern type: String iso
        | let s': String iso => consume s'
          ^
    <source>:9:15: matching String iso! with String iso could violate capabilities: iso! isn't a subcap of iso
        | let s': String iso => consume s'

So yes, my initial solution was incorrect. I missed that we were in fact aliasing again and that it should be iso! unless you do match consume foo.

@jemc that isn't something that changed in the Stead model is it?

[jasoncarr0]

Oh yeah this is a longstanding issue that's very hard to fix without breaking valid code:
#3596
This example is a little bit simpler though

[jemc]

So what was the match expression aliasing behavior prior to PR #3643?

I'm confused as to why this was working properly in older versions of ponyc (as mentioned in above comments in this ticket).

[SeanTAllen]

So what was the match expression aliasing behavior prior to PR #3643?

Beyond the basics that I did for run with previous to verify basic behavior, I think we need to crack open the code together @jemc and go spelunking. It very much looks like that the let was correctly aliasing the binding (as should happen based on my discussions with Sylvan).

[jasoncarr0]

Presumably it's just https://github.com/ponylang/ponyc/pull/3643/files#diff-5c1159210a17e5115177c6e16b9eecb3f0dc0a56b6d0fc564dac282b5604ba0cL509
But I'm a bit surprised at both that change, as well as code that would rely on the lack of aliasing. The issue I linked is before #3643

The correct change for this line of code is to make the pattern_type of the branches ephemeral when checking to match the other changes to aliasing (i.e. instead of A! <= B, check A <= B^)

[SeanTAllen]

@jemc here is the patch for what you and i did during sync that we want to pick up from or at least save for posterity.
patch.txt

[jemc]

During the sync call, we explored the above patch, which did bring back the desired error for the hole in this ticket, but it also invalidated other valid match statements in the standard library, such as a match statement in string.pony where the iso^ returned by String.from was used as the match expression, and compared for equality against string literals (val).

More work is needed to create a correct patch.

[SeanTAllen]

@jemc I think perhaps we are approaching this slightly wrong. We are thinking about this from a "pre-steed" model. Consider the following code:

actor Main
  new create(env: Env) =>
    let x = recover iso "h".clone() end
    let a = A
    a.f(x)
    
actor A
  new create() => None
  be f(a: String iso) =>
    None

The error we get now is:

main.pony:5:9: argument not assignable to parameter
    a.f(x)
        ^
    Info:
    main.pony:5:9: argument type is String iso
        a.f(x)
            ^
    main.pony:9:8: parameter type requires String iso^
      be f(a: String iso) =>
           ^
    /root/.local/share/ponyup/ponyc-release-0.58.9-x86_64-linux-musl/packages/builtin/string.pony:604:16: String iso is not a subtype of String iso^: iso is not a subcap of iso^
      fun clone(): String iso^ =>
                   ^
    /root/.local/share/ponyup/ponyc-release-0.58.9-x86_64-linux-musl/packages/builtin/string.pony:604:23: this would be possible if the subcap were more ephemeral. Perhaps you meant to consume a variable here
      fun clone(): String iso^ =>

Prior to the steed change, this was:

Error:
<source>:5:9: argument not a subtype of parameter
    a.f(x)
        ^
    Info:
    <source>:5:9: argument type is String iso!
        a.f(x)
            ^
    <source>:9:8: parameter type is String iso
      be f(a: String iso) =>
           ^
    /opt/compiler-explorer/ponyc-0.40.0/packages/builtin/string.pony:604:16: String iso! is not a subtype of String iso: iso! is not a subcap of iso
      fun clone(): String iso^ =>
                   ^
    /opt/compiler-explorer/ponyc-0.40.0/packages/builtin/string.pony:604:23: this would be possible if the subcap were more ephemeral
      fun clone(): String iso^ =>

So I think what we want is perhaps that the match requires a iso^ rather than it doing aliasing. Therefore we have to consume it. To use in the match. I haven't fully thought this through, but based on our discussions during sync, perhaps we should be approaching from that "same thing, different angle"?

To match on an iso field we would need to do something like (pre or post stead)

class Bad
  var _s: String iso

  new iso create(s: String iso) =>
    _s = consume s

  fun ref take(): String iso^ =>
  
    let old = _s = recover iso _s.clone() end
    
    match consume old
    | let s': String iso => consume s'
    end

Note, the above change makes it compile pre-steed.

Also note all this still leaves the (iso | None) issue. I am approaching this from "let's fix the hole then address the union type usability issue with iso".

I think this is how you would need to address (right now) the | None problem with a field. It's ugly but it puts together the dynamics we need:

class Bad
  var _s: (String iso | None) = None

  new iso create(s: String iso) =>
    _s = consume s

  fun ref take(): String iso^ =>
    let o = _s = None
    _s = match (consume o)
    | let x: String iso => x.append(" there")
    | None => recover iso "hello".clone() end
    end
  
    "a".clone()

[SeanTAllen]

@jemc and i got one of the use cases correct (no tests for them yet) but there's two interesting failing runner tests we haven't had time to look at. We need to add tests for the identified cases above plus look into the failing:

[  FAILED  ] codegen-trace-tuple-boxed
[  FAILED  ] codegen-trace-tuple-dynamic

runner tests.

The current patch is attached.
patch.txt