Skip to content

Commit 7b6e6a2

Browse files
oveeernightoveeernight
committed
[fix] collecting latest nodes; style
1 parent c7f669e commit 7b6e6a2

File tree

12 files changed

+43
-63
lines changed

12 files changed

+43
-63
lines changed

‎VSharp.SILI.Core/API.fs‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -468,11 +468,6 @@ module API =
468468
let TryAddressFromRefFork state ref =
469469
CommonTryAddressFromRef state ref true
470470

471-
let private transformBoxedRef ref =
472-
match ref.term with
473-
| HeapRef _ -> HeapReferenceToBoxReference ref
474-
| _ -> ref
475-
476471
let ExtractAddress ref = extractAddress ref
477472
let ExtractPointerOffset ptr = extractPointerOffset ptr
478473

@@ -540,11 +535,10 @@ module API =
540535
let WriteStackLocation state location value = state.memory.WriteStackLocation location value
541536

542537
let Write state reference value = state.memory.Write emptyReporter reference value
543-
544538

545539
let WriteUnsafe (reporter : IErrorReporter) state reference value =
546540
reporter.ConfigureState state
547-
state.memory.WriteUnsafe reporter reference value
541+
state.memory.Write reporter reference value
548542

549543
let WriteStructField structure field value = writeStruct structure field value
550544

‎VSharp.SILI.Core/Branching.fs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,7 @@ module internal Branching =
1818
let statedApply (pc, v) k = f (state.Copy pc) v k
1919
Cps.List.mapk statedApply filteredBranches (fun appliedBranches ->
2020
f state iteType.elseValue (fun appliedElse ->
21-
appliedBranches @ [appliedElse] |> mergeResults |> k
22-
)))
21+
appliedBranches @ [appliedElse] |> mergeResults |> k)))
2322
| _ -> f state term (List.singleton >> k)
2423
let guardedStatedApplyk f state term k = commonGuardedStatedApplyk f state term State.mergeResults k
2524
let guardedStatedApply f state term = guardedStatedApplyk (Cps.ret2 f) state term id

‎VSharp.SILI.Core/Memory.fs‎

Lines changed: 15 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -308,7 +308,7 @@ module internal Memory =
308308
Ref (BoxedLocation(address, typ))
309309
| Ite iteType -> Merging.guardedMap heapReferenceToBoxReference iteType
310310
| _ -> internalfailf $"Unboxing: expected heap reference, but got {reference}"
311-
let private transformBoxedRef ref =
311+
let transformBoxedRef ref =
312312
match ref.term with
313313
| HeapRef _ -> heapReferenceToBoxReference ref
314314
| _ -> ref
@@ -1503,7 +1503,7 @@ module internal Memory =
15031503
| StructField(address, field) ->
15041504
let oldStruct = self.ReadSafe reporter address
15051505
let updatedStruct = guardedWriteStruct guard oldStruct field value
1506-
self.WriteSafe reporter None address updatedStruct // is guard needed?
1506+
self.WriteSafe reporter None address updatedStruct
15071507
// TODO: need concrete memory for BoxedLocation?
15081508
| BoxedLocation(address, _) -> self.WriteBoxedLocation guard address value
15091509
| StackBufferIndex(key, index) -> writeStackBuffer key guard index value
@@ -1760,8 +1760,9 @@ module internal Memory =
17601760
if not currentMethod.IsStaticConstructor then
17611761
concreteMemory.StaticFieldChanged field
17621762

1763-
member private self.CommonWrite (reporter : IErrorReporter) isSafe guard reference value =
1764-
let transformed = if isSafe then transformBoxedRef reference else reference
1763+
member private self.CommonWrite (reporter : IErrorReporter) guard reference value =
1764+
assert(if Option.isSome guard then isTrue guard.Value |> not else true)
1765+
let transformed = transformBoxedRef reference
17651766
match transformed.term with
17661767
| Ref address -> self.WriteSafe reporter guard address value
17671768
| DetachedPtr _ -> reporter.ReportFatalError "writing by detached pointer" (True()) |> ignore
@@ -1771,7 +1772,7 @@ module internal Memory =
17711772
| Ite iteType ->
17721773
let filtered = iteType.filter(fun r -> Pointers.isBadRef r |> isTrue |> not)
17731774
filtered.ToDisjunctiveGvs()
1774-
|> List.iter (fun (g, r) -> self.CommonWrite reporter isSafe (Some g) r value)
1775+
|> List.iter (fun (g, r) -> self.CommonWrite reporter (Some g) r value)
17751776
| _ -> internalfail $"Writing: expected reference, but got {reference}"
17761777

