[Civl] Add type param to Loc (#1031)

Author: shazqadeer

Source/Core/base.bpl

@@ -329,19 +329,19 @@ pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} l: One K, {:li
 pure procedure Map_GetValue<K,V>({:linear} path: Map K V, k: K) returns ({:linear} v: V);
 pure procedure Map_PutValue<K,V>({:linear} path: Map K V, k: K, {:linear_in} v: V);
 
-type Loc;
+type Loc _;
 
-pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One Loc)
+pure procedure {:inline 1} Loc_New<V>() returns ({:linear} {:pool "Loc_New"} l: One (Loc V))
 {
   assume {:add_to_pool "Loc_New", l} true;
 }
 
-datatype TaggedLoc<K> { TaggedLoc(loc: Loc, tag: K) }
+datatype TaggedLoc<V,T> { TaggedLoc(loc: Loc V, tag: T) }
 
-pure procedure {:inline 1} TaggedLocSet_New<K>(ks: Set K) returns ({:linear} {:pool "Loc_New"} l: One Loc, {:linear} tagged_locs: Set (TaggedLoc K))
+pure procedure {:inline 1} TaggedLocSet_New<V,T>(tags: Set T) returns ({:linear} {:pool "Loc_New"} l: One (Loc V), {:linear} tagged_locs: Set (TaggedLoc V T))
 {
   assume {:add_to_pool "Loc_New", l} true;
-  tagged_locs := Set((lambda x: TaggedLoc K :: x->loc == l->val && Set_Contains(ks, x->tag)));
+  tagged_locs := Set((lambda x: TaggedLoc V T :: x->loc == l->val && Set_Contains(tags, x->tag)));
 }
 
 procedure create_async<T>(PA: T);

Source/Core/node.bpl

@@ -1,76 +1,77 @@
-datatype Node<K,T> { Node(next: Option K, val: T) }
+datatype Node<T> { Node(next: Option (Loc (Node T)), val: T) }
+type LocNode T = Loc (Node T);
 
-function Between<K,T>(f: [K]Node K T, x: Option K, y: Option K, z: Option K): bool;
-function Avoiding<K,T>(f: [K]Node K T, x: Option K, y: Option K, z: Option K): bool;
-function {:inline} BetweenSet<K,T>(f:[K]Node K T, x: Option K, z: Option K): [K]bool
+function Between<T>(f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T))): bool;
+function Avoiding<T>(f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T))): bool;
+function {:inline} BetweenSet<T>(f:[Loc (Node T)]Node T, x: Option (Loc (Node T)), z: Option (Loc (Node T))): [Loc (Node T)]bool
 {
-  (lambda y: K :: Between(f, x, Some(y), z))
+  (lambda y: Loc (Node T) :: Between(f, x, Some(y), z))
 }
 
 // reflexive
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K :: Between(f, x, x, x));
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)) :: Between(f, x, x, x));
 
 // step
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T) ::
   {f[x]} 
   Between(f, Some(x), f[x]->next, f[x]->next));
 
 // reach
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T), y: Option (Loc (Node T)) ::
   {f[x], Between(f, Some(x), y, y)} 
   Between(f, Some(x), y, y) ==> Some(x) == y || Between(f, Some(x), f[x]->next, y));
 
 // cycle
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T), y: Option (Loc (Node T)) ::
   {f[x], Between(f, Some(x), y, y)} 
   f[x]->next == Some(x) && Between(f, Some(x), y, y) ==> Some(x) == y);
 
 // sandwich
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)) ::
   {Between(f, x, y, x)} 
   Between(f, x, y, x) ==> x == y);
 
 // order1
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, y), Between(f, x, z, z)} 
   Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y));
 
 // order2
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, z)} 
   Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z));
 
 // transitive1
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, y), Between(f, y, z, z)} 
   Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z));
 
 // transitive2
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K, w: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)), w: Option (Loc (Node T)) ::
   {Between(f, x, y, z), Between(f, y, w, z)} 
   Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z));
 
 // transitive3
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K, w: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)), w: Option (Loc (Node T)) ::
   {Between(f, x, y, z), Between(f, x, w, y)} 
   Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z));
 
 // This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.
 // It cannot be proved using the rest of the axioms.
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, u: Option K, x: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, u: Option (Loc (Node T)), x: Option (Loc (Node T)) ::
   {Between(f, u, x, x)} 
   Between(f, u, x, x) ==> Between(f, u, u, x));
 
 // relation between Avoiding and Between
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Avoiding(f, x, y, z)} 
   Avoiding(f, x, y, z) <==> Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z)));
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, z)} 
   Between(f, x, y, z) <==> Avoiding(f, x, y, z) && Avoiding(f, x, z, z));
 
 // update
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, u: Option K, v: Option K, x: Option K, p: K, q: Node K T :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, u: Option (Loc (Node T)), v: Option (Loc (Node T)), x: Option (Loc (Node T)), p: Loc (Node T), q: Node T ::
   {Avoiding(f[p := q], u, v, x)} 
   Avoiding(f[p := q], u, v, x) <==>
     (Avoiding(f, u, v, Some(p)) && Avoiding(f, u, v, x)) || 

Test/civl/large-samples/GC.bpl

@@ -2,7 +2,7 @@
 // Copyright (c) Microsoft Corporation.  All rights reserved.
 //
 
-// RUN: %parallel-boogie -lib:set_size "%s" > "%t"
+// RUN: %parallel-boogie -lib:set_size -timeLimit:0 -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Tid(i, ps) represents a linear thread id for thread number i, where i > 0 and ps = {Left(i), Right(i)}.