Skip to content

Commit

Permalink
[PEx] Make receive inside while as not implemented for now
Browse files Browse the repository at this point in the history
Update enum logging and stats reporting

PMap: throw error if adding already existing key
  • Loading branch information
aman-goel committed May 14, 2024
1 parent cfb47f5 commit c405fae
Show file tree
Hide file tree
Showing 6 changed files with 142 additions and 66 deletions.
139 changes: 86 additions & 53 deletions Src/PCompiler/CompilerCore/Backend/PExplicit/TransformASTPass.cs
Original file line number Diff line number Diff line change
Expand Up @@ -531,17 +531,39 @@ static private IPStmt ReplaceBreaks(IPStmt stmt, List<IPStmt> afterStmts)
{
statements.Add(inner);
}
if (statements.Count() == 0)
if (statements.Count == 0)
{
return returnStmt;
}
else
statements.Add(returnStmt);
return new CompoundStmt(returnStmt.SourceLocation, statements);
default:
return stmt;
}
}

static private bool CanReceive(IPStmt stmt)
{
if (stmt == null) return false;
switch(stmt)
{
case CompoundStmt compoundStmt:
foreach (var inner in compoundStmt.Statements)
{
statements.Add(returnStmt);
return new CompoundStmt(returnStmt.SourceLocation, statements);
if (CanReceive(inner))
{
return true;
}
}
return false;
case IfStmt ifStmt:
return CanReceive(ifStmt.ThenBranch) || CanReceive(ifStmt.ElseBranch);
case WhileStmt whileStmt:
return CanReceive(whileStmt.Body);
case ReceiveStmt:
return true;
default:
return stmt;
return false;
}
}

Expand Down Expand Up @@ -696,58 +718,69 @@ static private IPStmt HandleReceives(IPStmt statement, Function function, Machin
result.Add(split);
break;
case WhileStmt loop:
// throw new NotImplementedException($"Receive in a while statement is not yet supported, found in {machine.Name}");
// turn the while statement into a recursive function
var whileName = $"while_{whileNumber}";
whileNumber++;
var rec = new WhileFunction(whileName, loop.SourceLocation);
rec.Owner = function.Owner;
rec.ParentFunction = function;
foreach (var param in function.Signature.Parameters) rec.AddParameter(param);
var newVarMap = new Dictionary<Variable,Variable>();
foreach (var local in function.LocalVariables)
if (CanReceive(loop.Body))
{
var machineVar = new Variable($"{whileName}_{local.Name}", local.SourceLocation, local.Role);
machineVar.Type = local.Type;
machine.AddField(machineVar);
newVarMap.Add(local, machineVar);
throw new NotImplementedException($"Receive in a while statement is not yet supported, found in {machine.Name}");
// // turn the while statement into a recursive function
// var whileName = $"while_{whileNumber}";
// whileNumber++;
// var rec = new WhileFunction(whileName, loop.SourceLocation);
// rec.Owner = function.Owner;
// rec.ParentFunction = function;
// foreach (var param in function.Signature.Parameters) rec.AddParameter(param);
// var newVarMap = new Dictionary<Variable,Variable>();
// foreach (var local in function.LocalVariables)
// {
// var machineVar = new Variable($"{whileName}_{local.Name}", local.SourceLocation, local.Role);
// machineVar.Type = local.Type;
// machine.AddField(machineVar);
// newVarMap.Add(local, machineVar);
// }
// foreach (var i in function.CreatesInterfaces) rec.AddCreatesInterface(i);
// rec.CanChangeState = function.CanChangeState;
// rec.CanRaiseEvent = function.CanRaiseEvent;
// rec.CanReceive = function.CanReceive;
// rec.IsNondeterministic = function.IsNondeterministic;
// // make while loop body
// var loopBody = new List<IPStmt>();
// var bodyEnumerator = loop.Body.Statements.GetEnumerator();
// while (bodyEnumerator.MoveNext())
// {
// var stmt = bodyEnumerator.Current;
// var replaceBreak = ReplaceBreaks(stmt, afterStmts);
// if (replaceBreak != null) {
// loopBody.Add(ReplaceVars(replaceBreak, newVarMap));
// }
// }
// var recArgs = new List<VariableAccessExpr>();
// foreach (var param in rec.Signature.Parameters)
// {
// recArgs.Add(new VariableAccessExpr(rec.SourceLocation, param));
// }
// // call the function
// var recCall = new FunCallStmt(loop.SourceLocation, rec, recArgs);
// loopBody.Add(recCall);
// rec.AddCallee(rec);
// loopBody = new List<IPStmt>(((CompoundStmt) HandleReceives(new CompoundStmt(rec.SourceLocation, loopBody), rec, machine)).Statements);
// rec.Body = new CompoundStmt(rec.SourceLocation, loopBody);
// if (machine != null) machine.AddMethod(rec);
// // assign local variables
// foreach (var local in function.LocalVariables)
// {
// result.Add(new AssignStmt(local.SourceLocation, new VariableAccessExpr(local.SourceLocation, newVarMap[local]), new VariableAccessExpr(local.SourceLocation, local)));
// }
// // replace the while statement with a function call
// result.Add(recCall);
// result.Add(new ReturnStmt(loop.SourceLocation, null));
// function.AddCallee(rec);
}
foreach (var i in function.CreatesInterfaces) rec.AddCreatesInterface(i);
rec.CanChangeState = function.CanChangeState;
rec.CanRaiseEvent = function.CanRaiseEvent;
rec.CanReceive = function.CanReceive;
rec.IsNondeterministic = function.IsNondeterministic;
// make while loop body
var loopBody = new List<IPStmt>();
var bodyEnumerator = loop.Body.Statements.GetEnumerator();
while (bodyEnumerator.MoveNext())
{
var stmt = bodyEnumerator.Current;
var replaceBreak = ReplaceBreaks(stmt, afterStmts);
if (replaceBreak != null) {
loopBody.Add(ReplaceVars(replaceBreak, newVarMap));
}
}
var recArgs = new List<VariableAccessExpr>();
foreach (var param in rec.Signature.Parameters)
{
recArgs.Add(new VariableAccessExpr(rec.SourceLocation, param));
}
// call the function
var recCall = new FunCallStmt(loop.SourceLocation, rec, recArgs);
loopBody.Add(recCall);
rec.AddCallee(rec);
loopBody = new List<IPStmt>(((CompoundStmt) HandleReceives(new CompoundStmt(rec.SourceLocation, loopBody), rec, machine)).Statements);
rec.Body = new CompoundStmt(rec.SourceLocation, loopBody);
if (machine != null) machine.AddMethod(rec);
// assign local variables
foreach (var local in function.LocalVariables)
else
{
result.Add(new AssignStmt(local.SourceLocation, new VariableAccessExpr(local.SourceLocation, newVarMap[local]), new VariableAccessExpr(local.SourceLocation, local)));
if (after == null) return compound;
result.Add(first);
after = (CompoundStmt) HandleReceives(after, function, machine);
result.Add(after);
}
// replace the while statement with a function call
result.Add(recCall);
function.AddCallee(rec);
break;
default:
if (after == null) return compound;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,8 @@ private static void printStats() {
scheduler.recordStats();
if (PExplicitGlobal.getResult().equals("correct for any depth")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED);
} else if (PExplicitGlobal.getResult().startsWith("correct up to step")) {
PExplicitGlobal.setStatus(STATUS.VERIFIED_UPTO_MAX_STEPS);
}
StatWriter.log("time-search-seconds", String.format("%.1f", searchTime));
}
Expand Down
Original file line number Diff line number Diff line change
@@ -1,12 +1,29 @@
package pexplicit.runtime;

