Generated test seems incomplete for this input

[smhmhmd]

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;
        }

    }
}

[MchKosticyn]

Hi @smhmhmd

Actually I don't see 'return true' branch either. That happens, because every loop bound is symbolic, so symbolic execution creates new symbolic state on each loop iteration. This leads to exponential growth of symbolic states. This is main problem of symbolic execution.
Will try to fix that.

[smhmhmd]

Hi @MchKosticyn
Where can I add prints to print all the states ? Is it possible to use a heuristic to protect against exponential growth of symbolic states ?

[MchKosticyn]

Hi @smhmhmd

If you want to print all states, which are complete exploration, you can do it inside "Explorer.fs:reportState" function. But there are so many symbolic states...
About heuristics, searching strategy is exactly it. I already tried every strategy and cannot reach 'return true' branch.
Will try to modify strategies later.

[smhmhmd]

Hi @MchKosticyn
The input code above is adapted from https://www.geeksforgeeks.org/8-queen-problem/, need to check if the input code is satisfiable.

[MchKosticyn]

Hi @smhmhmd

Branch 'return true' is reachable, here is example:

public class Program
    {
        public static void Main()
        {
            var board = new int[8][]
            {
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 },
                new int[8] { 0, 0, 0, 0, 0, 0, 0, 1 }
            };
            var eightQueens = new EightQueens(board);
            Console.WriteLine(eightQueens.CheckSolution());
        }
    }

But there is a bug inside constructor: check should be board.Length != N, because 'board' is not multidimensional array, it is array of arrays.

[smhmhmd]

Hi @MchKosticyn

Branch 'return true' is reachable.

Thanks for running it. So it is satisfiable although it is not an 8-queens solution.
The generated test would be the solution you added above.

But there is a bug inside constructor: check should be board.Length != N, because 'board' is not multidimensional array, it is array of arrays.

I changed 'N*N' to 'N' and rebuilt, but the 'true' branch issue persists.

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

Generated test:

 cat ../out/BranchesAndLoops.Tests/EightQueensTests.cs 
using NUnit.Framework;
using VSharp.TestExtensions;

namespace BranchesAndLoops.Tests;

[TestFixture]
class EightQueensTests
{
    [Test, Category("Generated")]
    public void CheckSolutionError()
    {
        // arrange
        int[][] _board = new int[15][];
        int[] _board_Elem0 = new int[15];
        Allocator.Fill(_board_Elem0, 1);
        int[] _board_Elem1 = new int[15];
        Allocator.Fill(_board_Elem1, 1);
        int[] _board_Elem3 = new int[15];
        Allocator.Fill(_board_Elem3, 1);
        int[] _board_Elem4 = new int[15];
        Allocator.Fill(_board_Elem4, 1);
        int[] _board_Elem5 = new int[15];
        Allocator.Fill(_board_Elem5, 1);
        int[] _board_Elem6 = new int[39];
        Allocator.Fill(_board_Elem6, 1);
        int[] _board_Elem7 = new int[7];
        Allocator.Fill(_board_Elem7, 1);
        _board[0] = _board_Elem0;
        _board[1] = _board_Elem1;
        _board[2] = _board_Elem1;
        _board[3] = _board_Elem3;
        _board[4] = _board_Elem4;
        _board[5] = _board_Elem5;
        _board[6] = _board_Elem6;
        _board[7] = _board_Elem7;
        EightQueens thisArg = new Allocator<EightQueens>{
            ["_board"] = _board
        }.Object;

        // act
        thisArg.CheckSolution();
    }

    [Test, Category("Generated")]
    public void CheckSolutionError1()
    {
        // arrange
        int[][] _board = new int[15][];
        int[] _board_Elem0 = new int[15];
        Allocator.Fill(_board_Elem0, 1);
        int[] _board_Elem1 = new int[15];
        Allocator.Fill(_board_Elem1, 1);
        int[] _board_Elem3 = new int[15];
        Allocator.Fill(_board_Elem3, 1);
        int[] _board_Elem4 = new int[15];
        Allocator.Fill(_board_Elem4, 1);
        int[] _board_Elem5 = new int[15];
        Allocator.Fill(_board_Elem5, 1);
        int[] _board_Elem6 = new int[39];
        Allocator.Fill(_board_Elem6, 1);
        _board[0] = _board_Elem0;
        _board[1] = _board_Elem1;
        _board[2] = _board_Elem1;
        _board[3] = _board_Elem3;
        _board[4] = _board_Elem4;
        _board[5] = _board_Elem5;
        _board[6] = _board_Elem6;
        EightQueens thisArg = new Allocator<EightQueens>{
            ["_board"] = _board
        }.Object;

        // act
        thisArg.CheckSolution();
    }