17771778
// ------------------------------- Allocation -------------------------------
@@ -2088,8 +2089,7 @@ module internal Memory =
20882089
member self.RemoveDelegate sourceRef toRemoveRef typ = self.RemoveDelegate sourceRef toRemoveRef typ
20892090
member self.StringArrayInfo stringAddress length = self.StringArrayInfo stringAddress length
20902091
member self.TypeOfHeapLocation address = self.TypeOfHeapLocation address
2091-
member self.Write reporter reference value = self.CommonWrite reporter true None reference value
2092-
member self.WriteUnsafe reporter reference value = self.CommonWrite reporter false None reference value
2092+
member self.Write reporter reference value = self.CommonWrite reporter None reference value
20932093
member self.WriteStaticField typ field value = self.CommonWriteStaticField None typ field value
20942094

20952095
type heapReading<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> with
@@ -2103,12 +2103,10 @@ module internal Memory =
21032103
let effect = MemoryRegion.map substTerm substType substTime x.memoryObject
21042104
let before = x.picker.extract state
21052105
let after = MemoryRegion.compose before effect
2106-
let read region =
2107-
assert(state.memory :? Memory)
2108-
let memory = state.memory :?> Memory
2109-
let inst typ region = memory.MakeSymbolicHeapRead x.picker key state.startingTime typ region
2110-
MemoryRegion.read region key (x.picker.isDefaultKey state) inst (fun _ _ -> __unreachable__())
2111-
read after
2106+
assert(state.memory :? Memory)
2107+
let memory = state.memory :?> Memory
2108+
let inst typ region = memory.MakeSymbolicHeapRead x.picker key state.startingTime typ region
2109+
MemoryRegion.read after key (x.picker.isDefaultKey state) inst memory.RangeReadingUnreachable
21122110

21132111
type arrayReading with
21142112
interface IMemoryAccessConstantSource with
@@ -2125,12 +2123,10 @@ module internal Memory =
21252123
let before = x.picker.extract state
21262124
MemoryRegion.compose before effect
21272125
else x.memoryObject
2128-
let read region =
2129-
assert(state.memory :? Memory)
2130-
let memory = state.memory :?> Memory
2131-
let inst = memory.MakeArraySymbolicHeapRead x.picker key state.startingTime
2132-
MemoryRegion.read region key (x.picker.isDefaultKey state) inst memory.SpecializedReading
2133-
read after
2126+
assert(state.memory :? Memory)
2127+
let memory = state.memory :?> Memory
2128+
let inst = memory.MakeArraySymbolicHeapRead x.picker key state.startingTime
2129+
MemoryRegion.read after key (x.picker.isDefaultKey state) inst memory.SpecializedReading
21342130

21352131
type state with
21362132
static member MakeEmpty complete =

‎VSharp.SILI.Core/MemoryRegion.fs‎

Lines changed: 9 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,10 @@ type heapArrayKey =
319319
match a.term with
320320
| ConcreteHeapAddress addr -> PersistentSet.contains addr explicitAddresses
321321
| _ -> false
322-
override x.IsRange = match x with | OneArrayIndexKey _ -> false | RangeArrayIndexKey _ -> true
322+
override x.IsRange =
323+
match x with
324+
| OneArrayIndexKey _ -> false
325+
| RangeArrayIndexKey _ -> true
323326

324327
interface IComparable with
325328
override x.CompareTo y =
@@ -504,7 +507,7 @@ and ISymbolicTypeKey = IMemoryKey<symbolicTypeKey, freeRegion<typeWrapper>>
504507
type updateTreeKey<'key, 'value when 'key : equality> =
505508
{key : 'key; value : 'value; guard : term option; time : vectorTime}
506509
interface IRegionTreeKey<updateTreeKey<'key, 'value>> with
507-
override x.Hides y = x.key = y.key
510+
override x.Hides y = x.key = y.key && x.hasTrueGuard
508511
member x.termGuard = Option.defaultValue (True()) x.guard
509512
member x.hasTrueGuard =
510513
match x.guard with
@@ -514,7 +517,7 @@ type updateTreeKey<'key, 'value when 'key : equality> =
514517
match x.guard with
515518
| Some g when isFalse g -> true
516519
| _ -> false
517-
override x.ToString() = (x.key, x.value, x.guard).ToString()
520+
override x.ToString() = (x.key, x.value, x.guard, x.time).ToString()
518521