public enum STATUS {
INCOMPLETE, // search still ongoing
SCHEDULEOUT, // schedule limit reached
TIMEOUT, // timeout reached
MEMOUT, // memout reached
VERIFIED, // full state space explored and no bug found
BUG_FOUND, // found a bug
INTERRUPTED, // interrupted by user
ERROR // unexpected error encountered
INCOMPLETE("incomplete"), // search still ongoing
SCHEDULEOUT("scheduleout"), // schedule limit reached
TIMEOUT("timeout"), // timeout reached
MEMOUT("memout"), // memout reached
VERIFIED("proved"), // full state space explored and no bug found
VERIFIED_UPTO_MAX_STEPS("proved"), // full state space explored and no bug found upto max steps
BUG_FOUND("cex"), // found a bug
INTERRUPTED("interrupted"), // interrupted by user
ERROR("error"); // unexpected error encountered

private String name;

/**
* Constructor
*
* @param n Name of the enum
*/
STATUS(String n) {
this.name = n;
}

@Override
public String toString() {
return this.name;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -590,13 +590,13 @@ public void recordStats() {
StatWriter.log("time-seconds", String.format("%.1f", timeUsed));
StatWriter.log("memory-max-MB", String.format("%.1f", MemoryMonitor.getMaxMemSpent()));
StatWriter.log("memory-current-MB", String.format("%.1f", memoryUsed));
StatWriter.log("#-schedules", String.format("%d", SearchStatistics.iteration));
StatWriter.log("#-executions", String.format("%d", SearchStatistics.iteration));
if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
StatWriter.log("#-states", String.format("%d", SearchStatistics.totalStates));
StatWriter.log("#-distinct-states", String.format("%d", SearchStatistics.totalDistinctStates));
}
StatWriter.log("steps-min", String.format("%d", SearchStatistics.minSteps));
StatWriter.log("steps-max", String.format("%d", SearchStatistics.maxSteps));
StatWriter.log("max-depth-explored", String.format("%d", SearchStatistics.maxSteps));
StatWriter.log("steps-avg", String.format("%d", SearchStatistics.totalSteps / SearchStatistics.iteration));
StatWriter.log("#-choices-unexplored", String.format("%d", getNumUnexploredChoices()));
StatWriter.log("%-choices-unexplored-data", String.format("%.1f", getUnexploredDataChoicesPercent()));
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,23 @@
package pexplicit.runtime.scheduler.explicit.strategy;

public enum SearchStrategyMode {
DepthFirst,
Random,
Astar
DepthFirst("dfs"),
Random("random"),
Astar("astar");

private String name;

/**
* Constructor
*
* @param n Name of the enum
*/
SearchStrategyMode(String n) {
this.name = n;
}

@Override
public String toString() {
return this.name;
}
}
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package pexplicit.values;

import pexplicit.utils.misc.Assert;
import pexplicit.values.exceptions.KeyNotFoundException;

import java.util.ArrayList;
Expand Down Expand Up @@ -88,6 +89,13 @@ public PMap put(PValue<?> key, PValue<?> val) {
* @param val value to set
*/
public PMap add(PValue<?> key, PValue<?> val) {
if (map.containsKey(key)) {
Assert.fromModel(
false,
String.format(
"ArgumentException: An item with the same key has already been added. Key: %s, Value: %s",
key, map.get(key)));
}
return put(key, val);
}

Expand Down

0 comments on commit c405fae

Please sign in to comment.