diff --git a/VSharp.API/Options.cs b/VSharp.API/Options.cs new file mode 100644 index 000000000..6376e4795 --- /dev/null +++ b/VSharp.API/Options.cs @@ -0,0 +1,90 @@ +using System.IO; +using VSharp.Interpreter.IL; + +namespace VSharp +{ + /// + /// Symbolic virtual machine execution mode. + /// + public enum ExecutionMode + { + /// + /// Pure symbolic execution. Cannot cope with external dependencies in code. + /// + Symbolic, + /// + /// (Experimental) Concrete and symbolic execution combination. Allows to explore code with external dependencies by + /// instantiating concrete objects. + /// + Concolic + } + + /// + /// + /// + public enum SearchStrategy + { + DFS, + BFS, + ShortestDistance + } + + /// + /// Parameters of the test generation run. + /// + /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// null by default. + /// + /// Symbolic virtual machine execution mode. by default. + /// + /// + /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption). + /// -1 by default + /// If true, constraint independence optimization is enabled: independent constraint sets are maintained + /// during symbolic execution. In general, improves execution time. true by default. + /// If true, SMT solver works in incremental mode during symbolic execution. May improve execution + /// time in some cases. false by default. + /// If true, symbolic execution process animation is saved in /visualize subdirectory of the . + public readonly record struct CoverOptions( + DirectoryInfo OutputDirectory = null, + SearchStrategy SearchStrategy = SearchStrategy.DFS, + ExecutionMode ExecutionMode = ExecutionMode.Symbolic, + bool GuidedSearch = false, + uint RecThreshold = 0u, + int Timeout = -1, + bool IsConstraintIndependenceEnabled = true, + bool IsSolverIncrementalityEnabled = false, + bool Visualize = false + ) + { + internal SiliOptions ToSiliOptions(coverageZone coverageZone) + { + var searchMode = SearchStrategy switch + { + SearchStrategy.DFS => Interpreter.IL.searchMode.DFSMode, + SearchStrategy.BFS => Interpreter.IL.searchMode.BFSMode, + SearchStrategy.ShortestDistance => Interpreter.IL.searchMode.ShortestDistanceBasedMode + }; + + if (GuidedSearch) + { + searchMode = searchMode.NewGuidedMode(searchMode); + } + + var executionMode = ExecutionMode switch + { + ExecutionMode.Symbolic => Interpreter.IL.executionMode.SymbolicMode, + ExecutionMode.Concolic => Interpreter.IL.executionMode.ConcolicMode + }; + + return new SiliOptions( + explorationMode.NewTestCoverageMode(coverageZone, searchMode), + executionMode, + OutputDirectory, + RecThreshold, + Timeout, + Visualize + ); + } + } +} diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index c4604393a..aaa9ac348 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -28,7 +28,7 @@ internal Statistics(TimeSpan time, DirectoryInfo outputDir, uint tests, uint err public TimeSpan TestGenerationTime { get; } /// - /// Directory where *.vst tests are placed + /// Directory where *.vst tests are placed. /// public DirectoryInfo OutputDir { get; } @@ -71,21 +71,16 @@ public void GenerateReport(TextWriter writer) public static class TestGenerator { - private static Statistics StartExploration(List methods, string resultsFolder, string[] mainArguments = null, int timeout = -1) + private static Statistics StartExploration(List methods, CoverOptions options = new(), string[] mainArguments = null) { - var recThreshold = 0u; - UnitTests unitTests = new UnitTests(resultsFolder); + var outputDirectory = options.OutputDirectory ?? new DirectoryInfo(Directory.GetCurrentDirectory()); // TODO: customize search strategies via console options - var options = - new SiliOptions( - explorationMode.NewTestCoverageMode(coverageZone.MethodZone, searchMode.DFSMode), - executionMode.SymbolicMode, - unitTests.TestDirectory, - recThreshold, - timeout, - false); - SILI explorer = new SILI(options); - Core.API.ConfigureSolver(SolverPool.mkSolver()); + UnitTests unitTests = new UnitTests(outputDirectory.FullName); + SILI explorer = new SILI(options.ToSiliOptions(coverageZone.MethodZone)); + // TODO: refresh solver ctx for each method in incremental mode + Core.API.ConfigureSolver(SolverPool.mkSolver(), options.IsSolverIncrementalityEnabled); + Core.API.SetConstraintIndependenceEnabled(options.IsConstraintIndependenceEnabled); + foreach (var method in methods) { if (method == method.Module.Assembly.EntryPoint) @@ -116,24 +111,22 @@ public static bool Reproduce(DirectoryInfo testDir) /// Generates test coverage for specified method. /// /// Type to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// Summary of tests generation process. - public static Statistics Cover(MethodBase method, int timeout = -1, string outputDirectory = "") + public static Statistics Cover(MethodBase method, CoverOptions options = new()) { List methods = new List {method}; - return StartExploration(methods, outputDirectory, null, timeout); + return StartExploration(methods, options); } /// /// Generates test coverage for all public methods of specified type. /// /// Type to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// Summary of tests generation process. /// Thrown if specified class does not contain public methods. - public static Statistics Cover(Type type, int timeout = -1, string outputDirectory = "") + public static Statistics Cover(Type type, CoverOptions options = new()) { List methods = new List(type.GetConstructors()); @@ -146,19 +139,18 @@ public static Statistics Cover(Type type, int timeout = -1, string outputDirecto throw new ArgumentException("I've not found any public method or constructor of class " + type.FullName); } - return StartExploration(methods, outputDirectory, null, timeout); + return StartExploration(methods, options); } /// /// Generates test coverage for all public methods of all public classes in the specified assembly. /// /// Assembly to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// Summary of tests generation process. /// Thrown if no public methods found in assembly. /// - public static Statistics Cover(Assembly assembly, int timeout = -1, string outputDirectory = "") + public static Statistics Cover(Assembly assembly, CoverOptions options = new()) { List methods; BindingFlags bindingFlags = BindingFlags.Instance | BindingFlags.Static | BindingFlags.Public | @@ -180,20 +172,19 @@ public static Statistics Cover(Assembly assembly, int timeout = -1, string outpu throw new ArgumentException("I've not found any public method in assembly"); } - return StartExploration(methods, outputDirectory, null, timeout); + return StartExploration(methods, options); } /// /// Generates test coverage for the entry point of the specified assembly. /// /// Assembly to be covered with tests. - /// Command line arguments of entry point - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Command line arguments of entry point. + /// Additional parameters of the run. /// Summary of tests generation process. /// Thrown if assembly does not contain entry point. /// - public static Statistics Cover(Assembly assembly, string[] args, int timeout = -1, string outputDirectory = "") + public static Statistics Cover(Assembly assembly, string[] args, CoverOptions options = new()) { List methods; var entryPoint = assembly.EntryPoint; @@ -203,19 +194,18 @@ public static Statistics Cover(Assembly assembly, string[] args, int timeout = - } methods = new List { entryPoint }; - return StartExploration(methods, outputDirectory, args, timeout); + return StartExploration(methods, options, args); } /// /// Generates test coverage for the specified method and runs all tests. /// /// Type to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// True if all generated tests have passed. - public static bool CoverAndRun(MethodBase method, int timeout = -1, string outputDirectory = "") + public static bool CoverAndRun(MethodBase method, CoverOptions options = new()) { - var stats = Cover(method, timeout, outputDirectory); + var stats = Cover(method, options); return Reproduce(stats.OutputDir); } @@ -223,13 +213,12 @@ public static bool CoverAndRun(MethodBase method, int timeout = -1, string outpu /// Generates test coverage for the specified type and runs all tests. /// /// Type to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// True if all generated tests have passed. /// Thrown if specified class does not contain public methods. - public static bool CoverAndRun(Type type, int timeout = -1, string outputDirectory = "") + public static bool CoverAndRun(Type type, CoverOptions options = new()) { - var stats = Cover(type, timeout, outputDirectory); + var stats = Cover(type, options); return Reproduce(stats.OutputDir); } @@ -237,14 +226,13 @@ public static bool CoverAndRun(Type type, int timeout = -1, string outputDirecto /// Generates test coverage for all public methods of all public classes of the specified assembly and runs all tests. /// /// Assembly to be covered with tests. - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Additional parameters of the run. /// True if all generated tests have passed. /// Thrown if no public methods found in assembly. /// - public static bool CoverAndRun(Assembly assembly, int timeout = -1, string outputDirectory = "") + public static bool CoverAndRun(Assembly assembly, CoverOptions options = new()) { - var stats = Cover(assembly, timeout, outputDirectory); + var stats = Cover(assembly, options); return Reproduce(stats.OutputDir); } @@ -252,14 +240,13 @@ public static bool CoverAndRun(Assembly assembly, int timeout = -1, string outpu /// Generates test coverage for entry point of the specified assembly and runs all tests. /// /// Assembly to be covered with tests. - /// Command line arguments of entry point - /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interuption). - /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Command line arguments of entry point. + /// Additional parameters of the run. /// True if all generated tests have passed. /// Thrown if assembly does not contain entry point. - public static bool CoverAndRun(Assembly assembly, string[] args, int timeout = -1, string outputDirectory = "") + public static bool CoverAndRun(Assembly assembly, string[] args, CoverOptions options = new()) { - var stats = Cover(assembly, args, timeout, outputDirectory); + var stats = Cover(assembly, args, options); return Reproduce(stats.OutputDir); } diff --git a/VSharp.Runner/RunnerProgram.cs b/VSharp.Runner/RunnerProgram.cs index 41024cc90..323d88788 100644 --- a/VSharp.Runner/RunnerProgram.cs +++ b/VSharp.Runner/RunnerProgram.cs @@ -1,5 +1,4 @@ using System; -using System.Collections.Generic; using System.CommandLine; using System.CommandLine.Invocation; using System.IO; @@ -111,20 +110,45 @@ private static void PostProcess(Statistics statistics) public static int Main(string[] args) { + var defaultOptions = new CoverOptions(); + var assemblyPathArgument = new Argument("assembly-path", description: "Path to the target assembly"); - var timeoutOption = - new Option(aliases: new[] { "--timeout", "-t" }, - () => -1, - "Time for test generation. Negative values mean no timeout."); - var outputOption = - new Option(aliases: new[] { "--output", "-o" }, - () => new DirectoryInfo(Directory.GetCurrentDirectory()), - "Path where unit tests will be generated"); + + var timeoutOption = new Option( + aliases: new[] { "--timeout", "-t" }, + description: "Time for test generation. Negative values mean no timeout", + getDefaultValue: () => defaultOptions.Timeout + ); + + var outputOption = new Option( + aliases: new[] { "--output", "-o" }, + description: "Path where unit tests will be generated. Process working directory by default", + getDefaultValue: () => defaultOptions.OutputDirectory + ); + var concreteArguments = new Argument("args", description: "Command line arguments"); - var unknownArgsOption = - new Option("--unknown-args", description: "Force engine to generate various input console arguments"); + + var unknownArgsOption = new Option( + "--unknown-args", + description: "Force engine to generate various input console arguments", + getDefaultValue: () => false + ); + + var constraintIndependenceOption = new Option( + "--c-independence", + description: "If true, constraint independence optimization is enabled: independent constraint sets are maintained " + + "during symbolic execution. In general, improves execution time", + getDefaultValue: () => defaultOptions.IsConstraintIndependenceEnabled + ); + + var incrementalityOption = new Option( + "--incrementality", + description: "If true, SMT solver works in incremental mode during symbolic execution. May improve execution time" + + " in some cases", + getDefaultValue: () => defaultOptions.IsSolverIncrementalityEnabled + ); var rootCommand = new RootCommand(); @@ -136,12 +160,18 @@ public static int Main(string[] args) entryPointCommand.AddGlobalOption(timeoutOption); entryPointCommand.AddGlobalOption(outputOption); entryPointCommand.AddOption(unknownArgsOption); + entryPointCommand.AddOption(constraintIndependenceOption); + entryPointCommand.AddOption(incrementalityOption); + var allPublicMethodsCommand = new Command("--all-public-methods", "Generate unit tests for all public methods of all public classes of assembly"); rootCommand.AddCommand(allPublicMethodsCommand); allPublicMethodsCommand.AddArgument(assemblyPathArgument); allPublicMethodsCommand.AddGlobalOption(timeoutOption); allPublicMethodsCommand.AddGlobalOption(outputOption); + allPublicMethodsCommand.AddOption(constraintIndependenceOption); + allPublicMethodsCommand.AddOption(incrementalityOption); + var publicMethodsOfClassCommand = new Command("--public-methods-of-class", "Generate unit tests for all public methods of specified class"); rootCommand.AddCommand(publicMethodsOfClassCommand); @@ -150,6 +180,9 @@ public static int Main(string[] args) publicMethodsOfClassCommand.AddArgument(assemblyPathArgument); publicMethodsOfClassCommand.AddGlobalOption(timeoutOption); publicMethodsOfClassCommand.AddGlobalOption(outputOption); + publicMethodsOfClassCommand.AddOption(constraintIndependenceOption); + publicMethodsOfClassCommand.AddOption(incrementalityOption); + var specificMethodCommand = new Command("--method", "Try to resolve and generate unit test coverage for the specified method"); rootCommand.AddCommand(specificMethodCommand); @@ -158,47 +191,93 @@ public static int Main(string[] args) specificMethodCommand.AddArgument(assemblyPathArgument); specificMethodCommand.AddGlobalOption(timeoutOption); specificMethodCommand.AddGlobalOption(outputOption); + specificMethodCommand.AddOption(constraintIndependenceOption); + specificMethodCommand.AddOption(incrementalityOption); rootCommand.Description = "Symbolic execution engine for .NET"; - entryPointCommand.Handler = CommandHandler.Create((assemblyPath, args, timeout, output, unknownArgs) => - { - var assembly = ResolveAssembly(assemblyPath); - if (unknownArgs) - args = null; - if (assembly != null) - PostProcess(TestGenerator.Cover(assembly, args, timeout, output.FullName)); - }); - allPublicMethodsCommand.Handler = CommandHandler.Create((assemblyPath, timeout, output) => - { - var assembly = ResolveAssembly(assemblyPath); - if (assembly != null) - PostProcess(TestGenerator.Cover(assembly, timeout, output.FullName)); - }); - publicMethodsOfClassCommand.Handler = CommandHandler.Create((className, assemblyPath, timeout, output) => - { - var assembly = ResolveAssembly(assemblyPath); - if (assembly != null) + entryPointCommand.Handler = CommandHandler.Create + ( + (assemblyPath, args, timeout, output, unknownArgs, cIndependence, incrementality) => { - var type = ResolveType(assembly, className); - if (type != null) + var assembly = ResolveAssembly(assemblyPath); + if (unknownArgs) + args = null; + if (assembly != null) { - PostProcess(TestGenerator.Cover(type, timeout, output.FullName)); + var options = new CoverOptions( + OutputDirectory: output, + IsConstraintIndependenceEnabled: cIndependence, + IsSolverIncrementalityEnabled: incrementality, + Timeout: timeout + ); + + PostProcess(TestGenerator.Cover(assembly, args, options)); } } - }); - specificMethodCommand.Handler = CommandHandler.Create((methodName, assemblyPath, timeout, output) => - { - var assembly = ResolveAssembly(assemblyPath); - if (assembly != null) + ); + allPublicMethodsCommand.Handler = CommandHandler.Create + ( + (assemblyPath, timeout, output, cIndependence, incrementality) => + { + var assembly = ResolveAssembly(assemblyPath); + if (assembly != null) + { + var options = new CoverOptions( + OutputDirectory: output, + IsConstraintIndependenceEnabled: cIndependence, + IsSolverIncrementalityEnabled: incrementality, + Timeout: timeout + ); + + PostProcess(TestGenerator.Cover(assembly, options)); + } + } + ); + publicMethodsOfClassCommand.Handler = CommandHandler.Create + ( + (className, assemblyPath, timeout, output, cIndependence, incrementality) => + { + var assembly = ResolveAssembly(assemblyPath); + if (assembly != null) + { + var type = ResolveType(assembly, className); + if (type != null) + { + var options = new CoverOptions( + OutputDirectory: output, + IsConstraintIndependenceEnabled: cIndependence, + IsSolverIncrementalityEnabled: incrementality, + Timeout: timeout + ); + + PostProcess(TestGenerator.Cover(type, options)); + } + } + } + ); + specificMethodCommand.Handler = CommandHandler.Create + ( + (methodName, assemblyPath, timeout, output, cIndependence, incrementality) => { - var method = ResolveMethod(assembly, methodName); - if (method != null) + var assembly = ResolveAssembly(assemblyPath); + if (assembly != null) { - PostProcess(TestGenerator.Cover(method, timeout, output.FullName)); + var method = ResolveMethod(assembly, methodName); + if (method != null) + { + var options = new CoverOptions( + OutputDirectory: output, + IsConstraintIndependenceEnabled: cIndependence, + IsSolverIncrementalityEnabled: incrementality, + Timeout: timeout + ); + + PostProcess(TestGenerator.Cover(method, options)); + } } } - }); + ); return rootCommand.InvokeAsync(args).Result; } diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index e171173c1..fb8534650 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -6,8 +6,10 @@ open FSharpx.Collections open VSharp module API = - let ConfigureSolver solver = - SolverInteraction.configureSolver solver + let SetConstraintIndependenceEnabled enabled = + FeatureFlags.setConstraintIndependenceEnabled enabled + let ConfigureSolver solver enableIncrementalMode = + SolverInteraction.configureSolver solver enableIncrementalMode let ConfigureSimplifier simplifier = configureSimplifier simplifier @@ -165,10 +167,12 @@ module API = | _ -> internalfailf "Unboxing: expected heap reference, but got %O" reference let AddConstraint conditionState condition = Memory.addConstraint conditionState condition - let IsFalsePathCondition conditionState = PC.isFalse conditionState.pc - let Contradicts state condition = PC.add state.pc condition |> PC.isFalse - let PathConditionToSeq (pc : pathCondition) = PC.toSeq pc - let EmptyPathCondition = PC.empty + let IsFalsePathCondition conditionState = conditionState.pc.IsFalse + let Contradicts state condition = + let copy = PC.add state.pc condition + copy.IsFalse + let PathConditionToSeq (pc : IPathCondition) = pc.ToSeq() + let EmptyPathCondition() = PC.create() module Types = let Numeric t = Types.Numeric t @@ -273,9 +277,9 @@ module API = let EmptyStack = EvaluationStack.empty module public Memory = - let EmptyState() = Memory.makeEmpty false + let EmptyState() = State.makeEmpty false let EmptyModel method = - let modelState = Memory.makeEmpty true + let modelState = State.makeEmpty true Memory.fillWithParametersAndThis modelState method {subst = Dictionary<_,_>(); state = modelState} @@ -390,6 +394,7 @@ module API = let MakeSymbolicThis m = Memory.makeSymbolicThis m let MakeSymbolicValue source name typ = Memory.makeSymbolicValue source name typ + let FillWithParametersAndThis state method = Memory.fillWithParametersAndThis state method let CallStackContainsFunction state method = CallStack.containsFunc state.stack method let CallStackSize state = CallStack.size state.stack @@ -403,6 +408,8 @@ module API = let InitializeStaticMembers state targetType = Memory.initializeStaticMembers state targetType + + let AllocateOnStack state key term = Memory.allocateOnStack state key term let AllocateTemporaryLocalVariable state typ term = let tmpKey = TemporaryLocalVariableKey typ @@ -523,7 +530,7 @@ module API = | _ -> internalfailf "constructing string from char array: expected string reference, but got %O" dstRef let ComposeStates state state' = Memory.composeStates state state' - let WLP state pc' = PC.mapPC (Memory.fillHoles state) pc' |> PC.union state.pc + let WLP state (pc' : IPathCondition) = PC.map (Memory.fillHoles state) pc' |> PC.unionWith state.pc let Merge2States (s1 : state) (s2 : state) = Memory.merge2States s1 s2 let Merge2Results (r1, s1 : state) (r2, s2 : state) = Memory.merge2Results (r1, s1) (r2, s2) @@ -546,7 +553,9 @@ module API = state.lowerBounds <- PersistentDict.update state.lowerBounds typ (MemoryRegion.empty Types.lengthType) (MemoryRegion.fillRegion value) | StackBufferSort key -> state.stackBuffers <- PersistentDict.update state.stackBuffers key (MemoryRegion.empty Types.Int8) (MemoryRegion.fillRegion value) + + let IsStackEmpty state = CallStack.isEmpty state.stack module Print = let Dump state = Memory.dump state - let PrintPC pc = PC.toString pc + let PrintPC (pc : IPathCondition) = pc.ToString() diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index a0bf3524a..b25e8d640 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -5,7 +5,8 @@ open System.Reflection [] module API = - val ConfigureSolver : SolverInteraction.ISolver -> unit + val SetConstraintIndependenceEnabled : bool -> unit + val ConfigureSolver : SolverInteraction.ISolver -> bool -> unit val ConfigureSimplifier : IPropositionalSimplifier -> unit val Reset : unit -> unit val SaveConfiguration : unit -> unit @@ -18,7 +19,7 @@ module API = val StatedConditionalExecutionAppendResults : (state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (state list -> 'a) -> 'a) -> (state -> (state list -> 'a) -> 'a) -> (state list -> 'a) -> 'b) val GuardedApplyExpression : term -> (term -> term) -> term - val GuardedApplyExpressionWithPC : pathCondition -> term -> (term -> term) -> term + val GuardedApplyExpressionWithPC : IPathCondition -> term -> (term -> term) -> term val GuardedStatedApplyStatementK : state -> term -> (state -> term -> (term * state -> 'a) -> 'a) -> ((term * state) list -> 'a) -> 'a val GuardedStatedApplyk : (state -> term -> ('item -> 'a) -> 'a) -> state -> term -> ('item list -> 'item list) -> ('item list -> 'a) -> 'a @@ -107,8 +108,8 @@ module API = val AddConstraint : state -> term -> unit val IsFalsePathCondition : state -> bool val Contradicts : state -> term -> bool - val PathConditionToSeq : pathCondition -> term seq - val EmptyPathCondition : pathCondition + val PathConditionToSeq : IPathCondition -> term seq + val EmptyPathCondition : unit -> IPathCondition module Types = val Numeric : System.Type -> symbolicType @@ -244,6 +245,7 @@ module API = val MakeSymbolicThis : IMethod -> term val MakeSymbolicValue : IMemoryAccessConstantSource -> string -> symbolicType -> term + val FillWithParametersAndThis : state -> IMethod -> unit val CallStackContainsFunction : state -> IMethod -> bool val CallStackSize : state -> int @@ -253,6 +255,7 @@ module API = val InitializeStaticMembers : state -> symbolicType -> unit + val AllocateOnStack : state -> stackKey -> term -> unit val AllocateTemporaryLocalVariable : state -> System.Type -> term -> term val AllocateDefaultClass : state -> symbolicType -> term val AllocateDefaultArray : state -> term list -> symbolicType -> term @@ -288,16 +291,18 @@ module API = // TODO: get rid of all unnecessary stuff below! val ComposeStates : state -> state -> state list - val WLP : state -> pathCondition -> pathCondition + val WLP : state -> IPathCondition -> IPathCondition val Merge2States : state -> state -> state list val Merge2Results : term * state -> term * state -> (term * state) list val FillRegion : state -> term -> regionSort -> unit + + val IsStackEmpty : state -> bool module Print = val Dump : state -> string - val PrintPC : pathCondition -> string + val PrintPC : IPathCondition -> string // module Marshalling = // val Unmarshal : state -> obj -> term * state diff --git a/VSharp.SILI.Core/Branching.fs b/VSharp.SILI.Core/Branching.fs index 79a7cd1f3..412d8c8d6 100644 --- a/VSharp.SILI.Core/Branching.fs +++ b/VSharp.SILI.Core/Branching.fs @@ -2,7 +2,16 @@ namespace VSharp.Core open VSharp -module Branching = +module internal Branching = + + let private keepDependentWith (pc : IPathCondition) cond = + if FeatureFlags.isConstraintIndependenceEnabled() then + pc.Fragments + |> Seq.tryFind (fun pc -> pc.ToSeq() |> Seq.contains cond) + |> Option.defaultValue pc + else + pc + let checkSat state = TypeCasting.checkSatWithSubtyping state let commonGuardedStatedApplyk f state term mergeResults k = @@ -10,7 +19,7 @@ module Branching = | Union gvs -> let filterUnsat (g, v) k = let pc = PC.add state.pc g - if PC.isFalse pc then k None + if pc.IsFalse then k None else Some (pc, v) |> k Cps.List.choosek filterUnsat gvs (fun pcs -> match pcs with @@ -63,11 +72,13 @@ module Branching = | Some model -> model.Eval condition | None -> __unreachable__() if isTrue evaled then - let elsePc = PC.add pc !!condition - if PC.isFalse elsePc then + let notCondition = !!condition + let elsePc = PC.add pc notCondition + if elsePc.IsFalse then thenBranch conditionState (List.singleton >> k) elif not branchesReleased then - conditionState.pc <- elsePc + let independentElsePc = keepDependentWith elsePc notCondition + conditionState.pc <- independentElsePc match checkSat conditionState with | SolverInteraction.SmtUnsat _ -> conditionState.pc <- pc @@ -87,10 +98,11 @@ module Branching = elif isFalse evaled then let notCondition = !!condition let thenPc = PC.add state.pc condition - if PC.isFalse thenPc then + if thenPc.IsFalse then elseBranch conditionState (List.singleton >> k) elif not branchesReleased then - conditionState.pc <- thenPc + let independentThenPc = keepDependentWith thenPc condition + conditionState.pc <- independentThenPc match checkSat conditionState with | SolverInteraction.SmtUnsat _ -> conditionState.pc <- pc @@ -102,7 +114,7 @@ module Branching = let thenState = conditionState let elseState = Memory.copy conditionState (PC.add pc notCondition) thenState.model <- Some model.mdl - elseState.pc <- PC.add pc notCondition + thenState.pc <- thenPc execution thenState elseState condition k else conditionState.pc <- PC.add pc notCondition diff --git a/VSharp.SILI.Core/Copying.fs b/VSharp.SILI.Core/Copying.fs index c88441bd6..932e77b4a 100644 --- a/VSharp.SILI.Core/Copying.fs +++ b/VSharp.SILI.Core/Copying.fs @@ -13,13 +13,19 @@ module internal Copying = interface INonComposableSymbolicConstantSource with override x.SubTerms = seq[] :> term seq override x.Time = VectorTime.zero + override x.IndependentWith otherSource = + match otherSource with + | :? symbolicArrayIndexSource as otherIndex -> + x.lowerBound <> otherIndex.lowerBound || x.upperBound <> otherIndex.upperBound + | _ -> true let private makeArrayIndexConstant state lowerBound upperBound = let source = {lowerBound = lowerBound; upperBound = upperBound} let constant = Constant "i" source Types.Int32 let leftBound = simplifyLessOrEqual lowerBound constant id let rightBound = simplifyLessOrEqual constant upperBound id - let pcWithBounds = PC.add (PC.add state.pc leftBound) rightBound + let pcWithBounds = PC.add state.pc leftBound + pcWithBounds.Add rightBound state.pc <- pcWithBounds constant diff --git a/VSharp.SILI.Core/FeatureFlags.fs b/VSharp.SILI.Core/FeatureFlags.fs new file mode 100644 index 000000000..8f8327645 --- /dev/null +++ b/VSharp.SILI.Core/FeatureFlags.fs @@ -0,0 +1,10 @@ +namespace VSharp.Core + +module internal FeatureFlags = + + let mutable private _isConstraintIndependenceEnabled = false + + let public isConstraintIndependenceEnabled() = _isConstraintIndependenceEnabled + + let public setConstraintIndependenceEnabled enabled = + _isConstraintIndependenceEnabled <- enabled diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 8b6a182c2..94c08bd06 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -5,6 +5,7 @@ open System.Collections.Generic open System.Text open FSharpx.Collections open VSharp +open VSharp.Core open VSharp.Core.Types open VSharp.Core.Types.Constructor open VSharp.Utils @@ -18,31 +19,7 @@ type IMemoryAccessConstantSource = module internal Memory = // ------------------------------- Primitives ------------------------------- - - let makeEmpty complete = { - pc = PC.empty - evaluationStack = EvaluationStack.empty - exceptionsRegister = NoException - stack = CallStack.empty - stackBuffers = PersistentDict.empty - classFields = PersistentDict.empty - arrays = PersistentDict.empty - lengths = PersistentDict.empty - lowerBounds = PersistentDict.empty - staticFields = PersistentDict.empty - boxedLocations = PersistentDict.empty - initializedTypes = SymbolicSet.empty - concreteMemory = Dictionary<_,_>() - physToVirt = PersistentDict.empty - allocatedTypes = PersistentDict.empty - typeVariables = (MappedStack.empty, Stack.empty) - delegates = PersistentDict.empty - currentTime = [1] - startingTime = VectorTime.zero - model = None - complete = complete - } - + type memoryMode = | ConcreteMemory | SymbolicMemory @@ -54,13 +31,13 @@ module internal Memory = match memoryMode with | ConcreteMemory -> ConcreteMemory.deepCopy state | SymbolicMemory -> state - { state with pc = newPc } + { state with id = Guid.NewGuid().ToString(); pc = newPc } let private isZeroAddress (x : concreteHeapAddress) = x = VectorTime.zero let addConstraint (s : state) cond = - s.pc <- PC.add s.pc cond + s.pc.Add cond let delinearizeArrayIndex ind lens lbs = let detachOne (acc, lens) lb = @@ -179,6 +156,14 @@ module internal Memory = interface IStatedSymbolicConstantSource with override x.SubTerms = Seq.empty override x.Time = VectorTime.zero + override x.IndependentWith otherSource = + match otherSource with + | :? hashCodeSource as otherHashCodeSource -> + match otherHashCodeSource.object, x.object with + | ConstantT(_, otherConstantSource, _), ConstantT(_, constantSource, _) -> + otherConstantSource.IndependentWith constantSource + | _ -> true + | _ -> true let hashConcreteAddress (address : concreteHeapAddress) = address.GetHashCode() |> makeNumber @@ -215,14 +200,29 @@ module internal Memory = | Some time -> time | None -> internalfailf "Requesting time of primitive stack location %O" x.key override x.TypeOfLocation = x.key.TypeOfLocation + override x.IndependentWith otherSource = + match otherSource with + | :? stackReading as otherReading -> x <> otherReading + | _ -> true [] type private heapReading<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = {picker : regionPicker<'key, 'reg>; key : 'key; memoryObject : memoryRegion<'key, 'reg>; time : vectorTime} interface IMemoryAccessConstantSource with - override x.SubTerms = Seq.empty + override x.SubTerms = + let addKeySubTerms _ (regionKey : updateTreeKey<'key, term>) acc = + Seq.fold PersistentSet.add acc regionKey.key.SubTerms + RegionTree.foldr addKeySubTerms PersistentSet.empty x.memoryObject.updates + |> PersistentSet.toSeq + |> Seq.append x.key.SubTerms override x.Time = x.time override x.TypeOfLocation = x.picker.sort.TypeOfLocation + override x.IndependentWith otherSource = + match otherSource with + | :? heapReading<'key, 'reg> as otherReading -> + let rootRegions hr = match hr.memoryObject.updates with | Node dict -> PersistentDict.keys dict + Seq.allPairs (rootRegions x) (rootRegions otherReading) |> Seq.forall (fun (reg1, reg2) -> reg1.CompareTo reg2 = Disjoint) + | _ -> true let (|HeapReading|_|) (src : IMemoryAccessConstantSource) = match src with @@ -272,6 +272,11 @@ module internal Memory = override x.SubTerms = x.baseSource.SubTerms override x.Time = x.baseSource.Time override x.TypeOfLocation = fromDotNetType x.field.typ + override x.IndependentWith otherSource = + match otherSource with + | :? structField as otherField -> + x.field <> otherField.field && x.baseSource.IndependentWith otherField.baseSource + | _ -> true let (|StructFieldSource|_|) (src : IMemoryAccessConstantSource) = match src with @@ -285,6 +290,10 @@ module internal Memory = override x.SubTerms = x.baseSource.SubTerms override x.Time = x.baseSource.Time override x.TypeOfLocation = x.baseSource.TypeOfLocation + override x.IndependentWith otherSource = + match otherSource with + | :? heapAddressSource as otherAddress -> x.baseSource.IndependentWith otherAddress.baseSource + | _ -> true let (|HeapAddressSource|_|) (src : IMemoryAccessConstantSource) = match src with @@ -297,6 +306,13 @@ module internal Memory = interface IStatedSymbolicConstantSource with override x.SubTerms = Seq.empty override x.Time = VectorTime.zero + override x.IndependentWith otherSource = + match otherSource with + | :? typeInitialized as otherType -> + let xDotNetType = toDotNetType x.typ + let otherDotNetType = toDotNetType otherType.typ + structuralInfimum xDotNetType otherDotNetType = None + | _ -> true let (|TypeInitializedSource|_|) (src : IStatedSymbolicConstantSource) = match src with @@ -630,7 +646,7 @@ module internal Memory = let private checkBlockBounds state reportError blockSize startByte endByte = let failCondition = simplifyGreater endByte blockSize id ||| simplifyLess startByte (makeNumber 0) id // NOTE: disables overflow in solver - state.pc <- PC.add state.pc (makeExpressionNoOvf failCondition id) + state.pc.Add (makeExpressionNoOvf failCondition id) reportError state failCondition let private readAddressUnsafe address startByte endByte = @@ -653,7 +669,7 @@ module internal Memory = and private readStructUnsafe fields structType startByte endByte = let readField fieldId = fields.[fieldId] - readFieldsUnsafe (makeEmpty false) (fun _ -> __unreachable__()) readField false structType startByte endByte + readFieldsUnsafe (State.makeEmpty false) (fun _ -> __unreachable__()) readField false structType startByte endByte and private getAffectedFields state reportError readField isStatic (blockType : symbolicType) startByte endByte = let t = toDotNetType blockType @@ -980,7 +996,7 @@ module internal Memory = and private writeStructUnsafe structTerm fields structType startByte value = let readField fieldId = fields.[fieldId] - let updatedFields = writeFieldsUnsafe (makeEmpty false) (fun _ -> __unreachable__()) readField false structType startByte value + let updatedFields = writeFieldsUnsafe (State.makeEmpty false) (fun _ -> __unreachable__()) readField false structType startByte value let writeField structTerm (fieldId, value) = writeStruct structTerm fieldId value List.fold writeField structTerm updatedFields @@ -1364,7 +1380,7 @@ module internal Memory = assert(not <| VectorTime.isEmpty state.currentTime) // TODO: do nothing if state is empty! list { - let pc = PC.mapPC (fillHoles state) state'.pc |> PC.union state.pc + let pc = PC.map (fillHoles state) state'.pc |> PC.unionWith state.pc // Note: this is not final evaluationStack of resulting cilState, here we forget left state's opStack at all let evaluationStack = composeEvaluationStacksOf state state'.evaluationStack let exceptionRegister = composeRaisedExceptionsOf state state'.exceptionsRegister @@ -1386,6 +1402,7 @@ module internal Memory = let g = g1 &&& g2 &&& g3 &&& g4 &&& g5 &&& g6 if not <| isFalse g then return { + id = Guid.NewGuid().ToString() pc = if isTrue g then pc else PC.add pc g evaluationStack = evaluationStack exceptionsRegister = exceptionRegister @@ -1460,7 +1477,7 @@ module internal Memory = // TODO: print lower bounds? let sortBy sorter = Seq.sortBy (fst >> sorter) let sb = StringBuilder() - let sb = if PC.isEmpty s.pc then sb else s.pc |> PC.toString |> sprintf "Path condition: %s" |> PrettyPrinting.appendLine sb + let sb = if s.pc.IsEmpty then sb else s.pc.ToString() |> sprintf ("Path condition: %s") |> PrettyPrinting.appendLine sb let sb = dumpDict "Fields" (sortBy toString) toString (MemoryRegion.toString " ") sb s.classFields let sb = dumpDict "Concrete memory" sortVectorTime VectorTime.print toString sb (s.concreteMemory |> Seq.map (fun kvp -> (kvp.Key, kvp.Value)) |> PersistentDict.ofSeq) let sb = dumpDict "Array contents" (sortBy arrayTypeToString) arrayTypeToString (MemoryRegion.toString " ") sb s.arrays diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index b3ce29a17..bad9f4208 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -11,6 +11,7 @@ type IMemoryKey<'a, 'reg when 'reg :> IRegion<'reg>> = abstract Map : (term -> term) -> (symbolicType -> symbolicType) -> (vectorTime -> vectorTime) -> 'reg -> 'reg * 'a abstract IsUnion : bool abstract Unguard : (term * 'a) list + abstract SubTerms : seq type regionSort = | HeapFieldSort of fieldId @@ -63,6 +64,8 @@ type heapAddressKey = newReg, {address = mapTerm x.address} override x.IsUnion = isUnion x.address override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr})) + override x.SubTerms = Seq.singleton x.address + interface IComparable with override x.CompareTo y = match y with @@ -84,6 +87,8 @@ type heapArrayIndexKey = reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; indices = List.map mapTerm x.indices} override x.IsUnion = isUnion x.address override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr; indices = x.indices})) // TODO: if x.indices is the union of concrete values, then unguard indices as well + override x.SubTerms = x.address :: x.indices |> List.toSeq + interface IComparable with override x.CompareTo y = match y with @@ -108,6 +113,7 @@ type heapVectorIndexKey = reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; index = mapTerm x.index} override x.IsUnion = isUnion x.address override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr; index = x.index})) // TODO: if x.index is the union of concrete values, then unguard index as well + override x.SubTerms = [x.address; x.index] |> List.toSeq interface IComparable with override x.CompareTo y = match y with @@ -134,6 +140,8 @@ type stackBufferIndexKey = match x.index.term with | Union gvs when List.forall (fst >> isConcrete) gvs -> gvs |> List.map (fun (g, idx) -> (g, {index = idx})) | _ -> [(True, x)] + override x.SubTerms = Seq.singleton x.index + interface IComparable with override x.CompareTo y = match y with @@ -151,6 +159,8 @@ type symbolicTypeKey = reg.Map mapper, {typ = mapper x.typ} override x.IsUnion = false override x.Unguard = [(True, x)] + override x.SubTerms = Seq.empty + override x.ToString() = x.typ.ToString() type updateTreeKey<'key, 'value when 'key : equality> = diff --git a/VSharp.SILI.Core/Merging.fs b/VSharp.SILI.Core/Merging.fs index 7f10d5707..02991715c 100644 --- a/VSharp.SILI.Core/Merging.fs +++ b/VSharp.SILI.Core/Merging.fs @@ -102,10 +102,10 @@ module internal Merging = let guardedApplyk f term k = commonGuardedApplyk f term merge k let guardedApply f term = guardedApplyk (Cps.ret f) term id - let commonGuardedMapkWithPC pc mapper gvs merge k = + let commonGuardedMapkWithPC (pc : IPathCondition) mapper gvs merge k = let foldFunc gvs (g, v) k = let pc' = PC.add pc g - if PC.isFalse pc' then k gvs + if pc'.IsFalse then k gvs else mapper v (fun t -> k ((g, t) :: gvs)) Cps.List.foldlk foldFunc [] gvs (merge >> k) diff --git a/VSharp.SILI.Core/PathCondition.fs b/VSharp.SILI.Core/PathCondition.fs index 45826af00..32cee9412 100644 --- a/VSharp.SILI.Core/PathCondition.fs +++ b/VSharp.SILI.Core/PathCondition.fs @@ -1,40 +1,283 @@ namespace VSharp.Core open VSharp +open System.Collections.Generic -type pathCondition = pset - -// Invariants: -// - PC does not contain True -// - if PC contains False then False is the only element in PC +type public IPathCondition = + abstract Add : term -> unit + abstract Copy : unit -> IPathCondition + abstract ToSeq : unit -> term seq + abstract UnionWith : IPathCondition -> IPathCondition + abstract Map : (term -> term) -> IPathCondition + abstract IsEmpty : bool + abstract IsFalse : bool + abstract Fragments : IPathCondition seq + abstract Constants : term seq module internal PC = + + /// + /// Naive path condition implementation which maintains a single set of constraints + /// + type private PathCondition private (constraints : HashSet, isFalse : bool) = + + let mutable isFalse = isFalse + + let becomeTrivialFalse() = + constraints.Clear() + isFalse <- true + + new() = PathCondition(HashSet(), false) + + override this.ToString() = + if (this :> IPathCondition).IsEmpty then + if isFalse then "false" else "true" + else Seq.map (fun c -> $"({c})") constraints |> join " /\ " + + interface IPathCondition with + + member this.Add newConstraint = + match newConstraint with + | _ when isFalse -> () + | True -> () + | False -> becomeTrivialFalse() + | _ when constraints.Contains(newConstraint) -> () + // what if constraint is not equal to newConstraint structurally, but is equal logically? + | _ when constraints.Contains(!!newConstraint) -> becomeTrivialFalse() + | _ -> constraints.Add(newConstraint) |> ignore + + member this.Copy() = PathCondition(HashSet(constraints), isFalse) + + member this.ToSeq() = seq constraints + + member this.UnionWith (anotherPc : IPathCondition) = + let union = (this :> IPathCondition).Copy() + anotherPc.ToSeq() |> Seq.iter union.Add + union + + member this.Map mapper = + let mapped = PathCondition() :> IPathCondition + Seq.iter (mapper >> mapped.Add) constraints + mapped + + member this.IsEmpty = constraints.Count = 0 + + member this.IsFalse = isFalse + + member this.Fragments = Seq.singleton this + + member this.Constants = seq constraints |> Seq.map Seq.singleton |> Seq.collect discoverConstants + + type private node = + | Tail of term * term pset + | Node of term + | Empty + + let private unwrapNode = function + | Tail(constant, _) -> constant + | Node(constant) -> constant + | Empty -> invalidOp "Cannot unwrap empty node" + + /// + /// Path condition implementation which maintains independent subsets of constants and constraints ("constraint independence") + /// + (* + constants -- dictionary used as union-find structure for constants. Constants of one subset are + cyclically mapping to each other. There is only one node.Tail in subset and it is the representative + element of the subset. Tail also contains the constraints corresponding to the constants subset + + constraints -- contains all constraints of the PC. Used to avoid picking constraints from subsets each time + when the complete PC is needed + + isFalse -- flag used to determine if the PC is false trivially (i. e. c an !c were added to it). + Invariant: PC doesn't contain True or False as elements. + *) + type private IndependentPathCondition private (constants : Dictionary, constraints : HashSet, isFalse : bool) = + + let mutable isFalse = isFalse + + let nextNode constant = + let mutable found = Empty + constants.TryGetValue(constant, &found) |> ignore + found + + /// + /// Find operation of the union-find structure. Returns not the representative element, but the element before it + /// (for convenience) + /// + let rec findPrevious constant = + match nextNode constant with + | Tail _ -> Some constant + | Node nextTerm -> findPrevious nextTerm + | Empty -> None + + /// + /// Union operation of the union-find structure. Subsets containing oneConstant and anotherConstant are merged. + /// oneConstant and anotherConstant don't need to be the representatives + /// + let union oneConstant anotherConstant = + match findPrevious oneConstant, findPrevious anotherConstant with + | Some onePrevious, Some anotherPrevious -> + match nextNode onePrevious, nextNode anotherPrevious with + | Tail(oneRepresentative, oneConstraints), Tail(anotherRepresentative, anotherConstraints) when + oneRepresentative <> anotherRepresentative -> + let constraintsUnion = PersistentSet.union oneConstraints anotherConstraints + constants.[onePrevious] <- Tail(anotherRepresentative, constraintsUnion) + constants.[anotherPrevious] <- Node(oneRepresentative) + | _ -> () + | _ -> invalidOp "Constant not found in dictionary" + + /// + /// Returns union-find subset (of constants) containing the specified constant + /// + let subset constantInSubset = + seq { + let rec inner currentConstant = + seq { + if currentConstant <> constantInSubset then + yield currentConstant + match nextNode currentConstant with + | Empty -> __unreachable__() + | node -> yield! inner (unwrapNode node) + } + match nextNode constantInSubset with + | Empty -> invalidOp "Constant not found in dictionary" + | node -> + yield constantInSubset + yield! inner (unwrapNode node) + } + + let becomeTrivialFalse() = + constants.Clear() + constraints.Clear() + isFalse <- true + + /// + /// Adds a cyclic subset to the union-find structure + /// + /// Union-find structure + /// Constants to add as nodes to the subset + /// Constraints to add to the tail + let addSubset (constants : Dictionary) constantsToAdd constraintsToAdd = + let firstConstant = constantsToAdd |> Seq.head + + let addNode i (previous, next) = + if i <> Seq.length constantsToAdd - 2 then + constants.[previous] <- Node(next) + else + constants.[previous] <- Tail(next, constraintsToAdd) + constants.[next] <- Node(firstConstant) + + if Seq.length constantsToAdd = 1 then constants.[firstConstant] <- Tail(firstConstant, constraintsToAdd) + else constantsToAdd |> Seq.pairwise |> Seq.iteri addNode + + let addConstraintsToSubset subsetConstant constraintsToAdd = + match findPrevious subsetConstant with + | Some previous -> + match nextNode previous with + | Tail(representative, constraints) -> + let constraintsUnion = PersistentSet.union constraints constraintsToAdd + constants.[previous] <- Tail(representative, constraintsUnion) + | _ -> __unreachable__() + | _ -> __unreachable__() + + let constSourcesIndependent = function + | ConstantT(_, oneSrc, _), ConstantT(_, anotherSrc, _) -> oneSrc.IndependentWith anotherSrc + | _ -> true + + let addNewConstraintWithMerge newConstraint = + let constraintConstants = discoverConstants [newConstraint] + let oldConstants, newConstants = constraintConstants |> Seq.splitBy constants.ContainsKey + + // are there constraints without constants at all? + // answer: yes, in ArrayConcreteUnsafeRead, is it ok? + let newConstraintSet = PersistentSet.add PersistentSet.empty newConstraint + + if Seq.isEmpty newConstants |> not then addSubset constants newConstants newConstraintSet + elif Seq.isEmpty oldConstants |> not then addConstraintsToSubset (Seq.head oldConstants) newConstraintSet + + constraints.Add(newConstraint) |> ignore + + Seq.allPairs newConstants constants.Keys + |> Seq.filter (constSourcesIndependent >> not) + |> Seq.iter (fun (oneConst, anotherConst) -> union oneConst anotherConst) + + match Seq.tryHead oldConstants with + | Some someOldConstant -> + Seq.iter (union someOldConstant) oldConstants + match Seq.tryHead newConstants with + | Some someNewConstant -> union someNewConstant someOldConstant + | _ -> () + | _ -> () + + internal new() = IndependentPathCondition(Dictionary(), HashSet(), false) + + override this.ToString() = + if (this :> IPathCondition).IsEmpty then + if isFalse then "false" else "true" + else Seq.map (fun c -> $"({c})") constraints |> join " /\ " + + interface IPathCondition with + + member this.Copy() = IndependentPathCondition(Dictionary(constants), HashSet(constraints), isFalse) + + member this.IsFalse = isFalse + + member this.IsEmpty = constraints.Count = 0 - let public empty : pathCondition = PersistentSet.empty - let public isEmpty pc = PersistentSet.isEmpty pc + member this.ToSeq() = seq constraints - let public toSeq pc = PersistentSet.toSeq pc + member this.Add newConstraint = + match newConstraint with + | _ when isFalse -> () + | True -> () + | False -> becomeTrivialFalse() + | _ when constraints.Contains(newConstraint) -> () + // what if constraint is not equal to newConstraint structurally, but is equal logically? + | _ when constraints.Contains(!!newConstraint) -> becomeTrivialFalse() + | _ -> addNewConstraintWithMerge newConstraint - let private falsePC = PersistentSet.add empty False - let public isFalse pc = - let isFalsePC = PersistentSet.contains False pc - if isFalsePC then assert(toSeq pc |> Seq.length = 1) - isFalsePC + member this.Map mapper = + let mapped = IndependentPathCondition() :> IPathCondition + Seq.iter (mapper >> mapped.Add) constraints + mapped - let public add pc cond : pathCondition = - match cond with - | True -> pc - | False -> falsePC - | _ when isFalse pc -> falsePC - | _ when PersistentSet.contains !!cond pc -> falsePC - | _ -> PersistentSet.add pc cond + member this.UnionWith (anotherPc : IPathCondition) = + let union = (this :> IPathCondition).Copy() + anotherPc.ToSeq() |> Seq.iter union.Add + union - let public mapPC mapper (pc : pathCondition) : pathCondition = - let mapAndAdd acc cond k = - let acc' = mapper cond |> add acc - if isFalse acc' then falsePC else k acc' - Cps.Seq.foldlk mapAndAdd empty (toSeq pc) id - let public mapSeq mapper (pc : pathCondition) = toSeq pc |> Seq.map mapper + /// + /// Returns the sequence of path conditions such that constants contained in + /// one path condition are independent with constants contained in another one + /// + member this.Fragments = + let getSubsetByRepresentative = function + | Tail(representative, constraints) -> + let constants = Dictionary() + addSubset constants (subset representative) constraints + let constraints = HashSet(PersistentSet.toSeq constraints) + Some(IndependentPathCondition(constants, constraints, false)) + | _ -> None + + if isFalse then + Seq.singleton this + else + Seq.choose getSubsetByRepresentative constants.Values + |> Seq.cast + + member this.Constants = constants.Keys - let toString pc = mapSeq toString pc |> Seq.sort |> join " /\ " + let public add (pc : IPathCondition) newConstraint = + let copy = pc.Copy() + copy.Add newConstraint + copy - let union (pc1 : pathCondition) (pc2 : pathCondition) = Seq.fold add pc1 (toSeq pc2) + let public toSeq (pc : IPathCondition) = pc.ToSeq() + + let public map mapper (pc : IPathCondition) = pc.Map mapper + + let public unionWith anotherPc (pc : IPathCondition) = pc.UnionWith anotherPc + + let public create() : IPathCondition = + if FeatureFlags.isConstraintIndependenceEnabled() then IndependentPathCondition() + else PathCondition() diff --git a/VSharp.SILI.Core/Propositional.fs b/VSharp.SILI.Core/Propositional.fs index da42e3e0e..d284b3738 100644 --- a/VSharp.SILI.Core/Propositional.fs +++ b/VSharp.SILI.Core/Propositional.fs @@ -1,6 +1,7 @@ namespace VSharp.Core open VSharp +open VSharp.Core type IPropositionalSimplifier = abstract member Simplify : term -> term @@ -245,6 +246,11 @@ module internal Propositional = if Seq.isEmpty xs then x else Seq.fold (&&&) x xs | _ -> True + + let splitConjunction term = + match term.term with + | Conjunction args -> List.toSeq args + | _ -> Seq.singleton term let disjunction = function | Seq.Cons(x, xs) -> diff --git a/VSharp.SILI.Core/SolverInteraction.fs b/VSharp.SILI.Core/SolverInteraction.fs index b93667ac6..087ec6365 100644 --- a/VSharp.SILI.Core/SolverInteraction.fs +++ b/VSharp.SILI.Core/SolverInteraction.fs @@ -1,6 +1,8 @@ namespace VSharp.Core +open System.Collections.Generic open FSharpx.Collections +open Microsoft.FSharp.Core open VSharp module public SolverInteraction = @@ -19,12 +21,16 @@ module public SolverInteraction = | SmtUnknown of string type ISolver = - abstract CheckSat : encodingContext -> term -> smtResult + abstract CheckSat : encodingContext -> term -> model -> smtResult abstract Assert : encodingContext -> term -> unit + abstract CheckAssumptions : encodingContext -> term seq -> model -> smtResult - let mutable private solver : ISolver option = None + let mutable private mSolver : ISolver option = None + let mutable private isIncrementalModeEnabled : bool = false - let configureSolver s = solver <- Some s + let configureSolver solver enableIncrementalMode = + mSolver <- Some solver + isIncrementalModeEnabled <- enableIncrementalMode let getEncodingContext (state : state) = let addresses = PersistentDict.keys state.allocatedTypes @@ -32,10 +38,24 @@ module public SolverInteraction = let order = Seq.fold (fun (map, i) address -> Map.add address i map, i + 1) (Map.empty, 1) sortedAddresses |> fst let orderWithNull = Map.add VectorTime.zero 0 order { addressOrder = orderWithNull } - - let checkSat state = // TODO: need to solve types here? #do + + let private getOrEmpty = Option.defaultValue { state = State.makeEmpty true; subst = Dictionary<_, _>() } + + let private checkSatPlainly state = + let ctx = getEncodingContext state + let formula = state.pc.ToSeq() |> conjunction + match mSolver with + | Some s -> s.CheckSat ctx formula (getOrEmpty state.model) + | None -> SmtUnknown "Solver not configured" + + let private checkSatIncrementally state = let ctx = getEncodingContext state - let formula = PC.toSeq state.pc |> conjunction - match solver with - | Some s -> s.CheckSat ctx formula - | None -> SmtUnknown "" + let conditions = state.pc |> PC.toSeq + match mSolver with + | Some s -> s.CheckAssumptions ctx conditions (getOrEmpty state.model) + | None -> SmtUnknown "Solver not configured" + + let checkSat state = + // TODO: need to solve types here? #do + if isIncrementalModeEnabled then checkSatIncrementally state + else checkSatPlainly state diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index 7433f9d71..7de1def01 100644 --- a/VSharp.SILI.Core/State.fs +++ b/VSharp.SILI.Core/State.fs @@ -3,7 +3,6 @@ namespace VSharp.Core open System open System.Collections.Generic open VSharp -open VSharp.Core.Types.Constructor open VSharp.Utils type typeVariables = mappedStack * typeId list stack @@ -89,30 +88,58 @@ with and [] state = { - mutable pc : pathCondition - mutable evaluationStack : evaluationStack - mutable stack : callStack // Arguments and local variables - mutable stackBuffers : pdict // Buffers allocated via stackAlloc - mutable classFields : pdict // Fields of classes in heap - mutable arrays : pdict // Contents of arrays in heap - mutable lengths : pdict // Lengths by dimensions of arrays in heap - mutable lowerBounds : pdict // Lower bounds by dimensions of arrays in heap - mutable staticFields : pdict // Static fields of types without type variables - mutable boxedLocations : pdict // Value types boxed in heap - mutable initializedTypes : symbolicTypeSet // Types with initialized static members - concreteMemory : concreteMemory // Fully concrete objects - mutable physToVirt : pdict // Map from physical address (obj) to concreteHeapAddress - mutable allocatedTypes : pdict // Types of heap locations allocated via new - mutable typeVariables : typeVariables // Type variables assignment in the current state - mutable delegates : pdict // Subtypes of System.Delegate allocated in heap - mutable currentTime : vectorTime // Current timestamp (and next allocated address as well) in this state - mutable startingTime : vectorTime // Timestamp before which all allocated addresses will be considered symbolic - mutable exceptionsRegister : exceptionRegister // Heap-address of exception object - mutable model : model option // Concrete valuation of symbolics - complete : bool // If true, reading of undefined locations would result in default values -} + id : string // Unique identifier for state tracking + mutable pc : IPathCondition + mutable evaluationStack : evaluationStack + mutable stack : callStack // Arguments and local variables + mutable stackBuffers : pdict // Buffers allocated via stackAlloc + mutable classFields : pdict // Fields of classes in heap + mutable arrays : pdict // Contents of arrays in heap + mutable lengths : pdict // Lengths by dimensions of arrays in heap + mutable lowerBounds : pdict // Lower bounds by dimensions of arrays in heap + mutable staticFields : pdict // Static fields of types without type variables + mutable boxedLocations : pdict // Value types boxed in heap + mutable initializedTypes : symbolicTypeSet // Types with initialized static members + concreteMemory : concreteMemory // Fully concrete objects + mutable physToVirt : pdict // Map from physical address (obj) to concreteHeapAddress + mutable allocatedTypes : pdict // Types of heap locations allocated via new + mutable typeVariables : typeVariables // Type variables assignment in the current state + mutable delegates : pdict // Subtypes of System.Delegate allocated in heap + mutable currentTime : vectorTime // Current timestamp (and next allocated address as well) in this state + mutable startingTime : vectorTime // Timestamp before which all allocated addresses will be considered symbolic + mutable exceptionsRegister : exceptionRegister // Heap-address of exception object + mutable model : model option // Concrete valuation of symbolics + complete : bool // If true, reading of undefined locations would result in default values + } and IStatedSymbolicConstantSource = inherit ISymbolicConstantSource abstract Compose : state -> term + +module public State = + + let makeEmpty complete = { + id = Guid.NewGuid().ToString() + pc = PC.create() + evaluationStack = EvaluationStack.empty + exceptionsRegister = NoException + stack = CallStack.empty + stackBuffers = PersistentDict.empty + classFields = PersistentDict.empty + arrays = PersistentDict.empty + lengths = PersistentDict.empty + lowerBounds = PersistentDict.empty + staticFields = PersistentDict.empty + boxedLocations = PersistentDict.empty + initializedTypes = SymbolicSet.empty + concreteMemory = Dictionary<_,_>() + physToVirt = PersistentDict.empty + allocatedTypes = PersistentDict.empty + typeVariables = (MappedStack.empty, Stack.empty) + delegates = PersistentDict.empty + currentTime = [1] + startingTime = VectorTime.zero + model = None + complete = complete + } diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index e52043e81..2bf54c8eb 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -247,6 +247,7 @@ and ISymbolicConstantSource = abstract SubTerms : term seq abstract Time : vectorTime + abstract IndependentWith : ISymbolicConstantSource -> bool type INonComposableSymbolicConstantSource = inherit ISymbolicConstantSource @@ -535,6 +536,10 @@ module internal Terms = let (|UnionT|_|) = term >> function | Union gvs -> Some(UnionT gvs) | _ -> None + + let (|ConstantT|_|) = term >> function + | Constant(name, src, typ) -> Some(ConstantT name, src, typ) + | _ -> None let (|GuardedValues|_|) = function // TODO: this could be ineffective (because of unzip) | Union gvs -> Some(GuardedValues(List.unzip gvs)) @@ -736,10 +741,9 @@ module internal Terms = | GuardedValues(gs, vs) -> foldSeq folder gs state |> foldSeq folder vs | Slice(t, s, e, pos) -> - let state = folder state t - let state = folder state s - let state = folder state e - folder state pos + foldSeq folder [t; s; e; pos] state + | Union(terms) -> + foldSeq folder (List.unzip terms |> (fun (l1, l2) -> List.append l1 l2)) state | _ -> state and doFold folder state term = diff --git a/VSharp.SILI.Core/TypeCasting.fs b/VSharp.SILI.Core/TypeCasting.fs index 281ed08c2..22549e1ec 100644 --- a/VSharp.SILI.Core/TypeCasting.fs +++ b/VSharp.SILI.Core/TypeCasting.fs @@ -27,6 +27,10 @@ module internal TypeCasting = interface IStatedSymbolicConstantSource with override x.SubTerms = optCons (optCons [] x.left.SubTerm) x.right.SubTerm :> term seq override x.Time = VectorTime.zero + override x.IndependentWith otherSource = + match otherSource with + | :? symbolicSubtypeSource as otherSubtype -> x <> otherSubtype + | _ -> true let (|TypeSubtypeTypeSource|_|) (src : ISymbolicConstantSource) = match src with diff --git a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj index 66cbf9abd..d4a68c336 100644 --- a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj +++ b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj @@ -17,6 +17,7 @@ + diff --git a/VSharp.SILI/SILI.fs b/VSharp.SILI/SILI.fs index 5ecdee705..20d551730 100644 --- a/VSharp.SILI/SILI.fs +++ b/VSharp.SILI/SILI.fs @@ -75,7 +75,7 @@ type public SILI(options : SiliOptions) = let coveragePobsForMethod (method : Method) = let cfg = method.CFG cfg.SortedOffsets |> Seq.map (fun offset -> - {loc = {offset = offset; method = method}; lvl = infty; pc = EmptyPathCondition}) + {loc = {offset = offset; method = method}; lvl = infty; pc = EmptyPathCondition()}) |> List.ofSeq let reportState reporter isError method cmdArgs state = diff --git a/VSharp.SILI/Statistics.fs b/VSharp.SILI/Statistics.fs index 27d159b59..4ac429dea 100644 --- a/VSharp.SILI/Statistics.fs +++ b/VSharp.SILI/Statistics.fs @@ -12,7 +12,7 @@ open VSharp.Utils open CilStateOperations open ipOperations -type pob = {loc : codeLocation; lvl : uint; pc : pathCondition} +type pob = {loc : codeLocation; lvl : uint; pc : IPathCondition} with override x.ToString() = $"loc = {x.loc}; lvl = %d{x.lvl}; pc = %s{Print.PrintPC x.pc}" diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 1221a4e46..c4a37d463 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -123,6 +123,7 @@ module TestGenerator = let state2test isError (m : Method) cmdArgs (cilState : cilState) = let indices = Dictionary() let test = UnitTest m.MethodBase + test.StateId <- Some cilState.state.id let hasException = match cilState.state.exceptionsRegister with | Unhandled e -> diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 6621a9632..e9291fa24 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -9,7 +9,6 @@ open VSharp.Core.SolverInteraction open Logger module internal Z3 = - // ------------------------------- Exceptions ------------------------------- type EncodingException(msg : string) = @@ -38,30 +37,30 @@ module internal Z3 = type private encodingCache = { sorts : IDictionary - e2t : IDictionary - t2e : IDictionary + expressionToTerm : IDictionary + termToExpression : IDictionary heapAddresses : IDictionary staticKeys : IDictionary regionConstants : Dictionary mutable lastSymbolicAddress : int32 } with member x.Get(term, encoder : unit -> Expr) = - Dict.tryGetValue2 x.t2e term (fun () -> + Dict.tryGetValue2 x.termToExpression term (fun () -> let result = {expr = encoder(); assumptions = List.empty} - x.e2t.[result.expr] <- term - x.t2e.[term] <- result + x.expressionToTerm.[result.expr] <- term + x.termToExpression.[term] <- result result) member x.Get(term, encoder : unit -> encodingResult) = - Dict.tryGetValue2 x.t2e term (fun () -> + Dict.tryGetValue2 x.termToExpression term (fun () -> let result = encoder() - x.e2t.[result.expr] <- term - x.t2e.[term] <- result + x.expressionToTerm.[result.expr] <- term + x.termToExpression.[term] <- result result) let private freshCache () = { sorts = Dictionary() - e2t = Dictionary() - t2e = Dictionary() + expressionToTerm = Dictionary() + termToExpression = Dictionary() heapAddresses = Dictionary() staticKeys = Dictionary() regionConstants = Dictionary() @@ -76,7 +75,7 @@ module internal Z3 = let getMemoryConstant mkConst (typ : regionSort * fieldId list) = let result : ArrayExpr ref = ref null - if encodingCache.regionConstants.TryGetValue(typ, result) then !result + if encodingCache.regionConstants.TryGetValue(typ, result) then result.Value else let regConst = mkConst() encodingCache.regionConstants.Add(typ, regConst) @@ -84,6 +83,11 @@ module internal Z3 = member x.Reset() = encodingCache <- freshCache() + + member x.ClearQueryScopedCache() = + encodingCache.termToExpression.Clear() + encodingCache.heapAddresses.Clear() + encodingCache.regionConstants.Clear() member private x.ValidateId id = assert(not <| String.IsNullOrWhiteSpace id) @@ -615,12 +619,12 @@ module internal Z3 = let address = x.DecodeConcreteHeapAddress t bv |> ConcreteHeapAddress HeapRef address t | :? BitVecExpr as bv when bv.IsConst -> - if encodingCache.e2t.ContainsKey(expr) then encodingCache.e2t.[expr] + if encodingCache.expressionToTerm.ContainsKey(expr) then encodingCache.expressionToTerm.[expr] else x.GetTypeOfBV bv |> Concrete expr.String | :? IntNum as i -> Concrete i.Int (Numeric (Id typeof)) | :? RatNum as r -> Concrete (double(r.Numerator.Int) * 1.0 / double(r.Denominator.Int)) (Numeric (Id typeof)) | _ -> - if encodingCache.e2t.ContainsKey(expr) then encodingCache.e2t.[expr] + if encodingCache.expressionToTerm.ContainsKey(expr) then encodingCache.expressionToTerm.[expr] elif expr.IsTrue then True elif expr.IsFalse then False elif expr.IsNot then x.DecodeBoolExpr OperationType.LogicalNot expr @@ -657,44 +661,48 @@ module internal Z3 = Memory.DefaultOf structureType |> ref) structureRef.Value <- x.WriteFields structureRef.Value value fields - member x.MkModel (m : Model) = - let subst = Dictionary() + member x.UpdateModel (z3Model : Model) (targetModel : model) = + encodingCache.lastSymbolicAddress <- targetModel.state.startingTime.Head let stackEntries = Dictionary() - encodingCache.t2e |> Seq.iter (fun kvp -> + encodingCache.termToExpression |> Seq.iter (fun kvp -> match kvp.Key with | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} as constant -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) let decoded = x.Decode t refinedExpr if decoded <> constant then x.WriteDictOfValueTypes stackEntries key fields key.TypeOfLocation decoded + | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} -> + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) + x.Decode t refinedExpr + |> x.WriteDictOfValueTypes stackEntries key fields key.TypeOfLocation | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} -> match ms with | HeapAddressSource(StackReading(key)) -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) let t = key.TypeOfLocation let addr = refinedExpr |> x.DecodeConcreteHeapAddress t |> ConcreteHeapAddress stackEntries.Add(key, HeapRef addr t |> ref) | _ -> () | {term = Constant(_, :? IStatedSymbolicConstantSource, _)} -> () | {term = Constant(_, source, t)} -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) let term = x.Decode t refinedExpr - subst.Add(source, term) + targetModel.subst.[source] <- term | _ -> ()) + + if Memory.IsStackEmpty targetModel.state then + Memory.NewStackFrame targetModel.state None List.empty - let state = {Memory.EmptyState() with complete = true} - let frame = stackEntries |> Seq.map (fun kvp -> - let key = kvp.Key - let term = kvp.Value.Value - let typ = TypeOf term - (key, Some term, typ)) - Memory.NewStackFrame state None (List.ofSeq frame) + stackEntries |> Seq.iter (fun kvp -> + let key = kvp.Key + let term = kvp.Value.Value + Memory.AllocateOnStack targetModel.state key term) let defaultValues = Dictionary() encodingCache.regionConstants |> Seq.iter (fun kvp -> let region, fields = kvp.Key let constant = kvp.Value - let arr = m.Eval(constant, false) + let arr = z3Model.Eval(constant, false) let typeOfLocation = if fields.IsEmpty then region.TypeOfLocation else fields.Head.typ |> Types.FromDotNetType @@ -720,33 +728,31 @@ module internal Z3 = let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress typeOfLocation |> ConcreteHeapAddress HeapRef address typeOfLocation let address = fields |> List.fold (fun address field -> StructField(address, field)) address - let states = Memory.Write state (Ref address) value - assert(states.Length = 1 && states.[0] = state) + let states = Memory.Write targetModel.state (Ref address) value + assert(states.Length = 1 && states.[0] = targetModel.state) elif arr.IsConst then () else internalfailf "Unexpected array expression in model: %O" arr parseArray arr) defaultValues |> Seq.iter (fun kvp -> let region = kvp.Key - let constantValue = !kvp.Value - Memory.FillRegion state constantValue region) + let constantValue = kvp.Value.Value + Memory.FillRegion targetModel.state constantValue region) encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then - state.allocatedTypes <- PersistentDict.add addr typ state.allocatedTypes) - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] - - encodingCache.heapAddresses.Clear() - {state = state; subst = subst} - + if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr targetModel.state.allocatedTypes then + targetModel.state.allocatedTypes <- PersistentDict.add addr typ targetModel.state.allocatedTypes) + targetModel.state.startingTime <- VectorTime.min targetModel.state.startingTime [encodingCache.lastSymbolicAddress - 1] let private ctx = new Context() let private builder = Z3Builder(ctx) type internal Z3Solver() = // let optCtx = ctx.MkOptimize() + // Why Solver is named optCtx? let optCtx = ctx.MkSolver() + let assumptions = Dictionary() // let addSoftConstraints lvl = // let pathAtoms = @@ -762,36 +768,42 @@ module internal Z3 = // pathAtoms interface ISolver with - member x.CheckSat (encCtx : encodingContext) (q : term) : smtResult = + member x.CheckSat (encCtx : encodingContext) (q : term) (currentModel : model) : smtResult = printLog Trace "SOLVER: trying to solve constraints..." printLogLazy Trace "%s" (lazy(q.ToString())) try - let query = builder.EncodeTerm encCtx q - let assumptions = query.assumptions - let assumptions = - seq { - yield! (Seq.cast<_> assumptions) - yield query.expr - } |> Array.ofSeq -// let pathAtoms = addSoftConstraints q.lvl - let result = optCtx.Check assumptions - match result with - | Status.SATISFIABLE -> - trace "SATISFIABLE" - let z3Model = optCtx.Model - let model = builder.MkModel z3Model - SmtSat { mdl = model } - | Status.UNSATISFIABLE -> - trace "UNSATISFIABLE" - SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) } - | Status.UNKNOWN -> - trace "UNKNOWN" - SmtUnknown optCtx.ReasonUnknown - | _ -> __unreachable__() - with - | :? EncodingException as e -> - printLog Info "SOLVER: exception was thrown: %s" e.Message - SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message) + try + let query = builder.EncodeTerm encCtx q + let assumptions = query.assumptions + let assumptions = + seq { + yield! (Seq.cast<_> assumptions) + yield query.expr + } + |> Seq.distinct |> Array.ofSeq +// let pathAtoms = addSoftConstraints q.lvl + let result = optCtx.Check assumptions + match result with + | Status.SATISFIABLE -> + trace "SATISFIABLE" + let z3Model = optCtx.Model + let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}} + builder.UpdateModel z3Model updatedModel + SmtSat { mdl = updatedModel } + | Status.UNSATISFIABLE -> + trace "UNSATISFIABLE" + SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) } + | Status.UNKNOWN -> + trace "UNKNOWN" + SmtUnknown optCtx.ReasonUnknown + | _ -> __unreachable__() + with + | :? EncodingException as e -> + printLog Info "SOLVER: exception was thrown: %s" e.Message + SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message) + finally + builder.ClearQueryScopedCache() + member x.Assert encCtx (fml : term) = printLogLazy Trace "SOLVER: Asserting: %s" (lazy(fml.ToString())) @@ -799,5 +811,53 @@ module internal Z3 = let encoded = List.fold (fun acc x -> builder.MkAnd(acc, x)) (encoded.expr :?> BoolExpr) encoded.assumptions optCtx.Assert(encoded) + member x.CheckAssumptions encCtx formulas currentModel = + let encodeToBoolExprs formula = + let encoded = builder.EncodeTerm encCtx formula + seq { + yield! Seq.cast encoded.assumptions + yield encoded.expr :?> BoolExpr + } + try + try + let exprs = Seq.collect encodeToBoolExprs formulas |> Seq.distinct + let boolConsts = seq { + for expr in exprs do + let mutable name = "" + if assumptions.TryGetValue(expr, &name) then + yield ctx.MkBoolConst name + else + name <- $"p{assumptions.Count}" + printLog Trace $"SOLVER: assert: {name} => {expr}" + assumptions.[expr] <- name + let boolConst = ctx.MkBoolConst name + let implication = ctx.MkImplies(boolConst, expr) + optCtx.Assert implication + yield boolConst + } + let names = boolConsts |> Seq.map (fun c -> c.ToString()) + printLog Trace $"""SOLVER: check: {join " & " names}""" + let result = optCtx.Check boolConsts + match result with + | Status.SATISFIABLE -> + trace "SATISFIABLE" + let z3Model = optCtx.Model + let updatedModel = {currentModel with state = {currentModel.state with model = currentModel.state.model}} + builder.UpdateModel z3Model updatedModel + SmtSat { mdl = updatedModel } + | Status.UNSATISFIABLE -> + trace "UNSATISFIABLE" + SmtUnsat { core = Array.empty } + | Status.UNKNOWN -> + trace "UNKNOWN" + SmtUnknown optCtx.ReasonUnknown + | _ -> __unreachable__() + with + | :? EncodingException as e -> + printLog Info "SOLVER: exception was thrown: %s" e.Message + SmtUnknown (sprintf "Z3 has thrown an exception: %s" e.Message) + finally + builder.ClearQueryScopedCache() + let reset() = builder.Reset() diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 358e54c70..e780ea52d 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -1,8 +1,8 @@ using System; -using System.IO; using System.Collections.Generic; using System.Diagnostics; using System.Globalization; +using System.IO; using System.Linq; using System.Threading; using NUnit.Framework; @@ -15,13 +15,6 @@ namespace VSharp.Test { - public enum SearchStrategy - { - DFS, - BFS, - ShortestDistance - } - public class TestSvmFixtureAttribute : NUnitAttribute, IFixtureBuilder { public IEnumerable BuildFrom(ITypeInfo typeInfo) @@ -126,7 +119,9 @@ public TestSvmCommand( private TestResult Explore(TestExecutionContext context) { - Core.API.ConfigureSolver(SolverPool.mkSolver()); + Core.API.ConfigureSolver(SolverPool.mkSolver(), false); + Core.API.SetConstraintIndependenceEnabled(true); + var methodInfo = innerCommand.Test.Method.MethodInfo; try { @@ -169,7 +164,7 @@ private TestResult Explore(TestExecutionContext context) } catch (Exception e) { - context.CurrentResult.SetResult(ResultState.Error, e.Message); + context.CurrentResult.SetResult(ResultState.Error, e.Message, e.StackTrace); } return context.CurrentResult; diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 38ce534bd..543632eb2 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -3,6 +3,7 @@ using System.Linq; using NUnit.Framework; using VSharp.Test; + #pragma warning disable CS0108, CS0114, CS0649 namespace IntegrationTests @@ -1337,7 +1338,7 @@ public bool ArrayContainsOurCustomer(Customerrr[] customers) } [TestSvm(100)] - public bool ContainsOurCustomer(Customerrr other) + public bool EqualsOurCustomer(Customerrr other) { if (other.Equals(_customer)) { diff --git a/VSharp.Test/Tests/LoanExam/CreditCalculator.cs b/VSharp.Test/Tests/LoanExam/CreditCalculator.cs index 3a4d29455..e8d615cb2 100644 --- a/VSharp.Test/Tests/LoanExam/CreditCalculator.cs +++ b/VSharp.Test/Tests/LoanExam/CreditCalculator.cs @@ -1,6 +1,7 @@ using InstantCredit.Shared.Models.Enums; using LoanExam.Models; using System; +using VSharp; using VSharp.Test; namespace LoanExam; diff --git a/VSharp.Test/Tests/Recursion.cs b/VSharp.Test/Tests/Recursion.cs index b1809ca81..d6b78fe84 100644 --- a/VSharp.Test/Tests/Recursion.cs +++ b/VSharp.Test/Tests/Recursion.cs @@ -14,13 +14,13 @@ private static int FibRec(int n) return FibRec(n - 1) + FibRec(n - 2); } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int Fib2() { return FibRec(2); } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int Fib5() { return FibRec(5); @@ -46,7 +46,7 @@ private static void MutatingFib(int n) } } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int FibUnbound(int n) { _c = 42; @@ -68,13 +68,13 @@ private static int GcdRec(int n, int m) return GcdRec(n, m - n); } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int Gcd1() { return GcdRec(15, 4); } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int Gcd15() { return GcdRec(30, 75); @@ -84,7 +84,7 @@ public static int Gcd15() [TestSvmFixture] public static class McCarthy91 { - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static int McCarthy(int n) { return n > 100 ? n - 10 : McCarthy(McCarthy(n + 11)); @@ -135,7 +135,7 @@ private static BigClass MutateAfterRecursion(BigClass s, int n) return s; } - [Ignore("Forward exploration does not handle recursion now")] + [TestSvm] public static SmallClass MutationAfterRecursionTest(int n) { var s1 = new BigClass {Small = new SmallClass()}; diff --git a/VSharp.Test/Tests/RegExTest.cs b/VSharp.Test/Tests/RegExTest.cs index d280823d3..2bad28a77 100644 --- a/VSharp.Test/Tests/RegExTest.cs +++ b/VSharp.Test/Tests/RegExTest.cs @@ -51,9 +51,9 @@ public static bool Match(string re, string text) public class RegExTest { [TestSvm(100)] - public static string OwnImplementationTest(char c1, char c2, char c3, char c4, char c5, char c6) + public static string OwnImplementationTest(char c1, char c2, char c3, char c4, char c5, char c6, char c7, char c8) { - string pattern = new string(new char[] {c1, c2, c3}); + string pattern = new string(new char[] {c1, c2, c3, c4, c5, c6, c7, c8}); string result = ""; if (RegExImplementation.Match(pattern, "hello")) { diff --git a/VSharp.Test/Tests/SolverBenchmark.cs b/VSharp.Test/Tests/SolverBenchmark.cs new file mode 100644 index 000000000..46e209f17 --- /dev/null +++ b/VSharp.Test/Tests/SolverBenchmark.cs @@ -0,0 +1,325 @@ +using System; +using NUnit.Framework; +using VSharp.Test; + +namespace IntegrationTests +{ + [TestSvmFixture] + public static class SolverBenchmark + { + /* + * Idea with Collatz conjecture is taken from + * 'On Benchmarking the Capability of Symbolic Execution Tools with Logic Bombs' + * by Hui Xu et al. + */ + private static int CollatzStep(int a) + { + if (a % 2 == 0) + { + return a / 2; + } + + return 3 * a + 1; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb1(int i) + { + if (i <= 0) + { + return 0; + } + + var loopCount = 0; + var j = i; + + while (j != 1) + { + j = CollatzStep(j); + ++loopCount; + } + + if (loopCount % 2 == 0) + { + return 1; + } + + return 2; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb2(int i) + { + if (i <= 0 || i >= 100) + { + return 0; + } + + var loopCount = 0; + var j = i; + + while (j != 1) + { + j = CollatzStep(j); + ++loopCount; + } + + // Fails with 17 + if (loopCount == 9) + { + return 1; + } + + return 2; + } + + private static int CustomCollatzStep(int a, int b) + { + if (a % 2 == 0) + { + return a / 2; + } + + return b * a + 1; + } + + // Fails with j == 11 and loopCount == 14 + [TestSvm(100)] + public static int CollatzLogicBomOmb3(int i) + { + var j = 12; + var loopCount = 0; + + while (j != 1) + { + j = CustomCollatzStep(j, i); + ++loopCount; + } + + if (loopCount == 9) + { + return 1; + } + + return 2; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb4(int i, int j) + { + var loopCount = 0; + + while (i != 1) + { + if (j == 1) + { + break; + } + + i = CollatzStep(i); + j = CollatzStep(j); + + ++loopCount; + } + + if (loopCount > 3) + { + return 1; + } + + return 2; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb5(int i, int j, int k) + { + var loopCount = 0; + + while (i != 1) + { + if (j == 1) + { + break; + } + + if (k == 1) + { + break; + } + + i = CollatzStep(i); + j = CollatzStep(j); + k = CollatzStep(k); + + ++loopCount; + } + + if (loopCount > 2) + { + return 1; + } + + return 2; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb6(int i, int j) + { + var loopCount = 0; + + while (i + j != 2) + { + i = CollatzStep(i); + j = CollatzStep(j); + + ++loopCount; + } + + if (loopCount > 3) + { + return 1; + } + + return 2; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb7(int i) + { + for (var j = 1; j < 100; ++j) + { + var k = j; + + while (k != i) + { + k = CollatzStep(k); + } + } + + return 0; + } + + [TestSvm(100)] + public static int CollatzLogicBomOmb8(int i, int j) + { + for (var k = 1; k < 17; ++k) + { + var l = k; + + while (l != i) + { + l = CustomCollatzStep(l, j); + } + } + + return 0; + } + + private static int[,] sudoku = + { + { 0, 2, 0, 0 }, + { 3, 0, 0, 0 }, + { 2, 0, 0, 0 }, + { 0, 3, 0, 4 } + }; + + [Ignore("Fails with 'key not found' in getOpCode")] + public static bool SudokuSolution(int[] values) + { + for (var i = 0; i < values.Length; ++i) + { + if (values[i] < 1 || values[i] > 4) + { + return false; + } + } + + var zeroCount = 0; + + for (var i = 0; i < 4; ++i) + { + for (var j = 0; j < 4; ++j) + { + if (sudoku[i, j] == 0) + { + ++zeroCount; + } + } + } + + if (zeroCount != values.Length) + { + return false; + } + + var currentZero = 0; + + for (var i = 0; i < 4; ++i) + { + for (var j = 0; j < 4; ++j) + { + if (sudoku[i, j] == 0) + { + sudoku[i, j] = values[currentZero]; + ++currentZero; + } + } + } + + for (var i = 0; i < 4; ++i) + { + var filled = new bool[4]; + for (var j = 0; j < 4; ++j) + { + filled[sudoku[i, j] - 1] = true; + } + for (var j = 0; j < 4; ++j) + { + if (!filled[j]) + { + return false; + } + } + } + + for (var i = 0; i < 4; ++i) + { + var filled = new bool[4]; + for (var j = 0; j < 4; ++j) + { + filled[sudoku[j, i] - 1] = true; + } + for (var j = 0; j < 4; ++j) + { + if (!filled[j]) + { + return false; + } + } + } + + for (var i = 0; i < 4; i += 2) + { + for (var j = 0; j < 4; j += 2) + { + var filled = new bool[4]; + + for (var k = 0; k < 2; ++k) + { + for (var l = 0; l < 2; ++l) + { + filled[sudoku[i + k, j + l] - 1] = true; + } + } + + if (!filled[j]) + { + return false; + } + } + } + + return true; + } + } +} diff --git a/VSharp.Test/VSharp.Test.csproj b/VSharp.Test/VSharp.Test.csproj index a7c6b94ab..db96cb7c7 100644 --- a/VSharp.Test/VSharp.Test.csproj +++ b/VSharp.Test/VSharp.Test.csproj @@ -40,6 +40,7 @@ + diff --git a/VSharp.Utils/Collections.fs b/VSharp.Utils/Collections.fs index 57fee4f2b..be5b7bd69 100644 --- a/VSharp.Utils/Collections.fs +++ b/VSharp.Utils/Collections.fs @@ -31,6 +31,19 @@ module public Seq = lenProd <- lenProd * lengths.[i] Array.mapFold detachOne (idx, lenProd) (Array.init lengths.Length id) |> fst + /// + /// Splits sequence into two sequences: with elements which satisfy condition and with those + /// which don't + /// + let splitBy condition seq = + let grouped = Seq.groupBy (fun element -> condition element) seq + match Seq.tryFind (fun (value, _) -> value) grouped, + Seq.tryFind (fun (value, _) -> value |> not) grouped with + | Some(_, trueSeq), Some(_, falseSeq) -> trueSeq, falseSeq + | Some(_, trueSeq), None -> trueSeq, Seq.empty + | None, Some(_, falseSeq) -> Seq.empty, falseSeq + | None, None -> Seq.empty, Seq.empty + module public List = let rec private mappedPartitionAcc f left right = function | [] -> (List.rev left, List.rev right) diff --git a/VSharp.Utils/PersistentDictionary.fs b/VSharp.Utils/PersistentDictionary.fs index b72da08ed..6f1a76259 100644 --- a/VSharp.Utils/PersistentDictionary.fs +++ b/VSharp.Utils/PersistentDictionary.fs @@ -50,8 +50,12 @@ module public PersistentDict = let public size (d : pdict<'a, 'b>) = d.impl.Length - let public map (keyMapper : 'a -> 'a) (valueMapper : 'b -> 'c) (d : pdict<'a, 'b>) : pdict<'a, 'c> = + let public map (keyMapper : 'a -> 'd) (valueMapper : 'b -> 'c) (d : pdict<'a, 'b>) : pdict<'d, 'c> = d |> toSeq |> Seq.map (fun (k, v) -> (keyMapper k, valueMapper v)) |> ofSeq + + let public filterKeys (filter : 'a -> bool) (d : pdict<'a, 'b>) : pdict<'a, 'b> = + d |> toSeq |> Seq.filter (fun (k, _) -> filter k) |> ofSeq + let public iter (action : 'a * 'b -> unit) (d : pdict<'a, 'b>) : unit = d |> toSeq |> Seq.iter action let public fold folder state (d : pdict<'a, 'b>) = @@ -118,6 +122,9 @@ module PersistentSet = let public isEmpty (d : pset<'a>) = PersistentDict.isEmpty d let public toSeq (d : pset<'a>) = PersistentDict.keys d + + let public ofSeq (s : seq<'a>) : pset<'a> = + s |> Seq.map (fun k -> k, 0) |> PersistentDict.ofSeq let public contains (key : 'a) (d : pset<'a>) = PersistentDict.contains key d @@ -131,8 +138,16 @@ module PersistentSet = d |> toSeq |> Seq.fold folder state let public forall predicate (d : pset<'a>) = d |> toSeq |> Seq.forall predicate - let public map (mapper : 'a -> 'a) (d : pset<'a>) : pset<'a> = + + let public map (mapper : 'a -> 'b) (d : pset<'a>) : pset<'b> = PersistentDict.map mapper id d + + let public filter (filter : 'a -> bool) (d : pset<'a>) : pset<'a> = + PersistentDict.filterKeys filter d + + let public choose (chooser : 'a -> 'b option) (d : pset<'a>) : pset<'b> = + d |> toSeq |> Seq.choose chooser |> ofSeq + let public iter (action : 'a -> unit) (d : pset<'a>) : unit = PersistentDict.iter (fst >> action) d diff --git a/VSharp.Utils/UnitTest.fs b/VSharp.Utils/UnitTest.fs index 52814a1b6..ed344acbb 100644 --- a/VSharp.Utils/UnitTest.fs +++ b/VSharp.Utils/UnitTest.fs @@ -55,8 +55,14 @@ type UnitTest private (m : MethodBase, info : testInfo) = let classTypeParameters = info.classTypeParameters |> Array.map Serialization.decodeType let methodTypeParameters = info.methodTypeParameters |> Array.map Serialization.decodeType let mutable extraAssemblyLoadDirs : string list = [Directory.GetCurrentDirectory()] + let mutable stateId : string option = None new(m : MethodBase) = UnitTest(m, testInfo.OfMethod m) + + member x.StateId + with get() = stateId + and set id = + stateId <- id member x.Method with get() = m member x.ThisArg diff --git a/VSharp.Utils/VSharp.Utils.fsproj b/VSharp.Utils/VSharp.Utils.fsproj index fb882b1cc..bedbde253 100644 --- a/VSharp.Utils/VSharp.Utils.fsproj +++ b/VSharp.Utils/VSharp.Utils.fsproj @@ -45,6 +45,7 @@ + diff --git a/rd b/rd new file mode 160000 index 000000000..bf4aca09e --- /dev/null +++ b/rd @@ -0,0 +1 @@ +Subproject commit bf4aca09e7e73dc8681067487c1ccb79f715cf10