Skip to content

Commit

Permalink
[clean-up] unnecessary option types (#761)
Browse files Browse the repository at this point in the history
  • Loading branch information
AD1024 authored Aug 20, 2024
1 parent 2011ffa commit 177ac07
Show file tree
Hide file tree
Showing 7 changed files with 51 additions and 39 deletions.
10 changes: 5 additions & 5 deletions Src/PCompiler/CompilerCore/Backend/CSharp/CSharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -657,7 +657,7 @@ private void WriteNamedFunctionWrapper(CompilationContext context, StringWriter
if (function.Role == FunctionRole.Method || function.Role == FunctionRole.Foreign)
return;

var isAsync = function.CanReceive == true;
var isAsync = function.CanReceive;
var signature = function.Signature;

var functionName = context.Names.GetNameForDecl(function);
Expand Down Expand Up @@ -701,7 +701,7 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
WriteNamedFunctionWrapper(context, output, function);
}

var isAsync = function.CanReceive == true;
var isAsync = function.CanReceive;
var signature = function.Signature;

var staticKeyword = isStatic ? "static " : "";
Expand Down Expand Up @@ -737,7 +737,7 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
WriteFunctionBody(context, output, function);

// for monitor
if (!(function.CanCreate == true || function.CanSend == true || function.IsNondeterministic == true || function.CanReceive == true))
if (!(function.CanCreate || function.CanSend || function.IsNondeterministic || function.CanReceive))
{
var functionParameters_monitor = functionParameters + string.Concat(seperator, "PMonitor currentMachine");
context.WriteLine(output,
Expand Down Expand Up @@ -889,7 +889,7 @@ private void WriteStmt(CompilationContext context, StringWriter output, Function

case FunCallStmt funCallStmt:
var isStatic = funCallStmt.Function.Owner == null;
var awaitMethod = funCallStmt.Function.CanReceive == true ? "await " : "";
var awaitMethod = funCallStmt.Function.CanReceive ? "await " : "";
var globalFunctionClass = isStatic ? $"{context.GlobalFunctionClassName}." : "";
context.Write(output,
$"{awaitMethod}{globalFunctionClass}{context.Names.GetNameForDecl(funCallStmt.Function)}(");
Expand Down Expand Up @@ -1413,7 +1413,7 @@ private void WriteExpr(CompilationContext context, StringWriter output, IPExpr p

case FunCallExpr funCallExpr:
var isStatic = funCallExpr.Function.Owner == null;
var awaitMethod = funCallExpr.Function.CanReceive == true ? "await " : "";
var awaitMethod = funCallExpr.Function.CanReceive ? "await " : "";
var globalFunctionClass = isStatic ? $"{context.GlobalFunctionClassName}." : "";
context.Write(output,
$"{awaitMethod}{globalFunctionClass}{context.Names.GetNameForDecl(funCallExpr.Function)}(");
Expand Down
6 changes: 3 additions & 3 deletions Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ private void WriteFunction(Function f)
return;
}

if (f.CanReceive == true)
if (f.CanReceive)
{
WriteLine($"// Async function {f.Name} elided");
return;
Expand Down Expand Up @@ -228,11 +228,11 @@ private void WriteFunctionSignature(Function f)
// If this function has exceptional control flow (for raising events or state transition)
// we need to annotate it appropriately.
var throwables = new List<string>();
if (f.CanChangeState == true)
if (f.CanChangeState)
{
throwables.Add("prt.exceptions.TransitionException");
}
if (f.CanRaiseEvent == true)
if (f.CanRaiseEvent)
{
throwables.Add("prt.exceptions.RaiseEventException");
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -466,9 +466,9 @@ private void WriteState(CompilationContext context, StringWriter output, State s
var entryFunc = state.Entry;
entryFunc.Name = $"{context.GetNameForDecl(state)}_entry";
context.Write(output, $"(({context.GetNameForDecl(entryFunc.Owner)})machine).{context.GetNameForDecl(entryFunc)}({entryPcScope.PathConstraintVar}, machine.getSendBuffer()");
if (entryFunc.CanChangeState ?? false)
if (entryFunc.CanChangeState)
context.Write(output, ", outcome");
else if (entryFunc.CanRaiseEvent ?? false)
else if (entryFunc.CanRaiseEvent)
context.Write(output, ", outcome");
if (entryFunc.Signature.Parameters.Any())
{
Expand All @@ -489,8 +489,8 @@ private void WriteState(CompilationContext context, StringWriter output, State s

var exitFunc = state.Exit;
exitFunc.Name = $"{context.GetNameForDecl(state)}_exit";
Debug.Assert(!(exitFunc.CanChangeState ?? false));
Debug.Assert(!(exitFunc.CanRaiseEvent ?? false));
Debug.Assert(!exitFunc.CanChangeState);
Debug.Assert(!exitFunc.CanRaiseEvent);
if (exitFunc.Signature.Parameters.Count() != 0)
throw new NotImplementedException("Exit functions with payloads are not yet supported");
context.WriteLine(output, $"(({context.GetNameForDecl(exitFunc.Owner)})machine).{context.GetNameForDecl(exitFunc)}(pc, machine.getSendBuffer());");
Expand All @@ -515,9 +515,9 @@ private void WriteEventHandler(CompilationContext context, StringWriter output,
if (actionFunc.Name == "")
actionFunc.Name = $"{context.GetNameForDecl(state)}_{eventTag}";
context.Write(output, $"(({context.GetNameForDecl(actionFunc.Owner)})machine).{context.GetNameForDecl(actionFunc)}(pc, machine.getSendBuffer()");
if (actionFunc.CanChangeState ?? false)
if (actionFunc.CanChangeState)
context.Write(output, ", outcome");
else if (actionFunc.CanRaiseEvent ?? false)
else if (actionFunc.CanRaiseEvent)
context.Write(output, ", outcome");
if (actionFunc.Signature.Parameters.Count() == 1)
{
Expand All @@ -541,8 +541,8 @@ private void WriteEventHandler(CompilationContext context, StringWriter output,
context.WriteLine(output, "@Override public void transitionFunction(Guard pc, Machine machine, UnionVS payload) {");

var transitionFunc = gotoState.TransitionFunction;
Debug.Assert(!(transitionFunc.CanChangeState ?? false));
Debug.Assert(!(transitionFunc.CanRaiseEvent ?? false));
Debug.Assert(!transitionFunc.CanChangeState);
Debug.Assert(!transitionFunc.CanRaiseEvent);
if (transitionFunc.Name == "")
transitionFunc.Name = $"{context.GetNameForDecl(state)}_{eventTag}_{destTag}";

Expand Down Expand Up @@ -598,7 +598,7 @@ internal ControlFlowContext FreshBranchSubContext(CompilationContext context)

private bool MayExitWithOutcome(Function func)
{
return (func.CanChangeState ?? false) || (func.CanRaiseEvent ?? false);
return func.CanChangeState || func.CanRaiseEvent;
}

private enum FunctionReturnConvention
Expand Down Expand Up @@ -631,7 +631,7 @@ private void WriteForeignFunction(CompilationContext context, StringWriter outpu
{
var isStatic = function.Owner == null;

if (function.CanReceive == true)
if (function.CanReceive)
throw new NotImplementedException($"Async functions {context.GetNameForDecl(function)} are not supported");

var staticKeyword = isStatic ? "static " : "";
Expand Down Expand Up @@ -714,13 +714,13 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
context.WriteLine(output, $"(");
context.WriteLine(output, $"Guard {rootPCScope.PathConstraintVar},");
context.Write(output, $"EventBuffer {CompilationContext.EffectCollectionVar}");
if (function.CanChangeState ?? false)
if (function.CanChangeState)
{
Debug.Assert(function.Owner != null);
context.WriteLine(output, ",");
context.Write(output, "EventHandlerReturnReason outcome");
}
else if (function.CanRaiseEvent ?? false)
else if (function.CanRaiseEvent)
{
context.WriteLine(output, ",");
context.Write(output, "EventHandlerReturnReason outcome");
Expand Down Expand Up @@ -1691,10 +1691,10 @@ private void WriteFunCallStmt(CompilationContext context, StringWriter output, C

context.Write(output, $"{context.GetNameForDecl(function)}({flowContext.pcScope.PathConstraintVar}, {CompilationContext.EffectCollectionVar}");

if (function.CanChangeState ?? false)
if (function.CanChangeState)
context.Write(output, ", outcome");

else if (function.CanRaiseEvent ?? false)
else if (function.CanRaiseEvent)
context.Write(output, ", outcome");


Expand Down
12 changes: 6 additions & 6 deletions Src/PCompiler/CompilerCore/Backend/Symbolic/TransformASTPass.cs
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ static private IPDecl TransformDecl(IPDecl decl)
if (function.IsForeign)
return function;
else
if (function.CanReceive == true)
if (function.CanReceive)
{
return null;
}
Expand Down Expand Up @@ -150,7 +150,7 @@ static private State TransformState(State state, IDictionary<Function, Function>

if (transformedState.Exit != null)
{
if (transformedState.Exit.CanReceive == true)
if (transformedState.Exit.CanReceive)
{
throw new NotImplementedException($"Receive in state exit functions are not supported, found in state {transformedState.Name} of machine {transformedState.OwningMachine.Name}");
}
Expand Down Expand Up @@ -281,7 +281,7 @@ static private void InlineStmt(Function function, IPStmt stmt, List<IPStmt> body
foreach (var statement in compound.Statements) InlineStmt(function, statement, body);
break;
case FunCallStmt call:
if ((!call.Function.IsForeign) & (call.Function.CanReceive == true))
if ((!call.Function.IsForeign) & (call.Function.CanReceive))
{
var inlined = InlineInFunction(call.Function);
if (inlined)
Expand Down Expand Up @@ -323,7 +323,7 @@ static private void InlineStmt(Function function, IPStmt stmt, List<IPStmt> body

static private bool InlineInFunction(Function function)
{
if (!function.Callees.Contains(function) && (function.CanReceive == true)) {
if (!function.Callees.Contains(function) && (function.CanReceive)) {
var body = new List<IPStmt>();
foreach (var stmt in function.Body.Statements)
{
Expand Down Expand Up @@ -606,7 +606,7 @@ static private IPStmt HandleReceives(IPStmt statement, Function function, Machin
var canReceiveInCase = false;
foreach (var c in recv.Cases)
{
if (c.Value.CanReceive == true)
if (c.Value.CanReceive)
{
canReceiveInCase = true;
if (c.Value.LocalVariables.Count() != 0)
Expand Down Expand Up @@ -659,7 +659,7 @@ static private IPStmt HandleReceives(IPStmt statement, Function function, Machin
}
}

if (canReceiveInCase == true && after != null)
if (canReceiveInCase && after != null)
{
var caseStmts = new List<IPStmt>();
var caseBody = c.Value.Body;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,22 @@ sourceNode is PParser.WhileStmtContext ||
sourceNode is PParser.ForeachStmtContext);
Name = name;
SourceLocation = sourceNode;
CanCreate = false;
CanSend = false;
IsNondeterministic = false;
CanReceive = false;
CanRaiseEvent = false;
CanChangeState = false;
}

public Function(ParserRuleContext sourceNode) : this("", sourceNode)
{
CanCreate = false;
CanSend = false;
IsNondeterministic = false;
CanReceive = false;
CanRaiseEvent = false;
CanChangeState = false;
}

public Machine Owner { get; set; }
Expand Down Expand Up @@ -93,14 +105,14 @@ public void RemoveCallee(Function callee)

public bool IsAnon => string.IsNullOrEmpty(Name);

public bool? CanChangeState { get; set; }
public bool? CanRaiseEvent { get; set; }
public bool? CanReceive { get; set; }
public bool CanChangeState { get; set; }
public bool CanRaiseEvent { get; set; }
public bool CanReceive { get; set; }

public bool? CanSend { get; set; }
public bool CanSend { get; set; }

public bool? CanCreate { get; set; }
public bool? IsNondeterministic { get; set; }
public bool CanCreate { get; set; }
public bool IsNondeterministic { get; set; }

public IEnumerable<Function> Callers => callers;
public IEnumerable<Function> Callees => callees;
Expand Down
6 changes: 3 additions & 3 deletions Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs
Original file line number Diff line number Diff line change
Expand Up @@ -57,13 +57,13 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
foreach (var function in allFunctions)
{
// This can been checked before but just doing it again for safety!
if (function.Owner?.IsSpec == true && (function.IsNondeterministic == true || function.CanCreate == true || function.CanSend == true|| function.CanReceive == true))
if (function.Owner?.IsSpec == true && (function.IsNondeterministic || function.CanCreate || function.CanSend || function.CanReceive))
{
throw handler.IllegalFunctionUsedInSpecMachine(function, function.Owner);
}

// A static function if it has side effects or is non-deterministic then it cannot be called from a spec machine
if (function.Owner == null && (function.IsNondeterministic == true || function.CanCreate == true || function.CanSend == true|| function.CanReceive == true))
if (function.Owner == null && (function.IsNondeterministic || function.CanCreate || function.CanSend|| function.CanReceive))
{
foreach (var caller in function.Callers)
{
Expand All @@ -73,7 +73,7 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
}
}
}
if ((function.CanChangeState == true || function.CanRaiseEvent == true) &&
if ((function.CanChangeState || function.CanRaiseEvent) &&
(function.Role.HasFlag(FunctionRole.TransitionFunction) ||
function.Role.HasFlag(FunctionRole.ExitHandler)))
{
Expand Down
4 changes: 2 additions & 2 deletions Src/PCompiler/CompilerCore/TypeChecker/StatementVisitor.cs
Original file line number Diff line number Diff line change
Expand Up @@ -515,7 +515,7 @@ public override IPStmt VisitReceiveStmt(PParser.ReceiveStmtContext context)
pEvent.PayloadType);
}

if (recvHandler.CanChangeState == true)
if (recvHandler.CanChangeState)
{
if (!method.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
{
Expand All @@ -525,7 +525,7 @@ public override IPStmt VisitReceiveStmt(PParser.ReceiveStmtContext context)
method.CanChangeState = true;
}

if (recvHandler.CanRaiseEvent == true)
if (recvHandler.CanRaiseEvent)
{
if (!method.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
{
Expand Down

0 comments on commit 177ac07

Please sign in to comment.