Skip to content

Commit 7698597

Browse files
shazqadeershazqadeer
committed
cleaned up annotations
1 parent 6af7d16 commit 7698597

File tree

11 files changed

+32
-41
lines changed

11 files changed

+32
-41
lines changed

‎Source/Concurrency/CivlTypeChecker.cs‎

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -441,16 +441,9 @@ private void MatchFormals(List<Variable> formals1, List<Variable> formals2, stri
441441
{
442442
checkingContext.Error(formals1[i], $"mismatched type of {inout}-parameter {name1} in {decl2.Name}");
443443
}
444-
else if (checkLinearity &&
445-
(QKeyValue.FindStringAttribute(formals1[i].Attributes, CivlAttributes.LINEAR) !=
446-
QKeyValue.FindStringAttribute(formals2[i].Attributes, CivlAttributes.LINEAR) ||
447-
QKeyValue.FindStringAttribute(formals1[i].Attributes, CivlAttributes.LINEAR_IN) !=
448-
QKeyValue.FindStringAttribute(formals2[i].Attributes, CivlAttributes.LINEAR_IN) ||
449-
QKeyValue.FindStringAttribute(formals1[i].Attributes, CivlAttributes.LINEAR_OUT) !=
450-
QKeyValue.FindStringAttribute(formals2[i].Attributes, CivlAttributes.LINEAR_OUT)))
444+
else if (checkLinearity && LinearTypeChecker.FindLinearKind(formals1[i]) != LinearTypeChecker.FindLinearKind(formals2[i]))
451445
{
452-
checkingContext.Error(formals1[i],
453-
$"mismatched linearity annotation of {inout}-parameter {name1} in {decl2.Name}");
446+
checkingContext.Error(formals1[i], $"mismatched linearity annotation of {inout}-parameter {name1} in {decl2.Name}");
454447
}
455448
}
456449
}

‎Source/ExecutionEngine/CommandLineOptions.cs‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1744,13 +1744,11 @@ Local variable collecting pending asyncs in yielding procedure.
17441744
{:sync}
17451745
Synchronized async call.
17461746
1747-
{:linear ""domain""}
1748-
Permission type for domain.
1749-
Collector function for domain.
1750-
Linear variable (both global and local).
1747+
{:linear}
1748+
Linear variable (both global and input/output parameter).
17511749
1752-
{:linear_in ""domain""}
1753-
{:linear_out ""domain""}
1750+
{:linear_in}
1751+
{:linear_out}
17541752
Linear input/output parameter.";
17551753

17561754
protected override string HelpHeader =>

‎Test/civl/large-samples/shared-vector.bpl‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ var {:layer 2, 3} IntArrayPool: Map (One (Loc IntArray)) (Vec int);
88

99
datatype IntArray {
1010
IntArray(
11-
{:linear "no_collect_keys"} mutexes: Map int (One (Loc int)),
12-
{:linear "no_collect_keys"} values: Map int (Cell (Loc int) int)
11+
mutexes: Map int (One (Loc int)),
12+
values: Map int (Cell (Loc int) int)
1313
)
1414
}
1515

