[Civl] Eliminate type parameter of Loc (#954)

Source/Concurrency/CivlTypeChecker.cs

@@ -298,8 +298,8 @@ private void InlineAtomicActions(HashSet<ActionDecl> actionDecls)
     {
       var primitiveImpls = program.TopLevelDeclarations.OfType<Implementation>().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;

Source/Core/base.bpl

@@ -358,9 +358,9 @@ pure procedure {:inline 1} Map_Assume<K,V>({:linear} src: Map K V, {:linear} dst
   assume Set_IsDisjoint(src->dom, dst->dom);
 }
 
-type Loc _;
+type Loc;
 
-pure procedure {:inline 1} One_New<V>() 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;
 }

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,17 +316,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_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'));
     }
-}
+}

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
 

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