Skip to content

Commit 17f805c

Browse files
shazqadeershazqadeer
committed
first commit of LinearTypeCollector
1 parent 9cc5137 commit 17f805c

File tree

3 files changed

+152
-27
lines changed

3 files changed

+152
-27
lines changed

‎Source/Concurrency/LinearDomainCollector.cs‎

Lines changed: 0 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -80,33 +80,6 @@ public static (Dictionary<Type, LinearDomain>, Dictionary<Type, Dictionary<Type,
8080
collector.VisitProgram(linearTypeChecker.program);
8181
return (collector.permissionTypeToLinearDomain, collector.collectors);
8282
}
83-
84-
public override Implementation VisitImplementation(Implementation node)
85-
{
86-
// Boogie parser strips the attributes from the parameters of the implementation
87-
// leaving them only on the parameters of the corresponding procedures.
88-
// This override exists only to patch this problem.
89-
var proc = node.Proc;
90-
for (int i = 0; i < proc.InParams.Count; i++)
91-
{
92-
var procInParam = proc.InParams[i];
93-
if (procInParam.Attributes != null)
94-
{
95-
var implInParam = node.InParams[i];
96-
implInParam.Attributes = (QKeyValue)procInParam.Attributes.Clone();
97-
}
98-
}
99-
for (int i = 0; i < proc.OutParams.Count; i++)
100-
{
101-
var procOutParam = proc.OutParams[i];
102-
if (procOutParam.Attributes != null)
103-
{
104-
var implOutParam = node.OutParams[i];
105-
implOutParam.Attributes = (QKeyValue)procOutParam.Attributes.Clone();
106-
}
107-
}
108-
return base.VisitImplementation(node);
109-
}
11083

11184
public override Variable VisitVariable(Variable node)
11285
{

‎Source/Concurrency/LinearTypeChecker.cs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,9 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker)
4141

