I've lamented here and elsewhere some unfortunate inconveniences and asymmetries in the CLR -- for example, we have nullable structs but lack non-nullable reference types, an issue I address in my Sasa class library.
I've recently completed some Sasa abstractions for safe reflection, and an IL rewriter based on Mono.Cecil which allows C# source code to specify type constraints that are supported by the CLR but unnecessarily restricted in C#. In the process, I came across another unjustified decision regarding verification: the jmp instruction.
The jmp instruction strikes me as potentially incredibly useful for alternative dispatch techniques, and yet I recently discovered that it's classified as unverifiable. This seems very odd, since the instruction is fully statically typed, and I can't think of a way its use could corrupt the VM.
In short, the instruction performs a control transfer to a named method with a signature matching exactly the current method's signature, as long as the evaluation stack is empty and you are not currently in a try-catch block (see section 3.37 of the ECMA specification).
This seems eminently verifiable given a simple control-flow analysis, an analysis which the verifier already performs to verify control-flow safety of some other verifiable instructions. If anyone can shed some light on this I would appreciate it.