Constraint independence

VSharp.SILI.Core/API.fs

@@ -1,5 +1,6 @@
 namespace VSharp.Core
 
+open System.Reflection
 open FSharpx.Collections
 open VSharp
 
@@ -237,7 +238,7 @@ module API =
         let EmptyStack = EvaluationStack.empty
 
     module public Memory =
-        let EmptyState() = Memory.makeEmpty()
+        let EmptyState modelState = State.makeEmpty modelState
         let PopFrame state = Memory.popFrame state
         let ForcePopFrames count state = Memory.forcePopFrames count state
         let PopTypeVariables state = Memory.popTypeVariablesSubstitution state
@@ -339,6 +340,7 @@ module API =
 
         let MakeSymbolicThis m = Memory.makeSymbolicThis m
         let MakeSymbolicValue source name typ = Memory.makeSymbolicValue source name typ
+        let FillWithParametersAndThis state method = Memory.fillWithParametersAndThis state method
 
         let CallStackContainsFunction state method = CallStack.containsFunc state.stack method
         let CallStackSize state = CallStack.size state.stack
@@ -352,6 +354,8 @@ module API =
 
         let InitializeStaticMembers state targetType =
             Memory.initializeStaticMembers state targetType
+
+        let Allocate state key term = Memory.allocateOnStack state key term
 
         let AllocateTemporaryLocalVariable state typ term =
             let tmpKey = TemporaryLocalVariableKey typ
@@ -489,7 +493,8 @@ module API =
                 state.lowerBounds <- PersistentDict.update state.lowerBounds typ (MemoryRegion.empty Types.lengthType) (MemoryRegion.fillRegion value)
             | StackBufferSort key ->
                 state.stackBuffers <- PersistentDict.update state.stackBuffers key (MemoryRegion.empty Types.Int8) (MemoryRegion.fillRegion value)
-
+
+        let IsStackEmpty state = CallStack.isEmpty state.stack
 
     module Print =
         let Dump state = Memory.dump state

VSharp.SILI.Core/API.fsi

@@ -196,7 +196,7 @@ module API =
         val EmptyStack : evaluationStack
 
     module public Memory =
-        val EmptyState : unit -> state
+        val EmptyState : state option -> state
         val PopFrame : state -> unit
         val ForcePopFrames : int -> state -> unit
         val PopTypeVariables : state -> unit
@@ -231,6 +231,7 @@ module API =
 
         val MakeSymbolicThis : MethodBase -> term
         val MakeSymbolicValue : IMemoryAccessConstantSource -> string -> symbolicType -> term
+        val FillWithParametersAndThis : state -> MethodBase -> unit
 
         val CallStackContainsFunction : state -> MethodBase -> bool
         val CallStackSize : state -> int
@@ -240,6 +241,7 @@ module API =
 
         val InitializeStaticMembers : state -> symbolicType -> unit
 
+        val Allocate : state -> stackKey -> term -> unit
         val AllocateTemporaryLocalVariable : state -> System.Type -> term -> term
         val AllocateDefaultClass : state -> symbolicType -> term
         val AllocateDefaultArray : state -> term list -> symbolicType -> term
@@ -279,6 +281,8 @@ module API =
 
 
         val FillRegion : state -> term -> regionSort -> unit
+
+        val IsStackEmpty : state -> bool
 
     module Print =
         val Dump : state -> string

VSharp.SILI.Core/Copying.fs

@@ -13,6 +13,11 @@ module internal Copying =
         interface INonComposableSymbolicConstantSource with
             override x.SubTerms = seq[] :> term seq
             override x.Time = VectorTime.zero
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? symbolicArrayIndexSource as otherIndex ->
+                    x.lowerBound <> otherIndex.lowerBound || x.upperBound <> otherIndex.upperBound
+                | _ -> true
 
     let private makeArrayIndexConstant state lowerBound upperBound =
         let source = {lowerBound = lowerBound; upperBound = upperBound}

VSharp.SILI.Core/Database.fs

@@ -186,7 +186,7 @@ type path =
         sprintf "{path [lvl %s]: %O}" (Level.toString x.lvl) x.state.pc
 
 type query =
-    { lvl : level; queryFml : formula } with
+    { lvl : level; queryFml : formula; currentModel : model } with
     override x.ToString() =
         sprintf "{query [lvl %s]: %O}" (Level.toString x.lvl) x.queryFml
 

VSharp.SILI.Core/Memory.fs

@@ -18,30 +18,7 @@ type IMemoryAccessConstantSource =
 module internal Memory =
 
 // ------------------------------- Primitives -------------------------------
