vsharp-team / vsharp Goto Github PK

Symbolic execution engine for .NET Core

License: Apache License 2.0

F# 13.03% C# 8.15% CMake 0.49% C++ 63.89% C 13.56% Perl 0.13% Objective-C 0.01% Pawn 0.10% Assembly 0.64% Batchfile 0.01%

testing symbolic-execution test-generation

vsharp's People

Contributors

Stargazers

Watchers

vsharp's Issues

NRE on rendering Blogifier test with enums

Commit: 4ce8161

Get https://github.com/blogifierdotnet/Blogifier project (commit 150b145)
Publish it
Try to run Runner CLI on SetPostType method with test rendering
Get NRE on test Rendering in Release or Assertion failed in Debug config

Incorrect namespace generation

Description

Wrong namespace is generated for the project stored in directory containing - in its name.

Environment

Docker, Ubuntu 20.04, .NET 6.0, Mono 6
VSharp console runner with special option --single-file

Steps to reproduce

Run command such as (for the source code below):

dotnet /usr/src/vsharp_runner/VSharp.Runner.dll --all-public-methods /usr/src/binary-search/bin/Debug/net6.0/binary-search.dll --render-tests --single-file
See generated file contains incorrect namespace (binary-search)

Source code

public static class Algorithms {
	public static int BinarySearch(int value, int[] a)
	{
		var l = a.GetLowerBound(0);
		var r = a.GetLength(0);
		while (l < r)
		{
			var mid = (l + r) / 2;
			int element = a[mid];
			if (element == value)
				return mid;
			if (element < value)
				r = mid - 1;
			l = mid + 1;
		}
		return -1;
	}
}

Generated tests

using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
using System.Runtime.Serialization;
using NUnit.Framework;

namespace VSharp.TestExtensions
{

internal static class CartesianProductExtension
{
    internal static IEnumerable<IEnumerable<T>> CartesianProduct<T>(this IEnumerable<IEnumerable<T>> sequences)
    {
        IEnumerable<IEnumerable<T>> emptyProduct =
            new[] { Enumerable.Empty<T>() };
        return sequences.Aggregate(
            emptyProduct,
            (accumulator, sequence) =>
                from accseq in accumulator
                from item in sequence
                select accseq.Concat(new[] {item}));
    }
}

public static class Allocator
{
    private static void FillFast<TElem>(Array? arr, TElem value)
    {
        if (arr != null)
        {
            ref var bytePtr = ref MemoryMarshal.GetArrayDataReference(arr);
            ref var ptr = ref Unsafe.As<byte, TElem>(ref bytePtr);
            var span = MemoryMarshal.CreateSpan(ref ptr, arr.Length);
            span.Fill(value);
        }
    }

    /// Fills zero-initialized array with value
    public static void Fill(Array? arr, object? value)
    {
        if (value == null)
        {
            // Do nothing because arr is already filled with nulls
            return;
        }

        var t = value.GetType();
        if (arr != null && (!t.IsValueType || Nullable.GetUnderlyingType(t) != null ||
                            value != FormatterServices.GetUninitializedObject(t)))
        {
            var elementType = arr.GetType().GetElementType();
            switch (value)
            {
                case int i when elementType == typeof(int):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(byte):
                    FillFast(arr, i);
                    break;
                case char i when elementType == typeof(char):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(uint):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(Int64):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(UInt64):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(double):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(float):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(Int16):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(UInt16):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(sbyte):
                    FillFast(arr, i);
                    break;
                default:
                    var rank = arr.Rank;
                    var indices =
                        Enumerable.Range(0, rank)
                            .Select(i => Enumerable.Range(arr.GetLowerBound(i), arr.GetLength(i)))
                            .CartesianProduct();
                    foreach (var i in indices)
                    {
                        arr.SetValue(value, i.ToArray());
                    }

                    break;
            }
        }
    }
}

public class Allocator<T>
{
    private readonly Type _objectType = typeof(T);
    private readonly object _toAllocate;

    public Allocator()
    {
        _toAllocate = FormatterServices.GetUninitializedObject(_objectType);
    }

    public Allocator(string typeName)
    {
        Type? notPublicType = Type.GetType(typeName);
        _objectType = notPublicType ?? _objectType;
        _toAllocate = FormatterServices.GetUninitializedObject(_objectType);
    }

    public Allocator(object? defaultValue, params int[] lengths)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = Array.CreateInstance(_objectType.GetElementType()!, lengths);
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public Allocator(object? defaultValue, int[] lengths, int[] lowerBounds)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = Array.CreateInstance(_objectType.GetElementType()!, lengths, lowerBounds);
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public Allocator(object allocated)
    {
        _toAllocate = allocated;
    }

    public Allocator(object allocated, object defaultValue)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = allocated;
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public object this[string fieldName]
    {
        set
        {
            var allBindingFlags = BindingFlags.Instance | BindingFlags.NonPublic | BindingFlags.Public;
            var field = _objectType.GetField(fieldName, allBindingFlags);
            var property = _objectType.GetField($"<{fieldName}>k__BackingField", allBindingFlags);
            Debug.Assert(field != null || property != null);
            field ??= property;
            if (field != null)
                field.SetValue(_toAllocate, value);
        }
    }

    public object this[params int[] index]
    {
        set
        {
            Debug.Assert(_objectType.IsArray);
            var array = _toAllocate as Array;
            array?.SetValue(value, index);
        }
    }

    public T Object => (T)_toAllocate;
}

public static class ObjectsComparer
{
    private static bool StructurallyEqual(object? expected, object? got)
    {
        Debug.Assert(expected != null && got != null && expected.GetType() == got.GetType());
        var flags = BindingFlags.Public | BindingFlags.NonPublic | BindingFlags.Instance;
        var fields = expected.GetType().GetFields(flags);
        foreach (var field in fields)
        {
            if (!typeof(MulticastDelegate).IsAssignableFrom(field.FieldType) &&
                !field.Name.Contains("threadid", StringComparison.OrdinalIgnoreCase) &&
                !CompareObjects(field.GetValue(expected), field.GetValue(got)))
            {
                return false;
            }
        }

        return true;
    }

    private static bool ContentwiseEqual(global::System.Array? expected, global::System.Array? got)
    {
        Debug.Assert(expected != null && got != null && expected.GetType() == got.GetType());
        if (expected.Rank != got.Rank)
            return false;
        for (int i = 0; i < expected.Rank; ++i)
            if (expected.GetLength(i) != got.GetLength(i) || expected.GetLowerBound(i) != got.GetLowerBound(i))
                return false;
        var enum1 = expected.GetEnumerator();
        var enum2 = got.GetEnumerator();
        while (enum1.MoveNext() && enum2.MoveNext())
        {
            if (!CompareObjects(enum1.Current, enum2.Current))
                return false;
        }
        return true;
    }

    public static bool CompareObjects(object? expected, object? got)
    {
        if (expected == null)
            return got == null;
        if (got == null)
            return false;
        var type = expected.GetType();
        if (type != got.GetType())
            return false;

        if (Object.ReferenceEquals(expected, got))
            return true;

        if (type == typeof(Pointer) || type.IsPrimitive || expected is string || type.IsEnum)
        {
            // TODO: compare double with epsilon?
            return got.Equals(expected);
        }

        if (expected is global::System.Array array)
            return ContentwiseEqual(array, got as global::System.Array);
        return StructurallyEqual(expected, got);
    }
}
}

