Skip to content

Commit c7f669e

Browse files
oveeernightoveeernight
committed
[fix] remove write branching; add guarded write
1 parent 93a9318 commit c7f669e

18 files changed

Lines changed: 202 additions & 199 deletions

File tree

‎VSharp.InternalCalls/ByReference.fs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,12 @@ module ByReference =
1818
assert(isValueField field)
1919
Memory.ReferenceField state this field
2020

21-
let internal ctor (state : state) (args : term list) : (term * state) list =
21+
let internal ctor (state : state) (args : term list) : term =
2222
assert(List.length args = 3)
2323
let this, ref = List.item 0 args, List.item 2 args
2424
let fieldRef = referenceValueField state this
25-
Memory.Write state fieldRef ref |> List.map (withFst (Nop()))
25+
Memory.Write state fieldRef ref
26+
Nop()
2627

2728
let internal getValue (state : state) (args : term list) : term =
2829
assert(List.length args = 2)

‎VSharp.InternalCalls/ByReference.fsi‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ module internal ByReference =
99
val isValueField : fieldId -> bool
1010

1111
[<Implements("System.Void System.ByReference`1[T]..ctor(this, T&)")>]
12-
val ctor : state -> term list -> (term * state) list
12+
val ctor : state -> term list -> term
1313

1414
[<Implements("T& System.ByReference`1[T].get_Value(this)")>]
1515
val getValue : state -> term list -> term

‎VSharp.InternalCalls/Enum.fs‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -68,12 +68,14 @@ module internal Enum =
6868
valuesList.Add(TypeUtils.convert v typeof<UInt64> :?> UInt64)
6969
let values = Memory.ObjectToTerm state (valuesList.ToArray()) typeof<UInt64[]>
7070
let valuesCase state k =
71-
Memory.Write state valuesPtr values |> k
71+
Memory.Write state valuesPtr values
72+
List.singleton state |> k
7273
let namesAndValuesCase state k =
7374
let names = Memory.ObjectToTerm state names typeof<string[]>
7475
let namesPtr = Memory.ReadField state namesRef refField
75-
let states = Memory.Write state valuesPtr values
76-
List.collect (fun state -> Memory.Write state namesPtr names) states |> k
76+
Memory.Write state valuesPtr values
77+
Memory.Write state namesPtr names
78+
List.singleton state |> k
7779
let needNames = (Types.Cast getNamesFlag typeof<int>) === (MakeNumber 1)
7880
StatedConditionalExecutionAppend state
7981
(fun state k -> k (needNames, state))

‎VSharp.InternalCalls/Environment.fs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,7 @@ module internal Environment =
3636
let dir = Memory.AllocateDefaultClass state t
3737
let fields = Reflection.fieldsOf false t
3838
let nameField = fields |> Array.find (fun (f, _) -> f.name = "_name") |> fst
39-
let states = Memory.WriteClassField state dir nameField name
40-
assert(List.length states = 1)
39+
Memory.WriteClassField state dir nameField name
4140
dir
4241

4342
let FileExists (_ : state) (args : term list) =

‎VSharp.InternalCalls/IntPtr.fs‎

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,21 +8,23 @@ open VSharp.Core
88

99
module IntPtr =
1010

11-
let private intPtrCtor (state : state) this term : (term * state) list =
11+
let private intPtrCtor (state : state) this term : term =
1212
let ptr = MakeIntPtr term
13-
Memory.Write state this ptr |> List.map (withFst (Nop()))
13+
Memory.Write state this ptr
14+
Nop()
15+
1416

15-
let internal intPtrCtorFromInt (state : state) (args : term list) : (term * state) list =
17+
let internal intPtrCtorFromInt (state : state) (args : term list) : term =
1618
assert(List.length args = 2)
1719
let this, intTerm = List.item 0 args, List.item 1 args
1820
intPtrCtor state this intTerm
1921

