-
Notifications
You must be signed in to change notification settings - Fork 36
Expand file tree
/
Copy pathMemory.fs
More file actions
1620 lines (1415 loc) · 82.2 KB
/
Memory.fs
File metadata and controls
1620 lines (1415 loc) · 82.2 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
namespace VSharp.Core
open System
open System.Collections.Generic
open System.Text
open FSharpx.Collections
open VSharp
open VSharp.Core
open VSharp.TypeUtils
open VSharp.Utils
#nowarn "69"
type IMemoryAccessConstantSource =
inherit IStatedSymbolicConstantSource
module internal Memory =
// ------------------------------- Primitives -------------------------------
let makeEmpty complete = {
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 = ConcreteMemory()
allocatedTypes = PersistentDict.empty
typeVariables = (MappedStack.empty, Stack.empty)
delegates = PersistentDict.empty
currentTime = [1]
startingTime = VectorTime.zero
model = PrimitiveModel (Dictionary())
complete = complete
typeMocks = Dictionary<_,_>()
}
type memoryMode =
| ConcreteMemory
| SymbolicMemory
let mutable memoryMode = ConcreteMemory
let copy (state : state) newPc =
let cm = state.concreteMemory.Copy()
let newTypeMocks = Dictionary<_,_>()
state.typeMocks |> Seq.iter (fun kvp -> newTypeMocks.Add(kvp.Key, kvp.Value.Copy()))
{ state with pc = newPc; concreteMemory = cm }
let private isZeroAddress (x : concreteHeapAddress) =
x = VectorTime.zero
let addConstraint (s : state) cond =
s.pc <- PC.add s.pc cond
let delinearizeArrayIndex ind lens lbs =
let detachOne (acc, lens) lb =
let lensProd = List.fold mul (makeNumber 1) (List.tail lens)
let curOffset = div acc lensProd
let curIndex = add curOffset lb
let rest = rem acc lensProd
curIndex, (rest, List.tail lens)
List.mapFold detachOne (ind, lens) lbs |> fst
let linearizeArrayIndex (lens : term list) (lbs : term list) (indices : term list) =
let length = List.length indices
let attachOne acc i =
let relOffset = sub indices.[i] lbs.[i]
let prod acc j = mul acc lens.[j]
let lensProd = List.fold prod (makeNumber 1) [i .. length - 1]
let absOffset = mul relOffset lensProd
add acc absOffset
List.fold attachOne (makeNumber 0) [0 .. length - 1]
// ------------------------------- Stack -------------------------------
let newStackFrame (s : state) m frame =
let stack = CallStack.newStackFrame s.stack m frame
let evaluationStack = EvaluationStack.newStackFrame s.evaluationStack
s.stack <- stack
s.evaluationStack <- evaluationStack
let popFrame (s : state) =
let stack = CallStack.popFrame s.stack
let evaluationStack = EvaluationStack.popStackFrame s.evaluationStack
s.stack <- stack
s.evaluationStack <- evaluationStack
let forcePopFrames (count : int) (s : state) =
let stack = CallStack.popFrames s.stack count
let evaluationStack = EvaluationStack.forcePopStackFrames count s.evaluationStack
s.stack <- stack
s.evaluationStack <- evaluationStack
// ------------------------------- Types -------------------------------
let pushTypeVariablesSubstitution state subst =
assert (subst <> [])
let oldMappedStack, oldStack = state.typeVariables
let newStack = subst |> List.unzip |> fst |> Stack.push oldStack
let newMappedStack = subst |> List.fold (fun acc (k, v) -> MappedStack.push {t=k} v acc) oldMappedStack
state.typeVariables <- (newMappedStack, newStack)
let popTypeVariablesSubstitution state =
let oldMappedStack, oldStack = state.typeVariables
let toPop, newStack = Stack.pop oldStack
let newMappedStack = List.fold MappedStack.remove oldMappedStack (List.map (fun t -> {t=t}) toPop)
state.typeVariables <- (newMappedStack, newStack)
let commonTypeVariableSubst state (t : Type) noneCase =
match MappedStack.tryFind {t=t} (fst state.typeVariables) with
| Some typ -> typ
| None -> noneCase
let rec substituteTypeVariables (state : state) typ =
let substituteTypeVariables = substituteTypeVariables state
match typ with
| Bool
| AddressType
| Numeric _ -> typ
| StructType(t, args)
| ClassType(t, args)
| InterfaceType(t, args) ->
let args' = Array.map substituteTypeVariables args
if args = args' then typ
else
t.MakeGenericType args'
| TypeVariable t -> commonTypeVariableSubst state t typ
| ArrayType(t, dim) ->
let t' = substituteTypeVariables t
if t = t' then typ
else
match dim with
| Vector -> t'.MakeArrayType()
| ConcreteDimension d -> t'.MakeArrayType(d)
| SymbolicDimension -> __unreachable__()
| Pointer t ->
let t' = substituteTypeVariables t
if t = t' then typ else t'.MakePointerType()
| ByRef t ->
let t' = substituteTypeVariables t
if t = t' then typ else t'.MakeByRefType()
| _ -> __unreachable__()
let private substituteTypeVariablesIntoArrayType state ((et, i, b) : arrayType) : arrayType =
(substituteTypeVariables state et, i, b)
let typeVariableSubst state (t : Type) = commonTypeVariableSubst state t t
let private substituteTypeVariablesIntoField state (f : fieldId) =
Reflection.concretizeField f (typeVariableSubst state)
let private typeOfConcreteHeapAddress state address =
if address = VectorTime.zero then typeof<obj>
else
match PersistentDict.find state.allocatedTypes address with
| ConcreteType t -> t
| MockType _ -> __unreachable__() // Mock types may appear only in models
// TODO: use only mostConcreteTypeOfHeapRef someday
let rec typeOfHeapLocation state (address : heapAddress) =
let getTypeOfAddress = term >> function
| ConcreteHeapAddress address -> typeOfConcreteHeapAddress state address
| Constant(_, (:? IMemoryAccessConstantSource as source), AddressType) -> source.TypeOfLocation
| _ -> __unreachable__()
commonTypeOf getTypeOfAddress address
let mostConcreteTypeOfHeapRef state address sightType =
let locationType = typeOfHeapLocation state address
if isAssignable locationType sightType then locationType
else
if isAssignable sightType locationType |> not then
Logger.trace "mostConcreteTypeOfHeapRef: Sight type (%O) of address %O differs from type in heap (%O)" sightType address locationType
sightType
let baseTypeOfAddress state address =
match address with
| BoxedLocation(addr, _) -> typeOfConcreteHeapAddress state addr
| _ -> typeOfAddress address
// -------------------------------- GetHashCode --------------------------------
[<StructuralEquality;NoComparison>]
type private hashCodeSource =
{object : term}
interface IStatedSymbolicConstantSource with
override x.SubTerms = Seq.empty
override x.Time = VectorTime.zero
override x.TypeOfLocation = typeof<int32>
let hashConcreteAddress (address : concreteHeapAddress) =
address.GetHashCode() |> makeNumber
let getHashCode object =
assert(isReference object)
// TODO: implement GetHashCode() for value type (it's boxed)
match object.term with
| HeapRef({term = ConcreteHeapAddress address}, _) -> hashConcreteAddress address
| HeapRef(address, _) ->
let name = sprintf "HashCode(%O)" address
let source = {object = address}
Constant name source typeof<Int32>
| _ -> internalfailf "expected HeapRef, but got %O" object
// ------------------------------- Instantiation -------------------------------
[<CustomEquality;NoComparison>]
type regionPicker<'key, 'reg when 'key : equality and 'key :> IMemoryKey<'key, 'reg> and 'reg : equality and 'reg :> IRegion<'reg>> =
{sort : regionSort; extract : state -> memoryRegion<'key, 'reg>; mkname : 'key -> string; isDefaultKey : state -> 'key -> bool}
override x.Equals y =
match y with
| :? regionPicker<'key, 'reg> as y -> x.sort = y.sort
| _ -> false
override x.GetHashCode() = x.sort.GetHashCode()
[<StructuralEquality;NoComparison>]
type private stackReading =
{key : stackKey; time : vectorTime option}
interface IMemoryAccessConstantSource with
override x.SubTerms = Seq.empty
override x.Time =
match x.time with
| Some time -> time
| None -> internalfailf "Requesting time of primitive stack location %O" x.key
override x.TypeOfLocation = x.key.TypeOfLocation
[<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.Time = x.time
override x.TypeOfLocation = x.picker.sort.TypeOfLocation
let (|HeapReading|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapReading<heapAddressKey, vectorTime intervals> as hr -> Some(hr.key, hr.memoryObject)
| _ -> None
let (|ArrayIndexReading|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapReading<heapArrayIndexKey, productRegion<vectorTime intervals, int points listProductRegion>> as ar ->
Some(isConcreteHeapAddress ar.key.address, ar.key, ar.memoryObject)
| _ -> None
// VectorIndexKey is used for length and lower bounds
// We suppose, that lower bounds will always be default -- 0
let (|VectorIndexReading|_|) (src : ISymbolicConstantSource) =
let isLowerBoundKey = function
| ArrayLowerBoundSort _ -> true
| _ -> false
match src with
| :? heapReading<heapVectorIndexKey, productRegion<vectorTime intervals, int points>> as vr ->
Some(isConcreteHeapAddress vr.key.address || isLowerBoundKey vr.picker.sort, vr.key, vr.memoryObject)
| _ -> None
let (|StackBufferReading|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapReading<stackBufferIndexKey, int points> as sbr -> Some(sbr.key, sbr.memoryObject)
| _ -> None
let (|StaticsReading|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapReading<symbolicTypeKey, freeRegion<typeWrapper>> as sr -> Some(sr.key, sr.memoryObject)
| _ -> None
let getHeapReadingRegionSort (src : ISymbolicConstantSource) =
match src with
| :? heapReading<heapAddressKey, vectorTime intervals> as hr -> hr.picker.sort
| :? heapReading<heapArrayIndexKey, productRegion<vectorTime intervals, int points listProductRegion>> as hr -> hr.picker.sort
| :? heapReading<heapVectorIndexKey, productRegion<vectorTime intervals, int points>> as hr -> hr.picker.sort
| :? heapReading<stackBufferIndexKey, int points> as hr -> hr.picker.sort
| :? heapReading<symbolicTypeKey, freeRegion<typeWrapper>> as hr -> hr.picker.sort
| _ -> __unreachable__()
[<StructuralEquality;NoComparison>]
type private structField =
{baseSource : ISymbolicConstantSource; field : fieldId}
interface IMemoryAccessConstantSource with
override x.SubTerms = x.baseSource.SubTerms
override x.Time = x.baseSource.Time
override x.TypeOfLocation = x.field.typ
let (|StructFieldSource|_|) (src : ISymbolicConstantSource) =
match src with
| :? structField as sf -> Some(sf.baseSource, sf.field)
| _ -> None
[<StructuralEquality;NoComparison>]
type private heapAddressSource =
{baseSource : ISymbolicConstantSource}
interface IMemoryAccessConstantSource with
override x.SubTerms = x.baseSource.SubTerms
override x.Time = x.baseSource.Time
override x.TypeOfLocation = x.baseSource.TypeOfLocation
let (|HeapAddressSource|_|) (src : ISymbolicConstantSource) =
match src with
| :? heapAddressSource as heapAddress -> Some(heapAddress.baseSource)
| _ -> None
[<StructuralEquality;NoComparison>]
type private typeInitialized =
{typ : Type; matchingTypes : symbolicTypeSet}
interface IStatedSymbolicConstantSource with
override x.SubTerms = Seq.empty
override x.Time = VectorTime.zero
override x.TypeOfLocation = typeof<bool>
let (|TypeInitializedSource|_|) (src : IStatedSymbolicConstantSource) =
match src with
| :? typeInitialized as ti -> Some(ti.typ, ti.matchingTypes)
| _ -> None
let rec makeSymbolicValue (source : ISymbolicConstantSource) name typ =
match typ with
| Bool
| AddressType
| Numeric _ -> Constant name source typ
| StructType _ ->
let makeField _ field typ =
let fieldSource = {baseSource = source; field = field}
makeSymbolicValue fieldSource (toString field) typ
makeStruct false makeField typ
| ReferenceType ->
let addressSource : heapAddressSource = {baseSource = source}
let address = makeSymbolicValue addressSource name addressType
HeapRef address typ
| ValueType -> __insufficientInformation__ "Can't instantiate symbolic value of unknown value type %O" typ
| ByRef _ -> __insufficientInformation__ "Can't instantiate symbolic value of ByRef type %O" typ
| _ -> __insufficientInformation__ "Not sure which value to instantiate, because it's unknown if %O is a reference or a value type" typ
let private makeSymbolicStackRead key typ time =
let source = {key = key; time = time}
let name = toString key
makeSymbolicValue source name typ
let private makeSymbolicHeapRead picker key time typ memoryObject =
let source = {picker = picker; key = key; memoryObject = memoryObject; time = time}
let name = picker.mkname key
makeSymbolicValue source name typ
let makeSymbolicThis (m : IMethod) =
let declaringType = 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 fillModelWithParametersAndThis state (method : IMethod) =
let parameters = method.Parameters |> Seq.map (fun param ->
(ParameterKey param, None, param.ParameterType)) |> List.ofSeq
let parametersAndThis =
if method.HasThis then
let t = method.DeclaringType
let addr = [-1]
let thisRef = HeapRef (ConcreteHeapAddress addr) t
state.concreteMemory.Allocate addr (Reflection.createObject t) // TODO: do we need here protection from abstract types?
state.allocatedTypes <- PersistentDict.add addr (ConcreteType 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 None parametersAndThis
// -------------------------- Allocation helpers --------------------------
let freshAddress state =
state.currentTime <- VectorTime.advance state.currentTime
state.currentTime
let allocateType state (typ : Type) =
assert(not typ.IsAbstract)
let concreteAddress = freshAddress state
assert(not <| PersistentDict.contains concreteAddress state.allocatedTypes)
match state.model with
| PrimitiveModel _ ->
// try concrete allocation
let cm = state.concreteMemory
assert(not <| cm.Contains concreteAddress)
try
cm.Allocate concreteAddress (Reflection.createObject typ)
with
| _ -> ()
| _ -> ()
state.allocatedTypes <- PersistentDict.add concreteAddress (ConcreteType typ) state.allocatedTypes
concreteAddress
// =============== Marshalling/unmarshalling without state changing ===============
// ------------------ Object to term ------------------
let private allocateObjectIfNeed state (obj : obj) t =
assert(memoryMode = ConcreteMemory)
let cm = state.concreteMemory
let address =
match cm.TryPhysToVirt obj with
| Some address -> address
| None when obj = null -> VectorTime.zero
| None ->
let typ = mostConcreteType t (obj.GetType())
if typ.IsValueType then Logger.trace "allocateObjectIfNeed: boxing concrete struct %O" obj
let concreteAddress = allocateType state typ
cm.Allocate concreteAddress obj
concreteAddress
ConcreteHeapAddress address
let private referenceTypeToTerm state (obj : obj) t =
let address = allocateObjectIfNeed state obj t
let objType = typeOfHeapLocation state address
HeapRef address objType
let rec objToTerm (state : state) (t : Type) (obj : obj) =
match obj with
| _ when isNullable t -> nullableToTerm state t obj
| null -> nullRef t
| :? bool as b -> makeBool b
| _ when isNumeric t -> makeNumber obj
// TODO: need pointer?
| _ when isPointer t -> Concrete obj t
| _ when t.IsValueType -> structToTerm state obj t
| _ -> referenceTypeToTerm state obj t
and private structToTerm state (obj : obj) t =
let makeField (fieldInfo : Reflection.FieldInfo) _ _ =
fieldInfo.GetValue(obj) |> objToTerm state fieldInfo.FieldType
makeStruct false makeField t
and private nullableToTerm state t (obj : obj) =
let nullableType = Nullable.GetUnderlyingType t
let valueField, hasValueField = Reflection.fieldsOfNullable t
let value, hasValue =
if box obj <> null then objToTerm state nullableType obj, True
else objToTerm state nullableType (Reflection.createObject nullableType), False
let fields = PersistentDict.ofSeq <| seq [(valueField, value); (hasValueField, hasValue)]
Struct fields t
// ---------------- Try term to object ----------------
let tryAddressToObj (state : state) objCreate address (typ : Type) =
if address = VectorTime.zero then Some null
else
match state.concreteMemory.TryVirtToPhys address with
| Some o -> Some o
| None ->
objCreate address typ
state.concreteMemory.TryVirtToPhys address
let tryPointerToObj state address (offset : int) =
let cm = state.concreteMemory
match cm.TryVirtToPhys address with
| Some obj ->
let gch = Runtime.InteropServices.GCHandle.Alloc(obj, Runtime.InteropServices.GCHandleType.Pinned)
let pObj = gch.AddrOfPinnedObject() + (nativeint offset)
Some (pObj :> obj)
| None -> None
let rec tryTermToObj (state : state) objCreate term =
match term.term with
| Concrete(obj, _) -> Some obj
| Struct(fields, typ) when isNullable typ -> tryNullableTermToObj state objCreate fields typ
| Struct(fields, typ) when not typ.IsByRefLike -> tryStructTermToObj state objCreate fields typ
| HeapRef({term = ConcreteHeapAddress a}, typ) -> tryAddressToObj state objCreate a typ
| Ptr(HeapLocation({term = ConcreteHeapAddress a}, _), _, ConcreteT (:? int as offset, _)) ->
tryPointerToObj state a offset
| _ -> None
and tryStructTermToObj (state : state) objCreate fields typ =
let structObj = Reflection.createObject typ
let addField _ (fieldId, value) k =
let fieldInfo = Reflection.getFieldInfo fieldId
match tryTermToObj state objCreate value with
// field was not found in the structure, skipping it
| _ when fieldInfo = null -> k ()
// field can be converted to obj, so continue
| Some v -> fieldInfo.SetValue(structObj, v) |> k
// field can not be converted to obj, so break and return None
| None -> None
Cps.Seq.foldlk addField () (PersistentDict.toSeq fields) (fun _ -> Some structObj)
and tryNullableTermToObj (state : state) objCreate fields typ =
let valueField, hasValueField = Reflection.fieldsOfNullable typ
let value = PersistentDict.find fields valueField
let hasValue = PersistentDict.find fields hasValueField
match tryTermToObj state objCreate value with
| Some obj when hasValue = True -> Some obj
| _ when hasValue = False -> Some null
| _ -> None
// ------------------------------- Merging -------------------------------
let rec findCommonSuffix common pc1 pc2 =
match pc1, pc2 with
| [], [] -> [], [], common
| [], rest2 -> [], rest2, common
| rest1, [] -> rest1, [], common
| x :: xs, y :: ys when x = y -> findCommonSuffix (y :: common) xs ys
| _ -> pc1, pc2, common
let private merge2StatesInternal state1 state2 =
if state1.stack <> state2.stack then None
else
// TODO: implement it! See InterpreterBase::interpret::merge
None
let merge2States state1 state2 =
match merge2StatesInternal state1 state2 with
| Some state -> [state]
| None -> [state1; state2]
let merge2Results (term1 : term, state1) (term2, state2) =
match merge2StatesInternal state1 state2 with
| Some _ -> __notImplemented__()
| None -> [(term1, state1); (term2, state2)]
let mergeStates states =
// TODO: implement merging by calling merge2StatesInternal one-by-one for each state
states
let mergeResults (results : (term * state) list) =
// TODO
results
// ------------------------------- Safe reading -------------------------------
let private accessRegion (dict : pdict<'a, memoryRegion<'key, 'reg>>) key typ =
match PersistentDict.tryFind dict key with
| Some value -> value
| None -> MemoryRegion.empty typ
let rec extractAddress reference =
match reference.term with
| HeapRef(address, _) -> address
| Union gvs -> gvs |> List.map (fun (g, v) -> (g, extractAddress v)) |> Merging.merge
| _ -> internalfail "Extracting heap address: expected heap reference, but got %O" reference
let isConcreteHeapAddress = term >> function
| ConcreteHeapAddress _ -> true
| _ -> false
let private isHeapAddressDefault state address =
state.complete ||
match address.term with
| ConcreteHeapAddress address -> VectorTime.less state.startingTime address
| _ -> false
let readStackLocation (s : state) key =
let makeSymbolic typ =
if s.complete then makeDefaultValue typ
else
let time = if isValueType typ then None else Some s.startingTime
makeSymbolicStackRead key typ time
CallStack.readStackLocation s.stack key makeSymbolic
let readStruct (structTerm : term) (field : fieldId) =
match structTerm with
| { term = Struct(fields, _) } -> fields.[field]
| _ -> internalfailf "Reading field of structure: expected struct, but got %O" structTerm
let private readLowerBoundSymbolic (state : state) address dimension arrayType =
let extractor (state : state) = accessRegion state.lowerBounds (substituteTypeVariablesIntoArrayType state arrayType) lengthType
let mkname = fun (key : heapVectorIndexKey) -> sprintf "LowerBound(%O, %O)" key.address key.index
let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address || thd3 arrayType
let key = {address = address; index = dimension}
MemoryRegion.read (extractor state) key (isDefault state)
(makeSymbolicHeapRead {sort = ArrayLowerBoundSort arrayType; extract = extractor; mkname = mkname; isDefaultKey = isDefault} key state.startingTime)
let readLowerBound state address dimension arrayType =
let cm = state.concreteMemory
match address.term, dimension.term with
| ConcreteHeapAddress address, Concrete(:? int as dim, _) when cm.Contains address ->
cm.ReadArrayLowerBound address dim |> objToTerm state typeof<int>
| _ -> readLowerBoundSymbolic state address dimension arrayType
let private readLengthSymbolic state address dimension arrayType =
let extractor (state : state) = accessRegion state.lengths (substituteTypeVariablesIntoArrayType state arrayType) lengthType
let mkname = fun (key : heapVectorIndexKey) -> sprintf "Length(%O, %O)" key.address key.index
let isDefault state (key : heapVectorIndexKey) = isHeapAddressDefault state key.address
let key = {address = address; index = dimension}
MemoryRegion.read (extractor state) key (isDefault state)
(makeSymbolicHeapRead {sort = ArrayLengthSort arrayType; extract = extractor; mkname = mkname; isDefaultKey = isDefault} key state.startingTime)
let readLength state address dimension arrayType =
let cm = state.concreteMemory
match address.term, dimension.term with
| ConcreteHeapAddress address, Concrete(:? int as dim, _) when cm.Contains address ->
cm.ReadArrayLength address dim |> objToTerm state typeof<int>
| _ -> readLengthSymbolic state address dimension arrayType
let private readArrayRegion state arrayType extractor region address indices =
let key = {address = address; indices = indices}
let isDefault state (key : heapArrayIndexKey) = isHeapAddressDefault state key.address
let instantiate typ memory =
let mkname = fun (key : heapArrayIndexKey) -> sprintf "%O[%s]" key.address (List.map toString key.indices |> join ", ")
let picker = {sort = ArrayIndexSort arrayType; extract = extractor; mkname = mkname; isDefaultKey = isDefault}
let time =
if isValueType typ then state.startingTime
else MemoryRegion.maxTime region.updates state.startingTime
makeSymbolicHeapRead picker key time typ memory
MemoryRegion.read region key (isDefault state) instantiate
let private readArrayIndexSymbolic state address indices arrayType =
let extractor state = accessRegion state.arrays (substituteTypeVariablesIntoArrayType state arrayType) (fst3 arrayType)
readArrayRegion state arrayType extractor (extractor state) address indices
let private readSymbolicIndexFromConcreteArray state address arrayData indices arrayType =
let writeOneIndex mr (index, value) =
let key = {address = address; indices = List.map makeNumber index}
objToTerm state (value.GetType()) value |> MemoryRegion.write mr key
let region = arrayData |> Seq.fold writeOneIndex (MemoryRegion.empty (fst3 arrayType))
readArrayRegion state arrayType (always region) region address indices
let readArrayIndex state address indices arrayType =
let cm = state.concreteMemory
let concreteIndices = tryIntListFromTermList indices
match address.term, concreteIndices with
| ConcreteHeapAddress address, Some concreteIndices when cm.Contains address ->
cm.ReadArrayIndex address concreteIndices |> objToTerm state (fst3 arrayType)
| ConcreteHeapAddress concreteAddress, None when cm.Contains concreteAddress ->
let data = cm.GetAllArrayData concreteAddress
readSymbolicIndexFromConcreteArray state address data indices arrayType
| _ -> readArrayIndexSymbolic state address indices arrayType
let private readClassFieldSymbolic state address (field : fieldId) =
if field = Reflection.stringFirstCharField then
readArrayIndexSymbolic state address [makeNumber 0] (typeof<char>, 1, true)
else
let symbolicType = field.typ
let extractor state = accessRegion state.classFields (substituteTypeVariablesIntoField state field) (substituteTypeVariables state symbolicType)
let region = extractor state
let mkname = fun (key : heapAddressKey) -> sprintf "%O.%O" key.address field
let isDefault state (key : heapAddressKey) = isHeapAddressDefault state key.address
let key = {address = address}
let instantiate typ memory =
let picker = {sort = HeapFieldSort field; extract = extractor; mkname = mkname; isDefaultKey = isDefault}
let time =
if isValueType typ then state.startingTime
else MemoryRegion.maxTime region.updates state.startingTime
makeSymbolicHeapRead picker key time typ memory
MemoryRegion.read region key (isDefault state) instantiate
let readClassField (state : state) address (field : fieldId) =
let cm = state.concreteMemory
match address.term with
| ConcreteHeapAddress address when cm.Contains address ->
cm.ReadClassField address field |> objToTerm state field.typ
| _ -> readClassFieldSymbolic state address field
let readStaticField state typ (field : fieldId) =
let extractor state = accessRegion state.staticFields (substituteTypeVariablesIntoField state field) (substituteTypeVariables state field.typ)
let mkname = fun (key : symbolicTypeKey) -> sprintf "%O.%O" key.typ field
let isDefault _ _ = state.complete // TODO: when statics are allocated? always or never? depends on our exploration strategy
let key = {typ = typ}
MemoryRegion.read (extractor state) key (isDefault state)
(makeSymbolicHeapRead {sort = StaticFieldSort field; extract = extractor; mkname = mkname; isDefaultKey = isDefault} key state.startingTime)
let readStackBuffer state (stackKey : stackKey) index =
let extractor state = accessRegion state.stackBuffers (stackKey.Map (typeVariableSubst state)) typeof<int8>
let mkname = fun (key : stackBufferIndexKey) -> sprintf "%O[%O]" stackKey key.index
let isDefault _ _ = true
let key : stackBufferIndexKey = {index = index}
MemoryRegion.read (extractor state) key (isDefault state)
(makeSymbolicHeapRead {sort = StackBufferSort stackKey; extract = extractor; mkname = mkname; isDefaultKey = isDefault} key state.startingTime)
let readBoxedLocation state (address : concreteHeapAddress) =
let cm = state.concreteMemory
let typ = typeOfConcreteHeapAddress state address
match cm.TryVirtToPhys address, PersistentDict.tryFind state.boxedLocations address with
| Some value, _ -> objToTerm state typ value
| None, Some value -> value
| _ -> internalfailf "Boxed location %O was not found in heap: this should not happen!" address
let rec readDelegate state reference =
match reference.term with
| HeapRef(address, _) ->
match address.term with
| ConcreteHeapAddress address -> Some state.delegates.[address]
| _ -> None
| Union gvs ->
let delegates = gvs |> List.choose (fun (g, v) ->
Option.bind (fun d -> Some(g, d)) (readDelegate state v))
if delegates.Length = gvs.Length then delegates |> Merging.merge |> Some else None
| _ -> internalfailf "Reading delegate: expected heap reference, but got %O" reference
let rec private readSafe state = function
| PrimitiveStackLocation key -> readStackLocation state key
| ClassField(address, field) -> readClassField state address field
// [NOTE] ref must be the most concrete, otherwise region will be not found
| ArrayIndex(address, indices, typ) -> readArrayIndex state address indices typ
| StaticField(typ, field) -> readStaticField state typ field
| StructField(address, field) ->
let structTerm = readSafe state address
readStruct structTerm field
| ArrayLength(address, dimension, typ) -> readLength state address dimension typ
| BoxedLocation(address, _) -> readBoxedLocation state address
| StackBufferIndex(key, index) -> readStackBuffer state key index
| ArrayLowerBound(address, dimension, typ) -> readLowerBound state address dimension typ
let readArrayParams typ cha eval =
match typ with
| ArrayType(elemType, dim) ->
let arrayType, (lengths : int array), (lowerBounds : int array) =
match dim with
| Vector ->
let arrayType = (elemType, 1, true)
arrayType, [| ArrayLength(cha, makeNumber 0, arrayType) |> eval |], null
| ConcreteDimension rank ->
let arrayType = (elemType, rank, false)
arrayType,
Array.init rank (fun i -> ArrayLength(cha, makeNumber i, arrayType) |> eval),
Array.init rank (fun i -> ArrayLowerBound(cha, makeNumber i, arrayType) |> eval)
| SymbolicDimension -> __unreachable__()
arrayType, lengths, lowerBounds
| _ -> internalfail "reading array parameters for invalid type"
// ------------------------------- Unsafe reading -------------------------------
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)
reportError state failCondition
let private readAddressUnsafe address startByte endByte =
let size = sizeOf address
match startByte.term, endByte.term with
| Concrete(:? int as s, _), Concrete(:? int as e, _) when s = 0 && size = e -> List.singleton address
| _ -> sprintf "reading: reinterpreting %O" address |> undefinedBehaviour
// NOTE: returns list of slices
let rec private readTermUnsafe term startByte endByte =
match term.term with
| Struct(fields, t) -> readStructUnsafe fields t startByte endByte
| HeapRef _
| Ref _
| Ptr _ -> readAddressUnsafe term startByte endByte
| Concrete _
| Constant _
| Expression _ -> Slice term startByte endByte startByte |> List.singleton
| _ -> internalfailf "readTermUnsafe: unexpected term %O" term
and private readStructUnsafe fields structType startByte endByte =
let readField fieldId = fields.[fieldId]
readFieldsUnsafe (makeEmpty false) (fun _ -> __unreachable__()) readField false structType startByte endByte
and private getAffectedFields state reportError readField isStatic (blockType : Type) startByte endByte =
let blockSize = CSharpUtils.LayoutUtils.ClassSize blockType
if isValueType blockType |> not then checkBlockBounds state reportError (makeNumber blockSize) startByte endByte
let fields = Reflection.fieldsOf isStatic blockType
let getOffsetAndSize (fieldId, fieldInfo : Reflection.FieldInfo) =
fieldId, CSharpUtils.LayoutUtils.GetFieldOffset fieldInfo, internalSizeOf fieldInfo.FieldType
let fieldIntervals = Array.map getOffsetAndSize fields |> Array.sortBy snd3
let betweenField = {name = ""; declaringType = blockType; typ = typeof<byte>}
let addZerosBetween (_, offset, size as field) (allFields, nextOffset) =
let curEnd = offset + size
let between = nextOffset - curEnd
// TODO: add there is enough space, insert short, int or long
let zeros = if between > 0 then List.init between (fun i -> betweenField, curEnd + i, 1) else List.empty
let fieldsWithZeros = List.foldBack (fun zero fields -> zero :: fields) zeros allFields
field :: fieldsWithZeros, offset
let fieldsWithZeros, fstOffset = Array.foldBack addZerosBetween fieldIntervals (List.empty, blockSize)
let zeros = if fstOffset > 0 then List.init fstOffset (fun i -> betweenField, i, 1) else List.empty
let allFields = List.foldBack (fun zero fields -> zero :: fields) zeros fieldsWithZeros
let readFieldOrZero fieldId =
if fieldId.name = "" then makeDefaultValue fieldId.typ
else readField fieldId
let getField (fieldId, fieldOffset, _) =
let fieldValue = readFieldOrZero fieldId
let fieldOffset = makeNumber fieldOffset
let startByte = sub startByte fieldOffset
let endByte = sub endByte fieldOffset
fieldId, fieldValue, startByte, endByte
match startByte.term, endByte.term with
| Concrete(:? int as s, _), Concrete(:? int as e, _) ->
let concreteGetField (_, fieldOffset, fieldSize as field) affectedFields =
if (e > fieldOffset && s < fieldOffset + fieldSize) then
getField field :: affectedFields
else affectedFields
List.foldBack concreteGetField allFields List.empty
| _ -> List.map getField allFields
and private readFieldsUnsafe state reportError readField isStatic (blockType : Type) startByte endByte =
let affectedFields = getAffectedFields state reportError readField isStatic blockType startByte endByte
List.collect (fun (_, v, s, e) -> readTermUnsafe v s e) affectedFields
// TODO: Add undefined behaviour:
// TODO: 1. when reading info between fields
// TODO: 3. when reading info outside block
// TODO: 3. reinterpreting ref or ptr should return symbolic ref or ptr
let private readClassUnsafe state reportError address classType offset (viewSize : int) =
let endByte = makeNumber viewSize |> add offset
let readField fieldId = readClassField state address fieldId
readFieldsUnsafe state reportError readField false classType offset endByte
let arrayIndicesToOffset state address (elementType, dim, _ as arrayType) indices =
let lens = List.init dim (fun dim -> readLength state address (makeNumber dim) arrayType)
let lbs = List.init dim (fun dim -> readLowerBound state address (makeNumber dim) arrayType)
let linearIndex = linearizeArrayIndex lens lbs indices
mul linearIndex (internalSizeOf elementType |> makeNumber)
let private getAffectedIndices state reportError address (elementType, dim, _ as arrayType) offset viewSize =
let concreteElementSize = internalSizeOf elementType
let elementSize = makeNumber concreteElementSize
let lens = List.init dim (fun dim -> readLength state address (makeNumber dim) arrayType)
let lbs = List.init dim (fun dim -> readLowerBound state address (makeNumber dim) arrayType)
let arraySize = List.fold mul elementSize lens
checkBlockBounds state reportError arraySize offset (makeNumber viewSize |> add offset)
let firstElement = div offset elementSize
let elementOffset = rem offset elementSize
let countToRead =
match elementOffset.term with
| Concrete(:? int as i, _) when (i + viewSize) % concreteElementSize = 0 -> (i + viewSize) / concreteElementSize
// NOTE: if offset inside element > 0 then one more element is needed
| _ -> (viewSize / concreteElementSize) + 1
let getElement currentOffset i =
let linearIndex = makeNumber i |> add firstElement
let indices = delinearizeArrayIndex linearIndex lens lbs
let element = readArrayIndex state address indices arrayType
let startByte = sub offset currentOffset
let endByte = makeNumber viewSize |> add startByte
(indices, element, startByte, endByte), add currentOffset elementSize
List.mapFold getElement (mul firstElement elementSize) [0 .. countToRead - 1] |> fst
let private readArrayUnsafe state reportError address arrayType offset viewSize =
let indices = getAffectedIndices state reportError address (symbolicTypeToArrayType arrayType) offset viewSize
List.collect (fun (_, elem, s, e) -> readTermUnsafe elem s e) indices
let private readStringUnsafe state reportError address offset viewSize =
// TODO: handle case, when reading string length
let indices = getAffectedIndices state reportError address (typeof<char>, 1, true) offset viewSize
List.collect (fun (_, elem, s, e) -> readTermUnsafe elem s e) indices
let private readStaticUnsafe state reportError t offset (viewSize : int) =
let endByte = makeNumber viewSize |> add offset
let readField fieldId = readStaticField state t fieldId
readFieldsUnsafe state reportError readField true t offset endByte
let private readStackUnsafe state reportError loc offset (viewSize : int) =
let term = readStackLocation state loc
let locSize = sizeOf term |> makeNumber
let endByte = makeNumber viewSize |> add offset
checkBlockBounds state reportError locSize offset endByte
readTermUnsafe term offset endByte
let private readBoxedStructUnsafe state loc typ offset viewSize =
let address =
match loc.term with
| ConcreteHeapAddress address -> BoxedLocation(address, typ)
| _ -> internalfail "readUnsafe: struct case is not fully implemented"
let fields =
match readSafe state address with
| {term = Struct(fields, _)} -> fields
| term -> internalfailf "readUnsafe: reading struct resulted in term %O" term
let endByte = makeNumber viewSize |> add offset
readStructUnsafe fields typ offset endByte
let private readUnsafe state reportError baseAddress offset sightType =
let viewSize = internalSizeOf sightType
let slices =
match baseAddress with
| HeapLocation(loc, sightType) ->
let typ = mostConcreteTypeOfHeapRef state loc sightType
match typ with
| StringType -> readStringUnsafe state reportError loc offset viewSize
| ClassType _ -> readClassUnsafe state reportError loc typ offset viewSize
| ArrayType _ -> readArrayUnsafe state reportError loc typ offset viewSize
| StructType _ -> readBoxedStructUnsafe state loc typ offset viewSize
| _ -> internalfailf "expected complex type, but got %O" typ
| StackLocation loc -> readStackUnsafe state reportError loc offset viewSize
| StaticLocation loc -> readStaticUnsafe state reportError loc offset viewSize
combine slices sightType
// --------------------------- General reading ---------------------------
let isTypeInitialized state (typ : Type) =
let key : symbolicTypeKey = {typ=typ}
let matchingTypes = SymbolicSet.matchingElements key state.initializedTypes
match matchingTypes with
| [x] when x = key -> True
| _ ->
let name = sprintf "%O_initialized" typ
let source : typeInitialized = {typ = typ; matchingTypes = SymbolicSet.ofSeq matchingTypes}
Constant name source typeof<bool>
// TODO: take type of heap address
let rec read state reportError reference =
match reference.term with
| Ref address -> readSafe state address
| Ptr(baseAddress, sightType, offset) -> readUnsafe state reportError baseAddress offset sightType
| Union gvs -> gvs |> List.map (fun (g, v) -> (g, read state reportError v)) |> Merging.merge
| _ -> internalfailf "Safe reading: expected reference, but got %O" reference
// ------------------------------- Writing -------------------------------
let rec private ensureConcreteType typ =
if isOpenType typ then __insufficientInformation__ "Cannot write value of generic type %O" typ
let writeStackLocation (s : state) key value =
s.stack <- CallStack.writeStackLocation s.stack key value
let writeStruct (structTerm : term) (field : fieldId) value =
match structTerm with
| { term = Struct(fields, typ) } -> Struct (PersistentDict.add field value fields) typ
| _ -> internalfailf "Writing field of structure: expected struct, but got %O" structTerm
let private writeClassFieldSymbolic state address (field : fieldId) value =
ensureConcreteType field.typ
let mr = accessRegion state.classFields field field.typ
let key = {address = address}
let mr' = MemoryRegion.write mr key value
state.classFields <- PersistentDict.add field mr' state.classFields
let private writeArrayIndexSymbolic state address indices arrayType value =
let elementType = fst3 arrayType
ensureConcreteType elementType
let mr = accessRegion state.arrays arrayType elementType
let key = {address = address; indices = indices}
let mr' = MemoryRegion.write mr key value
state.arrays <- PersistentDict.add arrayType mr' state.arrays
let initializeArray state address indicesAndValues arrayType =
let elementType = fst3 arrayType
ensureConcreteType elementType
let mr = accessRegion state.arrays arrayType elementType
let keysAndValues = Seq.map (fun (i, v) -> {address = address; indices = i}, v) indicesAndValues
let mr' = MemoryRegion.memset mr keysAndValues
state.arrays <- PersistentDict.add arrayType mr' state.arrays
let writeStaticField state typ (field : fieldId) value =
ensureConcreteType field.typ
let mr = accessRegion state.staticFields field field.typ
let key = {typ = typ}
let mr' = MemoryRegion.write mr key value
state.staticFields <- PersistentDict.add field mr' state.staticFields
let private writeLowerBoundSymbolic (state : state) address dimension arrayType value =
ensureConcreteType (fst3 arrayType)
let mr = accessRegion state.lowerBounds arrayType lengthType
let key = {address = address; index = dimension}
let mr' = MemoryRegion.write mr key value
state.lowerBounds <- PersistentDict.add arrayType mr' state.lowerBounds
let writeLengthSymbolic (state : state) address dimension arrayType value =
ensureConcreteType (fst3 arrayType)
let mr = accessRegion state.lengths arrayType lengthType
let key = {address = address; index = dimension}
let mr' = MemoryRegion.write mr key value
state.lengths <- PersistentDict.add arrayType mr' state.lengths
let private fillArrayBoundsSymbolic state address lengths lowerBounds arrayType =
let d = List.length lengths
assert(d = snd3 arrayType)
assert(List.length lowerBounds = d)
let writeLengths state l i = writeLengthSymbolic state address (Concrete i lengthType) arrayType l
let writeLowerBounds state l i = writeLowerBoundSymbolic state address (Concrete i lengthType) arrayType l
List.iter2 (writeLengths state) lengths [0 .. d-1]
List.iter2 (writeLowerBounds state) lowerBounds [0 .. d-1]
let writeStackBuffer state stackKey index value =
let mr = accessRegion state.stackBuffers stackKey typeof<int8>
let key : stackBufferIndexKey = {index = index}
let mr' = MemoryRegion.write mr key value
state.stackBuffers <- PersistentDict.add stackKey mr' state.stackBuffers
let writeBoxedLocationSymbolic state (address : concreteHeapAddress) value =
state.boxedLocations <- PersistentDict.add address value state.boxedLocations
let writeBoxedLocation state (address : concreteHeapAddress) value =
let cm = state.concreteMemory
match tryTermToObj state (fun _ _ -> ()) value with
| Some value when cm.Contains(address) ->
cm.Remove address
cm.Allocate address value
| _ -> writeBoxedLocationSymbolic state address value
// ----------------- Unmarshalling: from concrete to symbolic memory -----------------
let private unmarshallClass (state : state) address obj =
let writeField state (fieldId, fieldInfo : Reflection.FieldInfo) =
let value = fieldInfo.GetValue obj |> objToTerm state fieldInfo.FieldType
writeClassFieldSymbolic state address fieldId value
let fields = obj.GetType() |> Reflection.fieldsOf false
Array.iter (writeField state) fields
let private unmarshallArray (state : state) address (array : Array) =
let elemType, dim, _ as arrayType = array.GetType() |> symbolicTypeToArrayType
let lbs = List.init dim array.GetLowerBound
let lens = List.init dim array.GetLength
let writeIndex state (indices : int list) =
let value = array.GetValue(Array.ofList indices) |> objToTerm state elemType
let termIndices = List.map makeNumber indices
writeArrayIndexSymbolic state address termIndices arrayType value
let allIndices = Array.allIndicesOfArray lbs lens
Seq.iter (writeIndex state) allIndices
let termLBs = List.map (objToTerm state typeof<int>) lbs
let termLens = List.map (objToTerm state typeof<int>) lens
fillArrayBoundsSymbolic state address termLens termLBs arrayType