Exit PPTs not created for method throwing an exception

[GoogleCodeExporter]

What steps will reproduce the problem?

Here's an example from the Absy class of https://boogie.codeplex.com/.

public virtual Absy StdDispatch(StandardVisitor visitor) {
  Contract.Requires(visitor != null);
  Contract.Ensures(Contract.Result<Absy>() != null);
  System.Diagnostics.Debug.Fail("Unknown Absy node type: " + this.GetType());
      throw new System.NotImplementedException();
}

What is the expected output? What do you see instead?

Celeriac doesn't create an exit PPT for this method, which causes a error in 
Daikon since the exit PPT is marked as parent of the overridding methods.

Original issue reported on code.google.com by Todd.Sch...@gmail.com on 10 Jun 2013 at 1:05

[GoogleCodeExporter]

Hmm this is strange, Celeriac doesn't seem to be generating a try/catch block 
at all.

Original comment by melonhea...@gmail.com on 10 Jun 2013 at 10:51

[GoogleCodeExporter]

The exception handling code never gets called because there's no ret 
instruction, which is when it normally gets triggered. 

Original comment by melonhea...@gmail.com on 10 Jun 2013 at 11:14

[GoogleCodeExporter]

Do we need to detect methods with no return instruction as a special case, and 
force them to have a regular exit ppt, and an exception exception ppt for the 
exception that is thrown?

Original comment by Todd.Sch...@gmail.com on 10 Jun 2013 at 3:32

[GoogleCodeExporter]

We need to either insert a fake return (but this causes the rewriter to crash), 
or move the method ending code out of the section of the switch statement it's 
currently in inside EmitOperations().

Original comment by melonhea...@gmail.com on 10 Jun 2013 at 9:04

[GoogleCodeExporter]

Since these methods won't likely actually be called, would an appropriate 
solution (for now) be to output the DECLS but not have the correct MSIL?

If the method was ever called, Daikon would complain that it saw unmatched 
entries, but would still be able to output invariants.

Original comment by Todd.Sch...@gmail.com on 10 Jun 2013 at 9:13

[GoogleCodeExporter]

I somewhat did this. I declare a fake return, and include a return instruction 
so the IL will verify. Fixed in ab269b1a3be5

Original comment by melonhea...@gmail.com on 11 Jun 2013 at 8:39

[GoogleCodeExporter]

Kellen fixed in ab269b1a3be5

Original comment by Todd.Sch...@gmail.com on 11 Jun 2013 at 7:58

• Changed state: Fixed

[GoogleCodeExporter]

I think your fix produces invalid IL. Here's the output I get when 
instrumenting the Absy class in Boogie 
)https://boogie.codeplex.com/SourceControl/latest#Source/Core/Absy.cs):

[IL]: Error: [C:\Projects\scratch\boogie\Binaries\Core.dll.instr : 
Microsoft.Boogie.Absy::StdDispatch][offset 0x000000CC
] Return value missing on the stack.

Looks like you may need to also throw a dummy value onto the stack.

Original comment by Todd.Sch...@gmail.com on 12 Jun 2013 at 2:01

• Changed state: Started

[GoogleCodeExporter]

I'll add a dummy value. What part of Absy are you running on so I can check 
this myself, if this fix doesn't work?

Original comment by melonhea...@gmail.com on 12 Jun 2013 at 9:05

[GoogleCodeExporter]

I downloaded Boogie from https://boogie.codeplex.com/releases/view/96678 and 
tried to instrument Core.dll using the 
--ppt-select-pattern="^Microsoft.Boogie.Absy" option.

Original comment by Todd.Sch...@gmail.com on 12 Jun 2013 at 3:38

[GoogleCodeExporter]

Original comment by Todd.Sch...@gmail.com on 14 Jun 2013 at 5:30

• Added labels: Milestone-Release1.0

[GoogleCodeExporter]

Dropping to medium priority, since this only causes a problem for virtual 
methods that have an overriding method.

Original comment by Todd.Sch...@gmail.com on 14 Jun 2013 at 5:31

• Added labels: Priority-Medium
• Removed labels: Priority-High, Milestone-Release1.0

[GoogleCodeExporter]

Fixed in dbee1fea4359, checked against the Absy class described above and the 
whole DLL, both of which pass the verifier

Original comment by melonhea...@gmail.com on 14 Jun 2013 at 10:30

• Changed state: Fixed