Merge inprogress/pex into dev_p3.0/pex #841
Merged
Conversation
This file contains 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
0: ok, 2: bug, 3: bug (too_many_choices), 4: timeout, 5: memout, 6: error
[PEx] minor change
* [PEx] Several updates to logging, PEx config Changes default max choices limit to 20 per call and 250 per schedule (to account for open-source protocols with monolithic transition relation modeled as single action) Adds logging support to print choose(.) location info for easy debugging TooManyChoicesException via replayer log Minor correction * [PEx] Refactoring and formatting changes * [PEx] Update cli default Change each task to 2K schedules by default
Make sure continuation with loop does not declare local var twice
* [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
There was a problem hiding this comment.
Copilot reviewed 133 out of 136 changed files in this pull request and generated 1 comment.
Files not reviewed (3)
- Src/PRuntimes/PExRuntime/pom.xml: Language not supported
- Src/PRuntimes/PExRuntime/scripts/build.sh: Language not supported
- Src/PRuntimes/PExRuntime/src/main/java/META-INF/MANIFEST.MF: Language not supported
| var localAccess = new VariableAccessExpr(SourceLocation, local); | ||
| var storeAccess = new VariableAccessExpr(SourceLocation, store); | ||
| var storeStmt = new AssignStmt(SourceLocation, storeAccess, localAccess); | ||
| storeForLocal.Add(local, store); |
There was a problem hiding this comment.
The local variable 'storeStmt' is created but never used; consider either removing this assignment or employing the created statement in the continuation's logic.
Suggested change
| storeForLocal.Add(local, store); | |
| storeForLocal.Add(local, store); | |
| statements.Add(storeStmt); |
Copilot is powered by AI, so mistakes are possible. Review output carefully before use.
aman-goel
reviewed
Apr 8, 2025
aman-goel
reviewed
Apr 8, 2025
aman-goel
approved these changes
Apr 9, 2025
ankushdesai
approved these changes
Apr 14, 2025
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.
dev_p3.0/pex has changes from major/P3.0 and master branch
This PR merges all the changes from inprogress/pex to dev_p3.0/pex