Merge pull request #282 from mxprshn/cecil-fixes

Type solver & mock with enums fixes

.github/workflows/build_vsharp.yml

@@ -24,8 +24,8 @@ jobs:
     - uses: actions/upload-artifact@v3
       with:
         name: runner
-        path: ./VSharp.Runner/bin/DebugTailRec/netcoreapp6.0
+        path: ./VSharp.Runner/bin/DebugTailRec/net7.0
     - uses: actions/upload-artifact@v3
       with:
         name: test_runner
-        path: ./VSharp.TestRunner/bin/DebugTailRec/netcoreapp6.0
+        path: ./VSharp.TestRunner/bin/DebugTailRec/net7.0

VSharp.IL/MethodBody.fs

@@ -137,7 +137,7 @@ type MethodWithBody internal (m : MethodBase) =
     member x.GenericArguments with get() = genericArguments.Force()
     member x.GetGenericMethodDefinition() =
         match m with
-        | :? MethodInfo as m -> if isGenericMethod then m.GetGenericMethodDefinition() else m
+        | :? MethodInfo as m -> if isGenericMethod then Reflection.getGenericMethodDefinition m else m
         | _ -> internalfailf $"Asking generic method definition for non-method {x}"
     member x.GetGenericArguments() =
         match m with
@@ -235,6 +235,10 @@ type MethodWithBody internal (m : MethodBase) =
             match y with
             | :? MethodWithBody as y -> Reflection.compareMethods (x :> Core.IMethod).MethodBase (y :> Core.IMethod).MethodBase
             | _ -> -1
+        override x.ResolveOverrideInType t = x.ResolveOverrideInType t
+        override x.CanBeOverriddenInType t = x.CanBeOverriden t
+        override x.IsImplementedInType t = x.IsImplementedInType t
+
         // TODO: make it private!
         override x.MethodBase : MethodBase = m
 
@@ -293,6 +297,19 @@ type MethodWithBody internal (m : MethodBase) =
         let calledMethod = x.ResolveMethodFromMetadata (pos + Offset.from opCode.Size)
         opCode, calledMethod
 