519522
type updateTree<'key, 'value, 'reg when 'key :> IMemoryKey<'key, 'reg> and 'reg :> IRegion<'reg> and 'key : equality and 'value : equality and 'reg : equality> =
520523
regionTree<updateTreeKey<'key, 'value>, 'reg>
@@ -563,13 +566,7 @@ module private UpdateTree =
563566
let rec private collectBranchLatestRecords (Node d) predicate latestRecords =
564567
let collectSubtreeNodes acc r (k, st) =
565568
if predicate k then
566-
let recLatestRecords = collectBranchLatestRecords st predicate acc
567-
let recLatestTime = (recLatestRecords |> List.head |> snd).time
568-
let currLatestTime = (acc |> List.head |> snd).time
569-
if (VectorTime.greater recLatestTime currLatestTime) then
570-
recLatestRecords
571-
else
572-
(r,k)::recLatestRecords
569+
collectBranchLatestRecords st predicate acc
573570
else
574571
let currLatestTime = (latestRecords |> List.head |> snd).time
575572
if VectorTime.greater k.time currLatestTime then // found strictly later record, reset acc
@@ -593,7 +590,6 @@ module private UpdateTree =
593590
let keyRegion = List.fold (fun acc (r, _) -> (acc :> IRegion<_>).Subtract r) reg otherKeys
594591
if reg = keyRegion && (List.head sameKey |> snd).hasTrueGuard then
595592
let key = List.head sameKey |> snd
596-
assert(sameKey |> List.forall (fun (_, k) -> k.value = key.value))
597593
key.value
598594
else if key.IsRange then makeSymbolic (Node d)
599595
else splitRead d key explicitAddresses specializedReading predicate isDefault makeSymbolic makeDefault
@@ -624,7 +620,7 @@ module private UpdateTree =
624620
let unguardedKey = (utKey.key :> IMemoryKey<_,_>).Unguard
625621
let disjointUnguardedKey = List.mapFold (fun disjGuard (g, k) -> (disjGuard &&& g, k), !!g &&& disjGuard) (True()) unguardedKey |> fst
626622
let writeOneKey (g, k) accTree =
627-
let included, disjoint = RegionTree.localizeFilter region utKey accTree
623+
let included, disjoint = RegionTree.localizeFilterHidden region utKey accTree
628624
let refinedKey =
629625
let guard = utKey.termGuard &&& g |> Some
630626
{utKey with guard = guard; key = k}
@@ -650,7 +646,7 @@ module private UpdateTree =
650646
let writeOneKey reg utKey (accTree, time) =
651647
assert(not (utKey.key :> IMemoryKey<_,_>).IsUnion)
652648
write reg {utKey with time = time} accTree predicate, VectorTime.next time
653-
later |> RegionTree.foldr writeOneKey (earlier, nextUpdateTime)
649+
RegionTree.foldr writeOneKey (earlier, nextUpdateTime) later
654650

655651
let deterministicCompose earlier later = RegionTree.append earlier later
656652

‎VSharp.SILI.Core/Propositional.fs‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -276,8 +276,7 @@ module internal Propositional =
276276
| _ -> __unreachable__()
277277
let simplifiedDisjunctions = List.map filterDisjunction disjunctions
278278
conjunction (List.append literals simplifiedDisjunctions)
279-
| _ -> res
280-
)
279+
| _ -> res)
281280

282281
let lazyConjunction xs =
283282
Cps.Seq.foldlk lazyAnd (True()) xs id
@@ -317,7 +316,7 @@ module internal Propositional =
317316

318317
type genericIteType<'a> with
319318
member x.ToDisjunctiveIte() =
320-
let disjointBranches, elseGuard = List.mapFold (fun disjG (g, v) -> (g &&& disjG , v) , (!!g) &&& disjG) (True()) x.branches
319+
let disjointBranches, elseGuard = List.mapFold (fun disjG (g, v) -> (g &&& disjG, v) , (!!g) &&& disjG) (True()) x.branches
321320
{x with branches = disjointBranches}, elseGuard
322321
member x.ToDisjunctiveGvs() =
323322
let disjointX, elseGuard = x.ToDisjunctiveIte()
@@ -328,4 +327,3 @@ module internal Propositional =
328327
| False -> None
329328
| _ -> Some(g, v)
330329
{x with branches = List.choose chooser x.branches}
331-

‎VSharp.SILI.Core/State.fs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -261,7 +261,6 @@ and IMemory =
261261
abstract GuardedWriteClassField : term option -> term -> fieldId -> term -> unit
262262

263263
abstract Write : IErrorReporter -> term -> term -> unit
264-
abstract WriteUnsafe : IErrorReporter -> term -> term -> unit
265264
abstract AllocateOnStack : stackKey -> term -> unit
266265

267266
abstract AllocateClass : Type -> term

‎VSharp.SILI/CILState.fs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -443,18 +443,18 @@ module CilState =
443443
Memory.ReadArrayIndexUnsafe x.ErrorReporter.Value x.state term index valueType
444444

445445
member x.Write ref value =
446-
let state = Memory.WriteUnsafe x.ErrorReporter.Value x.state ref value
446+
Memory.WriteUnsafe x.ErrorReporter.Value x.state ref value
447447
List.singleton x
448448

