[fix] fixed type solver

- added equality constraints

VSharp.SILI.Core/API.fs

@@ -219,6 +219,7 @@ module API =
         let (|TypeInitializedSource|_|) src = Memory.(|TypeInitializedSource|_|) src
         let (|TypeSubtypeTypeSource|_|) src = TypeCasting.(|TypeSubtypeTypeSource|_|) src
         let (|RefSubtypeTypeSource|_|) src = TypeCasting.(|RefSubtypeTypeSource|_|) src
+        let (|RefEqTypeSource|_|) src = TypeCasting.(|RefEqTypeSource|_|) src
         let (|TypeSubtypeRefSource|_|) src = TypeCasting.(|TypeSubtypeRefSource|_|) src
         let (|RefSubtypeRefSource|_|) src = TypeCasting.(|RefSubtypeRefSource|_|) src
         let (|GetHashCodeSource|_|) s = Memory.(|GetHashCodeSource|_|) s
@@ -278,7 +279,7 @@ module API =
         let TypeIsType leftType rightType = TypeCasting.typeIsType leftType rightType
         let TypeIsRef state typ ref = TypeCasting.typeIsRef state typ ref
         let RefIsType state ref typ = TypeCasting.refIsType state ref typ
-        let RefIsAssignableToType state ref typ = TypeCasting.refIsAssignableToType state ref typ
+        let RefEqType state ref typ = TypeCasting.refEqType state ref typ
         let RefIsRef state ref1 ref2 = TypeCasting.refIsRef state ref1 ref2
 
         let IsCast state term targetType = TypeCasting.canCast state term targetType

VSharp.SILI.Core/API.fsi

@@ -121,6 +121,7 @@ module API =
         val (|TypeInitializedSource|_|) : IStatedSymbolicConstantSource -> option<Type * symbolicTypeSet>
         val (|TypeSubtypeTypeSource|_|) : ISymbolicConstantSource -> option<Type * Type>
         val (|RefSubtypeTypeSource|_|) : ISymbolicConstantSource -> option<heapAddress * Type>
+        val (|RefEqTypeSource|_|) : ISymbolicConstantSource -> option<heapAddress * Type>
         val (|TypeSubtypeRefSource|_|) : ISymbolicConstantSource -> option<Type * heapAddress>
         val (|RefSubtypeRefSource|_|) : ISymbolicConstantSource -> option<heapAddress * heapAddress>
         val (|GetHashCodeSource|_|) : ISymbolicConstantSource -> option<term>
@@ -177,7 +178,7 @@ module API =
         val IsNullable : Type -> bool
         val TypeIsRef :  state -> Type -> term -> term
         val RefIsType : state -> term -> Type -> term
-        val RefIsAssignableToType : state -> term -> Type -> term
+        val RefEqType : state -> term -> Type -> term
         val RefIsRef : state -> term -> term -> term
         val IsCast : state -> term -> Type -> term
         val Cast : term -> Type -> term

VSharp.SILI.Core/TypeCasting.fs

@@ -60,28 +60,52 @@ module internal TypeCasting =
             | _ -> None
         | _ -> None
 
+    [<StructuralEquality;NoComparison>]
+    type private symbolicTypeEqualSource =
+        { address : term; targetType : Type }
+        interface IStatedSymbolicConstantSource with
+            override x.SubTerms = List.singleton x.address
+            override x.Time = VectorTime.zero
+            override x.TypeOfLocation = typeof<bool>
+
+    let (|RefEqTypeSource|_|) (src : ISymbolicConstantSource) =
+        match src with
+        | :? symbolicTypeEqualSource as s -> Some(s.address, s.targetType)
+        | _ -> None
+
     let private makeSubtypeBoolConst left right =
-        let subtypeName = sprintf "(%O <: %O)" left right
+        let subtypeName = $"({left} <: {right})"
         let source = {left = left; right = right}
         Constant subtypeName source typeof<bool>
 