4242
private void Error(Absy node, string message)
4343
{
44+
// Availability checking might process each command multiple times
45+
// potentially reporting the same error multiple times.
46+
// The errors dictionary ensures that each error is reported exactly once.
4447
if (errors.Contains((node, message)))
4548
{
4649
return;

‎Source/Concurrency/LinearTypeCollector.cs‎

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
using System.Collections.Generic;
2+
using System.Linq;
3+
4+
namespace Microsoft.Boogie
5+
{
6+
class LinearTypeCollector
7+
{
8+
private readonly Program program;
9+
private readonly TypecheckingContext checkingContext;
10+
private readonly Dictionary<Type, HashSet<Type>> linearTypes;
11+
12+
public static Dictionary<Type, HashSet<Type>> CollectLinearTypes(Program program, TypecheckingContext checkingContext)
13+
{
14+
var linearTypeCollector = new LinearTypeCollector(program, checkingContext);
15+
linearTypeCollector.Collect();
16+
linearTypeCollector.Check();
17+
return linearTypeCollector.linearTypes;
18+
}
19+
20+
private void Collect()
21+
{
22+
var decls = program.TopLevelDeclarations.OfType<DatatypeTypeCtorDecl>();
23+
var allDataTypes = decls.Select(decl => new CtorType(Token.NoToken, decl, []));
24+
while (true)
25+
{
26+
var count = linearTypes.Values.Select(x => x.Count).Sum();
27+
var visitedTypes = new HashSet<Type>();
28+
foreach (var type in allDataTypes)
29+
{
30+
VisitType(type, visitedTypes);
31+
}
32+
if (count == linearTypes.Values.Select(x => x.Count).Sum())
33+
{
34+
break;
35+
}
36+
}
37+
}
38+
private void Check()
39+
{
40+
foreach (var datatypeTypeCtorDecl in linearTypes.Keys.OfType<CtorType>().Select(ctorType => ctorType.Decl).OfType<DatatypeTypeCtorDecl>())
41+
{
42+
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
43+
var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl);
44+
var typeName = originalTypeCtorDecl.Name;
45+
if (typeName == "One")
46+
{
47+
var innerType = actualTypeParams[0];
48+
if (linearTypes.ContainsKey(innerType))
49+
{
50+
checkingContext.Error(originalTypeCtorDecl, "One instantiated with a linear type");
51+
}
52+
}
53+
else if (typeName == "Map")
54+
{
55+
var keyType = actualTypeParams[0];
56+
if (!IsOneType(keyType) && linearTypes.ContainsKey(keyType))
57+
{
58+
checkingContext.Error(originalTypeCtorDecl, "Map instantiated with a key type that is neither One _ nor ordinary");
59+
}
60+
}
61+
}
62+
}
63+
64+
65+
66+
private LinearTypeCollector(Program program, TypecheckingContext checkingContext)
67+
{
68+
this.program = program;
69+
this.checkingContext = checkingContext;
70+
this.linearTypes = [];
71+
}
72+
73+
private void VisitType(Type type, HashSet<Type> visitedTypes)
74+
{
75+
if (visitedTypes.Contains(type))
76+
{
77+
return;
78+
}
79+
visitedTypes.Add(type);
80+
81+
if (type is CtorType ctorType && ctorType.Decl is DatatypeTypeCtorDecl datatypeTypeCtorDecl)
82+
{
83+
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
84+
var typeName = originalTypeCtorDecl.Name;
85+
if (!(typeName == "One" || typeName == "Set" || typeName == "Map"))
86+
{
87+
VisitDatatype(ctorType, visitedTypes);
88+
return;
89+
}
90+
var actualTypeParams = program.monomorphizer.GetTypeInstantiation(datatypeTypeCtorDecl);
91+
actualTypeParams.ForEach(type => VisitType(type, visitedTypes));
92+
var permissionType = typeName == "One" ? type : actualTypeParams[0];
93+
if (IsOneType(permissionType))
94+
{
95+
AddPermissionType(type, permissionType);
96+
}
97+
if (typeName == "Map")
98+
{
99+
var valueType = actualTypeParams[1];
100+
if (linearTypes.TryGetValue(valueType, out HashSet<Type> permissionTypes))
101+
{
102+
AddPermissionTypes(type, permissionTypes);
103+
}
104+
}
105+
}
106+
}
107+
108+
private void VisitDatatype(CtorType ctorType, HashSet<Type> visitedTypes)
109+
{
110+
var datatypeTypeCtorDecl = (DatatypeTypeCtorDecl)ctorType.Decl;
111+
var constructors = datatypeTypeCtorDecl.Constructors;
112+
constructors.ForEach(constructor => constructor.InParams.ForEach(formal => VisitType(formal.TypedIdent.Type, visitedTypes)));
113+
constructors.ForEach(constructor =>
114+
constructor.InParams.Where(formal =>
115+
linearTypes.ContainsKey(formal.TypedIdent.Type)).ForEach(formal =>
116+
AddPermissionTypes(ctorType, linearTypes[formal.TypedIdent.Type])));
117+
}
118+
119+
private static bool IsOneType(Type type)
120+
{
121+
if (type is CtorType ctorType && ctorType.Decl is DatatypeTypeCtorDecl datatypeTypeCtorDecl)
122+
{
123+
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(datatypeTypeCtorDecl);
124+
return originalTypeCtorDecl.Name == "One";
125+
}
126+
return false;
127+
}
128+
129+
private void AddLinearType(Type linearType)
130+
{
131+
if (!linearTypes.ContainsKey(linearType))
132+
{
133+
linearTypes.Add(linearType, []);
134+
}
135+
}
136+
137+
private void AddPermissionType(Type linearType, Type permissionType)
138+
{
139+
AddLinearType(linearType);
140+
linearTypes[linearType].Add(permissionType);
141+
}
142+
143+
private void AddPermissionTypes(Type linearType, HashSet<Type> permissionTypes)
144+
{
145+
AddLinearType(linearType);
146+
linearTypes[linearType].UnionWith(permissionTypes);
147+
}
148+
}
149+
}

0 commit comments

Comments
 (0)