From 39f0461b7b055832441b91054578a4e1f5fca042 Mon Sep 17 00:00:00 2001
From: Aman Goel <goelaman@amazon.com>
Date: Fri, 20 Oct 2023 17:26:14 -0700
Subject: [PATCH] [PObserve] Correct name conflict in FFI interface

Corrects spec machine name conflicts when calling spec local foreign functions

Renamed to <spec machine>Foreign to implement foreign functions local to a spec machine
---
 Src/PCompiler/CompilerCore/Backend/Java/Constants.cs        | 1 +
 Src/PCompiler/CompilerCore/Backend/Java/FFIStubGenerator.cs | 6 +++---
 Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs | 2 +-
 3 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs b/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
index 38b642248..b8c883993 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/Constants.cs
@@ -80,6 +80,7 @@ Please separate each generated class into its own .java file (detailed throughou
 
         public static readonly string FFIPackage = "PForeign";
         public static readonly string FFIGlobalScopeCname = "PObserveGlobal";
+        public static readonly string FFILocalScopeSuffix = "Foreign";
 
 
         // Something that is clearly not valid Java.
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/FFIStubGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/FFIStubGenerator.cs
index 02816fb8d..66133fd5d 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/FFIStubGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/FFIStubGenerator.cs
@@ -144,7 +144,7 @@ private void WriteFFITypesHeader(string classname)
         private void WriteFFIHeader(string monitorName)
         {
             WriteLine(Constants.AsFFIComment(
-                $"Please place and complete the following class in {Constants.FFIPackage}/{monitorName}.java :"));
+                $"Please place and complete the following class in {Constants.FFIPackage}/{monitorName}{Constants.FFILocalScopeSuffix}.java :"));
         }
 
         private void WriteForeignTypeStub(ForeignType t)
@@ -275,7 +275,7 @@ private void WriteForeignFunctions(Machine m)
             // Class definition: By convention, this "para-class" has the same name as
             // the P machine it is defined within, to mimic the C#-style partial class mixin
             // functionalty that we are not afforded in Java, unfortunately.
-            WriteLine($"public class {mname} {{");
+            WriteLine($"public class {mname}{Constants.FFILocalScopeSuffix} {{");
             foreach (var f in ffs)
             {
                 WriteForeignFunctionStub(f, m);
@@ -324,7 +324,7 @@ void WriteForeignFunctionStub(Function f, Machine m = null)
             }
 
             WriteLine(") {");
-            WriteLine(" /* throws RaiseEventException, TransitionException */ {");
+            WriteLine(" /* throws RaiseEventException, TransitionException */");
 
             if (ret is TypeManager.JType.JVoid _)
             {
diff --git a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
index f44072f89..91aedd0f6 100644
--- a/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
+++ b/Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs
@@ -625,7 +625,7 @@ private void WriteFunctionCallExpr(Function f, IEnumerable<IPExpr> args)
                 var ffiBridge = Names.FFIBridgeForMachine(
                     isStatic
                     ? Constants.FFIGlobalScopeCname
-                    : _currentMachine.Name);
+                    : $"{_currentMachine.Name}{Constants.FFILocalScopeSuffix}");
                 Write($"{ffiBridge}.{fname}(");
 
                 // All foreign functions have an implicit first argument to the current machine