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<T> : IEnumerator<T>, IEnumerator
+ {
+ private readonly List<T> _list;
+ private int _index;
+ private T? _current;
+
+ internal ListEnumerator(List<T> 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<T>(List<T> 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<T>(List<T> 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<T>(List<T> 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<T>(List<T> 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<T>(List<T> 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<T>.GetEnumerator(this)")]
+ public static IEnumerator<T> GetEnumerator<T>(List<T> list)
+ {
+ return new ListEnumerator<T>(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 =
+
+ [<Implements("System.Int32 System.Collections.Generic.Dictionary`2[TKey,TValue].get_Count(this)")>]
+ val GetCount : state -> term list -> term
+
+ [<Implements("System.Boolean System.Collections.Generic.Dictionary`2[TKey,TValue].ContainsKey(this, TKey)")>]
+ val IsContainsKey : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("TValue System.Collections.Generic.Dictionary`2[TKey,TValue].get_Item(this, TKey)")>]
+ val GetItem : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.Dictionary`2[TKey,TValue].set_Item(this, TKey, TValue)")>]
+ val SetItem : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.Dictionary`2[TKey,TValue].Add(this, TKey, TValue)")>]
+ 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 =
+
+ [<Implements("System.Int32 System.Collections.Generic.List`1[T].get_Count(this)")>]
+ [<Implements("System.Int32 System.Collections.Generic.LinkedList`1[T].get_Count(this)")>]
+ val GetCount : state -> term list -> term
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].Add(this, T)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].Add(this, T)")>]
+ val AddItem : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].set_Item(this, System.Int32, T)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].set_Item(this, System.Int32, T)")>]
+ val SetItem : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("T System.Collections.Generic.List`1[T].get_Item(this, System.Int32)")>]
+ [<Implements("T System.Collections.Generic.LinkedList`1[T].get_Item(this, System.Int32)")>]
+ val ReadByIndex : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("T System.Collections.Generic.List`1[T].First(this)")>]
+ [<Implements("T System.Collections.Generic.LinkedList`1[T].First(this)")>]
+ val ReadFirst : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("T System.Collections.Generic.List`1[T].Last(this)")>]
+ [<Implements("T System.Collections.Generic.LinkedList`1[T].Last(this)")>]
+ val ReadLast : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].RemoveAt(this, System.Int32)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].RemoveAt(this, System.Int32)")>]
+ val RemoveAt : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].Insert(this, System.Int32, T)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].Insert(this, System.Int32, T)")>]
+ val Insert : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].CopyTo(this, System.Int32, T[], System.Int32, System.Int32)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].CopyTo(this, System.Int32, T[], System.Int32, System.Int32)")>]
+ val CopyToRange : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].CopyTo(this, T[], System.Int32)")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].CopyTo(this, T[], System.Int32)")>]
+ val CopyToFull : IInterpreter -> cilState -> term list -> cilState list
+
+ [<Implements("System.Void System.Collections.Generic.List`1[T].CopyTo(this, T[])")>]
+ [<Implements("System.Void System.Collections.Generic.LinkedList`1[T].CopyTo(this, T[])")>]
+ 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 =
+ [<Implements("System.Boolean System.Collections.Generic.SortedSet`1[T].Add(this, T)")>]
+ [<Implements("System.Boolean System.Collections.Generic.HashSet`1[T].Add(this, T)")>]
+ val AddItem : state -> term list -> term
+
+ [<Implements("System.Boolean System.Collections.Generic.SortedSet`1[T].Remove(this, T)")>]
+ [<Implements("System.Boolean System.Collections.Generic.HashSet`1[T].Remove(this, T)")>]
+ val RemoveItem : state -> term list -> term
+
+ [<Implements("System.Boolean System.Collections.Generic.SortedSet`1[T].Contains(this, T)")>]
+ [<Implements("System.Boolean System.Collections.Generic.HashSet`1[T].Contains(this, T)")>]
+ val IsContainsItem : state -> term list -> term
+
+ [<Implements("System.Int32 System.Collections.Generic.SortedSet`1[T].get_Count(this)")>]
+ [<Implements("System.Int32 System.Collections.Generic.HashSet`1[T].get_Count(this)")>]
+ 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<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, points<'key>>>.Empty() dictionaryType.valueType
+ let fill (region : IMemoryRegion) =
+ let region = region :?> memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool>
+ | ByteDictionary _ -> FillGeneralDictionaryRegion<byte>
+ | SByteDictionary _ -> FillGeneralDictionaryRegion<sbyte>
+ | CharDictionary _ -> FillGeneralDictionaryRegion<char>
+ | DecimalDictionary _ -> FillGeneralDictionaryRegion<decimal>
+ | DoubleDictionary _ -> FillGeneralDictionaryRegion<double>
+ | IntDictionary _ -> FillGeneralDictionaryRegion<int>
+ | UIntDictionary _ -> FillGeneralDictionaryRegion<uint>
+ | LongDictionary _ -> FillGeneralDictionaryRegion<int64>
+ | ULongDictionary _ -> FillGeneralDictionaryRegion<uint64>
+ | ShortDictionary _ -> FillGeneralDictionaryRegion<int16>
+ | UShortDictionary _ -> FillGeneralDictionaryRegion<uint16>
+ | 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<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, points<'key>>>.Empty() typeof<bool>
+ let fill (region : IMemoryRegion) =
+ let region = region :?> memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool>
+ | ByteDictionary _ -> FillGeneralDictionaryKeysRegion<byte>
+ | SByteDictionary _ -> FillGeneralDictionaryKeysRegion<sbyte>
+ | CharDictionary _ -> FillGeneralDictionaryKeysRegion<char>
+ | DecimalDictionary _ -> FillGeneralDictionaryKeysRegion<decimal>
+ | DoubleDictionary _ -> FillGeneralDictionaryKeysRegion<double>
+ | IntDictionary _ -> FillGeneralDictionaryKeysRegion<int>
+ | UIntDictionary _ -> FillGeneralDictionaryKeysRegion<uint>
+ | LongDictionary _ -> FillGeneralDictionaryKeysRegion<int64>
+ | ULongDictionary _ -> FillGeneralDictionaryKeysRegion<uint64>
+ | ShortDictionary _ -> FillGeneralDictionaryKeysRegion<int16>
+ | UShortDictionary _ -> FillGeneralDictionaryKeysRegion<uint16>
+ | 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<bool>
+ 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<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, points<'key>>>.Empty() typeof<bool>
+ let fill (region : IMemoryRegion) =
+ let region = region :?> memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool>
+ | ByteSet _ -> FillGeneralSetRegion<byte>
+ | SByteSet _ -> FillGeneralSetRegion<sbyte>
+ | CharSet _ -> FillGeneralSetRegion<char>
+ | DecimalSet _ -> FillGeneralSetRegion<decimal>
+ | DoubleSet _ -> FillGeneralSetRegion<double>
+ | IntSet _ -> FillGeneralSetRegion<int>
+ | UIntSet _ -> FillGeneralSetRegion<uint>
+ | LongSet _ -> FillGeneralSetRegion<int64>
+ | ULongSet _ -> FillGeneralSetRegion<uint64>
+ | ShortSet _ -> FillGeneralSetRegion<int16>
+ | UShortSet _ -> FillGeneralSetRegion<uint16>
+ | 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<bool>
+ 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<int8>
- 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<int8>
+ 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<heapAddressKey * memoryRegion<heapAddressKey, vectorTime intervals>>
val (|ArrayRangeReading|_|) : ISymbolicConstantSource -> option<unit>
val (|ArrayIndexReading|_|) : ISymbolicConstantSource -> option<bool * heapArrayKey * memoryRegion<heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>>
+ val (|BoolDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<bool> * boolDictionariesRegion>
+ val (|ByteDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<byte> * byteDictionariesRegion>
+ val (|SByteDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<sbyte> * sbyteDictionariesRegion>
+ val (|CharDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<char> * charDictionariesRegion>
+ val (|DecimalDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<decimal> * decimalDictionariesRegion>
+ val (|DoubleDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<double> * doubleDictionariesRegion>
+ val (|IntDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int> * intDictionariesRegion>
+ val (|UIntDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint> * uintDictionariesRegion>
+ val (|LongDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int64> * longDictionariesRegion>
+ val (|ULongDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint64> * ulongDictionariesRegion>
+ val (|ShortDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int16> * shortDictionariesRegion>
+ val (|UShortDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint16> * ushortDictionariesRegion>
+ val (|AddrDictionaryReading|_|) : ISymbolicConstantSource -> option<bool * addrCollectionKey * addrDictionariesRegion>
+ val (|BoolSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<bool> * boolSetsRegion>
+ val (|ByteSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<byte> * byteSetsRegion>
+ val (|SByteSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<sbyte> * sbyteSetsRegion>
+ val (|CharSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<char> * charSetsRegion>
+ val (|DecimalSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<decimal> * decimalSetsRegion>
+ val (|DoubleSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<double> * doubleSetsRegion>
+ val (|IntSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int> * intSetsRegion>
+ val (|UIntSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint> * uintSetsRegion>
+ val (|LongSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int64> * longSetsRegion>
+ val (|ULongSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint64> * ulongSetsRegion>
+ val (|ShortSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<int16> * shortSetsRegion>
+ val (|UShortSetReading|_|) : ISymbolicConstantSource -> option<bool * heapCollectionKey<uint16> * ushortSetsRegion>
+ val (|AddrSetReading|_|) : ISymbolicConstantSource -> option<bool * addrCollectionKey * addrSetsRegion>
val (|VectorIndexReading|_|) : ISymbolicConstantSource -> option<bool * heapVectorIndexKey * memoryRegion<heapVectorIndexKey, productRegion<vectorTime intervals, int points>>>
val (|StackBufferReading|_|) : ISymbolicConstantSource -> option<stackBufferIndexKey * memoryRegion<stackBufferIndexKey, int points>>
val (|StaticsReading|_|) : ISymbolicConstantSource -> option<symbolicTypeKey * memoryRegion<symbolicTypeKey, freeRegion<typeWrapper>>>
@@ -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<int>; array.GetType(); typeof<int>; typeof<int> |]
+ 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<int list * obj>
+ member internal GetAllDictionaryData : concreteHeapAddress -> seq<obj * obj>
+ member internal GetAllSetData : concreteHeapAddress -> seq<obj>
+ member internal GetAllListData : concreteHeapAddress -> seq<obj>
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 --------------------------------
+
[<StructuralEquality;NoComparison>]
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<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+ type private addrDictionaryReading = heapReading<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+ type private dictionaryCountReading = heapReading<heapAddressKey, vectorTime intervals>
+
+ type private generalSetReading<'key when 'key : equality> = heapReading<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+ type private addrSetReading = heapReading<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+ type private setCountReading = heapReading<heapAddressKey, vectorTime intervals>
+
let (|HeapReading|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapReading<heapAddressKey, vectorTime intervals> 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<bool> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|ByteDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<byte> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|SByteDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<sbyte> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|CharDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<char> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|DecimalDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<decimal> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|DoubleDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<double> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|IntDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<int> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|UIntDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<uint> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|LongDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<int64> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|ULongDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<uint64> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|ShortDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<int16> as dr -> Some(isConcreteHeapAddress dr.key.address, dr.key, dr.memoryObject)
+ | _ -> None
+
+ let (|UShortDictionaryReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalDictionaryReading<uint16> 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<bool> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|ByteSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<byte> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|SByteSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<sbyte> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|CharSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<char> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|DecimalSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<decimal> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|DoubleSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<double> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|IntSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<int> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|UIntSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<uint> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|LongSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<int64> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|ULongSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<uint64> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|ShortSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<int16> as st -> Some(isConcreteHeapAddress st.key.address, st.key, st.memoryObject)
+ | _ -> None
+
+ let (|UShortSetReading|_|) (src : ISymbolicConstantSource) =
+ match src with
+ | :? generalSetReading<uint16> 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<heapAddressKey, vectorTime intervals> as hr -> hr.picker.sort
+ | :? heapReading<heapAddressKey, vectorTime intervals> as hr -> hr.picker.sort
| :? heapReading<heapVectorIndexKey, productRegion<vectorTime intervals, int points>> as hr -> hr.picker.sort
- | :? heapReading<stackBufferIndexKey, int points> as hr -> hr.picker.sort
- | :? heapReading<symbolicTypeKey, freeRegion<typeWrapper>> as hr -> hr.picker.sort
+ | :? heapReading<stackBufferIndexKey, int points> as hr -> hr.picker.sort
+ | :? heapReading<symbolicTypeKey, freeRegion<typeWrapper>> as hr -> hr.picker.sort
| :? heapReading<heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>> ->
internalfail "unexpected array index reading via 'heapReading' source"
| :? arrayReading as ar -> ar.picker.sort
+ | :? generalDictionaryReading<bool> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<byte> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<sbyte> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<char> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<decimal> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<double> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<int> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<uint> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<int64> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<uint64> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<int16> as dr -> dr.picker.sort
+ | :? generalDictionaryReading<uint16> as dr -> dr.picker.sort
+ | :? addrDictionaryReading as dr -> dr.picker.sort
+ | :? generalSetReading<bool> as st -> st.picker.sort
+ | :? generalSetReading<byte> as st -> st.picker.sort
+ | :? generalSetReading<sbyte> as st -> st.picker.sort
+ | :? generalSetReading<char> as st -> st.picker.sort
+ | :? generalSetReading<decimal> as st -> st.picker.sort
+ | :? generalSetReading<double> as st -> st.picker.sort
+ | :? generalSetReading<int> as st -> st.picker.sort
+ | :? generalSetReading<uint> as st -> st.picker.sort
+ | :? generalSetReading<int64> as st -> st.picker.sort
+ | :? generalSetReading<uint64> as st -> st.picker.sort
+ | :? generalSetReading<int16> as st -> st.picker.sort
+ | :? generalSetReading<uint16> 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<Void>)
neededType = actualType
@@ -349,13 +513,7 @@ module internal Memory =
type Memory private (
evaluationStack : evaluationStack,
stack : callStack, // Arguments and local variables
- stackBuffers : pdict<stackKey, stackBufferRegion>, // Buffers allocated via stackAlloc
- classFields : pdict<fieldId, heapRegion>, // Fields of classes in heap
- arrays : pdict<arrayType, arrayRegion>, // Contents of arrays in heap
- lengths : pdict<arrayType, vectorRegion>, // Lengths by dimensions of arrays in heap
- lowerBounds : pdict<arrayType, vectorRegion>, // Lower bounds by dimensions of arrays in heap
- staticFields : pdict<fieldId, staticsRegion>, // Static fields of types without type variables
- boxedLocations : pdict<Type, heapRegion>, // Value types boxed in heap
+ memoryRegions : pdict<IMemoryRegionId, IMemoryRegion>,
concreteMemory : ConcreteMemory, // Fully concrete objects
allocatedTypes : pdict<concreteHeapAddress, symbolicType>, // Types of heap locations allocated via new
initializedAddresses : pset<term>, // 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<int>) 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<bool> :?> 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<bool> :?> 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<bool>)
+ | ByteDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<byte>)
+ | SByteDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<sbyte>)
+ | CharDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<char>)
+ | DecimalDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<decimal>)
+ | DoubleDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<double>)
+ | IntDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<int>)
+ | UIntDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<uint>)
+ | LongDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<int64>)
+ | ULongDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<uint64>)
+ | ShortDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<int16>)
+ | UShortDictionary _ -> writeGeneralDictionaryKeySymbolic <| ({ address = address; key = key } : heapCollectionKey<uint16>)
+ | 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<bool>)
+ | ByteDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<byte>)
+ | SByteDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<sbyte>)
+ | CharDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<char>)
+ | DecimalDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<decimal>)
+ | DoubleDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<double>)
+ | IntDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<int>)
+ | UIntDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<uint>)
+ | LongDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<int64>)
+ | ULongDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<uint64>)
+ | ShortDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<int16>)
+ | UShortDictionary _ -> writeGeneralDictionaryKeyToKeysSymbolic <| ({ address = address; key = key } : heapCollectionKey<uint16>)
+ | 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<bool> :?> 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<bool> :?> 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<bool>)
+ | ByteSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<byte>)
+ | SByteSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<sbyte>)
+ | CharSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<char>)
+ | DecimalSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<decimal>)
+ | DoubleSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<double>)
+ | IntSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<int>)
+ | UIntSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<uint>)
+ | LongSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<int64>)
+ | ULongSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<uint64>)
+ | ShortSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<int16>)
+ | UShortSet _ -> writeGeneralSetKeySymbolic <| ({ address = address; key = item } : heapCollectionKey<uint16>)
+ | 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<int>) 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<int8>
+ let mrKey = MemoryRegionId.createStackBuffersId stackKey
+ let mr = getOrPutRegion mrKey typeof<int8> :?> 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<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+ 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<bool>
+ | ByteDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<byte>
+ | SByteDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<sbyte>
+ | CharDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<char>
+ | DecimalDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<decimal>
+ | DoubleDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<double>
+ | IntDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<int>
+ | UIntDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<uint>
+ | LongDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<int64>
+ | ULongDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<uint64>
+ | ShortDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<int16>
+ | UShortDictionary _ -> self.ReadGeneralDictionaryKeySymbolic<uint16>
+ | 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<bool> state.memory.MemoryRegions
+ :?> memoryRegion<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+ 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<bool> 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<bool>
+ | ByteDictionary _ -> self.HasGeneralDictionaryKeySymbolic<byte>
+ | SByteDictionary _ -> self.HasGeneralDictionaryKeySymbolic<sbyte>
+ | CharDictionary _ -> self.HasGeneralDictionaryKeySymbolic<char>
+ | DecimalDictionary _ -> self.HasGeneralDictionaryKeySymbolic<decimal>
+ | DoubleDictionary _ -> self.HasGeneralDictionaryKeySymbolic<double>
+ | IntDictionary _ -> self.HasGeneralDictionaryKeySymbolic<int>
+ | UIntDictionary _ -> self.HasGeneralDictionaryKeySymbolic<uint>
+ | LongDictionary _ -> self.HasGeneralDictionaryKeySymbolic<int64>
+ | ULongDictionary _ -> self.HasGeneralDictionaryKeySymbolic<uint64>
+ | ShortDictionary _ -> self.HasGeneralDictionaryKeySymbolic<int16>
+ | UShortDictionary _ -> self.HasGeneralDictionaryKeySymbolic<uint16>
+ | 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<bool> state.memory.MemoryRegions
+ :?> memoryRegion<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+ 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<bool> 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<bool>
+ | ByteSet _ -> self.ReadGeneralSetKeySymbolic<byte>
+ | SByteSet _ -> self.ReadGeneralSetKeySymbolic<sbyte>
+ | CharSet _ -> self.ReadGeneralSetKeySymbolic<char>
+ | DecimalSet _ -> self.ReadGeneralSetKeySymbolic<decimal>
+ | DoubleSet _ -> self.ReadGeneralSetKeySymbolic<double>
+ | IntSet _ -> self.ReadGeneralSetKeySymbolic<int>
+ | UIntSet _ -> self.ReadGeneralSetKeySymbolic<uint>
+ | LongSet _ -> self.ReadGeneralSetKeySymbolic<int64>
+ | ULongSet _ -> self.ReadGeneralSetKeySymbolic<uint64>
+ | ShortSet _ -> self.ReadGeneralSetKeySymbolic<int16>
+ | UShortSet _ -> self.ReadGeneralSetKeySymbolic<uint16>
+ | AddrSet _ -> self.ReadAddrSetKeySymbolic
+ | _ -> __unreachable__()
+ read address item setType
+
member private self.ReadArrayIndexSymbolic address indices arrayType =
let indices = List.map (fun i -> primitiveCast i typeof<int>) 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<obj>) 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<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool>
+ | ByteDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<byte>
+ | SByteDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<sbyte>
+ | CharDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<char>
+ | DecimalDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<decimal>
+ | DoubleDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<double>
+ | IntDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<int>
+ | UIntDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<uint>
+ | LongDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<int64>
+ | ULongDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<uint64>
+ | ShortDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<int16>
+ | UShortDictionary _ -> self.ReadSymbolicKeyFromConcreteGeneralDictionary<uint16>
+ | 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<bool> concreteAddress
+ let region : memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool> 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<bool>
+ | ByteDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<byte>
+ | SByteDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<sbyte>
+ | CharDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<char>
+ | DecimalDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<decimal>
+ | DoubleDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<double>
+ | IntDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<int>
+ | UIntDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<uint>
+ | LongDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<int64>
+ | ULongDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<uint64>
+ | ShortDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<int16>
+ | UShortDictionary _ -> self.HasSymbolicKeyFromConcreteGeneralDictionary<uint16>
+ | 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<bool> concreteAddress
+ let region : memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool> 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<bool>
+ | ByteSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<byte>
+ | SByteSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<sbyte>
+ | CharSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<char>
+ | DecimalSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<decimal>
+ | DoubleSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<double>
+ | IntSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<int>
+ | UIntSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<uint>
+ | LongSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<int64>
+ | ULongSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<uint64>
+ | ShortSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<int16>
+ | UShortSet _ -> self.ReadSymbolicKeyFromConcreteGeneralSet<uint16>
+ | 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<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool>
+ | ByteDictionary _ -> self.GeneralDictionaryMemsetData<byte>
+ | SByteDictionary _ -> self.GeneralDictionaryMemsetData<sbyte>
+ | CharDictionary _ -> self.GeneralDictionaryMemsetData<char>
+ | DecimalDictionary _ -> self.GeneralDictionaryMemsetData<decimal>
+ | DoubleDictionary _ -> self.GeneralDictionaryMemsetData<double>
+ | IntDictionary _ -> self.GeneralDictionaryMemsetData<int>
+ | UIntDictionary _ -> self.GeneralDictionaryMemsetData<uint>
+ | LongDictionary _ -> self.GeneralDictionaryMemsetData<int64>
+ | ULongDictionary _ -> self.GeneralDictionaryMemsetData<uint64>
+ | ShortDictionary _ -> self.GeneralDictionaryMemsetData<int16>
+ | UShortDictionary _ -> self.GeneralDictionaryMemsetData<uint16>
+ | 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<bool> :?> memoryRegion<heapCollectionKey<'key>, productRegion<intervals<vectorTime>, 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<bool> :?> 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<bool>
+ | ByteSet _ -> self.GeneralSetMemsetData<byte>
+ | SByteSet _ -> self.GeneralSetMemsetData<sbyte>
+ | CharSet _ -> self.GeneralSetMemsetData<char>
+ | DecimalSet _ -> self.GeneralSetMemsetData<decimal>
+ | DoubleSet _ -> self.GeneralSetMemsetData<double>
+ | IntSet _ -> self.GeneralSetMemsetData<int>
+ | UIntSet _ -> self.GeneralSetMemsetData<uint>
+ | LongSet _ -> self.GeneralSetMemsetData<int64>
+ | ULongSet _ -> self.GeneralSetMemsetData<uint64>
+ | ShortSet _ -> self.GeneralSetMemsetData<int16>
+ | UShortSet _ -> self.GeneralSetMemsetData<uint16>
+ | 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<int>
| _ -> 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<int>
+ | _ -> 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<int>
+ | _ -> 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<int>
+ | _ -> 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<int8>
+ let extractor (state : state) =
+ let mrKey = MemoryRegionId.createStackBuffersId <| stackKey.Map state.TypeVariableSubst
+ getOrPutRegionCommon mrKey typeof<int8> 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<byte>.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<bool>
| ArrayLengthSort _
- | ArrayLowerBoundSort _ -> typeof<int32>
+ | ArrayLowerBoundSort _
+ | DictionaryCountSort _
+ | SetCountSort _
+ | ListCountSort _ -> typeof<int32>
| StackBufferSort _ -> typeof<int8>
| 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<int>.Singleton value
| None -> points<int>.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<points<int>>.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<heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
+[<CustomEquality;CustomComparison>]
+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<vectorTime intervals, 'key points>.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<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+
+[<CustomEquality;CustomComparison>]
+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<vectorTime intervals, vectorTime intervals>.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<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+
[<CustomEquality;CustomComparison>]
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
+
[<CustomEquality; NoComparison>]
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
+
+[<CustomEquality; NoComparison>]
+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<stackKey, stackBufferIndexKey, int points>
+type classFieldsId = memoryRegionId<fieldId, heapAddressKey, vectorTime intervals>
+type staticFieldsId = memoryRegionId<fieldId, symbolicTypeKey, freeRegion<typeWrapper>>
+type boxedLocationsId = memoryRegionId<Type, heapAddressKey, vectorTime intervals>
+type arraysId = memoryRegionId<arrayType, heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>
+type arrayLengthsId = memoryRegionId<arrayType, heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
+type arrayLowerBoundsId = memoryRegionId<arrayType, heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
+
+type dictionariesId<'key when 'key : equality> = memoryRegionId<dictionaryType, heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+type boolDictionariesId = dictionariesId<bool>
+type byteDictionariesId = dictionariesId<byte>
+type sbyteDictionariesId = dictionariesId<sbyte>
+type charDictionariesId = dictionariesId<char>
+type decimalDictionariesId = dictionariesId<decimal>
+type doubleDictionariesId = dictionariesId<double>
+type intDictionariesId = dictionariesId<int>
+type uintDictionariesId = dictionariesId<uint>
+type longDictionariesId = dictionariesId<int64>
+type ulongDictionariesId = dictionariesId<uint64>
+type shortDictionariesId = dictionariesId<int16>
+type ushortDictionariesId = dictionariesId<uint16>
+type addrDictionariesId = memoryRegionId<dictionaryType, addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+
+type dictionaryKeysId<'key when 'key : equality> = memoryRegionId<dictionaryType, heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+type boolDictionaryKeysId = dictionaryKeysId<bool>
+type byteDictionaryKeysId = dictionaryKeysId<byte>
+type sbyteDictionaryKeysId = dictionaryKeysId<sbyte>
+type charDictionaryKeysId = dictionaryKeysId<char>
+type decimalDictionaryKeysId = dictionaryKeysId<decimal>
+type doubleDictionaryKeysId = dictionaryKeysId<double>
+type intDictionaryKeysId = dictionaryKeysId<int>
+type uintDictionaryKeysId = dictionaryKeysId<uint>
+type longDictionaryKeysId = dictionaryKeysId<int64>
+type ulongDictionaryKeysId = dictionaryKeysId<uint64>
+type shortDictionaryKeysId = dictionaryKeysId<int16>
+type ushortDictionaryKeysId = dictionaryKeysId<uint16>
+type addrDictionaryKeysId = memoryRegionId<dictionaryType, addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+type dictionaryCountsId = memoryRegionId<dictionaryType, heapAddressKey, vectorTime intervals>
+
+type setsId<'key when 'key : equality> = memoryRegionId<setType, heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+type boolSetsId = setsId<bool>
+type byteSetsId = setsId<byte>
+type sbyteSetsId = setsId<sbyte>
+type charSetsId = setsId<char>
+type decimalSetsId = setsId<decimal>
+type doubleSetsId = setsId<double>
+type intSetsId = setsId<int>
+type uintSetsId = setsId<uint>
+type longSetsId = setsId<int64>
+type ulongSetsId = setsId<uint64>
+type shortSetsId = setsId<int16>
+type ushortSetsId = setsId<uint16>
+type addrSetsId = memoryRegionId<setType, addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+type setCountsId = memoryRegionId<setType, heapAddressKey, vectorTime intervals>
+
+type listsId = memoryRegionId<listType, heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>
+type listCountsId = memoryRegionId<listType, heapAddressKey, vectorTime intervals>
+
+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<bool>) :> IMemoryRegionId
+ | ByteDictionary dt -> ({ id = dt; sort = ByteDictionariesSort } : dictionaryKeysId<byte>) :> IMemoryRegionId
+ | SByteDictionary dt -> ({ id = dt; sort = SByteDictionariesSort } : dictionaryKeysId<sbyte>) :> IMemoryRegionId
+ | CharDictionary dt -> ({ id = dt; sort = CharDictionariesSort } : dictionaryKeysId<char>) :> IMemoryRegionId
+ | DecimalDictionary dt -> ({ id = dt; sort = DecimalDictionariesSort } : dictionaryKeysId<decimal>) :> IMemoryRegionId
+ | DoubleDictionary dt -> ({ id = dt; sort = DoubleDictionariesSort } : dictionaryKeysId<double>) :> IMemoryRegionId
+ | IntDictionary dt -> ({ id = dt; sort = IntDictionariesSort } : dictionaryKeysId<int>) :> IMemoryRegionId
+ | UIntDictionary dt -> ({ id = dt; sort = UIntDictionariesSort } : dictionaryKeysId<uint>) :> IMemoryRegionId
+ | LongDictionary dt -> ({ id = dt; sort = LongDictionariesSort } : dictionaryKeysId<int64>) :> IMemoryRegionId
+ | ULongDictionary dt -> ({ id = dt; sort = ULongDictionariesSort } : dictionaryKeysId<uint64>) :> IMemoryRegionId
+ | ShortDictionary dt -> ({ id = dt; sort = ShortDictionariesSort } : dictionaryKeysId<int16>) :> IMemoryRegionId
+ | UShortDictionary dt -> ({ id = dt; sort = UShortDictionariesSort } : dictionaryKeysId<uint16>) :> 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<bool>) :> IMemoryRegionId
+ | ByteDictionary dt -> ({ id = dt; sort = ByteDictionaryKeysSort } : dictionaryKeysId<byte>) :> IMemoryRegionId
+ | SByteDictionary dt -> ({ id = dt; sort = SByteDictionaryKeysSort } : dictionaryKeysId<sbyte>) :> IMemoryRegionId
+ | CharDictionary dt -> ({ id = dt; sort = CharDictionaryKeysSort } : dictionaryKeysId<char>) :> IMemoryRegionId
+ | DecimalDictionary dt -> ({ id = dt; sort = DecimalDictionaryKeysSort } : dictionaryKeysId<decimal>) :> IMemoryRegionId
+ | DoubleDictionary dt -> ({ id = dt; sort = DoubleDictionaryKeysSort } : dictionaryKeysId<double>) :> IMemoryRegionId
+ | IntDictionary dt -> ({ id = dt; sort = IntDictionaryKeysSort } : dictionaryKeysId<int>) :> IMemoryRegionId
+ | UIntDictionary dt -> ({ id = dt; sort = UIntDictionaryKeysSort } : dictionaryKeysId<uint>) :> IMemoryRegionId
+ | LongDictionary dt -> ({ id = dt; sort = LongDictionaryKeysSort } : dictionaryKeysId<int64>) :> IMemoryRegionId
+ | ULongDictionary dt -> ({ id = dt; sort = ULongDictionaryKeysSort } : dictionaryKeysId<uint64>) :> IMemoryRegionId
+ | ShortDictionary dt -> ({ id = dt; sort = ShortDictionaryKeysSort } : dictionaryKeysId<int16>) :> IMemoryRegionId
+ | UShortDictionary dt -> ({ id = dt; sort = UShortDictionaryKeysSort } : dictionaryKeysId<uint16>) :> 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<bool>):> IMemoryRegionId
+ | ByteSet st -> ({ id = st; sort = ByteSetsSort } : setsId<byte>):> IMemoryRegionId
+ | SByteSet st -> ({ id = st; sort = SByteSetsSort } : setsId<sbyte>):> IMemoryRegionId
+ | CharSet st -> ({ id = st; sort = CharSetsSort } : setsId<char>):> IMemoryRegionId
+ | DecimalSet st -> ({ id = st; sort = DecimalSetsSort } : setsId<decimal>):> IMemoryRegionId
+ | DoubleSet st ->({ id = st; sort = DoubleSetsSort } : setsId<double>):> IMemoryRegionId
+ | IntSet st -> ({ id = st; sort = IntSetsSort } : setsId<int>):> IMemoryRegionId
+ | UIntSet st -> ({ id = st; sort = UIntSetsSort } : setsId<uint>):> IMemoryRegionId
+ | LongSet st -> ({ id = st; sort = LongSetsSort } : setsId<int64>):> IMemoryRegionId
+ | ULongSet st -> ({ id = st; sort = ULongSetsSort } : setsId<uint64>):> IMemoryRegionId
+ | ShortSet st -> ({ id = st; sort = ShortSetsSort } : setsId<int16>):> IMemoryRegionId
+ | UShortSet st -> ({ id = st; sort = UShortSetsSort } : setsId<uint16>):> 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<setKeyWrapper<'key>> 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<heapAddressKey, vectorTime intervals>
-type arrayRegion = memoryRegion<heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>
-type vectorRegion = memoryRegion<heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
-type stackBufferRegion = memoryRegion<stackBufferIndexKey, int points>
-type staticsRegion = memoryRegion<symbolicTypeKey, freeRegion<typeWrapper>>
type symbolicTypeSet = symbolicSet<symbolicTypeKey, freeRegion<typeWrapper>>
+
+type stackBuffersRegion = memoryRegion<stackBufferIndexKey, int points>
+type classFieldsRegion = memoryRegion<heapAddressKey, vectorTime intervals>
+type staticFieldsRegion = memoryRegion<symbolicTypeKey, freeRegion<typeWrapper>>
+type boxedLocationsRegion = memoryRegion<heapAddressKey, vectorTime intervals>
+type arraysRegion = memoryRegion<heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>
+type arrayLengthsRegion = memoryRegion<heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
+type arrayLowerBoundsRegion = memoryRegion<heapVectorIndexKey, productRegion<vectorTime intervals, int points>>
+
+type dictionariesRegion<'key when 'key : equality> = memoryRegion<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+type boolDictionariesRegion = dictionariesRegion<bool>
+type byteDictionariesRegion = dictionariesRegion<byte>
+type sbyteDictionariesRegion = dictionariesRegion<sbyte>
+type charDictionariesRegion = dictionariesRegion<char>
+type decimalDictionariesRegion = dictionariesRegion<decimal>
+type doubleDictionariesRegion = dictionariesRegion<double>
+type intDictionariesRegion = dictionariesRegion<int>
+type uintDictionariesRegion = dictionariesRegion<uint>
+type longDictionariesRegion = dictionariesRegion<int64>
+type ulongDictionariesRegion = dictionariesRegion<uint64>
+type shortDictionariesRegion = dictionariesRegion<int16>
+type ushortDictionariesRegion = dictionariesRegion<uint16>
+type addrDictionariesRegion = memoryRegion<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+type boolDictionaryKeysRegion = dictionariesRegion<bool>
+type byteDictionaryKeysRegion = dictionariesRegion<byte>
+type sbyteDictionaryKeysRegion = dictionariesRegion<sbyte>
+type charDictionaryKeysRegion = dictionariesRegion<char>
+type decimalDictionaryKeysRegion = dictionariesRegion<decimal>
+type doubleDictionaryKeysRegion = dictionariesRegion<double>
+type intDictionaryKeysRegion = dictionariesRegion<int>
+type uintDictionaryKeysRegion = dictionariesRegion<uint>
+type longDictionaryKeysRegion = dictionariesRegion<int64>
+type ulongDictionaryKeysRegion = dictionariesRegion<uint64>
+type shortDictionaryKeysRegion = dictionariesRegion<int16>
+type ushortDictionaryKeysRegion = dictionariesRegion<uint16>
+type addrDictionaryKeysRegion = memoryRegion<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+
+type dictionaryCountsRegion = memoryRegion<heapAddressKey, vectorTime intervals>
+
+type setsRegion<'key when 'key : equality> = memoryRegion<heapCollectionKey<'key>, productRegion<vectorTime intervals, 'key points>>
+type boolSetsRegion = setsRegion<bool>
+type byteSetsRegion = setsRegion<byte>
+type sbyteSetsRegion = setsRegion<sbyte>
+type charSetsRegion = setsRegion<char>
+type decimalSetsRegion = setsRegion<decimal>
+type doubleSetsRegion = setsRegion<double>
+type intSetsRegion = setsRegion<int>
+type uintSetsRegion = setsRegion<uint>
+type longSetsRegion = setsRegion<int64>
+type ulongSetsRegion = setsRegion<uint64>
+type shortSetsRegion = setsRegion<int16>
+type ushortSetsRegion = setsRegion<uint16>
+type addrSetsRegion = memoryRegion<addrCollectionKey, productRegion<vectorTime intervals, vectorTime intervals>>
+
+type setCountsRegion = memoryRegion<heapAddressKey, vectorTime intervals>
+
+type listsRegion = memoryRegion<heapArrayKey, productRegion<vectorTime intervals, int points listProductRegion>>
+type listCountsRegion = memoryRegion<heapAddressKey, vectorTime intervals>
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<stackKey, stackBufferRegion> with get, set
-
- abstract ClassFields : pdict<fieldId, heapRegion> with get, set
-
- abstract Arrays : pdict<arrayType, arrayRegion> with get, set
-
- abstract Lengths : pdict<arrayType, vectorRegion> with get, set
-
- abstract LowerBounds : pdict<arrayType, vectorRegion> with get, set
-
- abstract StaticFields : pdict<fieldId, staticsRegion> with get, set
-
- abstract BoxedLocations : pdict<Type, heapRegion> with get, set
+ abstract MemoryRegions : pdict<IMemoryRegionId, IMemoryRegion> 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<char>
+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<bool> -> Some dt
+ | _ -> None
+ let (|ByteDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<byte> -> Some dt
+ | _ -> None
+ let (|SByteDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<sbyte> -> Some dt
+ | _ -> None
+ let (|CharDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<char> -> Some dt
+ | _ -> None
+ let (|DecimalDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<decimal> -> Some dt
+ | _ -> None
+ let (|DoubleDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<double> -> Some dt
+ | _ -> None
+ let (|IntDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<int> -> Some dt
+ | _ -> None
+ let (|UIntDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<uint> -> Some dt
+ | _ -> None
+ let (|LongDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<int64> -> Some dt
+ | _ -> None
+ let (|ULongDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<uint64> -> Some dt
+ | _ -> None
+ let (|ShortDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<int16> -> Some dt
+ | _ -> None
+ let (|UShortDictionary|_|) = function
+ | (dt : dictionaryType) when dt.keyType = typeof<uint16> -> 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<bool> -> Some st
+ | _ -> None
+
+ let (|ByteSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<byte> -> Some st
+ | _ -> None
+
+ let (|SByteSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<sbyte> -> Some st
+ | _ -> None
+
+ let (|CharSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<char> -> Some st
+ | _ -> None
+
+ let (|DecimalSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<decimal> -> Some st
+ | _ -> None
+
+ let (|DoubleSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<double> -> Some st
+ | _ -> None
+
+ let (|IntSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<int> -> Some st
+ | _ -> None
+
+ let (|UIntSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<uint> -> Some st
+ | _ -> None
+
+ let (|LongSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<int64> -> Some st
+ | _ -> None
+
+ let (|ULongSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<uint64> -> Some st
+ | _ -> None
+
+ let (|ShortSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<int16> -> Some st
+ | _ -> None
+
+ let (|UShortSet|_|) = function
+ | (st : setType) when st.setValueType = typeof<uint16> -> 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 }
+
[<StructuralEquality;NoComparison>]
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<bool>
| BoxedLocation(_, typ) -> typ
| ArrayLength _
- | ArrayLowerBound _ -> lengthType
+ | ArrayLowerBound _
+ | DictionaryCount _
+ | ListCount _
+ | SetCount _ -> lengthType
| StackBufferIndex _ -> typeof<int8>
| 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<bool>
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<InvalidProgramException> [] cilState
+ member x.InvalidOperationException cilState =
+ x.CreateException typeof<InvalidOperationException> [] cilState
member x.NullReferenceException cilState =
x.CreateException typeof<NullReferenceException> [] 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<intervals<vectorTime>, 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<char> 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<char> then x.GenerateCharAssumptions res else res
+ res
+ // TODO: Counts Assumptions
+
+ member private x.SetReading<'key when 'key : equality>
+ (keysAreMatch : heapCollectionKey<'key> -> heapCollectionKey<'key> -> productRegion<intervals<vectorTime>, 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<bool>
+ 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<vectorTime>, intervals<vectorTime>> -> 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<bool>
+ 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<bool> key hasDefaultValue mo typ source path name
+ | ByteDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<byte> key hasDefaultValue mo typ source path name
+ | SByteDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<sbyte> key hasDefaultValue mo typ source path name
+ | CharDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<char> key hasDefaultValue mo typ source path name
+ | DecimalDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<decimal> key hasDefaultValue mo typ source path name
+ | DoubleDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<double> key hasDefaultValue mo typ source path name
+ | IntDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<int> key hasDefaultValue mo typ source path name
+ | UIntDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<uint> key hasDefaultValue mo typ source path name
+ | LongDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<int64> key hasDefaultValue mo typ source path name
+ | ULongDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<uint64> key hasDefaultValue mo typ source path name
+ | ShortDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<int16> key hasDefaultValue mo typ source path name
+ | UShortDictionaryReading(hasDefaultValue, key, mo) ->
+ x.DictionaryKeyReading<uint16> 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<bool> key hasDefaultValue mo typ source path name
+ | ByteSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<byte> key hasDefaultValue mo typ source path name
+ | SByteSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<sbyte> key hasDefaultValue mo typ source path name
+ | CharSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<char> key hasDefaultValue mo typ source path name
+ | DecimalSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<decimal> key hasDefaultValue mo typ source path name
+ | DoubleSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<double> key hasDefaultValue mo typ source path name
+ | IntSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<int> key hasDefaultValue mo typ source path name
+ | UIntSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<uint> key hasDefaultValue mo typ source path name
+ | LongSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<int64> key hasDefaultValue mo typ source path name
+ | ULongSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<uint64> key hasDefaultValue mo typ source path name
+ | ShortSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<int16> key hasDefaultValue mo typ source path name
+ | UShortSetReading(hasDefaultValue, key, mo) ->
+ x.SetKeyReading<uint16> 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<int> 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<T>
- {
- [TestSvm]
- public static T Cast(object o)
- {
- return (T) o;
- }
- }
-
+
[TestSvmFixture]
[IgnoreFuzzer("(Known bug) Last generated test is incorrect")]
public class BoxUnboxWithGeneric<G, T, U, V>
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<char, int>()
+ {
+ {a, 1},
+ {'b', 2},
+ {'c', b}
+ };
+ return dict['a'];
+ }
+
+ [TestSvm]
+ public int SymbolicInitialize2(Dictionary<int, int> d)
+ {
+ d[1] = 1;
+ return d[1];
+ }
+
+ [TestSvm]
+ public int SymbolicInitialize3(Dictionary<int, int> d, int a, int b)
+ {
+ d[a] = b;
+ d[2] = 2;
+ return d[a];
+ }
+
+ [TestSvm]
+ public float Mutate(long i)
+ {
+ var dict = new Dictionary<long, float>()
+ {
+ {1L, 1f},
+ {2L, 2f},
+ {3L, 3f},
+ {4L, 4f}
+ };
+ dict[1L] = 40f;
+ dict[i] = 10f;
+ return dict[3L];
+ }
+
+ [TestSvm]
+ public float Mutate2(Dictionary<long, float> dict, long i)
+ {
+ dict[i] = 10f;
+ return dict[3L];
+ }
+
+ [TestSvm]
+ public int SymbolicWriteAfterConcreteWrite(int k)
+ {
+ var dict = new Dictionary<int, int>();
+ dict[2] = 42;
+ dict[k] = 12;
+ return dict[2];
+ }
+
+ [TestSvm]
+ public int SymbolicWriteAfterConcreteWrite3(Dictionary<int, int> dict, int k)
+ {
+ dict[2] = 42;
+ dict[k] = 12;
+ return dict[2];
+ }
+
+ [TestSvm]
+ public Dictionary<byte, decimal> RetDictionary(bool flag1, bool flag2)
+ {
+ var dict = new Dictionary<byte, decimal>();
+ if (flag1)
+ {
+ dict[1] = 42;
+ }
+ else if (flag2)
+ {
+ dict[1] = 89;
+ }
+
+ return dict;
+ }
+
+ /*[TestSvm]
+ public int SymbolicWriteAfterConcreteWrite2(Dictionary<int, int> d, int k)
+ {
+ d[2] = 42;
+ d[k] = 12;
+ return d[2];
+ }
+
+ [TestSvm]
+ public int SolverTestDictionaryKey(Dictionary<int, int> 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<int, int> 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<int, string> a, Dictionary<int, string> 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<int, int>()
+ {
+ {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<int, int>()
+ {
+ {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<char, int> dict)
+ {
+ if (dict.Count > 0)
+ {
+ return true;
+ }
+ else
+ {
+ return false;
+ }
+ }
+
+ [TestSvm]
+ public bool CountSymbolicTest2(Dictionary<char, int> 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<short, long>()
+ {
+ { 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<short, long> 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<Bag<int>> list)
+ public static int NestedGenericsSmokeTest(Bag<int>[] list)
{
- if (list.Count > 0)
+ if (list.Length > 0)
{
return 0;
}
@@ -750,7 +750,7 @@ public static int NestedGenericsSmokeTest(List<Bag<int>> list)
return 1;
}
- [TestSvm(100)]
+ /*[TestSvm(100)]
[IgnoreFuzzer("Need recursion constraints in generators")]
public static int NestedGenericsSmokeTest2(Dictionary<int, Bag<int>> dict)
{
@@ -760,7 +760,7 @@ public static int NestedGenericsSmokeTest2(Dictionary<int, Bag<int>> 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<int, List<string>>();
- d.Add(1, new List<string> { "2", "3" });
- d.Add(4, new List<string> { "5", "6" });
- if (d.TryGetValue(a, out var res))
+ var d = new Dictionary<int, List<int>>();
+ d.Add(1, new List<int> { 2, 3 });
+ d.Add(4, new List<int> { 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<object> 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<int> _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<int> set)
+ {
+ return set.Contains(42);
+ }
+
+ [TestSvm]
+ public bool ContainsConcreteTest2(int item)
+ {
+ var set = new HashSet<int>() { 4 };
+
+ return set.Contains(item);
+ }
+
+ [TestSvm]
+ public bool ContainsConcreteTest3(int item)
+ {
+ var set = new HashSet<int>() { 4 };
+ set.Add(item);
+
+ return set.Contains(item);
+ }
+
+ [TestSvm]
+ public bool ContainsSymbolicTest(HashSet<int> set, int item)
+ {
+ return set.Contains(item);
+ }
+
+ [TestSvm]
+ public HashSet<byte> AddConcreteTest(HashSet<byte> set)
+ {
+ set.Add(42);
+
+ return set;
+ }
+
+ [TestSvm]
+ public HashSet<byte> AddConcreteTest2(byte item)
+ {
+ var set = new HashSet<byte>();
+ set.Add(42);
+
+ return set;
+ }
+
+ [TestSvm]
+ public HashSet<char> AddSymbolicTest(HashSet<char> set, char item)
+ {
+ set.Add(item);
+
+ return set;
+ }
+
+ [TestSvm]
+ public HashSet<char> RemoveSymbolicTest(HashSet<char> set, char item)
+ {
+ set.Remove(item);
+
+ return set;
+ }
+
+ // TODO: construct symbolic set with elements from region in test generator
+ /*[TestSvm]
+ public bool RemoveConcreteTest(HashSet<char> set)
+ {
+ var isRemoved = set.Remove('a');
+
+ if (isRemoved)
+ {
+ return true;
+ }
+
+ return false;
+ }*/
+
+ [TestSvm]
+ public bool RemoveConcreteTest2(long item)
+ {
+ var set = new HashSet<long>() { 1, 2, 3, 4 };
+
+ return set.Remove(item);
+ }
+
+ [TestSvm]
+ public bool CommonSymbolicTest(HashSet<char> set, char item, char item2)
+ {
+ set.Add(item);
+ set.Add(item2);
+ set.Remove(item);
+
+ return set.Contains(item);
+ }
+
+ [TestSvm]
+ public bool CommonSymbolicTest2(HashSet<char> 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<char> set, char item, char item2)
+ {
+ set.Add(item);
+ set.Add(item2);
+ set.Remove('z');
+
+ return set.Contains(item);
+ }
+
+ [TestSvm]
+ public int CountSymbolicTest(HashSet<long> set)
+ {
+ return set.Count;
+ }
+
+ [TestSvm]
+ public bool CountSymbolicTest2(HashSet<long> set, long item)
+ {
+ set.Add(item);
+
+ if (set.Count < 1)
+ {
+ return false;
+ }
+
+ return true;
+ }
+
+ [TestSvm]
+ public int CountSymbolicTest3(long item)
+ {
+ var set = new HashSet<long>() { 1, 2, 4 };
+
+ set.Add(item);
+ set.Add(item);
+
+ return set.Count;
+ }
+
+ [TestSvm]
+ public int CountSymbolicTest4(HashSet<long> 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<long>() { 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<char>() { 'a', 'b', 'c' };
+
+ l[index] = 'd';
+
+ if (l[index] == 'd')
+ {
+ return true;
+ }
+
+ return false;
+ }
+
+ [TestSvm]
+ public bool ConcreteTest2(int index)
+ {
+ var l = new List<char>() { 'a', 'b', 'c' };
+
+ if (l[index] == 'a')
+ {
+ return true;
+ }
+
+ return false;
+ }
+
+ [TestSvm]
+ public bool ConcreteTest3(int index)
+ {
+ var l = new List<char>() { '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<char>() { '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<char>() { 'a', 'b', 'c' };
+
+ if (l.IndexOf(item) == 1)
+ {
+ return true;
+ }
+
+ return false;
+ }
+
+ [TestSvm]
+ public bool ConcreteTest6(char item)
+ {
+ var l = new List<char>() { 'a', 'b', 'c' };
+
+ l.Remove(item);
+
+ if (l.Count > 2)
+ {
+ return true;
+ }
+
+ return false;
+ }
+
+ [TestSvm]
+ public int ConcreteMemoryTest(int i)
+ {
+ var l = new List<int>();
+ 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 _