Static Specification Mining Using Automata-Based Abstractions* - Mining Software Specifications: Methodologies and Applications - page 186

6.7 Experimental Results
We have implemented a prototype of our analysis based on the WALA
analysis framework [28] and the typestate analysis framework of [11]. Our
analysis builds on a general Reps-Horwitz-Sagiv (RHS) IFDS tabulation solver
implementation [26]. We extended the RHS solver to support dynamic changes
and merges in the set of dataflow facts. The pointer analysis adds one level
of call-string context to calls to various library factory methods, arraycopy ,
and clone statements, which tend to badly pollute pointer flow precision if
handled without context-sensitivity. The system uses a substantial library of
models of native code behavior for the standard libraries.

6.7.1 Benchmarks
Table 6.2 lists the benchmarks used in this study. Each of the benchmarks
bobalice , js-chap13 , and j2ns is a set of examples taken from a book on Java se-
curity [25]. flickrapi is an open source program providing a wrapper over flickr
APIs, as well as some utilities using it. ganymed is a library implementing the
SSH-2 protocol in pure Java; the library comes with examples and utility pro-
grams that use it. javacup and jlex are a parser generator and lexical analyzer,
respectively, for Java. jbidwatcher is an online auction tool. jfreechart is a Java
chart library. tinysql is a lightweight Java SQL engine. tvla is a static analysis
framework.
The table reports size characteristics restricted to methods discovered by
on-the-fly call-graph construction. The call graph includes methods from both
the application and the libraries; for many programs the size of the program

TABLE 6.2: Benchmarks

Num Benchmark Classes Methods Bytecodes Contexts Clients

1 aamfetch 635 2544 246284 3316 2

2 bobalice 259 1318 71048 1917 2

3 crypty 450 2138 127130 2794 1

4 flickrapi 123 423 26607 527 2

5 ganymed 121 649 49232 919 4

6 j2ns 944 4817 399402 6570 5

7 javacup 373 2000 122592 2981 2

8 javasign 111 473 45670 740 11

9 jbidwatcher 64 525 18717 269 9

10 jfreechart 654 2644 250718 3457 18

11 jlex 89 317 25261 382 2

12 jpat-p 374 2043 141649 5570 1

13 JPDStore 109 359 23040 418 2

14 js-chap13 661 2795 259273 3770 6

15 privatray 175 665 56543 876 1

16 tinysql 701 3019 277881 3980 2

17 tvla 643 2572 249243 3355 3