Skip to content

Commit cf2c84f

Browse files
aman-goelaman-goel
authored
[PEx] Correct inlining functions with non-null return without assignment (#850)
* [PEx] Correct inlining functions with non-null return without assignment, support test driver name same as test machine name [PEx IR] Adds support for inlining functions that return non-null but are not assigned to a variable during function call [PEx IR+RT] Prefixes test driver names with test_ to support test name same as test main machine name [Tst] Adds unit test with test case name same as main machine name * [PEx IR] Correct IR for functions returning null * [Tst] Update new unit test to align with hardcoded test name in C# unit test runner * [Tst] Dropping unit test since C# test runner uses hardcoded test name and main machine * [PEx IR] Minor correction when pritning source location in exception
1 parent f6b4c95 commit cf2c84f

File tree

5 files changed

+46
-20
lines changed

5 files changed

+46
-20
lines changed

‎Src/PCompiler/CompilerCore/Backend/PEx/CompilationContext.cs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,7 +77,7 @@ internal string GetNameForDecl(IPDecl decl)
7777
return $"{pEvent.Name}";
7878
return $"_{pEvent.Name}";
7979
case SafetyTest safety:
80-
return $"{safety.Name}";
80+
return $"test_{safety.Name}";
8181
default:
8282
throw new NotImplementedException($"decl type {decl.GetType().Name} not supported");
8383
}

