From f7d003decfe54113208918965658cc162240925b Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sun, 29 Sep 2024 20:12:03 -0700 Subject: [PATCH] [Civl] Eliminate type parameter of Loc (#954) --- Source/Concurrency/CivlTypeChecker.cs | 4 +- Source/Core/base.bpl | 4 +- .../distributed-snapshot.bpl | 70 ++++++----- Test/civl/regression-tests/is2-attributes.bpl | 33 ------ .../is2-attributes.bpl.expect | 2 - .../pa-noninterference-check.bpl.expect | 2 +- ...ding-async-noninterference-fail.bpl.expect | 2 +- Test/civl/samples/treiber-stack.bpl | 110 +++++++++--------- Test/datatypes/node-client.bpl | 19 ++- 9 files changed, 110 insertions(+), 136 deletions(-) delete mode 100644 Test/civl/regression-tests/is2-attributes.bpl delete mode 100644 Test/civl/regression-tests/is2-attributes.bpl.expect diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index 56183e37b..e9da9ce8c 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -298,8 +298,8 @@ private void InlineAtomicActions(HashSet actionDecls) { var primitiveImpls = program.TopLevelDeclarations.OfType().Where(impl => { - var originalDecl = impl.Proc.OriginalDeclWithFormals; - return originalDecl != null && CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name); + var originalDecl = Monomorphizer.GetOriginalDecl(impl); + return CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name); }); primitiveImpls.ForEach(impl => { impl.OriginalBlocks = impl.Blocks; diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index 39fdd70d7..0f9b93fa4 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -358,9 +358,9 @@ pure procedure {:inline 1} Map_Assume({:linear} src: Map K V, {:linear} dst assume Set_IsDisjoint(src->dom, dst->dom); } -type Loc _; +type Loc; -pure procedure {:inline 1} One_New() returns ({:linear} {:pool "One_New"} l: One (Loc V)) +pure procedure {:inline 1} One_New() returns ({:linear} {:pool "One_New"} l: One Loc) { assume {:add_to_pool "One_New", l} true; } diff --git a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl index e5f822b8e..1fd91f61b 100644 --- a/Test/civl/inductive-sequentialization/distributed-snapshot.bpl +++ b/Test/civl/inductive-sequentialization/distributed-snapshot.bpl @@ -1,4 +1,4 @@ -// RUN: %parallel-boogie "%s" > "%t" +// RUN: %parallel-boogie /vcsSplitOnEveryAssert "%s" > "%t" // RUN: %diff "%s.expect" "%t" type Value; @@ -10,7 +10,7 @@ datatype StampedValue { } type Channel; // Send + Receive -type ChannelPiece = Fraction (Loc Channel) ChannelOp; // Send or Receive piece +type ChannelPiece = Fraction Loc ChannelOp; // Send or Receive piece type MemIndexPiece = Fraction ChannelPiece int; // Each mem index piece of Channel Piece type Snapshot = [int]StampedValue; @@ -37,53 +37,61 @@ function {:inline} IsSendSecond(piece: ChannelPiece): bool { piece == Fraction(piece->val, SendSecond(), ChannelOps()) } -function {:inline} ToReceive(loc_channel: Loc Channel): ChannelPiece { +function {:inline} ToReceive(loc_channel: Loc): ChannelPiece { Fraction(loc_channel, Receive(), ChannelOps()) } -function {:inline} ToSendFirst(loc_channel: Loc Channel): ChannelPiece { +function {:inline} ToSendFirst(loc_channel: Loc): ChannelPiece { Fraction(loc_channel, SendFirst(), ChannelOps()) } -function {:inline} ToSendSecond(loc_channel: Loc Channel): ChannelPiece { +function {:inline} ToSendSecond(loc_channel: Loc): ChannelPiece { Fraction(loc_channel, SendSecond(), ChannelOps()) } const NumMemIndices: int; axiom NumMemIndices >= 1; +const MemIndices: Set int; +axiom (forall x: int :: Set_Contains(MemIndices, x) <==> 1 <= x && x <= NumMemIndices); + function {:inline} MemIndexPieces(s: ChannelPiece, j: int): Set MemIndexPiece { - Set((lambda {:pool "MemIndexPieces"} x: MemIndexPiece :: x->val == s && x->ids == MemIndices() && 1 <= x->id && x->id <= j)) + Set((lambda {:pool "MemIndexPieces"} x: MemIndexPiece :: x->val == s && x->ids == MemIndices && 1 <= x->id && x->id <= j)) } function {:inline} AllMemIndexPieces(s: ChannelPiece): Set MemIndexPiece { MemIndexPieces(s, NumMemIndices) } -function {:inline} MemIndices(): Set int { - Set((lambda {:pool "MemIndices"} x: int :: 1 <= x && x <= NumMemIndices)) -} - function {:inline} IsValidMemIndexPiece(piece: MemIndexPiece): bool { Set_Contains(piece->ids, piece->id) && - piece->ids == MemIndices() + piece->ids == MemIndices } function {:inline} MemIndexPiece(cp: ChannelPiece, i: int): MemIndexPiece { - Fraction(cp, i, MemIndices()) + Fraction(cp, i, MemIndices) +} + +function {:inline} Read_f_asyncs(sps: Set MemIndexPiece): [read_f]bool { + (lambda {:pool "Read_PAs"} pa: read_f :: Set_Contains(sps, pa->perm->val)) +} + +function {:inline} Read_s_asyncs(sps: Set MemIndexPiece): [read_s]bool { + (lambda {:pool "Read_PAs"} pa: read_s :: Set_Contains(sps, pa->perm->val)) } var {:layer 0,3} mem: Snapshot; var {:linear} {:layer 0,2} pset: Map MemIndexPiece StampedValue; -atomic action {:layer 3} GetSnapshot({:linear_in} one_loc_channel: One (Loc Channel)) returns (snapshot: [int]StampedValue) +atomic action {:layer 3} GetSnapshot() returns (snapshot: [int]StampedValue) { assume (forall i:int :: 1 <= i && i <= NumMemIndices ==> snapshot[i] == mem[i]); } -yield procedure {:layer 2} Coordinator({:linear_in} one_loc_channel: One (Loc Channel)) returns (snapshot: [int]StampedValue) +yield procedure {:layer 2} Coordinator() returns (snapshot: [int]StampedValue) refines GetSnapshot; { + var {:linear} one_loc_channel: One Loc; var {:linear} channelOps: Set ChannelPiece; var {:linear} one_r: One ChannelPiece; var {:linear} one_s_first: One ChannelPiece; @@ -92,12 +100,13 @@ refines GetSnapshot; var {:linear} sps_second: Set MemIndexPiece; var snapshot': Snapshot; + call one_loc_channel := One_New(); call channelOps := One_To_Fractions(one_loc_channel, ChannelOps()); call one_r := One_Get(channelOps, ToReceive(one_loc_channel->val)); call one_s_first := One_Get(channelOps, ToSendFirst(one_loc_channel->val)); call one_s_second := One_Get(channelOps, ToSendSecond(one_loc_channel->val)); - call sps_first := One_To_Fractions(one_s_first, MemIndices()); - call sps_second := One_To_Fractions(one_s_second, MemIndices()); + call sps_first := One_To_Fractions(one_s_first, MemIndices); + call sps_second := One_To_Fractions(one_s_second, MemIndices); while (true) invariant {:yields} true; @@ -135,7 +144,7 @@ asserts Set_IsSubset(AllMemIndexPieces(s), pset->dom); call map := Map_Split(pset, AllMemIndexPieces(s)); call sps, data := Map_Unpack(map); - snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices())]); + snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices)]); } yield procedure {:layer 1} _ReceiveSecond({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot) refines ReceiveSecond; @@ -155,7 +164,7 @@ asserts IsSendFirst(s) || IsSendSecond(s); assume Set_IsSubset(AllMemIndexPieces(s), pset->dom); call map := Map_Split(pset, AllMemIndexPieces(s)); call sps, data := Map_Unpack(map); - snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices())]); + snapshot := (lambda x: int :: data[Fraction(s, x, MemIndices)]); } yield procedure {:layer 0} _ReceiveFirst({:linear} one_r: One ChannelPiece, s: ChannelPiece) returns ({:linear} sps: Set MemIndexPiece, snapshot: Snapshot); refines ReceiveFirst; @@ -179,7 +188,7 @@ asserts sps == AllMemIndexPieces(s); var {:linear} map: Map MemIndexPiece StampedValue; assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - assume (forall i: int :: 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); + assume (forall i: int :: {:add_to_pool "X", i} 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); call map := Map_Pack(sps, data); call Map_Join(pset, map); } @@ -193,7 +202,7 @@ asserts sps == AllMemIndexPieces(s); var data: [MemIndexPiece]StampedValue; assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - call {:linear sps} create_asyncs((lambda pa: read_f :: Set_Contains(sps, pa->perm->val))); + call {:linear sps} create_asyncs(Read_f_asyncs(sps)); } yield procedure {:layer 0} _main_f(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece); refines main_f; @@ -231,18 +240,18 @@ asserts sps == AllMemIndexPieces(s); var {:pool "Data"} data: [MemIndexPiece]StampedValue; assume {:add_to_pool "MemIndices", 0, j+1, NumMemIndices} {:add_to_pool "Data", data} 0 <= j && j <= NumMemIndices; - assume (forall i: int :: 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); - + assume (forall {:pool "X"} i: int :: {:add_to_pool "X", i} 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts < mem[i]->ts || data[x] == mem[i])); + assume {:add_to_pool "MemIndexPieces", Fraction(s, 1, MemIndices), Fraction(s, j+1, MemIndices), Fraction(s, NumMemIndices, MemIndices)} true; sps' := sps; call done_set := Set_Get(sps', MemIndexPieces(s, j)->val); call map := Map_Pack(done_set, data); call Map_Join(pset, map); if (j < NumMemIndices) { - choice := read_f(One(Fraction(s, j+1, MemIndices()))); + choice := read_f(One(Fraction(s, j+1, MemIndices))); call set_choice(choice); assume {:add_to_pool "Read_PAs", choice} true; - call {:linear sps'} create_asyncs((lambda {:pool "Read_PAs"} pa: read_f :: Set_Contains(sps', pa->perm->val))); + call {:linear sps'} create_asyncs((Read_f_asyncs(sps'))); } } @@ -257,7 +266,7 @@ asserts sps == AllMemIndexPieces(s); var {:linear} map: Map MemIndexPiece StampedValue; assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - assume (forall i: int :: 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); + assume (forall i: int :: {:add_to_pool "X", i} 1 <= i && i <= NumMemIndices ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); call map := Map_Pack(sps, data); call Map_Join(pset, map); } @@ -271,7 +280,7 @@ asserts sps == AllMemIndexPieces(s); var data: [MemIndexPiece]StampedValue; assume {:add_to_pool "MemIndices", 0, NumMemIndices} {:add_to_pool "Data", data} true; - call {:linear sps} create_asyncs((lambda pa: read_s :: Set_Contains(sps, pa->perm->val))); + call {:linear sps} create_asyncs(Read_s_asyncs(sps)); } yield procedure {:layer 0} _main_s(s: ChannelPiece, {:linear_in} sps: Set MemIndexPiece); refines main_s; @@ -307,7 +316,8 @@ asserts sps == AllMemIndexPieces(s); var {:pool "Data"} data: [MemIndexPiece]StampedValue; assume {:add_to_pool "MemIndices", 0, j+1, NumMemIndices} {:add_to_pool "Data", data} 0 <= j && j <= NumMemIndices; - assume (forall i: int :: 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); + assume (forall {:pool "X"} i: int :: {:add_to_pool "X", i} 1 <= i && i <= j ==> (var x := MemIndexPiece(s, i); data[x]->ts > mem[i]->ts || data[x] == mem[i])); + assume {:add_to_pool "MemIndexPieces", Fraction(s, 1, MemIndices), Fraction(s, j+1, MemIndices), Fraction(s, NumMemIndices, MemIndices)} true; sps' := sps; call done_set := Set_Get(sps', MemIndexPieces(s, j)->val); @@ -315,9 +325,9 @@ asserts sps == AllMemIndexPieces(s); call Map_Join(pset, map); if (j < NumMemIndices) { - choice := read_s(One(Fraction(s, j+1, MemIndices()))); + choice := read_s(One(Fraction(s, j+1, MemIndices))); call set_choice(choice); assume {:add_to_pool "Read_PAs", choice} true; - call {:linear sps'} create_asyncs((lambda {:pool "Read_PAs"} pa: read_s :: Set_Contains(sps', pa->perm->val))); + call {:linear sps'} create_asyncs(Read_s_asyncs(sps')); } -} \ No newline at end of file +} diff --git a/Test/civl/regression-tests/is2-attributes.bpl b/Test/civl/regression-tests/is2-attributes.bpl deleted file mode 100644 index 0bab41652..000000000 --- a/Test/civl/regression-tests/is2-attributes.bpl +++ /dev/null @@ -1,33 +0,0 @@ -// RUN: %parallel-boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// UNSUPPORTED: batch_mode - -// This is identical to "rec-IS1.bpl", -// but with the {:IS_right} attribute - -async left action {:layer 1} main_f''() -refines {:IS_right} final using Inv; -creates main_f''; -{ - if (*) { - } - else { - async call main_f''(); - } -} - -left action {:layer 2} final() -{ - -} - -action {:layer 1} Inv() -creates main_f''; -{ - if (*) { - } - else { - async call main_f''(); - call set_choice(main_f''()); - } -} \ No newline at end of file diff --git a/Test/civl/regression-tests/is2-attributes.bpl.expect b/Test/civl/regression-tests/is2-attributes.bpl.expect deleted file mode 100644 index c89aa63e6..000000000 --- a/Test/civl/regression-tests/is2-attributes.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 8 verified, 0 errors \ No newline at end of file diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect index f88e1245d..b97bf307f 100644 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect +++ b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect @@ -1,6 +1,6 @@ pa-noninterference-check.bpl(26,1): Error: Non-interference check failed Execution trace: - pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Entry + (0,0): init pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0 pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect index 49138df83..29a3c680e 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect +++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect @@ -1,6 +1,6 @@ pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed Execution trace: - pending-async-noninterference-fail.bpl(9,32): inline$A$0$Entry + (0,0): init pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0 pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl index 21340742e..5a164c949 100644 --- a/Test/civl/samples/treiber-stack.bpl +++ b/Test/civl/samples/treiber-stack.bpl @@ -7,39 +7,39 @@ function {:inline} AllLocPieces(): Set LocPiece { } type TreiberNode _; -type LocTreiberNode T = Fraction (Loc (TreiberNode T)) LocPiece; +type LocTreiberNode T = Fraction Loc LocPiece; type StackElem T = Node (LocTreiberNode T) T; type StackMap T = Map (LocTreiberNode T) (StackElem T); datatype Treiber { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) } type X; // module type parameter -var {:layer 4, 5} Stack: Map (Loc (Treiber X)) (Vec X); -var {:layer 0, 4} {:linear} ts: Map (Loc (Treiber X)) (Treiber X); +var {:layer 4, 5} Stack: Map Loc (Vec X); +var {:layer 0, 4} {:linear} ts: Map Loc (Treiber X); /// Yield invariants -function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) { +function {:inline} Domain(ts: Map Loc (Treiber X), loc_t: Loc): Set (LocTreiberNode X) { ts->val[loc_t]->stack->dom } yield invariant {:layer 1} Yield(); -yield invariant {:layer 2} TopInStack(loc_t: Loc (Treiber X)); +yield invariant {:layer 2} TopInStack(loc_t: Loc); invariant Map_Contains(ts, loc_t); invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); invariant (forall loc_n: LocTreiberNode X :: Set_Contains(Domain(ts, loc_t), loc_n) ==> (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); -yield invariant {:layer 2} LocInStackOrNone(loc_t: Loc (Treiber X), loc_n: Option (LocTreiberNode X)); +yield invariant {:layer 2} LocInStackOrNone(loc_t: Loc, loc_n: Option (LocTreiberNode X)); invariant Map_Contains(ts, loc_t); invariant loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); -yield invariant {:layer 3} LocInStack(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X); +yield invariant {:layer 3} LocInStack(loc_t: Loc, loc_n: LocTreiberNode X); invariant Map_Contains(ts, loc_t); invariant Set_Contains(Domain(ts, loc_t), loc_n); -yield invariant {:layer 4} ReachInStack(loc_t: Loc (Treiber X)); +yield invariant {:layer 4} ReachInStack(loc_t: Loc); invariant Map_Contains(ts, loc_t); invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); @@ -53,7 +53,7 @@ yield invariant {:layer 4} StackDom(); invariant Stack->dom == ts->dom; yield invariant {:layer 4} PushLocInStack( - loc_t: Loc (Treiber X), node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)); + loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)); invariant Map_Contains(ts, loc_t); invariant Set_Contains(Domain(ts, loc_t), new_loc_n); invariant right_loc_piece->val == Fraction(new_loc_n->val, Right(), AllLocPieces()); @@ -62,25 +62,25 @@ invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !Betw /// Layered implementation -atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc (Treiber X)) +atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc) modifies Stack; { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; call one_loc_t := One_New(); loc_t := one_loc_t->val; assume !Map_Contains(Stack, loc_t); Stack := Map_Update(Stack, loc_t, Vec_Empty()); } -yield procedure {:layer 4} Alloc() returns (loc_t: Loc (Treiber X)) +yield procedure {:layer 4} Alloc() returns (loc_t: Loc) refines AtomicAlloc; preserves call StackDom(); { var top: Option (LocTreiberNode X); var {:linear} stack: StackMap X; var {:linear} treiber: Treiber X; - var {:linear} one_loc_t: One (Loc (Treiber X)); - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} one_loc_t: One Loc; + var {:linear} cell_t: Cell Loc (Treiber X); top := None(); call stack := Map_MakeEmpty(); @@ -93,7 +93,7 @@ preserves call StackDom(); call {:layer 4} AbsLemma(treiber); } -atomic action {:layer 5} AtomicPush(loc_t: Loc (Treiber X), x: X) returns (success: bool) +atomic action {:layer 5} AtomicPush(loc_t: Loc, x: X) returns (success: bool) modifies Stack; { if (*) { @@ -103,7 +103,7 @@ modifies Stack; success := false; } } -yield procedure {:layer 4} Push(loc_t: Loc (Treiber X), x: X) returns (success: bool) +yield procedure {:layer 4} Push(loc_t: Loc, x: X) returns (success: bool) refines AtomicPush; preserves call TopInStack(loc_t); preserves call ReachInStack(loc_t); @@ -126,7 +126,7 @@ preserves call StackDom(); } } -atomic action {:layer 5} AtomicPop(loc_t: Loc (Treiber X)) returns (success: bool, x_opt: Option X) +atomic action {:layer 5} AtomicPop(loc_t: Loc) returns (success: bool, x_opt: Option X) modifies Stack; { var stack: Vec X; @@ -145,7 +145,7 @@ modifies Stack; x_opt := None(); } } -yield procedure {:layer 4} Pop(loc_t: Loc (Treiber X)) returns (success: bool, x_opt: Option X) +yield procedure {:layer 4} Pop(loc_t: Loc) returns (success: bool, x_opt: Option X) refines AtomicPop; preserves call TopInStack(loc_t); preserves call ReachInStack(loc_t); @@ -159,20 +159,20 @@ preserves call StackDom(); } } -atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc (Treiber X), x: X) +atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc, x: X) returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) modifies ts; asserts Map_Contains(ts, loc_t); { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; var top: Option (LocTreiberNode X); var {:linear} stack: StackMap X; - var {:linear} one_loc_n: One (Loc (TreiberNode X)); + var {:linear} one_loc_n: One Loc; var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); - var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); + var {:linear} cell_t: Cell Loc (Treiber X); + var {:linear} loc_pieces: Set (Fraction Loc LocPiece); + var {:linear} left_loc_piece: One (Fraction Loc LocPiece); call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); @@ -189,16 +189,16 @@ asserts Map_Contains(ts, loc_t); call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 3} AllocNode#3(loc_t: Loc (Treiber X), x: X) +yield procedure {:layer 3} AllocNode#3(loc_t: Loc, x: X) returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X)) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, Some(new_loc_n)); refines AtomicAllocNode#3; { - var {:linear} one_loc_n: One (Loc (TreiberNode X)); + var {:linear} one_loc_n: One Loc; var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X); - var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece); - var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece); + var {:linear} loc_pieces: Set (Fraction Loc LocPiece); + var {:linear} left_loc_piece: One (Fraction Loc LocPiece); call loc_n := ReadTopOfStack#Push(loc_t); call one_loc_n := One_New(); @@ -210,15 +210,15 @@ refines AtomicAllocNode#3; call AllocNode#0(loc_t, cell_n); } -atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x_opt: Option X) +atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) modifies ts; { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; var loc_n: Option (LocTreiberNode X); var {:linear} treiber: Treiber X; var top: Option (LocTreiberNode X); var {:linear} stack: StackMap X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} cell_t: Cell Loc (Treiber X); var x: X; assert Map_Contains(ts, loc_t); @@ -243,7 +243,7 @@ modifies ts; success := false; } } -yield procedure {:layer 3} PopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x_opt: Option X) +yield procedure {:layer 3} PopIntermediate(loc_t: Loc) returns (success: bool, x_opt: Option X) refines AtomicPopIntermediate; preserves call TopInStack(loc_t); { @@ -269,12 +269,12 @@ preserves call TopInStack(loc_t); } } -right action {:layer 3} AtomicReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +right action {:layer 3} AtomicReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) { assert Map_Contains(ts, loc_t); assume loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t); } -yield procedure {:layer 2} ReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +yield procedure {:layer 2} ReadTopOfStack#Push(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, loc_n); refines AtomicReadTopOfStack#Push; @@ -282,12 +282,12 @@ refines AtomicReadTopOfStack#Push; call loc_n := ReadTopOfStack#0(loc_t); } -atomic action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +atomic action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) { assert Map_Contains(ts, loc_t); assume if loc_n is None then Map_At(ts, loc_t)->top is None else Set_Contains(Domain(ts, loc_t), loc_n->t); } -yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) preserves call TopInStack(loc_t); ensures call LocInStackOrNone(loc_t, loc_n); refines AtomicReadTopOfStack#Pop; @@ -295,7 +295,7 @@ refines AtomicReadTopOfStack#Pop; call loc_n := ReadTopOfStack#0(loc_t); } -right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) +right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X) { assert Map_Contains(ts, loc_t); assert Map_Contains(Map_At(ts, loc_t)->stack, loc_n); @@ -304,13 +304,13 @@ right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc (Treiber X), loc_n: LocTre /// Primitives -atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X) +atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X) modifies ts; refines AtomicLoadNode#1; { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} cell_t: Cell Loc (Treiber X); var top: Option (LocTreiberNode X); var {:linear} stack: StackMap X; var {:linear} one_loc_n: One (LocTreiberNode X); @@ -327,15 +327,15 @@ refines AtomicLoadNode#1; call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} LoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X); +yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode X) returns (node: StackElem X); refines AtomicLoadNode#0; -atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)) +atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)) modifies ts; { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} cell_t: Cell Loc (Treiber X); call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); @@ -343,16 +343,16 @@ modifies ts; call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X)); +yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option (LocTreiberNode X)); refines AtomicReadTopOfStack#0; atomic action {:layer 1,4} AtomicWriteTopOfStack#0( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool) + loc_t: Loc, old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool) modifies ts; { var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} cell_t: Cell Loc (Treiber X); + var {:linear} one_loc_t: One Loc; call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); @@ -366,15 +366,15 @@ modifies ts; call Map_Put(ts, cell_t); } yield procedure {:layer 0} WriteTopOfStack#0( - loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool); + loc_t: Loc, old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool); refines AtomicWriteTopOfStack#0; -atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)) +atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)) modifies ts; { - var {:linear} one_loc_t: One (Loc (Treiber X)); + var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; - var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X); + var {:linear} cell_t: Cell Loc (Treiber X); call cell_t := Map_Get(ts, loc_t); call one_loc_t, treiber := Cell_Unpack(cell_t); @@ -382,15 +382,15 @@ modifies ts; call cell_t := Cell_Pack(one_loc_t, treiber); call Map_Put(ts, cell_t); } -yield procedure {:layer 0} AllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); +yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X)); refines AtomicAllocNode#0; -atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)) +atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} cell_t: Cell Loc (Treiber X)) modifies ts; { call Map_Put(ts, cell_t); } -yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X)); +yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell Loc (Treiber X)); refines AtomicAllocTreiber#0; /// Proof of abstraction with a manual encoding of termination diff --git a/Test/datatypes/node-client.bpl b/Test/datatypes/node-client.bpl index d50b33d4b..d177f9f90 100644 --- a/Test/datatypes/node-client.bpl +++ b/Test/datatypes/node-client.bpl @@ -2,15 +2,14 @@ // RUN: %diff "%s.expect" "%t" type TreiberNode _; -type LocTreiberNode T = Loc (TreiberNode T); -type StackElem T = Node (LocTreiberNode T) T; -type StackMap T = Map (LocTreiberNode T) (StackElem T); -datatype Treiber { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) } +type StackElem T = Node Loc T; +type StackMap T = Map Loc (StackElem T); +datatype Treiber { Treiber(top: Option Loc, {:linear} stack: StackMap T) } type X; -var ts: Map (Loc (Treiber X)) (Treiber X); +var ts: Map Loc (Treiber X); -procedure YieldInv(ref_t: Loc (Treiber X)) +procedure YieldInv(ref_t: Loc) requires Map_Contains(ts, ref_t); requires (var t := Map_At(ts, ref_t); Between(t->stack->val, t->top, None(), None())); requires (var t := Map_At(ts, ref_t); (var m := t->stack; IsSubset(BetweenSet(m->val, t->top, None()), m->dom->val))); @@ -24,11 +23,11 @@ modifies ts; call AtomicPushIntermediate(ref_t, x); } -procedure {:inline 1} AtomicPopIntermediate(loc_t: Loc (Treiber X)) returns (x: X) +procedure {:inline 1} AtomicPopIntermediate(loc_t: Loc) returns (x: X) modifies ts; { var treiber: Treiber X; - var loc_n_opt: Option (LocTreiberNode X); + var loc_n_opt: Option Loc; assert Map_Contains(ts, loc_t); treiber := Map_At(ts, loc_t); assume treiber->top is Some && Map_Contains(treiber->stack, treiber->top->t); @@ -37,11 +36,11 @@ modifies ts; ts := Map_Update(ts, loc_t, treiber); } -procedure {:inline 1} AtomicPushIntermediate(loc_t: Loc (Treiber X), x: X) +procedure {:inline 1} AtomicPushIntermediate(loc_t: Loc, x: X) modifies ts; { var treiber: Treiber X; - var loc_n: LocTreiberNode X; + var loc_n: Loc; assert Map_Contains(ts, loc_t); treiber := Map_At(ts, loc_t); assume !Map_Contains(treiber->stack, loc_n);