Generated test seems incomplete for this input

[smhmhmd]

Generated test seems incomplete for this input

[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.

[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
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 ?

[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.
    }
}