-
-    let makeEmpty() = {
-        pc = PC.empty
-        evaluationStack = EvaluationStack.empty
-        exceptionsRegister = NoException
-        stack = CallStack.empty
-        stackBuffers = PersistentDict.empty
-        classFields = PersistentDict.empty
-        arrays = PersistentDict.empty
-        lengths = PersistentDict.empty
-        lowerBounds = PersistentDict.empty
-        staticFields = PersistentDict.empty
-        boxedLocations = PersistentDict.empty
-        initializedTypes = SymbolicSet.empty
-        concreteMemory = Dictionary<_,_>()
-        physToVirt = PersistentDict.empty
-        allocatedTypes = PersistentDict.empty
-        typeVariables = (MappedStack.empty, Stack.empty)
-        delegates = PersistentDict.empty
-        currentTime = [1]
-        startingTime = VectorTime.zero
-        model = None
-    }
-
+
     type memoryMode =
         | ConcreteMemory
         | SymbolicMemory
@@ -53,7 +30,7 @@ module internal Memory =
             match memoryMode with
             | ConcreteMemory -> ConcreteMemory.deepCopy state
             | SymbolicMemory -> state
-        { state with pc = newPc }
+        { state with pc = newPc; id = Guid.NewGuid().ToString() }
 
     let private isZeroAddress (x : concreteHeapAddress) =
         x = VectorTime.zero
@@ -176,7 +153,15 @@ module internal Memory =
         {object : term}
         interface IStatedSymbolicConstantSource with
             override x.SubTerms = Seq.empty
-            override x.Time = VectorTime.zero
+            override x.Time = VectorTime.zero            
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? hashCodeSource as otherHashCodeSource ->
+                    match otherHashCodeSource.object, x.object with
+                    | ConstantT(_, otherConstantSource, _), ConstantT(_, constantSource, _) ->
+                        otherConstantSource.IndependentWith constantSource
+                    | _ -> true
+                | _ -> true 
 
     let hashConcreteAddress (address : concreteHeapAddress) =
         address.GetHashCode() |> makeNumber
