diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 25604dd0d..78a456787 100644 --- a/VSharp.SILI.Core/API.fs +++ b/VSharp.SILI.Core/API.fs @@ -238,6 +238,8 @@ module API = let (|UInt32T|_|) t = if typeOf t = typeof then Some() else None let (|Int64T|_|) t = if typeOf t = typeof then Some() else None let (|UInt64T|_|) t = if typeOf t = typeof then Some() else None + let (|IntPtrT|_|) t = if typeOf t = typeof then Some() else None + let (|UIntPtrT|_|) t = if typeOf t = typeof then Some() else None let (|BoolT|_|) t = if isBool t then Some() else None let (|Float32T|_|) t = if typeOf t = typeof then Some() else None let (|Float64T|_|) t = if typeOf t = typeof then Some() else None diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 0d3ffe18f..39a752fbd 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/VSharp.SILI.Core/API.fsi @@ -137,6 +137,8 @@ module API = val (|UInt32T|_|) : term -> option val (|Int64T|_|) : term -> option val (|UInt64T|_|) : term -> option + val (|IntPtrT|_|) : term -> option + val (|UIntPtrT|_|) : term -> option val (|BoolT|_|) : term -> option val (|Float32T|_|) : term -> option val (|Float64T|_|) : term -> option diff --git a/VSharp.SILI.Core/Arithmetics.fs b/VSharp.SILI.Core/Arithmetics.fs index fe68694d4..33a4e78c9 100644 --- a/VSharp.SILI.Core/Arithmetics.fs +++ b/VSharp.SILI.Core/Arithmetics.fs @@ -1143,33 +1143,79 @@ module internal Arithmetics = | Concrete(x, t1), Concrete(y, t2) -> let mutable noOverflow = true assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 try - if isUnsigned t1 then - ILCalculator.addOvfUn(x, y, t1) |> ignore - elif isUnsigned t2 then - ILCalculator.addOvfUn(x, y, t2) |> ignore - else ILCalculator.addOvf(x, y, t1) |> ignore + ILCalculator.addOvf(x, y, retType) |> ignore with :? System.OverflowException -> noOverflow <- false makeBool noOverflow | _ -> makeBinary OperationType.AddNoOvf x y bool + let simplifyAddNoOvfUn x y = + match x.term, y.term with + | Concrete(x, t1), Concrete(y, t2) -> + let mutable noOverflow = true + assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 + try + ILCalculator.addOvfUn(x, y, retType) |> ignore + with :? System.OverflowException -> + noOverflow <- false + makeBool noOverflow + | _ -> makeBinary OperationType.AddNoOvf_Un x y bool + let simplifyMultiplyNoOvf x y = match x.term, y.term with | Concrete(x, t1), Concrete(y, t2) -> let mutable noOverflow = true assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 try - if isUnsigned t1 then - ILCalculator.mulOvfUn(x, y, t1) |> ignore - elif isUnsigned t2 then - ILCalculator.mulOvfUn(x, y, t2) |> ignore - else ILCalculator.mulOvf(x, y, t1) |> ignore + ILCalculator.mulOvf(x, y, retType) |> ignore with :? System.OverflowException -> noOverflow <- false makeBool noOverflow | _ -> makeBinary OperationType.MultiplyNoOvf x y bool + let simplifyMultiplyNoOvfUn x y = + match x.term, y.term with + | Concrete(x, t1), Concrete(y, t2) -> + let mutable noOverflow = true + assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 + try + ILCalculator.mulOvfUn(x, y, retType) |> ignore + with :? System.OverflowException -> + noOverflow <- false + makeBool noOverflow + | _ -> makeBinary OperationType.MultiplyNoOvf_Un x y bool + + let simplifySubNoOvf x y = + match x.term, y.term with + | Concrete(x, t1), Concrete(y, t2) -> + let mutable noOverflow = true + assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 + try + ILCalculator.subOvf(x, y, retType) |> ignore + with :? System.OverflowException -> + noOverflow <- false + makeBool noOverflow + | _ -> makeBinary OperationType.SubNoOvf x y bool + + let simplifySubNoOvfUn x y = + match x.term, y.term with + | Concrete(x, t1), Concrete(y, t2) -> + let mutable noOverflow = true + assert(isNumeric t1 && isNumeric t2) + let retType = deduceSimpleArithmeticOperationTargetType t1 t2 + try + ILCalculator.subOvfUn(x, y, retType) |> ignore + with :? System.OverflowException -> + noOverflow <- false + makeBool noOverflow + | _ -> makeBinary OperationType.SubNoOvf_Un x y bool + // ------------------------------- General functions ------------------------------- let inline private deduceArithmeticTargetType x y = @@ -1226,7 +1272,11 @@ module internal Arithmetics = | OperationType.BitwiseOr | OperationType.BitwiseXor -> simplifyBitwise op x y t k | OperationType.AddNoOvf -> simplifyAddNoOvf x y |> k + | OperationType.AddNoOvf_Un -> simplifyAddNoOvfUn x y |> k | OperationType.MultiplyNoOvf -> simplifyMultiplyNoOvf x y |> k + | OperationType.MultiplyNoOvf_Un -> simplifyMultiplyNoOvfUn x y |> k + | OperationType.SubNoOvf -> simplifySubNoOvf x y |> k + | OperationType.SubNoOvf_Un -> simplifySubNoOvfUn x y |> k | _ -> internalfailf $"{op} is not a binary arithmetical operator" let simplifyUnaryOperation op x t k = @@ -1240,9 +1290,13 @@ module internal Arithmetics = match op with | OperationType.Add | OperationType.AddNoOvf + | OperationType.AddNoOvf_Un | OperationType.Subtract + | OperationType.SubNoOvf + | OperationType.SubNoOvf_Un | OperationType.Multiply | OperationType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un | OperationType.Divide | OperationType.Divide_Un | OperationType.Remainder @@ -1270,13 +1324,12 @@ module internal Arithmetics = let checkEqualZero y k = simplifyEqual y (castConcrete 0 (typeOf y)) k - // TODO: implement without using of expression AddNoOvf or MultiplyNoOvf: - // TODO: - if signed, then it should keep the sign let makeExpressionNoOvf expr = let collectConditions acc expr next into = match expr with - | Add(x, y, _) -> acc &&& simplifyAddNoOvf x y |> next - | Mul(x, y, _) -> acc &&& simplifyMultiplyNoOvf x y |> next + | Add(x, y, t) -> acc &&& (if isSigned t then simplifyAddNoOvf x y else simplifyAddNoOvfUn x y) |> next + | Sub(x, y, t) -> acc &&& (if isSigned t then simplifySubNoOvf x y else simplifySubNoOvfUn x y) |> next + | Mul(x, y, t) -> acc &&& (if isSigned t then simplifyMultiplyNoOvf x y else simplifyMultiplyNoOvfUn x y) |> next | {term = Expression _ } -> into acc | _ -> next acc Seq.singleton expr |> fold collectConditions (True()) diff --git a/VSharp.SILI.Core/Operations.fs b/VSharp.SILI.Core/Operations.fs index c3f0bda1e..6ec973f98 100644 --- a/VSharp.SILI.Core/Operations.fs +++ b/VSharp.SILI.Core/Operations.fs @@ -22,16 +22,20 @@ type OperationType = | LessOrEqual_Un = 18 | Add = 19 | AddNoOvf = 20 - | Subtract = 21 - | Divide = 22 - | Divide_Un = 23 - | Multiply = 24 - | MultiplyNoOvf = 25 - | Remainder = 26 - | Remainder_Un = 27 - | ShiftLeft = 28 - | ShiftRight = 29 - | ShiftRight_Un = 30 + | AddNoOvf_Un = 21 + | Subtract = 22 + | SubNoOvf = 23 + | SubNoOvf_Un = 24 + | Divide = 25 + | Divide_Un = 26 + | Multiply = 27 + | MultiplyNoOvf = 28 + | MultiplyNoOvf_Un = 29 + | Remainder = 30 + | Remainder_Un = 31 + | ShiftLeft = 32 + | ShiftRight = 33 + | ShiftRight_Un = 34 type StandardFunction = | Arccosine @@ -106,7 +110,11 @@ module internal Operations = | OperationType.ShiftRight | OperationType.ShiftRight_Un -> maxPriority - 3 | OperationType.AddNoOvf + | OperationType.AddNoOvf_Un | OperationType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un + | OperationType.SubNoOvf + | OperationType.SubNoOvf_Un | OperationType.Less | OperationType.Less_Un | OperationType.LessOrEqual @@ -128,8 +136,10 @@ module internal Operations = let isCommutative = function | OperationType.Add | OperationType.AddNoOvf + | OperationType.AddNoOvf_Un | OperationType.Multiply | OperationType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un | OperationType.Equal | OperationType.BitwiseAnd | OperationType.BitwiseOr @@ -169,14 +179,22 @@ module internal Operations = | OperationType.ShiftRight_Un -> " >> " | OperationType.Subtract -> " - " | OperationType.UnaryMinus -> "-%s" - | OperationType.AddNoOvf -> " + (no ovf) " - | OperationType.MultiplyNoOvf -> " * (no ovf) " + | OperationType.AddNoOvf + | OperationType.AddNoOvf_Un -> " + (no ovf) " + | OperationType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un -> " * (no ovf) " + | OperationType.SubNoOvf + | OperationType.SubNoOvf_Un -> " - (no ovf) " | _ -> "" let deduceArithmeticBinaryExpressionTargetType op x y = match op with | OperationType.AddNoOvf + | OperationType.AddNoOvf_Un | OperationType.MultiplyNoOvf + | OperationType.MultiplyNoOvf_Un + | OperationType.SubNoOvf + | OperationType.SubNoOvf_Un | OperationType.Equal | OperationType.NotEqual | OperationType.Greater diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index 947789cbf..31e6c168a 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -64,6 +64,14 @@ module TypeUtils = module UInt64 = let Zero() = MakeNumber 0UL let MaxValue() = MakeNumber UInt64.MaxValue + module IntPtr = + let Zero() = MakeNumber IntPtr.Zero + let MinusOne() = MakeNumber (IntPtr(-1)) + let MinValue() = MakeNumber IntPtr.MinValue + let MaxValue() = MakeNumber IntPtr.MaxValue + module UIntPtr = + let Zero() = MakeNumber UIntPtr.Zero + let MaxValue() = MakeNumber UIntPtr.MaxValue module internal InstructionsSet = @@ -276,7 +284,9 @@ module internal InstructionsSet = match TypeOf term with | Types.Bool -> k <| Types.Cast term TypeUtils.uint32Type | t when t = typeof || t = typeof -> k term - | t when TypeUtils.isIntegral t -> k <| Types.Cast term (TypeUtils.signedToUnsigned t) // no specs found about overflows + | t when TypeUtils.isIntegral t -> + let unsignedType = TypeUtils.signedToUnsigned t + k <| Types.Cast term unsignedType // no specs found about overflows | _ -> k term let performUnsignedIntegerOperation op (cilState : cilState) = @@ -1666,216 +1676,80 @@ type ILInterpreter() as this = let rem x y = API.PerformBinaryOperation OperationType.Remainder_Un x y id this.CommonUnsignedDivRem true rem cilState - member private this.UnsignedCheckOverflow checkOverflowForUnsigned (cilState : cilState) = - let y, x = cilState.Pop2() - match y, x with - | Int64T, _ - | _, Int64T - | UInt64T, _ - | _, UInt64T -> - let x = makeUnsignedInteger x id - let y = makeUnsignedInteger y id - let max = TypeUtils.UInt64.MaxValue() - let zero = TypeUtils.UInt64.Zero() - checkOverflowForUnsigned zero max x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic - | _ when TypeUtils.isIntegralTerm x && TypeUtils.isIntegralTerm y -> - let x, y = makeUnsignedInteger x id, makeUnsignedInteger y id - let max = TypeUtils.UInt32.MaxValue() - let zero = TypeUtils.UInt32.Zero() - checkOverflowForUnsigned zero max x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic - | _ -> internalfail "incompatible operands for UnsignedCheckOverflow" - - member private this.SignedCheckOverflow checkOverflow (cilState : cilState) = - let y, x = cilState.Pop2() - match y, x with - | Int64T, _ - | _, Int64T -> - let min = TypeUtils.Int64.MinValue() - let max = TypeUtils.Int64.MaxValue() - let zero = TypeUtils.Int64.Zero() - let minusOne = TypeUtils.Int64.MinusOne() - checkOverflow min max zero minusOne x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic - | UInt64T, _ - | _, UInt64T -> __unreachable__() // instead of add_ovf should be called add_ovf_un - | FloatT, _ - | _, FloatT -> __unreachable__() // only integers - | _ -> - let min = TypeUtils.Int32.MinValue() - let max = TypeUtils.Int32.MaxValue() - let zero = TypeUtils.Int32.Zero() - let minusOne = TypeUtils.Int32.MinusOne() - checkOverflow min max zero minusOne x y cilState // TODO: maybe rearrange x and y if y is concrete and x is symbolic - member private this.Add_ovf (cilState : cilState) = // min <= x + y <= max - let checkOverflow min max zero _ x y (cilState : cilState) = - let (>>=) = API.Arithmetics.(>>=) - let xMoreThan0 state k = k (x >>= zero, state) - let yMoreThan0 state k = k (y >>= zero, state) - let checkOverflowWhenMoreThan0 (state : state) k = // x >= 0 && y >= 0 - PerformBinaryOperation OperationType.Subtract max y (fun diff -> - k (diff >>= x, state)) - let checkOverflowWhenLessThan0 (state : state) k = - PerformBinaryOperation OperationType.Subtract min y (fun diff -> - k (x >>= diff, state)) - let add (cilState : cilState) k = // no overflow - PerformBinaryOperation OperationType.Add x y (fun sum -> - cilState.Push sum - k [cilState]) - cilState.StatedConditionalExecutionCIL xMoreThan0 - (fun cilState -> // x >= 0 - cilState.StatedConditionalExecutionCIL yMoreThan0 - (fun cilState -> // y >= 0 - cilState.StatedConditionalExecutionCIL - checkOverflowWhenMoreThan0 - add - (this.Raise this.OverflowException)) - add) - (fun cilState -> // x < 0 - cilState.StatedConditionalExecutionCIL yMoreThan0 - add - (fun cilState -> // x < 0 && y < 0 - cilState.StatedConditionalExecutionCIL - checkOverflowWhenLessThan0 - add - (this.Raise this.OverflowException))) - id - this.SignedCheckOverflow checkOverflow cilState + let y, x = cilState.Pop2() + let fits state k = k (PerformBinaryOperation OperationType.AddNoOvf x y id, state) + let add (cilState : cilState) k = // no overflow + PerformBinaryOperation OperationType.Add x y (fun sum -> + cilState.Push sum + k [cilState]) + cilState.StatedConditionalExecutionCIL fits + add + (this.Raise this.OverflowException) + id member private this.Mul_ovf (cilState : cilState) = // min <= x * y <= max - let checkOverflow min max zero _ x y (cilState : cilState) = - let (>>=) = API.Arithmetics.(>>=) - let (>>) = API.Arithmetics.(>>) - let isZero state k = k ((x === zero) ||| (y === zero), state) - let xMoreThan0 state k = k (x >> zero, state) - let yMoreThan0 state k = k (y >> zero, state) - let checkOverflowWhenXM0YM0 (state : state) k = // x > 0 && y > 0 - PerformBinaryOperation OperationType.Divide max y (fun quotient -> - k (quotient >>= x, state)) - let checkOverflowWhenXL0YL0 (state : state) k = // x < 0 && y < 0 - PerformBinaryOperation OperationType.Divide max y (fun quotient -> - k (x >>= quotient, state)) - let checkOverflowWhenXM0YL0 (state : state) k = // x > 0 && y < 0 - PerformBinaryOperation OperationType.Divide min x (fun quotient -> - k (y >>= quotient, state)) - let checkOverflowWhenXL0YM0 (state : state) k = // x < 0 && y > 0 - PerformBinaryOperation OperationType.Divide min y (fun quotient -> - k (x >>= quotient, state)) - let mul (cilState : cilState) k = // no overflow - PerformBinaryOperation OperationType.Multiply x y (fun res -> - cilState.Push res - k [cilState]) - cilState.StatedConditionalExecutionCIL isZero - (fun cilState k -> - cilState.Push zero - k [cilState]) - (fun cilState -> - cilState.StatedConditionalExecutionCIL xMoreThan0 - (fun cilState -> // x > 0 - cilState.StatedConditionalExecutionCIL yMoreThan0 - (fun cilState -> // y > 0 - cilState.StatedConditionalExecutionCIL checkOverflowWhenXM0YM0 - mul - (this.Raise this.OverflowException)) - (fun cilState -> // y < 0 - cilState.StatedConditionalExecutionCIL checkOverflowWhenXM0YL0 - mul - (this.Raise this.OverflowException))) - (fun cilState -> // x < 0 - cilState.StatedConditionalExecutionCIL yMoreThan0 - (fun cilState -> // y > 0 - cilState.StatedConditionalExecutionCIL checkOverflowWhenXL0YM0 - mul - (this.Raise this.OverflowException)) - (fun cilState k -> // y < 0 - cilState.StatedConditionalExecutionCIL checkOverflowWhenXL0YL0 - mul - (this.Raise this.OverflowException) - k))) - id - this.SignedCheckOverflow checkOverflow cilState + let y, x = cilState.Pop2() + let fits state k = k (PerformBinaryOperation OperationType.MultiplyNoOvf x y id, state) + let mul (cilState : cilState) k = // no overflow + PerformBinaryOperation OperationType.Multiply x y (fun res -> + cilState.Push res + k [cilState]) + cilState.StatedConditionalExecutionCIL fits + mul + (this.Raise this.OverflowException) + id member private this.Add_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned _ max x y (cilState : cilState) = - let (>>=) = API.Arithmetics.(>>=) - cilState.StatedConditionalExecutionCIL - (fun state k -> - PerformBinaryOperation OperationType.Subtract max x (fun diff -> - k (diff >>= y, state))) - (fun cilState k -> PerformBinaryOperation OperationType.Add x y (fun res -> - cilState.Push res - k [cilState])) - (this.Raise this.OverflowException) - id - this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + let y, x = cilState.Pop2() + let fits state k = k (PerformBinaryOperation OperationType.AddNoOvf_Un x y id, state) + let add (cilState : cilState) k = + PerformBinaryOperation OperationType.Add x y (fun res -> + cilState.Push res + k [cilState]) + cilState.StatedConditionalExecutionCIL fits + add + (this.Raise this.OverflowException) + id member private this.Mul_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned zero max x y (cilState : cilState) = - let isZero state k = k ((x === zero) ||| (y === zero), state) - let zeroCase (cilState : cilState) k = - cilState.Push zero - List.singleton cilState |> k - let checkOverflow (cilState : cilState) k = - let evalCondition state k = - PerformBinaryOperation OperationType.Divide max x (fun quotient -> - k (Arithmetics.GreaterOrEqualUn quotient y, state)) - let mul (cilState : cilState) k = - PerformBinaryOperation OperationType.Multiply x y (fun res -> - cilState.Push res - List.singleton cilState |> k) - cilState.StatedConditionalExecutionCIL evalCondition - mul - (this.Raise this.OverflowException) - k - cilState.StatedConditionalExecutionCIL isZero - zeroCase - checkOverflow - id - this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + let y, x = cilState.Pop2() + let fits state k = k (PerformBinaryOperation OperationType.MultiplyNoOvf_Un x y id, state) + let mul (cilState : cilState) k = + PerformBinaryOperation OperationType.Multiply x y (fun res -> + cilState.Push res + List.singleton cilState |> k) + cilState.StatedConditionalExecutionCIL fits + mul + (this.Raise this.OverflowException) + id member private this.Sub_ovf_un (cilState : cilState) = - let checkOverflowForUnsigned _ _ x y (cilState : cilState) = - let (>>=) = API.Arithmetics.(>>=) - cilState.StatedConditionalExecutionCIL - (fun state k -> k (x >>= y, state)) - (fun (cilState : cilState) k -> // no overflow - PerformBinaryOperation OperationType.Subtract x y (fun res -> - cilState.Push res - k [cilState])) - (this.Raise this.OverflowException) - id - this.UnsignedCheckOverflow checkOverflowForUnsigned cilState + let y, x = cilState.Pop2() + cilState.StatedConditionalExecutionCIL + (fun state k -> k (Arithmetics.GreaterOrEqualUn x y, state)) + (fun (cilState : cilState) k -> // no overflow + PerformBinaryOperation OperationType.Subtract x y (fun res -> + cilState.Push res + k [cilState])) + (this.Raise this.OverflowException) + id member private this.Sub_ovf (cilState : cilState) = // there is no way to reduce current operation to [x `Add_Ovf` (-y)] // min <= x - y <= max - let checkOverflowForSigned min max zero minusOne x y (cilState : cilState) = - let (>>=) = API.Arithmetics.(>>=) - let xGreaterEqualZero state k = k (x >>= zero, state) - let sub (cilState : cilState) k = // no overflow - PerformBinaryOperation OperationType.Subtract x y (fun res -> - cilState.Push res - k [cilState]) - cilState.StatedConditionalExecutionCIL xGreaterEqualZero - (fun cilState -> // x >= 0 => max - x >= 0 => no overflow for [-1 * (max - x)] - cilState.StatedConditionalExecutionCIL - (fun state k -> - PerformBinaryOperation OperationType.Subtract max x (fun diff -> - PerformBinaryOperation OperationType.Multiply diff minusOne (fun minusDiff -> - k (y >>= minusDiff, state)))) // y >= -(max - x) - sub - (this.Raise this.OverflowException)) - (fun cilState -> // x < 0 => no overflow for [min - x] # x < 0 => [min - x] != min => no overflow for (-1) * [min - x] - cilState.StatedConditionalExecutionCIL - (fun state k -> - PerformBinaryOperation OperationType.Subtract min x (fun diff -> - PerformBinaryOperation OperationType.Multiply diff minusOne (fun minusDiff -> - k (minusDiff >>= y, state)))) // -(min - x) >= y - sub - (this.Raise this.OverflowException)) - id - this.SignedCheckOverflow checkOverflowForSigned cilState + let y, x = cilState.Pop2() + let fits state k = k (PerformBinaryOperation OperationType.SubNoOvf x y id, state) + let sub (cilState : cilState) k = // no overflow + PerformBinaryOperation OperationType.Subtract x y (fun res -> + cilState.Push res + k [cilState]) + cilState.StatedConditionalExecutionCIL fits + sub + (this.Raise this.OverflowException) + id member private x.Newarr (m : Method) offset (cilState : cilState) = let (>>=) = API.Arithmetics.(>>=) diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index 2b6bbf937..35abf5326 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -464,6 +464,10 @@ module internal Z3 = let left, right = x.ExtendIfNeed operands true ctx.MkBVAddNoOverflow(left, right, true) + member private x.MkBVAddNoOverflowUn operands : BoolExpr = + let left, right = x.ExtendIfNeed operands false + ctx.MkBVAddNoOverflow(left, right, false) + member private x.MkBVMulT typ operands : BitVecExpr = x.ChangeSizeIfNeed operands typ |> ctx.MkBVMul @@ -477,12 +481,28 @@ module internal Z3 = let left, right = x.ExtendIfNeed operands true ctx.MkBVMulNoOverflow(left, right, true) + member private x.MkBVMulNoOverflowUn operands : BoolExpr = + let left, right = x.ExtendIfNeed operands false + ctx.MkBVMulNoOverflow(left, right, false) + member private x.MkBVSubT typ operands : BitVecExpr = x.ChangeSizeIfNeed operands typ |> ctx.MkBVSub member private x.MkBVSub operands : BitVecExpr = x.ExtendIfNeed operands true |> ctx.MkBVSub + member private x.MkBVSubNoUnderflow operands : BoolExpr = + let left, right = x.ExtendIfNeed operands true + ctx.MkBVSubNoUnderflow(left, right, true) + + member private x.MkBVSubNoUnderflowUn operands : BoolExpr = + let left, right = x.ExtendIfNeed operands false + ctx.MkBVSubNoUnderflow(left, right, false) + + member private x.MkBVSubNoOverflow operands : BoolExpr = + let left, right = x.ExtendIfNeed operands true + ctx.MkBVSubNoOverflow(left, right) + member private x.MkBVSDivT typ operands : BitVecExpr = assert(isSigned typ) x.ChangeSizeIfNeed operands typ |> ctx.MkBVSDiv @@ -654,12 +674,19 @@ module internal Z3 = let operation (l, r) = x.MkAnd(x.MkBVAddNoUnderflow(l, r), x.MkBVAddNoOverflow(l, r)) x.MakeBinary operation args + | OperationType.AddNoOvf_Un -> x.MakeBinary x.MkBVAddNoOverflowUn args | OperationType.Multiply -> x.MakeBinary (x.MkBVMulT typ) args | OperationType.MultiplyNoOvf -> let operation (l, r) = x.MkAnd(x.MkBVMulNoUnderflow(l, r), x.MkBVMulNoOverflow(l, r)) x.MakeBinary operation args + | OperationType.MultiplyNoOvf_Un -> x.MakeBinary x.MkBVMulNoOverflowUn args | OperationType.Subtract -> x.MakeBinary (x.MkBVSubT typ) args + | OperationType.SubNoOvf -> + let operation (l, r) = + x.MkAnd(x.MkBVSubNoOverflow(l, r), x.MkBVSubNoUnderflow(l, r)) + x.MakeBinary operation args + | OperationType.SubNoOvf_Un -> x.MakeBinary x.MkBVSubNoUnderflowUn args | OperationType.Divide -> x.MakeBinary (x.MkBVSDivT typ) args | OperationType.Divide_Un -> x.MakeBinary (x.MkBVUDivT typ) args | OperationType.Remainder -> x.MakeBinary (x.MkBVSRemT typ) args diff --git a/VSharp.Test/Tests/Arithmetics.cs b/VSharp.Test/Tests/Arithmetics.cs index 29d3061aa..fa5c1b26e 100644 --- a/VSharp.Test/Tests/Arithmetics.cs +++ b/VSharp.Test/Tests/Arithmetics.cs @@ -182,6 +182,12 @@ public static UInt64 Mul_Ovf_U64(UInt64 a, UInt64 b) return checked(a * b); } + [TestSvm] + public static IntPtr Mul_Ovf_IntPtr(int x) + { + return checked(unchecked((IntPtr)(uint)x) * sizeof(long)); + } + [TestSvm] public static int Mul_No_OverFlow1() { diff --git a/VSharp.Utils/TypeUtils.fs b/VSharp.Utils/TypeUtils.fs index 0780e31ba..6a1038039 100644 --- a/VSharp.Utils/TypeUtils.fs +++ b/VSharp.Utils/TypeUtils.fs @@ -569,6 +569,8 @@ module TypeUtils = || isLong x && isULong y || isULong x && isLong y if isReal x || isReal y (* || areSameButSignedAndUnsigned *) then failDeduceBinaryTargetType op x y + elif isNative x then x + elif isNative y then y elif isLong x then x // DO NOT REORDER THESE elif's! elif isLong y then y elif isULong x then x