Runtime Safety Checks implementation in Interpreter

[RishabhRD]

The document assumes that one can do bad things in language only using unsafe memory access using pointers. (Please point other possibilities if is there).

With unsafe memory access using pointers, we need to tackle following problems:

1. Accessing invalid place,
2. Reading from memory that is not initialized yet,
3. Invalid access to a place (e.g., inout access to a place currently having let access).
   (Please point out, if there are other possible problems I am missing here).

There are 2 sections:

1. Possible solution with composed region
2. An alternate solution, that deals with these subproblems independently.

Solution with Composed region

Accessing Invalid Place

Motivating usecase: store instruction doesn't need destination place to be in composed region. However, still the place should be valid i.e., it should not be allowed to store an Int in an allocation at offset o where a Float should have been stored.

Solution:

• Every allocation would contain its type layout.
• Recursive traversal in type layout can detect this kind of invalid access.
• Unions/Enums would be an interesting case, as while recursive traversal we would also need to check if discriminator is in composed region. And thus, we need to simeltaneously traverse the composed region elements too.

Reading from memory that is not initialized yet

Motivating usecase: load from source where source is a valid place. However, source is not initialized yet.

Solution (Part 1):

• Recursive traversal on composed region can detect this kind of access.

Solution (Part 2):

• We need to maintain the composed region records for the same; i.e., whenever a memory is initialized, we put it to composed region.
• store and memory_copy instruction actually writes to memory and thus update composed regions after these instructions.
• If every element of tuple/union has been put in composed region, replace the records with tuple/union record up until root (if possible).

Invalid access to place

Motivating usecase: First let access to a place and then attempting inout access to same place without end_access.

Solution:

• We need to maintain stack of access for the same.
• If we define ordering: set > inout > let, then every composed region can have stack of accesses with invariant that "greater" access can't appear after "smaller" access.
• For subfield mutable access like: a.b, on inout access of b, replaces the composition records of a with children of a with all accesses of a, plus inout access for b too.

Alternate Solution

To me, it seems that initialization records and stack of access is being merged using composed region strategy and making it really complex. This merging of responsibility comes from one of @dabrahams line: "inout access replaces composed region of parent with children".

Also, it feels to me, we need to traverse composed region and type layout multiple times to implement the above strategy, that feels like duplicate work.

Instead, we can use 3 different data structures to solve these problems independently:

1. Initialization byte-mask
2. Type layout of allocation
3. Stack of access per region in storage

(I believe, Rust's Miri does some similar thing, but not sure on that).

Initialization byte-mask

• Along with storage in allocation, we can store var initialized: [Bool] in the allocation of same size as storage.
• Whenever we write to offset i, we update the initialized to be true.

Type layout of allocation

• To detect invalid place access.
• Will use initialization byte-mask for checking if discriminator is initialized for Union/Enum case.

Stack of access per region

• An access can be (id, access_type) describing an access in allocation for any offset region.
• We maintain [(i, j), Access], describing access for bytes in [i, j).
• One can't push "greater" access if "lower" access is on top based on ordering: set > inout > let.
• If all accesses are let, then any access can be used for reading memory, otherwise only top access can be used.

For subfield access:

Valid example for struct A[B(0-4) C(4-8)]:

• Initially: [(0, 8), [base]] // base is initial access
• with let on C: [(0, 4), [base]], [(4, 8), [base , let]]
• with let on A: [(0, 4), [base, let]], [(4, 8), [base , let, let]]
  Other than base access, every access is a let access for records being updated and hence a valid operation.

Valid example for struct A[B(0-4) C(4-8)]:

• Initially: [(0, 8), [base]] // base is initial access
• with inout on C: [(0, 4), [base]], [(4, 8), [base , inout]]
• with inout on C: [(0, 4), [base, let]], [(4, 8), [base , inout, inout]]
  Can create multiple inout access to same element in array, if top element in inout.

Invalid example for struct A[B(0-4) C(4-8)]:

• Initially: [(0, 8), [base]] // base is initial access
• with inout on C: [(0, 4), [base]], [(4, 8), [base , inout]]
• with inout on A: Other than base access, there is already existing inout access for records being updated (for multiple record case) and thus, we are trying to create bigger inout than possible. Thus reject it.

[dabrahams]

Allocations don't have a type layout. It should be possible to dynamically allocate raw memory and then write and read various types from it.

[dabrahams]

Yes, in general allocations don't have any type information associated with them and can be used to store anything that fits when properly aligned.

This

If not, then we certainly need

Only makes sense to me if you replace "not" with "so"

[dabrahams]

Here's a motivating example: I want to build a stack of heterogeneous elements in contiguous memory. I cannot know statically where things are placed in this memory.

I understand why composition might look too complicated or even problematic. For example, should this be legal?

struct A<T> { 
  let x: Int

  init() {
   x = 3
   
   // `init` not finished but members initialized, so accessing `self`'s memory as `A<T>` is OK.
   print(self)
   
   // Equivalent
   print(pointer[to: self].unsafe[])
      
   // The members of an A<A<T>> are the same, so is accessing `self`'s memory as `A<A<T>>` OK?
   print(
      Pointer<A<A<T>>>(
        type_punning: pointer[to: self]
      ).unsafe[]
    )
  }
}

If the last statement is legal, then composition records merely act as a cache of last access information, and for the last statement the memory needs to be decomposed and then re-composed as an A<A<T>>, a process that would be reversed as soon as self was accessed as A<T> again.

If the last statement is illegal, then we need some logic that explains why. For example, we could say that entering A<T>.init “primes” the region for composition as A<T> and it becomes composed as soon as all the members are initialized.

My intuition is that we want the last statement to be illegal.

[dabrahams]

Agreed in the meeting: we want the last statement to be illegal.

However, that makes me realize the data structure I implemented doesn't store enough information. Consider:

fun f(_ x: inout A) {
  consume(x.y)
  // x is decomposed; there is no `A` there

  x.y = z
  // x is recomposed as `A`
}

When decomposing a whole due to consuming/deinitializing a part, we need to keep a record of the whole so we can recompose that. It's easy to see how the code above knows what to do, but we can do the same thing with pointers, to see why keeping a record matters:

fun g(_ px: PointerToMutable<A>) {
  consume(px.unsafe[].y)
  // px.unsafe[] is decomposed; there is no `A` there

  px[\A.y].unsafe[].init(z) // see https://val-qs97696.slack.com/archives/C036N9ACU8Y/p1773182817401999
  // px.unsafe[] is recomposed as `A`, not as any other arbitrary type.
}

[RishabhRD]

Yes, we always need to have information of "root" type we are tying to build. So, instead of just storing type of composed region, we can store:

• The root type (the type we are trying to build by composing)
• RecordPath of type of composed region
  to have this information.

[dabrahams]

There is no "trying to build" in the scenario I just outlined, but I guess when a type is decomposed due to consumption of a part we could view that as trying to build that type again.