+    member x.ResolveOverrideInType t =
+        match m with
+        | :? ConstructorInfo when m.DeclaringType = t -> x
+        | :? MethodInfo as mi ->
+            (Reflection.resolveOverridingMethod t mi :> MethodBase) |> MethodWithBody.InstantiateNew
+        | _ -> __unreachable__()
+
+    member x.IsImplementedInType t =
+        match m with
+        | :? ConstructorInfo -> m.DeclaringType = t
+        | :? MethodInfo as mi -> Reflection.typeImplementsMethod t mi
+        | _ -> __unreachable__()
+
 module MethodBody =
 
     let private operandType2operandSize = [| 4<offsets>; 4<offsets>; 4<offsets>; 8<offsets>; 4<offsets>

VSharp.InternalCalls/Interlocked.fs

@@ -36,15 +36,19 @@ module internal Interlocked =
         let location, value, compared = args[1], args[2], args[3]
         compareExchange interpreter cilState location value compared
 
-    let intCompareExchange (interpreter : IInterpreter) cilState (args : term list) =
+    let commonCompareExchange (interpreter : IInterpreter) cilState (args : term list) =
         assert(List.length args = 3)
         let location, value, compared = args[0], args[1], args[2]
         compareExchange interpreter cilState location value compared
 
+    let intCompareExchange (interpreter : IInterpreter) cilState (args : term list) =
+        commonCompareExchange interpreter cilState args
+
+    let int64CompareExchange (interpreter : IInterpreter) cilState (args : term list) =
+        commonCompareExchange interpreter cilState args
+
     let intPtrCompareExchange (interpreter : IInterpreter) cilState (args : term list) =
-        assert(List.length args = 3)
-        let location, value, compared = args[0], args[1], args[2]
-        compareExchange interpreter cilState location value compared
+        commonCompareExchange interpreter cilState args
 
     let genericExchange (interpreter : IInterpreter) cilState (args : term list) =
         assert(List.length args = 3)
@@ -56,17 +60,17 @@ module internal Interlocked =
         let location, value = args[0], args[1]
         exchange interpreter cilState location value
 
-    let intExchangeAdd (interpreter : IInterpreter) cilState (args : term list) =
+    let commonExchangeAdd (interpreter : IInterpreter) cilState (args : term list) =
         assert(List.length args = 2)
         let location, value = args[0], args[1]
         let value = Arithmetics.Add (read cilState location) value
         exchange interpreter cilState location value
 
+    let intExchangeAdd (interpreter : IInterpreter) cilState (args : term list) =
+        commonExchangeAdd interpreter cilState args
+
     let longExchangeAdd (interpreter : IInterpreter) cilState (args : term list) =
-        assert(List.length args = 2)
-        let location, value = args[0], args[1]
-        let value = Arithmetics.Add (read cilState location) value
-        exchange interpreter cilState location value
+        commonExchangeAdd interpreter cilState args
 
     let memoryBarrier (_ : state) (_ : term list) : term =
         Nop()

VSharp.InternalCalls/Interlocked.fsi

@@ -13,6 +13,9 @@ module internal Interlocked =
     [<Implements("System.Int32 System.Threading.Interlocked.CompareExchange(System.Int32&, System.Int32, System.Int32)")>]
     val intCompareExchange : IInterpreter -> cilState -> term list -> cilState list
 
+    [<Implements("System.Int64 System.Threading.Interlocked.CompareExchange(System.Int64&, System.Int64, System.Int64)")>]
+    val int64CompareExchange : IInterpreter -> cilState -> term list -> cilState list
+
     [<Implements("System.IntPtr System.Threading.Interlocked.CompareExchange(System.IntPtr&, System.IntPtr, System.IntPtr)")>]
     [<Implements("System.Object System.Runtime.InteropServices.GCHandle.InternalCompareExchange(System.IntPtr, System.Object, System.Object)")>]
     val intPtrCompareExchange : IInterpreter -> cilState -> term list -> cilState list

VSharp.InternalCalls/SR.fs

@@ -119,3 +119,7 @@ module SR =
     let internal get_Arg_NotImplementedException (state : state) (args : term list) : term =
         assert(List.length args = 0)
         Memory.AllocateString "get_Arg_NotImplementedException" state
+
+    let internal get_Argument_InvalidTypeWithPointersNotSupported (state : state) (args : term list) : term =
+        assert(List.length args = 0)
+        Memory.AllocateString "get_Argument_InvalidTypeWithPointersNotSupported" state

VSharp.InternalCalls/SR.fsi

@@ -89,3 +89,6 @@ module internal SR =
 
     [<Implements("System.String System.SR.get_Arg_NotImplementedException()")>]
     val get_Arg_NotImplementedException : state -> term list -> term
+
+    [<Implements("System.String System.SR.get_Argument_InvalidTypeWithPointersNotSupported()")>]
+    val get_Argument_InvalidTypeWithPointersNotSupported : state -> term list -> term

VSharp.SILI.Core/API.fs

@@ -58,6 +58,8 @@ module API =
 
     let ResolveCallVirt state thisAddress thisType ancestorMethod = TypeSolver.getCallVirtCandidates state thisAddress thisType ancestorMethod
 
+    let KeepOnlyMock state thisAddress = TypeSolver.keepOnlyMock state thisAddress
+
     let MethodMockAndCall state method this args = MethodMocking.mockAndCall state method this args Default
     let ExternMockAndCall state method this args = MethodMocking.mockAndCall state method this args Extern
 

VSharp.SILI.Core/API.fsi

@@ -33,6 +33,7 @@ module API =
     val SolveGenericMethodParameters : typeStorage -> IMethod -> (symbolicType[] * symbolicType[]) option
     val SolveThisType : state -> term -> unit
     val ResolveCallVirt : state -> term -> Type -> IMethod -> symbolicType seq
+    val KeepOnlyMock : state -> term -> unit
 
     val MethodMockAndCall : state -> IMethod -> term option -> term list -> term option
     val ExternMockAndCall : state -> IMethod -> term option -> term list -> term option

VSharp.SILI.Core/State.fs

@@ -384,6 +384,8 @@ and candidates private(publicBuiltInTypes, publicUserTypes, privateUserTypes, re
             if mock.IsSome then yield mock.Value |> MockType
         }
 
+    member x.HasMock = Option.isSome mock
+
     static member Empty() =
         candidates(Seq.empty, None, Reflection.mscorlibAssembly)
 
@@ -402,12 +404,16 @@ and candidates private(publicBuiltInTypes, publicUserTypes, privateUserTypes, re
         let publicUserTypes = Seq.filter typesPredicate publicUserTypes
         let privateUserTypes = Seq.filter typesPredicate privateUserTypes
         let rest = Seq.filter typesPredicate rest
-        let mock =
-            match mock with
-            | Some typeMock -> refineMock typeMock
-            | None -> None
+        let mock = Option.bind refineMock mock
         candidates(publicBuiltInTypes, publicUserTypes, privateUserTypes, rest, mock, userAssembly)
 
+    member x.KeepOnlyMock() =
+        candidates(Seq.empty, Seq.empty, Seq.empty, Seq.empty, mock, userAssembly)
+
+    member x.DistinctBy(keySelector : Type -> 'a) =
+        let distinctOrderedTypes = Seq.distinctBy keySelector orderedTypes
+        candidates(distinctOrderedTypes, mock, userAssembly)
+
     member x.Take(count) =
         let types =
             match mock with

VSharp.SILI.Core/Terms.fs

@@ -22,6 +22,9 @@ type IMethod =
     abstract ContainsGenericParameters : bool
     abstract GenericArguments : Type[]
     abstract SubstituteTypeVariables : (Type -> Type) -> IMethod
+    abstract ResolveOverrideInType : Type -> IMethod
+    abstract CanBeOverriddenInType : Type -> bool
+    abstract IsImplementedInType : Type -> bool
     abstract MethodBase : System.Reflection.MethodBase
 
 [<CustomEquality;CustomComparison>]

VSharp.SILI.Core/TypeSolver.fs

@@ -115,13 +115,13 @@ module TypeSolver =
         }
 
     let private enumerateNonAbstractSupertypes predicate (typ : Type) =
-        let rec getNonAbstractSupertypes predicate (t: Type) =
-            if typ = null || typ.IsAbstract then List.empty
+        let rec getNonAbstractSupertypes (t: Type) (supertypes : Type list) =
+            if t = null then supertypes
             else
-                let supertypes = getNonAbstractSupertypes predicate t.BaseType
-                if predicate typ then typ::supertypes else supertypes
+                let supertypes = if not t.IsAbstract && predicate t then t::supertypes else supertypes
+                getNonAbstractSupertypes t.BaseType supertypes
         assert userAssembly.IsSome
-        let types = getNonAbstractSupertypes predicate typ
+        let types = getNonAbstractSupertypes typ List.empty
         candidates(types, None, userAssembly.Value)
 
     let private hasSubtypes (t : Type) =
@@ -484,7 +484,18 @@ module TypeSolver =
         | TypeSat _ -> ()
         | TypeUnsat -> internalfail "Refining types: branch is unreachable"
 
-    let getCallVirtCandidates state (thisRef : heapAddress) (thisType: Type) (ancestorMethod : IMethod) =
+    let keepOnlyMock state thisRef =
+        match thisRef.term with
+        | HeapRef({term = ConcreteHeapAddress thisAddress}, _) when VectorTime.less state.startingTime thisAddress -> ()
+        | HeapRef(thisAddress, _) ->
+            let typeStorage = state.typeStorage
+            match typeStorage[thisAddress] with
+            | Some candidates ->
+                typeStorage[thisAddress] <- candidates.KeepOnlyMock()
+            | None -> ()
+        | _ -> ()
+
+    let getCallVirtCandidates state (thisRef : heapAddress) (thisType : Type) (ancestorMethod : IMethod) =
         userAssembly <- Some ancestorMethod.DeclaringType.Assembly
         match thisRef.term with
         | HeapRef({term = ConcreteHeapAddress thisAddress}, _) when VectorTime.less state.startingTime thisAddress ->
@@ -493,21 +504,20 @@ module TypeSolver =
             let thisConstraints = List.singleton thisType |> typeConstraints.FromSuperTypes
             let typeStorage = state.typeStorage
             typeStorage.AddConstraint thisAddress thisConstraints
-            let ancestorMethod = ancestorMethod.MethodBase :?> MethodInfo
-            let checkOverrides t =
-                 Reflection.canOverrideMethod t ancestorMethod
             let getMock = getMock typeStorage.TypeMocks
             let result = refineStorage getMock typeStorage Array.empty Array.empty
             match result with
             | TypeSat ->
                 let candidates = typeStorage[thisAddress].Value
-                let optionMock m = Some m
-                let filtered = candidates.Filter(checkOverrides, optionMock)
-                let truncated = filtered.Take(5)
-                typeStorage[thisAddress] <- truncated.Eval()
-                truncated.Types
+                let typeFilter t = ancestorMethod.CanBeOverriddenInType t
+                let resolveOverride t =
+                    let overridden = ancestorMethod.ResolveOverrideInType t
+                    overridden.DeclaringType
+                let filtered = candidates.Filter(typeFilter, Some).DistinctBy(resolveOverride).Take(5).Eval()
+                typeStorage[thisAddress] <- filtered
+                filtered.Types
             | TypeUnsat -> Seq.empty
-        | Ref address when Reflection.typeImplementsMethod thisType (ancestorMethod.MethodBase :?> MethodInfo) ->
+        | Ref address when ancestorMethod.IsImplementedInType thisType ->
             assert(thisType = address.TypeOfLocation)
             ConcreteType thisType |> Seq.singleton
         | _ -> internalfail $"Getting callvirt candidates: unexpected this {thisRef}"

VSharp.SILI/Interpreter.fs

@@ -856,36 +856,16 @@ type ILInterpreter() as this =
         ILInterpreter.CheckDisallowNullAttribute method (Some args) cilState true (fun states ->
         Cps.List.mapk inlineOrCall states (List.concat >> k))
 
-    member x.ResolveVirtualMethod targetType (ancestorMethod : Method) =
-        let genericCalledMethod = ancestorMethod.GetGenericMethodDefinition()
-        let genericMethodInfo =
-            Reflection.resolveOverridingMethod targetType genericCalledMethod
-        if genericMethodInfo.IsGenericMethodDefinition then
-            genericMethodInfo.MakeGenericMethod(ancestorMethod.GetGenericArguments())
-        else genericMethodInfo
-        |> Application.getMethod
-
-    member x.CallAbstract targetType (ancestorMethod : Method) (this : term) (arguments : term list) cilState k =
+    member x.CallAbstract targetType (ancestorMethod : MethodWithBody) (this : term) (arguments : term list) cilState k =
         let thisType = MostConcreteTypeOfRef cilState.state this
         let candidateTypes = ResolveCallVirt cilState.state this thisType ancestorMethod |> List.ofSeq
-        let getMethods t (concreteMethods, mockTypes) =
-            match t with
-            | ConcreteType t ->
-                let overriden = x.ResolveVirtualMethod t ancestorMethod
-                if overriden.InCoverageZone || t.IsAssignableTo targetType && targetType.Assembly = t.Assembly then
-                    (t, overriden) :: concreteMethods, mockTypes
-                else concreteMethods, mockTypes
-            | MockType m -> concreteMethods, (m :: mockTypes)
-        let candidateMethods, typeMocks = List.foldBack getMethods candidateTypes (List.empty, List.empty)
-        assert(List.length typeMocks <= 1)
-        let candidateMethods = List.distinctBy snd candidateMethods
         let invokeMock cilState k =
-            if Seq.isEmpty typeMocks then
-                __insufficientInformation__ $"Trying to 'CallVirt' method {ancestorMethod} without mocks"
-            let overriden =
-                if ancestorMethod.DeclaringType.IsInterface then ancestorMethod
-                else x.ResolveVirtualMethod targetType ancestorMethod
-            let returnValue = MethodMockAndCall cilState.state overriden (Some this) []
+            let mockMethod =
+                if ancestorMethod.DeclaringType.IsInterface then
+                    ancestorMethod
+                else
+                    ancestorMethod.ResolveOverrideInType targetType
+            let returnValue = MethodMockAndCall cilState.state mockMethod (Some this) []
             match returnValue with
             | Some symVal ->
                 push symVal cilState
@@ -895,18 +875,29 @@ type ILInterpreter() as this =
                 // Moving ip to next instruction after mocking method result
                 fallThrough loc.method loc.offset cilState (fun _ _ _ -> ()) |> k
             | _ -> __unreachable__()
-        let rec dispatch candidates cilState k =
+        let rec dispatch (candidates : symbolicType list) cilState k =
             match candidates with
-            | [] -> invokeMock cilState k
-            | (t, method : Method)::rest ->
-                StatedConditionalExecutionCIL cilState
-                    (fun cilState k -> k (API.Types.TypeIsRef cilState t this, cilState))
-                    (fun cilState k ->
-                        let this = Types.Cast this method.ReflectedType
-                        x.CommonCall method arguments (Some this) cilState k)
-                    (dispatch rest)
-                    k
-        dispatch candidateMethods cilState k
+            | [MockType _] ->
+                KeepOnlyMock cilState.state this
+                invokeMock cilState k
+            | ConcreteType candidateType :: rest ->
+                let overridden =
+                    ancestorMethod.ResolveOverrideInType candidateType :?> Method
+                if overridden.InCoverageZone || candidateType.IsAssignableTo targetType && targetType.Assembly = candidateType.Assembly then
+                    StatedConditionalExecutionCIL cilState
+                        (fun cilState k -> k (API.Types.TypeIsRef cilState candidateType this, cilState))
+                        (fun cilState k ->
+                            let this = Types.Cast this overridden.ReflectedType
+                            x.CommonCall overridden arguments (Some this) cilState k)
+                        (dispatch rest)
+                        k
+                else
+                    dispatch rest cilState k
+            | MockType _ :: _ ->
+                __unreachable__()
+            | [] ->
+                __insufficientInformation__ $"Trying to 'CallVirt' method {ancestorMethod} without mocks"
+        dispatch candidateTypes cilState k
 
     member private x.ConvOvf targetType (cilState : cilState) =
         let supersetsOf =
@@ -1066,12 +1057,12 @@ type ILInterpreter() as this =
             if baseType.IsAbstract || canBeOverriden() || ancestorMethod.IsDelegate then
                 x.CallAbstract baseType ancestorMethod this args cilState k
             else
-                let targetMethod = x.ResolveVirtualMethod baseType ancestorMethod
+                let targetMethod = ancestorMethod.ResolveOverrideInType baseType
                 if targetMethod.IsAbstract then
-                    x.CallAbstract baseType targetMethod this args cilState k
+                    x.CallAbstract baseType (targetMethod :?> Method) this args cilState k
                 else
                     let this = Types.Cast this targetMethod.ReflectedType
-                    x.CommonCall targetMethod args (Some this) cilState k
+                    x.CommonCall (targetMethod :?> Method) args (Some this) cilState k
 
         // NOTE: there is no need to initialize statics, because they were initialized before ``newobj'' execution
         let call (cilState : cilState) k =