Make PInfer standalone by placing Java runtime dependencies

Src/PCompiler/CompilerCore/Backend/Java/Constants.cs

@@ -148,19 +148,6 @@ internal static string PomTemplate(bool pinferMode) {
             <artifactId>commons-cli</artifactId>
             <version>1.8.0</version>
         </dependency>" : "")}
-        <dependency>
-            <groupId>p.runtime</groupId>
-            <artifactId>PJavaRuntime</artifactId>
-            <version>1.0-SNAPSHOT</version>
-
-            <!-- Do not transitively bundle log4j as whoever uses this jar will also depend on it. -->
-            <exclusions>
-                <exclusion>
-                    <groupId>org.apache.logging.log4j</groupId>
-                    <artifactId>*</artifactId>
-                </exclusion>
-            </exclusions>
-        </dependency>
     </dependencies>
 
     <build>
@@ -225,13 +212,13 @@ internal static string PomTemplate(bool pinferMode) {
         /// The fully-qualified name of the static `deepEquality(Object, Object)` method
         /// exposed by the Java PRT runtime.
         /// </summary>
-        internal static readonly string PrtDeepEqualsMethodName = "com.amazon.pobserve.runtime.values.Equality.deepEquals";
+        internal static string PrtDeepEqualsMethodName() => PInferMode ? "Equality.deepEquals" : "com.amazon.pobserve.runtime.values.Equality.deepEquals";
 
         /// <summary>
         /// The fully-qualified name of the static `compare(Comparable, Comparable)` method
         /// exposed by the Java PRT runtime.
         /// </summary>
-        internal static readonly string PrtCompareMethodName = "com.amazon.pobserve.runtime.values.Equality.compare";
+        internal static string PrtCompareMethodName() => PInferMode ? "Equality.compare" : "com.amazon.pobserve.runtime.values.Equality.compare";
 
         /// <summary>
         /// The fully-qualified name of the static `elementAt(LinkedHashSet, long)` method
@@ -242,12 +229,12 @@ internal static string PomTemplate(bool pinferMode) {
         /// <summary>
         /// The fully-qualified class name of the Java P runtime's PValue class.
         /// </summary>
-        internal static readonly string PValueClass = "com.amazon.pobserve.runtime.values.PValue";
+        internal static string PValueClass() => PInferMode ? "PValue" : "com.amazon.pobserve.runtime.values.PValue";
 
         /// <summary>
         /// The fully-qualified class name of the Java P runtime's Event class.
         /// </summary>
-        internal static readonly string EventsClass = "com.amazon.pobserve.runtime.events.Event";
+        internal static string EventsClass() => PInferMode ? "PEvent" : "com.amazon.pobserve.runtime.events.Event";
 
         #endregion
 

Src/PCompiler/CompilerCore/Backend/Java/EventGenerator.cs

@@ -78,7 +78,7 @@ internal void WriteEventDecl(Event e, bool pinfer = false)
             var payloadType = argType.TypeName;
             var payloadRefType = argType.ReferenceTypeName;
 
-            WriteLine($"public static class {eventName} extends {Constants.EventsClass}<{payloadRefType}> implements Serializable {{");
+            WriteLine($"public static class {eventName} extends {Constants.EventsClass()}<{payloadRefType}> implements Serializable {{");
 
             var hasPayload = !(argType is TypeManager.JType.JVoid);
             if (pinfer)

Src/PCompiler/CompilerCore/Backend/Java/MachineGenerator.cs

@@ -893,7 +893,7 @@ void WritePrim()
                 case BinOpKind.Comparison:
                     Write("(");
 
-                    Write($"{Constants.PrtCompareMethodName}(");
+                    Write($"{Constants.PrtCompareMethodName()}(");
                     WriteExpr(left);
                     Write(", ");
                     WriteExpr(right);
@@ -906,7 +906,7 @@ void WritePrim()
                 case BinOpKind.Equality:
                     Write("(");
 
-                    Write($"{Constants.PrtDeepEqualsMethodName}(");
+                    Write($"{Constants.PrtDeepEqualsMethodName()}(");
                     WriteExpr(left);
                     Write(", ");
                     WriteExpr(right);
@@ -1007,7 +1007,7 @@ private void WriteOverloads()
                 Write("&& ");
                 WriteLine(jType.IsPrimitive
                     ? $"this.{fieldName} == other.{fieldName}"
-                    : $"{Constants.PrtDeepEqualsMethodName}(this.{fieldName}, other.{fieldName})");
+                    : $"{Constants.PrtDeepEqualsMethodName()}(this.{fieldName}, other.{fieldName})");
             }
             WriteLine(");");
             WriteLine("} // deepEquals()");

Src/PCompiler/CompilerCore/Backend/Java/TypeManager.cs

@@ -515,7 +515,7 @@ internal class JEvent : JType
             {
                 internal JEvent()
                 {
-                    _unboxedType = $"{Constants.EventsClass}<?>";
+                    _unboxedType = $"{Constants.EventsClass()}<?>";
                 }
                 internal override bool IsPrimitive => false;
                 internal override string GenerateFromJSON(string jsonVariable, string fieldName)

Src/PCompiler/CompilerCore/Backend/Java/TypesGenerator.cs

@@ -127,7 +127,7 @@ private void WriteNamedTupleDecl(NamedTupleType t, bool pinfer = false)
             }
 
             var tname = Names.NameForNamedTuple(t);
-            WriteLine($"public static class {tname} implements {Constants.PValueClass}<{tname}>, Serializable {{");
+            WriteLine($"public static class {tname} implements {Constants.PValueClass()}<{tname}>, Serializable {{");
             WriteLine($"// {t.CanonicalRepresentation}");
 
             WriteNamedTupleFields(fields);
@@ -243,7 +243,7 @@ private void WriteNamedTupleEqualityMethods(string tname, List<(TypeManager.JTyp
                 Write(" && ");
                 WriteLine(jType.IsPrimitive
                     ? $"Objects.equals(this.{fieldName}, other.{fieldName})"
-                    : $"{Constants.PrtDeepEqualsMethodName}(this.{fieldName}, other.{fieldName})");
+                    : $"{Constants.PrtDeepEqualsMethodName()}(this.{fieldName}, other.{fieldName})");
             }
             WriteLine(");");
             WriteLine("} // deepEquals()");

Src/PCompiler/CompilerCore/Backend/PInfer/JavaSourceGenerator.cs

@@ -103,7 +103,7 @@ protected void WriteTermInterface(IDictionary<string, (string, List<PEventVariab
             WriteLine("return res;");
             WriteLine("}");
 
-            WriteLine($"public static Object termOf(String repr, {Constants.EventsClass}<?>[] arguments) {{");
+            WriteLine($"public static Object termOf(String repr, {Constants.EventsClass()}<?>[] arguments) {{");
             if (nameMap.Count == 0)
             {
                 WriteLine("return null;");
@@ -123,7 +123,7 @@ protected void WriteTermInterface(IDictionary<string, (string, List<PEventVariab
 
         protected void WritePredicateInterface(IDictionary<string, (string, List<PEventVariable>)> nameMap)
         {
-            WriteLine($"public static boolean invoke(PredicateWrapper repr, {Constants.EventsClass}<?>[] arguments) {{");
+            WriteLine($"public static boolean invoke(PredicateWrapper repr, {Constants.EventsClass()}<?>[] arguments) {{");
             if (nameMap.Count == 0)
             {
                 WriteLine("return false;");
@@ -140,7 +140,7 @@ protected void WritePredicateInterface(IDictionary<string, (string, List<PEventV
             }
             WriteLine("}");
 
-            WriteLine($"public static boolean conjoin(List<PredicateWrapper> repr, {Constants.EventsClass}<?>[] arguments) {{");
+            WriteLine($"public static boolean conjoin(List<PredicateWrapper> repr, {Constants.EventsClass()}<?>[] arguments) {{");
             WriteLine("for (PredicateWrapper wrapper: repr) {");
             WriteLine("if (wrapper.negate() == invoke(wrapper, arguments)) return false;");
             WriteLine("}");

Src/PCompiler/CompilerCore/Backend/PInfer/PInferDriverGenerator.cs

@@ -20,13 +20,13 @@ protected override void GenerateCodeImpl()
             foreach (string name in TemplateNames)
             {
                 insert += @$"case ""{name}"":
-                for (List<{Constants.EventsClass}<?>> ts: eventsTrace) {{
+                for (List<{Constants.EventsClass()}<?>> ts: eventsTrace) {{
                     Templates.{name}.execute(indices, ts, guards, filters, forallTerms, existsTerms);
                 }}
                 break;
                 ";
             }
-            WriteLine(template.Replace("%TEMPLATE%", insert).Replace("%EVENT_BASE%", $"{Constants.EventsClass}<?>").Replace("%PROJECT_NAME%", Job.ProjectName));
+            WriteLine(template.Replace("%TEMPLATE%", insert).Replace("%EVENT_BASE%", $"{Constants.EventsClass()}<?>").Replace("%PROJECT_NAME%", Job.ProjectName));
         }
     }
 }

Src/PCompiler/CompilerCore/Backend/PInfer/PInferPredicateGenerator.cs

@@ -229,6 +229,8 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
             Console.WriteLine($"Generated {numTerms} terms and {numPredicates} predicates");
             NumTerms = numTerms;
             NumPredicates = numPredicates;
+            var pJavaRtDependencies = PreambleConstants.PObserveDeps;
+            var outDepsFiles = pJavaRtDependencies.SelectMany(x => new PJavaRtDependenciesGenerator(job, x, PreambleConstants.ReadTemplate(x)).GenerateCode(javaCtx, globalScope));
             return compiledJavaSrc.Concat(new TraceReaderGenerator(job, quantifiedEvents.Concat([configEvent])).GenerateCode(javaCtx, globalScope))
                                 .Concat(templateCodegen.GenerateCode(javaCtx, globalScope))
                                 .Concat(new DriverGenerator(job, templateCodegen.TemplateNames).GenerateCode(javaCtx, globalScope))
@@ -241,6 +243,7 @@ public IEnumerable<CompiledFile> GenerateCode(ICompilerConfiguration job, Scope
                                 .Concat(new TermEnumeratorGenerator(job).GenerateCode(javaCtx, globalScope))
                                 .Concat(new TemplateInstantiatorGenerator(job, quantifiedEvents.Count).GenerateCode(javaCtx, globalScope))
                                 .Concat(new TraceIndexGenerator(job).GenerateCode(javaCtx, globalScope))
+                                .Concat(outDepsFiles)
                                 .Concat([terms, predicates]);
         }
 

Src/PCompiler/CompilerCore/Backend/PInfer/PInferTemplateGenerator.cs

@@ -206,16 +206,16 @@ private void GenerateTemplate(int numForall, int numExists,
             // exists-n (e.g. quorum)
             bool generateExistsN = ConfigEvent != null && numExists != 0;
             static string getEventTypeName(string e) => $"{Constants.EventNamespaceName}.{e}.class";
-            void declVar(string name, string idx) => WriteLine($"{Constants.EventsClass}<?> {name} = trace.get({idx});");
+            void declVar(string name, string idx) => WriteLine($"{Constants.EventsClass()}<?> {name} = trace.get({idx});");
             WriteDefAndConstructor(templateName, fullDecls, numExists != 0, generateExistsN);
-            WriteLine($"public static void execute(TraceIndex indices, List<{Constants.EventsClass}<?>> trace, List<{Job.ProjectName}.PredicateWrapper> guards, List<{Job.ProjectName}.PredicateWrapper> filters, List<String> forallTerms, List<String> existsTerms) {{");
+            WriteLine($"public static void execute(TraceIndex indices, List<{Constants.EventsClass()}<?>> trace, List<{Job.ProjectName}.PredicateWrapper> guards, List<{Job.ProjectName}.PredicateWrapper> filters, List<String> forallTerms, List<String> existsTerms) {{");
             if (numExists > 0)
             {
                 for (int i = 0; i < existsTypeDecls.Count; ++i)
                 {
                     WriteLine($"List<List<{existsTypeDecls[i].ReferenceTypeName}>> etLst{i} = new ArrayList<>();");
                 }
-                WriteLine($"List<{Constants.EventsClass}[]> guardsArgsLst = new ArrayList<>();");
+                WriteLine($"List<{Constants.EventsClass()}[]> guardsArgsLst = new ArrayList<>();");
                 WriteLine($"List<Integer> numExistsLst = new ArrayList<>();");
             }
             if (generateExistsN)
@@ -240,7 +240,7 @@ private void GenerateTemplate(int numForall, int numExists,
             WriteLine("try {");
             if (numForall > 0)
             {
-                WriteLine($"{Constants.EventsClass}<?>[] guardsArgs = {{ {string.Join(", ", Enumerable.Range(0, numForall).Select(i => $"e{i}"))} }};");
+                WriteLine($"{Constants.EventsClass()}<?>[] guardsArgs = {{ {string.Join(", ", Enumerable.Range(0, numForall).Select(i => $"e{i}"))} }};");
                 WriteLine($"if (!({Job.ProjectName}.conjoin(guards, guardsArgs))) continue;");
             }
             // define aggregation arrays for each existentially quantified terms
@@ -259,7 +259,7 @@ private void GenerateTemplate(int numForall, int numExists,
             }
             if (numExists > 0)
             {
-                WriteLine($"{Constants.EventsClass}<?>[] filterArgs = {{ {string.Join(", ", Enumerable.Range(0, numForall + numExists).Select(i => $"e{i}"))} }};");
+                WriteLine($"{Constants.EventsClass()}<?>[] filterArgs = {{ {string.Join(", ", Enumerable.Range(0, numForall + numExists).Select(i => $"e{i}"))} }};");
                 WriteLine($"if (!({Job.ProjectName}.conjoin(filters, filterArgs))) continue;");
                 WriteLine($"numExistsComb += 1;");
             }

Src/PCompiler/CompilerCore/Backend/PInfer/PJavaRtDependenciesGenerator.cs

@@ -0,0 +1,19 @@
+using Plang.Compiler.Backend.Java;
+
+namespace Plang.Compiler.Backend.PInfer
+{
+    internal class PJavaRtDependenciesGenerator : MachineGenerator
+    {
+
+        private readonly string _myCode = "";
+        public PJavaRtDependenciesGenerator(ICompilerConfiguration job, string filename, string code) : base(job, filename)
+        {
+            _myCode = code;
+        }
+
+        protected override void GenerateCodeImpl()
+        {
+            Write(_myCode.Replace("%PROJECT_NAME%", Job.ProjectName));
+        }
+    }
+}

Src/PCompiler/CompilerCore/Backend/PInfer/Preamble.cs

@@ -17,6 +17,9 @@ internal class PreambleConstants
         internal static string PredicateEnumeratorFileName = "PredicateEnumerator.java";
         internal static string TermEnumeratorFileName = "TermEnumerator.java";
         internal static string TraceIndexFileName = "TraceIndex.java";
+        // inlined dependencies
+        internal static string[] PObserveDeps = ["PEvent.java", "PValue.java", "Clone.java", "Equality.java",
+                                                "IncomparableValuesException.java", "UncloneableValueException.java"];
         internal static string TraceReaderTemplate = @$"
 import com.alibaba.fastjson2.*;
 
@@ -34,18 +37,18 @@ private JSONArray read(File jsonFile) {{
         }}
     }}
 
-    public List<List<{Constants.EventsClass}<?>>> loadTrace(String fp) {{
+    public List<List<{Constants.EventsClass()}<?>>> loadTrace(String fp) {{
         File jsonFile = new File(fp);
         if (!jsonFile.exists()) {{
             throw new RuntimeException(""Trace file not found: "" + fp);
         }}
-        List<List<{Constants.EventsClass}<?>>> result = new ArrayList<>();
+        List<List<{Constants.EventsClass()}<?>>> result = new ArrayList<>();
         JSONArray traces = read(jsonFile);
         if (traces == null)
             throw new RuntimeException(""Trace "" + jsonFile.getAbsolutePath() + "" cannot be parsed"");
         for (Object obj : traces) {{
             JSONArray trace = (JSONArray) obj;
-            List<{Constants.EventsClass}<?>> events = new ArrayList<>();
+            List<{Constants.EventsClass()}<?>> events = new ArrayList<>();
             for (int i = 0; i < trace.size(); i++) {{
                 JSONObject e = trace.getJSONObject(i);
                 String sender = e.containsKey(""sender"") ? e.getString(""sender"") : null;
@@ -115,7 +118,7 @@ internal static string ReadTemplate(string filename)
             var currentDir = AppDomain.CurrentDomain.BaseDirectory;
             DirectoryInfo info = new(currentDir);
             return string.Join("\n", File.ReadAllLines(
-                Path.Combine(Path.Combine(info.Parent.Parent.Parent.Parent.Parent.ToString(), "PInferTemplates"), filename)
+                Path.Combine(Path.Combine([info.Parent.Parent.Parent.Parent.Parent.ToString(), "Src", "PInfer", "PInferTemplates"]), filename)
             ));
         }
     }