search

VSharp-team / VSharp

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

Test class needs different parameters ? #322

Closed smhmhmd closed 5 months ago

smhmhmd commented 5 months ago

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);
    }
}
MchKosticyn commented 5 months ago

Hi @smhmhmd Branch 'return true' is unreachable, isn't it? Variables 'i' and 'j' should be '0' for method 'Foobar' not to throw exception (array 'a' contains only one element). So, condition in first 'if' statement evaluates to 'false', but second condition evaluates to 'true', because 'i' and 'j' are equal to '0'.

smhmhmd commented 5 months ago

Hi @MchKosticyn

Branch 'return true' is unreachable, isn't it? You are right.

For this input code:

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

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

     a[i] = 5;

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

     return true;
 }
The test is generated correctly

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

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

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