diff --git a/VSharp.SILI.Core/API.fs b/VSharp.SILI.Core/API.fs index 2fc7f4850..a2e4b143f 100644 --- a/VSharp.SILI.Core/API.fs +++ b/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() diff --git a/VSharp.SILI.Core/API.fsi b/VSharp.SILI.Core/API.fsi index 4612b8e4f..ca62a04eb 100644 --- a/VSharp.SILI.Core/API.fsi +++ b/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 diff --git a/VSharp.SILI.Core/Copying.fs b/VSharp.SILI.Core/Copying.fs index c88441bd6..1233f4a19 100644 --- a/VSharp.SILI.Core/Copying.fs +++ b/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 diff --git a/VSharp.SILI.Core/Database.fs b/VSharp.SILI.Core/Database.fs index 0ec48cd30..68a58aee3 100644 --- a/VSharp.SILI.Core/Database.fs +++ b/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 diff --git a/VSharp.SILI.Core/Memory.fs b/VSharp.SILI.Core/Memory.fs index d782dc90a..1c26d54a1 100644 --- a/VSharp.SILI.Core/Memory.fs +++ b/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,13 +30,13 @@ 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 let addConstraint (s : state) cond = - s.pc <- PC.add s.pc cond + s.pc.Add cond let delinearizeArrayIndex ind lens lbs = let detachOne (acc, lens) lb = @@ -178,6 +155,14 @@ module internal Memory = interface IStatedSymbolicConstantSource with override x.SubTerms = Seq.empty 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 @@ -214,14 +199,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 [] 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 @@ -271,6 +271,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 @@ -284,6 +289,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 @@ -296,6 +305,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 @@ -334,6 +350,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 =============== @@ -443,8 +473,8 @@ module internal Memory = match term.term with | Union gvs -> let filterUnsat (g, v) k = - let pc = PC.add state.pc g - if PC.isFalse pc then k None + let pc = PC.add g state.pc + if pc.IsFalse then k None else Some (pc, v) |> k Cps.List.choosek filterUnsat gvs (fun pcs -> match pcs with @@ -463,47 +493,56 @@ 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 = + let keepDependentWith (pc : PC.PathCondition) cond = + pc.Fragments + |> Seq.tryFind (fun pc -> 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) -> - let thenPc = PC.add state.pc condition - let elsePc = PC.add state.pc (!!condition) - if PC.isFalse thenPc then + let negatedCondition = !!condition + let thenPc = PC.add condition state.pc + let elsePc = PC.add negatedCondition state.pc + let independentThenPc = keepDependentWith thenPc condition + // In fact, this call is redundant because independentElsePc == independentThenPc with negated cond + let independentElsePc = keepDependentWith elsePc negatedCondition + if thenPc.IsFalse then conditionState.pc <- elsePc elseBranch conditionState (List.singleton >> k) - elif PC.isFalse elsePc then + elif elsePc.IsFalse 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.model <- Some model.mdl + | SolverInteraction.SmtSat elseModel -> + conditionState.pc <- elsePc + conditionState.model <- Some elseModel.mdl elseBranch conditionState (List.singleton >> k) | SolverInteraction.SmtUnsat _ -> conditionState.pc <- elsePc 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 thenBranch conditionState (List.singleton >> k) - | SolverInteraction.SmtSat model -> + | SolverInteraction.SmtSat elseModel -> + conditionState.model <- Some thenModel.mdl let thenState = conditionState let elseState = copy conditionState elsePc - elseState.model <- Some model.mdl + elseState.model <- Some elseModel.mdl thenState.pc <- thenPc execution thenState elseState condition k) @@ -691,7 +730,7 @@ module internal Memory = let private checkBlockBounds state reportError blockSize startByte endByte = let failCondition = simplifyGreater endByte blockSize id ||| simplifyLess startByte (makeNumber 0) id // NOTE: disables overflow in solver - state.pc <- PC.add state.pc (makeExpressionNoOvf failCondition id) + state.pc.Add (makeExpressionNoOvf failCondition id) reportErrorIfNeed state reportError failCondition let private readAddressUnsafe address startByte endByte = @@ -714,7 +753,7 @@ module internal Memory = and private readStructUnsafe fields structType startByte endByte = let readField fieldId = fields.[fieldId] - readFieldsUnsafe (makeEmpty()) (fun _ -> __unreachable__()) readField false structType startByte endByte + readFieldsUnsafe (State.makeEmpty None) (fun _ -> __unreachable__()) readField false structType startByte endByte and private getAffectedFields state reportError readField isStatic (blockType : symbolicType) startByte endByte = let t = toDotNetType blockType @@ -1041,7 +1080,7 @@ module internal Memory = and private writeStructUnsafe structTerm fields structType startByte value = let readField fieldId = fields.[fieldId] - let updatedFields = writeFieldsUnsafe (makeEmpty()) (fun _ -> __unreachable__()) readField false structType startByte value + let updatedFields = writeFieldsUnsafe (State.makeEmpty None) (fun _ -> __unreachable__()) readField false structType startByte value let writeField structTerm (fieldId, value) = writeStruct structTerm fieldId value List.fold writeField structTerm updatedFields @@ -1428,7 +1467,7 @@ module internal Memory = assert(not <| VectorTime.isEmpty state.currentTime) // TODO: do nothing if state is empty! list { - let pc = PC.mapPC (fillHoles state) state'.pc |> PC.union state.pc + let pc = PC.map (fillHoles state) state'.pc |> PC.unionWith state.pc // Note: this is not final evaluationStack of resulting cilState, here we forget left state's opStack at all let evaluationStack = composeEvaluationStacksOf state state'.evaluationStack let exceptionRegister = composeRaisedExceptionsOf state state'.exceptionsRegister @@ -1450,7 +1489,8 @@ module internal Memory = let g = g1 &&& g2 &&& g3 &&& g4 &&& g5 &&& g6 if not <| isFalse g then return { - pc = if isTrue g then pc else PC.add pc g + id = Guid.NewGuid().ToString() + pc = if isTrue g then pc else PC.add g pc evaluationStack = evaluationStack exceptionsRegister = exceptionRegister stack = stack @@ -1523,7 +1563,7 @@ module internal Memory = // TODO: print lower bounds? let sortBy sorter = Seq.sortBy (fst >> sorter) let sb = StringBuilder() - let sb = if PC.isEmpty s.pc then sb else s.pc |> PC.toString |> sprintf ("Path condition: %s") |> PrettyPrinting.appendLine sb + let sb = if s.pc.IsEmpty then sb else s.pc.ToString() |> sprintf ("Path condition: %s") |> PrettyPrinting.appendLine sb let sb = dumpDict "Fields" (sortBy toString) toString (MemoryRegion.toString " ") sb s.classFields let sb = dumpDict "Concrete memory" sortVectorTime VectorTime.print toString sb (s.concreteMemory |> Seq.map (fun kvp -> (kvp.Key, kvp.Value)) |> PersistentDict.ofSeq) let sb = dumpDict "Array contents" (sortBy arrayTypeToString) arrayTypeToString (MemoryRegion.toString " ") sb s.arrays diff --git a/VSharp.SILI.Core/MemoryRegion.fs b/VSharp.SILI.Core/MemoryRegion.fs index b3ce29a17..bad9f4208 100644 --- a/VSharp.SILI.Core/MemoryRegion.fs +++ b/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 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> = diff --git a/VSharp.SILI.Core/Merging.fs b/VSharp.SILI.Core/Merging.fs index 7f10d5707..520dc7a06 100644 --- a/VSharp.SILI.Core/Merging.fs +++ b/VSharp.SILI.Core/Merging.fs @@ -102,10 +102,10 @@ module internal Merging = let guardedApplyk f term k = commonGuardedApplyk f term merge k let guardedApply f term = guardedApplyk (Cps.ret f) term id - let commonGuardedMapkWithPC pc mapper gvs merge k = + let commonGuardedMapkWithPC (pc : PC.PathCondition) mapper gvs merge k = let foldFunc gvs (g, v) k = - let pc' = PC.add pc g - if PC.isFalse pc' then k gvs + let pc' = PC.add g pc + if pc'.IsFalse then k gvs else mapper v (fun t -> k ((g, t) :: gvs)) Cps.List.foldlk foldFunc [] gvs (merge >> k) diff --git a/VSharp.SILI.Core/PathCondition.fs b/VSharp.SILI.Core/PathCondition.fs index 45826af00..ca7c85831 100644 --- a/VSharp.SILI.Core/PathCondition.fs +++ b/VSharp.SILI.Core/PathCondition.fs @@ -1,40 +1,218 @@ namespace VSharp.Core open VSharp +open VSharp.Utils +open System.Collections.Generic -type pathCondition = pset +module public PC = + + type private node = + | Tail of term * term pset + | Node of term + | Empty -// Invariants: -// - PC does not contain True -// - if PC contains False then False is the only element in PC + let private unwrapNode = + function + | Tail(constant, _) -> constant + | Node(constant) -> constant + | Empty -> invalidOp "Cannot unwrap empty node" + + (* + Path condition maintains independent subsets of constants and constraints ("constraint independence") + + constants -- dictionary used as union-find structure for constants. Constants of one subset are + cyclically mapping to each other. There is only one node.Tail in subset and it is the representative + element of the subset. Tail also contains the constraints corresponding to the constants subset + + constraints -- contains all constraints of the PC. Used to avoid picking constraints from subsets each time + when the complete PC is needed + + isFalse -- flag used to determine if the PC is false trivially (i. e. c an !c were added to it). + Invariant: PC doesn't contain True or False as elements. + *) + type public PathCondition private(constants : Dictionary, constraints : HashSet, isFalse : bool) = + + let mutable isFalse = isFalse -module internal PC = + let nextNode constant = + let mutable found = Empty + constants.TryGetValue(constant, &found) |> ignore + found + + /// + /// Find operation of the union-find structure. Returns not the representative element, but the element before it + /// (for convenience) + /// + let rec findPrevious constant = + match nextNode constant with + | Tail _ -> Some(constant) + | Node nextTerm -> findPrevious nextTerm + | Empty -> None - let public empty : pathCondition = PersistentSet.empty - let public isEmpty pc = PersistentSet.isEmpty pc + /// + /// Union operation of the union-find structure. Subsets containing oneConstant and anotherConstant are merged. + /// oneConstant and anotherConstant don't need to be the representatives + /// + let union oneConstant anotherConstant = + match (findPrevious oneConstant), (findPrevious anotherConstant) with + | Some(onePrevious), Some(anotherPrevious) -> + match (nextNode onePrevious), (nextNode anotherPrevious) with + | Tail(oneRepresentative, oneConstraints), Tail(anotherRepresentative, anotherConstraints) when + oneRepresentative <> anotherRepresentative -> + let constraintsUnion = PersistentSet.union oneConstraints anotherConstraints + constants.[onePrevious] <- Tail(anotherRepresentative, constraintsUnion) + constants.[anotherPrevious] <- Node(oneRepresentative) + | _ -> () + | _ -> invalidOp "Constant not found in dictionary" - let public toSeq pc = PersistentSet.toSeq pc + /// + /// Returns union-find subset (of constants) containing the specified constant + /// + let subset constantInSubset = + seq { + let rec inner currentConstant = + seq { + if currentConstant <> constantInSubset then + yield currentConstant + match nextNode currentConstant with + | Empty -> __unreachable__() + | node -> yield! inner (unwrapNode node) + } + match nextNode constantInSubset with + | Empty -> invalidOp "Constant not found in dictionary" + | node -> + yield constantInSubset + yield! inner (unwrapNode node) + } - let private falsePC = PersistentSet.add empty False - let public isFalse pc = - let isFalsePC = PersistentSet.contains False pc - if isFalsePC then assert(toSeq pc |> Seq.length = 1) - isFalsePC + let becomeTrivialFalse() = + constants.Clear() + constraints.Clear() + isFalse <- true - let public add pc cond : pathCondition = - match cond with - | True -> pc - | False -> falsePC - | _ when isFalse pc -> falsePC - | _ when PersistentSet.contains !!cond pc -> falsePC - | _ -> PersistentSet.add pc cond + /// + /// Adds a cyclic subset to the union-find structure + /// + /// Union-find structure + /// Constants to add as nodes to the subset + /// Constraints to add to the tail + let addSubset (constants : Dictionary) constantsToAdd constraintsToAdd = + let firstConstant = constantsToAdd |> Seq.head + if Seq.length constantsToAdd = 1 then + constants.[firstConstant] <- Tail(firstConstant, constraintsToAdd) + else + constantsToAdd + |> Seq.pairwise + |> Seq.iteri (fun i (previous, next) -> + if (i <> Seq.length constantsToAdd - 2) then + constants.[previous] <- Node(next) + else + constants.[previous] <- Tail(next, constraintsToAdd) + constants.[next] <- Node(firstConstant) + ) + + let addConstraintsToSubset subsetConstant constraintsToAdd = + match findPrevious subsetConstant with + | Some(previous) -> + match nextNode previous with + | Tail(representative, constraints) -> + let constraintsUnion = PersistentSet.union constraints constraintsToAdd + constants.[previous] <- Tail(representative, constraintsUnion) + | _ -> __unreachable__() + | _ -> __unreachable__() - let public mapPC mapper (pc : pathCondition) : pathCondition = - let mapAndAdd acc cond k = - let acc' = mapper cond |> add acc - if isFalse acc' then falsePC else k acc' - Cps.Seq.foldlk mapAndAdd empty (toSeq pc) id - let public mapSeq mapper (pc : pathCondition) = toSeq pc |> Seq.map mapper + let constSourcesIndependent = + function + | ConstantT(_, oneSrc, _), ConstantT(_, anotherSrc, _) -> oneSrc.IndependentWith anotherSrc + | _ -> true - let toString pc = mapSeq toString pc |> Seq.sort |> join " /\ " + let addNewConstraintWithMerge newConstraint = + let constraintConstants = discoverConstants [newConstraint] + let oldConstants, newConstants = + constraintConstants + |> Seq.splitBy constants.ContainsKey + + // are there constraints without constants at all? + // answer: yes, in ArrayConcreteUnsafeRead, is it ok? + let newConstraintSet = PersistentSet.add PersistentSet.empty newConstraint + if Seq.isEmpty newConstants |> not then + addSubset constants newConstants newConstraintSet + else if Seq.isEmpty oldConstants |> not then + addConstraintsToSubset (Seq.head oldConstants) newConstraintSet + + constraints.Add(newConstraint) |> ignore - let union (pc1 : pathCondition) (pc2 : pathCondition) = Seq.fold add pc1 (toSeq pc2) + Seq.allPairs newConstants constants.Keys + |> Seq.filter (constSourcesIndependent >> not) + |> Seq.iter (fun (oneConst, anotherConst) -> union oneConst anotherConst) + + match (Seq.tryHead oldConstants) with + | Some(someOldConstant) -> + Seq.iter (union someOldConstant) oldConstants + match (Seq.tryHead newConstants) with + | Some(someNewConstant) -> union someNewConstant someOldConstant + | _ -> () + | _ -> () + + new() = + PathCondition(Dictionary(), HashSet(), false) + + override this.ToString() = + Seq.map toString constraints |> Seq.sort |> join " /\ " + + member this.Copy() = + PathCondition(Dictionary(constants), HashSet(constraints), isFalse) + + member this.IsFalse = isFalse + + member this.IsEmpty = constraints.Count = 0 + + member this.ToSeq() = seq constraints + + member this.Add newConstraint = + match newConstraint with + | True -> () + | False -> becomeTrivialFalse() + | _ when isFalse -> () + | _ when constraints.Contains(newConstraint) -> () + // what if constraint is not equal to newConstraint structurally, but is equal logically? + | _ when constraints.Contains(!!newConstraint) -> becomeTrivialFalse() + | _ -> addNewConstraintWithMerge newConstraint + + member this.Map mapper = + let mapped = PathCondition() + Seq.iter (mapper >> mapped.Add) constraints + mapped + + member this.UnionWith (anotherPc : PathCondition) = + let union = this.Copy() + anotherPc.ToSeq() |> Seq.iter union.Add + union + + /// + /// Returns the sequence of path conditions such that constants contained in + /// one path condition are independent with constants contained in another one + /// + member this.Fragments = + if isFalse then + Seq.singleton this + else + let getSubsetByRepresentative = + function + | Tail(representative, constraints) -> + let constants = Dictionary() + addSubset constants (subset representative) constraints + let constraints = HashSet(PersistentSet.toSeq constraints) + Some(PathCondition(constants, constraints, false)) + | _ -> None + Seq.choose getSubsetByRepresentative constants.Values + + let public add newConstraint (pc : PathCondition) = + let copy = pc.Copy() + copy.Add newConstraint + copy + + let public toSeq (pc : PathCondition) = pc.ToSeq() + + let public map mapper (pc : PathCondition) = pc.Map mapper + + let public unionWith anotherPc (pc : PathCondition) = pc.UnionWith anotherPc diff --git a/VSharp.SILI.Core/SolverInteraction.fs b/VSharp.SILI.Core/SolverInteraction.fs index ec9e8d9a9..84083e0ef 100644 --- a/VSharp.SILI.Core/SolverInteraction.fs +++ b/VSharp.SILI.Core/SolverInteraction.fs @@ -1,5 +1,7 @@ namespace VSharp.Core +open System +open System.Collections.Generic open FSharpx.Collections open VSharp @@ -36,7 +38,12 @@ module public SolverInteraction = let checkSat state = // TODO: need to solve types here? #do let ctx = getEncodingContext state - let formula = PC.toSeq state.pc |> conjunction + let formula = state.pc.ToSeq() |> conjunction match solver with - | Some s -> s.CheckSat ctx {lvl = Level.zero; queryFml = formula } + | Some s -> + let model = + state.model + |> Option.defaultValue { state = State.makeEmpty None; subst = Dictionary<_, _>(); complete = true } + s.CheckSat ctx { lvl = Level.zero; queryFml = formula; currentModel = model } | None -> SmtUnknown "" + \ No newline at end of file diff --git a/VSharp.SILI.Core/State.fs b/VSharp.SILI.Core/State.fs index 0401f5e2c..a3444afbc 100644 --- a/VSharp.SILI.Core/State.fs +++ b/VSharp.SILI.Core/State.fs @@ -2,6 +2,7 @@ namespace VSharp.Core open System open System.Collections.Generic +open System.Reflection open VSharp open VSharp.Core.Types.Constructor open VSharp.Utils @@ -115,7 +116,8 @@ with and [] state = { - mutable pc : pathCondition + id : string + mutable pc : PC.PathCondition mutable evaluationStack : evaluationStack mutable stack : callStack // Arguments and local variables mutable stackBuffers : pdict // Buffers allocated via stackAlloc @@ -141,3 +143,30 @@ and IStatedSymbolicConstantSource = inherit ISymbolicConstantSource abstract Compose : state -> term + +module public State = + let makeEmpty modelState = { + id = Guid.NewGuid().ToString() + pc = PC.PathCondition() + 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 = + Option.bind (fun state -> Some {subst = Dictionary<_,_>(); state = state; complete = true}) modelState + } + diff --git a/VSharp.SILI.Core/Terms.fs b/VSharp.SILI.Core/Terms.fs index 54f139b0c..ee73174a9 100644 --- a/VSharp.SILI.Core/Terms.fs +++ b/VSharp.SILI.Core/Terms.fs @@ -232,6 +232,7 @@ and ISymbolicConstantSource = abstract SubTerms : term seq abstract Time : vectorTime + abstract IndependentWith : ISymbolicConstantSource -> bool type INonComposableSymbolicConstantSource = inherit ISymbolicConstantSource @@ -518,6 +519,10 @@ module internal Terms = let (|UnionT|_|) = term >> function | Union gvs -> Some(UnionT gvs) | _ -> None + + let (|ConstantT|_|) = term >> function + | Constant(name, src, typ) -> Some(ConstantT name, src, typ) + | _ -> None let (|GuardedValues|_|) = function // TODO: this could be ineffective (because of unzip) | Union gvs -> Some(GuardedValues(List.unzip gvs)) @@ -719,10 +724,9 @@ module internal Terms = | GuardedValues(gs, vs) -> foldSeq folder gs state |> foldSeq folder vs | Slice(t, s, e, pos) -> - let state = folder state t - let state = folder state s - let state = folder state e - folder state pos + foldSeq folder [t; s; e; pos] state + | Union(terms) -> + foldSeq folder (List.unzip terms |> (fun (l1, l2) -> List.append l1 l2)) state | _ -> state and doFold folder state term = diff --git a/VSharp.SILI.Core/TypeCasting.fs b/VSharp.SILI.Core/TypeCasting.fs index c8795d5f3..eeae9192e 100644 --- a/VSharp.SILI.Core/TypeCasting.fs +++ b/VSharp.SILI.Core/TypeCasting.fs @@ -24,6 +24,10 @@ module internal TypeCasting = interface IStatedSymbolicConstantSource with override x.SubTerms = optCons (optCons [] x.left.SubTerm) x.right.SubTerm :> term seq override x.Time = VectorTime.zero + override x.IndependentWith otherSource = + match otherSource with + | :? symbolicSubtypeSource as otherSubtype -> x <> otherSubtype + | _ -> true let (|TypeSubtypeTypeSource|_|) (src : ISymbolicConstantSource) = match src with diff --git a/VSharp.SILI/Interpreter.fs b/VSharp.SILI/Interpreter.fs index c93e90386..85f76a149 100644 --- a/VSharp.SILI/Interpreter.fs +++ b/VSharp.SILI/Interpreter.fs @@ -1949,7 +1949,8 @@ type internal ILInterpreter(isConcolicMode : bool) as this = let rec makeStep' ip k = match ip with | Instruction(offset, m) -> - if offset = 0 then Logger.printLogLazy Logger.Info "Starting to explore method %O" (lazy Reflection.getFullMethodName m) + if offset = 0 then + Logger.printLogLazy Logger.Info "Starting to explore method %O" (lazy Reflection.getFullMethodName m) x.ExecuteInstruction m offset cilState |> k | Exit m -> exit m diff --git a/VSharp.SILI/SILI.fs b/VSharp.SILI/SILI.fs index 8370e1bb1..9b6b71b82 100644 --- a/VSharp.SILI/SILI.fs +++ b/VSharp.SILI/SILI.fs @@ -15,7 +15,7 @@ type public SILI(options : SiliOptions) = let statistics = SILIStatistics() let infty = UInt32.MaxValue - let emptyState = Memory.EmptyState() + let emptyState = Memory.EmptyState None let isConcolicMode = match options.executionMode with | ConcolicMode -> true @@ -52,7 +52,7 @@ type public SILI(options : SiliOptions) = let coveragePobsForMethod (method : MethodBase) = let cfg = CFG.findCfg method cfg.sortedOffsets |> Seq.map (fun offset -> - {loc = {offset = offset; method = method}; lvl = infty; pc = EmptyPathCondition}) + {loc = {offset = offset; method = method}; lvl = infty; pc = EmptyPathCondition()}) |> List.ofSeq let reportState reporter isError method cmdArgs state = @@ -80,7 +80,9 @@ type public SILI(options : SiliOptions) = action.Invoke e static member private FormInitialStateWithoutStatics (method : MethodBase) = - let initialState = Memory.EmptyState() + let modelState = Memory.EmptyState None + Memory.FillWithParametersAndThis modelState method + let initialState = Memory.EmptyState (Some modelState) let cilState = makeInitialState method initialState try let this(*, isMethodOfStruct*) = @@ -197,7 +199,9 @@ type public SILI(options : SiliOptions) = reportIncomplete <- wrapOnIIE onIIE reportInternalFail <- wrapOnInternalFail onInternalFail interpreter.ConfigureErrorReporter reportError - let state = Memory.EmptyState() + let modelState = Memory.EmptyState None + Memory.FillWithParametersAndThis modelState method + let state = Memory.EmptyState (Some modelState) let argsToState args = let argTerms = Seq.map (fun str -> Memory.AllocateString str state) args let stringType = Types.FromDotNetType typeof diff --git a/VSharp.SILI/Statistics.fs b/VSharp.SILI/Statistics.fs index a4950b80e..f14319f15 100644 --- a/VSharp.SILI/Statistics.fs +++ b/VSharp.SILI/Statistics.fs @@ -12,7 +12,7 @@ open VSharp.Utils open CilStateOperations open ipOperations -type pob = {loc : codeLocation; lvl : uint; pc : pathCondition} +type pob = {loc : codeLocation; lvl : uint; pc : PC.PathCondition} with override x.ToString() = sprintf "loc = %O; lvl = %d; pc = %s" x.loc x.lvl (Print.PrintPC x.pc) diff --git a/VSharp.SILI/TestGenerator.fs b/VSharp.SILI/TestGenerator.fs index 507ab859f..8ec3366b5 100644 --- a/VSharp.SILI/TestGenerator.fs +++ b/VSharp.SILI/TestGenerator.fs @@ -123,6 +123,7 @@ module TestGenerator = let state2test isError (m : MethodBase) cmdArgs (cilState : cilState) = let indices = Dictionary() let test = UnitTest m + test.StateId <- Some cilState.state.id let hasException = match cilState.state.exceptionsRegister with | Unhandled e -> diff --git a/VSharp.Solver/Z3.fs b/VSharp.Solver/Z3.fs index b5539aea2..4d5d7f804 100644 --- a/VSharp.Solver/Z3.fs +++ b/VSharp.Solver/Z3.fs @@ -9,7 +9,6 @@ open VSharp.Core.SolverInteraction open Logger module internal Z3 = - // ------------------------------- Exceptions ------------------------------- type EncodingException(msg : string) = @@ -72,7 +71,7 @@ module internal Z3 = type private Z3Builder(ctx : Context) = let mutable encodingCache = freshCache() - let emptyState = Memory.EmptyState() + let emptyState = Memory.EmptyState None let getMemoryConstant mkConst (typ : regionSort * fieldId list) = let result : ArrayExpr ref = ref null @@ -84,6 +83,9 @@ module internal Z3 = member x.Reset() = encodingCache <- freshCache() + + member x.ClearT2E() = + encodingCache.t2e.Clear() member private x.ValidateId id = assert(not <| String.IsNullOrWhiteSpace id) @@ -657,43 +659,42 @@ module internal Z3 = Memory.DefaultOf structureType |> ref) structureRef.Value <- x.WriteFields structureRef.Value value fields - member x.MkModel (m : Model) = - let subst = Dictionary() + member x.UpdateModel (z3Model : Model) (targetModel : model) = let stackEntries = Dictionary() encodingCache.t2e |> Seq.iter (fun kvp -> match kvp.Key with | {term = Constant(_, StructFieldChain(fields, StackReading(key)), t)} -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) x.Decode t refinedExpr |> x.WriteDictOfValueTypes stackEntries key fields key.TypeOfLocation | {term = Constant(_, (:? IMemoryAccessConstantSource as ms), _)} -> match ms with | HeapAddressSource(StackReading(key)) -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) let t = key.TypeOfLocation let addr = refinedExpr |> x.DecodeConcreteHeapAddress t |> ConcreteHeapAddress stackEntries.Add(key, HeapRef addr t |> ref) | _ -> () | {term = Constant(_, :? IStatedSymbolicConstantSource, _)} -> () | {term = Constant(_, source, t)} -> - let refinedExpr = m.Eval(kvp.Value.expr, false) + let refinedExpr = z3Model.Eval(kvp.Value.expr, false) let term = x.Decode t refinedExpr - subst.Add(source, term) + targetModel.subst.[source] <- term | _ -> ()) - let state = Memory.EmptyState() - let frame = stackEntries |> Seq.map (fun kvp -> + if (Memory.IsStackEmpty targetModel.state) then + Memory.NewStackFrame targetModel.state null List.empty + + stackEntries |> Seq.iter (fun kvp -> let key = kvp.Key let term = !kvp.Value - let typ = TypeOf term - (key, Some term, typ)) - Memory.NewStackFrame state null (List.ofSeq frame) + Memory.Allocate targetModel.state key term) let defaultValues = Dictionary() encodingCache.regionConstants |> Seq.iter (fun kvp -> let region, fields = kvp.Key let constant = kvp.Value - let arr = m.Eval(constant, false) + let arr = z3Model.Eval(constant, false) let rec parseArray (arr : Expr) = if arr.IsConstantArray then assert(arr.Args.Length = 1) @@ -717,26 +718,25 @@ module internal Z3 = let address = arr.Args |> Array.last |> x.DecodeConcreteHeapAddress t |> ConcreteHeapAddress HeapRef address t let address = fields |> List.fold (fun address field -> StructField(address, field)) address - let states = Memory.Write state (Ref address) value - assert(states.Length = 1 && states.[0] = state) + let states = Memory.Write targetModel.state (Ref address) value + assert(states.Length = 1 && states.[0] = targetModel.state) elif arr.IsConst then () else internalfailf "Unexpected array expression in model: %O" arr parseArray arr) defaultValues |> Seq.iter (fun kvp -> let region = kvp.Key let constantValue = !kvp.Value - Memory.FillRegion state constantValue region) + Memory.FillRegion targetModel.state constantValue region) encodingCache.heapAddresses |> Seq.iter (fun kvp -> let typ, _ = kvp.Key let addr = kvp.Value - if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr state.allocatedTypes then - state.allocatedTypes <- PersistentDict.add addr typ state.allocatedTypes) - state.startingTime <- [encodingCache.lastSymbolicAddress - 1] + if VectorTime.less addr VectorTime.zero && not <| PersistentDict.contains addr targetModel.state.allocatedTypes then + targetModel.state.allocatedTypes <- PersistentDict.add addr typ targetModel.state.allocatedTypes) + targetModel.state.startingTime <- VectorTime.min targetModel.state.startingTime [encodingCache.lastSymbolicAddress - 1] encodingCache.heapAddresses.Clear() - {state = state; subst = subst; complete = true} - + encodingCache.t2e.Clear() let private ctx = new Context() let private builder = Z3Builder(ctx) @@ -803,15 +803,19 @@ module internal Z3 = match result with | Status.SATISFIABLE -> let z3Model = optCtx.Model - let model = builder.MkModel z3Model + let updatedModel = {q.currentModel with state = {q.currentModel.state with model = q.currentModel.state.model}} + builder.UpdateModel z3Model updatedModel // let usedPaths = // pathAtoms // |> Seq.filter (fun atom -> z3Model.Eval(atom, false).IsTrue) // |> Seq.map (fun atom -> paths.[atom]) - SmtSat { mdl = model; usedPaths = [](*usedPaths*) } + builder.ClearT2E() + SmtSat { mdl = updatedModel; usedPaths = [](*usedPaths*) } | Status.UNSATISFIABLE -> + builder.ClearT2E() SmtUnsat { core = Array.empty (*optCtx.UnsatCore |> Array.map (builder.Decode Bool)*) } | Status.UNKNOWN -> + builder.ClearT2E() SmtUnknown optCtx.ReasonUnknown | _ -> __unreachable__() with diff --git a/VSharp.Test/IntegrationTests.cs b/VSharp.Test/IntegrationTests.cs index 129b4c868..806ab4e55 100644 --- a/VSharp.Test/IntegrationTests.cs +++ b/VSharp.Test/IntegrationTests.cs @@ -5,6 +5,7 @@ using System.Globalization; using System.Linq; using System.Threading; +using Microsoft.FSharp.Core; using NUnit.Framework; using NUnit.Framework.Interfaces; using NUnit.Framework.Internal; @@ -108,7 +109,7 @@ private TestResult Explore(TestExecutionContext context) UnitTests unitTests = new UnitTests(Directory.GetCurrentDirectory()); explorer.InterpretIsolated(methodInfo, unitTests.GenerateTest, unitTests.GenerateError, _ => { }, e => throw e); - + if (unitTests.UnitTestsCount == 0 && unitTests.ErrorsCount == 0 && explorer.Statistics.IncompleteStates.Count == 0) { throw new Exception("No states were obtained! Most probably this is bug."); @@ -132,6 +133,9 @@ private TestResult Explore(TestExecutionContext context) { context.CurrentResult.SetResult(ResultState.Success); } + + Stopwatch.saveMeasurements(methodInfo.Name); + Stopwatch.clear(); } catch (Exception e) { diff --git a/VSharp.Utils/Collections.fs b/VSharp.Utils/Collections.fs index 57fee4f2b..ae72a81aa 100644 --- a/VSharp.Utils/Collections.fs +++ b/VSharp.Utils/Collections.fs @@ -31,6 +31,15 @@ module public Seq = lenProd <- lenProd * lengths.[i] Array.mapFold detachOne (idx, lenProd) (Array.init lengths.Length id) |> fst + let splitBy condition seq = + let grouped = Seq.groupBy (fun element -> condition element) seq + match (Seq.tryFind (fun (value, _) -> value) grouped), + (Seq.tryFind (fun (value, _) -> value |> not) grouped) with + | Some(_, trueSeq), Some(_, falseSeq) -> trueSeq, falseSeq + | Some(_, trueSeq), None -> trueSeq, Seq.empty + | None, Some(_, falseSeq) -> Seq.empty, falseSeq + | None, None -> Seq.empty, Seq.empty + module public List = let rec private mappedPartitionAcc f left right = function | [] -> (List.rev left, List.rev right) diff --git a/VSharp.Utils/PersistentDictionary.fs b/VSharp.Utils/PersistentDictionary.fs index b72da08ed..6f1a76259 100644 --- a/VSharp.Utils/PersistentDictionary.fs +++ b/VSharp.Utils/PersistentDictionary.fs @@ -50,8 +50,12 @@ module public PersistentDict = let public size (d : pdict<'a, 'b>) = d.impl.Length - let public map (keyMapper : 'a -> 'a) (valueMapper : 'b -> 'c) (d : pdict<'a, 'b>) : pdict<'a, 'c> = + let public map (keyMapper : 'a -> 'd) (valueMapper : 'b -> 'c) (d : pdict<'a, 'b>) : pdict<'d, 'c> = d |> toSeq |> Seq.map (fun (k, v) -> (keyMapper k, valueMapper v)) |> ofSeq + + let public filterKeys (filter : 'a -> bool) (d : pdict<'a, 'b>) : pdict<'a, 'b> = + d |> toSeq |> Seq.filter (fun (k, _) -> filter k) |> ofSeq + let public iter (action : 'a * 'b -> unit) (d : pdict<'a, 'b>) : unit = d |> toSeq |> Seq.iter action let public fold folder state (d : pdict<'a, 'b>) = @@ -118,6 +122,9 @@ module PersistentSet = let public isEmpty (d : pset<'a>) = PersistentDict.isEmpty d let public toSeq (d : pset<'a>) = PersistentDict.keys d + + let public ofSeq (s : seq<'a>) : pset<'a> = + s |> Seq.map (fun k -> k, 0) |> PersistentDict.ofSeq let public contains (key : 'a) (d : pset<'a>) = PersistentDict.contains key d @@ -131,8 +138,16 @@ module PersistentSet = d |> toSeq |> Seq.fold folder state let public forall predicate (d : pset<'a>) = d |> toSeq |> Seq.forall predicate - let public map (mapper : 'a -> 'a) (d : pset<'a>) : pset<'a> = + + let public map (mapper : 'a -> 'b) (d : pset<'a>) : pset<'b> = PersistentDict.map mapper id d + + let public filter (filter : 'a -> bool) (d : pset<'a>) : pset<'a> = + PersistentDict.filterKeys filter d + + let public choose (chooser : 'a -> 'b option) (d : pset<'a>) : pset<'b> = + d |> toSeq |> Seq.choose chooser |> ofSeq + let public iter (action : 'a -> unit) (d : pset<'a>) : unit = PersistentDict.iter (fst >> action) d diff --git a/VSharp.Utils/Stopwatch.fs b/VSharp.Utils/Stopwatch.fs new file mode 100644 index 000000000..f83acc22b --- /dev/null +++ b/VSharp.Utils/Stopwatch.fs @@ -0,0 +1,119 @@ +namespace VSharp + +open System +open System.Collections.Generic +open System.Diagnostics +open System.Globalization +open System.IO +open CsvHelper +open CsvHelper.Configuration + +/// +/// Contains functions for running code with time measurement and measurement results export +/// +module Stopwatch = + + type private measurement = { stopwatch: Stopwatch; mutable timesCalled: int } + type private csvRecord = + { + commitHash: string + dateTime: string + caseName: string + tag: string + timesCalled: int + totalTicks: int64 + totalMs: int64 + } + + let private csvPath = Path.Combine(Environment.GetFolderPath(Environment.SpecialFolder.MyDocuments), "VSharpBenchmark") + let private csvFilename = "benchmark.csv" + let private measurements = Dictionary() + + let private getGitCommitHash () = + let procStartInfo = ProcessStartInfo("git", "rev-parse --short HEAD") + + procStartInfo.RedirectStandardOutput <- true + procStartInfo.UseShellExecute <- false + procStartInfo.CreateNoWindow <- true + + use proc = new Process() + proc.StartInfo <- procStartInfo + + proc.Start() |> ignore + proc.WaitForExit() + + proc.StandardOutput.ReadLine() + + /// + /// Runs function saving its execution time + /// + /// Tag to save results with. Results from multiple runs with the same tag are added up + /// Function to run + let public runMeasuringTime tag action = + let measurement = + if (measurements.ContainsKey tag) then + measurements.[tag] + else + let newMeasurement = { stopwatch = Stopwatch(); timesCalled = 0 } + measurements.[tag] <- newMeasurement + newMeasurement + if measurement.stopwatch.IsRunning then + measurement.timesCalled <- measurement.timesCalled + 1 + action() + else + try + measurement.stopwatch.Start() + measurement.timesCalled <- measurement.timesCalled + 1 + action() + finally + measurement.stopwatch.Stop() + + /// + /// Stops all running measurements + /// + let public stopAll () = + measurements + |> Seq.map (|KeyValue|) + |> Seq.iter (fun (_, m) -> m.stopwatch.Stop()) + + /// + /// Saves all current measurement results to .csv file. If the file already exists, appends lines + /// + /// Additional tag given to the saved measurements + let public saveMeasurements caseName = + stopAll() + + let commitHash = getGitCommitHash() + let currentDateTime = DateTime.Now.ToString("yyyy-MM-ddTHH-mm-ss") + + let records = + measurements + |> Seq.map (|KeyValue|) + |> Seq.map (fun (tag, m) -> + { + commitHash = commitHash + dateTime = currentDateTime + caseName = caseName + tag = tag + timesCalled = m.timesCalled + totalTicks = m.stopwatch.ElapsedTicks + totalMs = m.stopwatch.ElapsedMilliseconds + } + ) + + let targetPath = Path.Combine(csvPath, csvFilename) + + let configuration = CsvConfiguration(CultureInfo.InvariantCulture) + configuration.IncludePrivateMembers <- true + configuration.HasHeaderRecord <- File.Exists(targetPath) |> not + + Directory.CreateDirectory(csvPath) |> ignore + use streamWriter = File.AppendText(targetPath) + use csvWriter = new CsvWriter(streamWriter, configuration) + + csvWriter.WriteRecords(records) + + /// + /// Clears all current measurements + /// + let public clear () = measurements.Clear() diff --git a/VSharp.Utils/TaggedLogger.fs b/VSharp.Utils/TaggedLogger.fs new file mode 100644 index 000000000..0f0017d61 --- /dev/null +++ b/VSharp.Utils/TaggedLogger.fs @@ -0,0 +1,40 @@ +namespace VSharp + +open System +open System.Collections.Generic +open System.IO +open System.Text + +/// +/// Contains functions for saving logs with tag keys. +/// May be used to save logs from different states separately +/// +module TaggedLogger = + + let logs = Dictionary() + + /// + /// Saves log with the tag + /// + /// Tag to save the log with + /// Message to log + let public log tag (message : string) = + if not <| logs.ContainsKey(tag) then logs.Add(tag, StringBuilder()) + logs.[tag].AppendLine(message) |> ignore + + /// + /// Saves with toTag all logs with fromTag + /// + let public copy fromTag toTag = + let from = logs.GetValueOrDefault(fromTag, StringBuilder()).ToString() + logs.[toTag] <- StringBuilder().AppendLine(from) + + /// + /// Saves all logs with the specified tag to the file + /// + /// Tag to save the logs with + /// Path of the file to save + let public saveLog tag path = + if logs.ContainsKey tag then + let log = logs[tag].ToString() + File.WriteAllText(path, log) diff --git a/VSharp.Utils/UnitTest.fs b/VSharp.Utils/UnitTest.fs index 52814a1b6..ed344acbb 100644 --- a/VSharp.Utils/UnitTest.fs +++ b/VSharp.Utils/UnitTest.fs @@ -55,8 +55,14 @@ type UnitTest private (m : MethodBase, info : testInfo) = let classTypeParameters = info.classTypeParameters |> Array.map Serialization.decodeType let methodTypeParameters = info.methodTypeParameters |> Array.map Serialization.decodeType let mutable extraAssemblyLoadDirs : string list = [Directory.GetCurrentDirectory()] + let mutable stateId : string option = None new(m : MethodBase) = UnitTest(m, testInfo.OfMethod m) + + member x.StateId + with get() = stateId + and set id = + stateId <- id member x.Method with get() = m member x.ThisArg diff --git a/VSharp.Utils/UnitTests.fs b/VSharp.Utils/UnitTests.fs index 5f7848453..70f01f2b6 100644 --- a/VSharp.Utils/UnitTests.fs +++ b/VSharp.Utils/UnitTests.fs @@ -32,6 +32,8 @@ type UnitTests(outputDir : string) = member x.GenerateTest (test : UnitTest) = testNumber <- testNumber + 1u + if test.StateId.IsSome then + TaggedLogger.saveLog test.StateId.Value $"%s{currentDir.FullName}%c{Path.DirectorySeparatorChar}info%s{testNumber.ToString()}.txt" generateTest test ("test" + testNumber.ToString()) member x.GenerateError (test : UnitTest) = diff --git a/VSharp.Utils/VSharp.Utils.fsproj b/VSharp.Utils/VSharp.Utils.fsproj index dea7e5963..8daf2334c 100644 --- a/VSharp.Utils/VSharp.Utils.fsproj +++ b/VSharp.Utils/VSharp.Utils.fsproj @@ -17,7 +17,9 @@ + + @@ -44,6 +46,7 @@ + diff --git a/runtime b/runtime index 3a25a7f1c..d7619cd4b 160000 --- a/runtime +++ b/runtime @@ -1 +1 @@ -Subproject commit 3a25a7f1cc446b60678ed25c9d829420d6321eba +Subproject commit d7619cd4b165c13430484e381042f055d4c5a9c7