Finish Python Soundness Tests #4
Description
The SoundnessSpec module defines what relation between a concrete interpreter and our abstract interpreter should hold.
Currently, the tests are complete for Scheme (stores from the abstract and the concrete semantics are compared to determine whether the analysis is sound), unfortunately, the same is not true for the Python Analysis.
Some infrastructure for Python is already provided. A pythonSoundness specification is written, but an implementation for comparing the analysis' store with the actual concrete memory is missing.
Implementing this using existing Python interpreter is tricky:
- The analysis uses a lot of memory allocations to abstract heap-allocated objects. Similar allocations have to happen at the concrete side so that concrete addresses can be compared to abstract addresses.
- Communicating between an existing Python interpreter and Monarch is tricky. One way to achieve this is to use the stdout or stderr of the Python process to communicate concrete information about the program. This approach was used in the soundness tests contained within SimpleActor analysis (i.e.,
analysis/simpleactor) but is more difficult for Python since it has more complex data types and events (function calls, method lookup, ...) than the SimpleActor language.
In any case, to use existing Python interpreters, some form of instrumentation and/or shadow execution will be necessary so that we can access the internals of the concrete interpreter (i.e., memory, addresses, ...).