From f6a295d86ca7777201ac8f05b28666a2a7899a3d Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:19:23 +0300 Subject: [PATCH 01/20] [fix] fixed 'hasNonVoidResult' check --- VSharp.Utils/Reflection.fs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/VSharp.Utils/Reflection.fs b/VSharp.Utils/Reflection.fs index 6e90074b6..ae371f9c5 100644 --- a/VSharp.Utils/Reflection.fs +++ b/VSharp.Utils/Reflection.fs @@ -120,7 +120,8 @@ module public Reflection = | :? MethodInfo as m -> m.ReturnType | _ -> internalfail "unknown MethodBase" - let hasNonVoidResult m = (getMethodReturnType m).FullName <> typeof.FullName + let hasNonVoidResult m = + getMethodReturnType m <> typeof && not m.IsConstructor let hasThis (m : MethodBase) = m.CallingConvention.HasFlag(CallingConventions.HasThis) From 22d0427dae28e92bce97fe78e154acaec22b5c37 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:19:40 +0300 Subject: [PATCH 02/20] [fix] fixed pointer deserialization --- {VSharp.InternalCalls => VSharp.IL}/Loader.fs | 44 +++++----- VSharp.InternalCalls/Delegate.fs | 83 +++++++++++++++++++ VSharp.InternalCalls/Delegate.fsi | 14 ++++ VSharp.InternalCalls/Diagnostics.fs | 20 +++++ VSharp.InternalCalls/Diagnostics.fsi | 11 +++ VSharp.InternalCalls/HashHelpers.fs | 27 ++++++ VSharp.InternalCalls/HashHelpers.fsi | 11 +++ .../BidirectionalSearcher.fs | 26 +++--- .../CombinedWeighter.fs | 3 +- .../ContributedCoverageSearcher.fs | 4 +- .../DFSSortedByContributedCoverageSearcher.fs | 6 +- .../DistanceWeighter.fs | 5 +- {VSharp.SILI => VSharp.SVM}/ExecutionTree.fs | 2 +- .../ExecutionTreeSearcher.fs | 4 +- {VSharp.SILI => VSharp.SVM}/FairSearcher.fs | 18 ++-- {VSharp.SILI => VSharp.SVM}/GuidedSearcher.fs | 8 +- .../InterleavedSearcher.fs | 2 +- {VSharp.SILI => VSharp.SVM}/Options.fs | 4 +- VSharp.SILI/SILI.fs => VSharp.SVM/SVM.fs | 22 ++--- {VSharp.SILI => VSharp.SVM}/Searcher.fs | 2 +- {VSharp.SILI => VSharp.SVM}/Statistics.fs | 4 +- VSharp.SVM/VSharp.SVM.fsproj | 36 ++++++++ VSharp.Utils/MemoryGraph.fs | 8 +- 23 files changed, 287 insertions(+), 77 deletions(-) rename {VSharp.InternalCalls => VSharp.IL}/Loader.fs (87%) create mode 100644 VSharp.InternalCalls/Delegate.fs create mode 100644 VSharp.InternalCalls/Delegate.fsi create mode 100644 VSharp.InternalCalls/Diagnostics.fs create mode 100644 VSharp.InternalCalls/Diagnostics.fsi create mode 100644 VSharp.InternalCalls/HashHelpers.fs create mode 100644 VSharp.InternalCalls/HashHelpers.fsi rename {VSharp.SILI => VSharp.SVM}/BidirectionalSearcher.fs (94%) rename {VSharp.SILI => VSharp.SVM}/CombinedWeighter.fs (96%) rename {VSharp.SILI => VSharp.SVM}/ContributedCoverageSearcher.fs (90%) rename {VSharp.SILI => VSharp.SVM}/DFSSortedByContributedCoverageSearcher.fs (97%) rename {VSharp.SILI => VSharp.SVM}/DistanceWeighter.fs (98%) rename {VSharp.SILI => VSharp.SVM}/ExecutionTree.fs (99%) rename {VSharp.SILI => VSharp.SVM}/ExecutionTreeSearcher.fs (98%) rename {VSharp.SILI => VSharp.SVM}/FairSearcher.fs (94%) rename {VSharp.SILI => VSharp.SVM}/GuidedSearcher.fs (96%) rename {VSharp.SILI => VSharp.SVM}/InterleavedSearcher.fs (98%) rename {VSharp.SILI => VSharp.SVM}/Options.fs (93%) rename VSharp.SILI/SILI.fs => VSharp.SVM/SVM.fs (97%) rename {VSharp.SILI => VSharp.SVM}/Searcher.fs (99%) rename {VSharp.SILI => VSharp.SVM}/Statistics.fs (99%) create mode 100644 VSharp.SVM/VSharp.SVM.fsproj diff --git a/VSharp.InternalCalls/Loader.fs b/VSharp.IL/Loader.fs similarity index 87% rename from VSharp.InternalCalls/Loader.fs rename to VSharp.IL/Loader.fs index 22176d037..109a4d80c 100644 --- a/VSharp.InternalCalls/Loader.fs +++ b/VSharp.IL/Loader.fs @@ -28,7 +28,7 @@ module Loader = let private CSharpUtilsAssembly = AssemblyName("VSharp.CSharpUtils").FullName |> AssemblyManager.LoadFromAssemblyName - let public CSharpImplementations = + let internal CSharpImplementations = // Loading assembly and collecting methods via VSharp assembly load context, // because C# internal calls will be explored by VSharp seq [ @@ -51,15 +51,19 @@ module Loader = ] |> collectImplementations - let public FSharpImplementations = - // Loading assembly and collecting methods via default assembly load context, - // because all VSharp types, like VSharp.Core.state are loaded via default load context, - // so F# internal calls (which use state) must be loaded via default load context - Assembly.GetExecutingAssembly().GetTypes() - |> Array.filter Microsoft.FSharp.Reflection.FSharpType.IsModule - |> collectImplementations + // Loading assembly and collecting methods via default assembly load context, + // because all VSharp types, like VSharp.Core.state are loaded via default load context, + // so F# internal calls (which use state) must be loaded via default load context + let mutable internal FSharpImplementations : Map = Map.empty + + let public SetInternalCallsAssembly (asm : Assembly) = + let implementations = + asm.GetTypes() + |> Array.filter Microsoft.FSharp.Reflection.FSharpType.IsModule + |> collectImplementations + FSharpImplementations <- implementations - let private runtimeExceptionsConstructors = + let internal runtimeExceptionsConstructors = // Loading assembly and collecting methods via VSharp assembly load context, // because exceptions constructors will be explored by VSharp CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.Exceptions") @@ -69,18 +73,9 @@ module Loader = let private runtimeExceptionsImplementations = runtimeExceptionsConstructors.Values |> Seq.map Reflection.getFullMethodName |> set - let mutable public CilStateImplementations : string seq = - Seq.empty - - let public hasRuntimeExceptionsImplementation (fullMethodName : string) = - Map.containsKey fullMethodName runtimeExceptionsConstructors - - let public isRuntimeExceptionsImplementation (fullMethodName : string) = + let internal isRuntimeExceptionsImplementation (fullMethodName : string) = Set.contains fullMethodName runtimeExceptionsImplementations - let public getRuntimeExceptionsImplementation (fullMethodName : string) = - runtimeExceptionsConstructors.[fullMethodName] - let private shimImplementations = set [ "System.DateTime System.DateTime.get_Now()" @@ -92,9 +87,15 @@ module Loader = // Socket.Read TODO: writing to the out parameters ] - let public isShimmed (fullMethodName : string) = + let internal isShimmed (fullMethodName : string) = Set.contains fullMethodName shimImplementations + let internal trustedIntrinsics = + let intPtr = Reflection.getAllMethods typeof |> Array.map Reflection.getFullMethodName + let volatile = Reflection.getAllMethods typeof |> Array.map Reflection.getFullMethodName + let defaultComparer = [|"System.Collections.Generic.Comparer`1[T] System.Collections.Generic.Comparer`1[T].get_Default()"|] + Array.concat [intPtr; volatile; defaultComparer] + let private concreteInvocations = set [ // Types @@ -133,6 +134,7 @@ module Loader = "System.RuntimeType System.ModuleHandle.GetModuleType(System.Reflection.RuntimeModule)" "System.Type System.RuntimeType.get_DeclaringType(this)" "System.String System.RuntimeType.get_Namespace(this)" + "System.Boolean System.Type.get_IsAbstract(this)" // EqualityComparer "System.Object System.Collections.Generic.ComparerHelpers.CreateDefaultEqualityComparer(System.Type)" @@ -179,5 +181,5 @@ module Loader = "System.Void VSharp.CSharpUtils.Exceptions.CreateOutOfMemoryException()" ] - let isInvokeInternalCall (fullMethodName : string) = + let internal isInvokeInternalCall (fullMethodName : string) = concreteInvocations.Contains fullMethodName diff --git a/VSharp.InternalCalls/Delegate.fs b/VSharp.InternalCalls/Delegate.fs new file mode 100644 index 000000000..ca9dfafc9 --- /dev/null +++ b/VSharp.InternalCalls/Delegate.fs @@ -0,0 +1,83 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations + +module internal Delegate = + + let DelegateCombine (i : IInterpreter) 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 d = Memory.CombineDelegates cilState.state args t + push d cilState + List.singleton cilState |> k + let typesCheck 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 + (fun state k -> k (Types.RefIsType state d2 t, state)) + (combine t) + (i.Raise i.ArgumentException) + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (Types.RefIsType state d1 t, state)) + secondCheck + (i.Raise i.ArgumentException) + k + let nullCheck cilState k = + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference d2, state)) + (fun cilState k -> push d1 cilState; List.singleton cilState |> k) + typesCheck + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference d1, state)) + (fun cilState k -> push d2 cilState; List.singleton cilState |> k) + nullCheck + id + + let DelegateRemove (i : IInterpreter) 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 d = Memory.RemoveDelegate cilState.state source toRemove t + push d cilState + List.singleton cilState |> k + let typesCheck 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 + (fun state k -> k (Types.RefIsType state toRemove t, state)) + (remove t) + (i.Raise i.ArgumentException) + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (Types.RefIsType state source t, state)) + secondCheck + (i.Raise i.ArgumentException) + k + let nullCheck cilState k = + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference source, state)) + (fun cilState k -> push (TypeOf source |> NullRef) cilState; List.singleton cilState |> k) + typesCheck + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference toRemove, state)) + (fun cilState k -> push source cilState; List.singleton cilState |> k) + nullCheck + id diff --git a/VSharp.InternalCalls/Delegate.fsi b/VSharp.InternalCalls/Delegate.fsi new file mode 100644 index 000000000..574a0587f --- /dev/null +++ b/VSharp.InternalCalls/Delegate.fsi @@ -0,0 +1,14 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL + +module internal Delegate = + + [] + val DelegateCombine : IInterpreter -> cilState -> term list -> cilState list + + [] + val DelegateRemove : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/Diagnostics.fs b/VSharp.InternalCalls/Diagnostics.fs new file mode 100644 index 000000000..e304d1274 --- /dev/null +++ b/VSharp.InternalCalls/Diagnostics.fs @@ -0,0 +1,20 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations + +module internal Diagnostics = + + let DebugAssert (_ : IInterpreter) cilState (args : term list) = + assert(List.length args = 1) + let condition = List.head args + StatedConditionalExecutionCIL cilState + (fun state k -> k (condition, state)) + (fun cilState k -> (); k [cilState]) + (fun cilState k -> + ErrorReporter.ReportFatalError cilState "Debug.Assert failed" + k []) + id diff --git a/VSharp.InternalCalls/Diagnostics.fsi b/VSharp.InternalCalls/Diagnostics.fsi new file mode 100644 index 000000000..6bb260ab8 --- /dev/null +++ b/VSharp.InternalCalls/Diagnostics.fsi @@ -0,0 +1,11 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL + +module internal Diagnostics = + + [] + val DebugAssert : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/HashHelpers.fs b/VSharp.InternalCalls/HashHelpers.fs new file mode 100644 index 000000000..f0f98a080 --- /dev/null +++ b/VSharp.InternalCalls/HashHelpers.fs @@ -0,0 +1,27 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations + +module internal HashHelpers = + + let FastMod (i : IInterpreter) cilState (args : term list) = + assert(List.length args = 3) + let left, right = args[0], args[1] + let validCase 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 + k [cilState] + StatedConditionalExecutionCIL cilState + (fun state k -> k (right === MakeNumber 0, state)) + (i.Raise i.DivideByZeroException) + validCase + id diff --git a/VSharp.InternalCalls/HashHelpers.fsi b/VSharp.InternalCalls/HashHelpers.fsi new file mode 100644 index 000000000..d9e45432a --- /dev/null +++ b/VSharp.InternalCalls/HashHelpers.fsi @@ -0,0 +1,11 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL + +module internal HashHelpers = + + [] + val FastMod : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.SILI/BidirectionalSearcher.fs b/VSharp.SVM/BidirectionalSearcher.fs similarity index 94% rename from VSharp.SILI/BidirectionalSearcher.fs rename to VSharp.SVM/BidirectionalSearcher.fs index ff0cb242f..6c3c9b7d0 100644 --- a/VSharp.SILI/BidirectionalSearcher.fs +++ b/VSharp.SVM/BidirectionalSearcher.fs @@ -1,8 +1,10 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Collections.Generic open FSharpx.Collections + open VSharp +open VSharp.Interpreter.IL type BidirectionalSearcher(forward : IForwardSearcher, backward : IBackwardSearcher, targeted : ITargetedSearcher) = @@ -123,7 +125,7 @@ type BackwardSearcher() = let addPob parent child = if not <| ancestorOf.ContainsKey(child) then ancestorOf.Add(child, List<_>()) - ancestorOf.[child].Add(parent) + ancestorOf[child].Add(parent) doAddPob child let updateQBack s : pob list = @@ -143,7 +145,7 @@ type BackwardSearcher() = if (not <| loc2pob.ContainsKey(p'.loc)) then assert(mainPobs.Contains p') else - let list = loc2pob.[p'.loc] + let list = loc2pob[p'.loc] list.Remove(p') |> ignore if list.Count = 0 then loc2pob.Remove(p'.loc) |> ignore currentPobs.Remove(p') |> ignore @@ -151,14 +153,14 @@ type BackwardSearcher() = if Seq.contains p' mainPobs then mainPobs.Remove(p') |> ignore if not(answeredPobs.ContainsKey p') then answeredPobs.Add(p', Witnessed s') - else answeredPobs.[p'] <- Witnessed s' + else answeredPobs[p'] <- Witnessed s' Application.removeGoal p'.loc if ancestorOf.ContainsKey p' then // assert(ancestorOf.[p'] <> null) Seq.iter (fun (ancestor : pob) -> assert(p' <> ancestor) if currentPobs.Contains(ancestor) || mainPobs.Contains(ancestor) then - answerYes s' ancestor) ancestorOf.[p'] + answerYes s' ancestor) ancestorOf[p'] let clear() = mainPobs.Clear() @@ -185,7 +187,7 @@ type BackwardSearcher() = override x.Pick() = if qBack.Count > 0 then - let ps = qBack.[0] + let ps = qBack[0] qBack.RemoveAt(0) Propagate ps else NoAction @@ -226,18 +228,18 @@ module DummyTargetedSearcher = assert(targets.ContainsKey from) let current = currentIp s - if isIIEState s || isUnhandledError s || not(isExecutable(s)) then - finished.[from].Add(s); Seq.empty - elif targets.[from].Contains(current) then addReached from s + if isIIEState s || isUnhandledExceptionOrError s || not(isExecutable(s)) then + finished[from].Add(s); Seq.empty + elif targets[from].Contains(current) then addReached from s else - let list = forPropagation.[from] + let list = forPropagation[from] if not <| list.Contains s then list.Add(s) Seq.empty interface ITargetedSearcher with override x.SetTargets from tos = if not (targets.ContainsKey from) then targets.Add(from, List()) - targets.[from].AddRange(tos) + targets[from].AddRange(tos) override x.Update parent children = let from = parent.startingIP @@ -245,7 +247,7 @@ module DummyTargetedSearcher = Seq.map add (Seq.cons parent children) |> Seq.concat override x.Pick () = - targets.Keys |> Seq.tryPick (fun ip -> forPropagation.[ip] |> Seq.tryHead) + targets.Keys |> Seq.tryPick (fun ip -> forPropagation[ip] |> Seq.tryHead) override x.Reset () = forPropagation.Clear() diff --git a/VSharp.SILI/CombinedWeighter.fs b/VSharp.SVM/CombinedWeighter.fs similarity index 96% rename from VSharp.SILI/CombinedWeighter.fs rename to VSharp.SVM/CombinedWeighter.fs index 4c08fdceb..cdff37c18 100644 --- a/VSharp.SILI/CombinedWeighter.fs +++ b/VSharp.SVM/CombinedWeighter.fs @@ -1,7 +1,6 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System -open VSharp.Interpreter.IL /// /// Combines two weighters using the given combinator function. diff --git a/VSharp.SILI/ContributedCoverageSearcher.fs b/VSharp.SVM/ContributedCoverageSearcher.fs similarity index 90% rename from VSharp.SILI/ContributedCoverageSearcher.fs rename to VSharp.SVM/ContributedCoverageSearcher.fs index 53ae367d8..871ff9be7 100644 --- a/VSharp.SILI/ContributedCoverageSearcher.fs +++ b/VSharp.SVM/ContributedCoverageSearcher.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open VSharp.Utils @@ -6,7 +6,7 @@ open VSharp.Utils /// /// Considers the number of visited basic blocks not covered yet by tests as a state's weight. /// -type internal ContributedCoverageWeighter(statistics : SILIStatistics) = +type internal ContributedCoverageWeighter(statistics : SVMStatistics) = let weight state = Some(statistics.GetVisitedBlocksNotCoveredByTests(state).Count |> uint) diff --git a/VSharp.SILI/DFSSortedByContributedCoverageSearcher.fs b/VSharp.SVM/DFSSortedByContributedCoverageSearcher.fs similarity index 97% rename from VSharp.SILI/DFSSortedByContributedCoverageSearcher.fs rename to VSharp.SVM/DFSSortedByContributedCoverageSearcher.fs index e6ccbc85b..140b64fe2 100644 --- a/VSharp.SILI/DFSSortedByContributedCoverageSearcher.fs +++ b/VSharp.SVM/DFSSortedByContributedCoverageSearcher.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Collections.Generic open Microsoft.FSharp.Core @@ -24,12 +24,12 @@ type DFSSortedByContributedCoverageSearcher(statistics) = let comparer = Comparer.Create(compareWeightOpts) let getWeight = contributedCoverageWeighter.Weight - + let update newStates = states.AddRange newStates // Stable sorting states <- states.OrderBy(getWeight, comparer).ToList() - + interface IForwardSearcher with override x.Init initialStates = initialStates.OrderBy(getWeight, comparer) |> states.AddRange override x.Pick selector = Seq.tryFindBack selector states diff --git a/VSharp.SILI/DistanceWeighter.fs b/VSharp.SVM/DistanceWeighter.fs similarity index 98% rename from VSharp.SILI/DistanceWeighter.fs rename to VSharp.SVM/DistanceWeighter.fs index e9a6b3c02..b362e2198 100644 --- a/VSharp.SILI/DistanceWeighter.fs +++ b/VSharp.SVM/DistanceWeighter.fs @@ -1,8 +1,9 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open VSharp +open VSharp.Interpreter.IL open VSharp.Interpreter.IL.CilStateOperations open VSharp.Interpreter.IL.ipOperations @@ -101,7 +102,7 @@ type ShortestDistanceWeighter(target : codeLocation) = | None -> return 1u } -type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SILIStatistics) = +type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SVMStatistics) = let minDistance (method : Method) fromLoc = let infinity = UInt32.MaxValue diff --git a/VSharp.SILI/ExecutionTree.fs b/VSharp.SVM/ExecutionTree.fs similarity index 99% rename from VSharp.SILI/ExecutionTree.fs rename to VSharp.SVM/ExecutionTree.fs index 17d5fc53a..9c721667c 100644 --- a/VSharp.SILI/ExecutionTree.fs +++ b/VSharp.SVM/ExecutionTree.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Collections.Generic diff --git a/VSharp.SILI/ExecutionTreeSearcher.fs b/VSharp.SVM/ExecutionTreeSearcher.fs similarity index 98% rename from VSharp.SILI/ExecutionTreeSearcher.fs rename to VSharp.SVM/ExecutionTreeSearcher.fs index b33310952..268801989 100644 --- a/VSharp.SILI/ExecutionTreeSearcher.fs +++ b/VSharp.SVM/ExecutionTreeSearcher.fs @@ -1,8 +1,10 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open System.Collections.Generic + open VSharp +open VSharp.Interpreter.IL type internal ExecutionTreeSearcher(randomSeed : int option) = diff --git a/VSharp.SILI/FairSearcher.fs b/VSharp.SVM/FairSearcher.fs similarity index 94% rename from VSharp.SILI/FairSearcher.fs rename to VSharp.SVM/FairSearcher.fs index 8f2d7051b..eba7c462b 100644 --- a/VSharp.SILI/FairSearcher.fs +++ b/VSharp.SVM/FairSearcher.fs @@ -1,9 +1,11 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open System.Collections.Generic open System.Diagnostics + open VSharp +open VSharp.Interpreter.IL /// /// Enumerates initial values as follows: when pick() yielded a value for the first time, it will continue to yield it until timeout, then @@ -61,7 +63,7 @@ type private FairEnumerator<'a>(initialValues : 'a list, getElementTimeoutMs : ' member x.StopCurrent() = stopCurrent() -type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeoutMillis : uint, statistics : SILIStatistics) = +type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeoutMillis : uint, statistics : SVMStatistics) = let baseSearcher = baseSearcherFactory() @@ -77,11 +79,11 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo // (method count * 10)ms is hardcoded time minimum to avoid too small timeouts // and too frequent switching between methods - let shouldStopMethod typ = getTypeTimeout() <= uint methodEnumerators.[typ].Count * 10u + let shouldStopMethod typ = getTypeTimeout() <= uint methodEnumerators[typ].Count * 10u - let getMethodTimeout typ = getTypeTimeout() / uint methodEnumerators.[typ].Count + let getMethodTimeout typ = getTypeTimeout() / uint methodEnumerators[typ].Count - let onTypeTimeout typ _ = elapsedTime <- elapsedTime + methodEnumerators.[typ].StopCurrent() + let onTypeTimeout typ _ = elapsedTime <- elapsedTime + methodEnumerators[typ].StopCurrent() let onMethodTimeout _ elapsed = elapsedTime <- elapsedTime + elapsed @@ -107,7 +109,7 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo let groupedByType = initialStates |> Seq.map CilStateOperations.entryMethodOf |> 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( + methodEnumerators[typ] <- FairEnumerator( // Heuristics to explore the methods without calls first methods |> Seq.sortBy getCallsCount |> Seq.toList, (fun _ -> getMethodTimeout typ), @@ -122,14 +124,14 @@ type internal FairSearcher(baseSearcherFactory : unit -> IForwardSearcher, timeo match typeEnumerator.Pick() with | None -> None | Some typ -> - match methodEnumerators.[typ].Pick() with + match methodEnumerators[typ].Pick() with | None -> typeEnumerator.DropCurrent() |> ignore pick selector | Some method -> match baseSearcher.Pick (fun s -> CilStateOperations.entryMethodOf s = method && selector s) with | None -> - elapsedTime <- elapsedTime + methodEnumerators.[typ].DropCurrent() + elapsedTime <- elapsedTime + methodEnumerators[typ].DropCurrent() pick selector | Some _ as stateOpt -> stateOpt diff --git a/VSharp.SILI/GuidedSearcher.fs b/VSharp.SVM/GuidedSearcher.fs similarity index 96% rename from VSharp.SILI/GuidedSearcher.fs rename to VSharp.SVM/GuidedSearcher.fs index da6ea61c5..ce6e9ced1 100644 --- a/VSharp.SILI/GuidedSearcher.fs +++ b/VSharp.SVM/GuidedSearcher.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Collections.Generic @@ -50,7 +50,7 @@ type ITargetManager = abstract member CalculateTarget : cilState -> codeLocation option abstract member IsStuck : cilState -> bool -type RecursionBasedTargetManager(statistics : SILIStatistics, threshold : uint) = +type RecursionBasedTargetManager(statistics : SVMStatistics, threshold : uint) = interface ITargetManager with override x.IsStuck state = match tryCurrentLoc state with @@ -197,8 +197,8 @@ type GuidedSearcher(baseSearcher : IForwardSearcher, targetManager : ITargetMana override x.StatesCount with get() = baseSearcher.StatesCount + (targetedSearchers.Values |> Seq.sumBy (fun s -> int s.Count)) -type ShortestDistanceBasedSearcher(statistics : SILIStatistics) = +type ShortestDistanceBasedSearcher(statistics : SVMStatistics) = inherit WeightedSearcher(IntraproceduralShortestDistanceToUncoveredWeighter(statistics), BidictionaryPriorityQueue()) -type RandomShortestDistanceBasedSearcher(statistics : SILIStatistics, randomSeed : int option) = +type RandomShortestDistanceBasedSearcher(statistics : SVMStatistics, randomSeed : int option) = inherit WeightedSearcher(AugmentedWeighter(IntraproceduralShortestDistanceToUncoveredWeighter(statistics), (WeightOperations.inverseLogarithmic 7u)), DiscretePDF(mkCilStateHashComparer, randomSeed)) diff --git a/VSharp.SILI/InterleavedSearcher.fs b/VSharp.SVM/InterleavedSearcher.fs similarity index 98% rename from VSharp.SILI/InterleavedSearcher.fs rename to VSharp.SVM/InterleavedSearcher.fs index c1e805273..2040b400f 100644 --- a/VSharp.SILI/InterleavedSearcher.fs +++ b/VSharp.SVM/InterleavedSearcher.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Linq diff --git a/VSharp.SILI/Options.fs b/VSharp.SVM/Options.fs similarity index 93% rename from VSharp.SILI/Options.fs rename to VSharp.SVM/Options.fs index 1fcfb4bbc..29952c9dd 100644 --- a/VSharp.SILI/Options.fs +++ b/VSharp.SVM/Options.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Diagnostics open System.IO @@ -22,7 +22,7 @@ type explorationMode = | TestCoverageMode of coverageZone * searchMode | StackTraceReproductionMode of StackTrace -type SiliOptions = { +type SVMOptions = { explorationMode : explorationMode outputDirectory : DirectoryInfo recThreshold : uint diff --git a/VSharp.SILI/SILI.fs b/VSharp.SVM/SVM.fs similarity index 97% rename from VSharp.SILI/SILI.fs rename to VSharp.SVM/SVM.fs index 2d9aca598..1a552be9c 100644 --- a/VSharp.SILI/SILI.fs +++ b/VSharp.SVM/SVM.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open System.Reflection @@ -7,11 +7,11 @@ open FSharpx.Collections open VSharp open VSharp.Core -open CilStateOperations +open VSharp.Interpreter.IL.CilStateOperations open VSharp.Interpreter.IL open VSharp.Solver -type public SILI(options : SiliOptions) = +type public SVM(options : SVMOptions) = let hasTimeout = options.timeout > 0 let timeout = @@ -31,11 +31,12 @@ type public SILI(options : SiliOptions) = let hasStepsLimit = options.stepsLimit > 0u do API.ConfigureSolver(SolverPool.mkSolver(solverTimeout)) + do VSharp.System.SetUp.ConfigureInternalCalls() let mutable branchesReleased = false let mutable isStopped = false - let statistics = new SILIStatistics(Seq.empty) + let statistics = new SVMStatistics(Seq.empty) let emptyState = Memory.EmptyState() let interpreter = ILInterpreter() @@ -118,12 +119,10 @@ type public SILI(options : SiliOptions) = | Error(msg, isFatal) -> statistics.IsNewError cilState msg isFatal if isNewTest then let callStackSize = Memory.CallStackSize cilState.state - let methodHasByRefParameter (m : Method) = - m.Parameters |> Array.exists (fun pi -> pi.ParameterType.IsByRef) let entryMethod = entryMethodOf cilState - let hasException = isUnhandledError cilState + let hasException = isUnhandledException cilState if isError && not hasException then - if entryMethod.DeclaringType.IsValueType || methodHasByRefParameter entryMethod 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 @@ -245,7 +244,7 @@ type public SILI(options : SiliOptions) = !!(IsNullReference this) |> AddConstraint initialState Some this else None - let parameters = SILI.AllocateByRefParameters initialState method + let parameters = SVM.AllocateByRefParameters initialState method Memory.InitFunctionFrame initialState method this (Some parameters) match this with | Some this -> SolveThisType initialState this @@ -303,12 +302,13 @@ type public SILI(options : SiliOptions) = // TODO: update pobs when visiting new methods; use coverageZone let goodStates, iieStates, errors = interpreter.ExecuteOneInstruction s for s in goodStates @ iieStates @ errors do - if hasRuntimeException s |> not then + if hasRuntimeExceptionOrError s |> not then statistics.TrackStepForward s ip let goodStates, toReportFinished = goodStates |> List.partition (fun s -> isExecutable s || isIsolated s) 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 hasRuntimeException + let runtimeExceptions, userExceptions = toReportExceptions |> List.partition hasRuntimeExceptionOrError runtimeExceptions |> List.iter (fun state -> reportError state null) userExceptions |> List.iter reportFinished let iieStates, toReportIIE = iieStates |> List.partition isIsolated diff --git a/VSharp.SILI/Searcher.fs b/VSharp.SVM/Searcher.fs similarity index 99% rename from VSharp.SILI/Searcher.fs rename to VSharp.SVM/Searcher.fs index 2e205b42e..975dd6c66 100644 --- a/VSharp.SILI/Searcher.fs +++ b/VSharp.SVM/Searcher.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System.Collections.Generic open FSharpx.Collections diff --git a/VSharp.SILI/Statistics.fs b/VSharp.SVM/Statistics.fs similarity index 99% rename from VSharp.SILI/Statistics.fs rename to VSharp.SVM/Statistics.fs index 0f032c0be..47c98db0a 100644 --- a/VSharp.SILI/Statistics.fs +++ b/VSharp.SVM/Statistics.fs @@ -1,4 +1,4 @@ -namespace VSharp.Interpreter.IL +namespace VSharp.SVM open System open System.Diagnostics @@ -51,7 +51,7 @@ type generatedTestInfo = } // TODO: move statistics into (unique) instances of code location! -type public SILIStatistics(entryMethods : Method seq) = +type public SVMStatistics(entryMethods : Method seq) = let entryMethods = List(entryMethods) diff --git a/VSharp.SVM/VSharp.SVM.fsproj b/VSharp.SVM/VSharp.SVM.fsproj new file mode 100644 index 000000000..bf18f4cbf --- /dev/null +++ b/VSharp.SVM/VSharp.SVM.fsproj @@ -0,0 +1,36 @@ + + + + net7.0 + true + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/VSharp.Utils/MemoryGraph.fs b/VSharp.Utils/MemoryGraph.fs index ba291df89..b136c0f89 100644 --- a/VSharp.Utils/MemoryGraph.fs +++ b/VSharp.Utils/MemoryGraph.fs @@ -316,18 +316,18 @@ type MemoryGraph(repr : memoryRepr, mockStorage : MockStorage, createCompactRepr let shift = decodeValue repr.shift :?> int64 |> uint64 UIntPtr(shift) :> obj | :? pointerRepr as repr -> - let shift = decodeValue repr.shift :?> int64 |> nativeint + let shift = decodeValue repr.shift :?> int64 let sightType = sourceTypes[repr.sightType] let index = repr.index let pointer = if index <> nullSourceIndex then // Case for pointer, attached to address 'index' let obj = sourceObjects[repr.index] - let refWithOffset = System.Runtime.CompilerServices.Unsafe.AddByteOffset(ref obj, shift) - System.Runtime.CompilerServices.Unsafe.AsPointer(ref refWithOffset) + let ptr = System.Runtime.CompilerServices.Unsafe.AsPointer(ref obj) + System.Runtime.CompilerServices.Unsafe.Add(ptr, int shift) else // Case for detached pointer - shift.ToPointer() + (nativeint shift).ToPointer() Pointer.Box(pointer, sightType.MakePointerType()) | :? structureRepr as repr when repr.typ >= 0 -> // Case for structs or classes of .NET type From 6e63d2ceb941632abc05b09e9fe1bb234f76aef8 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:26:14 +0300 Subject: [PATCH 03/20] [fix] fixed internal calls - fixed 'Activator.CreateInstance' - fixed style --- VSharp.InternalCalls/Activator.fs | 2 +- VSharp.InternalCalls/Activator.fsi | 4 +- VSharp.InternalCalls/ByReference.fsi | 6 +-- VSharp.InternalCalls/ChessDotNet.fsi | 4 +- VSharp.InternalCalls/Enum.fsi | 4 +- VSharp.InternalCalls/Environment.fsi | 14 +++--- VSharp.InternalCalls/EqualityComparer.fsi | 9 ++-- VSharp.InternalCalls/Globalization.fsi | 8 ++-- VSharp.InternalCalls/IntPtr.fsi | 16 +++---- VSharp.InternalCalls/InteropServices.fsi | 6 +-- VSharp.InternalCalls/PlatformHelper.fsi | 12 ++--- VSharp.InternalCalls/SR.fsi | 56 +++++++++++------------ VSharp.InternalCalls/Span.fsi | 14 +++--- VSharp.InternalCalls/Unsafe.fsi | 34 +++++++------- VSharp.InternalCalls/Volatile.fsi | 4 +- 15 files changed, 96 insertions(+), 97 deletions(-) diff --git a/VSharp.InternalCalls/Activator.fs b/VSharp.InternalCalls/Activator.fs index 8a22d364c..7339e1244 100644 --- a/VSharp.InternalCalls/Activator.fs +++ b/VSharp.InternalCalls/Activator.fs @@ -5,7 +5,7 @@ open VSharp.Core module internal Activator = - let internal CreateInstance (state : state) (args : term list) : term = + let internal CreateInstance (_ : state) (args : term list) : term = assert(List.length args = 1) let t = args[0] |> Helpers.unwrapType Memory.DefaultOf t diff --git a/VSharp.InternalCalls/Activator.fsi b/VSharp.InternalCalls/Activator.fsi index 461c682a5..44a98673a 100644 --- a/VSharp.InternalCalls/Activator.fsi +++ b/VSharp.InternalCalls/Activator.fsi @@ -5,5 +5,5 @@ open VSharp.Core module internal Activator = - [] - val internal CreateInstance : state -> term list -> term + [] + val CreateInstance : state -> term list -> term diff --git a/VSharp.InternalCalls/ByReference.fsi b/VSharp.InternalCalls/ByReference.fsi index a90fd27ee..5ef25986f 100644 --- a/VSharp.InternalCalls/ByReference.fsi +++ b/VSharp.InternalCalls/ByReference.fsi @@ -6,10 +6,10 @@ open VSharp.Core module internal ByReference = - val internal isValueField : fieldId -> bool + val isValueField : fieldId -> bool [] - val internal ctor : state -> term list -> (term * state) list + val ctor : state -> term list -> (term * state) list [] - val internal getValue : state -> term list -> term + val getValue : state -> term list -> term diff --git a/VSharp.InternalCalls/ChessDotNet.fsi b/VSharp.InternalCalls/ChessDotNet.fsi index 1ce28bef5..251913a7b 100644 --- a/VSharp.InternalCalls/ChessDotNet.fsi +++ b/VSharp.InternalCalls/ChessDotNet.fsi @@ -7,7 +7,7 @@ open VSharp.Core module internal ChessDotNet = [] - val internal PositionEquals : state -> term list -> term + val PositionEquals : state -> term list -> term [] - val internal PieceEquals : state -> term list -> term + val PieceEquals : state -> term list -> term diff --git a/VSharp.InternalCalls/Enum.fsi b/VSharp.InternalCalls/Enum.fsi index d651eda5e..753ad01c4 100644 --- a/VSharp.InternalCalls/Enum.fsi +++ b/VSharp.InternalCalls/Enum.fsi @@ -6,7 +6,7 @@ open VSharp.Core module internal Enum = [] - val internal InternalGetCorElementType : state -> term list -> term + val InternalGetCorElementType : state -> term list -> term [] - val internal GetEnumValuesAndNames : state -> term list -> (term * state) list + val GetEnumValuesAndNames : state -> term list -> (term * state) list diff --git a/VSharp.InternalCalls/Environment.fsi b/VSharp.InternalCalls/Environment.fsi index 83d759865..05634c242 100644 --- a/VSharp.InternalCalls/Environment.fsi +++ b/VSharp.InternalCalls/Environment.fsi @@ -6,22 +6,22 @@ open VSharp.Core // ------------------------------- mscorlib.System.Environment ------------------------------- -module Environment = +module internal Environment = [] - val internal GetResourceFromDefault : state -> term list -> term + val GetResourceFromDefault : state -> term list -> term [] - val internal GetCurrentManagedThreadId : state -> term list -> term + val GetCurrentManagedThreadId : state -> term list -> term [] - val internal GetManagedThreadId : state -> term list -> term + val GetManagedThreadId : state -> term list -> term [] - val internal WriteLine : state -> term list -> term + val WriteLine : state -> term list -> term [] - val internal get_IsOutputRedirected : state -> term list -> term + val get_IsOutputRedirected : state -> term list -> term [] - val internal consoleClear : state -> term list -> term + val consoleClear : state -> term list -> term diff --git a/VSharp.InternalCalls/EqualityComparer.fsi b/VSharp.InternalCalls/EqualityComparer.fsi index 32acfa50e..aa8fbd432 100644 --- a/VSharp.InternalCalls/EqualityComparer.fsi +++ b/VSharp.InternalCalls/EqualityComparer.fsi @@ -1,18 +1,17 @@ namespace VSharp.System open global.System -open VSharp open VSharp.Core module internal EqualityComparer = // [] - val internal CreateDefaultEqualityComparer : state -> term list -> term + val CreateDefaultEqualityComparer : state -> term list -> term // [] - val internal CreateDefaultComparer : state -> term list -> term + val CreateDefaultComparer : state -> term list -> term // [] - val internal get_Default : state -> term list -> term + val get_Default : state -> term list -> term - val internal structuralEquality : state -> term -> term -> term + val structuralEquality : state -> term -> term -> term diff --git a/VSharp.InternalCalls/Globalization.fsi b/VSharp.InternalCalls/Globalization.fsi index 5f023beed..421eafa90 100644 --- a/VSharp.InternalCalls/Globalization.fsi +++ b/VSharp.InternalCalls/Globalization.fsi @@ -7,13 +7,13 @@ open VSharp.Core module internal Globalization = [] - val internal get_CurrentCulture : state -> term list -> term + val get_CurrentCulture : state -> term list -> term [] - val internal get_InvariantCulture : state -> term list -> term + val get_InvariantCulture : state -> term list -> term [] - val internal get_CompareInfo : state -> term list -> term + val get_CompareInfo : state -> term list -> term [] - val internal get_Invariant : state -> term list -> term + val get_Invariant : state -> term list -> term diff --git a/VSharp.InternalCalls/IntPtr.fsi b/VSharp.InternalCalls/IntPtr.fsi index f756f8569..f9021ae2e 100644 --- a/VSharp.InternalCalls/IntPtr.fsi +++ b/VSharp.InternalCalls/IntPtr.fsi @@ -7,27 +7,27 @@ open VSharp.Core module internal IntPtr = [] - val internal intPtrCtorFromInt : state -> term list -> (term * state) list + val intPtrCtorFromInt : state -> term list -> (term * state) list [] - val internal intPtrCtorFromPtr : state -> term list -> (term * state) list + val intPtrCtorFromPtr : state -> term list -> (term * state) list [] - val internal intPtrCtorFromLong : state -> term list -> (term * state) list + val intPtrCtorFromLong : state -> term list -> (term * state) list [] - val internal intPtrToPointer : state -> term list -> term + val intPtrToPointer : state -> term list -> term module internal UIntPtr = [] - val internal uintPtrCtorFromUInt : state -> term list -> (term * state) list + val uintPtrCtorFromUInt : state -> term list -> (term * state) list [] - val internal uintPtrCtorFromPtr : state -> term list -> (term * state) list + val uintPtrCtorFromPtr : state -> term list -> (term * state) list [] - val internal uintPtrCtorFromULong : state -> term list -> (term * state) list + val uintPtrCtorFromULong : state -> term list -> (term * state) list [] - val internal uintPtrToPointer : state -> term list -> term + val uintPtrToPointer : state -> term list -> term diff --git a/VSharp.InternalCalls/InteropServices.fsi b/VSharp.InternalCalls/InteropServices.fsi index bc5c11e6f..e883e0b3e 100644 --- a/VSharp.InternalCalls/InteropServices.fsi +++ b/VSharp.InternalCalls/InteropServices.fsi @@ -6,10 +6,10 @@ open VSharp.Core module internal InteropServices = [] - val internal GetArrayDataReference : state -> term list -> term + val GetArrayDataReference : state -> term list -> term [] - val internal Free : state -> term list -> term + val Free : state -> term list -> term [] - val internal AlignedAlloc : state -> term list -> term + val AlignedAlloc : state -> term list -> term diff --git a/VSharp.InternalCalls/PlatformHelper.fsi b/VSharp.InternalCalls/PlatformHelper.fsi index 04d290180..d194914a8 100644 --- a/VSharp.InternalCalls/PlatformHelper.fsi +++ b/VSharp.InternalCalls/PlatformHelper.fsi @@ -8,26 +8,26 @@ module internal PlatformHelper = [] [] - val internal get_ProcessorCount : state -> term list -> term + val get_ProcessorCount : state -> term list -> term [] [] - val internal lzcntIsSupported : state -> term list -> term + val lzcntIsSupported : state -> term list -> term [] [] [] - val internal armBaseIsSupported : state -> term list -> term + val armBaseIsSupported : state -> term list -> term [] - val internal avx2IsSupported : state -> term list -> term + val avx2IsSupported : state -> term list -> term [] - val internal sse2IsSupported : state -> term list -> term + val sse2IsSupported : state -> term list -> term [] [] - val internal x86BaseIsSupported : state -> term list -> term + val x86BaseIsSupported : state -> term list -> term [] val vector128IsHardwareAccelerated : state -> term list -> term diff --git a/VSharp.InternalCalls/SR.fsi b/VSharp.InternalCalls/SR.fsi index 810dcf219..94de4f06a 100644 --- a/VSharp.InternalCalls/SR.fsi +++ b/VSharp.InternalCalls/SR.fsi @@ -7,85 +7,85 @@ open VSharp.Core module internal SR = [] - val internal get_Arg_OverflowException : state -> term list -> term + val get_Arg_OverflowException : state -> term list -> term [] - val internal get_Arg_SystemException : state -> term list -> term + val get_Arg_SystemException : state -> term list -> term [] - val internal get_Arg_IndexOutOfRangeException : state -> term list -> term + val get_Arg_IndexOutOfRangeException : state -> term list -> term [] - val internal get_Arg_NullReferenceException : state -> term list -> term + val get_Arg_NullReferenceException : state -> term list -> term [] - val internal get_Arg_ArrayTypeMismatchException : state -> term list -> term + val get_Arg_ArrayTypeMismatchException : state -> term list -> term [] - val internal get_Arg_InvalidHandle : state -> term list -> term + val get_Arg_InvalidHandle : state -> term list -> term [] - val internal get_Arg_InvalidOperationException : state -> term list -> term + val get_Arg_InvalidOperationException : state -> term list -> term [] - val internal get_ArgumentOutOfRange_Index : state -> term list -> term + val get_ArgumentOutOfRange_Index : state -> term list -> term [] - val internal get_Arg_PlatformNotSupported : state -> term list -> term + val get_Arg_PlatformNotSupported : state -> term list -> term [] - val internal get_Arg_NotGenericTypeDefinition : state -> term list -> term + val get_Arg_NotGenericTypeDefinition : state -> term list -> term [] - val internal get_Arg_ArgumentException : state -> term list -> term + val get_Arg_ArgumentException : state -> term list -> term [] - val internal get_Arg_ArgumentOutOfRangeException : state -> term list -> term + val get_Arg_ArgumentOutOfRangeException : state -> term list -> term [] - val internal get_Arg_ArgumentNullException : state -> term list -> term + val get_Arg_ArgumentNullException : state -> term list -> term [] - val internal get_ArgumentNull_Generic : state -> term list -> term + val get_ArgumentNull_Generic : state -> term list -> term [] - val internal get_Arg_DivideByZero : state -> term list -> term + val get_Arg_DivideByZero : state -> term list -> term [] - val internal get_Arg_ArithmeticException : state -> term list -> term + val get_Arg_ArithmeticException : state -> term list -> term [] - val internal get_Arg_KeyNotFoundWithKey : state -> term list -> term + val get_Arg_KeyNotFoundWithKey : state -> term list -> term [] - val internal get_InvalidOperation_EmptyStack : state -> term list -> term + val get_InvalidOperation_EmptyStack : state -> term list -> term [] - val internal getMessageFromNativeResources : state -> term list -> term + val getMessageFromNativeResources : state -> term list -> term [] - val internal concurrencyLevelMustBePositive : state -> term list -> term + val concurrencyLevelMustBePositive : state -> term list -> term [] - val internal concurrencyLevelMustBeNegative : state -> term list -> term + val concurrencyLevelMustBeNegative : state -> term list -> term [] - val internal get_ArgumentOutOfRange_BadYearMonthDay : state -> term list -> term + val get_ArgumentOutOfRange_BadYearMonthDay : state -> term list -> term [] - val internal get_ArgumentOutOfRange_Count : state -> term list -> term + val get_ArgumentOutOfRange_Count : state -> term list -> term [] - val internal get_ArgumentOutOfRange_StartIndex : state -> term list -> term + val get_ArgumentOutOfRange_StartIndex : state -> term list -> term [] - val internal get_ArgumentOutOfRange_SmallCapacity : state -> term list -> term + val get_ArgumentOutOfRange_SmallCapacity : state -> term list -> term [] - val internal get_Argument_HasToBeArrayClass : state -> term list -> term + val get_Argument_HasToBeArrayClass : state -> term list -> term [] - val internal get_ThreadLocal_Disposed : state -> term list -> term + val get_ThreadLocal_Disposed : state -> term list -> term [] - val internal get_Arg_NotImplementedException : state -> term list -> term + val get_Arg_NotImplementedException : state -> term list -> term diff --git a/VSharp.InternalCalls/Span.fsi b/VSharp.InternalCalls/Span.fsi index bf60f8bc7..a65fc48dd 100644 --- a/VSharp.InternalCalls/Span.fsi +++ b/VSharp.InternalCalls/Span.fsi @@ -6,23 +6,23 @@ open VSharp.Core module internal ReadOnlySpan = - val internal GetContentsRef : state -> term -> term - val internal GetLength : state -> term -> term + val GetContentsRef : state -> term -> term + val GetLength : state -> term -> term [] - val internal GetItemFromReadOnlySpan : state -> term list -> term + val GetItemFromReadOnlySpan : state -> term list -> term [] - val internal GetItemFromSpan : state -> term list -> term + val GetItemFromSpan : state -> term list -> term [] - val internal CtorFromPtrForSpan : state -> term list -> (term * state) list + val CtorFromPtrForSpan : state -> term list -> (term * state) list [] - val internal CtorFromPtrForReadOnlySpan : state -> term list -> (term * state) list + val CtorFromPtrForReadOnlySpan : state -> term list -> (term * state) list [] - val internal CtorFromArrayForReadOnlySpan : state -> term list -> (term * state) list + val CtorFromArrayForReadOnlySpan : state -> term list -> (term * state) list [] val ReadOnlySpanCreateFromString : state -> term list -> term diff --git a/VSharp.InternalCalls/Unsafe.fsi b/VSharp.InternalCalls/Unsafe.fsi index 69bc379c3..8047965f2 100644 --- a/VSharp.InternalCalls/Unsafe.fsi +++ b/VSharp.InternalCalls/Unsafe.fsi @@ -8,72 +8,72 @@ module internal Unsafe = [] [] - val internal AsPointer : state -> term list -> term + val AsPointer : state -> term list -> term [] [] - val internal ObjectAsT : state -> term list -> term + val ObjectAsT : state -> term list -> term [] [] - val internal AsRef : state -> term list -> term + val AsRef : state -> term list -> term [] [] - val internal PointerAsRef : state -> term list -> term + val PointerAsRef : state -> term list -> term [] [] - val internal TFromAsTTo : state -> term list -> term + val TFromAsTTo : state -> term list -> term [] [] - val internal NullRef : state -> term list -> term + val NullRef : state -> term list -> term [] [] - val internal IsNullRef : state -> term list -> term + val IsNullRef : state -> term list -> term [] [] [] [] - val internal AddByteOffset : state -> term list -> term + val AddByteOffset : state -> term list -> term [] [] - val internal ByteOffset : state -> term list -> term + val ByteOffset : state -> term list -> term [] [] [] [] - val internal AddIntPtr : state -> term list -> term + val AddIntPtr : state -> term list -> term [] [] - val internal AddInt : state -> term list -> term + val AddInt : state -> term list -> term [] [] - val internal ReadUnaligned : state -> term list -> term + val ReadUnaligned : state -> term list -> term [] [] - val internal WriteUnaligned : state -> term list -> (term * state) list + val WriteUnaligned : state -> term list -> (term * state) list [] [] - val internal SizeOf : state -> term list -> term + val SizeOf : state -> term list -> term [] [] - val internal AreSame : state -> term list -> term + val AreSame : state -> term list -> term [] [] - val internal GetRawData : state -> term list -> term + val GetRawData : state -> term list -> term [] [] - val internal SkipInit : state -> term list -> term + val SkipInit : state -> term list -> term diff --git a/VSharp.InternalCalls/Volatile.fsi b/VSharp.InternalCalls/Volatile.fsi index a3d9f4f6d..e93086dcc 100644 --- a/VSharp.InternalCalls/Volatile.fsi +++ b/VSharp.InternalCalls/Volatile.fsi @@ -6,7 +6,7 @@ open VSharp.Core // ------------------------------ mscorlib.System.Threading.Volatile -------------------------------- -module Volatile = +module internal Volatile = [] - val internal Read : state -> term list -> term + val Read : state -> term list -> term From e4893f0710a78b69791ac0192215dbbd372609df Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:35:24 +0300 Subject: [PATCH 04/20] [fix] fixed symbolic memory - fixed unsafe operations - added 'Ref' creation from 'Ptr' --- VSharp.SILI.Core/API.fs | 52 +------- VSharp.SILI.Core/API.fsi | 2 +- VSharp.SILI.Core/Memory.fs | 265 ++++++++++++++++++++++++------------- VSharp.SILI.Core/Terms.fs | 2 +- 4 files changed, 184 insertions(+), 137 deletions(-) diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index b8ee2e86e..2e2cbbda5 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -114,8 +114,8 @@ module API = let ReinterpretConcretes terms t = reinterpretConcretes terms t - let TryPtrToArrayInfo pointerBase sightType offset = - Memory.tryPtrToArrayInfo pointerBase sightType offset + let TryPtrToRef state pointerBase sightType offset = + Memory.tryPtrToRef state pointerBase sightType offset let TryTermToObj state term = Memory.tryTermToObj state term @@ -190,11 +190,7 @@ module API = let SpecializeWithKey constant key writeKey = Memory.specializeWithKey constant key writeKey - let rec HeapReferenceToBoxReference reference = - match reference.term with - | HeapRef(address, typ) -> Ref (BoxedLocation(address, typ)) - | Union gvs -> gvs |> List.map (fun (g, v) -> (g, HeapReferenceToBoxReference v)) |> Merging.merge - | _ -> internalfailf "Unboxing: expected heap reference, but got %O" reference + let HeapReferenceToBoxReference reference = Memory.heapReferenceToBoxReference reference let AddConstraint conditionState condition = Memory.addConstraint conditionState condition @@ -364,42 +360,8 @@ module API = | Union gvs -> gvs |> List.map (fun (g, v) -> (g, ReferenceArrayIndex state v indices valueType)) |> Merging.merge | _ -> internalfailf "Referencing array index: expected reference, but got %O" arrayRef - let rec ReferenceField state reference fieldId = - let declaringType = fieldId.declaringType - let isSuitableField address typ = - let typ = Memory.mostConcreteTypeOfHeapRef state address typ - declaringType.IsAssignableFrom typ - match reference.term with - | HeapRef(address, typ) when isSuitableField address typ |> not -> - // TODO: check this case with casting via "is" - Logger.trace "[WARNING] unsafe cast of term %O in safe context" reference - let offset = Reflection.getFieldIdOffset fieldId |> MakeNumber - Ptr (HeapLocation(address, typ)) fieldId.typ offset - | HeapRef(address, typ) when typ = typeof && fieldId = Reflection.stringFirstCharField -> - let address, arrayType = Memory.stringArrayInfo state address None - ArrayIndex(address, [makeNumber 0], arrayType) |> Ref - | HeapRef(address, typ) when declaringType.IsValueType -> - // TODO: Need to check mostConcreteTypeOfHeapRef using pathCondition? - assert(isSuitableField address typ) - let ref = HeapReferenceToBoxReference reference - ReferenceField state ref fieldId - | HeapRef(address, typ) -> - // TODO: Need to check mostConcreteTypeOfHeapRef using pathCondition? - assert(isSuitableField address typ) - ClassField(address, fieldId) |> Ref - | Ref address when declaringType.IsAssignableFrom(address.TypeOfLocation) -> - assert declaringType.IsValueType - StructField(address, fieldId) |> Ref - | Ref address -> - assert declaringType.IsValueType - let pointerBase, offset = AddressToBaseAndOffset address - let fieldOffset = Reflection.getFieldIdOffset fieldId |> makeNumber - Ptr pointerBase fieldId.typ (add offset fieldOffset) - | Ptr(baseAddress, _, offset) -> - let fieldOffset = Reflection.getFieldIdOffset fieldId |> makeNumber - Ptr baseAddress fieldId.typ (add offset fieldOffset) - | Union gvs -> gvs |> List.map (fun (g, v) -> (g, ReferenceField state v fieldId)) |> Merging.merge - | _ -> internalfailf "Referencing field: expected reference, but got %O" reference + let ReferenceField state reference fieldId = + Memory.referenceField state reference fieldId let private transformBoxedRef ref = match ref.term with @@ -424,8 +386,8 @@ module API = | HeapRef _ | Ptr _ | Ref _ -> ReferenceField state target field |> Memory.read reporter state - | Struct _ -> Memory.readStruct reporter target field - | Combined _ -> Memory.readFieldUnsafe reporter target field + | Struct _ -> Memory.readStruct reporter state target field + | Combined _ -> Memory.readFieldUnsafe reporter state target field | _ -> internalfailf "Reading field of %O" term Merging.guardedApply doRead term diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 9fa6e6a83..eea8b3857 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -71,7 +71,7 @@ module API = val ReinterpretConcretes : term list -> Type -> obj - val TryPtrToArrayInfo : Type -> Type -> term -> option + val TryPtrToRef : state -> pointerBase -> Type -> term -> option
val TryTermToObj : state -> term -> obj option diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 026e6ea8c..82ff2f2b8 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -84,21 +84,6 @@ module internal Memory = add acc absOffset List.fold attachOne (makeNumber 0) [0 .. length] - let tryPtrToArrayInfo (typeOfBase : Type) sightType offset = - assert(typeOf offset = typeof) - let checkType() = - typeOfBase.IsSZArray && typeOfBase.GetElementType() = sightType - || typeOfBase = typeof && sightType = typeof - let mutable elemSize = Nop() - let checkOffset() = - elemSize <- makeNumber (internalSizeOf sightType) - rem offset elemSize = makeNumber 0 - if not typeOfBase.ContainsGenericParameters && checkType() && checkOffset() then - let arrayType = (sightType, 1, true) - let index = div offset elemSize - Some ([index], arrayType) - else None - // -------------------------- Error reporter -------------------------- type internal EmptyErrorReporter() = @@ -965,11 +950,11 @@ module internal Memory = objToTerm state source typ value | _ -> readBoxedSymbolic state address typ - let rec readStruct reporter (structTerm : term) (field : fieldId) = + let rec readStruct reporter state (structTerm : term) (field : fieldId) = match structTerm.term with | Struct(fields, _) -> fields[field] - | Combined _ -> readFieldUnsafe reporter structTerm field - | _ -> internalfailf "Reading field of structure: expected struct, but got %O" structTerm + | Combined _ -> readFieldUnsafe reporter state structTerm field + | _ -> internalfail $"Reading field of structure: expected struct, but got {structTerm}" and private readSafe reporter state = function | PrimitiveStackLocation key -> readStackLocation state key @@ -979,7 +964,7 @@ module internal Memory = | StaticField(typ, field) -> readStaticField state typ field | StructField(address, field) -> let structTerm = readSafe reporter state address - readStruct reporter structTerm field + readStruct reporter state structTerm field | ArrayLength(address, dimension, typ) -> readLength state address dimension typ | BoxedLocation(address, typ) -> readBoxedLocation state address typ | StackBufferIndex(key, index) -> readStackBuffer state key index @@ -1021,35 +1006,39 @@ module internal Memory = // NOTE: returns list of slices // TODO: return empty if every slice is invalid - and private commonReadTermUnsafe (reporter : IErrorReporter) term startByte endByte pos stablePos = - match term.term with - | Struct(fields, t) -> commonReadStructUnsafe reporter fields t startByte endByte pos stablePos - | HeapRef _ - | Ref _ - | Ptr _ -> readAddressUnsafe reporter term startByte endByte - | Combined([t], _) -> commonReadTermUnsafe reporter t startByte endByte pos stablePos - | Combined(slices, _) -> - let readSlice part = commonReadTermUnsafe reporter part startByte endByte pos stablePos + and private commonReadTermUnsafe (reporter : IErrorReporter) term startByte endByte pos stablePos sightType = + let typ = typeOf term + let size = internalSizeOf typ + match term.term, sightType with + | _, Some sightType when startByte = makeNumber 0 && endByte = makeNumber size && typ = sightType -> + List.singleton term + | Struct(fields, t), _ -> commonReadStructUnsafe reporter fields t startByte endByte pos stablePos sightType + | HeapRef _, _ + | Ref _, _ + | Ptr _, _ -> readAddressUnsafe reporter term startByte endByte + | Combined([t], _), _ -> commonReadTermUnsafe reporter t startByte endByte pos stablePos sightType + | Combined(slices, _), _ -> + let readSlice part = commonReadTermUnsafe reporter part startByte endByte pos stablePos sightType List.collect readSlice slices - | Slice _ - | Concrete _ - | Constant _ - | Expression _ -> + | Slice _, _ + | Concrete _, _ + | Constant _, _ + | Expression _, _ -> sliceTerm term startByte endByte pos stablePos |> List.singleton | _ -> internalfailf "readTermUnsafe: unexpected term %O" term - and private readTermUnsafe reporter term startByte endByte = - commonReadTermUnsafe reporter term startByte endByte (neg startByte) false + and private readTermUnsafe reporter term startByte endByte sightType = + commonReadTermUnsafe reporter term startByte endByte (neg startByte) false sightType - and private readTermPartUnsafe reporter term startByte endByte = - commonReadTermUnsafe reporter term startByte endByte startByte true + and private readTermPartUnsafe reporter term startByte endByte sightType = + commonReadTermUnsafe reporter term startByte endByte startByte true sightType - and private commonReadStructUnsafe reporter fields structType startByte endByte pos stablePos = + and private commonReadStructUnsafe reporter fields structType startByte endByte pos stablePos sightType = let readField fieldId = fields[fieldId] - commonReadFieldsUnsafe reporter readField false structType startByte endByte pos stablePos + commonReadFieldsUnsafe reporter readField false structType startByte endByte pos stablePos sightType - and private readStructUnsafe reporter fields structType startByte endByte = - commonReadStructUnsafe reporter fields structType startByte endByte (neg startByte) false + and private readStructUnsafe reporter fields structType startByte endByte sightType = + commonReadStructUnsafe reporter fields structType startByte endByte (neg startByte) false sightType and private getAffectedFields reporter readField isStatic (blockType : Type) startByte endByte = let blockSize = Reflection.blockSize blockType @@ -1088,23 +1077,23 @@ module internal Memory = List.foldBack concreteGetField allFields List.empty | _ -> List.map getField allFields - and private commonReadFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte pos stablePos = + and private commonReadFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte pos stablePos sightType = let affectedFields = getAffectedFields reporter readField isStatic blockType startByte endByte let readField (_, o, v, s, e) = - commonReadTermUnsafe reporter v s e (add pos o) stablePos + commonReadTermUnsafe reporter v s e (add pos o) stablePos sightType List.collect readField affectedFields - and private readFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte = - commonReadFieldsUnsafe reporter readField isStatic blockType startByte endByte (neg startByte) false + and private readFieldsUnsafe reporter readField isStatic (blockType : Type) startByte endByte sightType = + commonReadFieldsUnsafe reporter readField isStatic blockType startByte endByte (neg startByte) false sightType // TODO: Add undefined behaviour: // TODO: 1. when reading info between fields // TODO: 3. when reading info outside block // TODO: 3. reinterpreting ref or ptr should return symbolic ref or ptr - and private readClassUnsafe reporter state address classType offset (viewSize : int) = + and private readClassUnsafe reporter state address classType offset (viewSize : int) sightType = let endByte = makeNumber viewSize |> add offset let readField fieldId = readClassField state address fieldId - readFieldsUnsafe reporter readField false classType offset endByte + readFieldsUnsafe reporter readField false classType offset endByte sightType and arrayIndicesToOffset state address (elementType, dim, _ as arrayType) indices = let lens = List.init dim (fun dim -> readLength state address (makeNumber dim) arrayType) @@ -1135,81 +1124,165 @@ module internal Memory = (indices, element, startByte, endByte), add currentOffset elementSize List.mapFold getElement (mul firstElement elementSize) [0 .. countToRead - 1] |> fst - and private readArrayUnsafe reporter state address arrayType offset viewSize = + and private readArrayUnsafe reporter state address arrayType offset viewSize sightType = let indices = getAffectedIndices reporter state address (symbolicTypeToArrayType arrayType) offset viewSize let readIndex (_, elem, s, e) = - readTermUnsafe reporter elem s e + readTermUnsafe reporter elem s e sightType List.collect readIndex indices - and private readStringUnsafe reporter state address offset viewSize = + and private readStringUnsafe reporter state address offset viewSize sightType = // TODO: handle case, when reading string length let address, arrayType = stringArrayInfo state address None let indices = getAffectedIndices reporter state address arrayType offset viewSize let readChar (_, elem, s, e) = - readTermUnsafe reporter elem s e + readTermUnsafe reporter elem s e sightType List.collect readChar indices - and private readStaticUnsafe reporter state t offset (viewSize : int) = + and private readStaticUnsafe reporter state t offset (viewSize : int) sightType = let endByte = makeNumber viewSize |> add offset let readField fieldId = readStaticField state t fieldId - readFieldsUnsafe reporter readField true t offset endByte + readFieldsUnsafe reporter readField true t offset endByte sightType - and private readStackUnsafe reporter state loc offset (viewSize : int) = + and private readStackUnsafe reporter state loc offset (viewSize : int) sightType = let term = readStackLocation state loc let locSize = sizeOf term |> makeNumber let endByte = makeNumber viewSize |> add offset checkBlockBounds reporter locSize offset endByte - readTermUnsafe reporter term offset endByte + readTermUnsafe reporter term offset endByte sightType - and private readBoxedUnsafe reporter state loc typ offset viewSize = + and private readBoxedUnsafe reporter state loc typ offset viewSize sightType = let address = BoxedLocation(loc, typ) let endByte = makeNumber viewSize |> add offset match readSafe reporter state address with - | {term = Struct(fields, _)} -> readStructUnsafe reporter fields typ offset endByte - | term when isPrimitive typ || typ.IsEnum -> readTermUnsafe reporter term offset endByte + | {term = Struct(fields, _)} -> readStructUnsafe reporter fields typ offset endByte sightType + | term when isPrimitive typ || typ.IsEnum -> readTermUnsafe reporter term offset endByte sightType | term -> internalfail $"readUnsafe: reading struct resulted in term {term}" and private readUnsafe reporter state baseAddress offset sightType = let viewSize = internalSizeOf sightType let slices = + let sightType = Some sightType match baseAddress with - | HeapLocation(loc, sightType) -> - let typ = mostConcreteTypeOfHeapRef state loc sightType + | HeapLocation(loc, t) -> + let typ = mostConcreteTypeOfHeapRef state loc t match typ with - | StringType -> readStringUnsafe reporter state loc offset viewSize - | ClassType _ -> readClassUnsafe reporter state loc typ offset viewSize - | ArrayType _ -> readArrayUnsafe reporter state loc typ offset viewSize + | StringType -> readStringUnsafe reporter state loc offset viewSize sightType + | ClassType _ -> readClassUnsafe reporter state loc typ offset viewSize sightType + | ArrayType _ -> readArrayUnsafe reporter state loc typ offset viewSize sightType | _ when typ = typeof -> internalfail $"readUnsafe: reading from 'Void' by reference {baseAddress}" - | StructType _ -> readBoxedUnsafe reporter state loc typ offset viewSize + | StructType _ -> readBoxedUnsafe reporter state loc typ offset viewSize sightType | _ when isPrimitive typ || typ.IsEnum -> - readBoxedUnsafe reporter state loc typ offset viewSize + readBoxedUnsafe reporter state loc typ offset viewSize sightType | _ -> internalfailf $"Expected complex type, but got {typ}" - | StackLocation loc -> readStackUnsafe reporter state loc offset viewSize - | StaticLocation loc -> readStaticUnsafe reporter state loc offset viewSize + | StackLocation loc -> readStackUnsafe reporter state loc offset viewSize sightType + | StaticLocation loc -> readStaticUnsafe reporter state loc offset viewSize sightType combine slices sightType - and readFieldUnsafe (reporter : IErrorReporter) block (field : fieldId) = - assert(sizeOf block = internalSizeOf field.declaringType) - let fieldType = field.typ - let startByte = Reflection.getFieldIdOffset field - let endByte = startByte + internalSizeOf fieldType - let slices = readTermUnsafe reporter block (makeNumber startByte) (makeNumber endByte) - combine slices fieldType + and readFieldUnsafe (reporter : IErrorReporter) (state : state) (block : term) (field : fieldId) = + let declaringType = field.declaringType + match block.term with + | Combined(_, t) when declaringType.IsAssignableFrom t || sizeOf block = internalSizeOf field.declaringType -> + assert(sizeOf block = internalSizeOf field.declaringType) + let fieldType = field.typ + let startByte = Reflection.getFieldIdOffset field + let endByte = startByte + internalSizeOf fieldType + let sightType = Some fieldType + let slices = readTermUnsafe reporter block (makeNumber startByte) (makeNumber endByte) sightType + combine slices fieldType + | Combined(slices, _) -> + let isSuitableRef slice = + match slice.term with + | _ when isReference slice -> mostConcreteTypeOfRef state slice |> declaringType.IsAssignableFrom + | Ptr(pointerBase, sightType, offset) -> + match tryPtrToRef state pointerBase sightType offset with + | Some address -> declaringType.IsAssignableFrom(address.TypeOfLocation) + | None -> false + | _ -> false + let refs = List.filter isSuitableRef slices |> List.distinct + if List.length refs = 1 then + let ref = List.head refs + referenceField state ref field |> read reporter state + else internalfail $"readFieldUnsafe: unexpected block {block}" + | _ -> internalfail $"readFieldUnsafe: unexpected block {block}" + +// -------------------------------- Pointer helpers -------------------------------- + + and tryPtrToRef state pointerBase sightType offset : address option = + assert(typeOf offset = typeof) + let zero = makeNumber 0 + match pointerBase with + | HeapLocation(address, t) -> + let typ = typeOfHeapLocation state address |> mostConcreteType t + let isArray() = + typ.IsSZArray && typ.GetElementType() = sightType + || typ = typeof && sightType = typeof + if typ.ContainsGenericParameters then None + elif isArray() then + let mutable elemSize = Nop() + let checkOffset() = + elemSize <- makeNumber (internalSizeOf sightType) + rem offset elemSize = zero + if checkOffset() then + let index = div offset elemSize + let address, arrayType = + if t = typeof then stringArrayInfo state address None + else address, (sightType, 1, true) + ArrayIndex(address, [index], arrayType) |> Some + else None + elif typ.IsValueType && sightType = typ && offset = zero then + BoxedLocation(address, t) |> Some + else None + | StackLocation stackKey when stackKey.TypeOfLocation = sightType && offset = zero -> + PrimitiveStackLocation stackKey |> Some + | _ -> None -// --------------------------- General reading --------------------------- + and heapReferenceToBoxReference reference = + match reference.term with + | HeapRef(address, typ) -> Ref (BoxedLocation(address, typ)) + | Union gvs -> gvs |> List.map (fun (g, v) -> (g, heapReferenceToBoxReference v)) |> Merging.merge + | _ -> internalfailf "Unboxing: expected heap reference, but got %O" reference + + and referenceField state reference fieldId = + let declaringType = fieldId.declaringType + let isSuitableField address typ = + let typ = mostConcreteTypeOfHeapRef state address typ + declaringType.IsAssignableFrom typ + match reference.term with + | HeapRef(address, typ) when isSuitableField address typ |> not -> + // TODO: check this case with casting via "is" + Logger.trace "[WARNING] unsafe cast of term %O in safe context" reference + let offset = Reflection.getFieldIdOffset fieldId |> makeNumber + Ptr (HeapLocation(address, typ)) fieldId.typ offset + | HeapRef(address, typ) when typ = typeof && fieldId = Reflection.stringFirstCharField -> + let address, arrayType = stringArrayInfo state address None + ArrayIndex(address, [makeNumber 0], arrayType) |> Ref + | HeapRef(address, typ) when declaringType.IsValueType -> + // TODO: Need to check mostConcreteTypeOfHeapRef using pathCondition? + assert(isSuitableField address typ) + let ref = heapReferenceToBoxReference reference + referenceField state ref fieldId + | HeapRef(address, typ) -> + // TODO: Need to check mostConcreteTypeOfHeapRef using pathCondition? + assert(isSuitableField address typ) + ClassField(address, fieldId) |> Ref + | Ref address when declaringType.IsAssignableFrom(address.TypeOfLocation) -> + assert declaringType.IsValueType + StructField(address, fieldId) |> Ref + | Ref address -> + assert declaringType.IsValueType + let pointerBase, offset = Pointers.addressToBaseAndOffset address + let fieldOffset = Reflection.getFieldIdOffset fieldId |> makeNumber + Ptr pointerBase fieldId.typ (add offset fieldOffset) + | Ptr(baseAddress, _, offset) -> + let fieldOffset = Reflection.getFieldIdOffset fieldId |> makeNumber + Ptr baseAddress fieldId.typ (add offset fieldOffset) + | Union gvs -> gvs |> List.map (fun (g, v) -> (g, referenceField state v fieldId)) |> Merging.merge + | _ -> internalfailf "Referencing field: expected reference, but got %O" reference - let isTypeInitialized state (typ : Type) = - let key : symbolicTypeKey = {typ=typ} - let matchingTypes = SymbolicSet.matchingElements key state.initializedTypes - match matchingTypes with - | [x] when x = key -> True() - | _ -> - let name = sprintf "%O_initialized" typ - let source : typeInitialized = {typ = typ; matchingTypes = SymbolicSet.ofSeq matchingTypes} - Constant name source typeof +// --------------------------- General reading --------------------------- // TODO: take type of heap address - let rec read (reporter : IErrorReporter) state reference = + and read (reporter : IErrorReporter) state reference = match reference.term with | Ref address -> readSafe reporter state address | DetachedPtr _ -> @@ -1225,6 +1298,16 @@ module internal Memory = Nop() | _ -> internalfailf $"Reading: expected reference, but got {reference}" + let isTypeInitialized state (typ : Type) = + let key : symbolicTypeKey = {typ=typ} + let matchingTypes = SymbolicSet.matchingElements key state.initializedTypes + match matchingTypes with + | [x] when x = key -> True() + | _ -> + let name = sprintf "%O_initialized" typ + let source : typeInitialized = {typ = typ; matchingTypes = SymbolicSet.ofSeq matchingTypes} + Constant name source typeof + // ------------------------------- Writing ------------------------------- let writeStackLocation (s : state) key value = @@ -1417,7 +1500,10 @@ module internal Memory = value let rec writeTermUnsafe reporter term startByte value = + let termType = typeOf term + let valueType = typeOf value match term.term with + | _ when startByte = makeNumber 0 && termType = valueType -> value | Struct(fields, t) -> writeStructUnsafe reporter term fields t startByte value | HeapRef _ | Ref _ @@ -1425,9 +1511,8 @@ module internal Memory = | Concrete _ | Constant _ | Expression _ -> - let termType = typeOf term let termSize = internalSizeOf termType - let valueSize = sizeOf value + let valueSize = internalSizeOf valueType match startByte.term with | Concrete(:? int as startByte, _) when startByte = 0 && valueSize = termSize -> combine (List.singleton value) termType @@ -1435,9 +1520,9 @@ module internal Memory = let zero = makeNumber 0 let termSize = makeNumber termSize let valueSize = makeNumber valueSize - let left = readTermPartUnsafe reporter term zero startByte - let valueSlices = readTermUnsafe reporter value (neg startByte) (sub termSize startByte) - let right = readTermPartUnsafe reporter term (add startByte valueSize) termSize + let left = readTermPartUnsafe reporter term zero startByte None + let valueSlices = readTermUnsafe reporter value (neg startByte) (sub termSize startByte) None + let right = readTermPartUnsafe reporter term (add startByte valueSize) termSize None combine (left @ valueSlices @ right) termType | _ -> internalfailf "writeTermUnsafe: unexpected term %O" term @@ -1901,7 +1986,7 @@ module internal Memory = match x.baseSource with | :? IStatedSymbolicConstantSource as baseSource -> let structTerm = baseSource.Compose state - readStruct emptyReporter structTerm x.field + readStruct emptyReporter state structTerm x.field | _ -> let x = x :> ISymbolicConstantSource match state.model with diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index cb0014bf3..e62bd8880 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -892,7 +892,7 @@ module internal Terms = let defaultCase() = Expression Combine terms t let isSolid term typeOfTerm = - typeOfTerm = t || isRefOrPtr term + typeOfTerm = t || isRefOrPtr term && (not t.IsValueType || t.IsByRef || isNative t || t.IsPrimitive) let simplify p s e pos = let typ = typeOf p let termSize = lazy (internalSizeOf typ) From 1819e8acd0dae851f818272b0fd57fb73e9182f6 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:36:42 +0300 Subject: [PATCH 05/20] [fix] fixed concrete memory for empty string case --- VSharp.SILI.Core/ConcreteMemory.fs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index cd580af2f..db0f35768 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/VSharp.SILI.Core/ConcreteMemory.fs @@ -73,7 +73,9 @@ type public ConcreteMemory private (physToVirt, virtToPhys) = if exists && oldPhys = phys then virtToPhys'.Add(virt, phys') let key' = key.FromPhysicalAddress phys' - physToVirt'.Add(key', virt) + // Empty string is interned + if key' = RefKey {object = String.Empty} then physToVirt'[key'] <- virt + else physToVirt'.Add(key', virt) ConcreteMemory(physToVirt', virtToPhys') // ----------------------------- Primitives ----------------------------- From e640ee5ed5a922bdeaab8d77fe56d767d1bb6d96 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:38:46 +0300 Subject: [PATCH 06/20] [feat] added operations to 'Method' --- VSharp.IL/MethodBody.fs | 46 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 42 insertions(+), 4 deletions(-) diff --git a/VSharp.IL/MethodBody.fs b/VSharp.IL/MethodBody.fs index f7d9c4b2d..c57dbd1a7 100644 --- a/VSharp.IL/MethodBody.fs +++ b/VSharp.IL/MethodBody.fs @@ -30,6 +30,7 @@ type MethodWithBody internal (m : MethodBase) = let returnType = Reflection.getMethodReturnType m let parameters = m.GetParameters() let hasThis = Reflection.hasThis m + let hasNonVoidResult = lazy(Reflection.hasNonVoidResult m) let isDynamic = m :? DynamicMethod let metadataToken = if isDynamic then m.GetHashCode() else m.MetadataToken let isStatic = m.IsStatic @@ -45,11 +46,22 @@ type MethodWithBody internal (m : MethodBase) = let methodImplementationFlags = lazy m.GetMethodImplementationFlags() let isDelegateConstructor = lazy(Reflection.isDelegateConstructor m) let isDelegate = lazy(Reflection.isDelegate m) - let isFSharpInternalCall = lazy(Map.containsKey fullGenericMethodName.Value Loader.FSharpImplementations) + let tryFSharpInternalCall = lazy(Map.tryFind fullGenericMethodName.Value Loader.FSharpImplementations) + let isFSharpInternalCall = lazy(Option.isSome tryFSharpInternalCall.Value) let isCSharpInternalCall = lazy(Map.containsKey fullGenericMethodName.Value Loader.CSharpImplementations) - let isCilStateInternalCall = lazy(Seq.contains fullGenericMethodName.Value Loader.CilStateImplementations) + let isShimmed = lazy(Loader.isShimmed fullGenericMethodName.Value) + let isConcreteCall = lazy(Loader.isInvokeInternalCall fullGenericMethodName.Value) + let isRuntimeException = lazy(Loader.isRuntimeExceptionsImplementation fullGenericMethodName.Value) + let runtimeExceptionImpl = lazy(Map.tryFind fullGenericMethodName.Value Loader.runtimeExceptionsConstructors) + let isNotImplementedIntrinsic = + lazy( + let isIntrinsic = + let intrinsicAttr = "System.Runtime.CompilerServices.IntrinsicAttribute" + customAttributes |> Seq.exists (fun m -> m.AttributeType.ToString() = intrinsicAttr) + isIntrinsic && (Array.contains fullGenericMethodName.Value Loader.trustedIntrinsics |> not) + ) let isImplementedInternalCall = - lazy(isFSharpInternalCall.Value || isCSharpInternalCall.Value || isCilStateInternalCall.Value) + lazy(isFSharpInternalCall.Value || isCSharpInternalCall.Value) let isInternalCall = lazy ( int (m.GetMethodImplementationFlags() &&& MethodImplAttributes.InternalCall) <> 0 @@ -60,7 +72,7 @@ type MethodWithBody internal (m : MethodBase) = if not isCSharpInternalCall.Value then m else Loader.CSharpImplementations[fullGenericMethodName.Value] let methodBodyBytes = - if isFSharpInternalCall.Value || isCilStateInternalCall.Value then null + if isFSharpInternalCall.Value then null else actualMethod.GetMethodBody() let localVariables = if methodBodyBytes = null then null else methodBodyBytes.LocalVariables let methodBody = lazy( @@ -107,6 +119,9 @@ type MethodWithBody internal (m : MethodBase) = member x.DeclaringType = declaringType member x.ReflectedType = m.ReflectedType member x.Parameters = parameters + member x.HasParameterOnStack = + x.DeclaringType.IsValueType && not x.IsStatic + || x.Parameters |> Array.exists (fun p -> p.ParameterType.IsByRef) member x.LocalVariables = localVariables member x.HasThis = hasThis member x.MetadataToken = metadataToken @@ -199,6 +214,8 @@ type MethodWithBody internal (m : MethodBase) = member x.IsExternalMethod with get() = Reflection.isExternalMethod m member x.IsQCall with get() = DllManager.isQCall m + member x.HasNonVoidResult = hasNonVoidResult.Value + interface VSharp.Core.IMethod with override x.Name = name override x.FullName = fullName @@ -235,6 +252,27 @@ type MethodWithBody internal (m : MethodBase) = member x.IsInternalCall with get() = isInternalCall.Value member x.IsImplementedInternalCall with get () = isImplementedInternalCall.Value + member x.IsShimmed with get() = isShimmed.Value + + member x.CanCallConcrete with get() = x.IsConcretelyInvokable && isConcreteCall.Value + + member x.IsFSharpInternalCall with get() = isFSharpInternalCall.Value + member x.IsCSharpInternalCall with get() = isCSharpInternalCall.Value + + member x.GetInternalCall with get() = + match tryFSharpInternalCall.Value with + | Some method -> method + | None -> internalfail $"GetInternalCall: no internal call for method {fullGenericMethodName.Value}" + + member x.IsRuntimeException with get() = isRuntimeException.Value + member x.HasRuntimeExceptionImpl with get() = Option.isSome runtimeExceptionImpl.Value + member x.RuntimeExceptionImpl with get() = + match runtimeExceptionImpl.Value with + | Some ctor -> ctor + | None -> internalfail $"RuntimeExceptionImpl: no runtime exception implementation for method {fullGenericMethodName.Value}" + + member x.IsNotImplementedIntrinsic with get() = isNotImplementedIntrinsic.Value + member x.CanBeOverriden targetType = match m with | :? ConstructorInfo -> false From 8717197bea0b74d39d4dde7de5a28ba282f1228d Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:39:45 +0300 Subject: [PATCH 07/20] [style] added exceptions handling in 'MkModel' --- VSharp.Solver/Z3.fs | 212 ++++++++++++++++++++++---------------------- 1 file changed, 107 insertions(+), 105 deletions(-) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index fd80bd172..95c516846 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -1062,117 +1062,119 @@ module internal Z3 = term.Value <- x.WriteByPath term.Value value path.parts member x.MkModel (m : Model) = - let subst = Dictionary() - let stackEntries = Dictionary() - let state = {Memory.EmptyState() with complete = true} - - for KeyValue(key, value) in encodingCache.t2e do - match key with - | {term = Constant(_, Path.Path(path, StackReading(key)), t)} as constant -> - let refinedExpr = m.Eval(value.expr, false) - let decoded = x.Decode t refinedExpr - if decoded <> constant then - x.WriteDictOfValueTypes stackEntries key path key.TypeOfLocation decoded - | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} as constant -> - match ms with - | HeapAddressSource(Path.Path(path, StackReading(key))) -> + try + let subst = Dictionary() + let stackEntries = Dictionary() + let state = {Memory.EmptyState() with complete = true} + + for KeyValue(key, value) in encodingCache.t2e do + match key with + | {term = Constant(_, Path.Path(path, StackReading(key)), t)} as constant -> let refinedExpr = m.Eval(value.expr, false) - let t = if path.IsEmpty then key.TypeOfLocation else path.TypeOfLocation - let address = x.DecodeConcreteHeapAddress refinedExpr |> ConcreteHeapAddress - let value = HeapRef address t - x.WriteDictOfValueTypes stackEntries key path key.TypeOfLocation value - | HeapAddressSource(Path.Path(_, (:? functionResultConstantSource as frs))) - | Path.Path(_, (:? functionResultConstantSource as frs)) -> + let decoded = x.Decode t refinedExpr + if decoded <> constant then + x.WriteDictOfValueTypes stackEntries key path key.TypeOfLocation decoded + | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} as constant -> + match ms with + | HeapAddressSource(Path.Path(path, StackReading(key))) -> + let refinedExpr = m.Eval(value.expr, false) + let t = if path.IsEmpty then key.TypeOfLocation else path.TypeOfLocation + let address = x.DecodeConcreteHeapAddress refinedExpr |> ConcreteHeapAddress + let value = HeapRef address t + x.WriteDictOfValueTypes stackEntries key path key.TypeOfLocation value + | HeapAddressSource(Path.Path(_, (:? functionResultConstantSource as frs))) + | Path.Path(_, (:? functionResultConstantSource as frs)) -> + let refinedExpr = m.Eval(value.expr, false) + let t = (frs :> ISymbolicConstantSource).TypeOfLocation + let term = x.Decode t refinedExpr + assert(not (constant = term) || value.expr = refinedExpr) + if constant <> term then subst.Add(ms, term) + | _ -> () + | {term = Constant(_, :? IStatedSymbolicConstantSource, _)} -> () + | {term = Constant(_, source, t)} as constant -> let refinedExpr = m.Eval(value.expr, false) - let t = (frs :> ISymbolicConstantSource).TypeOfLocation let term = x.Decode t refinedExpr assert(not (constant = term) || value.expr = refinedExpr) - if constant <> term then subst.Add(ms, term) + if constant <> term then subst.Add(source, term) | _ -> () - | {term = Constant(_, :? IStatedSymbolicConstantSource, _)} -> () - | {term = Constant(_, source, t)} as constant -> - let refinedExpr = m.Eval(value.expr, false) - let term = x.Decode t refinedExpr - assert(not (constant = term) || value.expr = refinedExpr) - if constant <> term then subst.Add(source, term) - | _ -> () - - let frame = stackEntries |> Seq.map (fun kvp -> - let key = kvp.Key - let term = kvp.Value.Value - let typ = TypeOf term - (key, Some term, typ)) - Memory.NewStackFrame state None (List.ofSeq frame) - - let pointers = Dictionary() - let defaultValues = Dictionary() - for kvp in encodingCache.regionConstants do - let region, path = kvp.Key - let constant = kvp.Value - let arr = m.Eval(constant, false) - let typeOfLocation = - if path.IsEmpty then region.TypeOfLocation - else path.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 region.TypeOfLocation constantValue - elif arr.IsDefaultArray then - assert(arr.Args.Length = 1) - elif arr.IsStore then - assert(arr.Args.Length >= 3) - 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 - let address, ptrPart = path.ToAddress address - match ptrPart with - | Some kind -> - let exists, ptr = pointers.TryGetValue(address) - let ptr = - if exists then ptr - else Memory.DefaultOf address.TypeOfLocation - match kind, ptr.term with - | PointerAddress, Ptr(HeapLocation(_, t), s, o) -> - pointers[address] <- Ptr (HeapLocation(value, t)) s o - | PointerOffset, Ptr(HeapLocation(a, t), s, _) -> - pointers[address] <- Ptr (HeapLocation(a, t)) s value - | _ -> internalfail $"MkModel: unexpected path {kind}" - | None -> - let states = Memory.Write state (Ref address) value - assert(states.Length = 1 && states[0] = state) - elif arr.IsConst then () - elif arr.IsQuantifier then - let quantifier = arr :?> Quantifier - let body = quantifier.Body - // This case decodes predicates, for example: \x -> x = 100, where 'x' is address - if body.IsApp && body.IsEq && body.Args.Length = 2 then - // Firstly, setting all values to 'false' - x.WriteDictOfValueTypes defaultValues region path region.TypeOfLocation (MakeBool false) - let address = x.DecodeMemoryKey region (Array.singleton body.Args[1]) + + let frame = stackEntries |> Seq.map (fun kvp -> + let key = kvp.Key + let term = kvp.Value.Value + let typ = TypeOf term + (key, Some term, typ)) + Memory.NewStackFrame state None (List.ofSeq frame) + + let pointers = Dictionary() + let defaultValues = Dictionary() + for kvp in encodingCache.regionConstants do + let region, path = kvp.Key + let constant = kvp.Value + let arr = m.Eval(constant, false) + let typeOfLocation = + if path.IsEmpty then region.TypeOfLocation + else path.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 region.TypeOfLocation constantValue + elif arr.IsDefaultArray then + assert(arr.Args.Length = 1) + elif arr.IsStore then + assert(arr.Args.Length >= 3) + 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 let address, ptrPart = path.ToAddress address - assert(Option.isNone ptrPart) - // Secondly, setting 'true' value for concrete address from predicate - let states = Memory.Write state (Ref address) (MakeBool true) - assert(states.Length = 1 && states[0] = state) - else internalfailf "Unexpected quantifier expression in model: %O" arr - else internalfailf "Unexpected array expression in model: %O" arr - parseArray arr - - for KeyValue(address, ptr) in pointers do - let states = Memory.Write state (Ref address) ptr - assert(states.Length = 1 && states[0] = state) - - for kvp in defaultValues do - let region = kvp.Key - let constantValue = kvp.Value.Value - Memory.FillRegion state constantValue region - - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] - - encodingCache.heapAddresses.Clear() - state.model <- PrimitiveModel subst - StateModel state + match ptrPart with + | Some kind -> + let exists, ptr = pointers.TryGetValue(address) + let ptr = + if exists then ptr + else Memory.DefaultOf address.TypeOfLocation + match kind, ptr.term with + | PointerAddress, Ptr(HeapLocation(_, t), s, o) -> + pointers[address] <- Ptr (HeapLocation(value, t)) s o + | PointerOffset, Ptr(HeapLocation(a, t), s, _) -> + pointers[address] <- Ptr (HeapLocation(a, t)) s value + | _ -> internalfail $"MkModel: unexpected path {kind}" + | None -> + let states = Memory.Write state (Ref address) value + assert(states.Length = 1 && states[0] = state) + elif arr.IsConst then () + elif arr.IsQuantifier then + let quantifier = arr :?> Quantifier + let body = quantifier.Body + // This case decodes predicates, for example: \x -> x = 100, where 'x' is address + if body.IsApp && body.IsEq && body.Args.Length = 2 then + // Firstly, setting all values to 'false' + x.WriteDictOfValueTypes defaultValues region path region.TypeOfLocation (MakeBool false) + let address = x.DecodeMemoryKey region (Array.singleton body.Args[1]) + let address, ptrPart = path.ToAddress address + assert(Option.isNone ptrPart) + // Secondly, setting 'true' value for concrete address from predicate + let states = Memory.Write state (Ref address) (MakeBool true) + assert(states.Length = 1 && states[0] = state) + else internalfailf "Unexpected quantifier expression in model: %O" arr + else internalfailf "Unexpected array expression in model: %O" arr + parseArray arr + + for KeyValue(address, ptr) in pointers do + let states = Memory.Write state (Ref address) ptr + assert(states.Length = 1 && states[0] = state) + + for kvp in defaultValues do + let region = kvp.Key + let constantValue = kvp.Value.Value + Memory.FillRegion state constantValue region + + state.startingTime <- [encodingCache.lastSymbolicAddress - 1] + + encodingCache.heapAddresses.Clear() + state.model <- PrimitiveModel subst + StateModel state + with e -> internalfail $"MkModel: caught exception {e}" let private ctx = new Context() From 3b4489881a0dd4f2a154b68d646428c052ecc5f0 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:43:26 +0300 Subject: [PATCH 08/20] [fix] fixed 'ldobj' instruction --- VSharp.SILI/Interpreter.fs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index 24df2aa4b..7e791ebf8 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -1167,7 +1167,7 @@ type internal ILInterpreter() as this = // TODO: add Address function for array and return Ptr #do elif x.IsArrayGetOrSet method then x.InvokeArrayGetOrSet cilState method thisOption typeAndMethodArgs |> List.map fallThroughCall |> k - elif ExternMocker.ExtMocksSupported && x.ShouldMock method fullMethodName then + elif ExternMocker.ExtMocksSupported && x.ShouldMock method then let mockMethod = ExternMockAndCall cilState.state method None [] match mockMethod with | Some symVal -> @@ -1521,14 +1521,14 @@ type internal ILInterpreter() as this = let address = pop cilState let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Ldobj.Size) let readValue cilState k = + let actualType = MostConcreteTypeOfRef cilState.state address let value = - if IsPtr address then - let address = Types.Cast address (typ.MakePointerType()) - read cilState address - else - // TODO: try always cast reference, instead of value + if typ.IsAssignableFrom actualType then let value = read cilState address Types.Cast value typ + else + let address = Types.Cast address (typ.MakePointerType()) + read cilState address push value cilState List.singleton cilState |> k x.NpeOrInvokeStatementCIL cilState address readValue id From 9c94f639763da899b2126613f8f78931c367f829 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:44:43 +0300 Subject: [PATCH 09/20] [style] fixed style --- VSharp.CSharpUtils/ReflectionUtils.cs | 4 +++- VSharp.TestGenerator/TestGenerator.fs | 8 +++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/VSharp.CSharpUtils/ReflectionUtils.cs b/VSharp.CSharpUtils/ReflectionUtils.cs index 0ddef67de..071749594 100644 --- a/VSharp.CSharpUtils/ReflectionUtils.cs +++ b/VSharp.CSharpUtils/ReflectionUtils.cs @@ -48,7 +48,9 @@ public static IEnumerable EnumerateExplorableTypes(this Assembly assembly) private static bool IsPublic(Type t) { Debug.Assert(t != null && t != t.DeclaringType); - return t.IsPublic || t.IsNestedPublic && IsPublic(t.DeclaringType); + return + t.IsPublic + || t is { IsNestedPublic: true, DeclaringType: not null } && IsPublic(t.DeclaringType); } public static IEnumerable GetExportedTypesChecked(this Assembly assembly) diff --git a/VSharp.TestGenerator/TestGenerator.fs b/VSharp.TestGenerator/TestGenerator.fs index 5275de6bd..e78f7c918 100644 --- a/VSharp.TestGenerator/TestGenerator.fs +++ b/VSharp.TestGenerator/TestGenerator.fs @@ -351,13 +351,11 @@ module TestGenerator = let private model2test (test : UnitTest) suite indices mockCache (m : Method) model (state : state) = let suitableState state = - let methodHasByRefParameter = m.Parameters |> Seq.exists (fun pi -> pi.ParameterType.IsByRef) - if m.DeclaringType.IsValueType && not m.IsStatic || methodHasByRefParameter then - Memory.CallStackSize state = 2 + if m.HasParameterOnStack then Memory.CallStackSize state = 2 else Memory.CallStackSize state = 1 - if not <| suitableState state - then internalfail "Finished state has many frames on stack! (possibly unhandled exception)" + if not <| suitableState state then + internalfail "Finished state has many frames on stack! (possibly unhandled exception)" match model with | StateModel modelState -> modelState2test test suite indices mockCache m model modelState state From ad85ee289fce89e937044170043890b74a56da19 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:46:33 +0300 Subject: [PATCH 10/20] [fix] fixed internal calls --- VSharp.InternalCalls/Buffer.fs | 69 ++++++++++++++++++++++----------- VSharp.InternalCalls/Buffer.fsi | 8 ++-- VSharp.InternalCalls/Span.fs | 12 ++++-- 3 files changed, 60 insertions(+), 29 deletions(-) diff --git a/VSharp.InternalCalls/Buffer.fs b/VSharp.InternalCalls/Buffer.fs index 8f8c6159f..20af0191b 100644 --- a/VSharp.InternalCalls/Buffer.fs +++ b/VSharp.InternalCalls/Buffer.fs @@ -6,48 +6,73 @@ open VSharp.Core // ------------------------------ System.Buffer -------------------------------- -module Buffer = +module internal Buffer = - let private Memmove (state : state) dst src elemCount = - let elemCount = Types.Cast elemCount typeof - let getArrayInfo ref = - match ref.term with - | Ref(ArrayIndex(address, indices, arrayType)) -> address, indices, arrayType - | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField -> + let private getArrayInfo state ref = + let zero = MakeNumber 0 + match ref.term with + | HeapRef(address, _) -> + let t = MostConcreteTypeOfRef state ref + if TypeUtils.isArrayType t then + let elemType = t.GetElementType() + let indices, arrayType = + if t.IsSZArray then [zero], (elemType, 1, true) + else + let rank = t.GetArrayRank() + let indices = List.init rank (fun _ -> zero) + let arrayType = (elemType, rank, false) + indices, arrayType + address, indices, arrayType + elif t = typeof then let address, stringArrayType = Memory.StringArrayInfo state address None - address, [MakeNumber 0], stringArrayType - | Ptr(HeapLocation(address, t), sightType, offset) -> - match TryPtrToArrayInfo t sightType offset with - | Some(index, arrayType) -> - let address = - if t = typeof then Memory.StringArrayInfo state address None |> fst - else address - address, index, arrayType - | None -> internalfail $"Memmove: unexpected pointer {ref}" - | _ -> internalfail $"Memmove: unexpected reference {ref}" - let dstAddr, dstIndices, dstArrayType = getArrayInfo dst - let srcAddr, srcIndices, srcArrayType = getArrayInfo src + address, [zero], stringArrayType + else internalfail $"Memmove: unexpected HeapRef type {t}" + | Ref(ArrayIndex(address, indices, arrayType)) -> address, indices, arrayType + | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField -> + let address, stringArrayType = Memory.StringArrayInfo state address None + address, [zero], stringArrayType + | Ptr(HeapLocation _ as pointerBase, sightType, offset) -> + match TryPtrToRef state pointerBase sightType offset with + | Some(ArrayIndex(address, index, arrayType)) -> address, index, arrayType + | _ -> internalfail $"Memmove: unexpected pointer {ref}" + | _ -> internalfail $"Memmove: unexpected reference {ref}" + + let CommonMemmove (state : state) dst dstIndex src srcIndex elemCount = + let elemCount = Types.Cast elemCount typeof + let dstAddr, dstIndices, dstArrayType = getArrayInfo state dst + let srcAddr, srcIndices, srcArrayType = getArrayInfo state src let dstType = Types.ArrayTypeToSymbolicType dstArrayType let srcType = Types.ArrayTypeToSymbolicType srcArrayType let dstHeapRef = HeapRef dstAddr dstType let srcHeapRef = HeapRef srcAddr srcType let dstLinearIndex = Memory.LinearizeArrayIndex state dstAddr dstIndices dstArrayType + let dstLinearIndex = + match dstIndex with + | Some dstIndex -> API.Arithmetics.Add dstLinearIndex dstIndex + | None -> dstLinearIndex let srcLinearIndex = Memory.LinearizeArrayIndex state srcAddr srcIndices srcArrayType + let srcLinearIndex = + match srcIndex with + | Some srcIndex -> API.Arithmetics.Add srcLinearIndex srcIndex + | None -> srcLinearIndex Memory.CopyArray state srcHeapRef srcLinearIndex srcType dstHeapRef dstLinearIndex dstType elemCount - let internal GenericMemmove (state : state) (args : term list) : term = + let Memmove (state : state) dst src elemCount = + CommonMemmove state dst None src None elemCount + + let GenericMemmove (state : state) (args : term list) : term = assert(List.length args = 4) let dst, src, elemCount = args[1], args[2], args[3] Memmove state dst src elemCount Nop() - let internal ByteMemmove (state : state) (args : term list) : term = + let ByteMemmove (state : state) (args : term list) : term = assert(List.length args = 3) let dst, src, elemCount = args[0], args[1], args[2] Memmove state dst src elemCount Nop() - let internal MemoryCopy (state : state) (args : term list) : term = + let MemoryCopy (state : state) (args : term list) : term = assert(List.length args = 4) let dst, src, dstSize, count = args[0], args[1], args[2], args[3] // TODO: use 'dstSize' to check for exception diff --git a/VSharp.InternalCalls/Buffer.fsi b/VSharp.InternalCalls/Buffer.fsi index b40f9b48f..1fdcf6510 100644 --- a/VSharp.InternalCalls/Buffer.fsi +++ b/VSharp.InternalCalls/Buffer.fsi @@ -6,11 +6,13 @@ open VSharp.Core module internal Buffer = + val CommonMemmove : state -> term -> term option -> term -> term option -> term -> unit + [] - val internal GenericMemmove : state -> term list -> term + val GenericMemmove : state -> term list -> term [] - val internal ByteMemmove : state -> term list -> term + val ByteMemmove : state -> term list -> term [] - val internal MemoryCopy : state -> term list -> term + val MemoryCopy : state -> term list -> term diff --git a/VSharp.InternalCalls/Span.fs b/VSharp.InternalCalls/Span.fs index ee7469a25..6fdf7d560 100644 --- a/VSharp.InternalCalls/Span.fs +++ b/VSharp.InternalCalls/Span.fs @@ -60,12 +60,16 @@ module ReadOnlySpan = HeapRef address typeof | Ref(ArrayIndex(addr, indices, arrayType)) when indices = [MakeNumber 0] -> CreateArrayRef addr indices arrayType - | Ptr(HeapLocation(address, t), sightType, offset) -> - match TryPtrToArrayInfo t sightType offset with - | Some(indices, arrayType) -> CreateArrayRef address indices arrayType + | Ptr(HeapLocation(_, t) as pointerBase, sightType, offset) -> + match TryPtrToRef state pointerBase sightType offset with + | Some(ArrayIndex(address, indices, arrayType)) -> CreateArrayRef address indices arrayType + | Some address -> Ref address | None when t.IsSZArray || t = typeof -> ptr | None -> internalfail $"GetContentsRef: unexpected pointer to contents {ptr}" - | Ptr _ when len = MakeNumber 1 -> ptr + | Ptr(pointerBase, sightType, offset) when len = MakeNumber 1 -> + match TryPtrToRef state pointerBase sightType offset with + | Some address -> Ref address + | _ -> ptr | _ -> internalfail $"GetContentsRef: unexpected reference to contents {ptr}" let internal GetItemFromReadOnlySpan (state : state) (args : term list) : term = From fe3720530e7cca31034a8cbb1e83e878aae7037e Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:56:41 +0300 Subject: [PATCH 11/20] [refactor] internal calls use cilState - VSharp.SILI splitted on two projects: VSharp.SILI (interpreter and cilState operations) and VSharp.SVM (searchers and others) - Loader moved to VSharp.IL - VSharp.InternalCalls is dependent on VSharp.SILI - ErrorReporter moved to 'CilState.fs' - added 'errorReported' field to 'cilState' --- VSharp.API/VSharp.API.csproj | 1 + VSharp.API/VSharp.cs | 6 +- VSharp.IL/VSharp.IL.fsproj | 2 +- VSharp.InternalCalls/Helpers.fs | 5 + VSharp.InternalCalls/Interlocked.fs | 72 ++- VSharp.InternalCalls/Interlocked.fsi | 17 +- ...Runtime.CompilerServices.RuntimeHelpers.fs | 12 +- ...untime.CompilerServices.RuntimeHelpers.fsi | 7 +- VSharp.InternalCalls/String.fs | 70 ++- VSharp.InternalCalls/String.fsi | 10 + VSharp.InternalCalls/SystemArray.fs | 145 +++++ VSharp.InternalCalls/SystemArray.fsi | 25 + VSharp.InternalCalls/Thread.fs | 20 + VSharp.InternalCalls/Thread.fsi | 21 +- .../VSharp.InternalCalls.fsproj | 12 +- VSharp.SILI/CILState.fs | 108 +++- VSharp.SILI/Interpreter.fs | 592 ++++-------------- VSharp.SILI/VSharp.SILI.fsproj | 17 - VSharp.Test/Benchmarks/BenchmarkResult.cs | 4 +- VSharp.Test/Benchmarks/Benchmarks.cs | 6 +- VSharp.Test/Benchmarks/SearcherBenchmarks.cs | 1 + VSharp.Test/CsvStatisticsReporter.cs | 10 +- VSharp.Test/ExecutionTreeTests.cs | 2 +- VSharp.Test/IntegrationTests.cs | 15 +- VSharp.Test/TestStatistics.cs | 7 +- VSharp.sln | 8 + 26 files changed, 622 insertions(+), 573 deletions(-) diff --git a/VSharp.API/VSharp.API.csproj b/VSharp.API/VSharp.API.csproj index 514039e49..4cb08c6b6 100644 --- a/VSharp.API/VSharp.API.csproj +++ b/VSharp.API/VSharp.API.csproj @@ -60,6 +60,7 @@ + diff --git a/VSharp.API/VSharp.cs b/VSharp.API/VSharp.cs index 2d46d3e77..f0ff1f033 100644 --- a/VSharp.API/VSharp.cs +++ b/VSharp.API/VSharp.cs @@ -8,6 +8,7 @@ using System.Text; using VSharp.CSharpUtils; using VSharp.Interpreter.IL; +using VSharp.SVM; namespace VSharp { @@ -117,7 +118,7 @@ private static Statistics StartExploration( var baseSearchMode = options.SearchStrategy.ToSiliMode(); // TODO: customize search strategies via console options var siliOptions = - new SiliOptions( + new SVMOptions( explorationMode: explorationMode.NewTestCoverageMode( coverageZone, options.Timeout > 0 ? searchMode.NewFairMode(baseSearchMode) : baseSearchMode @@ -135,7 +136,7 @@ private static Statistics StartExploration( stepsLimit: options.StepsLimit ); - using var explorer = new SILI(siliOptions); + using var explorer = new SVM.SVM(siliOptions); var statistics = explorer.Statistics; void HandleInternalFail(Method? method, Exception exception) @@ -148,6 +149,7 @@ void HandleInternalFail(Method? method, Exception exception) if (exception is UnknownMethodException unknownMethodException) { Logger.printLogString(Logger.Error, $"Unknown method: {unknownMethodException.Method.FullName}"); + Logger.printLogString(Logger.Error, $"StackTrace: {unknownMethodException.InterpreterStackTrace}"); return; } diff --git a/VSharp.IL/VSharp.IL.fsproj b/VSharp.IL/VSharp.IL.fsproj index 0f7afa0cc..4e92c2b05 100644 --- a/VSharp.IL/VSharp.IL.fsproj +++ b/VSharp.IL/VSharp.IL.fsproj @@ -14,6 +14,7 @@ + @@ -22,7 +23,6 @@ - diff --git a/VSharp.InternalCalls/Helpers.fs b/VSharp.InternalCalls/Helpers.fs index 46173151c..78ff5c55f 100644 --- a/VSharp.InternalCalls/Helpers.fs +++ b/VSharp.InternalCalls/Helpers.fs @@ -10,3 +10,8 @@ module internal Helpers = match term.term with | Concrete(:? Type as t, _) -> t | _ -> internalfail $"InternalCalls: unexpected wrapped type {term}" + +module SetUp = + + let ConfigureInternalCalls() = + Loader.SetInternalCallsAssembly (System.Reflection.Assembly.GetExecutingAssembly()) diff --git a/VSharp.InternalCalls/Interlocked.fs b/VSharp.InternalCalls/Interlocked.fs index ba8abcd26..407b6c922 100644 --- a/VSharp.InternalCalls/Interlocked.fs +++ b/VSharp.InternalCalls/Interlocked.fs @@ -3,58 +3,70 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations module internal Interlocked = - let exchange state location value = - let currentValue = Memory.Read state location - let state' = Memory.Write state location value - List.map (withFst currentValue) state' - - let compareExchange state location value compared = - let currentValue = Memory.Read state location - let state' = - StatedConditionalExecutionAppendResults state - (fun state k -> k (currentValue === compared, state)) - (fun state k -> k (Memory.Write state location value)) - (fun state k -> k (List.singleton state)) - id - List.map (withFst currentValue) state' - - let genericCompareExchange (state : state) (args : term list) : (term * state) list = + let exchange (interpreter : IInterpreter) cilState location value = + let exchange cilState k = + let currentValue = read cilState location + let cilStates = write cilState location value + for cilState in cilStates do + push currentValue cilState + k cilStates + interpreter.NpeOrInvoke cilState location exchange id + + let compareExchange (interpreter : IInterpreter) cilState location value compared = + let compareExchange cilState k = + let currentValue = read cilState location + let cilStates = + StatedConditionalExecutionCIL cilState + (fun cilState k -> k (currentValue === compared, cilState)) + (fun cilState k -> k (write cilState location value)) + (fun cilState k -> k (List.singleton cilState)) + id + for cilState in cilStates do + push currentValue cilState + k cilStates + interpreter.NpeOrInvoke cilState location compareExchange id + + let genericCompareExchange (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 4) let location, value, compared = args[1], args[2], args[3] - compareExchange state location value compared + compareExchange interpreter cilState location value compared - let intCompareExchange (state : state) (args : term list) : (term * state) list = + let intCompareExchange (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 3) let location, value, compared = args[0], args[1], args[2] - compareExchange state location value compared + compareExchange interpreter cilState location value compared - let intPtrCompareExchange (state : state) (args : term list) : (term * state) list = + let intPtrCompareExchange (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 3) let location, value, compared = args[0], args[1], args[2] - compareExchange state location value compared + compareExchange interpreter cilState location value compared - let genericExchange (state : state) (args : term list) : (term * state) list = + let genericExchange (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 3) let location, value = args[1], args[2] - exchange state location value + exchange interpreter cilState location value - let intExchange (state : state) (args : term list) : (term * state) list = + let intExchange (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 2) let location, value = args[0], args[1] - exchange state location value + exchange interpreter cilState location value - let intExchangeAdd (state : state) (args : term list) : (term * state) list = + let intExchangeAdd (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 2) let location, value = args[0], args[1] - exchange state location (Arithmetics.Add (Memory.Read state location) value) + let value = Arithmetics.Add (read cilState location) value + exchange interpreter cilState location value - let longExchangeAdd (state : state) (args : term list) : (term * state) list = + let longExchangeAdd (interpreter : IInterpreter) cilState (args : term list) = assert(List.length args = 2) let location, value = args[0], args[1] - exchange state location (Arithmetics.Add (Memory.Read state location) value) + let value = Arithmetics.Add (read cilState location) value + exchange interpreter cilState location value - let memoryBarrier (state : state) (args : term list) : term = + let memoryBarrier (_ : state) (_ : term list) : term = Nop() diff --git a/VSharp.InternalCalls/Interlocked.fsi b/VSharp.InternalCalls/Interlocked.fsi index e6b9238e7..e437b4205 100644 --- a/VSharp.InternalCalls/Interlocked.fsi +++ b/VSharp.InternalCalls/Interlocked.fsi @@ -3,30 +3,31 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL module internal Interlocked = [] - val internal genericCompareExchange : state -> term list -> (term * state) list + val genericCompareExchange : IInterpreter -> cilState -> term list -> cilState list [] - val internal intCompareExchange : state -> term list -> (term * state) list + val intCompareExchange : IInterpreter -> cilState -> term list -> cilState list [] [] - val internal intPtrCompareExchange : state -> term list -> (term * state) list + val intPtrCompareExchange : IInterpreter -> cilState -> term list -> cilState list [] - val internal genericExchange : state -> term list -> (term * state) list + val genericExchange : IInterpreter -> cilState -> term list -> cilState list [] - val internal intExchange : state -> term list -> (term * state) list + val intExchange : IInterpreter -> cilState -> term list -> cilState list [] - val internal intExchangeAdd : state -> term list -> (term * state) list + val intExchangeAdd : IInterpreter -> cilState -> term list -> cilState list [] - val internal longExchangeAdd : state -> term list -> (term * state) list + val longExchangeAdd : IInterpreter -> cilState -> term list -> cilState list [] - val internal memoryBarrier : state -> term list -> term + val memoryBarrier : state -> term list -> term diff --git a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs index 89f46cafe..97594ee18 100644 --- a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs +++ b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fs @@ -3,8 +3,7 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core -open System.Runtime.InteropServices -open System.Reflection +open VSharp.Interpreter.IL module Runtime_CompilerServices_RuntimeHelpers = @@ -20,7 +19,7 @@ module Runtime_CompilerServices_RuntimeHelpers = let typ = List.head args |> Helpers.unwrapType MakeBool (Reflection.isReferenceOrContainsReferences typ) - let CommonGetHashCode (state : state) (args : term list) : term = + let CommonGetHashCode (_ : state) (args : term list) : term = assert(List.length args = 1) let object = List.head args GetHashCode object @@ -37,7 +36,12 @@ module Runtime_CompilerServices_RuntimeHelpers = let enumValue = Memory.Read state boxedThis GetHashCode enumValue - let Equals (state : state) (args : term list) : term = + let Equals (_ : state) (args : term list) : term = assert(List.length args = 2) let x, y = args.[0], args.[1] x === y + + let RunStaticCtor (_ : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 1) + // TODO: initialize statics of argument + List.singleton cilState diff --git a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi index 74933ff12..1d0f9693c 100644 --- a/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi +++ b/VSharp.InternalCalls/Runtime.CompilerServices.RuntimeHelpers.fsi @@ -3,8 +3,9 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL -module Runtime_CompilerServices_RuntimeHelpers = +module internal Runtime_CompilerServices_RuntimeHelpers = [] val IsBitwiseEquatable : state -> term list -> term @@ -23,3 +24,7 @@ module Runtime_CompilerServices_RuntimeHelpers = [] val Equals : state -> term list -> term + + [] + [] + val RunStaticCtor : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/String.fs b/VSharp.InternalCalls/String.fs index 9a43bb18b..ac389d643 100644 --- a/VSharp.InternalCalls/String.fs +++ b/VSharp.InternalCalls/String.fs @@ -2,8 +2,12 @@ namespace VSharp.System open FSharpx.Collections open global.System + open VSharp open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations +open VSharp.Core.API.Arithmetics // ------------------------------- mscorlib.System.Array ------------------------------- @@ -17,7 +21,7 @@ module internal String = let CtorFromReplicatedChar state args = assert(List.length args = 3) - let this, char, length = args.[0], args.[1], args.[2] + let this, char, length = args[0], args[1], args[2] Memory.StringFromReplicatedChar state this char length Nop() @@ -31,6 +35,41 @@ module internal String = | [ _ ] -> Nop() | _ -> internalfail "CtorFromSpan: need to branch execution" + let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 4) + let this = args[0] + let ptr = args[1] + let startIndex = args[2] + let length = args[3] + let zero = MakeNumber 0 + let rangeCheck() = + (length >>= zero) + &&& (startIndex >>= zero) + let copy cilState k = + let cilStates = writeClassField cilState this Reflection.stringLengthField length + for cilState in cilStates do + Buffer.CommonMemmove cilState.state this None ptr (Some startIndex) length + k cilStates + let checkPtr cilState k = + StatedConditionalExecutionCIL cilState + (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 + (fun state k -> k (length === zero, state)) + emptyStringCase + checkPtr + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (rangeCheck(), state)) + checkLength + (i.Raise i.ArgumentOutOfRangeException) + id + let GetLength (state : state) (args : term list) = assert(List.length args = 1) Memory.StringLength state (List.head args) @@ -93,3 +132,32 @@ module internal String = assert(List.length args = 1) let length = List.head args Memory.AllocateEmptyString state length + + let FillStringChecked (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 3) + let state = cilState.state + let dest, destPos, src = args[0], args[1], args[2] + let srcPos = MakeNumber 0 + let srcLength = Memory.StringLength state src + let destLength = Memory.StringLength state dest + let (<<=) = Arithmetics.(<<=) + let check = srcLength <<= (Arithmetics.Sub destLength destPos) + let copy (cilState : cilState) k = + Memory.CopyStringArray cilState.state src srcPos dest destPos srcLength + k [cilState] + StatedConditionalExecutionCIL cilState + (fun state k -> k (check, state)) + copy + (interpreter.Raise interpreter.IndexOutOfRangeException) + id + + let GetChars (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 2) + let this = args[0] + let index = args[1] + let length = Memory.StringLength cilState.state this + let getChar cilState k = + let char = Memory.ReadStringChar cilState.state this index + push char cilState + List.singleton cilState |> k + interpreter.AccessArray getChar cilState length index id diff --git a/VSharp.InternalCalls/String.fsi b/VSharp.InternalCalls/String.fsi index 70ceea588..928decc58 100644 --- a/VSharp.InternalCalls/String.fsi +++ b/VSharp.InternalCalls/String.fsi @@ -3,6 +3,7 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL // ------------------------------- mscorlib.System.String ------------------------------- @@ -17,6 +18,9 @@ module internal String = [] val CtorFromSpan : state -> term list -> term + [] + val CtorFromPtr : IInterpreter -> cilState -> term list -> cilState list + [] val GetLength : state -> term list -> term @@ -35,3 +39,9 @@ module internal String = [] val FastAllocateString : state -> term list -> term + + [] + val FillStringChecked : IInterpreter -> cilState -> term list -> cilState list + + [] + val GetChars : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/SystemArray.fs b/VSharp.InternalCalls/SystemArray.fs index 0084d4611..32bee49e5 100644 --- a/VSharp.InternalCalls/SystemArray.fs +++ b/VSharp.InternalCalls/SystemArray.fs @@ -3,6 +3,8 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations // ------------------------------- mscorlib.System.Array ------------------------------- @@ -54,3 +56,146 @@ module internal SystemArray = assert(List.length args = 3) 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 + k [cilState] + interpreter.AccessArrayDimension arrayLengthByDimension cilState array dim + + let GetArrayLowerBound (interpreter : IInterpreter) cilState args = + 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 + k [cilState] + interpreter.AccessArrayDimension arrayLowerBoundByDimension cilState array dim + + let CommonInitializeArray (interpreter : IInterpreter) cilState args = + assert(List.length args = 2) + let array = args[0] + let handleTerm = args[1] + let initArray (cilState : cilState) k = + Memory.InitializeArray cilState.state array handleTerm + k [cilState] + interpreter.NpeOrInvoke cilState array (fun cilState k -> + interpreter.NpeOrInvoke cilState handleTerm initArray k) id + + let Clear (interpreter : IInterpreter) cilState args = + assert(List.length args = 3) + let array, index, length = args[0], args[1], args[2] + let (>>) = API.Arithmetics.(>>) + let (<<) = API.Arithmetics.(<<) + let clearCase (cilState : cilState) k = + Memory.ClearArray cilState.state array index length + k [cilState] + let nonNullCase (cilState : cilState) k = + let zero = MakeNumber 0 + let lb = Memory.ArrayLowerBoundByDimension cilState.state array zero + let numOfAllElements = Memory.CountOfArrayElements cilState.state array + let check = + (index << lb) + ||| ((Arithmetics.Add index length) >> numOfAllElements) + ||| (length << zero) + StatedConditionalExecutionCIL cilState + (fun state k -> k (check, state)) + (interpreter.Raise interpreter.IndexOutOfRangeException) + clearCase + k + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference array, state)) + (interpreter.Raise interpreter.ArgumentNullException) + nonNullCase + id + + let CommonCopyArray (i : IInterpreter) (cilState : cilState) src srcIndex dst dstIndex length = + let state = cilState.state + let srcType = MostConcreteTypeOfRef state src + let dstType = MostConcreteTypeOfRef state dst + let (>>) = API.Arithmetics.(>>) + let (>>=) = API.Arithmetics.(>>=) + let (<<) = API.Arithmetics.(<<) + let add = Arithmetics.Add + let zero = TypeUtils.Int32.Zero() + let srcLB = Memory.ArrayLowerBoundByDimension state src zero + let dstLB = Memory.ArrayLowerBoundByDimension state dst zero + let srcNumOfAllElements = Memory.CountOfArrayElements state src + let dstNumOfAllElements = Memory.CountOfArrayElements state dst + let defaultCase (cilState : cilState) k = + Memory.CopyArray cilState.state src srcIndex srcType dst dstIndex dstType length + k [cilState] + let lengthCheck (cilState : cilState) = + let endSrcIndex = add srcIndex length + let srcNumOfAllElements = srcNumOfAllElements + let endDstIndex = add dstIndex length + let dstNumOfAllElements = dstNumOfAllElements + let check = + (endSrcIndex >> srcNumOfAllElements) ||| (endSrcIndex << srcLB) + ||| (endDstIndex >> dstNumOfAllElements) ||| (endDstIndex << dstLB) + StatedConditionalExecutionCIL cilState + (fun state k -> k (check, state)) + (i.Raise i.ArgumentException) + defaultCase + let indicesCheck (cilState : cilState) = + // TODO: extended form needs + let primitiveLengthCheck = (length << zero) ||| (if TypeUtils.isLong length then length >> TypeUtils.Int32.MaxValue() else False()) + 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 + (fun state k -> k (primitiveLengthCheck ||| srcIndexCheck ||| dstIndexCheck, state)) + (i.Raise i.ArgumentOutOfRangeException) + lengthCheck + let assignableCheck (cilState : cilState) = + let srcElemType = Types.ElementType srcType + let dstElemType = Types.ElementType dstType + let condition = + if Types.IsValueType srcElemType then True() + else Types.TypeIsType srcElemType dstElemType + StatedConditionalExecutionCIL cilState + (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 + (fun state k -> k (IsNullReference src ||| IsNullReference dst, state)) + (i.Raise i.ArgumentNullException) + rankCheck + id + + let CopyArrayExtendedForm1 (interpreter : IInterpreter) cilState args = + assert(List.length args = 6) + 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 CopyArrayExtendedForm2 (interpreter : IInterpreter) cilState args = + assert(List.length args = 5) + 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 = + assert(List.length args = 3) + let src, dst, length = args[0], args[1], args[2] + let state = cilState.state + let zero = TypeUtils.Int32.Zero() + let srcLB = Memory.ArrayLowerBoundByDimension state src zero + let dstLB = Memory.ArrayLowerBoundByDimension state dst zero + CommonCopyArray interpreter cilState src srcLB dst dstLB length + + let FillArray (interpreter : IInterpreter) cilState args = + assert(List.length args = 3) + let array, value = args[1], args[2] + let fill cilState k = + Memory.FillArray cilState.state array value + k [cilState] + StatedConditionalExecutionCIL cilState + (fun state k -> k (IsNullReference array, state)) + (interpreter.Raise interpreter.ArgumentNullException) + fill + id diff --git a/VSharp.InternalCalls/SystemArray.fsi b/VSharp.InternalCalls/SystemArray.fsi index a40a589cc..1d939e59b 100644 --- a/VSharp.InternalCalls/SystemArray.fsi +++ b/VSharp.InternalCalls/SystemArray.fsi @@ -3,6 +3,7 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL // ------------------------------- mscorlib.System.Array ------------------------------- @@ -25,3 +26,27 @@ module internal SystemArray = [] val GetItem : state -> term list -> term + + [] + val GetArrayLength : IInterpreter -> cilState -> term list -> cilState list + + [] + val GetArrayLowerBound : IInterpreter -> cilState -> term list -> cilState list + + [] + val CommonInitializeArray : IInterpreter -> cilState -> term list -> cilState list + + [] + val Clear : IInterpreter -> cilState -> term list -> cilState list + + [] + val CopyArrayExtendedForm1 : IInterpreter -> cilState -> term list -> cilState list + + [] + val CopyArrayExtendedForm2 : IInterpreter -> cilState -> term list -> cilState list + + [] + val CopyArrayShortForm : IInterpreter -> cilState -> term list -> cilState list + + [] + val FillArray : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/Thread.fs b/VSharp.InternalCalls/Thread.fs index cf0e77f25..a7e8d4863 100644 --- a/VSharp.InternalCalls/Thread.fs +++ b/VSharp.InternalCalls/Thread.fs @@ -2,6 +2,8 @@ namespace VSharp.System open global.System open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations // ------------------------------ mscorlib.System.Threading.Thread -------------------------------- @@ -26,3 +28,21 @@ module Thread = let internal SleepInternal (_ : state) (args : term list) = assert(List.length args = 1) Nop() + + 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 + (interpreter.Raise interpreter.ArgumentNullException) + success + id + + let MonitorEnter (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 1) + let obj = List.head args + BranchOnNullCIL cilState obj + (interpreter.Raise interpreter.ArgumentNullException) + (fun cilState k -> List.singleton cilState |> k) + id diff --git a/VSharp.InternalCalls/Thread.fsi b/VSharp.InternalCalls/Thread.fsi index a1b925e7b..7a949d646 100644 --- a/VSharp.InternalCalls/Thread.fsi +++ b/VSharp.InternalCalls/Thread.fsi @@ -3,25 +3,32 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL // ------------------------------ mscorlib.System.Threading.Thread -------------------------------- -module Thread = +module internal Thread = [] - val internal GetFastDomainInternal : state -> term list -> term + val GetFastDomainInternal : state -> term list -> term [] - val internal GetDomainInternal : state -> term list -> term + val GetDomainInternal : state -> term list -> term [] - val internal SpinWaitInternal : state -> term list -> term + val SpinWaitInternal : state -> term list -> term [] - val internal SpinOnce : state -> term list -> term + val SpinOnce : state -> term list -> term [] - val internal Yield : state -> term list -> term + val Yield : state -> term list -> term [] - val internal SleepInternal : state -> term list -> term + val SleepInternal : state -> term list -> term + + [] + val MonitorReliableEnter : IInterpreter -> cilState -> term list -> cilState list + + [] + val MonitorEnter : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/VSharp.InternalCalls.fsproj b/VSharp.InternalCalls/VSharp.InternalCalls.fsproj index f68be08de..7db7b6571 100644 --- a/VSharp.InternalCalls/VSharp.InternalCalls.fsproj +++ b/VSharp.InternalCalls/VSharp.InternalCalls.fsproj @@ -42,10 +42,10 @@ - - + + @@ -56,17 +56,23 @@ + + + + + + - + diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index 9af9425e0..281b81161 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -20,6 +20,7 @@ type cilState = // 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 errorReported : bool mutable filterResult : term option //TODO: #mb frames list #mb transfer to Core.State mutable iie : InsufficientInformationException option @@ -53,7 +54,7 @@ type cilStateComparer(comparer) = override _.Compare(x : cilState, y : cilState) = comparer x y -module internal CilStateOperations = +module CilStateOperations = let mutable currentStateId = 0u let getNextStateId() = @@ -68,6 +69,7 @@ module internal CilStateOperations = prefixContext = List.empty currentLoc = currentLoc state = state + errorReported = false filterResult = None iie = None level = PersistentDict.empty @@ -101,15 +103,16 @@ module internal CilStateOperations = | [ Exit _ ] -> false | _ -> true - let isError (s : cilState) = - match s.state.exceptionsRegister with - | NoException -> false - | _ -> true - let isUnhandledError (s : cilState) = + let isUnhandledException (s : cilState) = match s.state.exceptionsRegister with | Unhandled _ -> true | _ -> false + let isUnhandledExceptionOrError (s : cilState) = + match s.state.exceptionsRegister with + | Unhandled _ -> true + | _ -> s.errorReported + let levelToUnsignedInt (lvl : level) = PersistentDict.fold (fun acc _ v -> max acc v) 0u lvl //TODO: remove it when ``level'' subtraction would be generalized let currentIp (s : cilState) = match s.ipStack with @@ -122,11 +125,14 @@ module internal CilStateOperations = | SearchingForHandler([], []) -> true | _ -> false - let hasRuntimeException (s : cilState) = + let hasRuntimeExceptionOrError (s : cilState) = match s.state.exceptionsRegister 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 @@ -289,6 +295,94 @@ module internal CilStateOperations = 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) = + let mutable cilState = cilState + let mutable stateConfigured : bool = false + + static member ReportError cilState message = + cilState.errorReported <- true + reportError cilState message + + static member ReportFatalError cilState message = + cilState.errorReported <- true + 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 + reportError cilState msg |> k + StatedConditionalExecution cilState.state + (fun state k -> k (!!failCondition, state)) + (fun _ k -> k ()) + report + (fun _ _ -> []) + ignore + + override x.ReportFatalError msg failCondition = + assert stateConfigured + let report state k = + let cilState = changeState cilState state + cilState.errorReported <- true + reportFatalError cilState msg |> k + StatedConditionalExecution cilState.state + (fun state k -> k (!!failCondition, state)) + (fun _ k -> k ()) + report + (fun _ _ -> []) + ignore + + override x.ConfigureState state = + cilState <- changeState cilState 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 ------------------------------- // TODO: not used diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index 7e791ebf8..43a4989bc 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -16,7 +16,7 @@ open MethodBody type cfg = CfgInfo -module internal TypeUtils = +module TypeUtils = open Types let float64Type = typedefof @@ -65,72 +65,10 @@ module internal TypeUtils = let Zero() = MakeNumber 0UL let MaxValue() = MakeNumber UInt64.MaxValue -type internal ErrorReporter(reportError, reportFatalError, cilState) = - let mutable cilState = cilState - let mutable stateConfigured : bool = false - - interface IErrorReporter with - override x.ReportError msg failCondition = - assert stateConfigured - Branching.commonStatedConditionalExecutionk cilState.state - (fun state k -> k (!!failCondition, state)) - (fun _ k -> k ()) - (fun state k -> k (reportError (changeState cilState state) msg)) - (fun _ _ -> []) - ignore - - override x.ReportFatalError msg failCondition = - assert stateConfigured - Branching.commonStatedConditionalExecutionk cilState.state - (fun state k -> k (!!failCondition, state)) - (fun _ k -> k ()) - (fun state k -> k (reportFatalError (changeState cilState state) msg)) - (fun _ _ -> []) - ignore - - override x.ConfigureState state = - cilState <- changeState cilState state - stateConfigured <- true - module internal InstructionsSet = - let mutable reportError : cilState -> string -> unit = - fun _ _ -> internalfail "'reportError' is not ready" - - let mutable reportFatalError : cilState -> string -> unit = - fun _ _ -> internalfail "'reportError' is not ready" - - let createErrorReporter cilState = - ErrorReporter(reportError, reportFatalError, cilState) - let idTransformation term k = k term - // ------------------------------------ Memory Interaction ------------------------------------ - - 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 - Memory.WriteUnsafe reporter cilState.state ref value - - 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 - Memory.WriteArrayIndexUnsafe reporter cilState.state term index value valueType - // ------------------------------------ Metadata Interaction ------------------------------------ let resolveFieldFromMetadata (m : Method) offset = m.ResolveFieldFromMetadata offset @@ -148,39 +86,6 @@ module internal InstructionsSet = | Leave(ip, _, _, _) -> (|InstructionEndingIp|_|) ip | _ -> None - // ------------------------------- Environment interaction ------------------------------- - - let rec internalCall (methodInfo : MethodInfo) (argsAndThis : term list) cilState k = - let s = cilState.state - let parameters : obj [] = - match methodInfo.GetParameters().Length with - | 2 -> [| s; argsAndThis |] - | _ -> internalfail "Only internal calls with signature 'state * term list -> term | (term * state) list' are supported" - let result = - try - methodInfo.Invoke(null, parameters) - with - | :? TargetInvocationException as targetException -> - Logger.trace $"InternalCall got TargetInvocationException {targetException.Message}" - let actualException = targetException.GetBaseException() - Logger.trace $"TargetInvocationException.GetBaseException {actualException.Message}" - raise actualException - | e -> - Logger.trace $"InternalCall got exception {e.Message}" - reraise() - - let pushOnEvaluationStack (term : term, cilState : cilState) = - match term.term with - | Nop -> () - | _ -> push term cilState - match result with - | :? term as r -> - let cilState = changeState cilState s - pushOnEvaluationStack(r, cilState); k [cilState] - | :? ((term * state) list) as r -> - r |> List.map (fun (t, s) -> let s' = changeState cilState s in pushOnEvaluationStack(t, s'); s') |> k - | _ -> internalfail "Internal call should return 'term' or tuple 'term * state'!" - // ------------------------------- CIL instructions ------------------------------- let referenceLocalVariable index (method : Method) = @@ -233,8 +138,7 @@ module internal InstructionsSet = let location = referenceLocalVariable variableIndex m let typ = TypeOfLocation location let value = Types.Cast right typ - let states = write cilState location value - states |> List.map (changeState cilState) + write cilState location value let private simplifyConditionResult state res k = if Contradicts state !!res then k (True()) elif Contradicts state res then k (False()) @@ -549,11 +453,11 @@ module internal InstructionsSet = let private fallThroughImpl stackSizeBefore newIp cilState = // if not constructing runtime exception - if not <| isUnhandledError cilState && Memory.CallStackSize cilState.state = stackSizeBefore then + if not <| isUnhandledExceptionOrError cilState && Memory.CallStackSize cilState.state = stackSizeBefore then setCurrentIp newIp cilState let fallThrough (m : Method) offset cilState op = - assert(not <| isUnhandledError cilState) + assert(not <| isUnhandledExceptionOrError cilState) let stackSizeBefore = Memory.CallStackSize cilState.state let newIp = instruction m (fallThroughTarget m offset) op m offset cilState @@ -561,7 +465,7 @@ module internal InstructionsSet = [cilState] let forkThrough (m : Method) offset cilState op = - assert(not <| isUnhandledError cilState) + assert(not <| isUnhandledExceptionOrError cilState) let stackSizeBefore = Memory.CallStackSize cilState.state let newIp = instruction m (fallThroughTarget m offset) let cilStates = op m offset cilState @@ -583,38 +487,74 @@ type UnknownMethodException(message : string, methodInfo : Method, interpreterSt member x.Method with get() = methodInfo member x.InterpreterStackTrace with get() = interpreterStackTrace -type internal ILInterpreter() as this = - - let cilStateImplementations : Map term option -> term list -> cilState list> = - Map.ofList [ - "System.Int32 System.Array.GetLength(this, System.Int32)", this.CommonGetArrayLength - "System.Int32 System.Array.GetLowerBound(this, System.Int32)", this.GetArrayLowerBound - "System.Void System.Runtime.CompilerServices.RuntimeHelpers.InitializeArray(System.Array, System.RuntimeFieldHandle)", this.CommonInitializeArray - "System.Void System.String.FillStringChecked(System.String, System.Int32, System.String)", this.FillStringChecked - "System.Void System.Array.Clear(System.Array, System.Int32, System.Int32)", this.ClearArray - "System.Void System.Array.Copy(System.Array, System.Int32, System.Array, System.Int32, System.Int32, System.Boolean)", this.CopyArrayExtendedForm1 - "System.Void System.Array.Copy(System.Array, System.Int32, System.Array, System.Int32, System.Int32)", this.CopyArrayExtendedForm2 - "System.Void System.Array.Copy(System.Array, System.Array, System.Int32)", this.CopyArrayShortForm - "System.Void System.Array.Fill(T[], T)", this.FillArray - "System.Char System.String.get_Chars(this, System.Int32)", this.GetChars - "System.Void System.Threading.Monitor.ReliableEnter(System.Object, System.Boolean&)", this.MonitorReliableEnter - "System.Void System.Threading.Monitor.Enter(System.Object)", this.MonitorEnter - "System.Void System.Diagnostics.Debug.Assert(System.Boolean)", this.DebugAssert - "System.UInt32 System.Collections.HashHelpers.FastMod(System.UInt32, System.UInt32, System.UInt64)", this.FastMod - "System.Void System.Runtime.CompilerServices.RuntimeHelpers._RunClassConstructor(System.RuntimeType)", this.RunStaticCtor - "System.Void System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(System.Runtime.CompilerServices.QCallTypeHandle)", this.RunStaticCtor - "System.Delegate System.Delegate.Combine(System.Delegate, System.Delegate)", this.DelegateCombine - "System.Delegate System.Delegate.Remove(System.Delegate, System.Delegate)", this.DelegateRemove - ] - - // NOTE: adding implementation names into Loader - do Loader.CilStateImplementations <- cilStateImplementations.Keys +// Interface for internal calls interaction +type IInterpreter = + abstract Raise : (cilState -> unit) -> cilState -> (cilState list -> 'a) -> 'a + abstract NpeOrInvoke : cilState -> term -> (cilState -> (cilState list -> 'a) -> 'a) -> (cilState list -> 'a) -> 'a + abstract InvalidProgramException : cilState -> unit + abstract NullReferenceException : cilState -> unit + abstract ArgumentException : cilState -> unit + abstract ArgumentNullException : cilState -> unit + abstract ArgumentOutOfRangeException : cilState -> unit + abstract IndexOutOfRangeException : cilState -> unit + abstract ArrayTypeMismatchException : cilState -> unit + abstract RankException : cilState -> unit + abstract DivideByZeroException : cilState -> unit + abstract OverflowException : cilState -> unit + abstract ArithmeticException : cilState -> unit + abstract TypeInitializerException : string -> term -> cilState -> unit + abstract InvalidCastException : cilState -> unit + abstract OutOfMemoryException : cilState -> unit + abstract AccessArrayDimension : (term -> term -> cilState -> (cilState list -> cilState list) -> cilState list) -> cilState -> term -> term -> cilState list + abstract AccessArray : (cilState -> (cilState list -> 'a) -> 'a) -> cilState -> term -> term -> (cilState list -> 'a) -> 'a + +type ILInterpreter() as this = + + // ------------------------------- Environment interaction ------------------------------- + + member x.InternalCall (originMethod : Method) (methodInfo : MethodInfo) (argsAndThis : term list) cilState k = + let neededParams = methodInfo.GetParameters() |> Array.map (fun p -> p.ParameterType) + let parameters : obj[] = + match neededParams with + | [| t1; t2; t3 |] when t1 = typeof && t2 = typeof && t3 = typeof -> + [| x :> IInterpreter; cilState; argsAndThis |] + | [| t1; t2 |] when t1 = typeof && t2 = typeof -> + [| cilState.state; argsAndThis |] + | _ -> internalfail $"InternalCall: unsupported signature of internal call {neededParams}" + + let result = + try + methodInfo.Invoke(null, parameters) + with + | :? TargetInvocationException as targetException -> + Logger.error $"InternalCall got TargetInvocationException {targetException.Message}" + let actualException = targetException.GetBaseException() + Logger.error $"TargetInvocationException.GetBaseException {actualException.Message}" + raise actualException + | e -> + Logger.error $"InternalCall got exception {e.Message}" + reraise() + + match result with + | :? term as result when not originMethod.HasNonVoidResult -> + assert(result = Nop()) + k [cilState] + | :? term as result when originMethod.HasNonVoidResult -> + assert(result <> Nop()) + push result cilState + 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 + | :? ((term * state) list) as results -> + results |> List.map (fun (_, s) -> changeState cilState 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 = - reportError <- errorReporter - reportFatalError <- fatalErrorReporter + configureErrorReporter errorReporter fatalErrorReporter - member private x.Raise createException (cilState : cilState) k = + member x.Raise createException (cilState : cilState) k = createException cilState k [cilState] @@ -641,324 +581,15 @@ type internal ILInterpreter() as this = let upperBound = Memory.ArrayRank cilState.state this x.AccessArray (accessor this dimension) cilState upperBound dimension id - member private x.CommonGetArrayLength (cilState : cilState) thisOption args = - match args with - | [dimensionsKey] -> - let arrayLengthByDimension arrayRef index cilState (k : cilState list -> 'a) = - push (Memory.ArrayLengthByDimension cilState.state arrayRef index) cilState - k [cilState] - x.AccessArrayDimension arrayLengthByDimension cilState (Option.get thisOption) dimensionsKey - | _ -> internalfail "unexpected number of arguments" - - member private x.GetArrayLowerBound (cilState : cilState) (this : term option) args = - match args with - | [dimension] -> - let arrayLowerBoundByDimension arrayRef index (cilState : cilState) k = - push (Memory.ArrayLowerBoundByDimension cilState.state arrayRef index) cilState - k [cilState] - x.AccessArrayDimension arrayLowerBoundByDimension cilState (Option.get this) dimension - | _ -> internalfail "unexpected number of arguments" - - member private x.NpeOrInvokeStatementCIL (cilState : cilState) (this : term) statement (k : cilState list -> 'a) = + member x.NpeOrInvokeStatementCIL (cilState : cilState) (this : term) statement (k : cilState list -> 'a) = StatedConditionalExecutionCIL cilState (fun state k -> k (IsBadRef this, state)) (x.Raise x.NullReferenceException) statement k - member private x.CommonInitializeArray (cilState : cilState) _ (args : term list) = - match args with - | [arrayRef; handleTerm] -> - let initArray (cilState : cilState) k = - Memory.InitializeArray cilState.state arrayRef handleTerm - k [cilState] - x.NpeOrInvokeStatementCIL cilState arrayRef initArray id - | _ -> internalfail "unexpected number of arguments" - - member private x.FillStringChecked (cilState : cilState) _ (args : term list) = - assert(List.length args = 3) - let state = cilState.state - let dest, destPos, src = args[0], args[1], args[2] - let srcPos = MakeNumber 0 - let srcLength = Memory.StringLength state src - let destLength = Memory.StringLength state dest - let (<<=) = Arithmetics.(<<=) - let check = srcLength <<= (Arithmetics.Sub destLength destPos) - let copy (cilState : cilState) k = - Memory.CopyStringArray cilState.state src srcPos dest destPos srcLength - k [cilState] - StatedConditionalExecutionCIL cilState - (fun state k -> k (check, state)) - copy - (x.Raise x.IndexOutOfRangeException) - id - - member private x.ClearArray (cilState : cilState) _ (args : term list) = - assert(List.length args = 3) - let array, index, length = args[0], args[1], args[2] - let (>>) = API.Arithmetics.(>>) - let (<<) = API.Arithmetics.(<<) - let clearCase (cilState : cilState) k = - Memory.ClearArray cilState.state array index length - k [cilState] - let nonNullCase (cilState : cilState) k = - let zero = MakeNumber 0 - let lb = Memory.ArrayLowerBoundByDimension cilState.state array zero - let numOfAllElements = Memory.CountOfArrayElements cilState.state array - let check = (index << lb) ||| ((Arithmetics.Add index length) >> numOfAllElements) ||| (length << zero) - StatedConditionalExecutionCIL cilState - (fun state k -> k (check, state)) - (x.Raise x.IndexOutOfRangeException) - clearCase - k - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference array, state)) - (x.Raise x.ArgumentNullException) - nonNullCase - id - - member private x.CommonCopyArray (cilState : cilState) src srcIndex dst dstIndex length = - let state = cilState.state - let srcType = MostConcreteTypeOfRef state src - let dstType = MostConcreteTypeOfRef state dst - let (>>) = API.Arithmetics.(>>) - let (>>=) = API.Arithmetics.(>>=) - let (<<) = API.Arithmetics.(<<) - let add = Arithmetics.Add - let zero = TypeUtils.Int32.Zero() - let srcLB = Memory.ArrayLowerBoundByDimension state src zero - let dstLB = Memory.ArrayLowerBoundByDimension state dst zero - let srcNumOfAllElements = Memory.CountOfArrayElements state src - let dstNumOfAllElements = Memory.CountOfArrayElements state dst - let defaultCase (cilState : cilState) k = - Memory.CopyArray cilState.state src srcIndex srcType dst dstIndex dstType length - k [cilState] - let lengthCheck (cilState : cilState) = - let endSrcIndex = add srcIndex length - let srcNumOfAllElements = srcNumOfAllElements - let endDstIndex = add dstIndex length - let dstNumOfAllElements = dstNumOfAllElements - let check = - (endSrcIndex >> srcNumOfAllElements) ||| (endSrcIndex << srcLB) - ||| (endDstIndex >> dstNumOfAllElements) ||| (endDstIndex << dstLB) - StatedConditionalExecutionCIL cilState - (fun state k -> k (check, state)) - (x.Raise x.ArgumentException) - defaultCase - let indicesCheck (cilState : cilState) = - // TODO: extended form needs - let primitiveLengthCheck = (length << zero) ||| (if TypeUtils.isLong length then length >> TypeUtils.Int32.MaxValue() else False()) - 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 - (fun state k -> k (primitiveLengthCheck ||| srcIndexCheck ||| dstIndexCheck, state)) - (x.Raise x.ArgumentOutOfRangeException) - lengthCheck - let assignableCheck (cilState : cilState) = - let srcElemType = Types.ElementType srcType - let dstElemType = Types.ElementType dstType - let condition = - if Types.IsValueType srcElemType then True() - else Types.TypeIsType srcElemType dstElemType - StatedConditionalExecutionCIL cilState - (fun state k -> k (condition, state)) - indicesCheck - (x.Raise x.InvalidCastException) - let rankCheck (cilState : cilState) = - if Types.RankOf srcType = Types.RankOf dstType then assignableCheck cilState - else x.Raise x.RankException cilState - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference src ||| IsNullReference dst, state)) - (x.Raise x.ArgumentNullException) - rankCheck - id - - member private x.CopyArrayExtendedForm1 (cilState : cilState) _ (args : term list) = - assert(List.length args = 6) - let src, srcIndex, dst, dstIndex, length = args[0], args[1], args[2], args[3], args[4] - x.CommonCopyArray cilState src srcIndex dst dstIndex length - - member private x.CopyArrayExtendedForm2 (cilState : cilState) _ (args : term list) = - assert(List.length args = 5) - let src, srcIndex, dst, dstIndex, length = args[0], args[1], args[2], args[3], args[4] - x.CommonCopyArray cilState src srcIndex dst dstIndex length - - member private x.CopyArrayShortForm (cilState : cilState) _ (args : term list) = - assert(List.length args = 3) - let src, dst, length = args[0], args[1], args[2] - let state = cilState.state - let zero = TypeUtils.Int32.Zero() - let srcLB = Memory.ArrayLowerBoundByDimension state src zero - let dstLB = Memory.ArrayLowerBoundByDimension state src zero - x.CommonCopyArray cilState src srcLB dst dstLB length - - member private x.FillArray (cilState : cilState) _ (args : term list) = - assert(List.length args = 3) - let array, value = args[1], args[2] - let fill cilState k = - Memory.FillArray cilState.state array value - k [cilState] - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference array, state)) - (x.Raise x.ArgumentNullException) - fill - id - - member private x.GetChars (cilState : cilState) this (args : term list) = - assert(List.length args = 1) - match this with - | Some this -> - let index = List.item 0 args - let length = Memory.StringLength cilState.state this - let getChar cilState k = - let char = Memory.ReadStringChar cilState.state this index - push char cilState - List.singleton cilState |> k - x.AccessArray getChar cilState length index id - | None -> internalfailf $"String.GetChars: unexpected this {this}" - - member private x.MonitorReliableEnter (cilState : cilState) this (args : term list) = - assert(List.length args = 2 && Option.isNone this) - let obj, resultRef = args[0], args[1] - let success cilState k = - Memory.Write cilState.state resultRef (True()) |> List.map (changeState cilState) |> k - BranchOnNullCIL cilState obj - (x.Raise x.ArgumentNullException) - success - id - - member private x.MonitorEnter (cilState : cilState) this (args : term list) = - assert(List.length args = 1 && Option.isNone this) - let obj = List.head args - BranchOnNullCIL cilState obj - (x.Raise x.ArgumentNullException) - (fun cilState k -> List.singleton cilState |> k) - id - - member private x.DebugAssert (cilState : cilState) this (args : term list) = - assert(List.length args = 1 && Option.isNone this) - let condition = List.head args - StatedConditionalExecutionCIL cilState - (fun state k -> k (condition, state)) - (fun cilState k -> (); k [cilState]) - (fun cilState k -> - reportFatalError cilState "Debug.Assert failed" - k []) - id - - member private x.FastMod (cilState : cilState) this (args : term list) = - assert(List.length args = 3 && Option.isNone this) - let left, right = args[0], args[1] - let validCase 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 - k [cilState] - StatedConditionalExecutionCIL cilState - (fun state k -> k (right === MakeNumber 0, state)) - (x.Raise x.DivideByZeroException) - validCase - id - - member private x.RunStaticCtor (cilState : cilState) this (args : term list) = - assert(List.length args = 1 && Option.isNone this) - // TODO: initialize statics of argument - List.singleton cilState - - member private x.DelegateCombine cilState _ args = - assert(List.length args = 2) - let d1 = args[0] - let d2 = args[1] - assert(IsReference d1 && IsReference d2) - let combine t cilState k = - let d = Memory.CombineDelegates cilState.state args t - push d cilState - List.singleton cilState |> k - let typesCheck 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 - (fun state k -> k (Types.RefIsType state d2 t, state)) - (combine t) - (x.Raise x.ArgumentException) - k - StatedConditionalExecutionCIL cilState - (fun state k -> k (Types.RefIsType state d1 t, state)) - secondCheck - (x.Raise x.ArgumentException) - k - let nullCheck cilState k = - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference d2, state)) - (fun cilState k -> push d1 cilState; List.singleton cilState |> k) - typesCheck - k - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference d1, state)) - (fun cilState k -> push d2 cilState; List.singleton cilState |> k) - nullCheck - id - - member private x.DelegateRemove cilState _ args = - assert(List.length args = 2) - let source = args[0] - let toRemove = args[1] - assert(IsReference source && IsReference toRemove) - let remove t cilState k = - let d = Memory.RemoveDelegate cilState.state source toRemove t - push d cilState - List.singleton cilState |> k - let typesCheck 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 - (fun state k -> k (Types.RefIsType state toRemove t, state)) - (remove t) - (x.Raise x.ArgumentException) - k - StatedConditionalExecutionCIL cilState - (fun state k -> k (Types.RefIsType state source t, state)) - secondCheck - (x.Raise x.ArgumentException) - k - let nullCheck cilState k = - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference source, state)) - (fun cilState k -> push (TypeOf source |> NullRef) cilState; List.singleton cilState |> k) - typesCheck - k - StatedConditionalExecutionCIL cilState - (fun state k -> k (IsNullReference toRemove, state)) - (fun cilState k -> push source cilState; List.singleton cilState |> k) - nullCheck - id - - member private x.TrustedIntrinsics = - let intPtr = Reflection.getAllMethods typeof |> Array.map Reflection.getFullMethodName - let volatile = Reflection.getAllMethods typeof |> Array.map Reflection.getFullMethodName - let defaultComparer = [|"System.Collections.Generic.Comparer`1[T] System.Collections.Generic.Comparer`1[T].get_Default()"|] - Array.concat [intPtr; volatile; defaultComparer] - - member private x.IsNotImplementedIntrinsic (method : Method) fullMethodName = - let isIntrinsic = - let intrinsicAttr = "System.Runtime.CompilerServices.IntrinsicAttribute" - method.CustomAttributes |> Seq.exists (fun m -> m.AttributeType.ToString() = intrinsicAttr) - isIntrinsic && (Array.contains fullMethodName x.TrustedIntrinsics |> not) - - member private x.ShouldMock (method : Method) fullMethodName = - Loader.isShimmed fullMethodName && ExternMocker.ShimSupported - || method.IsExternalMethod && not method.IsQCall + member private x.ShouldMock (method : Method) = + method.IsShimmed && ExternMocker.ShimSupported || method.IsExternalMethod && not method.IsQCall member private x.InstantiateThisIfNeed state thisOption (method : Method) = match thisOption with @@ -1007,7 +638,7 @@ type internal ILInterpreter() as this = (fun state k -> k (assumptions, state)) (fun cilState k -> k [cilState]) (fun cilState k -> - if shouldReportError then reportError cilState message + if shouldReportError then ErrorReporter.ReportError cilState message k []) k @@ -1038,7 +669,7 @@ type internal ILInterpreter() as this = (fun state k -> k (assumptions, state)) (fun cilState k -> k [cilState]) (fun cilState k -> - if shouldReportError then reportError cilState message + if shouldReportError then ErrorReporter.ReportError cilState message k []) k @@ -1105,9 +736,9 @@ type internal ILInterpreter() as this = let error = Memory.AllocateConcreteObject state e (e.GetType()) x.CommonThrow cilState error isRuntime - member private x.TryConcreteInvoke (method : Method) fullMethodName (args : term list) thisOption (cilState : cilState) = + member private x.TryConcreteInvoke (method : Method) (args : term list) thisOption (cilState : cilState) = let state = cilState.state - if method.IsConcretelyInvokable && Loader.isInvokeInternalCall fullMethodName then + if method.CanCallConcrete then // Before term args, type args are located let termArgs = List.skip (List.length args - method.Parameters.Length) args let objArgs = List.choose (TryTermToObj state) termArgs @@ -1134,7 +765,7 @@ type internal ILInterpreter() as this = push resultTerm cilState | _ -> () with :? TargetInvocationException as e -> - let isRuntime = Loader.isRuntimeExceptionsImplementation fullMethodName + let isRuntime = method.IsRuntimeException x.ConcreteInvokeCatch e.InnerException cilState isRuntime true else false @@ -1149,18 +780,17 @@ type internal ILInterpreter() as this = x.InstantiateThisIfNeed cilState.state thisOption method let fallThroughCall (cilState : cilState) = - if isUnhandledError cilState |> not then + if isUnhandledExceptionOrError cilState |> not then ILInterpreter.FallThroughCall cilState cilState - if x.TryConcreteInvoke method fullMethodName typeAndMethodArgs thisOption cilState then + if x.TryConcreteInvoke method typeAndMethodArgs thisOption cilState then fallThroughCall cilState |> List.singleton |> k - elif Map.containsKey fullMethodName cilStateImplementations then - cilStateImplementations[fullMethodName] cilState thisOption typeAndMethodArgs |> List.map fallThroughCall |> k - elif Map.containsKey fullMethodName Loader.FSharpImplementations then + elif method.IsFSharpInternalCall then let thisAndArguments = optCons typeAndMethodArgs thisOption - internalCall Loader.FSharpImplementations[fullMethodName] thisAndArguments cilState (List.map fallThroughCall >> k) - elif Map.containsKey fullMethodName Loader.CSharpImplementations then + let internalCall = method.GetInternalCall + x.InternalCall method internalCall thisAndArguments cilState (List.map fallThroughCall >> k) + elif method.IsCSharpInternalCall then assert method.HasBody ILInterpreter.InitFunctionFrameCIL cilState method thisOption (Some args) [cilState] |> k @@ -1183,7 +813,7 @@ type internal ILInterpreter() as this = let stackTrace = Memory.StackTraceString cilState.state.stack let message = $"Not supported internal call: {fullMethodName}" UnknownMethodException(message, method, stackTrace) |> raise - elif x.IsNotImplementedIntrinsic method fullMethodName then + elif method.IsNotImplementedIntrinsic then let stackTrace = Memory.StackTraceString cilState.state.stack let message = $"Not supported intrinsic method: {fullMethodName}" UnknownMethodException(message, method, stackTrace) |> raise @@ -1538,8 +1168,7 @@ type internal ILInterpreter() as this = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Stobj.Size) let store cilState k = let value = Types.Cast value typ - let states = write cilState ref value - states |> List.map (changeState cilState) |> k + write cilState ref value |> k x.NpeOrInvokeStatementCIL cilState ref store id member x.LdFldWithFieldInfo (fieldInfo : FieldInfo) addressNeeded (cilState : cilState) = @@ -1572,8 +1201,7 @@ type internal ILInterpreter() as this = let reference = if TypeUtils.isPointer fieldInfo.DeclaringType then targetRef else Reflection.wrapField fieldInfo |> Memory.ReferenceField cilState.state targetRef - let states = write cilState reference value - List.map (changeState cilState) states |> k + write cilState reference value |> k x.NpeOrInvokeStatementCIL cilState targetRef storeWhenTargetIsNotNull id member private x.LdElemCommon (typ : Type option) (cilState : cilState) arrayRef indices = @@ -1620,8 +1248,7 @@ type internal ILInterpreter() as this = let checkedStElem (cilState : cilState) (k : cilState list -> 'a) = let typeOfValue = TypeOf value let uncheckedStElem (cilState : cilState) (k : cilState list -> 'a) = - let states = writeIndex cilState arrayRef indices value typ - List.map (changeState cilState) states |> k + writeIndex cilState arrayRef indices value typ |> k let checkTypeMismatch (cilState : cilState) (k : cilState list -> 'a) = let condition = if Types.IsValueType typeOfValue then True() @@ -1680,8 +1307,7 @@ type internal ILInterpreter() as this = let value, address = pop2 cilState let store cilState k = let value = valueCast value - let states = write cilState address value - states |> List.map (changeState cilState) |> k + write cilState address value |> k x.NpeOrInvokeStatementCIL cilState address store id member x.BoxNullable (t : Type) (v : term) (cilState : cilState) : cilState list = @@ -1781,7 +1407,7 @@ type internal ILInterpreter() as this = member private x.Throw (cilState : cilState) = let error = peek cilState - let isRuntime = Loader.isRuntimeExceptionsImplementation (currentMethod cilState).FullName + let isRuntime = (currentMethod cilState).IsRuntimeException BranchOnNullCIL cilState error (x.Raise x.NullReferenceException) (fun cilState k -> @@ -2119,12 +1745,11 @@ type internal ILInterpreter() as this = && parameters |> Seq.forall2 (fun p1 p2 -> p2.ParameterType.IsAssignableFrom p1) argumentsTypes let ctors = constructors |> Array.filter suitable assert(Array.length ctors = 1) - let ctor = ctors[0] - let fullConstructorName = Reflection.getFullMethodName ctor - assert (Loader.hasRuntimeExceptionsImplementation fullConstructorName) - let proxyCtor = Loader.getRuntimeExceptionsImplementation fullConstructorName |> Application.getMethod + let ctor = Application.getMethod ctors[0] + assert ctor.HasRuntimeExceptionImpl + let proxyCtor = ctor.RuntimeExceptionImpl |> Application.getMethod ILInterpreter.InitFunctionFrameCIL cilState proxyCtor None (Some arguments) - let success = x.TryConcreteInvoke proxyCtor proxyCtor.FullName arguments None cilState + let success = x.TryConcreteInvoke proxyCtor arguments None cilState assert success member x.InvalidProgramException cilState = @@ -2193,7 +1818,7 @@ type internal ILInterpreter() as this = let ip = currentIp cilState try let allStates = x.MakeStep cilState - let newErrors, restStates = List.partition isUnhandledError allStates + let newErrors, restStates = List.partition isUnhandledExceptionOrError allStates let errors = errors @ newErrors let newIieStates, goodStates = List.partition isIIEState restStates let incompleteStates = newIieStates @ incompleteStates @@ -2594,7 +2219,32 @@ type internal ILInterpreter() as this = | _ -> __unreachable__() let renewInstructionsInfo cilState = - if not <| isUnhandledError cilState then + if not <| isUnhandledExceptionOrError cilState then x.IncrementLevelIfNeeded m offset cilState newSts |> List.iter renewInstructionsInfo newSts + +// ------------------------------------ IExceptionManager implementation ------------------------------------ + + interface IInterpreter with + override x.Raise createException cilState k = + x.Raise createException cilState k + override x.NpeOrInvoke cilState ref statement k = + x.NpeOrInvokeStatementCIL cilState ref statement k + override x.InvalidProgramException cilState = x.InvalidProgramException cilState + override x.NullReferenceException cilState = x.NullReferenceException cilState + override x.ArgumentException cilState = x.ArgumentException cilState + override x.ArgumentNullException cilState = x.ArgumentNullException cilState + override x.ArgumentOutOfRangeException cilState = x.ArgumentOutOfRangeException cilState + override x.IndexOutOfRangeException cilState = x.IndexOutOfRangeException cilState + override x.ArrayTypeMismatchException cilState = x.ArrayTypeMismatchException cilState + override x.RankException cilState = x.RankException cilState + override x.DivideByZeroException cilState = x.DivideByZeroException cilState + override x.OverflowException cilState = x.OverflowException cilState + override x.ArithmeticException cilState = x.ArithmeticException cilState + override x.TypeInitializerException qualifiedTypeName innerException cilState = + x.TypeInitializerException qualifiedTypeName innerException cilState + override x.InvalidCastException cilState = x.InvalidCastException cilState + override x.OutOfMemoryException cilState = x.OutOfMemoryException cilState + override x.AccessArrayDimension accessor cilState this dim = x.AccessArrayDimension accessor cilState this dim + override x.AccessArray accessor cilState length index k = x.AccessArray accessor cilState length index k diff --git a/VSharp.SILI/VSharp.SILI.fsproj b/VSharp.SILI/VSharp.SILI.fsproj index 3dada0836..a96abd2f2 100644 --- a/VSharp.SILI/VSharp.SILI.fsproj +++ b/VSharp.SILI/VSharp.SILI.fsproj @@ -17,31 +17,14 @@ - - - - - - - - - - - - - - - - - diff --git a/VSharp.Test/Benchmarks/BenchmarkResult.cs b/VSharp.Test/Benchmarks/BenchmarkResult.cs index 9dabf7b3b..a2bfcb7ea 100644 --- a/VSharp.Test/Benchmarks/BenchmarkResult.cs +++ b/VSharp.Test/Benchmarks/BenchmarkResult.cs @@ -1,11 +1,11 @@ #nullable enable -using VSharp.Interpreter.IL; +using VSharp.SVM; namespace VSharp.Test.Benchmarks; public readonly record struct BenchmarkResult( bool IsSuccessful, - SILIStatistics Statistics, + SVMStatistics Statistics, UnitTests Tests, BenchmarkTarget Target, int? Coverage = null diff --git a/VSharp.Test/Benchmarks/Benchmarks.cs b/VSharp.Test/Benchmarks/Benchmarks.cs index 9cd60b082..508bc99cb 100644 --- a/VSharp.Test/Benchmarks/Benchmarks.cs +++ b/VSharp.Test/Benchmarks/Benchmarks.cs @@ -7,7 +7,7 @@ using System.Reflection; using ConsoleTables; using NUnit.Framework; -using VSharp.Interpreter.IL; +using VSharp.SVM; using VSharp.TestRenderer; namespace VSharp.Test.Benchmarks; @@ -61,7 +61,7 @@ public static BenchmarkResult Run( Logger.currentLogLevel = Logger.Warning; var unitTests = new UnitTests(Directory.GetCurrentDirectory()); - var options = new SiliOptions( + var options = new SVMOptions( explorationMode: explorationMode.NewTestCoverageMode(coverageZone.MethodZone, searchStrategy), outputDirectory: unitTests.TestDirectory, recThreshold: 1, @@ -75,7 +75,7 @@ public static BenchmarkResult Run( randomSeed: randomSeed, stepsLimit: stepsLimit ); - using var explorer = new SILI(options); + using var explorer = new SVM.SVM(options); explorer.Interpret( new[] { exploredMethodInfo }, diff --git a/VSharp.Test/Benchmarks/SearcherBenchmarks.cs b/VSharp.Test/Benchmarks/SearcherBenchmarks.cs index 4e2a89639..b419858ad 100644 --- a/VSharp.Test/Benchmarks/SearcherBenchmarks.cs +++ b/VSharp.Test/Benchmarks/SearcherBenchmarks.cs @@ -2,6 +2,7 @@ using System.Linq; using NUnit.Framework; using VSharp.Interpreter.IL; +using VSharp.SVM; namespace VSharp.Test.Benchmarks; diff --git a/VSharp.Test/CsvStatisticsReporter.cs b/VSharp.Test/CsvStatisticsReporter.cs index ff33ec465..9d707497d 100644 --- a/VSharp.Test/CsvStatisticsReporter.cs +++ b/VSharp.Test/CsvStatisticsReporter.cs @@ -61,13 +61,13 @@ private CsvRecord StatisticsToCsvRecord(TestStatistics testStatistics) ReleaseBranchesEnabled: testStatistics.ReleaseBranchesEnabled.ToString(), Timeout: testStatistics.Timeout.ToString(), Exception: (testStatistics.Exception?.InnerException ?? testStatistics.Exception)?.GetType().Name ?? "", - Duration: testStatistics.SiliStatisticsDump?.time.ToString() ?? "", + Duration: testStatistics.SvmStatisticsDump?.time.ToString() ?? "", TestsGenerated: testStatistics.TestsGenerated.ToString() ?? "", Coverage: testStatistics.Coverage?.ToString() ?? "", - CoveringStepsInsideZone: testStatistics.SiliStatisticsDump?.coveringStepsInsideZone.ToString() ?? "", - NonCoveringStepsInsideZone: testStatistics.SiliStatisticsDump?.nonCoveringStepsInsideZone.ToString() ?? "", - CoveringStepsOutsideZone: testStatistics.SiliStatisticsDump?.coveringStepsOutsideZone.ToString() ?? "", - NonCoveringStepsOutsideZone: testStatistics.SiliStatisticsDump?.nonCoveringStepsOutsideZone.ToString() ?? "", + CoveringStepsInsideZone: testStatistics.SvmStatisticsDump?.coveringStepsInsideZone.ToString() ?? "", + NonCoveringStepsInsideZone: testStatistics.SvmStatisticsDump?.nonCoveringStepsInsideZone.ToString() ?? "", + CoveringStepsOutsideZone: testStatistics.SvmStatisticsDump?.coveringStepsOutsideZone.ToString() ?? "", + NonCoveringStepsOutsideZone: testStatistics.SvmStatisticsDump?.nonCoveringStepsOutsideZone.ToString() ?? "", TestsOutputDirectory: testStatistics.TestsOutputDirectory ?? "" ); } diff --git a/VSharp.Test/ExecutionTreeTests.cs b/VSharp.Test/ExecutionTreeTests.cs index 387be5194..e69e0a40c 100644 --- a/VSharp.Test/ExecutionTreeTests.cs +++ b/VSharp.Test/ExecutionTreeTests.cs @@ -2,7 +2,7 @@ using System.Collections.Generic; using Microsoft.FSharp.Core; using NUnit.Framework; -using VSharp.Interpreter.IL; +using VSharp.SVM; namespace VSharp.Test; diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 26d4c6d1f..9533d3a4a 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -15,6 +15,7 @@ using VSharp.CSharpUtils; using VSharp.Interpreter.IL; using VSharp.Solver; +using VSharp.SVM; using VSharp.TestRenderer; namespace VSharp.Test @@ -70,7 +71,7 @@ public class TestSvmAttribute : NUnitAttribute, IWrapTestMethod, ISimpleTestBuil private const string SolverTimeoutParameterName = "solverTimeout"; private const string ReleaseBranchesParameterName = "releaseBranches"; - private static SiliOptions _options = null; + private static SVMOptions _options; static TestSvmAttribute() { @@ -228,9 +229,9 @@ public TestSvmCommand( _coverageZone = coverageZone switch { - CoverageZone.Method => Interpreter.IL.coverageZone.MethodZone, - CoverageZone.Class => Interpreter.IL.coverageZone.ClassZone, - CoverageZone.Module => Interpreter.IL.coverageZone.ModuleZone, + CoverageZone.Method => SVM.coverageZone.MethodZone, + CoverageZone.Class => SVM.coverageZone.ClassZone, + CoverageZone.Module => SVM.coverageZone.ModuleZone, _ => throw new ArgumentOutOfRangeException(nameof(coverageZone), coverageZone, null) }; @@ -293,7 +294,7 @@ private TestResult Explore(TestExecutionContext context) try { var unitTests = new UnitTests(Directory.GetCurrentDirectory()); - _options = new SiliOptions( + _options = new SVMOptions( explorationMode: explorationMode.NewTestCoverageMode(_coverageZone, _searchStrat), outputDirectory: unitTests.TestDirectory, recThreshold: _recThresholdForTest, @@ -307,7 +308,7 @@ private TestResult Explore(TestExecutionContext context) randomSeed: _randomSeed, stepsLimit: _stepsLimit ); - using var explorer = new SILI(_options); + using var explorer = new SVM.SVM(_options); explorer.Interpret( new [] { exploredMethodInfo }, @@ -330,7 +331,7 @@ private TestResult Explore(TestExecutionContext context) stats = stats with { - SiliStatisticsDump = explorer.Statistics.DumpStatistics(), + SvmStatisticsDump = explorer.Statistics.DumpStatistics(), TestsGenerated = unitTests.UnitTestsCount, TestsOutputDirectory = unitTests.TestDirectory.FullName }; diff --git a/VSharp.Test/TestStatistics.cs b/VSharp.Test/TestStatistics.cs index 948327770..a544986f7 100644 --- a/VSharp.Test/TestStatistics.cs +++ b/VSharp.Test/TestStatistics.cs @@ -1,6 +1,7 @@ +#nullable enable using System; using System.Reflection; -using VSharp.Interpreter.IL; +using VSharp.SVM; namespace VSharp.Test; @@ -10,9 +11,9 @@ public record TestStatistics( int Timeout, SearchStrategy SearchStrategy, CoverageZone CoverageZone, - statisticsDump SiliStatisticsDump = null, + statisticsDump? SvmStatisticsDump = null, uint? Coverage = null, uint? TestsGenerated = null, string TestsOutputDirectory = "", - Exception Exception = null + Exception? Exception = null ); diff --git a/VSharp.sln b/VSharp.sln index 0ff25ce1f..3a02df194 100644 --- a/VSharp.sln +++ b/VSharp.sln @@ -30,6 +30,8 @@ Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.TestGenerator", "VSh EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VSharp.CoverageRunner", "VSharp.CoverageRunner\VSharp.CoverageRunner.csproj", "{AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}" EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "VSharp.SVM", "VSharp.SVM\VSharp.SVM.fsproj", "{9455C456-51A6-4CA3-B33A-4F168CBADADA}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -127,5 +129,11 @@ Global {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.Release|Any CPU.Build.0 = Release|Any CPU {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.DebugTailRec|Any CPU.ActiveCfg = DebugTailRec|Any CPU {AEB2ABD0-5045-4A28-BBEB-2F353BD543FE}.DebugTailRec|Any CPU.Build.0 = DebugTailRec|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.Debug|Any CPU.Build.0 = Debug|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.Release|Any CPU.ActiveCfg = Release|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.Release|Any CPU.Build.0 = Release|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.DebugTailRec|Any CPU.ActiveCfg = Debug|Any CPU + {9455C456-51A6-4CA3-B33A-4F168CBADADA}.DebugTailRec|Any CPU.Build.0 = Debug|Any CPU EndGlobalSection EndGlobal From 76cf21e29d32ecaa315fd30ffde3d4d0567e0e0d Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:57:13 +0300 Subject: [PATCH 12/20] [style] fixed style --- VSharp.SILI.Core/Branching.fs | 2 +- VSharp.SILI/CILState.fs | 13 ++++++++++--- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/VSharp.SILI.Core/Branching.fs b/VSharp.SILI.Core/Branching.fs index 654489ae4..1b8291259 100644 --- a/VSharp.SILI.Core/Branching.fs +++ b/VSharp.SILI.Core/Branching.fs @@ -2,7 +2,7 @@ namespace VSharp.Core open VSharp -module Branching = +module internal Branching = let checkSat state = SolverInteraction.checkSatWithSubtyping state diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index 281b81161..4d0142033 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -255,9 +255,16 @@ module CilStateOperations = let setException exc (cilState : cilState) = cilState.state.exceptionsRegister <- exc let push v (cilState : cilState) = - cilState.state.evaluationStack <- EvaluationStack.Push v cilState.state.evaluationStack - cilState.lastPushInfo <- Some v - let pushMany vs (cilState : cilState) = cilState.state.evaluationStack <- EvaluationStack.PushMany vs cilState.state.evaluationStack + match v.term with + | Nop -> internalfail "pushing 'NOP' value onto evaluation stack" + | _ -> + cilState.state.evaluationStack <- EvaluationStack.Push v cilState.state.evaluationStack + cilState.lastPushInfo <- Some v + + 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 From e632452a25a081603f7c2fbb8ea0d4e6383c11a9 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 15:57:36 +0300 Subject: [PATCH 13/20] [fix] fixed '.constrained' prefix --- VSharp.SILI/Interpreter.fs | 50 ++++++++++++++++++++++++-------------- 1 file changed, 32 insertions(+), 18 deletions(-) diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index 43a4989bc..bd03ca2bd 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -408,7 +408,34 @@ module internal InstructionsSet = let newIp = instruction m (unconditionalBranchTarget m offset) setCurrentIp newIp cilState - // '.constrained' is prefix, which is used before 'callvirt' instruction + let rec private constrainedImpl this method args 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 + | Ref _ when isValueType -> + let thisStruct = read cilState this + let heapRef = Memory.BoxValueType state thisStruct + push heapRef cilState + pushMany args cilState + | Ref _ -> + let this = read cilState this + push this cilState + pushMany args cilState + | Ptr(pointerBase, sightType, offset) -> + match TryPtrToRef state pointerBase sightType offset with + | Some(PrimitiveStackLocation _ as address) -> + let this = Ref address + constrainedImpl this method args cilState + | _ -> internalfail $"Calling 'callvirt' with '.constrained': unexpected ptr as 'this' {this}" + | _ -> internalfail $"Calling 'callvirt' with '.constrained': unexpected 'this' {this}" + + // '.constrained' is prefix, which is used before 'callvirt' or 'call' instruction + // used before 'call' instruction, only if member is static and declared in interface let constrained (m : Method) offset (cilState : cilState) = let typ = resolveTypeFromMetadata m (offset + Offset.from OpCodes.Constrained.Size) let method = @@ -426,25 +453,12 @@ module internal InstructionsSet = pushPrefixContext cilState (Constrained typ) else let n = method.GetParameters().Length - let args, evaluationStack = EvaluationStack.PopMany n cilState.state.evaluationStack + let state = cilState.state + let args, evaluationStack = EvaluationStack.PopMany n state.evaluationStack setEvaluationStack evaluationStack cilState let thisForCallVirt = pop cilState - let thisType = TypeOfLocation thisForCallVirt - let isValueType = Types.IsValueType thisType - match thisForCallVirt.term with - | Ref _ when isValueType && Reflection.typeImplementsMethod thisType method -> - push thisForCallVirt cilState - pushMany args cilState - | Ref _ when isValueType -> - let thisStruct = read cilState thisForCallVirt - let heapRef = Memory.BoxValueType cilState.state thisStruct - push heapRef cilState - pushMany args cilState - | Ref _ -> - let this = read cilState thisForCallVirt - push this cilState - pushMany args cilState - | _ -> internalfail $"Calling 'callvirt' with '.constrained': unexpected 'this' {thisForCallVirt}" + constrainedImpl thisForCallVirt method args cilState + let localloc (cilState : cilState) = // [NOTE] localloc usually is used for Span // So, pushing nullptr, because array will be allocated in Span constructor From 737aabbb6f9b8d4b0435b7f81ad2e56150aedb60 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 17:22:50 +0300 Subject: [PATCH 14/20] [test] unignored tests --- VSharp.Test/Tests/Lists.cs | 2 +- VSharp.Test/Tests/Strings.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 3fa62fdf1..03a2c60fc 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -869,7 +869,7 @@ public static Array RetSystemArray3(Array arr) [TestSvmFixture] public static class SpanTests { - [Ignore("check exceptions in 'Span.get_Item' internal call")] + [TestSvm(100)] public static unsafe byte SpanTest(int[] a, byte b, int i) { fixed (void* ptr = a) diff --git a/VSharp.Test/Tests/Strings.cs b/VSharp.Test/Tests/Strings.cs index 6987fb75d..2e8227ac2 100644 --- a/VSharp.Test/Tests/Strings.cs +++ b/VSharp.Test/Tests/Strings.cs @@ -110,7 +110,7 @@ public static bool ConcreteStringToUpper() return upper == str; } - [Ignore("use error reporter in 'Unsafe.ReadUnaligned' internal call")] + [TestSvm(100)] public static int Contains(string str) { if (str.Contains("d8")) From 9ec1cc16c2c379fd7cf030efb905fb2bc575b935 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 22:48:34 +0300 Subject: [PATCH 15/20] [style] fixed style --- VSharp.SILI.Core/API.fs | 11 +++++-- VSharp.SILI.Core/API.fsi | 9 +++++- VSharp.SILI.Core/Terms.fs | 46 +++++++++++++-------------- VSharp.SILI/Interpreter.fs | 2 +- VSharp.TestGenerator/TestGenerator.fs | 2 +- 5 files changed, 42 insertions(+), 28 deletions(-) diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 2e2cbbda5..75a5cb2b5 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -142,7 +142,8 @@ module API = | {term = Ptr(HeapLocation(addr, _), _, offset)} when addr = zeroAddress() && offset = makeNumber 0 -> Some() | _ -> None - let (|DetachedPtr|_|) term = (|DetachedPtr|_|) term.term + let (|DetachedPtr|_|) term = (|DetachedPtr|_|) term + let (|DetachedPtrTerm|_|) term = (|DetachedPtr|_|) term.term let (|StackReading|_|) src = Memory.(|StackReading|_|) src let (|HeapReading|_|) src = Memory.(|HeapReading|_|) src @@ -242,13 +243,19 @@ module API = module public Arithmetics = let (===) x y = simplifyEqual x y id + let Equality x y = simplifyEqual x y id let (!==) x y = simplifyNotEqual x y id + let Inequality x y = simplifyNotEqual x y id let (<<) x y = simplifyLess x y id + let Less x y = simplifyLess x y id let (<<=) x y = simplifyLessOrEqual x y id + let LessOrEqual x y = simplifyLessOrEqual x y id let (>>) x y = simplifyGreater x y id + let Greater x y = simplifyGreater x y id let (>>=) x y = simplifyGreaterOrEqual x y id - let (%%%) x y = simplifyRemainder true (TypeOf x) x y id + let GreaterOrEqual x y = simplifyGreaterOrEqual x y id let GreaterOrEqualUn x y = simplifyGreaterOrEqualUn x y id + let (%%%) x y = simplifyRemainder true (TypeOf x) x y id let Mul x y = mul x y let Sub x y = sub x y diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index eea8b3857..4d200cf13 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -99,7 +99,8 @@ module API = val (|NullRef|_|) : term -> Type option val (|NonNullRef|_|) : term -> unit option val (|NullPtr|_|) : term -> unit option - val (|DetachedPtr|_|) : term -> term option + val (|DetachedPtr|_|) : termNode -> term option + val (|DetachedPtrTerm|_|) : term -> term option val (|StackReading|_|) : ISymbolicConstantSource -> option val (|HeapReading|_|) : ISymbolicConstantSource -> option> @@ -194,6 +195,12 @@ module API = // Lightweight version: divide by zero exceptions are ignored! val (%%%) : term -> term -> term val GreaterOrEqualUn : term -> term -> term + val Equality : term -> term -> term + val Inequality : term -> term -> term + val Less : term -> term -> term + val LessOrEqual : term -> term -> term + val Greater : term -> term -> term + val GreaterOrEqual : term -> term -> term val Mul : term -> term -> term val Sub : term -> term -> term val Add : term -> term -> term diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index e62bd8880..a52b4878e 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -35,14 +35,14 @@ type stackKey = | ThisKey _ -> "this" | ParameterKey pi -> if String.IsNullOrEmpty pi.Name then "#" + toString pi.Position else pi.Name | LocalVariableKey (lvi,_) -> "__loc__" + lvi.LocalIndex.ToString() - | TemporaryLocalVariableKey (typ, index) -> sprintf "__tmp__%s%d" (Reflection.getFullTypeName typ) index + | TemporaryLocalVariableKey (typ, index) -> $"__tmp__%s{Reflection.getFullTypeName typ}%d{index}" override x.GetHashCode() = let fullname = match x with - | ThisKey m -> sprintf "%s##this" m.FullName - | ParameterKey pi -> sprintf "%O##%O##%d" pi.Member pi pi.Position - | LocalVariableKey (lvi, m) -> sprintf "%O##%s" m.FullName (lvi.ToString()) - | TemporaryLocalVariableKey (typ, index) -> sprintf "temporary##%s%d" (Reflection.getFullTypeName typ) index + | ThisKey m -> $"%s{m.FullName}##this" + | ParameterKey pi -> $"{pi.Member}##{pi}##%d{pi.Position}" + | LocalVariableKey (lvi, m) -> $"{m.FullName}##%s{lvi.ToString()}" + | TemporaryLocalVariableKey (typ, index) -> $"temporary##%s{Reflection.getFullTypeName typ}%d{index}" fullname.GetDeterministicHashCode() interface IComparable with override x.CompareTo(other: obj) = @@ -73,7 +73,7 @@ type stackKey = | ParameterKey p -> ParameterKey (Reflection.concretizeParameter p typeSubst) | LocalVariableKey(l, m) -> let m' = m.SubstituteTypeVariables typeSubst - let l' = m.LocalVariables.[l.LocalIndex] + let l' = m.LocalVariables[l.LocalIndex] LocalVariableKey(l', m') | TemporaryLocalVariableKey (typ, index) -> // TODO: index may become inconsistent here @@ -130,7 +130,7 @@ type termNode = | Nop -> k "" | Constant(name, _, _) -> k name.v | Concrete(_, (ClassType(t, _) as typ)) when isSubtypeOrEqual t typedefof -> - sprintf "" typ |> k + $"" |> 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 @@ -155,7 +155,7 @@ type termNode = | Cast(_, dest) -> assert (List.length operands = 1) toStr operation.priority indent (List.head operands).term (fun term -> - sprintf "(%O %s)" dest term + $"({dest} %s{term})" |> checkExpression operation.priority parentPriority |> k) | Application f -> @@ -170,7 +170,7 @@ type termNode = let guardedToString (guard, term) k = toStringWithParentIndent indent guard (fun guardString -> toStringWithParentIndent indent term (fun termString -> - sprintf "| %s ~> %s" guardString termString |> k)) + $"| %s{guardString} ~> %s{termString}" |> k)) Cps.Seq.mapk guardedToString guardedTerms (fun guards -> let printed = guards |> Seq.sort |> join ("\n" + indent) formatIfNotEmpty (formatWithIndent indent) printed |> sprintf "UNION[%s]" |> k) @@ -222,14 +222,14 @@ and address = override x.ToString() = match x with | PrimitiveStackLocation key -> toString key - | ClassField(addr, field) -> sprintf "%O.%O" addr field + | ClassField(addr, field) -> $"{addr}.{field}" | ArrayIndex(addr, idcs, _) -> sprintf "%O[%s]" addr (List.map toString idcs |> join ", ") - | StaticField(typ, field) -> sprintf "%O.%O" typ field - | StructField(addr, field) -> sprintf "%O.%O" addr field - | ArrayLength(addr, dim, _) -> sprintf "Length(%O, %O)" addr dim + | StaticField(typ, field) -> $"{typ}.{field}" + | StructField(addr, field) -> $"{addr}.{field}" + | ArrayLength(addr, dim, _) -> $"Length({addr}, {dim})" | BoxedLocation(addr, typ) -> $"{typ}^{addr}" - | StackBufferIndex(key, idx) -> sprintf "%O[%O]" key idx - | ArrayLowerBound(addr, dim, _) -> sprintf "LowerBound(%O, %O)" addr dim + | StackBufferIndex(key, idx) -> $"{key}[{idx}]" + | ArrayLowerBound(addr, dim, _) -> $"LowerBound({addr}, {dim})" member x.Zone() = match x with | PrimitiveStackLocation _ @@ -343,15 +343,15 @@ module internal Terms = let operationOf = term >> function | Expression(op, _, _) -> op - | term -> internalfailf "expression expected, %O received" term + | term -> internalfail $"expression expected, {term} received" let argumentsOf = term >> function | Expression(_, args, _) -> args - | term -> internalfailf "expression expected, %O received" term + | term -> internalfail $"expression expected, {term} received" let fieldsOf = term >> function | Struct(fields, _) -> fields - | term -> internalfailf "struct or class expected, %O received" term + | term -> internalfail $"struct or class expected, {term} received" let private typeOfUnion getType gvs = let types = List.map (snd >> getType) gvs @@ -361,7 +361,7 @@ module internal Terms = let allSame = List.forall ((=) t) ts if allSame then t - else internalfailf "evaluating type of unexpected union %O!" gvs + else internalfail $"evaluating type of unexpected union {gvs}!" let commonTypeOf getType term = match term.term with @@ -372,7 +372,7 @@ module internal Terms = let sightTypeOfPtr = let getTypeOfPtr = term >> function | Ptr(_, typ, _) -> typ - | term -> internalfailf "expected pointer, but got %O" term + | term -> internalfail $"expected pointer, but got {term}" commonTypeOf getTypeOfPtr let rec typeOfRef term = @@ -382,7 +382,7 @@ module internal Terms = | Ref address -> address.TypeOfLocation | Ptr(_, sightType, _) -> sightType | _ when typeOf term |> isNative -> typeof - | term -> internalfailf "expected reference, but got %O" term + | term -> internalfail $"expected reference, but got {term}" commonTypeOf getTypeOfRef term and typeOf term = @@ -395,7 +395,7 @@ module internal Terms = | Struct(_, t) -> t | Ref _ -> (typeOfRef term).MakeByRefType() | Ptr _ -> (sightTypeOfPtr term).MakePointerType() - | _ -> internalfailf "getting type of unexpected term %O" term + | _ -> internalfail $"getting type of unexpected term {term}" commonTypeOf getType term let symbolicTypeToArrayType = function @@ -404,7 +404,7 @@ module internal Terms = | Vector -> (elementType, 1, true) | ConcreteDimension d -> (elementType, d, false) | SymbolicDimension -> __insufficientInformation__ "Cannot process array of unknown dimension!" - | typ -> internalfailf "symbolicTypeToArrayType: expected array type, but got %O" typ + | typ -> internalfail $"symbolicTypeToArrayType: expected array type, but got {typ}" let arrayTypeToSymbolicType (elemType : Type, dim, isVector) = if isVector then elemType.MakeArrayType() diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index bd03ca2bd..aefa32bc3 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -1504,7 +1504,7 @@ type ILInterpreter() as this = match y, x with | _ when TypeUtils.isIntegralTerm x && TypeUtils.isIntegralTerm y -> divRem x y - | DetachedPtr offset2, DetachedPtr offset1 -> + | DetachedPtrTerm offset2, DetachedPtrTerm offset1 -> divRem offset1 offset2 | FloatT, _ | _, FloatT when isRem -> internalfailf "Rem.Un is unspecified for Floats" diff --git a/VSharp.TestGenerator/TestGenerator.fs b/VSharp.TestGenerator/TestGenerator.fs index e78f7c918..5fddee852 100644 --- a/VSharp.TestGenerator/TestGenerator.fs +++ b/VSharp.TestGenerator/TestGenerator.fs @@ -207,7 +207,7 @@ module TestGenerator = test.MemoryGraph.RepresentStruct t fieldReprs | NullRef _ | NullPtr -> null - | DetachedPtr offset -> + | DetachedPtrTerm offset -> let offset = TypeUtils.convert (term2obj offset) typeof :?> int64 test.MemoryGraph.RepresentDetachedPtr typeof offset | {term = Ptr(HeapLocation({term = ConcreteHeapAddress(addr)}, _), sightType, offset)} -> From 106292eb8abf92d5ec6daaa606248f7af2b87996 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 22:48:58 +0300 Subject: [PATCH 16/20] [fix] fixed 'localloc' instruction --- VSharp.SILI/CILState.fs | 13 +++++++++++++ VSharp.SILI/Interpreter.fs | 11 +++++++---- 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index 4d0142033..fb6be2f75 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -20,6 +20,7 @@ type cilState = // 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 @@ -69,6 +70,7 @@ module CilStateOperations = prefixContext = List.empty currentLoc = currentLoc state = state + stackArrays = PersistentSet.empty errorReported = false filterResult = None iie = None @@ -187,6 +189,17 @@ module CilStateOperations = 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) = diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index aefa32bc3..09542cfe9 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -460,10 +460,13 @@ module internal InstructionsSet = constrainedImpl thisForCallVirt method args cilState let localloc (cilState : cilState) = - // [NOTE] localloc usually is used for Span - // So, pushing nullptr, because array will be allocated in Span constructor - pop cilState |> ignore - push (MakeNullPtr typeof) cilState + let size = pop cilState + let ref = Memory.AllocateVectorArray cilState.state size typeof + match ref.term with + | HeapRef({term = ConcreteHeapAddress address}, _) -> + addStackArray cilState address + push ref cilState + | _ -> internalfail $"localloc: unexpected array reference {ref}" let private fallThroughImpl stackSizeBefore newIp cilState = // if not constructing runtime exception From 0b11b71173025023b8f460e6027f30ec428c7746 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 22:50:07 +0300 Subject: [PATCH 17/20] [fix] fixed unsafe reading --- VSharp.SILI.Core/Memory.fs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index 82ff2f2b8..ab27e2252 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -1007,11 +1007,15 @@ module internal Memory = // NOTE: returns list of slices // TODO: return empty if every slice is invalid and private commonReadTermUnsafe (reporter : IErrorReporter) term startByte endByte pos stablePos sightType = - let typ = typeOf term - let size = internalSizeOf typ match term.term, sightType with - | _, Some sightType when startByte = makeNumber 0 && endByte = makeNumber size && typ = sightType -> - List.singleton term + | Slice _, _ -> + sliceTerm term startByte endByte pos stablePos |> List.singleton + | _, Some sightType when + startByte = makeNumber 0 && + let typ = typeOf term + let size = internalSizeOf typ + endByte = makeNumber size && typ = sightType -> + List.singleton term | Struct(fields, t), _ -> commonReadStructUnsafe reporter fields t startByte endByte pos stablePos sightType | HeapRef _, _ | Ref _, _ @@ -1020,7 +1024,6 @@ module internal Memory = | Combined(slices, _), _ -> let readSlice part = commonReadTermUnsafe reporter part startByte endByte pos stablePos sightType List.collect readSlice slices - | Slice _, _ | Concrete _, _ | Constant _, _ | Expression _, _ -> From 1761591bff8dcd72fafc34e65f0ac7828b6ed80f Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 22:51:48 +0300 Subject: [PATCH 18/20] [fix] fixed internal calls - fixed 'Span' and 'String' internal calls --- VSharp.InternalCalls/Span.fs | 182 +++++++++++++++++++------------- VSharp.InternalCalls/Span.fsi | 18 ++-- VSharp.InternalCalls/String.fs | 10 +- VSharp.InternalCalls/String.fsi | 2 +- VSharp.InternalCalls/Unsafe.fs | 51 +++++---- VSharp.InternalCalls/Unsafe.fsi | 5 +- VSharp.SILI.Core/API.fs | 7 +- VSharp.SILI.Core/Memory.fs | 4 +- VSharp.SILI.Core/Pointers.fs | 2 +- VSharp.Utils/TypeUtils.fs | 6 +- 10 files changed, 165 insertions(+), 122 deletions(-) diff --git a/VSharp.InternalCalls/Span.fs b/VSharp.InternalCalls/Span.fs index 6fdf7d560..7035eb701 100644 --- a/VSharp.InternalCalls/Span.fs +++ b/VSharp.InternalCalls/Span.fs @@ -2,12 +2,15 @@ namespace VSharp.System open System open global.System + open VSharp open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations // ------------------------------ System.ReadOnlySpan -------------------------------- -module ReadOnlySpan = +module internal ReadOnlySpan = let private isContentReferenceField fieldId = let name = fieldId.name @@ -29,20 +32,20 @@ module ReadOnlySpan = HeapRef address (eType.MakeArrayType dim) else ArrayIndex(address, indices, arrayType) |> Ref - let internal GetLength (state : state) (spanStruct : term) = + let GetLength (state : state) (spanStruct : term) = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) let lenField = spanFields |> Array.find (fst >> isLengthField) |> fst Memory.ReadField state spanStruct lenField - let internal GetContentsRef (state : state) (spanStruct : term) = + let GetContents (cilState : cilState) (spanStruct : term) = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) + let state = cilState.state let ptrField = spanFields |> Array.find (fst >> isContentReferenceField) |> fst - // TODO: throw ThrowIndexOutOfRangeException if len is less or equal to index let lenField = spanFields |> Array.find (fst >> isLengthField) |> fst - let len = Memory.ReadField state spanStruct lenField - let ptrFieldValue = Memory.ReadField state spanStruct ptrField + let len = readField cilState spanStruct lenField + let ptrFieldValue = readField cilState spanStruct ptrField let ptrFieldType = ptrField.typ let ptr = if ptrFieldIsByRef ptrFieldType then @@ -50,52 +53,75 @@ module ReadOnlySpan = let byRefFields = Terms.TypeOf ptrFieldValue |> Reflection.fieldsOf false assert(Array.length byRefFields = 1) let byRefField = byRefFields |> Array.find (fst >> ByReference.isValueField) |> fst - Memory.ReadField state ptrFieldValue byRefField + readField cilState ptrFieldValue byRefField else // Case for .NET 7, where Span contains 'Byte&' field ptrFieldValue - match ptr.term with - // Case for char span made from string - | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField -> - HeapRef address typeof - | Ref(ArrayIndex(addr, indices, arrayType)) when indices = [MakeNumber 0] -> - CreateArrayRef addr indices arrayType - | Ptr(HeapLocation(_, t) as pointerBase, sightType, offset) -> - match TryPtrToRef state pointerBase sightType offset with - | Some(ArrayIndex(address, indices, arrayType)) -> CreateArrayRef address indices arrayType - | Some address -> Ref address - | None when t.IsSZArray || t = typeof -> ptr - | None -> internalfail $"GetContentsRef: unexpected pointer to contents {ptr}" - | Ptr(pointerBase, sightType, offset) when len = MakeNumber 1 -> - match TryPtrToRef state pointerBase sightType offset with - | Some address -> Ref address - | _ -> ptr - | _ -> internalfail $"GetContentsRef: unexpected reference to contents {ptr}" - - let internal GetItemFromReadOnlySpan (state : state) (args : term list) : term = + let ref = + match ptr.term with + // Case for char span made from string + | Ref(ClassField(address, field)) when field = Reflection.stringFirstCharField -> + let address, arrayType = Memory.StringArrayInfo state address None + CreateArrayRef address [MakeNumber 0] arrayType + | Ref(ArrayIndex(addr, indices, arrayType)) -> + CreateArrayRef addr indices arrayType + | HeapRef(address, _) -> + let t = MostConcreteTypeOfRef state ptr + if TypeUtils.isArrayType t then ptr + elif t = typeof then + let address, arrayType = Memory.StringArrayInfo state address None + CreateArrayRef address [MakeNumber 0] arrayType + elif TypeUtils.isValueType t && len = MakeNumber 1 then + HeapReferenceToBoxReference ptr + else internalfail $"GetContents: unexpected pointer {ptr}" + | DetachedPtr _ -> ptr + | Ptr(HeapLocation(_, t) as pointerBase, sightType, offset) -> + // TODO: add 'TryPtrToRef' to ctor + match TryPtrToRef state pointerBase sightType offset with + | Some(ArrayIndex(address, indices, arrayType)) -> CreateArrayRef address indices arrayType + | Some address -> Ref address + | None when t.IsSZArray || t = typeof -> ptr + | None -> internalfail $"GetContentsRef: unexpected pointer to contents {ptr}" + | Ptr(pointerBase, sightType, offset) when len = MakeNumber 1 -> + match TryPtrToRef state pointerBase sightType offset with + | Some address -> Ref address + | _ -> ptr + | _ -> internalfail $"GetContentsRef: unexpected reference to contents {ptr}" + ref, len + + let private IsArrayContents ref = + match ref.term with + | HeapRef(_, t) + | Ptr(HeapLocation(_, t), _, _) -> + TypeUtils.isArrayType t || t = typeof + | Ref(ArrayIndex _) -> true + | _ -> false + + let GetItem (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 3) let this, wrappedType, index = args[0], args[1], args[2] let t = Helpers.unwrapType wrappedType - let span = Memory.Read state this - let ref = GetContentsRef state span - let isArrayContents = - match ref.term with - | HeapRef(_, t) - | Ptr(HeapLocation(_, t), _, _) -> - TypeUtils.isArrayType t || t = typeof - | Ref(ArrayIndex _) -> true - | _ -> false - if isArrayContents then - Memory.ReferenceArrayIndex state ref [index] (Some t) - elif index = MakeNumber 0 then - assert(TypeOfLocation ref = t) - ref - else internalfail $"GetItemFromReadOnlySpan: unexpected contents ref {ref}" - - let internal GetItemFromSpan (state : state) (args : term list) : term = - GetItemFromReadOnlySpan state args - - let private InitSpanStruct spanStruct refToFirst length = + let span = read cilState this + let ref, len = GetContents cilState span + let checkIndex cilState k = + let readIndex cilState k = + let ref = + if IsArrayContents ref then + Memory.ReferenceArrayIndex cilState.state ref [index] (Some t) + elif index = MakeNumber 0 then + assert(TypeOfLocation ref = t) + ref + else internalfail $"GetItemFromReadOnlySpan: unexpected contents ref {ref}" + push ref cilState + List.singleton cilState |> k + StatedConditionalExecutionCIL cilState + (fun state k -> k (Arithmetics.Less index len, state)) + readIndex + (i.Raise i.IndexOutOfRangeException) + k + i.NpeOrInvoke cilState ref checkIndex id + + let private InitSpanStruct cilState spanStruct refToFirst length = let spanFields = Terms.TypeOf spanStruct |> Reflection.fieldsOf false assert(Array.length spanFields = 2) let ptrField, ptrFieldInfo = spanFields |> Array.find (fst >> isContentReferenceField) @@ -107,48 +133,54 @@ module ReadOnlySpan = let byRefFields = Reflection.fieldsOf false ptrFieldType assert(Array.length byRefFields = 1) let valueField = byRefFields |> Array.find (fst >> ByReference.isValueField) |> fst - let initializedByRef = Memory.WriteStructField byRef valueField refToFirst - Memory.WriteStructField spanStruct ptrField initializedByRef + let initializedByRef = writeStructField cilState byRef valueField refToFirst + writeStructField cilState spanStruct ptrField initializedByRef else // Case for .NET 7, where Span contains 'Byte&' field - Memory.WriteStructField spanStruct ptrField refToFirst + writeStructField cilState spanStruct ptrField refToFirst let lengthField = spanFields |> Array.find (fst >> isLengthField) |> fst - Memory.WriteStructField spanWithPtrField lengthField length - - let private CommonCtor (state : state) this refToFirst length = - let span = Memory.Read state this - let initializedSpan = InitSpanStruct span refToFirst length - Memory.Write state this initializedSpan |> List.map (withFst (Nop())) + writeStructField cilState spanWithPtrField lengthField length - let internal CtorFromFromArray (state : state) this arrayRef = - let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None - let lengthOfArray = Memory.ArrayLengthByDimension state arrayRef (MakeNumber 0) - CommonCtor state this refToFirstElement lengthOfArray + let private CommonCtor (cilState : cilState) this refToFirst length = + let span = read cilState this + let initializedSpan = InitSpanStruct cilState span refToFirst length + write cilState this initializedSpan - let internal CtorFromPtrForSpan (state : state) (args : term list) : (term * state) list = + 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] - if ptr = MakeNullPtr typeof then - // Ptr came from localloc instruction - let elementType = Helpers.unwrapType wrappedType - let arrayRef = Memory.AllocateVectorArray state size elementType - CtorFromFromArray state this arrayRef - else - CommonCtor state this ptr size - - let internal CtorFromPtrForReadOnlySpan (state : state) (args : term list) : (term * state) list = - CtorFromPtrForSpan state args - - let internal CtorFromArrayForReadOnlySpan (state : state) (args : term list) : (term * state) list = + let t = Helpers.unwrapType wrappedType + let ctor cilState k = + let state = cilState.state + let ptr = + if isStackArray cilState 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 + (fun state k -> k (Arithmetics.GreaterOrEqual size (MakeNumber 0), state)) + ctor + (i.Raise i.ArgumentOutOfRangeException) + id + + let CtorFromArray (_ : IInterpreter) (cilState : cilState) (args : term list) : cilState list = assert(List.length args = 3) let this, arrayRef = args[0], args[2] - CtorFromFromArray state this arrayRef + let state = cilState.state + let refToFirstElement = Memory.ReferenceArrayIndex state arrayRef [MakeNumber 0] None + let lengthOfArray = Memory.ArrayLengthByDimension state arrayRef (MakeNumber 0) + CommonCtor cilState this refToFirstElement lengthOfArray - let ReadOnlySpanCreateFromString (state : state) (args : term list) : term = + let CreateFromString (_ : IInterpreter) (cilState : cilState) (args : term list) : cilState list = assert(List.length args = 1) let string = args[0] let spanType = readOnlySpanType().MakeGenericType(typeof) let span = Memory.DefaultOf spanType + let state = cilState.state let refToFirst = Memory.ReferenceField state string Reflection.stringFirstCharField let length = Memory.StringLength state string - InitSpanStruct span refToFirst length + let spanStruct = InitSpanStruct cilState span refToFirst length + push spanStruct cilState + List.singleton cilState diff --git a/VSharp.InternalCalls/Span.fsi b/VSharp.InternalCalls/Span.fsi index a65fc48dd..eea071678 100644 --- a/VSharp.InternalCalls/Span.fsi +++ b/VSharp.InternalCalls/Span.fsi @@ -3,26 +3,24 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL module internal ReadOnlySpan = - val GetContentsRef : state -> term -> term + val GetContents : cilState -> term -> term * term val GetLength : state -> term -> term [] - val GetItemFromReadOnlySpan : state -> term list -> term - [] - val GetItemFromSpan : state -> term list -> term - - [] - val CtorFromPtrForSpan : state -> term list -> (term * state) list + val GetItem : IInterpreter -> cilState -> term list -> cilState list [] - val CtorFromPtrForReadOnlySpan : state -> term list -> (term * state) list + [] + val CtorFromPtr : IInterpreter -> cilState -> term list -> cilState list [] - val CtorFromArrayForReadOnlySpan : state -> term list -> (term * state) list + [] + val CtorFromArray : IInterpreter -> cilState -> term list -> cilState list [] - val ReadOnlySpanCreateFromString : state -> term list -> term + val CreateFromString : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/String.fs b/VSharp.InternalCalls/String.fs index ac389d643..6c831c6fe 100644 --- a/VSharp.InternalCalls/String.fs +++ b/VSharp.InternalCalls/String.fs @@ -25,15 +25,13 @@ module internal String = Memory.StringFromReplicatedChar state this char length Nop() - let CtorFromSpan (state : state) (args : term list) : term = + let CtorFromSpan (_ : IInterpreter) (cilState : cilState) (args : term list) : cilState list = assert(List.length args = 2) let this, span = args[0], args[1] - let ref = ReadOnlySpan.GetContentsRef state span + let ref, len = ReadOnlySpan.GetContents cilState span assert(TypeOf ref |> TypeUtils.isArrayType) - let len = ReadOnlySpan.GetLength state span - match Memory.StringCtorOfCharArrayAndLen state ref this len with - | [ _ ] -> Nop() - | _ -> internalfail "CtorFromSpan: need to branch execution" + let states = Memory.StringCtorOfCharArrayAndLen cilState.state ref this len + List.map (changeState cilState) states let CtorFromPtr (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 4) diff --git a/VSharp.InternalCalls/String.fsi b/VSharp.InternalCalls/String.fsi index 928decc58..a4ca19db1 100644 --- a/VSharp.InternalCalls/String.fsi +++ b/VSharp.InternalCalls/String.fsi @@ -16,7 +16,7 @@ module internal String = val CtorFromReplicatedChar : state -> term list -> term [] - val CtorFromSpan : state -> term list -> term + val CtorFromSpan : IInterpreter -> cilState -> term list -> cilState list [] val CtorFromPtr : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/Unsafe.fs b/VSharp.InternalCalls/Unsafe.fs index 3c13d2755..618f23f90 100644 --- a/VSharp.InternalCalls/Unsafe.fs +++ b/VSharp.InternalCalls/Unsafe.fs @@ -3,33 +3,35 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilStateOperations // ------------------------------ System.Unsafe -------------------------------- -module Unsafe = +module internal Unsafe = - let internal AsPointer (_ : state) (args : term list) : term = + let AsPointer (_ : state) (args : term list) : term = assert(List.length args = 2) // Types.Cast (List.item 1 args) (Pointer Void) List.item 1 args - let internal ObjectAsT (_ : state) (args : term list) : term = + let ObjectAsT (_ : state) (args : term list) : term = assert(List.length args = 2) let typ, ref = args[0], args[1] let typ = Helpers.unwrapType typ Types.Cast ref typ - let internal AsRef (_ : state) (args : term list) : term = + let AsRef (_ : state) (args : term list) : term = assert(List.length args = 2) let t = Helpers.unwrapType args[0] let ptr = args[1] Types.Cast ptr (t.MakePointerType()) - let internal PointerAsRef (_ : state) (args : term list) : term = + let PointerAsRef (_ : state) (args : term list) : term = assert(List.length args = 2) - args.[1] + args[1] - let internal TFromAsTTo (_ : state) (args : term list) : term = + let TFromAsTTo (_ : state) (args : term list) : term = assert(List.length args = 3) let toType = Helpers.unwrapType args[1] let pointerType = toType.MakePointerType() @@ -37,22 +39,22 @@ module Unsafe = assert(IsReference ref || IsPtr ref) Types.Cast ref pointerType - let internal NullRef (_ : state) (args : term list) : term = + let NullRef (_ : state) (args : term list) : term = match args with | [{term = Concrete(:? Type as t, _)}] -> NullRef t | _ -> __unreachable__() - let internal IsNullRef (_ : state) (args : term list) : term = + let IsNullRef (_ : state) (args : term list) : term = assert(List.length args = 2) let ref = args[1] IsNullReference ref - let internal AddByteOffset (_ : state) (args : term list) : term = + let AddByteOffset (_ : state) (args : term list) : term = assert(List.length args = 3) let ref, offset = args[1], args[2] PerformBinaryOperation OperationType.Add ref offset id - let internal ByteOffset (_ : state) (args : term list) : term = + let ByteOffset (_ : state) (args : term list) : term = assert(List.length args = 2) let origin, target = args[0], args[1] let offset = PerformBinaryOperation OperationType.Subtract target origin id @@ -63,42 +65,47 @@ module Unsafe = let byteOffset = Arithmetics.Mul offset size PerformBinaryOperation OperationType.Add ref byteOffset id - let internal AddIntPtr (_ : state) (args : term list) : term = + let AddIntPtr (_ : state) (args : term list) : term = assert(List.length args = 3) let typ, ref, offset = args[0], args[1], args[2] CommonAdd typ ref offset - let internal AddInt (_ : state) (args : term list) : term = + let AddInt (_ : state) (args : term list) : term = assert(List.length args = 3) let typ, ref, offset = args[0], args[1], args[2] CommonAdd typ ref offset - let internal ReadUnaligned (state : state) (args : term list) : term = + let ReadUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 2) let typ, ref = args[0], args[1] let typ = Helpers.unwrapType typ let castedPtr = Types.Cast ref (typ.MakePointerType()) - Memory.Read state castedPtr + let readByPtr cilState k = + let value = read cilState castedPtr + push value cilState + List.singleton cilState |> k + i.NpeOrInvoke cilState castedPtr readByPtr id - let WriteUnaligned (state : state) (args : term list) : (term * state) list = + let WriteUnaligned (i : IInterpreter) (cilState : cilState) (args : term list) = assert(List.length args = 3) let typ, ref, value = args[0], args[1], args[2] let typ = Helpers.unwrapType typ let castedPtr = Types.Cast ref (typ.MakePointerType()) - let states = Memory.Write state castedPtr value - List.map (withFst <| Nop()) states + let writeByPtr cilState k = + write cilState castedPtr value |> k + i.NpeOrInvoke cilState castedPtr writeByPtr id - let internal SizeOf (_ : state) (args : term list) : term = + let SizeOf (_ : state) (args : term list) : term = assert(List.length args = 1) let typ = Helpers.unwrapType args[0] Types.SizeOf typ |> MakeNumber - let internal AreSame (_ : state) (args : term list) : term = + let AreSame (_ : state) (args : term list) : term = assert(List.length args = 3) let ptr1, ptr2 = args[1], args[2] ptr1 === ptr2 - let internal GetRawData (state : state) (args : term list) : term = + let GetRawData (state : state) (args : term list) : term = assert(List.length args = 1) let ref = args[0] match ref.term with @@ -109,5 +116,5 @@ module Unsafe = Ptr (HeapLocation(address, t)) typeof (MakeNumber 0) | _ -> internalfail $"GetRawData: unexpected ref {ref}" - let internal SkipInit (_ : state) (_ : term list) : term = + let SkipInit (_ : state) (_ : term list) : term = Nop() diff --git a/VSharp.InternalCalls/Unsafe.fsi b/VSharp.InternalCalls/Unsafe.fsi index 8047965f2..ddd154ae4 100644 --- a/VSharp.InternalCalls/Unsafe.fsi +++ b/VSharp.InternalCalls/Unsafe.fsi @@ -3,6 +3,7 @@ namespace VSharp.System open global.System open VSharp open VSharp.Core +open VSharp.Interpreter.IL module internal Unsafe = @@ -56,11 +57,11 @@ module internal Unsafe = [] [] - val ReadUnaligned : state -> term list -> term + val ReadUnaligned : IInterpreter -> cilState -> term list -> cilState list [] [] - val WriteUnaligned : state -> term list -> (term * state) list + val WriteUnaligned : IInterpreter -> cilState -> term list -> cilState list [] [] diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 75a5cb2b5..64949971d 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -327,8 +327,11 @@ module API = let indices = List.map (fun i -> primitiveCast i typeof) indices match arrayRef.term with | HeapRef(addr, typ) -> - let elemType, dim, _ as arrayType = - Memory.mostConcreteTypeOfHeapRef state addr typ |> symbolicTypeToArrayType + let t = Memory.mostConcreteTypeOfHeapRef state addr typ + let addr, (elemType, dim, _ as arrayType) = + if TypeUtils.isArrayType t then + addr, symbolicTypeToArrayType t + else StringArrayInfo state addr None assert(dim = List.length indices) match valueType with | Some valueType when not (IsSafeContext elemType valueType) -> diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index ab27e2252..45012603e 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -1214,7 +1214,7 @@ module internal Memory = assert(typeOf offset = typeof) let zero = makeNumber 0 match pointerBase with - | HeapLocation(address, t) -> + | HeapLocation(address, t) when address <> zeroAddress() -> let typ = typeOfHeapLocation state address |> mostConcreteType t let isArray() = typ.IsSZArray && typ.GetElementType() = sightType @@ -1232,7 +1232,7 @@ module internal Memory = else address, (sightType, 1, true) ArrayIndex(address, [index], arrayType) |> Some else None - elif typ.IsValueType && sightType = typ && offset = zero then + elif isValueType typ && sightType = typ && offset = zero then BoxedLocation(address, t) |> Some else None | StackLocation stackKey when stackKey.TypeOfLocation = sightType && offset = zero -> diff --git a/VSharp.SILI.Core/Pointers.fs b/VSharp.SILI.Core/Pointers.fs index c3e4b3aa6..dfa3d9ec5 100644 --- a/VSharp.SILI.Core/Pointers.fs +++ b/VSharp.SILI.Core/Pointers.fs @@ -129,7 +129,7 @@ module internal Pointers = shift ptr bytesToShift |> k | HeapRef(address, t) -> assert t.IsArray - let ptrType = t.GetElementType().MakePointerType() + let ptrType = t.GetElementType() Ptr (HeapLocation(address, t)) ptrType bytesToShift |> k | _ -> internalfailf "address arithmetic: expected pointer, but got %O" ptr diff --git a/VSharp.Utils/TypeUtils.fs b/VSharp.Utils/TypeUtils.fs index c770c5ef6..b7fc68c5a 100644 --- a/VSharp.Utils/TypeUtils.fs +++ b/VSharp.Utils/TypeUtils.fs @@ -205,7 +205,7 @@ module TypeUtils = if isValueTypeParameter t then true elif isReferenceTypeParameter t then false else __insufficientInformation__ "Can't determine if %O is a value type or not!" t - | t -> t.IsValueType && t <> addressType + | t -> t.IsValueType && t <> addressType && t <> typeof let isNullable = function | (t : Type) when t.IsGenericParameter -> @@ -495,9 +495,13 @@ module TypeUtils = /// 'mostConcreteType' will return 'leftType' /// Example: mostConcreteType typeof typeof == typeof let inline mostConcreteType (leftType : Type) (rightType : Type) = + let isStringCase() = + rightType = typeof && leftType = typeof + || leftType = typeof && rightType = typeof if leftType = null then rightType elif rightType = null then leftType elif rightType.IsAssignableFrom(leftType) then leftType + elif isStringCase() then typeof else assert leftType.IsAssignableFrom(rightType) rightType From 95ecbcedfb21193574a2e0a8b279830def87614e Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Thu, 7 Sep 2023 22:53:12 +0300 Subject: [PATCH 19/20] [test] changed coverage for 'SpanTest' --- VSharp.Test/Tests/Lists.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 03a2c60fc..bdcf89619 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -869,7 +869,7 @@ public static Array RetSystemArray3(Array arr) [TestSvmFixture] public static class SpanTests { - [TestSvm(100)] + [TestSvm(96)] public static unsafe byte SpanTest(int[] a, byte b, int i) { fixed (void* ptr = a) From 15f152bb5c42475984a981ea6ecae54d9db15d81 Mon Sep 17 00:00:00 2001 From: MchKosticyn Date: Fri, 8 Sep 2023 17:32:03 +0300 Subject: [PATCH 20/20] [fix] deleted 'lastPushInfo' from cilState --- VSharp.SILI/CILState.fs | 3 --- 1 file changed, 3 deletions(-) diff --git a/VSharp.SILI/CILState.fs b/VSharp.SILI/CILState.fs index fb6be2f75..14fb53202 100644 --- a/VSharp.SILI/CILState.fs +++ b/VSharp.SILI/CILState.fs @@ -31,7 +31,6 @@ type cilState = mutable stepsNumber : uint mutable suspended : bool mutable targets : Set - mutable lastPushInfo : term option /// /// All basic blocks visited by the state. /// @@ -80,7 +79,6 @@ module CilStateOperations = stepsNumber = 0u suspended = false targets = Set.empty - lastPushInfo = None history = Set.empty entryMethod = Some entryMethod id = getNextStateId() @@ -272,7 +270,6 @@ module CilStateOperations = | Nop -> internalfail "pushing 'NOP' value onto evaluation stack" | _ -> cilState.state.evaluationStack <- EvaluationStack.Push v cilState.state.evaluationStack - cilState.lastPushInfo <- Some v let pushMany vs (cilState : cilState) = if List.contains (Nop()) vs then