Skip to content

Path condition #91

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Mar 20, 2025
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 14 additions & 6 deletions .github/workflows/build_vsharp.yml
Original file line number Diff line number Diff line change
@@ -1,31 +1,39 @@
name: 'Build VSharp'

on:
workflow_call
[workflow_call, pull_request, push]

jobs:
build:
runs-on: ubuntu-22.04
steps:
- uses: actions/setup-dotnet@v4
with:
dotnet-version: '7.0.x'

- name: Checkout VSharp
uses: actions/checkout@v3
uses: actions/checkout@v4
with:
submodules: false
- uses: actions/cache@v3

- uses: actions/cache@v4
id: nuget-cache
with:
path: ~/.nuget/packages
key: ${{ runner.os }}-nuget-${{ hashFiles('**/*.csproj', '**/*.fsproj') }}
restore-keys: |
${{ runner.os }}-nuget-
- name: Build VSharp
run:
dotnet build -c DebugTailRec
- uses: actions/upload-artifact@v3
dotnet build -c Release

- uses: actions/upload-artifact@v4
with:
name: runner
path: ./VSharp.Runner/bin/DebugTailRec/net7.0
- uses: actions/upload-artifact@v3

- uses: actions/upload-artifact@v4
with:
name: test_runner
path: ./VSharp.TestRunner/bin/DebugTailRec/net7.0
297 changes: 145 additions & 152 deletions VSharp.Explorer/AISearcher.fs

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion VSharp.IL/CFG.fs
Original file line number Diff line number Diff line change
@@ -8,6 +8,7 @@ open System.Reflection
open System.Collections.Generic
open Microsoft.FSharp.Collections
open VSharp
open VSharp.Core

type ICallGraphNode =
inherit IGraphNode<ICallGraphNode>
@@ -519,7 +520,7 @@ and IGraphTrackableState =
abstract member CodeLocation: codeLocation
abstract member CallStack: list<Method>
abstract member Id: uint<stateId>
abstract member PathConditionSize: uint
abstract member PathCondition: pathCondition
abstract member VisitedNotCoveredVerticesInZone: uint with get
abstract member VisitedNotCoveredVerticesOutOfZone: uint with get
abstract member VisitedAgainVertices: uint with get
630 changes: 434 additions & 196 deletions VSharp.IL/Serializer.fs

Large diffs are not rendered by default.

166 changes: 88 additions & 78 deletions VSharp.ML.GameServer.Runner/Main.fs
Original file line number Diff line number Diff line change
@@ -23,22 +23,22 @@ type ExplorationResult =
val TestsCount: uint<test>
val ErrorsCount: uint<error>
val StepsCount: uint<step>

new(actualCoverage, testsCount, errorsCount, stepsCount) =
{
ActualCoverage = actualCoverage
TestsCount = testsCount
ErrorsCount = errorsCount
StepsCount = stepsCount
}
{ ActualCoverage = actualCoverage
TestsCount = testsCount
ErrorsCount = errorsCount
StepsCount = stepsCount }

type Mode =
| Server = 0
| Generator = 1

type CliArguments =
| [<Unique>] Port of int
| [<Unique>] DatasetBasePath of string
| [<Unique>] DatasetDescription of string
| [<Unique ; Mandatory>] Mode of Mode
| [<Unique; Mandatory>] Mode of Mode
| [<Unique>] OutFolder of string
| [<Unique>] StepsToSerialize of uint
| [<Unique>] UseGPU
@@ -62,21 +62,21 @@ type CliArguments =
let mutable inTrainMode = true

let explore (gameMap: GameMap) options =
let assembly =
RunnerProgram.TryLoadAssembly <| FileInfo gameMap.AssemblyFullName
let method =
RunnerProgram.ResolveMethod (assembly, gameMap.NameOfObjectToCover)
let statistics =
TestGenerator.Cover (method, options)
let assembly = RunnerProgram.TryLoadAssembly <| FileInfo gameMap.AssemblyFullName
let method = RunnerProgram.ResolveMethod(assembly, gameMap.NameOfObjectToCover)
let statistics = TestGenerator.Cover(method, options)

