Merge pull request #331 from VSharp-team/unsafe-fixes

Unsafe fixes

Author: oveeernight

VSharp.SILI.Core/Memory.fs

@@ -1089,7 +1089,12 @@ module internal Memory =
                     match elementOffset.term with
                     | Concrete(:? int as i, _) when (i + viewSize) % concreteElementSize = 0 -> (i + viewSize) / concreteElementSize
                     // NOTE: if offset inside element > 0 then one more element is needed
-                    | _ -> (viewSize / concreteElementSize) + 1
+                    | _ ->
+                        let count = (viewSize / concreteElementSize) + 1
+                        // it is possible that two elements are affected, so we add 1, otherwise reading result will be
+                        // an empty slice
+                        if viewSize % concreteElementSize >= 2 then count + 1
+                        else count
                 let getElement currentOffset i =
                     let linearIndex = makeNumber i |> add firstElement
                     let indices = delinearizeArrayIndex linearIndex lens lbs

VSharp.Solver/Z3.fs

@@ -722,12 +722,6 @@ module internal Z3 =
             elif exprSize > size then ctx.MkExtract(size - 1u, 0u, expr)
             else ctx.MkSignExt(size - exprSize, expr)
 
-        member private x.ReverseBytes (expr : BitVecExpr) =
-            let size = int expr.SortSize
-            assert(size % 8 = 0)
-            let bytes = List.init (size / 8) (fun byte -> ctx.MkExtract(uint ((byte + 1) * 8) - 1u, uint (byte * 8), expr))
-            List.reduce (fun x y -> ctx.MkConcat(x, y)) bytes
-
         member private x.ComputeSliceBounds assumptions cuts termSortSize =
             assert(termSortSize % 8u = 0u && termSortSize > 0u)
             let zero = ctx.MkBV(0, termSortSize)
@@ -806,10 +800,8 @@ module internal Z3 =
             | _ -> x.EncodeTerm slice, List.empty
 
         member private x.EncodeCombine slices typ =
-            let size = x.SizeOfBV typ
-            let res = ctx.MkBV(0, size)
-            let window = res.SortSize
-            let windowExpr = ctx.MkNumeral(window, x.Type2Sort(Types.IndexType)) :?> BitVecExpr
+            let window = x.SizeOfBV typ
+            let res = ctx.MkBV(0, window)
             let addOneSlice (res, assumptions) slice =
                 let term, cuts = x.EncodeSlice slice
                 let t =
@@ -831,25 +823,21 @@ module internal Z3 =
                 let sliceSize = x.MkBVSub(rBit, lBit)
                 let zero = ctx.MkBV(0, termSize)
                 let intersects = x.MkBVSGT(sliceSize, zero)
-                let term = x.ReverseBytes t
                 let left = x.ExtractOrExtend lBit termSize
-                let term = x.MkBVShl(term, left)
-                let cutRight = x.ExtractOrExtend (x.MkBVSub(sizeExpr, rBit)) termSize
+                let right = x.ExtractOrExtend rBit termSize
+                let cutRight = x.MkBVSub(sizeExpr, right)
+                let term = x.MkBVShl(t, cutRight)
                 let term = x.MkBVLShr(term, x.MkBVAdd(left, cutRight))
                 let term =
                     if termSize > window then ctx.MkExtract(window - 1u, 0u, term)
                     else ctx.MkZeroExt(window - termSize, term)
                 let changedTermSize = term.SortSize
-                let w = x.ExtractOrExtend windowExpr changedTermSize
                 let pos = x.ExtractOrExtend posBit changedTermSize
-                let sliceSize = x.ExtractOrExtend sliceSize changedTermSize
-                let shift = x.MkBVSub(w, x.MkBVAdd(pos, sliceSize))
-                let part = x.MkBVShl(term, shift)
+                let part = x.MkBVShl(term, pos)
                 let res = x.MkITE(intersects, x.MkBVOr(res, part), res) :?> BitVecExpr
                 res, assumptions
             let result, assumptions = List.fold addOneSlice (res, List.empty) slices
-            let result = x.ReverseBytes result
-            let result = x.CreateCombineResult result typ size
+            let result = x.CreateCombineResult result typ window
             {expr = result; assumptions = assumptions}
 
         member private x.EncodeApplication sf typ (args : Expr array) =

VSharp.Test/Tests/Unsafe.cs

@@ -335,6 +335,89 @@ public static bool ArraySymbolicUnsafeWrite(int i)
             else
                 return true;
         }
+        
+        [TestSvm(95)]
+        public static bool ArraySymbolicUnsafeWrite11(int i, int j)
+        {
+            var array = new long[] {1, 2, 3, 4, 5};
+            fixed (long* ptr = &array[0])
+            {
+                var ptr2 = (byte*) ptr;
+                var ptr3 = ptr2 + i;
+                *ptr3 = 67;
+                var ptr4 = (int*)(ptr2 + j);
+                *ptr4 = 23181328;
+            }
+
+            if (i == 1 && j == 2 && array[0] != 1519211528961L)
+                return false;
+
+            return true;
+        }
+        
+        [TestSvm(95)]
+        public static bool ArraySymbolicUnsafeWrite12(int i, int j)
+        {
+            var array = new long[] { 1, 2, 3, 4, 5 };
+            fixed (long* ptr = &array[0])
+            {
+                var ptr1 = (byte*) ptr;
+                var ptr3 = (int*)(ptr1 + i);
+                *ptr3 = 67;
+                var ptr4 = (byte*)(ptr1 + i);
+                *ptr4 = 87;   
+            }
+
+            if (i == 2 && array[0] != 5701633)
+                return false;
+
+            return true;
+        }
+        
+        [TestSvm(94)]
+        public static bool ArrayWriteTargetingTwoElements(int i, int j)
+        {
+            var array = new long[] { 1, 2, 3, 4, 5 };
+            fixed (long* ptr = &array[0])
+            {
+                var ptr1 = (byte*) ptr;
+                var ptr3 = (short*)(ptr1 + i);
+                *ptr3 = 67;
+            }
+
+            if (i == 7 && array[1] == 2)
+                return false;
+
+            return true;
+        }
+
+        struct SomeStruct
+        {
+            public int x1;
+            public int x2;
+            public int x3;
+            public int x4;
+            public int x5;
+        }
+        
+        [TestSvm(96)]
+        public static bool ArrayWriteTargetingThreeElements(int i, int j)
+        {
+            var array = new long[] { 1, 2, 3, 4, 5 };
+            fixed (long* ptr = &array[0])
+            {
+                var ptr1 = (byte*) ptr;
+                var ptr3 = (SomeStruct*)(ptr1 + i);
+                var value = new SomeStruct() {x1 = 4455, x2 = 4143, x3 = 31323, x4 = 44, x5 = 3243};
+                *ptr3 = value;
+            }
+
+            // array[3] is affected by writing struct
+            if (i == 6 && array[3] == 4)
+                return false;
+
+            return true;
+        }
 
         [TestSvm(97)]
         public static bool ArraySymbolicUnsafeWrite2(int i)
@@ -808,6 +891,22 @@ public static int DoubleReinterpretation(long a, int i, int j)
             *ptr = v;
             return *(int*)((byte*)ptr + j);
         }
+        
+        [TestSvm(94)]
+        public static bool DoubleReinterpretation4(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 DoubleReinterpretation1(int[] arr, int i, int j)