-    let rec commonTypeIsType leftType rightType =
-        let boolConst left right = makeSubtypeBoolConst (ConcreteType left) (ConcreteType right)
-        isConcreteSubtype leftType rightType makeBool boolConst
+    let private makeTypeEqBoolConst ref typ =
+        let name = $"(typeof<{ref}> = {typ})"
+        let source = {address = ref; targetType = typ}
+        Constant name source typeof<bool>
 
     // left is subtype of right
-    let typeIsType = commonTypeIsType
+    let rec typeIsType leftType rightType =
+        let boolConst left right = makeSubtypeBoolConst (ConcreteType left) (ConcreteType right)
+        isConcreteSubtype leftType rightType makeBool boolConst
 
-    let commonAddressIsType leftAddress leftType targetTyp =
+    let addressIsType leftAddress leftType targetType =
         let typeCheck address =
             let boolConst address =
                 match address.term with
                 | ConcreteHeapAddress _ -> False()
-                | _ -> makeSubtypeBoolConst (SymbolicType address) (ConcreteType targetTyp)
-            commonTypeIsType leftType targetTyp ||| boolConst address
+                | _ -> makeSubtypeBoolConst (SymbolicType address) (ConcreteType targetType)
+            typeIsType leftType targetType ||| boolConst address
         Merging.guardedApply typeCheck leftAddress
 
-    let addressIsType = commonAddressIsType
+    let addressEqType address addressType targetType =
+        let typeCheck address =
+            let boolConst address =
+                match address.term with
+                | ConcreteHeapAddress _ -> False()
+                | _ -> makeTypeEqBoolConst address targetType
+            if addressType = targetType then True()
+            else boolConst address
+        Merging.guardedApply typeCheck address
 
     let typeIsAddress leftType rightAddress rightType =
         let typeCheck rightAddress =
@@ -114,23 +138,33 @@ module internal TypeCasting =
             let rightType = address.TypeOfLocation
             typeIsType typ rightType
         | Union gvs -> Merging.guardedMap (typeIsRef state typ) gvs
-        | _ -> internalfailf "Checking subtyping: expected heap reference, but got %O" ref
+        | _ -> internalfailf $"Checking subtyping: expected heap reference, but got {ref}"
 
-    let rec commonRefIsType state ref typ =
+    let rec refIsType state ref typ =
         match ref.term with
         | HeapRef(addr, sightType) ->
             let leftType = Memory.mostConcreteTypeOfHeapRef state addr sightType
-            commonAddressIsType addr leftType typ
+            addressIsType addr leftType typ
         | Ref address ->
             let leftType = address.TypeOfLocation
             typeIsType leftType typ
         | Union gvs ->
-            let commonRefIsType term = commonRefIsType state term typ
-            Merging.guardedMap commonRefIsType gvs
-        | _ -> internalfailf "Checking subtyping: expected heap reference, but got %O" ref
+            let refIsType term = refIsType state term typ
+            Merging.guardedMap refIsType gvs
+        | _ -> internalfailf $"Checking subtyping: expected heap reference, but got {ref}"
 
-    let refIsType = commonRefIsType
-    let refIsAssignableToType = commonRefIsType
+    let rec refEqType state ref typ =
+        match ref.term with
+        | HeapRef(addr, sightType) ->
+            let leftType = Memory.mostConcreteTypeOfHeapRef state addr sightType
+            addressEqType addr leftType typ
+        | Ref address ->
+            let leftType = address.TypeOfLocation
+            makeBool (leftType = typ)
+        | Union gvs ->
+            let refEqType term = refEqType state term typ
+            Merging.guardedMap refEqType gvs
+        | _ -> internalfailf $"Checking subtyping: expected heap reference, but got {ref}"
 
     let rec refIsRef state leftRef rightRef =
         match leftRef.term, rightRef.term with
@@ -148,9 +182,9 @@ module internal TypeCasting =
             addressIsType leftAddr leftType rightType
         | Union gvs, _ ->
             let refIsRef term = refIsRef state term rightRef
-            Merging.guardedMap refIsRef gvs 
+            Merging.guardedMap refIsRef gvs
         | _, Union gvs -> Merging.guardedMap (refIsRef state leftRef) gvs
