Skip to content

Commit

Permalink
Fixing while loops in linear types. Removing P samples from release b…
Browse files Browse the repository at this point in the history 
…uild
  • Loading branch information
Alex Reinking committed Dec 14, 2017
1 parent 8dfedc5 commit 9153956
Show file tree
Hide file tree
Showing 2 changed files with 59 additions and 64 deletions.
12 changes: 5 additions & 7 deletions P.sln
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@

Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 15
VisualStudioVersion = 15.0.26430.16
VisualStudioVersion = 15.0.27130.2003
MinimumVisualStudioVersion = 10.0.40219.1
Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "PrtWinUser", "Src\PrtDist\PrtWinUser.vcxproj", "{F8C72C0E-450C-4AE1-9885-31B8565C1D63}"
EndProject
Expand Down Expand Up @@ -110,6 +110,7 @@ Global
GlobalSection(ProjectConfigurationPlatforms) = postSolution
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Debug|Any CPU.ActiveCfg = Debug|Win32
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Debug|x64.ActiveCfg = Debug|x64
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Debug|x64.Build.0 = Debug|x64
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Debug|x86.ActiveCfg = Debug|Win32
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Debug|x86.Build.0 = Debug|Win32
{F8C72C0E-450C-4AE1-9885-31B8565C1D63}.Release|Any CPU.ActiveCfg = Release|Win32
Expand Down Expand Up @@ -163,7 +164,6 @@ Global
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Debug|x86.Build.0 = Debug|Win32
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Release|Any CPU.ActiveCfg = Release|Win32
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Release|x64.ActiveCfg = Release|x64
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Release|x64.Build.0 = Release|x64
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Release|x86.ActiveCfg = Release|Win32
{3EC51A08-22A0-4BB8-A784-6516F0DC1474}.Release|x86.Build.0 = Release|Win32
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Debug|Any CPU.ActiveCfg = Debug|Win32
Expand All @@ -172,7 +172,6 @@ Global
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Debug|x86.Build.0 = Debug|Win32
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Release|Any CPU.ActiveCfg = Release|Win32
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Release|x64.ActiveCfg = Release|x64
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Release|x64.Build.0 = Release|x64
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Release|x86.ActiveCfg = Release|Win32
{65DF9D53-1461-43AE-9A50-43E7C4D55E05}.Release|x86.Build.0 = Release|Win32
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Debug|Any CPU.ActiveCfg = Debug|Win32
Expand All @@ -181,7 +180,6 @@ Global
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Debug|x86.Build.0 = Debug|Win32
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Release|Any CPU.ActiveCfg = Release|Win32
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Release|x64.ActiveCfg = Release|x64
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Release|x64.Build.0 = Release|x64
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Release|x86.ActiveCfg = Release|Win32
{A57EA5EE-934D-41ED-9670-18AF76C52A96}.Release|x86.Build.0 = Release|Win32
{1454DADA-E822-43A6-B523-5F0C992D17F5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
Expand All @@ -202,7 +200,6 @@ Global
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Debug|x86.Build.0 = Debug|Win32
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Release|Any CPU.ActiveCfg = Release|Win32
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Release|x64.ActiveCfg = Release|x64
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Release|x64.Build.0 = Release|x64
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Release|x86.ActiveCfg = Release|Win32
{21BB07E5-A4E6-4BD3-AFC4-61B13BB0B667}.Release|x86.Build.0 = Release|Win32
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Debug|Any CPU.ActiveCfg = Debug|Win32
Expand All @@ -211,7 +208,6 @@ Global
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Debug|x86.Build.0 = Debug|Win32
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Release|Any CPU.ActiveCfg = Release|Win32
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Release|x64.ActiveCfg = Release|x64
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Release|x64.Build.0 = Release|x64
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Release|x86.ActiveCfg = Release|Win32
{2010A7BF-C537-4311-9EE6-34DB5D9464B5}.Release|x86.Build.0 = Release|Win32
{9F8DE18D-C64B-4D30-9CFF-6793FFEAFC04}.Debug|Any CPU.ActiveCfg = Debug|x86
Expand Down Expand Up @@ -284,7 +280,6 @@ Global
{25142DD0-BC85-4156-8691-416FF932D341}.Debug|x86.Build.0 = Debug|Win32
{25142DD0-BC85-4156-8691-416FF932D341}.Release|Any CPU.ActiveCfg = Release|Win32
{25142DD0-BC85-4156-8691-416FF932D341}.Release|x64.ActiveCfg = Release|x64
{25142DD0-BC85-4156-8691-416FF932D341}.Release|x64.Build.0 = Release|x64
{25142DD0-BC85-4156-8691-416FF932D341}.Release|x86.ActiveCfg = Release|Win32
{25142DD0-BC85-4156-8691-416FF932D341}.Release|x86.Build.0 = Release|Win32
{39B65065-C655-42E9-BE97-277A2BE471FE}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
Expand Down Expand Up @@ -337,4 +332,7 @@ Global
{39B65065-C655-42E9-BE97-277A2BE471FE} = {6B36C087-8924-4B31-BE1F-91837CED42A5}
{71691381-D3C9-478C-BA37-A94032A536DF} = {31FBBC4D-8756-4D60-B8D5-ED9E0FC8D4C1}
EndGlobalSection
GlobalSection(ExtensibilityGlobals) = postSolution
SolutionGuid = {BD6B0E25-71B7-4A8F-8D0F-946BA6D47C7C}
EndGlobalSection
EndGlobal
111 changes: 54 additions & 57 deletions Src/Pc/Compiler/TypeChecker/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ public static void AnalyzeMethods(ITranslationErrorHandler handler, IEnumerable<

private void CheckFunction(Function method)
{
ISet<Variable> unavailable = ProcessStatement(method.Body, new HashSet<Variable>());
ISet<Variable> unavailable = ProcessStatement(new HashSet<Variable>(), method.Body);
allUnavailableParams.UnionWith(unavailable.Where(var => var.Role.Equals(VariableRole.Param)));
}

Expand Down Expand Up @@ -64,39 +64,36 @@ private void CheckFunctionCall(Function function, IEnumerable<IPExpr> arguments)
}
}

