From 9c1c28a5e28f76af29805e6dd8b4b34c99fbe1b4 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 15 Jul 2014 19:47:44 -0700
Subject: updated the linear type system based on Chris' design with linear,
 linear_in, linear_out

---
 Test/linear/allocator.bpl        |  4 ++--
 Test/linear/async-bug.bpl        |  9 +++++++--
 Test/linear/async-bug.bpl.expect |  4 ++--
 Test/linear/f1.bpl               |  4 ++--
 Test/linear/f2.bpl               |  4 ++--
 Test/linear/f3.bpl               |  2 +-
 Test/linear/list.bpl             |  2 +-
 Test/linear/typecheck.bpl        | 10 +++++-----
 8 files changed, 22 insertions(+), 17 deletions(-)

(limited to 'Test/linear')

diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index 31f54f7e..147d700f 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -1,9 +1,9 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
+procedure A({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int);
   ensures i == i';
 
-procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 
+procedure B({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int) 
 {
   i := i';
   call i := A(i);
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index faa1a65d..ff6cdded 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -2,12 +2,17 @@
 // RUN: %diff "%s.expect" "%t"
 const GcTid:int;
 
-procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} Initialize({:linear "tid"} tid:int)
 requires{:phase 100} tid == GcTid;
 {
     yield;
     assert{:phase 100} tid == GcTid;
 
+    call GarbageCollect(tid);
+
+    yield;
+    assert{:phase 100} tid == GcTid;
+
     async call GarbageCollect(tid);
 
     yield;
@@ -22,7 +27,7 @@ requires{:phase 100} tid == GcTid;
     assert{:phase 100} tid == GcTid;
 }
 
-procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} GarbageCollect({:linear "tid"} tid:int)
 requires{:phase 100} tid == GcTid;
 {
     yield;
diff --git a/Test/linear/async-bug.bpl.expect b/Test/linear/async-bug.bpl.expect
index 8bfe61d1..73a5eaee 100644
--- a/Test/linear/async-bug.bpl.expect
+++ b/Test/linear/async-bug.bpl.expect
@@ -1,3 +1,3 @@
-async-bug.bpl(11,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call
-async-bug.bpl(16,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call
+async-bug.bpl(21,30): Error: unavailable source for a linear read
+async-bug.bpl(28,0): Error: Input variable tid must be available at a return
 2 type checking errors detected in async-bug.bpl
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
index e18fab9f..0d255149 100644
--- a/Test/linear/f1.bpl
+++ b/Test/linear/f1.bpl
@@ -21,7 +21,7 @@ axiom(!b6);
 axiom(!b7);
 axiom(b8);
 
-procedure {:entrypoint} main({:linear "1"} x_in: [int]bool) 
+procedure main({:linear_in "1"} x_in: [int]bool) 
   requires b0 ==> x_in == mapconstbool(true);
   requires b1 ==> x_in != mapconstbool(false);
 {
@@ -35,7 +35,7 @@ procedure {:entrypoint} main({:linear "1"} x_in: [int]bool)
    assert b8 ==> x == mapconstbool(false);
 }
 
-procedure foo({:linear "1"} x_in: [int]bool)
+procedure foo({:linear_in "1"} x_in: [int]bool)
   requires b2 ==> x_in == mapconstbool(true);
   requires b3 ==> x_in != mapconstbool(false);
 {
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 16863154..18f518da 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -3,12 +3,12 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
 function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
 
-procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
+procedure Split({:linear_in "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
 ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
 
 procedure Allocate() returns ({:linear "1"} x: [int]bool);
 
-procedure {:entrypoint} main() 
+procedure main() 
 {
    var {:linear "1"} x: [int] bool;
    var {:linear "1"} x1: [int] bool;
diff --git a/Test/linear/f3.bpl b/Test/linear/f3.bpl
index f5e08277..3a0e855c 100644
--- a/Test/linear/f3.bpl
+++ b/Test/linear/f3.bpl
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"
 procedure A() {}
 
-procedure B({:linear ""} tid:int) returns({:linear ""} tid':int)
+procedure B({:linear_in ""} tid:int) returns({:linear ""} tid':int)
 {
   tid' := tid;
   call A();
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index 72f165fb..804cb7e2 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -18,7 +18,7 @@ const nil: X;
 procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
 ensures M == MapConstBool(false)[x := true];
 
-procedure Join({:linear "Mem"} A: [X]bool);
+procedure Join({:linear_in "Mem"} A: [X]bool);
 modifies D;
 ensures MapOr(old(D), A) == D;
 
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index a3980a3e..057718cf 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -65,12 +65,12 @@ procedure {:yields} {:phase 1} D()
     yield;
 }
 
-procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
 {
     c := a;
 }
 
-procedure {:yields} {:phase 0} F({:linear "D"} a: X) returns ({:linear "D"} c: X);
+procedure {:yields} {:phase 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);
 
 var {:linear "x"} g:int;
 
@@ -85,7 +85,7 @@ modifies g;
   g := r;
 }
 
-procedure {:yields} {:phase 0} I({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)
 {
   x' := x;
 }
@@ -94,7 +94,7 @@ procedure {:yields} {:phase 0} J()
 {
 }
 
-procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
 {
   yield;
   par x' := I(x) | J();
@@ -103,7 +103,7 @@ procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':in
   yield;
 }
 
-procedure {:yields} {:phase 1} P2({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int)
 {
   yield;
   call x' := I(x);
-- 
cgit v1.2.3