diff options
| author |  qadeer <unknown> | 2013-11-22 13:04:51 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-11-22 13:04:51 -0800 |
| commit | 3c65f1b879a19c5ab1ed78ebfbcdb434fe7afe06 (patch) | |
| tree | 0703268a6d7676a2efb9da6b58e3351f41373d22 /Source/Concurrency | |
| parent | f0d11b78f3453b5cfbb524e6d0c7214442814351 (diff) | |
factored the concurrency checking code into a separate project
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/App.config | 6 | ||||
| -rw-r--r-- | Source/Concurrency/Concurrency.csproj | 88 | ||||
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 757 | ||||
| -rw-r--r-- | Source/Concurrency/MoverChecking.cs | 641 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 738 | ||||
| -rw-r--r-- | Source/Concurrency/Properties/AssemblyInfo.cs | 36 |
6 files changed, 2266 insertions, 0 deletions
diff --git a/Source/Concurrency/App.config b/Source/Concurrency/App.config new file mode 100644 index 00000000..84bc4207 --- /dev/null +++ b/Source/Concurrency/App.config @@ -0,0 +1,6 @@ +<?xml version="1.0"?>
+<configuration>
+ <startup>
+ <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.0,Profile=Client"/>
+ </startup>
+</configuration>
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj new file mode 100644 index 00000000..ba9a1dda --- /dev/null +++ b/Source/Concurrency/Concurrency.csproj @@ -0,0 +1,88 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProjectGuid>{D07B8E38-E172-47F4-AD02-0373014A46D3}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Concurrency</RootNamespace>
+ <AssemblyName>Concurrency</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup>
+ <StartupObject />
+ </PropertyGroup>
+ <PropertyGroup>
+ <SignAssembly>true</SignAssembly>
+ </PropertyGroup>
+ <PropertyGroup>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="LinearSets.cs" />
+ <Compile Include="MoverChecking.cs" />
+ <Compile Include="OwickiGries.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="App.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\Basetypes\Basetypes.csproj">
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Core\Core.csproj">
+ <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Graph\Graph.csproj">
+ <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Name>Graph</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
+ <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Name>ParserHelper</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs new file mode 100644 index 00000000..51f7f328 --- /dev/null +++ b/Source/Concurrency/LinearSets.cs @@ -0,0 +1,757 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie
+{
+ public class LinearEraser : StandardVisitor
+ {
+ private QKeyValue RemoveLinearAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveLinearAttribute(iter.Next);
+ return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ node.Attributes = RemoveLinearAttribute(node.Attributes);
+ return base.VisitVariable(node);
+ }
+ }
+
+ public class LinearTypeChecker : StandardVisitor
+ {
+ public Program program;
+ public int errorCount;
+ public CheckingContext checkingContext;
+ public Dictionary<string, Type> domainNameToType;
+ public Dictionary<Absy, HashSet<Variable>> availableLinearVars;
+ public Dictionary<Variable, string> inoutParamToDomainName;
+ public Dictionary<Variable, string> varToDomainName;
+ public Dictionary<Variable, string> globalVarToDomainName;
+ public Dictionary<string, LinearDomain> linearDomains;
+
+ public LinearTypeChecker(Program program)
+ {
+ this.program = program;
+ this.errorCount = 0;
+ this.checkingContext = new CheckingContext(null);
+ this.domainNameToType = new Dictionary<string, Type>();
+ this.parallelCallInvars = new HashSet<Variable>();
+ this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
+ this.inoutParamToDomainName = new Dictionary<Variable, string>();
+ this.varToDomainName = new Dictionary<Variable, string>();
+ this.linearDomains = new Dictionary<string, LinearDomain>();
+ }
+ public void Typecheck()
+ {
+ this.VisitProgram(program);
+ foreach (string domainName in domainNameToType.Keys)
+ {
+ this.linearDomains[domainName] = new LinearDomain(program, domainName, domainNameToType[domainName]);
+ }
+ }
+ private void Error(Absy node, string message)
+ {
+ checkingContext.Error(node, message);
+ errorCount++;
+ }
+ public override Program VisitProgram(Program node)
+ {
+ globalVarToDomainName = new Dictionary<Variable, string>();
+ foreach (GlobalVariable g in program.GlobalVariables())
+ {
+ string domainName = FindDomainName(g);
+ if (domainName != null)
+ {
+ globalVarToDomainName[g] = domainName;
+ }
+ }
+ return base.VisitProgram(node);
+ }
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);
+ for (int i = 0; i < node.InParams.Count; i++)
+ {
+ string domainName = FindDomainName(node.Proc.InParams[i]);
+ if (domainName != null)
+ {
+ inoutParamToDomainName[node.InParams[i]] = domainName;
+ start.Add(node.InParams[i]);
+ }
+ }
+ for (int i = 0; i < node.OutParams.Count; i++)
+ {
+ string domainName = FindDomainName(node.Proc.OutParams[i]);
+ if (domainName != null)
+ {
+ inoutParamToDomainName[node.OutParams[i]] = domainName;
+ }
+ }
+
+ var oldErrorCount = this.errorCount;
+ var impl = base.VisitImplementation(node);
+ if (oldErrorCount < this.errorCount)
+ return impl;
+
+ Stack<Block> dfsStack = new Stack<Block>();
+ HashSet<Block> dfsStackAsSet = new HashSet<Block>();
+ availableLinearVars[node.Blocks[0]] = start;
+ dfsStack.Push(node.Blocks[0]);
+ dfsStackAsSet.Add(node.Blocks[0]);
+ while (dfsStack.Count > 0)
+ {
+ Block b = dfsStack.Pop();
+ dfsStackAsSet.Remove(b);
+ HashSet<Variable> end = PropagateAvailableLinearVarsAcrossBlock(b);
+ if (b.TransferCmd is ReturnCmd)
+ {
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a return", g.Name));
+ }
+ foreach (Variable v in node.OutParams)
+ {
+ if (FindDomainName(v) == null || end.Contains(v)) continue;
+ Error(b, string.Format("Output variable {0} must be available at a return", v.Name));
+ }
+ continue;
+ }
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ if (!availableLinearVars.ContainsKey(target))
+ {
+ availableLinearVars[target] = new HashSet<Variable>(end);
+ dfsStack.Push(target);
+ dfsStackAsSet.Add(target);
+ }
+ else
+ {
+ var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);
+ availableLinearVars[target].IntersectWith(end);
+ if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))
+ {
+ dfsStack.Push(target);
+ dfsStackAsSet.Add(target);
+ }
+ }
+ }
+ }
+ return impl;
+ }
+ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {
+ HashSet<Variable> start = new HashSet<Variable>(availableLinearVars[b]);
+ foreach (Cmd cmd in b.Cmds)
+ {
+ if (cmd is AssignCmd)
+ {
+ AssignCmd assignCmd = (AssignCmd)cmd;
+ for (int i = 0; i < assignCmd.Lhss.Count; i++)
+ {
+ if (FindDomainName(assignCmd.Lhss[i].DeepAssignedVariable) == null) continue;
+ IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr;
+ if (start.Contains(ie.Decl))
+ {
+ start.Remove(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
+ }
+ foreach (AssignLhs assignLhs in assignCmd.Lhss)
+ {
+ if (FindDomainName(assignLhs.DeepAssignedVariable) == null) continue;
+ start.Add(assignLhs.DeepAssignedVariable);
+ }
+ }
+ else if (cmd is CallCmd)
+ {
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a call", g.Name));
+ }
+ CallCmd callCmd = (CallCmd)cmd;
+ while (callCmd != null)
+ {
+ for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
+ {
+ if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
+ IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ if (start.Contains(ie.Decl))
+ {
+ start.Remove(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
+ }
+ callCmd = callCmd.InParallelWith;
+ }
+ callCmd = (CallCmd)cmd;
+ availableLinearVars[callCmd] = new HashSet<Variable>(start);
+ while (callCmd != null)
+ {
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (FindDomainName(ie.Decl) == null) continue;
+ start.Add(ie.Decl);
+ }
+ callCmd = callCmd.InParallelWith;
+ }
+ }
+ else if (cmd is HavocCmd)
+ {
+ HavocCmd havocCmd = (HavocCmd) cmd;
+ foreach (IdentifierExpr ie in havocCmd.Vars)
+ {
+ if (FindDomainName(ie.Decl) == null) continue;
+ start.Remove(ie.Decl);
+ }
+ }
+ else if (cmd is YieldCmd)
+ {
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a yield", g.Name));
+ }
+ availableLinearVars[cmd] = new HashSet<Variable>(start);
+ }
+ }
+ return start;
+ }
+ public string FindDomainName(Variable v)
+ {
+ if (globalVarToDomainName.ContainsKey(v))
+ return globalVarToDomainName[v];
+ if (inoutParamToDomainName.ContainsKey(v))
+ return inoutParamToDomainName[v];
+ return QKeyValue.FindStringAttribute(v.Attributes, "linear");
+ }
+ public override Variable VisitVariable(Variable node)
+ {
+ string domainName = FindDomainName(node);
+ if (domainName != null)
+ {
+ Type type = node.TypedIdent.Type;
+ MapType mapType = type as MapType;
+ if (mapType != null)
+ {
+ if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool))
+ {
+ 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);
+ }
+ }
+ else
+ {
+ Error(node, "a linear domain can be attached to either a set or a scalar type");
+ return base.VisitVariable(node);
+ }
+ }
+ if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))
+ {
+ Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName));
+ }
+ else
+ {
+ domainNameToType[domainName] = type;
+ }
+ }
+ return base.VisitVariable(node);
+ }
+ public override Cmd VisitAssignCmd(AssignCmd node)
+ {
+ HashSet<Variable> rhsVars = new HashSet<Variable>();
+ for (int i = 0; i < node.Lhss.Count; i++)
+ {
+ AssignLhs lhs = node.Lhss[i];
+ Variable lhsVar = lhs.DeepAssignedVariable;
+ string domainName = FindDomainName(lhsVar);
+ if (domainName == null) continue;
+ SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
+ if (salhs == null)
+ {
+ Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name));
+ continue;
+ }
+ IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
+ if (rhs == null)
+ {
+ Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name));
+ continue;
+ }
+ string rhsDomainName = FindDomainName(rhs.Decl);
+ if (rhsDomainName == null)
+ {
+ Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name));
+ continue;
+ }
+ if (domainName != rhsDomainName)
+ {
+ Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName));
+ continue;
+ }
+ if (rhsVars.Contains(rhs.Decl))
+ {
+ Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name));
+ continue;
+ }
+ rhsVars.Add(rhs.Decl);
+ }
+ return base.VisitAssignCmd(node);
+ }
+ HashSet<Variable> parallelCallInvars;
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ HashSet<Variable> inVars = new HashSet<Variable>();
+ for (int i = 0; i < node.Proc.InParams.Count; i++)
+ {
+ Variable formal = node.Proc.InParams[i];
+ string domainName = FindDomainName(formal);
+ if (domainName == null) continue;
+ IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
+ if (actual == null)
+ {
+ Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name));
+ continue;
+ }
+ string actualDomainName = FindDomainName(actual.Decl);
+ if (actualDomainName == null)
+ {
+ Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name));
+ continue;
+ }
+ if (domainName != actualDomainName)
+ {
+ Error(node, "The domains of formal and actual parameters must be the same");
+ continue;
+ }
+ if (parallelCallInvars.Contains(actual.Decl))
+ {
+ Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));
+ continue;
+ }
+ if (actual.Decl is GlobalVariable)
+ {
+ Error(node, "Only local linear variable can be an actual input parameter of a procedure call");
+ continue;
+ }
+ inVars.Add(actual.Decl);
+ parallelCallInvars.Add(actual.Decl);
+ }
+ for (int i = 0; i < node.Proc.OutParams.Count; i++)
+ {
+ IdentifierExpr actual = node.Outs[i];
+ string actualDomainName = FindDomainName(actual.Decl);
+ if (actualDomainName == null) continue;
+ Variable formal = node.Proc.OutParams[i];
+ string domainName = FindDomainName(formal);
+ if (domainName == null)
+ {
+ Error(node, "Only a linear variable can be passed to a linear parameter");
+ continue;
+ }
+ if (domainName != actualDomainName)
+ {
+ Error(node, "The domains of formal and actual parameters must be the same");
+ continue;
+ }
+ if (actual.Decl is GlobalVariable)
+ {
+ Error(node, "Only local linear variable can be actual output parameter of a procedure call");
+ continue;
+ }
+ }
+ if (node.InParallelWith != null)
+ {
+ VisitCallCmd(node.InParallelWith);
+ }
+ foreach (Variable v in inVars)
+ {
+ parallelCallInvars.Remove(v);
+ }
+ return base.VisitCallCmd(node);
+ }
+
+ private void AddDisjointnessExpr(List<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
+ {
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
+ }
+ foreach (Variable v in availableLinearVars[absy])
+ {
+ var domainName = FindDomainName(v);
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (string domainName in linearDomains.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ }
+
+ public void Transform()
+ {
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ foreach (string domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ Formal f = new Formal(
+ Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "linear_" + domainName + "_in",
+ new MapType(Token.NoToken, new List<TypeVariable>(),
+ new List<Type> { domain.elementType }, Type.Bool)), true);
+ impl.InParams.Add(f);
+ domainNameToInputVar[domainName] = f;
+ }
+
+ foreach (Block b in impl.Blocks)
+ {
+ List<Cmd> newCmds = new List<Cmd>();
+ for (int i = 0; i < b.Cmds.Count; i++)
+ {
+ Cmd cmd = b.Cmds[i];
+ newCmds.Add(cmd);
+ if (cmd is CallCmd)
+ {
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd.IsAsync)
+ {
+ foreach (var domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ callCmd.Ins.Add(expr);
+ }
+ }
+ else if (callCmd.InParallelWith != null)
+ {
+ while (callCmd != null)
+ {
+ foreach (var domainName in linearDomains.Keys)
+ {
+ var domain = linearDomains[domainName];
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ callCmd.Ins.Add(expr);
+ }
+ callCmd = callCmd.InParallelWith;
+ }
+ }
+ else
+ {
+ Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+ foreach (var domainName in linearDomains.Keys)
+ {
+ domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ }
+ foreach (Variable v in availableLinearVars[callCmd])
+ {
+ var domainName = FindDomainName(v);
+ var domain = linearDomains[domainName];
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool),
+ new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ domainNameToExpr[domainName] = expr;
+ }
+ foreach (var domainName in linearDomains.Keys)
+ {
+ callCmd.Ins.Add(domainNameToExpr[domainName]);
+ }
+ }
+ }
+ else if (cmd is YieldCmd)
+ {
+ AddDisjointnessExpr(newCmds, cmd, domainNameToInputVar);
+ }
+ }
+ b.Cmds = newCmds;
+ }
+
+ {
+ // Loops
+ impl.PruneUnreachableBlocks();
+ impl.ComputePredecessorsForBlocks();
+ GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);
+ g.ComputeLoops();
+ if (g.Reducible)
+ {
+ foreach (Block header in g.Headers)
+ {
+ List<Cmd> newCmds = new List<Cmd>();
+ AddDisjointnessExpr(newCmds, header, domainNameToInputVar);
+ newCmds.AddRange(header.Cmds);
+ header.Cmds = newCmds;
+ }
+ }
+ }
+ }
+
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+
+ Dictionary<string, HashSet<Variable>> domainNameToInputScope = new Dictionary<string, HashSet<Variable>>();
+ Dictionary<string, HashSet<Variable>> domainNameToOutputScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearDomains.Keys)
+ {
+ domainNameToInputScope[domainName] = new HashSet<Variable>();
+ domainNameToOutputScope[domainName] = new HashSet<Variable>();
+
+ }
+ foreach (Variable v in globalVarToDomainName.Keys)
+ {
+ var domainName = globalVarToDomainName[v];
+ domainNameToInputScope[domainName].Add(v);
+ domainNameToOutputScope[domainName].Add(v);
+ }
+ foreach (Variable v in proc.InParams)
+ {
+ var domainName = FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToInputScope[domainName].Add(v);
+ }
+ foreach (Variable v in proc.OutParams)
+ {
+ var domainName = FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToOutputScope[domainName].Add(v);
+ }
+ foreach (var domainName in linearDomains.Keys)
+ {
+ proc.Requires.Add(new Requires(true, DisjointnessExpr(domainName, domainNameToInputScope[domainName])));
+ var domain = linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ proc.InParams.Add(f);
+ domainNameToOutputScope[domainName].Add(f);
+ proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));
+ }
+ }
+
+ foreach (LinearDomain domain in linearDomains.Values)
+ {
+ program.TopLevelDeclarations.Add(domain.mapConstBool);
+ program.TopLevelDeclarations.Add(domain.mapConstInt);
+ program.TopLevelDeclarations.Add(domain.mapEqInt);
+ program.TopLevelDeclarations.Add(domain.mapImpBool);
+ program.TopLevelDeclarations.Add(domain.mapOrBool);
+ foreach (Axiom axiom in domain.axioms)
+ {
+ program.TopLevelDeclarations.Add(axiom);
+ }
+ }
+
+ //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ //CommandLineOptions.Clo.PrintUnstructured = 1;
+ //PrintBplFile("lsd.bpl", program, false, false);
+ //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+
+ public Expr Singleton(Expr e, string domainName)
+ {
+ var domain = linearDomains[domainName];
+ return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }), e, Expr.True);
+ }
+
+ List<Expr> MkExprs(params Expr[] args)
+ {
+ return new List<Expr>(args);
+ }
+
+ public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)
+ {
+ LinearDomain domain = linearDomains[domainName];
+ BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));
+ Expr disjointExpr = Expr.True;
+ int count = 0;
+ foreach (Variable v in scope)
+ {
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List<Expr>{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } );
+ e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { new IdentifierExpr(Token.NoToken, partition), e } );
+ e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } );
+ e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));
+ disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);
+ }
+ var expr = new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ return expr;
+ }
+ }
+
+ public class LinearDomain
+ {
+ public Microsoft.Boogie.Type elementType;
+ public Function mapEqInt;
+ public Function mapConstInt;
+ public Function mapOrBool;
+ public Function mapImpBool;
+ public Function mapConstBool;
+ public List<Axiom> axioms;
+
+ public LinearDomain(Program program, string domainName, Type elementType)
+ {
+ this.elementType = elementType;
+ this.axioms = new List<Axiom>();
+
+ MapType mapTypeBool = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Bool);
+ MapType mapTypeInt = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Int);
+ this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr",
+ new List<Variable> { 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));
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapOrBool.AddAttribute("builtin", "MapOr");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List<Expr> { aie, bie } );
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie } );
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie } ),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie} ));
+ var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
+ new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
+ new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
+
+ this.mapImpBool = new Function(Token.NoToken, "linear_" + domainName + "_MapImp",
+ new List<Variable> { 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));
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapImpBool.AddAttribute("builtin", "MapImp");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List<Expr> { aie, bie });
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));
+ var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
+ new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
+ new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
+
+ this.mapConstBool = new Function(Token.NoToken, "linear_" + domainName + "_MapConstBool",
+ new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Bool), true) },
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeBool), false));
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstBool.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.True }), xie });
+ var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, trueTerm);
+ trueAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr));
+ var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1),
+ new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.False }), xie });
+ var falseAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm));
+ falseAxiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr));
+ }
+
+ this.mapEqInt = new Function(Token.NoToken, "linear_" + domainName + "_MapEq",
+ new List<Variable> { 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));
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapEqInt.AddAttribute("builtin", "MapEq");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt));
+ IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List<Expr> { aie, bie });
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });
+ var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { aie, xie }),
+ new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { bie, xie }));
+ var axiomExpr = new ForallExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable> { a, b }, null,
+ new Trigger(Token.NoToken, true, new List<Expr> { mapApplTerm }),
+ new ForallExpr(Token.NoToken, new List<Variable> { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm)));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
+
+ this.mapConstInt = new Function(Token.NoToken, "linear_" + domainName + "_MapConstInt",
+ new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "b", Type.Int), true) },
+ new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "c", mapTypeInt), false));
+ if (CommandLineOptions.Clo.UseArrayTheory)
+ {
+ this.mapConstInt.AddAttribute("builtin", "MapConst");
+ }
+ else
+ {
+ BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int));
+ IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);
+ BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));
+ IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);
+ var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List<Expr> { aie }), xie });
+ var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));
+ axiomExpr.Typecheck(new TypecheckingContext(null));
+ axioms.Add(new Axiom(Token.NoToken, axiomExpr));
+ }
+
+ foreach (var axiom in axioms)
+ {
+ axiom.Expr.Resolve(new ResolutionContext(null));
+ axiom.Expr.Typecheck(new TypecheckingContext(null));
+ }
+ }
+ }
+}
diff --git a/Source/Concurrency/MoverChecking.cs b/Source/Concurrency/MoverChecking.cs new file mode 100644 index 00000000..aeea3947 --- /dev/null +++ b/Source/Concurrency/MoverChecking.cs @@ -0,0 +1,641 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+ /*
+ * Typechecking rules:
+ * At most one atomic specification per procedure
+ * The gate of an atomic specification refers only to global and input variables
+ */
+ public class MoverChecking
+ {
+ HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
+ HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
+ LinearTypeChecker linearTypeChecker;
+ Program moverCheckerProgram;
+ private MoverChecking(LinearTypeChecker linearTypeChecker)
+ {
+ this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.linearTypeChecker = linearTypeChecker;
+ this.moverCheckerProgram = new Program();
+ foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations)
+ {
+ if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom)
+ this.moverCheckerProgram.TopLevelDeclarations.Add(decl);
+ }
+ foreach (Variable v in linearTypeChecker.program.GlobalVariables())
+ {
+ this.moverCheckerProgram.TopLevelDeclarations.Add(v);
+ }
+ }
+ private sealed class MySubstituter : Duplicator
+ {
+ private readonly Substitution outsideOld;
+ private readonly Substitution insideOld;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(insideOld != null);
+ }
+
+ public MySubstituter(Substitution outsideOld, Substitution insideOld)
+ : base()
+ {
+ Contract.Requires(outsideOld != null && insideOld != null);
+ this.outsideOld = outsideOld;
+ this.insideOld = insideOld;
+ }
+
+ private bool insideOldExpr = false;
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ Expr e = null;
+
+ if (insideOldExpr)
+ {
+ e = insideOld(node.Decl);
+ }
+ else
+ {
+ e = outsideOld(node.Decl);
+ }
+ return e == null ? base.VisitIdentifierExpr(node) : e;
+ }
+
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ bool previouslyInOld = insideOldExpr;
+ insideOldExpr = true;
+ Expr tmp = (Expr)this.Visit(node.Expr);
+ OldExpr e = new OldExpr(node.tok, tmp);
+ insideOldExpr = previouslyInOld;
+ return e;
+ }
+ }
+
+ enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ class ActionInfo
+ {
+ public Procedure proc;
+ public MoverType moverType;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+
+ public bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType)
+ {
+ this.proc = proc;
+ this.moverType = moverType;
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, assertCmd.Expr);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true);
+ this.thatInParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ this.thatOutParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ List<Variable> otherLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ otherLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnExprCmd(block.TransferCmd.tok, Expr.True);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(otherLocVars, otherBlocks);
+ }
+ }
+
+ public static void AddCheckers(LinearTypeChecker linearTypeChecker)
+ {
+ Program program = linearTypeChecker.program;
+ List<ActionInfo> gatedActions = new List<ActionInfo>();
+ foreach (Declaration decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ foreach (Ensures e in proc.Ensures)
+ {
+ MoverType moverType = GetMoverType(e);
+ if (moverType == MoverType.Top) continue;
+ CodeExpr codeExpr = e.Condition as CodeExpr;
+ if (codeExpr == null)
+ {
+ Console.WriteLine("Warning: an atomic action must be a CodeExpr");
+ continue;
+ }
+ ActionInfo info = new ActionInfo(proc, codeExpr, moverType);
+ gatedActions.Add(info);
+ }
+ }
+ if (gatedActions.Count == 0)
+ return;
+ MoverChecking moverChecking = new MoverChecking(linearTypeChecker);
+ foreach (ActionInfo first in gatedActions)
+ {
+ Debug.Assert(first.moverType != MoverType.Top);
+ if (first.moverType == MoverType.Atomic)
+ continue;
+ foreach (ActionInfo second in gatedActions)
+ {
+ if (first.IsRightMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, first, second);
+ moverChecking.CreateGatePreservationChecker(program, second, first);
+ }
+ if (first.IsLeftMover)
+ {
+ moverChecking.CreateCommutativityChecker(program, second, first);
+ moverChecking.CreateGatePreservationChecker(program, first, second);
+ moverChecking.CreateFailurePreservationChecker(program, second, first);
+ }
+ }
+ }
+ var eraser = new LinearEraser();
+ eraser.VisitProgram(moverChecking.moverCheckerProgram);
+ {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ using (TokenTextWriter writer = new TokenTextWriter("MoverChecker.bpl", false))
+ {
+ if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)
+ {
+ writer.WriteLine("// " + CommandLineOptions.Clo.Version);
+ writer.WriteLine("// " + CommandLineOptions.Clo.Environment);
+ }
+ writer.WriteLine();
+ moverChecking.moverCheckerProgram.Emit(writer);
+ }
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ }
+
+ private static MoverType GetMoverType(Ensures e)
+ {
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
+ return MoverType.Atomic;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ return MoverType.Right;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ return MoverType.Left;
+ else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ return MoverType.Both;
+ else
+ return MoverType.Top;
+ }
+
+ class TransitionRelationComputation
+ {
+ private Program program;
+ private ActionInfo first;
+ private ActionInfo second;
+ private Stack<Block> dfsStack;
+ private Expr transitionRelation;
+
+ public TransitionRelationComputation(Program program, ActionInfo second)
+ {
+ this.program = program;
+ this.first = null;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
+ {
+ this.program = program;
+ this.first = first;
+ this.second = second;
+ this.dfsStack = new Stack<Block>();
+ this.transitionRelation = Expr.False;
+ }
+
+ public Expr Compute()
+ {
+ Search(second.thatAction.Blocks[0], false);
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ if (first != null)
+ {
+ foreach (Variable v in first.thisAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type));
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ boundVars.Add(bv);
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ if (boundVars.Count > 0)
+ return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation));
+ else
+ return transitionRelation;
+ }
+
+ private Expr CalculatePathCondition()
+ {
+ Expr returnExpr = Expr.True;
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ if (first != null)
+ {
+ foreach (Variable v in first.thisOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));
+ returnExpr = Expr.And(eqExpr, returnExpr);
+ }
+ Block[] dfsStackAsArray = dfsStack.Reverse().ToArray();
+ for (int i = dfsStackAsArray.Length - 1; i >= 0; i--)
+ {
+ Block b = dfsStackAsArray[i];
+ for (int j = b.Cmds.Count - 1; j >= 0; j--)
+ {
+ Cmd cmd = b.Cmds[j];
+ if (cmd is AssumeCmd)
+ {
+ AssumeCmd assumeCmd = cmd as AssumeCmd;
+ returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);
+ }
+ else if (cmd is AssignCmd)
+ {
+ AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ for (int k = 0; k < assignCmd.Lhss.Count; k++)
+ {
+ map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
+ }
+ Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(map);
+ returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr);
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+ }
+ return returnExpr;
+ }
+
+ private void Search(Block b, bool inFirst)
+ {
+ dfsStack.Push(b);
+ if (b.TransferCmd is ReturnExprCmd)
+ {
+ if (first == null || inFirst)
+ {
+ transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());
+ }
+ else
+ {
+ Search(first.thisAction.Blocks[0], true);
+ }
+ }
+ else
+ {
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ Search(target, inFirst);
+ }
+ }
+ dfsStack.Pop();
+ }
+ }
+
+ private static List<Block> CloneBlocks(List<Block> blocks)
+ {
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> otherBlocks = new List<Block>();
+ foreach (Block block in blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(cmd);
+ }
+ Block otherBlock = new Block();
+ otherBlock.Cmds = otherCmds;
+ otherBlock.Label = block.Label;
+ otherBlocks.Add(otherBlock);
+ blockMap[block] = otherBlock;
+ }
+ foreach (Block block in blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ continue;
+ }
+ List<Block> otherGotoCmdLabelTargets = new List<Block>();
+ List<string> otherGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ otherGotoCmdLabelTargets.Add(blockMap[target]);
+ otherGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
+ }
+ return otherBlocks;
+ }
+
+ private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)
+ {
+ List<Requires> requires = new List<Requires>();
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ }
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (Variable v in first.thisInParams)
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ for (int i = 0; i < second.thatInParams.Count; i++)
+ {
+ var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(second.thatInParams[i]);
+ }
+ foreach (string domainName in domainNameToScope.Keys)
+ {
+ requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ return requires;
+ }
+
+ private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (commutativityCheckerCache.Contains(actionPair))
+ return;
+ commutativityCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(first.thisAction.LocVars);
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> firstBlocks = CloneBlocks(first.thisAction.Blocks);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ foreach (Block b in firstBlocks)
+ {
+ if (b.TransferCmd is ReturnCmd)
+ {
+ List<Block> bs = new List<Block>();
+ bs.Add(secondBlocks[0]);
+ List<string> ls = new List<string>();
+ ls.Add(secondBlocks[0].Label);
+ b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
+ }
+ }
+ List<Block> blocks = new List<Block>();
+ blocks.AddRange(firstBlocks);
+ blocks.AddRange(secondBlocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();
+ ensures.Add(new Ensures(false, transitionRelation));
+ string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+
+ private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (gatePreservationCheckerCache.Contains(actionPair))
+ return;
+ gatePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+ List<Variable> outputs = new List<Variable>();
+ outputs.AddRange(first.thisOutParams);
+ outputs.AddRange(second.thatOutParams);
+ List<Variable> locals = new List<Variable>();
+ locals.AddRange(second.thatAction.LocVars);
+ List<Block> secondBlocks = CloneBlocks(second.thatAction.Blocks);
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ List<Ensures> ensures = new List<Ensures>();
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ ensures.Add(new Ensures(false, assertCmd.Expr));
+ }
+ string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+
+ private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ {
+ Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ if (failurePreservationCheckerCache.Contains(actionPair))
+ return;
+ failurePreservationCheckerCache.Add(actionPair);
+
+ List<Variable> inputs = new List<Variable>();
+ inputs.AddRange(first.thisInParams);
+ inputs.AddRange(second.thatInParams);
+
+ Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();
+ Expr expr = Expr.True;
+ foreach (AssertCmd assertCmd in first.thisGate)
+ {
+ expr = Expr.And(assertCmd.Expr, expr);
+ }
+ List<Requires> requires = DisjointnessRequires(program, first, second);
+ requires.Add(new Requires(false, Expr.Not(expr)));
+ foreach (AssertCmd assertCmd in second.thatGate)
+ {
+ requires.Add(new Requires(false, assertCmd.Expr));
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();
+ List<Variable> boundVars = new List<Variable>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ foreach (Variable v in second.thatOutParams)
+ {
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ map[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+ }
+ foreach (Variable v in second.thatAction.LocVars)
+ {
+ BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));
+ boundVars.Add(bv);
+ oldMap[v] = new IdentifierExpr(Token.NoToken, bv);
+ }
+
+ Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr));
+ if (boundVars.Count > 0)
+ {
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);
+ ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, (Expr)new MySubstituter(subst, oldSubst).Visit(ensuresExpr));
+ }
+ List<Ensures> ensures = new List<Ensures>();
+ ensures.Add(new Ensures(false, ensuresExpr));
+ List<Block> blocks = new List<Block>();
+ blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
+ string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
+ Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, new List<IdentifierExpr>(), ensures);
+ Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+ impl.Proc = proc;
+ this.moverCheckerProgram.TopLevelDeclarations.Add(impl);
+ this.moverCheckerProgram.TopLevelDeclarations.Add(proc);
+ }
+ }
+}
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs new file mode 100644 index 00000000..4f0c7a4b --- /dev/null +++ b/Source/Concurrency/OwickiGries.cs @@ -0,0 +1,738 @@ +using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.Boogie;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie
+{
+ public class OwickiGriesTransform
+ {
+ List<IdentifierExpr> globalMods;
+ LinearTypeChecker linearTypeChecker;
+ Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
+ List<Procedure> yieldCheckerProcs;
+ List<Implementation> yieldCheckerImpls;
+ Procedure yieldProc;
+
+ public OwickiGriesTransform(LinearTypeChecker linearTypeChecker)
+ {
+ this.linearTypeChecker = linearTypeChecker;
+ Program program = linearTypeChecker.program;
+ globalMods = new List<IdentifierExpr>();
+ foreach (Variable g in program.GlobalVariables())
+ {
+ globalMods.Add(new IdentifierExpr(Token.NoToken, g));
+ }
+ asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
+ yieldCheckerProcs = new List<Procedure>();
+ yieldCheckerImpls = new List<Implementation>();
+ yieldProc = null;
+ }
+
+ private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+ {
+ List<Expr> exprSeq = new List<Expr>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
+ }
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
+ }
+ if (yieldProc == null)
+ {
+ List<Variable> inputs = new List<Variable>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ inputs.Add(f);
+ }
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
+ inputs.Add(f);
+ }
+ yieldProc = new Procedure(Token.NoToken, "og_yield", new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
+ yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ }
+ CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
+ yieldCallCmd.Proc = yieldProc;
+ newCmds.Add(yieldCallCmd);
+ }
+
+ private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
+ {
+ Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ domainNameToExpr[domainName] = expr;
+ }
+ foreach (Variable v in availableLinearVars)
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ var domain = linearTypeChecker.linearDomains[domainName];
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ expr.Resolve(new ResolutionContext(null));
+ expr.Typecheck(new TypecheckingContext(null));
+ domainNameToExpr[domainName] = expr;
+ }
+ return domainNameToExpr;
+ }
+
+ private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
+ {
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));
+ rhss.Add(domainNameToExpr[domainName]);
+ }
+ foreach (Variable g in ogOldGlobalMap.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
+ rhss.Add(new IdentifierExpr(Token.NoToken, g));
+ }
+ if (lhss.Count > 0)
+ {
+ newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+ }
+ }
+
+ private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+
+ if (globalMods.Count > 0)
+ {
+ newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
+ }
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[yieldCmd], domainNameToInputVar);
+ AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+
+ for (int j = 0; j < cmds.Count; j++)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmds[j];
+ newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
+ }
+ }
+
+ public Procedure DesugarParallelCallCmd(CallCmd callCmd, out List<Expr> ins, out List<IdentifierExpr> outs)
+ {
+ List<string> parallelCalleeNames = new List<string>();
+ CallCmd iter = callCmd;
+ ins = new List<Expr>();
+ outs = new List<IdentifierExpr>();
+ while (iter != null)
+ {
+ parallelCalleeNames.Add(iter.Proc.Name);
+ ins.AddRange(iter.Ins);
+ outs.AddRange(iter.Outs);
+ iter = iter.InParallelWith;
+ }
+ parallelCalleeNames.Sort();
+ string procName = "og";
+ foreach (string calleeName in parallelCalleeNames)
+ {
+ procName = procName + "_" + calleeName;
+ }
+ if (asyncAndParallelCallDesugarings.ContainsKey(procName))
+ return asyncAndParallelCallDesugarings[procName];
+
+ List<Variable> inParams = new List<Variable>();
+ List<Variable> outParams = new List<Variable>();
+ List<Requires> requiresSeq = new List<Requires>();
+ List<Ensures> ensuresSeq = new List<Ensures>();
+ int count = 0;
+ while (callCmd != null)
+ {
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in callCmd.Proc.InParams)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true);
+ inParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ foreach (Variable x in callCmd.Proc.OutParams)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false);
+ outParams.Add(y);
+ map[x] = new IdentifierExpr(Token.NoToken, y);
+ }
+ Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (Requires req in callCmd.Proc.Requires)
+ {
+ requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition)));
+ }
+ foreach (Ensures ens in callCmd.Proc.Ensures)
+ {
+ ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition)));
+ }
+ count++;
+ callCmd = callCmd.InParallelWith;
+ }
+
+ Procedure proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
+ proc.AddAttribute("yields");
+ asyncAndParallelCallDesugarings[procName] = proc;
+ return proc;
+ }
+
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)
+ {
+ if (yields.Count == 0) return;
+
+ Program program = linearTypeChecker.program;
+ List<Variable> locals = new List<Variable>();
+ List<Variable> inputs = new List<Variable>();
+ foreach (IdentifierExpr ie in map.Values)
+ {
+ locals.Add(ie.Decl);
+ }
+ for (int i = 0; i < decl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
+ {
+ Variable inParam = decl.InParams[i];
+ Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
+ locals.Add(copy);
+ map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ {
+ int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ Variable inParam = decl.InParams[i];
+ Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
+ inputs.Add(copy);
+ map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
+ i++;
+ }
+ }
+ for (int i = 0; i < decl.OutParams.Count; i++)
+ {
+ Variable outParam = decl.OutParams[i];
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
+ locals.Add(copy);
+ map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Variable g = ie.Decl;
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
+ locals.Add(copy);
+ ogOldLocalMap[g] = Expr.Ident(copy);
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);
+ inputs.Add(f);
+ assumeMap[g] = Expr.Ident(f);
+ }
+
+ Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
+ Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ List<Block> yieldCheckerBlocks = new List<Block>();
+ List<String> labels = new List<String>();
+ List<Block> labelTargets = new List<Block>();
+ Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ labels.Add(yieldCheckerBlock.Label);
+ labelTargets.Add(yieldCheckerBlock);
+ yieldCheckerBlocks.Add(yieldCheckerBlock);
+ int yieldCount = 0;
+ foreach (List<Cmd> cs in yields)
+ {
+ var linearDomains = linearTypeChecker.linearDomains;
+ List<Cmd> newCmds = new List<Cmd>();
+ foreach (Cmd cmd in cs)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
+ }
+ foreach (Cmd cmd in cs)
+ {
+ PredicateCmd predCmd = (PredicateCmd)cmd;
+ var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
+ if (predCmd is AssertCmd)
+ newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes));
+ else
+ newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
+ }
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
+ yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
+ labels.Add(yieldCheckerBlock.Label);
+ labelTargets.Add(yieldCheckerBlock);
+ yieldCheckerBlocks.Add(yieldCheckerBlock);
+ }
+ yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
+
+ // Create the yield checker procedure
+ var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);
+ var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
+ yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ yieldCheckerProcs.Add(yieldCheckerProc);
+
+ // Create the yield checker implementation
+ var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);
+ yieldCheckerImpl.Proc = yieldCheckerProc;
+ yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ yieldCheckerImpls.Add(yieldCheckerImpl);
+ }
+
+ private bool IsYieldingHeader(GraphUtil.Graph<Block> graph, Block header)
+ {
+ foreach (Block backEdgeNode in graph.BackEdgeNodes(header))
+ {
+ foreach (Block x in graph.NaturalLoops(header, backEdgeNode))
+ {
+ foreach (Cmd cmd in x.Cmds)
+ {
+ if (cmd is YieldCmd)
+ return true;
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd == null) continue;
+ if (callCmd.IsAsync || callCmd.InParallelWith != null || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ private void TransformImpl(Implementation impl)
+ {
+ if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return;
+
+ TransformProc(impl.Proc);
+
+ // Find the yielding loop headers
+ impl.PruneUnreachableBlocks();
+ impl.ComputePredecessorsForBlocks();
+ GraphUtil.Graph<Block> graph = Program.GraphFromImpl(impl);
+ graph.ComputeLoops();
+ if (!graph.Reducible)
+ {
+ throw new Exception("Irreducible flow graphs are unsupported.");
+ }
+ HashSet<Block> yieldingHeaders = new HashSet<Block>();
+ IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();
+ foreach (Block header in sortedHeaders)
+ {
+ if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))
+ {
+ yieldingHeaders.Add(header);
+ }
+ else if (IsYieldingHeader(graph, header))
+ {
+ yieldingHeaders.Add(header);
+ }
+ else
+ {
+ continue;
+ }
+ }
+
+ Program program = linearTypeChecker.program;
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable local in impl.LocVars)
+ {
+ var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
+ map[local] = new IdentifierExpr(Token.NoToken, copy);
+ }
+ Dictionary<Variable, Variable> ogOldGlobalMap = new Dictionary<Variable, Variable>();
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Variable g = ie.Decl;
+ LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
+ ogOldGlobalMap[g] = l;
+ impl.LocVars.Add(l);
+ }
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();
+ {
+ int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ Variable inParam = impl.InParams[i];
+ domainNameToInputVar[domainName] = inParam;
+ Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
+ domainNameToLocalVar[domainName] = l;
+ impl.LocVars.Add(l);
+ i++;
+ }
+ }
+
+ // Collect the yield predicates and desugar yields
+ List<List<Cmd>> yields = new List<List<Cmd>>();
+ List<Cmd> cmds = new List<Cmd>();
+ foreach (Block b in impl.Blocks)
+ {
+ YieldCmd yieldCmd = null;
+ List<Cmd> newCmds = new List<Cmd>();
+ for (int i = 0; i < b.Cmds.Count; i++)
+ {
+ Cmd cmd = b.Cmds[i];
+ if (cmd is YieldCmd)
+ {
+ yieldCmd = (YieldCmd)cmd;
+ continue;
+ }
+ if (yieldCmd != null)
+ {
+ PredicateCmd pcmd = cmd as PredicateCmd;
+ if (pcmd == null)
+ {
+ DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
+ if (cmds.Count > 0)
+ {
+ yields.Add(cmds);
+ cmds = new List<Cmd>();
+ }
+ yieldCmd = null;
+ }
+ else
+ {
+ cmds.Add(pcmd);
+ }
+ }
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd != null)
+ {
+ if (callCmd.InParallelWith != null || callCmd.IsAsync ||
+ QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ }
+ if (callCmd.InParallelWith != null)
+ {
+ List<Expr> ins;
+ List<IdentifierExpr> outs;
+ Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);
+ dummyCallCmd.Proc = dummyParallelCallDesugaring;
+ newCmds.Add(dummyCallCmd);
+ }
+ else if (callCmd.IsAsync)
+ {
+ if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
+ {
+ asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
+ }
+ var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
+ CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);
+ dummyCallCmd.Proc = dummyAsyncTargetProc;
+ newCmds.Add(dummyCallCmd);
+ }
+ else
+ {
+ newCmds.Add(callCmd);
+ }
+ if (callCmd.InParallelWith != null || callCmd.IsAsync ||
+ QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ {
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypeChecker.availableLinearVars[callCmd]);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;
+ availableLinearVars.Add(ie.Decl);
+ }
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
+ AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+ }
+ }
+ else
+ {
+ newCmds.Add(cmd);
+ }
+ }
+ if (yieldCmd != null)
+ {
+ DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
+ if (cmds.Count > 0)
+ {
+ yields.Add(cmds);
+ cmds = new List<Cmd>();
+ }
+ }
+ if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ {
+ AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
+ }
+ b.Cmds = newCmds;
+ }
+
+ foreach (Block header in yieldingHeaders)
+ {
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypeChecker.availableLinearVars[header], domainNameToInputVar);
+ foreach (Block pred in header.Predecessors)
+ {
+ AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
+ AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
+ }
+ List<Cmd> newCmds = new List<Cmd>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
+ }
+ foreach (Variable v in ogOldGlobalMap.Keys)
+ {
+ newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v]))));
+ }
+ newCmds.AddRange(header.Cmds);
+ header.Cmds = newCmds;
+ }
+
+ {
+ // Add initial block
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ List<Expr> rhss = new List<Expr>();
+ Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
+ }
+ for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
+ {
+ Variable v = impl.InParams[i];
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ var domain = linearTypeChecker.linearDomains[domainName];
+ IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);
+ domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });
+ }
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));
+ rhss.Add(domainNameToExpr[domainName]);
+ }
+ foreach (Variable g in ogOldGlobalMap.Keys)
+ {
+ lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
+ rhss.Add(Expr.Ident(g));
+ }
+ if (lhss.Count > 0)
+ {
+ Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));
+ impl.Blocks.Insert(0, initBlock);
+ }
+ }
+
+ CreateYieldCheckerImpl(impl, yields, map);
+ }
+
+ public void TransformProc(Procedure proc)
+ {
+ if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return;
+
+ Program program = linearTypeChecker.program;
+ Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
+ {
+ int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ Variable inParam = proc.InParams[i];
+ domainNameToInputVar[domainName] = inParam;
+ i++;
+ }
+ }
+
+ // Collect the yield predicates and desugar yields
+ List<List<Cmd>> yields = new List<List<Cmd>>();
+ List<Cmd> cmds = new List<Cmd>();
+ if (proc.Requires.Count > 0)
+ {
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
+ }
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
+ {
+ Variable v = proc.InParams[i];
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ foreach (Requires r in proc.Requires)
+ {
+ if (r.Free)
+ {
+ cmds.Add(new AssumeCmd(r.tok, r.Condition));
+ }
+ else
+ {
+ cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes));
+ }
+ }
+ yields.Add(cmds);
+ cmds = new List<Cmd>();
+ }
+ if (proc.Ensures.Count > 0)
+ {
+ Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
+ foreach (var domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ domainNameToScope[domainName] = new HashSet<Variable>();
+ domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
+ }
+ foreach (Variable v in program.GlobalVariables())
+ {
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ for (int i = 0; i < proc.OutParams.Count; i++)
+ {
+ Variable v = proc.OutParams[i];
+ var domainName = linearTypeChecker.FindDomainName(v);
+ if (domainName == null) continue;
+ domainNameToScope[domainName].Add(v);
+ }
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
+ }
+ foreach (Ensures e in proc.Ensures)
+ {
+ if (e.Free)
+ {
+ cmds.Add(new AssumeCmd(e.tok, e.Condition));
+ }
+ else
+ {
+ cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes));
+ }
+ }
+ yields.Add(cmds);
+ cmds = new List<Cmd>();
+ }
+ CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
+ }
+
+ private void AddYieldProcAndImpl()
+ {
+ if (yieldProc == null) return;
+
+ Program program = linearTypeChecker.program;
+ List<Variable> inputs = new List<Variable>();
+ foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+ {
+ var domain = linearTypeChecker.linearDomains[domainName];
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
+ inputs.Add(f);
+ }
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
+ inputs.Add(f);
+ }
+ List<Block> blocks = new List<Block>();
+ TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
+ if (yieldCheckerProcs.Count > 0)
+ {
+ List<Block> blockTargets = new List<Block>();
+ List<String> labelTargets = new List<String>();
+ int labelCount = 0;
+ foreach (Procedure proc in yieldCheckerProcs)
+ {
+ List<Expr> exprSeq = new List<Expr>();
+ foreach (Variable v in inputs)
+ {
+ exprSeq.Add(new IdentifierExpr(Token.NoToken, v));
+ }
+ CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());
+ callCmd.Proc = proc;
+ string label = string.Format("L_{0}", labelCount++);
+ Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));
+ labelTargets.Add(label);
+ blockTargets.Add(block);
+ blocks.Add(block);
+ }
+ transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
+ }
+ blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));
+
+ var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
+ yieldImpl.Proc = yieldProc;
+ yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
+ program.TopLevelDeclarations.Add(yieldProc);
+ program.TopLevelDeclarations.Add(yieldImpl);
+ }
+
+ private QKeyValue RemoveYieldsAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveYieldsAttribute(iter.Next);
+ return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;
+ }
+
+ public void Transform()
+ {
+ MoverChecking.AddCheckers(linearTypeChecker);
+
+ Program program = linearTypeChecker.program;
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ TransformImpl(impl);
+ }
+ foreach (Procedure proc in yieldCheckerProcs)
+ {
+ program.TopLevelDeclarations.Add(proc);
+ }
+ foreach (Implementation impl in yieldCheckerImpls)
+ {
+ program.TopLevelDeclarations.Add(impl);
+ }
+ foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)
+ {
+ program.TopLevelDeclarations.Add(proc);
+ }
+ AddYieldProcAndImpl();
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+ {
+ HashSet<Variable> modifiedVars = new HashSet<Variable>();
+ proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
+ foreach (GlobalVariable g in program.GlobalVariables())
+ {
+ if (modifiedVars.Contains(g)) continue;
+ proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
+ }
+ proc.Attributes = RemoveYieldsAttribute(proc.Attributes);
+ }
+ }
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ impl.Attributes = RemoveYieldsAttribute(impl.Attributes);
+ }
+ }
+ }
+}
diff --git a/Source/Concurrency/Properties/AssemblyInfo.cs b/Source/Concurrency/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..48430488 --- /dev/null +++ b/Source/Concurrency/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("Concurrency")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("Concurrency")]
+[assembly: AssemblyCopyright("Copyright © 2013")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("867039c5-87dc-4f76-9f90-4f52afc90116")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
|