Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Civl] Fix primitives #833

Merged
merged 1 commit into from
Jan 13, 2024
Merged

[Civl] Fix primitives #833

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
93 changes: 47 additions & 46 deletions Test/civl/samples/treiber-stack.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ type X; // module type parameter
var {:layer 4, 5} Stack: Map (RefTreiber X) (Vec X);
var {:layer 0, 4} ts: Lheap (Treiber X);

atomic action {:layer 5} AtomicTreiberAlloc() returns (loc_t: Lval (Loc (Treiber X)))
atomic action {:layer 5} AtomicAlloc() returns (loc_t: Lval (Loc (Treiber X)))
modifies Stack;
{
var ref_t: RefTreiber X;
Expand All @@ -18,13 +18,22 @@ modifies Stack;
assume !Map_Contains(Stack, ref_t);
Stack := Map_Update(Stack, ref_t, Vec_Empty());
}
yield procedure {:layer 4} TreiberAlloc() returns (loc_t: Lval (Loc (Treiber X)))
refines AtomicTreiberAlloc;
preserves call DomYieldInv#4();
yield procedure {:layer 4} Alloc() returns (loc_t: Lval (Loc (Treiber X)))
refines AtomicAlloc;
preserves call YieldInvDom#4();
{
var top: Ref (Node X);
var stack: Lheap (Node X);
var treiber: Treiber X;
var lmap_t: Lheap (Treiber X);
var ref_t: RefTreiber X;
call loc_t := Alloc#0();
top := Nil();
call stack := Lmap_Empty();
treiber := Treiber(top, stack);
call loc_t, lmap_t := Lmap_Alloc(treiber);
call {:layer 4} Lmap_Assume(lmap_t, ts);
ref_t := Ref(loc_t->val);
call AllocTreiber(lmap_t, ref_t);
call {:layer 4} Stack := Copy(Map_Update(Stack, ref_t, Vec_Empty()));
call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val);
}
Expand All @@ -40,7 +49,7 @@ yield procedure {:layer 4} Push(ref_t: RefTreiber X, x: X) returns (success: boo
refines AtomicPush;
preserves call YieldInv#2(ref_t);
preserves call YieldInv#4(ref_t);
preserves call DomYieldInv#4();
preserves call YieldInvDom#4();
{
var {:layer 4} old_top: RefNode X;
var {:layer 4} old_stack: Map (RefNode X) (Node X);
Expand Down Expand Up @@ -71,7 +80,7 @@ refines AtomicPop;
preserves call YieldInv#2(ref_t);
preserves call YieldInv#3(ref_t);
preserves call YieldInv#4(ref_t);
preserves call DomYieldInv#4();
preserves call YieldInvDom#4();
{
call {:layer 4} AbsLemma(ts->val->val[ref_t]->top, ts->val->val[ref_t]->stack->val);
call success, x := PopIntermediate(ref_t);
Expand Down Expand Up @@ -142,7 +151,7 @@ preserves call YieldInv#2(ref_t);
new_ref_n := Ref(new_loc_n->val);
call success := WriteTopOfStack(ref_t, ref_n, new_ref_n);
if (success) {
call AllocInStack(ref_t, new_ref_n, lmap_n);
call AllocNode(ref_t, new_ref_n, lmap_n);
}
}

Expand All @@ -168,14 +177,6 @@ refines AtomicReadTopOfStack#Push;
call ref_n := ReadTopOfStack(ref_t);
}

atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X)
{
assert Map_Contains(ts->val, ref_t);
ref_n := ts->val->val[ref_t]->top;
}
yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X);
refines AtomicReadTopOfStack;

right action {:layer 3} AtomicLoadNode(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X)
{
assert Map_Contains(ts->val, ref_t);
Expand All @@ -189,6 +190,27 @@ preserves call YieldInv#2(ref_t);
call node := LoadNode#0(ref_t, ref_n);
}

atomic action {:layer 3} AtomicWriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
{
assert NilDomain(ts, ref_t)[new_ref_n];
call r := AtomicWriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 2} WriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
refines AtomicWriteTopOfStack#Pop;
preserves call YieldInv#2(ref_t);
{
call r := WriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}