@@ -213,14 +198,29 @@ module internal Memory =
                 | Some time -> time
                 | None -> internalfailf "Requesting time of primitive stack location %O" x.key
             override x.TypeOfLocation = x.key.TypeOfLocation
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? stackReading as otherReading -> x <> otherReading
+                | _ -> true
 
     [<StructuralEquality;NoComparison>]
     type private heapReading<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> =
         {picker : regionPicker<'key, 'reg>; key : 'key; memoryObject : memoryRegion<'key, 'reg>; time : vectorTime}
         interface IMemoryAccessConstantSource with
-            override x.SubTerms = Seq.empty
+            override x.SubTerms =
+                let addKeySubTerms _ (regionKey : updateTreeKey<'key, term>) acc =
+                    Seq.fold PersistentSet.add acc regionKey.key.SubTerms
+                RegionTree.foldr addKeySubTerms PersistentSet.empty x.memoryObject.updates
+                |> PersistentSet.toSeq
+                |> Seq.append x.key.SubTerms
             override x.Time = x.time
             override x.TypeOfLocation = x.picker.sort.TypeOfLocation
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? heapReading<'key, 'reg> as otherReading ->
+                    let rootRegions hr = match hr.memoryObject.updates with | Node dict -> PersistentDict.keys dict
+                    Seq.allPairs (rootRegions x) (rootRegions otherReading) |> Seq.forall (fun (reg1, reg2) -> reg1.CompareTo reg2 = Disjoint)
+                | _ -> true
 
     let (|HeapReading|_|) (src : IMemoryAccessConstantSource) =
         match src with
@@ -270,6 +270,11 @@ module internal Memory =
             override x.SubTerms = x.baseSource.SubTerms
             override x.Time = x.baseSource.Time
             override x.TypeOfLocation = fromDotNetType x.field.typ
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? structField as otherField ->
+                    x.field <> otherField.field || x.baseSource.IndependentWith otherField.baseSource
+                | _ -> true
 
     let (|StructFieldSource|_|) (src : IMemoryAccessConstantSource) =
         match src with
@@ -283,6 +288,10 @@ module internal Memory =
             override x.SubTerms = x.baseSource.SubTerms
             override x.Time = x.baseSource.Time
             override x.TypeOfLocation = x.baseSource.TypeOfLocation
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? heapAddressSource as otherAddress -> x.baseSource.IndependentWith otherAddress.baseSource
+                | _ -> true
 
     let (|HeapAddressSource|_|) (src : IMemoryAccessConstantSource) =
         match src with
@@ -295,6 +304,13 @@ module internal Memory =
         interface IStatedSymbolicConstantSource  with
             override x.SubTerms = Seq.empty
             override x.Time = VectorTime.zero
+            override x.IndependentWith otherSource =
+                match otherSource with
+                | :? typeInitialized as otherType ->
+                    let xDotNetType = toDotNetType x.typ
+                    let otherDotNetType = toDotNetType otherType.typ
+                    structuralInfimum xDotNetType otherDotNetType = None
+                | _ -> true
 
     let (|TypeInitializedSource|_|) (src : IStatedSymbolicConstantSource) =
         match src with
@@ -333,6 +349,20 @@ module internal Memory =
         let declaringType = fromDotNetType m.DeclaringType
         if isValueType declaringType then __insufficientInformation__ "Can't execute in isolation methods of value types, because we can't be sure where exactly \"this\" is allocated!"
         else HeapRef (Constant "this" {baseSource = {key = ThisKey m; time = Some VectorTime.zero}} AddressType) declaringType
+
+    let fillWithParametersAndThis state (method : System.Reflection.MethodBase) =
+        let parameters = method.GetParameters() |> Seq.map (fun param ->
+            (ParameterKey param, None, fromDotNetType param.ParameterType)) |> List.ofSeq
+        let parametersAndThis =
+            if Reflection.hasThis method then
+                let t = fromDotNetType method.DeclaringType
+                let addr = [-1]
+                let thisRef = HeapRef (ConcreteHeapAddress addr) t
+                state.allocatedTypes <- PersistentDict.add addr t state.allocatedTypes
+                state.startingTime <- [-2]
+                (ThisKey method, Some thisRef, t) :: parameters // TODO: incorrect type when ``this'' is Ref to stack
+            else parameters
+        newStackFrame state method parametersAndThis
 
 // =============== Marshalling/unmarshalling without state changing ===============
 
@@ -646,48 +676,69 @@ module internal Memory =
         commonGuardedStatedApplyk (fun state term k -> mapper state term |> k) state term id id
 
     let commonStatedConditionalExecutionk (state : state) conditionInvocation thenBranch elseBranch merge2Results k =
+        // Returns PC containing only constraints dependent with cond
+        let keepDependentWith pc cond =
+            PC.fragments pc
+            |> Seq.tryFind (PC.toSeq >> Seq.contains cond)
+            |> Option.defaultValue pc
         let execution thenState elseState condition k =
             assert (condition <> True && condition <> False)
             thenBranch thenState (fun thenResult ->
             elseBranch elseState (fun elseResult ->
             merge2Results thenResult elseResult |> k))
-        conditionInvocation state (fun (condition, conditionState) ->
+        conditionInvocation state (fun (condition, conditionState) ->        
+        let negatedCondition = !!condition
         let thenPc = PC.add state.pc condition
-        let elsePc = PC.add state.pc (!!condition)
-        if PC.isFalse thenPc then
+        let elsePc = PC.add state.pc negatedCondition
+        let independentThenPc = keepDependentWith thenPc condition
+        // In fact, this call is redundant because independentElsePc == independentThenPc with negated cond
+        let independentElsePc = keepDependentWith elsePc negatedCondition 
+        if PC.isFalse independentThenPc then
             conditionState.pc <- elsePc
             elseBranch conditionState (List.singleton >> k)
-        elif PC.isFalse elsePc then
+        elif PC.isFalse independentElsePc then
             conditionState.pc <- thenPc
             thenBranch conditionState (List.singleton >> k)
         else
-            conditionState.pc <- thenPc
+            conditionState.pc <- independentThenPc
             match SolverInteraction.checkSat conditionState with
             | SolverInteraction.SmtUnknown _ ->
-                conditionState.pc <- elsePc
+                conditionState.pc <- independentElsePc
                 match SolverInteraction.checkSat conditionState with
                 | SolverInteraction.SmtUnsat _
                 | SolverInteraction.SmtUnknown _ ->
                     __insufficientInformation__ "Unable to witness branch"
                 | SolverInteraction.SmtSat model ->
+                    conditionState.pc <- elsePc
                     conditionState.model <- Some model.mdl
+                    StatedLogger.log conditionState.id $"Model stack: %s{model.mdl.state.stack.frames.ToString()}"
+                    StatedLogger.log conditionState.id $"Branching on: %s{(independentElsePc |> PC.toSeq |> conjunction).ToString()}"
                     elseBranch conditionState (List.singleton >> k)
             | SolverInteraction.SmtUnsat _ ->
                 conditionState.pc <- elsePc
+                StatedLogger.log conditionState.id $"Branching on: %s{(independentElsePc |> PC.toSeq |> conjunction).ToString()}"
                 elseBranch conditionState (List.singleton >> k)
-            | SolverInteraction.SmtSat model ->
-                conditionState.pc <- elsePc
-                conditionState.model <- Some model.mdl
+            | SolverInteraction.SmtSat thenModel ->
+                conditionState.pc <- independentElsePc
                 match SolverInteraction.checkSat conditionState with
                 | SolverInteraction.SmtUnsat _
                 | SolverInteraction.SmtUnknown _ ->
                     conditionState.pc <- thenPc
+                    conditionState.model <- Some thenModel.mdl
+                    StatedLogger.log conditionState.id $"Model stack: %s{thenModel.mdl.state.stack.frames.ToString()}"
+                    StatedLogger.log conditionState.id $"Branching on: %s{(independentThenPc |> PC.toSeq |> conjunction).ToString()}"
                     thenBranch conditionState (List.singleton >> k)
-                | SolverInteraction.SmtSat model ->
+                | SolverInteraction.SmtSat elseModel ->
+                    conditionState.pc <- thenPc
                     let thenState = conditionState
                     let elseState = copy conditionState elsePc
-                    elseState.model <- Some model.mdl
-                    thenState.pc <- thenPc
+                    StatedLogger.copy thenState.id elseState.id
+                    StatedLogger.log thenState.id $"Model stack: %s{thenModel.mdl.state.stack.frames.ToString()}"
+                    StatedLogger.log elseState.id $"Model stack: %s{elseModel.mdl.state.stack.frames.ToString()}"
+                    StatedLogger.log thenState.id $"Branching on: %s{(independentThenPc |> PC.toSeq |> conjunction).ToString()}"
+                    StatedLogger.log elseState.id $"Branching on: %s{(independentElsePc |> PC.toSeq |> conjunction).ToString()}"
+                    elseState.model <- Some elseModel.mdl
+                    thenState.model <- Some thenModel.mdl
                     execution thenState elseState condition k)
 
     let statedConditionalExecutionWithMergek state conditionInvocation thenBranch elseBranch k =
@@ -1482,6 +1533,7 @@ module internal Memory =
             let g = g1 &&& g2 &&& g3 &&& g4 &&& g5 &&& g6
             if not <| isFalse g then
                 return {
+                    id = Guid.NewGuid().ToString()
                     pc = if isTrue g then pc else PC.add pc g
                     evaluationStack = evaluationStack
                     exceptionsRegister = exceptionRegister

VSharp.SILI.Core/MemoryRegion.fs

@@ -11,6 +11,7 @@ type IMemoryKey<'a, 'reg when 'reg :> IRegion<'reg>> =
     abstract Map : (term -> term) -> (symbolicType -> symbolicType) -> (vectorTime -> vectorTime) -> 'reg -> 'reg * 'a
     abstract IsUnion : bool
     abstract Unguard : (term * 'a) list
+    abstract SubTerms : seq<term>
 
 type regionSort =
     | HeapFieldSort of fieldId
@@ -63,6 +64,8 @@ type heapAddressKey =
             newReg, {address = mapTerm x.address}
         override x.IsUnion = isUnion x.address
         override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr}))
+        override x.SubTerms = Seq.singleton x.address
+
     interface IComparable with
         override x.CompareTo y =
             match y with
@@ -84,6 +87,8 @@ type heapArrayIndexKey =
             reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; indices = List.map mapTerm x.indices}
         override x.IsUnion = isUnion x.address
         override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr; indices = x.indices}))  // TODO: if x.indices is the union of concrete values, then unguard indices as well