let actualCoverage =
try
let testsDir = statistics.OutputDir
let _expectedCoverage = 100
let exploredMethodInfo =
AssemblyManager.NormalizeMethod method
let exploredMethodInfo = AssemblyManager.NormalizeMethod method

let status, actualCoverage, message =
VSharp.Test.TestResultChecker.Check (testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage)
VSharp.Test.TestResultChecker.Check(testsDir, exploredMethodInfo :?> MethodInfo, _expectedCoverage)

printfn $"Actual coverage for {gameMap.MapName}: {actualCoverage}"

if actualCoverage < 0 then
0u<percent>
else
@@ -85,7 +85,7 @@ let explore (gameMap: GameMap) options =
printfn $"Coverage checking problem:{e.Message} \n {e.StackTrace}"
0u<percent>

ExplorationResult (
ExplorationResult(
actualCoverage,
statistics.TestsCount * 1u<test>,
statistics.ErrorsCount * 1u<error>,
@@ -94,11 +94,12 @@ let explore (gameMap: GameMap) options =


let loadGameMaps (datasetDescriptionFilePath: string) =
let jsonString =
File.ReadAllText datasetDescriptionFilePath
let maps = ResizeArray<GameMap> ()
let jsonString = File.ReadAllText datasetDescriptionFilePath
let maps = ResizeArray<GameMap>()

for map in System.Text.Json.JsonSerializer.Deserialize<GameMap[]> jsonString do
maps.Add map

maps

let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
@@ -111,6 +112,7 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
serializeOutgoingMessage message
|> System.Text.Encoding.UTF8.GetBytes
|> ByteSegment

webSocket.send Text byteResponse true

let oracle =
@@ -123,87 +125,99 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
| Feedback.ServerError s -> OutgoingMessage.ServerError s
| Feedback.MoveReward reward -> OutgoingMessage.MoveReward reward
| Feedback.IncorrectPredictedStateId i -> OutgoingMessage.IncorrectPredictedStateId i

do! sendResponse message
}

match Async.RunSynchronously res with
| Choice1Of2 () -> ()
| Choice1Of2() -> ()
| Choice2Of2 error -> failwithf $"Error: %A{error}"

let predict =
let mutable cnt = 0u

fun (gameState: GameState) ->
let toDot drawHistory =
let file = Path.Join ("dot", $"{cnt}.dot")
let file = Path.Join("dot", $"{cnt}.dot")
gameState.ToDot file drawHistory
cnt <- cnt + 1u
//toDot false
let res =
socket {
do! sendResponse (ReadyForNextStep gameState)
let! msg = webSocket.read ()

let res =
match msg with
| (Text, data, true) ->
let msg = deserializeInputMessage data

match msg with
| Step stepParams -> (stepParams.StateId)
| _ -> failwithf $"Unexpected message: %A{msg}"
| _ -> failwithf $"Unexpected message: %A{msg}"

return res
}

match Async.RunSynchronously res with
| Choice1Of2 i -> i
| Choice2Of2 error -> failwithf $"Error: %A{error}"

Oracle (predict, feedback)
Oracle(predict, feedback)

while loop do
let! msg = webSocket.read ()

match msg with
| (Text, data, true) ->
let message = deserializeInputMessage data

match message with
| ServerStop -> loop <- false
| Start gameMap ->
printfn $"Start map {gameMap.MapName}, port {port}"
let stepsToStart = gameMap.StepsToStart
let stepsToPlay = gameMap.StepsToPlay

let aiTrainingOptions =
{
stepsToSwitchToAI = stepsToStart
stepsToPlay = stepsToPlay
defaultSearchStrategy =
match gameMap.DefaultSearcher with
| searcher.BFS -> BFSMode
| searcher.DFS -> DFSMode
| x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now."
serializeSteps = false
mapName = gameMap.MapName
oracle = Some oracle
}
{ stepsToSwitchToAI = stepsToStart
stepsToPlay = stepsToPlay
defaultSearchStrategy =
match gameMap.DefaultSearcher with
| searcher.BFS -> BFSMode
| searcher.DFS -> DFSMode
| x -> failwithf $"Unexpected searcher {x}. Use DFS or BFS for now."
serializeSteps = false
mapName = gameMap.MapName
oracle = Some oracle }

let options =
VSharpOptions (
VSharpOptions(
timeout = 15 * 60,
outputDirectory = outputDirectory,
searchStrategy = SearchStrategy.AI,
aiAgentTrainingOptions = aiTrainingOptions,
stepsLimit = uint (stepsToPlay + stepsToStart),
solverTimeout = 2
)
let explorationResult =
explore gameMap options

let explorationResult = explore gameMap options

Application.reset ()
API.Reset ()
HashMap.hashMap.Clear ()
API.Reset()
HashMap.hashMap.Clear()
Serializer.pathConditionVertices.Clear()

do!
sendResponse (
GameOver (
GameOver(
explorationResult.ActualCoverage,
explorationResult.TestsCount,
explorationResult.ErrorsCount
)
)

printfn $"Finish map {gameMap.MapName}, port {port}"
| x -> failwithf $"Unexpected message: %A{x}"

@@ -215,65 +229,68 @@ let ws port outputDirectory (webSocket: WebSocket) (context: HttpContext) =
}

let app port outputDirectory : WebPart =
choose
[
path "/gameServer" >=> handShake (ws port outputDirectory)
]
choose [ path "/gameServer" >=> handShake (ws port outputDirectory) ]

let generateDataForPretraining outputDirectory datasetBasePath (maps: ResizeArray<GameMap>) stepsToSerialize =
for map in maps do
if map.StepsToStart = 0u<step> then
printfn $"Generation for {map.MapName} started."

let map =
GameMap (
GameMap(
map.StepsToPlay,
map.StepsToStart,
Path.Combine (datasetBasePath, map.AssemblyFullName),
Path.Combine(datasetBasePath, map.AssemblyFullName),
map.DefaultSearcher,
map.NameOfObjectToCover,
map.MapName
)

let aiTrainingOptions =
{
stepsToSwitchToAI = 0u<step>
stepsToPlay = 0u<step>
defaultSearchStrategy = searchMode.BFSMode
serializeSteps = true
mapName = map.MapName
oracle = None
}
{ stepsToSwitchToAI = 0u<step>
stepsToPlay = 0u<step>
defaultSearchStrategy = searchMode.BFSMode
serializeSteps = true
mapName = map.MapName
oracle = None }

let options =
VSharpOptions (
VSharpOptions(
timeout = 5 * 60,
outputDirectory = outputDirectory,
searchStrategy = SearchStrategy.ExecutionTreeContributedCoverage,
stepsLimit = stepsToSerialize,
solverTimeout = 2,
aiAgentTrainingOptions = aiTrainingOptions
)

let folderForResults =
Serializer.getFolderToStoreSerializationResult outputDirectory map.MapName

if Directory.Exists folderForResults then
Directory.Delete (folderForResults, true)
let _ =
Directory.CreateDirectory folderForResults
Directory.Delete(folderForResults, true)

let _ = Directory.CreateDirectory folderForResults

let explorationResult = explore map options
File.WriteAllText (
Path.Join (folderForResults, "result"),

File.WriteAllText(
Path.Join(folderForResults, "result"),
$"{explorationResult.ActualCoverage} {explorationResult.TestsCount} {explorationResult.StepsCount} {explorationResult.ErrorsCount}"
)

printfn
$"Generation for {map.MapName} finished with coverage {explorationResult.ActualCoverage}, tests {explorationResult.TestsCount}, steps {explorationResult.StepsCount},errors {explorationResult.ErrorsCount}."

Application.reset ()
API.Reset ()
HashMap.hashMap.Clear ()
API.Reset()
HashMap.hashMap.Clear()

[<EntryPoint>]
let main args =
let parser =
ArgumentParser.Create<CliArguments> (programName = "VSharp.ML.GameServer.Runner.exe")
ArgumentParser.Create<CliArguments>(programName = "VSharp.ML.GameServer.Runner.exe")

let args = parser.Parse args

let mode = args.GetResult <@ Mode @>
@@ -298,19 +315,16 @@ let main args =
| Some steps -> steps
| None -> 500u

let useGPU =
(args.TryGetResult <@ UseGPU @>).IsSome
let useGPU = (args.TryGetResult <@ UseGPU @>).IsSome

let optimize =
(args.TryGetResult <@ Optimize @>).IsSome
let optimize = (args.TryGetResult <@ Optimize @>).IsSome

let outputDirectory =
Path.Combine (Directory.GetCurrentDirectory (), string port)
let outputDirectory = Path.Combine(Directory.GetCurrentDirectory(), string port)

if Directory.Exists outputDirectory then
Directory.Delete (outputDirectory, true)
let testsDirInfo =
Directory.CreateDirectory outputDirectory
Directory.Delete(outputDirectory, true)

let testsDirInfo = Directory.CreateDirectory outputDirectory
printfn $"outputDir: {outputDirectory}"

match mode with
@@ -319,11 +333,7 @@ let main args =
startWebServer
{ defaultConfig with
logger = Targets.create Verbose [||]
bindings =
[
HttpBinding.createSimple HTTP "127.0.0.1" port
]
}
bindings = [ HttpBinding.createSimple HTTP "127.0.0.1" port ] }
(app port outputDirectory)
with e ->
printfn $"Failed on port {port}"
422 changes: 269 additions & 153 deletions VSharp.ML.GameServer/Messages.fs

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion VSharp.SILI.Core/PathCondition.fs
Original file line number Diff line number Diff line change
@@ -7,7 +7,7 @@ type pathCondition = pset<term>
// - PC does not contain True
// - if PC contains False then False is the only element in PC

module internal PC =
module PC =

let public empty : pathCondition = PersistentSet.empty<term>
let public isEmpty pc = PersistentSet.isEmpty pc
2 changes: 1 addition & 1 deletion VSharp.SILI/CILState.fs
Original file line number Diff line number Diff line change
@@ -544,7 +544,7 @@ module CilState =
override this.CodeLocation = this.approximateLoc
override this.CallStack = Memory.StackTrace this.state.memory.Stack |> List.map (fun m -> m :?> Method)
override this.Id = this.internalId
override this.PathConditionSize with get () = PersistentSet.cardinality this.state.pc |> uint32
override this.PathCondition with get () = this.state.pc
override this.VisitedAgainVertices with get () = this.visitedAgainVertices
override this.VisitedNotCoveredVerticesInZone with get () = this.visitedNotCoveredVerticesInZone
override this.VisitedNotCoveredVerticesOutOfZone with get () = this.visitedNotCoveredVerticesOutOfZone

Unchanged files with check annotations Beta

var methodName = t.Last();
var x = type.GetMethods(Reflection.allBindingFlags);
method ??= x
.Where(m => type.FullName.Split('.').Last().Contains(className) && m.Name.Contains(methodName))

Check warning on line 96 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Dereference of a possibly null reference.

Check warning on line 96 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Dereference of a possibly null reference.
.MinBy(m => m.Name.Length);
if (method != null)
break;
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 533 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.EntryPointHandler(FileInfo assemblyPath, string[]? args, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 533 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.EntryPointHandler(FileInfo assemblyPath, string[]? args, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 597 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.AllPublicMethodsHandler(FileInfo assemblyPath, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 597 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.AllPublicMethodsHandler(FileInfo assemblyPath, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
parseResult.GetValueForOption(pathToModelOption),

Check warning on line 627 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.PublicMethodsOfTypeHandler(FileInfo assemblyPath, string typeName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 627 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.PublicMethodsOfTypeHandler(FileInfo assemblyPath, string typeName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
parseResult.GetValueForOption(verbosityOption),
parseResult.GetValueForOption(recursionThresholdOption),
parseResult.GetValueForOption(explorationModeOption),
pathToModel,

Check warning on line 660 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.SpecificMethodHandler(FileInfo assemblyPath, string methodName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, bool checkCoverage, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.

Check warning on line 660 in VSharp.Runner/RunnerProgram.cs

GitHub Actions / build

Possible null reference argument for parameter 'pathToModel' in 'void RunnerProgram.SpecificMethodHandler(FileInfo assemblyPath, string methodName, int timeout, int solverTimeout, DirectoryInfo output, bool renderTests, bool runTests, bool checkCoverage, SearchStrategy strat, Verbosity verbosity, uint recursionThreshold, ExplorationMode explorationMode, string pathToModel, bool useGPU, bool optimize)'.
parseResult.GetValueForOption(useGPUOption),
parseResult.GetValueForOption(optimizeOption)
);
stepsLimit: options.StepsLimit,
aiAgentTrainingOptions: options.AIAgentTrainingOptions == null ? FSharpOption<AIAgentTrainingOptions>.None : FSharpOption<AIAgentTrainingOptions>.Some(options.AIAgentTrainingOptions),
pathToModel: options.PathToModel == null ? FSharpOption<string>.None : FSharpOption<string>.Some(options.PathToModel),
useGPU: options.UseGPU == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.UseGPU),

Check warning on line 196 in VSharp.API/VSharp.cs

GitHub Actions / build

The result of the expression is always 'false' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 196 in VSharp.API/VSharp.cs

GitHub Actions / build

The result of the expression is always 'false' since a value of type 'bool' is never equal to 'null' of type 'bool?'
optimize: options.Optimize == null ? FSharpOption<bool>.None : FSharpOption<bool>.Some(options.Optimize)

Check warning on line 197 in VSharp.API/VSharp.cs

GitHub Actions / build

The result of the expression is always 'false' since a value of type 'bool' is never equal to 'null' of type 'bool?'

Check warning on line 197 in VSharp.API/VSharp.cs

GitHub Actions / build

The result of the expression is always 'false' since a value of type 'bool' is never equal to 'null' of type 'bool?'
);
var fuzzerOptions =
// TODO: merging!
type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> with
override x.ToString() = MemoryRegion.toString "" x

Check warning on line 788 in VSharp.SILI.Core/MemoryRegion.fs

GitHub Actions / build

Override implementations in augmentations are now deprecated. Override implementations should be given as part of the initial declaration of a type.

Check warning on line 788 in VSharp.SILI.Core/MemoryRegion.fs

GitHub Actions / build

Override implementations in augmentations are now deprecated. Override implementations should be given as part of the initial declaration of a type.
type setKeyWrapper<'key when 'key : equality> =
{key : 'key}
returnType = types.Last();
}
var declaringType = mi.DeclaringType;
return declaringType.GetProperty(propertyName, Reflection.allBindingFlags, null, returnType, argumentTypes, null) != null;

Check warning on line 152 in VSharp.TestRenderer/CodeRenderer.cs

GitHub Actions / build

Dereference of a possibly null reference.

Check warning on line 152 in VSharp.TestRenderer/CodeRenderer.cs

GitHub Actions / build

Dereference of a possibly null reference.
}
propertyName = string.Empty;
// NOTE: first 16 bytes contain array meta info
public const int ArrayElementsOffset = 16;
public static readonly int StringElementsOffset = RuntimeHelpers.OffsetToStringData;

Check warning on line 56 in VSharp.CSharpUtils/LayoutUtils.cs

GitHub Actions / build

'RuntimeHelpers.OffsetToStringData' is obsolete: 'OffsetToStringData has been deprecated. Use string.GetPinnableReference() instead.'

Check warning on line 56 in VSharp.CSharpUtils/LayoutUtils.cs

GitHub Actions / build

'RuntimeHelpers.OffsetToStringData' is obsolete: 'OffsetToStringData has been deprecated. Use string.GetPinnableReference() instead.'
}
}