Add symbolic collections

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);
+        }
+    }
+}

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
 

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()

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

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