@@ -43,8 +43,8 @@ preserves call IntArrayDom();
4343
{
4444
var {:linear} one_loc_mutex: One (Loc int);
4545
var {:linear} cell_int: Cell (Loc int) int;
46-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
47-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
46+
var {:linear} mutexes: Map int (One (Loc int));
47+
var {:linear} values: Map int (Cell (Loc int) int);
4848
var {:linear} intvec: IntArray;
4949
var i: int;
5050
var {:linear} one_loc_i: One (Loc int);
@@ -209,8 +209,8 @@ modifies IntArrayPoolLow;
209209
{
210210
var {:linear} one_loc_iv: One (Loc IntArray);
211211
var {:linear} intvec: IntArray;
212-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
213-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
212+
var {:linear} mutexes: Map int (One (Loc int));
213+
var {:linear} values: Map int (Cell (Loc int) int);
214214

215215
one_loc_iv := One(loc_iv);
216216
call intvec := Map_Get(IntArrayPoolLow, one_loc_iv);
@@ -235,8 +235,8 @@ modifies IntArrayPoolLow;
235235
{
236236
var {:linear} one_loc_iv: One (Loc IntArray);
237237
var {:linear} intvec: IntArray;
238-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
239-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
238+
var {:linear} mutexes: Map int (One (Loc int));
239+
var {:linear} values: Map int (Cell (Loc int) int);
240240

241241
one_loc_iv := One(loc_iv);
242242
call intvec := Map_Get(IntArrayPoolLow, one_loc_iv);
@@ -261,8 +261,8 @@ refines right action {:layer 1, 2} _
261261
{
262262
var {:linear} one_loc_iv: One (Loc IntArray);
263263
var {:linear} intvec: IntArray;
264-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
265-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
264+
var {:linear} mutexes: Map int (One (Loc int));
265+
var {:linear} values: Map int (Cell (Loc int) int);
266266
var {:linear} one_loc_mutex: One (Loc int);
267267

268268
one_loc_iv := One(loc_iv);
@@ -280,8 +280,8 @@ refines atomic action {:layer 1, 1} _
280280
{
281281
var {:linear} one_loc_iv: One (Loc IntArray);
282282
var {:linear} intvec: IntArray;
283-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
284-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
283+
var {:linear} mutexes: Map int (One (Loc int));
284+
var {:linear} values: Map int (Cell (Loc int) int);
285285

286286
one_loc_iv := One(loc_iv);
287287
call intvec := Map_Get(IntArrayPoolLow, one_loc_iv);
@@ -296,8 +296,8 @@ refines atomic action {:layer 1, 1} _
296296
{
297297
var {:linear} one_loc_iv: One (Loc IntArray);
298298
var {:linear} intvec: IntArray;
299-
var {:linear "no_collect_keys"} mutexes: Map int (One (Loc int));
300-
var {:linear "no_collect_keys"} values: Map int (Cell (Loc int) int);
299+
var {:linear} mutexes: Map int (One (Loc int));
300+
var {:linear} values: Map int (Cell (Loc int) int);
301301

302302
one_loc_iv := One(loc_iv);
303303
call intvec := Map_Get(IntArrayPoolLow, one_loc_iv);

‎Test/civl/large-samples/treiber-stack.bpl‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
type TaggedLocNode V = TaggedLoc (Node V) Unit;
55

6-
datatype Treiber<V> { Treiber(top: Option (LocNode V), {:linear} nodes: Map (One (LocNode V)) (Node V)) }
6+
datatype Treiber<V> { Treiber(top: Option (LocNode V), nodes: Map (One (LocNode V)) (Node V)) }
77
type LocTreiber V = Loc (Treiber V);
88
type TaggedLocTreiber V = TaggedLoc (Treiber V) Unit;
99

‎Test/civl/regression-tests/call-yield-invariant-errors.bpl‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,16 @@ yield invariant {:layer 1} linear_yield_x({:linear} n: int);
66
preserves x >= n;
77

88
yield procedure {:layer 1}
9-
p2({:linear_in "lin"} b: int);
9+
p2({:linear_in} b: int);
1010

1111
yield procedure {:layer 1}
12-
P1({:linear} x: int, {:linear_in "lin"} y: int)
12+
P1({:linear} x: int, {:linear_in} y: int)
1313
{
1414
call Q(x) | Q(x);
1515
}
1616

1717
yield procedure {:layer 1}
18-
P2({:linear} x: int, {:linear_in "lin"} y: int)
18+
P2({:linear} x: int, {:linear_in} y: int)
1919
{
2020
call Q(x) | linear_yield_x(y) | linear_yield_x(y);
2121
call Q(x) | linear_yield_x(x) | linear_yield_x(y);

‎Test/civl/regression-tests/permissions.bpl‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,21 +16,21 @@ yield procedure {:layer 1} Proc1 ({:linear} i: One int)
1616
pure procedure Lemma (set: Set (One int), i: One int);
1717
requires !Set_Contains(set, i);
1818

19-
datatype D { D1({:linear} x: One int), D2({:linear} x: One int) }
19+
datatype D { D1(x: One int), D2(x: One int) }
2020

2121
yield procedure {:layer 1} Proc2 ({:linear} d: D)
2222
{
2323
call {:layer 1} Lemma(A, d->x);
2424
}
2525

26-
datatype E { E({:linear} d: D) }
26+
datatype E { E(d: D) }
2727

2828
yield procedure {:layer 1} Proc3 ({:linear} e: E)
2929
{
3030
call {:layer 1} Lemma(A, e->d->x);
3131
}
3232

33-
datatype D' { X({:linear} x: One int), Y(x: One int) }
33+
datatype D' { X(x: One int), Y(x: One int) }
3434

3535
yield procedure {:layer 1} Proc4 ({:linear} d: D')
3636
requires {:layer 1} d is X;

‎Test/civl/regression-tests/signature-mismatch.bpl‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ atomic action {:layer 1,1} atomic_write_x_3 ({:linear} x':int)
3333
modifies x;
3434
{ x := x'; }
3535

36-
yield procedure {:layer 0} write_x_3 ({:linear_in "lin"} x':int);
36+
yield procedure {:layer 0} write_x_3 ({:linear_in} x':int);
3737
refines atomic_write_x_3;
3838

3939
////////////////////////////////////////////////////////////////////////////////

‎Test/civl/regression-tests/signature-mismatch.bpl.expect‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
signature-mismatch.bpl(17,38): Error: mismatched name of in-parameter y': (named x' in atomic_write_x_1)
22
signature-mismatch.bpl(26,27): Error: mismatched number of in-parameters in atomic_write_x_2
3-
signature-mismatch.bpl(36,57): Error: mismatched linearity annotation of in-parameter x' in atomic_write_x_3
3+
signature-mismatch.bpl(36,51): Error: mismatched linearity annotation of in-parameter x' in atomic_write_x_3
44
signature-mismatch.bpl(45,38): Error: mismatched type of in-parameter x' in atomic_write_x_4
55
4 type checking errors detected in signature-mismatch.bpl

‎Test/civl/regression-tests/yield-requires-ensures-errors-4.bpl‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ yield invariant {:layer 1} linear_yield_x({:linear} n: int);
99
preserves x >= n;
1010

1111
yield procedure {:layer 1}
12-
p3({:linear} a: int, {:linear_in "lin"} b: int, {:linear_out "lin"} c: int);
12+
p3({:linear} a: int, {:linear_in} b: int, {:linear_out} c: int);
1313
requires call linear_yield_x(a);
1414
ensures call linear_yield_x(a);
1515
requires call linear_yield_x(c);

‎Test/civl/samples/two-queues.bpl‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t"
22
// RUN: %diff "%s.expect" "%t"
33

4-
datatype Queue<V> { Queue(head: LocNode V, tail: LocNode V, {:linear} nodes: Map (One (LocNode V)) (Node V)) }
4+
datatype Queue<V> { Queue(head: LocNode V, tail: LocNode V, nodes: Map (One (LocNode V)) (Node V)) }
55

66
type LocQueue V = Loc (Queue V);
77

0 commit comments

Comments
 (0)