[PObserve/CLI] Updates (#656)

* [PSym] Force minimum version, update logs

* [PSym] Bump version

* [PObserve] Adds --pobserve-package <string> option

Adds hidden option -po <str> to configure PObserve package name in generated output (defaults to <project-name>.pobserve as before)

* [PObserve] Support static functions

Adds support for printing static functions that are used in the spec

Implemented via tracking all static functions that are called during spec code generation and printing those static functions after spec code is generated

* [CLI] Update auto-detection of P compiled assembly

Update auto-detection to use OutputDir from *.pproj file (if present) instead of CWD

Src/PChecker/CheckerCore/CheckerConfiguration.cs

@@ -19,6 +19,12 @@ namespace PChecker
     public class CheckerConfiguration
     {
 
+        /// <summary>
+        /// The P compiled path.
+        /// </summary>
+        [DataMember]
+        public string PCompiledPath;
+
         /// <summary>
         /// The output path.
         /// </summary>
@@ -280,6 +286,7 @@ public int MaxSchedulingSteps
         /// </summary>
         protected CheckerConfiguration()
         {
+            PCompiledPath = Directory.GetCurrentDirectory();
             OutputPath = "PCheckerOutput";
 
             Timeout = 0;

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

@@ -115,10 +115,10 @@ internal static string AsFFIComment(string line)
     <modelVersion>4.0.0</modelVersion>
 
     <groupId>com.amazon.p</groupId>
-    <artifactId>-project-name-</artifactId>
+    <artifactId>-package-name-</artifactId>
     <version>1.0-SNAPSHOT</version>
 
-    <name>-project-name-</name>
+    <name>-package-name-</name>
     <properties>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
         <maven.compiler.source>11</maven.compiler.source>
@@ -165,7 +165,6 @@ internal static string AsFFIComment(string line)
                 </executions>
             </plugin>
         </plugins>
-        <directory>${{buildDirectory}}</directory>
         <sourceDirectory>.</sourceDirectory>
     </build>
 </project>";

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

@@ -14,7 +14,7 @@ public void GenerateBuildScript(ICompilerConfiguration job)
 
             // create the pom.xml file
             var pomTemplate = Constants.pomTemplate;
-            pomTemplate = pomTemplate.Replace("-project-name-",job.ProjectName);
+            pomTemplate = pomTemplate.Replace("-package-name-",job.PObservePackageName);
 
             string foreignInclude = "";
             var foreignFiles = job.InputForeignFiles.Where(x => x.EndsWith(".java"));

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

@@ -14,7 +14,7 @@ public abstract class JavaSourceGenerator
 
         internal NameManager Names => _context.Names;
         internal TypeManager Types => _context.Types;
-        internal String PackageName => $"{Job.ProjectName}.pobserve";
+        internal String PackageName => $"{Job.PObservePackageName}";
 
         /// <summary>
         /// Constructs a new Java source generator for a particular output file.

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

@@ -15,6 +15,7 @@ internal class MachineGenerator : JavaSourceGenerator
     {
 
         private Machine _currentMachine; // Some generated code is machine-dependent, so stash the current machine here.
+        private HashSet<Function> _calledStaticFunctions = new HashSet<Function>(); // static functions allowed 
 
         internal MachineGenerator(ICompilerConfiguration job, string filename) : base(job, filename)
         {
@@ -47,6 +48,13 @@ protected override void GenerateCodeImpl()
                 }
                 _currentMachine = null;
             }
+
+            // static functions
+            foreach (var f in _calledStaticFunctions)
+            {
+                WriteFunction(f);
+            }
+
             WriteLine("}");
         }
 
@@ -608,7 +616,7 @@ private void WriteFunctionCallExpr(Function f, IEnumerable<IPExpr> args)
             var isStatic = f.Owner == null;
             if (isStatic && !f.IsForeign)
             {
-                throw new NotImplementedException("StaticFunCallExpr is not implemented.");
+                _calledStaticFunctions.Add(f);
             }
 
             var fname = Names.GetNameForDecl(f);

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

@@ -62,7 +62,7 @@ internal class Constants
         <dependency>
             <groupId>io.github.p-org</groupId>
             <artifactId>psym</artifactId>
-            <version>[1.0.10,)</version>
+            <version>[1.1.0,)</version>
         </dependency>
 
         <!-- https://mvnrepository.com/artifact/org.projectlombok/lombok -->

Src/PCompiler/CompilerCore/CompilerConfiguration.cs

@@ -16,6 +16,7 @@ public CompilerConfiguration()
             InputForeignFiles = new List<string>();
             Output = null;
             ProjectName = "generatedOutput";
+            PObservePackageName = $"{ProjectName}.pobserve";
             ProjectRootPath = new DirectoryInfo(Directory.GetCurrentDirectory());
             LocationResolver = new DefaultLocationResolver();
             Handler = new DefaultTranslationErrorHandler(LocationResolver);
@@ -47,6 +48,7 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, Co
                 }
             }
             ProjectName = projectName ?? Path.GetFileNameWithoutExtension(inputFiles[0]);