    [Test, Category("Generated")]
    public void CheckSolutionError2()
    {
        // arrange
        int[][] _board = new int[7][];
        int[] _board_Elem0 = new int[15];
        Allocator.Fill(_board_Elem0, 1);
        int[] _board_Elem1 = new int[15];
        Allocator.Fill(_board_Elem1, 1);
        int[] _board_Elem3 = new int[15];
        Allocator.Fill(_board_Elem3, 1);
        int[] _board_Elem4 = new int[15];
        Allocator.Fill(_board_Elem4, 1);
        int[] _board_Elem5 = new int[15];
        Allocator.Fill(_board_Elem5, 1);
        _board[0] = _board_Elem0;
        _board[1] = _board_Elem1;
        _board[2] = _board_Elem1;
        _board[3] = _board_Elem3;
        _board[4] = _board_Elem4;
        _board[5] = _board_Elem5;
        _board[6] = _board_Elem5;
        EightQueens thisArg = new Allocator<EightQueens>{
            ["_board"] = _board
        }.Object;

        // act
        thisArg.CheckSolution();
    }

    [Test, Category("Generated")]
    public void CheckSolutionTest()
    {
        // arrange
        int[][] _board = new int[0][];
        EightQueens thisArg = new Allocator<EightQueens>{
            ["_board"] = _board
        }.Object;

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

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

    [Test, Category("Generated")]
    public void CheckSolutionTest1()
    {
        // arrange
        int[][] _board = new int[15][];
        int[] _board_Elem0 = new int[15];
        Allocator.Fill(_board_Elem0, 1);
        int[] _board_Elem1 = new int[15];
        Allocator.Fill(_board_Elem1, 1);
        int[] _board_Elem3 = new int[15];
        Allocator.Fill(_board_Elem3, 1);
        int[] _board_Elem4 = new int[15];
        Allocator.Fill(_board_Elem4, 1);
        int[] _board_Elem5 = new int[15];
        Allocator.Fill(_board_Elem5, 1);
        int[] _board_Elem6 = new int[39];
        Allocator.Fill(_board_Elem6, 1);
        _board[0] = _board_Elem0;
        _board[1] = _board_Elem1;
        _board[2] = _board_Elem1;
        _board[3] = _board_Elem3;
        _board[4] = _board_Elem4;
        _board[5] = _board_Elem5;
        _board[6] = _board_Elem6;
        _board[7] = _board_Elem6;
        EightQueens thisArg = new Allocator<EightQueens>{
            ["_board"] = _board
        }.Object;

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

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

[smhmhmd]

Hi @MchKosticyn

In the sample code below, I have both Mono.cecil and System.Reflection, Mono.cecil works and System.Reflection has this error

Unhandled exception. System.Reflection.ReflectionTypeLoadException: Unable to load one or more of the requested types.
Could not load file or assembly 'System.Security.Permissions, Version=0.0.0.0, Culture=neutral, PublicKeyToken=cc7b13ffcd2ddd51'. The system cannot find the file specified.

using System.Collections.Immutable;
using System.IO;
using System.Reflection.Metadata;
using System.Reflection.Metadata.Ecma335;
using System.Runtime.CompilerServices;
using Microsoft.Win32.SafeHandles;
using System.Reflection.PortableExecutable;
using System.Xml;
using System.Diagnostics;
using System.Reflection;
using System.Reflection.Emit;
using System.Xml.Linq;
using Mono.Cecil;

class Program
{
    static void Main(string[] args)
    {

        // Use mono.cecil
        var inputAssembly =
            @"D:\Users\samiull\Documents\2024\nopCommerce-release-3.80\src\Libraries\Nop.Core\bin\Debug\Nop.Core.dll";
        var path = Path.GetDirectoryName(inputAssembly);

        var assemblyResolver = new DefaultAssemblyResolver();
        var assemblyLocation = Path.GetDirectoryName(inputAssembly);
        assemblyResolver.AddSearchDirectory(assemblyLocation);

        var readerParameters = new ReaderParameters { AssemblyResolver = assemblyResolver };

        var assemblyDefinition = Mono.Cecil.AssemblyDefinition.ReadAssembly(
            @"D:\Users\samiull\Documents\2024\nopCommerce-release-3.80\src\Libraries\Nop.Core\bin\Debug\Nop.Core.dll",
            readerParameters);

        var module = assemblyDefinition.MainModule;
        foreach (var typeDefinition in module.Types)
        {
            Console.WriteLine("Type = " + typeDefinition.ToString());
        }

        var methods = assemblyDefinition.MainModule
            .GetTypes()
            .SelectMany(t => t.Methods
                .Where(m => m.HasBody)
                .Select(m => m));

        foreach (var m in methods)
        {
            var count = m.Body.Instructions.Count;
            Console.WriteLine("Method " + m.Name + " has " + count + " instructions");
        }

        // Use system.reflection
        Assembly SampleAssembly;
        SampleAssembly = Assembly.LoadFrom("D:\\Users\\samiull\\Documents\\2024\\nopCommerce-release-3.80\\src\\Libraries\\Nop.Core\\bin\\Debug\\Nop.Core.dll");
        // Obtain a reference to a method known to exist in assembly.
        MethodInfo[] Method = SampleAssembly.GetTypes()[0].GetMethods();
        // Obtain a reference to the parameters collection of the MethodInfo instance.
    }
}