Branch Tracing with Σοφία
Branch tracing in Sofya (Σοφία) generates a list of
covered edges in the CFG graph of
the Java subject being analyzed. The edges returned are not the edges reported in
the sofya.viewers.CFGViewer output however, but are instead an
internally represented edge-id specific
to the true/false paths (for -I if type branch coverage) that are
traversed.
The problem of which edge was traversed is further complicated by the way Sofya
subsumes edges that are not related to the instrumented branch type (e.g.
if branches.) Sofya will not enumerate intermediate edges
that are present between these branches but instead only reports the edges
that are directly associated with the instrumented branch type.
The best way to explain this difference in edge identifiers is by an example with a sample test program, Test.java. The source for Test.java is as follows:
public class Test {
public static void main(String[] args) {
Test test=new Test();
test.findsVertex("T");
}
public String findsVertex( String theName ) {
int i=0;
String theVertex;
String[] vertices=new String[]{"S","X","T","DD"};
// if we are dealing with the root
if ( theName==null )
return null;
for( i=0; i < vertices.length; i++ ) {
theVertex = ( String )vertices[i];
if ( theName.equals(theVertex) )
return theVertex;
}
return null;
}
}
Using the sofya.graphs.cfg.jCFG analysis tool on Test.java
produces the Sofya CFG file $HOME/.sofyadb/Test.java.cf.
For our example Test.java, this is the Test.java.cf
file that is created by the jCFG tool:
$ cat $HOME/.sofyadb/Test.java.cfg 0 Control Flow Information 0 File: Test.java Created: Fri May 13 07:41:50 CDT 2011 0 version 2.1.2-beta 0 1 "Test.public_String_findsVertex(String_arg1)" 11 11 8 8 4 Test#findsVertex#(Ljava/lang/String;)Ljava/lang/String; 3 1 2 1 1:16 3 2 4 2 2:1 T 3 3 3 2 3:1 F 3 4 10 3 3:1 3 5 5 4 2:1 3 6 9 5 5:1 T 3 7 6 5 6:1 F 3 8 8 6 4:1 T 3 9 7 6 7:1 F 3 10 10 7 7:1 3 11 5 8 4:1 3 12 10 9 5:1 0 end of method Test.public_String_findsVertex(String_arg1) 1 "Test.public_static_void_main(String[]_arg0)" 10 10 6 6 4 Test#main#([Ljava/lang/String;)V 3 1 2 1 1:16 3 2 3 2 2:8 <r> 3 3 4 3 2:8 3 4 5 4 4:8 <r> 3 5 6 5 4:8 3 6 7 6 4:8 3 7 9 2 3:8 <any> 3 8 10 4 5:8 <any> 0 end of method Test.public_static_void_main(String[]_arg0) 1 "Test.public_void_<init>()" 4 4 2 2 4 Test#<init>#()V 3 1 2 1 1:16 3 2 3 2 1:16 0 end of method Test.public_void_<init>()
Test.java.cf file
This raw CFG output can be viewed using the sofya.viewers.CFViewer
tool. The output from the CFVviewer for the example Test.java looks like this:
$ java sofya.viewers.CFViewer Test.java Control Flow Information for File Test.java Method: "Test.public_void_<init>()" CFG root node: 1 node label endline cf-successors (node-id(edge-id,"edge-label")) ---------------------------------------------------------------------------- 1 E 0 2(1,-) 2 K 4 3(2,-) 3 X 4 4 X 4 Method: "Test.public_String_findsVertex(String_arg1)" CFG root node: 1 node label endline cf-successors (node-id(edge-id,"edge-label")) ---------------------------------------------------------------------------- 1 E 0 2(1,-) 2 K 29 4(2,"T") 3(3,"F") 3 K 33 10(4,-) 4 K 35 5(5,-) 5 K 40 9(6,"T") 6(7,"F") 6 K 53 8(8,"T") 7(9,"F") 7 K 57 10(10,-) 8 K 61 5(11,-) 9 K 65 10(12,-) 10 X 65 11 X 65 Method: "Test.public_static_void_main(String[]_arg0)" CFG root node: 1 node label endline cf-successors (node-id(edge-id,"edge-label")) ---------------------------------------------------------------------------- 1 E 0 2(1,-) 2 F 4 3(2,"<r>") 9(7,"<any>") 3 T 4 4(3,-) 4 F 11 5(4,"<r>") 10(8,"<any>") 5 T 11 6(5,-) 6 K 15 7(6,-) 7 X 15 8 X 15 9 X 4 10 X 11
CFViewer for Test.java
Drawing the CFG from the CFViewer output for the findVertex()
method in Test.java would produce a CFG diagram like this:
The CFViewer output provides block and edge-ids that are correct
for the purposes of
analyzing the findVertex() method within the Test.java subject when basic
block type analysis is performed.
Branch tracing analysis in Sofya localizes the edges of concern to only those that are representative of the branch type being traced. These edge-ids frequently diverge from the edge-ids assigned in CFG analysis due to this focus on branch-type concerns and the subsumed edges in the Sofya branch analysis.
Instrumenting the Test subject for tracing if branches
using sofya.ed.cfInstrumentor and
executing the subject using sofya.ed.BranchTracer
produces an output file, instout.tr, which contains:
$ java sofya.viewers.TraceViewer ~/.sofyadb/instout.tr Trace Information for trace file /home/username/.sofyadb/instout.tr Trace Type: If Method: "Test.public_void_<init>()" Method: "Test.public_String_findsVertex(String_arg1)" Edges Hit: 2 4 6 7 Method: "Test.public_static_void_main(String[]_arg0)"
TraceViewer for Test.javaNotice that the edges hit are 2, 4, 6 and 7 within the method findVertex(). If we look at what edges these are in the CFViewer output of Listing 3 above, the edges traversed are not the ones we expected, e.g. edge 4 could not have been traversed since it leads directly from node 3 to node 10 which is an error exit node and we know (by code inspection) that the program terminated normally.
Instead of looking at the edges in the CFViewer output we need to
look at the branch-ids provided by the -ext option
of CFViewer. The following CFViewer output using
the -ext option demonstrates where these branch-ids are
presented in the report:
$ java sofya.viewers.CFViewer -ext Test.java
Control Flow Information for File Test.java
Method: "Test.public_void_<init>()"
CFG root node: 1
offsets successors
node label S E node-id(edge-id,"edge-label",[branch-ids])
--------------------------------------------------------------------------------
1 E 0 0 2(1,-,[1])
2 K 0 4 3(2,-,[1])
3 X 4 4
4 X 0 4
Method: "Test.public_String_findsVertex(String_theName)"
CFG root node: 1
offsets successors
node label S E node-id(edge-id,"edge-label",[branch-ids])
--------------------------------------------------------------------------------
1 E 0 0 2(1,-,[1])
2 K 0 29 4(2,"T",[2]) 3(3,"F",[3])
3 K 32 33 10(4,-,[3])
4 K 34 36 8(5,-,[2])
5 K 39 49 7(6,"T",[5]) 6(7,"F",[6])
6 K 52 53 10(8,-,[6])
7 K 54 54 8(9,-,[5])
8 K 57 61 5(10,"T",[4]) 9(11,"F",[7])
9 K 64 65 10(12,-,[7])
10 X 65 65
11 X 0 65
Method: "Test.public_static_void_main(String[]_args)"
CFG root node: 1
offsets successors
node label S E node-id(edge-id,"edge-label",[branch-ids])
--------------------------------------------------------------------------------
1 E 0 0 2(1,-,[1])
2 F 0 4 3(2,"<r>",[2]) 9(7,"<any>",[3])
3 T 4 4 4(3,-,[2])
4 F 7 11 5(4,"<r>",[4]) 10(8,"<any>",[5])
5 T 11 11 6(5,-,[4])
6 K 14 15 7(6,-,[4])
7 X 15 15
8 X 0 15
9 X 0 4
10 X 7 11
In the report, the branch-ids are shown within the successor node-ids
column of the report enclosed in square brackets. If we examine only the
findVertex() method, the edges hit during the BranchTracer
execution step (as reported by the TraceViewer in
Listing 4) now make sense
and can be traced through the expected execution path. The -ext output
may show these branch-ids (internal edge-ids) applied in multiple
places. Sofya simplifies the CFG graph to optimize the analysis by ignoring
branch-types that are not instrumented and intermediate code blocks without
branch statements.
These ignored branch-type statements and non-branching blocks are subsumed
into the graph so the analysis is focused on the instrumented branch-types only.
When diagrammed, the CFG that results from the subsumption of nodes and edges
by Sofya for if branch-types would look like this
(with the original nodes or subsumed nodes as comma separated lists and
using these internal edge-ids labels) and the associated findVertex() method
as it is represented in the Test.java.cf file and
the CFViewer -ext output for comparison:
1 "Test.public_String_findsVertex(String_arg1)" 11 11 8 8 4 Test#findsVertex#(Ljava/lang/String;)Ljava/lang/String; 3 1 2 1 1:16 3 2 4 2 2:1 T 3 3 3 2 3:1 F 3 4 10 3 3:1 3 5 5 4 2:1 3 6 9 5 5:1 T 3 7 6 5 6:1 F 3 8 8 6 4:1 T 3 9 7 6 7:1 F 3 10 10 7 7:1 3 11 5 8 4:1 3 12 10 9 5:1
Method: "Test.public_String_findsVertex(String_theName)"
CFG root node: 1
offsets successors
node label S E node-id(edge-id,"edge-label",[branch-ids])
----------------------------------------------------------------------
1 E 0 0 2(1,-,[1])
2 K 0 29 4(2,"T",[2]) 3(3,"F",[3])
3 K 32 33 10(4,-,[3])
4 K 34 36 8(5,-,[2])
5 K 39 49 7(6,"T",[5]) 6(7,"F",[6])
6 K 52 53 10(8,-,[6])
7 K 54 54 8(9,-,[5])
8 K 57 61 5(10,"T",[4]) 9(11,"F",[7])
9 K 64 65 10(12,-,[7])
10 X 65 65
11 X 0 65