Constraint independence

VSharp.SILI.Core/API.fs

@@ -66,7 +66,7 @@ module API =
             | {term = ConcreteHeapAddress _} -> ()
             | term -> internalfailf "Unexpected address %O in subtyping constraint!" term
 
-        PC.toSeq state.pc |> Seq.iter (term >> function
+        state.pc.ToSeq() |> Seq.iter (term >> function
             | Constant(_, TypeCasting.TypeSubtypeTypeSource _, _) -> __notImplemented__()
             | Constant(_, TypeCasting.RefSubtypeTypeSource(address, typ), _) -> add supertypeConstraints address typ
             | Constant(_, TypeCasting.TypeSubtypeRefSource(typ, address), _) -> add subtypeConstraints address typ
@@ -229,10 +229,12 @@ module API =
             | _ -> internalfailf "Unboxing: expected heap reference, but got %O" reference
 
         let AddConstraint conditionState condition = Memory.addConstraint conditionState condition
-        let IsFalsePathCondition conditionState = PC.isFalse conditionState.pc
-        let Contradicts state condition = PC.add state.pc condition |> PC.isFalse
-        let PathConditionToSeq (pc : pathCondition) = PC.toSeq pc
-        let EmptyPathCondition = PC.empty
+        let IsFalsePathCondition conditionState = conditionState.pc.IsFalse
+        let Contradicts state condition = 
+            let copy = PC.add condition state.pc
+            copy.IsFalse
+        let PathConditionToSeq (pc : PC.PathCondition) = pc.ToSeq()
+        let EmptyPathCondition() = PC.PathCondition()
 
     module Types =
         let Numeric t = Types.Numeric t
@@ -337,7 +339,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
@@ -447,6 +449,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
@@ -460,6 +463,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
@@ -579,7 +584,7 @@ module API =
             | _ -> internalfailf "constructing string from char array: expected string reference, but got %O" dstRef
 
         let ComposeStates state state' = Memory.composeStates state state'
-        let WLP state pc' = PC.mapPC (Memory.fillHoles state) pc' |> PC.union state.pc
+        let WLP state (pc' : PC.PathCondition) = PC.map (Memory.fillHoles state) pc' |> PC.unionWith state.pc
 
         let Merge2States (s1 : state) (s2 : state) = Memory.merge2States s1 s2
         let Merge2Results (r1, s1 : state) (r2, s2 : state) = Memory.merge2Results (r1, s1) (r2, s2)
@@ -602,7 +607,9 @@ 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
-        let PrintPC pc = PC.toString pc
+        let PrintPC (pc : PC.PathCondition) = pc.ToString()

VSharp.SILI.Core/API.fsi

@@ -18,7 +18,7 @@ module API =
     val StatedConditionalExecutionAppendResults : (state -> (state -> (term * state -> 'a) -> 'b) -> (state -> (state list -> 'a) -> 'a) -> (state -> (state list -> 'a) -> 'a) -> (state list -> 'a) -> 'b)
 
     val GuardedApplyExpression : term -> (term -> term) -> term
-    val GuardedApplyExpressionWithPC : pathCondition -> term -> (term -> term) -> term
+    val GuardedApplyExpressionWithPC : PC.PathCondition -> term -> (term -> term) -> term
     val GuardedStatedApplyStatementK : state -> term -> (state -> term -> (term * state -> 'a) -> 'a) -> ((term * state) list -> 'a) -> 'a
     val GuardedStatedApplyk : (state -> term -> ('item -> 'a) -> 'a) -> state -> term -> ('item list -> 'item list) -> ('item list -> 'a) -> 'a
 
@@ -105,8 +105,8 @@ module API =
         val AddConstraint : state -> term -> unit
         val IsFalsePathCondition : state -> bool
         val Contradicts : state -> term -> bool
-        val PathConditionToSeq : pathCondition -> term seq
-        val EmptyPathCondition : pathCondition
+        val PathConditionToSeq : PC.PathCondition -> term seq
+        val EmptyPathCondition : unit -> PC.PathCondition
 
     module Types =
         val Numeric : System.Type -> symbolicType
@@ -208,7 +208,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
@@ -241,6 +241,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
@@ -250,6 +251,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
@@ -284,16 +286,18 @@ module API =
 
         // TODO: get rid of all unnecessary stuff below!
         val ComposeStates : state -> state -> state list
-        val WLP : state -> pathCondition -> pathCondition
+        val WLP : state -> PC.PathCondition -> PC.PathCondition
 
         val Merge2States : state -> state -> state list
         val Merge2Results : term * state -> term * state -> (term * state) list
 
         val FillRegion : state -> term -> regionSort -> unit
+
+        val IsStackEmpty : state -> bool
 
     module Print =
         val Dump : state -> string
-        val PrintPC : pathCondition -> string
+        val PrintPC : PC.PathCondition -> string
 
 //    module Marshalling =
 //        val Unmarshal : state -> obj -> term * state

VSharp.SILI.Core/Copying.fs

@@ -13,13 +13,19 @@ 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}
         let constant = Constant "i" source Types.Int32
         let leftBound = simplifyLessOrEqual lowerBound constant id
         let rightBound = simplifyLessOrEqual constant upperBound id
-        let pcWithBounds = PC.add (PC.add state.pc leftBound) rightBound
+        let pcWithBounds =
+            PC.add leftBound state.pc |> PC.add rightBound
         state.pc <- pcWithBounds
         constant
 

VSharp.SILI.Core/Database.fs

@@ -194,7 +194,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