namespace binary-search.Tests
{
[TestFixture]
class AlgorithmsTests
{
    [Test, Category("Generated")]
    public void BinarySearchError()
    {
        // act
        Algorithms.BinarySearch(0, null!);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest()
    {
        // arrange
        int[] a = new int[1];

        // act
        var result = Algorithms.BinarySearch(0, a);

        // assert
        Assert.AreEqual(0, result);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest1()
    {
        // arrange
        int[] a = new int[0];

        // act
        var result = Algorithms.BinarySearch(0, a);

        // assert
        Assert.AreEqual(-1, result);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest2()
    {
        // arrange
        int[] a = new int[1];

        // act
        var result = Algorithms.BinarySearch(1, a);

        // assert
        Assert.AreEqual(-1, result);
    }
}}

Typo in test runner's option name

I guess that Test suit should be renamed to Test suite

All types and modules in VSharp namespace are visible from NuGet package

NuGet package version: 0.0.6 (in 0.0.5 there is no problem)

V# generates incorrect test: an attempt to use Object instead of specific type

Test to reproduce
Steps to reproduce
- Remove this attribute
- Run the test
- Compile generated tests
- Get a number of erros KnapsackBagTests.cs(23, 21): [CS1061] 'object' does not contain a definition for 'Calculate' and no accessible extension method 'Calculate' accepting a first argument of type 'object' could be found (are you missing a using directive or an assembly reference?)

`Cast (System.Boolean, System.Byte)` is not supported in Z3 EncodeExpression

V# throws "The method or operation is not implemented." from Z3 EncodeExpression. Looks like the case Cast (System.Boolean, System.Byte) is not supported.

Steps to eproduce

Run this test

Low coverage example

For this test 50% coverage can be achieved in few seconds, but even 51% can not be reached in reasonable time (with default settings).

Test generation failed: `Microsoft.Z3.Z3Exception: invalid argument`

Steps to reproduce:

Run this test

Get an exception:

Microsoft.Z3.Z3Exception: invalid argument
at Microsoft.Z3.Native.Z3_mk_int(IntPtr a0, Int32 a1, IntPtr a2)
at Microsoft.Z3.Context.MkNumeral(Int32 v, Sort ty)
at [email protected](Expr[] k) in /home/gsv/Projects/VSharp/VSharp.Solver/Z3.fs:line 587
at VSharp.Solver.Z3.Z3Builder.MemoryReading[h,a,b,i,j,k,l,m](encodingContext encCtx, FSharpFunc`2 specializeWithKey, FSharpFunc`2 keyInRegion, FSharpFunc`2 keysAreMatch, FSharpFunc`2 encodeKey, FSharpFunc`2 inst, FSharpList`1 structFields, h left, memoryRegion`2 mo, m typ) in

Generate extensions code when it's required

Description

When tests are generated with VSharp.Runner, tests extensions are always included into generated tests.
When we generate tests without special option --single-file they are generated into Extensions directory. When we use special option --single-file extensions are generated into file with tests.

Expected

Extensions are generated only when they are required for tests.

To reproduce

VSharp console runner with special option --single-file:

dotnet /usr/src/vsharp_runner/VSharp.Runner.dll --all-public-methods /usr/src/project/bin/Debug/net6.0/project.dll --render-tests --single-file

Stack Overflow during render-tests for inheritance example

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 [email protected](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 <[email protected]>
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]

Change DeclaringType to ReflectedType

Test all usages of DeclaringType and change them on ReflectedType if need.

V# generates incorrect test

V# generates test which can not be compiled.

Steps to reproduce

Change attribute of this test to [TestSvm(100,guidedMode:false)]
Run test
Try to compile generated test which should looks like follows.

[Test, Category("Generated")]
    public void KMPSearchMainTest()
    {
        // arrange
        List<int> expected = new Allocator<List<int>>{
            ["_items"] = new[]{},
            ["_size"] = 0,
            ["_version"] = 0
        }.Object;

        // act
        var result = KMPSearch.KMPSearchMain("", "!");

        // assert
        Assert.IsTrue(CompareObjects(expected, result));
    }

You shoulg get a compilation error No best type found for implicitly-typed array

Place tests extensions code after tests

Description

When tests are generated into single file with VSharp.Runner, tests extensions code is placed before tests code. This is inconvenient for the user as the user should scroll file with tests to see tests.

To reproduce

VSharp console runner with special option --single-file:

dotnet /usr/src/vsharp_runner/VSharp.Runner.dll --all-public-methods /usr/src/project/bin/Debug/net6.0/project.dll --render-tests --single-file

Web benchmark: 'Could not load file or assembly' in VSharp.Mocking.Type.Build

Run V# CLI (2a3e2d9) on https://github.com/VSharp-team/VSharp-bench/blob/327df044c180ff2679d1b0509d2c6b9c0c0bd360/max_arshinov_web/HightechAngular.Web.dll (commit a85c3d1)
with params: --method get_Cart D:\VSharp-bench\max_arshinov_web\HightechAngular.Web.dll --render-tests, Debug configuration
Get the following error:

[Error] [12/29/2022 4:00:42 PM] Tests renderer: deserialization of test failed: System.IO.InvalidDataException: Input test is incorrect
 ---> System.IO.FileNotFoundException: Could not load file or assembly 'Microsoft.AspNetCore.Http.Features, Version=3.1.0.0, Culture=neutral, PublicKeyToken=adb9793829ddae60'
. The system cannot find the file specified.
File name: 'Microsoft.AspNetCore.Http.Features, Version=3.1.0.0, Culture=neutral, PublicKeyToken=adb9793829ddae60'
   at System.Reflection.Emit.TypeBuilder.CreateTypeNoLock()
   at System.Reflection.Emit.TypeBuilder.CreateType()
   at VSharp.Mocking.Type.Build(ModuleBuilder moduleBuilder) in D:\VSharp-fork\VSharp.Utils\Mocking.fs:line 204
   at VSharp.Mocking.Mocker.BuildDynamicType(typeMockRepr repr) in D:\VSharp-fork\VSharp.Utils\Mocking.fs:line 320
   at VSharp.Mocking.Mocker.VSharp.ITypeMockSerializer.Deserialize(FSharpFunc`2 decode, Object repr) in D:\VSharp-fork\VSharp.Utils\Mocking.fs:line 290
   at VSharp.MemoryGraph..ctor(memoryRepr repr, ITypeMockSerializer mocker, Boolean createCompactRepr) in D:\VSharp-fork\VSharp.Utils\MemoryGraph.fs:line 131
   at VSharp.UnitTest..ctor(MethodBase m, testInfo info, Boolean createCompactRepr) in D:\VSharp-fork\VSharp.Utils\UnitTest.fs:line 58
   at VSharp.UnitTest.DeserializeFromTestInfo(testInfo ti, Boolean createCompactRepr) in D:\VSharp-fork\VSharp.Utils\UnitTest.fs:line 215
   --- End of inner exception stack trace ---
   at VSharp.UnitTest.DeserializeFromTestInfo(testInfo ti, Boolean createCompactRepr) in D:\VSharp-fork\VSharp.Utils\UnitTest.fs:line 218
   at VSharp.TestRenderer.Renderer.DeserializeTest(FileInfo test) in D:\VSharp-fork\VSharp.TestRenderer\RendererTool.cs:line 541
   at VSharp.TestRenderer.Renderer.DeserializeTests(IEnumerable`1 tests) in D:\VSharp-fork\VSharp.TestRenderer\RendererTool.cs:line 551

Support for various non-zero exit codes for cli utilities

Now VSharp and TestRunner will return a null code even if some of the tests fail, or if exceptions are thrown during branch parsing.

I propose to consider the possibility of returning different codes depending on the quality of the work done. For example, if most of the generated tests fail, then you can return a special code. Also, the codes may depend on the degree of importance of the detected errors.

An example of such a system can be found here: https://pvs-studio.com/en/docs/manual/0035/.

The proposed approach will make it more convenient to embed VSharp in CI systems - automation will be able to interpret the results in a single way. In particular, it will be easier for us to understand with what status the benchmarks ended.

Generated test seems incomplete for this input

Hi @MchKosticyn,

For the following input, I am not seeing tests for the "true branches" for CheckSolution(), please try this out and let me know, thanks again.

$ cat testgen.bat 
dotnet ..\..\..\testGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll  --method CheckSolution bin\Debug\net6.0\BranchesAndLoops.dll -t 90 -o ..\out --render-tests --run-tests -v Trace

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2023/testgen/testgen/csharp/branches-quickstart
$ cat EightQueens.cs 
using System;

namespace BranchesAndLoops
{
    public class EightQueens
    {
        private readonly int[][] _board;
        private const int N = 8;

        public EightQueens(int[][] board)
        {
            this._board = board;
            if (board.Length != N*N)
            {
                throw new ArgumentException("Board length is not 64");
            }
        }

        private bool IsSafe(int row, int col)
        {

            // check if there is a queen in the same row to the
            // left
            for (int x = 0; x < col; x++)
                if (_board[row][x] == 1)
                    return false;

            // check if there is a queen in the upper left
            // diagonal
            for (int x = row, y = col; x >= 0 && y >= 0;
                 x--, y--)
                if (_board[x][y] == 1)
                    return false;

            // check if there is a queen in the lower left
            // diagonal
            for (int x = row, y = col; x < N && y >= 0;
                 x++, y--)
                if (_board[x][y] == 1)
                    return false;

            // if there is no queen in any of the above
            // positions, then it is safe to place a queen
            return true;
        }

        public bool CheckSolution()
        {
            if (this._board.Length == 0)
            {
                Console.WriteLine("Return false");
                return false;
            }

            int numQueens = 0;
            for (int i = 0; i < N; i++)
            {
                for (int j = 0; j < N; j++)
                {
                    if (_board[i][j] == 1)
                    {
                        numQueens++;
                    }
                }
            }

            if (numQueens != N)
            {
                return false;
            }

            for (int row = 0; row < this._board.Length/2; row++)
            {
                for (int col = 0; col < this._board.Length/2; col++)
                {
                    if (!IsSafe(row, col))
                    {
                        Console.WriteLine("Return false");
                        return false;
                    }
                }
            }

            Console.WriteLine("Return true");
            return true;
        }

    }
}

/tmp directory grows in size too much during test execution on Linux Mint

Specs: Linux Mint 20.1 Ulyssa, Intel(R) Core(TM) i5-8250U CPU @ 1.60GHz, 4 Gb DDR4 (dual boot with Windows 10)
Commit: a8eaebb
.NET version: 6.0.200

Problem: After running the tests with dotnet test -c Release /tmp grows in size too much:

sudo watch "du -skh /tmp"
233M    /tmp
... running tests ...
5,9G    /tmp

After next runs it grows again by the same size and gets larger and larger

As it turns out, the directory /tmp/JetBrainsPerUserTemp-1000-1 is filled with a lot of temporary files 4.2 MB each which look like jb.106018.u5z461.tmp

Implement Memory.getHashCode for value types

Now there is an assertion in Memory.getHashCode which requires the passed object to be of reference type

An example of method for which this assertion fails is JetBrains.Collections.ReferenceEqualityComparer<JetBrains.Threading.ByteBufferAsyncProcessor>.GetHashCode(JetBrains.Threading.ByteBufferAsyncProcessor) in JetBrains.Lifetimes benchmark

V# generates incorrect test: an attempt to instantiate private class

V# version to reproduce
Test to reproduce
Steps
- Run the test
- Compile generated tests
- Get a number of errors " GraphTests.cs(107, 34): [CS0122] 'Graph.Edge' is inaccessible due to its protection level"

Tests renderer: deserialization of test failed due to System.Collections.Generic.KeyNotFoundException

Commit: 00bf945 with cherry-picked fc58e4af529a0e402d6c37d19f07e551da7ece39 (from @MchKosticyn fork)

Tested code:

namespace NetFeaturesDemo;

public enum EventType
{
    Save,
    Change
}

public record Event(int UserId, EventType Type, string Delta);

public interface ISaver<in T>
{
    bool Save(IEnumerable<T> deltas);
}

public static class AutoSaveService
{
    public static bool AutoSave(int userId, int autoSaveThreshold, ISaver<string> saver)
    {
        var events = new List<Event>
        {
            new Event(1, EventType.Change, "gcctaca"),
            new Event(1, EventType.Change, "ctccagg"),
            new Event(1, EventType.Save, ""),
            new Event(1, EventType.Change, "gatagtc"),
            new Event(2, EventType.Change, "agcggaa"),
        };

        var notSavedChanges =
            from e in events where e.UserId == userId select e;
        notSavedChanges = notSavedChanges.TakeWhile(e => e.Type == EventType.Change);

        if (notSavedChanges.Count() > autoSaveThreshold)
        {
            return saver.Save(from e in notSavedChanges select e.Delta);
        }

        return false;
    }
}

Runner config: --all-public-methods <dll path> --render-tests --single-file --output <output path>

Stack trace:

[Error] [15/12/2022 12:50:36] Tests renderer: deserialization of test failed: System.IO.InvalidDataException: Input test is incorrect
 ---> System.Collections.Generic.KeyNotFoundException: An index satisfying the predicate was not found in the collection.
   at Microsoft.FSharp.Collections.SeqModule.Find[T](FSharpFunc`2 predicate, IEnumerable`1 source) in D:\a\_work\1\s\src\FSharp.Core\seq.fs:line 811
   at VSharp.methodRepr.Decode() in D:\VSharp\VSharp.Utils\Mocking.fs:line 21
   at [email protected](methodRepr m, Object[] c) in D:\VSharp\VSharp.Utils\Mocking.fs:line 153
   at Microsoft.FSharp.Collections.ArrayModule.Map2[T1,T2,TResult](FSharpFunc`2 mapping, T1[] array1, T2[] array2) in D:\a\_work\1\s\src\FSharp.Core\array.fs:line 393
   at VSharp.Mocking.Type..ctor(typeMockRepr repr) in D:\VSharp\VSharp.Utils\Mocking.fs:line 153
   at VSharp.UnitTest..ctor(MethodBase m, testInfo info, Boolean createCompactRepr) in D:\VSharp\VSharp.Utils\UnitTest.fs:line 57
   at VSharp.UnitTest.DeserializeFromTestInfo(testInfo ti, Boolean createCompactRepr) in D:\VSharp\VSharp.Utils\UnitTest.fs:line 215
   --- End of inner exception stack trace ---
   at VSharp.UnitTest.DeserializeFromTestInfo(testInfo ti, Boolean createCompactRepr) in D:\VSharp\VSharp.Utils\UnitTest.fs:line 218
   at VSharp.TestRenderer.Renderer.DeserializeTest(FileInfo test) in D:\VSharp\VSharp.TestRenderer\RendererTool.cs:line 539
   at VSharp.TestRenderer.Renderer.DeserializeTests(IEnumerable`1 tests) in D:\VSharp\VSharp.TestRenderer\RendererTool.cs:line 549
[Error] [15/12/2022 12:50:37] Tests renderer: rendering test failed: System.NotImplementedException: rendering constructors not supported yet
   at VSharp.TestRenderer.TestsRenderer.RenderTestsForType(IEnumerable`1 tests, ProgramRenderer testsProgram, ProgramRenderer mocksProgram, Type declaringType, Boolean wrapErrors) in D
:\VSharp\VSharp.TestRenderer\TestsRenderer.cs:line 588

NB: generation for this code works fine

public static class Linq
{
    private enum EventType
    {
        Save,
        Change
    }

    private record Event(int UserId, EventType Type, string Delta);

    public interface ISaver<in T>
    {
        bool Save(IEnumerable<T> deltas);
    }

    public static class AutoSaveService
    {
        public static bool AutoSave(int userId, int autoSaveThreshold, ISaver<string> saver)
        {
            var events = new List<Event>
            {
                new Event(1, EventType.Change, "gcctaca"),
                new Event(1, EventType.Change, "ctccagg"),
                new Event(1, EventType.Save, ""),
                new Event(1, EventType.Change, "gatagtc"),
                new Event(2, EventType.Change, "agcggaa"),
            };

            var notSavedChanges =
                from e in events where e.UserId == userId select e;
            notSavedChanges = notSavedChanges.TakeWhile(e => e.Type == EventType.Change);

            if (notSavedChanges.Count() > autoSaveThreshold)
            {
                return saver.Save(from e in notSavedChanges select e.Delta);
            }

            return false;
        }
    }
}

Generate tests for code written in older .NET frameworks

Hi @MchKosticyn

Nopcommerce-release-3.80 uses the older Windows-based .NET Framework (VS upgrades to .NET Framework 4.8), can VSharp generate tests for such code, I got this error while running VSharp from Visual Studio on Windows-10:

Unhandled exception: System.TypeLoadException: Could not load type 'System.Web.HttpResponseBase' from assembly 'System.Web, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.
   at System.RuntimeMethodHandle.GetMethodBody(IRuntimeMethodInfo method, RuntimeType declaringType)
   at System.Reflection.RuntimeMethodInfo.GetMethodBody()
   at VSharp.CSharpUtils.ReflectionUtils.<>c__DisplayClass1_0.<EnumerateExplorableMethods>b__0(MethodInfo m) in D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.CSharpUtils\ReflectionUtils.cs:line 23
   at System.Linq.Enumerable.WhereArrayIterator`1.MoveNext()
   at VSharp.CSharpUtils.ReflectionUtils.EnumerateExplorableMethods(Type type)+MoveNext() in D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.CSharpUtils\ReflectionUtils.cs:line 23
   at System.Linq.Enumerable.SelectManySingleSelectorIterator`2.MoveNext()
   at System.Collections.Generic.List`1..ctor(IEnumerable`1 collection)
   at VSharp.TestGenerator.Cover(Assembly assembly, VSharpOptions options, Boolean renderSingleFile) in D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.API\VSharp.cs:line 455
   at VSharp.Runner.RunnerProgram.AllPublicMethodsHandler(FileInfo assemblyPath, Int32 timeout, Int32 solverTimeout, DirectoryInfo output, Boolean renderTests, Boolean runTests, SearchStrategy strat, Verbosity verbosity, UInt32 recursionThreshold, ExplorationMode explorationMode) in D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.Runner\RunnerProgram.cs:line 173
   at VSharp.Runner.RunnerProgram.<>c__DisplayClass9_0.<Main>b__9(InvocationContext context) in D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.Runner\RunnerProgram.cs:line 451
   at System.CommandLine.Invocation.AnonymousCommandHandler.Invoke(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous l

Command in Visual Studio is --all-public-methods D:\Users\samiull\Documents\2024\nopCommerce-release-3.80\src\Presentation\Nop.Web\bin\Nop.Core.dll -t 30 -o ..\out -v Trace

Cannot resolve generic type on rendering tests

Commit: 4ce8161

Run VSharp runner CLI on method ForEachValue in JetBrains.Lifetimes (also available in bench repo) with test rendering enabled
Test renderer fails with NRE due to not resolved generic type
TestRunner works fine with generated .vst files!

API.Restore() crashes in SILI.fs if there was an exception before API.Reset()

If there was an exception in SILI.Interpret before call to API.Reset(), V# crashes in finally with not pretty looking exception:


 ---> System.InvalidOperationException: Stack empty.
   at System.Collections.Generic.Stack`1.ThrowForEmptyStack()
   at System.Collections.Generic.Stack`1.Pop()
   at VSharp.persistent`1.Restore() in D:\VSharp\VSharp.Utils\Persistent.fs:line 9
   at VSharp.IdGenerator.restore() in D:\VSharp\VSharp.Utils\IdGenerator.fs:line 48
   at VSharp.Core.API.Restore() in D:\VSharp\VSharp.SILI.Core\API.fs:line 19

[README] Add CPP part related stuff to requirements

Add LLVM/GGC version and other information to README to simplify build from scratch.

V#.Runner could not find public method of nested public static type

public static class Linq
{
    private enum EventType
    {
        Save,
        Change
    }
    private record Event(int UserId, EventType Type, string Delta);
    public interface ISaver<in T>
    {
        bool Save(IEnumerable<T> deltas);
    }
    public static class AutoSaveService
    {
        public static bool AutoSave(int userId, int autoSaveThreshold, ISaver<string> saver)
        {
            var events = new List<Event>
            {
                new Event(1, EventType.Change, "gcctaca"),
                new Event(1, EventType.Change, "ctccagg"),
                new Event(1, EventType.Save, ""),
                new Event(1, EventType.Change, "gatagtc"),
                new Event(2, EventType.Change, "agcggaa"),
            };

            var notSavedChanges =
                from e in events where e.UserId == userId select e;
            notSavedChanges = notSavedChanges.TakeWhile(e => e.Type == EventType.Change);

            if (notSavedChanges.Count() > autoSaveThreshold)
            {
                return saver.Save(from e in notSavedChanges select e.Delta);
            }

            return false;
        }
    }
}

StackTrace:

Unhandled exception. System.ArgumentException: I've not found any public method or constructor of class Linq
   at VSharp.TestGenerator.Cover(Type type, Int32 timeout, String outputDirectory, Boolean renderTests, SearchStrategy searchStrategy, Verbosity verbosity)
   at VSharp.TestGenerator.CoverAndRun(Type type, Int32 timeout, String outputDirectory, Boolean renderTests, SearchStrategy searchStrategy, Verbosity verbosity)
   at Program.Main() in /Users/michael/Documents/Work/ConsoleApp1/ConsoleApp1/Program.cs:line 53

Add up-for-grabs issues

Could you please add up-for-grab issues to help first time contributors get started with project?

Invalid error generated for Newtonsoft.Json.DateTimeUtils

Clone and publish https://github.com/JamesNK/Newtonsoft.Json (commit c908de3017ee32278c5330f715cef0e9733ce9db), Release, net6.0
Run V# runner (commit 56d2a46) CLI as follows: --public-methods-of-class DateTimeUtils ...\Newtonsoft.Json.dll
Invalid error is generated:

Starting reproducing error1.vst for method System.TimeSpan GetUtcOffset(System.DateTime)
Test error1.vst failed! The expected exception System.NullReferenceException was not thrown

BitWuzla solver support

Currently V# supports only Z3 SMT solver.

It would be nice to try BitWuzla, which should be more efficient for solving bitvector+array constraints.

To do this, we should

implement the ISolver interface
updating the SolverPool
encoding term conditions to its expressions (similarly to Z3 term builder)
use BitWuzla's API to solve constrains
construct V# model from BitWuzla model. This could be done similarly to Z3 model decoding (possibly, with refactoring-out the common part).

Invalid tests generated for Newtonsoft.Json.KeyValuePairConverter

Clone and publish https://github.com/JamesNK/Newtonsoft.Json (commit c908de3017ee32278c5330f715cef0e9733ce9db), Release, net6.0
Run V# runner (commit 56d2a46) CLI as follows: --public-methods-of-class KeyValuePairConverter ...\Newtonsoft.Json.dll
4 tests are generated and they all fail with incorrect exception thrown or exception not thrown at all:

Test test1.vst throws System.NullReferenceException: Object reference not set to an instance of an object.
   at Newtonsoft.Json.Converters.KeyValuePairConverter.WriteJson(JsonWriter writer, Object value, JsonSerializer serializer) in D:\Newtonsoft.Json\Src\Newtonsoft.Json\Convert
ers\KeyValuePairConverter.cs:line 63 when the expected exception was System.ArgumentOutOfRangeException!
Error (test1.vst): System.NullReferenceException: Object reference not set to an instance of an object.
   at VSharp.TestRunner.TestRunner.ReproduceTest(FileInfo fileInfo, SuiteType suiteType, Boolean checkResult, Boolean fileMode) in D:\VSharp-fork\VSharp.TestRunner\TestRunner
Tool.cs:line 114
Starting reproducing test2.vst for method System.Object ReadJson(Newtonsoft.Json.JsonReader, System.Type, System.Object, Newtonsoft.Json.JsonSerializer)
Test test2.vst throws System.NullReferenceException: Object reference not set to an instance of an object.
   at Newtonsoft.Json.Converters.KeyValuePairConverter.ReadJson(JsonReader reader, Type objectType, Object existingValue, JsonSerializer serializer) in D:\Newtonsoft.Json\Src
\Newtonsoft.Json\Converters\KeyValuePairConverter.cs:line 89 when the expected exception was System.ArgumentOutOfRangeException!
Error (test2.vst): System.NullReferenceException: Object reference not set to an instance of an object.
   at VSharp.TestRunner.TestRunner.ReproduceTest(FileInfo fileInfo, SuiteType suiteType, Boolean checkResult, Boolean fileMode) in D:\VSharp-fork\VSharp.TestRunner\TestRunner
Tool.cs:line 114
Starting reproducing test3.vst for method Boolean CanConvert(System.Type)
Test test3.vst throws System.ArgumentNullException: Value cannot be null. (Parameter 't')
   at Newtonsoft.Json.Utilities.ValidationUtils.ArgumentNotNull(Object value, String parameterName) in D:\Newtonsoft.Json\Src\Newtonsoft.Json\Utilities\ValidationUtils.cs:lin
e 38
   at Newtonsoft.Json.Utilities.ReflectionUtils.IsNullableType(Type t) in D:\Newtonsoft.Json\Src\Newtonsoft.Json\Utilities\ReflectionUtils.cs:line 278
   at Newtonsoft.Json.Converters.KeyValuePairConverter.CanConvert(Type objectType) in D:\Newtonsoft.Json\Src\Newtonsoft.Json\Converters\KeyValuePairConverter.cs:line 147 when
 the expected exception was System.ArgumentOutOfRangeException!
Error (test3.vst): System.ArgumentNullException: Value cannot be null. (Parameter 't')
   at VSharp.TestRunner.TestRunner.ReproduceTest(FileInfo fileInfo, SuiteType suiteType, Boolean checkResult, Boolean fileMode) in D:\VSharp-fork\VSharp.TestRunner\TestRunner
Tool.cs:line 114
Starting reproducing test4.vst for method Void .ctor()
Test test4.vst failed! The expe
```cted exception System.ArgumentOutOfRangeException was not thrown

[followup] Test generation incomplete for switch statement

This is a followup of #318.
The following uses the latest VSharp after 'git pull'.
Do you see the same issue ? Am I running this right ?

Here is input

namespace BranchesAndLoops
{
    public class SwitchStatement
    {
        public SwitchStatement(int x, int y, int z)
        {
            this.X = x;
            this.Y = y;
            this.Z = z;
        }

        int X { get; }
        int Y { get;  }
        int Z {get; }

        public bool SimpleSwitchWithAdditionAndMultiplication()
        {

            switch (checked(X + Y + Z + X*Y*Z + 1))
            {
                case 256: return true;

                case 512: return false;

                case 1024: return false;
            }

            return false;

        }

    }
}

Only one test-case was generated, it does not include the "true" branch in the code i.e "case 256: return true":

  [Test, Category("Generated")]^M
    public void SimpleSwitchWithAdditionAndMultiplicationTest()^M
    {^M
        // arrange
        SwitchStatement thisArg = new Allocator<SwitchStatement>{
            ["X"] = 4096,
            ["Y"] = 4096,
            ["Z"] = 0
        }.Object;^M

        // act
        var result = thisArg.SimpleSwitchWithAdditionAndMultiplication();^M

        // assert
        Assert.AreEqual(false, result);^M
    }^M

The value should be [z = -7, x = -20, y = 2]:

$ cat test.py
from z3 import *

x = Int('x')
y = Int('y')
z = Int('z')
s = Solver()
s.add(x + y + z + x*y*z + 1 == 256)
print(s.check())
print(s.model())

$ python3 test.py
sat
[z = -7, x = -20, y = 2]

dotnet tool

Please, wrap VSharp in dotnet tool.

Transformations: foreach, while/do-while, using

C# spec-related transformation: link

Generation of tables with test results in benchmarks

It would be convenient after each launch of the benchmark to receive a summary table with a list of tests and their statuses: successful or failed. This will help you quickly identify degradations and improvements in vhsrap.

I also suggest adding to the table a list of parameters with which the benchmark was launched. Now in the gui it is quite difficult to understand with what data the launch was made.

Test class needs different parameters ?

Hi @MchKosticyn

This is from the paper you had mentioned earlier in another issue.
Test class:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace ConsoleApp2
{
    class Class1
    {
        public bool Foobar(int i, int j)
        {
            int[] a = { 0 };

            if (a[i] > 1 || a[j] > 1) return false;

            a[i] = 5;

            if (a[j] == 5) return false;

            return true;
        }
    }
}

Here is the generated test class, the last test that asserts the 'return true' should have had parameters as (1, 0) ?

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2024/cymbal/ConsoleApp2
$ ./testgen.bat

D:\Users\samiull\Documents\2024\cymbal\ConsoleApp2>dotnet d:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll  --method Foobar bin\Debug\net6.0\ConsoleApp2.dll -t 90 -o ..\out --render-tests --run-tests -v Trace 
[Info] [5/12/2024 10:17:48 AM] Starting to explore method System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
[Trace] [5/12/2024 10:17:48 AM] Add CFG for System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32).
[Trace] [5/12/2024 10:17:48 AM] SOLVER: trying to solve constraints...
[Trace] [5/12/2024 10:17:48 AM] !(null == this) & (!(i < 1) | !(i >= 0))
[Trace] [5/12/2024 10:17:48 AM] SATISFIABLE
[Info] [5/12/2024 10:17:48 AM] System.IndexOutOfRangeException!
Stack trace:
System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
[Info] [5/12/2024 10:17:48 AM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateIndexOutOfRangeException()
[Trace] [5/12/2024 10:17:48 AM] Exception thrown (HeapRef 3 to System.IndexOutOfRangeException), StackTrace:
[method = System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
offset = A]
[Trace] [5/12/2024 10:17:48 AM] SOLVER: trying to solve constraints...
[Trace] [5/12/2024 10:17:48 AM] !(null == this) & 2[i] > 1 & i < 1 & i >= 0
[Trace] [5/12/2024 10:17:49 AM] UNSATISFIABLE
[Trace] [5/12/2024 10:17:49 AM] SOLVER: trying to solve constraints...
[Trace] [5/12/2024 10:17:49 AM] !(null == this) & (!(j < 1) | !(j >= 0)) & i < 1 & i >= 0
[Trace] [5/12/2024 10:17:49 AM] SATISFIABLE
[Info] [5/12/2024 10:17:49 AM] System.IndexOutOfRangeException!
Stack trace:
System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
[Info] [5/12/2024 10:17:49 AM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateIndexOutOfRangeException()
[Trace] [5/12/2024 10:17:49 AM] Exception thrown (HeapRef 3 to System.IndexOutOfRangeException), StackTrace:
[method = System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
offset = 10]
[Trace] [5/12/2024 10:17:49 AM] SOLVER: trying to solve constraints...
[Trace] [5/12/2024 10:17:49 AM] !(null == this) & 2[j] > 1 & i < 1 & i >= 0 & j < 1 & j >= 0
[Trace] [5/12/2024 10:17:49 AM] UNSATISFIABLE
[Trace] [5/12/2024 10:17:49 AM] SOLVER: trying to solve constraints...
[Trace] [5/12/2024 10:17:49 AM] !(2[j] == 5) & !(null == this) & i < 1 & i >= 0 & j < 1 & j >= 0
[Trace] [5/12/2024 10:17:49 AM] UNSATISFIABLE
[Info] [5/12/2024 10:17:49 AM] Result of method System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32) is False
The template "NUnit 3 Test Project" was created successfully.

Processing post-creation actions...
Restoring D:\Users\samiull\Documents\2024\cymbal\out\ConsoleApp2.Tests\ConsoleApp2.Tests.csproj:
  Determining projects to restore...
  Restored D:\Users\samiull\Documents\2024\cymbal\out\ConsoleApp2.Tests\ConsoleApp2.Tests.csproj (in 802 ms).
Restore succeeded.


Starting reproducing error1.vst for method System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
Test error1.vst throws the expected exception System.IndexOutOfRangeException!
error1.vst passed!
Starting reproducing error2.vst for method System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
Test error2.vst throws the expected exception System.IndexOutOfRangeException!
error2.vst passed!
Starting reproducing test1.vst for method System.Boolean ConsoleApp2.Class1.Foobar(this, System.Int32, System.Int32)
test1.vst passed!
Total time: 00:00:00.821.
Approximate coverage: 83.33333333333334
Test results written to D:\Users\samiull\Documents\2024\cymbal\out\VSharp.tests.0
Tests generated: 1
Errors generated: 2

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2024/cymbal/ConsoleApp2
$ cat ../out/
ConsoleApp2.Tests/ VSharp.tests.0/    

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2024/cymbal/ConsoleApp2
$ cat ../out/ConsoleApp2.Tests/
Class1Tests.cs            Extensions/               
ConsoleApp2.Tests.csproj  obj/                      

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2024/cymbal/ConsoleApp2
$ cat ../out/ConsoleApp2.Tests/Class1Tests.cs 
using NUnit.Framework;
using VSharp.TestExtensions;

namespace ConsoleApp2.Tests;

[TestFixture]
class Class1Tests
{
    [Test, Category("Generated")]
    public void FoobarError()
    {
        // arrange
        object thisArg = new Allocator<object>("ConsoleApp2.Class1, ConsoleApp2, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null").Object;

        // act
        thisArg.Call("Foobar", 0, -2147483648);
    }

    [Test, Category("Generated")]
    public void FoobarError1()
    {
        // arrange
        object thisArg = new Allocator<object>("ConsoleApp2.Class1, ConsoleApp2, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null").Object;

        // act
        thisArg.Call("Foobar", -2147483648, 0);
    }

    [Test, Category("Generated")]
    public void FoobarTest()
    {
        // arrange
        object thisArg = new Allocator<object>("ConsoleApp2.Class1, ConsoleApp2, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null").Object;

        // act
        var result = thisArg.Call("Foobar", 0, 0);

        // assert
        Assert.AreEqual(false, result);
    }
}

ShortestDistanceWeighter tries to get CFG for external method that leads to error

Execution of this test leads to the following error:

Getting CFG of method System.Int32 System.String.get_Length(this) without body (extern or abstract)
   at VSharp.Test.TestSvmAttribute.TestSvmCommand.<>c.<Explore>b__12_1(FSharpOption`1 _, Exception e) in /home/gsv/Projects/VSharp/VSharp.Test/IntegrationTests.cs:line 257
   at <StartupCode$VSharp-SILI>[email protected](FSharpOption`1 method, Exception e)
   at VSharp.Interpreter.IL.SILI.Interpret(IEnumerable`1 isolated, IEnumerable`1 entryPoints, Action`1 onFinished, Action`1 onException, Action`1 onIIE, Action`2 onInternalFail) in /home/gsv/Projects/VSharp/VSharp.SILI/SILI.fs:line 425
   at VSharp.Test.TestSvmAttribute.TestSvmCommand.Explore(TestExecutionContext context) in /home/gsv/Projects/VSharp/VSharp.Test/IntegrationTests.cs:line 257

Debugging shows that it is caused by attempt to get CFG for external method.

Wrong namespace indents

Description

Test namespace indents are generated wrongly.

Environment

Docker, Ubuntu 20.04, .NET 6.0, Mono 6
VSharp console runner with special option --single-file

Steps to reproduce

Run command such as (for the source code below):
dotnet /usr/src/vsharp_runner/VSharp.Runner.dll --all-public-methods /usr/src/project/bin/Debug/net6.0/project.dll --render-tests --single-file
See generated tests contain wrong namespace indents.

Open https://www.utbot.org/demo
Choose C# language
Paste the source code from below
See generated tests contain wrong namespace indents.

Source code

namespace Algorithms;

public static class Searches {
	public static int BinarySearch(int value, int[] a)
	{
		var l = a.GetLowerBound(0);
		var r = a.GetLength(0);
		while (l < r)
		{
			var mid = (l + r) / 2;
			int element = a[mid];
			if (element == value)
				return mid;
			if (element < value)
				r = mid - 1;
			l = mid + 1;
		}
		return -1;
	}
}

Generated test

using System;
using System.Collections.Generic;
using System.Diagnostics;
using System.Linq;
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;
using System.Runtime.Serialization;
using NUnit.Framework;
using Algorithms;

namespace VSharp.TestExtensions
{

internal static class CartesianProductExtension
{
    internal static IEnumerable<IEnumerable<T>> CartesianProduct<T>(this IEnumerable<IEnumerable<T>> sequences)
    {
        IEnumerable<IEnumerable<T>> emptyProduct =
            new[] { Enumerable.Empty<T>() };
        return sequences.Aggregate(
            emptyProduct,
            (accumulator, sequence) =>
                from accseq in accumulator
                from item in sequence
                select accseq.Concat(new[] {item}));
    }
}

public static class Allocator
{
    private static void FillFast<TElem>(Array? arr, TElem value)
    {
        if (arr != null)
        {
            ref var bytePtr = ref MemoryMarshal.GetArrayDataReference(arr);
            ref var ptr = ref Unsafe.As<byte, TElem>(ref bytePtr);
            var span = MemoryMarshal.CreateSpan(ref ptr, arr.Length);
            span.Fill(value);
        }
    }

    /// Fills zero-initialized array with value
    public static void Fill(Array? arr, object? value)
    {
        if (value == null)
        {
            // Do nothing because arr is already filled with nulls
            return;
        }

        var t = value.GetType();
        if (arr != null && (!t.IsValueType || Nullable.GetUnderlyingType(t) != null ||
                            value != FormatterServices.GetUninitializedObject(t)))
        {
            var elementType = arr.GetType().GetElementType();
            switch (value)
            {
                case int i when elementType == typeof(int):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(byte):
                    FillFast(arr, i);
                    break;
                case char i when elementType == typeof(char):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(uint):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(Int64):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(UInt64):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(double):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(float):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(Int16):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(UInt16):
                    FillFast(arr, i);
                    break;
                case byte i when elementType == typeof(sbyte):
                    FillFast(arr, i);
                    break;
                default:
                    var rank = arr.Rank;
                    var indices =
                        Enumerable.Range(0, rank)
                            .Select(i => Enumerable.Range(arr.GetLowerBound(i), arr.GetLength(i)))
                            .CartesianProduct();
                    foreach (var i in indices)
                    {
                        arr.SetValue(value, i.ToArray());
                    }

                    break;
            }
        }
    }
}

public class Allocator<T>
{
    private readonly Type _objectType = typeof(T);
    private readonly object _toAllocate;

    public Allocator()
    {
        _toAllocate = FormatterServices.GetUninitializedObject(_objectType);
    }

    public Allocator(string typeName)
    {
        Type? notPublicType = Type.GetType(typeName);
        _objectType = notPublicType ?? _objectType;
        _toAllocate = FormatterServices.GetUninitializedObject(_objectType);
    }

    public Allocator(object? defaultValue, params int[] lengths)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = Array.CreateInstance(_objectType.GetElementType()!, lengths);
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public Allocator(object? defaultValue, int[] lengths, int[] lowerBounds)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = Array.CreateInstance(_objectType.GetElementType()!, lengths, lowerBounds);
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public Allocator(object allocated)
    {
        _toAllocate = allocated;
    }

    public Allocator(object allocated, object defaultValue)
    {
        Debug.Assert(_objectType.IsArray);
        _toAllocate = allocated;
        Allocator.Fill(_toAllocate as Array, defaultValue);
    }

    public object this[string fieldName]
    {
        set
        {
            var allBindingFlags = BindingFlags.Instance | BindingFlags.NonPublic | BindingFlags.Public;
            var field = _objectType.GetField(fieldName, allBindingFlags);
            var property = _objectType.GetField($"<{fieldName}>k__BackingField", allBindingFlags);
            Debug.Assert(field != null || property != null);
            field ??= property;
            if (field != null)
                field.SetValue(_toAllocate, value);
        }
    }

    public object this[params int[] index]
    {
        set
        {
            Debug.Assert(_objectType.IsArray);
            var array = _toAllocate as Array;
            array?.SetValue(value, index);
        }
    }

    public T Object => (T)_toAllocate;
}

public static class ObjectsComparer
{
    private static bool StructurallyEqual(object? expected, object? got)
    {
        Debug.Assert(expected != null && got != null && expected.GetType() == got.GetType());
        var flags = BindingFlags.Public | BindingFlags.NonPublic | BindingFlags.Instance;
        var fields = expected.GetType().GetFields(flags);
        foreach (var field in fields)
        {
            if (!typeof(MulticastDelegate).IsAssignableFrom(field.FieldType) &&
                !field.Name.Contains("threadid", StringComparison.OrdinalIgnoreCase) &&
                !CompareObjects(field.GetValue(expected), field.GetValue(got)))
            {
                return false;
            }
        }

        return true;
    }

    private static bool ContentwiseEqual(global::System.Array? expected, global::System.Array? got)
    {
        Debug.Assert(expected != null && got != null && expected.GetType() == got.GetType());
        if (expected.Rank != got.Rank)
            return false;
        for (int i = 0; i < expected.Rank; ++i)
            if (expected.GetLength(i) != got.GetLength(i) || expected.GetLowerBound(i) != got.GetLowerBound(i))
                return false;
        var enum1 = expected.GetEnumerator();
        var enum2 = got.GetEnumerator();
        while (enum1.MoveNext() && enum2.MoveNext())
        {
            if (!CompareObjects(enum1.Current, enum2.Current))
                return false;
        }
        return true;
    }

    public static bool CompareObjects(object? expected, object? got)
    {
        if (expected == null)
            return got == null;
        if (got == null)
            return false;
        var type = expected.GetType();
        if (type != got.GetType())
            return false;

        if (Object.ReferenceEquals(expected, got))
            return true;

        if (type == typeof(Pointer) || type.IsPrimitive || expected is string || type.IsEnum)
        {
            // TODO: compare double with epsilon?
            return got.Equals(expected);
        }

        if (expected is global::System.Array array)
            return ContentwiseEqual(array, got as global::System.Array);
        return StructurallyEqual(expected, got);
    }
}
}

namespace project.Tests
{
[TestFixture]
class SearchesTests
{
    [Test, Category("Generated")]
    public void BinarySearchError()
    {
        // act
        Searches.BinarySearch(0, null!);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest()
    {
        // arrange
        int[] a = new int[1];

        // act
        var result = Searches.BinarySearch(0, a);

        // assert
        Assert.AreEqual(0, result);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest1()
    {
        // arrange
        int[] a = new int[0];

        // act
        var result = Searches.BinarySearch(0, a);

        // assert
        Assert.AreEqual(-1, result);
    }

    [Test, Category("Generated")]
    public void BinarySearchTest2()
    {
        // arrange
        int[] a = new int[1];

        // act
        var result = Searches.BinarySearch(1, a);

        // assert
        Assert.AreEqual(-1, result);
    }
}}

NullReferenceException expected on correct DateTime constructor

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.

Single Assembly resolver

Now in runner and test runner we have different code which resolves assemblies:

https://github.com/VSharp-team/VSharp/blob/master/VSharp.Utils/AssemblyManager.fs for runner (and test renderer)

and

VSharp/VSharp.TestRunner/TestRunnerTool.cs

Lines 17 to 34 in 2a3e2d9

 private static Assembly TryLoadAssemblyFrom(object sender, ResolveEventArgs args) 

 { 

 var existingInstance = AppDomain.CurrentDomain.GetAssemblies().FirstOrDefault(assembly => assembly.FullName == args.Name); 

 if (existingInstance != null) 

 { 

 return existingInstance; 

 } 

 foreach (string path in _extraAssemblyLoadDirs) 

 { 

 string assemblyPath = Path.Combine(path, new AssemblyName(args.Name).Name + ".dll"); 

 if (!File.Exists(assemblyPath)) 

 return null; 

 Assembly assembly = Assembly.LoadFrom(assemblyPath); 

 return assembly; 

 } 

 return null; 

 }

for test runner

In particular, this code loads assemblies into different contexts, which means that something can work fine in runner, but don't work in test runner, or vice versa.

So, we need to use a single assembly manager for the whole V#. This manager should load assemblies into separate context (like https://github.com/VSharp-team/VSharp/blob/master/VSharp.Utils/AssemblyManager.fs)

Integer overflow in generated test

The following generated test has an integer overflow due to the input values used.

Input class:

    public class SomeClass
    {
        public SomeClass()
        {
        }

        public int Foo(int v)
        {
            return 2 * v;
        }

        public void TestMe(int x, int y)
        {
            int z = Foo(y);
            if (z == x)
            {
                if (x > y + 10)
                {
                    throw new Exception("Caught error");
                }
            }
        }
    }

Integer overflow in int Foo(int v)

    [Test, Category("Generated")]
    public void TestMeTest()
    {
        // arrange
        SomeClass thisArg = new Allocator<SomeClass>().Object;

        // assert
        Assert.Throws<Exception>(() => thisArg.TestMe(2147483630, -1073741833));
    }

Test generation incomplete for switch statement

Hi,

The test code generated does not exercise the path with the "true" return statement - "case 256: return true;"

Here is the generated code:

using NUnit.Framework;
using VSharp.TestExtensions;

namespace BranchesAndLoops.Tests;

[TestFixture]
class SwitchStatementTests
{
    [Test, Category("Generated")]
    public void SimpleSwitchWithAdditionAndMultiplicationTest()
    {
        // arrange
        SwitchStatement thisArg = new Allocator<SwitchStatement>{
            ["X"] = 8,
            ["Y"] = 0
        }.Object;

        // act
        var result = thisArg.SimpleSwitchWithAdditionAndMultiplication();

        // assert
        Assert.AreEqual(false, result);
    }
}

This is the input:

namespace BranchesAndLoops
{
    public class SwitchStatement
    {
        public SwitchStatement(int x, int y)
        {
            this.X = x;
            this.Y = y;
        }

        int X { get; }
        int Y { get;  }

        public bool SimpleSwitchWithAdditionAndMultiplication()
        {
            if (X <= 0 || Y <= 0)
            {
                return false;
            }

            switch (checked(X + Y + X*Y + 1))
            {
                case 256: return true;

                case 512: return false;

                case 1024: return false;
            }

            return false;

        }

    }
}

Script to execute:

dotnet ..\..\..\Cymbal-TestGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll --all-public-methods  bin\Debug\net6.0\BranchesAndLoops.dll -t 30 -o ..\out --render-tests --run-tests

V# throws `creating object from term: unexpected term`

Steps to reproduce:

Run this test
Get creating object from term: unexpected term exception

Generated tests classes names can be long for generics

When declaringType is not passed to Render, test class name is composed from the type name with generic parameters substituted, so theoretically it can be too long and hard to read

Test case for ReginTree performance tuning

Create test using class from attached file.
Change values of MAXS and MAXC (lines 8 and 13). While values increase, performance slow down dramatically.
AhoCorasik.txt

C# test generator

For now, V# supports only XML-based unit test representation. Besides unreadability issues, we need the special tool for running these tests. That is, given a collection of UnitTest objects, currently we print them using XmlSerializer.

The usability of V# can be massively improved, if we had C# test printer. It would be nice to have various printers sharing the common printer core: MsTest, NUnit, XUnit, etc.

Every unit test should roughly look like

[Test]
public void Test1() {
    // Allocate objects graph, including `thisObject` (if F is not static) and reference type arguments.
    try {
        TResult result = thisObject.F<T1, ..., Tn>(arg_1, ..., arg_m);
        Assert.<check result match>(...);
    } 
    catch (ExpectedException1 e) {
        // success
    }
    ....
    catch (ExpectedExceptionN e) {
        // success
    }
}

Allocating complex types

For now, classes could be allocated by using System.Runtime.Serialization.FormatterServices.GetUninitializedObject and then initializing their contents by reflection. In future, we consider to allocate objects using their public API. However, this requires additional research.

Strange interpretation of coverage incompleteness : Incomplete coverage! Expected 50, but got 67

V# version to reproduce
Test to reproduce
Steps
- Run the test
- Get exception "Incomplete coverage! Expected 50, but got 67"
Expected: I think, that it is not an exception when actual coverage higher that expected.

	private static Assembly TryLoadAssemblyFrom(object sender, ResolveEventArgs args)
	{
	var existingInstance = AppDomain.CurrentDomain.GetAssemblies().FirstOrDefault(assembly => assembly.FullName == args.Name);
	if (existingInstance != null)
	{
	return existingInstance;
	}
	foreach (string path in _extraAssemblyLoadDirs)
	{
	string assemblyPath = Path.Combine(path, new AssemblyName(args.Name).Name + ".dll");
	if (!File.Exists(assemblyPath))
	return null;
	Assembly assembly = Assembly.LoadFrom(assemblyPath);
	return assembly;
	}

	return null;
	}

vsharp-team / vsharp Goto Github PK

vsharp's People

Contributors

Stargazers

Watchers

Forkers

vsharp's Issues

Description

Environment

Steps to reproduce

Source code

Generated tests

Description

Expected

To reproduce

Description

To reproduce

Description

Environment

Steps to reproduce

Source code

Generated test

Recommend Projects

Recommend Topics

Recommend Org