+        override x.SubTerms = x.address :: x.indices |> List.toSeq
+
     interface IComparable with
         override x.CompareTo y =
             match y with
@@ -108,6 +113,7 @@ type heapVectorIndexKey =
             reg.Map (fun x -> x.Map mapTime) id, {address = mapTerm x.address; index = mapTerm x.index}
         override x.IsUnion = isUnion x.address
         override x.Unguard = Merging.unguard x.address |> List.map (fun (g, addr) -> (g, {address = addr; index = x.index}))  // TODO: if x.index is the union of concrete values, then unguard index as well
+        override x.SubTerms = [x.address; x.index] |> List.toSeq
     interface IComparable with
         override x.CompareTo y =
             match y with
@@ -134,6 +140,8 @@ type stackBufferIndexKey =
             match x.index.term with
             | Union gvs when List.forall (fst >> isConcrete) gvs -> gvs |> List.map (fun (g, idx) -> (g, {index = idx}))
             | _ -> [(True, x)]
+        override x.SubTerms = Seq.singleton x.index
+
     interface IComparable with
         override x.CompareTo y =
             match y with
@@ -151,6 +159,8 @@ type symbolicTypeKey =
             reg.Map mapper, {typ = mapper x.typ}
         override x.IsUnion = false
         override x.Unguard = [(True, x)]
+        override x.SubTerms = Seq.empty
+
     override x.ToString() = x.typ.ToString()
 
 type updateTreeKey<'key, 'value when 'key : equality> =