wip

VSharp.Explorer/Statistics.fs

@@ -16,7 +16,6 @@ open VSharp.Interpreter.IL
 open VSharp.Utils
 
 open CilState
-open IpOperations
 open CodeLocation
 
 type pob = {loc : codeLocation; lvl : uint; pc : pathCondition}

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/IntPtr.fs

@@ -12,7 +12,6 @@ module IntPtr =
         let ptr = MakeIntPtr term
         Memory.Write state this ptr
         Nop()
-
 
     let internal intPtrCtorFromInt (state : state) (args : term list) : term =
         assert(List.length args = 2)

VSharp.SILI.Core/MemoryRegion.fs

@@ -280,7 +280,8 @@ type heapArrayKey =
                         let! gu, u = Merging.unguardGvs ub
                         return (g &&& gl &&& gu, l::accLbs, u::accUbs)
                     }
-                let boundsPairs = List.foldBack2 unGuard lowerBounds upperBounds [True(), [], []]
+                let initialState = List.singleton (True(), List.empty, List.empty)
+                let boundsPairs = List.foldBack2 unGuard lowerBounds upperBounds initialState
                 let addresses = Merging.unguardGvs address
                 list {
                     let! gAddr, addr = addresses
@@ -716,6 +717,7 @@ module MemoryRegion =
 
     let maxTime (tree : updateTree<'a, heapAddress, 'b>) startingTime =
         RegionTree.foldl (fun m _ {key=_; value=v} -> VectorTime.max m (timeOf v)) startingTime tree
+
     let read mr key isDefault instantiate specializedReading =
         let makeSymbolic tree = instantiate mr.typ {mr with updates = tree}
         let makeDefault () =

VSharp.Solver/Z3.fs

@@ -1491,7 +1491,6 @@ module internal Z3 =
                 StateModel state
             with e -> internalfail $"MkModel: caught exception {e}"
 
-
     let private ctx = new Context()
     let private builder = Z3Builder(ctx)
 

VSharp.Test/Tests/BoxUnbox.cs

@@ -17,11 +17,11 @@ public A()
             }
         }
 
-        public struct B
+        public struct B<T>
         {
-            private double x;
+            private T x;
 
-            public B(double z)
+            public B(T z)
             {
                 x = z;
             }
@@ -45,14 +45,14 @@ private static T Cast<T> (object o)
         [TestSvm]
         public static B UnboxAny1()
         {
-            var b = new B(5);
+            var b = new B<int>(5);
             return Cast<B>(b);
         }
 
         [TestSvm]
         public static object UnboxAny2()
         {
-            var b = new B(5);
+            var b = new B<int>(5);
             return Cast<A>(b);
         }
 

VSharp.Test/Tests/Unsafe.cs

@@ -822,6 +822,32 @@ public static int DoubleReinterpretation1(int[] arr, int i, int j)
             }
         }
 
+        [TestSvm(100)]
+        public static int DoubleReinterpretation2(long a, int i)
+        {
+            var p = &a;
+            var ptr = (int*)((byte*)p + i);
+            var v = *ptr;
+            var ptr2 = (byte*)&v + 1;
+            return *ptr2;
+        }
+
+        [TestSvm(94)]
+        public static bool DoubleReinterpretation3(long a, int i, int j)
+        {
+            var b = a;
+            var p = &a;
+            var ptr = (int*)((byte*)p + i);
+            var v = *ptr;
+            ptr = (int*)((byte *)p + i);
+            *ptr = v;
+            var p2 = &b;
+            var ptr2 = (int*)((byte *)p2 + i);
+            if (*(int*)((byte *)ptr + j) == *(int*)((byte *)ptr2 + j))
+                return true;
+            return false;
+        }
+
         [TestSvm(100)]
         public static int DoubleWrite(long[] arr, int i, int v, byte v2)
         {