private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavailable)
private ISet<Variable> ProcessStatement(ISet<Variable> unavailable, IPStmt statement)
{
switch (statement)
{
case null:
throw new ArgumentOutOfRangeException(nameof(statement));
case CompoundStmt compoundStmt:
foreach (IPStmt stmtStatement in compoundStmt.Statements)
{
unavailable = ProcessStatement(stmtStatement, unavailable);
}
unavailable = compoundStmt.Statements.Aggregate(unavailable, ProcessStatement);
break;
case AssertStmt assertStmt:
unavailable = ProcessExpr(assertStmt.Assertion, unavailable);
unavailable = ProcessExpr(unavailable, assertStmt.Assertion);
break;
case PrintStmt printStmt:
unavailable = ProcessArgList(printStmt.Args, unavailable, false);
break;
case ReturnStmt returnStmt:
if (returnStmt.ReturnValue != null)
{
unavailable = ProcessExpr(returnStmt.ReturnValue, unavailable);
unavailable = ProcessExpr(unavailable, returnStmt.ReturnValue);
}
break;
case AssignStmt assignStmt:
unavailable = ProcessExpr(assignStmt.Value, unavailable);
unavailable = ProcessExpr(unavailable, assignStmt.Value);
if (assignStmt.Variable is VariableAccessExpr assignAccess)
{
unavailable.Remove(assignAccess.Variable);
}
else
{
unavailable = ProcessExpr(assignStmt.Variable, unavailable);
unavailable = ProcessExpr(unavailable, assignStmt.Variable);
}
break;
case MoveAssignStmt moveAssignStmt:
Expand All @@ -112,7 +109,7 @@ private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavail
}
else
{
unavailable = ProcessExpr(moveAssignStmt.ToLocation, unavailable);
unavailable = ProcessExpr(unavailable, moveAssignStmt.ToLocation);
}
break;
case SwapAssignStmt swapAssignStmt:
Expand All @@ -127,7 +124,7 @@ private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavail
}
else
{
unavailable = ProcessExpr(swapAssignStmt.NewLocation, unavailable);
unavailable = ProcessExpr(unavailable, swapAssignStmt.NewLocation);
}

