[fix] Filter overrides by coverage zone in Interpreter

VSharp.IL/CFG.fs

@@ -1,7 +1,6 @@
 namespace VSharp
 
 open System.Collections.Concurrent
-open VSharp.Core
 open VSharp.GraphUtils
 open global.System
 open System.Reflection
@@ -344,10 +343,7 @@ and Method internal (m : MethodBase) as this =
     static member internal ReportCFGLoaded with get() = Method.cfgReporter and set v = Method.cfgReporter <- v
     static member val internal CoverageZone : Method -> bool = fun _ -> true with get, set
 
-    member x.IsInCoverageZone with get() = Method.CoverageZone x
-
-    interface IMethod with
-        member x.IsInCoverageZone with get() = x.IsInCoverageZone
+    member x.InCoverageZone with get() = Method.CoverageZone x
 
     interface ICallGraphNode with
         member this.OutgoingEdges with get () =

VSharp.IL/MethodBody.fs

@@ -229,7 +229,6 @@ type MethodWithBody internal (m : MethodBase) =
         override x.IsExternalMethod with get() = x.IsExternalMethod
         override x.ContainsGenericParameters with get() = x.ContainsGenericParameters
         override x.GenericArguments with get() = genericArguments.Value
-        override x.IsInCoverageZone = false
         override x.SubstituteTypeVariables subst =
             Reflection.concretizeMethodBase m subst |> MethodWithBody.InstantiateNew :> VSharp.Core.IMethod
         override x.CompareTo(y : obj) =
@@ -299,15 +298,11 @@ type MethodWithBody internal (m : MethodBase) =
         opCode, calledMethod
 
     member x.ResolveOverrideInType t =
-        let genericCalledMethod = x.GetGenericMethodDefinition()
-        let genericMethodInfo =
-            Reflection.resolveOverridingMethod t genericCalledMethod
-        let genericMethodWithArgs =
-            if genericMethodInfo.IsGenericMethodDefinition then
-                genericMethodInfo.MakeGenericMethod(x.GetGenericArguments())
-            else
-                genericMethodInfo
-        MethodWithBody.InstantiateNew genericMethodWithArgs
+        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

VSharp.SILI.Core/API.fs

@@ -56,7 +56,9 @@ module API =
         | Ref _ -> ()
         | _ -> internalfail $"unexpected this {ref}"
 
-    let ResolveCallVirt state thisAddress thisType targetType ancestorMethod = TypeSolver.getCallVirtCandidates state thisAddress thisType targetType ancestorMethod
+    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

@@ -32,7 +32,8 @@ module API =
 
     val SolveGenericMethodParameters : typeStorage -> IMethod -> (symbolicType[] * symbolicType[]) option
     val SolveThisType : state -> term -> unit
-    val ResolveCallVirt : state -> term -> Type -> Type -> IMethod -> (symbolicType * IMethod) seq
+    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

@@ -404,29 +404,15 @@ 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.TakeWithDistinctOverrides(
-        resolveOverride : Type -> 'm option,
-        resolveMockOverride : unit -> 'm,
-        count : int
-    ) =
-        let withOverride t = Option.map (fun o -> t, o) (resolveOverride t)
-        let orderedTypesWithOverrides = Seq.choose withOverride orderedTypes |> Seq.distinctBy snd
-        let truncated =
-            match mock with
-            | Some _ -> Seq.truncate (count - 1) orderedTypesWithOverrides
-            | None -> Seq.truncate count orderedTypesWithOverrides
-        let overrides = seq {
-            yield! Seq.map snd truncated
-            if x.HasMock then
-                yield resolveMockOverride()
-        }
-        candidates(Seq.map fst truncated, mock, userAssembly), overrides
+    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 =

VSharp.SILI.Core/Terms.fs

@@ -21,7 +21,6 @@ type IMethod =
     abstract IsExternalMethod : bool
     abstract ContainsGenericParameters : bool
     abstract GenericArguments : Type[]
-    abstract IsInCoverageZone : bool
     abstract SubstituteTypeVariables : (Type -> Type) -> IMethod
     abstract ResolveOverrideInType : Type -> IMethod
     abstract CanBeOverriddenInType : Type -> bool

VSharp.SILI.Core/TypeSolver.fs

@@ -484,31 +484,22 @@ module TypeSolver =
         | TypeSat _ -> ()
         | TypeUnsat -> internalfail "Refining types: branch is unreachable"
 
