[fix] splitting fixes, optimizations

Author: oveeernight

VSharp.SILI.Core/API.fs

@@ -556,8 +556,8 @@ module API =
             | Ite iteType ->
                 let filtered = iteType.filter (fun r -> Pointers.isBadRef r |> isTrue |> not)
                 filtered.ToDisjunctiveGvs()
-                |> List.iter (fun (g, r) -> state.memory.GuardedWriteClassField (Some g) (extractAddress r) field value)
-            | _ -> state.memory.WriteClassField (extractAddress reference) field value
+                |> List.iter (fun (g, r) -> state.memory.WriteClassField (Some g) (extractAddress r) field value)
+            | _ -> state.memory.WriteClassField None (extractAddress reference) field value
 
         let WriteClassField state reference field value =
             WriteClassFieldUnsafe emptyReporter state reference field value
@@ -733,7 +733,7 @@ module API =
             let symbolicCase address =
                 let address, arrayType = memory.StringArrayInfo address (Some length)
                 Copying.fillArray state address arrayType (makeNumber 0) length char
-                memory.WriteClassField address Reflection.stringLengthField length
+                memory.WriteClassField None address Reflection.stringLengthField length
             match string.term, concreteChar, concreteLen with
             | HeapRef({term = ConcreteHeapAddress a} as address, sightType), Some (:? char as c), Some (:? int as len)
                 when cm.Contains a ->

VSharp.SILI.Core/Copying.fs

@@ -75,7 +75,7 @@ module internal Copying =
         let stringAddress = ConcreteHeapAddress stringConcreteAddress
         let stringAddress, arrayType = memory.StringArrayInfo stringAddress (Some arrayLength)
         copyArray state arrayAddress startIndex arrayType stringAddress (makeNumber 0) arrayType arrayLength
-        memory.WriteClassField stringAddress Reflection.stringLengthField arrayLength
+        memory.WriteClassField None stringAddress Reflection.stringLengthField arrayLength
 
     let copyCharArrayToString (state : state) arrayAddress stringConcreteAddress startIndex length =
         let memory = state.memory

VSharp.SILI.Core/Memory.fs

@@ -2040,9 +2040,7 @@ module internal Memory =
                 self.CommonWriteArrayIndex None address indices arrayType value
             member self.WriteArrayRange address fromIndices toIndices arrayType value =
                 self.CommonWriteArrayRange None address fromIndices toIndices arrayType value
-            member self.WriteClassField address field value =
-                self.CommonWriteClassField None address field value
-            member self.GuardedWriteClassField guard address field value =
+            member self.WriteClassField guard address field value =
                 self.CommonWriteClassField guard address field value
 
             member self.WriteStackLocation key value = writeStackLocation key value

VSharp.SILI.Core/MemoryRegion.fs

@@ -257,9 +257,7 @@ and IMemory =
 
     abstract WriteStackLocation : stackKey -> term -> unit
 
-    abstract WriteClassField : term -> fieldId -> term -> unit
-    abstract GuardedWriteClassField : term option -> term -> fieldId -> term -> unit
-
+    abstract WriteClassField : term option -> term -> fieldId -> term -> unit
     abstract Write : IErrorReporter -> term -> term -> unit
     abstract AllocateOnStack : stackKey -> term -> unit
 

VSharp.SILI.Core/State.fs

@@ -220,16 +220,22 @@ and iteType = genericIteType<term>
 and genericIteType<'a> = {branches: (term * 'a) list; elseValue : 'a}
     with
     static member FromGvs gvs =
-        if List.length gvs < 2 then internalfail "Empty and one-element unions are forbidden!"
+        if List.length gvs < 2 then internalfail "Empty and one-element ite's are forbidden!"
         let branches, e = List.splitAt (List.length gvs - 1) gvs
         {branches = branches; elseValue =  e |> List.head |> snd}
+
     member x.mapValues mapper =
         {branches = List.map (fun (g, v) -> (g, mapper v)) x.branches; elseValue = mapper x.elseValue}
+
     member x.filter predicate =
         if predicate x.elseValue then
             {branches = List.filter (snd >> predicate) x.branches; elseValue = x.elseValue}
         else
             List.filter (snd >> predicate) x.branches |> genericIteType<'a>.FromGvs
+
+    member x.exists predicate =
+        predicate x.elseValue || List.exists (fun (g, v) -> predicate v) x.branches
+
     member x.choose mapper =
         let chooser (g, v) = Option.bind (fun w -> Some(g, w)) (mapper v)
         match mapper x.elseValue with

