isolate happily compiles despite not being able to prove the absence of captured refs

[obadz]

To set the stage, this works fine:

import std/isolation

type Z = ref object
  i: int

type A = object
  z: Z

func z_to_a(z: Z): A =
  result = A(z: z)

let z = Z(i: 3)
let a = isolate(z_to_a(z)) # Error: expression cannot be isolated: z_to_a(z)

Example

On the other hand, these two cases are unsafe:

Returning a subgraph:

import std/isolation

type Z = ref object
  i: int

type A = object
  z: Z

func a_to_z(a: A): Z =
  result = a.z

let a = A(z: Z(i: 3))
let z = isolate(a_to_z(a))

echo repr(z) # [value = ref 0x7fca2c6d9050 --> [i = 3]]
inc a.z.i
echo repr(z) # [value = ref 0x7fca2c6d9050 --> [i = 4]]

Overlapping subgraphs:

import std/isolation

type Z = ref object
  i: int

type A = object
  z: Z

type B = object
  z: Z

func a_to_b(a: A): B =
  result = B(z: a.z)

let a = A(z: Z(i: 3))
let b = isolate(a_to_b(a))

echo repr(b) # [value = [z = ref 0x7f8650b6b050 --> [i = 3]]]
inc a.z.i
echo repr(b) # [value = [z = ref 0x7f8650b6b050 --> [i = 4]]]

Current Output

Compiles fine and I expect would produce refcount corruption in a multi threaded environment, exposing the user to memory related crashes.

Expected Output

Refuse to compile with cannot be isolated.

Possible Solution

I think isolate should rule out any cases where the input & output types share a common ref subgraph.

Ideally an isolate_copy function would always succeed and create fresh copies of every ref whose count is > 1. In fact maybe the current function should be isolate_nocopy and the default behaviour should just be to copy the refs when the RC is > 1?

Additional Information

Mentionned in nim-lang/RFCs#244 (comment)

$ nim -v
Nim Compiler Version 1.4.8 [Linux: amd64]

[deech]

I think the problem here is the isolation check passes alias analysis when it shouldn't. I was able get to the desired behavior by annotating the return types with lent. Maybe the solution is when an nnkCall node is passed to isolate it should pretend that the return type is annotated with lent but that might be too strict when the function does actually create a fresh ref. While this is just a quick-and-dirty suggestion the compiler's lifetime analysis machinery can statically track provenance so it shouldn't be hard to fix this generally.

[deech]

Also I recommend that since Isolate is essentially a compiler primitive and the recommended way of protecting a data structure from mutation an error message that points to the specific part of the input that cannot be isolated is necessary.