search

VSharp-team / VSharp

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

Stack Overflow during render-tests for inheritance example #308

Closed smhmhmd closed 9 months ago

smhmhmd commented 10 months ago

Error while trying to create unit tests for C# inheritance example from here

dotnet  VSharp\VSharp.Runner\bin\Debug\net7.0\VSharp.Runner.dll  --all-public-methods C:\Users\samiull\Documents\2023\testgen\demoproject2\bin\Debug\net6.0\demoproject2.dll -t 60 -o c:\Users\samiull\Documents\2023\testgen\out --render-tests
Stack overflow.
   at System.String.FormatHelper(System.IFormatProvider, System.String, System.ReadOnlySpan`1<System.Object>)
   at Microsoft.FSharp.Core.PrintfImpl+InterpolandToString@924.Invoke(System.Object)
   at Microsoft.FSharp.Core.PrintfImpl+PrintfEnv`3[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].RunSteps(System.Object[], System.Type[], Step[])
   at Microsoft.FSharp.Core.PrintfModule.PrintFormatToStringThen[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.FSharp.Core.PrintfFormat`4<System.__Canon,Microsoft.FSharp.Core.Unit,System.String,System.String>)
   at <StartupCode$VSharp-SILI-Core>.$Terms+toStr@160-4[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(System.String)
   at <StartupCode$VSharp-SILI-Core>.$Terms+toStr@131T[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(Int32, System.String, VSharp.Core.termNode, Microsoft.FSharp.Core.FSharpFunc`2<System.String,System.__Canon>)
   at <StartupCode$VSharp-SILI-Core>.$Terms+toStr@152-2[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(VSharp.Core.term, Microsoft.FSharp.Core.FSharpFunc`2<System.String,System.__Canon>)
   at VSharp.Cps+List.mapk[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]](Microsoft.FSharp.Core.FSharpFunc`2<System.__Canon,Microsoft.FSharp.Core.FSharpFunc`2<Microsoft.FSharp.Core.FSharpFunc`2<System.__Canon,System.__Canon>,System.__Canon>>, Microsoft.FSharp.Collections.FSharpList`1<System.__Canon>, Microsoft.FSharp.Core.FSharpFunc`2<Microsoft.FSharp.Collections.FSharpList`1<System.__Canon>,System.__Canon>)
   at VSharp.Cps+List+mapk@16[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(System.__Canon)
   at <StartupCode$VSharp-SILI-Core>.$Terms+toStr@152-3[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(Microsoft.FSharp.Collections.FSharpList`1<System.String>)
   at VSharp.Cps+List+mapk@16-2[[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e],[System.__Canon, System.Private.CoreLib, Version=7.0.0.0, Culture=neutral, PublicKeyToken=7cec85d7bea7798e]].Invoke(Microsoft.FSharp.Collections.FSharpList`1<System.__Canon>)

Here is the input:

using System;

namespace DemoProject2
{
    public enum PublicationType { Misc, Book, Magazine, Article };

    public abstract class Publication
    {
        private bool _published = false;
        private DateTime _datePublished;
        private int _totalPages;

        public Publication(string title, string publisher, PublicationType type)
        {
            if (string.IsNullOrWhiteSpace(publisher))
                throw new ArgumentException("The publisher is required.");
            Publisher = publisher;

            if (string.IsNullOrWhiteSpace(title))
                throw new ArgumentException("The title is required.");
            Title = title;

            Type = type;
        }

        public string Publisher { get; }

        public string Title { get; }

        public PublicationType Type { get; }

        public string? CopyrightName { get; private set; }

        public int CopyrightDate { get; private set; }

        public int Pages
        {
            get { return _totalPages; }
            set
            {
                if (value <= 0)
                    throw new ArgumentOutOfRangeException(nameof(value), "The number of pages cannot be zero or negative.");
                _totalPages = value;
            }
        }

        public string GetPublicationDate()
        {
            if (!_published)
                return "NYP";
            else
                return _datePublished.ToString("d");
        }

        public void Publish(DateTime datePublished)
        {
            _published = true;
            _datePublished = datePublished;
        }

        public void Copyright(string copyrightName, int copyrightDate)
        {
            if (string.IsNullOrWhiteSpace(copyrightName))
                throw new ArgumentException("The name of the copyright holder is required.");
            CopyrightName = copyrightName;

            int currentYear = DateTime.Now.Year;
            if (copyrightDate < currentYear - 10 || copyrightDate > currentYear + 2)
                throw new ArgumentOutOfRangeException($"The copyright year must be between {currentYear - 10} and {currentYear + 1}");
            CopyrightDate = copyrightDate;
        }

        public override string ToString() => Title;
    }

    public sealed class Book : Publication
    {
        public Book(string title, string author, string publisher) :
            this(title, string.Empty, author, publisher)
        { }

        public Book(string title, string isbn, string author, string publisher) : base(title, publisher, PublicationType.Book)
        {
            // isbn argument must be a 10- or 13-character numeric string without "-" characters.
            // We could also determine whether the ISBN is valid by comparing its checksum digit
            // with a computed checksum.
            //
            if (!string.IsNullOrEmpty(isbn))
            {
                // Determine if ISBN length is correct.
                if (!(isbn.Length == 10 | isbn.Length == 13))
                    throw new ArgumentException("The ISBN must be a 10- or 13-character numeric string.");
                if (!ulong.TryParse(isbn, out _))
                    throw new ArgumentException("The ISBN can consist of numeric characters only.");
            }
            ISBN = isbn;

            Author = author;
        }

        public string ISBN { get; }

        public string Author { get; }

        public decimal Price { get; private set; }

        // A three-digit ISO currency symbol.
        public string? Currency { get; private set; }

        // Returns the old price, and sets a new price.
        public decimal SetPrice(decimal price, string currency)
        {
            if (price < 0)
                throw new ArgumentOutOfRangeException(nameof(price), "The price cannot be negative.");
            decimal oldValue = Price;
            Price = price;

            if (currency.Length != 3)
                throw new ArgumentException("The ISO currency symbol is a 3-character string.");
            Currency = currency;

            return oldValue;
        }

        public override bool Equals(object? obj)
        {
            if (obj is not Book book)
                return false;
            else
                return ISBN == book.ISBN;
        }

        public override int GetHashCode() => ISBN.GetHashCode();

        public override string ToString() => $"{(string.IsNullOrEmpty(Author) ? "" : Author + ", ")}{Title}";
    }
}

VSharp Top of tree is at:

commit 0833c679b746be5de1de041510dcfb146b1bc59a (HEAD -> master, origin/master, origin/HEAD)
Merge: ee642d02 d809676a
Author: Mikhail Kosticyn <mishakosticyn@yandex.ru>
Date:   Thu Nov 30 23:22:20 2023 +0300

dotnet versions:

C:\Users\samiull\Documents\2023\testgen\VSharp>dotnet --version
8.0.100

C:\Users\samiull\Documents\2023\testgen\VSharp>dotnet --list-sdks
6.0.417 [C:\Program Files\dotnet\sdk]
8.0.100 [C:\Program Files\dotnet\sdk]

C:\Users\samiull\Documents\2023\testgen\VSharp>dotnet --list-runtimes
Microsoft.AspNetCore.App 6.0.25 [C:\Program Files\dotnet\shared\Microsoft.AspNetCore.App]
Microsoft.AspNetCore.App 7.0.14 [C:\Program Files\dotnet\shared\Microsoft.AspNetCore.App]
Microsoft.AspNetCore.App 8.0.0 [C:\Program Files\dotnet\shared\Microsoft.AspNetCore.App]
Microsoft.NETCore.App 6.0.25 [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
Microsoft.NETCore.App 7.0.14 [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
Microsoft.NETCore.App 8.0.0 [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
Microsoft.WindowsDesktop.App 6.0.25 [C:\Program Files\dotnet\shared\Microsoft.WindowsDesktop.App]
Microsoft.WindowsDesktop.App 7.0.14 [C:\Program Files\dotnet\shared\Microsoft.WindowsDesktop.App]
Microsoft.WindowsDesktop.App 8.0.0 [C:\Program Files\dotnet\shared\Microsoft.WindowsDesktop.App]
MchKosticyn commented 10 months ago

This happens, because of default configuration -- 'Debug'. To prevent stack overflow, V# uses CPS, but 'Debug' configuration does not use 'tailrec' optimization. Try to use 'Release' configuration, when building V# project.