-
Notifications
You must be signed in to change notification settings - Fork 2
/
README
246 lines (191 loc) · 10.2 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
BUILDING, DISTRIBUTING AND RUNNING JAVARIFIER
=============================================
JAVARIFIER USER DOCUMENTATION
=============================
User documentation for Javarifier can be found at:
distribution/doc/javarifier.html
Or on the web at:
https://types.cs.washington.edu/javarifier
The rest of this file is intended for Javarifier developers: people who
wish to build Javarifier and/or modify its source code.
DEPENDENCIES
============
The Javarifier depends on several other packages. See the "Building from
source" section of the user documentation.
These dependencies are automatically taken care of by the build.xml script.
For convenience, we list here all the projects the Javarifier depends on in
order to facilitate integration with Eclipse. Note that if you add a
project dependency in Eclipse, you must add it to the build.xml script in
the "libpath" property.
Projects to build Javarifier:
- "annotation-scene-lib", the annotation scene library.
- "asmx", the extended version of ASM.
- The following Soot-required libraries, which are in javari/javarifier/lib
sootclasses-2.2.3.jar
jasminclasses-2.2.3.jar
polyglotclasses-1.3.2.jar
- "annotations-compiler", the extended annotations compiler.
- "javari-annotated-jdk", a set of Javari pre-annotated builtin JDK classes.
- "checkers", the Checker Framework (which contains the Javari qualifiers)
- "jdk1.6.0", a directory containing an installation of a 1.6.0 JDK, which
should most likely be the JSR 308 distribution, since it is fully
backwards compatible.
RUNNING
=======
Full documentation for running Javarifier is in javarifier.html
or on the web at:
https://types.cs.washington.edu/javarifier
The javarifier script at
javarifier/scripts/javarifier
uses the locally-compiled class files, if any; otherwise, it uses the
javarifier.jar file. Using the class files permits testing without making
the jar file, which takes much longer than compiling.
TEST SUITE
==========
In brief, run 'ant run-tests'. For details, see file tests/README.txt .
CREATING A DISTRIBUTION
=======================
To make a Javarifier distribution:
0. Run these instructions in an account that uses JDK 7, not JDK 8.
1. Run 'ant -e zipfile' to ensure that you can build javarifier.zip.
2. Manually verify that the release notes at the end of javarifier.html
are up-to-date.
3. Synchronize the version number in javarifier.html to the version number
in javarifier.Main.versionString (in src/javarifier/Main.java).
4. Run 'ant -e web'. This copies the distribution (javarifier.zip) and the
user documentation to https://types.cs.washington.edu/javarifier .
5. Test it. From a brand-new account, run the following:
## Install Checker Framework
# Cut and paste from
# https://types.cs.washington.edu/checker-framework/current/checkers-manual.html#javac-installation
# (but maybe use a different checkers.zip URL, such as one of:
# wget http://homes.cs.washington.edu/~mernst/jsr308test/checker-framework/current/checkers.zip
# cp -pf /home/cf/jsr308/checker-framework/tmp/1.1.1/checkers.zip .
# ).
# Sanity-check by following instructions at
# https://types.cs.washington.edu/checker-framework/current/checkers-manual.html#example-use
## Install Annotation File Utilities
cd ~/jsr308
# For unreleased version: cp -pf ~cf/jsr308/annotation-tools/annotation-file-utilities/annotation-tools.zip .
wget https://types.cs.washington.edu/annotation-file-utilities/annotation-tools.zip
rm -rf annotation-tools
unzip annotation-tools.zip
## Install Javarifier (these commands implement the instructions at
# https://types.cs.washington.edu/javari/javarifier/#installation):
cd ~/jsr308
# For unreleased version: cp -pf ~cf/jsr308/javarifier/javarifier.zip .
wget https://types.cs.washington.edu/javari/javarifier/javarifier.zip
rm -rf javarifier
unzip javarifier.zip
# Shouldn't have to add javarifier/scripts directory to my path.
cd javarifier
ant run-tests
6. Tag the release, for example:
git tag v0.1.4
JAVARIFIER DOCUMENTATION
========================
As of May 2008, the theory and algorithm behind the Javarifier is
Jaime Quinonez's thesis, located at:
javari/design/thesis-jaime/main.pdf
Or on the web at:
http://groups.csail.mit.edu/pag/pubs/Quinonez2008-abstract.html
A condensed version is located in the paper titled
"Inference of reference immutability", located at:
javari/design/javarifier/paper.pdf
Or on the web at:
http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html
User documentation for the Javarifier tool can be found at:
javarifier.html
Or on the web at:
https://types.cs.washington.edu/javarifier
Slides from talks on Javarifier can be found in the talks/ directory.
IMPLEMENTATION NOTES
====================
Official Java 6 class file specification:
http://jcp.org/aboutJava/communityprocess/pr/jsr202/index.html
The Javarifier is split into two main components: modified Soot classes to
contain extra information so that Soot is a sufficient class representation,
and Javari-specific classes that actually implement the reference immutability
inference algorithm. These components are in the src/soot and src/javarifier
directories, respectively. The implementation of the inference algorithm keeps
a scene of all the classes (represented as Soot classes) it is trying to infer
over, along with all the classes that it transitively depends on, including any
world classes (typically the annotated JDK).
Javarifier's changes to Soot
----------------------------
Javarifier uses a modified version of Soot 2.2.3
(http://www.sable.mcgill.ca/soot/) to translate class files to jimple,
which is a three-address language that is easy to analyze.
All of the modified classes are contained in javari/javarifier/src/soot
To update to a new version of Soot, download the new source code, make a diff
of the latest updates in javarifier/src/soot to the first version, then
apply these as a patch to the source of the new version of Soot.
The Javarifier source only includes the files that were actually modified;
it is intended that users will place the modified soot files earlier in the
class path than the original Soot.
There are two major changes to Soot:
1) Adding fields to AST nodes to contain information Javarifier needed
such as "Javari" type signatures, which include a full generic type
signature and mutability information. See SootMethod, JimpleLocal,
etc.
Even if a later version of Soot adds generic type signatures, mutability
information would still need to be stored.
Alternatives Matthew Tschantz considered but rejected include:
1) Subclassing Soot classes for which I needed to add fields, such
as soot.Local. This would require changing all "new" statements or
rewriting Soot to use factory methods.
2) Using Maps that map from soot.Local's to the new information. This
makes the code annoying to read and I don't trust all of Soot's
hashCode and equal methods.
2) Changes to the way Soot resolves and load classes. Soot seems
overly aggressive with loading classes. Additionally, I ensured that
"stub" classes wouldn't be loaded. See FastHierarchy, PackManager,
SootResolver, and SourceLocator.
Two smaller changes are:
3) Changing the local splitting convention. See toolkits/scalar/LocalSplitter.
4) Adding a lot of back pointers, to make debugging easier. For example,
so I could print the name of the method a local variable is from.
Problems with Soot that required the above changes
--------------------------------------------------
First, Soot does not (currently) operate over Java 1.5 types. Soot
fails completely on Java 1.5 source, but will work somewhat on Java
1.5 classfiles. When operating on classfiles, Soot will store Java
1.5 type signatures attributes on classes, methods, and fields as
"tags" on the appropriate SootClass, SootMethod, or SootField (see
soot.tagkit.AbstractHost). This tag, is simply a wrapper for a String
holding the JVML class signature, method signature, or type. Soot does
not process LocalVariableTypeTables, and, thus, does not have have any
Java 1.5 type signatures for locals.
Since Strings are difficult to work with, we have created the
ClassSig, MethodSig, and JrType classes. SootClass, SootMethod,
SootField, and Local are all given new fields that reference these
data structures. These data structures are added to the Soot
structures by JrTyper.
To obtain Java 1.5 type signatures for locals JrTyper uses ASM.
Second, Soot normally performs a number of optimizations that can harm
our type analysis. For example, Soot normally executes local
splitting, which is not safe, because that would allow a split local
to possibly have two different types. common.sh contains a series of
options that seem to work.
Third, Soot's whole program analysis mode can be difficult to work
with. When operating in whole program mode, Soot will pull in the
entire JDK because Object references String which references ... so on,
until every class is included in the analysis. To prevent this, we
use stub classes (a class file with mutability information already
included). Soot's class loading code (soot.SootResolver) had to be
modified to not pull in classes only referenced by a class which is
stubbed. Thus, we can stub Object, and an analysis will not pull in
every JDK class just because it references Object. Ultimately, we
plan to provide stub classes for the entire JDK.
END
===
These are words the spell-checker should accept.
LocalWords: Javarifier ASM cd javarifier chmod classfiles classfile java asmx
LocalWords: packagename classname javarify JARs ASM's jdk xml hg jsr libpath
LocalWords: builtin javari builtins nonnull FIXME classpaths classpath JDK's
LocalWords: rt tex com bcel javap util src jimple SootMethod txt pdf pdflatex
LocalWords: JimpleLocal Local's FastHierarchy PackManager SootResolver JVML
LocalWords: SourceLocator SootClass SootField acroread ClassSig MethodSig
LocalWords: LocalVariableTypeTables JrType JrTyper langtools zipfile html
LocalWords: myPackage MyClass Quinonez's Javarifier's diff Tschantz hashCode
LocalWords: Subclassing