If I told you that I have a snippet of machine code that:
- obeys the ABI of your safe language (ie it has exactly the calling convention that safe language uses)
- corresponds exactly to a function body whose signature is T->U (or whatever, different safe languages have different function type syntax)
- obeys the language’s type system.
Then you could run an abstract interpreter to check that the machine code follows that type system. Simple example: given the above claims, if we further assume that the host language impl puts argument one into register 5, and the first argument’s type is “pointer to an array of bytes”, and we know that arrays have a 64-bit length prefixed to the start, then the abstract interpreter would just need to check that any deref of register 5 is preceded by a bounds check on whatever was loaded at offset -8 from register 5. And so on, for every possible thing you can do in the language.
Then the JIT would just have to make sure it puts checks in all of the places that the absint expects them. If the absint fails, then the machine code is rejected.
If I told you that I have a snippet of machine code that:
- obeys the ABI of your safe language (ie it has exactly the calling convention that safe language uses)
- corresponds exactly to a function body whose signature is T->U (or whatever, different safe languages have different function type syntax)
- obeys the language’s type system.
Then you could run an abstract interpreter to check that the machine code follows that type system. Simple example: given the above claims, if we further assume that the host language impl puts argument one into register 5, and the first argument’s type is “pointer to an array of bytes”, and we know that arrays have a 64-bit length prefixed to the start, then the abstract interpreter would just need to check that any deref of register 5 is preceded by a bounds check on whatever was loaded at offset -8 from register 5. And so on, for every possible thing you can do in the language.
Then the JIT would just have to make sure it puts checks in all of the places that the absint expects them. If the absint fails, then the machine code is rejected.