From 8f370a6afd57bcf283b549e9292841d44ca4895c Mon Sep 17 00:00:00 2001 From: Startsev Matvey Date: Thu, 1 Aug 2024 21:55:23 +0300 Subject: [PATCH] [feat] add symbolic collections Signed-off-by: Startsev Matvey --- VSharp.CSharpUtils/ListUtils.cs | 158 ++++ VSharp.IL/Loader.fs | 2 + VSharp.IL/MethodBody.fs | 8 +- VSharp.InternalCalls/Dictionary.fs | 104 +++ VSharp.InternalCalls/Dictionary.fsi | 24 + VSharp.InternalCalls/List.fs | 174 ++++ VSharp.InternalCalls/List.fsi | 53 ++ VSharp.InternalCalls/Set.fs | 39 + VSharp.InternalCalls/Set.fsi | 24 + VSharp.SILI.Core/API.fs | 448 ++++++++- VSharp.SILI.Core/API.fsi | 57 ++ VSharp.SILI.Core/Branching.fs | 17 + VSharp.SILI.Core/ConcreteMemory.fs | 148 ++- VSharp.SILI.Core/ConcreteMemory.fsi | 16 + VSharp.SILI.Core/Memory.fs | 1248 +++++++++++++++++++++++-- VSharp.SILI.Core/MemoryRegion.fs | 382 +++++++- VSharp.SILI.Core/State.fs | 47 +- VSharp.SILI.Core/Substitution.fs | 9 + VSharp.SILI.Core/Terms.fs | 242 ++++- VSharp.SILI/Interpreter.fs | 4 + VSharp.Solver/Z3.fs | 253 ++++- VSharp.Test/Tests/BoxUnbox.cs | 12 +- VSharp.Test/Tests/Dictionaries.cs | 247 +++++ VSharp.Test/Tests/Generic.cs | 8 +- VSharp.Test/Tests/Lists.cs | 23 +- VSharp.Test/Tests/Sets.cs | 188 ++++ VSharp.Test/Tests/SymbolicLists.cs | 114 +++ VSharp.TestGenerator/TestGenerator.fs | 13 +- VSharp.Utils/Reflection.fs | 15 + VSharp.Utils/TypeUtils.fs | 34 + 30 files changed, 3938 insertions(+), 173 deletions(-) create mode 100644 VSharp.CSharpUtils/ListUtils.cs create mode 100644 VSharp.InternalCalls/Dictionary.fs create mode 100644 VSharp.InternalCalls/Dictionary.fsi create mode 100644 VSharp.InternalCalls/List.fs create mode 100644 VSharp.InternalCalls/List.fsi create mode 100644 VSharp.InternalCalls/Set.fs create mode 100644 VSharp.InternalCalls/Set.fsi create mode 100644 VSharp.Test/Tests/Dictionaries.cs create mode 100644 VSharp.Test/Tests/Sets.cs create mode 100644 VSharp.Test/Tests/SymbolicLists.cs diff --git a/VSharp.CSharpUtils/ListUtils.cs b/VSharp.CSharpUtils/ListUtils.cs new file mode 100644 index 000000000..4a8ae379c --- /dev/null +++ b/VSharp.CSharpUtils/ListUtils.cs @@ -0,0 +1,158 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; + +namespace VSharp.CSharpUtils +{ + public struct ListEnumerator : IEnumerator, IEnumerator + { + private readonly List _list; + private int _index; + private T? _current; + + internal ListEnumerator(List list) + { + _list = list; + _index = 0; + _current = default; + } + + public void Dispose() + { + } + + public bool MoveNext() + { + if ((uint)_index < (uint)_list.Count) + { + _current = _list[_index]; + _index++; + return true; + } + return MoveNextRare(); + } + + private bool MoveNextRare() + { + _index = _list.Count + 1; + _current = default; + return false; + } + + public T Current => _current!; + + object? IEnumerator.Current + { + get + { + if (_index == 0 || _index == _list.Count + 1) + { + throw new InvalidOperationException(); + } + return Current; + } + } + + void IEnumerator.Reset() + { + _index = 0; + _current = default; + } + } + + public static class ListUtils + { + [Implements("System.Int32 System.Collections.Generic.LinkedList`1[T].IndexOf(this, T)")] + [Implements("System.Int32 System.Collections.Generic.List`1[T].IndexOf(this, T)")] + public static int IndexOf(List list, T value) + { + var count = list.Count; + var index = 0; + + while (index < count) + { + if (list[index].Equals(value)) return index; + + index++; + } + + return -1; + } + + [Implements("System.Boolean System.Collections.Generic.LinkedList`1[T].Remove(this, T)")] + [Implements("System.Boolean System.Collections.Generic.List`1[T].Remove(this, T)")] + public static bool Remove(List list, T value) + { + var count = list.Count; + var index = 0; + + while (index < count) + { + if (list[index].Equals(value)) break; + + index++; + } + + if (index == -1) + { + return false; + } + + list.RemoveAt(index); + return true; + } + + [Implements("T System.Collections.Generic.LinkedList`1[T].LastOrDefault(this)")] + [Implements("T System.Collections.Generic.List`1[T].LastOrDefault(this)")] + public static T LastOrDefault(List list) + { + if (list.Count == 0) + { + return default(T); + } + + return list.Last(); + } + + [Implements("System.Boolean System.Collections.Generic.LinkedList`1[T].Contains(this, T)")] + [Implements("System.Boolean System.Collections.Generic.List`1[T].Contains(this, T)")] + public static bool Contains(List list, T item) + { + var count = list.Count; + var index = 0; + + while (index < count) + { + if (list[index].Equals(item)) return true; + + index++; + } + + return false; + } + + [Implements("System.Int32 System.Collections.Generic.LinkedList`1[T].LastIndexOf(this, T)")] + [Implements("System.Int32 System.Collections.Generic.List`1[T].LastIndexOf(this, T)")] + public static int LastIndexOf(List list, T item) + { + var index = list.Count - 1; + + while (0 <= index) + { + if (list[index].Equals(item)) return index; + + index--; + } + + return -1; + } + + [Implements( + "System.Collections.Generic.IEnumerator`1[T] System.Collections.Generic.List`1[T].System.Collections.Generic.IEnumerable.GetEnumerator(this)")] + public static IEnumerator GetEnumerator(List list) + { + return new ListEnumerator(list); + } + } +} diff --git a/VSharp.IL/Loader.fs b/VSharp.IL/Loader.fs index 08a50023f..df6505781 100644 --- a/VSharp.IL/Loader.fs +++ b/VSharp.IL/Loader.fs @@ -49,6 +49,8 @@ module Loader = CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.DebugProviderUtils") CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.EnvironmentUtils") CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.JetBrainsDiagnosticsUtils") + CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.ListUtils") + CSharpUtilsAssembly.GetType("VSharp.CSharpUtils.ListEnumerator`1") ] |> collectImplementations diff --git a/VSharp.IL/MethodBody.fs b/VSharp.IL/MethodBody.fs index 5f80a459c..692f23fe7 100644 --- a/VSharp.IL/MethodBody.fs +++ b/VSharp.IL/MethodBody.fs @@ -84,7 +84,13 @@ type MethodWithBody internal (m : MethodBase) = let actualMethod = if not isCSharpInternalCall.Value then m - else Loader.CSharpImplementations[fullGenericMethodName.Value] + else + let method = Loader.CSharpImplementations[fullGenericMethodName.Value] + if method.IsGenericMethod && (m.DeclaringType.IsGenericType || m.IsGenericMethod) then + let _, genericArgs, _ = Reflection.generalizeMethodBase m + method.MakeGenericMethod(genericArgs) + else method + let methodBodyBytes = if isFSharpInternalCall.Value then null else actualMethod.GetMethodBody() diff --git a/VSharp.InternalCalls/Dictionary.fs b/VSharp.InternalCalls/Dictionary.fs new file mode 100644 index 000000000..5618ed04b --- /dev/null +++ b/VSharp.InternalCalls/Dictionary.fs @@ -0,0 +1,104 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState +open VSharp.TypeUtils +open Arithmetics + +module internal Dictionary = + let GetCount (state : state) (args : term list) = + assert(List.length args = 3) + let this = args[0] + Memory.GetDictionaryCount state this + + let IsContainsKey (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 4) + let this, key = args[0], args[3] + let keyType = TypeOf key + let contains (cilState : cilState) k = + cilState.Push <| Memory.ContainsKey cilState.state this key + k [cilState] + match keyType with + | ReferenceType -> + cilState.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference key, state)) + (interpreter.Raise interpreter.ArgumentNullException) + contains + id + | _ -> contains cilState id + + let GetItem (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 4) + let dictionary, key = args[0], args[3] + let keyType = TypeOf key + let get (cilState : cilState) k = + let state = cilState.state + let count = Memory.GetDictionaryCount state dictionary + let assume = count >> MakeNumber 0 + AssumeStatedConditionalExecution state assume + let value = Memory.ReadDictionaryKey state dictionary key + cilState.Push value + k [cilState] + let elseBranch (cilState : cilState) k = + k <| cilState.StatedConditionalExecutionCIL + (fun state k -> k (Memory.ContainsKey cilState.state dictionary key, state)) + get + (interpreter.Raise interpreter.ArgumentException) + id + match keyType with + | ReferenceType -> + cilState.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference key, state)) + (interpreter.Raise interpreter.ArgumentNullException) + elseBranch + id + | _ -> elseBranch cilState id + + let SetItem (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 5) + let dictionary, key, value = args[0], args[3], args[4] + let keyType = TypeOf key + let set (cilState : cilState) k = + let state = cilState.state + Memory.WriteDictionaryKey cilState.state dictionary key value + let count = Memory.GetDictionaryCount state dictionary + let assume = count >> MakeNumber 0 + AssumeStatedConditionalExecution state assume + k [cilState] + match keyType with + | ReferenceType -> + cilState.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference key, state)) + (interpreter.Raise interpreter.ArgumentNullException) + set + id + | _ -> set cilState id + + let AddElement (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(List.length args = 5) + let dictionary, key, value = args[0], args[3], args[4] + let keyType = TypeOf key + let add (cilState : cilState) k = + let state = cilState.state + Memory.WriteDictionaryKey state dictionary key value + let count = Memory.GetDictionaryCount state dictionary + let assume = count >> MakeNumber 0 + AssumeStatedConditionalExecution state assume + k [cilState] + let elseBranch (cilState : cilState) k = + k <| cilState.StatedConditionalExecutionCIL + (fun state k -> k (Memory.ContainsKey cilState.state dictionary key, state)) + (interpreter.Raise interpreter.ArgumentException) + add + id + match keyType with + | ReferenceType -> + cilState.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference key, state)) + (interpreter.Raise interpreter.ArgumentNullException) + elseBranch + id + | _ -> elseBranch cilState id diff --git a/VSharp.InternalCalls/Dictionary.fsi b/VSharp.InternalCalls/Dictionary.fsi new file mode 100644 index 000000000..84eaba56d --- /dev/null +++ b/VSharp.InternalCalls/Dictionary.fsi @@ -0,0 +1,24 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState + +module internal Dictionary = + + [] + val GetCount : state -> term list -> term + + [] + val IsContainsKey : IInterpreter -> cilState -> term list -> cilState list + + [] + val GetItem : IInterpreter -> cilState -> term list -> cilState list + + [] + val SetItem : IInterpreter -> cilState -> term list -> cilState list + + [] + val AddElement : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/List.fs b/VSharp.InternalCalls/List.fs new file mode 100644 index 000000000..8874511e7 --- /dev/null +++ b/VSharp.InternalCalls/List.fs @@ -0,0 +1,174 @@ +namespace VSharp.System + +open System +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState +open VSharp.TypeUtils +open Arithmetics + +module internal List = + let inRange index count = + let left = (MakeNumber 0) <<= index + let right = index << count + left &&& right + + let GetCount (state : state) (args : term list) = + assert(args.Length = 2) + let this = args[0] + Memory.GetListCount state this + + let AddItem (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 3) + let this, item = args[0], args[2] + let state = cilState.state + let count = Memory.GetListCount state this + Memory.WriteListKey state this count item + let newCount = Memory.GetListCount state this + let assume = (MakeNumber 0) << newCount + AssumeStatedConditionalExecution state assume + [cilState] + + let SetItem (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 4) + let this, index, item = args[0], args[2], args[3] + let count = Memory.GetListCount cilState.state this + let notEmpty = count !== (MakeNumber 0) + let set (cilState : cilState) k = + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + Memory.WriteListKey cilState.state this index item + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k ((&&&) notEmpty <| inRange index count, state)) + set + (interpreter.Raise interpreter.ArgumentOutOfRangeException) + id + + let ReadByIndex (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 3) + let this, index = args[0], args[2] + let count = Memory.GetListCount cilState.state this + let read (cilState : cilState) k = + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + cilState.Push <| Memory.ReadListIndex cilState.state this index + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k (inRange index count, state)) + read + (interpreter.Raise interpreter.ArgumentOutOfRangeException) + id + + let ReadFirst (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 2) + let this = args[0] + let index = MakeNumber 0 + let count = Memory.GetListCount cilState.state this + let notEmpty = count !== (MakeNumber 0) + let read (cilState : cilState) k = + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + cilState.Push <| Memory.ReadListIndex cilState.state this index + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k (notEmpty, state)) + read + (interpreter.Raise interpreter.InvalidOperationException) + id + + let ReadLast (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 2) + let this = args[0] + let count = Memory.GetListCount cilState.state this + let index = Sub count <| MakeNumber 1 + let notEmpty = count !== (MakeNumber 0) + let read (cilState : cilState) k = + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + cilState.Push <| Memory.ReadListIndex cilState.state this index + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k (notEmpty, state)) + read + (interpreter.Raise interpreter.InvalidOperationException) + id + + let RemoveAt (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 3) + let this, index = args[0], args[2] + let count = Memory.GetListCount cilState.state this + let remove (cilState : cilState) k = + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + Memory.RemoveListAtIndex cilState.state this index + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k (inRange index count, state)) + remove + (interpreter.Raise interpreter.ArgumentOutOfRangeException) + id + + let Insert (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 4) + let this, index, item = args[0], args[2], args[3] + let count = Memory.GetListCount cilState.state this + let condition = (inRange index count) ||| (index === count) + let insert (cilState : cilState) k = + Memory.InsertListIndex cilState.state this index item + let count = Memory.GetListCount cilState.state this + let assume = (MakeNumber 0) << count + AssumeStatedConditionalExecution cilState.state assume + k [cilState] + cilState.StatedConditionalExecutionCIL + (fun state k -> k (condition, state)) + insert + (interpreter.Raise interpreter.ArgumentOutOfRangeException) + id + + + let CopyToRange (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 6) + let this, index, array, arrayIndex, count = args[0], args[2], args[3], args[4], args[5] + let listCount = Memory.GetListCount cilState.state this + let arrayCount = SystemArray.get_Length cilState.state [array] + let copy (cilState : cilState) k = + Memory.ListCopyToRange cilState.state this index array arrayIndex count + k [cilState] + let inRangeBranch (cilState : cilState) k = + let condition = (Sub listCount index) >> (Sub arrayCount arrayIndex) + cilState.StatedConditionalExecutionCIL + (fun state k -> k (condition, state)) + (interpreter.Raise interpreter.ArgumentException) + copy + k + let notNullBranch (cilState : cilState) k = + let condition = + let isNegative term = (MakeNumber 0) >> term + (isNegative index) ||| (isNegative arrayIndex) ||| (isNegative count) + cilState.StatedConditionalExecutionCIL + (fun state k -> k (condition, state)) + (interpreter.Raise interpreter.ArgumentOutOfRangeException) + inRangeBranch + k + cilState.StatedConditionalExecutionCIL + (fun state k -> k (IsNullReference array, state)) + (interpreter.Raise interpreter.NullReferenceException) + notNullBranch + id + + let CopyToFull (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 4) + let this, array, arrayIndex = args[0], args[2], args[3] + let index = MakeNumber 0 + let count = Memory.GetListCount cilState.state this + CopyToRange interpreter cilState [this; args[1]; index; array; arrayIndex; count] + + let CopyToSimple (interpreter : IInterpreter) (cilState : cilState) (args : term list) = + assert(args.Length = 3) + let this, array = args[0], args[2] + let index = MakeNumber 0 + let count = Memory.GetListCount cilState.state this + CopyToRange interpreter cilState [this; args[1]; index; array; index; count] diff --git a/VSharp.InternalCalls/List.fsi b/VSharp.InternalCalls/List.fsi new file mode 100644 index 000000000..9cba5e96c --- /dev/null +++ b/VSharp.InternalCalls/List.fsi @@ -0,0 +1,53 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState + +module internal List = + + [] + [] + val GetCount : state -> term list -> term + + [] + [] + val AddItem : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val SetItem : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val ReadByIndex : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val ReadFirst : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val ReadLast : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val RemoveAt : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val Insert : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val CopyToRange : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val CopyToFull : IInterpreter -> cilState -> term list -> cilState list + + [] + [] + val CopyToSimple : IInterpreter -> cilState -> term list -> cilState list diff --git a/VSharp.InternalCalls/Set.fs b/VSharp.InternalCalls/Set.fs new file mode 100644 index 000000000..f5c2df26a --- /dev/null +++ b/VSharp.InternalCalls/Set.fs @@ -0,0 +1,39 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState +open VSharp.TypeUtils +open Arithmetics + +module internal Set = + + let IsContainsItem (state : state) (args : term list) = + assert(List.length args = 3) + let this, item = args[0], args[2] + Memory.IsSetContains state this item + + let AddItem (state : state) (args : term list) = + assert(List.length args = 3) + let this, item = args[0], args[2] + let isAdd = Memory.AddToSet state this item + let count = Memory.GetSetCount state this + let assume = count >> MakeNumber 0 + AssumeStatedConditionalExecution state assume + isAdd + + let RemoveItem (state : state) (args : term list) = + assert(List.length args = 3) + let this, item = args[0], args[2] + let count = Memory.GetSetCount state this + let contains = Memory.IsSetContains state this item + let assume = (!! contains) ||| (count >> MakeNumber 0) + AssumeStatedConditionalExecution state assume + Memory.RemoveFromSet state this item + + let GetCount (state : state) (args : term list) = + assert(List.length args = 2) + let this = args[0] + Memory.GetSetCount state this diff --git a/VSharp.InternalCalls/Set.fsi b/VSharp.InternalCalls/Set.fsi new file mode 100644 index 000000000..335ef7ac8 --- /dev/null +++ b/VSharp.InternalCalls/Set.fsi @@ -0,0 +1,24 @@ +namespace VSharp.System + +open global.System +open VSharp +open VSharp.Core +open VSharp.Interpreter.IL +open VSharp.Interpreter.IL.CilState + +module internal Set = + [] + [] + val AddItem : state -> term list -> term + + [] + [] + val RemoveItem : state -> term list -> term + + [] + [] + val IsContainsItem : state -> term list -> term + + [] + [] + val GetCount : state -> term list -> term diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 6c1359775..0978d0ace 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -4,6 +4,8 @@ open System open FSharpx.Collections open VSharp open VSharp.Core +open DictionaryType +open SetType module API = @@ -35,7 +37,7 @@ module API = let StatedConditionalExecutionAppend (state : state) conditionInvocation thenBranch elseBranch k = Branching.commonStatedConditionalExecutionk state conditionInvocation thenBranch elseBranch (fun x y -> [x;y]) (List.concat >> k) let StatedConditionalExecution = Branching.commonStatedConditionalExecutionk - + let AssumeStatedConditionalExecution state assume = Branching.assumeStatedConditionalExecution state assume let GuardedApplyExpressionWithPC pc term f = Merging.guardedApplyWithPC pc f term let GuardedApplyExpression term f = Merging.guardedApply f term let GuardedStatedApplyStatementK state term f k = Branching.guardedStatedApplyk f state term k @@ -120,7 +122,6 @@ module API = let IsBadRef term = Pointers.isBadRef term let GetHashCode term = Memory.getHashCode term - let ReinterpretConcretes terms t = reinterpretConcretes terms t let TryPtrToRef state pointerBase sightType offset = @@ -180,6 +181,9 @@ module API = let (|CombinedDelegate|_|) t = (|CombinedDelegate|_|) t.term let (|ConcreteDelegate|_|) t = (|ConcreteDelegate|_|) t.term + let IsTrue term = isTrue term + let IsFalse term = isFalse term + let (|True|_|) t = (|True|_|) t let (|False|_|) t = (|False|_|) t let (|Negation|_|) t = (|NegationT|_|) t @@ -208,6 +212,32 @@ module API = | _ -> None let (|ArrayIndexReading|_|) src = Memory.(|ArrayIndexReading|_|) src + let (|BoolDictionaryReading|_|) src = Memory.(|BoolDictionaryReading|_|) src + let (|ByteDictionaryReading|_|) src = Memory.(|ByteDictionaryReading|_|) src + let (|SByteDictionaryReading|_|) src = Memory.(|SByteDictionaryReading|_|) src + let (|CharDictionaryReading|_|) src = Memory.(|CharDictionaryReading|_|) src + let (|DecimalDictionaryReading|_|) src = Memory.(|DecimalDictionaryReading|_|) src + let (|DoubleDictionaryReading|_|) src = Memory.(|DoubleDictionaryReading|_|) src + let (|IntDictionaryReading|_|) src = Memory.(|IntDictionaryReading|_|) src + let (|UIntDictionaryReading|_|) src = Memory.(|UIntDictionaryReading|_|) src + let (|LongDictionaryReading|_|) src = Memory.(|LongDictionaryReading|_|) src + let (|ULongDictionaryReading|_|) src = Memory.(|ULongDictionaryReading|_|) src + let (|ShortDictionaryReading|_|) src = Memory.(|ShortDictionaryReading|_|) src + let (|UShortDictionaryReading|_|) src = Memory.(|UShortDictionaryReading|_|) src + let (|AddrDictionaryReading|_|) src = Memory.(|AddrDictionaryReading|_|) src + let (|BoolSetReading|_|) src = Memory.(|BoolSetReading|_|) src + let (|ByteSetReading|_|) src = Memory.(|ByteSetReading|_|) src + let (|SByteSetReading|_|) src = Memory.(|SByteSetReading|_|) src + let (|CharSetReading|_|) src = Memory.(|CharSetReading|_|) src + let (|DecimalSetReading|_|) src = Memory.(|DecimalSetReading|_|) src + let (|DoubleSetReading|_|) src = Memory.(|DoubleSetReading|_|) src + let (|IntSetReading|_|) src = Memory.(|IntSetReading|_|) src + let (|UIntSetReading|_|) src = Memory.(|UIntSetReading|_|) src + let (|LongSetReading|_|) src = Memory.(|LongSetReading|_|) src + let (|ULongSetReading|_|) src = Memory.(|ULongSetReading|_|) src + let (|ShortSetReading|_|) src = Memory.(|ShortSetReading|_|) src + let (|UShortSetReading|_|) src = Memory.(|UShortSetReading|_|) src + let (|AddrSetReading|_|) src = Memory.(|AddrSetReading|_|) src let (|VectorIndexReading|_|) src = Memory.(|VectorIndexReading|_|) src let (|StackBufferReading|_|) src = Memory.(|StackBufferReading|_|) src let (|StaticsReading|_|) src = Memory.(|StaticsReading|_|) src @@ -281,6 +311,8 @@ module API = let ArrayTypeToSymbolicType arrayType = arrayTypeToSymbolicType arrayType let SymbolicTypeToArrayType typ = symbolicTypeToArrayType typ + let SymbolicTypeToDictionaryType typ = symbolicTypeToDictionaryType typ + let SymbolicTypeToSetType typ = symbolicTypeToSetType typ let TypeIsType leftType rightType = TypeCasting.typeIsType leftType rightType let TypeIsRef state typ ref = TypeCasting.typeIsRef state typ ref let RefIsType state ref typ = TypeCasting.refIsType state ref typ @@ -364,7 +396,7 @@ module API = module public Memory = open Memory - + open Arithmetics let EmptyIsolatedState() = state.MakeEmpty false let EmptyCompleteState() = state.MakeEmpty true @@ -434,6 +466,27 @@ module API = let ReferenceField state reference fieldId = state.memory.ReferenceField reference fieldId + let ReferenceKey state reference key typ = + state.memory.ReferenceKey reference key typ + + let DictionaryKeyContains state dict key typ = + state.memory.DictionaryKeyContains dict key typ + + let DictionaryCount state dict typ = + state.memory.DictionaryCount dict typ + + let SetKey state set value typ = + state.memory.SetKey set value typ + + let SetCount state set typ = + state.memory.SetCount set typ + + let ListIndex state list index typ = + state.memory.ListIndex list index typ + + let ListCount state list typ = + state.memory.ListCount list typ + let private CommonTryAddressFromRef state ref shouldFork = let zero = MakeNumber 0 let singleton address = List.singleton (address, state) @@ -525,6 +578,121 @@ module API = let ReadStaticField state typ field = state.memory.ReadStaticField typ field let ReadDelegate state reference = state.memory.ReadDelegate reference + let rec CommonReadDictionaryKey reporter state dictionary key = + match dictionary.term with + | HeapRef(dictionary, typ) -> state.memory.Read reporter <| ReferenceKey state dictionary key typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonReadDictionaryKey reporter state t key) + | _ -> internalfail $"Reading by key at {dictionary}" + + let ReadDictionaryKey state (dictionary : term) (key : term) = + CommonReadDictionaryKey emptyReporter state dictionary key + + let rec CommonContainsKey reporter state dictionary key = + match dictionary.term with + | HeapRef(dictionary, typ) -> state.memory.Read reporter <| DictionaryKeyContains state dictionary key typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonContainsKey reporter state t key) + | _ -> internalfail $"Reading by key at {dictionary}" + + let ContainsKey state (dictionary : term) (key : term) = + CommonContainsKey emptyReporter state dictionary key + + let rec CommonGetDictionaryCount reporter state dict = + match dict.term with + | HeapRef(dict, typ) -> state.memory.Read reporter <| DictionaryCount state dict typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonGetDictionaryCount reporter state t) + | _ -> internalfail $"Reading count by key at {dict}" + + let GetDictionaryCount state (set : term) = + CommonGetDictionaryCount emptyReporter state set + + let rec CommonReadSetKey reporter state set item = + match set.term with + | HeapRef(set, typ) -> state.memory.Read reporter <| SetKey state set item typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonReadSetKey reporter state t item) + | _ -> internalfail $"Reading by key at {set}" + + let ReadSetKey state (set : term) (item : term) = + CommonReadSetKey emptyReporter state set item + + let IsSetContains state set item = ReadSetKey state set item + + let rec CommonReadSetCount reporter state set = + match set.term with + | HeapRef(set, typ) -> state.memory.Read reporter <| SetCount state set typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonReadSetCount reporter state t) + | _ -> internalfail $"Reading count of {set}" + + let GetSetCount state (set : term) = + CommonReadSetCount emptyReporter state set + + let rec CommonReadListIndex reporter state list index = + match list.term with + | HeapRef(list, typ) -> state.memory.Read reporter <| ListIndex state list index typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonReadListIndex reporter state t index) + | _ -> internalfail $"Reading by index at {list}" + + let ReadListIndex state (list : term) (index : term) = + CommonReadListIndex emptyReporter state list index + + let rec CommonGetListCount reporter state list = + match list.term with + | HeapRef(list, typ) -> state.memory.Read reporter <| ListCount state list typ + | Ite iteType -> + iteType.filter (fun v -> True() <> IsBadRef v) + |> Merging.guardedMap (fun t -> CommonGetListCount reporter state t) + | _ -> internalfail $"Reading count of {list}" + + let GetListCount state (list : term) = + CommonGetListCount emptyReporter state list + + let rec CommonRemoveListAtIndex reporter state list index = + match list.term with + | HeapRef(listAddr, typ) -> + let count = GetListCount state list + let listType = symbolicTypeToListType typ + state.memory.ListRemoveAt listAddr index listType count + let newCount = Sub count <| MakeNumber 1 + let address = ListCount state listAddr typ + state.memory.Write reporter address newCount + | _ -> internalfail $"Reading by index at {list}" + + let RemoveListAtIndex state (list : term) (index : term) = + CommonRemoveListAtIndex emptyReporter state list index + + let rec CommonInsertListIndex reporter state list index item = + match list.term with + | HeapRef(listAddr, typ) -> + let count = GetListCount state list + let listType = symbolicTypeToListType typ + state.memory.ListInsertIndex listAddr index item listType count + let newCount = Add count <| MakeNumber 1 + let address = ListCount state listAddr typ + state.memory.Write reporter address newCount + | _ -> internalfail $"Reading by index at {list}" + + let InsertListIndex state (list : term) (index : term) (item : term) = + CommonInsertListIndex emptyReporter state list index item + + let ListCopyToRange state list index array indexArray count = + match list.term, array.term with + | HeapRef(listAddr, listType), HeapRef(arrayAddr, arrayTyp) -> + let listType = symbolicTypeToListType listType + let arrayType = symbolicTypeToArrayType arrayTyp + state.memory.ListCopyToRange listAddr index arrayAddr indexArray count listType arrayType + | _ -> internalfail $"List copy to range at {list} and {array}" + let CombineDelegates state delegates t = state.memory.CombineDelegates delegates t let RemoveDelegate state source toRemove t = @@ -542,6 +710,77 @@ module API = let WriteStructField structure field value = writeStruct structure field value + let CommonUpdateDictionaryCount reporter state dictionary contains typ = + let address = DictionaryCount state dictionary typ + let oldCount = state.memory.Read reporter address + let falseValue = Add oldCount <| MakeNumber 1 + let iteType = { branches = [(contains, oldCount)]; elseValue = falseValue } + let newCount = Ite iteType + state.memory.Write reporter address newCount + + let CommonWriteDictionaryKey reporter state dictionary key value = + match dictionary.term with + | HeapRef(dictAddr, typ) -> + let address = ReferenceKey state dictAddr key typ + let contains = ContainsKey state dictionary key + state.memory.Write reporter address value + CommonUpdateDictionaryCount reporter state dictAddr contains typ + | _ -> internalfail $"Writing at {dictionary} by key" + + let WriteDictionaryKey state dictionary key value = + CommonWriteDictionaryKey emptyReporter state dictionary key value + + let CommonUpdateSetCount reporter state set isAdd isContains typ = + let address = SetCount state set typ + let oldCount = state.memory.Read reporter address + let trueValue = if isAdd then oldCount else Sub oldCount <| makeNumber 1 + let falseValue = if isAdd then Add oldCount <| makeNumber 1 else oldCount + let iteType = { branches = [(isContains, trueValue)]; elseValue = falseValue } + let newCount = Ite iteType + state.memory.Write reporter address newCount + + let CommonUpdateSet reporter state set item value = + match set.term with + | HeapRef(set, typ) -> + let address = SetKey state set item typ + let contains = state.memory.Read reporter address + state.memory.Write reporter address <| makeBool value + CommonUpdateSetCount reporter state set value contains typ + contains + | _ -> internalfail $"Updating {set}" + + let UpdateSet state set item value = + CommonUpdateSet emptyReporter state set item value + + let AddToSet state set (item : term) = + (!!) <| UpdateSet state set item true + + let RemoveFromSet state set (item : term) = + UpdateSet state set item false + + let CommonUpdateListCount reporter state list (index : term) typ = + let address = ListCount state list typ + let oldCount = state.memory.Read reporter address + let inRange = + let left = (MakeNumber 0) <<= index + let right = index << oldCount + left &&& right + let falseValue = Add oldCount <| MakeNumber 1 + let iteType = { branches = [(inRange, oldCount)]; elseValue = falseValue } + let newCount = Ite iteType + state.memory.Write reporter address newCount + + let CommonWriteListKey reporter state list index item = + match list.term with + | HeapRef(list, typ) -> + let address = ListIndex state list index typ + state.memory.Write reporter address item + CommonUpdateListCount reporter state list index typ + | _ -> internalfail $"Writing at {list} by index" + + let WriteListKey state list index item = + CommonWriteListKey emptyReporter state list index item + let WriteStructFieldUnsafe (reporter : IErrorReporter) state structure field value = reporter.ConfigureState state writeStruct structure field value @@ -830,39 +1069,200 @@ module API = let Merge2Results (r1, s1 : state) (r2, s2 : state) = State.merge2Results (r1, s1) (r2, s2) let FillClassFieldsRegion state (field : fieldId) value = - let defaultValue = MemoryRegion.empty field.typ - let fill region = MemoryRegion.fillRegion value region - state.memory.ClassFields <- PersistentDict.update state.memory.ClassFields field defaultValue fill + let mrKey = MemoryRegionId.createClassFieldsId field + let defaultValue = classFieldsRegion.Empty() field.typ + let fill (region : IMemoryRegion) = + let region = region :?> classFieldsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillStaticsRegion state (field : fieldId) value = - let defaultValue = MemoryRegion.empty field.typ - let fill region = MemoryRegion.fillRegion value region - state.memory.StaticFields <- PersistentDict.update state.memory.StaticFields field defaultValue fill + let mrKey = MemoryRegionId.createStaticFieldsId field + let defaultValue = staticFieldsRegion.Empty() field.typ + let fill (region : IMemoryRegion) = + let region = region :?> staticFieldsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillArrayRegion state arrayType value = - let defaultValue = MemoryRegion.empty arrayType.elemType - let fill region = MemoryRegion.fillRegion value region - state.memory.Arrays <- PersistentDict.update state.memory.Arrays arrayType defaultValue fill + let mrKey = MemoryRegionId.createArraysId arrayType + let defaultValue = arraysRegion.Empty() arrayType.elemType + let fill (region : IMemoryRegion) = + let region = region :?> arraysRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillGeneralDictionaryRegion<'key when 'key : equality> state dictionaryType value = + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let defaultValue = + memoryRegion, productRegion, points<'key>>>.Empty() dictionaryType.valueType + let fill (region : IMemoryRegion) = + let region = region :?> memoryRegion, productRegion, points<'key>>> + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillDictionaryRegion state dictionaryType value = + let fill = + match dictionaryType with + | BoolDictionary _ -> FillGeneralDictionaryRegion + | ByteDictionary _ -> FillGeneralDictionaryRegion + | SByteDictionary _ -> FillGeneralDictionaryRegion + | CharDictionary _ -> FillGeneralDictionaryRegion + | DecimalDictionary _ -> FillGeneralDictionaryRegion + | DoubleDictionary _ -> FillGeneralDictionaryRegion + | IntDictionary _ -> FillGeneralDictionaryRegion + | UIntDictionary _ -> FillGeneralDictionaryRegion + | LongDictionary _ -> FillGeneralDictionaryRegion + | ULongDictionary _ -> FillGeneralDictionaryRegion + | ShortDictionary _ -> FillGeneralDictionaryRegion + | UShortDictionary _ -> FillGeneralDictionaryRegion + | dt -> internalfail $"Fill dictionary region: got {dt.keyType} key" + fill state dictionaryType value + + let FillAddrDictionaryRegion state dictionaryType value = + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let defaultValue = + addrDictionariesRegion.Empty() dictionaryType.valueType + let fill (region : IMemoryRegion) = + let region = region :?> addrDictionariesRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillGeneralDictionaryKeysRegion<'key when 'key : equality> state setType value = + let mrKey = MemoryRegionId.createDictionaryKeysId setType + let defaultValue = + memoryRegion, productRegion, points<'key>>>.Empty() typeof + let fill (region : IMemoryRegion) = + let region = region :?> memoryRegion, productRegion, points<'key>>> + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillDictionaryKeysRegion state dictionaryType value = + let fill = + match dictionaryType with + | BoolDictionary _ -> FillGeneralDictionaryKeysRegion + | ByteDictionary _ -> FillGeneralDictionaryKeysRegion + | SByteDictionary _ -> FillGeneralDictionaryKeysRegion + | CharDictionary _ -> FillGeneralDictionaryKeysRegion + | DecimalDictionary _ -> FillGeneralDictionaryKeysRegion + | DoubleDictionary _ -> FillGeneralDictionaryKeysRegion + | IntDictionary _ -> FillGeneralDictionaryKeysRegion + | UIntDictionary _ -> FillGeneralDictionaryKeysRegion + | LongDictionary _ -> FillGeneralDictionaryKeysRegion + | ULongDictionary _ -> FillGeneralDictionaryKeysRegion + | ShortDictionary _ -> FillGeneralDictionaryKeysRegion + | UShortDictionary _ -> FillGeneralDictionaryKeysRegion + | dt -> internalfail $"Fill dictionary keys region: got {dt.keyType} key" + fill state dictionaryType value + + let FillAddrDictionaryKeysRegion state setType value = + let mrKey = MemoryRegionId.createDictionaryKeysId setType + let defaultValue = + addrSetsRegion.Empty() typeof + let fill (region : IMemoryRegion) = + let region = region :?> addrDictionaryKeysRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillGeneralSetRegion<'key when 'key : equality> state setType value = + let mrKey = MemoryRegionId.createSetsId setType + let defaultValue = + memoryRegion, productRegion, points<'key>>>.Empty() typeof + let fill (region : IMemoryRegion) = + let region = region :?> memoryRegion, productRegion, points<'key>>> + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillSetRegion state setType value = + let fill = + match setType with + | BoolSet _ -> FillGeneralSetRegion + | ByteSet _ -> FillGeneralSetRegion + | SByteSet _ -> FillGeneralSetRegion + | CharSet _ -> FillGeneralSetRegion + | DecimalSet _ -> FillGeneralSetRegion + | DoubleSet _ -> FillGeneralSetRegion + | IntSet _ -> FillGeneralSetRegion + | UIntSet _ -> FillGeneralSetRegion + | LongSet _ -> FillGeneralSetRegion + | ULongSet _ -> FillGeneralSetRegion + | ShortSet _ -> FillGeneralSetRegion + | UShortSet _ -> FillGeneralSetRegion + | st -> internalfail $"Fill set region: got {st.setValueType} item" + fill state setType value + + let FillAddrSetRegion state setType value = + let mrKey = MemoryRegionId.createSetsId setType + let defaultValue = + addrSetsRegion.Empty() typeof + let fill (region : IMemoryRegion) = + let region = region :?> addrSetsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillListRegion state listType value = + let mrKey = MemoryRegionId.createListsId listType + let defaultValue = listsRegion.Empty() listType.listValueType + let fill (region : IMemoryRegion) = + let region = region :?> listsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillLengthRegion state typ value = - let defaultValue = MemoryRegion.empty TypeUtils.lengthType - let fill region = MemoryRegion.fillRegion value region - state.memory.Lengths <- PersistentDict.update state.memory.Lengths typ defaultValue fill + let mrKey = MemoryRegionId.createArrayLengthsId typ + let defaultValue = arrayLengthsRegion.Empty() TypeUtils.lengthType + let fill (region : IMemoryRegion) = + let region = region :?> arrayLengthsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillDictionaryCountRegion state typ value = + let mrKey = MemoryRegionId.createDictionaryCountsId typ + let defaultValue = dictionaryCountsRegion.Empty() TypeUtils.lengthType + let fill (region : IMemoryRegion) = + let region = region :?> dictionaryCountsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillSetCountRegion state typ value = + let mrKey = MemoryRegionId.createSetCountsId typ + let defaultValue = setCountsRegion.Empty() TypeUtils.lengthType + let fill (region : IMemoryRegion) = + let region = region :?> setCountsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill + + let FillListCountRegion state typ value = + let mrKey = MemoryRegionId.createListCountsId typ + let defaultValue = listCountsRegion.Empty() TypeUtils.lengthType + let fill (region : IMemoryRegion) = + let region = region :?> listCountsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillLowerBoundRegion state typ value = - let defaultValue = MemoryRegion.empty TypeUtils.lengthType - let fill region = MemoryRegion.fillRegion value region - state.memory.LowerBounds <- PersistentDict.update state.memory.LowerBounds typ defaultValue fill + let mrKey = MemoryRegionId.createArrayLowerBoundsId typ + let defaultValue = arrayLowerBoundsRegion.Empty() TypeUtils.lengthType + let fill (region : IMemoryRegion) = + let region = region :?> arrayLowerBoundsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillStackBufferRegion state key value = - let defaultValue = MemoryRegion.empty typeof - let fill region = MemoryRegion.fillRegion value region - state.memory.StackBuffers <- PersistentDict.update state.memory.StackBuffers key defaultValue fill + let mrKey = MemoryRegionId.createStackBuffersId key + let defaultValue = stackBuffersRegion.Empty() typeof + let fill (region : IMemoryRegion) = + let region = region :?> stackBuffersRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let FillBoxedRegion state typ value = - let defaultValue = MemoryRegion.empty typ - let fill region = MemoryRegion.fillRegion value region - state.memory.BoxedLocations <- PersistentDict.update state.memory.BoxedLocations typ defaultValue fill + let mrKey = MemoryRegionId.createBoxedLocationsId typ + let defaultValue = boxedLocationsRegion.Empty() typ + let fill (region : IMemoryRegion) = + let region = region :?> boxedLocationsRegion + MemoryRegion.fillRegion value region :> IMemoryRegion + state.memory.MemoryRegions <- PersistentDict.update state.memory.MemoryRegions mrKey defaultValue fill let ObjectToTerm (state : state) (o : obj) (typ : Type) = state.memory.ObjToTerm typ o let TryTermToObject (state : state) term = state.memory.TryTermToObj term diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 2ff9dff61..3ce66b192 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -21,6 +21,7 @@ module API = val BranchExpressions : ((term -> 'a) -> 'b) -> ((term -> 'a) -> 'a) -> ((term -> 'a) -> 'a) -> (term -> 'a) -> 'b val StatedConditionalExecution : (state -> (state -> (term * state -> 'a) -> 'b) -> (state -> ('item -> 'a) -> 'a) -> (state -> ('item -> 'a) -> 'a) -> ('item -> 'item -> 'item list) -> ('item list -> 'a) -> 'b) val StatedConditionalExecutionAppend : (state -> (state -> (term * state -> 'a) -> 'b) -> (state -> ('c list -> 'a) -> 'a) -> (state -> ('c list -> 'a) -> 'a) -> ('c list -> 'a) -> 'b) + val AssumeStatedConditionalExecution : state -> term -> unit val GuardedApplyExpression : term -> (term -> term) -> term val GuardedApplyExpressionWithPC : pathCondition -> term -> (term -> term) -> term @@ -97,6 +98,9 @@ module API = val (|CombinedDelegate|_|) : term -> term list option val (|ConcreteDelegate|_|) : term -> delegateInfo option + val IsTrue : term -> bool + val IsFalse : term -> bool + val (|True|_|) : term -> unit option val (|False|_|) : term -> unit option val (|Negation|_|) : term -> term option @@ -112,6 +116,32 @@ module API = val (|HeapReading|_|) : ISymbolicConstantSource -> option> val (|ArrayRangeReading|_|) : ISymbolicConstantSource -> option val (|ArrayIndexReading|_|) : ISymbolicConstantSource -> option>> + val (|BoolDictionaryReading|_|) : ISymbolicConstantSource -> option * boolDictionariesRegion> + val (|ByteDictionaryReading|_|) : ISymbolicConstantSource -> option * byteDictionariesRegion> + val (|SByteDictionaryReading|_|) : ISymbolicConstantSource -> option * sbyteDictionariesRegion> + val (|CharDictionaryReading|_|) : ISymbolicConstantSource -> option * charDictionariesRegion> + val (|DecimalDictionaryReading|_|) : ISymbolicConstantSource -> option * decimalDictionariesRegion> + val (|DoubleDictionaryReading|_|) : ISymbolicConstantSource -> option * doubleDictionariesRegion> + val (|IntDictionaryReading|_|) : ISymbolicConstantSource -> option * intDictionariesRegion> + val (|UIntDictionaryReading|_|) : ISymbolicConstantSource -> option * uintDictionariesRegion> + val (|LongDictionaryReading|_|) : ISymbolicConstantSource -> option * longDictionariesRegion> + val (|ULongDictionaryReading|_|) : ISymbolicConstantSource -> option * ulongDictionariesRegion> + val (|ShortDictionaryReading|_|) : ISymbolicConstantSource -> option * shortDictionariesRegion> + val (|UShortDictionaryReading|_|) : ISymbolicConstantSource -> option * ushortDictionariesRegion> + val (|AddrDictionaryReading|_|) : ISymbolicConstantSource -> option + val (|BoolSetReading|_|) : ISymbolicConstantSource -> option * boolSetsRegion> + val (|ByteSetReading|_|) : ISymbolicConstantSource -> option * byteSetsRegion> + val (|SByteSetReading|_|) : ISymbolicConstantSource -> option * sbyteSetsRegion> + val (|CharSetReading|_|) : ISymbolicConstantSource -> option * charSetsRegion> + val (|DecimalSetReading|_|) : ISymbolicConstantSource -> option * decimalSetsRegion> + val (|DoubleSetReading|_|) : ISymbolicConstantSource -> option * doubleSetsRegion> + val (|IntSetReading|_|) : ISymbolicConstantSource -> option * intSetsRegion> + val (|UIntSetReading|_|) : ISymbolicConstantSource -> option * uintSetsRegion> + val (|LongSetReading|_|) : ISymbolicConstantSource -> option * longSetsRegion> + val (|ULongSetReading|_|) : ISymbolicConstantSource -> option * ulongSetsRegion> + val (|ShortSetReading|_|) : ISymbolicConstantSource -> option * shortSetsRegion> + val (|UShortSetReading|_|) : ISymbolicConstantSource -> option * ushortSetsRegion> + val (|AddrSetReading|_|) : ISymbolicConstantSource -> option val (|VectorIndexReading|_|) : ISymbolicConstantSource -> option>> val (|StackBufferReading|_|) : ISymbolicConstantSource -> option> val (|StaticsReading|_|) : ISymbolicConstantSource -> option>> @@ -176,6 +206,9 @@ module API = val ArrayTypeToSymbolicType : arrayType -> Type val SymbolicTypeToArrayType : Type -> arrayType + val SymbolicTypeToDictionaryType : Type -> dictionaryType + val SymbolicTypeToSetType : Type -> setType + val TypeIsType : Type -> Type -> term val IsNullable : Type -> bool val TypeIsRef : state -> Type -> term -> term @@ -288,6 +321,19 @@ module API = val ReadStringChar : state -> term -> term -> term val ReadStaticField : state -> Type -> fieldId -> term val ReadDelegate : state -> term -> term option + val ReadDictionaryKey : state -> term -> term -> term + val ContainsKey : state -> term -> term -> term + val GetDictionaryCount : state -> term -> term + val AddToSet : state -> term -> term -> term + val RemoveFromSet : state -> term -> term -> term + val IsSetContains : state -> term -> term -> term + val GetSetCount : state -> term -> term + val ReadListIndex : state -> term -> term -> term + val GetListCount : state -> term -> term + val WriteListKey : state -> term -> term -> term -> unit + val RemoveListAtIndex : state -> term -> term -> unit + val InsertListIndex : state -> term -> term -> term -> unit + val ListCopyToRange : state -> term -> term -> term -> term -> term -> unit val CombineDelegates : state -> term list -> Type -> term val RemoveDelegate : state -> term -> term -> Type -> term @@ -303,6 +349,7 @@ module API = val WriteClassField : state -> term -> fieldId -> term -> unit val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> unit val WriteStaticField : state -> Type -> fieldId -> term -> unit + val WriteDictionaryKey : state -> term -> term -> term -> unit val DefaultOf : Type -> term @@ -373,7 +420,17 @@ module API = val FillClassFieldsRegion : state -> fieldId -> term -> unit val FillStaticsRegion : state -> fieldId -> term -> unit val FillArrayRegion : state -> arrayType -> term -> unit + val FillDictionaryRegion : state -> dictionaryType -> term -> unit + val FillAddrDictionaryRegion : state -> dictionaryType -> term -> unit + val FillDictionaryKeysRegion : state -> dictionaryType -> term -> unit + val FillAddrDictionaryKeysRegion : state -> dictionaryType -> term -> unit + val FillSetRegion : state -> setType -> term -> unit + val FillAddrSetRegion : state -> setType -> term -> unit + val FillListRegion : state -> listType -> term -> unit val FillLengthRegion : state -> arrayType -> term -> unit + val FillDictionaryCountRegion : state -> dictionaryType -> term -> unit + val FillSetCountRegion : state -> setType -> term -> unit + val FillListCountRegion : state -> listType -> term -> unit val FillLowerBoundRegion : state -> arrayType -> term -> unit val FillStackBufferRegion : state -> stackKey -> term -> unit val FillBoxedRegion : state -> Type -> term -> unit diff --git a/VSharp.SILI.Core/Branching.fs b/VSharp.SILI.Core/Branching.fs index 2837370ab..2d31f476b 100644 --- a/VSharp.SILI.Core/Branching.fs +++ b/VSharp.SILI.Core/Branching.fs @@ -115,3 +115,20 @@ module internal Branching = commonStatedConditionalExecutionk state conditionInvocation thenBranch elseBranch State.merge2Results k let statedConditionalExecutionWithMerge state conditionInvocation thenBranch elseBranch = statedConditionalExecutionWithMergek state conditionInvocation thenBranch elseBranch id + + let assumeStatedConditionalExecution (state : state) assume = + assert(isBool assume) + let pc = state.pc + assert(PC.toSeq pc |> conjunction |> state.model.Eval |> isTrue) + let assumePc = PC.add pc assume + state.AddConstraint assume + let typeStorage = state.typeStorage + TypeStorage.addTypeConstraint typeStorage.Constraints assume + if state.model.Eval assume |> isFalse then + match checkSat state with + | SolverInteraction.SmtUnsat _ + | SolverInteraction.SmtUnknown _ -> + internalfail "assumeStatedConditionalExecution: fail" + | SolverInteraction.SmtSat model -> + state.model <- model.mdl + assert(PC.toSeq assumePc |> conjunction |> state.model.Eval |> isTrue) diff --git a/VSharp.SILI.Core/ConcreteMemory.fs b/VSharp.SILI.Core/ConcreteMemory.fs index 74ed514a7..e1b85b4bb 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fs +++ b/VSharp.SILI.Core/ConcreteMemory.fs @@ -1,19 +1,24 @@ namespace VSharp.Core open System +open System.Collections open System.Collections.Generic open System.Runtime.CompilerServices +open FSharpx.Collections open VSharp open VSharp.Utils +open VSharp.TypeUtils type private ChildKind = | Field of fieldId | Index of int[] * Type + | Key of collectionKey * Type with member x.Type with get() = match x with | Field f -> f.typ - | Index(_, t) -> t + | Index(_, t) + | Key(_, t) -> t type private ChildLocation = { childKind : ChildKind; structFields : fieldId list } @@ -329,12 +334,71 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c else string[index] :> obj | obj -> internalfail $"reading array index from concrete memory: expected to read array, but got {obj}" + member internal x.ReadDictionaryKey address (key : collectionKey) = + match x.ReadObject address with + | :? IDictionary as dict -> + let valueType = dict.GetType().GetGenericArguments()[1] + let k = collectionKeyValueToObj key + let value = dict[k] + if Reflection.isReferenceOrContainsReferences valueType then + x.TrackChild(address, value, Key(key, valueType)) + value + | obj -> internalfail $"reading dictionary key from concrete memory: expected to read dictionary, but got {obj}" + + member internal x.DictionaryHasKey address (key : collectionKey) = + match x.ReadObject address with + | :? IDictionary as dict -> + let k = collectionKeyValueToObj key + dict.Contains(k) + | obj -> internalfail $"contains dictionary key from concrete memory: expected to read dictionary, but got {obj}" + + member internal x.ReadSetKey address (item : collectionKey) = + match x.ReadObject address with + | Set set -> + let valueType = set.GetType().GetGenericArguments()[0] + let i = collectionKeyValueToObj item + let method = set.GetType().GetMethod("Contains") + let contains = method.Invoke(set, [| i |]) + if Reflection.isReferenceOrContainsReferences valueType then + x.TrackChild(address, contains, Key(item, valueType)) + contains :?> bool + | obj -> internalfail $"reading set from concrete memory: expected to read set, but got {obj}" + + member internal x.ReadListIndex address index = + match x.ReadObject address with + | :? IList as list -> + let valueType = list.GetType().GetGenericArguments()[0] + let value = list[index] + if Reflection.isReferenceOrContainsReferences valueType then + x.TrackChild(address, value, Index([| index |], valueType)) + value + | obj -> internalfail $"reading list index from concrete memory: expected to read list, but got {obj}" + member internal x.GetAllArrayData address = match x.ReadObject address with | :? Array as array -> Array.getArrayIndicesWithValues array | :? String as string -> string.ToCharArray() |> Array.getArrayIndicesWithValues | obj -> internalfail $"reading array data concrete memory: expected to read array, but got {obj}" + member internal x.GetAllDictionaryData address = + match x.ReadObject address with + | :? IDictionary as dict -> + Reflection.keyAndValueSeqFromDictionaryObj dict + | obj -> internalfail $"reading dictionary data concrete memory: expected to read dictionary, but got {obj}" + + member internal x.GetAllSetData address = + match x.ReadObject address with + | Set obj -> + let set = obj :?> IEnumerable + seq { for obj in set -> obj } + | obj -> internalfail $"reading set data concrete memory: expected to read set, but got {obj}" + + member internal x.GetAllListData address = + match x.ReadObject address with + | :? IList as list -> + seq { for obj in list -> obj } + | obj -> internalfail $"reading list data concrete memory: expected to read list, but got {obj}" + member internal x.ReadArrayLowerBound address dimension = match x.ReadObject address with | :? Array as array -> array.GetLowerBound(dimension) @@ -347,6 +411,21 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c | :? String as string when dimension = 0 -> 1 + string.Length | obj -> internalfail $"reading array length from concrete memory: expected to read array, but got {obj}" + member internal x.ReadDictionaryCount address = + match x.ReadObject address with + | dict when dict.GetType().Name = "Dictionary`2" -> Reflection.getCountByReflection dict + | obj -> internalfail $"reading dictionary length from concrete memory: expected to read dictionary, but got {obj}" + + member internal x.ReadSetCount address = + match x.ReadObject address with + | Set set -> Reflection.getCountByReflection set + | obj -> internalfail $"reading set length from concrete memory: expected to read set, but got {obj}" + + member internal x.ReadListCount address = + match x.ReadObject address with + | List list -> Reflection.getCountByReflection list + | obj -> internalfail $"reading list length from concrete memory: expected to read list, but got {obj}" + member internal x.ReadBoxedLocation address = let obj = x.ReadObject address assert(obj :? ValueType) @@ -389,6 +468,73 @@ type public ConcreteMemory private (physToVirt, virtToPhys, children, parents, c x.WriteObject address newString | obj -> internalfail $"writing array index to concrete memory: expected to read array, but got {obj}" + member internal x.WriteDictionaryKey address (key : collectionKey) value = + match x.ReadObject address with + | :? IDictionary as dict -> + let valueType = dict.GetType().GetGenericArguments()[1] + let castedValue = + if value <> null then x.CastIfNeed value valueType + else value + let objKey = collectionKeyValueToObj key + dict[objKey] <- castedValue + if Reflection.isReferenceOrContainsReferences valueType then + x.SetChild(dict, value, Key(key, valueType)) + | obj -> internalfail $"writing dictionary key to concrete memory: expected to read dictionary, but got {obj}" + member internal x.WriteSetKey address (item : collectionKey) (value : obj) = + ignore <| + match x.ReadObject address with + | Set set -> + let itemType = set.GetType().GetGenericArguments()[0] + let i = collectionKeyValueToObj item + let i = + if i <> null then x.CastIfNeed i itemType + else i + let methodName = if (value :?> bool) then "Add" else "Remove" + let method = set.GetType().GetMethod(methodName) + let contains = method.Invoke(set, [| i |]) + if Reflection.isReferenceOrContainsReferences itemType then + x.TrackChild(address, contains, Key(item, itemType)) + contains :?> bool + | obj -> internalfail $"writing set key to concrete memory: expected to read set, but got {obj}" + + member internal x.WriteListIndex address (index : int) item = + match x.ReadObject address with + | List list -> + let itemType = list.GetType().GetGenericArguments()[0] + let castedValue = + if item <> null then x.CastIfNeed item itemType + else item + let list = list :?> IList + let count = list.Count + if index < count then list[index] <- castedValue + else ignore <| list.Add(castedValue) + if Reflection.isReferenceOrContainsReferences itemType then + x.SetChild(dict, item, Index([| index |], itemType)) + | obj -> internalfail $"writing list index to concrete memory: expected to read list, but got {obj}" + + member internal x.ListRemoveAt address (index : int) = + match x.ReadObject address with + | :? IList as list -> list.RemoveAt(index) + | obj -> internalfail $"remove from list in concrete memory: expected to read list, but got {obj}" + + member internal x.InsertIndex address (index : int) (item : obj) = + match x.ReadObject address with + | :? IList as list -> + let itemType = list.GetType().GetGenericArguments()[0] + let castedValue = + if item <> null then x.CastIfNeed item itemType + else item + list.Insert(index, castedValue) + | obj -> internalfail $"insert in list in concrete memory: expected to read list, but got {obj}" + + member internal x.ListCopyToRange list (index : int) array (arrayIndex : int) (count : int) = + match x.ReadObject list, x.ReadObject array with + | List list, (:? Array as array) -> + let argty = [| typeof; array.GetType(); typeof; typeof |] + let method = list.GetType().GetMethod("CopyTo", argty) + ignore <| method.Invoke(list, [| index; array; arrayIndex; count |]) + | list, array -> internalfail $"list copyToRange in concrete memory: got {list}, {array}" + member internal x.WriteBoxedLocation (address : concreteHeapAddress) (obj : obj) : unit = let phys = virtToPhys[address] let oldObj = phys.object diff --git a/VSharp.SILI.Core/ConcreteMemory.fsi b/VSharp.SILI.Core/ConcreteMemory.fsi index 23d6997e6..708355c18 100644 --- a/VSharp.SILI.Core/ConcreteMemory.fsi +++ b/VSharp.SILI.Core/ConcreteMemory.fsi @@ -18,13 +18,29 @@ type public ConcreteMemory = member internal AllocateBoxedLocation : concreteHeapAddress -> obj -> Type -> unit member internal ReadClassField : concreteHeapAddress -> fieldId -> obj member internal ReadArrayIndex : concreteHeapAddress -> int list -> obj + member internal ReadDictionaryKey : concreteHeapAddress -> collectionKey -> obj + member internal DictionaryHasKey : concreteHeapAddress -> collectionKey -> bool + member internal ReadSetKey : concreteHeapAddress -> collectionKey -> bool + member internal ReadListIndex : concreteHeapAddress -> int -> obj member internal GetAllArrayData : concreteHeapAddress -> seq + member internal GetAllDictionaryData : concreteHeapAddress -> seq + member internal GetAllSetData : concreteHeapAddress -> seq + member internal GetAllListData : concreteHeapAddress -> seq member internal ReadArrayLowerBound : concreteHeapAddress -> int -> int member internal ReadArrayLength : concreteHeapAddress -> int -> int + member internal ReadDictionaryCount : concreteHeapAddress -> int + member internal ReadSetCount : concreteHeapAddress -> int + member internal ReadListCount : concreteHeapAddress -> int member internal ReadBoxedLocation : concreteHeapAddress -> ValueType member internal ReadDelegate : concreteHeapAddress -> Delegate member internal WriteClassField : concreteHeapAddress -> fieldId -> obj -> unit member internal WriteArrayIndex : concreteHeapAddress -> int list -> obj -> unit + member internal WriteDictionaryKey : concreteHeapAddress -> collectionKey -> obj -> unit + member internal WriteSetKey : concreteHeapAddress -> collectionKey -> obj -> unit + member internal WriteListIndex : concreteHeapAddress -> int -> obj -> unit + member internal ListRemoveAt : concreteHeapAddress -> int -> unit + member internal InsertIndex : concreteHeapAddress -> int -> obj -> unit + member internal ListCopyToRange : concreteHeapAddress -> int -> concreteHeapAddress -> int -> int -> unit member internal WriteBoxedLocation : concreteHeapAddress -> obj -> unit member internal InitializeArray : concreteHeapAddress -> RuntimeFieldHandle -> unit member internal FillArray : concreteHeapAddress -> int -> int -> obj -> unit diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index d2a561367..399cb8ed3 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/VSharp.SILI.Core/Memory.fs @@ -1,6 +1,7 @@ namespace VSharp.Core open System +open System.Collections open System.Collections.Generic open System.Reflection open FSharpx.Collections @@ -8,6 +9,8 @@ open VSharp open VSharp.Core open VSharp.TypeUtils open VSharp.Utils +open DictionaryType +open SetType #nowarn "69" @@ -130,6 +133,8 @@ module internal Memory = override x.Time = x.time override x.TypeOfLocation = x.key.TypeOfLocation + // -------------------------------- Reading -------------------------------- + [] type private heapReading<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = {picker : regionPicker<'key, 'reg>; key : 'key; memoryObject : memoryRegion<'key, 'reg>; time : vectorTime} @@ -151,6 +156,14 @@ module internal Memory = override x.Time = x.time override x.TypeOfLocation = x.picker.sort.TypeOfLocation + type private generalDictionaryReading<'key when 'key : equality> = heapReading, productRegion> + type private addrDictionaryReading = heapReading> + type private dictionaryCountReading = heapReading + + type private generalSetReading<'key when 'key : equality> = heapReading, productRegion> + type private addrSetReading = heapReading> + type private setCountReading = heapReading + let (|HeapReading|_|) (src : ISymbolicConstantSource) = match src with | :? heapReading as hr -> Some(hr.key, hr.memoryObject) @@ -163,6 +176,136 @@ module internal Memory = | :? arrayReading as ar -> Some(isConcreteHeapAddress ar.key.Address, ar.key, ar.memoryObject) | _ -> None + let (|BoolDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|ByteDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|SByteDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|CharDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|DecimalDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|DoubleDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|IntDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|UIntDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|LongDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|ULongDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|ShortDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|UShortDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|AddrDictionaryReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? addrDictionaryReading as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject) + | _ -> None + + let (|BoolSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|ByteSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|SByteSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|CharSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|DecimalSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|DoubleSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|IntSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|UIntSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|LongSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|ULongSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|ShortSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|UShortSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? generalSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + + let (|AddrSetReading|_|) (src : ISymbolicConstantSource) = + match src with + | :? addrSetReading as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject) + | _ -> None + let (|ArrayRangeReading|_|) (src : ISymbolicConstantSource) = match src with | :? arrayReading as { memoryObject = mo; key = RangeArrayIndexKey(address, fromIndices, toIndices); picker = picker; time = time } -> @@ -192,13 +335,39 @@ module internal Memory = let getHeapReadingRegionSort (src : ISymbolicConstantSource) = match src with - | :? heapReading as hr -> hr.picker.sort + | :? heapReading as hr -> hr.picker.sort | :? heapReading> as hr -> hr.picker.sort - | :? heapReading as hr -> hr.picker.sort - | :? heapReading> as hr -> hr.picker.sort + | :? heapReading as hr -> hr.picker.sort + | :? heapReading> as hr -> hr.picker.sort | :? heapReading> -> internalfail "unexpected array index reading via 'heapReading' source" | :? arrayReading as ar -> ar.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? generalDictionaryReading as dr -> dr.picker.sort + | :? addrDictionaryReading as dr -> dr.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? generalSetReading as st -> st.picker.sort + | :? addrSetReading as st -> st.picker.sort | _ -> __unreachable__() let composeBaseSource state (baseSource : ISymbolicConstantSource) = @@ -290,11 +459,6 @@ module internal Memory = Constant name source typ | _ -> constant - let private accessRegion (dict : pdict<'a, memoryRegion<'key, 'reg>>) key typ = - match PersistentDict.tryFind dict key with - | Some value -> value - | None -> MemoryRegion.empty typ - let private isHeapAddressDefault state address = state.complete || match address.term with @@ -325,7 +489,7 @@ module internal Memory = let writeStruct structTerm field value = commonWriteStruct None structTerm field value let guardedWriteStruct guard structTerm field value = commonWriteStruct guard structTerm field value - + let isSafeContextWrite actualType neededType = assert(neededType <> typeof) neededType = actualType @@ -349,13 +513,7 @@ module internal Memory = type Memory private ( evaluationStack : evaluationStack, stack : callStack, // Arguments and local variables - stackBuffers : pdict, // Buffers allocated via stackAlloc - classFields : pdict, // Fields of classes in heap - arrays : pdict, // Contents of arrays in heap - lengths : pdict, // Lengths by dimensions of arrays in heap - lowerBounds : pdict, // Lower bounds by dimensions of arrays in heap - staticFields : pdict, // Static fields of types without type variables - boxedLocations : pdict, // Value types boxed in heap + memoryRegions : pdict, concreteMemory : ConcreteMemory, // Fully concrete objects allocatedTypes : pdict, // Types of heap locations allocated via new initializedAddresses : pset, // Addresses, which invariants were initialized @@ -369,14 +527,8 @@ module internal Memory = let mutable stack = stack let mutable evaluationStack = evaluationStack let mutable allocatedTypes = allocatedTypes - let mutable arrays = arrays - let mutable lowerBounds = lowerBounds - let mutable lengths = lengths let mutable initializedAddresses = initializedAddresses - let mutable classFields = classFields - let mutable staticFields = staticFields - let mutable stackBuffers = stackBuffers - let mutable boxedLocations = boxedLocations + let mutable memoryRegions = memoryRegions let mutable delegates = delegates let mutable memoryMode = memoryMode @@ -397,6 +549,13 @@ module internal Memory = allocatedTypes <- PersistentDict.add concreteAddress symbolicType allocatedTypes concreteAddress + let getOrPutRegionCommon (key : IMemoryRegionId) typ memory = + match PersistentDict.tryFind memory key with + | Some value -> value + | None -> key.Empty typ + + let getOrPutRegion key typ = getOrPutRegionCommon key typ memoryRegions + // ---------------- Try term to object ---------------- let tryAddressToObj fullyConcrete address = @@ -428,40 +587,175 @@ module internal Memory = let writeLowerBoundSymbolic guard address dimension arrayType value = ensureConcreteType arrayType.elemType - let mr = accessRegion lowerBounds arrayType lengthType + let mrKey = MemoryRegionId.createArrayLowerBoundsId arrayType + let mr = getOrPutRegion mrKey lengthType :?> arrayLowerBoundsRegion let key = {address = address; index = dimension} let mr' = MemoryRegion.write mr guard key value - lowerBounds <- PersistentDict.add arrayType mr' lowerBounds + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeLengthSymbolic guard address dimension arrayType value = ensureConcreteType arrayType.elemType - let mr = accessRegion lengths arrayType lengthType + let mrKey = MemoryRegionId.createArrayLengthsId arrayType + let mr = getOrPutRegion mrKey lengthType :?> arrayLengthsRegion let key = {address = address; index = dimension} let mr' = MemoryRegion.write mr guard key value - lengths <- PersistentDict.add arrayType mr' lengths + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeDictionaryCount guard address dictionaryType value = + ensureConcreteType dictionaryType.keyType + let mrKey = MemoryRegionId.createDictionaryCountsId dictionaryType + let mr = getOrPutRegion mrKey lengthType :?> dictionaryCountsRegion + let key = { address = address } + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeSetCount guard address setType value = + ensureConcreteType setType.setValueType + let mrKey = MemoryRegionId.createSetCountsId setType + let mr = getOrPutRegion mrKey lengthType :?> setCountsRegion + let key = { address = address } + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeListCount guard address listType value = + ensureConcreteType listType.listValueType + let mrKey = MemoryRegionId.createListCountsId listType + let mr = getOrPutRegion mrKey lengthType :?> listCountsRegion + let key = { address = address } + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeArrayKeySymbolic guard key arrayType value = let elementType = arrayType.elemType ensureConcreteType elementType - let mr = accessRegion arrays arrayType elementType + let mrKey = MemoryRegionId.createArraysId arrayType + let mr = getOrPutRegion mrKey elementType :?> arraysRegion let mr' = MemoryRegion.write mr guard key value - let newArrays = PersistentDict.add arrayType mr' arrays - arrays <- newArrays + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeArrayIndexSymbolic guard address indices arrayType value = let indices = List.map (fun i -> primitiveCast i typeof) indices let key = OneArrayIndexKey(address, indices) writeArrayKeySymbolic guard key arrayType value + let writeGeneralDictionaryKeyToKeysSymbolic (key : heapCollectionKey<'key>) guard dictionaryType value = + let mrKey = MemoryRegionId.createDictionaryKeysId dictionaryType + let mr = getOrPutRegion mrKey typeof :?> dictionariesRegion<'key> + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeGeneralDictionaryKeySymbolic (key : heapCollectionKey<'key>) guard dictionaryType value valueType = + writeGeneralDictionaryKeyToKeysSymbolic key guard dictionaryType <| True() + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let mr = getOrPutRegion mrKey valueType :?> dictionariesRegion<'key> + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeAddrDictionaryKeyToKeysSymbolic key guard dictionaryType value = + let mrKey = MemoryRegionId.createDictionaryKeysId dictionaryType + let mr = getOrPutRegion mrKey typeof :?> addrDictionaryKeysRegion + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeAddrDictionaryKeySymbolic key guard dictionaryType value valueType = + writeAddrDictionaryKeyToKeysSymbolic key guard dictionaryType <| True() + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let mr = getOrPutRegion mrKey valueType :?> addrDictionariesRegion + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeDictionaryKeySymbolic guard address key (dictionaryType : dictionaryType) value = + let valueType = dictionaryType.valueType + ensureConcreteType valueType + let write = + match dictionaryType with + | BoolDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ByteDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | SByteDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | CharDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | DecimalDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | DoubleDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | IntDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | UIntDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | LongDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ULongDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ShortDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | UShortDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey) + | AddrDictionary _ -> writeAddrDictionaryKeySymbolic <| ({ address = address; key = key } : addrCollectionKey) + | _ -> __unreachable__() + write guard dictionaryType value valueType + + let writeDictionaryKeyToKeysSymbolic guard address key (dictionaryType : dictionaryType) value = + let valueType = dictionaryType.valueType + ensureConcreteType valueType + let write = + match dictionaryType with + | BoolDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ByteDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | SByteDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | CharDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | DecimalDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | DoubleDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | IntDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | UIntDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | LongDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ULongDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | ShortDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | UShortDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey) + | AddrDictionary _ -> writeAddrDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : addrCollectionKey) + | _ -> __unreachable__() + write guard dictionaryType value + + let writeGeneralSetKeySymbolic (key : heapCollectionKey<'key>) guard setType value = + let mrKey = MemoryRegionId.createSetsId setType + let mr = getOrPutRegion mrKey typeof :?> setsRegion<'key> + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeAddrSetKeySymbolic key guard setType value = + let mrKey = MemoryRegionId.createSetsId setType + let mr = getOrPutRegion mrKey typeof :?> addrSetsRegion + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + + let writeSetKeySymbolic guard address item (setType : setType) value = + let itemType = setType.setValueType + ensureConcreteType itemType + let write = + match setType with + | BoolSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | ByteSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | SByteSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | CharSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | DecimalSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | DoubleSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | IntSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | UIntSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | LongSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | ULongSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | ShortSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | UShortSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey) + | AddrSet _ -> writeAddrSetKeySymbolic <| ({ address = address; key = item } : addrCollectionKey) + | _ -> __unreachable__() + write guard setType value + + let writeListIndexSymbolic guard address index (listType : listType) value = + let key = OneArrayIndexKey(address, [index]) + let mrKey = MemoryRegionId.createListsId listType + let mr = getOrPutRegion mrKey listType.listValueType :?> listsRegion + let mr' = MemoryRegion.write mr guard key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + let writeStackLocation key value = stack <- CallStack.writeStackLocation stack key value let writeClassFieldSymbolic guard address (field : fieldId) value = ensureConcreteType field.typ - let mr = accessRegion classFields field field.typ + let mrKey = MemoryRegionId.createClassFieldsId field + let mr = getOrPutRegion mrKey field.typ :?> classFieldsRegion let key = {address = address} let mr' = MemoryRegion.write mr guard key value - classFields <- PersistentDict.add field mr' classFields + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeArrayRangeSymbolic guard address fromIndices toIndices arrayType value = let fromIndices = List.map (fun i -> primitiveCast i typeof) fromIndices @@ -469,6 +763,13 @@ module internal Memory = let key = RangeArrayIndexKey(address, fromIndices, toIndices) writeArrayKeySymbolic guard key arrayType value + let writeListRangeSymbolic address fromIdx toIdx listType value = + let key = RangeArrayIndexKey(address, [fromIdx], [toIdx]) + let mrKey = MemoryRegionId.createListsId listType + let mr = getOrPutRegion mrKey listType.listValueType :?> listsRegion + let mr' = MemoryRegion.write mr None key value + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions + let fillArrayBoundsSymbolic guard address lengths lowerBounds arrayType = let d = List.length lengths assert(d = arrayType.dimension) @@ -479,17 +780,19 @@ module internal Memory = List.iter2 writeLowerBounds lowerBounds [0 .. d-1] let writeStackBuffer stackKey guard index value = - let mr = accessRegion stackBuffers stackKey typeof + let mrKey = MemoryRegionId.createStackBuffersId stackKey + let mr = getOrPutRegion mrKey typeof :?> stackBuffersRegion let key : stackBufferIndexKey = {index = index} let mr' = MemoryRegion.write mr guard key value - stackBuffers <- PersistentDict.add stackKey mr' stackBuffers + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeBoxedLocationSymbolic guard (address : term) value typ = ensureConcreteType typ - let mr = accessRegion boxedLocations typ typ + let mrKey = MemoryRegionId.createBoxedLocationsId typ + let mr = getOrPutRegion mrKey typ :?> boxedLocationsRegion let key = {address = address} let mr' = MemoryRegion.write mr guard key value - boxedLocations <- PersistentDict.add typ mr' boxedLocations + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let writeAddressUnsafe (reporter : IErrorReporter) address startByte value = let addressSize = sizeOf address @@ -567,12 +870,6 @@ module internal Memory = EvaluationStack.empty, CallStack.empty, PersistentDict.empty, - PersistentDict.empty, - PersistentDict.empty, - PersistentDict.empty, - PersistentDict.empty, - PersistentDict.empty, - PersistentDict.empty, ConcreteMemory(), PersistentDict.empty, PersistentSet.empty, @@ -698,6 +995,27 @@ module internal Memory = let source : arrayReading = {picker = picker; key = key; memoryObject = memoryObject; time = time} let name = picker.mkName key self.MakeSymbolicValue source name typ + + member self.MakeGeneralDictionarySymbolicHeapRead<'key when 'key : equality> picker (key : heapCollectionKey<'key>) time typ memoryObject = + let source : generalDictionaryReading<'key> = {picker = picker; key = key; memoryObject = memoryObject; time = time} + let name = picker.mkName key + self.MakeSymbolicValue source name typ + + member self.MakeAddrDictionarySymbolicHeapRead picker (key : addrCollectionKey) time typ memoryObject = + let source : addrDictionaryReading = {picker = picker; key = key; memoryObject = memoryObject; time = time} + let name = picker.mkName key + self.MakeSymbolicValue source name typ + + member self.MakeGeneralSetSymbolicHeapRead<'key when 'key : equality> picker (key : heapCollectionKey<'key>) time typ memoryObject = + let source : generalSetReading<'key> = {picker = picker; key = key; memoryObject = memoryObject; time = time} + let name = picker.mkName key + self.MakeSymbolicValue source name typ + + member self.MakeAddrSetSymbolicHeapRead picker (key : addrCollectionKey) time typ memoryObject = + let source : addrSetReading = {picker = picker; key = key; memoryObject = memoryObject; time = time} + let name = picker.mkName key + self.MakeSymbolicValue source name typ + member self.RangeReadingUnreachable _ _ = __unreachable__() member self.SpecializedReading (readKey : heapArrayKey) utKey = match utKey with @@ -711,7 +1029,8 @@ module internal Memory = member private self.ReadLowerBoundSymbolic address dimension arrayType = let extractor (state : state) = - accessRegion state.memory.LowerBounds (state.SubstituteTypeVariablesIntoArrayType arrayType) lengthType + let mrKey = MemoryRegionId.createArrayLowerBoundsId <| state.SubstituteTypeVariablesIntoArrayType arrayType + getOrPutRegionCommon mrKey lengthType state.memory.MemoryRegions :?> arrayLowerBoundsRegion let mkName (key : heapVectorIndexKey) = $"LowerBound({key.address}, {key.index})" let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address || arrayType.isVector let key = {address = address; index = dimension} @@ -727,7 +1046,8 @@ module internal Memory = member private self.ReadLengthSymbolic address dimension arrayType = let extractor (state : state) = - accessRegion state.memory.Lengths (state.SubstituteTypeVariablesIntoArrayType arrayType) lengthType + let mrKey = MemoryRegionId.createArrayLengthsId <| state.SubstituteTypeVariablesIntoArrayType arrayType + getOrPutRegionCommon mrKey lengthType state.memory.MemoryRegions :?> arrayLengthsRegion let mkName (key : heapVectorIndexKey) = $"Length({key.address}, {key.index})" let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address let key = {address = address; index = dimension} @@ -741,6 +1061,57 @@ module internal Memory = self.MakeSymbolicHeapRead picker key state.startingTime typ memoryRegion MemoryRegion.read (extractor state) key (isDefault state) inst self.RangeReadingUnreachable + member private self.ReadDictionaryCountSymbolic address dictionaryType = + let extractor (state : state) = + let mrKey = MemoryRegionId.createDictionaryCountsId <| state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + getOrPutRegionCommon mrKey lengthType state.memory.MemoryRegions :?> dictionaryCountsRegion + let mkName (key : heapAddressKey) = $"Count({key.address})" + let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address + let key = { address = address } + let inst typ memoryRegion = + let sort = DictionaryCountSort dictionaryType + let picker = + { + sort = sort; extract = extractor; mkName = mkName + isDefaultKey = isDefault; isDefaultRegion = false + } + self.MakeSymbolicHeapRead picker key state.startingTime typ memoryRegion + MemoryRegion.read (extractor state) key (isDefault state) inst self.RangeReadingUnreachable + + member private self.ReadSetCountSymbolic address setType = + let extractor (state : state) = + let mrKey = MemoryRegionId.createSetCountsId <| state.SubstituteTypeVariablesIntoSetType setType + getOrPutRegionCommon mrKey lengthType state.memory.MemoryRegions :?> setCountsRegion + let mkName (key : heapAddressKey) = $"Count({key.address})" + let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address + let key = { address = address } + let inst typ memoryRegion = + let sort = SetCountSort setType + let picker = + { + sort = sort; extract = extractor; mkName = mkName + isDefaultKey = isDefault; isDefaultRegion = false + } + self.MakeSymbolicHeapRead picker key state.startingTime typ memoryRegion + MemoryRegion.read (extractor state) key (isDefault state) inst self.RangeReadingUnreachable + + member private self.ReadListCountSymbolic address listType = + let extractor (state : state) = + let mrKey = MemoryRegionId.createListCountsId <| state.SubstituteTypeVariablesIntoListType listType + getOrPutRegionCommon mrKey lengthType state.memory.MemoryRegions :?> listCountsRegion + let mkName (key : heapAddressKey) = $"Count({key.address})" + let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address + let key = { address = address } + let inst typ memoryRegion = + let sort = ListCountSort listType + let picker = + { + sort = sort; extract = extractor; mkName = mkName + isDefaultKey = isDefault; isDefaultRegion = false + } + self.MakeSymbolicHeapRead picker key state.startingTime typ memoryRegion + MemoryRegion.read (extractor state) key (isDefault state) inst self.RangeReadingUnreachable + member private self.ReadArrayRegion arrayType extractor region (isDefaultRegion : bool) (key : heapArrayKey) = let isDefault state (key : heapArrayKey) = isHeapAddressDefault state key.Address let instantiate typ memory = @@ -756,12 +1127,244 @@ module internal Memory = self.MakeArraySymbolicHeapRead picker key time typ memory MemoryRegion.read region key (isDefault state) instantiate self.SpecializedReading + member private self.ReadListRegion listType extractor region (isDefaultRegion : bool) (key : heapArrayKey) = + let isDefault state (key : heapArrayKey) = isHeapAddressDefault state key.Address + let instantiate typ memory = + let sort = ListIndexSort listType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeArraySymbolicHeapRead picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.SpecializedReading + + member private self.ReadGeneralDictionaryRegion<'key when 'key : equality> dictionaryType extractor region (isDefaultRegion : bool) (key : heapCollectionKey<'key>) = + let isDefault state (key : heapCollectionKey<'key>) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = DictionaryKeySort dictionaryType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeGeneralDictionarySymbolicHeapRead<'key> picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + + member private self.ReadAddrDictionaryRegion dictionaryType extractor region (isDefaultRegion : bool) (key : addrCollectionKey) = + let isDefault state (key : addrCollectionKey) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = AddrDictionaryKeySort dictionaryType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeAddrDictionarySymbolicHeapRead picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + + member private self.HasGeneralDictionaryRegion<'key when 'key : equality> dictionaryType extractor region (isDefaultRegion : bool) (key : heapCollectionKey<'key>) = + let isDefault state (key : heapCollectionKey<'key>) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = DictionaryHasKeySort dictionaryType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeGeneralSetSymbolicHeapRead<'key> picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + + member private self.HasAddrDictionaryRegion dictionaryType extractor region (isDefaultRegion : bool) (key : addrCollectionKey) = + let isDefault state (key : addrCollectionKey) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = AddrDictionaryHasKeySort dictionaryType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeAddrSetSymbolicHeapRead picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + + member private self.ReadGeneralSetRegion<'key when 'key : equality> setType extractor region (isDefaultRegion : bool) (key : heapCollectionKey<'key>) = + let isDefault state (key : heapCollectionKey<'key>) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = SetKeySort setType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeGeneralSetSymbolicHeapRead<'key> picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + + member private self.ReadAddrSetRegion setType extractor region (isDefaultRegion : bool) (key : addrCollectionKey) = + let isDefault state (key : addrCollectionKey) = isHeapAddressDefault state key.address + let instantiate typ memory = + let sort = AddrSetKeySort setType + let picker = + { + sort = sort; extract = extractor; mkName = toString + isDefaultKey = isDefault; isDefaultRegion = isDefaultRegion + } + let time = + if isValueType typ then state.startingTime + else MemoryRegion.maxTime region.updates state.startingTime + self.MakeAddrSetSymbolicHeapRead picker key time typ memory + MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable + member private self.ReadArrayKeySymbolic key arrayType = let extractor (state : state) = let arrayType = state.SubstituteTypeVariablesIntoArrayType arrayType - accessRegion state.memory.Arrays arrayType arrayType.elemType + let mrKey = MemoryRegionId.createArraysId arrayType + getOrPutRegionCommon mrKey arrayType.elemType state.memory.MemoryRegions :?> arraysRegion self.ReadArrayRegion arrayType extractor (extractor state) false key + + member private self.ReadListRangeSymbolic address fromIdx toIdx listType = + let key = RangeArrayIndexKey(address, [fromIdx], [toIdx]) + let extractor (state : state) = + let listType = state.SubstituteTypeVariablesIntoListType listType + let mrKey = MemoryRegionId.createListsId listType + getOrPutRegionCommon mrKey listType.listValueType state.memory.MemoryRegions :?> listsRegion + self.ReadListRegion listType extractor (extractor state) false key + + member private self.ReadListIndexSymbolic address index listType = + let key = OneArrayIndexKey(address, [index]) + let extractor (state : state) = + let listType = state.SubstituteTypeVariablesIntoListType listType + let mrKey = MemoryRegionId.createListsId listType + getOrPutRegionCommon mrKey listType.listValueType state.memory.MemoryRegions + :?> listsRegion + self.ReadListRegion listType extractor (extractor state) false key + + member private self.ReadGeneralDictionaryKeySymbolic<'key when 'key : equality> address key dictionaryType = + let key : heapCollectionKey<'key> = { address = address; key = key } + let extractor (state : state) = + let dictionaryType = state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + getOrPutRegionCommon mrKey dictionaryType.valueType state.memory.MemoryRegions + :?> memoryRegion, productRegion> + self.ReadGeneralDictionaryRegion<'key> dictionaryType extractor (extractor state) false key + + member private self.ReadAddrDictionaryKeySymbolic address key dictionaryType = + let key : addrCollectionKey = { address = address; key = key } + let extractor (state : state) = + let dictionaryType = state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + getOrPutRegionCommon mrKey dictionaryType.valueType state.memory.MemoryRegions :?> addrDictionariesRegion + self.ReadAddrDictionaryRegion dictionaryType extractor (extractor state) false key + + member private self.ReadDictionaryKeySymbolic address key dictionaryType = + let read = + match dictionaryType with + | BoolDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | ByteDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | SByteDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | CharDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | DecimalDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | DoubleDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | IntDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | UIntDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | LongDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | ULongDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | ShortDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | UShortDictionary _ -> self.ReadGeneralDictionaryKeySymbolic + | AddrDictionary _ -> self.ReadAddrDictionaryKeySymbolic + | _ -> __unreachable__() + read address key dictionaryType + + member private self.HasGeneralDictionaryKeySymbolic<'key when 'key : equality> address key dictionaryType = + let key : heapCollectionKey<'key> = { address = address; key = key } + let extractor (state : state) = + let dictionaryType = state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + let mrKey = MemoryRegionId.createDictionaryKeysId dictionaryType + getOrPutRegionCommon mrKey typeof state.memory.MemoryRegions + :?> memoryRegion, productRegion> + self.HasGeneralDictionaryRegion<'key> dictionaryType extractor (extractor state) false key + + member private self.HasAddrDictionaryKeySymbolic address key dictionaryType = + let key : addrCollectionKey = { address = address; key = key } + let extractor (state : state) = + let dictionaryType = state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + let mrKey = MemoryRegionId.createDictionaryKeysId dictionaryType + getOrPutRegionCommon mrKey typeof state.memory.MemoryRegions :?> addrDictionaryKeysRegion + self.HasAddrDictionaryRegion dictionaryType extractor (extractor state) false key + + member private self.DictionaryHasKeySymbolic address key dictionaryType = + let read = + match dictionaryType with + | BoolDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | ByteDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | SByteDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | CharDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | DecimalDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | DoubleDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | IntDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | UIntDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | LongDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | ULongDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | ShortDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | UShortDictionary _ -> self.HasGeneralDictionaryKeySymbolic + | AddrDictionary _ -> self.HasAddrDictionaryKeySymbolic + | _ -> __unreachable__() + read address key dictionaryType + + member private self.ReadGeneralSetKeySymbolic<'key when 'key : equality> address item setType = + let key : heapCollectionKey<'key> = { address = address; key = item } + let extractor (state : state) = + let setType = state.SubstituteTypeVariablesIntoSetType setType + let mrKey = MemoryRegionId.createSetsId setType + getOrPutRegionCommon mrKey typeof state.memory.MemoryRegions + :?> memoryRegion, productRegion> + self.ReadGeneralSetRegion<'key> setType extractor (extractor state) false key + + member private self.ReadAddrSetKeySymbolic address item setType = + let key : addrCollectionKey = { address = address; key = item } + let extractor (state : state) = + let setType = state.SubstituteTypeVariablesIntoSetType setType + let mrKey = MemoryRegionId.createSetsId setType + getOrPutRegionCommon mrKey typeof state.memory.MemoryRegions :?> addrSetsRegion + self.ReadAddrSetRegion setType extractor (extractor state) false key + + member private self.ReadSetKeySymbolic address item setType = + let read = + match setType with + | BoolSet _ -> self.ReadGeneralSetKeySymbolic + | ByteSet _ -> self.ReadGeneralSetKeySymbolic + | SByteSet _ -> self.ReadGeneralSetKeySymbolic + | CharSet _ -> self.ReadGeneralSetKeySymbolic + | DecimalSet _ -> self.ReadGeneralSetKeySymbolic + | DoubleSet _ -> self.ReadGeneralSetKeySymbolic + | IntSet _ -> self.ReadGeneralSetKeySymbolic + | UIntSet _ -> self.ReadGeneralSetKeySymbolic + | LongSet _ -> self.ReadGeneralSetKeySymbolic + | ULongSet _ -> self.ReadGeneralSetKeySymbolic + | ShortSet _ -> self.ReadGeneralSetKeySymbolic + | UShortSet _ -> self.ReadGeneralSetKeySymbolic + | AddrSet _ -> self.ReadAddrSetKeySymbolic + | _ -> __unreachable__() + read address item setType + member private self.ReadArrayIndexSymbolic address indices arrayType = let indices = List.map (fun i -> primitiveCast i typeof) indices let key = OneArrayIndexKey(address, indices) @@ -781,6 +1384,49 @@ module internal Memory = key, value Seq.map prepareData data |> MemoryRegion.memset region + member private self.ListRegionMemsetData concreteAddress data listType (region : listsRegion) = + let address = ConcreteHeapAddress concreteAddress + let regionType = listType.listValueType + let prepareData idx value = + let key = OneArrayIndexKey(address, [makeNumber idx]) + let value = self.ObjToTerm regionType value + key, value + Seq.mapi prepareData data |> MemoryRegion.memset region + + member private self.AddrDictionaryRegionMemsetData concreteAddress data dictionaryType (region : addrDictionariesRegion) = + let address = ConcreteHeapAddress concreteAddress + let keyType = dictionaryType.keyType + let regionType = dictionaryType.valueType + let prepareData (key, value) = + let key : addrCollectionKey = { address = address; key = self.ObjToTerm keyType key } + let value = self.ObjToTerm regionType (value :> obj) + key, value + Seq.map prepareData data |> MemoryRegion.memset region + + member private self.GeneralDictionaryRegionMemsetData<'key when 'key : equality> concreteAddress data dictionaryType region = + let address = ConcreteHeapAddress concreteAddress + let keyType = dictionaryType.keyType + let regionType = dictionaryType.valueType + let prepareData (key, value) = + let key : heapCollectionKey<'key> = { address = address; key = self.ObjToTerm keyType key } + let value = self.ObjToTerm regionType (value :> obj) + key, value + Seq.map prepareData data |> MemoryRegion.memset region + + member private self.GeneralSetRegionMemsetData<'key when 'key : equality> concreteAddress (data : seq) itemType region = + let address = ConcreteHeapAddress concreteAddress + let prepareData item = + let key : heapCollectionKey<'key> = { address = address; key = self.ObjToTerm itemType item } + key, True() + Seq.map prepareData data |> MemoryRegion.memset region + + member private self.AddrSetRegionMemsetData concreteAddress data itemType region = + let address = ConcreteHeapAddress concreteAddress + let prepareData item = + let key : addrCollectionKey = { address = address; key = self.ObjToTerm itemType item } + key, True() + Seq.map prepareData data |> MemoryRegion.memset region + member private self.ArrayRegionFromData concreteAddress data regionType = let region = MemoryRegion.emptyWithExplicit regionType concreteAddress self.ArrayRegionMemsetData concreteAddress data regionType region @@ -800,14 +1446,208 @@ module internal Memory = let key = OneArrayIndexKey(address, indices) self.ReadArrayRegion arrayType (always region) region true key + member private self.ReadSymbolicIndexFromConcreteList concreteAddress listData index listType = + let address = ConcreteHeapAddress concreteAddress + let region = MemoryRegion.emptyWithExplicit listType.listValueType concreteAddress + let region : listsRegion = self.ListRegionMemsetData concreteAddress listData listType region + let key = OneArrayIndexKey(address, [index]) + self.ReadListRegion listType (always region) region true key + + member private self.ReadSymbolicKeyFromConcreteGeneralDictionary<'key when 'key : equality> concreteAddress data key dictionaryType = + let address = ConcreteHeapAddress concreteAddress + let region = MemoryRegion.emptyWithExplicit dictionaryType.valueType concreteAddress + let region : memoryRegion, productRegion, points<'key>>> = + self.GeneralDictionaryRegionMemsetData<'key> concreteAddress data dictionaryType region + let key : heapCollectionKey<'key> = { address = address; key = key } + self.ReadGeneralDictionaryRegion<'key> dictionaryType (always region) region true key + + member private self.ReadSymbolicKeyFromConcreteAddrDictionary concreteAddress data key dictionaryType = + let address = ConcreteHeapAddress concreteAddress + let regionType = dictionaryType.valueType + let region = MemoryRegion.emptyWithExplicit regionType concreteAddress + let region : addrDictionariesRegion = self.AddrDictionaryRegionMemsetData concreteAddress data dictionaryType region + let key : addrCollectionKey = { address = address; key = key } + self.ReadAddrDictionaryRegion dictionaryType (always region) region true key + + member private self.ReadSymbolicKeyFromConcreteDictionary concreteAddress data key dictionaryType = + let read = + match dictionaryType with + | BoolDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | ByteDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | SByteDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | CharDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | DecimalDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | DoubleDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | IntDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | UIntDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | LongDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | ULongDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | ShortDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | UShortDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary + | AddrDictionary _ -> self.ReadSymbolicKeyFromConcreteAddrDictionary + | _ -> __unreachable__() + read concreteAddress data key dictionaryType + + member private self.HasSymbolicKeyFromConcreteGeneralDictionary<'key when 'key : equality> concreteAddress data key dictionaryType = + let address = ConcreteHeapAddress concreteAddress + let keyType = dictionaryType.keyType + let region = MemoryRegion.emptyWithExplicit typeof concreteAddress + let region : memoryRegion, productRegion, points<'key>>> = + self.GeneralSetRegionMemsetData<'key> concreteAddress data keyType region + let key : heapCollectionKey<'key> = { address = address; key = key } + self.HasGeneralDictionaryRegion<'key> dictionaryType (always region) region true key + + member private self.HasSymbolicKeyFromConcreteAddrDictionary concreteAddress data key dictionaryType = + let address = ConcreteHeapAddress concreteAddress + let keyType = dictionaryType.keyType + let region = MemoryRegion.emptyWithExplicit typeof concreteAddress + let region : addrDictionaryKeysRegion = self.AddrSetRegionMemsetData concreteAddress data keyType region + let key : addrCollectionKey = { address = address; key = key } + self.HasAddrDictionaryRegion dictionaryType (always region) region true key + + member private self.DictionaryHasSymbolicKeyFromConcreteDictionary concreteAddress data key dictionaryType = + let contains = + match dictionaryType with + | BoolDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | ByteDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | SByteDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | CharDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | DecimalDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | DoubleDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | IntDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | UIntDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | LongDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | ULongDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | ShortDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | UShortDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary + | AddrDictionary _ -> self.HasSymbolicKeyFromConcreteAddrDictionary + | _ -> __unreachable__() + contains concreteAddress data key dictionaryType + + member private self.ReadSymbolicKeyFromConcreteGeneralSet<'key when 'key : equality> concreteAddress data item setType = + let address = ConcreteHeapAddress concreteAddress + let itemType = setType.setValueType + let region = MemoryRegion.emptyWithExplicit typeof concreteAddress + let region : memoryRegion, productRegion, points<'key>>> = + self.GeneralSetRegionMemsetData<'key> concreteAddress data itemType region + let key : heapCollectionKey<'key> = { address = address; key = item } + self.ReadGeneralSetRegion<'key> setType (always region) region true key + + member private self.ReadSymbolicKeyFromConcreteAddrSet concreteAddress data item setType = + let address = ConcreteHeapAddress concreteAddress + let itemType = setType.setValueType + let region = MemoryRegion.emptyWithExplicit typeof concreteAddress + let region : addrSetsRegion = self.AddrSetRegionMemsetData concreteAddress data itemType region + let key : addrCollectionKey = { address = address; key = item } + self.ReadAddrSetRegion setType (always region) region true key + + member private self.ReadSymbolicKeyFromConcreteSet concreteAddress data item setType = + let read = + match setType with + | BoolSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | ByteSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | SByteSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | CharSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | DecimalSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | DoubleSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | IntSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | UIntSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | LongSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | ULongSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | ShortSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | UShortSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet + | AddrSet _ -> self.ReadSymbolicKeyFromConcreteAddrSet + | _ -> __unreachable__() + read concreteAddress data item setType + member private self.ArrayMemsetData concreteAddress data arrayType = let arrayType = state.SubstituteTypeVariablesIntoArrayType arrayType let elemType = arrayType.elemType ensureConcreteType elemType - let region = accessRegion arrays arrayType elemType + let mrKey = MemoryRegionId.createArraysId arrayType + let region = getOrPutRegion mrKey elemType :?> arraysRegion let region' = self.ArrayRegionMemsetData concreteAddress data elemType region let region' = MemoryRegion.addExplicitAddress concreteAddress region' - arrays <- PersistentDict.add arrayType region' arrays + memoryRegions <- PersistentDict.add mrKey region' memoryRegions + + member private self.GeneralDictionaryMemsetData<'key when 'key : equality> concreteAddress data valueType dictionaryType = + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let region = getOrPutRegion mrKey valueType :?> memoryRegion, productRegion, points<'key>>> + let region' = self.GeneralDictionaryRegionMemsetData<'key> concreteAddress data dictionaryType region + let region' = MemoryRegion.addExplicitAddress concreteAddress region' + memoryRegions <- PersistentDict.add mrKey region' memoryRegions + + member private self.AddrDictionaryMemsetData concreteAddress data valueType dictionaryType = + let mrKey = MemoryRegionId.createDictionariesId dictionaryType + let region = getOrPutRegion mrKey valueType :?> addrDictionariesRegion + let region' = self.AddrDictionaryRegionMemsetData concreteAddress data dictionaryType region + let region' = MemoryRegion.addExplicitAddress concreteAddress region' + memoryRegions <- PersistentDict.add mrKey region' memoryRegions + + member private self.DictionaryMemsetData concreteAddress data dictionaryType = + let dictionaryType = state.SubstituteTypeVariablesIntoDictionaryType dictionaryType + let valueType = dictionaryType.valueType + ensureConcreteType valueType + let memset = + match dictionaryType with + | BoolDictionary _ -> self.GeneralDictionaryMemsetData + | ByteDictionary _ -> self.GeneralDictionaryMemsetData + | SByteDictionary _ -> self.GeneralDictionaryMemsetData + | CharDictionary _ -> self.GeneralDictionaryMemsetData + | DecimalDictionary _ -> self.GeneralDictionaryMemsetData + | DoubleDictionary _ -> self.GeneralDictionaryMemsetData + | IntDictionary _ -> self.GeneralDictionaryMemsetData + | UIntDictionary _ -> self.GeneralDictionaryMemsetData + | LongDictionary _ -> self.GeneralDictionaryMemsetData + | ULongDictionary _ -> self.GeneralDictionaryMemsetData + | ShortDictionary _ -> self.GeneralDictionaryMemsetData + | UShortDictionary _ -> self.GeneralDictionaryMemsetData + | AddrDictionary _ -> self.AddrDictionaryMemsetData + | kt -> internalfail $"Dictionary memset data: expected key type but get {kt}" + memset concreteAddress data valueType dictionaryType + + member private self.GeneralSetMemsetData<'key when 'key : equality> concreteAddress data setType = + let mrKey = MemoryRegionId.createSetsId setType + let region = getOrPutRegion mrKey typeof :?> memoryRegion, productRegion, points<'key>>> + let region' = self.GeneralSetRegionMemsetData<'key> concreteAddress data setType.setValueType region + let region' = MemoryRegion.addExplicitAddress concreteAddress region' + memoryRegions <- PersistentDict.add mrKey region' memoryRegions + + member private self.AddrSetMemsetData concreteAddress data setType = + let mrKey = MemoryRegionId.createSetsId setType + let region = getOrPutRegion mrKey typeof :?> addrSetsRegion + let region' = self.AddrSetRegionMemsetData concreteAddress data setType.setValueType region + let region' = MemoryRegion.addExplicitAddress concreteAddress region' + memoryRegions <- PersistentDict.add mrKey region' memoryRegions + + member private self.SetMemsetData concreteAddress data setType = + let setType = state.SubstituteTypeVariablesIntoSetType setType + let itemType = setType.setValueType + ensureConcreteType itemType + let memset = + match setType with + | BoolSet _ -> self.GeneralSetMemsetData + | ByteSet _ -> self.GeneralSetMemsetData + | SByteSet _ -> self.GeneralSetMemsetData + | CharSet _ -> self.GeneralSetMemsetData + | DecimalSet _ -> self.GeneralSetMemsetData + | DoubleSet _ -> self.GeneralSetMemsetData + | IntSet _ -> self.GeneralSetMemsetData + | UIntSet _ -> self.GeneralSetMemsetData + | LongSet _ -> self.GeneralSetMemsetData + | ULongSet _ -> self.GeneralSetMemsetData + | ShortSet _ -> self.GeneralSetMemsetData + | UShortSet _ -> self.GeneralSetMemsetData + | AddrSet _ -> self.AddrSetMemsetData + | st -> internalfail $"Set memset data: expected item type but get {st}" + memset concreteAddress data setType + + member private self.ListMemsetData concreteAddress data listType = + let mrKey = MemoryRegionId.createListsId listType + let region = getOrPutRegion mrKey listType.listValueType :?> listsRegion + let region' = self.ListRegionMemsetData concreteAddress data listType region + let region' = MemoryRegion.addExplicitAddress concreteAddress region' + memoryRegions <- PersistentDict.add mrKey region' memoryRegions member private self.MakeSymbolicStackRead key typ time = let source = {key = key; time = time} @@ -828,6 +1668,27 @@ module internal Memory = cm.ReadArrayLength address dim |> self.ObjToTerm typeof | _ -> self.ReadLengthSymbolic address dimension arrayType + member private self.ReadDictionaryCount address dictionaryType = + let cm = concreteMemory + match address.term with + | ConcreteHeapAddress address when cm.Contains address -> + cm.ReadDictionaryCount address |> self.ObjToTerm typeof + | _ -> self.ReadDictionaryCountSymbolic address dictionaryType + + member private self.ReadSetCount address setType = + let cm = concreteMemory + match address.term with + | ConcreteHeapAddress address when cm.Contains address -> + cm.ReadSetCount address |> self.ObjToTerm typeof + | _ -> self.ReadSetCountSymbolic address setType + + member private self.ReadListCount address listType = + let cm = concreteMemory + match address.term with + | ConcreteHeapAddress address when cm.Contains address -> + cm.ReadListCount address |> self.ObjToTerm typeof + | _ -> self.ReadListCountSymbolic address listType + member private self.ReadArrayIndex address indices arrayType = let cm = concreteMemory let concreteIndices = tryIntListFromTermList indices @@ -840,12 +1701,57 @@ module internal Memory = // TODO: remember all concrete data from 'ConcreteMemory' and add it to symbolic constant [Test: ConcreteDictionaryTest1] | _ -> self.ReadArrayIndexSymbolic address indices arrayType + member private self.ReadDictionaryKey address key dictionaryType = + let cm = concreteMemory + let concreteKey = tryCollectionKeyFromTerm key + match address.term, concreteKey with + | ConcreteHeapAddress address, Some concreteKey when cm.Contains address -> + cm.ReadDictionaryKey address concreteKey |> self.ObjToTerm dictionaryType.valueType + | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress -> + let data = cm.GetAllDictionaryData concreteAddress + self.ReadSymbolicKeyFromConcreteDictionary concreteAddress data key dictionaryType + | _ -> self.ReadDictionaryKeySymbolic address key dictionaryType + + member private self.ReadDictionaryKeyContains address key dictionaryType = + let cm = concreteMemory + let concreteKey = tryCollectionKeyFromTerm key + match address.term, concreteKey with + | ConcreteHeapAddress address, Some concreteKey when cm.Contains address -> + cm.DictionaryHasKey address concreteKey |> makeBool + | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress -> + let data = Seq.map fst <| cm.GetAllDictionaryData concreteAddress + self.DictionaryHasSymbolicKeyFromConcreteDictionary concreteAddress data key dictionaryType + | _ -> self.DictionaryHasKeySymbolic address key dictionaryType + + member private self.ReadSetKey address item setType = + let cm = concreteMemory + let concreteItem = tryCollectionKeyFromTerm item + match address.term, concreteItem with + | ConcreteHeapAddress address, Some concreteItem when cm.Contains address -> + cm.ReadSetKey address concreteItem |> makeBool + | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress -> + let data = cm.GetAllSetData concreteAddress + self.ReadSymbolicKeyFromConcreteSet concreteAddress data item setType + | _ -> self.ReadSetKeySymbolic address item setType + + member private self.ReadListIndex address index listType = + let cm = concreteMemory + let concreteIndex = tryIntFromTerm index + match address.term, concreteIndex with + | ConcreteHeapAddress address, Some concreteIndex when cm.Contains address -> + cm.ReadListIndex address concreteIndex |> self.ObjToTerm listType.listValueType + | ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress -> + let data = cm.GetAllListData concreteAddress + self.ReadSymbolicIndexFromConcreteList concreteAddress data index listType + | _ -> self.ReadListIndexSymbolic address index listType + member private self.CommonReadClassFieldSymbolic address (field : fieldId) = let symbolicType = field.typ let extractor (state : state) = let field = state.SubstituteTypeVariablesIntoField field let typ = state.SubstituteTypeVariables symbolicType - accessRegion state.memory.ClassFields field typ + let mrKey = MemoryRegionId.createClassFieldsId field + getOrPutRegionCommon mrKey typ state.memory.MemoryRegions :?> classFieldsRegion let region = extractor state let mkName = fun (key : heapAddressKey) -> $"{key.address}.{field}" let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address @@ -864,7 +1770,9 @@ module internal Memory = MemoryRegion.read region key (isDefault state) instantiate self.RangeReadingUnreachable member private self.ReadBoxedSymbolic address typ = - let extractor state = accessRegion state.memory.BoxedLocations typ typ + let extractor (state : state) = + let mrKey = MemoryRegionId.createBoxedLocationsId typ + getOrPutRegionCommon mrKey typ state.memory.MemoryRegions :?> boxedLocationsRegion let region = extractor state let mkName (key : heapAddressKey) = $"boxed {key.address} of {typ}" let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address @@ -896,7 +1804,8 @@ module internal Memory = let extractor (state : state) = let field = state.SubstituteTypeVariablesIntoField field let typ = state.SubstituteTypeVariables field.typ - accessRegion state.memory.StaticFields field typ + let mrKey = MemoryRegionId.createStaticFieldsId field + getOrPutRegionCommon mrKey typ state.memory.MemoryRegions :?> staticFieldsRegion let mkName = fun (key : symbolicTypeKey) -> $"{key.typ}.{field}" let isDefault state _ = state.complete // TODO: when statics are allocated? always or never? depends on our exploration strategy let key = {typ = typ} @@ -911,7 +1820,9 @@ module internal Memory = MemoryRegion.read (extractor state) key (isDefault state) inst self.RangeReadingUnreachable member private self.ReadStackBuffer (stackKey : stackKey) index = - let extractor state = accessRegion state.memory.StackBuffers (stackKey.Map state.TypeVariableSubst) typeof + let extractor (state : state) = + let mrKey = MemoryRegionId.createStackBuffersId <| stackKey.Map state.TypeVariableSubst + getOrPutRegionCommon mrKey typeof state.memory.MemoryRegions :?> stackBuffersRegion let mkName (key : stackBufferIndexKey) = $"{stackKey}[{key.index}]" let isDefault _ _ = true let key : stackBufferIndexKey = {index = index} @@ -948,6 +1859,13 @@ module internal Memory = | BoxedLocation(address, typ) -> self.ReadBoxedLocation address typ | StackBufferIndex(key, index) -> self.ReadStackBuffer key index | ArrayLowerBound(address, dimension, typ) -> self.ReadLowerBound address dimension typ + | DictionaryKey(address, key, typ) -> self.ReadDictionaryKey address key typ + | DictionaryCount(address, typ) -> self.ReadDictionaryCount address typ + | DictionaryHasKey(address, key, typ) -> self.ReadDictionaryKeyContains address key typ + | SetKey(address, item, typ) -> self.ReadSetKey address item typ + | SetCount(address, typ) -> self.ReadSetCount address typ + | ListIndex(address, index, typ) -> self.ReadListIndex address index typ + | ListCount(address, typ) -> self.ReadListCount address typ // ------------------------------- Unsafe reading ------------------------------- @@ -1271,6 +2189,34 @@ module internal Memory = Merging.guardedMap referenceField filtered | _ -> internalfailf $"Referencing field: expected reference, but got {reference}" + member private self.ReferenceKey reference key typ = + let t = symbolicTypeToDictionaryType typ + Ref <| DictionaryKey(reference, key, t) + + member private self.DictionaryKeyContains dict key typ = + let t = symbolicTypeToDictionaryType typ + Ref <| DictionaryHasKey(dict, key, t) + + member private self.DictionaryCount dict typ = + let t = symbolicTypeToDictionaryType typ + Ref <| DictionaryCount(dict, t) + + member private self.SetKey reference item typ = + let t = symbolicTypeToSetType typ + Ref <| SetKey(reference, item, t) + + member private self.SetCount reference typ = + let t = symbolicTypeToSetType typ + Ref <| SetCount(reference, t) + + member private self.ListIndex reference index typ = + let t = symbolicTypeToListType typ + Ref <| ListIndex(reference, index, t) + + member private self.ListCount reference typ = + let t = symbolicTypeToListType typ + Ref <| ListCount(reference, t) + // --------------------------- General reading --------------------------- // TODO: take type of heap address @@ -1314,6 +2260,46 @@ module internal Memory = let termLens = List.map lenToObj lens fillArrayBoundsSymbolic None address termLens termLBs arrayType + member private self.FillDictionaryKeysSymbolic guard address data dictionaryType = + let fill (key, _) = + let key = self.ObjToTerm dictionaryType.keyType key + writeDictionaryKeyToKeysSymbolic guard address key dictionaryType <| True() + Seq.iter fill data + + member private self.FillDictionaryCountsSymbolic guard address data dictionaryType = + let count = makeNumber <| Seq.length data + writeDictionaryCount guard address dictionaryType count + + member private self.UnmarshallDictionary concreteAddress (dict : IDictionary) = + let address = ConcreteHeapAddress concreteAddress + let dictionaryType = dict.GetType() |> symbolicTypeToDictionaryType + let data = Reflection.keyAndValueSeqFromDictionaryObj dict + self.DictionaryMemsetData concreteAddress data dictionaryType + self.FillDictionaryKeysSymbolic None address data dictionaryType + self.FillDictionaryCountsSymbolic None address data dictionaryType + + member private self.FillSetCountsSymbolic guard address data setType = + let count = Seq.length data |> makeNumber + writeSetCount guard address setType count + + member private self.UnmarshallSet concreteAddress (set : obj) = + let address = ConcreteHeapAddress concreteAddress + let setType = set.GetType() |> symbolicTypeToSetType + let data = seq { for item in (set :?> IEnumerable) -> item } + self.SetMemsetData concreteAddress data setType + self.FillSetCountsSymbolic None address data setType + + member private self.FillListCountsSymbolic guard address data listType = + let count = Seq.length data |> makeNumber + writeListCount guard address listType count + + member private self.UnmarshallList concreteAddress (list : obj) = + let address = ConcreteHeapAddress concreteAddress + let listType = list.GetType() |> symbolicTypeToListType + let data = seq { for item in (list :?> IEnumerable) -> item } + self.ListMemsetData concreteAddress data listType + self.FillListCountsSymbolic None address data listType + member private self.UnmarshallString concreteAddress (string : string) = let address = ConcreteHeapAddress concreteAddress let concreteStringLength = string.Length @@ -1328,6 +2314,9 @@ module internal Memory = concreteMemory.Remove concreteAddress match obj with | :? Array as array -> self.UnmarshallArray concreteAddress array + | :? IDictionary as dict -> self.UnmarshallDictionary concreteAddress dict + | Set set -> self.UnmarshallSet concreteAddress set + | List list -> self.UnmarshallList concreteAddress list | :? String as string -> self.UnmarshallString concreteAddress string | _ -> self.UnmarshallClass concreteAddress obj @@ -1354,6 +2343,99 @@ module internal Memory = writeArrayIndexSymbolic guard address indices arrayType value | _ -> writeArrayIndexSymbolic guard address indices arrayType value + member private self.CommonWriteDictionaryKey guard address key dictionaryType value = + let concreteValue = self.TryTermToObj value + let concreteKey = tryCollectionKeyFromTerm key + match address.term, concreteValue, concreteKey, guard with + | ConcreteHeapAddress a, Some obj, Some concreteKey, None when concreteMemory.Contains a -> + concreteMemory.WriteDictionaryKey a concreteKey obj + | ConcreteHeapAddress a, _, _, _ when concreteMemory.Contains a -> + self.Unmarshall a + writeDictionaryKeySymbolic guard address key dictionaryType value + | _ -> writeDictionaryKeySymbolic guard address key dictionaryType value + + member private self.CommonWriteSetKey guard address item setType value = + let concreteValue = self.TryTermToObj value + let concreteKey = tryCollectionKeyFromTerm item + match address.term, concreteValue, concreteKey, guard with + | ConcreteHeapAddress a, Some obj, Some concreteKey, None when concreteMemory.Contains a -> + concreteMemory.WriteSetKey a concreteKey obj + | ConcreteHeapAddress a, _, _, _ when concreteMemory.Contains a -> + self.Unmarshall a + writeSetKeySymbolic guard address item setType value + | _ -> writeSetKeySymbolic guard address item setType value + + member private self.CommonWriteListIndex guard address index listType value = + let concreteValue = self.TryTermToObj value + let concreteIndex = tryIntFromTerm index + match address.term, concreteValue, concreteIndex, guard with + | ConcreteHeapAddress a, Some obj, Some concreteIndex, None when concreteMemory.Contains a -> + concreteMemory.WriteListIndex a concreteIndex obj + | ConcreteHeapAddress a, _, _, _ when concreteMemory.Contains a -> + self.Unmarshall a + writeListIndexSymbolic guard address index listType value + | _ -> writeListIndexSymbolic guard address index listType value + + member private self.ListRemoveAt address index (listType : listType) count = + let concreteIndex = tryIntFromTerm index + match address.term, concreteIndex with + | ConcreteHeapAddress a, Some concreteIndex when concreteMemory.Contains a -> + concreteMemory.ListRemoveAt a concreteIndex + | ConcreteHeapAddress a, _ when concreteMemory.Contains a -> + self.Unmarshall a + let srcFrom = add index <| makeNumber 1 + let srcMemory = self.ReadListRangeSymbolic address srcFrom count listType + let dstTo = sub count <| makeNumber 1 + writeListRangeSymbolic address index dstTo listType srcMemory + | _ -> + let srcFrom = add index <| makeNumber 1 + let srcMemory = self.ReadListRangeSymbolic address srcFrom count listType + let dstTo = sub count <| makeNumber 1 + writeListRangeSymbolic address index dstTo listType srcMemory + + member private self.ListInsertIndex address index value (listType : listType) count = + let concreteIndex = tryIntFromTerm index + let concreteValue = self.TryTermToObj value + match address.term, concreteIndex, concreteValue with + | ConcreteHeapAddress a, Some concreteIndex, Some concreteValue when concreteMemory.Contains a -> + concreteMemory.InsertIndex a concreteIndex concreteValue + | ConcreteHeapAddress a, _, _ when concreteMemory.Contains a -> + self.Unmarshall a + let srcMemory = self.ReadListRangeSymbolic address index count listType + let dstTo = add count <| makeNumber 1 + let dstFrom = add index <| makeNumber 1 + writeListRangeSymbolic address dstFrom dstTo listType srcMemory + writeListIndexSymbolic None address index listType value + | _ -> + let srcMemory = self.ReadListRangeSymbolic address index count listType + let dstTo = add count <| makeNumber 1 + let dstFrom = add index <| makeNumber 1 + writeListRangeSymbolic address dstFrom dstTo listType srcMemory + writeListIndexSymbolic None address index listType value + + member private self.ListCopyToSymbolic list array index arrayIndex count listType arrayType = + let srcTo = add index count + let srcMemory = self.ReadListRangeSymbolic list index srcTo listType + let dstTo = add arrayIndex count + writeArrayRangeSymbolic None array [arrayIndex] [dstTo] arrayType srcMemory + + member private self.ListCopyToRange list index array arrayIndex count listType arrayType = + let conIdx = tryIntFromTerm index + let conArrayIdx = tryIntFromTerm arrayIndex + let conCount = tryIntFromTerm count + let cm = concreteMemory + match list.term, array.term, conIdx, conArrayIdx, conCount with + | ConcreteHeapAddress listAddr, ConcreteHeapAddress arrayAddr, Some conIdx, Some conArrayIdx, Some conCount + when (cm.Contains listAddr) && (cm.Contains arrayAddr) -> + cm.ListCopyToRange listAddr conIdx arrayAddr conArrayIdx conCount + | ConcreteHeapAddress listAddr, _, _, _, _ when cm.Contains listAddr -> + self.Unmarshall listAddr + self.ListCopyToSymbolic list array index arrayIndex count listType arrayType + | _, ConcreteHeapAddress arrayAddr, _, _, _ when cm.Contains arrayAddr -> + self.Unmarshall arrayAddr + self.ListCopyToSymbolic list array index arrayIndex count listType arrayType + | _ -> self.ListCopyToSymbolic list array index arrayIndex count listType arrayType + member private self.CommonWriteArrayRange guard address fromIndices toIndices arrayType value = let concreteValue = self.TryTermToObj value let concreteFromIndices = tryIntListFromTermList fromIndices @@ -1499,6 +2581,9 @@ module internal Memory = self.WriteIntersectingField reporter guard address field value | ClassField(address, field) -> self.CommonWriteClassField guard address field value | ArrayIndex(address, indices, typ) -> self.CommonWriteArrayIndex guard address indices typ value + | DictionaryKey(address, key, typ) -> self.CommonWriteDictionaryKey guard address key typ value + | SetKey(address, item, typ) -> self.CommonWriteSetKey guard address item typ value + | ListIndex(address, index, typ) -> self.CommonWriteListIndex guard address index typ value | StaticField(typ, field) -> self.CommonWriteStaticField guard typ field value | StructField(address, field) -> let oldStruct = self.ReadSafe reporter address @@ -1510,6 +2595,10 @@ module internal Memory = // NOTE: Cases below is needed to construct a model | ArrayLength(address, dimension, typ) -> writeLengthSymbolic guard address dimension typ value | ArrayLowerBound(address, dimension, typ) -> writeLowerBoundSymbolic guard address dimension typ value + | DictionaryCount(address, typ) -> writeDictionaryCount guard address typ value + | DictionaryHasKey(address, key, typ) -> writeDictionaryKeyToKeysSymbolic guard address key typ value + | SetCount(address, typ) -> writeSetCount guard address typ value + | ListCount(address, typ) -> writeListCount guard address typ value // TODO: unify allocation with unmarshalling member private self.CommonAllocateString length contents = @@ -1742,20 +2831,22 @@ module internal Memory = member private self.InitializeArray address indicesAndValues arrayType = let elementType = arrayType.elemType ensureConcreteType elementType - let mr = accessRegion arrays arrayType elementType + let mrKey = MemoryRegionId.createArraysId arrayType + let mr = getOrPutRegion mrKey elementType :?> arraysRegion let keysAndValues = Seq.map (fun (i, v) -> OneArrayIndexKey(address, i), v) indicesAndValues let mr' = MemoryRegion.memset mr keysAndValues - arrays <- PersistentDict.add arrayType mr' arrays + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions member private self.CommonWriteStaticField guard typ (field : fieldId) value = ensureConcreteType field.typ let fieldType = if isImplementationDetails typ then typeof.MakeArrayType() else field.typ - let mr = accessRegion staticFields field fieldType + let mrKey = MemoryRegionId.createStaticFieldsId field + let mr = getOrPutRegion mrKey fieldType :?> staticFieldsRegion let key = {typ = typ} let mr' = MemoryRegion.write mr guard key value - staticFields <- PersistentDict.add field mr' staticFields + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions let currentMethod = CallStack.getCurrentFunc stack if not currentMethod.IsStaticConstructor then concreteMemory.StaticFieldChanged field @@ -1824,10 +2915,11 @@ module internal Memory = | _ -> let address = self.AllocateVector elementType length let arrayType = arrayType.CreateVector elementType - let mr = accessRegion arrays arrayType elementType + let mrKey = MemoryRegionId.createArraysId arrayType + let mr = getOrPutRegion mrKey elementType :?> arraysRegion let keysAndValues = Seq.mapi (fun i v -> OneArrayIndexKey(address, [makeNumber i]), Concrete v elementType) contents let mr' = MemoryRegion.memset mr keysAndValues - arrays <- PersistentDict.add arrayType mr' arrays + memoryRegions <- PersistentDict.add mrKey mr' memoryRegions address member private self.AllocateEmptyString length = @@ -1970,51 +3062,27 @@ module internal Memory = override _.AllocatedTypes with get() = allocatedTypes and set value = allocatedTypes <- value - override _.Arrays - with get() = arrays - and set value = arrays <- value - override _.BoxedLocations - with get() = boxedLocations - and set value = boxedLocations <- value - override _.ClassFields - with get() = classFields - and set value = classFields <- value + override _.MemoryRegions + with get() = memoryRegions + and set value = memoryRegions <- value override _.ConcreteMemory with get() = concreteMemory override _.Delegates with get() = delegates override _.EvaluationStack with get() = evaluationStack and set value = evaluationStack <- value override _.InitializedAddresses with get() = initializedAddresses - override _.Lengths - with get() = lengths - and set value = lengths <- value - override _.LowerBounds - with get() = lowerBounds - and set value = lowerBounds <- value override _.MemoryMode with get() = memoryMode and set value = memoryMode <- value override _.Stack with get() = stack and set(callStack: callStack) = stack <- callStack - override _.StackBuffers - with get() = stackBuffers - and set value = stackBuffers <- value - override _.StaticFields - with get() = staticFields - and set value = staticFields <- value override self.Copy() = let copy = Memory( evaluationStack, stack, - stackBuffers, - classFields, - arrays, - lengths, - lowerBounds, - staticFields, - boxedLocations, + memoryRegions, concreteMemory.Copy(), allocatedTypes, initializedAddresses, @@ -2032,6 +3100,16 @@ module internal Memory = member self.ReadLowerBound address dimension arrayType = self.ReadLowerBound address dimension arrayType member self.ReadStaticField typ field = self.ReadStaticField typ field member self.ReferenceField reference fieldId = self.ReferenceField reference fieldId + member self.ReferenceKey reference key typ = self.ReferenceKey reference key typ + member self.DictionaryKeyContains reference key typ = self.DictionaryKeyContains reference key typ + member self.DictionaryCount reference typ = self.DictionaryCount reference typ + member self.SetKey reference item typ = self.SetKey reference item typ + member self.SetCount reference typ = self.SetCount reference typ + member self.ListIndex reference index typ = self.ListIndex reference index typ + member self.ListCount reference typ = self.ListCount reference typ + member self.ListRemoveAt reference index listType count = self.ListRemoveAt reference index listType count + member self.ListInsertIndex reference index value listType count = self.ListInsertIndex reference index value listType count + member self.ListCopyToRange list index array arrayIndex count listType arrayType = self.ListCopyToRange list index array arrayIndex count listType arrayType member self.TryPtrToRef pointerBase sightType offset = self.TryPtrToRef pointerBase sightType offset member self.TryTermToFullyConcreteObj term = self.TryTermToFullyConcreteObj term member self.TryTermToObj term = self.TryTermToObj term diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index 471aa6144..e7445ecc3 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/VSharp.SILI.Core/MemoryRegion.fs @@ -6,6 +6,8 @@ open Microsoft.FSharp.Core open VSharp open VSharp.CSharpUtils open TypeUtils +open DictionaryType +open SetType open VSharp.Core type IMemoryKey<'a, 'reg when 'reg :> IRegion<'reg>> = @@ -23,6 +25,16 @@ type regionSort = | HeapFieldSort of fieldId | StaticFieldSort of fieldId | ArrayIndexSort of arrayType + | DictionaryKeySort of dictionaryType + | AddrDictionaryKeySort of dictionaryType + | DictionaryHasKeySort of dictionaryType + | AddrDictionaryHasKeySort of dictionaryType + | DictionaryCountSort of dictionaryType + | SetKeySort of setType + | AddrSetKeySort of setType + | SetCountSort of setType + | ListIndexSort of listType + | ListCountSort of listType | ArrayLengthSort of arrayType | ArrayLowerBoundSort of arrayType | StackBufferSort of stackKey @@ -33,8 +45,18 @@ type regionSort = | HeapFieldSort field | StaticFieldSort field -> field.typ | ArrayIndexSort arrayType -> arrayType.elemType + | DictionaryKeySort dictionaryType + | AddrDictionaryKeySort dictionaryType -> dictionaryType.valueType + | ListIndexSort listType -> listType.listValueType + | DictionaryHasKeySort _ + | AddrDictionaryHasKeySort _ + | SetKeySort _ + | AddrSetKeySort _ -> typeof | ArrayLengthSort _ - | ArrayLowerBoundSort _ -> typeof + | ArrayLowerBoundSort _ + | DictionaryCountSort _ + | SetCountSort _ + | ListCountSort _ -> typeof | StackBufferSort _ -> typeof | BoxedSort t -> t @@ -56,6 +78,23 @@ type regionSort = else $"ArrayLowerBound to {elementType}[{dim}]" | StackBufferSort stackKey -> $"StackBuffer of {stackKey}" | BoxedSort t -> $"Boxed of {t}" + | DictionaryKeySort dictionaryType + | AddrDictionaryKeySort dictionaryType -> + $"DictionaryKey to {dictionaryType.valueType}" + | DictionaryHasKeySort dictionaryType + | AddrDictionaryHasKeySort dictionaryType -> + $"DictionaryHasKey to {dictionaryType.valueType}" + | DictionaryCountSort dictionaryType -> + $"Counts to {dictionaryType.valueType}" + | SetKeySort setType + | AddrSetKeySort setType -> + $"SetKey to {setType.setValueType}" + | SetCountSort setType -> + $"Counts of {setType.setValueType}" + | ListIndexSort listType -> + $"ListIndex to {listType.listValueType}" + | ListCountSort listType -> + $"Counts of {listType.listValueType}" module private MemoryKeyUtils = @@ -72,6 +111,11 @@ module private MemoryKeyUtils = | Some value -> points.Singleton value | None -> points.Universe + let regionOfValueTerm<'key when 'key : equality> (typ : Type) = function + | {term = Concrete(:? 'key as value, typ)} when typ = typ -> + points<'key>.Singleton value + | _ -> points<'key>.Universe + let regionsOfIntegerTerms = List.map regionOfIntegerTerm >> listProductRegion>.OfSeq let regionOfIntegerRange lowerBound upperBound = @@ -111,6 +155,15 @@ module private MemoryKeyUtils = let keyInPoints point = key === (point2Term point) PersistentSet.fold (fun acc p -> acc ||| (keyInPoints p)) (False()) points |> negateIfNeed + let keyInPoints<'key when 'key : equality> key (region : points<'key>) = + let points, negateIfNeed = + match region with + | {points = points; thrown = true} -> points, (!!) + | {points = points; thrown = false} -> points, id + let point2Term point = Concrete point indexType + let keyInPoints point = key === (point2Term point) + PersistentSet.fold (fun acc p -> acc ||| (keyInPoints p)) (False()) points |> negateIfNeed + let keyInProductRegion keyInFst keyInSnd (region : productRegion<'a,'b>) = let checkInOne acc (first, second) = acc &&& (keyInFst first) &&& (keyInSnd second) List.fold checkInOne (True()) region.products @@ -193,7 +246,7 @@ type heapArrayKey = match x with | OneArrayIndexKey _ -> true | _ -> false - + member x.Specialize writeKey srcA srcF srcT = match x, writeKey with | OneArrayIndexKey(_, i), OneArrayIndexKey(_, dstI) @@ -411,6 +464,100 @@ type heapVectorIndexKey = and IHeapVectorIndexKey = IMemoryKey> +[] +type heapCollectionKey<'key when 'key : equality> = + { address : heapAddress; key : term } + + interface IHeapCollectionKey<'key> with + override x.Region = + let addrReg = MemoryKeyUtils.regionOfHeapAddress x.address + let keyReg = MemoryKeyUtils.regionOfValueTerm typeof<'key> x.key + productRegion.ProductOf addrReg keyReg + override x.Map mapTerm _ mapTime reg = + reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; key = mapTerm x.key} + override x.IsUnion = isUnion x.address + override x.Unguard = + Merging.unguardGvs x.address |> List.map (fun (g, a) -> (g, {address = a; key = x.key})) + override x.InRegionCondition region = + let addressInVtIntervals = MemoryKeyUtils.heapAddressInVectorTimeIntervals x.address + let indexInPoints = MemoryKeyUtils.keyInPoints x.key + MemoryKeyUtils.keyInProductRegion addressInVtIntervals indexInPoints region + override x.IntersectionCondition key = + (x.address === key.address) &&& (x.key === key.key) + override x.MatchCondition key keyIndexingRegion = + let keysAreEqual = (x :> IHeapCollectionKey<'key>).IntersectionCondition key + let xInKeyRegion = (x :> IHeapCollectionKey<'key>).InRegionCondition keyIndexingRegion + keysAreEqual &&& xInKeyRegion + override x.IsExplicit explicitAddresses = + match x.address.term with + | ConcreteHeapAddress addr -> PersistentSet.contains addr explicitAddresses + | _ -> false + override x.IsRange = false + interface IComparable with + override x.CompareTo y = + match y with + | :? heapCollectionKey<'key> as y -> + let cmp = compareTerms x.address y.address + if cmp = 0 then compareTerms x.key y.key + else cmp + | _ -> -1 + override x.ToString() = $"{x.address}[{x.key}]" + override x.Equals(other : obj) = + match other with + | :? heapCollectionKey<'key> as other -> + x.address = other.address && x.key = other.key + | _ -> false + override x.GetHashCode() = HashCode.Combine(x.address, x.key) + +and IHeapCollectionKey<'key when 'key : equality> = IMemoryKey, productRegion> + +[] +type addrCollectionKey = + { address : heapAddress; key : heapAddress } + + interface IHeapAddrCollectionKey with + override x.Region = + let addrReg = MemoryKeyUtils.regionOfHeapAddress x.address + let keyReg = MemoryKeyUtils.regionOfHeapAddress x.key + productRegion.ProductOf addrReg keyReg + override x.Map mapTerm _ mapTime reg = + reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; key = mapTerm x.key} + override x.IsUnion = isUnion x.address + override x.Unguard = + Merging.unguardGvs x.address |> List.map (fun (g, a) -> (g, {address = a; key = x.key})) + override x.InRegionCondition region = + let addressInVtIntervals = MemoryKeyUtils.heapAddressInVectorTimeIntervals x.address + let indexInPoints = MemoryKeyUtils.heapAddressInVectorTimeIntervals x.key + MemoryKeyUtils.keyInProductRegion addressInVtIntervals indexInPoints region + override x.IntersectionCondition key = + (x.address === key.address) &&& (x.key === key.key) + override x.MatchCondition key keyIndexingRegion = + let keysAreEqual = (x :> IHeapAddrCollectionKey).IntersectionCondition key + let xInKeyRegion = (x :> IHeapAddrCollectionKey).InRegionCondition keyIndexingRegion + keysAreEqual &&& xInKeyRegion + override x.IsExplicit explicitAddresses = + match x.address.term with + | ConcreteHeapAddress addr -> PersistentSet.contains addr explicitAddresses + | _ -> false + override x.IsRange = false + interface IComparable with + override x.CompareTo y = + match y with + | :? addrCollectionKey as y -> + let cmp = compareTerms x.address y.address + if cmp = 0 then compareTerms x.key y.key + else cmp + | _ -> -1 + override x.ToString() = $"{x.address}[{x.key}]" + override x.Equals(other : obj) = + match other with + | :? addrCollectionKey as other -> + x.address = other.address && x.key = other.key + | _ -> false + override x.GetHashCode() = HashCode.Combine(x.address, x.key) + +and IHeapAddrCollectionKey = IMemoryKey> + [] type stackBufferIndexKey = {index : term} @@ -552,7 +699,13 @@ module private UpdateTree = (utKey.termGuard, rangeReading)::acc else (utKey.termGuard, utKey.value)::acc) [] (Node concrete) - if PersistentDict.isEmpty symbolic && key.IsExplicit explicitAddresses then iteType.FromGvs branches + + if PersistentDict.isEmpty symbolic && key.IsExplicit explicitAddresses then + if branches.Length > 1 then iteType.FromGvs branches + else + let condition, value = branches[0] + assert(isTrue condition) + { branches = []; elseValue = value } else if PersistentDict.isEmpty symbolic && isDefault key then assert not (key.IsExplicit explicitAddresses) let defaultCase = makeDefault() @@ -561,7 +714,7 @@ module private UpdateTree = let symbolicCase = makeSymbolic (Node symbolic) {branches = branches; elseValue = symbolicCase} |> Merging.merge - + ///Collects nodes that should have been on the top of update tree if we did not use splitting let rec private collectBranchLatestRecords (Node d) predicate latestRecords = let collectSubtreeNodes acc r (k, st) = @@ -631,7 +784,7 @@ module private UpdateTree = PersistentDict.append modifiedTree disjoint |> Node List.foldBack writeOneKey disjointUnguardedKey tree - + let map (mapKey : 'reg -> 'key -> 'reg * 'key) mapValue (tree : updateTree<'key, 'value, 'reg>) predicate = let mapper reg {key=k; value=v; guard = g; time = t} = let reg', k' = mapKey reg k @@ -662,10 +815,16 @@ module private UpdateTree = let forall predicate tree = RegionTree.foldl (fun acc _ k -> acc && predicate k) true tree +type IMemoryRegion = + abstract member ToString : unit -> string + [] type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = {typ : Type; updates : updateTree<'key, term, 'reg>; defaultValue : term option; nextUpdateTime : vectorTime; explicitAddresses : vectorTime pset} with + interface IMemoryRegion with + override x.ToString() = x.ToString() + override x.Equals(other : obj) = match other with | :? memoryRegion<'key, 'reg> as other -> @@ -779,6 +938,156 @@ module MemoryRegion = type memoryRegion<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> with override x.ToString() = MemoryRegion.toString "" x + static member Empty() typ : memoryRegion<'key, 'reg> = MemoryRegion.empty typ + +type IMemoryRegionId = + abstract member ToString : unit -> string + abstract member Empty : Type -> IMemoryRegion + +type memoryRegionSort = + | StackBuffersSort | ClassFieldsSort | StaticFieldsSort | BoxedLocationsSort | ArraysSort | ArrayLengthsSort + | ArrayLowerBoundsSort | BoolDictionariesSort | ByteDictionariesSort | SByteDictionariesSort | CharDictionariesSort + | DecimalDictionariesSort | DoubleDictionariesSort | IntDictionariesSort | UIntDictionariesSort | LongDictionariesSort + | ULongDictionariesSort | ShortDictionariesSort | UShortDictionariesSort | AddrDictionariesSort | BoolDictionaryKeysSort + | ByteDictionaryKeysSort | SByteDictionaryKeysSort | CharDictionaryKeysSort | DecimalDictionaryKeysSort + | DoubleDictionaryKeysSort | IntDictionaryKeysSort | UIntDictionaryKeysSort | LongDictionaryKeysSort | ULongDictionaryKeysSort + | ShortDictionaryKeysSort | UShortDictionaryKeysSort | AddrDictionaryKeysSort | DictionaryCountsSort + | BoolSetsSort | ByteSetsSort | SByteSetsSort | CharSetsSort | DecimalSetsSort | DoubleSetsSort | IntSetsSort + | UIntSetsSort | LongSetsSort | ULongSetsSort | ShortSetsSort | UShortSetsSort | AddrSetsSort | SetCountsSort + | ListsSort | ListCountsSort + +[] +type memoryRegionId<'id, 'key, 'reg when 'id : equality and 'key : equality and 'key :> IMemoryKey<'key,'reg> and 'reg : equality and 'reg :> IRegion<'reg>> = + { id : 'id; sort : memoryRegionSort } + with + interface IMemoryRegionId with + override x.ToString() = x.ToString() + override x.Empty typ = memoryRegion<'key, 'reg>.Empty() typ + + override x.Equals(other : obj) = + match other with + | :? memoryRegionId<'id, 'key, 'reg> as other -> + x.id = other.id && x.sort = other.sort + | _ -> false + override x.GetHashCode() = + HashCode.Combine(x.id, x.sort) + +type stackBuffersId = memoryRegionId +type classFieldsId = memoryRegionId +type staticFieldsId = memoryRegionId> +type boxedLocationsId = memoryRegionId +type arraysId = memoryRegionId> +type arrayLengthsId = memoryRegionId> +type arrayLowerBoundsId = memoryRegionId> + +type dictionariesId<'key when 'key : equality> = memoryRegionId, productRegion> +type boolDictionariesId = dictionariesId +type byteDictionariesId = dictionariesId +type sbyteDictionariesId = dictionariesId +type charDictionariesId = dictionariesId +type decimalDictionariesId = dictionariesId +type doubleDictionariesId = dictionariesId +type intDictionariesId = dictionariesId +type uintDictionariesId = dictionariesId +type longDictionariesId = dictionariesId +type ulongDictionariesId = dictionariesId +type shortDictionariesId = dictionariesId +type ushortDictionariesId = dictionariesId +type addrDictionariesId = memoryRegionId> + +type dictionaryKeysId<'key when 'key : equality> = memoryRegionId, productRegion> +type boolDictionaryKeysId = dictionaryKeysId +type byteDictionaryKeysId = dictionaryKeysId +type sbyteDictionaryKeysId = dictionaryKeysId +type charDictionaryKeysId = dictionaryKeysId +type decimalDictionaryKeysId = dictionaryKeysId +type doubleDictionaryKeysId = dictionaryKeysId +type intDictionaryKeysId = dictionaryKeysId +type uintDictionaryKeysId = dictionaryKeysId +type longDictionaryKeysId = dictionaryKeysId +type ulongDictionaryKeysId = dictionaryKeysId +type shortDictionaryKeysId = dictionaryKeysId +type ushortDictionaryKeysId = dictionaryKeysId +type addrDictionaryKeysId = memoryRegionId> +type dictionaryCountsId = memoryRegionId + +type setsId<'key when 'key : equality> = memoryRegionId, productRegion> +type boolSetsId = setsId +type byteSetsId = setsId +type sbyteSetsId = setsId +type charSetsId = setsId +type decimalSetsId = setsId +type doubleSetsId = setsId +type intSetsId = setsId +type uintSetsId = setsId +type longSetsId = setsId +type ulongSetsId = setsId +type shortSetsId = setsId +type ushortSetsId = setsId +type addrSetsId = memoryRegionId> +type setCountsId = memoryRegionId + +type listsId = memoryRegionId> +type listCountsId = memoryRegionId + +module MemoryRegionId = + let createStackBuffersId id : stackBuffersId = { id = id; sort = StackBuffersSort } + let createClassFieldsId id : classFieldsId = { id = id; sort = ClassFieldsSort } + let createStaticFieldsId id : staticFieldsId = { id = id; sort = StaticFieldsSort } + let createBoxedLocationsId id : boxedLocationsId = { id = id; sort = BoxedLocationsSort} + let createArraysId id : arraysId = { id = id; sort = ArraysSort } + let createArrayLengthsId id : arrayLengthsId = { id = id; sort = ArrayLengthsSort } + let createArrayLowerBoundsId id : arrayLowerBoundsId = { id = id; sort = ArrayLowerBoundsSort } + let createDictionariesId = function + | BoolDictionary dt -> ({ id = dt; sort = BoolDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | ByteDictionary dt -> ({ id = dt; sort = ByteDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | SByteDictionary dt -> ({ id = dt; sort = SByteDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | CharDictionary dt -> ({ id = dt; sort = CharDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | DecimalDictionary dt -> ({ id = dt; sort = DecimalDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | DoubleDictionary dt -> ({ id = dt; sort = DoubleDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | IntDictionary dt -> ({ id = dt; sort = IntDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | UIntDictionary dt -> ({ id = dt; sort = UIntDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | LongDictionary dt -> ({ id = dt; sort = LongDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | ULongDictionary dt -> ({ id = dt; sort = ULongDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | ShortDictionary dt -> ({ id = dt; sort = ShortDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | UShortDictionary dt -> ({ id = dt; sort = UShortDictionariesSort } : dictionaryKeysId) :> IMemoryRegionId + | AddrDictionary dt -> ({ id = dt; sort = AddrDictionariesSort } : addrDictionariesId) :> IMemoryRegionId + | dt -> internalfail $"Create dictionaries id: unexpected key type {dt.keyType}" + let createDictionaryKeysId = function + | BoolDictionary dt -> ({ id = dt; sort = BoolDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | ByteDictionary dt -> ({ id = dt; sort = ByteDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | SByteDictionary dt -> ({ id = dt; sort = SByteDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | CharDictionary dt -> ({ id = dt; sort = CharDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | DecimalDictionary dt -> ({ id = dt; sort = DecimalDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | DoubleDictionary dt -> ({ id = dt; sort = DoubleDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | IntDictionary dt -> ({ id = dt; sort = IntDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | UIntDictionary dt -> ({ id = dt; sort = UIntDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | LongDictionary dt -> ({ id = dt; sort = LongDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | ULongDictionary dt -> ({ id = dt; sort = ULongDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | ShortDictionary dt -> ({ id = dt; sort = ShortDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | UShortDictionary dt -> ({ id = dt; sort = UShortDictionaryKeysSort } : dictionaryKeysId) :> IMemoryRegionId + | AddrDictionary dt -> ({ id = dt; sort = AddrDictionaryKeysSort } : addrDictionaryKeysId) :> IMemoryRegionId + | dt -> internalfail $"Create DictionaryKeys id: unexpected key type {dt.keyType}" + let createDictionaryCountsId id : dictionaryCountsId = { id = id; sort = DictionaryCountsSort } + let createSetsId = function + | BoolSet st -> ({ id = st; sort = BoolSetsSort } : setsId):> IMemoryRegionId + | ByteSet st -> ({ id = st; sort = ByteSetsSort } : setsId):> IMemoryRegionId + | SByteSet st -> ({ id = st; sort = SByteSetsSort } : setsId):> IMemoryRegionId + | CharSet st -> ({ id = st; sort = CharSetsSort } : setsId):> IMemoryRegionId + | DecimalSet st -> ({ id = st; sort = DecimalSetsSort } : setsId):> IMemoryRegionId + | DoubleSet st ->({ id = st; sort = DoubleSetsSort } : setsId):> IMemoryRegionId + | IntSet st -> ({ id = st; sort = IntSetsSort } : setsId):> IMemoryRegionId + | UIntSet st -> ({ id = st; sort = UIntSetsSort } : setsId):> IMemoryRegionId + | LongSet st -> ({ id = st; sort = LongSetsSort } : setsId):> IMemoryRegionId + | ULongSet st -> ({ id = st; sort = ULongSetsSort } : setsId):> IMemoryRegionId + | ShortSet st -> ({ id = st; sort = ShortSetsSort } : setsId):> IMemoryRegionId + | UShortSet st -> ({ id = st; sort = UShortSetsSort } : setsId):> IMemoryRegionId + | AddrSet st -> ({ id = st; sort = AddrSetsSort } : addrSetsId ):> IMemoryRegionId + | st -> internalfail $"Create Sets id: unexpected key type {st.setValueType}" + let createSetCountsId id : setCountsId = { id = id; sort = SetCountsSort } + let createListsId id : listsId = { id = id; sort = ListsSort } + let createListCountsId id : listCountsId = { id = id; sort = ListCountsSort } + type setKeyWrapper<'key when 'key : equality> = {key : 'key} interface IRegionTreeKey> with @@ -806,9 +1115,62 @@ module SymbolicSet = let sb = s |> RegionTree.foldl (fun (sb : StringBuilder) _ -> toString >> sprintf "%s, " >> sb.Append) (StringBuilder().Append "{ ") (if sb.Length > 2 then sb.Remove(sb.Length - 2, 2) else sb).Append(" }").ToString() -type heapRegion = memoryRegion -type arrayRegion = memoryRegion> -type vectorRegion = memoryRegion> -type stackBufferRegion = memoryRegion -type staticsRegion = memoryRegion> type symbolicTypeSet = symbolicSet> + +type stackBuffersRegion = memoryRegion +type classFieldsRegion = memoryRegion +type staticFieldsRegion = memoryRegion> +type boxedLocationsRegion = memoryRegion +type arraysRegion = memoryRegion> +type arrayLengthsRegion = memoryRegion> +type arrayLowerBoundsRegion = memoryRegion> + +type dictionariesRegion<'key when 'key : equality> = memoryRegion, productRegion> +type boolDictionariesRegion = dictionariesRegion +type byteDictionariesRegion = dictionariesRegion +type sbyteDictionariesRegion = dictionariesRegion +type charDictionariesRegion = dictionariesRegion +type decimalDictionariesRegion = dictionariesRegion +type doubleDictionariesRegion = dictionariesRegion +type intDictionariesRegion = dictionariesRegion +type uintDictionariesRegion = dictionariesRegion +type longDictionariesRegion = dictionariesRegion +type ulongDictionariesRegion = dictionariesRegion +type shortDictionariesRegion = dictionariesRegion +type ushortDictionariesRegion = dictionariesRegion +type addrDictionariesRegion = memoryRegion> +type boolDictionaryKeysRegion = dictionariesRegion +type byteDictionaryKeysRegion = dictionariesRegion +type sbyteDictionaryKeysRegion = dictionariesRegion +type charDictionaryKeysRegion = dictionariesRegion +type decimalDictionaryKeysRegion = dictionariesRegion +type doubleDictionaryKeysRegion = dictionariesRegion +type intDictionaryKeysRegion = dictionariesRegion +type uintDictionaryKeysRegion = dictionariesRegion +type longDictionaryKeysRegion = dictionariesRegion +type ulongDictionaryKeysRegion = dictionariesRegion +type shortDictionaryKeysRegion = dictionariesRegion +type ushortDictionaryKeysRegion = dictionariesRegion +type addrDictionaryKeysRegion = memoryRegion> + +type dictionaryCountsRegion = memoryRegion + +type setsRegion<'key when 'key : equality> = memoryRegion, productRegion> +type boolSetsRegion = setsRegion +type byteSetsRegion = setsRegion +type sbyteSetsRegion = setsRegion +type charSetsRegion = setsRegion +type decimalSetsRegion = setsRegion +type doubleSetsRegion = setsRegion +type intSetsRegion = setsRegion +type uintSetsRegion = setsRegion +type longSetsRegion = setsRegion +type ulongSetsRegion = setsRegion +type shortSetsRegion = setsRegion +type ushortSetsRegion = setsRegion +type addrSetsRegion = memoryRegion> + +type setCountsRegion = memoryRegion + +type listsRegion = memoryRegion> +type listCountsRegion = memoryRegion diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index 6950e4b28..e4830ce9a 100644 --- a/VSharp.SILI.Core/State.fs +++ b/VSharp.SILI.Core/State.fs @@ -164,19 +164,7 @@ and IMemory = abstract Stack : callStack with get, set - abstract StackBuffers : pdict with get, set - - abstract ClassFields : pdict with get, set - - abstract Arrays : pdict with get, set - - abstract Lengths : pdict with get, set - - abstract LowerBounds : pdict with get, set - - abstract StaticFields : pdict with get, set - - abstract BoxedLocations : pdict with get, set + abstract MemoryRegions : pdict with get, set abstract ConcreteMemory : ConcreteMemory @@ -223,6 +211,16 @@ and IMemory = abstract ReadStaticField : Type -> fieldId -> term + abstract ReferenceKey : term -> term -> Type -> term + abstract DictionaryKeyContains : term -> term -> Type -> term + abstract DictionaryCount : term -> Type -> term + + abstract SetKey : term -> term -> Type -> term + abstract SetCount : term -> Type -> term + + abstract ListIndex : term -> term -> Type -> term + abstract ListCount : term -> Type -> term + abstract Read : IErrorReporter -> term -> term abstract ObjToTerm : Type -> obj -> term @@ -251,6 +249,10 @@ and IMemory = abstract WriteArrayIndex : term -> term list -> arrayType -> term -> unit + abstract ListRemoveAt : term -> term -> listType -> term -> unit + abstract ListInsertIndex : term -> term -> term -> listType -> term -> unit + abstract ListCopyToRange : term -> term -> term -> term -> term -> listType -> arrayType -> unit + abstract WriteArrayRange : term -> term list -> term list -> arrayType -> term -> unit abstract WriteStaticField : Type -> fieldId -> term -> unit @@ -370,6 +372,14 @@ and member x.SubstituteTypeVariablesIntoArrayType ({elemType = et} as arrayType) : arrayType = { arrayType with elemType = x.SubstituteTypeVariables et } + member x.SubstituteTypeVariablesIntoDictionaryType { keyType = kt; valueType = vt } : dictionaryType = + { keyType = x.SubstituteTypeVariables kt; valueType = x.SubstituteTypeVariables vt } + + member x.SubstituteTypeVariablesIntoSetType { setValueType = vt } : setType = + { setValueType = x.SubstituteTypeVariables vt } + + member x.SubstituteTypeVariablesIntoListType { listValueType = lt } : listType = + { listValueType = x.SubstituteTypeVariables lt } member x.TypeVariableSubst (t : Type) = x.CommonTypeVariableSubst t t member x.SubstituteTypeVariablesIntoField (f : fieldId) = @@ -445,6 +455,12 @@ and member private x.SortVectorTime<'a> vts : (vectorTime * 'a) seq = Seq.sortWith (fun (k1, _ ) (k2, _ ) -> VectorTime.compare k1 k2) vts + member private x.MemoryRegionIdToString (id : IMemoryRegionId) = + id.ToString() + + member private x.MemoryRegionToString (reg : IMemoryRegion) = + reg.ToString() + member x.Dump () = // TODO: print lower bounds? let sortBy sorter = Seq.sortBy (fst >> sorter) @@ -452,11 +468,8 @@ and let sb = StringBuilder() let sb = (if PC.isEmpty x.pc then sb else x.pc |> PC.toString |> sprintf "Path condition: %s" |> PrettyPrinting.appendLine sb) - |> x.DumpDict "Fields" (sortBy toString) toString (MemoryRegion.toString " ") memory.ClassFields - |> x.DumpDict "Array contents" (sortBy x.ArrayTypeToString) x.ArrayTypeToString (MemoryRegion.toString " ") memory.Arrays - |> x.DumpDict "Array lengths" (sortBy x.ArrayTypeToString) x.ArrayTypeToString (MemoryRegion.toString " ") memory.Lengths + |> x.DumpDict "Memory regions" (sortBy x.MemoryRegionIdToString) x.MemoryRegionIdToString x.MemoryRegionToString memory.MemoryRegions |> x.DumpDict "Types tokens" x.SortVectorTime VectorTime.print toString memory.AllocatedTypes - |> x.DumpDict "Static fields" (sortBy toString) toString (MemoryRegion.toString " ") memory.StaticFields |> x.DumpDict "Delegates" x.SortVectorTime VectorTime.print toString memory.Delegates |> x.DumpStack memory.Stack |> x.DumpInitializedTypes x.initializedTypes diff --git a/VSharp.SILI.Core/Substitution.fs b/VSharp.SILI.Core/Substitution.fs index 892857407..b4b5e4c05 100644 --- a/VSharp.SILI.Core/Substitution.fs +++ b/VSharp.SILI.Core/Substitution.fs @@ -15,6 +15,11 @@ module Substitution = termSubst addr (fun addr' -> Cps.List.mapk termSubst index (fun index' -> ArrayIndex(addr', index', arrayType) |> k)) + | DictionaryKey(addr, key, ({valueType = valueType} as dictionaryType)) -> + let dictionaryType = { dictionaryType with valueType = typeSubst valueType } + termSubst addr (fun addr' -> + termSubst key (fun key' -> + DictionaryKey(addr', key', dictionaryType) |> k)) | StructField(addr, field) -> substituteAddress termSubst typeSubst addr (fun addr' -> StructField(addr', field) |> k) @@ -24,6 +29,10 @@ module Substitution = termSubst addr (fun addr' -> termSubst dim (fun dim' -> ArrayLength(addr', dim', arrayType) |> k)) + | DictionaryCount(addr, ({valueType = valueType} as dictionaryType)) -> + let dictionaryType = { dictionaryType with valueType = typeSubst valueType } + termSubst addr (fun addr' -> + DictionaryCount(addr', dictionaryType) |> k) | BoxedLocation(addr, typ) -> termSubst addr (fun addr' -> BoxedLocation(addr', typeSubst typ) |> k) diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 756fe8b27..50a67161e 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -88,6 +88,21 @@ type stackKey = type concreteHeapAddress = vectorTime +type collectionKey = + | CKBool of bool + | CKByte of byte + | CKSByte of sbyte + | CKChar of char + | CKDecimal of decimal + | CKDouble of double // float = double + | CKInt of int + | CKUInt of uint + | CKLong of int64 + | CKULong of uint64 + | CKShort of int16 + | CKUShort of uint16 + | CKAddr of concreteHeapAddress + type arrayType = { elemType : Type; dimension : int; isVector : bool } with @@ -100,6 +115,120 @@ type arrayType = member x.IsCharVector = x.IsVector && x.elemType = typeof +type dictionaryType = + { keyType : Type; valueType : Type } + with + static member CreateDictionary keyType valueType = + { keyType = keyType; valueType = valueType } + +module DictionaryType = + let (|BoolDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|ByteDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|SByteDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|CharDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|DecimalDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|DoubleDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|IntDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|UIntDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|LongDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|ULongDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|ShortDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|UShortDictionary|_|) = function + | (dt : dictionaryType) when dt.keyType = typeof -> Some dt + | _ -> None + let (|AddrDictionary|_|) (dt : dictionaryType) = + match dt.keyType with + | ReferenceType -> Some dt + | _ -> None + +type setType = + { setValueType : Type } + with + static member CreateSet valueType = + { setValueType = valueType } + +module SetType = + let (|BoolSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|ByteSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|SByteSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|CharSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|DecimalSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|DoubleSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|IntSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|UIntSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|LongSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|ULongSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|ShortSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|UShortSet|_|) = function + | (st : setType) when st.setValueType = typeof -> Some st + | _ -> None + + let (|AddrSet|_|) (st : setType) = + match st.setValueType with + | ReferenceType -> Some st + | _ -> None + +type listType = + { listValueType : Type } + with + static member CreateList valueType = + { listValueType = valueType } + [] type operation = | Operator of OperationType @@ -256,6 +385,13 @@ and address = | ArrayIndex of heapAddress * term list * arrayType | ArrayLowerBound of heapAddress * term * arrayType | ArrayLength of heapAddress * term * arrayType + | DictionaryKey of heapAddress * term * dictionaryType + | DictionaryCount of heapAddress * dictionaryType + | DictionaryHasKey of heapAddress * term * dictionaryType + | SetKey of heapAddress * term * setType + | SetCount of heapAddress * setType + | ListIndex of heapAddress * term * listType + | ListCount of heapAddress * listType | StaticField of Type * fieldId override x.ToString() = match x with @@ -268,6 +404,13 @@ and address = | BoxedLocation(addr, typ) -> $"{typ}^{addr}" | StackBufferIndex(key, idx) -> $"{key}[{idx}]" | ArrayLowerBound(addr, dim, _) -> $"LowerBound({addr}, {dim})" + | DictionaryKey (addr, key, typ) -> $"{addr}<{typ.keyType},{typ.valueType}>[{key}]" + | DictionaryCount (addr, typ) -> $"Length({addr}<{typ.keyType},{typ.valueType}>)" + | DictionaryHasKey(addr, key, typ) -> $"HasKey({addr}<{typ.keyType},{typ.valueType}>[{key}])" + | SetKey(addr, item, typ) -> $"{addr}<{typ.setValueType}>[{item}]" + | SetCount(addr, typ) -> $"Length({addr}<{typ.setValueType}>)" + | ListIndex(addr, idx, typ) -> $"{addr}<{typ.listValueType}[{idx}]" + | ListCount(addr, typ) -> $"Length({addr}<{typ.listValueType}>)" member x.Zone() = match x with | PrimitiveStackLocation _ @@ -276,7 +419,14 @@ and address = | ArrayIndex _ | ArrayLength _ | BoxedLocation _ - | ArrayLowerBound _ -> "Heap" + | ArrayLowerBound _ + | DictionaryKey _ + | DictionaryCount _ + | DictionaryHasKey _ + | SetKey _ + | SetCount _ + | ListIndex _ + | ListCount _ -> "Heap" | StaticField _ -> "Statics" | StructField(addr, _) -> addr.Zone() member x.TypeOfLocation with get() = @@ -285,9 +435,16 @@ and address = | StructField(_, field) | StaticField(_, field) -> field.typ | ArrayIndex(_, _, { elemType = elementType }) -> elementType + | DictionaryKey(_, _, typ) -> typ.valueType + | ListIndex(_, _, typ) -> typ.listValueType + | DictionaryHasKey _ + | SetKey _ -> typeof | BoxedLocation(_, typ) -> typ | ArrayLength _ - | ArrayLowerBound _ -> lengthType + | ArrayLowerBound _ + | DictionaryCount _ + | ListCount _ + | SetCount _ -> lengthType | StackBufferIndex _ -> typeof | PrimitiveStackLocation loc -> loc.TypeOfLocation @@ -346,7 +503,10 @@ module internal Terms = // --------------------------------------- Primitives --------------------------------------- let Nop() = HashMap.addTerm Nop - let Concrete obj typ = HashMap.addTerm (Concrete(obj, typ)) + let Concrete (obj : obj) typ = + assert (not <| obj :? term) + HashMap.addTerm (Concrete(obj, typ)) + let Constant name source typ = HashMap.addTerm (Constant({v=name}, source, typ)) let Expression op args typ = HashMap.addTerm (Expression(op, args, typ)) let Struct fields typ = HashMap.addTerm (Struct(fields, typ)) @@ -371,7 +531,7 @@ module internal Terms = let makeNullPtr typ = Ptr (HeapLocation(zeroAddress(), typ)) typ (makeNumber 0) - + let True() = Concrete (box true) typeof let IteAsGvs iteType = iteType.branches @ [(True(), iteType.elseValue)] @@ -435,7 +595,7 @@ module internal Terms = | term -> internalfail $"struct or class expected, {term} received" let private typeOfIte (getType : 'a -> Type) (iteType : iteType) = - let types = iteType.mapValues getType + let types = iteType.mapValues getType match types with | {branches = []; elseValue = _} -> __unreachable__() | {branches = branches; elseValue = elset} -> @@ -489,6 +649,21 @@ module internal Terms = | SymbolicDimension -> __insufficientInformation__ "Cannot process array of unknown dimension!" | typ -> internalfail $"symbolicTypeToArrayType: expected array type, but got {typ}" + let symbolicTypeToDictionaryType = function + | DictionaryType(keyType, valueType) -> + { keyType = keyType; valueType = valueType } + | typ -> internalfail $"symbolicTypeToDictionaryType: expected dictionary type, but got {typ}" + + let symbolicTypeToSetType = function + | SetType(valueType) -> + { setValueType = valueType } + | typ -> internalfail $"symbolicTypeToSetType: expected set type, but got {typ}" + + let symbolicTypeToListType = function + | ListType(valueType) -> + { listValueType = valueType } + | typ -> internalfail $"symbolicTypeToListType: expected list type, but got {typ}" + let arrayTypeToSymbolicType arrayType = if arrayType.isVector then arrayType.elemType.MakeArrayType() else arrayType.elemType.MakeArrayType(arrayType.dimension) @@ -770,6 +945,49 @@ module internal Terms = | _ -> None Cps.List.foldrk addElement List.empty termList Some + and tryIntFromTerm (term : term) = + match term.term with + | Concrete(:? int16 as i, _) -> Some <| int i + | Concrete(:? uint16 as i, _) -> Some <| int i + | Concrete(:? char as i, _) -> Some <| int i + | Concrete(:? int as i, _) -> Some i + | Concrete(:? uint as i, _) -> Some <| int i + | Concrete(:? int64 as i, _) -> Some <| int i + | Concrete(:? uint64 as i, _) -> Some <| int i + | _ -> None + + and tryCollectionKeyFromTerm (term : term) = + match term.term with + | Concrete(:? bool as value, _) -> Some <| CKBool value + | Concrete(:? byte as value, _) -> Some <| CKByte value + | Concrete(:? sbyte as value, _) -> Some <| CKSByte value + | Concrete(:? char as value, _) -> Some <| CKChar value + | Concrete(:? decimal as value, _) -> Some <| CKDecimal value + | Concrete(:? double as value, _) -> Some <| CKDouble value + | Concrete(:? int as value, _) -> Some <| CKInt value + | Concrete(:? uint as value, _) -> Some <| CKUInt value + | Concrete(:? int64 as value, _) -> Some <| CKLong value + | Concrete(:? uint64 as value, _) -> Some <| CKULong value + | Concrete(:? int16 as value, _) -> Some <| CKShort value + | Concrete(:? uint16 as value, _) -> Some <| CKUShort value + | Concrete(:? concreteHeapAddress as value, _) -> Some <| CKAddr value + | _ -> None + + and collectionKeyValueToObj = function + | CKBool value -> value :> obj + | CKByte value -> value :> obj + | CKSByte value -> value :> obj + | CKChar value -> value :> obj + | CKDecimal value -> value :> obj + | CKDouble value -> value :> obj + | CKInt value -> value :> obj + | CKUInt value -> value :> obj + | CKLong value -> value :> obj + | CKULong value -> value :> obj + | CKShort value -> value :> obj + | CKUShort value -> value :> obj + | CKAddr value -> value :> obj + and isConcreteHeapAddress term = match term.term with | ConcreteHeapAddress _ -> true @@ -1096,11 +1314,25 @@ module internal Terms = | ArrayIndex(addr, indices, _) -> doFold folder state addr (fun state -> foldList folder indices state k) + | DictionaryKey(addr, key, _) -> + doFold folder state addr (fun state -> + doFold folder state key k) + | ListIndex(addr, idx, _) -> + doFold folder state addr (fun state -> + doFold folder state idx k) + | DictionaryHasKey(addr, item, _) + | SetKey(addr, item, _) -> + doFold folder state addr (fun state -> + doFold folder state item k) | StructField(addr, _) -> foldAddress folder state addr k | ArrayLength(addr, idx, _) | ArrayLowerBound(addr, idx, _) -> doFold folder state addr (fun state -> doFold folder state idx k) + | DictionaryCount(addr, _) + | SetCount(addr, _) + | ListCount(addr, _) -> + doFold folder state addr k | StackBufferIndex(_, idx) -> doFold folder state idx k and foldPointerBase folder state pointerBase k = diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index cc781868d..0cd191d3f 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -539,6 +539,7 @@ 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 InvalidOperationException : cilState -> unit abstract NullReferenceException : cilState -> unit abstract ArgumentException : cilState -> unit abstract ArgumentNullException : cilState -> unit @@ -1881,6 +1882,8 @@ type ILInterpreter() as this = member x.InvalidProgramException cilState = x.CreateException typeof [] cilState + member x.InvalidOperationException cilState = + x.CreateException typeof [] cilState member x.NullReferenceException cilState = x.CreateException typeof [] cilState member x.ArgumentException cilState = @@ -2395,6 +2398,7 @@ type ILInterpreter() as this = override x.NpeOrInvoke cilState ref statement k = x.NpeOrInvokeStatementCIL cilState ref statement k override x.InvalidProgramException cilState = x.InvalidProgramException cilState + override x.InvalidOperationException cilState = x.InvalidOperationException cilState override x.NullReferenceException cilState = x.NullReferenceException cilState override x.ArgumentException cilState = x.ArgumentException cilState override x.ArgumentNullException cilState = x.ArgumentNullException cilState diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 35a4385ee..105f7a3c9 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -7,6 +7,7 @@ open System.Collections.Generic open VSharp open VSharp.TypeUtils open VSharp.Core +open VSharp.Core.API.Types open VSharp.Core.API.Memory open VSharp.Core.SolverInteraction @@ -869,7 +870,7 @@ module internal Z3 = (x.MkITE(guard :?> BoolExpr, value, prevIte), assumptions) |> k Cps.List.foldrk constructUnion (elseValue, []) iteType.branches (fun (ite, assumptions) -> {expr = ite; assumptions = assumptions}) - + member private x.EncodeExpression term op args typ = encodingCache.Get(term, fun () -> match op with @@ -1020,6 +1021,9 @@ module internal Z3 = let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo match regionSort with | HeapFieldSort field when field = Reflection.stringLengthField -> x.GenerateLengthAssumptions res + | SetCountSort _ + | DictionaryCountSort _ + | ListCountSort _ -> x.GenerateLengthAssumptions res | _ -> res // Generating assumptions for instantiation @@ -1074,6 +1078,112 @@ module internal Z3 = | ArrayLengthSort _ -> x.GenerateLengthAssumptions res | _ -> res + member private x.DictionaryReading<'key when 'key : equality> + (keysAreMatch : heapCollectionKey<'key> -> heapCollectionKey<'key> -> productRegion, points<'key>> -> BoolExpr list * BoolExpr) + encodeKey + hasDefaultValue + (key : heapCollectionKey<'key>) + mo + typ + source + path + name + = + assert mo.defaultValue.IsNone + let inst (k : Expr[]) = + let domainSort = [|x.Type2Sort addressType; x.Type2Sort typeof<'key>|] + let valueSort = x.Type2Sort typ + if hasDefaultValue then x.DefaultValue valueSort, List.empty + else + let regionSort = GetHeapReadingRegionSort source + let sort = ctx.MkArraySort(domainSort, valueSort) + let array = x.GetRegionConstant name sort path regionSort + if containsAddress typ then + addRegionAccess regionSort path k + let expr = ctx.MkSelect(array, k) + expr, x.GenerateInstAssumptions expr typ + let specialize v _ _ = v + let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo + let res = if typ = typeof then x.GenerateCharAssumptions res else res + res + // TODO: Counts Assumptions + + member private x.AddrDictionaryReading keysAreMatch encodeKey hasDefaultValue key mo typ source path name = + assert mo.defaultValue.IsNone + let inst (k : Expr[]) = + let domainSort = [|x.Type2Sort addressType; x.Type2Sort addressType|] + let valueSort = x.Type2Sort typ + if hasDefaultValue then x.DefaultValue valueSort, List.empty + else + let regionSort = GetHeapReadingRegionSort source + let sort = ctx.MkArraySort(domainSort, valueSort) + let array = x.GetRegionConstant name sort path regionSort + if containsAddress typ then + addRegionAccess regionSort path k + let expr = ctx.MkSelect(array, k) + expr, x.GenerateInstAssumptions expr typ + let specialize v _ _ = v + let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo + let res = if typ = typeof then x.GenerateCharAssumptions res else res + res + // TODO: Counts Assumptions + + member private x.SetReading<'key when 'key : equality> + (keysAreMatch : heapCollectionKey<'key> -> heapCollectionKey<'key> -> productRegion, points<'key>> -> BoolExpr list * BoolExpr) + encodeKey + hasDefaultValue + (key : heapCollectionKey<'key>) + mo + typ + source + path + name + = + assert mo.defaultValue.IsNone + let inst (k : Expr[]) = + let domainSort = [|x.Type2Sort addressType; x.Type2Sort typeof<'key>|] + let valueSort = x.Type2Sort typeof + if hasDefaultValue then x.DefaultValue valueSort, List.empty + else + let regionSort = GetHeapReadingRegionSort source + let sort = ctx.MkArraySort(domainSort, valueSort) + let array = x.GetRegionConstant name sort path regionSort + if containsAddress typ then + addRegionAccess regionSort path k + let expr = ctx.MkSelect(array, k) + expr, x.GenerateInstAssumptions expr typ + let specialize v _ _ = v + let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo + res + + member private x.AddrSetReading + (keysAreMatch : addrCollectionKey -> addrCollectionKey-> productRegion, intervals> -> BoolExpr list * BoolExpr) + encodeKey + hasDefaultValue + (key : addrCollectionKey) + mo + typ + source + path + name + = + assert mo.defaultValue.IsNone + let inst (k : Expr[]) = + let domainSort = [|x.Type2Sort addressType; x.Type2Sort addressType|] + let valueSort = x.Type2Sort typeof + if hasDefaultValue then x.DefaultValue valueSort, List.empty + else + let regionSort = GetHeapReadingRegionSort source + let sort = ctx.MkArraySort(domainSort, valueSort) + let array = x.GetRegionConstant name sort path regionSort + if containsAddress typ then + addRegionAccess regionSort path k + let expr = ctx.MkSelect(array, k) + expr, x.GenerateInstAssumptions expr typ + let specialize v _ _ = v + let res = x.MemoryReading specialize keysAreMatch encodeKey inst path key mo + res + member private x.ArrayIndexReading key hasDefaultValue mo typ source path name = let encodeKey = function | OneArrayIndexKey(address, indices) -> address :: indices |> x.EncodeTerms @@ -1088,6 +1198,38 @@ module internal Z3 = | _ -> internalfail $"EncodeMemoryAccessConstant: unexpected array key {key}" x.ArrayReading SpecializeWithKey keysAreMatch encodeKey hasDefaultValue indices key mo typ source path name + member private x.DictionaryKeyReading<'key when 'key : equality> (key : heapCollectionKey<'key>) hasDefaultValue mo typ source path name = + let encodeKey ({address = address; key = key} : heapCollectionKey<'key>) = [address; key] |> x.EncodeTerms + let keysAreMatch read update updateRegion = + let matchCondition = (read :> IMemoryKey<'a,'b>).MatchCondition update updateRegion + let {expr = matchConditionEncoded; assumptions = assumptions} = x.EncodeTerm matchCondition + assumptions, matchConditionEncoded :?> BoolExpr + x.DictionaryReading<'key> keysAreMatch encodeKey hasDefaultValue key mo typ source path name + + member private x.AddrDictionaryKeyReading (key : addrCollectionKey) hasDefaultValue mo typ source path name = + let encodeKey ({address = address; key = key} : addrCollectionKey) = [address; key] |> x.EncodeTerms + let keysAreMatch read update updateRegion = + let matchCondition = (read :> IMemoryKey<'a,'b>).MatchCondition update updateRegion + let {expr = matchConditionEncoded; assumptions = assumptions} = x.EncodeTerm matchCondition + assumptions, matchConditionEncoded :?> BoolExpr + x.AddrDictionaryReading keysAreMatch encodeKey hasDefaultValue key mo typ source path name + + member private x.SetKeyReading<'key when 'key : equality> (key : heapCollectionKey<'key>) hasDefaultValue mo typ source path name = + let encodeKey ({address = address; key = item} : heapCollectionKey<'key>) = [address; item] |> x.EncodeTerms + let keysAreMatch read update updateRegion = + let matchCondition = (read :> IMemoryKey<'a,'b>).MatchCondition update updateRegion + let {expr = matchConditionEncoded; assumptions = assumptions} = x.EncodeTerm matchCondition + assumptions, matchConditionEncoded :?> BoolExpr + x.SetReading<'key> keysAreMatch encodeKey hasDefaultValue key mo typ source path name + + member private x.AddrSetKeyReading (key : addrCollectionKey) hasDefaultValue mo typ source path name = + let encodeKey ({address = address; key = item} : addrCollectionKey) = [address; item] |> x.EncodeTerms + let keysAreMatch read update updateRegion = + let matchCondition = (read :> IMemoryKey<'a,'b>).MatchCondition update updateRegion + let {expr = matchConditionEncoded; assumptions = assumptions} = x.EncodeTerm matchCondition + assumptions, matchConditionEncoded :?> BoolExpr + x.AddrSetReading keysAreMatch encodeKey hasDefaultValue key mo typ source path name + member private x.VectorIndexReading (key : heapVectorIndexKey) hasDefaultValue mo typ source path name = let encodeKey (k : heapVectorIndexKey) = x.EncodeTerms [|k.address; k.index|] @@ -1156,6 +1298,58 @@ module internal Z3 = | HeapReading(key, mo) -> x.HeapReading key mo typ source path name | ArrayIndexReading(hasDefaultValue, key, mo) -> x.ArrayIndexReading key hasDefaultValue mo typ source path name + | BoolDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | ByteDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | SByteDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | CharDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | DecimalDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | DoubleDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | IntDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | UIntDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | LongDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | ULongDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | ShortDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | UShortDictionaryReading(hasDefaultValue, key, mo) -> + x.DictionaryKeyReading key hasDefaultValue mo typ source path name + | AddrDictionaryReading(hasDefaultValue, key, mo) -> + x.AddrDictionaryKeyReading key hasDefaultValue mo typ source path name + | BoolSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | ByteSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | SByteSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | CharSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | DecimalSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | DoubleSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | IntSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | UIntSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | LongSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | ULongSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | ShortSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | UShortSetReading(hasDefaultValue, key, mo) -> + x.SetKeyReading key hasDefaultValue mo typ source path name + | AddrSetReading(hasDefaultValue, key, mo) -> + x.AddrSetKeyReading key hasDefaultValue mo typ source path name | VectorIndexReading(hasDefaultValue, key, mo) -> x.VectorIndexReading key hasDefaultValue mo typ source path name | StackBufferReading(key, mo) -> x.StackBufferReading key mo typ source path name @@ -1223,11 +1417,58 @@ module internal Z3 = let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress let indices = exprs |> Seq.tail |> Seq.map (x.Decode Types.IndexType) |> List.ofSeq ArrayIndex(heapAddress, indices, typ) + | DictionaryKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let key = x.Decode typ.keyType exprs[1] + DictionaryKey(heapAddress, key, typ) + | AddrDictionaryKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let key = x.Decode addressType exprs[1] + DictionaryKey(heapAddress, key, typ) + | DictionaryHasKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let key = x.Decode typ.keyType exprs[1] + DictionaryHasKey(heapAddress, key, typ) + | AddrDictionaryHasKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let key = x.Decode typ.keyType exprs[1] + DictionaryHasKey(heapAddress, key, typ) + | SetKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let item = x.Decode typ.setValueType exprs[1] + SetKey(heapAddress, item, typ) + | AddrSetKeySort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let item = x.Decode addressType exprs[1] + SetKey(heapAddress, item, typ) + | ListIndexSort typ -> + assert(exprs.Length = 2) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + let index = x.Decode typeof exprs[1] + ListIndex(heapAddress, index, typ) | ArrayLengthSort typ -> assert(exprs.Length = 2) let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress let index = x.Decode Types.IndexType exprs[1] ArrayLength(heapAddress, index, typ) + | DictionaryCountSort typ -> + assert(exprs.Length = 1) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + DictionaryCount(heapAddress, typ) + | SetCountSort typ -> + assert(exprs.Length = 1) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + SetCount(heapAddress, typ) + | ListCountSort typ -> + assert(exprs.Length = 1) + let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress + ListCount(heapAddress, typ) | ArrayLowerBoundSort typ -> assert(exprs.Length = 2) let heapAddress = x.DecodeConcreteHeapAddress exprs[0] |> ConcreteHeapAddress @@ -1356,7 +1597,17 @@ module internal Z3 = | HeapFieldSort field -> FillClassFieldsRegion state field constantValue | StaticFieldSort typ -> FillStaticsRegion state typ constantValue | ArrayIndexSort arrayType -> FillArrayRegion state arrayType constantValue + | DictionaryKeySort dictionaryType -> FillDictionaryRegion state dictionaryType constantValue + | AddrDictionaryKeySort dictionaryType -> FillAddrDictionaryRegion state dictionaryType constantValue + | DictionaryHasKeySort dictionaryType -> FillDictionaryKeysRegion state dictionaryType constantValue + | AddrDictionaryHasKeySort dictionaryType -> FillAddrDictionaryKeysRegion state dictionaryType constantValue + | SetKeySort setType -> FillSetRegion state setType constantValue + | AddrSetKeySort setType -> FillAddrSetRegion state setType constantValue + | ListIndexSort listType -> FillListRegion state listType constantValue | ArrayLengthSort arrayType -> FillLengthRegion state arrayType constantValue + | DictionaryCountSort dictionaryType -> FillDictionaryCountRegion state dictionaryType constantValue + | SetCountSort setType -> FillSetCountRegion state setType constantValue + | ListCountSort listType -> FillListCountRegion state listType constantValue | ArrayLowerBoundSort arrayType -> FillLowerBoundRegion state arrayType constantValue | StackBufferSort key -> FillStackBufferRegion state key constantValue | BoxedSort typ -> FillBoxedRegion state typ constantValue diff --git a/VSharp.Test/Tests/BoxUnbox.cs b/VSharp.Test/Tests/BoxUnbox.cs index b60190d7a..c1343541e 100644 --- a/VSharp.Test/Tests/BoxUnbox.cs +++ b/VSharp.Test/Tests/BoxUnbox.cs @@ -154,17 +154,7 @@ public static bool True3() return x == y; } } - - [TestSvmFixture] - public class UnboxGeneric - { - [TestSvm] - public static T Cast(object o) - { - return (T) o; - } - } - + [TestSvmFixture] [IgnoreFuzzer("(Known bug) Last generated test is incorrect")] public class BoxUnboxWithGeneric diff --git a/VSharp.Test/Tests/Dictionaries.cs b/VSharp.Test/Tests/Dictionaries.cs new file mode 100644 index 000000000..2fb54400f --- /dev/null +++ b/VSharp.Test/Tests/Dictionaries.cs @@ -0,0 +1,247 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using NUnit.Framework; +using VSharp.Test; + +#pragma warning disable CS0108, CS0114, CS0649 + +namespace IntegrationTests +{ + [TestSvmFixture] + public class Dictionaries + { + [TestSvm] + public int SymbolicInitialize(char a, int b) + { + var dict = new Dictionary() + { + {a, 1}, + {'b', 2}, + {'c', b} + }; + return dict['a']; + } + + [TestSvm] + public int SymbolicInitialize2(Dictionary d) + { + d[1] = 1; + return d[1]; + } + + [TestSvm] + public int SymbolicInitialize3(Dictionary d, int a, int b) + { + d[a] = b; + d[2] = 2; + return d[a]; + } + + [TestSvm] + public float Mutate(long i) + { + var dict = new Dictionary() + { + {1L, 1f}, + {2L, 2f}, + {3L, 3f}, + {4L, 4f} + }; + dict[1L] = 40f; + dict[i] = 10f; + return dict[3L]; + } + + [TestSvm] + public float Mutate2(Dictionary dict, long i) + { + dict[i] = 10f; + return dict[3L]; + } + + [TestSvm] + public int SymbolicWriteAfterConcreteWrite(int k) + { + var dict = new Dictionary(); + dict[2] = 42; + dict[k] = 12; + return dict[2]; + } + + [TestSvm] + public int SymbolicWriteAfterConcreteWrite3(Dictionary dict, int k) + { + dict[2] = 42; + dict[k] = 12; + return dict[2]; + } + + [TestSvm] + public Dictionary RetDictionary(bool flag1, bool flag2) + { + var dict = new Dictionary(); + if (flag1) + { + dict[1] = 42; + } + else if (flag2) + { + dict[1] = 89; + } + + return dict; + } + + /*[TestSvm] + public int SymbolicWriteAfterConcreteWrite2(Dictionary d, int k) + { + d[2] = 42; + d[k] = 12; + return d[2]; + } + + [TestSvm] + public int SolverTestDictionaryKey(Dictionary d, int x) + { + d[1] = 12; + d[x] = 12; + if (x != 10) + { + d[10] = 42; + } + + var res = 0; + if (d[x] == 12) + { + res = 1; + } + + return res; + }*/ + + // TODO: see test generator's TODOs + /*[TestSvm] + public static int TestConnectionBetweenKeysAndValues(Dictionary d, int i, int j) + { + int x = d[i]; + int y = d[j]; + int res = 0; + if (i == j && x != y) + res = 1; + return res; + }*/ + + [TestSvm] + public static int LastRecordReachability(Dictionary a, Dictionary b, int i, string s) + { + a[i] = "1"; + b[1] = s; + if (b[1] != s) + { + // unreachable + return -1; + } + + return 0; + } + + [TestSvm] + public static bool DictionarySymbolicUpdate(int i) + { + var dict = new Dictionary() + { + {1, 1}, + {2, 2}, + {3, 3}, + {4, 4}, + {5, 5} + }; + dict[i] = 10; + if (i == 0 && dict[0] != 10) + return false; + else + return true; + } + + [TestSvm] + public static bool DictionarySymbolicUpdate2(int i) + { + var dict = new Dictionary() + { + {1, 1}, + {2, 2}, + {3, 3}, + {4, 4}, + {5, 5} + }; + dict[i] = 10; + dict[0] = 12; + if (i == 0 && dict[0] != 12) + return false; + else + return true; + } + + // TODO: see test generator's TODOs + /*[TestSvm] + public bool CountSymbolicTest(Dictionary dict) + { + if (dict.Count > 0) + { + return true; + } + else + { + return false; + } + } + + [TestSvm] + public bool CountSymbolicTest2(Dictionary dict, char key, int item) + { + dict.Add(key, item); + + if (dict.Count < 1) + { + return false; + } + + return true; + } + + [TestSvm] + public bool CountSymbolicTest3(short key, long item) + { + var dict = new Dictionary() + { + { 1, 1 }, + { 2, 2 }, + { 3, 3 } + }; + + dict.Add(key, item); + dict[key] = item; + + if (dict.Count > 3) + { + return false; + } + else + { + return true; + } + }*/ + + [TestSvm] + public int CountSymbolicTest4(Dictionary dict, short key, long item) + { + dict[key] = item; + dict[key] = item; + dict[key] = item; + + return dict.Count; + } + } +} diff --git a/VSharp.Test/Tests/Generic.cs b/VSharp.Test/Tests/Generic.cs index cf1e11fe7..510b12cd6 100644 --- a/VSharp.Test/Tests/Generic.cs +++ b/VSharp.Test/Tests/Generic.cs @@ -740,9 +740,9 @@ public static class NestedGenerics { [TestSvm(100)] [IgnoreFuzzer("Need recursion constraints in generators")] - public static int NestedGenericsSmokeTest(List> list) + public static int NestedGenericsSmokeTest(Bag[] list) { - if (list.Count > 0) + if (list.Length > 0) { return 0; } @@ -750,7 +750,7 @@ public static int NestedGenericsSmokeTest(List> list) return 1; } - [TestSvm(100)] + /*[TestSvm(100)] [IgnoreFuzzer("Need recursion constraints in generators")] public static int NestedGenericsSmokeTest2(Dictionary> dict) { @@ -760,7 +760,7 @@ public static int NestedGenericsSmokeTest2(Dictionary> dict) } return 1; - } + }*/ } // public static class GenericCast diff --git a/VSharp.Test/Tests/Lists.cs b/VSharp.Test/Tests/Lists.cs index 78d71aebb..cdfdcce4d 100644 --- a/VSharp.Test/Tests/Lists.cs +++ b/VSharp.Test/Tests/Lists.cs @@ -925,13 +925,14 @@ public static int ConcreteDictionaryTest(int v) } [TestSvm(100)] - public static int ConcreteDictionaryTest1(int a, string b) + public static int ConcreteDictionaryTest1(int a, int b) { - var d = new Dictionary>(); - d.Add(1, new List { "2", "3" }); - d.Add(4, new List { "5", "6" }); - if (d.TryGetValue(a, out var res)) + var d = new Dictionary>(); + d.Add(1, new List { 2, 3 }); + d.Add(4, new List { 5, 6 }); + if (d.ContainsKey(a)) { + var res = d[a]; if (res.Contains(b)) return 1; return 0; @@ -945,7 +946,7 @@ public class Person public string FirstName { get; set; } public string LastName { get; init; } }; - + [TestSvm(95)] public static int IteKeyWrite(int i) { @@ -1189,9 +1190,9 @@ public static int ListTest(decimal d1, decimal d2) [TestSvm(100)] [IgnoreFuzzer("Need recursion constraints in generators")] - public static int ListTest1(List l, object e) + public static int ListTest1(object[] l, object e) { - var i = l.LastIndexOf(e); + var i = Array.LastIndexOf(l, e); if (i >= 0) return i; return -1; @@ -1475,14 +1476,14 @@ public static unsafe byte SpanTest(int[] a, byte b, int i) [TestSvmFixture] public class ArrayCopying { - private List _elements; + private int[] _elements; - public int Count => _elements.Count - 1; + public int Count => _elements.Length - 1; [TestSvm(100)] public void CopyTo(int[] array, int arrayIndex) { - _elements.CopyTo(1, array, arrayIndex, Count); + _elements.CopyTo(array, arrayIndex); } } diff --git a/VSharp.Test/Tests/Sets.cs b/VSharp.Test/Tests/Sets.cs new file mode 100644 index 000000000..84a167809 --- /dev/null +++ b/VSharp.Test/Tests/Sets.cs @@ -0,0 +1,188 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using NUnit.Framework; +using VSharp.Test; + +#pragma warning disable CS0108, CS0114, CS0649 + +namespace IntegrationTests +{ + [TestSvmFixture] + public class Sets + { + [TestSvm] + public bool ContainsConcreteTest(HashSet set) + { + return set.Contains(42); + } + + [TestSvm] + public bool ContainsConcreteTest2(int item) + { + var set = new HashSet() { 4 }; + + return set.Contains(item); + } + + [TestSvm] + public bool ContainsConcreteTest3(int item) + { + var set = new HashSet() { 4 }; + set.Add(item); + + return set.Contains(item); + } + + [TestSvm] + public bool ContainsSymbolicTest(HashSet set, int item) + { + return set.Contains(item); + } + + [TestSvm] + public HashSet AddConcreteTest(HashSet set) + { + set.Add(42); + + return set; + } + + [TestSvm] + public HashSet AddConcreteTest2(byte item) + { + var set = new HashSet(); + set.Add(42); + + return set; + } + + [TestSvm] + public HashSet AddSymbolicTest(HashSet set, char item) + { + set.Add(item); + + return set; + } + + [TestSvm] + public HashSet RemoveSymbolicTest(HashSet set, char item) + { + set.Remove(item); + + return set; + } + + // TODO: construct symbolic set with elements from region in test generator + /*[TestSvm] + public bool RemoveConcreteTest(HashSet set) + { + var isRemoved = set.Remove('a'); + + if (isRemoved) + { + return true; + } + + return false; + }*/ + + [TestSvm] + public bool RemoveConcreteTest2(long item) + { + var set = new HashSet() { 1, 2, 3, 4 }; + + return set.Remove(item); + } + + [TestSvm] + public bool CommonSymbolicTest(HashSet set, char item, char item2) + { + set.Add(item); + set.Add(item2); + set.Remove(item); + + return set.Contains(item); + } + + [TestSvm] + public bool CommonSymbolicTest2(HashSet set, char item, char item2) + { + set.Add(item); + set.Add(item2); + set.Remove(item); + + if (set.Contains(item)) + { + return false; + } + + return true; + } + + [TestSvm] + public bool CommonSymbolicTest3(HashSet set, char item, char item2) + { + set.Add(item); + set.Add(item2); + set.Remove('z'); + + return set.Contains(item); + } + + [TestSvm] + public int CountSymbolicTest(HashSet set) + { + return set.Count; + } + + [TestSvm] + public bool CountSymbolicTest2(HashSet set, long item) + { + set.Add(item); + + if (set.Count < 1) + { + return false; + } + + return true; + } + + [TestSvm] + public int CountSymbolicTest3(long item) + { + var set = new HashSet() { 1, 2, 4 }; + + set.Add(item); + set.Add(item); + + return set.Count; + } + + [TestSvm] + public int CountSymbolicTest4(HashSet set, long item) + { + set.Add(item); + set.Add(item); + set.Add(item); + + return set.Count; + } + + [TestSvm] + public bool CountSymbolicTest5(long item) + { + var set = new HashSet() { 3 }; + set.Add(item); + + if (set.Count > 1) + { + return true; + } + + return false; + } + } +} diff --git a/VSharp.Test/Tests/SymbolicLists.cs b/VSharp.Test/Tests/SymbolicLists.cs new file mode 100644 index 000000000..78b842ef5 --- /dev/null +++ b/VSharp.Test/Tests/SymbolicLists.cs @@ -0,0 +1,114 @@ +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using NUnit.Framework; +using VSharp.Test; + +#pragma warning disable CS0108, CS0114, CS0649 + +namespace IntegrationTests +{ + [TestSvmFixture] + public class SymbolicLists + { + [TestSvm] + public bool ConcreteTest(int index) + { + var l = new List() { 'a', 'b', 'c' }; + + l[index] = 'd'; + + if (l[index] == 'd') + { + return true; + } + + return false; + } + + [TestSvm] + public bool ConcreteTest2(int index) + { + var l = new List() { 'a', 'b', 'c' }; + + if (l[index] == 'a') + { + return true; + } + + return false; + } + + [TestSvm] + public bool ConcreteTest3(int index) + { + var l = new List() { 'a', 'b', 'c' }; + + l.RemoveAt(index); + + if (l[index] == 'b') + { + return true; + } + + return false; + } + + [TestSvm] + public bool ConcreteTest4(int remove, int insert) + { + var l = new List() { 'a', 'b', 'c' }; + + l.Insert(insert, 'd'); + l.RemoveAt(remove); + + if (l[2] == 'd') + { + return true; + } + + return false; + } + + [TestSvm] + public bool ConcreteTest5(char item) + { + var l = new List() { 'a', 'b', 'c' }; + + if (l.IndexOf(item) == 1) + { + return true; + } + + return false; + } + + [TestSvm] + public bool ConcreteTest6(char item) + { + var l = new List() { 'a', 'b', 'c' }; + + l.Remove(item); + + if (l.Count > 2) + { + return true; + } + + return false; + } + + [TestSvm] + public int ConcreteMemoryTest(int i) + { + var l = new List(); + l.Add(1); + l.Add(2); + l.Add(i); + if (l[2] != i) + return -1; + return 1; + } + } +} diff --git a/VSharp.TestGenerator/TestGenerator.fs b/VSharp.TestGenerator/TestGenerator.fs index e77b20fd6..75fd88005 100644 --- a/VSharp.TestGenerator/TestGenerator.fs +++ b/VSharp.TestGenerator/TestGenerator.fs @@ -7,6 +7,11 @@ open VSharp open VSharp.Core open System.Linq +// TODO: Count of collection cases (like set.Count < 42 && ...) may generate incorrect tests, +// where count = 1, but set = { 1, 2, ... }. Its necessary to recognize them and generate them in a special way + +// TODO: Generate sets and dictionaries from model like objects + type public testSuite = | Test | Error of string * bool @@ -143,9 +148,9 @@ module TestGenerator = let arrays = if isModelArray then match model with - | StateModel modelState -> modelState.memory.Arrays + | StateModel modelState -> modelState.memory.MemoryRegions | _ -> __unreachable__() - else state.memory.Arrays + else state.memory.MemoryRegions let elemType = arrayType.elemType let checkElem value = match value.term, model with @@ -158,8 +163,10 @@ module TestGenerator = if isModelArray && not elemType.IsValueType then checkElem else fun _ -> true let defaultValue, indices, values = - match PersistentDict.tryFind arrays arrayType with + let key = MemoryRegionId.createArraysId arrayType + match PersistentDict.tryFind arrays key with | Some region -> + let region = region :?> arraysRegion let defaultValue = match region.defaultValue with | Some defaultValue -> encode defaultValue diff --git a/VSharp.Utils/Reflection.fs b/VSharp.Utils/Reflection.fs index 736831229..ddf7aabf0 100644 --- a/VSharp.Utils/Reflection.fs +++ b/VSharp.Utils/Reflection.fs @@ -1,6 +1,7 @@ namespace VSharp open System +open System.Collections open System.Collections.Generic open System.Reflection open System.Reflection.Emit @@ -617,6 +618,16 @@ module public Reflection = let size = byteSize / elemSize reinterpretValueTypeAsArray fieldValue elemType size + // TODO: optimize + let keyAndValueSeqFromDictionaryObj (dict : IDictionary) = + seq { + for obj in dict -> + let typ = obj.GetType() + let k = typ.GetProperty("Key").GetValue(obj) + let v = typ.GetProperty("Value").GetValue(obj) + (k, v) + } + // ------------------------------ Layout Utils ------------------------------ let getFieldOffset field = @@ -988,3 +999,7 @@ module public Reflection = let t = typeBuilder.CreateType() t.GetMethod(methodName, staticBindingFlags) + + let getCountByReflection obj = + let method = obj.GetType().GetMethod("get_Count") + method.Invoke(obj, [| |]) :?> int diff --git a/VSharp.Utils/TypeUtils.fs b/VSharp.Utils/TypeUtils.fs index 6a1038039..bd231028f 100644 --- a/VSharp.Utils/TypeUtils.fs +++ b/VSharp.Utils/TypeUtils.fs @@ -296,6 +296,40 @@ module TypeUtils = Some(ArrayType(a.GetElementType(), dim)) | _ -> None + let (|DictionaryType|_|) = function + | (a : Type) when a.Name = "Dictionary`2" -> + let generics = a.GetGenericArguments() + assert(generics.Length = 2) + let keyType, valueType = generics[0], generics[1] + Some(keyType, valueType) + | _ -> None + + let setNames = ["HashSet`1"; "SortedSet`1"] + + let (|SetType|_|) = function + | (a : Type) when List.contains a.Name setNames -> + let valueType = a.GetGenericArguments()[0] + Some(valueType) + | _ -> None + + let (|Set|_|) = function + | obj when List.contains (obj.GetType().Name) setNames -> + Some obj + | _ -> None + + let listNames = ["List`1"; "LinkedList`1"] + + let (|ListType|_|) = function + | (a : Type) when List.contains a.Name listNames -> + let valueType = a.GetGenericArguments()[0] + Some(valueType) + | _ -> None + + let (|List|_|) = function + | obj when List.contains (obj.GetType().Name) listNames -> + Some obj + | _ -> None + let (|ValueType|_|) = function | StructType(t, [||]) when t = addressType -> None | StructType _