Skip to content

Commit

Permalink
Merge pull request #331 from VSharp-team/unsafe-fixes
Browse files Browse the repository at this point in the history 
Unsafe fixes
  • Loading branch information
@oveeernight
oveeernight authored Oct 27, 2024
2 parents fa3fed0 + 8cdc162 commit 7aee14b
Show file tree
Hide file tree
Showing 3 changed files with 112 additions and 20 deletions.
7 changes: 6 additions & 1 deletion VSharp.SILI.Core/Memory.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
26 changes: 7 additions & 19 deletions VSharp.Solver/Z3.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 =
Expand All @@ -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) =
Expand Down
99 changes: 99 additions & 0 deletions VSharp.Test/Tests/Unsafe.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit 7aee14b

Please sign in to comment.