20-
let internal intPtrCtorFromPtr (state : state) (args : term list) : (term * state) list =
22+
let internal intPtrCtorFromPtr (state : state) (args : term list) : term =
2123
assert(List.length args = 2)
2224
let this, ptrTerm = List.item 0 args, List.item 1 args
2325
intPtrCtor state this ptrTerm
2426

25-
let internal intPtrCtorFromLong (state : state) (args : term list) : (term * state) list =
27+
let internal intPtrCtorFromLong (state : state) (args : term list) : term =
2628
assert(List.length args = 2)
2729
let this, intTerm = List.item 0 args, List.item 1 args
2830
intPtrCtor state this intTerm
@@ -37,21 +39,22 @@ module IntPtr =
3739

3840
module UIntPtr =
3941

40-
let private uintPtrCtor (state : state) this term : (term * state) list =
42+
let private uintPtrCtor (state : state) this term : term =
4143
let ptr = MakeUIntPtr term
42-
Memory.Write state this ptr |> List.map (withFst (Nop()))
44+
Memory.Write state this ptr
45+
Nop()
4346

44-
let internal uintPtrCtorFromUInt (state : state) (args : term list) : (term * state) list =
47+
let internal uintPtrCtorFromUInt (state : state) (args : term list) : term =
4548
assert(List.length args = 2)
4649
let this, intTerm = List.item 0 args, List.item 1 args
4750
uintPtrCtor state this intTerm
4851

49-
let internal uintPtrCtorFromPtr (state : state) (args : term list) : (term * state) list =
52+
let internal uintPtrCtorFromPtr (state : state) (args : term list) : term =
5053
assert(List.length args = 2)
5154
let this, ptrTerm = List.item 0 args, List.item 1 args
5255
uintPtrCtor state this ptrTerm
5356

54-
let internal uintPtrCtorFromULong (state : state) (args : term list) : (term * state) list =
57+
let internal uintPtrCtorFromULong (state : state) (args : term list) : term =
5558
assert(List.length args = 2)
5659
let this, intTerm = List.item 0 args, List.item 1 args
5760
uintPtrCtor state this intTerm

‎VSharp.InternalCalls/IntPtr.fsi‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,27 +7,27 @@ open VSharp.Core
77
module internal IntPtr =
88

99
[<Implements("System.Void System.IntPtr..ctor(this, System.Int32)")>]
10-
val intPtrCtorFromInt : state -> term list -> (term * state) list
10+
val intPtrCtorFromInt : state -> term list -> term
1111

1212
[<Implements("System.Void System.IntPtr..ctor(this, System.Void*)")>]
13-
val intPtrCtorFromPtr : state -> term list -> (term * state) list
13+
val intPtrCtorFromPtr : state -> term list -> term
1414

1515
[<Implements("System.Void System.IntPtr..ctor(this, System.Int64)")>]
16-
val intPtrCtorFromLong : state -> term list -> (term * state) list
16+
val intPtrCtorFromLong : state -> term list -> term
1717

1818
[<Implements("System.Void* System.IntPtr.ToPointer(this)")>]
1919
val intPtrToPointer : state -> term list -> term
2020

2121
module internal UIntPtr =
2222

2323
[<Implements("System.Void System.UIntPtr..ctor(this, System.UInt32)")>]
24-
val uintPtrCtorFromUInt : state -> term list -> (term * state) list
24+
val uintPtrCtorFromUInt : state -> term list -> term
2525

2626
[<Implements("System.Void System.UIntPtr..ctor(this, System.Void*)")>]
27-
val uintPtrCtorFromPtr : state -> term list -> (term * state) list
27+
val uintPtrCtorFromPtr : state -> term list -> term
2828

2929
[<Implements("System.Void System.UIntPtr..ctor(this, System.UInt64)")>]
30-
val uintPtrCtorFromULong : state -> term list -> (term * state) list
30+
val uintPtrCtorFromULong : state -> term list -> term
3131

3232
[<Implements("System.Void* System.UIntPtr.ToPointer(this)")>]
3333
val uintPtrToPointer : state -> term list -> term

‎VSharp.SILI.Core/API.fs‎

