-
Notifications
You must be signed in to change notification settings - Fork 2
/
javarifier.html
906 lines (787 loc) · 37 KB
/
javarifier.html
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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8"/>
<title>Javarifier</title>
</head>
<body>
<h1>Javarifier: Inference of reference immutability for Javari</h1>
<p>Contents:</p>
<!-- start toc. do not edit; run html-update-toc instead -->
<ul>
<li><a href="#motivation">Motivation: Inferring reference immutability in Java programs</a></li>
<li><a href="#javarifier-description">Javarifier</a>
<ul>
<li><a href="#stubs-description">Inference using existing Javari classes and stubs</a></li>
<li><a href="#javari-differences">Differences from previous versions of Javari</a></li>
</ul></li>
<li><a href="#installation">Installation</a></li>
<li><a href="#using">Using Javarifier</a>
<ul>
<li><a href="#using-classpath">Specifying a classpath</a></li>
<li><a href="#using-output">Outputting to a file</a></li>
<li><a href="#using-world">Specifying library jarfiles</a></li>
<li><a href="#using-stubs">Using stub classes</a></li>
<li><a href="#using-heuristics">Applying heuristics to exclude fields from the abstract state</a></li>
<li><a href="#using-debug">Understanding and debugging Javarifier output</a>
<ul>
<li><a href="#print-cause-tree">Printing the cause tree</a></li>
<li><a href="#print-constraints">Printing constraints</a></li>
<li><a href="#print-constraint-variable">Printing a constraint variable</a></li>
</ul></li>
<li><a href="#test-suite">Running the Javarifier test suite</a></li>
<li><a href="#command-line-opts">Command-line options</a></li>
</ul></li>
<li><a href="#building-from-source">Building from source</a>
<ul>
<li><a href="#compiling-with-eclipse">Compiling with Eclipse</a></li>
</ul></li>
<li><a href="#feedback">Feedback</a>
<ul>
<li><a href="#release-notes">Release notes</a></li>
</ul></li>
</ul>
<!-- end toc -->
<h2 id="motivation">Motivation: Inferring reference immutability in Java programs</h2>
<p>
Javarifier divides the variables in a program into two groups: the
variables the program mutates, and the variables that are never mutated.
In other words, Javarifier infers the immutability of every reference in a
Java program. Javarifier uses
<a href="https://types.cs.washington.edu/javari/">Javari</a>'s definition of
immutability. Thus, Javarifier converts Java programs and libraries to
Javari.
</p>
<p>
Annotating <em>programs</em> aids developers in reasoning about the code
and modifying it without introducing subtle mutation errors. Annotating
<em>libraries</em> is important because Javari programs use libraries
without Javari annotations often do not type-check. Manually determining
the mutability for each (public) parameter and return type is tedious and
error-prone. Javarifier automatically performs this analysis.
</p>
<p>
Javarifier can produce a textual output file, or can annotate
<code>.java</code> files with backward-compatible comments, or can annotate
<code>.class</code> files with backward-compatible attributes. The
algorithm for inferring Javari reference immutability is explained in the
paper
<a href="http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html">"Inference
of reference immutability"</a>, which appeared at ECOOP 2008.
</p>
<h2 id="javarifier-description">Javarifier</h2>
<p>
Javarifier's input is Java <code>.class</code> files.
Javarifier's output is an
<a href="https://checkerframework.org/annotation-file-utilities/">annotation
file</a>, a textual file format for describing annotations
of Java programs; the input class files are not
modified. The annotation file can be used by a tool such as the
<a href="https://checkerframework.org/annotation-file-utilities/">annotation
file utilities</a>, which inserts the annotations into either the
<code>.class</code> files or the corresponding <code>.java</code>
files. If Javari annotations are inserted into the source code, they can
be checked by the
<a href="https://checkerframework.org/">Javari type
checker</a>.
</p>
<h3 id="stubs-description">Inference using existing Javari classes and stubs</h3>
<p>
Javarifier respects all existing Javari annotations in the program classes
it analyzes. If any type is already annotated as <code>@ReadOnly</code>,
Javarifier uses this annotation to determine the mutability of other types
and does not change the existing <code>@ReadOnly</code> annotation. This
mechanism is how Javarifier infers annotations on a program that uses libraries
that have already been annotated using stub classes.
</p>
<h3 id="javari-differences">Differences from previous versions of Javari</h3>
<p>
In earlier versions of Javari, methods must be invariant in the mutability
of their parameters and return types. The newer definition of Javari used
by both Javarifier and the
<a href="https://checkerframework.org/">Javari type checker</a>
permits covariant subtyping on parameters and contra-variant subtyping on
return types.
</p>
<h2 id="installation">Installation</h2>
<p> The current distribution is <b>Javarifier version 0.1.4</b>,
released September 18, 2010. </p>
<p>
The following instructions assume either a Unix-like (e.g., Linux, Mac) or
Windows command-line environment.
</p>
<ol>
<li value="0">
Install the
<a href="https://checkerframework.org/manual/#installation">Checker
Framework</a> and the
<a href="https://checkerframework.org/annotation-file-utilities/#installation">Annotation
File Utilities</a>, in sibling directories; for example,
<tt>~/jsr308/checker-framework/</tt> and <tt>~/jsr308/annotation-tools/</tt>.
<br />
Neither is strictly necessary to run Javarifier, but you almost certainly
want both of them.
Javarifier uses the Checker Framework's annotated JDK, when available.
You will use the Annotation File Utilities to insert Javarifier's output
into <tt>.java</tt> or <tt>.class</tt> files, and the Checker Framework
to type-check the Javari annotations in <tt>.java</tt> files.
</li>
<li>
Download
<a href="https://types.cs.washington.edu/javari/javarifier/javarifier.zip">javarifier.zip</a>.
</li>
<li>
Unpack the distribution zipfile, as a sibling of the Checker Framework
(for example, in <tt>~/jsr308/javarifier/</tt>)
by running:
<pre> unzip javarifier.zip</pre>
</li>
<li>
Add the <tt>javarifier/scripts</tt> directory to your path.
<ul>
<li>
For <b>Unix</b>, add the directory to your PATH environment
variable. If you use the sh or bash shell, add to <tt>~/.bashrc</tt> or
<tt>~/.bash_profile</tt>:
<pre>export PATH=${PATH}:${HOME}/jsr308/javarifier/scripts/</pre>
<!-- Omitted: few people use this shell, and I want to keep the
instructions short.
For csh/tcsh, add to ~/.tcshrc or ~/.cshrc or ~/.login:
<pre>setenv PATH ${PATH}:${HOME}/jsr308/javarifier/scripts/</pre>
-->
</li>
<li>
For <b>Windows</b>, add the directory to your
<code>PATH</code> system
variable by going to
<pre> Control Panel → System → Advanced → Environment Variables </pre>
<p>
From there, find the <code> PATH </code> variable under “System variables”
and append to it the <code>javarifier</code> directory.
</p>
</li>
</ul>
</li>
</ol>
<h2 id="using">Using Javarifier</h2> <p> The following instructions
are for running <code>javarifier</code> on a Unix-like machine. The
instructions are the same for Windows, except the tool is
<code>javarifier.bat</code>, and you must use Windows path names
instead of Unix path names. </p>
<p> The <code>javarifier</code> tool takes as arguments
any number of fully-qualified names of the classes to analyze.
For example: </p>
<pre>javarifier myPackage.myClassOne myPackage.myClassTwo</pre>
To analyze all classes in a package <code>myPackage</code>, run the
following in its parent directory:
<pre>javarifier `find myPackage -type f -name '*.java' | perl -p -e 's/\.java//g; s/\//./g'`</pre>
<h3 id="using-classpath"> Specifying a classpath</h3>
<p>
All of the classes being analyzed must be on the path specified by the
<a href="#using-classpath">--programCPEntries</a> option, which defaults to
$CLASSPATH.
</p>
<p>
If you get an error "couldn't find class: ... (is your soot-class-path set
properly?)", then the problem may be that you did not set
<tt>--programCPEntries</tt>.
</p>
<!--
This isn't necessary any longer, I think:
<p>
(Just using the default <code>$CLASSPATH</code> may not work, because the
JVM may
also load classes from other locations, such as the boot class path.
An example is the classes in <code>jdk/jre/lib/jce.jar</code>.
Therefore, you may need to add such jar files to CLASSPATH, or explicitly
mention them on the javarifier command line
via the <a href="#using-world"><code>-world</code> option</a>.)
</p>
-->
<pre>
javarifier myPackage.myClassTwo --programCPEntries /path/to/classes1:/path/to/classes2
</pre>
<p>
These two examples are identical:
</p>
<pre>
javarifier myPackage.myClassTwo
javarifier myPackage.myClassTwo --programCPEntries $CLASSPATH
</pre>
<h3 id="using-output">Outputting to a file</h3>
<p>
By default, all output, including the results, is printed to standard
out. To output the results to an <a href="https://checkerframework.org/annotation-file-utilities/">annotation file</a>, use the
<code>--output</code> option, followed by the name of the output file.
Note that Javarifier outputs the results for all classes into a single
file. For example:
</p>
<pre>javarifier myPackage.myClassOne myPackage.myClassTwo --output myPackage.jaif</pre>
<h3 id="using-world">Specifying library jarfiles</h3>
<p>
The program on which you are running Javarifier may depend on
the JDK and other libraries.
By default, Javarifier assumes that those libraries are on your
CLASSPATH. For example, it assumes <code>rt.jar</code> is in your
CLASSPATH. If this is not the case, or if you wish to reference a
different JDK, you may use the <code>--world</code> option, followed by
the classpath of your JDK jarfiles. For example:
</p>
<pre>javarifier myPackage.myClassOne myPackage.myClassTwo --world /jdk1.7.0/jre/lib/rt.jar:/jdk1.7.0/jre/lib/resources.jar:/jdk1.7.0/jre/lib/all-other-jars.jar</pre>
<h3 id="using-stubs">Using stub classes</h3>
<p>A stub class gives Javari types for an external library.
The <a href="https://checkerframework.org/">Checker
Framework</a> comes with annotated versions of part of the JDK,
which Javarifier uses by default.
</p>
<p>
To inform Javari of additional stub classes (or
fully-annotated Javari classes), use the <code>--stubs</code> argument,
followed by a classpath to containing stub classes. All classes
found in that classpath will be treated as stub classes. For
example:
</p>
<pre><code> javarifier myPackage.myClassOne myPackage.myClassTwo --stubs /path/to/stubs/dir:/path/to/stubs.jar</code></pre>
<p>
If no stub class is available for a particular
class, then Javarifier assumes that every reference in that class has
<code>@Mutable</code> type.
The <code>--printStubs</code> flag causes Javarifier not to perform
inference, but only to output a list of classes for which stubs are needed.
</p>
<p>
If you get the error "Missing stub for class ...",
then your stub library is missing the given class, or you have not
specified the stub library location properly. (One reason this can happen
is that you are using JDK 7. You may need to add, to the Checker
Framework's annotated JDK, stubs for classes that are new in JDK 7.)
</p>
<p>
If you create stub versions of additional classes (whether in the JDK or
other libraries), or if you improve existing libraries by adding
annotations to them, please email them to
<a href="mailto:javarifier-dev@googlegroups.com">javarifier-dev@googlegroups.com</a> so that we
can include them in future releases.
</p>
<h3 id="using-heuristics">Applying heuristics to exclude fields from the abstract state</h3>
<p>
Javarifier implements several heuristics for inferring which fields should
be excluded from the abstract state of an object. These heuristics may
infer the <code>@Assignable</code>
and <code>@Mutable</code> field annotations, and these annotations
may affect the end results of Javarifier. To apply these heuristics, use
the <code>--applyHeuristics</code> flag, as follows:
</p>
<pre>javarifier myPackage.myClass --applyHeuristics</pre>
<p>
These heuristics only apply to private, non-static, non-final fields.
The following is a list of all heuristics currently implemented.
</p>
<ul>
<li> A field that is only written to in the constructor or in the <code>equals()</code> and <code>hashCode()</code> methods is inferred to be <code>@Assignable</code>.
</li>
<li> If a class implements the <code>equals()</code> method, any field that
is not read in the <code>equals()</code> method is inferred to be <code>@Assignable</code>.
</li>
<li> A field that is written to in a method that overrides either
<code>Iterator.next()</code> or <code>Enumeration.nextElement()</code>
is inferred to be <code>@Assignable</code>.
</li>
</ul>
<h3 id="using-debug">Understanding and debugging Javarifier output</h3>
<p>
Javarifier may infer some references to be <code>@Mutable</code> that you
believe should be <code>@ReadOnly</code> (or vice versa). This usually indicates a problem
with your code such as a bug, a missing <code>@Assignable</code> keyword,
or simply that you have misunderstood what your code does. Sometimes, it
can indicate a bug in Javarifier.
</p>
<p>
For more details about the constraints beyond this section of the manual,
see the paper
<a href="http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html">"Inference
of reference immutability"</a>. Contact us if you need more help
understanding the constraints.
</p>
<h4 id="print-cause-tree">Printing the cause tree</h4>
<p>
To understand why Javarifier inferred a particular type qualifier, you can
enumerate the causes for each qualifier. Use the <code>--dumpCauses</code> flag, as in:
</p>
<pre>javarifier myPackage.myClass --dumpCauses</pre>
<p>
For each annotation, this outputs the shortest-length inference tree. Each
node of the tree is a <em>cause</em>, which explains why a particular
variable is not readonly.
That cause may refer to other variables, and the rest of the tree explains
why those variables are not readonly.
The tree is at most binary — each node has 0, 1, or 2 children.
Most nodes have 1 child, making most of the tree a chain.
</p>
<p>
A <em>cause</em> consists of three pieces of information, each printed on its own line:
</p>
<ul>
<li>Constraint variable (not a program variable!) of a variable that is
not readonly. (<b>TODO:</b> check that.)
See below for an <a href="#print-constraint-variable">explanation of its formatting</a>.
</li>
<li>Source code information: location and pseudocode.
<ul>
<li>
The location takes one of three forms:
<ul>
<li>“<b>ClassName</b>:<b>LineNumber</b>:”, if debug
information (-g compiler flag) is available
</li>
<li>“<b>ClassName</b>:: <b>methodName</b>”, if debug information
is not available
</li>
<li>empty, if Javarifier has no source information for the constraint
(such as if the constraint came from a stub file, or subtyping
constraints in overriding relationships)
</li>
</ul>
</li>
<li>
The pseudocode represents an assignment of the form "$e1 = $e2;",
"name.field = $e2", "name[...] = $e3", etc., where $e<b>n</b> indicates a
variable introduced by Javarifier.
</li>
</ul>
</li>
<li>An explanation. This is sometimes the constraint that Javarifier generates
from the source code construct, and other times is an English description.
A common explanation to appear at the end of a cause chain is
"Stub", which indicates that the variable is known via a stub declaration.
</li>
</ul>
<p>
When the explanation mentions one other variable (e.g., when the constraint
leading to mutability of <tt>a</tt> is "b → a"), the cause for the other
variable is printed directly below, at the same indentation level.
When the explanation mentions two other variables
(e.g., when the constraint
leading to mutability of <tt>a</tt> is "c → b → a"), the cause for the
first variable is printed indented, after the word "GUARD", and the cause
for the second
variable is printed directly below, without any extra indentation.
</p>
<p>
Here is an abstract example of the output:
</p>
<pre>
<Var1>
<b>ClassName</b>:53: <b>Stmt1</b>
Var1 <: Var2
<Var2>
<b>ClassName</b>:: <b>MemberName</b> <b>Stmt2</b>
Why Var3 and Var4 implies Var2
GUARD:
<Var3>
<b>ClassName</b>:: <b>MemberName</b> <b>Stmt3</b>
Why Var3 is directly apparent
<Var4>
<b>ClassName</b>:: <b>MemberName</b>
Stub
</pre>
<h4 id="print-constraints">Printing constraints</h4>
<p>
If the cause tree is not sufficient to understand the output, then you can also
examine the raw constraints generated by Javarifier during its inference
process. Use the <code>--dumpConstraints</code> flag, as in:
</p>
<pre>javarifier myPackage.myClass --dumpConstraints</pre>
<p>
The Javarifier constraints are of three types:
</p>
<ul>
<li>
A line of the form "U: c1" indicates that the type in c1 must be mutable.
See below for an
<a href="#print-constraint-variable">explanation of constraint variable
formatting</a>.
An example of a constraint is
<pre><code> U: <Graph.createGraph.this: UNKNOWN Graph[] MUTABLE></code></pre>
This constraint indicates that the receiver (<code>this</code>) of method
<code>Graph.createGraph</code> must be mutable.
</li>
<li>A line of the form "G: c1 -> c2" indicates that if the type in c1 is
mutable, then the type in c2 must be mutable.
</li>
<li>A line of the form "GG: c1 => c2 -> c3" indicates that if the types
in both c1 and c2 are mutable, then the type in c3 must be mutable.
</li>
</ul>
<p>
You may find it helpful to cross-reference between Javarifier constraints
and the Java source code of the classes being analyzed (from the
constraints were generated).
</p>
<h4 id="print-constraint-variable">Printing a constraint variable</h4>
<p>
An example of a constraint variable is:
</p>
<pre><code> <Graph.createGraph.this: UNKNOWN Graph[] MUTABLE></code></pre>
<p>
It contains the following parts:
</p>
<ul>
<li>
The variable name from tho source code.
<ul>
<li>
For method receivers, the index -1 is used to refer to the receiver, as
in the following constraint:
<pre> U: <<Hashtable: int hashMap(java.lang.Object)>.-1: UNKNOWN Hashtable[] ctx:m></pre>
</li>
<li>Local variables are named if the classfile has the LocalVariableTypeTable
attribute. Otherwise, they are named by their index (e.g., "e0"), as are temporary
variables, as in:
<pre> U: <Graph.createGraph.$e0: UNKNOWN Vertex[] ctx:r></pre>
</li>
</ul>
</li>
<li>
The type, including mutability. In this case,
the string "UNKNOWN Graph[]" indicates that the mutability of the Graph
has not yet been determined. (Due to the unguarded constraint, it will be
mutable in the end.)
</li>
<li>
ctx:m represents the romaybe-context that the constraint is referring
to; this
is used for inferring romaybe (see the paper
<a href="http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html">"Inference
of reference immutability"</a> for details).
Often the constraints are the same across contexts, so
you might have the following two constraints:
<pre>
U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:m>
U: <HashEntry.setNext.this: UNKNOWN HashEntry[] ctx:r>
</pre>
</li>
</ul>
<h3 id="test-suite"> Running the Javarifier test suite </h3>
<p>
To run the test suite, do <em>any one</em> of the following commands:
</p>
<pre> ant run-tests
make -C tests
cd tests; make</pre>
<h3 id="command-line-opts">Command-line options</h3>
<!-- start options doc (DO NOT EDIT BY HAND) -->
<ul>
<li>General Options
<ul>
<li><b>-h</b> <b>-help</b> <b>--help=</b><i>boolean</i>. Print the short usage message. This does not include verbosity or
debugging options. [default false]</li>
<li><b>-H</b> <b>--allHelp=</b><i>boolean</i>. Print the extended usage message.
This includes verbosity and debugging options but not internal options. [default false]</li>
<li><b>-v</b> <b>-version</b> <b>--version=</b><i>boolean</i>. Print the current Javarifier version. [default false]</li>
</ul>
</li>
<li>Execution Options
<ul>
<li><b>-Q</b> <b>--reallyQuiet=</b><i>boolean</i>. Be quiet, do not print much information. [default false]</li>
<li><b>--applyHeuristics=</b><i>boolean</i>. Use heuristics to set fields that should be excluded from the abstract
state of the object to be assignable. See: <code>javarifier.HeuristicsVisitor</code>. [default false]</li>
<li><b>--openWorld=</b><i>boolean</i>. Forces all public method return types to have mutable (or polyread) types
and all public fields to have this-mutable types. See: <code>javarifier.OpenWorld</code>. [default false]</li>
</ul>
</li>
<li>Input Options
<ul>
<li><b>--programCPEntries=</b><i>string</i>. Specify a colon-delimited classpath other than <b>$CLASSPATH</b> for
Javarifier to use to look up classes being analyzed.</li>
<li><b>--stubs</b> <b>--stubCPEntries=</b><i>string</i>. Specify a colon-delimited classpath to look for stub classes. All
classes found in this path will be treated as stub classes.</li>
<li><b>--world</b> <b>--worldCPEntries=</b><i>string</i>. By default, Javarifier assumes that the JDK classes required by the
program classes on which you are running Javarifier are in your
<b>$CLASSPATH</b>. If this is not the case, or if you wish to reference
a different JDK, you may use this followed by the colon-delimited
classpath of your JDK jarfiles.</li>
<li><b>--useWorldAsStubs=</b><i>boolean</i>. If false (the default), then missing stubs cause Javarifier to halt.
If true, then Javarifier uses world classes as stubs, after both the
default stub entries and the stub entries. [default false]</li>
<li><b>--extraAnnotationInputFile=</b><i>filename</i>. If specified, annotations will be loaded from this annotation file as well as
the class files for all classes in the Soot scene.</li>
</ul>
</li>
<li>Output Options
<ul>
<li><b>--output</b> <b>--outputFile=</b><i>filename</i>. By default, all output, including the results, is printed to standard
out. Use this option to output the results to an annotation file. Note
that Javarifier outputs the results for all classes into a single file.</li>
<li><b>--outputFormat=</b><i>format</i>. Specify the output annotation format.
See <code>javarifier.OutputFormat</code> for a description of these formats. [default JAIF]<ul><li><b>SCENE_PRINTER</b> The traditional format showing full JrTypes.</li><li><b>JAIF</b> An annotation file showing types resugared as annotations.</li><li><b>TWO_FILES</b> Two files, one listing readonly method parameters and receivers and
another listing mutable ones. --outputFormat is ignored and both
output files are created in the current directory.</li><li><b>SHAY</b></li></ul></li>
<li><b>--outputFilterLocals=</b><i>boolean</i>. Tells <code>ScenePrinter</code> to omit a bunch of uninteresting local
variables from the output. These are generally the ones that cannot be
annotated in source code, so this option is good for comparing
Javarifier results with manual annotations. [default false]</li>
<li><b>--outputLimitKind=</b><i>construct</i>. Tells <code>ScenePrinter</code> to output "omitted" instead of the type for
elements not of the given construct. The construct can be "field",
"local", "parameter", "receiver", or "return". Useful to study the
types assigned to elements of each kind separately.</li>
<li><b>--outputSortMembers=</b><i>boolean</i>. Tells <code>ScenePrinter</code> to output fields and methods sorted by name
instead of by order of appearance in the class file. If several methods
have the same name, they are outputted in the order they appear in the
class file. [default false]</li>
<li><b>--outputMainClassFirst=</b><i>boolean</i>. Tells <code>ScenePrinter</code> to output all the classes mentioned on the
command line (in the order of first mention on the command line) before
all the other classes. [default false]</li>
<li><b>--skipEmpty=</b><i>boolean</i>. The skipEmpty flag indicates that annotations should not be outputted
for empty code. That is, there should be no annotations for interfaces
and abstract methods. [default false]</li>
<li><b>--includeImmutableClasses=</b><i>boolean</i>. The includeImmutableClasses flag indicates that @ReadOnly annotations
should be output even for references that are of some type that is known
to be @Unmodifiable, such as java.lang.String. [default false]</li>
</ul>
</li>
<li>Utility Options (no inference)
<ul>
<li><b>--justPassThrough=</b><i>boolean</i>. Do not perform inference. Just read annotations (treating even program
classes as fully annotated), expand defaults and @Unmodifiable, and write
the results back out. Use this mode to convert manual annotations to a
form in which they can be compared to Javarifier annotations. [default false]</li>
<li><b>--printStubs=</b><i>boolean</i>. Do not perform inference. Just output a list of classes for which stubs
are needed to perform inference. [default false]</li>
<li><b>--printMissingStubs=</b><i>boolean</i>. Do not perform inference. Just output a list of classes which are needed
to perform inference but missing. [default false]</li>
</ul>
</li>
<li>Verbosity Options
<ul>
<li><b>--dumpCauses=</b><i>boolean</i>. Enumerates the causes for each type
qualifier Javarifier infers. For each annotation this outputs the
shortest-length inference chain. See the manual section on
"Printing the cause tree". [default false]</li>
<li><b>--dumpConstraints=</b><i>boolean</i>. Dump the raw constraints generated by Javarifier during its inference
process. See the section on <code>-dumpConstraints</code> in the manual
for information. [default false]</li>
<li><b>--dumpResults=</b><i>boolean</i>. Dump results. [default false]</li>
<li><b>--dumpGeneratorConstraints=</b><i>boolean</i>. Dump generator constraints. See: <code>javarifier.ConstraintGenerator</code>. [default false]</li>
<li><b>--dumpBoundGuards=</b><i>boolean</i>. Dump bound guards. See: <code>javarifier.BoundGuarder</code>. [default false]</li>
<li><b>--dumpParamCons=</b><i>boolean</i>. Dump parameter constraints. See: <code>javarifier.ParameterConstraints</code>. [default false]</li>
<li><b>--dumpStubCons=</b><i>boolean</i>. Dump stub constraints. See: <code>javarifier.StubConstraints</code>. [default false]</li>
<li><b>--dumpSubtypeCons=</b><i>boolean</i>. Dump subtype constraints. See: <code>javarifier.SubtypeConstraints</code>. [default false]</li>
<li><b>--dumpOpenWorldCons=</b><i>boolean</i>. Dump open world constraints. See: <code>javarifier.OpenWorld</code>. [default false]</li>
</ul>
</li>
<li>Debugging Options
<ul>
<li><b>--debugLocalSplitting=</b><i>boolean</i>. Debug local splitting. See: <code>soot.toolkits.scalar.LocalSplitter</code>. [default false]</li>
<li><b>--debugStubs=</b><i>boolean</i>. Debug stubs. [default false]</li>
<li><b>--debugResolver=</b><i>boolean</i>. Debug signature resolver. See: <code>javarifier.TypeInitializer</code>. [default false]</li>
<li><b>--debugResolve=</b><i>boolean</i>. Debug Soot resolver. See: <code>soot.SootResolver</code>. [default false]</li>
<li><b>--debugTypeInference=</b><i>boolean</i>. Debug type inference. See: <code>javarifier.TypeInferencer</code>. [default false]</li>
<li><b>--debugBoundGuarder=</b><i>boolean</i>. Debug bound guarder. See: <code>javarifier.BoundGuarder</code>. [default false]</li>
<li><b>--debugSubtyping=</b><i>boolean</i>. Debug subtyping. See: <code>javarifier.ConstraintManager</code>. [default false]</li>
<li><b>--debugConstraintGeneration=</b><i>boolean</i>. Debug constraint generation. See: <code>javarifier.ConstraintGenerator</code>, <code>javarifier.ConstraintManager</code>. [default false]</li>
<li><b>--debugConstraints=</b><i>boolean</i>. Debug constraints. See: <code>javarifier.ConstraintTracker#printCauses</code>. [default false]</li>
<li><b>--debugSigParser=</b><i>boolean</i>. Debug signature parser. See: <code>javarifier.JVMLSigParser</code>. [default false]</li>
<li><b>--debugConstraintIncorporating=</b><i>boolean</i>. Debug constraint incorporating. See: <code>javarifier.Incorporater</code>. [default false]</li>
<li><b>--debugAnnotationLoading=</b><i>boolean</i>. Debug annotation loading. See: <code>javarifier.AnnotationScene</code>. [default false]</li>
<li><b>--debugAnnotationStoring=</b><i>boolean</i>. Debug annotation storing. See: <code>javarifier.AnnotationStorer</code>. [default false]</li>
</ul>
</li>
<li>Internal Options
<ul>
<li><b>--defaultStubCPEntries=</b><i>string</i>. Set the default classpath for stub classes.</li>
<li><b>--defaultWorldCPEntries=</b><i>string</i>. Set the default classpath for JDK jarfiles.</li>
</ul>
</li>
</ul>
<!-- end options doc -->
<h2 id="building-from-source"> Building from source </h2>
<p>
To build Javarifier from source, run the following commands:
</p>
<ol>
<li>Set environment variables. Add the following to your
<tt>~/.bashrc</tt> or equivalent. Set the <tt>JAVA_HOME</tt> environment variable
to the location of your JDK 7 installation (not the JRE installation). Then log out and log back in:
<pre>export JAVA_HOME=<em>/path/to/your/jdk</em>
export JSR308=$HOME/jsr308
export PATH=$JSR308/jsr308-langtools/dist/bin:${PATH}
export CLASSPATH=${CLASSPATH}:$JAVA_HOME/lib/tools.jar:$JSR308/checker-framework/checkers/binary/checkers.jar</pre>
</li>
<li>Obtain the source code.
<pre>mkdir -p $JSR308
cd $JSR308
hg clone https://code.google.com/p/jsr308-langtools/ jsr308-langtools
git clone https://github.com/typetools/annotation-tools.git annotation-tools
git clone https://github.com/typetools/checker-framework.git checker-framework
git clone https://github.com/typetools/javarifier.git javarifier</pre>
</li>
<li>Build everything. If any of the builds fails, consult that project's documentation.
<pre>cd $JSR308/jsr308-langtools/make \
&& ant clean build-javac build-javap \
&& cd $JSR308/annotation-tools \
&& ant \
&& cd $JSR308/checker-framework/checkers \
&& ant dist all-tests \
&& cd $JSR308/javarifier \
&& ant jarfile</pre>
<!--
(The form with && is better than pasting a set of separate commands
into a shell for two reasons. First, it halts if there is any error.
Second, <tt>ant</tt> seems to swallow all typeahead.) -->
</li>
</ol>
<p>
Later, to update all your sources and rebuild them, you can run:
</p>
<pre>
cd $JSR308/jsr308-langtools
hg pull -u
cd $JSR308/annotation-tools
git pull
cd $JSR308/checker-framework
git pull
cd $JSR308/javarifier
git pull
</pre>
<p>
and re-run the "Build everything" command immediately above.
</p>
<p>
Some additional notes appear in the <tt>README</tt> file.
</p>
<h3 id="compiling-with-eclipse">Compiling with Eclipse</h3>
<p>
The structure of the <tt>src/</tt> and <tt>bin/</tt> directories is such
that Eclipse can understand the Javarifier as a project, overwrites class
files in the same <tt>bin/</tt> directory the <tt>build.xml</tt> script
uses, and the <tt>build.xml</tt> file does not conflict with the
<tt>.classpath</tt> and <tt>.project</tt> files that Eclipse uses.
Therefore, you can safely use Eclipse for working on the Javarifier, but
before committing code changes you should make sure that the code compiles
using the build script.
</p>
<h2 id="feedback"> Feedback </h2>
<p>
If you encounter a problem in Javarifier, please submit a bug report via
its <a href="https://github.com/typetools/javarifier/issues">issue tracker</a>.
When reporting bugs, please help us to resolve the issue quickly by
including the complete
output of Javarifier, and exact instructions of how to
reproduce a bug (including all necessary input files).
</p>
<p>
Other questions, comments, and feature requests
can be sent to <a href="mailto:javarifier-dev@googlegroups.com">javarifier-dev@googlegroups.com</a>.
</p>
<h3 id="release-notes"> Release notes </h3>
<ul>
<li>
Version 0.1.4: (Released September 18, 2010)
<ul>
<li>Implemented and documented the heuristics for excluding fields
from the abstract state of an object.
See <a href="#using-heuristics"><code>--applyHeuristics</code></a>.
</li>
<li>Refactored the package containing all the Javari annotations from
<code>checkers.quals</code> to
<code>checkers.javari.quals</code>
</li>
<li>Command-line options now start with a double-dash prefix instead
of a single-dash prefix. Run <tt>javarifier -h</tt> for a list, or
<tt>javarifier -H</tt> for a full list.
</li>
<li>Improved diagnostic output (see <tt>--dumpCauses</tt>).
Removed some unnecessary and uninformative messages from output.
</li>
<li>The Javarifier release no longer includes a copy of the annotated
JDK. A Javarifier user should get the annotated JDK by installing the
<a href="https://checkerframework.org/">Checker
Framework</a>.
</li>
<li>Account for updates to scene library and Type Annotations specification.
</li>
<li>Add Eclipse .project and .classpath files.
</li>
<li>Many bug fixes to code, build files, and tests.
</li>
`<li>Uses <a href="https://mernst.github.io/plume-lib/">plume-lib</a>
(<tt>plume.jar</tt> added to <tt>lib/</tt>).
</li>
</ul>
</li>
<li>
Version 0.1.3: (Released April 27, 2008)
<ul>
<li> Changed the <code>@RoMaybe</code> qualifier for parametric
polymorphism over mutability to <code>@PolyRead</code>.
</li>
<li> Changed the type rule for inferring <code>@PolyRead</code>. Matches
<i>Inference of reference mutability</i>, which appears in ECOOP '08.
</li>
<li> Better documentation of the <code>--dumpConstraints</code>
command-line option and the format of its output.
</li>
<li> Documented the <code>--printStubs</code> command-line option.
</li>
<li> Included a test suite for testing Javarifier installation.
</li>
</ul>
</li>
<li>
Version 0.1.2: (Released March 7, 2008) Several bug fixes.
Javarifier now works on the Eclipse compiler, which is over
120,000 lines of Java code.
</li>
<li>
Version 0.1.1: (Released February 15, 2008) Several bug fixes and
updated documentation.
</li>
<li>
Version 0.1: (Released November 2, 2007) First release.
</li>
</ul>
<hr/>
<p>
Last revised: January 30, 2017
</p>
</body>
</html>
<!--
This makes Emacs update the "Last revised" paragraph above every time
you save the file.
-->
<!--
Local Variables:
time-stamp-start: "^Last revised: "
time-stamp-end: "\\.?$"
time-stamp-format: "%:b %:d, %:y"
time-stamp-line-limit: -100
End:
-->
<!-- LocalWords: utils bashrc tcsh tcshrc cshrc classpath Javarifier Javari -->
<!-- LocalWords: mutabilities subtyping contra javarifier zipfile csh GG im -->
<!-- LocalWords: Javarifier's Tschantz jarfiles programCPEntries LGraph JVML -->
<!-- LocalWords: romaybe LocalVariableTypeTable setenv myPackage cd -->
<!-- LocalWords: myClassOne myClassTwo perl jaif myClass applyHeuristics TODO -->
<!-- LocalWords: dumpCauses readonly ClassName LineNumber methodName hashMap -->
<!-- LocalWords: MemberName dumpConstraints ctx classfile HashEntry boolean -->
<!-- LocalWords: allHelp reallyQuiet openWorld polyread stubCPEntries jsr hg -->
<!-- LocalWords: worldCPEntries useWorldAsStubs extraAnnotationInputFile src -->
<!-- LocalWords: filename outputFile outputFormat annotationIndexFile dirname -->
<!-- LocalWords: scenePrinter twoFiles outputFilterLocals outputLimitKind xml -->
<!-- LocalWords: outputSortMembers outputMainClassFirst skipEmpty ReadOnly -->
<!-- LocalWords: includeImmutableClasses justPassThrough printStubs readlink -->
<!-- LocalWords: missingStubs dumpResults dumpGeneratorConstraints debugStubs -->
<!-- LocalWords: dumpBoundGuards dumpParamCons dumpStubCons dumpSubtypeCons -->
<!-- LocalWords: dumpOpenWorldCons debugLocalSplitting debugResolver mkdir -->
<!-- LocalWords: debugResolve debugTypeInference debugBoundGuarder langtools -->
<!-- LocalWords: debugSubtyping debugConstraintGeneration debugConstraints
-->
<!-- LocalWords: debugSigParser debugConstraintIncorporating javap jarfile
-->
<!-- LocalWords: debugAnnotationLoading debugAnnotationStoring typeahead
-->
<!-- LocalWords: defaultStubCPEntries defaultWorldCPEntries README
-->