Merging PEx into the Major release P 3.0 branch. #860
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
TODO: Implement basic new runtime interface to pass code compilation post generation
Removes using PMachineValue for now
Renames Machine/Monitor/Program to PMachine/PMonitor/PModel Corrects PBool value
* [PEx] Correct functions containing goto/raise Changes PEx IR to support functions that contain non-tail ending goto/raise Enables supporting needed function inlining in spec machines Bumps PEx runtime revision to 0.3.0 * [PEx] Remove wrongly-added files * [PEx IR] Correct function inlining for non-null returning functions Add guard conditions to disable function body statement if already returned Throw exception if inlining is unsupported
Merge inprogress/pex into dev_p3.0/pex
Throw compile-time exception for receive statement inside loop with appropriate message Adds try/catch to gracefully report not-supported errors during compiling for PEx PEX RT: exclude tests with receive inside loop
* Update build system and Java compiler, remove dependency JARs * Update CheckerCore logging and state machine components
…ent (#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
* Add global constant varaibles; TODO backend * Updated BuildGlobalScope * add global variable * fix global variable types * Allow multiple tests * Add int list literal syntax * add parametric test * Quick-fix * fix bad quick-fix * add rich syntax * Small merge error * Param (#833) * update assumption * fix: add deps back * refactor: constant -> param * fix * clean the code * unify normal/param/assume tests * clean the code * rename * merging safety test parser rules * clean the code * Update github CI action v2 to v3 * iUpdate github CI action v2 to v3 on ubuntu * rename variable "param" into "parameter" to avoid keyword conflicts * T-wise combinatorial test (#837) * add twise * clean the code * Solved Concerns from Lewis: + new allow twise number be 1 + unify twise number valid condition + add unit test * add new test case * unit test for ParamAssignment.IterateAssignments * merge * fix duplicate declears bug --------- Co-authored-by: Ankush Desai <[email protected]>
ankushdesai
commented
May 13, 2025
There was a problem hiding this comment.
Pull Request Overview
This pull request merges the new PEx components into the major P 3.0 branch, integrating new backend classes and updating configurations, logging, and build pipelines to support the PEx mode. Key changes include:
- New backend classes for PEx (e.g., WhileFunction, ReceiveSplitStmt, Continuation, Constants).
- Updates in the PChecker code generator and configuration to accommodate the new PEx mode.
- Adjustments to the project’s build configuration and workflow files.
Reviewed Changes
Copilot reviewed 188 out of 188 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| Src/PCompiler/CompilerCore/Backend/PEx/WhileFunction.cs | Introduces a simple WhileFunction class with an AddParameter method. |
| Src/PCompiler/CompilerCore/Backend/PEx/ReceiveSplitStmt.cs | Adds a new IPStmt implementation for receive split statements. |
| Src/PCompiler/CompilerCore/Backend/PEx/Continuation.cs | Implements Continuation with parameter management (note an unused assignment). |
| Src/PCompiler/CompilerCore/Backend/PEx/Constants.cs | Provides Maven POM templates with placeholder tokens. |
| Src/PCompiler/CompilerCore/Backend/PEx/CompilationContext.cs | Handles naming and temporary variable management for compilation. |
| Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs | Updates global parameter handling and safety test declaration methods. |
| Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs | Introduces a GlobalConfigName constant. |
| Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs | Documentation clean‐up in API methods. |
| Src/PChecker/CheckerCore/Runtime/StateMachines/Exceptions/OnEventDroppedHandler.cs | Minor docstring update. |
| Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs | Adds new logging callbacks and documentation comments. |
| Src/PChecker/CheckerCore/Runtime/Logging/LogWriter.cs | Updates logging documentation by removing obsolete parameter info. |
| Src/PChecker/CheckerCore/Runtime/Logging/IControlledRuntimeLog.cs | Adjusts docstrings to match the updated API. |
| Src/PChecker/CheckerCore/ExhaustiveEngine.cs | Adjusts argument usage switching from PSymArgs to CheckerArgs. |
| Src/PChecker/CheckerCore/CheckerMode.cs | Adds a new enum value for PEx mode. |
| Src/PChecker/CheckerCore/CheckerCore.csproj | Suppresses documentation warning 1591. |
| Src/PChecker/CheckerCore/CheckerConfiguration.cs | Renames configuration arguments and introduces an EnableDebugging flag. |
| Src/PChecker/CheckerCore/Checker.cs | Adds PEx mode support to the execution switch. |
| Ext/libhandler & .gitmodules | Removes the external libhandler submodule reference. |
| .github/workflows/pex.yml | Provides a GitHub Actions workflow for building and testing PEx. |
aman-goel
requested changes
May 14, 2025
…ality issues, added comments for placeholders, and added missing newlines at the end of files
|
Most of the comments are addressed. |
There was a problem hiding this comment.
Pull Request Overview
This PR merges the PEx backend into the P 3.0 branch and integrates PEx support into the PChecker tool.
- Adds new PEx compiler core classes for while loops, continuations, and receive-split statements
- Extends PChecker code generator, configuration, and runtime to support PEx mode and global parameters
- Removes the libhandler submodule and introduces a GitHub Actions workflow for building/testing PEx
Reviewed Changes
Copilot reviewed 188 out of 188 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| Src/PCompiler/CompilerCore/Backend/PEx/WhileFunction.cs | New WhileFunction class for PEx code generation |
| Src/PCompiler/CompilerCore/Backend/PEx/ReceiveSplitStmt.cs | New ReceiveSplitStmt AST node for PEx |
| Src/PCompiler/CompilerCore/Backend/PEx/Continuation.cs | Continuation class managing local/store mapping |
| Src/PCompiler/CompilerCore/Backend/PEx/Constants.cs | Maven POM template constants for PEx projects |
| Src/PCompiler/CompilerCore/Backend/PEx/CompilationContext.cs | Compilation context with naming and temp vars |
| Src/PCompiler/CompilerCore/Backend/PChecker/PCheckerCodeGenerator.cs | Extends generator with PEx mode and global params |
| Src/PCompiler/CompilerCore/Backend/ICodeGenerator.cs | Added GlobalConfigName constant |
| Src/PChecker/CheckerCore/Runtime/StateMachines/StateMachine.cs | Cleaned up obsolete XML docs for send/create APIs |
| Src/PChecker/CheckerCore/Runtime/StateMachines/Exceptions/OnEventDroppedHandler.cs | Updated handler summary doc |
| Src/PChecker/CheckerCore/Runtime/Logging/PCheckerLogJsonFormatter.cs | Added new log event methods for JSON formatter |
| Src/PChecker/CheckerCore/Runtime/Logging/LogWriter.cs | Removed outdated param doc |
| Src/PChecker/CheckerCore/Runtime/Logging/IControlledRuntimeLog.cs | Refined interface doc comments |
| Src/PChecker/CheckerCore/ExhaustiveEngine.cs | Updated argument logic to use PEx mode |
| Src/PChecker/CheckerCore/CheckerMode.cs | Replaced Verification/Coverage modes with PEx |
| Src/PChecker/CheckerCore/CheckerCore.csproj | Suppressed missing-doc warnings (1591) |
| Src/PChecker/CheckerCore/CheckerConfiguration.cs | Renamed PSymArgs → CheckerArgs, added debugging flag |
| Src/PChecker/CheckerCore/Checker.cs | Switch statements updated for PEx mode |
| Ext/libhandler | Removed libhandler submodule commit |
| .gitmodules | Removed libhandler submodule entry |
| .github/workflows/pex.yml | New GitHub Actions workflow for PEx build/test |
Comments suppressed due to low confidence (1)
Src/PCompiler/CompilerCore/Backend/PEx/ReceiveSplitStmt.cs:14
- [nitpick] The property name 'Cont' is abbreviated and may be unclear. Consider renaming it to 'Continuation' for clarity.
public Continuation Cont { get; }
Comment on lines
+36
to
+37
| var localAccess = new VariableAccessExpr(SourceLocation, local); | ||
| var storeAccess = new VariableAccessExpr(SourceLocation, store); |
There was a problem hiding this comment.
The variables localAccess and storeAccess are created but never used. Consider removing these unused variables to improve readability.
Suggested change
| var localAccess = new VariableAccessExpr(SourceLocation, local); | |
| var storeAccess = new VariableAccessExpr(SourceLocation, store); |
Copilot uses AI. Check for mistakes.
Comment on lines
+32
to
+34
| if (!storeParameters.Select(param => param.Name).Contains(store.Name)) | ||
| storeParameters.Add(store); | ||
| if (!localParameters.Select(param => param.Name).Contains(local.Name)) |
There was a problem hiding this comment.
Using Select(...).Contains(...) can be less efficient than Any; consider using storeParameters.Any(param => param.Name == store.Name) for clarity and a single-pass check.
Suggested change
| if (!storeParameters.Select(param => param.Name).Contains(store.Name)) | |
| storeParameters.Add(store); | |
| if (!localParameters.Select(param => param.Name).Contains(local.Name)) | |
| if (!storeParameters.Any(param => param.Name == store.Name)) | |
| storeParameters.Add(store); | |
| if (!localParameters.Any(param => param.Name == local.Name)) |
Copilot uses AI. Check for mistakes.
|
|
||
| if (!IsAsciiAlphabetic(ident[0])) | ||
| { | ||
| Console.WriteLine(ident[0]); |
There was a problem hiding this comment.
Logging directly to console in a utility method may be unintended. Remove or replace this with proper logging or exception handling.
Suggested change
| Console.WriteLine(ident[0]); | |
| Log($"Invalid starting character in identifier: {ident[0]}"); |
Copilot uses AI. Check for mistakes.
| @@ -21,6 +21,12 @@ public class PCheckerCodeGenerator : ICodeGenerator | |||
| /// This compiler has a compilation stage. | |||
| /// </summary> | |||
| public bool HasCompilationStage => true; | |||
| private static List<Variable> _globalParams = []; | |||
There was a problem hiding this comment.
The initializer '[]' is not valid for List. It should be initialized as 'new List()'.
Suggested change
| private static List<Variable> _globalParams = []; | |
| private static List<Variable> _globalParams = new List<Variable>(); |
Copilot uses AI. Check for mistakes.
| PEx-Build-And-Test-Ubuntu: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - uses: actions/checkout@v1 |
There was a problem hiding this comment.
[nitpick] This workflow uses an outdated actions/checkout version. Consider upgrading to 'actions/checkout@v3' for better performance and security.
Suggested change
| - uses: actions/checkout@v1 | |
| - uses: actions/checkout@v3 |
Copilot uses AI. Check for mistakes.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.