diff options
| -rw-r--r-- | Source/Core/LinearSets.cs | 123 | ||||
| -rw-r--r-- | Test/linear/Answer | 20 | ||||
| -rw-r--r-- | Test/linear/Maps.bpl | 24 | ||||
| -rw-r--r-- | Test/linear/list.bpl | 4 | ||||
| -rw-r--r-- | Test/linear/runtest.bat | 4 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 65 | ||||
| -rw-r--r-- | Test/og/DeviceCacheSimplified.bpl | 2 | ||||
| -rw-r--r-- | Test/og/FlanaganQadeer.bpl | 2 | ||||
| -rw-r--r-- | Test/og/Maps.bpl | 24 | ||||
| -rw-r--r-- | Test/og/linear-set.bpl | 13 | ||||
| -rw-r--r-- | Test/og/linear-set2.bpl | 13 | ||||
| -rw-r--r-- | Test/og/runtest.bat | 2 |
12 files changed, 172 insertions, 124 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index d2904d59..de90b9e1 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -23,7 +23,26 @@ namespace Microsoft.Boogie checkingContext.Error(node, message);
errorCount++;
}
-
+ private Dictionary<Variable, string> scope;
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ scope = new Dictionary<Variable, string>();
+ for (int i = 0; i < node.OutParams.Length; i++)
+ {
+ string domainName = QKeyValue.FindStringAttribute(node.Proc.OutParams[i].Attributes, "linear");
+ if (domainName != null)
+ {
+ scope[node.OutParams[i]] = domainName;
+ }
+ }
+ return base.VisitImplementation(node);
+ }
+ private string FindDomainName(Variable v)
+ {
+ if (scope.ContainsKey(v))
+ return scope[v];
+ return QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ }
public override Variable VisitVariable(Variable node)
{
string domainName = QKeyValue.FindStringAttribute(node.Attributes, "linear");
@@ -33,28 +52,29 @@ namespace Microsoft.Boogie MapType mapType = type as MapType;
if (mapType != null)
{
- if (mapType.Arguments.Length > 1)
+ if (mapType.Arguments.Length == 1 && mapType.Result.Equals(Type.Bool))
{
- Error(node, "a linear domain can be attached to either a set or a scalar type");
+ type = mapType.Arguments[0];
+ if (type is MapType)
+ {
+ Error(node, "the domain of a linear set must be a scalar type");
+ return base.VisitVariable(node);
+ }
}
- type = mapType.Arguments[0];
- }
- if (domainNameToType.ContainsKey(domainName))
- {
- if (!domainNameToType[domainName].Equals(type))
+ else
{
- Error(node, "a linear domain must be consistently attached to variables of a particular type");
+ Error(node, "a linear domain can be attached to either a set or a scalar type");
+ return base.VisitVariable(node);
}
}
- else if (type is MapType)
+ if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))
{
- Error(node, "a linear domain can be attached to either a set or a scalar type");
+ Error(node, "a linear domain must be consistently attached to variables of a particular type");
}
else
{
domainNameToType[domainName] = type;
}
-
}
return base.VisitVariable(node);
}
@@ -64,7 +84,7 @@ namespace Microsoft.Boogie for (int i = 0; i < node.Lhss.Count; i++)
{
AssignLhs lhs = node.Lhss[i];
- string domainName = QKeyValue.FindStringAttribute(lhs.DeepAssignedVariable.Attributes, "linear");
+ string domainName = FindDomainName(lhs.DeepAssignedVariable);
if (domainName == null) continue;
SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
if (salhs == null)
@@ -75,15 +95,10 @@ namespace Microsoft.Boogie IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
if (rhs == null)
{
- Error(node, "Only variable can be assigned to a linear set");
+ Error(node, "Only variable can be assigned to a linear variable");
continue;
}
- string rhsDomainName = QKeyValue.FindStringAttribute(rhs.Decl.Attributes, "linear");
- Formal formal = rhs.Decl as Formal;
- if (formal != null && formal.InComing)
- {
- rhsDomainName = null;
- }
+ string rhsDomainName = FindDomainName(rhs.Decl);
if (rhsDomainName == null)
{
Error(node, "Only linear variable can be assigned to another linear variable");
@@ -115,15 +130,10 @@ namespace Microsoft.Boogie IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
if (actual == null)
{
- Error(node, "Only variable can be assigned to a linear set");
+ Error(node, "Only variable can be assigned to a linear variable");
continue;
}
- string actualDomainName = QKeyValue.FindStringAttribute(actual.Decl.Attributes, "linear");
- Formal formal2 = actual.Decl as Formal;
- if (formal2 != null && formal2.InComing)
- {
- actualDomainName = null;
- }
+ string actualDomainName = FindDomainName(actual.Decl);
if (actualDomainName == null)
{
Error(node, "Only a linear argument can be passed to a linear parameter");
@@ -150,7 +160,7 @@ namespace Microsoft.Boogie for (int i = 0; i < node.Proc.OutParams.Length; i++)
{
IdentifierExpr actual = node.Outs[i];
- string actualDomainName = QKeyValue.FindStringAttribute(actual.Decl.Attributes, "linear");
+ string actualDomainName = FindDomainName(actual.Decl);
if (actualDomainName == null) continue;
Variable formal = node.Proc.OutParams[i];
string domainName = QKeyValue.FindStringAttribute(formal.Attributes, "linear");
@@ -570,33 +580,36 @@ namespace Microsoft.Boogie this.elementType = mapType.Arguments[0];
}
this.allocator = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("allocator_{0}", domainName), new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool)));
- foreach (var decl in program.TopLevelDeclarations)
- {
- Function func = decl as Function;
- if (func == null) continue;
- var name = QKeyValue.FindStringAttribute(func.Attributes, "builtin");
- if (name == null) continue;
- MapType mapType = func.OutParams[0].TypedIdent.Type as MapType;
- if (mapType == null) continue;
- if (mapType.Arguments.Length > 1) continue;
- if (!mapType.Arguments[0].Equals(elementType)) continue;
- if (mapType.Result.Equals(Microsoft.Boogie.Type.Bool))
- {
- if (name == "MapOr")
- this.mapOrBool = func;
- else if (name == "MapImp")
- this.mapImpBool = func;
- else if (name == "MapConst")
- this.mapConstBool = func;
- else if (name == "MapEq")
- this.mapEqInt = func;
- }
- else if (mapType.Result.Equals(Microsoft.Boogie.Type.Int))
- {
- if (name == "MapConst")
- this.mapConstInt = func;
- }
- }
+
+ MapType mapTypeBool = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Bool);
+ MapType mapTypeInt = new MapType(Token.NoToken, new TypeVariableSeq(), new TypeSeq(this.elementType), Type.Int);
+ this.mapOrBool = new Function(Token.NoToken, "linear@MapOr",
+ new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
+ this.mapOrBool.AddAttribute("builtin", "MapOr");
+
+ this.mapImpBool = new Function(Token.NoToken, "linear@MapImp",
+ new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool), true),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool), true)),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
+ this.mapImpBool.AddAttribute("builtin", "MapImp");
+
+ this.mapConstBool = new Function(Token.NoToken, "linear@MapConstBool",
+ new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true)),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
+ this.mapConstBool.AddAttribute("builtin", "MapConst");
+
+ this.mapEqInt = new Function(Token.NoToken, "linear@MapEq",
+ new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt), true),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt), true)),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
+ this.mapEqInt.AddAttribute("builtin", "MapEq");
+
+ this.mapConstInt = new Function(Token.NoToken, "linear@MapConstInt",
+ new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true)),
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
+ this.mapConstInt.AddAttribute("builtin", "MapConst");
}
}
}
diff --git a/Test/linear/Answer b/Test/linear/Answer new file mode 100644 index 00000000..86e42862 --- /dev/null +++ b/Test/linear/Answer @@ -0,0 +1,20 @@ +
+-------------------- typecheck.bpl --------------------
+typecheck.bpl(6,22): Error: a linear domain must be consistently attached to variables of a particular type
+typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type
+typecheck.bpl(31,9): Error: Only simple assignment allowed on linear sets
+typecheck.bpl(33,6): Error: Only variable can be assigned to a linear variable
+typecheck.bpl(35,6): Error: Only linear variable can be assigned to another linear variable
+typecheck.bpl(39,6): Error: Variable of one domain being assigned to a variable of another domain
+typecheck.bpl(45,9): Error: A linear set can occur only once in the rhs
+typecheck.bpl(49,4): Error: A linear set can occur only once as an in parameter
+typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable
+typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter
+typecheck.bpl(64,6): Error: Only linear variable can be assigned to another linear variable
+0 type checking errors detected in typecheck.bpl
+
+-------------------- list.bpl --------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/linear/Maps.bpl b/Test/linear/Maps.bpl deleted file mode 100644 index 5f302034..00000000 --- a/Test/linear/Maps.bpl +++ /dev/null @@ -1,24 +0,0 @@ -type X;
-
-function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;
-function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;
-function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;
-function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;
-function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;
-function {:builtin "MapConst"} MapConstInt(int) : [X]int;
-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
-function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;
-function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;
-function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;
-function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;
-function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;
-function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;
-function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;
-function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;
-function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;
-
-
-
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl index 9a333351..f4badca9 100644 --- a/Test/linear/list.bpl +++ b/Test/linear/list.bpl @@ -1,3 +1,7 @@ +type X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
+
var head: X;
var tail: X;
var {:linear "Mem"} D: [X]bool;
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat index 28c91996..df176994 100644 --- a/Test/linear/runtest.bat +++ b/Test/linear/runtest.bat @@ -3,9 +3,9 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (list.bpl) do (
+for %%f in (typecheck.bpl list.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f Maps.bpl
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
)
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl new file mode 100644 index 00000000..f79f8fb5 --- /dev/null +++ b/Test/linear/typecheck.bpl @@ -0,0 +1,65 @@ +type X;
+
+procedure A()
+{
+ var {:linear "A"} a: X;
+ var {:linear "A"} b: int;
+}
+
+procedure B()
+{
+ var {:linear "B"} a: X;
+ var {:linear "B"} b: [X]bool;
+}
+
+procedure C()
+{
+ var {:linear "C"} a: X;
+ var {:linear "C"} c: [X]int;
+}
+
+function f(X): X;
+
+procedure D()
+{
+ var {:linear "D"} a: X;
+ var {:linear "D"} x: X;
+ var {:linear "D"} b: [X]bool;
+ var c: X;
+ var {:linear "D2"} d: X;
+
+ b[a] := true;
+
+ a := f(a);
+
+ a := c;
+
+ c := a;
+
+ a := d;
+
+ a := a;
+
+ a, x := x, a;
+
+ a, x := x, x;
+
+ call a, x := E(a, x);
+
+ call a, x := E(a, a);
+
+ call a, x := E(a, f(a));
+
+ call a, x := E(a, d);
+
+ call d, x := E(a, x);
+
+ call a, x := E(c, x);
+
+ call c, x := E(a, x);
+}
+
+procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+{
+ c := a;
+}
\ No newline at end of file diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 40a0ab1c..c89bd793 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -1,3 +1,5 @@ +type X;
+
function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
{
currsize <= newsize && (ghostLock == nil <==> currsize == newsize)
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 63a7fc0d..8379925f 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -1,3 +1,5 @@ +type X;
+
const nil: X;
var l: X;
var x: int;
diff --git a/Test/og/Maps.bpl b/Test/og/Maps.bpl deleted file mode 100644 index 5f302034..00000000 --- a/Test/og/Maps.bpl +++ /dev/null @@ -1,24 +0,0 @@ -type X;
-
-function {:builtin "MapAdd"} MapAdd([X]int, [X]int) : [X]int;
-function {:builtin "MapSub"} MapSub([X]int, [X]int) : [X]int;
-function {:builtin "MapMul"} MapMul([X]int, [X]int) : [X]int;
-function {:builtin "MapDiv"} MapDiv([X]int, [X]int) : [X]int;
-function {:builtin "MapMod"} MapMod([X]int, [X]int) : [X]int;
-function {:builtin "MapConst"} MapConstInt(int) : [X]int;
-function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
-function {:builtin "MapAnd"} MapAnd([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapNot"} MapNot([X]bool) : [X]bool;
-function {:builtin "MapIte"} MapIteInt([X]bool, [X]int, [X]int) : [X]int;
-function {:builtin "MapIte"} MapIteBool([X]bool, [X]bool, [X]bool) : [X]bool;
-function {:builtin "MapLe"} MapLe([X]int, [X]int) : [X]bool;
-function {:builtin "MapLt"} MapLt([X]int, [X]int) : [X]bool;
-function {:builtin "MapGe"} MapGe([X]int, [X]int) : [X]bool;
-function {:builtin "MapGt"} MapGt([X]int, [X]int) : [X]bool;
-function {:builtin "MapEq"} MapEq([X]int, [X]int) : [X]bool;
-function {:builtin "MapIff"} MapIff([X]bool, [X]bool) : [X]bool;
-function {:builtin "MapImp"} MapImp([X]bool, [X]bool) : [X]bool;
-
-
-
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index 1a0cde42..04ad0df2 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -1,12 +1,7 @@ -function {:inline} Subset(a: [X]bool, b: [X]bool) : bool
-{
- MapImp(a, b) == MapConstBool(true)
-}
-
-function {:inline} In(a: X, b: [X]bool) : bool
-{
- b[a]
-}
+type X;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
function {:inline} None() : [X]bool
{
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index a91100b6..0df45254 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -1,12 +1,7 @@ -function {:inline} Subset(a: [X]bool, b: [X]bool) : bool
-{
- MapImp(a, b) == MapConstBool(true)
-}
-
-function {:inline} In(a: X, b: [X]bool) : bool
-{
- b[a]
-}
+type X;
+function {:builtin "MapConst"} MapConstInt(int) : [X]int;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;
function {:inline} None() : [X]bool
{
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat index 197f33f7..b00a3dda 100644 --- a/Test/og/runtest.bat +++ b/Test/og/runtest.bat @@ -12,6 +12,6 @@ for %%f in (foo.bpl bar.bpl one.bpl) do ( for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f Maps.bpl
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f
)
|