VSharp-team / VSharp

Symbolic execution engine for .NET Core
Apache License 2.0
50 stars 32 forks source link

NullReferenceException expected on correct DateTime constructor #218

Open Almazis opened 1 year ago

Almazis commented 1 year ago

Simple usage of DateTime constructor

public static DateTime DateTimeConstructor()
{
    var res = new DateTime(2022, 1, 1);
    return res;
}

generates the test with expected NullReferenceException

Before exception is generated (in ILInterpreter member x.Raise) ipstack:

[0] Instruction (54, System.UInt64 System.DateTime.DateToTicks(System.Int32, System.Int32, System.Int32))
[1] Instruction (4, System.Void System.DateTime..ctor(this, System.Int32, System.Int32, System.Int32))
[2] Instruction (7, System.DateTime IntegrationTests.Environment.DateTimeConstructor())

The latest frame points to if ((uint)day > days[month] - days[month - 1]) where array days is loaded from a static member :

private static readonly uint[] s_daysToMonth365 = {
    0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334, 365 };
private static readonly uint[] s_daysToMonth366 = {
    0, 31, 60, 91, 121, 152, 182, 213, 244, 274, 305, 335, 366 };

<...>

uint[] days = IsLeapYear(year) ? s_daysToMonth366 : s_daysToMonth365;

Possible reason for false NullReferenceException are uninitialized statics.