-    let getCallVirtCandidates state (thisRef : heapAddress) (thisType : Type) (targetType : 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
-        let resolveOverride t =
-            if not <| ancestorMethod.CanBeOverriddenInType t then
-                None
-            else
-                let overridden = ancestorMethod.ResolveOverrideInType t
-                if overridden.IsInCoverageZone || t.IsAssignableTo targetType && targetType.Assembly = t.Assembly then
-                    Some overridden
-                else
-                    None
-        let resolveMockOverride() =
-            if ancestorMethod.DeclaringType.IsInterface then
-                ancestorMethod
-            else
-                ancestorMethod.ResolveOverrideInType targetType
         match thisRef.term with
         | HeapRef({term = ConcreteHeapAddress thisAddress}, _) when VectorTime.less state.startingTime thisAddress ->
-            let actualThisType = state.allocatedTypes[thisAddress]
-            match actualThisType with
-            | MockType t -> (actualThisType, resolveMockOverride()) |> Seq.singleton
-            | ConcreteType t ->
-                match resolveOverride t with
-                | Some overridden -> (actualThisType, overridden) |> Seq.singleton
-                | None -> internalfailf "Getting callvirt candidates: method override should be resolved, but is wasn't"
+            state.allocatedTypes[thisAddress] |> Seq.singleton
         | HeapRef(thisAddress, _) ->
             let thisConstraints = List.singleton thisType |> typeConstraints.FromSuperTypes
             let typeStorage = state.typeStorage
@@ -518,13 +509,15 @@ module TypeSolver =
             match result with
             | TypeSat ->
                 let candidates = typeStorage[thisAddress].Value
-                let filtered, overrides = candidates.TakeWithDistinctOverrides(resolveOverride, resolveMockOverride, 5)
-                typeStorage[thisAddress] <- filtered.Eval()
-                Seq.zip filtered.Types overrides
+                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 ancestorMethod.IsImplementedInType thisType ->
             assert(thisType = address.TypeOfLocation)
-            match resolveOverride thisType with
-            | Some overridden -> (ConcreteType thisType, overridden) |> Seq.singleton
-            | None -> internalfailf "Getting callvirt candidates: method override should be resolved, but is wasn't"
+            ConcreteType thisType |> Seq.singleton
         | _ -> internalfail $"Getting callvirt candidates: unexpected this {thisRef}"

VSharp.SILI/Interpreter.fs

@@ -856,10 +856,15 @@ type ILInterpreter() as this =
         ILInterpreter.CheckDisallowNullAttribute method (Some args) cilState true (fun states ->
         Cps.List.mapk inlineOrCall states (List.concat >> k))
 
-    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 candidates = ResolveCallVirt cilState.state this thisType targetType ancestorMethod |> List.ofSeq
-        let invokeMock mockMethod cilState k =
+        let candidateTypes = ResolveCallVirt cilState.state this thisType ancestorMethod |> List.ofSeq
+        let invokeMock cilState k =
+            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 ->
@@ -870,26 +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 mutable wasMockInvoked = false
-        let rec dispatch (candidates : (symbolicType * IMethod) list) cilState k =
+        let rec dispatch (candidates : symbolicType list) cilState k =
             match candidates with
-            | (MockType mockType, mockOverride) :: rest ->
-                wasMockInvoked <- true
-                invokeMock mockOverride cilState k
-            | (ConcreteType candidateType, candidateOverride) :: rest ->
-                assert(candidateOverride :? Method)
-                let candidateOverride = candidateOverride :?> Method
-                StatedConditionalExecutionCIL cilState
-                    (fun cilState k -> k (API.Types.TypeIsRef cilState candidateType this, cilState))
-                    (fun cilState k ->
-                        let this = Types.Cast this candidateOverride.ReflectedType
-                        x.CommonCall candidateOverride arguments (Some this) cilState k)
-                    (dispatch rest)
-                    k
-            | [] when not wasMockInvoked ->
+            | [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"
-            | [] -> __unreachable__()
-        dispatch candidates cilState k
+        dispatch candidateTypes cilState k
 
     member private x.ConvOvf targetType (cilState : cilState) =
         let supersetsOf =

VSharp.SVM/DistanceWeighter.fs

@@ -117,7 +117,7 @@ type IntraproceduralShortestDistanceToUncoveredWeighter(statistics : SVMStatisti
         override x.Weight(state) =
             let calculateWeight ip =
                 match ip2codeLocation ip, ip with
-                | Some loc, _ when loc.method.IsInCoverageZone -> minDistance loc.method loc.offset |> Some
+                | Some loc, _ when loc.method.InCoverageZone -> minDistance loc.method loc.offset |> Some
                 | Some _, _-> None
                 | None, SearchingForHandler(toObserve, _) ->
                     List.length toObserve |> uint |> Some

VSharp.SVM/GuidedSearcher.fs

@@ -63,7 +63,7 @@ type RecursionBasedTargetManager(statistics : SVMStatistics, threshold : uint) =
 
         override x.CalculateTarget state =
             let locStack = state.ipStack |> Seq.choose ipOperations.ip2codeLocation
-            let inCoverageZone loc = loc.method.IsInCoverageZone
+            let inCoverageZone loc = loc.method.InCoverageZone
             Cps.Seq.foldlk (fun reachingLoc loc k ->
             match reachingLoc with
             | None when inCoverageZone loc ->

VSharp.SVM/SVM.fs

@@ -110,7 +110,7 @@ type public SVM(options : SVMOptions) =
     let reportState reporter (suite : testSuite) cilState =
         try
             let isNewHistory() =
-                let methodHistory = Set.filter (fun h -> h.method.IsInCoverageZone) cilState.history
+                let methodHistory = Set.filter (fun h -> h.method.InCoverageZone) cilState.history
                 Set.exists (not << statistics.IsBasicBlockCoveredByTest) methodHistory
             let isError = suite.IsErrorSuite
             let isNewTest =

VSharp.SVM/Statistics.fs

@@ -158,9 +158,9 @@ type public SVMStatistics(entryMethods : Method seq) =
 
             let currentMethod = currentLoc.method
             if totalRef.Value = 0u then
-                if currentMethod.IsInCoverageZone then coveringStepsInsideZone <- coveringStepsInsideZone + 1u
+                if currentMethod.InCoverageZone then coveringStepsInsideZone <- coveringStepsInsideZone + 1u
                 else coveringStepsOutsideZone <- coveringStepsOutsideZone + 1u
-            elif currentMethod.IsInCoverageZone then nonCoveringStepsInsideZone <- nonCoveringStepsInsideZone + 1u
+            elif currentMethod.InCoverageZone then nonCoveringStepsInsideZone <- nonCoveringStepsInsideZone + 1u
             else nonCoveringStepsOutsideZone <- nonCoveringStepsOutsideZone + 1u
 
             totalVisited[currentLoc] <- totalRef.Value + 1u
@@ -173,7 +173,7 @@ type public SVMStatistics(entryMethods : Method seq) =
                 if hasSiblings visitedState then historyRef.Value.Add visitedState |> ignore
 
             let isCovered = x.IsBasicBlockCoveredByTest currentLoc
-            if currentMethod.IsInCoverageZone && not isCovered then
+            if currentMethod.InCoverageZone && not isCovered then
                 visitedBlocksNotCoveredByTests.TryAdd(s, Set.empty) |> ignore
                 Interlocked.Exchange(ref isVisitedBlocksNotCoveredByTestsRelevant, 0) |> ignore
             setCoveredIfNeed currentLoc
@@ -206,7 +206,7 @@ type public SVMStatistics(entryMethods : Method seq) =
                 let coveredBlocks = ConcurrentDictionary()
                 coveredBlocks.TryAdd(block.offset, ()) |> ignore
                 blocksCoveredByTests[block.method] <- coveredBlocks
-            if block.method.IsInCoverageZone then
+            if block.method.InCoverageZone then
                 Interlocked.Exchange(ref isVisitedBlocksNotCoveredByTestsRelevant, 0) |> ignore
 
     member x.IsBasicBlockCoveredByTest (blockStart : codeLocation) =
@@ -223,7 +223,7 @@ type public SVMStatistics(entryMethods : Method seq) =
                 let cfg = m.CFG
                 coveredBlocksOffsets.Value |> Seq.sumBy (fun o -> (cfg.ResolveBasicBlock o.Key).BlockSize)
             else 0
-        let methodsInZone = methods |> List.filter (fun m -> m.IsInCoverageZone)
+        let methodsInZone = methods |> List.filter (fun m -> m.InCoverageZone)
         let totalInstructionsCount = methodsInZone |> List.sumBy (fun m -> m.CFG.MethodSize)
         let coveredInstructionsCount = methodsInZone |> List.sumBy getCoveredInstructionsCount
         if totalInstructionsCount <> 0 then
@@ -325,8 +325,8 @@ type public SVMStatistics(entryMethods : Method seq) =
             |> Seq.groupBy (fun kvp -> kvp.Key.method)
             |> Seq.map (snd >> Seq.maxBy (fun kvp -> kvp.Value))
             |> Seq.sortByDescending (fun kvp -> kvp.Value)
-        let topVisitedByMethodsInZone = topVisitedByMethods |> Seq.filter (fun kvp -> kvp.Key.method.IsInCoverageZone) |> Seq.truncate topN
-        let topVisitedByMethodsOutOfZone = topVisitedByMethods |> Seq.filter (fun kvp -> not kvp.Key.method.IsInCoverageZone) |> Seq.truncate topN
+        let topVisitedByMethodsInZone = topVisitedByMethods |> Seq.filter (fun kvp -> kvp.Key.method.InCoverageZone) |> Seq.truncate topN
+        let topVisitedByMethodsOutOfZone = topVisitedByMethods |> Seq.filter (fun kvp -> not kvp.Key.method.InCoverageZone) |> Seq.truncate topN
         {
             time = stopwatch.Elapsed
             solverTime = solverStopwatch.Elapsed