-        | _ -> internalfailf "Checking subtyping: expected heap reference, but got %O" ref
+        | _ -> internalfailf $"Checking subtyping: expected heap reference, but got {ref}"
 
     type symbolicSubtypeSource with
         interface IStatedSymbolicConstantSource with
@@ -186,6 +220,14 @@ module internal TypeCasting =
                     | _ -> notMock()
                 | ConcreteType l, ConcreteType r -> typeIsType (fillType l) (fillType r)
 
+    type symbolicTypeEqualSource with
+        interface IStatedSymbolicConstantSource with
+            override x.Compose state =
+                let address = Memory.fillHoles state x.address
+                let targetType = Memory.substituteTypeVariables state x.targetType
+                let addressType = Memory.typeOfHeapLocation state address
+                addressEqType address addressType targetType
+
     let private doCast term targetType =
         match term.term, targetType with
         | Ptr(address, _, indent), Pointer typ -> Ptr address typ indent

VSharp.SILI.Core/TypeSolver.fs

@@ -38,8 +38,10 @@ module TypeStorage =
 
     // TODO: move this to SolverInteraction and parse all pc at once
     let addTypeConstraints (typesConstraints : typesConstraints) conditions =
+        let equalityConstraints = Dictionary<term, HashSet<Type>>()
         let supertypeConstraints = Dictionary<term, HashSet<Type>>()
         let subtypeConstraints = Dictionary<term, HashSet<Type>>()
+        let inequalityConstraints = Dictionary<term, HashSet<Type>>()
         let notSupertypeConstraints = Dictionary<term, HashSet<Type>>()
         let notSubtypeConstraints = Dictionary<term, HashSet<Type>>()
         let addresses = ResizeArray<term>()
@@ -60,6 +62,8 @@ module TypeStorage =
             match term.term with
             | Constant(_, TypeCasting.TypeSubtypeTypeSource _, _) ->
                 internalfail "TypeSolver is not fully implemented"
+            | Constant(_, TypeCasting.RefEqTypeSource(address, typ), _) ->
+                add equalityConstraints address typ |> next
             | Constant(_, TypeCasting.RefSubtypeTypeSource(address, typ), _) ->
                 add supertypeConstraints address typ |> next
             | Constant(_, TypeCasting.TypeSubtypeRefSource(typ, address), _) ->
@@ -70,6 +74,8 @@ module TypeStorage =
                 internalfail "TypeSolver is not fully implemented"
             | Negation({term = Constant(_, TypeCasting.RefSubtypeTypeSource(address, typ), _)}) ->
                 add notSupertypeConstraints address typ |> next
+            | Negation({term = Constant(_, TypeCasting.RefEqTypeSource(address, typ), _)}) ->
+                add inequalityConstraints address typ |> next
             | Negation({term = Constant(_, TypeCasting.TypeSubtypeRefSource(typ, address), _)}) ->
                 add notSubtypeConstraints address typ |> next
             | Negation({term = Constant(_, TypeCasting.RefSubtypeRefSource _, _)}) ->
@@ -89,8 +95,10 @@ module TypeStorage =
         for address in addresses do
             let typeConstraints =
                 typeConstraints.Create
+                    (toList equalityConstraints address)
                     (toList supertypeConstraints address)
                     (toList subtypeConstraints address)
+                    (toList inequalityConstraints address)
                     (toList notSupertypeConstraints address)
                     (toList notSubtypeConstraints address)
             typesConstraints.Add address typeConstraints
@@ -221,6 +229,15 @@ module TypeSolver =
         | GenericCandidate gc ->
             gc.AddConstraints constraints |> Option.map GenericCandidate
 
+    let private candidatesFromEquality equalityConstraints validate =
+        assert userAssembly.IsSome
+        let userAssembly = userAssembly.Value
+        assert(List.length equalityConstraints = 1)
+        let t = List.head equalityConstraints
+        assert(validate t |> Option.isSome)
+        let types = Candidate t |> List.singleton
+        candidates(types, None, userAssembly)
+
     let private typeCandidates getMock subst constraints (makeGenericCandidates : Type -> genericCandidate option) =
         assert userAssembly.IsSome
         match constraints.supertypes |> List.tryFind (fun t -> t.IsSealed) with
