codespecs / daikon-dot-net-front-end

Celeriac .NET Front-End for Daikon
Other
9 stars 1 forks source link

Verifier errors when rewriting assemblies with Code Contract runtime checks #82

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
What steps will reproduce the problem?
1. Compile AutoDiff with Code Contract Runtime checking

[IL]: Error: 
[C:\Projects\celeriac-sample-programs\autodiff\Core\AutoDiff.Tests\bin\Debug\Aut
oDiff.dll.instr : AutoDiff.
CompiledDifferentiator`1[T]::Differentiate[S]][offset 0x00000000] Shared try 
has finally or fault handler.
[IL]: Error: 
[C:\Projects\celeriac-sample-programs\autodiff\Core\AutoDiff.Tests\bin\Debug\Aut
oDiff.dll.instr : AutoDiff.
CompiledDifferentiator`1[T]::Differentiate][offset 0x00000000] Shared try has 
finally or fault handler.
[IL]: Error: 
[C:\Projects\celeriac-sample-programs\autodiff\Core\AutoDiff.Tests\bin\Debug\Aut
oDiff.dll.instr : AutoDiff.
ParametricCompiledTerm::Differentiate][offset 0x00000000] Shared try has 
finally or fault handler.
[IL]: Error: 
[C:\Projects\celeriac-sample-programs\autodiff\Core\AutoDiff.Tests\bin\Debug\Aut
oDiff.dll.instr : AutoDiff.
TVec::op_Addition][offset 0x00000000] Shared try has finally or fault handler.
[IL]: Error: 
[C:\Projects\celeriac-sample-programs\autodiff\Core\AutoDiff.Tests\bin\Debug\Aut
oDiff.dll.instr : AutoDiff.
TVec::op_Subtraction][offset 0x00000000] Shared try has finally or fault 
handler.
5 Error(s) Verifying AutoDiff.dll.instr

Original issue reported on code.google.com by Todd.Sch...@gmail.com on 18 Mar 2013 at 6:57

GoogleCodeExporter commented 9 years ago
I think this is an error in exception handler branching.

I see the following in the Autodiff.TVec op_subtraction method

ILSpy produces this strange output:

            IL_00b9: call void System.Diagnostics.Contracts.__ContractsRuntime::Requires(bool, string, string)
            IL_00be: nop
            IL_00bf: leave.s IL_00ce
        } // end .try
        finally
        {
            IL_00c1: ldsfld int32 System.Diagnostics.Contracts.__ContractsRuntime::insideContractEvaluation
            IL_00c6: ldc.i4.1
            IL_00c7: sub
            IL_00c8: stsfld int32 System.Diagnostics.Contracts.__ContractsRuntime::insideContractEvaluation
            IL_00cd: endfinally
        } // end handler

        IL_00ce: ldarg.0
        IL_00cf: stloc.1
        IL_00d0: leave.s IL_00d8
        catch [mscorlib]System.Exception
        {
            IL_00d2: brtrue.s IL_00d6

            IL_00d4: rethrow

            IL_00d6: leave.s IL_00d8
        } // end handler

        IL_00d8: nop
        IL_00d9: ldarg.0
        IL_00da: ldfld class AutoDiff.Term[] AutoDiff.TVec::terms

Looking in ILSpy I see this:
    IL_00d2:  brtrue.s   IL_00d6
    IL_00d4:  rethrow
    IL_00d6:  leave.s    IL_00d8
    IL_00d8:  nop
    .try IL_0073 to IL_00c1 catch [mscorlib]System.Exception handler IL_00d2 to IL_00d8

Original comment by melonhea...@gmail.com on 18 Mar 2013 at 7:33

GoogleCodeExporter commented 9 years ago

Original comment by melonhea...@gmail.com on 2 Apr 2013 at 8:53

GoogleCodeExporter commented 9 years ago
I suspect there's an issue when a finally block is followed directly by another 
try block, where the second try block gets dropped:

        .try
        {
               ...
        }
    finally
    {
        IL_007a: ldsfld int32 System.Diagnostics.Contracts.__ContractsRuntime::insideContractEvaluation
        IL_007f: ldc.i4.1
        IL_0080: sub
        IL_0081: stsfld int32 System.Diagnostics.Contracts.__ContractsRuntime::insideContractEvaluation
        IL_0086: endfinally
    } // end handler
    .try
    {
        IL_0087: ldarg.1
        IL_0088: stloc.s 4
        IL_008a: leave IL_009b
    } // end .try
    catch [mscorlib]System.Exception
    {
        IL_008f: brtrue IL_0096
        IL_0094: rethrow
        IL_0096: leave IL_009b
    } // end handler

Original comment by Todd.Sch...@gmail.com on 8 Apr 2013 at 1:12

GoogleCodeExporter commented 9 years ago
This can't be recreated directly using only vanilla C#, since the C# compiler 
puts a couple NOPs between the finally and subsequent try block.

Original comment by Todd.Sch...@gmail.com on 9 Apr 2013 at 10:43

GoogleCodeExporter commented 9 years ago
I've attached a small repro for the verifier error from AutoDiff

Original comment by Todd.Sch...@gmail.com on 20 May 2013 at 5:05

Attachments:

GoogleCodeExporter commented 9 years ago
Fixed in 63c7a81da4ec

Original comment by melonhea...@gmail.com on 8 Jun 2013 at 9:09

GoogleCodeExporter commented 9 years ago

Original comment by melonhea...@gmail.com on 8 Jun 2013 at 9:09