[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

Author: aman-goel

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

@@ -77,7 +77,7 @@ internal string GetNameForDecl(IPDecl decl)
                     return $"{pEvent.Name}";
                 return $"_{pEvent.Name}";
             case SafetyTest safety:
-                return $"{safety.Name}";
+                return $"test_{safety.Name}";
             default:
                 throw new NotImplementedException($"decl type {decl.GetType().Name} not supported");
         }

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

@@ -203,7 +203,7 @@ private void WriteMainDriver(CompilationContext context, StringWriter output, Sc
                 return;
 
         context.WriteLine(output, "@Generated");
-        context.WriteLine(output, "public static class DefaultImpl extends PTestDriver {");
+        context.WriteLine(output, "public static class test_DefaultImpl extends PTestDriver {");
         WriteDriver(context, output, mainMachine.Name, decls);
         context.WriteLine(output, "}");
         context.WriteLine(output);

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

@@ -220,7 +220,10 @@ private static List<IPStmt> ReplaceReturn(IReadOnlyList<IPStmt> body, IPExpr loc
             switch (stmt)
             {
                 case ReturnStmt returnStmt:
-                    newBody.Add(new AssignStmt(returnStmt.SourceLocation, location, returnStmt.ReturnValue));
+                    if (location != null)
+                    {
+                        newBody.Add(new AssignStmt(returnStmt.SourceLocation, location, returnStmt.ReturnValue));
+                    }
                     newBody.Add(new AssignStmt(returnStmt.SourceLocation, 
                         new VariableAccessExpr(returnStmt.SourceLocation, inVar), 
                         new BoolLiteralExpr(returnStmt.SourceLocation, false)));
@@ -329,7 +332,20 @@ private static void InlineStmt(Function function, IPStmt stmt, List<IPStmt> body
                     var inlined = InlineInFunction(call.Function);
                     if (inlined)
                         function.RemoveCallee(call.Function);
-                    GenerateInline(function, call.Function, call.ArgsList, body, call.SourceLocation);
+                    var appendToBody = new List<IPStmt>();
+                    var inVar = GenerateInline(function, call.Function, call.ArgsList, appendToBody,
+                        call.SourceLocation);
+                    body.Add(new AssignStmt(call.SourceLocation, 
+                        new VariableAccessExpr(call.SourceLocation, inVar), 
+                        new BoolLiteralExpr(call.SourceLocation, true)));
+                    appendToBody = ReplaceReturn(appendToBody, null, inVar, call.Function);
+                    foreach (var statement in appendToBody)
+                    {
+                        var inCond = new BinOpExpr(statement.SourceLocation, BinOpType.Eq,
+                            new VariableAccessExpr(statement.SourceLocation, inVar),
+                            new BoolLiteralExpr(statement.SourceLocation, true));
+                        body.Add(new IfStmt(statement.SourceLocation, inCond, statement, null));
+                    }
                 }
                 else
                 {

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

@@ -142,7 +142,7 @@ private static void setTestDriver(Reflections reflections)
         Set<Class<? extends PTestDriver>> subTypesDriver = reflections.getSubTypesOf(PTestDriver.class);
         PTestDriver driver = null;
         for (Class<? extends PTestDriver> td : subTypesDriver) {
-            if (td.getSimpleName().equals(name)) {
+            if (PTestDriver.getTestName(td).equals(name)) {
                 driver = td.getDeclaredConstructor().newInstance();
                 break;
             }
@@ -163,15 +163,15 @@ private static void setTestDriver(Reflections reflections)
                             subTypesDriver.size()));
             PExLogger.logInfo("Possible options are:");
             for (Class<? extends PTestDriver> td : subTypesDriver) {
-                PExLogger.logInfo(String.format("%s", td.getSimpleName()));
+                PExLogger.logInfo(String.format("%s", PTestDriver.getTestName(td)));
             }
             if (!name.equals(defaultTestDriver)) {
                 throw new Exception("No test driver found named \"" + PExGlobal.getConfig().getTestDriver() + "\"");
             } else {
                 System.exit(6);
             }
         }
-        PExGlobal.getConfig().setTestDriver(driver.getClass().getSimpleName());
+        PExGlobal.getConfig().setTestDriver(PTestDriver.getTestName(driver.getClass()));
         PExGlobal.getModel().setTestDriver(driver);
     }
 

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

@@ -29,6 +29,16 @@ public PTestDriver() {
         configure();
     }
 
+    /**
+     * Get test driver name
+     */
+    public static String getTestName(Class<? extends PTestDriver> td) {
+        String result = td.getSimpleName();
+        if (result.startsWith("test_"))
+            return result.substring("test_".length());
+        return result;
+    }
+
     /**
      * Get the start/main machine of this test driver.
      *

Tst/RegressionTests/Integration/Correct/SEM_TwoMachines_15/TestSameAsMain.p

@@ -0,0 +1,22 @@
+// P semantics XYZ: two machines, announce announce instantiation parameter
+// This is validation XYZ for announceInvocation.p
+event E2 assert 1: bool;
+
+machine Main {
+    var XYZ: bool;
+	  var ev2: event;
+    start state Real1_Init {
+        entry {
+          ev2 = E2;
+			    announce ev2, XYZ;  //"null event" error in Zing
+		}
+	}
+}
+spec M observes E2 {
+	start state x {
+                on E2 do (payload: bool) { assert (payload == false); }
+	}
+}
+
+test Main [main=Main]: assert M in { Main };
+