VSharp.SILI.Core/Terms.fs

@@ -532,59 +532,6 @@ public static int TestOverlappingCopy1(int[] a, int i)
             return 3;
         }
 
-        [TestSvm(94)]
-        public static int TestSolvingCopyOverwrittenValueUnreachable1(string[] a, string[] b)
-        {
-            if (a != null && b != null && a.Length > b.Length)
-            {
-                a[0] = "42";
-                b[0] = "4";
-                Array.Copy(a, 0, b, 0, b.Length);
-                if (b[0] != "42") // unreachable
-                {
-                    return -1;
-                }
-
-                return 0;
-            }
-
-            return 3;
-        }
-
-        [TestSvm(95)]
-        public static int TestSolvingCopyOverwrittenValueUnreachable2(string[] a, int i, string[] b)
-        {
-            if (a != null && b != null && a.Length > b.Length)
-            {
-                b[i] = "500";
-                Array.Copy(a, 0, b, 0, b.Length);
-                if (b.Length > 0 && a[i] != "500" && b[i] == "500") // unreachable
-                {
-                    return -1;
-                }
-
-                return 0;
-            }
-
-            return 3;
-        }
-
-        [TestSvm(94)]
-        public static int TestSolvingCopy8(object[] a, object[] b, int i)
-        {
-            if (a.Length > b.Length && 0 <= i && i < b.Length)
-            {
-                Array.Fill(a, "abc");
-                Array.Copy(a, b, b.Length);
-
-                if (b[i] == b[i + 1])
-                    return 42;
-                return 10;
-            }
-
-            return 3;
-        }
-
         [TestSvm(97)]
         public static int TestSolvingCopy9(object[] a, int i, object[] b)
         {
@@ -785,20 +732,6 @@ public class MyClass
             public int x;
         }
 
-        [TestSvm(88)]
-        public static int LastRecordReachability(string[] a, string[] b, int i, string s)
-        {
-            a[i] = "1";
-            b[1] = s;
-            if (b[1] != s)
-            {
-                // unreachable
-                return -1;
-            }
-
-            return 0;
-        }
-
         [TestSvm(90)]
         public static int ArrayElementsAreReferences(MyClass[] a, int i, int j)
         {
@@ -924,44 +857,6 @@ public static int ConcreteDictionaryTest(int v)
             return 0;
         }
 
-        [TestSvm(100)]
-        public static int ConcreteDictionaryTest1(int a, string 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))
-            {
-                if (res.Contains(b))
-                    return 1;
-                return 0;
-            }
-
-            return 2;
-        }
-
-        public class Person
-        {
-            public string FirstName { get; set; }
-            public string LastName { get; init; }
-        };
-        
-        [TestSvm(95)]
-        public static int IteKeyWrite(int i)
-        {
-            var a = new Person[4];
-            a[0] = new Person() {FirstName = "asd", LastName = "qwe"};
-            a[3] = new Person() {FirstName = "zxc", LastName = "vbn"};
-            var p = a[i];
-            p.FirstName = "323";
-            if (i == 0 && a[3].FirstName == "323")
-            {
-                return -1;
-            }
-
-            return 1;
-        }
-
         [TestSvm(100)]
         public static int ListContains(int a, int b)
         {
@@ -1413,33 +1308,6 @@ public static int ConcurrentDict(int a, int b)
                 return -1;
             return 0;
         }
-        [TestSvm(95)]
-        public static int TestSplittingWithCopy(int srcI, int dstI, int len)
-        {
-            string[] arr = {"a", "b", "c", "d", "e"};
-            var a = new string[5];
-            Array.Copy(arr, srcI, a, dstI, len);
-            if (a[2].Length == 3)
-                return -1;
-            return 1;
-        }
-        [TestSvm(91)]
-        public static int TestSplittingWithCopyRegionsImportance(string[] a, int i)
-        {
-            a[i] = "a";
-            a[1] = "b";
-            var b = new string[a.Length];
-            Array.Copy(a, 0, b, 0, a.Length);
-            if (i == 1 && b[i] == "a") // unreachable
-                // record b[i], "a" exists only if i != 1
-                return -1;
-            if (i != 1 && b[i] != "a") // unreachable
-            {
-                return -2;
-            }
-
-            return 1;
-        }
 
         [TestSvm(83)]
         public static int VolatileWrite()