Modify bytecode injection logic for the new model checking algorithm

[eupp]

As a part of merging #410 , I moved some of the code into separate PR.

In particular, in this PR I transferred the required changes in the bytecode instrumentation:

• Add type parameter to memory access injection functions, representing the JVM type of the instrumented field or array access.
• Add optional ability to intercept results of reads and method calls.
• Add a flag to control whether final fields should be tracked or not.
• Add thread id parameter to onActorFinish method.

[ndkoval]

Let's postpone this PR until we pull changes from the trace-debugger branch