map local variables in V.map to those of source program

[Zell]

Hello, I do not see how to *automatically* map the local variables
gathered in v.map to the local variables in the source program?
I suppose there is an option that can give the results in term of
source code instead of quads?

My chord.properties is
**********************
chord.main.class=Main
chord.class.path=classes
chord.src.path=src
chord.run.analyses=V
*************************

My source program is
************
public class Main{
public static void main(String[] args){
String x = "hello";
A a = new A();
}
}
class A{}
*************

and my V.map is
****************
R0!<init>:()V@A
R0!main:([Ljava/lang/String;)V@Main
R1!main:([Ljava/lang/String;)V@Main
T2!main:([Ljava/lang/String;)V@Main
T3!main:([Ljava/lang/String;)V@Main
R4!main:([Ljava/lang/String;)V@Main
R0!<init>:()V...@java.lang.Object
**************

Any ideas? Thanks.

[Ariel Rabkin]

Howdy.

This is something I would also like. Mayur mentioned to me once that
there's a slightly-cumbersome way to do it. I discovered that for my
purposes, I didn't really need it. Line numbers, which are easy to
get, turned out to be more useful.

Here's some background that may be helpful:

The elements in the V domain don't correspond one-to-one with
variables. Internally, they're called "registers".
The ones numbered with a "T" generally correspond to unnamed
temporaries in the source code.
The ones named with R often, but don't always, correspond to named values.

Another relevant fact is that internally, JChord transforms methods
into what's called static-single-assignment form. This means it adds
additional temporaries to make sure that each variable is assigned a
value in exactly one place. So if you have code like a = 5; a*=2; a =
a+b; you'll get three different registers that all hold values for
'a'.

--Ari

> --
> You received this message because you are subscribed to the Google Groups "chord-discuss" group.
> To post to this group, send email to chord-...@googlegroups.com.
> To unsubscribe from this group, send email to chord-discus...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/chord-discuss?hl=en.
>

--
Ari Rabkin asra...@gmail.com
UC Berkeley Computer Science Department

[Zell]

Would you like to share the "slightly-cumbersome way to do it" of
Mayur? It could help. Thanks.

[Mayur Naik]

There is no correct code available that will give you this mapping.  But I'm providing information below that could be a good starting point.  Briefly, your class files need to contain the local variable table attribute (see Section 4.7.9 at http://java.sun.com/docs/books/jvms/second_edition/html/ClassFile.doc.html), and you need to map the (startPC, length, index) values in entries of this table to registers (locals) in the register factory.  This should be doable but is not entirely trivial because the "index" values in the entries are reused for different variables declared in non-overlapping scopes within the same method.  For instance, notice that both local variables named e and st are at index 3 in the below example, which seems fine because the startPC and length values indicate non-overlapping ranges of bytecode indices:

entry: (startPC=26,length=8,nd=e Ljava/io/FileNotFoundException;,index=3)

entry: (startPC=43,length=211,nd=st Ljava/io/StreamTokenizer;,index=3)

This means that you cannot merely map the above index values to registers in joeq, but you also need to map bytecode offsets to quads in joeq (which can be done using bcMap in jq_Method).

If you or someone else on the mailing list figures out how to do this, please let us know.  Several people ask me for this functionality from time to time.

-- Mayur

I wrote a simple analysis to try this out.  Run it as follows on an example:

ant -Dchord.work.dir=../test/bench/elevator -Dchord.run.analyses=localvar-java run

Then see the localNumbering map, stackNumbering map, and jq_LocalVarTableEntry array printed to log.txt.  The former two are in joeq.Compiler.Quad.RegisterFactory, and come from joeq's intermediate representation, while the latter is in joeq.Class.jq_Method, and comes from bytecode (assuming you compiled the .java files with debug info
to retain the local variable table attribute in the .class files).  I suspect there is a mapping between indices in the localNumbering map and jq_LocalVarTableEntry[] that you should be able to use.

Here is what is printed to log.txt when I run the above command:

local:  // localNumbering map
[java.lang.Object, 4]=R7
[long, 4]=R8
[java.lang.Object, 0]=R0
[long, 2]=R6
[java.lang.Object, 1]=R4

table: // jq_LocalVarTableEntry[]
entry: (startPC=0,length=71,nd=args [Ljava/lang/String;,index=0)
entry: (startPC=11,length=60,nd=building Lelevator/Elevator;,index=1)
entry: (startPC=22,length=49,nd=start J,index=2)
entry: (startPC=42,length=29,nd=end J,index=4)

Here is the quadcode:

 Control flow graph for main:([Ljava/lang/String;)V...@elevator.Elevator:
 BB0 (ENTRY)    (in: <none>, out: BB2)

 BB2    (in: BB0 (ENTRY), out: BB1 (EXIT))
 1   NEW                     T10,   elevator.Elevator
 2   MOVE_A                  T11,   T10
 3   NULL_CHECK              T-1,   R0
 4   BOUNDS_CHECK            R0,    IConst: 0,  T-1
 5   ALOAD_A                 T12,   R0, IConst: 0,  T-1
 7   NULL_CHECK              T-1,   T11
 6   INVOKESTATIC_V  <init>:(Ljava/lang/String;)V...@elevator.Elevator, (T11, T12)
 8   MOVE_A                  R4,    T10
 9   NEW                     T13,   java.util.Date
 10  MOVE_A                  T14,   T13
 12  NULL_CHECK              T-1,   T14
 11  INVOKESTATIC_V                 <init>:()V...@java.util.Date,  (T14)
 14  NULL_CHECK              T-1,   T13
 13  INVOKEVIRTUAL_L         T15,   getTime:()J...@java.util.Date, (T13)
 15  MOVE_L                  R6,    T15
 17  NULL_CHECK              T-1,   R4
 16  INVOKESTATIC_V                 begin:()V...@elevator.Elevator,    (R4)
 19  NULL_CHECK              T-1,   R4
 18  INVOKESTATIC_V  waitForLiftsToFinishOperation:()V...@elevator.Elevator,    (R4)
 20  NEW                     T16,   java.util.Date
 21  MOVE_A                  T17,   T16
 23  NULL_CHECK              T-1,   T17
 22  INVOKESTATIC_V                 <init>:()V...@java.util.Date,  (T17)
 25  NULL_CHECK              T-1,   T16
 24  INVOKEVIRTUAL_L         T18,   getTime:()J...@java.util.Date, (T16)
 26  MOVE_L                  R8,    T18
 27  GETSTATIC_A             T19,   .out
 28  NEW                     T20,   java.lang.StringBuilder
 29  MOVE_A                  T21,   T20
 31  NULL_CHECK              T-1,   T21
 30  INVOKESTATIC_V                 <init>:()V...@java.lang.StringBuilder, (T21)
 33  MOVE_A                  T22,   AConst: "Time taken in ms : "
 34  NULL_CHECK              T-1,   T20
 32  INVOKEVIRTUAL_A         T23, append:(Ljava/lang/String;)Ljava/lang/StringBuilder;@java.lang.StringBuilder, (T20, T22)
 35  SUB_L                   T9,    R8, R6
 37  NULL_CHECK              T-1,   T23
 36  INVOKEVIRTUAL_A         T24, append:(J)Ljava/lang/StringBuilder;@java.lang.StringBuilder,    (T23, T9)
 39  NULL_CHECK              T-1,   T24
 38  INVOKEVIRTUAL_A         T25, toString:()Ljava/lang/String;@java.lang.StringBuilder,  (T24)
 41  NULL_CHECK              T-1,   T19
 40  INVOKEVIRTUAL_V println:(Ljava/lang/String;)V...@java.io.PrintStream,  (T19, T25)
 42  RETURN_V

 BB1 (EXIT) (in: BB2, out: <none>)

 Exception handlers: []
 Register factory: Registers: 26

Look at the names/types of variable names in the java source code (test/bench/elevator/src/elevator/Elevator.java) and you will see the mapping:

[java.lang.Object, 0]=R0 corresponds to entry (startPC=0,length=71,nd=args [Ljava/lang/String;,index=0)

[java.lang.Object, 1]=R4 corresponds to entry (startPC=11,length=60,nd=building Lelevator/Elevator;,index=1)

[long, 4]=R8 corresponds to entry (startPC=42,length=29,nd=end J,index=4)

[long, 2]=R6 corresponds to entry (startPC=22,length=49,nd=start J,index=2)

In summary, match the integer-valued field in the domain of the localNumberingMap (values 0,1,4,2 above) to the 'index' field in jq_LocalVarTableEntry[].  I haven't tried this on other examples, but I suspect this is correct.  Let me know what you find.

Note: I tried this with SSA on (chord.ssa=true); this is default.  I haven't tried to see what happens if you switch SSA off (don't bother unless you have explicitly set chord.ssa=false). 

[Z]

Thanks for your reply.  I have a supplementary naive question here.  If I cannot even  figure out  the corresponding local variables of Vdom,  how can I use  jchord to understand the related results, such as the points-to information VH from cisa-0cfa-dlog?

If I understand well, VH.bdd can  be easily transformed into VH.tuples which are relationship between indexes of V.dom and indexes of H.Dom in term. For all local variables defined in the anaysed bytecode, there is an unique corresonding element in V.dom. From your last email, this correspondance is non-trivial. Thus, it seems non-trivail to illustrate the results of VH.bdd in bytecode level? 

I proabably misunderstand something here. Could you point it out? Thank for your ideas.

Zell.

[Ariel Rabkin]

I've never found VH all that useful on its own.

The things I usually care about are "where did the value that's set on
line XYZ come from?" And that's comparatively easy to do.
Every value in V is assigned a value in exactly one quad. Mapping from
quads to source lines is easy. So you can say, pretty easily, "the
variable that's given a value on line XYZ is pointing to the object
allocated on line ABC".

--Ari

> --
> You received this message because you are subscribed to the Google Groups
> "chord-discuss" group.
> To post to this group, send email to chord-...@googlegroups.com.
> To unsubscribe from this group, send email to
> chord-discus...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/chord-discuss?hl=en.

--

[Z]

Thanks for the reply.

If I understand well,  you mean
---- From an element of type chord.analyses.var.DomV
you can derive an element  joeq.compiler.Quad,
---- and from   joeq.compiler.Quad,  you can get its corresponding
line number (of type int) in the analysed bytecode.

Sorry but I am not that familiar with the API of jchord. Would you
like to indicate how do you achieve the 2 steps in Chord?

Thanks.

Zell.

[Ariel Rabkin]

On Fri, Dec 30, 2011 at 2:03 AM, Z <zel...@orange.fr> wrote:
> Thanks for the reply.
>
> If I understand well,  you mean
> ----  From an element of type  chord.analyses.var.DomV
> you can derive an element  joeq.compiler.Quad,

This part is a bit messy. What I had in mind was iterating over the
quads in a method and looking at the destination register.

> ---- and from   joeq.compiler.Quad,  you can get its corresponding
> line number (of type int) in the analysed bytecode.

You can just call Quad.getLineNumber();
Note that this is the line number in the original source code, NOT a
bytecode offset or anything like that.