Lines changed: 15 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ module API =
4040
let GuardedApplyExpression term f = Merging.guardedApply f term
4141
let GuardedStatedApplyStatementK state term f k = Branching.guardedStatedApplyk f state term k
4242
let GuardedStatedApplyk f state term mergeStates k =
43-
Branching.commonGuardedStatedApplyk f state term false mergeStates k
43+
Branching.commonGuardedStatedApplyk f state term mergeStates k
4444

4545
let ReleaseBranches() = Branching.branchesReleased <- true
4646
let AcquireBranches() = Branching.branchesReleased <- false
@@ -81,10 +81,6 @@ module API =
8181
let Ptr baseAddress typ offset = Ptr baseAddress typ offset
8282
let HeapRef address baseType = HeapRef address baseType
8383
let Ite iteType = Ite iteType
84-
let ConditionFilter term condition =
85-
match term.term with
86-
| Ite iteType -> iteType.ConditionFilter condition |> Merging.merge
87-
| _ -> term
8884

8985
let True() = True()
9086
let False() = False()
@@ -543,20 +539,12 @@ module API =
543539

544540
let WriteStackLocation state location value = state.memory.WriteStackLocation location value
545541

546-
let Write state reference value =
547-
let write state reference =
548-
state.memory.Write emptyReporter (transformBoxedRef reference) value
549-
Branching.guardedStatedMap write state reference
542+
let Write state reference value = state.memory.Write emptyReporter reference value
543+
550544

551545
let WriteUnsafe (reporter : IErrorReporter) state reference value =
552-
let filteredRef =
553-
match reference.term with
554-
| Ite iteType -> iteType.filter (fun v -> True() <> IsBadRef v) |> Merging.merge
555-
| _ -> reference
556-
let write state reference =
557-
reporter.ConfigureState state
558-
state.memory.Write reporter reference value
559-
Branching.disjunctiveGuardedStatedMap write state filteredRef
546+
reporter.ConfigureState state
547+
state.memory.WriteUnsafe reporter reference value
560548

561549
let WriteStructField structure field value = writeStruct structure field value
562550

@@ -565,13 +553,17 @@ module API =
565553
writeStruct structure field value
566554

567555
let WriteClassFieldUnsafe (reporter : IErrorReporter) state reference field value =
568-
let write state reference =
569-
reporter.ConfigureState state
570-
match reference.term with
571-
| HeapRef(addr, _) -> state.memory.WriteClassField addr field value
556+
let extractAddress ref =
557+
match ref.term with
558+
| HeapRef(addr, _) -> addr
572559
| _ -> internalfail $"Writing field of class: expected reference, but got {reference}"
573-
state
574-
Branching.guardedStatedMap write state reference
560+
reporter.ConfigureState state
561+
match reference.term with
562+
| Ite iteType ->
563+
let filtered = iteType.filter (fun r -> Pointers.isBadRef r |> isTrue |> not)
564+
filtered.ToDisjunctiveGvs()
565+
|> List.iter (fun (g, r) -> state.memory.GuardedWriteClassField (Some g) (extractAddress r) field value)
566+
| _ -> state.memory.WriteClassField (extractAddress reference) field value
575567

576568
let WriteClassField state reference field value =
577569
WriteClassFieldUnsafe emptyReporter state reference field value

‎VSharp.SILI.Core/API.fsi‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,6 @@ module API =
5252
val Ptr : pointerBase -> Type -> term -> term
5353
val HeapRef : heapAddress -> Type -> term
5454
val Ite : iteType -> term
55-
val ConditionFilter : term -> term -> term
5655
val True : unit -> term
5756
val False : unit -> term
5857
val NullRef : Type -> term
@@ -295,14 +294,14 @@ module API =
295294

296295
val InitializeArray : state -> term -> term -> unit
297296