449449
member x.WriteClassField ref field value =
450-
let state = Memory.WriteClassFieldUnsafe x.ErrorReporter.Value x.state ref field value
450+
Memory.WriteClassFieldUnsafe x.ErrorReporter.Value x.state ref field value
451451
List.singleton x
452452

453453
member x.WriteStructField term field value =
454454
Memory.WriteStructFieldUnsafe x.ErrorReporter.Value x.state term field value
455455

456456
member x.WriteIndex term index value valueType =
457-
let state = Memory.WriteArrayIndexUnsafe x.ErrorReporter.Value x.state term index value valueType
457+
Memory.WriteArrayIndexUnsafe x.ErrorReporter.Value x.state term index value valueType
458458
List.singleton x
459459

460460
// -------------------------- Branching --------------------------

‎VSharp.SILI/Interpreter.fs‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,7 @@ module internal InstructionsSet =
210210
| Some this when argumentIndex = 0 -> this
211211
| Some _ -> getArgTerm (argumentIndex - 1) m
212212
let value = cilState.Pop()
213-
let state = Memory.Write cilState.state argTerm value
213+
Memory.Write cilState.state argTerm value
214214
List.singleton cilState
215215

216216
let brcommon condTransform (m : Method) (offset : offset) (cilState : cilState) =
@@ -433,7 +433,7 @@ module internal InstructionsSet =
433433
let this = cilState.Read this
434434
cilState.Push this
435435
cilState.PushMany args
436-
List.singleton cilState
436+
List.singleton cilState
437437
| Ptr(pointerBase, sightType, offset) ->
438438
match TryPtrToRef state pointerBase sightType offset with
439439
| Some(PrimitiveStackLocation _ as address) ->
@@ -445,7 +445,6 @@ module internal InstructionsSet =
445445
cilState.PushMany args
446446
List.singleton cilState
447447
| Ite {branches = branches; elseValue = e} ->
448-
// TODO fork on args if they are ITEs
449448
match branches with
450449
| [(g, v)] ->
451450
cilState.StatedConditionalExecutionCIL
@@ -479,7 +478,7 @@ module internal InstructionsSet =
479478
// In this case, next called static method will be called via type 'typ'
480479
assert(List.isEmpty cilState.prefixContext)
481480
cilState.PushPrefixContext (Constrained typ)
482-
[cilState]
481+
List.singleton cilState
483482
else
484483
let args = method.GetParameters().Length |> cilState.PopMany
485484
let thisForCallVirt = cilState.Pop()
@@ -653,7 +652,7 @@ type ILInterpreter() as this =
653652
let thisType = TypeOfLocation this
654653
if Types.IsValueType thisType && (method :> IMethod).IsConstructor then
655654
let newThis = Memory.DefaultOf thisType
656-
Memory.Write state this newThis |> ignore
655+
Memory.Write state this newThis
657656
| None -> ()
658657

659658
member private x.IsArrayGetOrSet (method : Method) =
@@ -827,7 +826,7 @@ type ILInterpreter() as this =
827826
match thisOption, thisObj with
828827
| Some thisRef, Some thisObj ->
829828
let structTerm = Memory.ObjectToTerm state thisObj declaringType
830-
Memory.Write state thisRef structTerm |> ignore
829+
Memory.Write state thisRef structTerm
831830
| _ -> __unreachable__()
832831
with :? TargetInvocationException as e ->
833832
let isRuntime = method.IsRuntimeException

‎VSharp.Test/Tests/Lists.cs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -569,7 +569,7 @@ public static int TestSolvingCopyOverwrittenValueUnreachable2(string[] a, int i,
569569
return 3;
570570
}
571571

572-
[Ignore("No match condition for range keys")]
572+
[TestSvm(94)]
573573
public static int TestSolvingCopy8(object[] a, object[] b, int i)
574574
{
575575
if (a.Length > b.Length && 0 <= i && i < b.Length)
@@ -644,6 +644,7 @@ public static int TestSolvingCopy11(string[] a, int i, string[] b)
644644
return 3;
645645
}
646646

647+
[TestSvm(90)]
647648
public static int ArrayAliasWrite(object[] o, string[] s, string str1, string str2)
648649
{
649650
if (o[42] == str1)
@@ -961,7 +962,7 @@ public static int IteKeyWrite(int i)
961962
return 1;
962963
}
963964

964-
[TestSvm(100)]
965+
[TestSvm(100)]
965966
public static int ListContains(int a, int b)
966967
{
967968
var l = new List<int> {2, 3, b, 5};

‎VSharp.Test/VSharp.Test.csproj‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,6 @@
3535

3636
<ItemGroup>
3737
<Folder Include="GeneratedTests" Condition="Exists('GeneratedTests')" />
38-
<Folder Include="GeneratedTests\" />
3938
</ItemGroup>
4039

4140
</Project>

0 commit comments

Comments
 (0)