atomic action {:layer 1, 2} AtomicReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X)
{
assert Map_Contains(ts->val, ref_t);
ref_n := ts->val->val[ref_t]->top;
}
yield procedure {:layer 0} ReadTopOfStack(ref_t: RefTreiber X) returns (ref_n: RefNode X);
refines AtomicReadTopOfStack;

atomic action {:layer 1,2} AtomicLoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X)
{
assume Map_Contains(ts->val, ref_t);
Expand All @@ -198,29 +220,16 @@ atomic action {:layer 1,2} AtomicLoadNode#0(ref_t: RefTreiber X, ref_n: RefNode
yield procedure {:layer 0} LoadNode#0(ref_t: RefTreiber X, ref_n: RefNode X) returns (node: Node X);
refines AtomicLoadNode#0;

left action {:layer 1, 2} AtomicAllocInStack(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X))
left action {:layer 1, 2} AtomicAllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X))
modifies ts;
{
var lmap_n', lmap_n'': Lheap (Node X);
assert Map_Contains(ts->val, ref_t);
call lmap_n'', lmap_n' := Lmap_Move(lmap_n, ts->val->val[ref_t]->stack, ref_n);
ts->val->val[ref_t]->stack := lmap_n';
}
yield procedure {:layer 0} AllocInStack(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X));
refines AtomicAllocInStack;

atomic action {:layer 3} AtomicWriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
{
assert NilDomain(ts, ref_t)[new_ref_n];
call r := AtomicWriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 2} WriteTopOfStack#Pop(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
refines AtomicWriteTopOfStack#Pop;
preserves call YieldInv#2(ref_t);
{
call r := WriteTopOfStack(ref_t, old_ref_n, new_ref_n);
}
yield procedure {:layer 0} AllocNode(ref_t: RefTreiber X, ref_n: RefNode X, {:linear_in} lmap_n: Lheap (Node X));
refines AtomicAllocNode;

atomic action {:layer 1, 3} AtomicWriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool)
modifies ts;
Expand All @@ -239,22 +248,14 @@ modifies ts;
yield procedure {:layer 0} WriteTopOfStack(ref_t: RefTreiber X, old_ref_n: RefNode X, new_ref_n: RefNode X) returns (r: bool);
refines AtomicWriteTopOfStack;

atomic action {:layer 1, 4} AtomicAlloc#0() returns (loc_t: Lval (Loc (Treiber X)))
atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X)
modifies ts;
{
var top: Ref (Node X);
var stack: Lheap (Node X);
var treiber: Treiber X;
var lmap_t: Lheap (Treiber X);
top := Nil();
call stack := Lmap_Empty();
treiber := Treiber(top, stack);
call loc_t, lmap_t := Lmap_Alloc(treiber);
call Lmap_Assume(lmap_t, ts);
call lmap_t, ts := Lmap_Move(lmap_t, ts, Ref(loc_t->val));
var lmap_t': Lheap (Treiber X);
call lmap_t', ts := Lmap_Move(lmap_t, ts, ref_t);
}
yield procedure {:layer 0} Alloc#0() returns (loc_t: Lval (Loc (Treiber X)));
refines AtomicAlloc#0;
yield procedure {:layer 0} AllocTreiber({:linear_in} lmap_t: Lheap (Treiber X), ref_t: RefTreiber X);
refines AtomicAllocTreiber;

function {:inline} NilDomain(ts: Lheap (Treiber X), ref_t: RefTreiber X): [RefNode X]bool {
ts->val->val[ref_t]->stack->val->dom->val[Nil() := true]
Expand Down Expand Up @@ -322,5 +323,5 @@ invariant Map_At(Stack, ref_t) == (var t := ts->val->val[ref_t]; Abs(t->top, t->
invariant (var t := ts->val->val[ref_t]; Between(t->stack->val->val, t->top, t->top, Nil()));
invariant (var t := ts->val->val[ref_t]; IsSubset(BetweenSet(t->stack->val->val, t->top, Nil()), NilDomain(ts, ref_t)));

yield invariant {:layer 4} DomYieldInv#4();
yield invariant {:layer 4} YieldInvDom#4();
invariant Stack->dom == ts->val->dom;
Loading