if (unavailable.Contains(swapAssignStmt.OldLocation) ||
Expand All @@ -138,30 +135,34 @@ private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavail
}
break;
case InsertStmt insertStmt:
unavailable = ProcessExpr(insertStmt.Variable, unavailable);
unavailable = ProcessExpr(insertStmt.Index, unavailable);
unavailable = ProcessExpr(insertStmt.Value, unavailable);
unavailable = ProcessExpr(unavailable, insertStmt.Variable);
unavailable = ProcessExpr(unavailable, insertStmt.Index);
unavailable = ProcessExpr(unavailable, insertStmt.Value);
break;
case RemoveStmt removeStmt:
unavailable = ProcessExpr(removeStmt.Variable, unavailable);
unavailable = ProcessExpr(removeStmt.Value, unavailable);
unavailable = ProcessExpr(unavailable, removeStmt.Variable);
unavailable = ProcessExpr(unavailable, removeStmt.Value);
break;
case WhileStmt whileStmt:
unavailable = ProcessExpr(whileStmt.Condition, unavailable);
unavailable = ProcessExpr(unavailable, whileStmt.Condition);
// process running the body twice. on the first go, the loop can potentially relinquish additional variables
// on the second go, either the body will use one of these variables and throw or reach a fixed point since all
// paths are considered simultaneously. Then, we continue our overapproximation by taking the union of no runs
// and one or more runs.
ISet<Variable> bodyUnavailable =
ProcessStatement(whileStmt.Body, new HashSet<Variable>(unavailable));
bodyUnavailable = ProcessExpr(whileStmt.Condition, bodyUnavailable);
if (bodyUnavailable.IsProperSupersetOf(unavailable))
{
throw handler.IssueError(null, "while loops must not relinquish variables");
}
ProcessStatement(new HashSet<Variable>(unavailable), whileStmt.Body);
bodyUnavailable = ProcessExpr(bodyUnavailable, whileStmt.Condition);
// TODO: more efficient way of doing this?
bodyUnavailable = ProcessStatement(bodyUnavailable, whileStmt.Body);
bodyUnavailable = ProcessExpr(bodyUnavailable, whileStmt.Condition);
unavailable.UnionWith(bodyUnavailable);
break;
case IfStmt ifStmt:
unavailable = ProcessExpr(ifStmt.Condition, unavailable);
unavailable = ProcessExpr(unavailable, ifStmt.Condition);
ISet<Variable> thenUnavailable =
ProcessStatement(ifStmt.ThenBranch, new HashSet<Variable>(unavailable));
ProcessStatement(new HashSet<Variable>(unavailable), ifStmt.ThenBranch);
ISet<Variable> elseUnavailable =
ProcessStatement(ifStmt.ElseBranch, new HashSet<Variable>(unavailable));
ProcessStatement(new HashSet<Variable>(unavailable), ifStmt.ElseBranch);
thenUnavailable.UnionWith(elseUnavailable);
unavailable = thenUnavailable;
break;
Expand All @@ -173,25 +174,25 @@ private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavail
funCallStmts.Add(funCallStmt);
break;
case RaiseStmt raiseStmt:
unavailable = ProcessExpr(raiseStmt.PEvent, unavailable);
unavailable = ProcessExpr(unavailable, raiseStmt.PEvent);
unavailable = ProcessArgList(raiseStmt.Payload, unavailable, false);
break;
case SendStmt sendStmt:
unavailable = ProcessExpr(sendStmt.MachineExpr, unavailable);
unavailable = ProcessExpr(sendStmt.Evt, unavailable);
unavailable = ProcessExpr(unavailable, sendStmt.MachineExpr);
unavailable = ProcessExpr(unavailable, sendStmt.Evt);
unavailable = ProcessArgList(sendStmt.ArgsList, unavailable, false);
break;
case AnnounceStmt announceStmt:
unavailable = ProcessExpr(announceStmt.PEvent, unavailable);
unavailable = ProcessExpr(unavailable, announceStmt.PEvent);
if (announceStmt.Payload != null)
{
unavailable = ProcessExpr(announceStmt.Payload, unavailable);
unavailable = ProcessExpr(unavailable, announceStmt.Payload);
}
break;
case GotoStmt gotoStmt:
if (gotoStmt.Payload != null)
{
unavailable = ProcessExpr(gotoStmt.Payload, unavailable);
unavailable = ProcessExpr(unavailable, gotoStmt.Payload);
}
break;
case ReceiveStmt receiveStmt:
Expand All @@ -200,7 +201,7 @@ private ISet<Variable> ProcessStatement(IPStmt statement, ISet<Variable> unavail
foreach (KeyValuePair<PEvent, Function> recvCase in receiveStmt.Cases)
{
ISet<Variable> caseUnavailable =
ProcessStatement(recvCase.Value.Body, new HashSet<Variable>(unavailable));
ProcessStatement(new HashSet<Variable>(unavailable), recvCase.Value.Body);
postUnavailable.UnionWith(caseUnavailable);
caseVariables.UnionWith(recvCase.Value.Signature.Parameters);
}
Expand Down Expand Up @@ -233,31 +234,27 @@ private ISet<Variable> ProcessArgList(IEnumerable<IPExpr> arguments, ISet<Variab
}
else
{
unavailable = ProcessExpr(argument, unavailable);
unavailable = ProcessExpr(unavailable, argument);
}
}
foreach (ILinearRef linearRef in remainingLinearRefs)
{
unavailable = ProcessExpr(linearRef, unavailable);
}
return unavailable;
return remainingLinearRefs.Aggregate(unavailable, ProcessExpr);
}

