[Soot-list] Bytecode offsets and stack offsets question

[Soha H]

Hello,

  We are interested in trying to instrument the Java Symbolic Pathfinder
model checker in order to support static symbolic execution of code regions
(Veritesting).  To be able to do this, we need to identify regions of code
that can be statically executed and to translate the static regions.  We
were hoping to use Soot to do this; Shimple is an SSA form that is
straightforward to translate into static symbolic execution regions.

However in order to do so, we need to be able to precisely map bytecode
addresses for instructions corresponding to locations in Shimple, as well
as stack offsets and object field references to identifiers in Shimple.
The instruction locations will be used to "trap" the SPF execution to start
static symbolic execution.  At these trap points, we need to be able to
transfer information in and out of the stack locations and field references
that are used by the static code region.

Is it possible to use "as-is" or modify Soot in order to provide this
information?  We are interested either in the information from the original
code, or, if it is easier, rewritten bytecode from the Soot Shimple form.
In previous versions of Soot, we could grab the bytecode instructions, but
it looks like the current version using the ASM front end no longer has
support for this.

Once again, the things we need specifically are:
  - the java bytecode offsets corresponding to Shimple branching statements
  - the stack offsets for local variables referenced in Shimple
  - the field numbers associated with field references in Shimple.

Thank you very much for your time!


Soha
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20170925/f6611936/attachment-0001.html>