How to use Daikon to infer invariant of java.util classes ?
Duy Le
Michael Ernst
that you ran? Otherwise we are likely to spend more time trying to guess
what you actually did than investigating the problem.
Thanks,
-Mike
> Subject: How to use Daikon to infer invariant of java.util classes ?
> From: Duy Le <lebuit...@gmail.com>
> To: daikon-...@googlegroups.com
> Date: Wed, 23 Jul 2014 23:42:06 -0700 (PDT)
> You received this message because you are subscribed to the Google
> Groups "Daikon discuss" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to daikon-discus...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Duy Le
Thank you for the reply :-)
I have tried to infer invariants of java.util classes on one of DaCapo benchmarks (xalan) as follows
java -cp "path/to/daikon.jar":dacapo-9.12-bach.jar daikon.Chicory --daikon --ppt-select-pattern="^java.util" Harness xalan -t 1
(Download dacapo-9.12-bach.jar from http://dacapobench.org/; "t -1" is used to limit number of thread to 1 when running the benchmark.)
The output in my PC (CentOS 64-bit) is:
#####################################################################################################
Executing target program: java -cp /usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar:/usr2/MiningAndDynamicAnalyisiWorkspace/InstrumentedJDK/dacapo-9.12-bach.jar -ea -Xmx1000m -javaagent:/usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar=--daikon --ppt-select-pattern=^java.util --dtrace-file=Harness.dtrace.gz Harness xalan -t 1
entered daikon.chicory.Runtime.setDtrace(./Harness.dtrace.gz, false)...
Using scaled threading model. 24 processors detected, 1 threads used to drive the workload, in a possible range of [1,100]
===== DaCapo 9.12 xalan starting =====
Normal completion.
===== DaCapo 9.12 xalan PASSED in 4433 msec =====
Chicory warning: No methods were instrumented.
Check the --ppt-select-pattern and --ppt-omit-pattern options
Executing daikon: java -Xmx1000m -cp /usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar:/usr2/MiningAndDynamicAnalyisiWorkspace/InstrumentedJDK/dacapo-9.12-bach.jar -ea daikon.Daikon ./Harness.dtrace.gz
Daikon version 5.1.2, released June 30, 2014; http://plse.cs.washington.edu/daikon.
Processing trace data; reading 1 dtrace file:
[8:09:24 PM]: FinisNhoe dp rroegardaimn gp o.i/nHta rdneecslsa.rdattriaocnes .gwez re f ou nd .
#####################################################################################################
It seems there are no invariant that are captured if I use --ppt-select-pattern="^java.util". Then, I re-run the command without --ppt-select-pattern option
java -cp "path/to/daikon.jar":dacapo-9.12-bach.jar daikon.Chicory --daikon Harness xalan -t 1
The output in my PC (CentOS 64-bit) is
#####################################################################################################
Executing target program: java -cp /usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar:/usr2/MiningAndDynamicAnalyisiWorkspace/InstrumentedJDK/dacapo-9.12-bach.jar -ea -Xmx1000m -javaagent:/usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar=--daikon --dtrace-file=Harness.dtrace.gz Harness xalan -t 1
entered daikon.chicory.Runtime.setDtrace(./Harness.dtrace.gz, false)...
Using scaled threading model. 24 processors detected, 1 threads used to drive the workload, in a possible range of [1,100]
java.lang.reflect.InvocationTargetException
java.lang.reflect.InvocationTargetException
at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:57)
at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
at java.lang.reflect.Constructor.newInstance(Constructor.java:525)
at org.dacapo.harness.TestHarness.runBenchmark(TestHarness.java:211)
at org.dacapo.harness.TestHarness.main(TestHarness.java:171)
at Harness.main(Harness.java:17)
Caused by: java.lang.ClassCircularityError: org/dacapo/xalan/XSLTBench
at java.lang.Class.forName0(Native Method)
at java.lang.Class.forName(Class.java:266)
at daikon.chicory.ClassInfo.initViaReflection(ClassInfo.java:74)
at daikon.chicory.Runtime.process_new_classes(Runtime.java:436)
at daikon.chicory.Runtime.enter(Runtime.java:246)
at org.dacapo.harness.DacapoClassLoader.loadClass(DacapoClassLoader.java:119)
at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
at java.lang.ClassLoader.defineClass1(Native Method)
at java.lang.ClassLoader.defineClass(ClassLoader.java:791)
at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
at java.net.URLClassLoader.defineClass(URLClassLoader.java:449)
at java.net.URLClassLoader.access$100(URLClassLoader.java:71)
at java.net.URLClassLoader$1.run(URLClassLoader.java:361)
at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
at org.dacapo.harness.DacapoClassLoader.loadClass(DacapoClassLoader.java:124)
at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
at java.lang.Class.forName0(Native Method)
at java.lang.Class.forName(Class.java:266)
at org.dacapo.harness.Xalan.<init>(Xalan.java:33)
... 7 more
Warning: Did not run Daikon because target exited with 255 status
#####################################################################################################
Thank you
Duy
Mark Roberts
From: daikon-...@googlegroups.com [mailto:daikon-...@googlegroups.com] On Behalf Of Duy Le
Sent: Saturday, July 26, 2014 5:20 AM
To: daikon-...@googlegroups.com
Cc: lebuit...@gmail.com; mer...@cs.washington.edu
Subject: Re: How to use Daikon to infer invariant of java.util classes ?Hi,
Thank you for reply :-)
I have tried to infer invariants of java.util classes on one of DaCapo benchmarks (xalan) as follows
java -cp "path/to/daikon.jar":dacapo-9.12-bach.jar daikon.Chicory --daikon --ppt-select-pattern="^java.util" Harness xalan -t 1
(Download dacapo-9.12-bach.jar from http://dacapobench.org/; "t -1" is used to limit number of threads to 1 when running the benchmark.)
The output in my PC is:
#####################################################################################################
Executing target program: java -cp /usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar:/usr2/MiningAndDynamicAnalyisiWorkspace/InstrumentedJDK/dacapo-9.12-bach.jar -ea -Xmx1000m -javaagent:/usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar=--daikon --ppt-select-pattern=^java.util --dtrace-file=Harness.dtrace.gz Harness xalan -t 1
entered daikon.chicory.Runtime.setDtrace(./Harness.dtrace.gz, false)...
Using scaled threading model. 24 processors detected, 1 threads used to drive the workload, in a possible range of [1,100]
===== DaCapo 9.12 xalan starting =====
Normal completion.
===== DaCapo 9.12 xalan PASSED in 4433 msec =====
Chicory warning: No methods were instrumented.
Check the --ppt-select-pattern and --ppt-omit-pattern options
Executing daikon: java -Xmx1000m -cp /usr2/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar:/usr2/MiningAndDynamicAnalyisiWorkspace/InstrumentedJDK/dacapo-9.12-bach.jar -ea daikon.Daikon ./Harness.dtrace.gz
Daikon version 5.1.2, released June 30, 2014; http://plse.cs.washington.edu/daikon.
Processing trace data; reading 1 dtrace file:
[8:09:24 PM]: FinisNhoe dp rroegardaimn gp o.i/nHta rdneecslsa.rdattriaocnes .gwez re f ou nd .
#####################################################################################################
It seems there are no invariant that are captured if I use --ppt-select-pattern="^java.util". Then, I re-run the command without --ppt-select-pattern option
java -cp "path/to/daikon.jar":dacapo-9.12-bach.jar daikon.Chicory --daikon Harness xalan -t 1
The output in my PC is
Michael Ernst
> expressions which are not quite the same as what you may be used to.
> Caret (^) means negation, not anchor to first character. Try removing
> the caret. I think that should do it.
In Java regular expressions, caret means the same as in Perl:
^ means negation within a character class, as in [^abc]
^ means beginning of line when outside a character class, as in Duy
Le's example
See the "Comparison to Perl 5" section of the Pattern documentation:
http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html#jcc
-Mike
Duy Le
Dear Mike and Mark,
Thank you for your reply :-)
I removed the caret, but the same issue still happened. I also tried to infer invariants of java.util.StringTokenizer class in a simple example (see attachment). In the example, StringTokenizer is used to parse a string. The following is its source code
package example;
import java.util.StringTokenizer;
public class ParseString {
final static private String SAMPLE = " Manchester United's new manager Louis van Gaal made a winning start as Wayne Rooney scored twice in a 7-0 defeat of LA Galaxy in front of a crowd of 86,432 at the Rose Bowl in California.";
public static void main(String[] args) {
foo(SAMPLE);
System.out.println("SUCCESSFUL!!!");
}
private static void foo(String st) {
StringTokenizer stn = new StringTokenizer(st);
while (stn.hasMoreTokens()) {
stn.nextToken();
}
}
}
At first, Daikon still cannot infer invariant with the following command
java -cp bin:$DAIKON7 daikon.Chicory --daikon --ppt-select-pattern="^java.util" example.ParseString
Later, I copy the source code of java.util.StringTokenizer into my project, and change its package to duy.java.util. Then, I modify my example’s source code as follows (highlighted in red color)
package example;
import duy.java.util.StringTokenizer;
public class ParseString {
final static private String SAMPLE = " Manchester United's new manager Louis van Gaal made a winning start as Wayne Rooney scored twice in a 7-0 defeat of LA Galaxy in front of a crowd of 86,432 at the Rose Bowl in California.";
public static void main(String[] args) {
foo(SAMPLE);
System.out.println("SUCCESSFUL!!!");
}
private static void foo(String st) {
StringTokenizer stn = new StringTokenizer(st);
while (stn.hasMoreTokens()) {
stn.nextToken();
}
}
}
Here, Daikon is successful to infer invariant of StringTokenizer class with the following command
java -cp bin:$DAIKON7 daikon.Chicory --daikon --ppt-select-pattern="^duy.java.util" example.ParseString
Then, I continue to change the package of StringTokenizer to java.StringTokenizer, and I receive the following exception
Executing target program: java -cp bin:/usr2/btdle/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar -ea -Xmx1000m -javaagent:/usr2/btdle/MiningAndDynamicAnalyisiWorkspace/SpecificationMining/baselines/ivo/daikon_java7/daikon.jar=--daikon --ppt-select-pattern=StringTokenizer --dtrace-file=ParseString.dtrace.gz example.ParseString
entered daikon.chicory.Runtime.setDtrace(./ParseString.dtrace.gz, false)...
Exception in thread "main" java.lang.SecurityException: Prohibited package name: java
at java.lang.ClassLoader.preDefineClass(ClassLoader.java:649)
at java.lang.ClassLoader.defineClass(ClassCLhoicadoreyr .wajranvinag::7 8No5 )me
t haodts wjearev ai.nssetcruurmietnyt.eSdec.u
rCehCelcaks stLohead -er-.pdpetf-isneelCeclta-spastt(eSrenc uraneCd la-s-spLpota-doemri.jta-vpaa:t1t4e2)rn
oatp tjiaovnas.net.URLCl
assLoader.defineClass(URLClassLoader.java:449)
at java.net.URLClassLoader.access$100(URLClassLoader.java:71)
at java.net.URLClassLoader$1.run(URLClassLoader.java:361)
at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
at example.ParseString.foo(ParseString.java:14)
at example.ParseString.main(ParseString.java:9)
Warning: Did not run Daikon because target exited with 1 status
At point, I think some security features of Java 7 have prevented Daikon from inferring invariants of system classes.
Thanks
Duy
Mark Roberts
As you have noted, there is not an easy way to generate invariants within the JDK; we assume that the libraries are correct and the user is only interested in his own code. Your technique of making a copy of the runtime code you are interested in should work as you wish. I am curious as to why you felt it was necessary to change the package name of your local copy to “java.StringTokenizer”? This will not work as you discovered. What are to trying to achieve that your previous example (with “duy.java….”) didn’t accomplish?
Mark Roberts
From: daikon-...@googlegroups.com [mailto:daikon-...@googlegroups.com] On Behalf Of Duy Le
Sent: Saturday, July 26, 2014 8:13 AM
To: daikon-...@googlegroups.com
Cc: mar...@cs.washington.edu; mer...@cs.washington.edu
Subject: Re: How to use Daikon to infer invariant of java.util classes ?
Dear Mike and Mark,
--