diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index 33d3a048c..1ff049ad7 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -242,7 +242,7 @@ private static Statistics StartExploration( unitTests.UnitTestsCount, unitTests.ErrorsCount, statistics.StepsCount, - statistics.IncompleteStates.Select(e => e.iie.Value.Message).Distinct(), + statistics.IncompleteStates.Select(s => s.iie.Value.Message).Distinct(), generatedTestInfos); unitTests.WriteReport(statistics.PrintStatistics); diff --git a/VSharp.API/VSharpOptions.cs b/VSharp.API/VSharpOptions.cs index ee7d146a2..60e9af2a2 100644 --- a/VSharp.API/VSharpOptions.cs +++ b/VSharp.API/VSharpOptions.cs @@ -82,34 +82,77 @@ public enum ExplorationMode Interleaving } -/// -/// Symbolic virtual machine options. -/// -/// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption). -/// Timeout for SMT solver in seconds. Negative value means no timeout. -/// Directory to place generated *.vst tests. If null or empty, process working directory is used. -/// Directory to place the project with rendered NUnit tests (if is enabled). If null or empty, parent of process working directory is used. -/// If true, NUnit tests are rendered. -/// Strategy which symbolic virtual machine uses for branch selection. -/// Determines which messages are displayed in output. -/// If greater than zero, terminate exploration of states which have visited the same loop entry or method more times than the value. -/// If true and timeout is specified, a part of allotted time in the end is given to execute remaining states without branching. -/// Fixed seed for random operations. Used if greater than or equal to zero. -/// Number of symbolic machine steps to stop execution after. Zero value means no limit. -public readonly record struct VSharpOptions( - int Timeout = -1, - int SolverTimeout = -1, - string OutputDirectory = "", - string RenderedTestsDirectory = "", - bool RenderTests = false, - SearchStrategy SearchStrategy = SearchStrategy.BFS, - Verbosity Verbosity = Verbosity.Quiet, - uint RecursionThreshold = 0u, - ExplorationMode ExplorationMode = ExplorationMode.Sili, - bool ReleaseBranches = true, - int RandomSeed = -1, - uint StepsLimit = 0) +public readonly record struct VSharpOptions { + private const int DefaultTimeout = -1; + private const int DefaultSolverTimeout = -1; + private const string DefaultOutputDirectory = ""; + private const string DefaultRenderedTestsDirectory = ""; + private const bool DefaultRenderTests = false; + private const SearchStrategy DefaultSearchStrategy = SearchStrategy.BFS; + private const Verbosity DefaultVerbosity = Verbosity.Quiet; + private const uint DefaultRecursionThreshold = 0u; + private const ExplorationMode DefaultExplorationMode = ExplorationMode.Sili; + private const bool DefaultReleaseBranches = true; + private const int DefaultRandomSeed = -1; + private const uint DefaultStepsLimit = 0; + + public readonly int Timeout = DefaultTimeout; + public readonly int SolverTimeout = DefaultSolverTimeout; + public readonly string OutputDirectory = DefaultOutputDirectory; + public readonly string RenderedTestsDirectory = DefaultRenderedTestsDirectory; + public readonly bool RenderTests = DefaultRenderTests; + public readonly SearchStrategy SearchStrategy = DefaultSearchStrategy; + public readonly Verbosity Verbosity = DefaultVerbosity; + public readonly uint RecursionThreshold = DefaultRecursionThreshold; + public readonly ExplorationMode ExplorationMode = DefaultExplorationMode; + public readonly bool ReleaseBranches = DefaultReleaseBranches; + public readonly int RandomSeed = DefaultRandomSeed; + public readonly uint StepsLimit = DefaultStepsLimit; + + /// + /// Symbolic virtual machine options. + /// + /// Timeout for code exploration in seconds. Negative value means infinite timeout (up to exhaustive coverage or user interruption). + /// Timeout for SMT solver in seconds. Negative value means no timeout. + /// Directory to place generated *.vst tests. If null or empty, process working directory is used. + /// Directory to place the project with rendered NUnit tests (if is enabled). If null or empty, parent of process working directory is used. + /// If true, NUnit tests are rendered. + /// Strategy which symbolic virtual machine uses for branch selection. + /// Determines which messages are displayed in output. + /// If greater than zero, terminate exploration of states which have visited the same loop entry or method more times than the value. + /// Determines which mode is used for exploration. + /// If true and timeout is specified, a part of allotted time in the end is given to execute remaining states without branching. + /// Fixed seed for random operations. Used if greater than or equal to zero. + /// Number of symbolic machine steps to stop execution after. Zero value means no limit. + public VSharpOptions( + int timeout = DefaultTimeout, + int solverTimeout = DefaultSolverTimeout, + string outputDirectory = DefaultOutputDirectory, + string renderedTestsDirectory = DefaultRenderedTestsDirectory, + bool renderTests = DefaultRenderTests, + SearchStrategy searchStrategy = DefaultSearchStrategy, + Verbosity verbosity = DefaultVerbosity, + uint recursionThreshold = DefaultRecursionThreshold, + ExplorationMode explorationMode = DefaultExplorationMode, + bool releaseBranches = DefaultReleaseBranches, + int randomSeed = DefaultRandomSeed, + uint stepsLimit = DefaultStepsLimit) + { + Timeout = timeout; + SolverTimeout = solverTimeout; + OutputDirectory = outputDirectory; + RenderedTestsDirectory = renderedTestsDirectory; + RenderTests = renderTests; + SearchStrategy = searchStrategy; + Verbosity = verbosity; + RecursionThreshold = recursionThreshold; + ExplorationMode = explorationMode; + ReleaseBranches = releaseBranches; + RandomSeed = randomSeed; + StepsLimit = stepsLimit; + } + /// /// /// diff --git a/VSharp.CSharpUtils/VSharpAssemblyLoadContext.cs b/VSharp.CSharpUtils/VSharpAssemblyLoadContext.cs index 952b7a3a7..fea3a21ed 100644 --- a/VSharp.CSharpUtils/VSharpAssemblyLoadContext.cs +++ b/VSharp.CSharpUtils/VSharpAssemblyLoadContext.cs @@ -11,6 +11,11 @@ namespace VSharp.CSharpUtils { public class VSharpAssemblyLoadContext : AssemblyLoadContext, IDisposable { + private static string GetTypeName(Type t) + { + return t.AssemblyQualifiedName ?? t.FullName ?? t.Name; + } + private readonly Dictionary _resolvers = new(); private readonly Dictionary _assemblies = new(); @@ -106,7 +111,7 @@ protected override IntPtr LoadUnmanagedDll(string unmanagedDllName) continue; } - _types[type.FullName] = type; + _types[GetTypeName(type)] = type; } return asm; } @@ -140,7 +145,7 @@ public Type NormalizeType(Type t) return normalized.MakeGenericType(fixedGenericTypes); } - var name = t.FullName ?? t.Name; + var name = GetTypeName(t); if (_types.TryGetValue(name, out var normalizedType)) { return normalizedType; diff --git a/VSharp.Explorer/BidirectionalSearcher.fs b/VSharp.Explorer/BidirectionalSearcher.fs index dab23e0e1..72701fde0 100644 --- a/VSharp.Explorer/BidirectionalSearcher.fs +++ b/VSharp.Explorer/BidirectionalSearcher.fs @@ -5,6 +5,7 @@ open FSharpx.Collections open VSharp open VSharp.Interpreter.IL +open CilState type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearcher, targeted : ITargetedSearcher) = @@ -44,7 +45,7 @@ type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearc override x.UpdatePobs parent child = backward.Update parent child override x.UpdateStates parent children = - if not <| CilStateOperations.isIsolated parent then + if not parent.IsIsolated then forward.Update (parent, children) backward.AddBranch parent |> ignore Seq.iter (backward.AddBranch >> ignore) children @@ -128,8 +129,8 @@ type BackwardSearcher() = ancestorOf[child].Add(parent) doAddPob child - let updateQBack s : pob list = - match IpOperations.ip2codeLocation (CilStateOperations.currentIp s) with + let updateQBack (s : cilState) : pob list = + match s.CurrentIp.ToCodeLocation() with | None -> [] | Some loc -> let pobsList = ref null @@ -208,13 +209,12 @@ type BackwardSearcher() = override x.StatesCount with get() = qBack.Count module DummyTargetedSearcher = - open CilStateOperations type DummyTargetedSearcher() = - let forPropagation = Dictionary>() - let finished = Dictionary>() - let reached = Dictionary>() - let targets = Dictionary>() + let forPropagation = Dictionary>() + let finished = Dictionary>() + let reached = Dictionary>() + let targets = Dictionary>() let addReached from s = let mutable l = ref null @@ -226,9 +226,9 @@ module DummyTargetedSearcher = let add (s : cilState) : cilState seq = let from = s.startingIP assert(targets.ContainsKey from) - let current = currentIp s + let current = s.CurrentIp - if isIIEState s || isUnhandledExceptionOrError s || not(isExecutable(s)) then + if s.IsIIEState || s.IsUnhandledExceptionOrError || not s.IsExecutable then finished[from].Add(s); Seq.empty elif targets[from].Contains(current) then addReached from s else @@ -238,7 +238,7 @@ module DummyTargetedSearcher = interface ITargetedSearcher with override x.SetTargets from tos = - if not (targets.ContainsKey from) then targets.Add(from, List()) + if not (targets.ContainsKey from) then targets.Add(from, List()) targets[from].AddRange(tos) override x.Update parent children = diff --git a/VSharp.Explorer/DFSSortedByContributedCoverageSearcher.fs b/VSharp.Explorer/DFSSortedByContributedCoverageSearcher.fs index adbe158d3..0f9a8f51a 100644 --- a/VSharp.Explorer/DFSSortedByContributedCoverageSearcher.fs +++ b/VSharp.Explorer/DFSSortedByContributedCoverageSearcher.fs @@ -3,7 +3,7 @@ namespace VSharp.Explorer open System.Collections.Generic open Microsoft.FSharp.Core open VSharp -open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState open System.Linq /// diff --git a/VSharp.Explorer/DistanceWeighter.fs b/VSharp.Explorer/DistanceWeighter.fs index 3d7d662d8..01dd9c0d8 100644 --- a/VSharp.Explorer/DistanceWeighter.fs +++ b/VSharp.Explorer/DistanceWeighter.fs @@ -4,8 +4,7 @@ open System open VSharp open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations -open VSharp.Interpreter.IL.IpOperations +open VSharp.Interpreter.IL.CilState type ShortestDistanceWeighter(target : codeLocation) = let infinity = UInt32.MaxValue @@ -38,9 +37,9 @@ type ShortestDistanceWeighter(target : codeLocation) = |> Seq.min let calculateCallWeight (state : cilState) = - let suitable ip = - match offsetOf ip with - | Some offset -> Some (forceMethodOf ip, offset) + let suitable (ip : instructionPointer) = + match ip.Offset with + | Some offset -> Some (ip.ForceMethod(), offset) | None -> None let calculateWeight frameNumber (method, offset) = // TODO: do not execute this for frames with frameNumber > current minimum @@ -90,7 +89,7 @@ type ShortestDistanceWeighter(target : codeLocation) = interface IWeighter with override x.Weight(state) = option { - match tryCurrentLoc state with + match state.TryCurrentLoc with | Some currLoc -> let! callWeight = calculateCallWeight state let! weight = @@ -115,8 +114,8 @@ type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SVMStatisti interface IWeighter with override x.Weight(state) = - let calculateWeight ip = - match ip2codeLocation ip, ip with + let calculateWeight (ip : instructionPointer) = + match ip.ToCodeLocation(), ip with | Some loc, _ when loc.method.InCoverageZone -> minDistance loc.method loc.offset |> Some | Some _, _-> None | None, SearchingForHandler(_, _, toObserve, _) -> diff --git a/VSharp.Explorer/ExecutionTreeSearcher.fs b/VSharp.Explorer/ExecutionTreeSearcher.fs index 4536d8082..634ee5b5b 100644 --- a/VSharp.Explorer/ExecutionTreeSearcher.fs +++ b/VSharp.Explorer/ExecutionTreeSearcher.fs @@ -5,6 +5,7 @@ open System.Collections.Generic open VSharp open VSharp.Interpreter.IL +open CilState type internal ExecutionTreeSearcher(randomSeed : int option) = @@ -20,10 +21,10 @@ type internal ExecutionTreeSearcher(randomSeed : int option) = let rec getAllStates() = Seq.collect (fun (t : ExecutionTree) -> t.States) trees.Values - let init initialStates = + let init (initialStates : cilState seq) = if trees.Count > 0 then invalidOp "Trying to init non-empty execution tree searcher" - for method, methodStates in initialStates |> Seq.groupBy CilStateOperations.entryMethodOf do + for method, methodStates in initialStates |> Seq.groupBy (fun s -> s.EntryMethod) do methods.Add method if Seq.length methodStates > 1 then invalidOp "Cannot init execution tree searcher with more than 1 initial state for method" @@ -50,8 +51,8 @@ type internal ExecutionTreeSearcher(randomSeed : int option) = // Fallback (inefficient, in case of plain fair searcher should not happen) getAllStates() |> Seq.tryFind selector - let remove state = - let entryMethod = CilStateOperations.entryMethodOf state + let remove (state : cilState) = + let entryMethod = state.EntryMethod let tree = ref null let treeFound = trees.TryGetValue(entryMethod, tree) if treeFound then @@ -67,8 +68,8 @@ type internal ExecutionTreeSearcher(randomSeed : int option) = trees.Clear() methods.Clear() - let update parent newStates = - let entryMethod = CilStateOperations.entryMethodOf parent + let update (parent : cilState) newStates = + let entryMethod = parent.EntryMethod let tree = ref null let treeFound = trees.TryGetValue(entryMethod, tree) if treeFound then diff --git a/VSharp.Explorer/Explorer.fs b/VSharp.Explorer/Explorer.fs index eb4e31f42..630a95595 100644 --- a/VSharp.Explorer/Explorer.fs +++ b/VSharp.Explorer/Explorer.fs @@ -8,8 +8,8 @@ open FSharpx.Collections open VSharp open VSharp.Core -open VSharp.Interpreter.IL.CilStateOperations open VSharp.Interpreter.IL +open CilState open VSharp.Explorer open VSharp.Solver @@ -116,7 +116,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let reportIncomplete = reporter.ReportIIE - let reportState (suite : testSuite) cilState = + let reportState (suite : testSuite) (cilState : cilState) = try let isNewHistory() = let methodHistory = Set.filter (fun h -> h.method.InCoverageZone) cilState.history @@ -127,14 +127,15 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM | Test -> Set.isEmpty cilState.history || isNewHistory() | Error(msg, isFatal) -> statistics.IsNewError cilState msg isFatal if isNewTest then - let callStackSize = Memory.CallStackSize cilState.state - let entryMethod = entryMethodOf cilState - let hasException = isUnhandledException cilState + let state = cilState.state + let callStackSize = Memory.CallStackSize state + let entryMethod = cilState.EntryMethod + let hasException = cilState.IsUnhandledException if isError && not hasException then if entryMethod.HasParameterOnStack then - Memory.ForcePopFrames (callStackSize - 2) cilState.state - else Memory.ForcePopFrames (callStackSize - 1) cilState.state - match TestGenerator.state2test suite entryMethod cilState.state with + Memory.ForcePopFrames (callStackSize - 2) state + else Memory.ForcePopFrames (callStackSize - 1) state + match TestGenerator.state2test suite entryMethod state with | Some test -> statistics.TrackFinished(cilState, isError) match suite with @@ -144,20 +145,20 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM isStopped <- true | None -> () with :? InsufficientInformationException as e -> - cilState.iie <- Some e + cilState.SetIIE e reportStateIncomplete cilState let reportStateInternalFail (state : cilState) (e : Exception) = match e with | :? InsufficientInformationException as e -> - if state.iie.IsNone then - state.iie <- Some e + if not state.IsIIEState then + state.SetIIE e reportStateIncomplete state | _ -> searcher.Remove state statistics.InternalFails.Add(e) Application.terminateState state - reporter.ReportInternalFail (entryMethodOf state) e + reporter.ReportInternalFail state.EntryMethod e let reportInternalFail (method : Method) (e : Exception) = match e with @@ -169,13 +170,13 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let reportFinished (state : cilState) = let result = Memory.StateResult state.state - Logger.info $"Result of method %s{(entryMethodOf state).FullName} is {result}" + Logger.info $"Result of method {state.EntryMethod.FullName} is {result}" Application.terminateState state reportState Test state let wrapOnError isFatal (state : cilState) errorMessage = if not <| String.IsNullOrWhiteSpace errorMessage then - Logger.info $"Error in {(entryMethodOf state).FullName}: {errorMessage}" + Logger.info $"Error in {state.EntryMethod.FullName}: {errorMessage}" Application.terminateState state let testSuite = Error(errorMessage, isFatal) reportState testSuite state @@ -190,10 +191,11 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM static member private AllocateByRefParameters initialState (method : Method) = let allocateIfByRef (pi : ParameterInfo) = - if pi.ParameterType.IsByRef then + let parameterType = pi.ParameterType + if parameterType.IsByRef then if Memory.CallStackSize initialState = 0 then Memory.NewStackFrame initialState None [] - let typ = pi.ParameterType.GetElementType() + let typ = parameterType.GetElementType() let position = pi.Position + 1 let stackRef = Memory.AllocateTemporaryLocalVariableOfType initialState pi.Name position typ Some stackRef @@ -206,7 +208,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM try initialState.model <- Memory.EmptyModel method let declaringType = method.DeclaringType - let cilState = makeInitialState method initialState + let cilState = cilState.CreateInitial method initialState let this = if method.HasThis then if Types.IsValueType declaringType then @@ -262,7 +264,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let argsForModel = Memory.AllocateVectorArray modelState (MakeNumber 0) typeof Memory.WriteStackLocation modelState (ParameterKey argsParameter) argsForModel Memory.InitializeStaticMembers state method.DeclaringType - let initialState = makeInitialState method state + let initialState = cilState.CreateInitial method state [initialState] with | e -> @@ -270,21 +272,21 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM [] member private x.Forward (s : cilState) = - let loc = s.currentLoc - let ip = currentIp s + let loc = s.approximateLoc + let ip = s.CurrentIp // TODO: update pobs when visiting new methods; use coverageZone let goodStates, iieStates, errors = interpreter.ExecuteOneInstruction s for s in goodStates @ iieStates @ errors do - if hasRuntimeExceptionOrError s |> not then + if not s.HasRuntimeExceptionOrError then statistics.TrackStepForward s ip - let goodStates, toReportFinished = goodStates |> List.partition (fun s -> isExecutable s || isIsolated s) + let goodStates, toReportFinished = goodStates |> List.partition (fun s -> s.IsExecutable || s.IsIsolated) toReportFinished |> List.iter reportFinished - let errors, _ = errors |> List.partition (fun s -> hasReportedError s |> not) - let errors, toReportExceptions = errors |> List.partition (fun s -> isIsolated s || not <| stoppedByException s) - let runtimeExceptions, userExceptions = toReportExceptions |> List.partition hasRuntimeExceptionOrError + let errors, _ = errors |> List.partition (fun s -> not s.HasReportedError) + let errors, toReportExceptions = errors |> List.partition (fun s -> s.IsIsolated || not s.IsStoppedByException) + let runtimeExceptions, userExceptions = toReportExceptions |> List.partition (fun s -> s.HasRuntimeExceptionOrError) runtimeExceptions |> List.iter (fun state -> reportError state null) userExceptions |> List.iter reportFinished - let iieStates, toReportIIE = iieStates |> List.partition isIsolated + let iieStates, toReportIIE = iieStates |> List.partition (fun s -> s.IsIsolated) toReportIIE |> List.iter reportStateIncomplete let mutable sIsStopped = false let newStates = @@ -304,17 +306,17 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM if sIsStopped then searcher.Remove s - member private x.Backward p' s' = - assert(currentLoc s' = p'.loc) - let sLvl = levelToUnsignedInt s'.level + member private x.Backward p' (s' : cilState) = + assert(s'.CurrentLoc = p'.loc) + let sLvl = s'.Level if p'.lvl >= sLvl then let lvl = p'.lvl - sLvl let pc = Memory.WLP s'.state p'.pc match isSat pc with - | true when not <| isIsolated s' -> searcher.Answer p' (Witnessed s') + | true when not s'.IsIsolated -> searcher.Answer p' (Witnessed s') | true -> statistics.TrackStepBackward p' s' - let p = {loc = startingLoc s'; lvl = lvl; pc = pc} + let p = {loc = s'.StartingLoc; lvl = lvl; pc = pc} Logger.trace $"Backward:\nWas: {p'}\nNow: {p}\n\n" Application.addGoal p.loc searcher.UpdatePobs p' p @@ -353,7 +355,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM Application.spawnStates (Seq.cast<_> initialStates) mainPobs |> Seq.map (fun pob -> pob.loc) |> Seq.toArray |> Application.addGoals searcher.Init initialStates mainPobs - initialStates |> Seq.filter isIIEState |> Seq.iter reportStateIncomplete + initialStates |> Seq.filter (fun s -> s.IsIIEState) |> Seq.iter reportStateIncomplete x.BidirectionalSymbolicExecution() searcher.Statuses() |> Seq.iter (fun (pob, status) -> match status with @@ -391,7 +393,7 @@ type private SVMExplorer(explorationOptions: ExplorationOptions, statistics: SVM let entryPointsInitialStates = entryPoints |> List.collect x.FormEntryPointInitialStates let iieStates, initialStates = isolatedInitialStates @ entryPointsInitialStates - |> List.partition (fun state -> state.iie.IsSome) + |> List.partition (fun state -> state.IsIIEState) iieStates |> List.iter reportStateIncomplete statistics.SetStatesGetter(fun () -> searcher.States()) statistics.SetStatesCountGetter(fun () -> searcher.StatesCount) diff --git a/VSharp.Explorer/FairSearcher.fs b/VSharp.Explorer/FairSearcher.fs index a909edb1d..d516202a4 100644 --- a/VSharp.Explorer/FairSearcher.fs +++ b/VSharp.Explorer/FairSearcher.fs @@ -6,6 +6,7 @@ open System.Diagnostics open VSharp open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState /// /// Enumerates initial values as follows: when pick() yielded a value for the first time, it will continue to yield it until timeout, then @@ -106,7 +107,11 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo baseSearcher.Init initialStates // Some states may be filtered out let initialStates = baseSearcher.States() - let groupedByType = initialStates |> Seq.map CilStateOperations.entryMethodOf |> Seq.distinct |> Seq.groupBy (fun m -> m.DeclaringType) + let groupedByType = + initialStates + |> Seq.map (fun s -> s.EntryMethod) + |> Seq.distinct + |> Seq.groupBy (fun m -> m.DeclaringType) typeEnumerator <- FairEnumerator(groupedByType |> Seq.map fst |> Seq.toList, getTypeTimeout, shouldStopType, onTypeRound, onTypeTimeout) for typ, methods in groupedByType do methodEnumerators[typ] <- FairEnumerator( @@ -129,7 +134,7 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo typeEnumerator.DropCurrent() |> ignore pick selector | Some method -> - match baseSearcher.Pick (fun s -> CilStateOperations.entryMethodOf s = method && selector s) with + match baseSearcher.Pick (fun s -> s.EntryMethod = method && selector s) with | None -> elapsedTime <- elapsedTime + methodEnumerators[typ].DropCurrent() pick selector diff --git a/VSharp.Explorer/GuidedSearcher.fs b/VSharp.Explorer/GuidedSearcher.fs index ebd1ef5b7..e81170fb1 100644 --- a/VSharp.Explorer/GuidedSearcher.fs +++ b/VSharp.Explorer/GuidedSearcher.fs @@ -4,6 +4,7 @@ open System.Collections.Generic open VSharp open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState open VSharp.Utils open CilStateOperations @@ -13,12 +14,12 @@ type TargetedSearcher(target) = override x.Insert state = let wasInserted = base.Insert state if not wasInserted then - removeTarget state target |> ignore + state.RemoveTarget target |> ignore wasInserted override x.Update (parent, newStates) = - let needsUpdating state = - let currLoc = tryCurrentLoc state + let needsUpdating (state : cilState) = + let currLoc = state.TryCurrentLoc match currLoc with | Some loc -> let cfg = loc.method.CFG @@ -36,7 +37,7 @@ type TargetedSearcher(target) = for state in Seq.cons parent newStates do match x.TryGetWeight state with | None -> - removeTarget state target |> ignore + state.RemoveTarget target |> ignore | _ -> () wasAnyUpdated @@ -53,16 +54,16 @@ type ITargetManager = type RecursionBasedTargetManager(statistics : SVMStatistics, threshold : uint) = interface ITargetManager with override x.IsStuck state = - match tryCurrentLoc state with + match state.TryCurrentLoc with | Some currLoc -> let cfg = currLoc.method.CFG let onVertex = cfg.IsBasicBlockStart currLoc.offset - let level = if PersistentDict.contains currLoc state.level then state.level.[currLoc] else 0u + let level = state.LevelOfLocation currLoc onVertex && level > threshold | _ -> false override x.CalculateTarget state = - let locStack = state.ipStack |> Seq.choose IpOperations.ip2codeLocation + let locStack = state.ipStack |> Seq.choose (fun ip -> ip.ToCodeLocation()) let inCoverageZone loc = loc.method.InCoverageZone Cps.Seq.foldlk (fun reachingLoc loc k -> match reachingLoc with @@ -86,23 +87,23 @@ type GuidedSearcher(baseSearcher : IForwardSearcher, targetManager : ITargetMana let targetedSearcher = getTargetedSearcher target targetedSearcher.Insert state - let addReturnTarget state = - let startingLoc = startingLoc state + let addReturnTarget (state : cilState) = + let startingLoc = state.StartingLoc let startingMethod = startingLoc.method let cfg = startingMethod.CFG for retOffset in cfg.Sinks do let target = {offset = retOffset.StartOffset; method = startingMethod} - if addTarget state target then + if state.AddTarget target then insertInTargetedSearcher state target |> ignore let deleteTargetedSearcher target = let targetedSearcher = getTargetedSearcher target for state in targetedSearcher.ToSeq() do - removeTarget state target |> ignore + state.RemoveTarget target |> ignore targetedSearchers.Remove target |> ignore - let updateTargetedSearchers parent (newStates : cilState seq) = + let updateTargetedSearchers (parent : cilState) (newStates : cilState seq) = let cilStatesByTarget = Dictionary>() for target in parent.targets do @@ -170,12 +171,12 @@ type GuidedSearcher(baseSearcher : IForwardSearcher, targetManager : ITargetMana if Set.isEmpty state.targets && targetManager.IsStuck state then match targetManager.CalculateTarget state with | Some target -> - addTarget state target |> ignore + state.AddTarget target |> ignore if not <| insertInTargetedSearcher state target then - state.targets <- Set.empty + state.ClearTargets() remove state | None -> - state.targets <- Set.empty + state.ClearTargets() remove state let targetsWithEmptySearchers = targetedSearchers |> Seq.filter (fun (KeyValue(_, s)) -> s.Count = 0u) |> Seq.toList diff --git a/VSharp.Explorer/Searcher.fs b/VSharp.Explorer/Searcher.fs index 9763df311..bda33e6bb 100644 --- a/VSharp.Explorer/Searcher.fs +++ b/VSharp.Explorer/Searcher.fs @@ -4,6 +4,7 @@ open System.Collections.Generic open FSharpx.Collections open VSharp open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState open VSharp.Utils type action = @@ -34,14 +35,14 @@ type IForwardSearcher = abstract member StatesCount : int type ITargetedSearcher = - abstract member SetTargets : ip -> ip seq -> unit + abstract member SetTargets : instructionPointer -> instructionPointer seq -> unit abstract member Update : cilState -> cilState seq -> cilState seq // returns states that reached its target abstract member Pick : unit -> cilState option abstract member Reset : unit -> unit abstract member Remove : cilState -> unit abstract member StatesCount : int -type backwardAction = Propagate of cilState * pob | InitTarget of ip * pob seq | NoAction +type backwardAction = Propagate of cilState * pob | InitTarget of instructionPointer * pob seq | NoAction type IBackwardSearcher = abstract member Init : pob seq -> unit @@ -123,7 +124,7 @@ type WeightedSearcher(weighter : IWeighter, storage : IPriorityCollection - s.iie <- Some e + s.SetIIE e None | :? InternalException as e -> Logger.error $"WeightedSearcher: failed to get weight of state {e}" diff --git a/VSharp.Explorer/Statistics.fs b/VSharp.Explorer/Statistics.fs index 87adbc52b..3eabd6f43 100644 --- a/VSharp.Explorer/Statistics.fs +++ b/VSharp.Explorer/Statistics.fs @@ -15,7 +15,7 @@ open VSharp.Core open VSharp.Interpreter.IL open VSharp.Utils -open CilStateOperations +open CilState open IpOperations open CodeLocation @@ -113,7 +113,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage let printDict' placeHolder (d : Dictionary) sb (m : Method, locs) = let sb = PrettyPrinting.appendLine sb $"%s{placeHolder}Method = %s{m.FullName}: [" let sb = Seq.fold (fun sb (loc : codeLocation) -> - PrettyPrinting.appendLine sb (sprintf "%s\t\t%s <- %d" placeHolder ((int loc.offset).ToString("X")) d.[loc])) sb locs + PrettyPrinting.appendLine sb (sprintf "%s\t\t%s <- %d" placeHolder ((int loc.offset).ToString("X")) d[loc])) sb locs PrettyPrinting.appendLine sb $"%s{placeHolder}]" let printDict placeHolder sb (d : Dictionary) = @@ -158,23 +158,23 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage |> Seq.tryHead |> Option.map (fun offsetDistancePair -> { offset = offsetDistancePair.Key.Offset; method = method }) - member x.TrackStepForward (s : cilState) ip = + member x.TrackStepForward (s : cilState) (ip : instructionPointer) = stepsCount <- stepsCount + 1u - Logger.traceWithTag Logger.stateTraceTag $"{stepsCount} FORWARD: {s.id}" + Logger.traceWithTag Logger.stateTraceTag $"{stepsCount} FORWARD: {s.internalId}" let setCoveredIfNeeded (loc : codeLocation) = if loc.offset = loc.BasicBlock.FinalOffset then - addLocationToHistory s loc + s.AddLocationToHistory loc match s.ipStack with // Successfully exiting method, now its call can be considered covered | Exit _ :: callerIp :: _ -> - match ip2codeLocation callerIp with + match callerIp.ToCodeLocation() with | Some callerLoc -> setCoveredIfNeeded callerLoc | None -> __unreachable__() | _ -> () - let currentLoc = ip2codeLocation ip + let currentLoc = ip.ToCodeLocation() match currentLoc with | Some currentLoc when isHeadOfBasicBlock currentLoc -> let mutable totalRef = ref 0u @@ -227,7 +227,6 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage if visitedBlocksNotCoveredByTests.TryGetValue(s, blocks) then blocks.Value else Set.empty - // TODO: Generalize methods before tracking coverage member x.SetBasicBlocksAsCoveredByTest (blocks : codeLocation seq) = let mutable coveredBlocks = ref null let mutable hasNewCoverage = false @@ -279,7 +278,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage member x.TrackFinished (s : cilState, isError) = testsCount <- testsCount + 1u - x.SetBasicBlocksAsCoveredByTest s.history + x.SetBasicBlocksAsCoveredByTest s.history |> ignore let generatedTestInfo = { isError = isError @@ -288,12 +287,13 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage coverage = x.GetCurrentCoverage() } generatedTestInfos.Add generatedTestInfo - Logger.traceWithTag Logger.stateTraceTag $"FINISH: {s.id}" + Logger.traceWithTag Logger.stateTraceTag $"FINISH: {s.internalId}" member x.IsNewError (s : cilState) (errorMessage : string) isFatal = - match s.state.exceptionsRegister.Peek with + let state = s.state + match state.exceptionsRegister.Peek with | Unhandled(term, _, stackTrace) -> - let exceptionType = MostConcreteTypeOfRef s.state term + let exceptionType = MostConcreteTypeOfRef state term emittedExceptions.Add(exceptionType, stackTrace, errorMessage, isFatal) | _ -> emittedErrors.Add(s.ipStack, errorMessage, isFatal) @@ -303,7 +303,7 @@ type public SVMStatistics(entryMethods : Method seq, generalizeGenericsCoverage member x.TrackFork (parent : cilState) (children : cilState seq) = for child in children do - Logger.traceWithTag Logger.stateTraceTag $"BRANCH: {parent.id} -> {child.id}" + Logger.traceWithTag Logger.stateTraceTag $"BRANCH: {parent.internalId} -> {child.internalId}" let blocks = ref Set.empty // TODO: check why 'parent' may not be in 'visitedBlocksNotCoveredByTests' diff --git a/VSharp.IL/CFG.fs b/VSharp.IL/CFG.fs index 8a506f556..4544422c5 100644 --- a/VSharp.IL/CFG.fs +++ b/VSharp.IL/CFG.fs @@ -435,7 +435,7 @@ and | _ -> false override x.GetHashCode() = (x.offset, x.method).GetHashCode() override x.ToString() = - sprintf "[method = %s\noffset = %s]" x.method.FullName ((int x.offset).ToString("X")) + $"[method = {x.method.FullName}\noffset = {int x.offset : X}]" interface IComparable with override x.CompareTo y = match y with diff --git a/VSharp.IL/Loader.fs b/VSharp.IL/Loader.fs index 37ea93c3f..5a7365c9f 100644 --- a/VSharp.IL/Loader.fs +++ b/VSharp.IL/Loader.fs @@ -344,6 +344,7 @@ module Loader = "System.DateTime System.DateTime.get_Now()" "System.DateTime System.DateTime.get_UtcNow()" "System.DateTime System.Diagnostics.Process.get_StartTime(this)" + "System.String System.DateTime.ToString(this, System.String)" // FileSystem "System.String System.IO.FileSystemInfo.get_LinkTarget(this)" @@ -478,6 +479,10 @@ module Loader = // ResourceManager "System.Void System.Resources.ResourceManager..ctor(this, System.Type)" + // ProfileOptimization + "System.Void System.Runtime.ProfileOptimization.SetProfileRoot(System.String)" + "System.Void System.Runtime.ProfileOptimization.StartProfile(System.String)" + // Unsafe // "T Internal.Runtime.CompilerServices.Unsafe.As(System.Object)" // "T System.Runtime.CompilerServices.Unsafe.As(System.Object)" diff --git a/VSharp.IL/MethodBody.fs b/VSharp.IL/MethodBody.fs index 0037c4264..818728881 100644 --- a/VSharp.IL/MethodBody.fs +++ b/VSharp.IL/MethodBody.fs @@ -139,7 +139,7 @@ type MethodWithBody internal (m : MethodBase) = member x.ReflectedType = m.ReflectedType member x.Parameters = parameters member x.HasParameterOnStack = - x.DeclaringType.IsValueType && not x.IsStatic + x.ReflectedType.IsValueType && not x.IsStatic || x.Parameters |> Array.exists (fun p -> p.ParameterType.IsByRef) member x.LocalVariables = localVariables member x.HasThis = hasThis @@ -246,6 +246,7 @@ type MethodWithBody internal (m : MethodBase) = override x.Parameters = parameters override x.LocalVariables = localVariables override x.HasThis = hasThis + override x.HasParameterOnStack = x.HasParameterOnStack override x.IsConstructor = isConstructor override x.IsExternalMethod with get() = x.IsExternalMethod override x.ContainsGenericParameters with get() = x.ContainsGenericParameters diff --git a/VSharp.InternalCalls/Buffer.fs b/VSharp.InternalCalls/Buffer.fs index 5b521102a..7a91c07d1 100644 --- a/VSharp.InternalCalls/Buffer.fs +++ b/VSharp.InternalCalls/Buffer.fs @@ -4,30 +4,30 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------ System.Buffer -------------------------------- module internal Buffer = - let private getAddress cilState ref = + let private getAddress (cilState : cilState) ref = let state = cilState.state let cases = Memory.TryAddressFromRefFork state ref assert(List.length cases >= 1) let createArrayRef (address, state) = - let cilState = changeState cilState state + let cilState = cilState.ChangeState state match address with | Some address -> Some address, cilState | _ -> let iie = createInsufficientInformation "Memmove: unknown pointer" - cilState.iie <- Some iie + cilState.SetIIE iie None, cilState List.map createArrayRef cases let private Copy dstAddr dstIndex dstIndices dstArrayType srcAddr srcIndex srcIndices srcArrayType state bytesCount = if Memory.IsSafeContextCopy srcArrayType dstArrayType |> not then internalfail $"Buffer.Copy: unsafe memory copy is not implemented, src type {srcArrayType}, dst type {dstArrayType}" - let size = TypeUtils.internalSizeOf (fst3 srcArrayType) + let size = TypeUtils.internalSizeOf srcArrayType.elemType let elemCount = Arithmetics.Div bytesCount (MakeNumber size) let dstType = Types.ArrayTypeToSymbolicType dstArrayType let srcType = Types.ArrayTypeToSymbolicType srcArrayType @@ -50,10 +50,10 @@ module internal Buffer = else let state = cilState.state let bytesCount = Types.Cast bytesCount typeof - let checkDst (info, cilState) = + let checkDst (info, cilState : cilState) = match info with | Some (dstAddress : address) -> - let checkSrc (info, cilState) = + let checkSrc (info, cilState : cilState) = match info with | Some (srcAddress : address) -> let dstType = lazy dstAddress.TypeOfLocation @@ -70,20 +70,20 @@ module internal Buffer = let srcSafe = lazy(MakeNumber srcSize.Value = bytesCount) match dstAddress, srcAddress with | _ when allSafe() -> - let value = read cilState (Ref srcAddress) - let cilStates = write cilState (Ref dstAddress) value + let value = cilState.Read (Ref srcAddress) + let cilStates = cilState.Write (Ref dstAddress) value assert(List.length cilStates = 1) List.head cilStates | _ when dstSafe.Value -> let ptr = Types.Cast (Ref srcAddress) (dstType.Value.MakePointerType()) - let value = read cilState ptr - let cilStates = write cilState (Ref dstAddress) value + let value = cilState.Read ptr + let cilStates = cilState.Write (Ref dstAddress) value assert(List.length cilStates = 1) List.head cilStates | _ when srcSafe.Value -> - let value = read cilState (Ref srcAddress) + let value = cilState.Read (Ref srcAddress) let ptr = Types.Cast (Ref dstAddress) (srcType.Value.MakePointerType()) - let cilStates = write cilState ptr value + let cilStates = cilState.Write ptr value assert(List.length cilStates = 1) List.head cilStates | ArrayIndex(dstAddress, dstIndices, dstArrayType), ArrayIndex(srcAddress, srcIndices, srcArrayType) -> @@ -120,7 +120,7 @@ module internal Buffer = i.NpeOrInvoke cilState dst memMove k let checkSrc cilState k = i.NpeOrInvoke cilState src checkDst k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Arithmetics.LessOrEqual bytesCount dstBytesCount, state)) checkSrc (i.Raise i.ArgumentOutOfRangeException) diff --git a/VSharp.InternalCalls/Buffer.fsi b/VSharp.InternalCalls/Buffer.fsi index 7ea767734..ef970f4ea 100644 --- a/VSharp.InternalCalls/Buffer.fsi +++ b/VSharp.InternalCalls/Buffer.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Buffer = diff --git a/VSharp.InternalCalls/Delegate.fs b/VSharp.InternalCalls/Delegate.fs index ca9dfafc9..898b6f8d2 100644 --- a/VSharp.InternalCalls/Delegate.fs +++ b/VSharp.InternalCalls/Delegate.fs @@ -4,80 +4,80 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal Delegate = - let DelegateCombine (i : IInterpreter) cilState (args : term list) = + let DelegateCombine (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let d1 = args[0] let d2 = args[1] assert(IsReference d1 && IsReference d2) - let combine t cilState k = + let combine t (cilState : cilState) k = let d = Memory.CombineDelegates cilState.state args t - push d cilState + cilState.Push d List.singleton cilState |> k - let typesCheck cilState k = + let typesCheck (cilState : cilState) k = let state = cilState.state let d1Type = MostConcreteTypeOfRef state d1 let d2Type = MostConcreteTypeOfRef state d2 let t = TypeUtils.mostConcreteType d1Type d2Type - let secondCheck cilState k = - StatedConditionalExecutionCIL cilState + let secondCheck (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.RefIsType state d2 t, state)) (combine t) (i.Raise i.ArgumentException) k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.RefIsType state d1 t, state)) secondCheck (i.Raise i.ArgumentException) k - let nullCheck cilState k = - StatedConditionalExecutionCIL cilState + let nullCheck (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference d2, state)) - (fun cilState k -> push d1 cilState; List.singleton cilState |> k) + (fun cilState k -> cilState.Push d1; List.singleton cilState |> k) typesCheck k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference d1, state)) - (fun cilState k -> push d2 cilState; List.singleton cilState |> k) + (fun cilState k -> cilState.Push d2; List.singleton cilState |> k) nullCheck id - let DelegateRemove (i : IInterpreter) cilState (args : term list) = + let DelegateRemove (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let source = args[0] let toRemove = args[1] assert(IsReference source && IsReference toRemove) - let remove t cilState k = + let remove t (cilState : cilState) k = let d = Memory.RemoveDelegate cilState.state source toRemove t - push d cilState + cilState.Push d List.singleton cilState |> k - let typesCheck cilState k = + let typesCheck (cilState : cilState) k = let state = cilState.state let sourceType = MostConcreteTypeOfRef cilState.state source let toRemoveType = MostConcreteTypeOfRef state toRemove let t = TypeUtils.mostConcreteType sourceType toRemoveType - let secondCheck cilState k = - StatedConditionalExecutionCIL cilState + let secondCheck (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.RefIsType state toRemove t, state)) (remove t) (i.Raise i.ArgumentException) k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.RefIsType state source t, state)) secondCheck (i.Raise i.ArgumentException) k - let nullCheck cilState k = - StatedConditionalExecutionCIL cilState + let nullCheck (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference source, state)) - (fun cilState k -> push (TypeOf source |> NullRef) cilState; List.singleton cilState |> k) + (fun cilState k -> cilState.Push (TypeOf source |> NullRef); List.singleton cilState |> k) typesCheck k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference toRemove, state)) - (fun cilState k -> push source cilState; List.singleton cilState |> k) + (fun cilState k -> cilState.Push source; List.singleton cilState |> k) nullCheck id diff --git a/VSharp.InternalCalls/Delegate.fsi b/VSharp.InternalCalls/Delegate.fsi index 574a0587f..e0cd6ad4c 100644 --- a/VSharp.InternalCalls/Delegate.fsi +++ b/VSharp.InternalCalls/Delegate.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Delegate = diff --git a/VSharp.InternalCalls/Diagnostics.fs b/VSharp.InternalCalls/Diagnostics.fs index c382cbc7f..8c2c45e7e 100644 --- a/VSharp.InternalCalls/Diagnostics.fs +++ b/VSharp.InternalCalls/Diagnostics.fs @@ -4,14 +4,14 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal Diagnostics = - let DebugAssert (_ : IInterpreter) cilState (args : term list) = + let DebugAssert (_ : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 1) let condition = List.head args - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (condition, state)) (fun cilState k -> (); k [cilState]) (fun cilState k -> @@ -19,12 +19,12 @@ module internal Diagnostics = k []) id - let Fail (_ : IInterpreter) cilState (args : term list) = + let Fail (_ : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 1) ErrorReporter.ReportFatalError cilState "System.Diagnostics.Debug.Fail called" [cilState] - let FailWithDetailedMessage (_ : IInterpreter) cilState (args : term list) = + let FailWithDetailedMessage (_ : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) ErrorReporter.ReportFatalError cilState "System.Diagnostics.Debug.Fail called" [cilState] diff --git a/VSharp.InternalCalls/Diagnostics.fsi b/VSharp.InternalCalls/Diagnostics.fsi index 61a35a790..c9e0813bf 100644 --- a/VSharp.InternalCalls/Diagnostics.fsi +++ b/VSharp.InternalCalls/Diagnostics.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Diagnostics = diff --git a/VSharp.InternalCalls/HashHelpers.fs b/VSharp.InternalCalls/HashHelpers.fs index f0f98a080..df6725f95 100644 --- a/VSharp.InternalCalls/HashHelpers.fs +++ b/VSharp.InternalCalls/HashHelpers.fs @@ -4,23 +4,23 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal HashHelpers = - let FastMod (i : IInterpreter) cilState (args : term list) = + let FastMod (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 3) let left, right = args[0], args[1] - let validCase cilState k = + let validCase (cilState : cilState) k = let leftType = TypeOf left let rightType = TypeOf right let result = if TypeUtils.isUnsigned leftType || TypeUtils.isUnsigned rightType then Arithmetics.RemUn left right else Arithmetics.Rem left right - push result cilState + cilState.Push result k [cilState] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (right === MakeNumber 0, state)) (i.Raise i.DivideByZeroException) validCase diff --git a/VSharp.InternalCalls/HashHelpers.fsi b/VSharp.InternalCalls/HashHelpers.fsi index d9e45432a..eebb559a1 100644 --- a/VSharp.InternalCalls/HashHelpers.fsi +++ b/VSharp.InternalCalls/HashHelpers.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal HashHelpers = diff --git a/VSharp.InternalCalls/Interlocked.fs b/VSharp.InternalCalls/Interlocked.fs index beeb0f9c5..fd76c946e 100644 --- a/VSharp.InternalCalls/Interlocked.fs +++ b/VSharp.InternalCalls/Interlocked.fs @@ -4,30 +4,30 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal Interlocked = - let exchange (interpreter : IInterpreter) cilState location value = - let exchange cilState k = - let currentValue = read cilState location - let cilStates = write cilState location value + let exchange (interpreter : IInterpreter) (cilState : cilState) location value = + let exchange (cilState : cilState) k = + let currentValue = cilState.Read location + let cilStates = cilState.Write location value for cilState in cilStates do - push currentValue cilState + cilState.Push currentValue k cilStates interpreter.NpeOrInvoke cilState location exchange id - let commonCompareExchange (interpreter : IInterpreter) cilState location value compared = - let compareExchange cilState k = - let currentValue = read cilState location + let commonCompareExchange (interpreter : IInterpreter) (cilState : cilState) location value compared = + let compareExchange (cilState : cilState) k = + let currentValue = cilState.Read location let cilStates = - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun cilState k -> k (currentValue === compared, cilState)) - (fun cilState k -> k (write cilState location value)) + (fun cilState k -> k (cilState.Write location value)) (fun cilState k -> k (List.singleton cilState)) id for cilState in cilStates do - push currentValue cilState + cilState.Push currentValue k cilStates interpreter.NpeOrInvoke cilState location compareExchange id @@ -56,10 +56,10 @@ module internal Interlocked = let location, value = args[0], args[1] exchange interpreter cilState location value - let commonExchangeAdd (interpreter : IInterpreter) cilState (args : term list) = + let commonExchangeAdd (interpreter : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let location, value = args[0], args[1] - let value = Arithmetics.Add (read cilState location) value + let value = Arithmetics.Add (cilState.Read location) value exchange interpreter cilState location value let intExchangeAdd (interpreter : IInterpreter) cilState (args : term list) = diff --git a/VSharp.InternalCalls/Interlocked.fsi b/VSharp.InternalCalls/Interlocked.fsi index 90fd3b5cf..aadba4128 100644 --- a/VSharp.InternalCalls/Interlocked.fsi +++ b/VSharp.InternalCalls/Interlocked.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Interlocked = diff --git a/VSharp.InternalCalls/InteropServices.fs b/VSharp.InternalCalls/InteropServices.fs index 11dd3ddad..857d676e8 100644 --- a/VSharp.InternalCalls/InteropServices.fs +++ b/VSharp.InternalCalls/InteropServices.fs @@ -5,7 +5,7 @@ open System.Runtime.InteropServices open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal InteropServices = @@ -50,7 +50,7 @@ module internal InteropServices = let private isHandleField fieldId = fieldId.name = "_handle" - let private gcHandleType = typeof + let private gcHandleType = typeof let private gcHandleField = lazy( @@ -82,11 +82,11 @@ module internal InteropServices = let obj = args[0] CommonAlloc obj - let GCHandleInternalGet (_ : IInterpreter) cilState args = + let GCHandleInternalGet (_ : IInterpreter) (cilState : cilState) args = assert(List.length args = 1) let ptr = args[0] - let obj = read cilState ptr - push obj cilState + let obj = cilState.Read ptr + cilState.Push obj List.singleton cilState let GCHandleFree (_ : state) (args : term list) = diff --git a/VSharp.InternalCalls/InteropServices.fsi b/VSharp.InternalCalls/InteropServices.fsi index 9ad446f3f..372ff7793 100644 --- a/VSharp.InternalCalls/InteropServices.fsi +++ b/VSharp.InternalCalls/InteropServices.fsi @@ -3,6 +3,7 @@ namespace VSharp.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal InteropServices = diff --git a/VSharp.InternalCalls/Object.fs b/VSharp.InternalCalls/Object.fs index 2cf572b06..bf3a0b419 100644 --- a/VSharp.InternalCalls/Object.fs +++ b/VSharp.InternalCalls/Object.fs @@ -5,7 +5,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState module internal Object = @@ -21,12 +21,12 @@ module internal Object = let zero = MakeNumber 0 let len = Memory.ArrayLengthByDimension state object zero Memory.CopyArray state object zero t newObject zero t len - push newObject cilState + cilState.Push newObject List.singleton cilState elif t.IsValueType then - let v = read cilState object - let ref = Memory.BoxValueType cilState.state v - push ref cilState + let v = cilState.Read object + let ref = Memory.BoxValueType state v + cilState.Push ref List.singleton cilState else let t = @@ -42,11 +42,11 @@ module internal Object = let newObject = Memory.AllocateDefaultClass state t let fields = Reflection.fieldsOf false t let copyField cilStates (field, _) = - let copyForState cilState = - let v = readField cilState object field - writeClassField cilState newObject field v + let copyForState (cilState : cilState) = + let v = cilState.ReadField object field + cilState.WriteClassField newObject field v List.collect copyForState cilStates let cilStates = Array.fold copyField (List.singleton cilState) fields for cilState in cilStates do - push newObject cilState + cilState.Push newObject cilStates diff --git a/VSharp.InternalCalls/Object.fsi b/VSharp.InternalCalls/Object.fsi index 4563c6699..60506c9c5 100644 --- a/VSharp.InternalCalls/Object.fsi +++ b/VSharp.InternalCalls/Object.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Object = diff --git a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs index 42f9574f9..f55c45056 100644 --- a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs +++ b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module Runtime_CompilerServices_RuntimeHelpers = diff --git a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi index b7254b887..711e345ad 100644 --- a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi +++ b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Runtime_CompilerServices_RuntimeHelpers = diff --git a/VSharp.InternalCalls/Span.fs b/VSharp.InternalCalls/Span.fs index aeaface7e..cb5ab5e58 100644 --- a/VSharp.InternalCalls/Span.fs +++ b/VSharp.InternalCalls/Span.fs @@ -6,7 +6,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------ System.ReadOnlySpan -------------------------------- @@ -29,20 +29,20 @@ module internal ReadOnlySpan = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) let lenField = spanFields |> Array.find (fst >> isLengthField) |> fst - readField cilState spanStruct lenField + cilState.ReadField spanStruct lenField let GetContentsRef (cilState : cilState) (spanStruct : term) = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) let ptrField = spanFields |> Array.find (fst >> isContentReferenceField) |> fst - let ptrFieldValue = readField cilState spanStruct ptrField + let ptrFieldValue = cilState.ReadField spanStruct ptrField let ptrFieldType = ptrField.typ if ptrFieldIsByRef ptrFieldType then // Case for .NET 6, where Span contains 'System.ByReference' field let byRefFields = Terms.TypeOf ptrFieldValue |> Reflection.fieldsOf false assert(Array.length byRefFields = 1) let byRefField = byRefFields |> Array.find (fst >> ByReference.isValueField) |> fst - readField cilState ptrFieldValue byRefField + cilState.ReadField ptrFieldValue byRefField else // Case for .NET 7, where Span contains 'Byte&' field ptrFieldValue @@ -59,11 +59,11 @@ module internal ReadOnlySpan = assert(List.length args = 3) let this, wrappedType, index = args[0], args[1], args[2] let t = Helpers.unwrapType wrappedType - let spanStruct = read cilState this + let spanStruct = cilState.Read this let len = GetLength cilState spanStruct let ref = GetContentsRef cilState spanStruct - let checkIndex cilState k = - let readIndex cilState k = + let checkIndex (cilState : cilState) k = + let readIndex (cilState : cilState) k = let ref = match ref.term with | _ when IsArrayContents ref -> @@ -81,9 +81,9 @@ module internal ReadOnlySpan = let offset = Arithmetics.Add offset (Arithmetics.Mul index size) Ptr pointerBase t offset | _ -> internalfail $"GetItemFromReadOnlySpan: unexpected contents ref {ref}" - push ref cilState + cilState.Push ref List.singleton cilState |> k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Arithmetics.Less index len, state)) readIndex (i.Raise i.IndexOutOfRangeException) @@ -98,7 +98,7 @@ module internal ReadOnlySpan = | Some address -> Ref address | None -> ref - let private InitSpanStruct cilState spanStruct refToFirst length = + let private InitSpanStruct (cilState : cilState) spanStruct refToFirst length = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) let refToFirst = PrepareRefField cilState.state refToFirst @@ -111,33 +111,33 @@ module internal ReadOnlySpan = let byRefFields = Reflection.fieldsOf false ptrFieldType assert(Array.length byRefFields = 1) let valueField = byRefFields |> Array.find (fst >> ByReference.isValueField) |> fst - let initializedByRef = writeStructField cilState byRef valueField refToFirst - writeStructField cilState spanStruct ptrField initializedByRef + let initializedByRef = cilState.WriteStructField byRef valueField refToFirst + cilState.WriteStructField spanStruct ptrField initializedByRef else // Case for .NET 7, where Span contains 'Byte&' field - writeStructField cilState spanStruct ptrField refToFirst + cilState.WriteStructField spanStruct ptrField refToFirst let lengthField = spanFields |> Array.find (fst >> isLengthField) |> fst - writeStructField cilState spanWithPtrField lengthField length + cilState.WriteStructField spanWithPtrField lengthField length let private CommonCtor (cilState : cilState) this refToFirst length = - let span = read cilState this + let span = cilState.Read this let initializedSpan = InitSpanStruct cilState span refToFirst length - write cilState this initializedSpan + cilState.Write this initializedSpan let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) : cilState list = assert(List.length args = 4) let this, wrappedType, ptr, size = args[0], args[1], args[2], args[3] let t = Helpers.unwrapType wrappedType - let ctor cilState k = + let ctor (cilState : cilState) k = let state = cilState.state let ptr = - if isStackArray cilState ptr then + if cilState.IsStackArray ptr then // Ptr came from localloc instruction Memory.AllocateVectorArray state size t elif MostConcreteTypeOfRef state ptr = t then ptr else Types.Cast ptr (t.MakePointerType()) CommonCtor cilState this ptr size |> k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Arithmetics.GreaterOrEqual size (MakeNumber 0), state)) ctor (i.Raise i.ArgumentOutOfRangeException) @@ -147,7 +147,7 @@ module internal ReadOnlySpan = assert(List.length args = 3) let this, arrayRef = args[0], args[2] let state = cilState.state - let nullCase cilState k = + let nullCase (cilState : cilState) k = let t = MostConcreteTypeOfRef cilState.state arrayRef let ref = NullRef t CommonCtor cilState this ref (MakeNumber 0) |> k @@ -155,7 +155,7 @@ module internal ReadOnlySpan = let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None let lengthOfArray = Memory.ArrayLengthByDimension state arrayRef (MakeNumber 0) CommonCtor cilState this refToFirstElement lengthOfArray |> k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference arrayRef, state)) nullCase nonNullCase @@ -171,14 +171,14 @@ module internal ReadOnlySpan = let nullCase cilState k = let ref = NullRef typeof let span = InitSpanStruct cilState span ref (MakeNumber 0) - push span cilState + cilState.Push span List.singleton cilState |> k let nonNullCase cilState k = let refToFirst = Memory.ReferenceField state string Reflection.stringFirstCharField let span = InitSpanStruct cilState span refToFirst length - push span cilState + cilState.Push span List.singleton cilState |> k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference string, state)) nullCase nonNullCase diff --git a/VSharp.InternalCalls/Span.fsi b/VSharp.InternalCalls/Span.fsi index 7c58d3b81..fca416c9a 100644 --- a/VSharp.InternalCalls/Span.fsi +++ b/VSharp.InternalCalls/Span.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal ReadOnlySpan = diff --git a/VSharp.InternalCalls/String.fs b/VSharp.InternalCalls/String.fs index ab5158de0..414b2bc0b 100644 --- a/VSharp.InternalCalls/String.fs +++ b/VSharp.InternalCalls/String.fs @@ -6,10 +6,10 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState open VSharp.Core.API.Arithmetics -// ------------------------------- mscorlib.System.Array ------------------------------- +// ------------------------------- System.String ------------------------------- module internal String = @@ -34,7 +34,7 @@ module internal String = let t = MostConcreteTypeOfRef state ref assert(TypeUtils.isArrayType t || t = typeof || t = typeof) let states = Memory.StringCtorOfCharArrayAndLen state ref this len - List.map (changeState cilState) states + List.map cilState.ChangeState states let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 4) @@ -46,27 +46,27 @@ module internal String = let rangeCheck() = (length >>= zero) &&& (startIndex >>= zero) - let copy cilState k = - let cilStates = writeClassField cilState this Reflection.stringLengthField length + let copy (cilState : cilState) k = + let cilStates = cilState.WriteClassField this Reflection.stringLengthField length let bytesCount = Mul length (MakeNumber sizeof) let memMove cilState = Buffer.CommonMemmove cilState this None ptr (Some startIndex) bytesCount List.collect memMove cilStates |> k - let checkPtr cilState k = - StatedConditionalExecutionCIL cilState + let checkPtr (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (!!(IsBadRef ptr), state)) copy (i.Raise i.ArgumentOutOfRangeException) k - let emptyStringCase cilState k = - writeClassField cilState this Reflection.stringLengthField zero |> k - let checkLength cilState k = - StatedConditionalExecutionCIL cilState + let emptyStringCase (cilState : cilState) k = + cilState.WriteClassField this Reflection.stringLengthField zero |> k + let checkLength (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (length === zero, state)) emptyStringCase checkPtr k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (rangeCheck(), state)) checkLength (i.Raise i.ArgumentOutOfRangeException) @@ -147,7 +147,7 @@ module internal String = let copy (cilState : cilState) k = Memory.CopyStringArray cilState.state src srcPos dest destPos srcLength k [cilState] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (check, state)) copy (interpreter.Raise interpreter.IndexOutOfRangeException) @@ -158,9 +158,9 @@ module internal String = let this = args[0] let index = args[1] let length = Memory.StringLength cilState.state this - let getChar cilState k = + let getChar (cilState : cilState) k = let char = Memory.ReadStringChar cilState.state this index - push char cilState + cilState.Push char List.singleton cilState |> k let arrayLength = Add length (MakeNumber 1) interpreter.AccessArray getChar cilState arrayLength index id diff --git a/VSharp.InternalCalls/String.fsi b/VSharp.InternalCalls/String.fsi index d2bb49a72..e339d5b73 100644 --- a/VSharp.InternalCalls/String.fsi +++ b/VSharp.InternalCalls/String.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState // ------------------------------- mscorlib.System.String ------------------------------- diff --git a/VSharp.InternalCalls/SystemArray.fs b/VSharp.InternalCalls/SystemArray.fs index 299a32701..eafd4fae7 100644 --- a/VSharp.InternalCalls/SystemArray.fs +++ b/VSharp.InternalCalls/SystemArray.fs @@ -4,7 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------- mscorlib.System.Array ------------------------------- @@ -31,7 +31,7 @@ module internal SystemArray = let ContainsChar (state : state) args = assert(List.length args = 3) - let this, char = args.[0], args.[2] + let this, char = args[0], args[2] match this.term with | HeapRef({term = ConcreteHeapAddress _}, _) -> let checkOneElement acc i = @@ -54,15 +54,15 @@ module internal SystemArray = let GetItem (state : state) (args : term list) = assert(List.length args = 3) - let this, index = args.[0], args.[2] + let this, index = args[0], args[2] Memory.ReadArrayIndex state this [index] None let GetArrayLength (interpreter : IInterpreter) cilState args = assert(List.length args = 2) let array = args[0] let dim = args[1] - let arrayLengthByDimension arrayRef index cilState k = - push (Memory.ArrayLengthByDimension cilState.state arrayRef index) cilState + let arrayLengthByDimension arrayRef index (cilState : cilState) k = + cilState.Push (Memory.ArrayLengthByDimension cilState.state arrayRef index) k [cilState] interpreter.AccessArrayDimension arrayLengthByDimension cilState array dim @@ -70,8 +70,8 @@ module internal SystemArray = assert(List.length args = 2) let array = args[0] let dim = args[1] - let arrayLowerBoundByDimension arrayRef index cilState k = - push (Memory.ArrayLowerBoundByDimension cilState.state arrayRef index) cilState + let arrayLowerBoundByDimension arrayRef index (cilState : cilState) k = + cilState.Push (Memory.ArrayLowerBoundByDimension cilState.state arrayRef index) k [cilState] interpreter.AccessArrayDimension arrayLowerBoundByDimension cilState array dim @@ -85,7 +85,7 @@ module internal SystemArray = interpreter.NpeOrInvoke cilState array (fun cilState k -> interpreter.NpeOrInvoke cilState handleTerm initArray k) id - let ClearWithIndexLength (interpreter : IInterpreter) cilState args = + let ClearWithIndexLength (interpreter : IInterpreter) (cilState : cilState) args = assert(List.length args = 3) let array, index, length = args[0], args[1], args[2] let (>>) = API.Arithmetics.(>>) @@ -101,18 +101,18 @@ module internal SystemArray = (index << lb) ||| ((Arithmetics.Add index length) >> numOfAllElements) ||| (length << zero) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (check, state)) (interpreter.Raise interpreter.IndexOutOfRangeException) clearCase k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference array, state)) (interpreter.Raise interpreter.ArgumentNullException) nonNullCase id - let ClearWhole (interpreter : IInterpreter) cilState args = + let ClearWhole (interpreter : IInterpreter) (cilState : cilState) args = assert(List.length args = 1) let array = args[0] let clearCase (cilState : cilState) k = @@ -121,7 +121,7 @@ module internal SystemArray = let numOfAllElements = Memory.CountOfArrayElements cilState.state array Memory.ClearArray cilState.state array index numOfAllElements k [cilState] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference array, state)) (interpreter.Raise interpreter.ArgumentNullException) clearCase @@ -151,7 +151,7 @@ module internal SystemArray = let check = (endSrcIndex >> srcNumOfAllElements) ||| (endSrcIndex << srcLB) ||| (endDstIndex >> dstNumOfAllElements) ||| (endDstIndex << dstLB) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (check, state)) (i.Raise i.ArgumentException) defaultCase @@ -161,7 +161,7 @@ module internal SystemArray = let srcIndexCheck = (srcIndex << srcLB) ||| (if TypeUtils.isLong srcIndex then srcIndex >>= srcNumOfAllElements else False()) let dstIndexCheck = (dstIndex << dstLB) ||| (if TypeUtils.isLong dstIndex then dstIndex >>= dstNumOfAllElements else False()) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (primitiveLengthCheck ||| srcIndexCheck ||| dstIndexCheck, state)) (i.Raise i.ArgumentOutOfRangeException) lengthCheck @@ -171,14 +171,14 @@ module internal SystemArray = let condition = if Types.IsValueType srcElemType then True() else Types.TypeIsType srcElemType dstElemType - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (condition, state)) indicesCheck (i.Raise i.InvalidCastException) let rankCheck (cilState : cilState) = if Types.RankOf srcType = Types.RankOf dstType then assignableCheck cilState else i.Raise i.RankException cilState - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference src ||| IsNullReference dst, state)) (i.Raise i.ArgumentNullException) rankCheck @@ -194,7 +194,7 @@ module internal SystemArray = let src, srcIndex, dst, dstIndex, length = args[0], args[1], args[2], args[3], args[4] CommonCopyArray interpreter cilState src srcIndex dst dstIndex length - let CopyArrayShortForm (interpreter : IInterpreter) cilState args = + let CopyArrayShortForm (interpreter : IInterpreter) (cilState : cilState) args = assert(List.length args = 3) let src, dst, length = args[0], args[1], args[2] let state = cilState.state @@ -203,13 +203,13 @@ module internal SystemArray = let dstLB = Memory.ArrayLowerBoundByDimension state dst zero CommonCopyArray interpreter cilState src srcLB dst dstLB length - let FillArray (interpreter : IInterpreter) cilState args = + let FillArray (interpreter : IInterpreter) (cilState : cilState) args = assert(List.length args = 3) let array, value = args[1], args[2] - let fill cilState k = + let fill (cilState : cilState) k = Memory.FillArray cilState.state array value k [cilState] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference array, state)) (interpreter.Raise interpreter.ArgumentNullException) fill diff --git a/VSharp.InternalCalls/SystemArray.fsi b/VSharp.InternalCalls/SystemArray.fsi index 38b80a0f9..455d34d14 100644 --- a/VSharp.InternalCalls/SystemArray.fsi +++ b/VSharp.InternalCalls/SystemArray.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState // ------------------------------- mscorlib.System.Array ------------------------------- diff --git a/VSharp.InternalCalls/Thread.fs b/VSharp.InternalCalls/Thread.fs index 48c6dc946..77f01647a 100644 --- a/VSharp.InternalCalls/Thread.fs +++ b/VSharp.InternalCalls/Thread.fs @@ -3,7 +3,7 @@ namespace VSharp.System open global.System open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------ mscorlib.System.Threading.Thread -------------------------------- @@ -32,9 +32,9 @@ module Thread = let MonitorReliableEnter (interpreter : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let obj, resultRef = args[0], args[1] - let success cilState k = - write cilState resultRef (True()) |> k - BranchOnNullCIL cilState obj + let success (cilState : cilState) k = + cilState.Write resultRef (True()) |> k + cilState.BranchOnNullCIL obj (interpreter.Raise interpreter.ArgumentNullException) success id @@ -42,7 +42,7 @@ module Thread = let MonitorEnter (interpreter : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 1) let obj = List.head args - BranchOnNullCIL cilState obj + cilState.BranchOnNullCIL obj (interpreter.Raise interpreter.ArgumentNullException) (fun cilState k -> List.singleton cilState |> k) id @@ -64,10 +64,10 @@ module Thread = let MonitorWait (interpreter : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 1) let obj = List.head args - let nonNullCase cilState k = - push (MakeBool true) cilState + let nonNullCase (cilState : cilState) k = + cilState.Push (MakeBool true) List.singleton cilState |> k - BranchOnNullCIL cilState obj + cilState.BranchOnNullCIL obj (interpreter.Raise interpreter.ArgumentNullException) nonNullCase id diff --git a/VSharp.InternalCalls/Thread.fsi b/VSharp.InternalCalls/Thread.fsi index 38d4296b4..80849c63c 100644 --- a/VSharp.InternalCalls/Thread.fsi +++ b/VSharp.InternalCalls/Thread.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState // ------------------------------ mscorlib.System.Threading.Thread -------------------------------- diff --git a/VSharp.InternalCalls/Unsafe.fs b/VSharp.InternalCalls/Unsafe.fs index b103d4b4c..ffca3f0bd 100644 --- a/VSharp.InternalCalls/Unsafe.fs +++ b/VSharp.InternalCalls/Unsafe.fs @@ -4,7 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------ System.Unsafe -------------------------------- @@ -80,9 +80,9 @@ module internal Unsafe = let typ, ref = args[0], args[1] let typ = Helpers.unwrapType typ let castedPtr = Types.Cast ref (typ.MakePointerType()) - let readByPtr cilState k = - let value = read cilState castedPtr - push value cilState + let readByPtr (cilState : cilState) k = + let value = cilState.Read castedPtr + cilState.Push value List.singleton cilState |> k i.NpeOrInvoke cilState castedPtr readByPtr id @@ -91,15 +91,15 @@ module internal Unsafe = let typ, ref, value = args[0], args[1], args[2] let typ = Helpers.unwrapType typ let castedPtr = Types.Cast ref (typ.MakePointerType()) - let writeByPtr cilState k = - write cilState castedPtr value |> k + let writeByPtr (cilState : cilState) k = + cilState.Write castedPtr value |> k i.NpeOrInvoke cilState castedPtr writeByPtr id let WriteUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let ref, value = args[0], args[1] - let writeByPtr cilState k = - write cilState ref value |> k + let writeByPtr (cilState : cilState) k = + cilState.Write ref value |> k i.NpeOrInvoke cilState ref writeByPtr id let SizeOf (_ : state) (args : term list) : term = diff --git a/VSharp.InternalCalls/Unsafe.fsi b/VSharp.InternalCalls/Unsafe.fsi index ca272828c..9c08aacea 100644 --- a/VSharp.InternalCalls/Unsafe.fsi +++ b/VSharp.InternalCalls/Unsafe.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState module internal Unsafe = diff --git a/VSharp.InternalCalls/Volatile.fs b/VSharp.InternalCalls/Volatile.fs index 137498473..6b09b02de 100644 --- a/VSharp.InternalCalls/Volatile.fs +++ b/VSharp.InternalCalls/Volatile.fs @@ -4,7 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL -open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Interpreter.IL.CilState // ------------------------------ mscorlib.System.Threading.Volatile -------------------------------- @@ -13,11 +13,11 @@ module Volatile = let Read (_ : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let ref = args[1] - let value = read cilState ref - push value cilState + let value = cilState.Read ref + cilState.Push value List.singleton cilState let Write (_ : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 3) let ref, value = args[1], args[2] - write cilState ref value + cilState.Write ref value diff --git a/VSharp.InternalCalls/Volatile.fsi b/VSharp.InternalCalls/Volatile.fsi index e418529f3..f307952a9 100644 --- a/VSharp.InternalCalls/Volatile.fsi +++ b/VSharp.InternalCalls/Volatile.fsi @@ -4,6 +4,7 @@ open global.System open VSharp open VSharp.Core open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState // ------------------------------ mscorlib.System.Threading.Volatile -------------------------------- diff --git a/VSharp.Runner/RunnerProgram.cs b/VSharp.Runner/RunnerProgram.cs index 2b90235f1..fd6f7a615 100644 --- a/VSharp.Runner/RunnerProgram.cs +++ b/VSharp.Runner/RunnerProgram.cs @@ -161,17 +161,16 @@ public static int Main(string[] args) { var assembly = TryLoadAssembly(assemblyPath); var inputArgs = unknownArgs ? null : args; - var options = new VSharpOptions - { - Timeout = timeout, - SolverTimeout = solverTimeout, - OutputDirectory = output.FullName, - RenderTests = renderTests, - SearchStrategy = strat, - Verbosity = verbosity, - RecursionThreshold = recursionThreshold, - ExplorationMode = explorationMode - }; + var options = + new VSharpOptions( + timeout: timeout, + solverTimeout: solverTimeout, + outputDirectory: output.FullName, + renderTests: renderTests, + searchStrategy: strat, + verbosity: verbosity, + recursionThreshold: recursionThreshold, + explorationMode: explorationMode); if (assembly == null) return; @@ -187,17 +186,16 @@ public static int Main(string[] args) (assemblyPath, timeout, solverTimeout, output, renderTests, runTests, singleFile, strat, verbosity, recursionThreshold, explorationMode) => { var assembly = TryLoadAssembly(assemblyPath); - var options = new VSharpOptions - { - Timeout = timeout, - SolverTimeout = solverTimeout, - OutputDirectory = output.FullName, - RenderTests = renderTests, - SearchStrategy = strat, - Verbosity = verbosity, - RecursionThreshold = recursionThreshold, - ExplorationMode = explorationMode - }; + var options = + new VSharpOptions( + timeout: timeout, + solverTimeout: solverTimeout, + outputDirectory: output.FullName, + renderTests: renderTests, + searchStrategy: strat, + verbosity: verbosity, + recursionThreshold: recursionThreshold, + explorationMode: explorationMode); if (assembly == null) return; @@ -222,17 +220,16 @@ public static int Main(string[] args) return; } - var options = new VSharpOptions - { - Timeout = timeout, - SolverTimeout = solverTimeout, - OutputDirectory = output.FullName, - RenderTests = renderTests, - SearchStrategy = strat, - Verbosity = verbosity, - RecursionThreshold = recursionThreshold, - ExplorationMode = explorationMode - }; + var options = + new VSharpOptions( + timeout: timeout, + solverTimeout: solverTimeout, + outputDirectory: output.FullName, + renderTests: renderTests, + searchStrategy: strat, + verbosity: verbosity, + recursionThreshold: recursionThreshold, + explorationMode: explorationMode); if (runTests) { @@ -271,17 +268,16 @@ public static int Main(string[] args) } } - var options = new VSharpOptions - { - Timeout = timeout, - SolverTimeout = solverTimeout, - OutputDirectory = output.FullName, - RenderTests = renderTests, - SearchStrategy = strat, - Verbosity = verbosity, - RecursionThreshold = recursionThreshold, - ExplorationMode = explorationMode - }; + var options = + new VSharpOptions( + timeout: timeout, + solverTimeout: solverTimeout, + outputDirectory: output.FullName, + renderTests: renderTests, + searchStrategy: strat, + verbosity: verbosity, + recursionThreshold: recursionThreshold, + explorationMode: explorationMode); if (runTests) { @@ -304,17 +300,16 @@ public static int Main(string[] args) return; } - var options = new VSharpOptions - { - Timeout = timeout, - SolverTimeout = solverTimeout, - OutputDirectory = output.FullName, - RenderTests = renderTests, - SearchStrategy = strat, - Verbosity = verbosity, - RecursionThreshold = recursionThreshold, - ExplorationMode = explorationMode - }; + var options = + new VSharpOptions( + timeout: timeout, + solverTimeout: solverTimeout, + outputDirectory: output.FullName, + renderTests: renderTests, + searchStrategy: strat, + verbosity: verbosity, + recursionThreshold: recursionThreshold, + explorationMode: explorationMode); if (runTests) { TestGenerator.CoverAndRun(namespaceTypes, out var statistics, options); diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index a7ae15e99..f4f98c92c 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -351,6 +351,7 @@ module API = let Union oldStack newStack = EvaluationStack.union oldStack newStack let MakeSymbolicActiveFrame f evaluationStack = EvaluationStack.makeSymbolicActiveFrame f evaluationStack let Length evaluationStack = EvaluationStack.length evaluationStack + let FramesCount evaluationStack = EvaluationStack.framesCount evaluationStack let ToList evaluationStack = EvaluationStack.toList evaluationStack let ClearActiveFrame evaluationStack = EvaluationStack.clearActiveFrame evaluationStack let EmptyStack = EvaluationStack.empty @@ -371,30 +372,27 @@ module API = let StringArrayInfo state stringAddress length = Memory.stringArrayInfo state stringAddress length - let IsSafeContextWrite actualType neededType = - Memory.isSafeContextWrite actualType neededType - let rec ReferenceArrayIndex state arrayRef indices (valueType : Type option) = let indices = List.map (fun i -> primitiveCast i typeof) indices match arrayRef.term with | HeapRef(addr, typ) -> let t = Memory.mostConcreteTypeOfHeapRef state addr typ - let addr, (elemType, dim, _ as arrayType) = + let addr, arrayType = if TypeUtils.isArrayType t then addr, symbolicTypeToArrayType t else StringArrayInfo state addr None - assert(dim = List.length indices) + assert(arrayType.dimension = List.length indices) match valueType with - | Some valueType when not (Memory.isSafeContextWrite elemType valueType) -> + | Some valueType when not (Memory.isSafeContextWrite arrayType.elemType valueType) -> Ptr (HeapLocation(addr, typ)) valueType (Memory.arrayIndicesToOffset state addr arrayType indices) | _ -> ArrayIndex(addr, indices, arrayType) |> Ref - | Ref(ArrayIndex(address, innerIndices, (elemType, _, _ as arrayType)) as ref) -> + | Ref(ArrayIndex(address, innerIndices, arrayType) as ref) -> assert(List.length indices = List.length innerIndices) match valueType with | None -> let indices = List.map2 add indices innerIndices ArrayIndex(address, indices, arrayType) |> Ref - | Some typ when Memory.isSafeContextWrite elemType typ -> + | Some typ when Memory.isSafeContextWrite arrayType.elemType typ -> let indices = List.map2 add indices innerIndices ArrayIndex(address, indices, arrayType) |> Ref | Some typ -> @@ -406,7 +404,8 @@ module API = Ptr pointerBase typ offset | Ptr(HeapLocation(address, t) as baseAddress, _, offset) -> assert(TypeUtils.isArrayType t) - let elemType, _, _ as arrayType = symbolicTypeToArrayType t + let arrayType = symbolicTypeToArrayType t + let elemType = arrayType.elemType let sightType, indexOffset = match valueType with | None -> @@ -421,7 +420,7 @@ module API = | Union gvs -> let referenceArrayIndex term = ReferenceArrayIndex state term indices valueType Merging.guardedMap referenceArrayIndex gvs - | _ -> internalfailf "Referencing array index: expected reference, but got %O" arrayRef + | _ -> internalfail $"Referencing array index: expected reference, but got {arrayRef}" let ReferenceField state reference fieldId = Memory.referenceField state reference fieldId @@ -438,8 +437,8 @@ module API = | HeapRef(address, typ) -> let t = MostConcreteTypeOfRef state ref if TypeUtils.isArrayType t then - let _, dim, _ as arrayType = Types.SymbolicTypeToArrayType t - let indices = List.init dim (fun _ -> zero) + let arrayType = Types.SymbolicTypeToArrayType t + let indices = List.init arrayType.dimension (fun _ -> zero) ArrayIndex(address, indices, arrayType) |> Some |> singleton elif t = typeof then let address, arrayType = StringArrayInfo state address None @@ -485,7 +484,7 @@ module API = | Ref _ -> ReferenceField state target field |> Memory.read reporter state | Struct _ -> Memory.readStruct reporter state target field | Combined _ -> Memory.readFieldUnsafe reporter state target field - | _ -> internalfailf "Reading field of %O" term + | _ -> internalfail $"Reading field of {term}" Merging.guardedApply doRead term let ReadField state term field = @@ -517,7 +516,7 @@ module API = | Union gvs -> let readStringChar term = ReadStringChar state term index Merging.guardedMap readStringChar gvs - | _ -> internalfailf "Reading string char: expected reference, but got %O" reference + | _ -> internalfail $"Reading string char: expected reference, but got {reference}" let ReadStaticField state typ field = Memory.readStaticField state typ field let ReadDelegate state reference = Memory.readDelegate state reference @@ -535,8 +534,9 @@ module API = Branching.guardedStatedMap write state reference let WriteUnsafe (reporter : IErrorReporter) state reference value = - reporter.ConfigureState state - let write state reference = Memory.write reporter state reference value + let write state reference = + reporter.ConfigureState state + Memory.write reporter state reference value Branching.guardedStatedMap write state reference let WriteStructField structure field value = Memory.writeStruct structure field value @@ -545,35 +545,33 @@ module API = reporter.ConfigureState state Memory.writeStruct structure field value + let WriteClassFieldUnsafe (reporter : IErrorReporter) state reference field value = + let write state reference = + reporter.ConfigureState state + match reference.term with + | HeapRef(addr, _) -> Memory.writeClassField state addr field value + | _ -> internalfail $"Writing field of class: expected reference, but got {reference}" + state + Branching.guardedStatedMap write state reference + let WriteClassField state reference field value = - Branching.guardedStatedMap - (fun state reference -> - match reference.term with - | HeapRef(addr, _) -> Memory.writeClassField state addr field value - | _ -> internalfailf "Writing field of class: expected reference, but got %O" reference - state) - state reference - - let CommonWriteArrayIndex reporter state reference indices value valueType = + WriteClassFieldUnsafe Memory.emptyReporter state reference field value + + let WriteArrayIndexUnsafe (reporter : IErrorReporter) state reference indices value valueType = + reporter.ConfigureState state let ref = ReferenceArrayIndex state reference indices valueType let value = if isPtr ref then Option.fold (fun _ -> Types.Cast value) value valueType - else MostConcreteTypeOfRef state reference |> symbolicTypeToArrayType |> fst3 |> Types.Cast value + else + let arrayType = MostConcreteTypeOfRef state reference |> symbolicTypeToArrayType + Types.Cast value arrayType.elemType WriteUnsafe reporter state ref value - let WriteArrayIndex state reference indices value valueType = - CommonWriteArrayIndex Memory.emptyReporter state reference indices value valueType - - let WriteArrayIndexUnsafe (reporter : IErrorReporter) state reference indices value valueType = - reporter.ConfigureState state - CommonWriteArrayIndex reporter state reference indices value valueType - let WriteStaticField state typ field value = Memory.writeStaticField state typ field value let DefaultOf typ = makeDefaultValue typ let MakeSymbolicThis m = Memory.makeSymbolicThis m - let MakeSymbolicValue source name typ = Memory.makeSymbolicValue source name typ let CallStackContainsFunction state method = CallStack.containsFunc state.stack method let CallStackSize state = CallStack.size state.stack @@ -669,7 +667,8 @@ module API = let AllocateConcreteObject state (obj : obj) typ = Memory.allocateConcreteObject state obj typ - let LinearizeArrayIndex state address indices (_, dim, _ as arrayType) = + let LinearizeArrayIndex state address indices arrayType = + let dim = arrayType.dimension let lens = List.init dim (fun dim -> Memory.readLength state address (makeNumber dim) arrayType) let lbs = List.init dim (fun dim -> Memory.readLowerBound state address (makeNumber dim) arrayType) Memory.linearizeArrayIndex lens lbs indices @@ -677,13 +676,16 @@ module API = let IsSafeContextCopy (srcArrayType : arrayType) (dstArrayType : arrayType) = Copying.isSafeContextCopy srcArrayType dstArrayType + let IsSafeContextWrite actualType neededType = + Memory.isSafeContextWrite actualType neededType + let CopyArray state src srcIndex srcType dst dstIndex dstType length = match src.term, dst.term with | HeapRef(srcAddress, _), HeapRef(dstAddress, _) -> let srcType = symbolicTypeToArrayType srcType let dstType = symbolicTypeToArrayType dstType Copying.copyArray state srcAddress srcIndex srcType dstAddress dstIndex dstType length - | _ -> internalfailf "Coping arrays: expected heapRefs, but got %O, %O" src dst + | _ -> internalfail $"Coping arrays: expected heapRefs, but got {src}, {dst}" let CopyStringArray state src srcIndex dst dstIndex length = match src.term, dst.term with @@ -692,29 +694,29 @@ module API = assert(Memory.mostConcreteTypeOfHeapRef state dstAddress dstSightType = typeof) let srcAddress, srcType = Memory.stringArrayInfo state srcAddress None let dstAddress, dstType = Memory.stringArrayInfo state dstAddress None - assert(srcType = (typeof, 1, true) && dstType = (typeof, 1, true)) + assert(srcType = arrayType.CharVector && dstType = arrayType.CharVector) Copying.copyArray state srcAddress srcIndex srcType dstAddress dstIndex dstType length - | _ -> internalfailf "Coping arrays: expected heapRefs, but got %O, %O" src dst + | _ -> internalfail $"Coping arrays: expected heapRefs, but got {src}, {dst}" let ClearArray state array index length = match array.term with | HeapRef(address, sightType) -> let arrayType = Memory.mostConcreteTypeOfHeapRef state address sightType |> symbolicTypeToArrayType - let elemType = fst3 arrayType + let elemType = arrayType.elemType let value = makeDefaultValue elemType Copying.fillArray state address arrayType index length value - | _ -> internalfailf "Clearing array: expected heapRef, but got %O" array + | _ -> internalfail $"Clearing array: expected heapRef, but got {array}" let FillArray state array value = match array.term with | HeapRef(address, sightType) -> let arrayType = Memory.mostConcreteTypeOfHeapRef state address sightType |> symbolicTypeToArrayType // Asserting that array is vector (T[]) - assert(thd3 arrayType) + assert arrayType.isVector let zero = makeNumber 0 let length = Memory.readLength state address zero arrayType Copying.fillArray state address arrayType zero length value - | _ -> internalfailf "Filling array: expected heapRef, but got %O" array + | _ -> internalfail $"Filling array: expected heapRef, but got {array}" let StringFromReplicatedChar state string char length = let cm = state.concreteMemory @@ -740,7 +742,7 @@ module API = | HeapRef(address, sightType), _, _ -> assert(Memory.mostConcreteTypeOfHeapRef state address sightType = typeof) symbolicCase address - | _ -> internalfailf "Creating string from replicated char: expected heapRef, but got %O" string + | _ -> internalfail $"Creating string from replicated char: expected heapRef, but got {string}" let IsTypeInitialized state typ = Memory.isTypeInitialized state typ let Dump state = Memory.dump state @@ -752,30 +754,31 @@ module API = match arrayRef.term with | HeapRef(addr, typ) -> Memory.mostConcreteTypeOfHeapRef state addr typ |> TypeUtils.rankOf |> makeNumber | Union gvs -> Merging.guardedMap (ArrayRank state) gvs - | _ -> internalfailf "Getting rank of array: expected ref, but got %O" arrayRef + | _ -> internalfail $"Getting rank of array: expected ref, but got {arrayRef}" + let rec ArrayLengthByDimension state arrayRef index = match arrayRef.term with | HeapRef(addr, typ) -> Memory.mostConcreteTypeOfHeapRef state addr typ |> symbolicTypeToArrayType |> Memory.readLength state addr index | Union gvs -> let arrayLengthByDimension term = ArrayLengthByDimension state term index Merging.guardedMap arrayLengthByDimension gvs - | _ -> internalfailf "reading array length: expected heap reference, but got %O" arrayRef + | _ -> internalfail $"reading array length: expected heap reference, but got {arrayRef}" let rec ArrayLowerBoundByDimension state arrayRef index = match arrayRef.term with | HeapRef(addr, typ) -> Memory.mostConcreteTypeOfHeapRef state addr typ |> symbolicTypeToArrayType |> Memory.readLowerBound state addr index | Union gvs -> let arrayLowerBoundByDimension term = ArrayLowerBoundByDimension state term index Merging.guardedMap arrayLowerBoundByDimension gvs - | _ -> internalfailf "reading array lower bound: expected heap reference, but got %O" arrayRef + | _ -> internalfail $"reading array lower bound: expected heap reference, but got {arrayRef}" let rec CountOfArrayElements state arrayRef = match arrayRef.term with | HeapRef(address, typ) -> - let _, dim, _ as arrayType = Memory.mostConcreteTypeOfHeapRef state address typ |> symbolicTypeToArrayType - let lens = List.init dim (fun dim -> Memory.readLength state address (makeNumber dim) arrayType) + let arrayType = Memory.mostConcreteTypeOfHeapRef state address typ |> symbolicTypeToArrayType + let lens = List.init arrayType.dimension (fun dim -> Memory.readLength state address (makeNumber dim) arrayType) List.fold mul (makeNumber 1) lens | Union gvs -> Merging.guardedMap (CountOfArrayElements state) gvs - | _ -> internalfailf "counting array elements: expected heap reference, but got %O" arrayRef + | _ -> internalfail $"counting array elements: expected heap reference, but got {arrayRef}" let StringLength state strRef = Memory.lengthOfString state strRef @@ -789,8 +792,8 @@ module API = assert(let t = Memory.mostConcreteTypeOfHeapRef state arrayAddr typ in t = typeof || t = typeof) Copying.copyCharArrayToString state arrayAddr dstAddr (makeNumber 0) length k (Nop(), state) - | Ref(ArrayIndex(arrayAddr, indices, (elemType, dim, isVector))) -> - assert(isVector && dim = 1 && elemType = typeof && List.length indices = 1) + | Ref(ArrayIndex(arrayAddr, indices, arrayType)) -> + assert(arrayType.IsCharVector && List.length indices = 1) let index = indices[0] Copying.copyCharArrayToString state arrayAddr dstAddr index length k (Nop(), state) @@ -814,39 +817,39 @@ module API = let Merge2States (s1 : state) (s2 : state) = Memory.merge2States s1 s2 let Merge2Results (r1, s1 : state) (r2, s2 : state) = Memory.merge2Results (r1, s1) (r2, s2) - let FillClassFieldsRegion state (field : fieldId) value isSuitableKey = + let FillClassFieldsRegion state (field : fieldId) value = let defaultValue = MemoryRegion.empty field.typ - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.classFields <- PersistentDict.update state.classFields field defaultValue fill - let FillStaticsRegion state (field : fieldId) value isSuitableKey = + let FillStaticsRegion state (field : fieldId) value = let defaultValue = MemoryRegion.empty field.typ - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.staticFields <- PersistentDict.update state.staticFields field defaultValue fill - let FillArrayRegion state typ value isSuitableKey = - let defaultValue = fst3 typ |> MemoryRegion.empty - let fill region = MemoryRegion.fillRegion value isSuitableKey region - state.arrays <- PersistentDict.update state.arrays typ defaultValue fill + let FillArrayRegion state arrayType value = + let defaultValue = MemoryRegion.empty arrayType.elemType + let fill region = MemoryRegion.fillRegion value region + state.arrays <- PersistentDict.update state.arrays arrayType defaultValue fill - let FillLengthRegion state typ value isSuitableKey = + let FillLengthRegion state typ value = let defaultValue = MemoryRegion.empty TypeUtils.lengthType - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.lengths <- PersistentDict.update state.lengths typ defaultValue fill - let FillLowerBoundRegion state typ value isSuitableKey = + let FillLowerBoundRegion state typ value = let defaultValue = MemoryRegion.empty TypeUtils.lengthType - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.lowerBounds <- PersistentDict.update state.lowerBounds typ defaultValue fill - let FillStackBufferRegion state key value isSuitableKey = + let FillStackBufferRegion state key value = let defaultValue = MemoryRegion.empty typeof - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.stackBuffers <- PersistentDict.update state.stackBuffers key defaultValue fill - let FillBoxedRegion state typ value isSuitableKey = + let FillBoxedRegion state typ value = let defaultValue = MemoryRegion.empty typ - let fill region = MemoryRegion.fillRegion value isSuitableKey region + let fill region = MemoryRegion.fillRegion value region state.boxedLocations <- PersistentDict.update state.boxedLocations typ defaultValue fill let ObjectToTerm (state : state) (o : obj) (typ : Type) = Memory.objToTerm state typ o @@ -860,11 +863,9 @@ module API = | 1 -> let result = EvaluationStack.Pop state.evaluationStack |> fst let method = GetCurrentExploringFunction state - let hasByRefParameters = method.Parameters |> Array.exists (fun p -> p.ParameterType.IsByRef) - let thisIsValueType = method.HasThis && TypeUtils.isValueType method.ReflectedType - let additionalFrameIsNeeded = hasByRefParameters || thisIsValueType match method with - | _ when callStackSize = 1 || callStackSize = 2 && additionalFrameIsNeeded -> Types.Cast result method.ReturnType + | _ when callStackSize = 1 || callStackSize = 2 && method.HasParameterOnStack -> + Types.Cast result method.ReturnType | _ when state.exceptionsRegister.IsUnhandledError -> Nop() | _ -> internalfailf "Method is not finished! Stack trace = %O" CallStack.stackTraceString state.stack | _ -> internalfail "EvaluationStack size was bigger than 1" diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index b519e6485..3d5504aa3 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -1,6 +1,5 @@ namespace VSharp.Core -open System.Collections.Generic open VSharp open System open System.Reflection @@ -248,6 +247,7 @@ module API = val Union : evaluationStack -> evaluationStack -> evaluationStack val MakeSymbolicActiveFrame : (int -> term -> term) -> evaluationStack -> evaluationStack val Length : evaluationStack -> int + val FramesCount : evaluationStack -> int val ToList : evaluationStack -> term list val ClearActiveFrame : evaluationStack -> evaluationStack val EmptyStack : evaluationStack @@ -295,15 +295,14 @@ module API = val WriteStackLocation : state -> stackKey -> term -> unit val WriteStructField : term -> fieldId -> term -> term val WriteStructFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> term + val WriteClassFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> state list val WriteClassField : state -> term -> fieldId -> term -> state list - val WriteArrayIndex : state -> term -> term list -> term -> Type option -> state list val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> state list val WriteStaticField : state -> Type -> fieldId -> term -> unit val DefaultOf : Type -> term val MakeSymbolicThis : IMethod -> term - val MakeSymbolicValue : ISymbolicConstantSource -> string -> Type -> term val CallStackContainsFunction : state -> IMethod -> bool val CallStackSize : state -> int @@ -334,6 +333,7 @@ module API = val LinearizeArrayIndex : state -> term -> term list -> arrayType -> term val IsSafeContextCopy : arrayType -> arrayType -> bool + val IsSafeContextWrite : Type -> Type -> bool val CopyArray : state -> term -> term -> Type -> term -> term -> Type -> term -> unit val CopyStringArray : state -> term -> term -> term -> term -> term -> unit @@ -366,13 +366,13 @@ module API = val Merge2States : state -> state -> state list val Merge2Results : term * state -> term * state -> (term * state) list - val FillClassFieldsRegion : state -> fieldId -> term -> (IHeapAddressKey -> bool) -> unit - val FillStaticsRegion : state -> fieldId -> term -> (ISymbolicTypeKey -> bool) -> unit - val FillArrayRegion : state -> arrayType -> term -> (IHeapArrayKey -> bool) -> unit - val FillLengthRegion : state -> arrayType -> term -> (IHeapVectorIndexKey -> bool) -> unit - val FillLowerBoundRegion : state -> arrayType -> term -> (IHeapVectorIndexKey -> bool) -> unit - val FillStackBufferRegion : state -> stackKey -> term -> (IStackBufferIndexKey -> bool) -> unit - val FillBoxedRegion : state -> Type -> term -> (IHeapAddressKey -> bool) -> unit + val FillClassFieldsRegion : state -> fieldId -> term -> unit + val FillStaticsRegion : state -> fieldId -> term -> unit + val FillArrayRegion : state -> arrayType -> term -> unit + val FillLengthRegion : state -> arrayType -> term -> unit + val FillLowerBoundRegion : state -> arrayType -> term -> unit + val FillStackBufferRegion : state -> stackKey -> term -> unit + val FillBoxedRegion : state -> Type -> term -> unit val ObjectToTerm : state -> obj -> Type -> term val TryTermToObject : state -> term -> obj option diff --git a/VSharp.SILI.Core/ArrayInitialization.fs b/VSharp.SILI.Core/ArrayInitialization.fs index 138c16cd2..9dbe7d065 100644 --- a/VSharp.SILI.Core/ArrayInitialization.fs +++ b/VSharp.SILI.Core/ArrayInitialization.fs @@ -14,10 +14,10 @@ module internal ArrayInitialization = | 1uy -> True() | _ -> __unreachable__() let private byteTermCreator (rawData : byte []) index = - rawData.[index] |> makeNumber + rawData[index] |> makeNumber let private signedByteTermCreator (rawData : byte []) index = - rawData.[index] |> sbyte |> makeNumber + rawData[index] |> sbyte |> makeNumber let private charTermCreator (rawData : byte []) index = BitConverter.ToChar(rawData, index) |> makeNumber @@ -93,7 +93,7 @@ module internal ArrayInitialization = match arrayRef.term, Memory.tryTermToObj state handleTerm with | HeapRef(address, typ), Some(:? RuntimeFieldHandle as rfh) -> commonInitializeArray state address typ rfh - | _ -> internalfailf "initializeArray: case for (arrayRef = %O), (handleTerm = %O) is not implemented" arrayRef handleTerm + | _ -> internalfailf $"initializeArray: case for (arrayRef = {arrayRef}), (handleTerm = {handleTerm}) is not implemented" let allocateOptimizedArray state (fieldInfo : FieldInfo) = let arrayType = typeof.MakeArrayType() diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index b6818bbea..30100a0e7 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/VSharp.SILI.Core/ConcreteMemory.fs @@ -9,7 +9,7 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = // ----------------------------- Constructor ----------------------------- - new () = + internal new () = let physToVirt = Dictionary() let virtToPhys = Dictionary() ConcreteMemory(physToVirt, virtToPhys) @@ -36,189 +36,187 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = // ------------------------------- Copying ------------------------------- - interface IConcreteMemory with - - override x.Copy() = - let physToVirt' = Dictionary() - let virtToPhys' = Dictionary() - // Need to copy all addresses from physToVirt, because: - // 1. let complex object (A) contains another object (B), - // if object (B) was unmarshalled, physToVirt will contain mapping - // between old object (B) and virtual address of it (addr); - // symbolic memory will contain info of symbolic object (B) by it's address (addr) - // So, reading from object (A) object (B) will result in HeapRef (addr), - // which will be read from symbolic memory - let copier = Utils.Copier() - for KeyValue(phys, virt) in physToVirt do - let phys' = copier.DeepCopy phys - let exists, oldPhys = virtToPhys.TryGetValue(virt) - if exists && oldPhys = phys then - virtToPhys'.Add(virt, phys') - // Empty string is interned - if phys' = {object = String.Empty} then physToVirt'[phys'] <- virt - else physToVirt'.Add(phys', virt) - ConcreteMemory(physToVirt', virtToPhys') + member internal x.Copy() = + let physToVirt' = Dictionary() + let virtToPhys' = Dictionary() + // Need to copy all addresses from physToVirt, because: + // 1. let complex object (A) contains another object (B), + // if object (B) was unmarshalled, physToVirt will contain mapping + // between old object (B) and virtual address of it (addr); + // symbolic memory will contain info of symbolic object (B) by it's address (addr) + // So, reading from object (A) object (B) will result in HeapRef (addr), + // which will be read from symbolic memory + let copier = Utils.Copier() + for KeyValue(phys, virt) in physToVirt do + let phys' = copier.DeepCopy phys + let exists, oldPhys = virtToPhys.TryGetValue(virt) + if exists && oldPhys = phys then + virtToPhys'.Add(virt, phys') + // Empty string is interned + if phys' = {object = String.Empty} then physToVirt'[phys'] <- virt + else physToVirt'.Add(phys', virt) + ConcreteMemory(physToVirt', virtToPhys') // ----------------------------- Primitives ----------------------------- - override x.Contains address = - virtToPhys.ContainsKey address + member public x.Contains address = + virtToPhys.ContainsKey address - override x.VirtToPhys virtAddress = - x.ReadObject virtAddress + member public x.VirtToPhys virtAddress = + x.ReadObject virtAddress - override x.TryVirtToPhys virtAddress = - let exists, result = virtToPhys.TryGetValue(virtAddress) - if exists then Some result.object - else None + member public x.TryVirtToPhys virtAddress = + let exists, result = virtToPhys.TryGetValue(virtAddress) + if exists then Some result.object + else None - override x.PhysToVirt physAddress = - let cm = x :> IConcreteMemory - match cm.TryPhysToVirt physAddress with - | Some address -> address - | None -> internalfail $"PhysToVirt: unable to get virtual address for object {physAddress}" + member internal x.PhysToVirt (physAddress : obj) = + match x.TryPhysToVirt physAddress with + | Some address -> address + | None -> internalfail $"PhysToVirt: unable to get virtual address for object {physAddress}" - override x.TryPhysToVirt (physAddress : obj) = - let result = ref List.empty - if physToVirt.TryGetValue({object = physAddress}, result) then - Some result.Value - else None + member internal x.TryPhysToVirt (physAddress : obj) = + let result = ref List.empty + if physToVirt.TryGetValue({object = physAddress}, result) then + Some result.Value + else None // ----------------------------- Allocation ----------------------------- - override x.Allocate address (obj : obj) = - assert(obj <> null) - assert(virtToPhys.ContainsKey address |> not) - // Suppressing finalize, because 'obj' may implement 'Dispose()' method, which should not be invoked, - // because object may be in incorrect state (statics, for example) - GC.SuppressFinalize(obj) - let physicalAddress = {object = obj} - virtToPhys.Add(address, physicalAddress) - physToVirt[physicalAddress] <- address + member internal x.Allocate address (obj : obj) = + assert(obj <> null) + assert(virtToPhys.ContainsKey address |> not) + // Suppressing finalize, because 'obj' may implement 'Dispose()' method, which should not be invoked, + // because object may be in incorrect state (statics, for example) + GC.SuppressFinalize(obj) + let physicalAddress = {object = obj} + virtToPhys.Add(address, physicalAddress) + // TODO: take type as parameter? + let t = obj.GetType() + physToVirt[physicalAddress] <- address // ------------------------------- Reading ------------------------------- - override x.ReadClassField address (field : fieldId) = - let object = x.ReadObject address - let fieldInfo = Reflection.getFieldInfo field - fieldInfo.GetValue(object) - - // TODO: catch possible exceptions and raise exception register - override x.ReadArrayIndex address (indices : int list) = - match x.ReadObject address with - | :? Array as array -> array.GetValue(Array.ofList indices) - | :? String as string when List.length indices = 1 -> - let index = List.head indices - // Case 'index = string.Length' is needed for unsafe string reading: string contents end with null terminator - // In safe context this case will be filtered out in 'Interpreter', which checks indices before memory access - if index = string.Length then Char.MinValue :> obj - else string[index] :> obj - | obj -> internalfail $"reading array index from concrete memory: expected to read array, but got {obj}" - - override x.GetAllArrayData address = - match x.ReadObject address with - | :? Array as array -> Array.getArrayIndicesWithValues array - | :? String as string -> string.ToCharArray() |> Array.getArrayIndicesWithValues - | obj -> internalfail $"reading array data concrete memory: expected to read array, but got {obj}" - - override x.ReadArrayLowerBound address dimension = - match x.ReadObject address with - | :? Array as array -> array.GetLowerBound(dimension) - | :? String when dimension = 0 -> 0 - | obj -> internalfail $"reading array lower bound from concrete memory: expected to read array, but got {obj}" - - override x.ReadArrayLength address dimension = - match x.ReadObject address with - | :? Array as array -> array.GetLength(dimension) - | :? String as string when dimension = 0 -> (1 + string.Length) :> obj - | obj -> internalfail $"reading array length from concrete memory: expected to read array, but got {obj}" + member internal x.ReadClassField address (field : fieldId) = + let object = x.ReadObject address + let fieldInfo = Reflection.getFieldInfo field + fieldInfo.GetValue(object) + + member internal x.ReadArrayIndex address (indices : int list) = + match x.ReadObject address with + | :? Array as array -> array.GetValue(Array.ofList indices) + | :? String as string when List.length indices = 1 -> + let index = List.head indices + // Case 'index = string.Length' is needed for unsafe string reading: string contents end with null terminator + // In safe context this case will be filtered out in 'Interpreter', which checks indices before memory access + if index = string.Length then Char.MinValue :> obj + else string[index] :> obj + | obj -> internalfail $"reading array index from concrete memory: expected to read array, but got {obj}" + + member internal x.GetAllArrayData address = + match x.ReadObject address with + | :? Array as array -> Array.getArrayIndicesWithValues array + | :? String as string -> string.ToCharArray() |> Array.getArrayIndicesWithValues + | obj -> internalfail $"reading array data concrete memory: expected to read array, but got {obj}" + + member internal x.ReadArrayLowerBound address dimension = + match x.ReadObject address with + | :? Array as array -> array.GetLowerBound(dimension) + | :? String when dimension = 0 -> 0 + | obj -> internalfail $"reading array lower bound from concrete memory: expected to read array, but got {obj}" + + member internal x.ReadArrayLength address dimension = + match x.ReadObject address with + | :? Array as array -> array.GetLength(dimension) + | :? String as string when dimension = 0 -> 1 + string.Length + | obj -> internalfail $"reading array length from concrete memory: expected to read array, but got {obj}" // ------------------------------- Writing ------------------------------- - override x.WriteClassField address (field : fieldId) value = - let object = x.ReadObject address - let fieldInfo = Reflection.getFieldInfo field - let fieldType = fieldInfo.FieldType - let value = x.CastIfNeed value fieldType - fieldInfo.SetValue(object, value) - - override x.WriteArrayIndex address (indices : int list) value = - match x.ReadObject address with - | :? Array as array -> - let elemType = array.GetType().GetElementType() - let castedValue = - if value <> null then x.CastIfNeed value elemType - else value - array.SetValue(castedValue, Array.ofList indices) - // TODO: strings must be immutable! This is used by copying, so copy string another way #hack - | :? String as string when List.length indices = 1 -> - let charArray = string.ToCharArray() - assert(value <> null) - let castedValue = x.CastIfNeed value typeof - charArray.SetValue(castedValue, List.head indices) - let newString = String(charArray) - x.WriteObject address newString - | obj -> internalfail $"writing array index to concrete memory: expected to read array, but got {obj}" - - override x.InitializeArray address (rfh : RuntimeFieldHandle) = - match x.ReadObject address with - | :? Array as array -> RuntimeHelpers.InitializeArray(array, rfh) - | obj -> internalfail $"initializing array in concrete memory: expected to read array, but got {obj}" - - override x.FillArray address index length value = - match x.ReadObject address with - | :? Array as array when array.Rank = 1 -> - for i = index to index + length - 1 do - array.SetValue(value, i) - | :? Array -> internalfail "filling array in concrete memory: multidimensional arrays are not supported yet" - | obj -> internalfail $"filling array in concrete memory: expected to read array, but got {obj}" - - override x.CopyArray srcAddress dstAddress srcIndex dstIndex length = - match x.ReadObject srcAddress, x.ReadObject dstAddress with - | :? Array as srcArray, (:? Array as dstArray) -> - Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) - | :? String as srcString, (:? String as dstString) -> - let srcArray = srcString.ToCharArray() - let dstArray = dstString.ToCharArray() - Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) - let newString = String(dstArray) - x.WriteObject dstAddress newString - | :? String as srcString, (:? Array as dstArray) -> - let srcArray = srcString.ToCharArray() - Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) - | :? Array as srcArray, (:? String as dstString) -> - let dstArray = dstString.ToCharArray() - Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) - let newString = String(dstArray) - x.WriteObject dstAddress newString - | obj -> internalfail $"copying array in concrete memory: expected to read array, but got {obj}" - - override x.CopyCharArrayToString arrayAddress stringAddress startIndex = - let array = - match x.ReadObject arrayAddress with - | :? array as array -> array - | :? string as str -> str.ToCharArray() - | obj -> internalfail $"CopyCharArrayToString: unexpected array {obj}" - let string = new string(array[startIndex..]) :> obj - x.WriteObject stringAddress string - let physAddress = {object = string} - physToVirt[physAddress] <- stringAddress - - override x.CopyCharArrayToStringLen arrayAddress stringAddress startIndex length = - let array = - match x.ReadObject arrayAddress with - | :? array as array -> array - | :? string as str -> str.ToCharArray() - | obj -> internalfail $"CopyCharArrayToStringLen: unexpected array {obj}" - let string = new string(array[startIndex..(length - 1)]) :> obj - x.WriteObject stringAddress string - let physAddress = {object = string} - physToVirt[physAddress] <- stringAddress + member internal x.WriteClassField address (field : fieldId) (value : obj) = + let object = x.ReadObject address + let fieldInfo = Reflection.getFieldInfo field + let fieldType = fieldInfo.FieldType + let value = x.CastIfNeed value fieldType + fieldInfo.SetValue(object, value) + + member internal x.WriteArrayIndex address (indices : int list) value = + match x.ReadObject address with + | :? Array as array -> + let elemType = array.GetType().GetElementType() + let castedValue = + if value <> null then x.CastIfNeed value elemType + else value + array.SetValue(castedValue, Array.ofList indices) + // TODO: strings must be immutable! This is used by copying, so copy string another way #hack + | :? String as string when List.length indices = 1 -> + let charArray = string.ToCharArray() + assert(value <> null) + let castedValue = x.CastIfNeed value typeof + charArray.SetValue(castedValue, List.head indices) + let newString = String(charArray) + x.WriteObject address newString + | obj -> internalfail $"writing array index to concrete memory: expected to read array, but got {obj}" + + member internal x.InitializeArray address (rfh : RuntimeFieldHandle) = + match x.ReadObject address with + | :? Array as array -> RuntimeHelpers.InitializeArray(array, rfh) + | obj -> internalfail $"initializing array in concrete memory: expected to read array, but got {obj}" + + member internal x.FillArray address index length (value : obj) = + match x.ReadObject address with + | :? Array as array when array.Rank = 1 -> + for i = index to index + length - 1 do + array.SetValue(value, i) + | :? Array -> internalfail "filling array in concrete memory: multidimensional arrays are not supported yet" + | obj -> internalfail $"filling array in concrete memory: expected to read array, but got {obj}" + + member internal x.CopyArray srcAddress dstAddress (srcIndex : int64) (dstIndex : int64) length = + match x.ReadObject srcAddress, x.ReadObject dstAddress with + | :? Array as srcArray, (:? Array as dstArray) -> + Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) + | :? String as srcString, (:? String as dstString) -> + let srcArray = srcString.ToCharArray() + let dstArray = dstString.ToCharArray() + Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) + let newString = String(dstArray) + x.WriteObject dstAddress newString + | :? String as srcString, (:? Array as dstArray) -> + let srcArray = srcString.ToCharArray() + Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) + | :? Array as srcArray, (:? String as dstString) -> + let dstArray = dstString.ToCharArray() + Array.Copy(srcArray, srcIndex, dstArray, dstIndex, length) + let newString = String(dstArray) + x.WriteObject dstAddress newString + | obj -> internalfail $"copying array in concrete memory: expected to read array, but got {obj}" + + member internal x.CopyCharArrayToString arrayAddress stringAddress startIndex = + let array = + match x.ReadObject arrayAddress with + | :? array as array -> array + | :? string as str -> str.ToCharArray() + | obj -> internalfail $"CopyCharArrayToString: unexpected array {obj}" + let string = new string(array[startIndex..]) :> obj + x.WriteObject stringAddress string + let physAddress = {object = string} + physToVirt[physAddress] <- stringAddress + + member internal x.CopyCharArrayToStringLen arrayAddress stringAddress startIndex length = + let array = + match x.ReadObject arrayAddress with + | :? array as array -> array + | :? string as str -> str.ToCharArray() + | obj -> internalfail $"CopyCharArrayToStringLen: unexpected array {obj}" + let string = new string(array[startIndex..(length - 1)]) :> obj + x.WriteObject stringAddress string + let physAddress = {object = string} + physToVirt[physAddress] <- stringAddress // ------------------------------- Remove ------------------------------- - override x.Remove address = - // No need to remove physical addresses from physToVirt, because - // all objects must contain virtual address, even if they were unmarshalled - let removed = virtToPhys.Remove address - assert removed + member internal x.Remove address = + // No need to remove physical addresses from physToVirt, because + // all objects must contain virtual address, even if they were unmarshalled + let removed = virtToPhys.Remove address + assert removed diff --git a/VSharp.SILI.Core/ConcreteMemory.fsi b/VSharp.SILI.Core/ConcreteMemory.fsi new file mode 100644 index 000000000..96dff007f --- /dev/null +++ b/VSharp.SILI.Core/ConcreteMemory.fsi @@ -0,0 +1,27 @@ +namespace VSharp.Core + +open System +open VSharp + +type public ConcreteMemory = + internal new : unit -> ConcreteMemory + member internal Copy : unit -> ConcreteMemory + member public Contains : concreteHeapAddress -> bool + member public VirtToPhys : concreteHeapAddress -> obj + member public TryVirtToPhys : concreteHeapAddress -> obj option + member internal PhysToVirt : obj -> concreteHeapAddress + member internal TryPhysToVirt : obj -> concreteHeapAddress option + member internal Allocate : concreteHeapAddress -> obj -> unit + member internal ReadClassField : concreteHeapAddress -> fieldId -> obj + member internal ReadArrayIndex : concreteHeapAddress -> int list -> obj + member internal GetAllArrayData : concreteHeapAddress -> seq + member internal ReadArrayLowerBound : concreteHeapAddress -> int -> int + member internal ReadArrayLength : concreteHeapAddress -> int -> int + member internal WriteClassField : concreteHeapAddress -> fieldId -> obj -> unit + member internal WriteArrayIndex : concreteHeapAddress -> int list -> obj -> unit + member internal InitializeArray : concreteHeapAddress -> RuntimeFieldHandle -> unit + member internal FillArray : concreteHeapAddress -> int -> int -> obj -> unit + member internal CopyArray : concreteHeapAddress -> concreteHeapAddress -> int64 -> int64 -> int64 -> unit + member internal CopyCharArrayToString : concreteHeapAddress -> concreteHeapAddress -> int -> unit + member internal CopyCharArrayToStringLen : concreteHeapAddress -> concreteHeapAddress -> int -> int -> unit + member internal Remove : concreteHeapAddress -> unit diff --git a/VSharp.SILI.Core/Copying.fs b/VSharp.SILI.Core/Copying.fs index 24ed6c4c9..58393fe54 100644 --- a/VSharp.SILI.Core/Copying.fs +++ b/VSharp.SILI.Core/Copying.fs @@ -7,7 +7,7 @@ open VSharp.Core module internal Copying = let private copyArrayConcrete state srcAddress srcIndex srcType srcLens srcLBs dstAddress dstIndex dstType dstLens dstLBs length = - let dstElemType = fst3 dstType + let dstElemType = dstType.elemType let offsets = List.init length id let copyOneElem offset = let srcIndex = add srcIndex (makeNumber offset) @@ -25,7 +25,7 @@ module internal Copying = List.iter writeCopied toWrite let private copyArraySymbolic state srcAddress srcIndex srcType srcLens srcLBs dstAddress dstIndex dstType dstLens dstLBs length = - let dstElemType = fst3 dstType + let dstElemType = dstType.elemType let srcFromIndices = delinearizeArrayIndex srcIndex srcLens srcLBs let lenMinOne = sub length (makeNumber 1) let srcToIndices = delinearizeArrayIndex (add srcIndex lenMinOne) srcLens srcLBs @@ -35,8 +35,9 @@ module internal Copying = let dstToIndices = delinearizeArrayIndex (add dstIndex lenMinOne) dstLens dstLBs writeArrayRange state dstAddress dstFromIndices dstToIndices dstType casted - let private copyArrayCommon state srcAddress srcIndex (_, srcDim, _ as srcType) dstAddress dstIndex dstType length = - let dstDim = snd3 dstType + let private copyArrayCommon state srcAddress srcIndex srcType dstAddress dstIndex dstType length = + let srcDim = srcType.dimension + let dstDim = dstType.dimension let srcLBs = List.init srcDim (fun dim -> readLowerBound state srcAddress (makeNumber dim) srcType) let srcLens = List.init srcDim (fun dim -> readLength state srcAddress (makeNumber dim) srcType) let dstLBs = List.init dstDim (fun dim -> readLowerBound state dstAddress (makeNumber dim) dstType) @@ -49,9 +50,7 @@ module internal Copying = copyArraySymbolic state srcAddress srcIndex srcType srcLens srcLBs dstAddress dstIndex dstType dstLens dstLBs length let isSafeContextCopy srcArrayType dstArrayType = - let srcElemType = fst3 srcArrayType - let dstElemType = fst3 dstArrayType - isSafeContextWrite srcElemType dstElemType + isSafeContextWrite srcArrayType.elemType dstArrayType.elemType let copyArray state srcAddress srcIndex srcType dstAddress dstIndex dstType length = assert(isSafeContextCopy srcType dstType) @@ -103,7 +102,7 @@ module internal Copying = | _, _, None -> if cm.Contains stringConcreteAddress then cm.Remove stringConcreteAddress - let arrayType = (typeof, 1, true) + let arrayType = arrayType.CharVector let length = readLength state arrayAddress (makeNumber 0) arrayType copyCharArrayToStringSymbolic state arrayAddress stringConcreteAddress startIndex length @@ -121,8 +120,9 @@ module internal Copying = let upperBounds = delinearizeArrayIndex lastIndex lens lbs writeArrayRange state arrayAddress lowerBounds upperBounds arrayType castedValue - let private fillArrayCommon state arrayAddress (elemType, dim, _ as arrayType) index length value = - let castedValue = TypeCasting.cast value elemType + let private fillArrayCommon state arrayAddress arrayType index length value = + let dim = arrayType.dimension + let castedValue = TypeCasting.cast value arrayType.elemType let lbs = List.init dim (fun dim -> readLowerBound state arrayAddress (makeNumber dim) arrayType) let lens = List.init dim (fun dim -> readLength state arrayAddress (makeNumber dim) arrayType) match length.term with @@ -131,11 +131,11 @@ module internal Copying = fillArrayConcrete state arrayAddress arrayType index length lbs lens castedValue | _ -> fillArraySymbolic state arrayAddress arrayType index length lbs lens castedValue - let fillArray state arrayAddress (elemType, _, _ as arrayType) index length value = + let fillArray state arrayAddress arrayType index length value = let cm = state.concreteMemory let concreteIndex = tryTermToObj state index let concreteLength = tryTermToObj state length - let castedValue = TypeCasting.cast value elemType + let castedValue = TypeCasting.cast value arrayType.elemType let concreteValue = tryTermToObj state castedValue match arrayAddress.term, concreteIndex, concreteLength, concreteValue with | ConcreteHeapAddress address, Some i, Some l, Some v when cm.Contains address -> diff --git a/VSharp.SILI.Core/EvaluationStack.fs b/VSharp.SILI.Core/EvaluationStack.fs index 7ad44ac0b..f1260f729 100644 --- a/VSharp.SILI.Core/EvaluationStack.fs +++ b/VSharp.SILI.Core/EvaluationStack.fs @@ -31,15 +31,18 @@ module internal EvaluationStack = match evaluationStack.contents with | l :: ls -> {contents = (List.mapi f l) :: ls} | [] -> __corruptedStack__() + let clearActiveFrame evaluationStack = match evaluationStack.contents with | _ :: ls -> {contents = [] :: ls} | _ -> __corruptedStack__() + let newStackFrame evaluationStack = {contents = [] :: evaluationStack.contents} + let popStackFrame evaluationStack = match evaluationStack.contents with | [] :: ls -> {contents = ls} - | [_] :: [] -> evaluationStack // res case + | [ [_] ] -> evaluationStack // res case | [res] :: l :: ls -> {contents = (res :: l) :: ls} // call case | _ -> __corruptedStack__() @@ -60,6 +63,8 @@ module internal EvaluationStack = let length evaluationStack = List.fold (fun acc l -> List.length l + acc) 0 evaluationStack.contents + let framesCount evaluationStack = List.length evaluationStack.contents + let popMany n evaluationStack = match evaluationStack.contents with | l :: ls -> diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 499a24d34..b05493cb1 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -164,8 +164,8 @@ module internal Memory = if t = t' then typ else t'.MakeByRefType() | _ -> __unreachable__() - let private substituteTypeVariablesIntoArrayType state ((et, i, b) : arrayType) : arrayType = - (substituteTypeVariables state et, i, b) + let private substituteTypeVariablesIntoArrayType state ({elemType = et} as arrayType) : arrayType = + { arrayType with elemType = substituteTypeVariables state et } let typeVariableSubst state (t : Type) = commonTypeVariableSubst state t t @@ -192,8 +192,13 @@ module internal Memory = if isAssignable locationType sightType then locationType else if isAssignable sightType locationType |> not then - Logger.trace "mostConcreteTypeOfHeapRef: Sight type (%O) of address %O differs from type in heap (%O)" sightType address locationType - sightType + if locationType = typeof && sightType = typeof || locationType = typeof && sightType = typeof then + typeof + else + Logger.trace $"mostConcreteTypeOfHeapRef: Sight type ({sightType}) of address {address} differs from type in heap ({locationType})" + sightType + else + sightType let mostConcreteTypeOfRef state ref = let getType ref = @@ -201,7 +206,7 @@ module internal Memory = | HeapRef(address, sightType) -> mostConcreteTypeOfHeapRef state address sightType | Ref address -> address.TypeOfLocation | Ptr(_, t, _) -> t - | _ -> internalfailf "reading type token: expected heap reference, but got %O" ref + | _ -> internalfail $"reading type token: expected heap reference, but got {ref}" commonTypeOf getType ref let baseTypeOfAddress state address = @@ -694,7 +699,7 @@ module internal Memory = let private readLowerBoundSymbolic (state : state) address dimension arrayType = let extractor (state : state) = accessRegion state.lowerBounds (substituteTypeVariablesIntoArrayType state arrayType) lengthType let mkName (key : heapVectorIndexKey) = $"LowerBound({key.address}, {key.index})" - let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address || thd3 arrayType + let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address || arrayType.isVector let key = {address = address; index = dimension} let inst typ memoryRegion = let sort = ArrayLowerBoundSort arrayType @@ -753,7 +758,7 @@ module internal Memory = let private readArrayKeySymbolic state key arrayType = let extractor state = let arrayType = substituteTypeVariablesIntoArrayType state arrayType - accessRegion state.arrays arrayType (fst3 arrayType) + accessRegion state.arrays arrayType arrayType.elemType readArrayRegion state arrayType extractor (extractor state) false key let private readArrayIndexSymbolic state address indices arrayType = @@ -783,7 +788,7 @@ module internal Memory = let address = ConcreteHeapAddress concreteAddress let fromIndices = List.map (fun i -> primitiveCast i typeof) fromIndices let toIndices = List.map (fun i -> primitiveCast i typeof) toIndices - let region = arrayRegionFromData state concreteAddress arrayData (fst3 arrayType) + let region = arrayRegionFromData state concreteAddress arrayData arrayType.elemType let key = RangeArrayIndexKey(address, fromIndices, toIndices) readArrayRegion state arrayType (always region) region true key @@ -797,7 +802,7 @@ module internal Memory = let private readSymbolicIndexFromConcreteArray state concreteAddress arrayData indices arrayType = let address = ConcreteHeapAddress concreteAddress - let region = arrayRegionFromData state concreteAddress arrayData (fst3 arrayType) + let region = arrayRegionFromData state concreteAddress arrayData arrayType.elemType let indices = List.map (fun i -> primitiveCast i typeof) indices let key = OneArrayIndexKey(address, indices) readArrayRegion state arrayType (always region) region true key @@ -807,10 +812,11 @@ module internal Memory = let concreteIndices = tryIntListFromTermList indices match address.term, concreteIndices with | ConcreteHeapAddress address, Some concreteIndices when cm.Contains address -> - cm.ReadArrayIndex address concreteIndices |> objToTerm state (fst3 arrayType) + cm.ReadArrayIndex address concreteIndices |> objToTerm state arrayType.elemType | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress -> let data = cm.GetAllArrayData concreteAddress readSymbolicIndexFromConcreteArray state concreteAddress data indices arrayType + // TODO: remember all concrete data from 'ConcreteMemory' and add it to symbolic constant [Test: ConcreteDictionaryTest1] | _ -> readArrayIndexSymbolic state address indices arrayType // ------------------------------- Array writing ------------------------------- @@ -819,21 +825,21 @@ module internal Memory = if isOpenType typ then __insufficientInformation__ $"Cannot write value of generic type {typ}" let private writeLowerBoundSymbolic (state : state) address dimension arrayType value = - ensureConcreteType (fst3 arrayType) + ensureConcreteType arrayType.elemType let mr = accessRegion state.lowerBounds arrayType lengthType let key = {address = address; index = dimension} let mr' = MemoryRegion.write mr key value state.lowerBounds <- PersistentDict.add arrayType mr' state.lowerBounds let writeLengthSymbolic (state : state) address dimension arrayType value = - ensureConcreteType (fst3 arrayType) + ensureConcreteType arrayType.elemType let mr = accessRegion state.lengths arrayType lengthType let key = {address = address; index = dimension} let mr' = MemoryRegion.write mr key value state.lengths <- PersistentDict.add arrayType mr' state.lengths let private writeArrayKeySymbolic state key arrayType value = - let elementType = fst3 arrayType + let elementType = arrayType.elemType ensureConcreteType elementType let mr = accessRegion state.arrays arrayType elementType let mr' = MemoryRegion.write mr key value @@ -871,7 +877,7 @@ module internal Memory = MemoryRegion.read region key (isDefault state) instantiate let stringArrayInfo state stringAddress length = - let arrayType = typeof, 1, true + let arrayType = arrayType.CharVector if PersistentSet.contains stringAddress state.initializedAddresses then stringAddress, arrayType else @@ -904,6 +910,7 @@ module internal Memory = match address.term with | ConcreteHeapAddress address when cm.Contains address -> cm.ReadClassField address field |> objToTerm state field.typ + // TODO: remember all concrete field values from 'ConcreteMemory' and add it to symbolic constant [Test: ConcreteDictionaryTest1] | _ -> readClassFieldSymbolic state address field let readStaticField state typ (field : fieldId) = @@ -1117,13 +1124,13 @@ module internal Memory = let readField fieldId = readClassField state address fieldId readFieldsUnsafe reporter readField false classType offset endByte sightType - and arrayIndicesToOffset state address (elementType, dim, _ as arrayType) indices = + and arrayIndicesToOffset state address ({elemType = elementType; dimension = dim} as arrayType) indices = let lens = List.init dim (fun dim -> readLength state address (makeNumber dim) arrayType) let lbs = List.init dim (fun dim -> readLowerBound state address (makeNumber dim) arrayType) let linearIndex = linearizeArrayIndex lens lbs indices mul linearIndex (internalSizeOf elementType |> makeNumber) - and private getAffectedIndices reporter state address (elementType, dim, _ as arrayType) offset viewSize = + and private getAffectedIndices reporter state address ({elemType = elementType; dimension = dim} as arrayType) offset viewSize = let concreteElementSize = internalSizeOf elementType let elementSize = makeNumber concreteElementSize let lens = List.init dim (fun dim -> readLength state address (makeNumber dim) arrayType) @@ -1257,7 +1264,7 @@ module internal Memory = let index = div offset elemSize let address, arrayType = if typ = typeof then stringArrayInfo state address None - else address, (sightType, 1, true) + else address, arrayType.CreateVector sightType ArrayIndex(address, [index], arrayType) |> Some else None elif isValueType typ && suitableType typ && offset = zero then @@ -1366,14 +1373,14 @@ module internal Memory = let private arrayMemsetData state concreteAddress data arrayType = let arrayType = substituteTypeVariablesIntoArrayType state arrayType - let elemType = fst3 arrayType + let elemType = arrayType.elemType ensureConcreteType elemType let region = accessRegion state.arrays arrayType elemType let region' = arrayRegionMemsetData state concreteAddress data elemType region state.arrays <- PersistentDict.add arrayType region' state.arrays let initializeArray state address indicesAndValues arrayType = - let elementType = fst3 arrayType + let elementType = arrayType.elemType ensureConcreteType elementType let mr = accessRegion state.arrays arrayType elementType let keysAndValues = Seq.map (fun (i, v) -> OneArrayIndexKey(address, i), v) indicesAndValues @@ -1392,7 +1399,7 @@ module internal Memory = let private fillArrayBoundsSymbolic state address lengths lowerBounds arrayType = let d = List.length lengths - assert(d = snd3 arrayType) + assert(d = arrayType.dimension) assert(List.length lowerBounds = d) let writeLengths state l i = writeLengthSymbolic state address (Concrete i lengthType) arrayType l let writeLowerBounds state l i = writeLowerBoundSymbolic state address (Concrete i lengthType) arrayType l @@ -1437,7 +1444,8 @@ module internal Memory = let private unmarshallArray (state : state) concreteAddress (array : Array) = let address = ConcreteHeapAddress concreteAddress - let _, dim, _ as arrayType = array.GetType() |> symbolicTypeToArrayType + let arrayType = array.GetType() |> symbolicTypeToArrayType + let dim = arrayType.dimension let lbs = List.init dim array.GetLowerBound let lens = List.init dim array.GetLength let indicesWithValues = Array.getArrayIndicesWithValues array @@ -1709,7 +1717,7 @@ module internal Memory = ConcreteHeapAddress concreteAddress | _ -> let address = allocateVector state elementType length - let arrayType : arrayType = (elementType, 1, true) + let arrayType = arrayType.CreateVector elementType let mr = accessRegion state.arrays arrayType elementType let keysAndValues = Seq.mapi (fun i v -> OneArrayIndexKey(address, [makeNumber i]), Concrete v elementType) contents let mr' = MemoryRegion.memset mr keysAndValues @@ -2108,7 +2116,7 @@ module internal Memory = | None -> PersistentDict.add k' v' acc PersistentDict.fold fillAndMutate dict dict' - let private composeConcreteMemory mapKey (cm : IConcreteMemory) (cm' : IConcreteMemory) = + let private composeConcreteMemory mapKey (cm : ConcreteMemory) (cm' : ConcreteMemory) = // TODO: implement concrete memory composition () diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index 4414c426b..88194bf0c 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -28,7 +28,7 @@ type regionSort = match x with | HeapFieldSort field | StaticFieldSort field -> field.typ - | ArrayIndexSort(elementType, _, _) -> elementType + | ArrayIndexSort arrayType -> arrayType.elemType | ArrayLengthSort _ | ArrayLowerBoundSort _ -> typeof | StackBufferSort _ -> typeof @@ -38,15 +38,15 @@ type regionSort = match x with | HeapFieldSort field -> $"HeapField {field.FullName}" | StaticFieldSort field -> $"StaticField {field.FullName}" - | ArrayIndexSort(elementType, dim, isVector) -> + | ArrayIndexSort {elemType = elementType; dimension = dim; isVector = isVector} -> if isVector then $"VectorIndex to {elementType}[{dim}]" else $"ArrayIndex to {elementType}[{dim}]" - | ArrayLengthSort(elementType, dim, isVector) -> + | ArrayLengthSort {elemType = elementType; dimension = dim; isVector = isVector} -> if isVector then $"VectorLength to {elementType}[{dim}]" else $"ArrayLength to {elementType}[{dim}]" - | ArrayLowerBoundSort(elementType, dim, isVector) -> + | ArrayLowerBoundSort {elemType = elementType; dimension = dim; isVector = isVector} -> if isVector then $"VectorLowerBound to {elementType}[{dim}]" else $"ArrayLowerBound to {elementType}[{dim}]" @@ -113,7 +113,7 @@ module private MemoryKeyUtils = let rec keysInListProductRegion keys (region : int points listProductRegion) = match region, keys with - | NilRegion, Seq.Empty -> (True()) + | NilRegion, Seq.Empty -> True() | ConsRegion products, Seq.Cons(curr, rest) -> let keyInPoints = keyInIntPoints curr let keyInProduct = keysInListProductRegion rest @@ -429,11 +429,11 @@ type symbolicTypeKey = reg.Map (fun t -> {t = mapper t.t}), {typ = mapper x.typ} override x.IsUnion = false override x.Unguard = [(True(), x)] - override x.InRegionCondition region = + override x.InRegionCondition _ = // TODO implement some time if need True() - override x.MatchCondition key keyIndexingRegion = + override x.MatchCondition key _ = Concrete (x.typ = key.typ) typeof override x.ToString() = x.typ.ToString() @@ -514,7 +514,7 @@ module private UpdateTree = [] type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = - {typ : Type; updates : updateTree<'key, term, 'reg>; defaultValue : option -> bool)>} + {typ : Type; updates : updateTree<'key, term, 'reg>; defaultValue : term option} with override x.Equals(other : obj) = match other with @@ -522,7 +522,7 @@ type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, ' let compareDefault = lazy( match x.defaultValue, other.defaultValue with - | Some(v1, _), Some(v2, _) -> v1 = v2 + | Some v1, Some v2 -> v1 = v2 | None, None -> true | _ -> false ) @@ -531,7 +531,7 @@ type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, ' override x.GetHashCode() = let defaultValue = match x.defaultValue with - | Some(v, _) -> Some v + | Some v -> Some v | None -> None HashCode.Combine(x.typ, x.updates, defaultValue) @@ -540,8 +540,8 @@ module MemoryRegion = let empty typ = {typ = typ; updates = UpdateTree.empty; defaultValue = None} - let fillRegion defaultValue (isSuitableKey : IMemoryKey<_,_> -> bool) (region : memoryRegion<_,_>) = - { region with defaultValue = Some(defaultValue, isSuitableKey) } + let fillRegion defaultValue (region : memoryRegion<_,_>) = + { region with defaultValue = Some defaultValue } let maxTime (tree : updateTree<'a, heapAddress, 'b>) startingTime = RegionTree.foldl (fun m _ {key=_; value=v} -> VectorTime.max m (timeOf v)) startingTime tree @@ -550,7 +550,7 @@ module MemoryRegion = let makeSymbolic tree = instantiate mr.typ { typ = mr.typ; updates = tree; defaultValue = mr.defaultValue } let makeDefault () = match mr.defaultValue with - | Some (d, isSuitableKey) when isSuitableKey key -> d + | Some d -> d | _ -> makeDefaultValue mr.typ UpdateTree.read key isDefault makeSymbolic makeDefault mr.updates @@ -568,7 +568,7 @@ module MemoryRegion = let map (mapTerm : term -> term) (mapType : Type -> Type) (mapTime : vectorTime -> vectorTime) mr = let typ = mapType mr.typ let updates = UpdateTree.map (fun reg k -> k.Map mapTerm mapType mapTime reg) mapTerm mr.updates - let defaultValue = Option.map (fun (v, keys) -> mapTerm v, keys) mr.defaultValue + let defaultValue = Option.map mapTerm mr.defaultValue {typ = typ; updates = updates; defaultValue = defaultValue} let mapKeys<'reg, 'key when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> (mapKey : 'reg -> 'key -> 'reg * 'key) mr = diff --git a/VSharp.SILI.Core/Pointers.fs b/VSharp.SILI.Core/Pointers.fs index da4146c19..0e25ab8bc 100644 --- a/VSharp.SILI.Core/Pointers.fs +++ b/VSharp.SILI.Core/Pointers.fs @@ -36,7 +36,7 @@ module internal Pointers = // TODO: use specific 'getFieldOffset' StaticLocation symbolicType, getFieldOffset field // NOTE: only vector case - | ArrayIndex(heapAddress, [index], (elementType, _, true as arrayType)) -> + | ArrayIndex(heapAddress, [index], ({elemType = elementType; isVector = true} as arrayType)) -> let sizeOfElement = internalSizeOf elementType |> makeNumber let typ = arrayTypeToSymbolicType arrayType HeapLocation(heapAddress, typ), mul index sizeOfElement diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index a584419c4..51edf89de 100644 --- a/VSharp.SILI.Core/State.fs +++ b/VSharp.SILI.Core/State.fs @@ -11,28 +11,6 @@ type typeVariables = mappedStack * Type list stack type stackBufferKey = concreteHeapAddress -type IConcreteMemory = - abstract Copy : unit -> IConcreteMemory - abstract Contains : concreteHeapAddress -> bool - abstract VirtToPhys : concreteHeapAddress -> obj - abstract TryVirtToPhys : concreteHeapAddress -> obj option - abstract PhysToVirt : obj -> concreteHeapAddress - abstract TryPhysToVirt : obj -> concreteHeapAddress option - abstract Allocate : concreteHeapAddress -> obj -> unit - abstract ReadClassField : concreteHeapAddress -> fieldId -> obj - abstract ReadArrayIndex : concreteHeapAddress -> int list -> obj - abstract GetAllArrayData : concreteHeapAddress -> seq - abstract ReadArrayLowerBound : concreteHeapAddress -> int -> obj - abstract ReadArrayLength : concreteHeapAddress -> int -> obj - abstract WriteClassField : concreteHeapAddress -> fieldId -> obj -> unit - abstract WriteArrayIndex : concreteHeapAddress -> int list -> obj -> unit - abstract InitializeArray : concreteHeapAddress -> RuntimeFieldHandle -> unit - abstract FillArray : concreteHeapAddress -> int -> int -> obj -> unit - abstract CopyArray : concreteHeapAddress -> concreteHeapAddress -> int64 -> int64 -> int64 -> unit - abstract CopyCharArrayToString : concreteHeapAddress -> concreteHeapAddress -> int -> unit - abstract CopyCharArrayToStringLen : concreteHeapAddress -> concreteHeapAddress -> int -> int -> unit - abstract Remove : concreteHeapAddress -> unit - // TODO: is it good idea to add new constructor for recognizing cilStates that construct RuntimeExceptions? type exceptionRegister = | Unhandled of term * bool * string // Exception term * is runtime exception * stack trace @@ -195,7 +173,7 @@ and 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 : IConcreteMemory // Fully concrete objects + concreteMemory : ConcreteMemory // Fully concrete objects mutable allocatedTypes : pdict // Types of heap locations allocated via new mutable initializedAddresses : pset // Addresses, which invariants were initialized mutable typeVariables : typeVariables // Type variables assignment in the current state diff --git a/VSharp.SILI.Core/Substitution.fs b/VSharp.SILI.Core/Substitution.fs index 399f398f0..d05e510a3 100644 --- a/VSharp.SILI.Core/Substitution.fs +++ b/VSharp.SILI.Core/Substitution.fs @@ -7,14 +7,19 @@ module Substitution = let rec substituteAddress termSubst typeSubst = function | PrimitiveStackLocation _ as sl -> sl | ClassField(addr, field) -> ClassField(termSubst addr, field) - | ArrayIndex(addr, index, (elementType, dim, isVector)) -> - ArrayIndex(termSubst addr, List.map termSubst index, (typeSubst elementType, dim, isVector)) + | ArrayIndex(addr, index, ({elemType = elementType} as arrayType)) -> + let arrayType = { arrayType with elemType = typeSubst elementType } + ArrayIndex(termSubst addr, List.map termSubst index, arrayType) | StructField(addr, field) -> StructField(substituteAddress termSubst typeSubst addr, field) | StaticField(typ, field) -> StaticField(typeSubst typ, field) - | ArrayLength(addr, dim, (typ, d, isVector)) -> ArrayLength(termSubst addr, termSubst dim, (typeSubst typ, d, isVector)) + | ArrayLength(addr, dim, ({elemType = elementType} as arrayType)) -> + let arrayType = { arrayType with elemType = typeSubst elementType } + ArrayLength(termSubst addr, termSubst dim, arrayType) | BoxedLocation(addr, typ) -> BoxedLocation(termSubst addr, typeSubst typ) | StackBufferIndex(key, index) -> StackBufferIndex(key, termSubst index) - | ArrayLowerBound(addr, dim, (typ, d, isVector)) -> ArrayLowerBound(termSubst addr, termSubst dim, (typeSubst typ, d, isVector)) + | ArrayLowerBound(addr, dim, ({elemType = elementType} as arrayType)) -> + let arrayType = { arrayType with elemType = typeSubst elementType } + ArrayLowerBound(termSubst addr, termSubst dim, arrayType) let substitutePointerBase termSubst typeSubst = function | HeapLocation(loc, typ) -> HeapLocation(termSubst loc, typeSubst typ) diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index c9ba120f4..41023340d 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -17,6 +17,7 @@ type IMethod = abstract Parameters : Reflection.ParameterInfo[] abstract LocalVariables : IList abstract HasThis : bool + abstract HasParameterOnStack : bool abstract IsConstructor : bool abstract IsExternalMethod : bool abstract ContainsGenericParameters : bool @@ -83,7 +84,18 @@ type stackKey = TemporaryLocalVariableKey((Reflection.concretizeType typeSubst typ), index) type concreteHeapAddress = vectorTime -type arrayType = Type * int * bool // Element type * dimension * is vector + +type arrayType = + { elemType : Type; dimension : int; isVector : bool } + with + static member CreateVector (elemType : Type) = + { elemType = elemType; dimension = 1; isVector = true } + + static member CharVector = { elemType = typeof; dimension = 1; isVector = true } + + member x.IsVector = x.isVector && (assert(x.dimension = 1); true) + + member x.IsCharVector = x.IsVector && x.elemType = typeof [] type operation = @@ -136,7 +148,7 @@ type termNode = $"" |> k | Concrete(obj, AddressType) when (obj :?> int32 list) = [0] -> k "null" | Concrete(c, Char) when c :?> char = '\000' -> k "'\\000'" - | Concrete(c, Char) -> sprintf "'%O'" c |> k + | Concrete(c, Char) -> k $"'{c}'" | Concrete(:? concreteHeapAddress as addr, AddressType) -> VectorTime.print addr |> k | Concrete(value, _) -> value.ToString() |> k | Expression(operation, operands, _) -> @@ -178,8 +190,8 @@ type termNode = let printed = guards |> Seq.sort |> join ("\n" + indent) formatIfNotEmpty (formatWithIndent indent) printed |> sprintf "UNION[%s]" |> k) | HeapRef({term = Concrete(obj, AddressType)}, _) when (obj :?> int32 list) = [0] -> k "NullRef" - | HeapRef(address, baseType) -> sprintf "(HeapRef %O to %O)" address baseType |> k - | Ref address -> sprintf "(%sRef %O)" (address.Zone()) address |> k + | HeapRef(address, baseType) -> $"(HeapRef {address} to {baseType})" |> k + | Ref address -> $"({address.Zone()}Ref {address})" |> k | Ptr(HeapLocation(address, _), typ, shift) -> $"(HeapPtr {address} as {typ}, offset = {shift})" |> k | Ptr(StackLocation loc, typ, shift) -> @@ -226,7 +238,7 @@ and address = match x with | PrimitiveStackLocation key -> toString key | ClassField(addr, field) -> $"{addr}.{field}" - | ArrayIndex(addr, idcs, _) -> sprintf "%O[%s]" addr (List.map toString idcs |> join ", ") + | ArrayIndex(addr, indices, _) -> sprintf "%O[%s]" addr (List.map toString indices |> join ", ") | StaticField(typ, field) -> $"{typ}.{field}" | StructField(addr, field) -> $"{addr}.{field}" | ArrayLength(addr, dim, _) -> $"Length({addr}, {dim})" @@ -249,7 +261,7 @@ and address = | ClassField(_, field) | StructField(_, field) | StaticField(_, field) -> field.typ - | ArrayIndex(_, _, (elementType, _, _)) -> elementType + | ArrayIndex(_, _, { elemType = elementType }) -> elementType | BoxedLocation(_, typ) -> typ | ArrayLength _ | ArrayLowerBound _ -> lengthType @@ -319,7 +331,7 @@ module internal Terms = HashMap.addTerm (HeapRef(address, baseType)) let Ref address = match address with - | ArrayIndex(_, indices, (_, dim, _)) -> assert(List.length indices = dim) + | ArrayIndex(_, indices, { dimension = dim }) -> assert(List.length indices = dim) | _ -> () HashMap.addTerm (Ref address) let Ptr baseAddress typ offset = HashMap.addTerm (Ptr(baseAddress, typ, offset)) @@ -409,14 +421,14 @@ module internal Terms = let symbolicTypeToArrayType = function | ArrayType(elementType, dim) -> match dim with - | Vector -> (elementType, 1, true) - | ConcreteDimension d -> (elementType, d, false) + | Vector -> arrayType.CreateVector elementType + | ConcreteDimension d -> { elemType = elementType; dimension = d; isVector = false } | SymbolicDimension -> __insufficientInformation__ "Cannot process array of unknown dimension!" | typ -> internalfail $"symbolicTypeToArrayType: expected array type, but got {typ}" - let arrayTypeToSymbolicType (elemType : Type, dim, isVector) = - if isVector then elemType.MakeArrayType() - else elemType.MakeArrayType(dim) + let arrayTypeToSymbolicType arrayType = + if arrayType.isVector then arrayType.elemType.MakeArrayType() + else arrayType.elemType.MakeArrayType(arrayType.dimension) let sizeOf = typeOf >> internalSizeOf @@ -1000,7 +1012,7 @@ module internal Terms = | Constant(_, source, _) -> source.Time | HeapRef(address, _) -> timeOf address | Union gvs -> List.fold (fun m (_, v) -> VectorTime.max m (timeOf v)) VectorTime.zero gvs - | _ -> internalfailf "timeOf : expected heap address, but got %O" address + | _ -> internalfail $"timeOf : expected heap address, but got {address}" and compareTerms t1 t2 = match t1.term, t2.term with @@ -1044,9 +1056,9 @@ module internal Terms = | StaticField _ | BoxedLocation _ -> k state | ClassField(addr, _) -> doFold folder state addr k - | ArrayIndex(addr, idcs, _) -> + | ArrayIndex(addr, indices, _) -> doFold folder state addr (fun state -> - foldSeq folder idcs state k) + foldSeq folder indices state k) | StructField(addr, _) -> foldAddress folder state addr k | ArrayLength(addr, idx, _) | ArrayLowerBound(addr, idx, _) -> @@ -1114,7 +1126,7 @@ module internal Terms = | ClassType _ | InterfaceType _ -> nullRef typ | TypeVariable t when isReferenceTypeParameter t -> nullRef typ - | TypeVariable t -> __insufficientInformation__ "Cannot instantiate value of undefined type %O" t + | TypeVariable t -> __insufficientInformation__ $"Cannot instantiate value of undefined type {t}" | StructType _ -> makeStruct false (fun _ _ t -> makeDefaultValue t) typ | Pointer typ -> makeNullPtr typ | AddressType -> zeroAddress() diff --git a/VSharp.SILI.Core/TypeSolverUtils.fs b/VSharp.SILI.Core/TypeSolverUtils.fs index 6c2c387cf..9a9afe3b6 100644 --- a/VSharp.SILI.Core/TypeSolverUtils.fs +++ b/VSharp.SILI.Core/TypeSolverUtils.fs @@ -656,6 +656,7 @@ and genericCandidate private ( let supertypeDef = TypeUtils.getTypeDef supertype let supertypeDefArgs = TypeUtils.getGenericArgs supertypeDef let supertypeArgs = TypeUtils.getGenericArgs supertype + // TODO: need to check non-generic interfaces? let index = interfaces |> Array.tryFindIndex (fun t -> t = supertypeDef || t.IsGenericType && t.GetGenericTypeDefinition() = supertypeDef) match index with | Some index -> diff --git a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj index 16c63087e..b87de58a3 100644 --- a/VSharp.SILI.Core/VSharp.SILI.Core.fsproj +++ b/VSharp.SILI.Core/VSharp.SILI.Core.fsproj @@ -31,8 +31,9 @@ - + + diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index 56894ab42..e4b28c8ea 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -7,55 +7,10 @@ open VSharp.Core open VSharp.Interpreter.IL open IpOperations -type prefix = - | Constrained of System.Type - -[] -type cilState = - { - mutable ipStack : ipStack - // This field stores information about instruction prefix (for example, '.constrained' prefix) - mutable prefixContext : prefix list - // TODO: get rid of currentLoc! - // This field stores only approximate information and can't be used for getting the precise location. Instead, use ipStack.Head - mutable currentLoc : codeLocation - state : state - mutable stackArrays : pset - mutable errorReported : bool - mutable filterResult : term option - //TODO: #mb frames list #mb transfer to Core.State - mutable iie : InsufficientInformationException option - mutable level : level - startingIP : ip - mutable initialEvaluationStackSize : uint32 - mutable stepsNumber : uint - mutable suspended : bool - mutable targets : Set - /// - /// All basic blocks visited by the state. - /// - mutable history : Set - /// - /// If the state is not isolated (produced during forward execution), Some of it's entry point method, else None. - /// - entryMethod : Method option - /// - /// Deterministic state id. - /// - id : uint - } - override x.ToString() = System.String.Empty - - interface IGraphTrackableState with - override this.CodeLocation = this.currentLoc - override this.CallStack = Memory.StackTrace this.state.stack |> List.map (fun m -> m :?> Method) - -type cilStateComparer(comparer) = - interface IComparer with - override _.Compare(x : cilState, y : cilState) = - comparer x y +module CilState = -module CilStateOperations = + type prefix = + | Constrained of System.Type let mutable currentStateId = 0u let getNextStateId() = @@ -63,347 +18,33 @@ module CilStateOperations = currentStateId <- currentStateId + 1u nextId - let makeCilState entryMethod curV initialEvaluationStackSize state = - let currentLoc = ip2codeLocation curV |> Option.get - { - ipStack = [curV] - prefixContext = List.empty - currentLoc = currentLoc - state = state - stackArrays = PersistentSet.empty - errorReported = false - filterResult = None - iie = None - level = PersistentDict.empty - startingIP = curV - initialEvaluationStackSize = initialEvaluationStackSize - stepsNumber = 0u - suspended = false - targets = Set.empty - history = Set.empty - entryMethod = Some entryMethod - id = getNextStateId() - } - - let makeInitialState m state = makeCilState m (instruction m 0) 0u state - - let mkCilStateHashComparer = cilStateComparer (fun a b -> a.GetHashCode().CompareTo(b.GetHashCode())) - - let isIsolated state = state.entryMethod.IsNone - - let entryMethodOf state = - if isIsolated state then - invalidOp "Isolated state doesn't have an entry method" - state.entryMethod.Value - - let isIIEState (s : cilState) = Option.isSome s.iie - - let isExecutable (s : cilState) = - match s.ipStack with - | [] -> __unreachable__() - | [ Exit _ ] -> false - | _ -> true - - let isUnhandledException (s : cilState) = - match s.state.exceptionsRegister.Peek with - | Unhandled _ -> true - | _ -> false - - let isUnhandledExceptionOrError (s : cilState) = - match s.state.exceptionsRegister.Peek with - | Unhandled _ -> true - | _ -> s.errorReported - - let newExceptionRegister (cilState : cilState) = - let state = cilState.state - state.exceptionsRegister <- state.exceptionsRegister.Push NoException - - let popExceptionRegister (cilState : cilState) = - let state = cilState.state - state.exceptionsRegister <- state.exceptionsRegister.Tail - - let toUnhandledException cilState = - let state = cilState.state - state.exceptionsRegister <- state.exceptionsRegister.TransformToUnhandled() - - let toCaughtException cilState = - let state = cilState.state - state.exceptionsRegister <- state.exceptionsRegister.TransformToCaught() - - let moveDownExceptionRegister (cilState : cilState) = - let state = cilState.state - let elem, rest = state.exceptionsRegister.Pop() - state.exceptionsRegister <- rest.Tail.Push elem - - let levelToUnsignedInt (lvl : level) = - // TODO: remove it when ``level'' subtraction would be generalized - PersistentDict.fold (fun acc _ v -> max acc v) 0u lvl - - let currentIp (s : cilState) = - match s.ipStack with - | [] -> internalfail "currentIp: 'IP' stack is empty" - | h :: _ -> h - - let stoppedByException (s : cilState) = - match currentIp s with - | EmptySearchingForHandler -> true - | _ -> false - - let hasRuntimeExceptionOrError (s : cilState) = - match s.state.exceptionsRegister.Peek with - | _ when s.errorReported -> true - | Unhandled(_, isRuntime, _) -> isRuntime - | _ -> false - - let hasReportedError (s : cilState) = s.errorReported - - let isStopped s = isIIEState s || stoppedByException s || not(isExecutable(s)) - - let tryCurrentLoc = currentIp >> ip2codeLocation - let currentLoc = tryCurrentLoc >> Option.get - let startingLoc (s : cilState) = s.startingIP |> ip2codeLocation |> Option.get - - let violatesLevel (s : cilState) maxBound = - match tryCurrentLoc s with - | Some currLoc when PersistentDict.contains currLoc s.level -> - s.level[currLoc] >= maxBound - | _ -> false - - // [NOTE] Obtaining exploring method - let currentMethod = currentIp >> forceMethodOf - - let currentOffset = currentIp >> offsetOf - - let startsFromMethodBeginning (s : cilState) = - match s.startingIP with - | Instruction (0, _) -> true - | _ -> false - - let private moveCodeLoc (cilState : cilState) (ip : ip) = - match ip2codeLocation ip with - | Some loc when loc.method.HasBody -> cilState.currentLoc <- loc - | _ -> () - - let pushToIp (ip : ip) (cilState : cilState) = - let loc = cilState.currentLoc - match ip2codeLocation ip with - | Some loc' when loc'.method.HasBody -> - cilState.currentLoc <- loc' - Application.addCallEdge loc loc' - | _ -> () - cilState.ipStack <- ip :: cilState.ipStack - - let setCurrentIp (ip : ip) (cilState : cilState) = - moveCodeLoc cilState ip - assert(List.isEmpty cilState.ipStack |> not) - cilState.ipStack <- ip :: List.tail cilState.ipStack - - let rec private changeInnerIp oldIp newIp = - match oldIp with - | Leave(ip, e, i, m) -> - Leave(changeInnerIp ip newIp, e, i, m) - | InFilterHandler(ip, offset, e, f, lc, l) -> - InFilterHandler(changeInnerIp ip newIp, offset, e, f, lc, l) - | SecondBypass(Some ip, ehcs, lastBlocks, loc, cl, ftp) -> - SecondBypass(Some (changeInnerIp ip newIp), ehcs, lastBlocks, loc, cl, ftp) - | _ -> newIp - - let setCurrentIpSafe (ip : ip) (cilState : cilState) = - let oldIp = currentIp cilState - let ip = changeInnerIp oldIp ip - setCurrentIp ip cilState - - let private (|NonRecIp|_|) = function - | Instruction _ -> Some () - | Exit _ -> Some () - | SearchingForHandler _ -> Some () - | SecondBypass(None, _, _, _, _, _) -> Some() - | _ -> None - - let rec private createNewIp oldIp newIp = - match oldIp with - | InFilterHandler(NonRecIp _, _, _, _, _, _) -> newIp - | Leave(NonRecIp _, _, _, _) -> newIp - | SecondBypass(Some NonRecIp, _, _, _, _, _) -> newIp - | InFilterHandler(ip, offset, e, f, lc, l) -> - InFilterHandler(createNewIp ip newIp, offset, e, f, lc, l) - | Leave(ip, e, i, m) -> Leave(createNewIp ip newIp, e, i, m) - | SecondBypass(Some ip, ehcs, lastBlocks, lastLocation, locations, handlerLoc) -> - SecondBypass(Some (createNewIp ip newIp), ehcs, lastBlocks, lastLocation, locations, handlerLoc) - | _ -> newIp - - let replaceLastIp (ip : ip) (cilState : cilState) = - let oldIp = currentIp cilState - let newIp = createNewIp oldIp ip - setCurrentIp newIp cilState - - let pushPrefixContext (cilState : cilState) (prefix : prefix) = - cilState.prefixContext <- prefix :: cilState.prefixContext - - let popPrefixContext (cilState : cilState) = - match cilState.prefixContext with - | prefix :: context -> - cilState.prefixContext <- context - Some prefix - | _ -> None - - let addStackArray (cilState : cilState) (address : concreteHeapAddress) = - cilState.stackArrays <- PersistentSet.add cilState.stackArrays address - - let isStackArray cilState ref = - match ref.term with - | HeapRef({term = ConcreteHeapAddress address}, _) - | Ref(ArrayIndex({term = ConcreteHeapAddress address}, _, _)) - | Ptr(HeapLocation({term = ConcreteHeapAddress address}, _), _, _) -> - PersistentSet.contains address cilState.stackArrays - | _ -> false - - let composeIps (oldIpStack : ipStack) (newIpStack : ipStack) = newIpStack @ oldIpStack - - let composeLevel (lvl1 : level) (lvl2 : level) = - let composeOne (lvl : level) k v = - let oldValue = PersistentDict.tryFind lvl k |> Option.defaultValue 0u - PersistentDict.add k (v + oldValue) lvl - PersistentDict.fold composeOne lvl1 lvl2 - - let compose (cilState1 : cilState) (cilState2 : cilState) = - assert(currentIp cilState1 = cilState2.startingIP) - let level = - PersistentDict.fold (fun (acc : level) k v -> - let oldValue = if PersistentDict.contains k acc then PersistentDict.find acc k else 0u - PersistentDict.add k (v + oldValue) acc - ) cilState1.level cilState2.level - let iie = None // we might concretize state, so we should try executed instructions again - let ip = composeIps (List.tail cilState1.ipStack) cilState2.ipStack - let states = Memory.ComposeStates cilState1.state cilState2.state - let _, leftEvaluationStack = EvaluationStack.PopMany (int cilState2.initialEvaluationStackSize) cilState1.state.evaluationStack - let makeResultState (state : state) = - let state' = { state with evaluationStack = EvaluationStack.Union leftEvaluationStack state.evaluationStack } - {cilState2 with state = state'; ipStack = ip; level = level; initialEvaluationStackSize = cilState1.initialEvaluationStackSize - startingIP = cilState1.startingIP; iie = iie; id = getNextStateId()} - List.map makeResultState states - - let incrementLevel (cilState : cilState) codeLocation = - let lvl = cilState.level - let oldValue = PersistentDict.tryFind lvl codeLocation |> Option.defaultValue 0u - cilState.level <- PersistentDict.add codeLocation (oldValue + 1u) lvl - - let decrementLevel (cilState : cilState) codeLocation = - let lvl = cilState.level - let oldValue = PersistentDict.tryFind lvl codeLocation - match oldValue with - | Some value when value = 1u -> - cilState.level <- PersistentDict.remove codeLocation lvl - | Some value when value > 0u -> - cilState.level <- PersistentDict.add codeLocation (value - 1u) lvl - | _ -> () - - let addLocationToHistory (cilState : cilState) (loc : codeLocation) = - cilState.history <- Set.add loc cilState.history - - // ------------------------------- Helper functions for cilState and state interaction ------------------------------- - - let stateOf (cilState : cilState) = cilState.state - let popFrameOf (cilState : cilState) = - Memory.PopFrame cilState.state - let ip = List.tail cilState.ipStack - cilState.ipStack <- ip - match ip with - | ip::_ -> moveCodeLoc cilState ip - | [] -> () - - let setCurrentTime time (cilState : cilState) = cilState.state.currentTime <- time - let setEvaluationStack evaluationStack (cilState : cilState) = cilState.state.evaluationStack <- evaluationStack - - let clearEvaluationStackLastFrame (cilState : cilState) = - cilState.state.evaluationStack <- EvaluationStack.ClearActiveFrame cilState.state.evaluationStack - - // TODO: Not mutable -- copies cilState #do - let changeState (cilState : cilState) state = - if LanguagePrimitives.PhysicalEquality state cilState.state then cilState - else {cilState with state = state; id = getNextStateId()} - - let setException exc (cilState : cilState) = - let state = cilState.state - state.exceptionsRegister <- state.exceptionsRegister.Tail.Push exc - - let push v (cilState : cilState) = - match v.term with - | Nop -> internalfail "pushing 'NOP' value onto evaluation stack" - | _ -> - cilState.state.evaluationStack <- EvaluationStack.Push v cilState.state.evaluationStack - - let pushMany vs (cilState : cilState) = - if List.contains (Nop()) vs then - internalfail "pushing 'NOP' value onto evaluation stack" - cilState.state.evaluationStack <- EvaluationStack.PushMany vs cilState.state.evaluationStack - - let peek (cilState : cilState) = - EvaluationStack.Pop cilState.state.evaluationStack |> fst - let peek2 (cilState : cilState) = - let stack = cilState.state.evaluationStack - let arg2, stack = EvaluationStack.Pop stack - let arg1, _ = EvaluationStack.Pop stack - arg2, arg1 - let pop (cilState : cilState) = - let v, evaluationStack = EvaluationStack.Pop cilState.state.evaluationStack - cilState.state.evaluationStack <- evaluationStack - v - let pop2 (cilState : cilState) = - let arg2 = pop cilState - let arg1 = pop cilState - arg2, arg1 - let pop3 (cilState : cilState) = - let arg3 = pop cilState - let arg2 = pop cilState - let arg1 = pop cilState - arg3, arg2, arg1 - - let pushNewObjForValueTypes (afterCall : cilState) = - let ref = pop afterCall - let value = Memory.Read afterCall.state ref - push value afterCall - - let addTarget (state : cilState) target = - let prev = state.targets - state.targets <- Set.add target prev - prev.Count <> state.targets.Count - - let removeTarget (state : cilState) target = - let prev = state.targets - state.targets <- Set.remove target prev - prev.Count <> state.targets.Count - - // ------------------------------------ Memory Interaction ------------------------------------ - - let mutable private reportError : cilState -> string -> unit = - fun _ _ -> internalfail "'reportError' is not ready" - - let mutable private reportFatalError : cilState -> string -> unit = - fun _ _ -> internalfail "'reportError' is not ready" - - let configureErrorReporter reportErrorFunc reportFatalErrorFunc = - reportError <- reportErrorFunc - reportFatalError <- reportFatalErrorFunc - - type public ErrorReporter internal (reportError, reportFatalError, cilState) = + type public ErrorReporter internal (cilState : cilState) = let mutable cilState = cilState let mutable stateConfigured : bool = false - static member ReportError cilState message = - cilState.errorReported <- true + static let mutable reportError : cilState -> string -> unit = + fun _ _ -> internalfail "'reportError' is not ready" + static let mutable reportFatalError : cilState -> string -> unit = + fun _ _ -> internalfail "'reportFatalError' is not ready" + + static member Configure reportErrorFunc reportFatalErrorFunc = + reportError <- reportErrorFunc + reportFatalError <- reportFatalErrorFunc + + static member ReportError (cilState : cilState) message = + cilState.ReportError() reportError cilState message - static member ReportFatalError cilState message = - cilState.errorReported <- true + static member ReportFatalError (cilState : cilState) message = + cilState.ReportError() reportFatalError cilState message interface IErrorReporter with override x.ReportError msg failCondition = assert stateConfigured let report state k = - let cilState = changeState cilState state - cilState.errorReported <- true + let cilState = cilState.ChangeState state + cilState.ReportError() reportError cilState msg |> k let mutable isAlive = false StatedConditionalExecution cilState.state @@ -417,8 +58,8 @@ module CilStateOperations = override x.ReportFatalError msg failCondition = assert stateConfigured let report state k = - let cilState = changeState cilState state - cilState.errorReported <- true + let cilState = cilState.ChangeState state + cilState.ReportError() reportFatalError cilState msg |> k let mutable isAlive = false StatedConditionalExecution cilState.state @@ -430,90 +71,434 @@ module CilStateOperations = isAlive override x.ConfigureState state = - cilState <- changeState cilState state + cilState <- cilState.ChangeState state stateConfigured <- true - let internal createErrorReporter cilState = - ErrorReporter(reportError, reportFatalError, cilState) - - let read cilState ref = - let reporter = createErrorReporter cilState - Memory.ReadUnsafe reporter cilState.state ref - - let readField cilState term field = - let reporter = createErrorReporter cilState - Memory.ReadFieldUnsafe reporter cilState.state term field - - let readIndex cilState term index valueType = - let reporter = createErrorReporter cilState - Memory.ReadArrayIndexUnsafe reporter cilState.state term index valueType - - let write cilState ref value = - let reporter = createErrorReporter cilState - let states = Memory.WriteUnsafe reporter cilState.state ref value - List.map (changeState cilState) states - - let writeClassField cilState ref field value = - let states = Memory.WriteClassField cilState.state ref field value - List.map (changeState cilState) states - - let writeStructField cilState term field value = - let reporter = createErrorReporter cilState - Memory.WriteStructFieldUnsafe reporter cilState.state term field value - - let writeIndex cilState term index value valueType = - let reporter = createErrorReporter cilState - let states = Memory.WriteArrayIndexUnsafe reporter cilState.state term index value valueType - List.map (changeState cilState) states - - // ------------------------------- Helper functions for cilState ------------------------------- - - let GuardedApplyCIL (cilState : cilState) term (f : cilState -> term -> ('a list -> 'b) -> 'b) (k : 'a list -> 'b) = - let mkCilState state = - if LanguagePrimitives.PhysicalEquality state cilState.state then cilState - else {cilState with state = state; id = getNextStateId()} - GuardedStatedApplyk - (fun state term k -> f (mkCilState state) term k) - cilState.state term id (List.concat >> k) - - let StatedConditionalExecutionCIL (cilState : cilState) conditionInvocation thenBranch elseBranch k = - let origCilState = {cilState with state = cilState.state} - let mkCilState state = - if LanguagePrimitives.PhysicalEquality state cilState.state then cilState - else {origCilState with state = state; id = getNextStateId()} - StatedConditionalExecution cilState.state conditionInvocation - (fun state k -> thenBranch (mkCilState state) k) - (fun state k -> elseBranch (mkCilState state) k) - (fun x y -> [x; y]) - (List.concat >> k) - - let BranchOnNullCIL (cilState : cilState) term thenBranch elseBranch k = - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference term, state)) - thenBranch - elseBranch - k - - // ------------------------------- Pretty printing for cilState ------------------------------- - - let private dumpSectionValue section value (sb : StringBuilder) = - let sb = Utils.PrettyPrinting.dumpSection section sb - Utils.PrettyPrinting.appendLine sb value - - let private dumpIp (ipStack : ipStack) = - List.fold (fun acc entry -> sprintf "%s\n%O" acc entry) "" ipStack - - let ipAndMethodBase2String (codeLocation : codeLocation) = - sprintf "Method: %O, offset = %d" codeLocation.method codeLocation.offset - - // TODO: print filterResult and IIE ? - let dump (cilState : cilState) : string = - let sb = (StringBuilder()) - let sb = dumpSectionValue "Starting ip" (sprintf "%O" cilState.startingIP) sb - let sb = dumpSectionValue "IP" (dumpIp cilState.ipStack) sb - let sb = dumpSectionValue "IIE" (sprintf "%O" cilState.iie) sb - let sb = dumpSectionValue "Initial EvaluationStack Size" (sprintf "%O" cilState.initialEvaluationStackSize) sb - let sb = Utils.PrettyPrinting.dumpDict "Level" id ipAndMethodBase2String id sb cilState.level - let stateDump = Print.Dump cilState.state - let sb = dumpSectionValue "State" stateDump sb - if sb.Length = 0 then "" else sb.ToString() + and [] cilState = + { + mutable ipStack : ipStack + // This field stores information about instruction prefix (for example, '.constrained' prefix) + mutable prefixContext : prefix list + // TODO: get rid of approximateLoc! + // This field stores only approximate information and can't be used for getting the precise location. Instead, use ipStack.Head + mutable approximateLoc : codeLocation + state : state + mutable stackArrays : pset + mutable errorReported : bool + mutable filterResult : term option + mutable iie : InsufficientInformationException option + mutable level : level + startingIP : instructionPointer + mutable initialEvaluationStackSize : uint32 + mutable stepsNumber : uint + mutable suspended : bool + mutable targets : Set + /// + /// All basic blocks visited by the state. + /// + mutable history : Set + /// + /// If the state is not isolated (produced during forward execution), Some of it's entry point method, else None. + /// + entryMethod : Method option + /// + /// Deterministic state id. + /// + internalId : uint + } + + static member CreateInitial (m : Method) (state : state) = + let ip = Instruction(0, m) + let approximateLoc = ip.ToCodeLocation() |> Option.get + { + ipStack = List.singleton ip + prefixContext = List.empty + approximateLoc = approximateLoc + state = state + stackArrays = PersistentSet.empty + errorReported = false + filterResult = None + iie = None + level = PersistentDict.empty + startingIP = ip + initialEvaluationStackSize = 0u + stepsNumber = 0u + suspended = false + targets = Set.empty + history = Set.empty + entryMethod = Some m + internalId = getNextStateId() + } + + member private x.ErrorReporter = lazy ErrorReporter(x) + + member x.IsIsolated with get() = x.entryMethod.IsNone + + member x.EntryMethod with get() = + if x.IsIsolated then invalidOp "Isolated state doesn't have an entry method" + x.entryMethod.Value + + member x.StartsFromMethodBeginning with get() = + match x.startingIP with + | Instruction (0, _) -> true + | _ -> false + + member x.SetCurrentTime time = x.state.currentTime <- time + + // -------------------- Exception and errors operations -------------------- + + member x.SetException exc = + x.state.exceptionsRegister <- x.state.exceptionsRegister.Tail.Push exc + + member x.IsUnhandledException with get() = + match x.state.exceptionsRegister.Peek with + | Unhandled _ -> true + | _ -> false + + member x.IsUnhandledExceptionOrError with get() = + match x.state.exceptionsRegister.Peek with + | Unhandled _ -> true + | _ -> x.errorReported + + member x.HasReportedError with get() = x.errorReported + member x.ReportError() = x.errorReported <- true + + member x.IsStoppedByException with get() = + match x.CurrentIp with + | EmptySearchingForHandler -> true + | _ -> false + + member x.HasRuntimeExceptionOrError with get() = + match x.state.exceptionsRegister.Peek with + | _ when x.errorReported -> true + | Unhandled(_, isRuntime, _) -> isRuntime + | _ -> false + + member x.IsIIEState with get() = Option.isSome x.iie + + member x.SetIIE (e : InsufficientInformationException) = + x.iie <- Some e + + member x.IsExecutable with get() = + match x.ipStack with + | [] -> __unreachable__() + | [ Exit _ ] -> false + | _ -> true + + member x.IsStopped with get() = + x.IsIIEState || x.IsStoppedByException || not x.IsExecutable + + member x.NewExceptionRegister() = + x.state.exceptionsRegister <- x.state.exceptionsRegister.Push NoException + + member x.PopExceptionRegister() = + x.state.exceptionsRegister <- x.state.exceptionsRegister.Tail + + member x.ToUnhandledException() = + x.state.exceptionsRegister <- x.state.exceptionsRegister.TransformToUnhandled() + + member x.ToCaughtException() = + x.state.exceptionsRegister <- x.state.exceptionsRegister.TransformToCaught() + + member x.MoveDownExceptionRegister() = + let elem, rest = x.state.exceptionsRegister.Pop() + x.state.exceptionsRegister <- rest.Tail.Push elem + + // -------------------- Instruction pointer operations -------------------- + + member x.CurrentIp with get() = + match x.ipStack with + | [] -> internalfail "currentIp: 'IP' stack is empty" + | h :: _ -> h + + // Obtaining exploring method + member x.CurrentMethod with get() = x.CurrentIp.ForceMethod() + + member x.CurrentOffset with get() = x.CurrentIp.Offset + + member x.PushToIp (ip : instructionPointer) = + let loc = x.approximateLoc + match ip.ToCodeLocation() with + | Some loc' when loc'.method.HasBody -> + x.approximateLoc <- loc' + Application.addCallEdge loc loc' + | _ -> () + x.ipStack <- ip :: x.ipStack + + member x.SetCurrentIp (ip : instructionPointer) = + x.MoveCodeLoc ip + assert(List.isEmpty x.ipStack |> not) + x.ipStack <- ip :: List.tail x.ipStack + + member x.SetCurrentIpSafe (ip : instructionPointer) = + let ip = x.CurrentIp.ChangeInnerIp ip + x.SetCurrentIp ip + + member x.ReplaceLastIp (ip : instructionPointer) = + let newIp = x.CurrentIp.ReplaceRecIp ip + x.SetCurrentIp newIp + + member x.MarkExit (m : Method) = + match x.ipStack with + | ip :: ips -> + assert(ip.Method = Some m) + x.ipStack <- (Exit m) :: ips + | [] -> __unreachable__() + + member x.TryGetFilterIp with get() = x.ipStack |> List.tryFind (fun ip -> ip.IsInFilter) + + member x.TryCurrentLoc with get() = x.CurrentIp.ToCodeLocation() + + member x.CurrentLoc with get() = x.TryCurrentLoc |> Option.get + + member x.StartingLoc with get() = x.startingIP.ToCodeLocation() |> Option.get + + member x.CodeLocations with get() = + x.ipStack + |> List.takeWhile (fun ip -> not ip.IsFilter) + |> List.map (fun ip -> ip.ForceCodeLocation()) + + member private x.MoveCodeLoc (ip : instructionPointer) = + match ip.ToCodeLocation() with + | Some loc when loc.method.HasBody -> x.approximateLoc <- loc + | _ -> () + + // -------------------- Prefix context operations -------------------- + + member x.PushPrefixContext (prefix : prefix) = + x.prefixContext <- prefix :: x.prefixContext + + member x.PopPrefixContext() = + match x.prefixContext with + | prefix :: context -> + x.prefixContext <- context + Some prefix + | _ -> None + + // -------------------- Stack arrays operations -------------------- + + member x.AddStackArray (address : concreteHeapAddress) = + x.stackArrays <- PersistentSet.add x.stackArrays address + + member x.IsStackArray ref = + match ref.term with + | HeapRef({term = ConcreteHeapAddress address}, _) + | Ref(ArrayIndex({term = ConcreteHeapAddress address}, _, _)) + | Ptr(HeapLocation({term = ConcreteHeapAddress address}, _), _, _) -> + PersistentSet.contains address x.stackArrays + | _ -> false + + // -------------------- Level operations -------------------- + + member x.IncrementLevel codeLocation = + let oldValue = PersistentDict.tryFind x.level codeLocation |> Option.defaultValue 0u + x.level <- PersistentDict.add codeLocation (oldValue + 1u) x.level + + member x.DecrementLevel codeLocation = + let oldValue = PersistentDict.tryFind x.level codeLocation + match oldValue with + | Some value when value = 1u -> + x.level <- PersistentDict.remove codeLocation x.level + | Some value when value > 0u -> + x.level <- PersistentDict.add codeLocation (value - 1u) x.level + | _ -> () + + member x.ViolatesLevel maxBound = + match x.TryCurrentLoc with + | Some currLoc when PersistentDict.contains currLoc x.level -> + x.level[currLoc] >= maxBound + | _ -> false + + member x.LevelOfLocation loc = + if PersistentDict.contains loc x.level then x.level[loc] else 0u + + member x.Level with get() = Level.levelToUnsignedInt x.level + + // -------------------- History operations -------------------- + + member x.AddLocationToHistory (loc : codeLocation) = + x.history <- Set.add loc x.history + + // -------------------- EvaluationStack operations -------------------- + + member x.ClearEvaluationStackLastFrame() = + x.state.evaluationStack <- EvaluationStack.ClearActiveFrame x.state.evaluationStack + + member x.Push v = + match v.term with + | Nop -> internalfail "pushing 'NOP' value onto evaluation stack" + | _ -> x.state.evaluationStack <- EvaluationStack.Push v x.state.evaluationStack + + member x.PushMany vs = + if List.contains (Nop()) vs then + internalfail "pushing 'NOP' value onto evaluation stack" + x.state.evaluationStack <- EvaluationStack.PushMany vs x.state.evaluationStack + + member x.Peek() = EvaluationStack.Pop x.state.evaluationStack |> fst + + member x.Peek2() = + let stack = x.state.evaluationStack + let arg2, stack = EvaluationStack.Pop stack + let arg1, _ = EvaluationStack.Pop stack + arg2, arg1 + + member x.Pop() = + let v, evaluationStack = EvaluationStack.Pop x.state.evaluationStack + x.state.evaluationStack <- evaluationStack + v + + member x.Pop2() = + let arg2 = x.Pop() + let arg1 = x.Pop() + arg2, arg1 + + member x.Pop3() = + let arg3 = x.Pop() + let arg2 = x.Pop() + let arg1 = x.Pop() + arg3, arg2, arg1 + + member x.PopMany (count : int) = + let parameters, evaluationStack = EvaluationStack.PopMany count x.state.evaluationStack + x.state.evaluationStack <- evaluationStack + parameters + + member x.PushNewObjForValueTypes() = + let ref = x.Pop() + let value = Memory.Read x.state ref + x.Push value + + // -------------------- Filter result operations -------------------- + + member x.SetFilterResult (value : term) = + x.filterResult <- Some value + + member x.ClearFilterResult() = + x.filterResult <- None + + // -------------------- Targets operations -------------------- + + member x.AddTarget target = + let prev = x.targets + x.targets <- Set.add target prev + prev.Count <> x.targets.Count + + member x.RemoveTarget target = + let prev = x.targets + x.targets <- Set.remove target prev + prev.Count <> x.targets.Count + + member x.ClearTargets() = + x.targets <- Set.empty + + // -------------------- Memory interaction -------------------- + + member x.PopFrame() = + Memory.PopFrame x.state + let ip = List.tail x.ipStack + x.ipStack <- ip + assert(EvaluationStack.FramesCount x.state.evaluationStack = Memory.CallStackSize x.state) + match ip with + | ip :: _ -> x.MoveCodeLoc ip + | [] -> () + + member x.Read ref = + Memory.ReadUnsafe x.ErrorReporter.Value x.state ref + + member x.ReadField term field = + Memory.ReadFieldUnsafe x.ErrorReporter.Value x.state term field + + member x.ReadIndex term index valueType = + Memory.ReadArrayIndexUnsafe x.ErrorReporter.Value x.state term index valueType + + member x.Write ref value = + let states = Memory.WriteUnsafe x.ErrorReporter.Value x.state ref value + List.map x.ChangeState states + + member x.WriteClassField ref field value = + let states = Memory.WriteClassFieldUnsafe x.ErrorReporter.Value x.state ref field value + List.map x.ChangeState states + + member x.WriteStructField term field value = + Memory.WriteStructFieldUnsafe x.ErrorReporter.Value x.state term field value + + member x.WriteIndex term index value valueType = + let states = Memory.WriteArrayIndexUnsafe x.ErrorReporter.Value x.state term index value valueType + List.map x.ChangeState states + + // -------------------------- Branching -------------------------- + + member x.GuardedApplyCIL term (f : cilState -> term -> ('a list -> 'b) -> 'b) (k : 'a list -> 'b) = + GuardedStatedApplyk + (fun state term k -> f (x.ChangeState state) term k) + x.state term id (List.concat >> k) + + member x.StatedConditionalExecutionCIL conditionInvocation thenBranch elseBranch k = + let clone = { x with state = x.state } + let mkCilState state' = + if LanguagePrimitives.PhysicalEquality state' x.state then x + else clone.Copy(state') + StatedConditionalExecution x.state conditionInvocation + (fun state k -> thenBranch (mkCilState state) k) + (fun state k -> elseBranch (mkCilState state) k) + (fun x y -> [x; y]) + (List.concat >> k) + + member x.BranchOnNullCIL term thenBranch elseBranch k = + x.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference term, state)) + thenBranch + elseBranch + k + + // -------------------- Changing inner state -------------------- + + member private x.DumpSectionValue section value (sb : StringBuilder) = + let sb = Utils.PrettyPrinting.dumpSection section sb + Utils.PrettyPrinting.appendLine sb value + + member private x.DumpIpStack (ipStack : ipStack) = + List.fold (fun acc entry -> $"{acc}\n{entry}") "" ipStack + + member private x.Dump() : string = + let sb = StringBuilder() + let sb = x.DumpSectionValue "Starting ip" $"{x.startingIP}" sb + let sb = x.DumpSectionValue "IP" (x.DumpIpStack x.ipStack) sb + let sb = x.DumpSectionValue "IIE" $"{x.iie}" sb + let sb = x.DumpSectionValue "Initial EvaluationStack Size" $"{x.initialEvaluationStackSize}" sb + let sb = Utils.PrettyPrinting.dumpDict "Level" id toString id sb x.level + let sb = x.DumpSectionValue "State" (Print.Dump x.state) sb + if sb.Length = 0 then "" else sb.ToString() + + // -------------------- Changing inner state -------------------- + + member x.Copy(state : state) = + { x with state = state } + + // This function copies cilState, instead of mutation + member x.ChangeState state' : cilState = + if LanguagePrimitives.PhysicalEquality state' x.state then x + else x.Copy(state') + + // -------------------- Steps number -------------------- + + member x.IncrementStepsNumber() = + x.stepsNumber <- x.stepsNumber + 1u + + // -------------------- Overriding methods -------------------- + + override x.ToString() = System.String.Empty + + interface IGraphTrackableState with + override this.CodeLocation = this.approximateLoc + override this.CallStack = Memory.StackTrace this.state.stack |> List.map (fun m -> m :?> Method) + +module CilStateOperations = + open CilState + + type cilStateComparer() = + interface IComparer with + override _.Compare(x : cilState, y : cilState) = + x.GetHashCode().CompareTo(y.GetHashCode()) + + let mkCilStateHashComparer = cilStateComparer() diff --git a/VSharp.SILI/InstructionPointer.fs b/VSharp.SILI/InstructionPointer.fs index bd0eb90fc..ef1ba8d61 100644 --- a/VSharp.SILI/InstructionPointer.fs +++ b/VSharp.SILI/InstructionPointer.fs @@ -5,64 +5,59 @@ open MethodBody open System.Reflection.Emit [] -type ip = +type instructionPointer = | Exit of Method | Instruction of offset * Method - | Leave of ip * ExceptionHandlingClause list * offset * Method + | Leave of instructionPointer * ExceptionHandlingClause list * offset * Method // current observing clauses; observed clauses; frames to observe catch clause; frames to observe finally clauses | SearchingForHandler of ExceptionHandlingClause list option * ExceptionHandlingClause list * codeLocation list * codeLocation list // ip of filter function; handler offset; previous searching handler information - | InFilterHandler of ip * offset * ExceptionHandlingClause list * ExceptionHandlingClause list * codeLocation list * codeLocation list + | InFilterHandler of instructionPointer * offset * ExceptionHandlingClause list * ExceptionHandlingClause list * codeLocation list * codeLocation list // ``None'' -- we are seeking for next finally or fault handler, ``Some _'' -- we are executing handler; // current observing clauses; last clauses to observe; last location to check last clauses; // rest frames of possible handlers; starting code location of handler if one was valid - | SecondBypass of ip option * ExceptionHandlingClause list option * ExceptionHandlingClause list * codeLocation option * codeLocation list * codeLocation option + | SecondBypass of instructionPointer option * ExceptionHandlingClause list option * ExceptionHandlingClause list * codeLocation option * codeLocation list * codeLocation option with - override x.Equals y = - match y with - | :? ip as y -> - match x, y with - | Exit mx, Exit my -> mx = my - | Instruction(ix, mx), Instruction(iy, my) -> ix = iy && mx.Equals(my) - | Leave(ix, _, ipx, mx), Leave(iy, _, ipy, my) -> ix = iy && ipx.Equals(ipy) && mx.Equals(my) - | SearchingForHandler(handlersToSearch1, finallyEhcs1, toObserve1, framesToPop1), SearchingForHandler(handlersToSearch2, finallyEhcs2, toObserve2, framesToPop2) -> - toObserve1 = toObserve2 && framesToPop1 = framesToPop2 && finallyEhcs1 = finallyEhcs2 && handlersToSearch1 = handlersToSearch2 - | InFilterHandler(ip1, offset1, ehcs1, finallyEhcs1, toObserve1, toPop1), InFilterHandler(ip2, offset2, ehcs2, finallyEhcs2, toObserve2, toPop2) -> - ip1.Equals(ip2) && offset1.Equals(offset2) && toObserve1.Equals(toObserve2) && finallyEhcs1.Equals(finallyEhcs2) && toPop1.Equals(toPop2) && ehcs1.Equals(ehcs2) - | SecondBypass(ip1, ehcs1, lastEhcs1, loc, toFinalize1, location1), SecondBypass(ip2, ehcs2, lastEhcs2, method2, toFinalize2, location2) -> - ip1.Equals(ip2) && loc.Equals(method2) && ehcs1.Equals(ehcs2) && lastEhcs1.Equals(lastEhcs2) && toFinalize1.Equals(toFinalize2) && location1 = location2 - | _ -> false - | _ -> false - override x.GetHashCode() = x.ToString().GetHashCode() - - override x.ToString() = - match x with - | Instruction(offset, m) -> sprintf "{Instruction = %s; M = %s}" ((int offset).ToString("X")) m.FullName - | Exit m -> $"{{Exit from M = %s{m.FullName}}}" - | Leave(ip, _, offset, m) -> $"{{M = %s{m.FullName}; Leaving to %d{offset}\n;Currently in {ip}}}" - | SearchingForHandler(ehcs, finallyEhcs, toObserve, checkFinally) -> - $"SearchingForHandler({ehcs}, {finallyEhcs}, {toObserve}, {checkFinally})" - | SecondBypass(ip, ehcs, lastEhcs, method, restFrames, handler) -> - $"SecondBypass({ip}, {ehcs}, {lastEhcs}, {method}, {restFrames}, {handler})" - | InFilterHandler(ip, offset, ehcs, finallyEhcs, codeLocations, locations) -> - $"InFilterHandler({ip}, {offset}, {ehcs}, {finallyEhcs}, {codeLocations}, {locations}" - -and ipStack = ip list - -type level = pdict - -module IpOperations = - let exit m = Exit m - - let instruction m i = Instruction(i, m) - - let leave ip ehcs dst m = + static member internal CreateLeave ip ehcs dst m = match ip with | Exit _ -> internalfail "Leave over Exit!" | _ -> Leave(ip, ehcs, dst, m) - let moveInstruction (newOffset : offset) ip = + static member internal EmptySearchingForHandler = + SearchingForHandler(Some List.empty, List.empty, List.empty, List.empty) + + member internal x.ChangeInnerIp newIp = + match x with + | Leave(ip, e, i, m) -> + Leave(ip.ChangeInnerIp newIp, e, i, m) + | InFilterHandler(ip, offset, e, f, lc, l) -> + InFilterHandler(ip.ChangeInnerIp newIp, offset, e, f, lc, l) + | SecondBypass(Some ip, ehcs, lastBlocks, loc, cl, ftp) -> + SecondBypass(Some (ip.ChangeInnerIp newIp), ehcs, lastBlocks, loc, cl, ftp) + | _ -> newIp + + member private x.IsNonRecIp with get() = + match x with + | Instruction _ + | Exit _ + | SearchingForHandler _ + | SecondBypass(None, _, _, _, _, _) -> true + | _ -> false + + member internal x.ReplaceRecIp newIp = + match x with + | InFilterHandler(ip, _, _, _, _, _) + | Leave(ip, _, _, _) + | SecondBypass(Some ip, _, _, _, _, _) when ip.IsNonRecIp -> newIp + | InFilterHandler(ip, offset, e, f, lc, l) -> + InFilterHandler(ip.ReplaceRecIp newIp, offset, e, f, lc, l) + | Leave(ip, e, i, m) -> Leave(ip.ReplaceRecIp newIp, e, i, m) + | SecondBypass(Some ip, ehcs, lastBlocks, lastLocation, locations, handlerLoc) -> + SecondBypass(Some (ip.ReplaceRecIp newIp), ehcs, lastBlocks, lastLocation, locations, handlerLoc) + | _ -> newIp + + member internal x.MoveInstruction (newOffset : offset) = let rec helper (newOffset : offset) ip k = match ip with | Instruction(_, m) -> Instruction(newOffset, m) |> k @@ -74,22 +69,24 @@ module IpOperations = SecondBypass(Some ip', ehcs, lastEhcs, m, toPop, handler) |> k) | Leave(ip, ehcs, dst, m) -> helper newOffset ip (fun ip' -> - leave ip' ehcs dst m |> k) + instructionPointer.CreateLeave ip' ehcs dst m |> k) | SearchingForHandler _ -> internalfail "moveInstruction: SearchingForHandler is not implemented" | Exit _ -> __unreachable__() | _ -> __unreachable__() - helper newOffset ip id + helper newOffset x id - let rec offsetOf = function + member x.Offset with get() = + match x with | Exit _ -> None | Instruction(offset, _) -> Some offset - | Leave(ip, _, _, _) -> offsetOf ip + | Leave(ip, _, _, _) -> ip.Offset | SearchingForHandler _ -> None - | InFilterHandler(ip, _, _, _, _, _) -> offsetOf ip + | InFilterHandler(ip, _, _, _, _, _) -> ip.Offset | SecondBypass(None, _, _, _, _, _) -> None - | SecondBypass(Some ip, _, _, _, _, _) -> offsetOf ip + | SecondBypass(Some ip, _, _, _, _, _) -> ip.Offset - let rec methodOf = function + member internal x.Method with get() = + match x with | Exit m | Instruction(_, m) | Leave(_, _, _, m) -> Some m @@ -98,32 +95,74 @@ module IpOperations = | SearchingForHandler(_, _, _, codeLocations) -> let codeLoc = List.last codeLocations Some codeLoc.method - | InFilterHandler(ip, _, _, _, _, _) -> methodOf ip + | InFilterHandler(ip, _, _, _, _, _) -> ip.Method | SecondBypass(None, _, _, _, _, _) -> None - | SecondBypass(Some ip, _, _, _, _, _) -> methodOf ip + | SecondBypass(Some ip, _, _, _, _, _) -> ip.Method - let forceMethodOf ip = - match methodOf ip with + member x.ForceMethod() = + match x.Method with | Some method -> method - | None -> internalfail $"Getting current method: unexpected ip {ip}" + | None -> internalfail $"Getting current method: unexpected ip {x}" - let ip2codeLocation (ip : ip) = - match offsetOf ip, methodOf ip with + member x.ToCodeLocation() = + match x.Offset, x.Method with | None, _ -> None | Some offset, Some m -> let loc = {offset = offset; method = m} Some loc | _ -> __unreachable__() - let isFilter = function + member x.ForceCodeLocation() = + match x.Offset, x.Method with + | None, _ -> internalfail $"ForceCodeLocation: unable to get code location {x}" + | Some offset, Some m -> {offset = offset; method = m} + | _ -> __unreachable__() + + member x.IsFilter with get() = + match x with | InFilterHandler _ -> true | _ -> false - let rec ipIsInFilter ip = - match ip with + member x.IsInFilter with get() = + match x with | InFilterHandler _ -> true - | SecondBypass(Some ip, _, _, _, _, _) -> ipIsInFilter ip + | SecondBypass(Some ip, _, _, _, _, _) -> ip.IsInFilter + | _ -> false + + override x.Equals y = + match y with + | :? instructionPointer as y -> + match x, y with + | Exit mx, Exit my -> mx = my + | Instruction(ix, mx), Instruction(iy, my) -> ix = iy && mx.Equals(my) + | Leave(ix, _, ipx, mx), Leave(iy, _, ipy, my) -> ix = iy && ipx.Equals(ipy) && mx.Equals(my) + | SearchingForHandler(handlersToSearch1, finallyEhcs1, toObserve1, framesToPop1), SearchingForHandler(handlersToSearch2, finallyEhcs2, toObserve2, framesToPop2) -> + toObserve1 = toObserve2 && framesToPop1 = framesToPop2 && finallyEhcs1 = finallyEhcs2 && handlersToSearch1 = handlersToSearch2 + | InFilterHandler(ip1, offset1, ehcs1, finallyEhcs1, toObserve1, toPop1), InFilterHandler(ip2, offset2, ehcs2, finallyEhcs2, toObserve2, toPop2) -> + ip1.Equals(ip2) && offset1.Equals(offset2) && toObserve1.Equals(toObserve2) && finallyEhcs1.Equals(finallyEhcs2) && toPop1.Equals(toPop2) && ehcs1.Equals(ehcs2) + | SecondBypass(ip1, ehcs1, lastEhcs1, loc, toFinalize1, location1), SecondBypass(ip2, ehcs2, lastEhcs2, method2, toFinalize2, location2) -> + ip1.Equals(ip2) && loc.Equals(method2) && ehcs1.Equals(ehcs2) && lastEhcs1.Equals(lastEhcs2) && toFinalize1.Equals(toFinalize2) && location1 = location2 + | _ -> false | _ -> false + override x.GetHashCode() = x.ToString().GetHashCode() + + override x.ToString() = + match x with + | Instruction(offset, m) -> sprintf "{Instruction = %s; M = %s}" ((int offset).ToString("X")) m.FullName + | Exit m -> $"{{Exit from M = %s{m.FullName}}}" + | Leave(ip, _, offset, m) -> $"{{M = %s{m.FullName}; Leaving to %d{offset}\n;Currently in {ip}}}" + | SearchingForHandler(ehcs, finallyEhcs, toObserve, checkFinally) -> + $"SearchingForHandler({ehcs}, {finallyEhcs}, {toObserve}, {checkFinally})" + | SecondBypass(ip, ehcs, lastEhcs, method, restFrames, handler) -> + $"SecondBypass({ip}, {ehcs}, {lastEhcs}, {method}, {restFrames}, {handler})" + | InFilterHandler(ip, offset, ehcs, finallyEhcs, codeLocations, locations) -> + $"InFilterHandler({ip}, {offset}, {ehcs}, {finallyEhcs}, {codeLocations}, {locations}" + +and ipStack = instructionPointer list + +type level = pdict + +module IpOperations = let bypassShouldPopFrame bypassLocations locationToJump currentLoc = List.isEmpty bypassLocations |> not || @@ -131,9 +170,6 @@ module IpOperations = | Some loc -> loc.method <> currentLoc.method | None -> false - let emptySearchingForHandler = - SearchingForHandler(Some List.empty, List.empty, List.empty, List.empty) - let (|EndFinally|_|) = function | Instruction(offset, m) when parseInstruction m offset = OpCodes.Endfinally -> Some() | _ -> None @@ -157,7 +193,7 @@ module IpOperations = | SearchingForHandler(Some [], [], [], []) -> Some() | _ -> None - let isCallIp (ip : ip) = + let isCallIp (ip : instructionPointer) = match ip with | InstructionEndingIp(offset, m) -> let opCode = parseInstruction m offset @@ -181,3 +217,7 @@ module Level = let toString (lvl : level) = if isInf lvl then "inf" else lvl.ToString() + + let levelToUnsignedInt (lvl : level) = + // TODO: remove it when ``level'' subtraction would be generalized + PersistentDict.fold (fun acc _ v -> max acc v) 0u lvl diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index eef3f4992..212e8ece7 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -6,7 +6,7 @@ open System.Diagnostics open System.Reflection open System.Reflection.Emit open FSharpx.Collections -open CilStateOperations +open CilState open VSharp open VSharp.CSharpUtils open VSharp.Core @@ -90,13 +90,14 @@ module internal InstructionsSet = let castUnchecked typ term : term = Types.Cast term typ let ldc numberCreator t (m : Method) shiftedOffset (cilState : cilState) = let num = numberCreator m.ILBytes shiftedOffset - push (Concrete num t) cilState + cilState.Push (Concrete num t) let ldloc numberCreator (m : Method) shiftedOffset (cilState : cilState) = let index = numberCreator m.ILBytes shiftedOffset let reference = referenceLocalVariable index m let term = Memory.Read cilState.state reference - push term cilState + cilState.Push term + let ldarg numberCreator (m : Method) shiftedOffset (cilState : cilState) = let argumentIndex = numberCreator m.ILBytes shiftedOffset let arg = @@ -111,7 +112,8 @@ module internal InstructionsSet = | Some _, true -> let term = getArgTerm (argumentIndex - 1) m Memory.Read state term - push arg cilState + cilState.Push arg + let ldarga numberCreator (m : Method) shiftedOffset (cilState : cilState) = let argumentIndex = numberCreator m.ILBytes shiftedOffset let address = @@ -120,48 +122,51 @@ module internal InstructionsSet = | None -> getArgTerm argumentIndex m | Some _ when argumentIndex = 0 -> internalfail "can't load address of ``this''" | Some _ -> getArgTerm (argumentIndex - 1) m - push address cilState + cilState.Push address let stloc numberCreator (m : Method) shiftedOffset (cilState : cilState) = let variableIndex = numberCreator m.ILBytes shiftedOffset - let right = pop cilState + let right = cilState.Pop() let location = referenceLocalVariable variableIndex m let typ = TypeOfLocation location let value = Types.Cast right typ - write cilState location value + cilState.Write location value + let private simplifyConditionResult state res k = if Contradicts state !!res then k (True()) elif Contradicts state res then k (False()) else k res + let performCILUnaryOperation op (cilState : cilState) = - let x = pop cilState + let x = cilState.Pop() API.PerformUnaryOperation op x (fun interimRes -> - let res = if Terms.TypeOf x |> Types.IsBool then simplifyConditionResult cilState.state interimRes id else interimRes - push res cilState) + let isBool = Terms.TypeOf x |> Types.IsBool + let res = if isBool then simplifyConditionResult cilState.state interimRes id else interimRes + cilState.Push res) let performCILBinaryOperation op operand1Transform operand2Transform resultTransform (cilState : cilState) = - let arg2, arg1 = pop2 cilState + let arg2, arg1 = cilState.Pop2() operand1Transform arg1 (fun arg1 -> operand2Transform arg2 (fun arg2 -> API.PerformBinaryOperation op arg1 arg2 (fun interimRes -> resultTransform interimRes (fun res -> - push res cilState)))) + cilState.Push res)))) + let standardPerformBinaryOperation op = performCILBinaryOperation op idTransformation idTransformation idTransformation + let dup (cilState : cilState) = - let x = pop cilState - push x cilState - push x cilState + let x = cilState.Pop() + cilState.Push x + cilState.Push x let ret (m : Method) (cilState : cilState) = let resultTyp = m.ReturnType if resultTyp <> typeof then - let res = pop cilState + let res = cilState.Pop() let castedResult = Types.Cast res resultTyp - push castedResult cilState - match cilState.ipStack with - | _ :: ips -> cilState.ipStack <- (Exit m) :: ips - | [] -> __unreachable__() + cilState.Push castedResult + cilState.MarkExit m let transform2BooleanTerm pc (term : term) = let check term = @@ -187,12 +192,13 @@ module internal InstructionsSet = performCILBinaryOperation op operand1Transformation operand2Transformation (simplifyConditionResult cilState.state) cilState let ceq (cilState : cilState) = - let y, x = peek2 cilState + let y, x = cilState.Peek2() let transform = if TypeUtils.isBool x || TypeUtils.isBool y then fun t k -> k (transform2BooleanTerm cilState.state.pc t) else idTransformation binaryOperationWithBoolResult OperationType.Equal transform transform cilState + let starg numCreator (m : Method) offset (cilState : cilState) = let argumentIndex = numCreator m.ILBytes offset let argTerm = @@ -201,30 +207,35 @@ module internal InstructionsSet = | None -> getArgTerm argumentIndex m | Some this when argumentIndex = 0 -> this | Some _ -> getArgTerm (argumentIndex - 1) m - let value = pop cilState + let value = cilState.Pop() let states = Memory.Write cilState.state argTerm value - states |> List.map (changeState cilState) + states |> List.map cilState.ChangeState + let brcommon condTransform (m : Method) (offset : offset) (cilState : cilState) = - let cond = pop cilState - let oldIp = currentIp cilState + let cond = cilState.Pop() + let oldIp = cilState.CurrentIp let ipThen, ipElse = match conditionalBranchTarget m offset with - | offsetThen, [offsetElse] -> moveInstruction offsetThen oldIp, moveInstruction offsetElse oldIp + | offsetThen, [offsetElse] -> oldIp.MoveInstruction offsetThen, oldIp.MoveInstruction offsetElse | _ -> __unreachable__() - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (condTransform <| transform2BooleanTerm state.pc cond, state)) - (fun cilState k -> setCurrentIp ipThen cilState; k [cilState]) - (fun cilState k -> setCurrentIp ipElse cilState; k [cilState]) + (fun cilState k -> cilState.SetCurrentIp ipThen; k [cilState]) + (fun cilState k -> cilState.SetCurrentIp ipElse; k [cilState]) id + let brfalse = brcommon id let brtrue = brcommon (!!) + let applyAndBranch additionalFunction brtrueFunction (m : Method) offset (cilState : cilState) = additionalFunction cilState brtrueFunction m offset cilState + let boolToInt b = BranchExpressions (fun k -> k b) (fun k -> k <| TypeUtils.Int32.One()) (fun k -> k <| TypeUtils.Int32.Zero()) id + let bitwiseOrBoolOperation bitwiseOp boolOp (cilState : cilState) = - let arg2, arg1 = peek2 cilState + let arg2, arg1 = cilState.Peek2() let typ1, typ2 = TypeOf arg1, TypeOf arg2 match typ1, typ2 with | Types.Bool, Types.Bool -> @@ -233,10 +244,10 @@ module internal InstructionsSet = standardPerformBinaryOperation bitwiseOp cilState // Bitwise operations for pointers are pointless (unless result will be checked on null), so returning pointer | _ when TypeUtils.isPointer typ1 -> - pop cilState |> ignore + cilState.Pop() |> ignore | _ when TypeUtils.isPointer typ2 -> - pop2 cilState |> ignore - push arg2 cilState + cilState.Pop2() |> ignore + cilState.Push arg2 | Types.Bool, typ2 when TypeUtils.isIntegral typ2 -> let newArg1 = boolToInt arg1 performCILBinaryOperation bitwiseOp (fun _ k -> k newArg1) idTransformation idTransformation cilState @@ -244,20 +255,21 @@ module internal InstructionsSet = let newArg2 = boolToInt arg2 performCILBinaryOperation bitwiseOp idTransformation (fun _ k -> k newArg2) idTransformation cilState | typ1, typ2 -> internalfail $"unhandled case for bitwise operation {bitwiseOp} and types: {typ1} {typ2}" + let bitwiseOrBoolNot (cilState : cilState) = - let arg = peek cilState + let arg = cilState.Peek() let op = match TypeOf arg with | Types.Bool -> OperationType.LogicalNot | _ -> OperationType.BitwiseNot performCILUnaryOperation op cilState + let retrieveActualParameters (method : Method) (cilState : cilState) = let paramsNumber = method.Parameters.Length - let parameters, evaluationStack = EvaluationStack.PopMany paramsNumber cilState.state.evaluationStack + let parameters = cilState.PopMany paramsNumber let castParameter parameter (parInfo : ParameterInfo) = if method.IsDelegateConstructor && TypeUtils.isPointer parInfo.ParameterType then parameter else Types.Cast parameter parInfo.ParameterType - setEvaluationStack evaluationStack cilState Seq.map2 castParameter (List.rev parameters) method.Parameters |> List.ofSeq let makeUnsignedInteger term k = @@ -266,53 +278,63 @@ module internal InstructionsSet = | t when t = typeof || t = typeof -> k term | t when TypeUtils.isIntegral t -> k <| Types.Cast term (TypeUtils.signedToUnsigned t) // no specs found about overflows | _ -> k term + let performUnsignedIntegerOperation op (cilState : cilState) = - let arg2, arg1 = peek2 cilState + let arg2, arg1 = cilState.Peek2() if TypeUtils.isIntegralTerm arg1 && TypeUtils.isIntegralTerm arg2 then performCILBinaryOperation op makeUnsignedInteger makeUnsignedInteger idTransformation cilState - else internalfailf "arguments for %O are not Integers!" op + else internalfailf $"arguments for {op} are not Integers!" + let ldstr (m : Method) offset (cilState : cilState) = let stringToken = NumberCreator.extractInt32 m.ILBytes (offset + Offset.from OpCodes.Ldstr.Size) let string = m.Module.ResolveString stringToken let reference = Memory.AllocateString string cilState.state - push reference cilState + cilState.Push reference + let allocateValueTypeInHeap v (cilState : cilState) = let address = Memory.BoxValueType cilState.state v - push address cilState - let ldnull (cilState : cilState) = push (NullRef typeof) cilState + cilState.Push address + + let ldnull (cilState : cilState) = cilState.Push (NullRef typeof) + let convu (cilState : cilState) = - let ptr = pop cilState |> MakeUIntPtr - push ptr cilState + let ptr = cilState.Pop() |> MakeUIntPtr + cilState.Push ptr + let convi (cilState : cilState) = - let ptr = pop cilState |> MakeIntPtr - push ptr cilState + let ptr = cilState.Pop() |> MakeIntPtr + cilState.Push ptr + let castTopOfOperationalStack targetType (cilState : cilState) = - let t = pop cilState + let t = cilState.Pop() let termForStack = Types.Cast t targetType - push termForStack cilState + cilState.Push termForStack + let ldloca numberCreator (m : Method) shiftedOffset (cilState : cilState) = let index = numberCreator m.ILBytes shiftedOffset let term = referenceLocalVariable index m - push term cilState + cilState.Push term + let switch (m : Method) offset (cilState : cilState) = - let value = pop cilState + let value = cilState.Pop() let origPc = cilState.state.pc let value = makeUnsignedInteger value id - let checkOneCase (guard, newIp) cilState kRestCases = - StatedConditionalExecutionCIL cilState + let checkOneCase (guard, newIp) (cilState : cilState) kRestCases = + cilState.StatedConditionalExecutionCIL (fun state k -> k (guard, state)) - (fun cilState k -> setCurrentIp newIp cilState; k [cilState]) + (fun cilState k -> cilState.SetCurrentIp newIp; k [cilState]) (fun otherState k -> otherState.state.pc <- origPc // ignore pc because we always know that cases do not overlap kRestCases otherState k) - let oldIp = currentIp cilState + let oldIp = cilState.CurrentIp let fallThroughIp, restIps = match conditionalBranchTarget m offset with - | fall, rests -> moveInstruction fall oldIp, List.map (fun x -> moveInstruction x oldIp) rests + | fall, rests -> oldIp.MoveInstruction fall, List.map oldIp.MoveInstruction rests let casesAndOffsets = List.mapi (fun i offset -> value === MakeNumber i, offset) restIps let bound = makeUnsignedInteger (List.length restIps |> MakeNumber) id let fallThroughGuard = Arithmetics.GreaterOrEqualUn value bound Cps.List.foldrk checkOneCase cilState ((fallThroughGuard, fallThroughIp)::casesAndOffsets) (fun _ k -> k []) id + let ldtoken (m : Method) offset (cilState : cilState) = let memberInfo = resolveTokenFromMetadata m (offset + Offset.from OpCodes.Ldtoken.Size) let state = cilState.state @@ -322,79 +344,89 @@ module internal InstructionsSet = | :? Type as t -> Memory.ObjectToTerm state t.TypeHandle typeof | :? MethodInfo as mi -> Memory.ObjectToTerm state mi.MethodHandle typeof | _ -> internalfailf "Could not resolve token" - push res cilState + cilState.Push res + let ldftn (m : Method) offset (cilState : cilState) = let methodInfo = resolveMethodFromMetadata m (offset + Offset.from OpCodes.Ldftn.Size) let methodPtr = Terms.Concrete methodInfo (methodInfo.GetType()) - push methodPtr cilState + cilState.Push methodPtr + let initobj (m : Method) offset (cilState : cilState) = - let targetAddress = pop cilState + let targetAddress = cilState.Pop() let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Initobj.Size) let states = Memory.Write cilState.state targetAddress (Memory.DefaultOf typ) - states |> List.map (changeState cilState) + List.map cilState.ChangeState states let clt = binaryOperationWithBoolResult OperationType.Less idTransformation idTransformation + let cgt = binaryOperationWithBoolResult OperationType.Greater idTransformation idTransformation + let cltun = binaryOperationWithBoolResult OperationType.Less_Un makeUnsignedInteger makeUnsignedInteger + let bgeHelper (cilState : cilState) = - let arg1, arg2 = peek2 cilState + let arg1, arg2 = cilState.Peek2() let typ1, typ2 = Terms.TypeOf arg1, Terms.TypeOf arg2 if Types.isIntegral typ1 && Types.isIntegral typ2 then clt cilState elif Types.IsReal typ1 && Types.IsReal typ2 then cltun cilState else __notImplemented__() + let isinst (m : Method) offset (cilState : cilState) = - let object = pop cilState + let object = cilState.Pop() let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Isinst.Size) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference object, state)) - (fun cilState k -> push (NullRef typeof) cilState; k [cilState]) + (fun cilState k -> cilState.Push (NullRef typeof); k [cilState]) (fun cilState k -> - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.IsCast cilState.state object typ, state)) - (fun cilState k -> push object cilState; k [cilState]) - (fun cilState k -> push (NullRef typeof) cilState; k [cilState]) + (fun cilState k -> cilState.Push object; k [cilState]) + (fun cilState k -> cilState.Push (NullRef typeof); k [cilState]) k) id + let cgtun (cilState : cilState) = - let arg2, arg1 = peek2 cilState + let arg2, arg1 = cilState.Peek2() if IsReference arg2 && IsReference arg1 then binaryOperationWithBoolResult OperationType.NotEqual idTransformation idTransformation cilState else binaryOperationWithBoolResult OperationType.Greater_Un makeUnsignedInteger makeUnsignedInteger cilState + let sizeofInstruction (m : Method) offset (cilState : cilState) = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Sizeof.Size) let size = Types.SizeOf typ - push (MakeNumber size) cilState + cilState.Push (MakeNumber size) + let endfilter (cilState : cilState) = - let value, newStack = EvaluationStack.Pop cilState.state.evaluationStack - setEvaluationStack newStack cilState - popExceptionRegister cilState - cilState.filterResult <- Some value + let value = cilState.Pop() + cilState.PopExceptionRegister() + cilState.SetFilterResult value + let endfinally _ = // Should be handled in makeStep function __unreachable__() + let br (m : Method) offset (cilState : cilState) = - let oldIp = currentIp cilState - let newIp = moveInstruction (unconditionalBranchTarget m offset) oldIp - setCurrentIp newIp cilState + let oldIp = cilState.CurrentIp + let newIp = oldIp.MoveInstruction (unconditionalBranchTarget m offset) + cilState.SetCurrentIp newIp - let rec private constrainedImpl this method args cilState = + let rec private constrainedImpl this method args (cilState : cilState) = let state = cilState.state let thisType = TypeOfLocation this let isValueType = Types.IsValueType thisType let implements = lazy(Reflection.typeImplementsMethod thisType method) match this.term with | Ref _ when isValueType && implements.Value -> - push this cilState - pushMany args cilState + cilState.Push this + cilState.PushMany args | Ref _ when isValueType -> - let thisStruct = read cilState this + let thisStruct = cilState.Read this let heapRef = Memory.BoxValueType state thisStruct - push heapRef cilState - pushMany args cilState + cilState.Push heapRef + cilState.PushMany args | Ref _ -> - let this = read cilState this - push this cilState - pushMany args cilState + let this = cilState.Read this + cilState.Push this + cilState.PushMany args | Ptr(pointerBase, sightType, offset) -> match TryPtrToRef state pointerBase sightType offset with | Some(PrimitiveStackLocation _ as address) -> @@ -402,8 +434,8 @@ module internal InstructionsSet = constrainedImpl this method args cilState | _ -> // Inconsistent pointer, call will fork and filter this state - push this cilState - pushMany args cilState + cilState.Push this + cilState.PushMany args | _ -> internalfail $"Calling 'callvirt' with '.constrained': unexpected 'this' {this}" // '.constrained' is prefix, which is used before 'callvirt' or 'call' instruction @@ -422,55 +454,52 @@ module internal InstructionsSet = if method.IsStatic then // In this case, next called static method will be called via type 'typ' assert(List.isEmpty cilState.prefixContext) - pushPrefixContext cilState (Constrained typ) + cilState.PushPrefixContext (Constrained typ) else - let n = method.GetParameters().Length - let state = cilState.state - let args, evaluationStack = EvaluationStack.PopMany n state.evaluationStack - setEvaluationStack evaluationStack cilState - let thisForCallVirt = pop cilState + let args = method.GetParameters().Length |> cilState.PopMany + let thisForCallVirt = cilState.Pop() constrainedImpl thisForCallVirt method args cilState let localloc (cilState : cilState) = - let size = pop cilState + let size = cilState.Pop() let ref = Memory.AllocateVectorArray cilState.state size typeof match ref.term with | HeapRef({term = ConcreteHeapAddress concreteAddress} as address, t) -> assert(TypeUtils.isArrayType t) - addStackArray cilState concreteAddress + cilState.AddStackArray concreteAddress let arrayType = Types.SymbolicTypeToArrayType t let ref = Ref (ArrayIndex(address, [MakeNumber 0], arrayType)) - push ref cilState + cilState.Push ref | _ -> internalfail $"localloc: unexpected array reference {ref}" - let private fallThroughImpl stackSizeBefore newIp cilState = + let private fallThroughImpl stackSizeBefore newIp (cilState : cilState) = // if not constructing runtime exception - if not <| isUnhandledExceptionOrError cilState && Memory.CallStackSize cilState.state = stackSizeBefore then - setCurrentIp newIp cilState + if not cilState.IsUnhandledExceptionOrError && Memory.CallStackSize cilState.state = stackSizeBefore then + cilState.SetCurrentIp newIp - let fallThrough (m : Method) offset cilState op = - assert(not <| isUnhandledExceptionOrError cilState) + let fallThrough (m : Method) offset (cilState : cilState) op = + assert(not cilState.IsUnhandledExceptionOrError) let stackSizeBefore = Memory.CallStackSize cilState.state - let oldIp = currentIp cilState - let newIp = moveInstruction (fallThroughTarget m offset) oldIp + let oldIp = cilState.CurrentIp + let newIp = oldIp.MoveInstruction (fallThroughTarget m offset) op m offset cilState fallThroughImpl stackSizeBefore newIp cilState [cilState] - let forkThrough (m : Method) offset cilState op = - assert(not <| isUnhandledExceptionOrError cilState) + let forkThrough (m : Method) offset (cilState : cilState) op = + assert(not cilState.IsUnhandledExceptionOrError) let stackSizeBefore = Memory.CallStackSize cilState.state - let oldIp = currentIp cilState - let newIp = moveInstruction (fallThroughTarget m offset) oldIp + let oldIp = cilState.CurrentIp + let newIp = oldIp.MoveInstruction (fallThroughTarget m offset) let cilStates = op m offset cilState List.iter (fallThroughImpl stackSizeBefore newIp) cilStates cilStates - let readParameter (parameter : ParameterInfo) cilState = + let readParameter (parameter : ParameterInfo) (cilState : cilState) = if parameter.ParameterType.IsByRef then let key = ParameterKey parameter let stackRef = Memory.ReadLocalVariable cilState.state key - read cilState stackRef + cilState.Read stackRef else Memory.ReadArgument cilState.state parameter @@ -506,7 +535,7 @@ type ILInterpreter() as this = // ------------------------------- Environment interaction ------------------------------- - member x.InternalCall (originMethod : Method) (methodInfo : MethodInfo) (argsAndThis : term list) cilState k = + member x.InternalCall (originMethod : Method) (methodInfo : MethodInfo) (argsAndThis : term list) (cilState : cilState) k = let neededParams = methodInfo.GetParameters() |> Array.map (fun p -> p.ParameterType) let parameters : obj[] = match neededParams with @@ -535,18 +564,18 @@ type ILInterpreter() as this = k [cilState] | :? term as result when originMethod.HasNonVoidResult -> assert(result <> Nop()) - push result cilState + cilState.Push result k [cilState] | :? ((term * state) list) as results when originMethod.HasNonVoidResult -> - results |> List.map (fun (t, s) -> let s' = changeState cilState s in push t s'; s') |> k + results |> List.map (fun (t, s) -> let s' = cilState.ChangeState s in s'.Push t; s') |> k | :? ((term * state) list) as results -> - results |> List.map (fun (_, s) -> changeState cilState s) |> k + results |> List.map (fun (_, s) -> cilState.ChangeState s) |> k | :? (cilState list) as results -> k results | _ -> internalfail "Internal call should return 'term' or tuple 'term * state' or 'cilState list'!" member x.ConfigureErrorReporter errorReporter fatalErrorReporter = - configureErrorReporter errorReporter fatalErrorReporter + ErrorReporter.Configure errorReporter fatalErrorReporter member x.Raise createException (cilState : cilState) k = createException cilState @@ -562,7 +591,7 @@ type ILInterpreter() as this = assert(List.length lengths = List.length indices) let upperBoundsAndIndices = List.zip lengths indices List.fold checkOneBound (True()) upperBoundsAndIndices - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (checkArrayBounds lengths indices, state)) accessor (x.Raise x.IndexOutOfRangeException) @@ -576,15 +605,15 @@ type ILInterpreter() as this = x.AccessArray (accessor this dimension) cilState upperBound dimension id member x.NpeOrInvokeStatementCIL (cilState : cilState) (this : term) statement (k : cilState list -> 'a) = - let additionalCheck cilState k = - StatedConditionalExecutionCIL cilState + let additionalCheck (cilState : cilState) k = + cilState.StatedConditionalExecutionCIL (fun state k -> k (!!(IsBadRef this), state)) statement (fun cilState k -> ErrorReporter.ReportFatalError cilState "access violation" k []) k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (!!(IsNullReference this), state)) additionalCheck (x.Raise x.NullReferenceException) @@ -609,7 +638,7 @@ type ILInterpreter() as this = static member InitFunctionFrameCIL (cilState : cilState) (method : Method) this paramValues = Memory.InitFunctionFrame cilState.state method this (paramValues |> Option.bind (List.map Some >> Some)) - pushToIp (instruction method 0) cilState + Instruction(0, method) |> cilState.PushToIp static member CheckDisallowNullAttribute (method : Method) (argumentsOpt : term list option) (cilState : cilState) shouldReportError k = if not <| method.CheckAttributes then @@ -636,7 +665,7 @@ type ILInterpreter() as this = else let assumptions = conjunction assumptions let message = "DisallowNull attribute violation" - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (assumptions, state)) (fun cilState k -> k [cilState]) (fun cilState k -> @@ -651,8 +680,8 @@ type ILInterpreter() as this = let retValueAssumption = match method.ReturnParameter with | Some returnParameter when Attribute.IsDefined(returnParameter, typeof) -> - let res = pop cilState - push res cilState + let res = cilState.Pop() + cilState.Push res Some <| !!(IsNullReference res) | _ -> None @@ -667,7 +696,7 @@ type ILInterpreter() as this = else let assumptions = conjunction assumptions let message = "NotNull attribute violation" - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (assumptions, state)) (fun cilState k -> k [cilState]) (fun cilState k -> @@ -718,14 +747,15 @@ type ILInterpreter() as this = match t with | _ when t.IsGenericParameter -> whenInitializedCont cilState | _ -> - let typeInitialized = Memory.IsTypeInitialized cilState.state t + let state = cilState.state + let typeInitialized = Memory.IsTypeInitialized state t match typeInitialized with | True -> whenInitializedCont cilState | _ -> let fields = t.GetFields(Reflection.staticBindingFlags) let staticConstructor = t.GetConstructors(Reflection.staticBindingFlags) |> Array.tryHead Seq.iter (x.InitStaticFieldWithDefaultValue cilState.state) fields - Memory.InitializeStaticMembers cilState.state t + Memory.InitializeStaticMembers state t match staticConstructor with | Some cctor -> let cctor = Application.getMethod cctor @@ -733,9 +763,8 @@ type ILInterpreter() as this = | None -> whenInitializedCont cilState // TODO: make assumption ``Memory.withPathCondition state (!!typeInitialized)'' - member private x.ConcreteInvokeCatch (e : Exception) cilState isRuntime = - let state = cilState.state - let error = Memory.AllocateConcreteObject state e (e.GetType()) + member private x.ConcreteInvokeCatch (e : Exception) (cilState : cilState) isRuntime = + let error = Memory.AllocateConcreteObject cilState.state e (e.GetType()) x.CommonThrow cilState error isRuntime member private x.TryConcreteInvoke (method : Method) (args : term list) thisOption (cilState : cilState) = @@ -768,12 +797,12 @@ type ILInterpreter() as this = // When return type is interface or 'object', but real type is struct, // it should be boxed, so allocating it in heap let resultTerm = Memory.AllocateConcreteObject state result resultType - push resultTerm cilState + cilState.Push resultTerm | _ when returnType <> typeof -> // Case when method returns something let typ = TypeUtils.mostConcreteType resultType returnType let resultTerm = Memory.ObjectToTerm state result typ - push resultTerm cilState + cilState.Push resultTerm | _ when thisIsStruct && method.IsConstructor -> match thisOption, thisObj with | Some thisRef, Some thisObj -> @@ -797,7 +826,7 @@ type ILInterpreter() as this = x.InstantiateThisIfNeed cilState.state thisOption method let fallThroughCall (cilState : cilState) = - if isUnhandledExceptionOrError cilState |> not then + if not cilState.IsUnhandledExceptionOrError then ILInterpreter.FallThroughCall cilState cilState @@ -818,7 +847,7 @@ type ILInterpreter() as this = let mockMethod = ExternMockAndCall cilState.state method None args match mockMethod with | Some symVal -> - push symVal cilState + cilState.Push symVal | None -> () fallThroughCall cilState |> List.singleton |> k elif method.IsExternalMethod then @@ -845,10 +874,10 @@ type ILInterpreter() as this = ILInterpreter.CheckDisallowNullAttribute method (Some args) cilState true (fun states -> Cps.List.mapk inlineOrCall states (List.concat >> k)) - member x.CallAbstract targetType (ancestorMethod : MethodWithBody) (this : term) (arguments : term list) cilState k = + member x.CallAbstract targetType (ancestorMethod : MethodWithBody) (this : term) (arguments : term list) (cilState : cilState) k = let thisType = MostConcreteTypeOfRef cilState.state this let candidateTypes = ResolveCallVirt cilState.state this thisType ancestorMethod |> List.ofSeq - let invokeMock cilState k = + let invokeMock (cilState : cilState) k = let mockMethod = if ancestorMethod.DeclaringType.IsInterface then ancestorMethod @@ -857,14 +886,14 @@ type ILInterpreter() as this = let returnValue = MethodMockAndCall cilState.state mockMethod (Some this) arguments match returnValue with | Some symVal -> - push symVal cilState + cilState.Push symVal | None -> () - match tryCurrentLoc cilState with + match cilState.TryCurrentLoc with | Some loc -> // Moving ip to next instruction after mocking method result fallThrough loc.method loc.offset cilState (fun _ _ _ -> ()) |> k | _ -> __unreachable__() - let rec dispatch (candidates : symbolicType list) cilState k = + let rec dispatch (candidates : symbolicType list) (cilState : cilState) k = match candidates with | [MockType _] -> KeepOnlyMock cilState.state this @@ -873,7 +902,7 @@ type ILInterpreter() as this = let overridden = ancestorMethod.ResolveOverrideInType candidateType :?> Method if overridden.InCoverageZone || candidateType.IsAssignableTo targetType && targetType.Assembly = candidateType.Assembly then - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (API.Types.RefEqType state this candidateType, state)) (fun cilState k -> let this = Types.Cast this overridden.ReflectedType @@ -939,49 +968,49 @@ type ILInterpreter() as this = let leftBorder = Concrete min t // must save type info, because min is int64 let rightBorder = Concrete max t // must save type info, because max is int64 (leftBorder <<= term) &&& (term <<= rightBorder) - let t = pop cilState - StatedConditionalExecutionCIL cilState + let t = cilState.Pop() + cilState.StatedConditionalExecutionCIL (fun state k -> k (canCastWithoutOverflow t targetType, state)) (fun cilState k -> let castedResult = Types.Cast t targetType - push castedResult cilState + cilState.Push castedResult k [cilState]) (x.Raise x.OverflowException) id member private x.ConvOvfUn unsignedSightType targetType (cilState : cilState) = - let t = pop cilState + let t = cilState.Pop() let unsignedT = Types.Cast t unsignedSightType - push unsignedT cilState + cilState.Push unsignedT x.ConvOvf targetType cilState member private x.CommonCastClass (cilState : cilState) (term : term) (typ : Type) k = - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (IsNullReference term ||| Types.IsCast state term typ, state)) (fun cilState k -> - push (Types.Cast term typ) cilState + cilState.Push (Types.Cast term typ) k [cilState]) (x.Raise x.InvalidCastException) k member private x.CastClass (m : Method) offset (cilState : cilState) : cilState list = - let term = pop cilState + let term = cilState.Pop() let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Castclass.Size) x.CommonCastClass cilState term typ id member private x.PushNewObjResultOnEvaluationStack (cilState : cilState) reference (calledMethod : MethodBase) = let valueOnStack = - if calledMethod.DeclaringType.IsValueType then read cilState reference + if calledMethod.DeclaringType.IsValueType then cilState.Read reference else reference - push valueOnStack cilState + cilState.Push valueOnStack member x.RetrieveCalledMethodAndArgs (opCode : OpCode) (calledMethod : Method) (cilState : cilState) = let args = retrieveActualParameters calledMethod cilState let hasThis = calledMethod.HasThis && opCode <> OpCodes.Newobj - let this = if hasThis then pop cilState |> Some else None + let this = if hasThis then cilState.Pop() |> Some else None this, args member x.Call (m : Method) offset (cilState : cilState) = - let prefixContext = popPrefixContext cilState + let prefixContext = cilState.PopPrefixContext() let calledMethodBase = resolveMethodFromMetadata m (offset + Offset.from OpCodes.Call.Size) let calledMethod = match prefixContext with @@ -1056,7 +1085,7 @@ type ILInterpreter() as this = // NOTE: there is no need to initialize statics, because they were initialized before ``newobj'' execution let call (cilState : cilState) k = if ancestorMethod.IsVirtual && not ancestorMethod.IsFinal then - GuardedApplyCIL cilState this callVirtual k + cilState.GuardedApplyCIL this callVirtual k else let actualThis = Types.Cast this ancestorMethod.ReflectedType x.CommonCall ancestorMethod args (Some actualThis) cilState k @@ -1107,13 +1136,13 @@ type ILInterpreter() as this = let freshValue = Memory.DefaultOf typ Memory.AllocateTemporaryLocalVariable cilState.state -1 typ freshValue else Memory.AllocateDefaultClass cilState.state typ - push ref cilState + cilState.Push ref x.CommonCall constructorInfo args (Some ref) cilState id let k reference = - let newIp = moveInstruction (fallThroughTarget m offset) (currentIp cilState) - push reference cilState - setCurrentIp newIp cilState + let newIp = cilState.CurrentIp.MoveInstruction (fallThroughTarget m offset) + cilState.Push reference + cilState.SetCurrentIp newIp [cilState] if constructorInfo.IsDelegateConstructor then @@ -1127,7 +1156,7 @@ type ILInterpreter() as this = else blockCase cilState) member x.LdsFld addressNeeded (m : Method) offset (cilState : cilState) = - let newIp = moveInstruction (fallThroughTarget m offset) (currentIp cilState) + let newIp = cilState.CurrentIp.MoveInstruction (fallThroughTarget m offset) let fieldInfo = resolveFieldFromMetadata m (offset + Offset.from OpCodes.Ldsfld.Size) assert fieldInfo.IsStatic let declaringType = fieldInfo.DeclaringType @@ -1137,61 +1166,61 @@ type ILInterpreter() as this = if addressNeeded && not (TypeUtils.isImplementationDetails declaringType) then StaticField(declaringType, fieldId) |> Ref else Memory.ReadStaticField cilState.state declaringType fieldId - push value cilState - setCurrentIp newIp cilState + cilState.Push value + cilState.SetCurrentIp newIp [cilState]) member private x.StsFld (m : Method) offset (cilState : cilState) = - let newIp = moveInstruction (fallThroughTarget m offset) (currentIp cilState) // TODO: remove this copy-paste + let newIp = cilState.CurrentIp.MoveInstruction (fallThroughTarget m offset) // TODO: remove this copy-paste let fieldInfo = resolveFieldFromMetadata m (offset + Offset.from OpCodes.Stsfld.Size) assert fieldInfo.IsStatic x.InitializeStatics cilState fieldInfo.DeclaringType (fun cilState -> let declaringType = fieldInfo.DeclaringType let fieldId = Reflection.wrapField fieldInfo - let value = pop cilState + let value = cilState.Pop() let fieldType = fieldInfo.FieldType let value = Types.Cast value fieldType Memory.WriteStaticField cilState.state declaringType fieldId value - setCurrentIp newIp cilState + cilState.SetCurrentIp newIp [cilState]) member x.Ldobj (m : Method) offset (cilState : cilState) = - let address = pop cilState + let address = cilState.Pop() let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Ldobj.Size) - let readValue cilState k = + let readValue (cilState : cilState) k = let actualType = MostConcreteTypeOfRef cilState.state address let value = if typ.IsAssignableFrom actualType then - let value = read cilState address + let value = cilState.Read address Types.Cast value typ else let address = Types.Cast address (typ.MakePointerType()) - read cilState address - push value cilState + cilState.Read address + cilState.Push value List.singleton cilState |> k x.NpeOrInvokeStatementCIL cilState address readValue id member x.Stobj (m : Method) offset (cilState : cilState) = - let value, ref = pop2 cilState + let value, ref = cilState.Pop2() let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Stobj.Size) - let store cilState k = + let store (cilState : cilState) k = let value = Types.Cast value typ - write cilState ref value |> k + cilState.Write ref value |> k x.NpeOrInvokeStatementCIL cilState ref store id member x.LdFldWithFieldInfo (fieldInfo : FieldInfo) addressNeeded (cilState : cilState) = assert(not fieldInfo.IsStatic) - let target = pop cilState + let target = cilState.Pop() let loadWhenTargetIsNotNull (cilState : cilState) k = let fieldId = Reflection.wrapField fieldInfo let t = fieldInfo.DeclaringType let value = match t with | TypeUtils.Native when addressNeeded -> target - | TypeUtils.Native -> read cilState target + | TypeUtils.Native -> cilState.Read target | _ when addressNeeded -> Memory.ReferenceField cilState.state target fieldId - | _ -> readField cilState target fieldId - push value cilState + | _ -> cilState.ReadField target fieldId + cilState.Push value k [cilState] x.NpeOrInvokeStatementCIL cilState target loadWhenTargetIsNotNull id @@ -1202,46 +1231,51 @@ type ILInterpreter() as this = member x.StFld (m : Method) offset (cilState : cilState) = let fieldInfo = resolveFieldFromMetadata m (offset + Offset.from OpCodes.Stfld.Size) assert(not fieldInfo.IsStatic) - let value, targetRef = pop2 cilState + let value, targetRef = cilState.Pop2() let storeWhenTargetIsNotNull (cilState : cilState) k = let fieldType = fieldInfo.FieldType let value = Types.Cast value fieldType let reference = if TypeUtils.isPointer fieldInfo.DeclaringType then targetRef else Reflection.wrapField fieldInfo |> Memory.ReferenceField cilState.state targetRef - write cilState reference value |> k + cilState.Write reference value |> k x.NpeOrInvokeStatementCIL cilState targetRef storeWhenTargetIsNotNull id member private x.LdElemCommon (typ : Type option) (cilState : cilState) arrayRef indices = let arrayType = MostConcreteTypeOfRef cilState.state arrayRef let uncheckedLdElem (cilState : cilState) k = - let value = readIndex cilState arrayRef indices typ - push value cilState + let value = cilState.ReadIndex arrayRef indices typ + cilState.Push value k [cilState] let checkedLdElem (cilState : cilState) k = let dims = List.init (Types.RankOf arrayType) MakeNumber let lengths = List.map (Memory.ArrayLengthByDimension cilState.state arrayRef) dims x.AccessMultidimensionalArray uncheckedLdElem cilState lengths indices k // TODO: if ptr, do net use check #do x.NpeOrInvokeStatementCIL cilState arrayRef checkedLdElem id + member private x.LdElemWithCast typ (cilState : cilState) : cilState list = - let index, arrayRef = pop2 cilState + let index, arrayRef = cilState.Pop2() x.LdElemCommon typ cilState arrayRef [index] + member private x.LdElemTyp typ (cilState : cilState) = x.LdElemWithCast (Some typ) cilState + member private x.LdElem (m : Method) offset (cilState : cilState) = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Ldelem.Size) x.LdElemTyp typ cilState + member private x.LdElemRef = x.LdElemWithCast None + member private x.LdElema (m : Method) offset (cilState : cilState) = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Ldelema.Size) - let index, arrayRef = pop2 cilState + let index, arrayRef = cilState.Pop2() let index = Types.Cast index typeof let referenceLocation (cilState : cilState) k = let value = Memory.ReferenceArrayIndex cilState.state arrayRef [index] (Some typ) - push value cilState + cilState.Push value k [cilState] let checkTypeMismatch (cilState : cilState) (k : cilState list -> 'a) = let elementType = MostConcreteTypeOfRef cilState.state arrayRef |> Types.ElementType - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.TypeIsType typ elementType &&& Types.TypeIsType elementType typ, state)) referenceLocation (x.Raise x.ArrayTypeMismatchException) @@ -1250,18 +1284,19 @@ type ILInterpreter() as this = let length = Memory.ArrayLengthByDimension cilState.state arrayRef (MakeNumber 0) x.AccessArray checkTypeMismatch cilState length index k x.NpeOrInvokeStatementCIL cilState arrayRef checkIndex id + member private x.StElemCommon (typ : Type option) (cilState : cilState) arrayRef indices value = let arrayType = MostConcreteTypeOfRef cilState.state arrayRef let baseType = Types.ElementType arrayType let checkedStElem (cilState : cilState) (k : cilState list -> 'a) = let typeOfValue = TypeOf value let uncheckedStElem (cilState : cilState) (k : cilState list -> 'a) = - writeIndex cilState arrayRef indices value typ |> k + cilState.WriteIndex arrayRef indices value typ |> k let checkTypeMismatch (cilState : cilState) (k : cilState list -> 'a) = let condition = if Types.IsValueType typeOfValue then True() else Types.RefIsType cilState.state value baseType - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (condition, state)) uncheckedStElem (x.Raise x.ArrayTypeMismatchException) @@ -1270,26 +1305,31 @@ type ILInterpreter() as this = let lengths = List.map (Memory.ArrayLengthByDimension cilState.state arrayRef) dims x.AccessMultidimensionalArray checkTypeMismatch cilState lengths indices k x.NpeOrInvokeStatementCIL cilState arrayRef checkedStElem id + member private x.StElemWithCast typ (cilState : cilState) = - let value, index, arrayRef = pop3 cilState + let value, index, arrayRef = cilState.Pop3() x.StElemCommon typ cilState arrayRef [index] value + member private x.StElemTyp typ (cilState : cilState) = x.StElemWithCast (Some typ) cilState + member private x.StElem cfg offset (cilState : cilState) = let typ = resolveTypeFromMetadata cfg (offset + Offset.from OpCodes.Stelem.Size) x.StElemWithCast (Some typ) cilState + member private x.StElemRef = x.StElemWithCast None + member private x.LdLen (cilState : cilState) = - let arrayRef = pop cilState + let arrayRef = cilState.Pop() let ldlen (cilState : cilState) k = let length = Memory.ArrayLengthByDimension cilState.state arrayRef (MakeNumber 0) - push length cilState + cilState.Push length k [cilState] x.NpeOrInvokeStatementCIL cilState arrayRef ldlen id member private x.LdVirtFtn (m : Method) offset (cilState : cilState) = let ancestorMethodBase = resolveMethodFromMetadata m (offset + Offset.from OpCodes.Ldvirtftn.Size) - let this = pop cilState + let this = cilState.Pop() let ldvirtftn (cilState : cilState) k = assert(IsReference this) let thisType = MostConcreteTypeOfRef cilState.state this @@ -1298,7 +1338,7 @@ type ILInterpreter() as this = let methodInfo = (overriden :> IMethod).MethodBase let methodInfoType = methodInfo.GetType() let methodPtr = Terms.Concrete methodInfo methodInfoType - push methodPtr cilState + cilState.Push methodPtr k [cilState] x.NpeOrInvokeStatementCIL cilState this ldvirtftn id @@ -1308,64 +1348,65 @@ type ILInterpreter() as this = || refType = typeof && locationType = typeof member private x.Ldind t (cilState : cilState) = - let address = pop cilState - let load cilState k = + let address = cilState.Pop() + let load (cilState : cilState) k = let castedAddress = let locationType = TypeOfLocation address if x.CanReadSafe t locationType then address else Types.Cast address (t.MakePointerType()) - let value = read cilState castedAddress - push value cilState + let value = cilState.Read castedAddress + cilState.Push value k (List.singleton cilState) x.NpeOrInvokeStatementCIL cilState address load id member private x.Stind valueCast (cilState : cilState) = - let value, address = pop2 cilState - let store cilState k = + let value, address = cilState.Pop2() + let store (cilState : cilState) k = let value = valueCast value - write cilState address value |> k + cilState.Write address value |> k x.NpeOrInvokeStatementCIL cilState address store id member x.BoxNullable (t : Type) (v : term) (cilState : cilState) : cilState list = // TODO: move it to Reflection.fs; add more validation in case if .NET implementation does not have these fields let boxValue (cilState : cilState) = - let value = pop cilState + let value = cilState.Pop() let address = Memory.BoxValueType cilState.state value - push address cilState + cilState.Push address let hasValueCase (cilState : cilState) k = let valueFieldInfo = t.GetField("value", Reflection.instanceBindingFlags) - push v cilState + cilState.Push v let cilStates = x.LdFldWithFieldInfo valueFieldInfo false cilState List.iter boxValue cilStates k cilStates let boxNullable (hasValue, cilState : cilState) k = - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (hasValue, state)) hasValueCase (fun cilState k -> - push (NullRef t) cilState + cilState.Push (NullRef t) k [cilState]) k let hasValueFieldInfo = t.GetField("hasValue", Reflection.instanceBindingFlags) let hasValueResults = - push v cilState + cilState.Push v x.LdFldWithFieldInfo hasValueFieldInfo false cilState - |> List.map (fun cilState -> (pop cilState, cilState)) + |> List.map (fun cilState -> (cilState.Pop(), cilState)) Cps.List.mapk boxNullable hasValueResults List.concat member x.Box (m : Method) offset (cilState : cilState) = let t = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Box.Size) if Types.IsValueType t then - let v = pop cilState + let v = cilState.Pop() if Types.IsNullable t then x.BoxNullable t v cilState else let v = Types.Cast v t allocateValueTypeInHeap v cilState [cilState] else [cilState] - member private x.UnboxCommon cilState obj t handleRestResults k = + + member private x.UnboxCommon (cilState : cilState) obj t handleRestResults k = let nonExceptionCont (cilState : cilState) res k = - push res cilState + cilState.Push res k [cilState] assert(IsReference obj) assert(Types.IsValueType t) @@ -1380,16 +1421,16 @@ type ILInterpreter() as this = x.Raise x.NullReferenceException cilState k let nullableCase (cilState : cilState) = let underlyingTypeOfNullableT = Nullable.GetUnderlyingType t - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.RefIsType state obj underlyingTypeOfNullableT, state)) (fun cilState k -> - let value = HeapReferenceToBoxReference obj |> read cilState + let value = HeapReferenceToBoxReference obj |> cilState.Read let nullableTerm = Memory.DefaultOf t let valueField, hasValueField = Reflection.fieldsOfNullable t let nullableTerm = - writeStructField cilState nullableTerm valueField value + cilState.WriteStructField nullableTerm valueField value let nullableTerm = - writeStructField cilState nullableTerm hasValueField (MakeBool true) + cilState.WriteStructField nullableTerm hasValueField (MakeBool true) let address = Memory.BoxValueType cilState.state nullableTerm let ref = HeapReferenceToBoxReference address let res = handleRestResults cilState ref @@ -1399,39 +1440,38 @@ type ILInterpreter() as this = if Types.IsNullable t then nullableCase cilState else - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.IsCast state obj t, state)) (fun cilState k -> let ref = Types.Cast obj t |> HeapReferenceToBoxReference let res = handleRestResults cilState ref - push res cilState + cilState.Push res k [cilState]) (x.Raise x.InvalidCastException) - BranchOnNullCIL cilState obj + cilState.BranchOnNullCIL obj nullCase nonNullCase k - member private x.SetExceptionIP cilState = - let codeLocations = List.map (Option.get << ip2codeLocation) cilState.ipStack - setCurrentIp (SearchingForHandler(None, List.empty, codeLocations, List.empty)) cilState + member private x.SetExceptionIP (cilState : cilState) = + let ip = SearchingForHandler(None, List.empty, cilState.CodeLocations, List.empty) + cilState.SetCurrentIpSafe ip member private x.CommonThrow cilState error isRuntime = - let codeLocations = - List.takeUntil isFilter cilState.ipStack - |> List.map (Option.get << ip2codeLocation) + let codeLocations = cilState.CodeLocations let stackTrace = List.map toString codeLocations |> join "," - setCurrentIpSafe (SearchingForHandler(None, List.empty, codeLocations, List.empty)) cilState - setException (Unhandled(error, isRuntime, stackTrace)) cilState + let ip = SearchingForHandler(None, List.empty, codeLocations, List.empty) + cilState.SetCurrentIpSafe ip + cilState.SetException (Unhandled(error, isRuntime, stackTrace)) member private x.Throw (cilState : cilState) = - let error = peek cilState - let isRuntime = (currentMethod cilState).IsRuntimeException - BranchOnNullCIL cilState error + let error = cilState.Peek() + let isRuntime = cilState.CurrentMethod.IsRuntimeException + cilState.BranchOnNullCIL error (x.Raise x.NullReferenceException) (fun cilState k -> x.CommonThrow cilState error isRuntime - clearEvaluationStackLastFrame cilState + cilState.ClearEvaluationStackLastFrame() k [cilState]) id @@ -1442,7 +1482,7 @@ type ILInterpreter() as this = x.SetExceptionIP cilState List.singleton cilState - member private x.MoveToFinally cilState ehcs (tryBlocks : HashSet) (location : codeLocation) isSecondBypass = + member private x.MoveToFinally (cilState : cilState) ehcs (tryBlocks : HashSet) (location : codeLocation) isSecondBypass = let mutable ehcs = ehcs let mutable finallyHandlerIp = None let offset = location.offset @@ -1451,15 +1491,15 @@ type ILInterpreter() as this = ehcs <- List.tail ehcs match ehc.ehcType with | _ when x.InHandlerBlock offset ehc -> - if isSecondBypass then moveDownExceptionRegister cilState - else popExceptionRegister cilState + if isSecondBypass then cilState.MoveDownExceptionRegister() + else cilState.PopExceptionRegister() | Finally -> finallyHandlerIp <- Some (Instruction(ehc.handlerOffset, location.method)) | Fault when isSecondBypass -> finallyHandlerIp <- Some (Instruction(ehc.handlerOffset, location.method)) | _ when tryBlocks.Add(ehc.tryOffset, ehc.tryLength) -> - if isSecondBypass then moveDownExceptionRegister cilState - else popExceptionRegister cilState + if isSecondBypass then cilState.MoveDownExceptionRegister() + else cilState.PopExceptionRegister() | _ -> () finallyHandlerIp, ehcs @@ -1482,7 +1522,7 @@ type ILInterpreter() as this = // Look through blocks, if it is suitable catch, continue execution with 'SecondBypass' // If it is filter, push exception register and continue execution with 'InFilterHandler' // If suitable block was not found, try again with 'sortedBlocks = tail' sortedBlocks - member private x.FindCatch ehcs (observed : ExceptionHandlingClause list) (location : codeLocation) locations framesToPop cilState = + member private x.FindCatch ehcs (observed : ExceptionHandlingClause list) (location : codeLocation) locations framesToPop (cilState : cilState) = let state = cilState.state let errorRef = state.exceptionsRegister.GetError() let exceptionType = lazy(MostConcreteTypeOfRef state errorRef) @@ -1504,10 +1544,10 @@ type ILInterpreter() as this = | Filter o -> // Start executing filter let method = location.method - push errorRef cilState - newExceptionRegister cilState + cilState.Push errorRef + cilState.NewExceptionRegister() let handlerOffset = ehc.handlerOffset - let filterHandler = instruction method o + let filterHandler = Instruction(o, method) let observed = List.ofSeq observed nextIp <- Some (InFilterHandler(filterHandler, handlerOffset, ehcs, observed, locations, framesToPop)) | _ -> () // Handler is non-suitable catch or finally @@ -1526,54 +1566,56 @@ type ILInterpreter() as this = | None -> assert(List.isEmpty otherEchs) Instruction(dst, m) - | Some ip -> leave ip otherEchs dst m - setCurrentIpSafe currentIp cilState + | Some ip -> instructionPointer.CreateLeave ip otherEchs dst m + cilState.SetCurrentIpSafe currentIp member private x.Unbox (m : Method) offset (cilState : cilState) = let t = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Unbox.Size) - let obj = pop cilState + let obj = cilState.Pop() // TODO: Nullable.GetUnderlyingType for generics; use meta-information of generic type parameter if t.IsGenericParameter then let iie = createInsufficientInformation "Unboxing generic parameter" - cilState.iie <- Some iie + cilState.SetIIE iie [cilState] else x.UnboxCommon cilState obj t (fun _ x -> x) id + member private x.UnboxAny (m : Method) offset (cilState : cilState) = let t = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Unbox_Any.Size) let valueType = typeof - let obj = pop cilState + let obj = cilState.Pop() // TODO: Nullable.GetUnderlyingType for generics; use meta-information of generic type parameter if t.IsGenericParameter then let iie = createInsufficientInformation "Can't introduce generic type X for equation: T = Nullable" - cilState.iie <- Some iie + cilState.SetIIE iie [cilState] else - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Types.TypeIsType t valueType, state)) (fun cilState k -> - let handleRestResults cilState address = read cilState address + let handleRestResults (cilState : cilState) address = + cilState.Read address x.UnboxCommon cilState obj t handleRestResults k) (fun state k -> x.CommonCastClass state obj t k) id member private this.CommonDivRem performAction (cilState : cilState) = let integerCase (cilState : cilState) x y minusOne minValue = - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Arithmetics.IsZero y, state)) (this.Raise this.DivideByZeroException) (fun cilState -> - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k ((x === minValue) &&& (y === minusOne), state)) (this.Raise this.OverflowException) (fun cilState k -> - push (performAction x y) cilState + cilState.Push (performAction x y) k [cilState])) id - let y, x = pop2 cilState + let y, x = cilState.Pop2() match y, x with | FloatT, FloatT -> - push (performAction x y) cilState + cilState.Push (performAction x y) [cilState] | Int64T, _ | UInt64T, _ @@ -1581,6 +1623,7 @@ type ILInterpreter() as this = | _, UInt64T -> integerCase cilState x y (TypeUtils.Int64.MinusOne()) (TypeUtils.Int64.MinValue()) | _ -> integerCase cilState x y (TypeUtils.Int32.MinusOne()) (TypeUtils.Int32.MinValue()) | _ -> __unreachable__() + member private this.Div (cilState : cilState) = let div x y = API.PerformBinaryOperation OperationType.Divide x y id this.CommonDivRem div cilState @@ -1590,15 +1633,15 @@ type ILInterpreter() as this = this.CommonDivRem rem cilState member private this.CommonUnsignedDivRem isRem performAction (cilState : cilState) = - let y, x = pop2 cilState + let y, x = cilState.Pop2() let divRem x y = let x = makeUnsignedInteger x id let y = makeUnsignedInteger y id - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (Arithmetics.IsZero y, state)) (this.Raise this.DivideByZeroException) (fun cilState k -> - push (performAction x y) cilState + cilState.Push (performAction x y) k [cilState]) id match y, x with @@ -1607,7 +1650,7 @@ type ILInterpreter() as this = | DetachedPtrTerm offset2, DetachedPtrTerm offset1 -> divRem offset1 offset2 | FloatT, _ - | _, FloatT when isRem -> internalfailf "Rem.Un is unspecified for Floats" + | _, FloatT when isRem -> internalfail "Rem.Un is unspecified for Floats" | _ when IsRefOrPtr x || IsRefOrPtr y -> __insufficientInformation__ "trying to div/rem pointers" | _ -> internalfailf "incompatible operands for %s" (if isRem then "Rem.Un" else "Div.Un") @@ -1620,7 +1663,7 @@ type ILInterpreter() as this = this.CommonUnsignedDivRem true rem cilState member private this.UnsignedCheckOverflow checkOverflowForUnsigned (cilState : cilState) = - let y, x = pop2 cilState + let y, x = cilState.Pop2() match y, x with | Int64T, _ | _, Int64T @@ -1636,9 +1679,10 @@ type ILInterpreter() as this = let max = TypeUtils.UInt32.MaxValue() let zero = TypeUtils.UInt32.Zero() checkOverflowForUnsigned zero max x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic - | _ -> internalfailf "incompatible operands for UnsignedCheckOverflow" + | _ -> internalfail "incompatible operands for UnsignedCheckOverflow" + member private this.SignedCheckOverflow checkOverflow (cilState : cilState) = - let y, x = pop2 cilState + let y, x = cilState.Pop2() match y, x with | Int64T, _ | _, Int64T -> @@ -1657,9 +1701,10 @@ type ILInterpreter() as this = let zero = TypeUtils.Int32.Zero() let minusOne = TypeUtils.Int32.MinusOne() checkOverflow min max zero minusOne x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic + member private this.Add_ovf (cilState : cilState) = // min <= x + y <= max - let checkOverflow min max zero _ x y cilState = + let checkOverflow min max zero _ x y (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) let xMoreThan0 state k = k (x >>= zero, state) let yMoreThan0 state k = k (y >>= zero, state) @@ -1671,30 +1716,31 @@ type ILInterpreter() as this = k (x >>= diff, state)) let add (cilState : cilState) k = // no overflow PerformBinaryOperation OperationType.Add x y (fun sum -> - push sum cilState + cilState.Push sum k [cilState]) - StatedConditionalExecutionCIL cilState xMoreThan0 + cilState.StatedConditionalExecutionCIL xMoreThan0 (fun cilState -> // x >= 0 - StatedConditionalExecutionCIL cilState yMoreThan0 + cilState.StatedConditionalExecutionCIL yMoreThan0 (fun cilState -> // y >= 0 - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL checkOverflowWhenMoreThan0 add (this.Raise this.OverflowException)) add) (fun cilState -> // x < 0 - StatedConditionalExecutionCIL cilState yMoreThan0 + cilState.StatedConditionalExecutionCIL yMoreThan0 add (fun cilState -> // x < 0 && y < 0 - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL checkOverflowWhenLessThan0 add (this.Raise this.OverflowException))) id this.SignedCheckOverflow checkOverflow cilState + member private this.Mul_ovf (cilState : cilState) = // min <= x * y <= max - let checkOverflow min max zero _ x y cilState = + let checkOverflow min max zero _ x y (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) let (>>) = API.Arithmetics.(>>) let isZero state k = k ((x === zero) ||| (y === zero), state) @@ -1714,107 +1760,102 @@ type ILInterpreter() as this = k (x >>= quotient, state)) let mul (cilState : cilState) k = // no overflow PerformBinaryOperation OperationType.Multiply x y (fun res -> - push res cilState + cilState.Push res k [cilState]) - StatedConditionalExecutionCIL cilState isZero + cilState.StatedConditionalExecutionCIL isZero (fun cilState k -> - push zero cilState + cilState.Push zero k [cilState]) (fun cilState -> - StatedConditionalExecutionCIL cilState - xMoreThan0 + cilState.StatedConditionalExecutionCIL xMoreThan0 (fun cilState -> // x > 0 - StatedConditionalExecutionCIL cilState yMoreThan0 + cilState.StatedConditionalExecutionCIL yMoreThan0 (fun cilState -> // y > 0 - StatedConditionalExecutionCIL cilState - checkOverflowWhenXM0YM0 + cilState.StatedConditionalExecutionCIL checkOverflowWhenXM0YM0 mul (this.Raise this.OverflowException)) (fun cilState -> // y < 0 - StatedConditionalExecutionCIL cilState - checkOverflowWhenXM0YL0 + cilState.StatedConditionalExecutionCIL checkOverflowWhenXM0YL0 mul (this.Raise this.OverflowException))) (fun cilState -> // x < 0 - StatedConditionalExecutionCIL cilState - yMoreThan0 + cilState.StatedConditionalExecutionCIL yMoreThan0 (fun cilState -> // y > 0 - StatedConditionalExecutionCIL cilState - checkOverflowWhenXL0YM0 + cilState.StatedConditionalExecutionCIL checkOverflowWhenXL0YM0 mul (this.Raise this.OverflowException)) (fun cilState k -> // y < 0 - StatedConditionalExecutionCIL cilState - checkOverflowWhenXL0YL0 + cilState.StatedConditionalExecutionCIL checkOverflowWhenXL0YL0 mul (this.Raise this.OverflowException) k))) id this.SignedCheckOverflow checkOverflow cilState + member private this.Add_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned _ max x y cilState = + let checkOverflowForUnsigned _ max x y (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> PerformBinaryOperation OperationType.Subtract max x (fun diff -> k (diff >>= y, state))) (fun cilState k -> PerformBinaryOperation OperationType.Add x y (fun res -> - push res cilState + cilState.Push res k [cilState])) (this.Raise this.OverflowException) id this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + member private this.Mul_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned zero max x y cilState = + let checkOverflowForUnsigned zero max x y (cilState : cilState) = let isZero state k = k ((x === zero) ||| (y === zero), state) - let zeroCase cilState k = - push zero cilState + let zeroCase (cilState : cilState) k = + cilState.Push zero List.singleton cilState |> k - let checkOverflow cilState k = + let checkOverflow (cilState : cilState) k = let evalCondition state k = PerformBinaryOperation OperationType.Divide max x (fun quotient -> k (Arithmetics.GreaterOrEqualUn quotient y, state)) - let mul cilState k = + let mul (cilState : cilState) k = PerformBinaryOperation OperationType.Multiply x y (fun res -> - push res cilState + cilState.Push res List.singleton cilState |> k) - StatedConditionalExecutionCIL cilState - evalCondition + cilState.StatedConditionalExecutionCIL evalCondition mul (this.Raise this.OverflowException) k - StatedConditionalExecutionCIL cilState - isZero + cilState.StatedConditionalExecutionCIL isZero zeroCase checkOverflow id this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + member private this.Sub_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned _ _ x y cilState = + let checkOverflowForUnsigned _ _ x y (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (x >>= y, state)) (fun (cilState : cilState) k -> // no overflow PerformBinaryOperation OperationType.Subtract x y (fun res -> - push res cilState + cilState.Push res k [cilState])) (this.Raise this.OverflowException) id this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + member private this.Sub_ovf (cilState : cilState) = // there is no way to reduce current operation to [x `Add_Ovf` (-y)] // min <= x - y <= max - let checkOverflowForSigned min max zero minusOne x y cilState = + let checkOverflowForSigned min max zero minusOne x y (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) let xGreaterEqualZero state k = k (x >>= zero, state) let sub (cilState : cilState) k = // no overflow PerformBinaryOperation OperationType.Subtract x y (fun res -> - push res cilState + cilState.Push res k [cilState]) - StatedConditionalExecutionCIL cilState - xGreaterEqualZero + cilState.StatedConditionalExecutionCIL xGreaterEqualZero (fun cilState -> // x >= 0 => max - x >= 0 => no overflow for [-1 * (max - x)] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> PerformBinaryOperation OperationType.Subtract max x (fun diff -> PerformBinaryOperation OperationType.Multiply diff minusOne (fun minusDiff -> @@ -1822,7 +1863,7 @@ type ILInterpreter() as this = sub (this.Raise this.OverflowException)) (fun cilState -> // x < 0 => no overflow for [min - x] # x < 0 => [min - x] != min => no overflow for (-1) * [min - x] - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> PerformBinaryOperation OperationType.Subtract min x (fun diff -> PerformBinaryOperation OperationType.Multiply diff minusOne (fun minusDiff -> @@ -1835,25 +1876,25 @@ type ILInterpreter() as this = member private x.Newarr (m : Method) offset (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) let elemType = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Newarr.Size) - let numElements = pop cilState - let allocate cilState k = + let numElements = cilState.Pop() + let allocate (cilState : cilState) k = try let ref = Memory.AllocateVectorArray cilState.state numElements elemType - push ref cilState + cilState.Push ref k [cilState] with | :? OutOfMemoryException -> x.Raise x.OutOfMemoryException cilState k - StatedConditionalExecutionCIL cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (numElements >>= TypeUtils.Int32.Zero(), state)) allocate (this.Raise this.OverflowException) id - member x.CreateException (exceptionType : Type) arguments cilState = + member x.CreateException (exceptionType : Type) arguments (cilState : cilState) = assert(not exceptionType.IsValueType) let stackTrace = Memory.StackTrace cilState.state.stack |> List.map toString |> join "\n" Logger.info $"{exceptionType}!\nStack trace:\n{stackTrace}" - clearEvaluationStackLastFrame cilState + cilState.ClearEvaluationStackLastFrame() let constructors = exceptionType.GetConstructors() let argumentsLength = List.length arguments let argumentsTypes = List.map TypeOf arguments @@ -1907,33 +1948,35 @@ type ILInterpreter() as this = x.ExecuteAllInstructionsWhile (always false) cilState // returns finishedStates, incompleteStates, erroredStates - member x.ExecuteAllInstructionsWhile (condition : ip -> bool) (cilState : cilState) = - let rec executeAllInstructions (finishedStates, incompleteStates, errors) cilState k = - let ip = currentIp cilState + member x.ExecuteAllInstructionsWhile (condition : instructionPointer -> bool) (cilState : cilState) = + let rec executeAllInstructions (finishedStates, incompleteStates, errors) (cilState : cilState) k = + let ip = cilState.CurrentIp try let allStates = x.MakeStep cilState - let newErrors, restStates = List.partition isUnhandledExceptionOrError allStates + let newErrors, restStates = + allStates |> List.partition (fun cilState -> cilState.IsUnhandledExceptionOrError) let errors = errors @ newErrors - let newIieStates, goodStates = List.partition isIIEState restStates + let newIieStates, goodStates = + restStates |> List.partition (fun cilState -> cilState.IsIIEState) let incompleteStates = newIieStates @ incompleteStates match goodStates with - | _ when List.forall (currentIp >> condition) goodStates -> + | _ when List.forall (fun (cilState : cilState) -> condition cilState.CurrentIp) goodStates -> Cps.List.foldlk executeAllInstructions (finishedStates, incompleteStates, errors) goodStates k | _ -> (goodStates @ finishedStates, incompleteStates, errors) |> k with | :? InsufficientInformationException as iie -> - cilState.iie <- Some iie - setCurrentIp ip cilState + cilState.SetIIE iie + cilState.SetCurrentIp ip (finishedStates, cilState :: incompleteStates, errors) |> k executeAllInstructions ([],[],[]) cilState id member private x.IncrementLevelIfNeeded (m : Method) (offset : offset) (cilState : cilState) = if offset = 0 || m.CFG.IsLoopEntry offset then - incrementLevel cilState {offset = offset; method = m} + cilState.IncrementLevel {offset = offset; method = m} member private x.DecrementMethodLevel (cilState : cilState) method = let key = {offset = 0; method = method} - decrementLevel cilState key + cilState.DecrementLevel key member private x.InTryBlock offset (clause : ExceptionHandlingClause) = clause.tryOffset <= offset && offset < clause.tryOffset + clause.tryLength @@ -1954,11 +1997,11 @@ type ILInterpreter() as this = match cilState.ipStack with | InstructionEndingIp(offset, caller) as ip :: _ -> // TODO: assert (isCallIp ip) - let newIp = moveInstruction (fallThroughTarget caller offset) ip - setCurrentIp newIp cilState + let newIp = ip.MoveInstruction (fallThroughTarget caller offset) + cilState.SetCurrentIp newIp let callOpCode, calledMethod = caller.ParseCallSite offset if callOpCode = OpCodes.Newobj && (calledMethod.DeclaringType.IsValueType || TypeUtils.isPointer calledMethod.DeclaringType) then - pushNewObjForValueTypes cilState + cilState.PushNewObjForValueTypes() | _ -> __unreachable__() member private x.PushExceptionRegisterIfNeeded (cilState : cilState) (method : Method) (offset : offset) = @@ -1966,19 +2009,18 @@ type ILInterpreter() as this = for handler in method.ExceptionHandlers do let tryStart = handler.tryOffset if tryStart = offset && tryBlocks.Add(tryStart, handler.tryLength) then - newExceptionRegister cilState + cilState.NewExceptionRegister() - member x.MakeStep (cilState : cilState) = - cilState.stepsNumber <- cilState.stepsNumber + 1u + member x.MakeStep (cilState : cilState) : cilState list = let exit m = x.DecrementMethodLevel cilState m Logger.info $"Done with method {m}" match cilState.ipStack with | [ Exit _ ] -> () | Exit m :: _ when m.IsStaticConstructor -> - popFrameOf cilState + cilState.PopFrame() | Exit _ :: _ -> - popFrameOf cilState + cilState.PopFrame() ILInterpreter.FallThroughCall cilState | _ -> __unreachable__() let rec makeStep' ip k = @@ -2003,10 +2045,10 @@ type ILInterpreter() as this = | None -> assert(List.isEmpty otherEhcs) Instruction(dst, m) - | Some ip -> leave ip otherEhcs dst m - replaceLastIp currentIp cilState - clearEvaluationStackLastFrame cilState - popExceptionRegister cilState + | Some ip -> instructionPointer.CreateLeave ip otherEhcs dst m + cilState.ReplaceLastIp currentIp + cilState.ClearEvaluationStackLastFrame() + cilState.PopExceptionRegister() k [cilState] // Continue executing finally block | Leave(ip, _, _, _) -> @@ -2014,7 +2056,7 @@ type ILInterpreter() as this = // Searching for handler, no locations left where blocks can be | SearchingForHandler(_, _, [], framesToPop) -> let ip = SecondBypass(None, None, List.empty, None, framesToPop, None) - setCurrentIpSafe ip cilState + cilState.SetCurrentIpSafe ip k [cilState] // Searching for handler | SearchingForHandler(sortedBlocks, observed, (location :: otherLocations as locations), framesToPop) -> @@ -2024,20 +2066,20 @@ type ILInterpreter() as this = | None -> x.SortEHCBlocks location let nextIp = x.FindCatch ehcs observed location locations framesToPop cilState match nextIp with - | Some ip -> setCurrentIpSafe ip cilState + | Some ip -> cilState.SetCurrentIpSafe ip | None -> // Going to next method let ip = SearchingForHandler(None, List.empty, otherLocations, framesToPop @ [location]) - setCurrentIpSafe ip cilState + cilState.SetCurrentIpSafe ip k [cilState] // Exception occured while executing filter and no handlers were found // Exception means we return to searching for handler after filter block | InFilterHandler(EmptySecondBypass, _, ehcs, observed, locations, framesToPop) -> let newIp = SearchingForHandler(Some ehcs, observed, locations, framesToPop) - cilState.filterResult <- None - replaceLastIp newIp cilState - popExceptionRegister cilState - toUnhandledException cilState + cilState.ClearFilterResult() + cilState.ReplaceLastIp newIp + cilState.PopExceptionRegister() + cilState.ToUnhandledException() k [cilState] // Executing instructions inside filter block // Check filter result, if it is 'None' then continue execution @@ -2046,19 +2088,18 @@ type ILInterpreter() as this = match cilState.filterResult with | None -> makeStep' ip k | Some t -> - StatedConditionalExecutionCIL - cilState + cilState.StatedConditionalExecutionCIL (fun state k -> k (transform2BooleanTerm state.pc t, state)) (fun cilState k -> - cilState.filterResult <- None + cilState.ClearFilterResult() let handlerLoc = Some { method = location.method; offset = offset } let ipTrue = SecondBypass(None, None, observed, Some location, framesToPop, handlerLoc) - replaceLastIp ipTrue cilState + cilState.ReplaceLastIp ipTrue k [cilState]) (fun cilState k -> - cilState.filterResult <- None + cilState.ClearFilterResult() let ipFalse = SearchingForHandler(Some ehcs, observed, locations, framesToPop) - replaceLastIp ipFalse cilState + cilState.ReplaceLastIp ipFalse k [cilState]) k // Finished executing all finally blocks, and no handler was found @@ -2066,35 +2107,34 @@ type ILInterpreter() as this = // If we were in filter, continue searching for handler after filter block // Else we set terminating state for program (setting ip 'SearchingForHandler(Some [], [], [])') | EmptySecondBypass -> - let isInFilter = List.tryFind ipIsInFilter cilState.ipStack - match isInFilter with + match cilState.TryGetFilterIp with | Some (InFilterHandler(_, _, ehcs, observed, locations, framesToPop)) -> let ip = SearchingForHandler(Some ehcs, observed, locations, framesToPop) - popFrameOf cilState - replaceLastIp ip cilState - popExceptionRegister cilState - toUnhandledException cilState + cilState.PopFrame() + cilState.ReplaceLastIp ip + cilState.PopExceptionRegister() + cilState.ToUnhandledException() | _ -> - setCurrentIp emptySearchingForHandler cilState - toUnhandledException cilState + cilState.SetCurrentIp instructionPointer.EmptySearchingForHandler + cilState.ToUnhandledException() k [cilState] // Starting to explore catch clause // Set exception to caught and push exception object on stack | EmptySecondBypassWithCatch(codeLocation) -> let ip = Instruction(codeLocation.offset, codeLocation.method) - setCurrentIpSafe ip cilState - clearEvaluationStackLastFrame cilState - toCaughtException cilState - push (cilState.state.exceptionsRegister.GetError()) cilState + cilState.SetCurrentIpSafe ip + cilState.ClearEvaluationStackLastFrame() + cilState.ToCaughtException() + cilState.Push (cilState.state.exceptionsRegister.GetError()) k [cilState] // Finished executing finally block in second bypass // We move down exception as it is end of try block // Then we go and look for another block | SecondBypass(Some EndFinally, ehcs, lastEhcs, lastLocation, locations, codeLocation) -> let ip = SecondBypass(None, ehcs, lastEhcs, lastLocation, locations, codeLocation) - moveDownExceptionRegister cilState - toUnhandledException cilState - setCurrentIp ip cilState + cilState.MoveDownExceptionRegister() + cilState.ToUnhandledException() + cilState.SetCurrentIp ip k [cilState] // Executing finally block in second bypass | SecondBypass(Some ip, _, _, _, _, _) -> @@ -2117,19 +2157,19 @@ type ILInterpreter() as this = match locations with | _ :: otherLocations -> if List.isEmpty otherLocations |> not || Option.isSome codeLocation then - popFrameOf cilState - clearEvaluationStackLastFrame cilState + cilState.PopFrame() + cilState.ClearEvaluationStackLastFrame() otherLocations | _ -> locations None, locations | Some _ -> - toCaughtException cilState + cilState.ToCaughtException() Some otherEhcs, locations let ip = SecondBypass(finallyHandlerIp, otherEhcs, lastBlocks, lastLocation, locations, codeLocation) - setCurrentIpSafe ip cilState + cilState.SetCurrentIpSafe ip k [cilState] | _ -> __notImplemented__() - makeStep' (currentIp cilState) id + makeStep' cilState.CurrentIp id member private x.ExecuteInstruction m offset (cilState : cilState) = let opCode = parseInstruction m offset @@ -2242,7 +2282,7 @@ type ILInterpreter() as this = | OpCodeValues.Switch -> switch m offset cilState | OpCodeValues.Ldtoken -> ldtoken |> fallThrough m offset cilState | OpCodeValues.Ldftn -> ldftn |> fallThrough m offset cilState - | OpCodeValues.Pop -> (fun _ _ -> pop >> ignore) |> fallThrough m offset cilState + | OpCodeValues.Pop -> (fun _ _ (cilState : cilState) -> cilState.Pop() |> ignore) |> fallThrough m offset cilState | OpCodeValues.Initobj -> initobj |> forkThrough m offset cilState | OpCodeValues.Ldarga -> ldarga (fun ilBytes offset -> NumberCreator.extractUnsignedInt16 ilBytes (offset + Offset.from OpCodes.Ldarga.Size) |> int) |> fallThrough m offset cilState | OpCodeValues.Ldarga_S -> ldarga (fun ilBytes offset -> NumberCreator.extractUnsignedInt8 ilBytes (offset + Offset.from OpCodes.Ldarga_S.Size) |> int) |> fallThrough m offset cilState @@ -2372,8 +2412,8 @@ type ILInterpreter() as this = | OpCodeValues.Throw -> this.Throw cilState | _ -> __unreachable__() - let renewInstructionsInfo cilState = - if not <| isUnhandledExceptionOrError cilState then + let renewInstructionsInfo (cilState : cilState) = + if not cilState.IsUnhandledExceptionOrError then x.IncrementLevelIfNeeded m offset cilState newSts |> List.iter renewInstructionsInfo newSts diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index fb2464be5..86b6e8f01 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -115,7 +115,7 @@ module internal Z3 = heapAddresses : IDictionary staticKeys : IDictionary regionConstants : Dictionary - defaultValues : IDictionary> + regionAccesses : Dictionary> funcDecls : IDictionary mutable lastSymbolicAddress : int32 } with @@ -139,7 +139,7 @@ module internal Z3 = heapAddresses = Dictionary() staticKeys = Dictionary() regionConstants = Dictionary() - defaultValues = Dictionary>() + regionAccesses = Dictionary>() funcDecls = Dictionary() lastSymbolicAddress = 0 } @@ -151,6 +151,12 @@ module internal Z3 = let emptyState = Memory.EmptyState() let mutable maxBufferSize = 128 + let typeOfLocation (regionSort : regionSort) (path : path) = + if path.IsEmpty then regionSort.TypeOfLocation + else path.TypeOfLocation + + let containsAddress t = t = addressType || not t.IsValueType + let getMemoryConstant mkConst (typ : regionSort * path) = let result : ArrayExpr ref = ref null if encodingCache.regionConstants.TryGetValue(typ, result) then result.Value @@ -159,13 +165,35 @@ module internal Z3 = encodingCache.regionConstants.Add(typ, regConst) regConst - let getDefaultValues (regionSort : regionSort) = - let result : HashSet ref = ref null - if encodingCache.defaultValues.TryGetValue(regionSort, result) then result.Value + let addRegionAccess (sort : regionSort) (path : path) (key : Expr[]) = + assert(typeOfLocation sort path |> containsAddress) + let regionAccesses = encodingCache.regionAccesses + let typ = (sort, path) + let exists, keySet = regionAccesses.TryGetValue(typ) + if exists then keySet.Add(key) |> ignore else - let suitableKeys = HashSet() - encodingCache.defaultValues.Add(regionSort, suitableKeys) - suitableKeys + let keySet = HashSet() + keySet.Add(key) |> ignore + regionAccesses.Add(typ, keySet) + + let tryRemoveRegionAccess (m : Model) (typ : regionSort * path) (storeKey : Expr[]) = + let keySet = encodingCache.regionAccesses[typ] + let mutable toDelete = None + for k in keySet do + if Option.isNone toDelete then + let k' = Array.map (fun k -> m.Eval(k, false)) k + if k' = storeKey then + toDelete <- Some k + match toDelete with + | Some k -> + keySet.Remove(k) |> ignore + true + | None -> false + + let getRestRegionAccesses (m : Model) (typ : regionSort * path) : seq = + let exists, keySet = encodingCache.regionAccesses.TryGetValue(typ) + if exists then Seq.map (Array.map (fun k -> m.Eval(k, false))) keySet + else Seq.empty let getFuncDecl (name : string) (argsSort : Sort[]) (resultSort : Sort) = let result : FuncDecl ref = ref null @@ -905,8 +933,8 @@ module internal Z3 = let inst (k : Expr) = let sort = ctx.MkArraySort(x.Type2Sort addressType, x.Type2Sort typ) let array = x.GetRegionConstant name sort path regionSort - let defaultValues = getDefaultValues regionSort - defaultValues.Add(Array.singleton k) |> ignore + if containsAddress typ then + addRegionAccess regionSort path (Array.singleton k) let expr = ctx.MkSelect(array, k) expr, x.GenerateInstAssumptions expr typ let keysAreMatch read update updateRegion = @@ -959,10 +987,10 @@ module internal Z3 = if hasDefaultValue then x.DefaultValue valueSort, List.empty else let regionSort = GetHeapReadingRegionSort source - let defaultValues = getDefaultValues regionSort - defaultValues.Add(k) |> ignore let sort = ctx.MkArraySort(domainSort, valueSort) let array = x.GetRegionConstant name sort path regionSort + if containsAddress typ then + addRegionAccess regionSort path k let expr = ctx.MkSelect(array, k) expr, x.GenerateInstAssumptions expr typ let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo @@ -1002,8 +1030,8 @@ module internal Z3 = let regionSort = GetHeapReadingRegionSort source let sort = ctx.MkArraySort(x.Type2Sort addressType, x.Type2Sort typ) let array = x.GetRegionConstant name sort path regionSort - let defaultValues = getDefaultValues regionSort - defaultValues.Add(Array.singleton k) |> ignore + if containsAddress typ then + addRegionAccess regionSort path (Array.singleton k) let expr = ctx.MkSelect(array, k) expr, x.GenerateInstAssumptions expr typ let keysAreMatch read update updateRegion = @@ -1026,8 +1054,8 @@ module internal Z3 = let array = x.GetRegionConstant name sort path regionSort let encodedKey = ctx.MkConst(key.ToString(), keyType) encodingCache.staticKeys.Add(encodedKey, key.typ) - let defaultValues = getDefaultValues regionSort - defaultValues.Add(Array.singleton encodedKey) |> ignore + if containsAddress typ then + addRegionAccess regionSort path (Array.singleton encodedKey) {expr = ctx.MkSelect(array, encodedKey); assumptions = List.empty} member private x.StructReading (structSource : ISymbolicConstantSource) (field : fieldId) typ (path : path) name = @@ -1248,74 +1276,15 @@ module internal Z3 = if constant <> term then x.WriteDictOfValueTypes subst source path typ term - member private x.FillRegion state (m : Model) (regionSort : regionSort) constantValue = + member private x.FillRegion state (regionSort : regionSort) constantValue = match regionSort with - | HeapFieldSort field -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 1) - let refinedAddress = m.Eval(expressions[0], false) - let address = x.DecodeConcreteHeapAddress refinedAddress |> ConcreteHeapAddress - suitableKeys.Add({address = address}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillClassFieldsRegion state field constantValue isSuitable - | StaticFieldSort typ -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 1) - let address = expressions[0] - let typ = x.DecodeSymbolicTypeAddress address - suitableKeys.Add({typ = typ}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillStaticsRegion state typ constantValue isSuitable - | ArrayIndexSort arrayType -> - let suitableAddresses = HashSet() - for expressions in getDefaultValues regionSort do - let refinedAddress = m.Eval(expressions[0], false) - let address = x.DecodeConcreteHeapAddress refinedAddress |> ConcreteHeapAddress - suitableAddresses.Add(address) |> ignore - let isSuitable (key : IHeapArrayKey) = - match key with - | :? heapArrayKey as key -> suitableAddresses.Contains key.Address - | _ -> false - Memory.FillArrayRegion state arrayType constantValue isSuitable - | ArrayLengthSort arrayType -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 2) - let refinedAddress = m.Eval(expressions[0], false) - let address = x.DecodeConcreteHeapAddress refinedAddress |> ConcreteHeapAddress - let index = m.Eval(expressions[1], false) |> x.Decode typeof - suitableKeys.Add({address = address; index = index}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillLengthRegion state arrayType constantValue isSuitable - | ArrayLowerBoundSort arrayType -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 2) - let refinedAddress = m.Eval(expressions[0], false) - let address = x.DecodeConcreteHeapAddress refinedAddress |> ConcreteHeapAddress - let index = m.Eval(expressions[1], false) |> x.Decode typeof - suitableKeys.Add({address = address; index = index}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillLowerBoundRegion state arrayType constantValue isSuitable - | StackBufferSort key -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 1) - let index = m.Eval(expressions[0], false) |> x.Decode typeof - suitableKeys.Add({index = index}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillStackBufferRegion state key constantValue isSuitable - | BoxedSort typ -> - let suitableKeys = HashSet() - for expressions in getDefaultValues regionSort do - assert(Array.length expressions = 1) - let refinedAddress = m.Eval(expressions[0], false) - let address = x.DecodeConcreteHeapAddress refinedAddress |> ConcreteHeapAddress - suitableKeys.Add({address = address}) |> ignore - let isSuitable = suitableKeys.Contains - Memory.FillBoxedRegion state typ constantValue isSuitable + | HeapFieldSort field -> Memory.FillClassFieldsRegion state field constantValue + | StaticFieldSort typ -> Memory.FillStaticsRegion state typ constantValue + | ArrayIndexSort arrayType -> Memory.FillArrayRegion state arrayType constantValue + | ArrayLengthSort arrayType -> Memory.FillLengthRegion state arrayType constantValue + | ArrayLowerBoundSort arrayType -> Memory.FillLowerBoundRegion state arrayType constantValue + | StackBufferSort key -> Memory.FillStackBufferRegion state key constantValue + | BoxedSort typ -> Memory.FillBoxedRegion state typ constantValue member x.MkModel (m : Model) = try @@ -1358,28 +1327,43 @@ module internal Z3 = let stores = Dictionary
() let defaultValues = Dictionary() - for KeyValue((region, path), constant) in encodingCache.regionConstants do + + let store region (path : path) key value = + let address = x.DecodeMemoryKey region key + if path.IsEmpty then + let states = Memory.Write state (Ref address) value + assert(states.Length = 1 && states[0] = state) + else stores[(address, path)] <- value, region + + for KeyValue(region, path as typ, constant) in encodingCache.regionConstants do let arr = m.Eval(constant, false) let typeOfRegion = region.TypeOfLocation let typeOfLocation = if path.IsEmpty then typeOfRegion else path.TypeOfLocation + let containsAddress = containsAddress typeOfLocation let rec parseArray (arr : Expr) = if arr.IsConstantArray then assert(arr.Args.Length = 1) - let constantValue = x.Decode typeOfLocation arr.Args[0] - x.WriteDictOfValueTypes defaultValues region path typeOfRegion constantValue + if containsAddress then + let keys = getRestRegionAccesses m typ + if Seq.isEmpty keys |> not then + let constantValue = x.Decode typeOfLocation arr.Args[0] + for k in keys do + store region path k constantValue + else + let constantValue = x.Decode typeOfLocation arr.Args[0] + x.WriteDictOfValueTypes defaultValues region path typeOfRegion constantValue elif arr.IsDefaultArray then assert(arr.Args.Length = 1) elif arr.IsStore then assert(arr.Args.Length >= 3) + let key = arr.Args[1..arr.Args.Length - 2] + let shouldStore = not containsAddress || tryRemoveRegionAccess m typ key parseArray arr.Args[0] - let address = x.DecodeMemoryKey region arr.Args[1..arr.Args.Length - 2] - let value = Array.last arr.Args |> x.Decode typeOfLocation - if path.IsEmpty then - let states = Memory.Write state (Ref address) value - assert(states.Length = 1 && states[0] = state) - else stores[(address, path)] <- value, region + if shouldStore then + let value = Array.last arr.Args |> x.Decode typeOfLocation + store region path key value elif arr.IsConst then () elif arr.IsQuantifier then let quantifier = arr :?> Quantifier @@ -1420,7 +1404,7 @@ module internal Z3 = for KeyValue(regionSort, value) in defaultValues do let constantValue = value.Value - x.FillRegion state m regionSort constantValue + x.FillRegion state regionSort constantValue state.startingTime <- [encodingCache.lastSymbolicAddress - 1] diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 70e160341..337dc2b43 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -558,7 +558,7 @@ public static int TestSolvingCopy9(object[] a, int i, object[] b) return 3; } - [Ignore("fix creating SMT-solver model")] + [TestSvm(100)] public static int TestSolvingCopy10(string[] a, int i, string[] b) { if (a.Length > b.Length && 0 <= i && i < b.Length) @@ -815,6 +815,48 @@ public static int TypeSolverCheck3(object a, object b) return -12; } + [Ignore("fix concrete memory (check fully concreteness) and concrete invoke (by ref parameters)")] + public static int ConcreteDictionaryTest(int v) + { + var d = new Dictionary(); + d.Add(1, v); + if (d.TryGetValue(1, out var value)) + { + if (value != v) + { + return -1; + } + + return value; + } + + return 0; + } + + [Ignore("fix composition with concrete memory")] + public static int ConcreteDictionaryTest1(int a, int b) + { + var d = new Dictionary>(); + d.Add(1, new List {2, 3}); + d.Add(4, new List {5, 6}); + if (d.TryGetValue(a, out var res)) + { + if (res.Contains(b)) + return 1; + return 0; + } + return 2; + } + + [TestSvm(100)] + public static int ListContains(int a, int b) + { + var l = new List {2, 3, b, 5}; + if (l.Contains(a)) + return 1; + return 0; + } + [Ignore("Support rendering recursive arrays")] public static object[] ConcreteRecursiveArray() { diff --git a/VSharp.TestGenerator/TestGenerator.fs b/VSharp.TestGenerator/TestGenerator.fs index 770814603..c909d9745 100644 --- a/VSharp.TestGenerator/TestGenerator.fs +++ b/VSharp.TestGenerator/TestGenerator.fs @@ -72,14 +72,14 @@ module TestGenerator = let arrayType, (lengths : int array), (lowerBounds : int array) = match dim with | Vector -> - let arrayType = (elemType, 1, true) + let arrayType = arrayType.CreateVector elemType let len = ArrayLength(cha, MakeNumber 0, arrayType) |> eval |> unbox arrayType, [| len |], null | ConcreteDimension rank -> - let arrayType = (elemType, rank, false) - arrayType, - Array.init rank (fun i -> ArrayLength(cha, MakeNumber i, arrayType) |> eval |> unbox), - Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval |> unbox) + let arrayType = { elemType = elemType; dimension = rank; isVector = false } + let lens = Array.init rank (fun i -> ArrayLength(cha, MakeNumber i, arrayType) |> eval |> unbox) + let lbs = Array.init rank (fun i -> ArrayLowerBound(cha, MakeNumber i, arrayType) |> eval |> unbox) + arrayType, lens, lbs | SymbolicDimension -> __notImplemented__() let length = Array.reduce (*) lengths // TODO: normalize model (for example, try to minimize lengths of generated arrays) @@ -101,7 +101,7 @@ module TestGenerator = if length <= 0 then String.Empty else let readChar i = - ArrayIndex(cha, [MakeNumber i], (typeof, 1, true)) |> eval |> unbox + ArrayIndex(cha, [MakeNumber i], arrayType.CharVector) |> eval |> unbox let contents : char array = Array.init length readChar String(contents) memoryGraph.AddString index string @@ -121,6 +121,7 @@ module TestGenerator = addMockToMemoryGraph indices encodeMock (Some evalField) test addr mock let private encodeArrayCompactly (state : state) (model : model) (encode : term -> obj) (test : UnitTest) arrayType cha typ lengths lowerBounds index = + assert(TypeUtils.isArrayType typ) if state.concreteMemory.Contains cha then // TODO: Use compact representation for big arrays let contents = @@ -138,25 +139,38 @@ module TestGenerator = List.head i < lengths[0]) else List.toSeq >> Seq.zip3 lowerBounds lengths >> Seq.forall (fun (lb, l, i) -> i >= lb && i < lb + l) + let isModelArray = VectorTime.less cha VectorTime.zero let arrays = - if VectorTime.less cha VectorTime.zero then + if isModelArray then match model with | StateModel modelState -> modelState.arrays | _ -> __unreachable__() - else - state.arrays + else state.arrays + let elemType = arrayType.elemType + let checkElem value = + match value.term, model with + | HeapRef({term = ConcreteHeapAddress address}, _), StateModel modelState -> + match PersistentDict.tryFind modelState.allocatedTypes address with + | Some(ConcreteType typ) -> Memory.IsSafeContextWrite typ elemType + | _ -> true + | _ -> internalfail $"checkElem: unexpected element {value}" + let isSuitableElem = + if isModelArray && not elemType.IsValueType then checkElem + else fun _ -> true let defaultValue, indices, values = match PersistentDict.tryFind arrays arrayType with | Some region -> let defaultValue = match region.defaultValue with - | Some(defaultValue, _) -> encode defaultValue + | Some defaultValue -> encode defaultValue | None -> null let updates = region.updates let indicesWithValues = SortedDictionary() let addOneKey _ (k : updateTreeKey) () = let value = k.value match k.key with + // Filtering wrong store from SMT-model + | _ when isSuitableElem value |> not -> () | OneArrayIndexKey(address, keyIndices) -> let heapAddress = model.Eval address match heapAddress with @@ -233,7 +247,7 @@ module TestGenerator = | CombinedTerm(terms, t) -> let slices = List.map model.Eval terms ReinterpretConcretes slices t - | term -> internalfailf "term2obj: creating object from term: unexpected term %O" term + | term -> internalfail $"term2obj: creating object from term: unexpected term {term}" and private address2obj (model : model) state indices mockCache implementations (test : UnitTest) (address : concreteHeapAddress) : obj = let term2obj = term2obj model state indices mockCache implementations test diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index f73f350f6..a1d8a0e51 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -189,7 +189,6 @@ with t.MethodMocks |> Seq.map (fun m -> m.ReturnValues |> Array.map encode) |> Array.ofSeq outImplementations = t.MethodMocks |> Seq.map (fun m -> m.OutValues |> Array.map (Array.map encode)) |> Seq.toArray - } member x.Decode() = diff --git a/VSharp.Utils/Reflection.fs b/VSharp.Utils/Reflection.fs index 3dd024e42..80552d23f 100644 --- a/VSharp.Utils/Reflection.fs +++ b/VSharp.Utils/Reflection.fs @@ -520,7 +520,7 @@ module public Reflection = // TODO: add cache: map from wrapped field to unwrapped let wrapField (field : FieldInfo) = - {declaringType = field.DeclaringType; name = field.Name; typ = field.FieldType} + { declaringType = field.DeclaringType; name = field.Name; typ = field.FieldType } let getFieldInfo (field : fieldId) = let result = field.declaringType.GetField(field.name, allBindingFlags)