@@ -243,7 +260,9 @@ module TypeSolver =
                 | Some c -> chooseCandidate constraints subst c
                 | None -> None
 
+            let equal = constraints.equal
             match constraints.subtypes with
+            | _ when List.isEmpty equal |> not -> candidatesFromEquality equal validate
             | [] ->
                 let assemblies = getAssemblies()
                 enumerateNonAbstractTypes constraints.supertypes (getMock None) validate assemblies
@@ -289,23 +308,30 @@ module TypeSolver =
         genericCandidate.TryCreate typedef depth (makeParameterSubstitutions childDepth)
 
     let private refineMock getMock constraints (mock : ITypeMock) =
-        let constraintsSuperTypes = constraints.supertypes
-        let hasPrivateSuperType = List.exists (TypeUtils.isPublic >> not) constraintsSuperTypes
-        if hasPrivateSuperType then None
+        let supertypeConstraints = constraints.supertypes
+        let equalityConstraints = constraints.equal
+        let subtypeConstraints = constraints.subtypes
+        let hasPrivateSuperType = lazy (List.exists (TypeUtils.isPublic >> not) supertypeConstraints)
+        let hasEqualityConstraints = lazy (List.isEmpty equalityConstraints |> not)
+        let hasSubtypeConstraints = lazy (List.isEmpty subtypeConstraints |> not)
+        let canNotBeMocked = lazy (List.exists (canBeMocked >> not) supertypeConstraints)
+        let nonSuitable =
+            hasPrivateSuperType.Value
+            || hasEqualityConstraints.Value
+            || hasSubtypeConstraints.Value
+            || canNotBeMocked.Value
+        if nonSuitable then None
         else
             let mockSuperTypes = List.ofSeq mock.SuperTypes
             let supertypes =
-                if List.isEmpty constraintsSuperTypes then mockSuperTypes
-                else List.concat [mockSuperTypes; constraintsSuperTypes] |> List.distinct
+                if List.isEmpty supertypeConstraints then mockSuperTypes
+                else List.concat [mockSuperTypes; supertypeConstraints] |> List.distinct
             let numOfSuperTypes = List.length supertypes
             let numOfMockSuperTypes = List.length mockSuperTypes
             assert(numOfSuperTypes >= numOfMockSuperTypes)
             let changedSupertypes = numOfSuperTypes <> numOfMockSuperTypes
             let mockConstraints = {constraints with supertypes = supertypes}
-            let satisfies =
-                List.isEmpty constraints.subtypes
-                && (mockConstraints.IsContradicting() |> not)
-                && List.forall canBeMocked constraints.supertypes
+            let satisfies = mockConstraints.IsContradicting() |> not
             if satisfies && changedSupertypes then getMock (Some mock) supertypes |> Some
             elif satisfies then Some mock
             else None
@@ -387,8 +413,10 @@ module TypeSolver =
         else
             let decodeTypeSubst (subst : substitution) = CommonUtils.decodeTypeSubst subst typeParameters
             let collectVars acc constraints =
+                let acc = constraints.equal |> List.fold collectTypeVariables acc
                 let acc = constraints.supertypes |> List.fold collectTypeVariables acc
                 let acc = constraints.subtypes |> List.fold collectTypeVariables acc
+                let acc = constraints.notEqual |> List.fold collectTypeVariables acc
                 let acc = constraints.notSupertypes |> List.fold collectTypeVariables acc
                 constraints.notSubtypes |> List.fold collectTypeVariables acc
             let typeVars = Array.fold collectTypeVariables List.empty typeParameters
@@ -435,6 +463,7 @@ module TypeSolver =
     let private refineStorage getMock (typeStorage : typeStorage) typeGenericArguments methodGenericArguments =
         let mutable emptyCandidates = false
         let constraints = typeStorage.Constraints
+        assert constraints.IsValid()
         let addressesTypes = typeStorage.AddressesTypes
         let newAddresses = Dictionary<term, typeConstraints>()