298-
val Write : state -> term -> term -> state list
299-
val WriteUnsafe : IErrorReporter -> state -> term -> term -> state list
297+
val Write : state -> term -> term -> unit
298+
val WriteUnsafe : IErrorReporter -> state -> term -> term -> unit
300299
val WriteStackLocation : state -> stackKey -> term -> unit
301300
val WriteStructField : term -> fieldId -> term -> term
302301
val WriteStructFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> term
303-
val WriteClassFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> state list
304-
val WriteClassField : state -> term -> fieldId -> term -> state list
305-
val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> state list
302+
val WriteClassFieldUnsafe : IErrorReporter -> state -> term -> fieldId -> term -> unit
303+
val WriteClassField : state -> term -> fieldId -> term -> unit
304+
val WriteArrayIndexUnsafe : IErrorReporter -> state -> term -> term list -> term -> Type option -> unit
306305
val WriteStaticField : state -> Type -> fieldId -> term -> unit
307306

308307
val DefaultOf : Type -> term

‎VSharp.SILI.Core/Branching.fs‎

Lines changed: 10 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -7,29 +7,23 @@ module internal Branching =
77

88
let checkSat state = SolverInteraction.checkSatWithSubtyping state
99

10-
let commonGuardedStatedApplyk f state term isDisjunctive mergeResults k =
10+
let commonGuardedStatedApplyk f state term mergeResults k =
1111
match term.term with
1212
| Ite iteType ->
13-
let refinedIteType, elseGuard = if isDisjunctive then iteType.ToDisjunctiveIte() else iteType, True()
1413
let filterUnsat (g, v) k =
1514
let pc' = PC.add state.pc g
1615
if PC.isFalse pc' then k None
17-
else Some (state.pc, v) |> k
18-
Cps.List.choosek filterUnsat refinedIteType.branches (fun pcs ->
19-
let copyState (pc, v) k = f (state.Copy pc) v k
20-
Cps.List.mapk copyState pcs (fun results ->
21-
let pc' = PC.add state.pc elseGuard
22-
state.pc <- pc'
23-
f state refinedIteType.elseValue (fun r ->
24-
r::results |> mergeResults |> k)))
16+
else Some (pc', v) |> k
17+
Cps.List.choosek filterUnsat iteType.branches (fun filteredBranches ->
18+
let statedApply (pc, v) k = f (state.Copy pc) v k
19+
Cps.List.mapk statedApply filteredBranches (fun appliedBranches ->
20+
f state iteType.elseValue (fun appliedElse ->
21+
appliedBranches @ [appliedElse] |> mergeResults |> k
22+
)))
2523
| _ -> f state term (List.singleton >> k)
26-
let guardedStatedApplyk f state term k = commonGuardedStatedApplyk f state term false State.mergeResults k
24+
let guardedStatedApplyk f state term k = commonGuardedStatedApplyk f state term State.mergeResults k
2725
let guardedStatedApply f state term = guardedStatedApplyk (Cps.ret2 f) state term id
28-
29-
let guardedStatedMap mapper state term =
30-
commonGuardedStatedApplyk (Cps.ret2 mapper) state term false id id
31-
let disjunctiveGuardedStatedMap mapper state term =
32-
commonGuardedStatedApplyk (Cps.ret2 mapper) state term true id id
26+
let guardedStatedMap mapper state term = commonGuardedStatedApplyk (Cps.ret2 mapper) state term id id
3327

3428
let mutable branchesReleased = false
3529

@@ -41,10 +35,6 @@ module internal Branching =
4135
merge2Results thenResult elseResult |> k))
4236
conditionInvocation state (fun (condition, conditionState) ->
4337
let pc = state.pc
44-
if PC.toSeq pc |> conjunction |> state.model.Eval |> isFalse then do
45-
let wrong = PC.toSeq pc |> List.ofSeq |> List.filter (fun x -> x |> state.model.Eval |> isTrue |> not)
46-
let p = PC.toSeq pc |> conjunction
47-
internalfail "21"
4838
assert(PC.toSeq pc |> conjunction |> state.model.Eval |> isTrue)
4939
let typeStorage = conditionState.typeStorage
5040
let evaled = state.model.Eval condition

0 commit comments

Comments
 (0)