+            PObservePackageName = $"{ProjectName}.pobserve";
             ProjectRootPath = projectRoot;
             LocationResolver = new DefaultLocationResolver();
             Handler = new DefaultTranslationErrorHandler(LocationResolver);
@@ -59,6 +61,7 @@ public CompilerConfiguration(ICompilerOutput output, DirectoryInfo outputDir, Co
         public DirectoryInfo OutputDirectory { get; set; }
         public CompilerOutput OutputLanguage { get; set; }
         public string ProjectName { get; set; }
+        public string PObservePackageName { get; set; }
         public DirectoryInfo ProjectRootPath { get; set; }
         public ICodeGenerator Backend { get; set; }
         public IList<string> InputPFiles { get; set; }
@@ -79,6 +82,7 @@ public void Copy(CompilerConfiguration parsedConfig)
             LocationResolver = parsedConfig.LocationResolver;
             ProjectDependencies = parsedConfig.ProjectDependencies;
             ProjectName = parsedConfig.ProjectName;
+            PObservePackageName = parsedConfig.PObservePackageName;
             OutputLanguage = parsedConfig.OutputLanguage;
             ProjectRootPath = parsedConfig.ProjectRootPath;
         }

Src/PCompiler/CompilerCore/ICompilerConfiguration.cs

