Merge pull request #319 from MchKosticyn/overflowCheck

Fixed overflow check

VSharp.SILI.Core/API.fs

@@ -238,6 +238,8 @@ module API =
         let (|UInt32T|_|) t = if typeOf t = typeof<uint32> then Some() else None
         let (|Int64T|_|) t = if typeOf t = typeof<int64> then Some() else None
         let (|UInt64T|_|) t = if typeOf t = typeof<uint64> then Some() else None
+        let (|IntPtrT|_|) t = if typeOf t = typeof<IntPtr> then Some() else None
+        let (|UIntPtrT|_|) t = if typeOf t = typeof<UIntPtr> then Some() else None
         let (|BoolT|_|) t = if isBool t then Some() else None
         let (|Float32T|_|) t = if typeOf t = typeof<single> then Some() else None
         let (|Float64T|_|) t = if typeOf t = typeof<double> then Some() else None

VSharp.SILI.Core/API.fsi

@@ -137,6 +137,8 @@ module API =
         val (|UInt32T|_|) : term -> option<unit>
         val (|Int64T|_|) : term -> option<unit>
         val (|UInt64T|_|) : term -> option<unit>
+        val (|IntPtrT|_|) : term -> option<unit>
+        val (|UIntPtrT|_|) : term -> option<unit>
         val (|BoolT|_|) : term -> option<unit>
         val (|Float32T|_|) : term -> option<unit>
         val (|Float64T|_|) : term -> option<unit>

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())

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