private ISet<Variable> ProcessExpr(IPExpr expression, ISet<Variable> unavailable)
private ISet<Variable> ProcessExpr(ISet<Variable> unavailable, IPExpr expression)
{
switch (expression)
{
case null:
throw new ArgumentOutOfRangeException(nameof(expression));
case CastExpr castExpr:
unavailable = ProcessExpr(castExpr.SubExpr, unavailable);
unavailable = ProcessExpr(unavailable, castExpr.SubExpr);
break;
case CoerceExpr coerceExpr:
unavailable = ProcessExpr(coerceExpr.SubExpr, unavailable);
unavailable = ProcessExpr(unavailable, coerceExpr.SubExpr);
break;
case ContainsKeyExpr containsKeyExpr:
unavailable = ProcessExpr(containsKeyExpr.Map, unavailable);
unavailable = ProcessExpr(containsKeyExpr.Key, unavailable);
unavailable = ProcessExpr(unavailable, containsKeyExpr.Map);
unavailable = ProcessExpr(unavailable, containsKeyExpr.Key);
break;
case CtorExpr ctorExpr:
unavailable = ProcessArgList(ctorExpr.Arguments, unavailable, false);
Expand All @@ -267,7 +264,7 @@ private ISet<Variable> ProcessExpr(IPExpr expression, ISet<Variable> unavailable
funCallExprs.Add(funCallExpr);
break;
case KeysExpr keysExpr:
unavailable = ProcessExpr(keysExpr.Expr, unavailable);
unavailable = ProcessExpr(unavailable, keysExpr.Expr);
break;
case LinearAccessRefExpr linearAccessRefExpr:
if (unavailable.Contains(linearAccessRefExpr.Variable))
Expand All @@ -280,37 +277,37 @@ private ISet<Variable> ProcessExpr(IPExpr expression, ISet<Variable> unavailable
}
break;
case UnaryOpExpr unaryOp:
unavailable = ProcessExpr(unaryOp.SubExpr, unavailable);
unavailable = ProcessExpr(unavailable, unaryOp.SubExpr);
break;
case MapAccessExpr mapAccessExpr:
unavailable = ProcessExpr(mapAccessExpr.MapExpr, unavailable);
unavailable = ProcessExpr(mapAccessExpr.IndexExpr, unavailable);
unavailable = ProcessExpr(unavailable, mapAccessExpr.MapExpr);
unavailable = ProcessExpr(unavailable, mapAccessExpr.IndexExpr);
break;
case BinOpExpr binOp:
unavailable = ProcessExpr(binOp.Lhs, unavailable);
unavailable = ProcessExpr(binOp.Rhs, unavailable);
unavailable = ProcessExpr(unavailable, binOp.Lhs);
unavailable = ProcessExpr(unavailable, binOp.Rhs);
break;
case NamedTupleAccessExpr namedTupleAccessExpr:
unavailable = ProcessExpr(namedTupleAccessExpr.SubExpr, unavailable);
unavailable = ProcessExpr(unavailable, namedTupleAccessExpr.SubExpr);
break;
case NamedTupleExpr namedTupleExpr:
unavailable = ProcessArgList(namedTupleExpr.TupleFields, unavailable, false);
break;
case SeqAccessExpr seqAccessExpr:
unavailable = ProcessExpr(seqAccessExpr.SeqExpr, unavailable);
unavailable = ProcessExpr(seqAccessExpr.IndexExpr, unavailable);
unavailable = ProcessExpr(unavailable, seqAccessExpr.SeqExpr);
unavailable = ProcessExpr(unavailable, seqAccessExpr.IndexExpr);
break;
case SizeofExpr sizeofExpr:
unavailable = ProcessExpr(sizeofExpr.Expr, unavailable);
unavailable = ProcessExpr(unavailable, sizeofExpr.Expr);
break;
case TupleAccessExpr tupleAccessExpr:
unavailable = ProcessExpr(tupleAccessExpr.SubExpr, unavailable);
unavailable = ProcessExpr(unavailable, tupleAccessExpr.SubExpr);
break;
case UnnamedTupleExpr unnamedTupleExpr:
unavailable = ProcessArgList(unnamedTupleExpr.TupleFields, unavailable, false);
break;
case ValuesExpr valuesExpr:
unavailable = ProcessExpr(valuesExpr.Expr, unavailable);
unavailable = ProcessExpr(unavailable, valuesExpr.Expr);
break;
case VariableAccessExpr variableAccessExpr:
if (unavailable.Contains(variableAccessExpr.Variable))
Expand Down

0 comments on commit 9153956

Please sign in to comment.