@@ -8,6 +8,7 @@ namespace Plang.Compiler
     public interface ICompilerConfiguration
     {
         string ProjectName { get; }
+        string PObservePackageName { get; }
         DirectoryInfo ProjectRootPath { get; }
         CompilerOutput OutputLanguage { get; }
         ICompilerOutput Output { get; }

Src/PCompiler/PCommandLine/Options/PCheckerOptions.cs

@@ -86,6 +86,12 @@ internal CheckerConfiguration Parse(string[] args)
             try
             {
                 var result = Parser.ParseArguments(args);
+                // if there are no --pproj or --pfiles arguments, then search for a pproj file locally and load it
+                FindLocalPProject(result);
+
+                // load pproj file first
+                UpdateConfigurationWithPProjectFile(configuration, result);
+
                 foreach (var arg in result)
                 {
                     UpdateConfigurationWithParsedArgument(configuration, arg);
@@ -119,6 +125,50 @@ internal CheckerConfiguration Parse(string[] args)
             return configuration;
         }
 
+        private static void FindLocalPProject(List<CommandLineArgument> result)
+        {
+            // CommandLineOutput.WriteInfo(".. Searching for a P project file *.pproj locally in the current folder");
+            var filtered = 
+                from file in Directory.GetFiles(Directory.GetCurrentDirectory(), "*.pproj")
+                let info = new FileInfo(file)
+                where (((info.Attributes & FileAttributes.Hidden) ==0)& ((info.Attributes & FileAttributes.System)==0))
+                select file;
+            var files = filtered.ToArray();
+            if (files.Length == 0)
+            {
+                // CommandLineOutput.WriteInfo(
+                //     $".. No P project file *.pproj found in the current folder: {Directory.GetCurrentDirectory()}");
+            }
+            else
+            {
+                var commandlineArg = new CommandLineArgument();
+                commandlineArg.Value = files.First();
+                commandlineArg.LongName = "pproj";
+                commandlineArg.ShortName = "pp";
+                // CommandLineOutput.WriteInfo($".. Found P project file: {commandlineArg.Value}");
+                result.Add(commandlineArg);
+            }
+        }
+
+
+        /// <summary>
+        /// Updates the checker configuration with the specified P project file.
+        /// </summary>
+        private static void UpdateConfigurationWithPProjectFile(CheckerConfiguration configuration, List<CommandLineArgument> result)
+        {
+            foreach (var option in result)
+            {
+                switch (option.LongName)
+                {
+                    case "pproj":
+                    {
+                        new ParsePProjectFile().ParseProjectFileForChecker((string)option.Value, configuration);
+                    }
+                        return;
+                }
+            }
+        }
+
         /// <summary>
         /// Updates the checkerConfiguration with the specified parsed argument.
         /// </summary>
@@ -257,6 +307,9 @@ private static void UpdateConfigurationWithParsedArgument(CheckerConfiguration c
                 case "jvm-args":
                     checkerConfiguration.JvmArgs = ((string)option.Value).Replace(':', ' ');
                     break;
+                case "pproj":
+                    // do nothing, since already configured through UpdateConfigurationWithPProjectFile
+                    break;
                 default:
                     throw new Exception(string.Format("Unhandled parsed argument: '{0}'", option.LongName));
             }
@@ -306,7 +359,7 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura
         {
             if (checkerConfiguration.AssemblyToBeAnalyzed == string.Empty)
             {
-                CommandLineOutput.WriteInfo(".. Searching for a P compiled file locally in the current folder");
+                CommandLineOutput.WriteInfo($".. Searching for a P compiled file locally in folder {checkerConfiguration.PCompiledPath}");
                 var pathSep = Path.DirectorySeparatorChar;
 
                 string filePattern =  checkerConfiguration.Mode switch
@@ -323,7 +376,7 @@ private static void FindLocalPCompiledFile(CheckerConfiguration checkerConfigura
 
 
                 var files = 
-                    from file in Directory.GetFiles(Directory.GetCurrentDirectory(), filePattern, enumerationOptions)
+                    from file in Directory.GetFiles(checkerConfiguration.PCompiledPath, filePattern, enumerationOptions)
                     let info = new FileInfo(file)
                     where (((info.Attributes & FileAttributes.Hidden) ==0)& ((info.Attributes & FileAttributes.System)==0))
                     select file;

Src/PCompiler/PCommandLine/Options/PCompilerOptions.cs

@@ -42,6 +42,8 @@ internal PCompilerOptions()
             var modes = Parser.AddArgument("mode", "md", "Compilation mode :: (bugfinding, verification, coverage, pobserve, stately). (default: bugfinding)");
             modes.AllowedValues = new List<string>() { "bugfinding", "verification", "coverage", "pobserve", "stately" };
             modes.IsHidden = true;
+
+            Parser.AddArgument("pobserve-package", "po", "PObserve package name").IsHidden = true;
         }
 
         /// <summary>
@@ -132,7 +134,7 @@ private static void UpdateConfigurationWithPProjectFile(CompilerConfiguration co
                 {
                     case "pproj":
                     {
-                        new ParsePProjectFile().ParseProjectFile((string)option.Value, out var parsedConfig);
+                        new ParsePProjectFile().ParseProjectFileForCompiler((string)option.Value, out var parsedConfig);
                         compilerConfiguration.Copy(parsedConfig);
                     }
                         return;
@@ -169,6 +171,9 @@ private static void UpdateConfigurationWithParsedArgument(CompilerConfiguration
                         compilerConfiguration.Backend = TargetLanguage.GetCodeGenerator(compilerConfiguration.OutputLanguage);
                     }
                     break;
+                case "pobserve-package":
+                    compilerConfiguration.PObservePackageName = (string)option.Value;
+                    break;
                 case "pfiles":
                     {
                         var files = (string[])option.Value;

Src/PCompiler/PCommandLine/Parser/ParsePProjectFile.cs

@@ -3,6 +3,7 @@
 using System.IO;
 using System.Linq;
 using System.Xml.Linq;
+using PChecker;
 using PChecker.IO.Debugging;
 using Plang.Compiler;
 
@@ -12,12 +13,12 @@ internal class ParsePProjectFile
     {
 
         /// <summary>
-        /// Parse the P Project file
+        /// Parse the P Project file for compiler
         /// </summary>
         /// <param name="projectFile">Path to the P project file</param>
         /// <param name="job">out parameter of P compilation job, after parsing the project file</param>
         /// <returns></returns>
-        public void ParseProjectFile(string projectFile, out CompilerConfiguration job)
+        public void ParseProjectFileForCompiler(string projectFile, out CompilerConfiguration job)
         {
             job = null;
             try
@@ -65,6 +66,33 @@ public void ParseProjectFile(string projectFile, out CompilerConfiguration job)
             }
         }
 
+        /// <summary>
+        /// Parse the P Project file for P checker
+        /// </summary>
+        /// <param name="projectFile">Path to the P project file</param>
+        /// <param name="job">out parameter of P checker job, after parsing the project file</param>
+        /// <returns></returns>
+        public void ParseProjectFileForChecker(string projectFile, CheckerConfiguration job)
+        {
+            try
+            {
+                if (!CheckFileValidity.IsLegalPProjFile(projectFile, out var projectFilePath))
+                {
+                    throw new CommandlineParsingError($"Illegal P project file name {projectFile} or file {projectFilePath?.FullName} not found");
+                }
+
+                // set compiler output directory as p compiled path
+                job.PCompiledPath = GetOutputDirectoryName(projectFilePath);
+            }
+            catch (CommandlineParsingError ex)
+            {
+                Error.ReportAndExit($"<Error parsing project file>:\n {ex.Message}");
+            }
+            catch (Exception other)
+            {
+                Error.ReportAndExit($"<Internal Error>:\n {other.Message}\n <Please report to the P team or create a issue on GitHub, Thanks!>");
+            }
+        }
 
 
         /// <summary>
@@ -141,6 +169,20 @@ private DirectoryInfo GetOutputDirectory(FileInfo fullPathName)
                 return new DirectoryInfo(Directory.GetCurrentDirectory());
         }
 
+        /// <summary>
+        /// Parse the output directory information from the pproj file
+        /// </summary>
+        /// <param name="fullPathName"></param>
+        /// <returns>If present returns the output directory name, else the current directory name</returns>
+        private string GetOutputDirectoryName(FileInfo fullPathName)
+        {
+            var projectXml = XElement.Load(fullPathName.FullName);
+            if (projectXml.Elements("OutputDir").Any())
+                return projectXml.Element("OutputDir")?.Value;
+            else
+                return Directory.GetCurrentDirectory();
+        }
+
         private void GetTargetLanguage(FileInfo fullPathName, ref CompilerOutput outputLanguage, ref bool generateSourceMaps)
         {
             var projectXml = XElement.Load(fullPathName.FullName);

Src/PRuntimes/PSymRuntime/pom.xml

@@ -327,7 +327,7 @@
         <maven.compiler.target>11</maven.compiler.target>
         <log4j2.configurationFile>${project.basedir}/src/main/resources/log4j2.xml</log4j2.configurationFile>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-        <revision>1.0.11</revision>
+        <revision>1.1.1</revision>
 
         <deps.path>${project.basedir}/../../../Bld</deps.path>
 

Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSearchScheduler.java

@@ -382,21 +382,25 @@ public void reportEstimatedCoverage() {
       SearchLogger.log(String.format("Distinct States Explored %d", totalDistinctStateCount));
     }
 
-    BigDecimal coverage = PSymGlobal.getCoverage().getEstimatedCoverage(22);
-    assert (coverage.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+    BigDecimal coverage22 = PSymGlobal.getCoverage().getEstimatedCoverage(22);
+    assert (coverage22.compareTo(BigDecimal.ONE) <= 0) : "Error in progress estimation";
+
+    BigDecimal coverage12 = PSymGlobal.getCoverage().getEstimatedCoverage(12);
 
     String coverageGoalAchieved = PSymGlobal.getCoverage().getCoverageGoalAchieved();
     if (isFinalResult && PSymGlobal.getResult().equals("correct for any depth")) {
       PSymGlobal.getCoverage();
+      coverage22 = CoverageStats.getMaxCoverage();
+      coverage12 = CoverageStats.getMaxCoverage();
       coverageGoalAchieved = CoverageStats.getMaxCoverageGoal();
     }
 
-    StatWriter.log("progress", String.format("%.22f", coverage));
+    StatWriter.log("progress", String.format("%.22f", coverage22));
     StatWriter.log("coverage-achieved", String.format("%s", coverageGoalAchieved));
 
     SearchLogger.log(
         String.format(
-            "Progress Guarantee       %.12f", PSymGlobal.getCoverage().getEstimatedCoverage(12)));
+            "Progress Guarantee       %.12f", coverage12));
     SearchLogger.log(String.format("Coverage Goal Achieved   %s", coverageGoalAchieved));
   }