Why is this .Net IL not verifiable?

Question

I have a bit of custom IL I wrote and it won't pass PEVerify. The error I get is

$ peverify foo.exe

Microsoft (R) .NET Framework PE Verifier.  Version  4.0.30319.17929
Copyright (c) Microsoft Corporation.  All rights reserved.

[IL]: Error: [Z:\virtualbox_shared\foo.exe : HelloWorld.Program::Main][offset 0x00000021] Stack height at all points must be determinable in a single forward scan of IL.
1 Error(s) Verifying foo.exe

The program however will run fine without any exceptions. Here is the IL of the relevant method:

.method private static hidebysig
  default void Main (string[] args)  cil managed
{
// Method begins at RVA 0x2050
.entrypoint
// Code size 54 (0x36)
.maxstack 2

//custom IL
ldc.i4 1
ldc.i4 1
ceq
switch(first, second)

first:
ldc.i4 1
br.s temp
popit: pop
br.s second

temp: ldc.i4 1
brfalse temp2
temp2: br.s popit

second:
ldc.i4 2
pop

ret

} // end of method Program::Main

The full source code is at pastebin

Why am I getting this error?

Cockroach

I don't fully understand the logic, but it looks related to 1.7.5 Backward Branch Contraints (books.google.com/…) – Tablespoon

@Tablespoon I'm not really seeing that as applying here. Take a look at this code which passes verification.(in particular, the IL_0018 label) – Cockroach

Answer 1

must be determinable in a single forward scan of IL

That's the key part of the verification failure. The verifier doesn't try to verify every single branch path, that would require solving the Halting Problem. It is unhappy about the POP, it cannot see in a single forward scan that this opcode is reached by the backward branch with a non-empty stack and is therefore valid.

Sanborn

So it would appear that even my "workaround" only just happens to pass Microsoft's peverify. Looking in Partition III 1.7.5 of the ECMA spec this code appears to be completely non-conforming. I assume that local-variables in this case should be used rather than the stack – Cockroach

That's what any real compiler would do, yes. – Sanborn

Answer 2

I don't fully understand why this is the answer, but this caused it to PEVerify:

.method private static hidebysig
  default void Main (string[] args)  cil managed
{
// Method begins at RVA 0x2050
.entrypoint
// Code size 54 (0x36)
.maxstack 2

//custom IL
ldc.i4 1
ldc.i4 1
ceq
switch(first, second)

first:
ldc.i4 1
br.s temp
ldc.i4 1 //not reached, but required!
popit: pop
br.s second

temp: ldc.i4 1
brfalse temp2
temp2: br.s popit

second:
ldc.i4 2
pop

ret

} // end of method Program::Main

Cockroach