[PEx] Corrections to stateful search, support Java foreign functions

[aman-goel]

Updates include:

[PEx RT]

• Revamp a schedule/data Choice into separate classes ScheduleChoice or DataChoice. Only ScheduleChoice stores protocol state for stateful backtracking. Stateful backtracking for a DataChoice resumes from the most recent ScheduleChoice.
• Revamp StepState to not track step/choice number, only track current machines and machine states
• Revamp SearchTask to store full list of current choices (prefix) and assigned unexplored choices (suffix).
• Adds support for Java foreign functions
• Corrects replaying liveness/deadlock bug
• Throw error if N in choose(N) is greater than 10K.
• Minor refactoring and improvements to logging.

[PEx IR]

• Several minor corrections needed relating to dynamic type casting of PValue.
• Updates foreign function interface
• Corrects and improves IR generator for while loop containing receive statement.

[P CLI]

• Adds hidden option --checker-args <colon-separated args> to pass additional options to PEx or PSym.

[Misc]

• Sync with latest changes in master branch
• Adds few unit tests dealing with while and receive statements.

[aman-goel]

Some notes from offline discussion:

• We can safely do stateful backtracking (i.e., without repeating from step 0) only at schedule steps, and not when some machine is executing an event and making a data choice with choose(.). Each schedule step can involve multiple functions getting executed, like executing an event, followed by exiting current state, then entering a new state, then raising an event (all done in one schedule step). In the case of data choices, we would have to restore the intermediate place. So, when jumping to an unexplored data choice, we jump to the starting of the last schedule step and repeat from there until we reach that data choice.
• A step state consists of information relating to a schedule step, like how many machines of each type. And if stateful backtracking is enabled, the protocol state at the beginning of that schedule step.
• What we saw in previous experiments is that storing a single unexplored choice in a SearchTask can result in many more SearchTask objects being created. As well as, needing a separate flow for DFS strategy. With SearchTask composed of a N contiguous unexplored choices (i.e., DFS stack stlye), we can unify easily DFS and other strategies. I.e., if N is infinite, we always have 1 SearchTask and it becomes DFS style. With N = 1, we get what you suggested, exactly one unexplored choice in each search task. N is set by invisible option --schedules-per-task .
• SearchTask at choice number X is indeed a sequence of choices. The first part is composed of sequence of current (i.e., unexplored) choices from 0 to X-1. This is used to stitch together and get the full trace in case of bug or to reconstruct the state at X if stateful backtracking is disabled. The second part is composed of a sequence of unexplored choices starting from X.
• This SearchTask packaging is new. It will evolve with time. Earlier, we had to maintain separate flow for DFS vs random search. Now, we can make them unified and tunable so that each SearchTask is like an unexplored slice rooted at a node in the execution tree. We can make this slice too fine (i.e., N = 1) or too wide (like in DFS where N is no limit).