Skip to content

Generated test seems incomplete for this input #321

@smhmhmd

Description

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

    }
}


Activity

MchKosticyn

MchKosticyn commented on May 4, 2024

@MchKosticyn
Member

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

smhmhmd commented on May 10, 2024

@smhmhmd
Author

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

MchKosticyn commented on May 15, 2024

@MchKosticyn
Member

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

smhmhmd commented on May 15, 2024

@smhmhmd
Author

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

MchKosticyn commented on May 15, 2024

@MchKosticyn
Member

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

smhmhmd commented on May 15, 2024

@smhmhmd
Author

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

smhmhmd commented on May 16, 2024

@smhmhmd
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @smhmhmd@MchKosticyn

        Issue actions

          Generated test seems incomplete for this input · Issue #321 · VSharp-team/VSharp