[exec] Bounds check bulk-memory before execution

[eqrion]

Spec issue: #111

This commit changes the semantics of bulk-memory instructions to perform
an upfront bounds check and trap if any access would be out-of-bounds without
writing.

This affects the following:

• memory.init/copy/fill
• table.init/copy (fill requires reftypes)
• data segment init (lowers to memory.init)
• elem segment init (lowers to table.init)

This commit corrects an edge case where a memory/table.init with zero
length wouldn't trap even if the data/elem segment had been dropped.
This was due to an extra pattern in eval that would match zero-length
instructions and not check if the segment had been dropped. One test
case in bulk.wast had to be changed for this.

[eqrion]

I would also be interested in updating the spec-text as well, but will need some guidance.

Right now the instructions are implemented by lowering to plain i32.load8_u/i32.store8's for memory and table.get/table.set for tables.

I think there are a couple options here.

1. Use the stack as a temporary buffer.
   • Lower to a series of loads onto the stack, followed by a sequence of stores from high addresses to low.
2. Add new administrative functions.
   • transfer_memory(src: vec(u8), memory: mem_address, dest: offset)
   • transfer_elements(src: vec(elem), table: tab_address, dest: offset)
   • Lower init,copy,fill to these by constructing the appropriate src buffer.
3. Add a bounds check at the beginning of the existing semantics, keep everything else.

I think all of these can be equivalent in the single-threaded case, but I'm having a hard time reasoning about the implications for threading.

[rossberg]

Hi @eqrion, thanks for moving forward with this. Turns out we were in a race. :) I had started on a similar patch last week but didn't get to finish the spec part yet. I uploaded it here so that we can compare. But mine is more WIP. In particular, I did not properly fix the test generators. And I only started on the spec itself. So we should probably go with yours instead.

However, one relevant difference is that I kept and adapted the small-step semantics for the interpreter instead of going back to monolithic implementations. This is important for two reasons: (1) the interpreter should match the spec rules, and (2) the rules need to use small-step in order to be forward-compatible with the threads proposal, where bulk ops are no longer atomic operations.

How would you feel about incorporating my interpreter implementation into your patch?

[eqrion]

Hi @eqrion, thanks for moving forward with this. Turns out we were in a race. :) I had started on a similar patch last week but didn't get to finish the spec part yet. I uploaded it here so that we can compare. But mine is more WIP. In particular, I did not properly fix the test generators. And I only started on the spec itself. So we should probably go with yours instead.

However, one relevant difference is that I kept and adapted the small-step semantics for the interpreter instead of going back to monolithic implementations. This is important for two reasons: (1) the interpreter should match the spec rules, and (2) the rules need to use small-step in order to be forward-compatible with the threads proposal, where bulk ops are no longer atomic operations.

How would you feel about incorporating my interpreter implementation into your patch?

Ah apologies about the duplicated effort, I should have posted that I was taking a look at this. :)

Good to know about needing the small-step semantics, I think that was what I was getting at with my question. I'll adapt your interpreter implementation into my patch.

[rossberg]

Cool, thanks!

Forgot one thing. You mentioned:

This commit corrects an edge case where a memory/table.init with zero
length wouldn't trap even if the data/elem segment had been dropped.

This actually was an intentional fix in #115. The rationale being that accessing a dropped segment is equivalent to an out-of-bounds access, because a dropped segment is essentially a segment shrunk to size 0. A zero-length access should therefore behave consistently with no effect.

[eqrion]

Forgot one thing. You mentioned:

This commit corrects an edge case where a memory/table.init with zero
length wouldn't trap even if the data/elem segment had been dropped.

This actually was an intentional fix in #115. The rationale being that accessing a dropped segment is equivalent to an out-of-bounds access, because a dropped segment is essentially a segment shrunk to size 0. A zero-length access should therefore behave consistently with no effect.

Ah, I believe the exec-text for memory.init needs an update then. Step 10 does a trap if the data segment has been dropped, before step 17 does the check for cnt = 0. That was my reasoning for calling this a bug.

Spidermonkey will also need an update for this, as we will trap in this case.

[eqrion]

Ah, I believe the exec-text for memory.init needs an update then. Step 10 does a trap if the data segment has been dropped, before step 17 does the check for cnt = 0. That was my reasoning for calling this a bug.

On further examination, it appears that the formal rules are correct and the prose is what may need an update.

[rossberg]

Ah, I see. If you want, please feel free to fix this as part of this PR.

[eqrion]

I've updated the interpreter commit to use your patch, keep the small step semantics, and extend early bounds checking to the table operations. That commit should be good to go.

I've also added a commit for the dropped segments issue, and started looking at the spec text.

[rossberg]

Thanks!

[eqrion]

@rossberg Is this ready to go now?

[rossberg]

Yes, thanks!

[eqrion]

Thanks!