[PEx] Disable support for receive statement inside loop #843
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
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
ankushdesai
added a commit
that referenced
this pull request
May 21, 2025
* Removed the C backend completely in the P 2.1 * Upgraded P to use .Net 8.0 * Updated the actions to .Net 8.0 * [PSym] Upgrade to .NET 8.0 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [PCover] Adds initial version of cleaned up PCover backend TODO: Implement basic new runtime interface to pass code compilation post generation * [PCover] Minor * [PCover IR] Cleans up logic relating to event handlers Removes using PMachineValue for now * [CLI] Adds new pcover cli (hidden) * [PCover IR] Cleanup IR for sending event, machine creation, etc. * [PCover runtime] Adds basic runtime setup files * [PCover] Adds placeholder for CLI config * [PCover] Adds main and trace loggers using Log4J * [PCover] Adds event buffer represented as fifo queue with sender semantics * [PCover] Adds event handler placeholders * [PCover] Adds event/message placeholders * [PCover] Adds basic code for machine/state/test driver * [PCover] Adds basic code for scheduler * [PCover] Adds global data structures and program interface * [PCover] Adds utils * [PCover IR] Minor renaming * [PCover] Adds PValues for P data types * [PCover] Renaming and minor corrections Renames Machine/Monitor/Program to PMachine/PMonitor/PModel Corrects PBool value * [PCover] Minor update to javadocs * [PCover] Reformating * [PCover IR+RT] Rename Message to PMessage * [CLI] Minor correction * [PExplicit] Renames new PCover to PExplicit * [PExplicit] Minor correction to CLI * [PExplicit RT] Rename repeat to current, backtrack to unexplored choices * [PExplicit RT] Adds CLI options and config * [PExplicit RT] Adds new exceptions when a bug is found * [PExplicit RT] Adds timeout/memout monitors * [Pexplicit RT] Adds utils for timed call, random number generator, and in-line asserts * [Pexplicit RT] Adds more logging functions * [PExplicit RT] Updates machine and message queues to check if machine can run and if a message is a create machine event * [PExplicit RT] Add function to check if an event is a create machine event * [PExplicit RT] Improve choices and schedule fields * [PExplicit RT] Implements main PExplicit fentry point, runtime executor service, making timed call Deletes DeferQueue. Instead the plan is to handle defers as in C# runtime. Updates global fields * [PExplicit RT] Updates loggers Adds new log functions to the main logger, adds a scratch logger for intermediate printing * [PExplicit RT] Implements and cleans up certain PMachine/State functions * [PExplicit RT] Adds initial version of scheduler Work in progress: finish pending TODOs and JavaDoc comments * [PExplicit RT] Implements basic machine/scheduler/FIFO functions TODOs: receives, defers, etc. * [PExplicit RT] Adds initial support for stateless dfs-style backtracking Adds tracking all machine instances in global context * [PExplicit IR] Removes StringVS TODO: support formatted arguments in PString in RT * [PExplicit RT] Corrects basic dfs-search Corrects adding new machines to global and schedule context Adds basic functions for PMessage Corrects scheduler DFS-style search working on pingPong * [PExplicit RT] Improves how peeking into a machine's FIFO queue works * [PExplicit] Support formatted PString, initial support for defers and receives Adds support for formatted string Adds continuations to runtime and cleans up IR with a simplified interface Adds partial support for defers and receives TODO: finish defer and receive handling * [PExplicit RT] Adds support for defers and blocking receive Adds tracking deferred events via a defer queue Adds PContinuation to track all continuations Adds blocking on a continuation, and unblocking when handling one of the corresponding case event Corrects peeking logic in sender queue Renames FifoQueue to SenderQueue * [PExplicit] Adds support for receives, loops, and named tuple constructor Cleans up support for receives. Adds support for receives within while loop Simplifies IR for loops Updates PValue for PCollection types Corrects constructor for PNamedTuple * [PExplicit] Implements operations for primitive PValue types Minor renaming * [PExplicit] Adds running mvn test and github ci action * [PExplicit RT] Implement raising an event * Disable GitHub CI actions temporarily to only run PExplicit CI * [PExplicit] Several minor updates Support goto event handlers with transition functions Correct PTuple constructor Correct status and result when a bug is bound Cleanup return in functions in IR. Start adding pending/unsupported tests in PExplicit test runner * [PExplicit] Support announce, correct named tuple set ffield, support != operation * [PExplicit] Several corrections Implement raise event, updates logging, updates PCollection to be an interface, updates exclude list for regression runs Adds enforcing max step bound * [PExplicit] Correct raise event with payload * [PExplicit] Correct PString constructor * [PExplicit IR] Exit current flow context if raise or goto statements are present * Update gitignore * [PExplicit] Several corrections Changes PCollection types to not take parameters (so that collections over any type can be allowed) Corrects choosing from a PCollection Corrects IR to track whether function exited or not Avoid printing redundant code if receive cases already exited * [PExplicit] Support enum references with values specified Support enum to int Update excluded regressions list * [PExplicit IR] Correct dynamic type casting in IR * Suppress github ci failures due to not running them on current branch * [PExplicit] Cleaned up type casting in IR Added type casting regressions Corrected PTuple set field * [PExplicit] Support continue statement Remove unreachable code after receive case block * [PExplicit] Several small upgrades Support blocking receives during state transitions and exit functions Support getting values of a PMap Add logging for entering and exiting a state * [PExplicit] Several corrections and minor lang feature support Corrects type casting from any when a function returns a value Adds catching null pointer and stack overflow exceptions as a bug Implement get or default from a PMap Comments out liveness test regressions for now (added TODO) Cleans up PMachineValue constructor * [PExplicit] Refactoring and cleanup * Undo temporary changes to GitHub CI * [PExplicit] Update pom, minor refactoring * [PExplicit] Update to java 17 * [PExplicit] Minor: report class cast exception as a bug * [PExplicit] Convert run status to enum * [PExplicit] Clean up control flow relating to pending state transition (exit/new-state-entry) Renames blockedEntryState to blockedNewStateEntry * [PExplicit] Update comments * Added support for generating a warning when spec handles an event but does not add it in its observes list (#716) * Create custom converter for JSON serialization in .NET8 (#717) * Create custom converter for JSON serialization in .NET8 * Add check for different dictionary type for null replacement --------- Co-authored-by: Eric Hua <[email protected]> * [PExplicit] Support deadlock and liveness checking Adds deadlock checking Adds basic liveness checking, based on whether a monitor is in a hot state at the end of a schedule Updates logger to resemble like in C# * [PExplicit] Minor * [PExplicit] Adds buggy trace replayer and basic .schedule writer * [PExplicit] Correct issues when replaying buggy trace Corrected catching null/class-cast errors when replaying Corrected how a machine resets (to reset variables relating to blocking receives) Corrected how current choice is fetched when replaying * [PExplicit] Adds TextWriter to write trace in txt format Updates logging * [PExplicit] Correct halt event name * [PExplicit] Adds state caching Adds state caching to avoid revisiting same state more than once State caching mode can be: none, fingerprint (i.e., use hash codes), or exact (use exact values). Fingerprinting is the default. Updates logging and stats to track and report distinct states Minor cleanup to IR * [PExplicit] Minor refactoring * [PExplicit] Correct cycle error in replayer, enforce cycle detection only when --fail-on-maxsteps enabled * [PExplicit] Correct local var names in IR * [PExplicit] Correct replayer, add initial version of stateful backtracking * [PExplicit] Correct backtracking * [PExplicit] Refactor and enable stateful backtracking * [PExplicit] Minor improvement to stateful backtracking * [PExplicit] Reformat code * [PExplicit] More reformatting * [PExplicit] Minor corrections Correct comparing machines (including monitors) Correct printing step state * [PExplicit] Correct PMachine/PMonitor hashCode and compateTo functions * [PExplicit] Uniquify instanceId for PMachine as well as PMonitor * [PExplicit] Improve state caching Adds storing hashcode and string representation during PValue initialization Adds new state caching modes using hash functions from guava library New state caching modes include: hashcode (java built in, 32-bit), siphash24 (64-bit), murmur3_128 (128-bit, default), sha256 (256-bit), or exact (using exact string representation) * [PExplicit] Add non-chronological search Adds non-chronological search that implements search beyond DFS. New search modes include random, astar Each run is executed over search tasks, with each task tracking the set of unexplored choices it is assigned to explore Each search task can create new children sub-tasks * [Pexplicit] Minor * [PExplicit] Minor refactoring * [PExplicit] Refactoring and cleanup * Limit number of choices in choose expression to at most 10000 (#725) * Limit number of choices in a choose(.) to atmost 10,000 Adds throwing a compile-time or runtime error if the number of choices in a choose(.) is greater than 10000. Updates GitHub docs to reflect this change. * Adds regression tests for choose exceeding 10000 choices * [PSym] Throw error if number of choices are greater than 10000 * Make PEvents and PTypes serializable in java (#726) * [PExplicit IR] Minor correction * [PExplicit] Update usage via P CLI * [PExplicit] Several corrections to choice tracking Change choice in a schedule to be either ScheduleChoice or DataChoice Step state does not track step/choice number, only tracks current machines and machine states (in stateful backtracking) Correct SearchTask to store full list of prefix/suffix choices. Suffix choices contain list of unexplored choices assigned to this task. Update how liveness/deadlock checking is asserted and replayed. * [PExplicit] Minor refactoring * [PExplicit] Refactoring and setting defaults * [PExplicit] Correct counting unexplored choices * [PExplicit] Minor changes to logging and asserts * [PExplicit] Throw error if number of choices in choose(.) exceeds 10K * [PExplicit] Correct stateful backtracking with complex data choices * [PEx] Minor update * [PEx] Support Java foreign functions * [PEx] Minor corrections to IR * [PEx] Minor: correct an assertion * [PEx] Make receive inside while as not implemented for now Update enum logging and stats reporting PMap: throw error if adding already existing key * [PEx] Experimenting with while and receive in IR * [PEx] Correct corner cases with while, receive, and after statements * [Tst] Add unit test to check interaction between while, receive w/ case payload, and after statements after receive and while * Removed the C backend completely in the P 2.1 * [PCover] Adds temporary CLI mode to trigger new explicit engine * [CLI] Adds new pcover cli (hidden) * [PExplicit] Renames new PCover to PExplicit * Correct sync with mainline * [PEx] Revamps tracking unexplored choices, changes schedule choice (#745) * [PEx] Change schedule choice from PMachine to PMachineId * [PEx] Major revamping of Choice: 1/n Old schedule/data choice changed to schedule/data SearchUnit Added new class for schedule/data Choice, which is just a wrapper around PMachineId/PValue<?> TODO: clean up Schedule with new class structure * Revert "[PEx] Major revamping of Choice: 1/n" This reverts commit 53c5d15. * [PEx] Separates unexplored choices from schedule * [PEx] Cleanup and minor corrections to recent changes to SearchTask * [PEx] Minor correction * [PEx] Corrections to new backtracking logic * [PEx] Adds modes for stateful backtracking Adds CLI option --stateful-backtrack none|intra-task|all to limit stateful backtracking to OFF|within-a-task|ON * [PEx] Add support to serialize and deserialize search tasks in/from file * [PEx] Updates mvn test config * [PEx] Minor correction Fix issue relating to intra-task stateful backtracking with dynamic machine creation * [PEx IR] Minor correction * [PEx] Several improvements to IR Revamps IR to store continuation variables within PContinuation class Adds function to get the default value from a PValue object Removes generating get/set/reset functions for PMachine variables. Instead, using reflection in PEx RT. Minor refactoring * [PEx IR] Minor cleanup * [PEx] Cleanup disk tasks on exit, change defaults Cleanup tasks/ directory on exiting Change default for schedules-per-task to 500 Change report wait time to 10 sec. * [PEx] Minor: create .schedule only if bug is found * [PEx] Adds writing buggy trace in file Adds serializing buggy trace in file Minor renaming * [PEx] Adds option --replay <.schedule file> to replay a buggy trace * [PEx] Minor * [PEx] Fix serialization issues found by P regression tests * [PEx] Minor cleanup * [PEx] Improve cleanup of disk tasks on exit * [PEx] Minor correction Update liveness check, minor renaming * [PEx] Add first version of RL-based choice selection * [PEx] Correct timelines tracking and RL-based choice selection * [PEx] Update timelines, corrects CI * [PEx] Renaming and refactoring Renames PExplicit -> PEx, GlobalFunctions -> PExForeignCode, mode explicit -> pex Refactors PEx IR generator * [CLI] Update PEx CLI options Makes --mode option visible. * [CLI] Cleanup PEx CLI options * [CI] Correct PEx CI * [PEx] Add support for refinement interfaces * [Tutorial] Adds updates for running with PEx Adds changes/hints to enable running with PEx 1_ClientServer: limits number of withdraw requests to at most 5, adds 2 hints to limit data non-determinism 2_TwoPhaseCommit: adds hint to create random transaction without foreign code and with less data non-determinism 3_EspressoMachine: no change * [PEx] Minor: update pom.xml * [PEx] Implements multi-threaded PEx version (#768) * [PEx] Move globals to PExGlobal, adds --nproc CLI option Moves state cache, timelines, num tasks data structures to PEx global class Adds CLI option --nproc to provide number of threads * [PEx] Adds dedicated logger for each thread Moves global results reporting to global class * [PEx] parallel: adds todos, cleans up global class * [PEx] parallel: fix IR, move scheduler specific fields from globals * [PEx] parallel: update IR so that main machine and monitors are created by PEx runtime * [PEx] parallel: make search statistics thread safe * [PEx] parallel: completes first version Several updates: support multi-thread executor, result tracking, exceptions tracking, compiling results, terminating threads, resolving data conflicts, implements lock/release for shared constructs * [PEx] parallel: minor change * [PEx] parallel: update GitHub CI to run with 3 threads * [PEx] parallel: minor corrections Make global machine/monitor instance ids thread safe Add hash/name to PContinuation object for thread-safe state caching * [PEx] Adds tracking and limiting number of choices per choose(.) statement Adds tracking number of calls and total choices generated in a schedule corresponding to each choose(.) statement in the model. Adds option --max-choices-per-call and --max-choices-total to limit max number of choices in a schedule corresponding to a choose(.) statement (default is 10,000 for per choose.) call and no limit on total choices, as in C# backend). Else, a TooManyChoicesException is triggered as a bug. * [PEx] bump version, change cli defaults Change max choices per choose statement to 10 per call and 100 per schedule by default Minor renaming * [PEx] code cleanup and refactoring * [PEx] minor logging changes, [Tst] Change choose(100) to choose(10) * [PEx] Minor logging changes * [PEx] Changes return codes 0: ok, 2: bug, 3: bug (too_many_choices), 4: timeout, 5: memout, 6: error * [PEx] Correct return codes, [Tst] Limit choose choices * [Tutorial] Update hints for PEx [PEx] minor change * [PEx] Minor updates and cleanup (#775) * [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 * [PEx] Minor correction Make sure continuation with loop does not declare local var twice * [PEx] Correct repeated local var declaration in IR * [PEx] Correct code too large error due to receive-inside-loop inlining * [PEx] Adds PLoopObject to track receive-loop variables * [PEx] Minor: correct defaults in help menu * modified cache@v2 to cache@v4 * Rename PEvent to Event, Handle PrimitiveType.Null in GetDefaultValue * [PEx] Correct functions containing non-tail ending goto/raise (#835) * [PEx] Correct inlining for functions returning a value (#840) * [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 * removed CSharp, Java modes in CompilerOutput , removed global.json * Minor changes to make customer model to compile (#842) * [PEx] Disable support for receive statement inside loop (#843) 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 * Dev/remove libhandler (#847) * Update build system and Java compiler, remove dependency JARs (#849) * Update build system and Java compiler, remove dependency JARs * Update CheckerCore logging and state machine components * [PEx] Correct inlining functions with non-null return without assignment (#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 * Moved PEx outside the PRuntimes * Update pex.yml * Update build scripts and test executor; add build documentation * Fix Java version to 17 and correct P build directory path * Pex param test (#855) * 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]> * PR #860 Fixes: Removed Coverage and Verification modes, fixed code quality issues, added comments for placeholders, and added missing newlines at the end of files --------- Co-authored-by: Aman Goel <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: Eric Hua <[email protected]> Co-authored-by: mchadalavada <[email protected]> Co-authored-by: Aishwarya Jagarapu <[email protected]> Co-authored-by: aishu-j <[email protected]> Co-authored-by: ChristineZh0u <[email protected]> Co-authored-by: Zhe Zhou <[email protected]>
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.
Updates include:
[PEx IR]
[PEx RT]
[PCompiler]