# SPOT: Testing Stream Processing Programs with Symbolic Execution and Stream Synthesizing
## 3 Symbolic Analysis Approach
### Implementing JPF-Flink  
To be concrete, we choose Apache Flink as our subject DSP platform. Thus the JPF-DSP in Figure 3 is named JPF-Flink more specifically. JPF-Flink is a JPF extension built on jpf-core, providing symbolic analysis for Flink programs by interacting with SPF. It interprets the byte codes of one Flink program in a customized way. Once the byte codes relating to one Flink operator or its internal UDFs are detected, they will be redirected out of the standard byte code execution flow, and JPF-Flink will make necessary preparations for symbolic analysis and then delegate the symbolic execution to SPF. To make JPF-Flink work, we implement the main components as follows.  
**FlinkSymbolicInstructionFactory**. It extends the SymbolicInstructionFactory from SPF and is used to intercept the calls to invokevirtual byte code, which is one of the Java standard instructions and invokes instance method. We implement our Flink operator detection logic by overriding the invokevirtual method. This class is responsible for detecting whether the current instruction is relevant to Flink operators. Once instructions about Flink operators are detected, this class will emit a customized INVOKEVIRTUAL instruction.  
**INVOKEVIRTUAL.** We customize the new instruction execution flow by overriding the execute method in INVOKEVIRTUAL class from SPF. Once the new INVOKEVIRTUAL executes, that is to say, the execute method is invoked, we will compound several symbolic configuration clauses as the form \"symbolic.method=\" to specify the methods and their parameters to be executed symbolically.  
**FlinkOPListener.** It extends the PropertyListenerAdapter [[https://github.com/javapathfinder/jpf-core/wiki/Listeners](https://github.com/javapathfinder/jpf-core/wiki/Listeners)]([https://github.com/javapathfinder/jpf-core/wiki/Listeners](https://github.com/javapathfinder/jpf-core/wiki/Listeners)), accessed on 28 July 2021 from jpf-core. The FlinkOPListener monitors all VM- and Search-related events from JPF, and takes actions correspondingly. We override methods like instructionExecuted (every executing instruction will invoke this method), methodExited (the instruction that finishes running one operator will invoke it), et cetera. Once some interesting instructions are detected, this class will respond by calling the corresponding methods in OPSequenceCoordinator.  
**OPSequenceCoordinator**. It is the real workhorse that takes solid actions after FlinkOPListener receives interested events after executing instructions. For instance, once one instruction (detected in FlinkOPListener) corresponds to some Flink operator is detected, we then set up processing strategies (e.g., symbolic expression generation, et cetera) corresponding to this operator.  
**FlinkValidator.** It is used to determine whether one instruction corresponds to Flink operators or UDFs. The Flink operators that we will analyze are prespecified in one global ArrayList. Then, we can check by extracting the method's name from instructions and searching this global ArrayList. UDFs are determined by analyzing their parent operators.