‎Src/PCompiler/CompilerCore/Backend/PEx/PExCodeGenerator.cs

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -203,7 +203,7 @@ private void WriteMainDriver(CompilationContext context, StringWriter output, Sc
203203
return;
204204

205205
context.WriteLine(output, "@Generated");
206-
context.WriteLine(output, "public static class DefaultImpl extends PTestDriver {");
206+
context.WriteLine(output, "public static class test_DefaultImpl extends PTestDriver {");
207207
WriteDriver(context, output, mainMachine.Name, decls);
208208
context.WriteLine(output, "}");
209209
context.WriteLine(output);
@@ -478,7 +478,7 @@ private void WriteForeignFunction(CompilationContext context, StringWriter outpu
478478

479479
string returnType = null;
480480
var returnStatement = "";
481-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
481+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
482482
{
483483
returnType = "void";
484484
}
@@ -524,7 +524,7 @@ private void WriteFunction(CompilationContext context, StringWriter output, Func
524524
var staticKeyword = isStatic ? "static " : "";
525525

526526
string returnType = null;
527-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
527+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
528528
returnType = "void";
529529
else
530530
returnType = GetPExType(function.Signature.ReturnType);
@@ -599,7 +599,7 @@ private void WriteFunctionBody(CompilationContext context, StringWriter output,
599599
context.WriteLine(output);
600600
}
601601

602-
if (!function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
602+
if (function.Signature.ReturnType != null && !function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
603603
context.WriteLine(output,
604604
$"{GetPExType(function.Signature.ReturnType)} {CompilationContext.ReturnValue} = {GetDefaultValue(function.Signature.ReturnType)};");
605605

@@ -610,7 +610,7 @@ private void WriteFunctionBody(CompilationContext context, StringWriter output,
610610
else
611611
exited = WriteStmt(function, context, output, ControlFlowContext.FreshFuncContext(context), function.Body);
612612
if (!exited)
613-
if (!function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
613+
if (function.Signature.ReturnType != null && !function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
614614
context.Write(output, $"return {CompilationContext.ReturnValue};");
615615
}
616616

@@ -733,7 +733,7 @@ private bool WriteStmt(Function function, CompilationContext context, StringWrit
733733

734734
context.WriteLine(output, ");");
735735

736-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
736+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
737737
context.WriteLine(output, "return;");
738738
else
739739
context.WriteLine(output, "return null;");
@@ -756,7 +756,7 @@ private bool WriteStmt(Function function, CompilationContext context, StringWrit
756756

757757
context.WriteLine(output, ");");
758758

759-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
759+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
760760
context.WriteLine(output, "return;");
761761
else
762762
context.WriteLine(output, "return null;");
@@ -979,7 +979,7 @@ private bool WriteStmt(Function function, CompilationContext context, StringWrit
979979

980980
private void WriteContinuation(CompilationContext context, StringWriter output, Continuation continuation)
981981
{
982-
var voidReturn = continuation.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null);
982+
var voidReturn = continuation.Signature.ReturnType == null || continuation.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null);
983983
if (!voidReturn)
984984
throw new NotImplementedException(
985985
$"Receive statement in a function with non-void return type is not supported. Found in function named {continuation.ParentFunction.Name}.");
@@ -1143,14 +1143,14 @@ private void WriteForeignFunCallStmt(CompilationContext context, StringWriter ou
11431143
IReadOnlyList<IPExpr> args, IPExpr dest = null)
11441144
{
11451145
string returnTemp = null;
1146-
if (!function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
1146+
if (function.Signature.ReturnType != null && !function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
11471147
{
11481148
returnTemp = context.FreshTempVar();
11491149
context.Write(output,
11501150
$"{GetPExType(function.Signature.ReturnType)} {returnTemp} = ({GetPExType(function.Signature.ReturnType)})");
11511151
}
11521152

1153-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
1153+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
11541154
{
11551155
context.Write(output, "ForeignFunctionInterface.accept(");
11561156
context.Write(output, $"x -> ffi_{context.GetNameForDecl(function)}(x)");
@@ -1173,7 +1173,7 @@ private void WriteForeignFunCallStmt(CompilationContext context, StringWriter ou
11731173

11741174
context.WriteLine(output, ");");
11751175

1176-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
1176+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
11771177
{
11781178
Debug.Assert(dest == null);
11791179
}
@@ -1195,7 +1195,7 @@ private void WriteFunCallStmt(CompilationContext context, StringWriter output, F
11951195
}
11961196

11971197
string returnTemp = null;
1198-
if (!function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
1198+
if (function.Signature.ReturnType != null && !function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
11991199
{
12001200
returnTemp = context.FreshTempVar();
12011201
context.Write(output, $"{GetPExType(function.Signature.ReturnType)} {returnTemp} = ");
@@ -1213,7 +1213,7 @@ private void WriteFunCallStmt(CompilationContext context, StringWriter output, F
12131213

12141214
context.WriteLine(output, ");");
12151215

1216-
if (function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
1216+
if (function.Signature.ReturnType == null || function.Signature.ReturnType.IsSameTypeAs(PrimitiveType.Null))
12171217
{
12181218
Debug.Assert(dest == null);
12191219
}

‎Src/PCompiler/CompilerCore/Backend/PEx/TransformASTPass.cs

Lines changed: 19 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@ private static State TransformState(State state, IDictionary<Function, Function>
126126
{
127127
if (handler.Key.IsNullEvent)
128128
throw new NotImplementedException(
129-
$"{context.LocationResolver.GetLocation(handler.Key.SourceLocation)}: Null events are not supported in this mode.");
129+
$"{context.LocationResolver.GetLocation(handler.Value.SourceLocation)}: Null events are not supported in this mode.");
130130
transformedState[handler.Key] = TransformAction(handler.Value, functionMap);
131131
}
132132

@@ -220,7 +220,10 @@ private static List<IPStmt> ReplaceReturn(IReadOnlyList<IPStmt> body, IPExpr loc
220220
switch (stmt)
221221
{
222222
case ReturnStmt returnStmt:
223-
newBody.Add(new AssignStmt(returnStmt.SourceLocation, location, returnStmt.ReturnValue));
223+
if (location != null)
224+
{
225+
newBody.Add(new AssignStmt(returnStmt.SourceLocation, location, returnStmt.ReturnValue));
226+
}
224227
newBody.Add(new AssignStmt(returnStmt.SourceLocation,
225228
new VariableAccessExpr(returnStmt.SourceLocation, inVar),
226229
new BoolLiteralExpr(returnStmt.SourceLocation, false)));
@@ -329,7 +332,20 @@ private static void InlineStmt(Function function, IPStmt stmt, List<IPStmt> body
329332
var inlined = InlineInFunction(call.Function);
330333
if (inlined)
331334
function.RemoveCallee(call.Function);
332-
GenerateInline(function, call.Function, call.ArgsList, body, call.SourceLocation);
335+
var appendToBody = new List<IPStmt>();
336+
var inVar = GenerateInline(function, call.Function, call.ArgsList, appendToBody,
337+
call.SourceLocation);
338+
body.Add(new AssignStmt(call.SourceLocation,
339+
new VariableAccessExpr(call.SourceLocation, inVar),
340+
new BoolLiteralExpr(call.SourceLocation, true)));
341+
appendToBody = ReplaceReturn(appendToBody, null, inVar, call.Function);
342+
foreach (var statement in appendToBody)
343+
{
344+
var inCond = new BinOpExpr(statement.SourceLocation, BinOpType.Eq,
345+
new VariableAccessExpr(statement.SourceLocation, inVar),
346+
new BoolLiteralExpr(statement.SourceLocation, true));
347+
body.Add(new IfStmt(statement.SourceLocation, inCond, statement, null));
348+
}
333349
}
334350
else
335351
{

‎Src/PRuntimes/PExRuntime/src/main/java/pex/PEx.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,7 @@ private static void setTestDriver(Reflections reflections)
142142
Set<Class<? extends PTestDriver>> subTypesDriver = reflections.getSubTypesOf(PTestDriver.class);
143143
PTestDriver driver = null;
144144
for (Class<? extends PTestDriver> td : subTypesDriver) {
145-
if (td.getSimpleName().equals(name)) {
145+
if (PTestDriver.getTestName(td).equals(name)) {
146146
driver = td.getDeclaredConstructor().newInstance();
147147
break;
148148
}
@@ -163,15 +163,15 @@ private static void setTestDriver(Reflections reflections)
163163
subTypesDriver.size()));
164164
PExLogger.logInfo("Possible options are:");
165165
for (Class<? extends PTestDriver> td : subTypesDriver) {
166-
PExLogger.logInfo(String.format("%s", td.getSimpleName()));
166+
PExLogger.logInfo(String.format("%s", PTestDriver.getTestName(td)));
167167
}
168168
if (!name.equals(defaultTestDriver)) {
169169
throw new Exception("No test driver found named \"" + PExGlobal.getConfig().getTestDriver() + "\"");
170170
} else {
171171
System.exit(6);
172172
}
173173
}
174-
PExGlobal.getConfig().setTestDriver(driver.getClass().getSimpleName());
174+
PExGlobal.getConfig().setTestDriver(PTestDriver.getTestName(driver.getClass()));
175175
PExGlobal.getModel().setTestDriver(driver);
176176
}
177177

‎Src/PRuntimes/PExRuntime/src/main/java/pex/runtime/machine/PTestDriver.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,16 @@ public PTestDriver() {
2929
configure();
3030
}
3131

32+
/**
33+
* Get test driver name
34+
*/
35+
public static String getTestName(Class<? extends PTestDriver> td) {
36+
String result = td.getSimpleName();
37+
if (result.startsWith("test_"))
38+
return result.substring("test_".length());
39+
return result;
40+
}
41+
3242
/**
3343
* Get the start/main machine of this test driver.
3444
*

0 commit comments

Comments
 (0)