Adds the source of the checker framework

This needs to predate the rest of the changes to the checker framework to keep the build green.

Also add the source of javacutil part of the checker framework, that will be included in the next change.

Change-Id: Ie18d0e8e21035ce5141416e552a83d893f71b88b

20 files changed, 5772 insertions, 0 deletions

diff --git a/third_party/checker_framework_javacutil/LICENSE.txt b/third_party/checker_framework_javacutil/LICENSE.txt
new file mode 100644
index 0000000000..c4b232d9bc
--- /dev/null
+++ b/third_party/checker_framework_javacutil/LICENSE.txt
@@ -0,0 +1,417 @@
+Most of the Checker Framework is licensed under the GNU General Public
+License, version 2 (GPL2), with the classpath exception.  The text of this
+license appears below.  This is the same license used for OpenJDK.
+
+A few parts of the Checker Framework have more permissive licenses.
+
+ * The annotations are licensed under the MIT License.  (The text of this
+   license appears below.)  More specifically, all the parts of the Checker
+   Framework that you might want to include with your own program use the
+   MIT License.  This is the checker-qual.jar file and all the files that
+   appear in it:  every file in a qual/ directory, plus utility files such
+   as NullnessUtils.java, RegexUtil.java, UnsignednessUtil.java, etc.
+   In addition, the cleanroom implementations of third-party annotations,
+   which the Checker Framework recognizes as aliases for its own
+   annotations, are licensed under the MIT License.
+
+ * The Maven plugin is dual-licensed (you may use whichever you prefer)
+   under GPL2 and the Apache License, version 2.0 (Apache2).  The text of
+   Apache2 appears in file maven-plugin/LICENSE.txt.  Maven itself uses
+   Apache2.
+
+ * The Eclipse plugin is dual-licensed (you may use whichever you prefer)
+   under GPL2 and the Eclipse Public License Version 1.0 (EPL).  EPL
+   appears http://www.eclipse.org/org/documents/epl-v10.php.  Eclipse
+   itself uses EPL.
+
+Some external libraries that are included with the Checker Framework have
+different licenses.
+
+ * javaparser is licensed under the LGPL.  (The javaparser source code
+   contains a file with the text of the GPL, but it is not clear why, since
+   javaparser does not use the GPL.)  See file javaparser/COPYING.LESSER
+   and the source code of all its files.
+
+ * JUnit is licensed under the Common Public License v1.0 (see
+   http://www.junit.org/license), with parts (Hamcrest) licensed under the
+   BSD License (see http://hamcrest.org/JavaHamcrest/).
+
+ * plume-lib is licensed under the MIT License.
+
+The Checker Framework includes annotations for several libraries, in
+directory checker/jdk/.  Each annotated library uses the same license as
+the unannotated version of the library.
+
+===========================================================================
+
+The GNU General Public License (GPL)
+
+Version 2, June 1991
+
+Copyright (C) 1989, 1991 Free Software Foundation, Inc.
+59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+
+Everyone is permitted to copy and distribute verbatim copies of this license
+document, but changing it is not allowed.
+
+Preamble
+
+The licenses for most software are designed to take away your freedom to share
+and change it.  By contrast, the GNU General Public License is intended to
+guarantee your freedom to share and change free software--to make sure the
+software is free for all its users.  This General Public License applies to
+most of the Free Software Foundation's software and to any other program whose
+authors commit to using it.  (Some other Free Software Foundation software is
+covered by the GNU Library General Public License instead.) You can apply it to
+your programs, too.
+
+When we speak of free software, we are referring to freedom, not price.  Our
+General Public Licenses are designed to make sure that you have the freedom to
+distribute copies of free software (and charge for this service if you wish),
+that you receive source code or can get it if you want it, that you can change
+the software or use pieces of it in new free programs; and that you know you
+can do these things.
+
+To protect your rights, we need to make restrictions that forbid anyone to deny
+you these rights or to ask you to surrender the rights.  These restrictions
+translate to certain responsibilities for you if you distribute copies of the
+software, or if you modify it.
+
+For example, if you distribute copies of such a program, whether gratis or for
+a fee, you must give the recipients all the rights that you have.  You must
+make sure that they, too, receive or can get the source code.  And you must
+show them these terms so they know their rights.
+
+We protect your rights with two steps: (1) copyright the software, and (2)
+offer you this license which gives you legal permission to copy, distribute
+and/or modify the software.
+
+Also, for each author's protection and ours, we want to make certain that
+everyone understands that there is no warranty for this free software.  If the
+software is modified by someone else and passed on, we want its recipients to
+know that what they have is not the original, so that any problems introduced
+by others will not reflect on the original authors' reputations.
+
+Finally, any free program is threatened constantly by software patents.  We
+wish to avoid the danger that redistributors of a free program will
+individually obtain patent licenses, in effect making the program proprietary.
+To prevent this, we have made it clear that any patent must be licensed for
+everyone's free use or not licensed at all.
+
+The precise terms and conditions for copying, distribution and modification
+follow.
+
+TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+0. This License applies to any program or other work which contains a notice
+placed by the copyright holder saying it may be distributed under the terms of
+this General Public License.  The "Program", below, refers to any such program
+or work, and a "work based on the Program" means either the Program or any
+derivative work under copyright law: that is to say, a work containing the
+Program or a portion of it, either verbatim or with modifications and/or
+translated into another language.  (Hereinafter, translation is included
+without limitation in the term "modification".) Each licensee is addressed as
+"you".
+
+Activities other than copying, distribution and modification are not covered by
+this License; they are outside its scope.  The act of running the Program is
+not restricted, and the output from the Program is covered only if its contents
+constitute a work based on the Program (independent of having been made by
+running the Program).  Whether that is true depends on what the Program does.
+
+1. You may copy and distribute verbatim copies of the Program's source code as
+you receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice and
+disclaimer of warranty; keep intact all the notices that refer to this License
+and to the absence of any warranty; and give any other recipients of the
+Program a copy of this License along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and you may
+at your option offer warranty protection in exchange for a fee.
+
+2. You may modify your copy or copies of the Program or any portion of it, thus
+forming a work based on the Program, and copy and distribute such modifications
+or work under the terms of Section 1 above, provided that you also meet all of
+these conditions:
+
+    a) You must cause the modified files to carry prominent notices stating
+    that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in whole or
+    in part contains or is derived from the Program or any part thereof, to be
+    licensed as a whole at no charge to all third parties under the terms of
+    this License.
+
+    c) If the modified program normally reads commands interactively when run,
+    you must cause it, when started running for such interactive use in the
+    most ordinary way, to print or display an announcement including an
+    appropriate copyright notice and a notice that there is no warranty (or
+    else, saying that you provide a warranty) and that users may redistribute
+    the program under these conditions, and telling the user how to view a copy
+    of this License.  (Exception: if the Program itself is interactive but does
+    not normally print such an announcement, your work based on the Program is
+    not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If identifiable
+sections of that work are not derived from the Program, and can be reasonably
+considered independent and separate works in themselves, then this License, and
+its terms, do not apply to those sections when you distribute them as separate
+works.  But when you distribute the same sections as part of a whole which is a
+work based on the Program, the distribution of the whole must be on the terms
+of this License, whose permissions for other licensees extend to the entire
+whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest your
+rights to work written entirely by you; rather, the intent is to exercise the
+right to control the distribution of derivative or collective works based on
+the Program.
+
+In addition, mere aggregation of another work not based on the Program with the
+Program (or with a work based on the Program) on a volume of a storage or
+distribution medium does not bring the other work under the scope of this
+License.
+
+3. You may copy and distribute the Program (or a work based on it, under
+Section 2) in object code or executable form under the terms of Sections 1 and
+2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable source
+    code, which must be distributed under the terms of Sections 1 and 2 above
+    on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three years, to
+    give any third party, for a charge no more than your cost of physically
+    performing source distribution, a complete machine-readable copy of the
+    corresponding source code, to be distributed under the terms of Sections 1
+    and 2 above on a medium customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer to
+    distribute corresponding source code.  (This alternative is allowed only
+    for noncommercial distribution and only if you received the program in
+    object code or executable form with such an offer, in accord with
+    Subsection b above.)
+
+The source code for a work means the preferred form of the work for making
+modifications to it.  For an executable work, complete source code means all
+the source code for all modules it contains, plus any associated interface
+definition files, plus the scripts used to control compilation and installation
+of the executable.  However, as a special exception, the source code
+distributed need not include anything that is normally distributed (in either
+source or binary form) with the major components (compiler, kernel, and so on)
+of the operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering access to copy
+from a designated place, then offering equivalent access to copy the source
+code from the same place counts as distribution of the source code, even though
+third parties are not compelled to copy the source along with the object code.
+
+4. You may not copy, modify, sublicense, or distribute the Program except as
+expressly provided under this License.  Any attempt otherwise to copy, modify,
+sublicense or distribute the Program is void, and will automatically terminate
+your rights under this License.  However, parties who have received copies, or
+rights, from you under this License will not have their licenses terminated so
+long as such parties remain in full compliance.
+
+5. You are not required to accept this License, since you have not signed it.
+However, nothing else grants you permission to modify or distribute the Program
+or its derivative works.  These actions are prohibited by law if you do not
+accept this License.  Therefore, by modifying or distributing the Program (or
+any work based on the Program), you indicate your acceptance of this License to
+do so, and all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+6. Each time you redistribute the Program (or any work based on the Program),
+the recipient automatically receives a license from the original licensor to
+copy, distribute or modify the Program subject to these terms and conditions.
+You may not impose any further restrictions on the recipients' exercise of the
+rights granted herein.  You are not responsible for enforcing compliance by
+third parties to this License.
+
+7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues), conditions
+are imposed on you (whether by court order, agreement or otherwise) that
+contradict the conditions of this License, they do not excuse you from the
+conditions of this License.  If you cannot distribute so as to satisfy
+simultaneously your obligations under this License and any other pertinent
+obligations, then as a consequence you may not distribute the Program at all.
+For example, if a patent license would not permit royalty-free redistribution
+of the Program by all those who receive copies directly or indirectly through
+you, then the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under any
+particular circumstance, the balance of the section is intended to apply and
+the section as a whole is intended to apply in other circumstances.
+
+It is not the purpose of this section to induce you to infringe any patents or
+other property right claims or to contest validity of any such claims; this
+section has the sole purpose of protecting the integrity of the free software
+distribution system, which is implemented by public license practices.  Many
+people have made generous contributions to the wide range of software
+distributed through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing to
+distribute software through any other system and a licensee cannot impose that
+choice.
+
+This section is intended to make thoroughly clear what is believed to be a
+consequence of the rest of this License.
+
+8. If the distribution and/or use of the Program is restricted in certain
+countries either by patents or by copyrighted interfaces, the original
+copyright holder who places the Program under this License may add an explicit
+geographical distribution limitation excluding those countries, so that
+distribution is permitted only in or among countries not thus excluded.  In
+such case, this License incorporates the limitation as if written in the body
+of this License.
+
+9. The Free Software Foundation may publish revised and/or new versions of the
+General Public License from time to time.  Such new versions will be similar in
+spirit to the present version, but may differ in detail to address new problems
+or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any later
+version", you have the option of following the terms and conditions either of
+that version or of any later version published by the Free Software Foundation.
+If the Program does not specify a version number of this License, you may
+choose any version ever published by the Free Software Foundation.
+
+10. If you wish to incorporate parts of the Program into other free programs
+whose distribution conditions are different, write to the author to ask for
+permission.  For software which is copyrighted by the Free Software Foundation,
+write to the Free Software Foundation; we sometimes make exceptions for this.
+Our decision will be guided by the two goals of preserving the free status of
+all derivatives of our free software and of promoting the sharing and reuse of
+software generally.
+
+NO WARRANTY
+
+11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY FOR
+THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN OTHERWISE
+STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE
+PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED,
+INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
+FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
+PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE,
+YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL
+ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR REDISTRIBUTE THE
+PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR
+INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA
+BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
+FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER
+OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.
+
+END OF TERMS AND CONDITIONS
+
+How to Apply These Terms to Your New Programs
+
+If you develop a new program, and you want it to be of the greatest possible
+use to the public, the best way to achieve this is to make it free software
+which everyone can redistribute and change under these terms.
+
+To do so, attach the following notices to the program.  It is safest to attach
+them to the start of each source file to most effectively convey the exclusion
+of warranty; and each file should have at least the "copyright" line and a
+pointer to where the full notice is found.
+
+    One line to give the program's name and a brief idea of what it does.
+
+    Copyright (C) <year> <name of author>
+
+    This program is free software; you can redistribute it and/or modify it
+    under the terms of the GNU General Public License as published by the Free
+    Software Foundation; either version 2 of the License, or (at your option)
+    any later version.
+
+    This program is distributed in the hope that it will be useful, but WITHOUT
+    ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
+    FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
+    more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc., 59
+    Temple Place, Suite 330, Boston, MA 02111-1307 USA
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this when it
+starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author Gnomovision comes
+    with ABSOLUTELY NO WARRANTY; for details type 'show w'.  This is free
+    software, and you are welcome to redistribute it under certain conditions;
+    type 'show c' for details.
+
+The hypothetical commands 'show w' and 'show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may be
+called something other than 'show w' and 'show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.  Here
+is a sample; alter the names:
+
+    Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+    'Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+    signature of Ty Coon, 1 April 1989
+
+    Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Library General Public
+License instead of this License.
+
+
+"CLASSPATH" EXCEPTION TO THE GPL
+
+Certain source files distributed by Oracle America and/or its affiliates are
+subject to the following clarification and special exception to the GPL, but
+only where Oracle has expressly included in the particular source file's header
+the words "Oracle designates this particular file as subject to the "Classpath"
+exception as provided by Oracle in the LICENSE file that accompanied this code."
+
+    Linking this library statically or dynamically with other modules is making
+    a combined work based on this library.  Thus, the terms and conditions of
+    the GNU General Public License cover the whole combination.
+
+    As a special exception, the copyright holders of this library give you
+    permission to link this library with independent modules to produce an
+    executable, regardless of the license terms of these independent modules,
+    and to copy and distribute the resulting executable under terms of your
+    choice, provided that you also meet, for each linked independent module,
+    the terms and conditions of the license of that module.  An independent
+    module is a module which is not derived from or based on this library.  If
+    you modify this library, you may extend this exception to your version of
+    the library, but you are not obligated to do so.  If you do not wish to do
+    so, delete this exception statement from your version.
+
+===========================================================================
+
+MIT License:
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+
+===========================================================================
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AbstractTypeProcessor.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AbstractTypeProcessor.java
new file mode 100644
index 0000000000..8db8da333c
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AbstractTypeProcessor.java
@@ -0,0 +1,220 @@
+package org.checkerframework.javacutil;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import javax.annotation.processing.*;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.util.ElementFilter;
+
+import com.sun.tools.javac.main.JavaCompiler;
+import com.sun.tools.javac.comp.CompileStates.CompileState;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.Log;
+
+import com.sun.source.tree.ClassTree;
+import com.sun.source.util.JavacTask;
+import com.sun.source.util.TaskEvent;
+import com.sun.source.util.TaskListener;
+import com.sun.source.util.TreePath;
+import com.sun.source.util.Trees;
+
+/**
+ * This class is an abstract annotation processor designed to be a
+ * convenient superclass for concrete "type processors", processors that
+ * require the type information in the processed source.
+ *
+ * <p>Type processing occurs in one round after the tool (e.g. Java compiler)
+ * analyzes the source (all sources taken as input to the tool and sources
+ * generated by other annotation processors).
+ *
+ * <p>The tool infrastructure will interact with classes extending this abstract
+ * class as follows.
+ *
+ * <p>
+ *  1-3 are Identical to the {@link Processor} life cycle.
+ *  4-5 are unique to {@code AbstractTypeProcessor} subclasses.
+ *
+ * <ol>
+ *
+ * <li>If an existing {@code Processor} object is not being used, to
+ * create an instance of a processor the tool calls the no-arg
+ * constructor of the processor class.
+ *
+ * <li>Next, the tool calls the {@link #init init} method with
+ * an appropriate {@code ProcessingEnvironment}.
+ *
+ * <li>Afterwards, the tool calls {@link #getSupportedAnnotationTypes
+ * getSupportedAnnotationTypes}, {@link #getSupportedOptions
+ * getSupportedOptions}, and {@link #getSupportedSourceVersion
+ * getSupportedSourceVersion}.  These methods are only called once per
+ * run, not on each round.
+ *
+ *
+ * <li>For each class containing a supported annotation, the tool calls
+ * {@link #typeProcess(TypeElement, TreePath) typeProcess} method on the
+ * {@code Processor}.  The class is guaranteed to be type-checked Java code
+ * and all the tree type and symbol information is resolved.
+ *
+ * <li>Finally, the tools calls the
+ * {@link #typeProcessingOver() typeProcessingOver} method
+ * on the {@code Processor}.
+ *
+ * </ol>
+ *
+ * <p>The tool is permitted to ask type processors to process a class once
+ * it is analyzed before the rest of classes are analyzed.  The tool is also
+ * permitted to stop type processing immediately if any errors are raised,
+ * without invoking {@code typeProcessingOver}
+ *
+ * <p>A subclass may override any of the methods in this class, as long as the
+ * general {@link javax.annotation.processing.Processor Processor}
+ * contract is obeyed, with one notable exception.
+ * {@link #process(Set, RoundEnvironment)} may not be overridden, as it
+ * is called during the declaration annotation phase before classes are analyzed.
+ *
+ * @author Mahmood Ali
+ * @author Werner Dietl
+ */
+public abstract class AbstractTypeProcessor extends AbstractProcessor {
+    /**
+     * The set of fully-qualified element names that should be type-checked.
+     * We store the names of the elements, in order to prevent
+     * possible confusion between different Element instantiations.
+     */
+    private final Set<Name> elements = new HashSet<Name>();
+
+    /**
+     * Method {@link #typeProcessingStart()} must be invoked exactly once,
+     * before any invocation of {@link #typeProcess(TypeElement, TreePath)}.
+     */
+    private boolean hasInvokedTypeProcessingStart = false;
+
+    /**
+     * Method {@link #typeProcessingOver()} must be invoked exactly once,
+     * after the last invocation of {@link #typeProcess(TypeElement, TreePath)}.
+     */
+    private static boolean hasInvokedTypeProcessingOver = false;
+
+    /**
+     * The TaskListener registered for completion of attribution.
+     */
+    private final AttributionTaskListener listener = new AttributionTaskListener();
+
+    /**
+     * Constructor for subclasses to call.
+     */
+    protected AbstractTypeProcessor() { }
+
+    /**
+     * {@inheritDoc}
+     *
+     * Register a TaskListener that will get called after FLOW.
+     */
+    @Override
+    public void init(ProcessingEnvironment env) {
+        super.init(env);
+        JavacTask.instance(env).addTaskListener(listener);
+        Context ctx = ((JavacProcessingEnvironment) processingEnv).getContext();
+        JavaCompiler compiler = JavaCompiler.instance(ctx);
+        compiler.shouldStopPolicyIfNoError = CompileState.max(compiler.shouldStopPolicyIfNoError,
+                                                           CompileState.FLOW);
+    }
+
+    /**
+     * The use of this method is obsolete in type processors.  The method is
+     * called during declaration annotation processing phase only.
+     * It registers the names of elements to process.
+     */
+    @Override
+    public final boolean process(Set<? extends TypeElement> annotations,
+            RoundEnvironment roundEnv) {
+        for (TypeElement elem : ElementFilter.typesIn(roundEnv.getRootElements())) {
+            elements.add(elem.getQualifiedName());
+        }
+        return false;
+    }
+
+    /**
+     * A method to be called once before the first call to typeProcess.
+     *
+     * <p>Subclasses may override this method to do any initialization work.
+     */
+    public void typeProcessingStart() {}
+
+    /**
+     * Processes a fully-analyzed class that contains a supported annotation
+     * (see {@link #getSupportedAnnotationTypes()}).
+     *
+     * <p>The passed class is always valid type-checked Java code.
+     *
+     * @param element       element of the analyzed class
+     * @param tree  the tree path to the element, with the leaf being a
+     *              {@link ClassTree}
+     */
+    public abstract void typeProcess(TypeElement element, TreePath tree);
+
+    /**
+     * A method to be called once all the classes are processed and no error
+     * is reported.
+     *
+     * <p>Subclasses may override this method to do any aggregate analysis
+     * (e.g. generate report, persistence) or resource deallocation.
+     *
+     * <p>If an error (a Java error or a processor error) is reported, this
+     * method is not guaranteed to be invoked.
+     */
+    public void typeProcessingOver() { }
+
+    /**
+     * A task listener that invokes the processor whenever a class is fully
+     * analyzed.
+     */
+    private final class AttributionTaskListener implements TaskListener {
+
+        @Override
+        public void finished(TaskEvent e) {
+            if (e.getKind() != TaskEvent.Kind.ANALYZE) {
+                return;
+            }
+
+            if (!hasInvokedTypeProcessingStart) {
+                typeProcessingStart();
+                hasInvokedTypeProcessingStart = true;
+            }
+
+            Log log = Log.instance(((JavacProcessingEnvironment) processingEnv).getContext());
+
+            if (!hasInvokedTypeProcessingOver && elements.isEmpty() && log.nerrors == 0) {
+                typeProcessingOver();
+                hasInvokedTypeProcessingOver = true;
+            }
+
+            if (e.getTypeElement() == null) {
+                throw new AssertionError("event task without a type element");
+            }
+            if (e.getCompilationUnit() == null) {
+                throw new AssertionError("event task without compilation unit");
+            }
+
+            if (!elements.remove(e.getTypeElement().getQualifiedName())) {
+                return;
+            }
+
+            TypeElement elem = e.getTypeElement();
+            TreePath p = Trees.instance(processingEnv).getPath(elem);
+
+            typeProcess(elem, p);
+
+            if (!hasInvokedTypeProcessingOver && elements.isEmpty() && log.nerrors == 0) {
+                typeProcessingOver();
+                hasInvokedTypeProcessingOver = true;
+            }
+        }
+
+        @Override
+        public void started(TaskEvent e) { }
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationProvider.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationProvider.java
new file mode 100644
index 0000000000..580be40ef4
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationProvider.java
@@ -0,0 +1,38 @@
+package org.checkerframework.javacutil;
+
+import java.lang.annotation.Annotation;
+
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.Element;
+
+import com.sun.source.tree.Tree;
+
+/**
+ * An implementation of AnnotationProvider returns annotations on
+ * Java AST elements.
+ */
+public interface AnnotationProvider {
+
+    /**
+     * Returns the actual annotation mirror used to annotate this type,
+     * whose name equals the passed annotationName if one exists, null otherwise.
+     *
+     * @param anno annotation class
+     * @return the annotation mirror for anno
+     */
+    public AnnotationMirror getDeclAnnotation(Element elt,
+            Class<? extends Annotation> anno);
+
+    /**
+     * Return the annotation on {@code tree} that has the class
+     * {@code target}. If no annotation for the given target class exists,
+     * the result is {@code null}
+     *
+     * @param tree
+     *            The tree of which the annotation is returned
+     * @param target
+     *            The class of the annotation
+     */
+    public AnnotationMirror getAnnotationMirror(Tree tree,
+            Class<? extends Annotation> target);
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationUtils.java
new file mode 100644
index 0000000000..19eb74df49
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/AnnotationUtils.java
@@ -0,0 +1,612 @@
+package org.checkerframework.javacutil;
+
+/*>>>
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.checker.nullness.qual.*;
+import org.checkerframework.checker.interning.qual.*;
+*/
+
+
+import java.lang.annotation.Annotation;
+import java.lang.annotation.Inherited;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.TreeMap;
+import java.util.TreeSet;
+
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.AnnotationValue;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.ElementFilter;
+import javax.lang.model.util.Elements;
+
+import com.sun.source.tree.AnnotationTree;
+import com.sun.source.tree.MethodTree;
+import com.sun.source.tree.ModifiersTree;
+import com.sun.tools.javac.code.Symbol.VarSymbol;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.model.JavacElements;
+/**
+ * A utility class for working with annotations.
+ */
+public class AnnotationUtils {
+
+    // Class cannot be instantiated.
+    private AnnotationUtils() { throw new AssertionError("Class AnnotationUtils cannot be instantiated."); }
+
+    // TODO: hack to clear out static state.
+    // {@link org.checkerframework.qualframework.util.QualifierContext} should
+    // handle instantiation of utility classes.
+    public static void clear() {
+        annotationsFromNames.clear();
+        annotationMirrorNames.clear();
+        annotationMirrorSimpleNames.clear();
+        annotationClassNames.clear();
+    }
+
+    // **********************************************************************
+    // Factory Methods to create instances of AnnotationMirror
+    // **********************************************************************
+
+    /** Caching for annotation creation. */
+    private static final Map<CharSequence, AnnotationMirror> annotationsFromNames
+        = new HashMap<CharSequence, AnnotationMirror>();
+
+
+    private static final int ANNOTATION_CACHE_SIZE = 500;
+
+    /**
+     * Cache names of AnnotationMirrors for faster access.  Values in
+     * the map are interned Strings, so they can be compared with ==.
+     */
+    private static final Map<AnnotationMirror, /*@Interned*/ String> annotationMirrorNames
+        = CollectionUtils.createLRUCache(ANNOTATION_CACHE_SIZE);
+
+    /**
+     * Cache simple names of AnnotationMirrors for faster access.  Values in
+     * the map are interned Strings, so they can be compared with ==.
+     */
+    private static final Map<AnnotationMirror, /*@Interned*/ String> annotationMirrorSimpleNames
+        = CollectionUtils.createLRUCache(ANNOTATION_CACHE_SIZE);
+
+    /**
+     * Cache names of classes representing AnnotationMirrors for
+     * faster access.  Values in the map are interned Strings, so they
+     * can be compared with ==.
+     */
+    private static final Map<Class<? extends Annotation>, /*@Interned*/ String> annotationClassNames
+        = new HashMap<Class<? extends Annotation>, /*@Interned*/ String>();
+
+    /**
+     * Creates an {@link AnnotationMirror} given by a particular
+     * fully-qualified name.  getElementValues on the result returns an
+     * empty map.
+     *
+     * @param elements the element utilities to use
+     * @param name the name of the annotation to create
+     * @return an {@link AnnotationMirror} of type {@code} name
+     */
+    public static AnnotationMirror fromName(Elements elements, CharSequence name) {
+        if (annotationsFromNames.containsKey(name)) {
+            return annotationsFromNames.get(name);
+        }
+        final DeclaredType annoType = typeFromName(elements, name);
+        if (annoType == null) {
+            return null;
+        }
+        if (annoType.asElement().getKind() != ElementKind.ANNOTATION_TYPE) {
+            ErrorReporter.errorAbort(annoType + " is not an annotation");
+            return null; // dead code
+        }
+        AnnotationMirror result = new AnnotationMirror() {
+            String toString = "@" + annoType;
+
+            @Override
+            public DeclaredType getAnnotationType() {
+                return annoType;
+            }
+            @Override
+            public Map<? extends ExecutableElement, ? extends AnnotationValue>
+                getElementValues() {
+                return Collections.emptyMap();
+            }
+            /*@SideEffectFree*/
+            @Override
+            public String toString() {
+                return toString;
+            }
+        };
+        annotationsFromNames.put(name, result);
+        return result;
+    }
+
+    /**
+     * Creates an {@link AnnotationMirror} given by a particular annotation
+     * class.
+     *
+     * @param elements the element utilities to use
+     * @param clazz the annotation class
+     * @return an {@link AnnotationMirror} of type given type
+     */
+    public static AnnotationMirror fromClass(Elements elements, Class<? extends Annotation> clazz) {
+        return fromName(elements, clazz.getCanonicalName());
+    }
+
+    /**
+     * A utility method that converts a {@link CharSequence} (usually a {@link
+     * String}) into a {@link TypeMirror} named thereby.
+     *
+     * @param elements the element utilities to use
+     * @param name the name of a type
+     * @return the {@link TypeMirror} corresponding to that name
+     */
+    private static DeclaredType typeFromName(Elements elements, CharSequence name) {
+        /*@Nullable*/ TypeElement typeElt = elements.getTypeElement(name);
+        if (typeElt == null) {
+            return null;
+        }
+
+        return (DeclaredType) typeElt.asType();
+    }
+
+
+    // **********************************************************************
+    // Helper methods to handle annotations.  mainly workaround
+    // AnnotationMirror.equals undesired property
+    // (I think the undesired property is that it's reference equality.)
+    // **********************************************************************
+
+    /**
+     * @return the fully-qualified name of an annotation as a String
+     */
+    public static final /*@Interned*/ String annotationName(AnnotationMirror annotation) {
+        if (annotationMirrorNames.containsKey(annotation)) {
+            return annotationMirrorNames.get(annotation);
+        }
+
+        final DeclaredType annoType = annotation.getAnnotationType();
+        final TypeElement elm = (TypeElement) annoType.asElement();
+        /*@Interned*/ String name = elm.getQualifiedName().toString().intern();
+        annotationMirrorNames.put(annotation, name);
+        return name;
+    }
+
+    /**
+     * @return the simple name of an annotation as a String
+     */
+    public static String annotationSimpleName(AnnotationMirror annotation) {
+        if (annotationMirrorSimpleNames.containsKey(annotation)) {
+            return annotationMirrorSimpleNames.get(annotation);
+        }
+
+        final DeclaredType annoType = annotation.getAnnotationType();
+        final TypeElement elm = (TypeElement) annoType.asElement();
+        /*@Interned*/ String name = elm.getSimpleName().toString().intern();
+        annotationMirrorSimpleNames.put(annotation, name);
+        return name;
+    }
+
+    /**
+     * Checks if both annotations are the same.
+     *
+     * Returns true iff both annotations are of the same type and have the
+     * same annotation values.  This behavior differs from
+     * {@code AnnotationMirror.equals(Object)}.  The equals method returns
+     * true iff both annotations are the same and annotate the same annotation
+     * target (e.g. field, variable, etc).
+     *
+     * @return true iff a1 and a2 are the same annotation
+     */
+    public static boolean areSame(/*@Nullable*/ AnnotationMirror a1, /*@Nullable*/ AnnotationMirror a2) {
+        if (a1 != null && a2 != null) {
+            if (annotationName(a1) != annotationName(a2)) {
+                return false;
+            }
+
+            Map<? extends ExecutableElement, ? extends AnnotationValue> elval1 = getElementValuesWithDefaults(a1);
+            Map<? extends ExecutableElement, ? extends AnnotationValue> elval2 = getElementValuesWithDefaults(a2);
+
+            return elval1.toString().equals(elval2.toString());
+        }
+
+        // only true, iff both are null
+        return a1 == a2;
+    }
+
+    /**
+     * @see #areSame(AnnotationMirror, AnnotationMirror)
+     * @return true iff a1 and a2 have the same annotation type
+     */
+    public static boolean areSameIgnoringValues(AnnotationMirror a1, AnnotationMirror a2) {
+        if (a1 != null && a2 != null) {
+            return annotationName(a1) == annotationName(a2);
+        }
+        return a1 == a2;
+    }
+
+    /**
+     * Checks that the annotation {@code am} has the name {@code aname}. Values
+     * are ignored.
+     */
+    public static boolean areSameByName(AnnotationMirror am, /*@Interned*/ String aname) {
+        // Both strings are interned.
+        return annotationName(am) == aname;
+    }
+
+    /**
+     * Checks that the annotation {@code am} has the name of {@code anno}.
+     * Values are ignored.
+     */
+    public static boolean areSameByClass(AnnotationMirror am,
+            Class<? extends Annotation> anno) {
+        /*@Interned*/ String canonicalName;
+        if (annotationClassNames.containsKey(anno)) {
+            canonicalName = annotationClassNames.get(anno);
+        } else {
+            canonicalName = anno.getCanonicalName().intern();
+            annotationClassNames.put(anno, canonicalName);
+        }
+        return areSameByName(am, canonicalName);
+    }
+
+    /**
+     * Checks that two collections contain the same annotations.
+     *
+     * @return true iff c1 and c2 contain the same annotations
+     */
+    public static boolean areSame(Collection<? extends AnnotationMirror> c1, Collection<? extends AnnotationMirror> c2) {
+        if (c1.size() != c2.size()) {
+            return false;
+        }
+        if (c1.size() == 1) {
+            return areSame(c1.iterator().next(), c2.iterator().next());
+        }
+
+        Set<AnnotationMirror> s1 = createAnnotationSet();
+        Set<AnnotationMirror> s2 = createAnnotationSet();
+        s1.addAll(c1);
+        s2.addAll(c2);
+
+        // depend on the fact that Set is an ordered set.
+        Iterator<AnnotationMirror> iter1 = s1.iterator();
+        Iterator<AnnotationMirror> iter2 = s2.iterator();
+
+        while (iter1.hasNext()) {
+            AnnotationMirror anno1 = iter1.next();
+            AnnotationMirror anno2 = iter2.next();
+            if (!areSame(anno1, anno2)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    /**
+     * Checks that the collection contains the annotation.
+     * Using Collection.contains does not always work, because it
+     * does not use areSame for comparison.
+     *
+     * @return true iff c contains anno, according to areSame
+     */
+    public static boolean containsSame(Collection<? extends AnnotationMirror> c, AnnotationMirror anno) {
+        for (AnnotationMirror an : c) {
+            if (AnnotationUtils.areSame(an, anno)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * Checks that the collection contains the annotation.
+     * Using Collection.contains does not always work, because it
+     * does not use areSame for comparison.
+     *
+     * @return true iff c contains anno, according to areSameByClass
+     */
+    public static boolean containsSameByClass(Collection<? extends AnnotationMirror> c, Class<? extends Annotation> anno) {
+        for (AnnotationMirror an : c) {
+            if (AnnotationUtils.areSameByClass(an, anno)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * Checks that the collection contains the annotation ignoring values.
+     * Using Collection.contains does not always work, because it
+     * does not use areSameIgnoringValues for comparison.
+     *
+     * @return true iff c contains anno, according to areSameIgnoringValues
+     */
+    public static boolean containsSameIgnoringValues(Collection<? extends AnnotationMirror> c, AnnotationMirror anno) {
+        for (AnnotationMirror an : c) {
+            if (AnnotationUtils.areSameIgnoringValues(an, anno)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    private static final Comparator<AnnotationMirror> ANNOTATION_ORDERING
+    = new Comparator<AnnotationMirror>() {
+        @Override
+        public int compare(AnnotationMirror a1, AnnotationMirror a2) {
+            String n1 = a1.toString();
+            String n2 = a2.toString();
+
+            return n1.compareTo(n2);
+        }
+    };
+
+    /**
+     * provide ordering for {@link AnnotationMirror} based on their fully
+     * qualified name.  The ordering ignores annotation values when ordering.
+     *
+     * The ordering is meant to be used as {@link TreeSet} or {@link TreeMap}
+     * ordering.  A {@link Set} should not contain two annotations that only
+     * differ in values.
+     */
+    public static Comparator<AnnotationMirror> annotationOrdering() {
+        return ANNOTATION_ORDERING;
+    }
+
+    /**
+     * Create a map suitable for storing {@link AnnotationMirror} as keys.
+     *
+     * It can store one instance of {@link AnnotationMirror} of a given
+     * declared type, regardless of the annotation element values.
+     *
+     * @param <V> the value of the map
+     * @return a new map with {@link AnnotationMirror} as key
+     */
+    public static <V> Map<AnnotationMirror, V> createAnnotationMap() {
+        return new TreeMap<AnnotationMirror, V>(annotationOrdering());
+    }
+
+    /**
+     * Constructs a {@link Set} suitable for storing {@link AnnotationMirror}s.
+     *
+     * It stores at most once instance of {@link AnnotationMirror} of a given
+     * type, regardless of the annotation element values.
+     *
+     * @return a new set to store {@link AnnotationMirror} as element
+     */
+    public static Set<AnnotationMirror> createAnnotationSet() {
+        return new TreeSet<AnnotationMirror>(annotationOrdering());
+    }
+
+    /** Returns true if the given annotation has a @Inherited meta-annotation. */
+    public static boolean hasInheritedMeta(AnnotationMirror anno) {
+        return anno.getAnnotationType().asElement().getAnnotation(Inherited.class) != null;
+    }
+
+
+    // **********************************************************************
+    // Extractors for annotation values
+    // **********************************************************************
+
+    /**
+     * Returns the values of an annotation's attributes, including defaults.
+     * The method with the same name in JavacElements cannot be used directly,
+     * because it includes a cast to Attribute.Compound, which doesn't hold
+     * for annotations generated by the Checker Framework.
+     *
+     * @see AnnotationMirror#getElementValues()
+     * @see JavacElements#getElementValuesWithDefaults(AnnotationMirror)
+     *
+     * @param ad  annotation to examine
+     * @return the values of the annotation's elements, including defaults
+     */
+    public static Map<? extends ExecutableElement, ? extends AnnotationValue>
+    getElementValuesWithDefaults(AnnotationMirror ad) {
+        Map<ExecutableElement, AnnotationValue> valMap
+            = new HashMap<ExecutableElement, AnnotationValue>();
+        if (ad.getElementValues() != null) {
+            valMap.putAll(ad.getElementValues());
+        }
+        for (ExecutableElement meth :
+            ElementFilter.methodsIn(ad.getAnnotationType().asElement().getEnclosedElements())) {
+            AnnotationValue defaultValue = meth.getDefaultValue();
+            if (defaultValue != null && !valMap.containsKey(meth)) {
+                valMap.put(meth, defaultValue);
+            }
+        }
+        return valMap;
+    }
+
+
+    /**
+     * Verify whether the attribute with the name {@code name} exists in
+     * the annotation {@code anno}.
+     *
+     * @param anno the annotation to examine
+     * @param name the name of the attribute
+     * @return whether the attribute exists in anno
+     */
+    public static <T> boolean hasElementValue(AnnotationMirror anno, CharSequence name) {
+        Map<? extends ExecutableElement, ? extends AnnotationValue> valmap = anno.getElementValues();
+        for (ExecutableElement elem : valmap.keySet()) {
+            if (elem.getSimpleName().contentEquals(name)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * Get the attribute with the name {@code name} of the annotation
+     * {@code anno}. The result is expected to have type {@code expectedType}.
+     *
+     * <p>
+     * <em>Note 1</em>: The method does not work well for attributes of an array
+     * type (as it would return a list of {@link AnnotationValue}s). Use
+     * {@code getElementValueArray} instead.
+     *
+     * <p>
+     * <em>Note 2</em>: The method does not work for attributes of an enum type,
+     * as the AnnotationValue is a VarSymbol and would be cast to the enum type,
+     * which doesn't work. Use {@code getElementValueEnum} instead.
+     *
+     *
+     * @param anno the annotation to disassemble
+     * @param name the name of the attribute to access
+     * @param expectedType the expected type used to cast the return type
+     * @param useDefaults whether to apply default values to the attribute
+     * @return the value of the attribute with the given name
+     */
+    public static <T> T getElementValue(AnnotationMirror anno, CharSequence name,
+            Class<T> expectedType, boolean useDefaults) {
+        Map<? extends ExecutableElement, ? extends AnnotationValue> valmap;
+        if (useDefaults) {
+            valmap = getElementValuesWithDefaults(anno);
+        } else {
+            valmap = anno.getElementValues();
+        }
+        for (ExecutableElement elem : valmap.keySet()) {
+            if (elem.getSimpleName().contentEquals(name)) {
+                AnnotationValue val = valmap.get(elem);
+                return expectedType.cast(val.getValue());
+            }
+        }
+        ErrorReporter.errorAbort("No element with name \'" + name + "\' in annotation " + anno);
+        return null; // dead code
+    }
+
+    /**
+     * Version that is suitable for Enum elements.
+     */
+    public static <T extends Enum<T>> T getElementValueEnum(
+            AnnotationMirror anno, CharSequence name, Class<T> t,
+            boolean useDefaults) {
+        VarSymbol vs = getElementValue(anno, name, VarSymbol.class, useDefaults);
+        T value = Enum.valueOf(t, vs.getSimpleName().toString());
+        return value;
+    }
+
+    /**
+     * Get the attribute with the name {@code name} of the annotation
+     * {@code anno}, where the attribute has an array type. One element of the
+     * result is expected to have type {@code expectedType}.
+     *
+     * Parameter useDefaults is used to determine whether default values
+     * should be used for annotation values. Finding defaults requires
+     * more computation, so should be false when no defaulting is needed.
+     *
+     * @param anno the annotation to disassemble
+     * @param name the name of the attribute to access
+     * @param expectedType the expected type used to cast the return type
+     * @param useDefaults whether to apply default values to the attribute
+     * @return the value of the attribute with the given name
+     */
+    public static <T> List<T> getElementValueArray(AnnotationMirror anno,
+            CharSequence name, Class<T> expectedType, boolean useDefaults) {
+        @SuppressWarnings("unchecked")
+        List<AnnotationValue> la = getElementValue(anno, name, List.class, useDefaults);
+        List<T> result = new ArrayList<T>(la.size());
+        for (AnnotationValue a : la) {
+            result.add(expectedType.cast(a.getValue()));
+        }
+        return result;
+    }
+
+    /**
+     * Get the attribute with the name {@code name} of the annotation
+     * {@code anno}, or the default value if no attribute is present explicitly,
+     * where the attribute has an array type and the elements are {@code Enum}s.
+     * One element of the result is expected to have type {@code expectedType}.
+     */
+    public static <T extends Enum<T>> List<T> getElementValueEnumArray(
+            AnnotationMirror anno, CharSequence name, Class<T> t,
+            boolean useDefaults) {
+        @SuppressWarnings("unchecked")
+        List<AnnotationValue> la = getElementValue(anno, name, List.class, useDefaults);
+        List<T> result = new ArrayList<T>(la.size());
+        for (AnnotationValue a : la) {
+            T value = Enum.valueOf(t, a.getValue().toString());
+            result.add(value);
+        }
+        return result;
+    }
+
+    /**
+     * Get the Name of the class that is referenced by attribute 'name'.
+     * This is a convenience method for the most common use-case.
+     * Like getElementValue(anno, name, ClassType.class).getQualifiedName(), but
+     * this method ensures consistent use of the qualified name.
+     */
+    public static Name getElementValueClassName(AnnotationMirror anno, CharSequence name,
+            boolean useDefaults) {
+        Type.ClassType ct = getElementValue(anno, name, Type.ClassType.class, useDefaults);
+        // TODO:  Is it a problem that this returns the type parameters too?  Should I cut them off?
+        return ct.asElement().getQualifiedName();
+    }
+
+    /**
+     * Get the Class that is referenced by attribute 'name'.
+     * This method uses Class.forName to load the class. It returns
+     * null if the class wasn't found.
+     */
+    public static Class<?> getElementValueClass(AnnotationMirror anno, CharSequence name,
+            boolean useDefaults) {
+        Name cn = getElementValueClassName(anno, name, useDefaults);
+        try {
+            Class<?> cls =  Class.forName(cn.toString());
+            return cls;
+        } catch (ClassNotFoundException e) {
+            ErrorReporter.errorAbort("Could not load class '" + cn + "' for field '" + name +
+                    "' in annotation " + anno, e);
+            return null; // dead code
+        }
+    }
+
+    /**
+     * See checkers.types.QualifierHierarchy#updateMappingToMutableSet(QualifierHierarchy, Map, Object, AnnotationMirror)
+     * (Not linked because it is in an independent project.
+     */
+    public static <T> void updateMappingToImmutableSet(Map<T, Set<AnnotationMirror>> map,
+            T key, Set<AnnotationMirror> newQual) {
+
+        Set<AnnotationMirror> result = AnnotationUtils.createAnnotationSet();
+        // TODO: if T is also an AnnotationMirror, should we use areSame?
+        if (!map.containsKey(key)) {
+            result.addAll(newQual);
+        } else {
+            result.addAll(map.get(key));
+            result.addAll(newQual);
+        }
+        map.put(key, Collections.unmodifiableSet(result));
+    }
+
+    /**
+     * Returns the annotations explicitly written on a constructor result.
+     * Callers should check that {@code constructorDeclaration} is in fact a declaration
+     * of a constructor.
+     *
+     * @param constructorDeclaration declaration tree of constructor
+     * @return set of annotations explicit on the resulting type of the constructor
+     */
+    public static Set<AnnotationMirror> getExplicitAnnotationsOnConstructorResult(MethodTree constructorDeclaration) {
+        Set<AnnotationMirror> annotationSet = AnnotationUtils.createAnnotationSet();
+        ModifiersTree modifiersTree = constructorDeclaration.getModifiers();
+        if (modifiersTree != null) {
+            List<? extends AnnotationTree> annotationTrees = modifiersTree.getAnnotations();
+            annotationSet.addAll(InternalUtils.annotationsFromTypeAnnotationTrees(annotationTrees));
+        }
+        return annotationSet;
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicAnnotationProvider.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicAnnotationProvider.java
new file mode 100644
index 0000000000..b885b5cbea
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicAnnotationProvider.java
@@ -0,0 +1,35 @@
+package org.checkerframework.javacutil;
+
+import java.lang.annotation.Annotation;
+
+import java.util.List;
+
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.Element;
+
+import com.sun.source.tree.Tree;
+
+public class BasicAnnotationProvider implements AnnotationProvider {
+
+    @Override
+    public AnnotationMirror getDeclAnnotation(Element elt,
+            Class<? extends Annotation> anno) {
+        List<? extends AnnotationMirror> annotationMirrors = elt
+                .getAnnotationMirrors();
+
+        // Then look at the real annotations.
+        for (AnnotationMirror am : annotationMirrors) {
+            if (AnnotationUtils.areSameByClass(am, anno)) {
+                return am;
+            }
+        }
+
+        return null;
+    }
+
+    @Override
+    public AnnotationMirror getAnnotationMirror(Tree tree,
+            Class<? extends Annotation> target) {
+        return null;
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicTypeProcessor.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicTypeProcessor.java
new file mode 100644
index 0000000000..1fa1e6cb82
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/BasicTypeProcessor.java
@@ -0,0 +1,42 @@
+package org.checkerframework.javacutil;
+
+import javax.lang.model.element.TypeElement;
+
+import com.sun.source.tree.CompilationUnitTree;
+
+import com.sun.source.util.TreePath;
+import com.sun.source.util.TreePathScanner;
+
+/**
+ * Process the types in an AST in a trivial manner, with hooks for derived classes
+ * to actually do something.
+ */
+public abstract class BasicTypeProcessor extends AbstractTypeProcessor {
+    /** The source tree that's being scanned. */
+    protected CompilationUnitTree currentRoot;
+
+    /**
+     * Create a TreePathScanner at the given root.
+     */
+    protected abstract TreePathScanner<?, ?> createTreePathScanner(CompilationUnitTree root);
+
+    /**
+     * Visit the tree path for the type element.
+     */
+    @Override
+    public void typeProcess(TypeElement e, TreePath p) {
+        currentRoot = p.getCompilationUnit();
+
+        TreePathScanner<?, ?> scanner = null;
+        try {
+            scanner = createTreePathScanner(currentRoot);
+            scanner.scan(p, null);
+        } catch (Throwable t) {
+            System.err.println("BasicTypeProcessor.typeProcess: unexpected Throwable (" +
+                    t.getClass().getSimpleName() + ")  when processing "
+                    + currentRoot.getSourceFile().getName() +
+                    (t.getMessage()!=null ? "; message: " + t.getMessage() : ""));
+        }
+    }
+
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/CollectionUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/CollectionUtils.java
new file mode 100644
index 0000000000..eaaa69115d
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/CollectionUtils.java
@@ -0,0 +1,26 @@
+package org.checkerframework.javacutil;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+
+/**
+ * Utility methods related to Java Collections
+ */
+public class CollectionUtils {
+
+    /**
+     * A Utility method for creating LRU cache
+     * @param size  size of the cache
+     * @return  a new cache with the provided size
+     */
+    public static <K, V> Map<K, V> createLRUCache(final int size) {
+        return new LinkedHashMap<K, V>() {
+
+            private static final long serialVersionUID = 5261489276168775084L;
+            @Override
+            protected boolean removeEldestEntry(Map.Entry<K, V> entry) {
+                return size() > size;
+            }
+        };
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ElementUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ElementUtils.java
new file mode 100644
index 0000000000..19f0500585
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ElementUtils.java
@@ -0,0 +1,425 @@
+package org.checkerframework.javacutil;
+
+/*>>>
+import org.checkerframework.checker.nullness.qual.Nullable;
+*/
+
+import static com.sun.tools.javac.code.Flags.ABSTRACT;
+import static com.sun.tools.javac.code.Flags.EFFECTIVELY_FINAL;
+import static com.sun.tools.javac.code.Flags.FINAL;
+
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Deque;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Modifier;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.PackageElement;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.ElementFilter;
+import javax.lang.model.util.Elements;
+
+import com.sun.tools.javac.code.Symbol;
+
+/**
+ * A Utility class for analyzing {@code Element}s.
+ */
+public class ElementUtils {
+
+    // Class cannot be instantiated.
+    private ElementUtils() { throw new AssertionError("Class ElementUtils cannot be instantiated."); }
+
+    /**
+     * Returns the innermost type element enclosing the given element
+     *
+     * @param elem the enclosed element of a class
+     * @return  the innermost type element
+     */
+    public static TypeElement enclosingClass(final Element elem) {
+        Element result = elem;
+        while (result != null && !result.getKind().isClass()
+                && !result.getKind().isInterface()) {
+            /*@Nullable*/ Element encl = result.getEnclosingElement();
+            result = encl;
+        }
+        return (TypeElement) result;
+    }
+
+    /**
+     * Returns the innermost package element enclosing the given element.
+     * The same effect as {@link javax.lang.model.util.Elements#getPackageOf(Element)}.
+     * Returns the element itself if it is a package.
+     *
+     * @param elem the enclosed element of a package
+     * @return the innermost package element
+     *
+     */
+    public static PackageElement enclosingPackage(final Element elem) {
+        Element result = elem;
+        while (result != null && result.getKind() != ElementKind.PACKAGE) {
+            /*@Nullable*/ Element encl = result.getEnclosingElement();
+            result = encl;
+        }
+        return (PackageElement) result;
+    }
+
+    /**
+     * Returns the "parent" package element for the given package element.
+     * For package "A.B" it gives "A".
+     * For package "A" it gives the default package.
+     * For the default package it returns null;
+     *
+     * Note that packages are not enclosed within each other, we have to manually climb
+     * the namespaces. Calling "enclosingPackage" on a package element returns the
+     * package element itself again.
+     *
+     * @param elem the package to start from
+     * @return the parent package element
+     *
+     */
+    public static PackageElement parentPackage(final Elements e, final PackageElement elem) {
+        // The following might do the same thing:
+        //   ((Symbol) elt).owner;
+        // TODO: verify and see whether the change is worth it.
+        String fqnstart = elem.getQualifiedName().toString();
+        String fqn = fqnstart;
+        if (fqn != null && !fqn.isEmpty() && fqn.contains(".")) {
+            fqn = fqn.substring(0, fqn.lastIndexOf('.'));
+            return e.getPackageElement(fqn);
+        }
+        return null;
+    }
+
+    /**
+     * Returns true if the element is a static element: whether it is a static
+     * field, static method, or static class
+     *
+     * @return true if element is static
+     */
+    public static boolean isStatic(Element element) {
+        return element.getModifiers().contains(Modifier.STATIC);
+    }
+
+    /**
+     * Returns true if the element is a final element: a final field, final
+     * method, or final class
+     *
+     * @return true if the element is final
+     */
+    public static boolean isFinal(Element element) {
+        return element.getModifiers().contains(Modifier.FINAL);
+    }
+
+    /**
+     * Returns true if the element is a effectively final element.
+     *
+     * @return true if the element is effectively final
+     */
+    public static boolean isEffectivelyFinal(Element element) {
+        Symbol sym = (Symbol) element;
+        if (sym.getEnclosingElement().getKind() == ElementKind.METHOD &&
+                (sym.getEnclosingElement().flags() & ABSTRACT) != 0) {
+            return true;
+        }
+        return (sym.flags() & (FINAL | EFFECTIVELY_FINAL)) != 0;
+    }
+
+    /**
+     * Returns the {@code TypeMirror} for usage of Element as a value. It
+     * returns the return type of a method element, the class type of a
+     * constructor, or simply the type mirror of the element itself.
+     *
+     * @return  the type for the element used as a value
+     */
+    public static TypeMirror getType(Element element) {
+        if (element.getKind() == ElementKind.METHOD) {
+            return ((ExecutableElement)element).getReturnType();
+        } else if (element.getKind() == ElementKind.CONSTRUCTOR) {
+            return enclosingClass(element).asType();
+        } else {
+            return element.asType();
+        }
+    }
+
+    /**
+     * Returns the qualified name of the inner most class enclosing
+     * the provided {@code Element}
+     *
+     * @param element
+     *            an element enclosed by a class, or a
+     *            {@code TypeElement}
+     * @return the qualified {@code Name} of the innermost class
+     *         enclosing the element
+     */
+    public static /*@Nullable*/ Name getQualifiedClassName(Element element) {
+        if (element.getKind() == ElementKind.PACKAGE) {
+            PackageElement elem = (PackageElement) element;
+            return elem.getQualifiedName();
+        }
+
+        TypeElement elem = enclosingClass(element);
+        if (elem == null) {
+            return null;
+        }
+
+        return elem.getQualifiedName();
+    }
+
+    /**
+     * Returns a verbose name that identifies the element.
+     */
+    public static String getVerboseName(Element elt) {
+        if (elt.getKind() == ElementKind.PACKAGE ||
+                elt.getKind().isClass() ||
+                elt.getKind().isInterface()) {
+            return getQualifiedClassName(elt).toString();
+        } else {
+            return getQualifiedClassName(elt) + "." + elt.toString();
+        }
+    }
+
+    /**
+     * Check if the element is an element for 'java.lang.Object'
+     *
+     * @param element   the type element
+     * @return true iff the element is java.lang.Object element
+     */
+    public static boolean isObject(TypeElement element) {
+        return element.getQualifiedName().contentEquals("java.lang.Object");
+    }
+
+    /**
+     * Returns true if the element is a constant time reference
+     */
+    public static boolean isCompileTimeConstant(Element elt) {
+        return elt != null
+            && (elt.getKind() == ElementKind.FIELD || elt.getKind() == ElementKind.LOCAL_VARIABLE)
+            && ((VariableElement)elt).getConstantValue() != null;
+    }
+
+    /**
+     * Returns true if the element is declared in ByteCode.
+     * Always return false if elt is a package.
+     */
+    public static boolean isElementFromByteCode(Element elt) {
+        if (elt == null) {
+            return false;
+        }
+
+        if (elt instanceof Symbol.ClassSymbol) {
+            Symbol.ClassSymbol clss = (Symbol.ClassSymbol) elt;
+            if (null != clss.classfile) {
+                // The class file could be a .java file
+                return clss.classfile.getName().endsWith(".class");
+            } else {
+                return false;
+            }
+        }
+        return isElementFromByteCode(elt.getEnclosingElement(), elt);
+    }
+
+    /**
+     * Returns true if the element is declared in ByteCode.
+     * Always return false if elt is a package.
+     */
+    private static boolean isElementFromByteCode(Element elt, Element orig) {
+        if (elt == null) {
+            return false;
+        }
+        if (elt instanceof Symbol.ClassSymbol) {
+            Symbol.ClassSymbol clss = (Symbol.ClassSymbol) elt;
+            if (null != clss.classfile) {
+                // The class file could be a .java file
+                return (clss.classfile.getName().endsWith(".class") ||
+                        clss.classfile.getName().endsWith(".class)") ||
+                        clss.classfile.getName().endsWith(".class)]"));
+            } else {
+                return false;
+            }
+        }
+        return isElementFromByteCode(elt.getEnclosingElement(), elt);
+    }
+
+    /**
+     * Returns the field of the class
+     */
+    public static VariableElement findFieldInType(TypeElement type, String name) {
+        for (VariableElement field: ElementFilter.fieldsIn(type.getEnclosedElements())) {
+            if (field.getSimpleName().toString().equals(name)) {
+                return field;
+            }
+        }
+        return null;
+    }
+
+    public static Set<VariableElement> findFieldsInType(TypeElement type, Collection<String> names) {
+        Set<VariableElement> results = new HashSet<VariableElement>();
+        for (VariableElement field: ElementFilter.fieldsIn(type.getEnclosedElements())) {
+            if (names.contains(field.getSimpleName().toString())) {
+                results.add(field);
+            }
+        }
+        return results;
+    }
+
+    public static boolean isError(Element element) {
+        return element.getClass().getName().equals("com.sun.tools.javac.comp.Resolve$SymbolNotFoundError");
+    }
+
+    /**
+     * Does the given element need a receiver for accesses?
+     * For example, an access to a local variable does not require a receiver.
+     *
+     * @param element the element to test
+     * @return whether the element requires a receiver for accesses
+     */
+    public static boolean hasReceiver(Element element) {
+        return (element.getKind().isField() ||
+                element.getKind() == ElementKind.METHOD ||
+                element.getKind() == ElementKind.CONSTRUCTOR)
+                && !ElementUtils.isStatic(element);
+    }
+
+    /**
+     * Determine all type elements for the classes and interfaces referenced
+     * in the extends/implements clauses of the given type element.
+     * TODO: can we learn from the implementation of
+     * com.sun.tools.javac.model.JavacElements.getAllMembers(TypeElement)?
+     */
+    public static List<TypeElement> getSuperTypes(Elements elements, TypeElement type) {
+
+        List<TypeElement> superelems = new ArrayList<TypeElement>();
+        if (type == null) {
+            return superelems;
+        }
+
+        // Set up a stack containing type, which is our starting point.
+        Deque<TypeElement> stack = new ArrayDeque<TypeElement>();
+        stack.push(type);
+
+        while (!stack.isEmpty()) {
+            TypeElement current = stack.pop();
+
+            // For each direct supertype of the current type element, if it
+            // hasn't already been visited, push it onto the stack and
+            // add it to our superelems set.
+            TypeMirror supertypecls = current.getSuperclass();
+            if (supertypecls.getKind() != TypeKind.NONE) {
+                TypeElement supercls = (TypeElement) ((DeclaredType)supertypecls).asElement();
+                if (!superelems.contains(supercls)) {
+                    stack.push(supercls);
+                    superelems.add(supercls);
+                }
+            }
+            for (TypeMirror supertypeitf : current.getInterfaces()) {
+                TypeElement superitf = (TypeElement) ((DeclaredType)supertypeitf).asElement();
+                if (!superelems.contains(superitf)) {
+                    stack.push(superitf);
+                    superelems.add(superitf);
+                }
+            }
+        }
+
+        // Include java.lang.Object as implicit superclass for all classes and interfaces.
+        TypeElement jlobject = elements.getTypeElement("java.lang.Object");
+        if (!superelems.contains(jlobject)) {
+            superelems.add(jlobject);
+        }
+
+        return Collections.<TypeElement>unmodifiableList(superelems);
+    }
+
+    /**
+     * Return all fields declared in the given type or any superclass/interface.
+     * TODO: should this use javax.lang.model.util.Elements.getAllMembers(TypeElement)
+     * instead of our own getSuperTypes?
+     */
+    public static List<VariableElement> getAllFieldsIn(Elements elements, TypeElement type) {
+        List<VariableElement> fields = new ArrayList<VariableElement>();
+        fields.addAll(ElementFilter.fieldsIn(type.getEnclosedElements()));
+        List<TypeElement> alltypes = getSuperTypes(elements, type);
+        for (TypeElement atype : alltypes) {
+            fields.addAll(ElementFilter.fieldsIn(atype.getEnclosedElements()));
+        }
+        return Collections.<VariableElement>unmodifiableList(fields);
+    }
+
+    /**
+     * Return all methods declared in the given type or any superclass/interface.
+     * Note that no constructors will be returned.
+     * TODO: should this use javax.lang.model.util.Elements.getAllMembers(TypeElement)
+     * instead of our own getSuperTypes?
+     */
+    public static List<ExecutableElement> getAllMethodsIn(Elements elements, TypeElement type) {
+        List<ExecutableElement> meths = new ArrayList<ExecutableElement>();
+        meths.addAll(ElementFilter.methodsIn(type.getEnclosedElements()));
+
+        List<TypeElement> alltypes = getSuperTypes(elements, type);
+        for (TypeElement atype : alltypes) {
+            meths.addAll(ElementFilter.methodsIn(atype.getEnclosedElements()));
+        }
+        return Collections.<ExecutableElement>unmodifiableList(meths);
+    }
+
+    public static boolean isTypeDeclaration(Element elt) {
+        switch (elt.getKind()) {
+            // These tree kinds are always declarations.  Uses of the declared
+            // types have tree kind IDENTIFIER.
+            case ANNOTATION_TYPE:
+            case CLASS:
+            case ENUM:
+            case INTERFACE:
+            case TYPE_PARAMETER:
+                return true;
+
+            default:
+                return false;
+        }
+    }
+
+    /**
+     * Check that a method Element matches a signature.
+     *
+     * Note: Matching the receiver type must be done elsewhere as
+     * the Element receiver type is only populated when annotated.
+     *
+     * @param method the method Element
+     * @param methodName the name of the method
+     * @param parameters the formal parameters' Classes
+     * @return true if the method matches
+     */
+    public static boolean matchesElement(ExecutableElement method,
+            String methodName,
+            Class<?> ... parameters) {
+
+        if (!method.getSimpleName().toString().equals(methodName)) {
+            return false;
+        }
+
+        if (method.getParameters().size() != parameters.length) {
+            return false;
+        } else {
+            for (int i = 0; i < method.getParameters().size(); i++) {
+                if (!method.getParameters().get(i).asType().toString().equals(
+                        parameters[i].getName())) {
+
+                    return false;
+                }
+            }
+        }
+
+        return true;
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorHandler.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorHandler.java
new file mode 100644
index 0000000000..9e3c27a7b9
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorHandler.java
@@ -0,0 +1,18 @@
+package org.checkerframework.javacutil;
+
+/**
+ * An implementation of the ErrorHandler interface can be registered
+ * with the ErrorReporter class to change the default behavior on
+ * errors.
+ */
+public interface ErrorHandler {
+
+    /**
+     * Log an error message and abort processing.
+     *
+     * @param msg the error message to log
+     */
+    public void errorAbort(String msg);
+
+    public void errorAbort(String msg, Throwable cause);
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorReporter.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorReporter.java
new file mode 100644
index 0000000000..309f1bb4ee
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/ErrorReporter.java
@@ -0,0 +1,41 @@
+package org.checkerframework.javacutil;
+
+/**
+ * Handle errors detected in utility classes.  By default, the error reporter
+ * throws a RuntimeException, but clients of the utility library may register
+ * a handler to change the behavior.  For example, type checkers can direct
+ * errors to the org.checkerframework.framework.source.SourceChecker class.
+ */
+public class ErrorReporter {
+
+    protected static ErrorHandler handler = null;
+
+    /**
+     * Register a handler to customize error reporting.
+     */
+    public static void setHandler(ErrorHandler h) {
+        handler = h;
+    }
+
+    /**
+     * Log an error message and abort processing.
+     * Call this method instead of raising an exception.
+     *
+     * @param msg the error message to log
+     */
+    public static void errorAbort(String msg) {
+        if (handler != null) {
+            handler.errorAbort(msg);
+        } else {
+            throw new RuntimeException(msg, new Throwable());
+        }
+    }
+
+    public static void errorAbort(String msg, Throwable cause) {
+        if (handler != null) {
+            handler.errorAbort(msg, cause);
+        } else {
+            throw new RuntimeException(msg, cause);
+        }
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/InternalUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/InternalUtils.java
new file mode 100644
index 0000000000..dbff45169b
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/InternalUtils.java
@@ -0,0 +1,403 @@
+package org.checkerframework.javacutil;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.type.TypeVariable;
+import javax.lang.model.type.WildcardType;
+import javax.lang.model.util.Elements;
+
+import com.sun.source.tree.AnnotatedTypeTree;
+import com.sun.source.tree.AnnotationTree;
+import com.sun.source.tree.ArrayAccessTree;
+import com.sun.source.tree.AssignmentTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.MethodTree;
+import com.sun.source.tree.NewArrayTree;
+import com.sun.source.tree.NewClassTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.TypeParameterTree;
+import com.sun.source.util.TreePath;
+import com.sun.tools.javac.code.Flags;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.Symbol.TypeSymbol;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.Type.AnnotatedType;
+import com.sun.tools.javac.code.Types;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.tree.JCTree;
+import com.sun.tools.javac.tree.JCTree.JCAnnotatedType;
+import com.sun.tools.javac.tree.JCTree.JCAnnotation;
+import com.sun.tools.javac.tree.JCTree.JCExpressionStatement;
+import com.sun.tools.javac.tree.JCTree.JCMemberReference;
+import com.sun.tools.javac.tree.JCTree.JCMethodDecl;
+import com.sun.tools.javac.tree.JCTree.JCMethodInvocation;
+import com.sun.tools.javac.tree.JCTree.JCNewArray;
+import com.sun.tools.javac.tree.JCTree.JCNewClass;
+import com.sun.tools.javac.tree.JCTree.JCTypeParameter;
+import com.sun.tools.javac.tree.TreeInfo;
+import com.sun.tools.javac.util.Context;
+
+/*>>>
+ import org.checkerframework.checker.nullness.qual.*;
+ */
+
+/**
+ * Static utility methods used by annotation abstractions in this package. Some
+ * methods in this class depend on the use of Sun javac internals; any procedure
+ * in the Checker Framework that uses a non-public API should be placed here.
+ */
+public class InternalUtils {
+
+    // Class cannot be instantiated.
+    private InternalUtils() {
+        throw new AssertionError("Class InternalUtils cannot be instantiated.");
+    }
+
+    /**
+     * Gets the {@link Element} ("symbol") for the given Tree API node.
+     *
+     * @param tree the {@link Tree} node to get the symbol for
+     * @throws IllegalArgumentException
+     *         if {@code tree} is null or is not a valid javac-internal tree
+     *         (JCTree)
+     * @return the {@code {@link Symbol}} for the given tree, or null if one
+     *         could not be found
+     */
+    public static /*@Nullable*/ Element symbol(Tree tree) {
+        if (tree == null) {
+            ErrorReporter.errorAbort("InternalUtils.symbol: tree is null");
+            return null; // dead code
+        }
+
+        if (!(tree instanceof JCTree)) {
+            ErrorReporter.errorAbort("InternalUtils.symbol: tree is not a valid Javac tree");
+            return null; // dead code
+        }
+
+        if (TreeUtils.isExpressionTree(tree)) {
+            tree = TreeUtils.skipParens((ExpressionTree) tree);
+        }
+
+        switch (tree.getKind()) {
+            case VARIABLE:
+            case METHOD:
+            case CLASS:
+            case ENUM:
+            case INTERFACE:
+            case ANNOTATION_TYPE:
+            case TYPE_PARAMETER:
+                return TreeInfo.symbolFor((JCTree) tree);
+
+            // symbol() only works on MethodSelects, so we need to get it manually
+            // for method invocations.
+            case METHOD_INVOCATION:
+                return TreeInfo.symbol(((JCMethodInvocation) tree).getMethodSelect());
+
+            case ASSIGNMENT:
+                return TreeInfo.symbol((JCTree)((AssignmentTree)tree).getVariable());
+
+            case ARRAY_ACCESS:
+                return symbol(((ArrayAccessTree)tree).getExpression());
+
+            case NEW_CLASS:
+                return ((JCNewClass)tree).constructor;
+
+            case MEMBER_REFERENCE:
+                // TreeInfo.symbol, which is used in the default case, didn't handle
+                // member references until JDK8u20. So handle it here.
+                return ((JCMemberReference) tree).sym;
+
+            default:
+                return TreeInfo.symbol((JCTree) tree);
+        }
+    }
+
+    /**
+     * Determines whether or not the node referred to by the given
+     * {@link TreePath} is an anonymous constructor (the constructor for an
+     * anonymous class.
+     *
+     * @param method the {@link TreePath} for a node that may be an anonymous
+     *        constructor
+     * @return true if the given path points to an anonymous constructor, false
+     *         if it does not
+     */
+    public static boolean isAnonymousConstructor(final MethodTree method) {
+        /*@Nullable*/ Element e = InternalUtils.symbol(method);
+        if (e == null || !(e instanceof Symbol)) {
+            return false;
+        }
+
+        if ((((/*@NonNull*/ Symbol)e).flags() & Flags.ANONCONSTR) != 0) {
+            return true;
+        }
+
+        return false;
+    }
+
+    /**
+     * indicates whether it should return the constructor that gets invoked
+     * in cases of anonymous classes
+     */
+    private static final boolean RETURN_INVOKE_CONSTRUCTOR = true;
+
+    /**
+     * Determines the symbol for a constructor given an invocation via
+     * {@code new}.
+     *
+     * If the tree is a declaration of an anonymous class, then method returns
+     * constructor that gets invoked in the extended class, rather than the
+     * anonymous constructor implicitly added by the constructor (JLS 15.9.5.1)
+     *
+     * @param tree the constructor invocation
+     * @return the {@link ExecutableElement} corresponding to the constructor
+     *         call in {@code tree}
+     */
+    public static ExecutableElement constructor(NewClassTree tree) {
+
+        if (!(tree instanceof JCTree.JCNewClass)) {
+            ErrorReporter.errorAbort("InternalUtils.constructor: not a javac internal tree");
+            return null; // dead code
+        }
+
+        JCNewClass newClassTree = (JCNewClass) tree;
+
+        if (RETURN_INVOKE_CONSTRUCTOR && tree.getClassBody() != null) {
+            // anonymous constructor bodies should contain exactly one statement
+            // in the form:
+            //    super(arg1, ...)
+            // or
+            //    o.super(arg1, ...)
+            //
+            // which is a method invocation (!) to the actual constructor
+
+            // the method call is guaranteed to return nonnull
+            JCMethodDecl anonConstructor =
+                (JCMethodDecl) TreeInfo.declarationFor(newClassTree.constructor, newClassTree);
+            assert anonConstructor != null;
+            assert anonConstructor.body.stats.size() == 1;
+            JCExpressionStatement stmt = (JCExpressionStatement) anonConstructor.body.stats.head;
+            JCTree.JCMethodInvocation superInvok = (JCMethodInvocation) stmt.expr;
+            return (ExecutableElement) TreeInfo.symbol(superInvok.meth);
+        }
+
+        Element e = newClassTree.constructor;
+
+        assert e instanceof ExecutableElement;
+
+        return (ExecutableElement) e;
+    }
+
+    public final static List<AnnotationMirror> annotationsFromTypeAnnotationTrees(List<? extends AnnotationTree> annos) {
+        List<AnnotationMirror> annotations = new ArrayList<AnnotationMirror>(annos.size());
+        for (AnnotationTree anno : annos) {
+            annotations.add(((JCAnnotation)anno).attribute);
+        }
+        return annotations;
+    }
+
+    public final static List<? extends AnnotationMirror> annotationsFromTree(AnnotatedTypeTree node) {
+        return annotationsFromTypeAnnotationTrees(((JCAnnotatedType)node).annotations);
+    }
+
+    public final static List<? extends AnnotationMirror> annotationsFromTree(TypeParameterTree node) {
+        return annotationsFromTypeAnnotationTrees(((JCTypeParameter)node).annotations);
+    }
+
+    public final static List<? extends AnnotationMirror> annotationsFromArrayCreation(NewArrayTree node, int level) {
+
+        assert node instanceof JCNewArray;
+        final JCNewArray newArray = ((JCNewArray) node);
+
+        if (level == -1) {
+            return annotationsFromTypeAnnotationTrees(newArray.annotations);
+        }
+
+        if (newArray.dimAnnotations.length() > 0
+                && (level >= 0)
+                && (level < newArray.dimAnnotations.size()))
+            return annotationsFromTypeAnnotationTrees(newArray.dimAnnotations.get(level));
+
+        return Collections.emptyList();
+    }
+
+    public static TypeMirror typeOf(Tree tree) {
+        return ((JCTree) tree).type;
+    }
+
+    /**
+     * Returns whether a TypeVariable represents a captured type.
+     */
+    public static boolean isCaptured(TypeVariable typeVar) {
+        if (typeVar instanceof AnnotatedType) {
+            return ((Type.TypeVar) ((Type.AnnotatedType) typeVar).unannotatedType()).isCaptured();
+        }
+        return ((Type.TypeVar) typeVar).isCaptured();
+    }
+
+    /**
+     * Returns whether a TypeMirror represents a class type.
+     */
+    public static boolean isClassType(TypeMirror type) {
+        return (type instanceof Type.ClassType);
+    }
+
+    /**
+     * Returns the least upper bound of two {@link TypeMirror}s,
+     * ignoring any annotations on the types.
+     *
+     * Wrapper around Types.lub to add special handling for
+     * null types, primitives, and wildcards.
+     *
+     * @param processingEnv the {@link ProcessingEnvironment} to use.
+     * @param tm1 a {@link TypeMirror}.
+     * @param tm2 a {@link TypeMirror}.
+     * @return the least upper bound of {@code tm1} and {@code tm2}.
+     */
+    public static TypeMirror leastUpperBound(
+            ProcessingEnvironment processingEnv, TypeMirror tm1, TypeMirror tm2) {
+        Type t1 = ((Type) tm1).unannotatedType();
+        Type t2 = ((Type) tm2).unannotatedType();
+        JavacProcessingEnvironment javacEnv = (JavacProcessingEnvironment) processingEnv;
+        Types types = Types.instance(javacEnv.getContext());
+        if (types.isSameType(t1, t2)) {
+            // Special case if the two types are equal.
+            return t1;
+        }
+        // Handle the 'null' type manually (not done by types.lub).
+        if (t1.getKind() == TypeKind.NULL) {
+            return t2;
+        }
+        if (t2.getKind() == TypeKind.NULL) {
+            return t1;
+        }
+        // Special case for primitives.
+        if (TypesUtils.isPrimitive(t1) || TypesUtils.isPrimitive(t2)) {
+            if (types.isAssignable(t1, t2)) {
+                return t2;
+            } else if (types.isAssignable(t2, t1)) {
+                return t1;
+            } else {
+                return processingEnv.getTypeUtils().getNoType(TypeKind.NONE);
+            }
+        }
+        if (t1.getKind() == TypeKind.WILDCARD) {
+            WildcardType wc1 = (WildcardType) t1;
+            Type bound = (Type) wc1.getExtendsBound();
+            if (bound == null) {
+                // Implicit upper bound of java.lang.Object
+                Elements elements = processingEnv.getElementUtils();
+                return elements.getTypeElement("java.lang.Object").asType();
+            }
+            t1 = bound;
+        }
+        if (t2.getKind() == TypeKind.WILDCARD) {
+            WildcardType wc2 = (WildcardType) t2;
+            Type bound = (Type) wc2.getExtendsBound();
+            if (bound == null) {
+                // Implicit upper bound of java.lang.Object
+                Elements elements = processingEnv.getElementUtils();
+                return elements.getTypeElement("java.lang.Object").asType();
+            }
+            t2 = bound;
+        }
+        return types.lub(t1, t2);
+    }
+
+    /**
+     * Returns the greatest lower bound of two {@link TypeMirror}s,
+     * ignoring any annotations on the types.
+     *
+     * Wrapper around Types.glb to add special handling for
+     * null types, primitives, and wildcards.
+     *
+     *
+     * @param processingEnv the {@link ProcessingEnvironment} to use.
+     * @param tm1 a {@link TypeMirror}.
+     * @param tm2 a {@link TypeMirror}.
+     * @return the greatest lower bound of {@code tm1} and {@code tm2}.
+     */
+    public static TypeMirror greatestLowerBound(
+            ProcessingEnvironment processingEnv, TypeMirror tm1, TypeMirror tm2) {
+        Type t1 = ((Type) tm1).unannotatedType();
+        Type t2 = ((Type) tm2).unannotatedType();
+        JavacProcessingEnvironment javacEnv = (JavacProcessingEnvironment) processingEnv;
+        Types types = Types.instance(javacEnv.getContext());
+        if (types.isSameType(t1, t2)) {
+            // Special case if the two types are equal.
+            return t1;
+        }
+        // Handle the 'null' type manually.
+        if (t1.getKind() == TypeKind.NULL) {
+            return t1;
+        }
+        if (t2.getKind() == TypeKind.NULL) {
+            return t2;
+        }
+        // Special case for primitives.
+        if (TypesUtils.isPrimitive(t1) || TypesUtils.isPrimitive(t2)) {
+            if (types.isAssignable(t1, t2)) {
+                return t1;
+            } else if (types.isAssignable(t2, t1)) {
+                return t2;
+            } else {
+                // Javac types.glb returns TypeKind.Error when the GLB does
+                // not exist, but we can't create one.  Use TypeKind.NONE
+                // instead.
+                return processingEnv.getTypeUtils().getNoType(TypeKind.NONE);
+            }
+        }
+        if (t1.getKind() == TypeKind.WILDCARD) {
+            return t2;
+        }
+        if (t2.getKind() == TypeKind.WILDCARD) {
+            return t1;
+        }
+
+        // If neither type is a primitive type, null type, or wildcard
+        // and if the types are not the same, use javac types.glb
+        return types.glb(t1, t2);
+    }
+
+    /**
+     * Returns the return type of a method, where the "raw" return type of that
+     * method is given (i.e., the return type might still contain unsubstituted
+     * type variables), given the receiver of the method call.
+     */
+    public static TypeMirror substituteMethodReturnType(TypeMirror methodType,
+            TypeMirror substitutedReceiverType) {
+        if (methodType.getKind() != TypeKind.TYPEVAR) {
+            return methodType;
+        }
+        // TODO: find a nicer way to substitute type variables
+        String t = methodType.toString();
+        Type finalReceiverType = (Type) substitutedReceiverType;
+        int i = 0;
+        for (TypeSymbol typeParam : finalReceiverType.tsym.getTypeParameters()) {
+            if (t.equals(typeParam.toString())) {
+                return finalReceiverType.getTypeArguments().get(i);
+            }
+            i++;
+        }
+        assert false;
+        return null;
+    }
+
+    /** Helper function to extract the javac Context from the
+     * javac processing environment.
+     *
+     * @param env the processing environment
+     * @return the javac Context
+     */
+    public static Context getJavacContext(ProcessingEnvironment env) {
+        return ((JavacProcessingEnvironment)env).getContext();
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Pair.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Pair.java
new file mode 100644
index 0000000000..0d8a862f08
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Pair.java
@@ -0,0 +1,69 @@
+package org.checkerframework.javacutil;
+
+/*>>>
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+*/
+
+/**
+ * Simple pair class for multiple returns.
+ *
+ * TODO: as class is immutable, use @Covariant annotation.
+ */
+public class Pair<V1, V2> {
+    public final V1 first;
+    public final V2 second;
+
+    private Pair(V1 v1, V2 v2) {
+        this.first = v1;
+        this.second = v2;
+    }
+
+    public static <V1, V2> Pair<V1, V2> of(V1 v1, V2 v2) {
+        return new Pair<V1, V2>(v1, v2);
+    }
+
+    /*@SideEffectFree*/
+    @Override
+    public String toString() {
+        return "Pair(" + first + ", " + second + ")";
+    }
+
+    private int hashCode = -1;
+
+    /*@Pure*/
+    @Override
+    public int hashCode() {
+        if (hashCode == -1) {
+            hashCode = 31;
+            if (first != null) {
+                hashCode += 17 * first.hashCode();
+            }
+            if (second != null) {
+                hashCode += 17 * second.hashCode();
+            }
+        }
+        return hashCode;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (!(o instanceof Pair)) {
+            return false;
+        }
+        @SuppressWarnings("unchecked")
+        Pair<V1, V2> other = (Pair<V1, V2>) o;
+        if (this.first == null) {
+            if (other.first != null) return false;
+        } else {
+            if (!this.first.equals(other.first)) return false;
+        }
+        if (this.second == null) {
+            if (other.second != null) return false;
+        } else {
+            if (!this.second.equals(other.second)) return false;
+        }
+
+        return true;
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Resolver.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Resolver.java
new file mode 100644
index 0000000000..45d959fe02
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/Resolver.java
@@ -0,0 +1,381 @@
+package org.checkerframework.javacutil;
+
+import static com.sun.tools.javac.code.Kinds.PCK;
+import static com.sun.tools.javac.code.Kinds.TYP;
+import static com.sun.tools.javac.code.Kinds.VAR;
+
+import java.lang.reflect.Constructor;
+import java.lang.reflect.Field;
+import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.type.TypeMirror;
+
+import com.sun.source.util.TreePath;
+import com.sun.source.util.Trees;
+import com.sun.tools.javac.api.JavacScope;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.Symbol.ClassSymbol;
+import com.sun.tools.javac.code.Symbol.PackageSymbol;
+import com.sun.tools.javac.code.Symbol.TypeSymbol;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.comp.AttrContext;
+import com.sun.tools.javac.comp.DeferredAttr;
+import com.sun.tools.javac.comp.Env;
+import com.sun.tools.javac.comp.Resolve;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.List;
+import com.sun.tools.javac.util.Log;
+import com.sun.tools.javac.util.Name;
+import com.sun.tools.javac.util.Names;
+
+/**
+ * A Utility class to find symbols corresponding to string references.
+ */
+public class Resolver {
+    private final Resolve resolve;
+    private final Names names;
+    private final Trees trees;
+    private final Log log;
+
+    private static final Method FIND_METHOD;
+    private static final Method FIND_VAR;
+    private static final Method FIND_IDENT;
+    private static final Method FIND_IDENT_IN_TYPE;
+    private static final Method FIND_IDENT_IN_PACKAGE;
+    private static final Method FIND_TYPE;
+
+    private static final Class<?> ACCESSERROR;
+    // Note that currently access(...) is defined in InvalidSymbolError, a superclass of AccessError
+    private static final Method ACCESSERROR_ACCESS;
+
+    static {
+        try {
+            FIND_METHOD = Resolve.class.getDeclaredMethod("findMethod",
+                    Env.class, Type.class, Name.class, List.class, List.class,
+                    boolean.class, boolean.class, boolean.class);
+            FIND_METHOD.setAccessible(true);
+
+            FIND_VAR = Resolve.class.getDeclaredMethod("findVar",
+                    Env.class, Name.class);
+            FIND_VAR.setAccessible(true);
+
+            FIND_IDENT = Resolve.class.getDeclaredMethod(
+                    "findIdent", Env.class, Name.class, int.class);
+            FIND_IDENT.setAccessible(true);
+
+            FIND_IDENT_IN_TYPE = Resolve.class.getDeclaredMethod(
+                    "findIdentInType", Env.class, Type.class, Name.class,
+                    int.class);
+            FIND_IDENT_IN_TYPE.setAccessible(true);
+
+            FIND_IDENT_IN_PACKAGE = Resolve.class.getDeclaredMethod(
+                    "findIdentInPackage", Env.class, TypeSymbol.class, Name.class,
+                    int.class);
+            FIND_IDENT_IN_PACKAGE.setAccessible(true);
+
+            FIND_TYPE = Resolve.class.getDeclaredMethod(
+                    "findType", Env.class, Name.class);
+            FIND_TYPE.setAccessible(true);
+        } catch (Exception e) {
+            Error err = new AssertionError(
+                    "Compiler 'Resolve' class doesn't contain required 'find' method");
+            err.initCause(e);
+            throw err;
+        }
+
+        try {
+            ACCESSERROR = Class.forName("com.sun.tools.javac.comp.Resolve$AccessError");
+            ACCESSERROR_ACCESS = ACCESSERROR.getMethod("access", Name.class, TypeSymbol.class);
+            ACCESSERROR_ACCESS.setAccessible(true);
+        } catch (ClassNotFoundException e) {
+            ErrorReporter.errorAbort("Compiler 'Resolve$AccessError' class could not be retrieved.", e);
+            // Unreachable code - needed so the compiler does not warn about a possibly uninitialized final field.
+            throw new AssertionError();
+        } catch (NoSuchMethodException e) {
+            ErrorReporter.errorAbort("Compiler 'Resolve$AccessError' class doesn't contain required 'access' method", e);
+            // Unreachable code - needed so the compiler does not warn about a possibly uninitialized final field.
+            throw new AssertionError();
+        }
+    }
+
+    public Resolver(ProcessingEnvironment env) {
+        Context context = ((JavacProcessingEnvironment) env).getContext();
+        this.resolve = Resolve.instance(context);
+        this.names = Names.instance(context);
+        this.trees = Trees.instance(env);
+        this.log = Log.instance(context);
+    }
+
+    /**
+     * Finds the package with name {@code name}.
+     *
+     * @param name
+     *            The name of the package.
+     * @param path
+     *            The tree path to the local scope.
+     * @return the {@code PackageSymbol} for the package if it is found,
+     * {@code null} otherwise
+     */
+    public PackageSymbol findPackage(String name, TreePath path) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+            Element res = wrapInvocationOnResolveInstance(FIND_IDENT, env,
+                    names.fromString(name), PCK);
+            // findIdent will return a PackageSymbol even for a symbol that is not a package,
+            // such as a.b.c.MyClass.myStaticField. "exists()" must be called on it to ensure
+            // that it exists.
+            if (res.getKind() == ElementKind.PACKAGE) {
+                PackageSymbol ps = (PackageSymbol) res;
+                return ps.exists() ? ps : null;
+            } else {
+                return null;
+            }
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Finds the field with name {@code name} in a given type.
+     *
+     * <p>
+     * The method adheres to all the rules of Java's scoping (while also
+     * considering the imports) for name resolution.
+     *
+     * @param name
+     *            The name of the field.
+     * @param type
+     *            The type of the receiver (i.e., the type in which to look for
+     *            the field).
+     * @param path
+     *            The tree path to the local scope.
+     * @return the element for the field
+     */
+    public VariableElement findField(String name, TypeMirror type, TreePath path) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+            Element res = wrapInvocationOnResolveInstance(FIND_IDENT_IN_TYPE, env, type,
+                    names.fromString(name), VAR);
+            if (res.getKind() == ElementKind.FIELD) {
+                return (VariableElement) res;
+            } else if (res.getKind() == ElementKind.OTHER && ACCESSERROR.isInstance(res)) {
+                // Return the inaccessible field that was found
+                return (VariableElement) wrapInvocation(res, ACCESSERROR_ACCESS, null, null);
+            } else {
+                // Most likely didn't find the field and the Element is a SymbolNotFoundError
+                return null;
+            }
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Finds the local variable with name {@code name} in the given scope.
+     *
+     * @param name
+     *            The name of the local variable.
+     * @param path
+     *            The tree path to the local scope.
+     * @return the element for the local variable
+     */
+    public VariableElement findLocalVariableOrParameter(String name, TreePath path) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+            Element res = wrapInvocationOnResolveInstance(FIND_VAR, env,
+                    names.fromString(name));
+            if (res.getKind() == ElementKind.LOCAL_VARIABLE
+             || res.getKind() == ElementKind.PARAMETER) {
+                return (VariableElement) res;
+            } else {
+                // Most likely didn't find the variable and the Element is a SymbolNotFoundError
+                return null;
+            }
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Finds the class literal with name {@code name}.
+     *
+     * <p>
+     * The method adheres to all the rules of Java's scoping (while also
+     * considering the imports) for name resolution.
+     *
+     * @param name
+     *            The name of the class.
+     * @param path
+     *            The tree path to the local scope.
+     * @return the element for the class
+     */
+    public Element findClass(String name, TreePath path) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+            return wrapInvocationOnResolveInstance(FIND_TYPE, env, names.fromString(name));
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Finds the class with name {@code name} in a given package.
+     *
+     * @param name
+     *            The name of the class.
+     * @param pck
+     *            The PackageSymbol for the package.
+     * @param path
+     *            The tree path to the local scope.
+     * @return the {@code ClassSymbol} for the class if it is found,
+     * {@code null} otherwise
+     */
+    public ClassSymbol findClassInPackage(String name, PackageSymbol pck, TreePath path) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+            Element res = wrapInvocationOnResolveInstance(FIND_IDENT_IN_PACKAGE, env, pck,
+                    names.fromString(name), TYP);
+            if (res.getKind() == ElementKind.CLASS) {
+                return (ClassSymbol) res;
+            } else {
+                return null;
+            }
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Finds the method element for a given name and list of expected parameter
+     * types.
+     *
+     * <p>
+     * The method adheres to all the rules of Java's scoping (while also
+     * considering the imports) for name resolution.
+     *
+     * @param methodName
+     *            Name of the method to find.
+     * @param receiverType
+     *            Type of the receiver of the method
+     * @param path
+     *            Tree path.
+     * @return the method element (if found)
+     */
+    public Element findMethod(String methodName, TypeMirror receiverType,
+            TreePath path, java.util.List<TypeMirror> argumentTypes) {
+        Log.DiagnosticHandler discardDiagnosticHandler =
+            new Log.DiscardDiagnosticHandler(log);
+        try {
+            JavacScope scope = (JavacScope) trees.getScope(path);
+            Env<AttrContext> env = scope.getEnv();
+
+            Type site = (Type) receiverType;
+            Name name = names.fromString(methodName);
+            List<Type> argtypes = List.nil();
+            for (TypeMirror a : argumentTypes) {
+                argtypes = argtypes.append((Type) a);
+            }
+            List<Type> typeargtypes = List.nil();
+            boolean allowBoxing = true;
+            boolean useVarargs = false;
+            boolean operator = true;
+
+            try {
+                // For some reason we have to set our own method context, which is rather ugly.
+                // TODO: find a nicer way to do this.
+                Object methodContext = buildMethodContext();
+                Object oldContext = getField(resolve, "currentResolutionContext");
+                setField(resolve, "currentResolutionContext", methodContext);
+                Element result = wrapInvocationOnResolveInstance(FIND_METHOD, env, site, name, argtypes,
+                    typeargtypes, allowBoxing, useVarargs, operator);
+                setField(resolve, "currentResolutionContext", oldContext);
+                return result;
+            } catch (Throwable t) {
+                Error err = new AssertionError("Unexpected Reflection error");
+                err.initCause(t);
+                throw err;
+            }
+        } finally {
+            log.popDiagnosticHandler(discardDiagnosticHandler);
+        }
+    }
+
+    /**
+     * Build an instance of {@code Resolve$MethodResolutionContext}.
+     */
+    protected Object buildMethodContext() throws ClassNotFoundException,
+            InstantiationException, IllegalAccessException,
+            InvocationTargetException, NoSuchFieldException {
+        // Class is not accessible, instantiate reflectively.
+        Class<?> methCtxClss = Class.forName("com.sun.tools.javac.comp.Resolve$MethodResolutionContext");
+        Constructor<?> constructor = methCtxClss.getDeclaredConstructors()[0];
+        constructor.setAccessible(true);
+        Object methodContext = constructor.newInstance(resolve);
+        // we need to also initialize the fields attrMode and step
+        setField(methodContext, "attrMode", DeferredAttr.AttrMode.CHECK);
+        @SuppressWarnings("rawtypes")
+        List<?> phases = (List) getField(resolve, "methodResolutionSteps");
+        setField(methodContext, "step", phases.get(1));
+        return methodContext;
+    }
+
+    /** Reflectively set a field. */
+    private void setField(Object receiver, String fieldName,
+            Object value) throws NoSuchFieldException,
+            IllegalAccessException {
+        Field f = receiver.getClass().getDeclaredField(fieldName);
+        f.setAccessible(true);
+        f.set(receiver, value);
+    }
+
+    /** Reflectively get the value of a field. */
+    private Object getField(Object receiver, String fieldName) throws NoSuchFieldException,
+            IllegalAccessException {
+        Field f = receiver.getClass().getDeclaredField(fieldName);
+        f.setAccessible(true);
+        return f.get(receiver);
+    }
+
+    private Symbol wrapInvocationOnResolveInstance(Method method, Object... args) {
+        return wrapInvocation(resolve, method, args);
+    }
+
+    private Symbol wrapInvocation(Object receiver, Method method, Object... args) {
+        try {
+            return (Symbol) method.invoke(receiver, args);
+        } catch (IllegalAccessException e) {
+            Error err = new AssertionError("Unexpected Reflection error");
+            err.initCause(e);
+            throw err;
+        } catch (IllegalArgumentException e) {
+            Error err = new AssertionError("Unexpected Reflection error");
+            err.initCause(e);
+            throw err;
+        } catch (InvocationTargetException e) {
+            Error err = new AssertionError("Unexpected Reflection error");
+            err.initCause(e);
+            throw err;
+        }
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TreeUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TreeUtils.java
new file mode 100644
index 0000000000..5ceb5450dd
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TreeUtils.java
@@ -0,0 +1,967 @@
+package org.checkerframework.javacutil;
+
+/*>>>
+import org.checkerframework.checker.nullness.qual.*;
+*/
+
+import java.util.EnumSet;
+import java.util.Set;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.util.ElementFilter;
+
+import com.sun.source.tree.AnnotatedTypeTree;
+import com.sun.source.tree.ArrayAccessTree;
+import com.sun.source.tree.BinaryTree;
+import com.sun.source.tree.BlockTree;
+import com.sun.source.tree.ClassTree;
+import com.sun.source.tree.CompoundAssignmentTree;
+import com.sun.source.tree.ExpressionStatementTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.IdentifierTree;
+import com.sun.source.tree.LiteralTree;
+import com.sun.source.tree.MemberSelectTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.MethodTree;
+import com.sun.source.tree.NewClassTree;
+import com.sun.source.tree.ParameterizedTypeTree;
+import com.sun.source.tree.ParenthesizedTree;
+import com.sun.source.tree.PrimitiveTypeTree;
+import com.sun.source.tree.StatementTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.TypeCastTree;
+import com.sun.source.tree.VariableTree;
+import com.sun.source.util.TreePath;
+import com.sun.source.util.Trees;
+import com.sun.tools.javac.code.Flags;
+import com.sun.tools.javac.code.Symbol.MethodSymbol;
+import com.sun.tools.javac.tree.JCTree;
+
+/**
+ * A utility class made for helping to analyze a given {@code Tree}.
+ */
+// TODO: This class needs significant restructuring
+public final class TreeUtils {
+
+    // Class cannot be instantiated.
+    private TreeUtils() { throw new AssertionError("Class TreeUtils cannot be instantiated."); }
+
+    /**
+     * Checks if the provided method is a constructor method or no.
+     *
+     * @param tree
+     *            a tree defining the method
+     * @return true iff tree describes a constructor
+     */
+    public static boolean isConstructor(final MethodTree tree) {
+        return tree.getName().contentEquals("<init>");
+    }
+
+    /**
+     * Checks if the method invocation is a call to super.
+     *
+     * @param tree
+     *            a tree defining a method invocation
+     *
+     * @return true iff tree describes a call to super
+     */
+    public static boolean isSuperCall(MethodInvocationTree tree) {
+        return isNamedMethodCall("super", tree);
+    }
+
+    /**
+     * Checks if the method invocation is a call to this.
+     *
+     * @param tree
+     *            a tree defining a method invocation
+     *
+     * @return true iff tree describes a call to this
+     */
+    public static boolean isThisCall(MethodInvocationTree tree) {
+        return isNamedMethodCall("this", tree);
+
+    }
+
+    protected static boolean isNamedMethodCall(String name, MethodInvocationTree tree) {
+        /*@Nullable*/ ExpressionTree mst = tree.getMethodSelect();
+        assert mst != null; /*nninvariant*/
+
+        if (mst.getKind() == Tree.Kind.IDENTIFIER ) {
+            return ((IdentifierTree)mst).getName().contentEquals(name);
+        }
+
+        if (mst.getKind() == Tree.Kind.MEMBER_SELECT) {
+            MemberSelectTree selectTree = (MemberSelectTree)mst;
+
+            if (selectTree.getExpression().getKind() != Tree.Kind.IDENTIFIER) {
+                return false;
+            }
+
+            return ((IdentifierTree) selectTree.getExpression()).getName()
+                    .contentEquals(name);
+        }
+
+        return false;
+    }
+
+    /**
+     * Returns true if the tree is a tree that 'looks like' either an access
+     * of a field or an invocation of a method that are owned by the same
+     * accessing instance.
+     *
+     * It would only return true if the access tree is of the form:
+     * <pre>
+     *   field
+     *   this.field
+     *
+     *   method()
+     *   this.method()
+     * </pre>
+     *
+     * It does not perform any semantical check to differentiate between
+     * fields and local variables; local methods or imported static methods.
+     *
+     * @param tree  expression tree representing an access to object member
+     * @return {@code true} iff the member is a member of {@code this} instance
+     */
+    public static boolean isSelfAccess(final ExpressionTree tree) {
+        ExpressionTree tr = TreeUtils.skipParens(tree);
+        // If method invocation check the method select
+        if (tr.getKind() == Tree.Kind.ARRAY_ACCESS) {
+            return false;
+        }
+
+        if (tree.getKind() == Tree.Kind.METHOD_INVOCATION) {
+            tr = ((MethodInvocationTree)tree).getMethodSelect();
+        }
+        tr = TreeUtils.skipParens(tr);
+        if (tr.getKind() == Tree.Kind.TYPE_CAST) {
+            tr = ((TypeCastTree)tr).getExpression();
+        }
+        tr = TreeUtils.skipParens(tr);
+
+        if (tr.getKind() == Tree.Kind.IDENTIFIER) {
+            return true;
+        }
+
+        if (tr.getKind() == Tree.Kind.MEMBER_SELECT) {
+            tr = ((MemberSelectTree)tr).getExpression();
+            if (tr.getKind() == Tree.Kind.IDENTIFIER) {
+                Name ident = ((IdentifierTree)tr).getName();
+                return ident.contentEquals("this") ||
+                        ident.contentEquals("super");
+            }
+        }
+
+        return false;
+    }
+
+    /**
+     * Gets the first enclosing tree in path, of the specified kind.
+     *
+     * @param path  the path defining the tree node
+     * @param kind  the kind of the desired tree
+     * @return the enclosing tree of the given type as given by the path
+     */
+    public static Tree enclosingOfKind(final TreePath path, final Tree.Kind kind) {
+        return enclosingOfKind(path, EnumSet.of(kind));
+    }
+
+    /**
+     * Gets the first enclosing tree in path, with any one of the specified kinds.
+     *
+     * @param path  the path defining the tree node
+     * @param kinds  the set of kinds of the desired tree
+     * @return the enclosing tree of the given type as given by the path
+     */
+    public static Tree enclosingOfKind(final TreePath path, final Set<Tree.Kind> kinds) {
+        TreePath p = path;
+
+        while (p != null) {
+            Tree leaf = p.getLeaf();
+            assert leaf != null; /*nninvariant*/
+            if (kinds.contains(leaf.getKind())) {
+                return leaf;
+            }
+            p = p.getParentPath();
+        }
+
+        return null;
+    }
+
+    /**
+     * Gets path to the first enclosing class tree, where class is
+     * defined by the classTreeKinds method.
+     *
+     * @param path  the path defining the tree node
+     * @return the path to the enclosing class tree
+     */
+    public static TreePath pathTillClass(final TreePath path) {
+        return pathTillOfKind(path, classTreeKinds());
+    }
+
+    /**
+     * Gets path to the first enclosing tree of the specified kind.
+     *
+     * @param path  the path defining the tree node
+     * @param kind  the kind of the desired tree
+     * @return the path to the enclosing tree of the given type
+     */
+    public static TreePath pathTillOfKind(final TreePath path, final Tree.Kind kind) {
+        return pathTillOfKind(path, EnumSet.of(kind));
+    }
+
+    /**
+     * Gets path to the first enclosing tree with any one of the specified kinds.
+     *
+     * @param path  the path defining the tree node
+     * @param kinds  the set of kinds of the desired tree
+     * @return the path to the enclosing tree of the given type
+     */
+    public static TreePath pathTillOfKind(final TreePath path, final Set<Tree.Kind> kinds) {
+        TreePath p = path;
+
+        while (p != null) {
+            Tree leaf = p.getLeaf();
+            assert leaf != null; /*nninvariant*/
+            if (kinds.contains(leaf.getKind())) {
+                return p;
+            }
+            p = p.getParentPath();
+        }
+
+        return null;
+    }
+
+    /**
+     * Gets the first enclosing tree in path, of the specified class
+     *
+     * @param path  the path defining the tree node
+     * @param treeClass the class of the desired tree
+     * @return the enclosing tree of the given type as given by the path
+     */
+    public static <T extends Tree> T enclosingOfClass(final TreePath path, final Class<T> treeClass) {
+        TreePath p = path;
+
+        while (p != null) {
+            Tree leaf = p.getLeaf();
+            if (treeClass.isInstance(leaf)) {
+                return treeClass.cast(leaf);
+            }
+            p = p.getParentPath();
+        }
+
+        return null;
+    }
+
+    /**
+     * Gets the enclosing class of the tree node defined by the given
+     * {@code {@link TreePath}}. It returns a {@link Tree}, from which
+     * {@code checkers.types.AnnotatedTypeMirror} or {@link Element} can be
+     * obtained.
+     *
+     * @param path the path defining the tree node
+     * @return the enclosing class (or interface) as given by the path, or null
+     *         if one does not exist
+     */
+    public static /*@Nullable*/ ClassTree enclosingClass(final /*@Nullable*/ TreePath path) {
+        return (ClassTree) enclosingOfKind(path, classTreeKinds());
+    }
+
+    /**
+     * Gets the enclosing variable of a tree node defined by the given
+     * {@link TreePath}.
+     *
+     * @param path the path defining the tree node
+     * @return the enclosing variable as given by the path, or null if one does not exist
+     */
+    public static VariableTree enclosingVariable(final TreePath path) {
+        return (VariableTree) enclosingOfKind(path, Tree.Kind.VARIABLE);
+    }
+
+    /**
+     * Gets the enclosing method of the tree node defined by the given
+     * {@code {@link TreePath}}. It returns a {@link Tree}, from which an
+     * {@code checkers.types.AnnotatedTypeMirror} or {@link Element} can be
+     * obtained.
+     *
+     * @param path the path defining the tree node
+     * @return the enclosing method as given by the path, or null if one does
+     *         not exist
+     */
+    public static /*@Nullable*/ MethodTree enclosingMethod(final /*@Nullable*/ TreePath path) {
+        return (MethodTree) enclosingOfKind(path, Tree.Kind.METHOD);
+    }
+
+    public static /*@Nullable*/ BlockTree enclosingTopLevelBlock(TreePath path) {
+        TreePath parpath = path.getParentPath();
+        while (parpath!=null && parpath.getLeaf().getKind() != Tree.Kind.CLASS) {
+            path = parpath;
+            parpath = parpath.getParentPath();
+        }
+        if (path.getLeaf().getKind() == Tree.Kind.BLOCK) {
+            return (BlockTree) path.getLeaf();
+        }
+        return null;
+    }
+
+
+    /**
+     * If the given tree is a parenthesized tree, it returns the enclosed
+     * non-parenthesized tree. Otherwise, it returns the same tree.
+     *
+     * @param tree  an expression tree
+     * @return  the outermost non-parenthesized tree enclosed by the given tree
+     */
+    public static ExpressionTree skipParens(final ExpressionTree tree) {
+        ExpressionTree t = tree;
+        while (t.getKind() == Tree.Kind.PARENTHESIZED)
+            t = ((ParenthesizedTree)t).getExpression();
+        return t;
+    }
+
+    /**
+     * Returns the tree with the assignment context for the treePath
+     * leaf node.  (Does not handle pseudo-assignment of an argument to
+     * a parameter or a receiver expression to a receiver.)
+     *
+     * The assignment context for the {@code treePath} is the leaf of its parent,
+     * if the leaf is one of the following trees:
+     * <ul>
+     *   <li>AssignmentTree </li>
+     *   <li>CompoundAssignmentTree </li>
+     *   <li>MethodInvocationTree</li>
+     *   <li>NewArrayTree</li>
+     *   <li>NewClassTree</li>
+     *   <li>ReturnTree</li>
+     *   <li>VariableTree</li>
+     * </ul>
+     *
+     * If the leaf is a ConditionalExpressionTree or ParenthesizedTree, then recur on the leaf.
+     *
+     * Otherwise, null is returned.
+     *
+     * @return  the assignment context as described
+     */
+    public static Tree getAssignmentContext(final TreePath treePath) {
+        TreePath parentPath = treePath.getParentPath();
+
+        if (parentPath == null) {
+            return null;
+        }
+
+        Tree parent = parentPath.getLeaf();
+        switch (parent.getKind()) {
+        case PARENTHESIZED:
+        case CONDITIONAL_EXPRESSION:
+            return getAssignmentContext(parentPath);
+        case ASSIGNMENT:
+        case METHOD_INVOCATION:
+        case NEW_ARRAY:
+        case NEW_CLASS:
+        case RETURN:
+        case VARIABLE:
+            return parent;
+        default:
+            // 11 Tree.Kinds are CompoundAssignmentTrees,
+            // so use instanceof rather than listing all 11.
+            if (parent instanceof CompoundAssignmentTree) {
+                return parent;
+            }
+            return null;
+        }
+    }
+
+    /**
+     * Gets the element for a class corresponding to a declaration.
+     *
+     * @return the element for the given class
+     */
+    public static final TypeElement elementFromDeclaration(ClassTree node) {
+        TypeElement elt = (TypeElement) InternalUtils.symbol(node);
+        return elt;
+    }
+
+    /**
+     * Gets the element for a method corresponding to a declaration.
+     *
+     * @return the element for the given method
+     */
+    public static final ExecutableElement elementFromDeclaration(MethodTree node) {
+        ExecutableElement elt = (ExecutableElement) InternalUtils.symbol(node);
+        return elt;
+    }
+
+    /**
+     * Gets the element for a variable corresponding to its declaration.
+     *
+     * @return the element for the given variable
+     */
+    public static final VariableElement elementFromDeclaration(VariableTree node) {
+        VariableElement elt = (VariableElement) InternalUtils.symbol(node);
+        return elt;
+    }
+
+    /**
+     * Gets the element for the declaration corresponding to this use of an element.
+     * To get the element for a declaration, use {@link
+     * Trees#getElement(TreePath)} instead.
+     *
+     * TODO: remove this method, as it really doesn't do anything.
+     *
+     * @param node the tree corresponding to a use of an element
+     * @return the element for the corresponding declaration
+     */
+    public static final Element elementFromUse(ExpressionTree node) {
+        return InternalUtils.symbol(node);
+    }
+
+    // Specialization for return type.
+    public static final ExecutableElement elementFromUse(MethodInvocationTree node) {
+        return (ExecutableElement) elementFromUse((ExpressionTree) node);
+    }
+
+    // Specialization for return type.
+    public static final ExecutableElement elementFromUse(NewClassTree node) {
+        return (ExecutableElement) elementFromUse((ExpressionTree) node);
+    }
+
+
+    /**
+     * Determine whether the given ExpressionTree has an underlying element.
+     *
+     * @param node the ExpressionTree to test
+     * @return whether the tree refers to an identifier, member select, or method invocation
+     */
+    public static final boolean isUseOfElement(ExpressionTree node) {
+        node = TreeUtils.skipParens(node);
+        switch (node.getKind()) {
+            case IDENTIFIER:
+            case MEMBER_SELECT:
+            case METHOD_INVOCATION:
+            case NEW_CLASS:
+                return true;
+            default:
+                return false;
+        }
+    }
+
+    /**
+     * @return the name of the invoked method
+     */
+    public static final Name methodName(MethodInvocationTree node) {
+        ExpressionTree expr = node.getMethodSelect();
+        if (expr.getKind() == Tree.Kind.IDENTIFIER) {
+            return ((IdentifierTree)expr).getName();
+        } else if (expr.getKind() == Tree.Kind.MEMBER_SELECT) {
+            return ((MemberSelectTree)expr).getIdentifier();
+        }
+        ErrorReporter.errorAbort("TreeUtils.methodName: cannot be here: " + node);
+        return null; // dead code
+    }
+
+    /**
+     * @return true if the first statement in the body is a self constructor
+     *  invocation within a constructor
+     */
+    public static final boolean containsThisConstructorInvocation(MethodTree node) {
+        if (!TreeUtils.isConstructor(node)
+                || node.getBody().getStatements().isEmpty())
+            return false;
+
+        StatementTree st = node.getBody().getStatements().get(0);
+        if (!(st instanceof ExpressionStatementTree)
+                || !(((ExpressionStatementTree)st).getExpression() instanceof MethodInvocationTree))
+            return false;
+
+        MethodInvocationTree invocation = (MethodInvocationTree)
+            ((ExpressionStatementTree)st).getExpression();
+
+        return "this".contentEquals(TreeUtils.methodName(invocation));
+    }
+
+    public static final Tree firstStatement(Tree tree) {
+        Tree first;
+        if (tree.getKind() == Tree.Kind.BLOCK) {
+            BlockTree block = (BlockTree)tree;
+            if (block.getStatements().isEmpty()) {
+                first = block;
+            } else {
+                first = block.getStatements().iterator().next();
+            }
+        } else {
+            first = tree;
+        }
+        return first;
+    }
+
+    /**
+     * Determine whether the given class contains an explicit constructor.
+     *
+     * @param node a class tree
+     * @return true, iff there is an explicit constructor
+     */
+    public static boolean hasExplicitConstructor(ClassTree node) {
+        TypeElement elem = TreeUtils.elementFromDeclaration(node);
+
+        for ( ExecutableElement ee : ElementFilter.constructorsIn(elem.getEnclosedElements())) {
+            MethodSymbol ms = (MethodSymbol) ee;
+            long mod = ms.flags();
+
+            if ((mod & Flags.SYNTHETIC) == 0) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * Returns true if the tree is of a diamond type.
+     * In contrast to the implementation in TreeInfo, this version
+     * works on Trees.
+     *
+     * @see com.sun.tools.javac.tree.TreeInfo#isDiamond(JCTree)
+     */
+    public static final boolean isDiamondTree(Tree tree) {
+        switch (tree.getKind()) {
+        case ANNOTATED_TYPE: return isDiamondTree(((AnnotatedTypeTree)tree).getUnderlyingType());
+        case PARAMETERIZED_TYPE: return ((ParameterizedTypeTree)tree).getTypeArguments().isEmpty();
+        case NEW_CLASS: return isDiamondTree(((NewClassTree)tree).getIdentifier());
+        default: return false;
+        }
+    }
+
+    /**
+     * Returns true if the tree represents a {@code String} concatenation
+     * operation
+     */
+    public static final boolean isStringConcatenation(Tree tree) {
+        return (tree.getKind() == Tree.Kind.PLUS
+                && TypesUtils.isString(InternalUtils.typeOf(tree)));
+    }
+
+    /**
+     * Returns true if the compound assignment tree is a string concatenation
+     */
+    public static final boolean isStringCompoundConcatenation(CompoundAssignmentTree tree) {
+        return (tree.getKind() == Tree.Kind.PLUS_ASSIGNMENT
+                && TypesUtils.isString(InternalUtils.typeOf(tree)));
+    }
+
+    /**
+     * Returns true if the node is a constant-time expression.
+     *
+     * A tree is a constant-time expression if it is:
+     * <ol>
+     * <li>a literal tree
+     * <li>a reference to a final variable initialized with a compile time
+     *  constant
+     * <li>a String concatenation of two compile time constants
+     * </ol>
+     */
+    public static boolean isCompileTimeString(ExpressionTree node) {
+        ExpressionTree tree = TreeUtils.skipParens(node);
+        if (tree instanceof LiteralTree) {
+            return true;
+        }
+
+        if (TreeUtils.isUseOfElement(tree)) {
+            Element elt = TreeUtils.elementFromUse(tree);
+            return ElementUtils.isCompileTimeConstant(elt);
+        } else if (TreeUtils.isStringConcatenation(tree)) {
+            BinaryTree binOp = (BinaryTree) tree;
+            return isCompileTimeString(binOp.getLeftOperand())
+                && isCompileTimeString(binOp.getRightOperand());
+        } else {
+            return false;
+        }
+    }
+
+    /**
+     * Returns the receiver tree of a field access or a method invocation
+     */
+    public static ExpressionTree getReceiverTree(ExpressionTree expression) {
+        ExpressionTree receiver = TreeUtils.skipParens(expression);
+
+        if (!(receiver.getKind() == Tree.Kind.METHOD_INVOCATION
+                || receiver.getKind() == Tree.Kind.MEMBER_SELECT
+                || receiver.getKind() == Tree.Kind.IDENTIFIER
+                || receiver.getKind() == Tree.Kind.ARRAY_ACCESS)) {
+            // No receiver tree for anything but these four kinds.
+            return null;
+        }
+
+        if (receiver.getKind() == Tree.Kind.METHOD_INVOCATION) {
+            // Trying to handle receiver calls to trees of the form
+            //     ((m).getArray())
+            // returns the type of 'm' in this case
+            receiver = ((MethodInvocationTree)receiver).getMethodSelect();
+
+            if (receiver.getKind() == Tree.Kind.IDENTIFIER) {
+                // It's a method call "m(foo)" without an explicit receiver
+                return null;
+            } else if (receiver.getKind() == Tree.Kind.MEMBER_SELECT) {
+                receiver = ((MemberSelectTree)receiver).getExpression();
+            } else {
+                // Otherwise, e.g. a NEW_CLASS: nothing to do.
+            }
+        } else if (receiver.getKind() == Tree.Kind.IDENTIFIER) {
+            // It's a field access on implicit this or a local variable/parameter.
+            return null;
+        } else if (receiver.getKind() == Tree.Kind.ARRAY_ACCESS) {
+            return TreeUtils.skipParens(((ArrayAccessTree)receiver).getExpression());
+        } else if (receiver.getKind() == Tree.Kind.MEMBER_SELECT) {
+            receiver = ((MemberSelectTree)receiver).getExpression();
+            // Avoid int.class
+            if (receiver instanceof PrimitiveTypeTree) {
+                return null;
+            }
+        }
+
+        // Receiver is now really just the receiver tree.
+        return TreeUtils.skipParens(receiver);
+    }
+
+    // TODO: What about anonymous classes?
+    // Adding Tree.Kind.NEW_CLASS here doesn't work, because then a
+    // tree gets cast to ClassTree when it is actually a NewClassTree,
+    // for example in enclosingClass above.
+    private final static Set<Tree.Kind> classTreeKinds = EnumSet.of(
+            Tree.Kind.CLASS,
+            Tree.Kind.ENUM,
+            Tree.Kind.INTERFACE,
+            Tree.Kind.ANNOTATION_TYPE
+    );
+
+    public static Set<Tree.Kind> classTreeKinds() {
+        return classTreeKinds;
+    }
+
+    /**
+     * Is the given tree kind a class, i.e. a class, enum,
+     * interface, or annotation type.
+     *
+     * @param tree the tree to test
+     * @return true, iff the given kind is a class kind
+     */
+    public static boolean isClassTree(Tree tree) {
+        return classTreeKinds().contains(tree.getKind());
+    }
+
+    private final static Set<Tree.Kind> typeTreeKinds = EnumSet.of(
+            Tree.Kind.PRIMITIVE_TYPE,
+            Tree.Kind.PARAMETERIZED_TYPE,
+            Tree.Kind.TYPE_PARAMETER,
+            Tree.Kind.ARRAY_TYPE,
+            Tree.Kind.UNBOUNDED_WILDCARD,
+            Tree.Kind.EXTENDS_WILDCARD,
+            Tree.Kind.SUPER_WILDCARD,
+            Tree.Kind.ANNOTATED_TYPE
+    );
+
+    public static Set<Tree.Kind> typeTreeKinds() {
+        return typeTreeKinds;
+    }
+
+    /**
+     * Is the given tree a type instantiation?
+     *
+     * TODO: this is an under-approximation: e.g. an identifier could
+     * be either a type use or an expression. How can we distinguish.
+     *
+     * @param tree the tree to test
+     * @return true, iff the given tree is a type
+     */
+    public static boolean isTypeTree(Tree tree) {
+        return typeTreeKinds().contains(tree.getKind());
+    }
+
+    /**
+     * Returns true if the given element is an invocation of the method, or
+     * of any method that overrides that one.
+     */
+    public static boolean isMethodInvocation(Tree tree, ExecutableElement method, ProcessingEnvironment env) {
+        if (!(tree instanceof MethodInvocationTree)) {
+            return false;
+        }
+        MethodInvocationTree methInvok = (MethodInvocationTree)tree;
+        ExecutableElement invoked = TreeUtils.elementFromUse(methInvok);
+        return isMethod(invoked, method, env);
+    }
+
+    /** Returns true if the given element is, or overrides, method. */
+    private static boolean isMethod(ExecutableElement questioned, ExecutableElement method, ProcessingEnvironment env) {
+        return (questioned.equals(method)
+                || env.getElementUtils().overrides(questioned, method,
+                        (TypeElement)questioned.getEnclosingElement()));
+    }
+
+    /**
+     * Returns the ExecutableElement for a method declaration of
+     * methodName, in class typeName, with params parameters.
+     *
+     * TODO: to precisely resolve method overloading, we should use parameter types and not just
+     * the number of parameters!
+     */
+    public static ExecutableElement getMethod(String typeName, String methodName, int params, ProcessingEnvironment env) {
+        TypeElement mapElt = env.getElementUtils().getTypeElement(typeName);
+        for (ExecutableElement exec : ElementFilter.methodsIn(mapElt.getEnclosedElements())) {
+            if (exec.getSimpleName().contentEquals(methodName)
+                    && exec.getParameters().size() == params)
+                return exec;
+        }
+        ErrorReporter.errorAbort("TreeUtils.getMethod: shouldn't be here!");
+        return null; // dead code
+    }
+
+    /**
+     * Determine whether the given expression is either "this" or an outer
+     * "C.this".
+     *
+     * <p>
+     * TODO: Should this also handle "super"?
+     */
+    public static final boolean isExplicitThisDereference(ExpressionTree tree) {
+        if (tree.getKind() == Tree.Kind.IDENTIFIER
+                && ((IdentifierTree)tree).getName().contentEquals("this")) {
+            // Explicit this reference "this"
+            return true;
+        }
+
+        if (tree.getKind() != Tree.Kind.MEMBER_SELECT) {
+            return false;
+        }
+
+        MemberSelectTree memSelTree = (MemberSelectTree) tree;
+        if (memSelTree.getIdentifier().contentEquals("this")) {
+            // Outer this reference "C.this"
+            return true;
+        }
+        return false;
+    }
+
+    /**
+     * Determine whether {@code tree} is a class literal, such
+     * as
+     *
+     * <pre>
+     *   <em>Object</em> . <em>class</em>
+     * </pre>
+     *
+     * @return true iff if tree is a class literal
+     */
+    public static boolean isClassLiteral(Tree tree) {
+        if (tree.getKind() != Tree.Kind.MEMBER_SELECT) {
+            return false;
+        }
+        return "class".equals(((MemberSelectTree) tree).getIdentifier().toString());
+    }
+
+    /**
+     * Determine whether {@code tree} is a field access expressions, such
+     * as
+     *
+     * <pre>
+     *   <em>f</em>
+     *   <em>obj</em> . <em>f</em>
+     * </pre>
+     *
+     * @return true iff if tree is a field access expression (implicit or
+     *         explicit)
+     */
+    public static boolean isFieldAccess(Tree tree) {
+        if (tree.getKind().equals(Tree.Kind.MEMBER_SELECT)) {
+            // explicit field access
+            MemberSelectTree memberSelect = (MemberSelectTree) tree;
+            Element el = TreeUtils.elementFromUse(memberSelect);
+            return el.getKind().isField();
+        } else if (tree.getKind().equals(Tree.Kind.IDENTIFIER)) {
+            // implicit field access
+            IdentifierTree ident = (IdentifierTree) tree;
+            Element el = TreeUtils.elementFromUse(ident);
+            return el.getKind().isField()
+                    && !ident.getName().contentEquals("this") && !ident.getName().contentEquals("super");
+        }
+        return false;
+    }
+
+    /**
+     * Compute the name of the field that the field access {@code tree}
+     * accesses. Requires {@code tree} to be a field access, as determined
+     * by {@code isFieldAccess}.
+     *
+     * @return the name of the field accessed by {@code tree}.
+     */
+    public static String getFieldName(Tree tree) {
+        assert isFieldAccess(tree);
+        if (tree.getKind().equals(Tree.Kind.MEMBER_SELECT)) {
+            MemberSelectTree mtree = (MemberSelectTree) tree;
+            return mtree.getIdentifier().toString();
+        } else {
+            IdentifierTree itree = (IdentifierTree) tree;
+            return itree.getName().toString();
+        }
+    }
+
+    /**
+     * Determine whether {@code tree} refers to a method element, such
+     * as
+     *
+     * <pre>
+     *   <em>m</em>(...)
+     *   <em>obj</em> . <em>m</em>(...)
+     * </pre>
+     *
+     * @return true iff if tree is a method access expression (implicit or
+     *         explicit)
+     */
+    public static boolean isMethodAccess(Tree tree) {
+        if (tree.getKind().equals(Tree.Kind.MEMBER_SELECT)) {
+            // explicit method access
+            MemberSelectTree memberSelect = (MemberSelectTree) tree;
+            Element el = TreeUtils.elementFromUse(memberSelect);
+            return el.getKind() == ElementKind.METHOD
+                    || el.getKind() == ElementKind.CONSTRUCTOR;
+        } else if (tree.getKind().equals(Tree.Kind.IDENTIFIER)) {
+            // implicit method access
+            IdentifierTree ident = (IdentifierTree) tree;
+            // The field "super" and "this" are also legal methods
+            if (ident.getName().contentEquals("super")
+                    || ident.getName().contentEquals("this")) {
+                return true;
+            }
+            Element el = TreeUtils.elementFromUse(ident);
+            return el.getKind() == ElementKind.METHOD
+                    || el.getKind() == ElementKind.CONSTRUCTOR;
+        }
+        return false;
+    }
+
+    /**
+     * Compute the name of the method that the method access {@code tree}
+     * accesses. Requires {@code tree} to be a method access, as determined
+     * by {@code isMethodAccess}.
+     *
+     * @return the name of the method accessed by {@code tree}.
+     */
+    public static String getMethodName(Tree tree) {
+        assert isMethodAccess(tree);
+        if (tree.getKind().equals(Tree.Kind.MEMBER_SELECT)) {
+            MemberSelectTree mtree = (MemberSelectTree) tree;
+            return mtree.getIdentifier().toString();
+        } else {
+            IdentifierTree itree = (IdentifierTree) tree;
+            return itree.getName().toString();
+        }
+    }
+
+    /**
+     * @return {@code true} if and only if {@code tree} can have a type
+     *         annotation.
+     *
+     * TODO: is this implementation precise enough? E.g. does
+     * a .class literal work correctly?
+     */
+    public static boolean canHaveTypeAnnotation(Tree tree) {
+        return ((JCTree) tree).type != null;
+    }
+
+    /**
+     * Returns true if and only if the given {@code tree} represents a field
+     * access of the given {@link VariableElement}.
+     */
+    public static boolean isSpecificFieldAccess(Tree tree, VariableElement var) {
+        if (tree instanceof MemberSelectTree) {
+            MemberSelectTree memSel = (MemberSelectTree) tree;
+            Element field = TreeUtils.elementFromUse(memSel);
+            return field.equals(var);
+        } else if (tree instanceof IdentifierTree) {
+            IdentifierTree idTree = (IdentifierTree) tree;
+            Element field = TreeUtils.elementFromUse(idTree);
+            return field.equals(var);
+        } else {
+            return false;
+        }
+    }
+
+    /**
+     * Returns the VariableElement for a field declaration.
+     *
+     * @param typeName the class where the field is declared
+     * @param fieldName the name of the field
+     * @param env the processing environment
+     * @return the VariableElement for typeName.fieldName
+     */
+    public static VariableElement getField(String typeName, String fieldName, ProcessingEnvironment env) {
+        TypeElement mapElt = env.getElementUtils().getTypeElement(typeName);
+        for (VariableElement var : ElementFilter.fieldsIn(mapElt.getEnclosedElements())) {
+            if (var.getSimpleName().contentEquals(fieldName)) {
+                return var;
+            }
+        }
+        ErrorReporter.errorAbort("TreeUtils.getField: shouldn't be here!");
+        return null; // dead code
+    }
+
+    /** Determine whether the given tree represents an ExpressionTree.
+     *
+     * TODO: is there a nicer way than an instanceof?
+     *
+     * @param tree the Tree to test
+     * @return whether the tree is an ExpressionTree
+     */
+    public static boolean isExpressionTree(Tree tree) {
+        return tree instanceof ExpressionTree;
+    }
+
+    /**
+     * @param node the method invocation to check
+     * @return true if this is a super call to the {@link Enum} constructor
+     */
+    public static boolean isEnumSuper(MethodInvocationTree node) {
+        ExecutableElement ex = TreeUtils.elementFromUse(node);
+        Name name = ElementUtils.getQualifiedClassName(ex);
+        boolean correctClass = "java.lang.Enum".contentEquals(name);
+        boolean correctMethod = "<init>".contentEquals(ex.getSimpleName());
+        return correctClass && correctMethod;
+    }
+
+    /** Determine whether the given tree represents a declaration of a type
+     * (including type parameters).
+     *
+     * @param node  the Tree to test
+     * @return true if the tree is a type declaration
+     */
+    public static boolean isTypeDeclaration(Tree node) {
+        switch (node.getKind()) {
+            // These tree kinds are always declarations.  Uses of the declared
+            // types have tree kind IDENTIFIER.
+            case ANNOTATION_TYPE:
+            case CLASS:
+            case ENUM:
+            case INTERFACE:
+            case TYPE_PARAMETER:
+                return true;
+
+            default:
+                return false;
+        }
+    }
+
+    /**
+     * @see Object#getClass()
+     * @return true iff invocationTree is an instance of getClass()
+     */
+    public static boolean isGetClassInvocation(MethodInvocationTree invocationTree) {
+        final Element declarationElement = elementFromUse(invocationTree);
+        String ownerName = ElementUtils.getQualifiedClassName(declarationElement.getEnclosingElement()).toString();
+        return ownerName.equals("java.lang.Object")
+                && declarationElement.getSimpleName().toString().equals("getClass");
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypeAnnotationUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypeAnnotationUtils.java
new file mode 100644
index 0000000000..c7faceb53a
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypeAnnotationUtils.java
@@ -0,0 +1,627 @@
+package org.checkerframework.javacutil;
+
+import java.lang.reflect.InvocationTargetException;
+import java.nio.ByteBuffer;
+import java.util.Arrays;
+import java.util.Map;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.SourceVersion;
+import javax.lang.model.element.AnnotationMirror;
+import javax.lang.model.element.AnnotationValue;
+import javax.lang.model.element.AnnotationValueVisitor;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.type.ArrayType;
+import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.Elements;
+import javax.lang.model.util.Types;
+
+import com.sun.tools.javac.code.Attribute;
+import com.sun.tools.javac.code.Attribute.TypeCompound;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.TargetType;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeAnnotationPosition;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.tree.JCTree.JCLambda;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.List;
+import com.sun.tools.javac.util.Name;
+import com.sun.tools.javac.util.Pair;
+
+/**
+ * A collection of helper methods related to type annotation handling.
+ *
+ * @see AnnotationUtils
+ */
+public class TypeAnnotationUtils {
+
+    // Class cannot be instantiated.
+    private TypeAnnotationUtils() { throw new AssertionError("Class TypeAnnotationUtils cannot be instantiated."); }
+
+    /**
+     * Check whether a TypeCompound is contained in a list of TypeCompounds.
+     *
+     * @param list the input list of TypeCompounds
+     * @param tc the TypeCompound to find
+     * @return true, iff a TypeCompound equal to tc is contained in list
+     */
+    public static boolean isTypeCompoundContained(Types types, List<TypeCompound> list, TypeCompound tc) {
+        for (Attribute.TypeCompound rawat : list) {
+            if (contentEquals(rawat.type.tsym.name, tc.type.tsym.name) &&
+                    // TODO: in previous line, it would be nicer to use reference equality:
+                    //   rawat.type == tc.type &&
+                    // or at least "isSameType":
+                    //   types.isSameType(rawat.type, tc.type) &&
+                    // but each fails in some cases.
+                    rawat.values.equals(tc.values) &&
+                    isSameTAPositionExceptTreePos(rawat.position, tc.position)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    private static boolean contentEquals(Name n1, Name n2) {
+        // Views of underlying bytes, not copies as with Name#contentEquals
+        ByteBuffer b1 = ByteBuffer.wrap(n1.getByteArray(), n1.getByteOffset(), n1.getByteLength());
+        ByteBuffer b2 = ByteBuffer.wrap(n2.getByteArray(), n2.getByteOffset(), n2.getByteLength());
+
+        return b1.equals(b2);
+    }
+
+    /**
+     * Compare two TypeAnnotationPositions for equality.
+     *
+     * @param p1 the first position
+     * @param p2 the second position
+     * @return true, iff the two positions are equal
+     */
+    public static boolean isSameTAPosition(TypeAnnotationPosition p1,
+            TypeAnnotationPosition p2) {
+        return isSameTAPositionExceptTreePos(p1, p2) && p1.pos == p2.pos;
+    }
+
+    public static boolean isSameTAPositionExceptTreePos(TypeAnnotationPosition p1,
+                                           TypeAnnotationPosition p2) {
+        return p1.isValidOffset == p2.isValidOffset &&
+               p1.bound_index == p2.bound_index &&
+               p1.exception_index == p2.exception_index &&
+               p1.location.equals(p2.location) &&
+               Arrays.equals(p1.lvarIndex, p2.lvarIndex) &&
+               Arrays.equals(p1.lvarLength, p2.lvarLength) &&
+               Arrays.equals(p1.lvarOffset, p2.lvarOffset) &&
+               p1.offset == p2.offset &&
+               p1.onLambda == p2.onLambda &&
+               p1.parameter_index == p2.parameter_index &&
+               p1.type == p2.type &&
+               p1.type_index == p2.type_index;
+    }
+
+    /**
+     * Returns a newly created Attribute.Compound corresponding to an
+     * argument AnnotationMirror.
+     *
+     * @param am  an AnnotationMirror, which may be part of an AST or an internally
+     *            created subclass
+     * @return  a new Attribute.Compound corresponding to the AnnotationMirror
+     */
+    public static Attribute.Compound createCompoundFromAnnotationMirror(ProcessingEnvironment env,
+            AnnotationMirror am) {
+        // Create a new Attribute to match the AnnotationMirror.
+        List<Pair<Symbol.MethodSymbol, Attribute>> values = List.nil();
+        for (Map.Entry<? extends ExecutableElement, ? extends AnnotationValue> entry :
+                 am.getElementValues().entrySet()) {
+            Attribute attribute = attributeFromAnnotationValue(env, entry.getKey(), entry.getValue());
+            values = values.append(new Pair<>((Symbol.MethodSymbol)entry.getKey(),
+                                              attribute));
+        }
+        return new Attribute.Compound((Type.ClassType)am.getAnnotationType(), values);
+    }
+
+    /**
+     * Returns a newly created Attribute.TypeCompound corresponding to an
+     * argument AnnotationMirror.
+     *
+     * @param am  an AnnotationMirror, which may be part of an AST or an internally
+     *            created subclass
+     * @param tapos  the type annotation position to use
+     * @return  a new Attribute.TypeCompound corresponding to the AnnotationMirror
+     */
+    public static Attribute.TypeCompound createTypeCompoundFromAnnotationMirror(ProcessingEnvironment env,
+            AnnotationMirror am, TypeAnnotationPosition tapos) {
+        // Create a new Attribute to match the AnnotationMirror.
+        List<Pair<Symbol.MethodSymbol, Attribute>> values = List.nil();
+        for (Map.Entry<? extends ExecutableElement, ? extends AnnotationValue> entry :
+                 am.getElementValues().entrySet()) {
+            Attribute attribute = attributeFromAnnotationValue(env, entry.getKey(), entry.getValue());
+            values = values.append(new Pair<>((Symbol.MethodSymbol)entry.getKey(),
+                                              attribute));
+        }
+        return new Attribute.TypeCompound((Type.ClassType)am.getAnnotationType(), values, tapos);
+    }
+
+    /**
+     * Returns a newly created Attribute corresponding to an argument
+     * AnnotationValue.
+     *
+     * @param meth the ExecutableElement that is assigned the value, needed for empty arrays
+     * @param av  an AnnotationValue, which may be part of an AST or an internally
+     *            created subclass
+     * @return  a new Attribute corresponding to the AnnotationValue
+     */
+    public static Attribute attributeFromAnnotationValue(ProcessingEnvironment env, ExecutableElement meth, AnnotationValue av) {
+        return av.accept(new AttributeCreator(env, meth), null);
+    }
+
+    private static class AttributeCreator implements AnnotationValueVisitor<Attribute, Void> {
+        private final ProcessingEnvironment processingEnv;
+        private final Types modelTypes;
+        private final Elements elements;
+        private final com.sun.tools.javac.code.Types javacTypes;
+
+        private final ExecutableElement meth;
+
+        public AttributeCreator(ProcessingEnvironment env, ExecutableElement meth) {
+            this.processingEnv = env;
+            Context context = ((JavacProcessingEnvironment)env).getContext();
+            this.elements = env.getElementUtils();
+            this.modelTypes = env.getTypeUtils();
+            this.javacTypes = com.sun.tools.javac.code.Types.instance(context);
+
+            this.meth = meth;
+        }
+
+        @Override
+        public Attribute visit(AnnotationValue av, Void p) {
+            return av.accept(this, p);
+        }
+
+        @Override
+        public Attribute visit(AnnotationValue av) {
+            return visit(av, null);
+        }
+
+        @Override
+        public Attribute visitBoolean(boolean b, Void p) {
+            TypeMirror booleanType = modelTypes.getPrimitiveType(TypeKind.BOOLEAN);
+            return new Attribute.Constant((Type) booleanType, b ? 1 : 0);
+        }
+
+        @Override
+        public Attribute visitByte(byte b, Void p) {
+            TypeMirror byteType = modelTypes.getPrimitiveType(TypeKind.BYTE);
+            return new Attribute.Constant((Type)byteType, b);
+        }
+
+        @Override
+        public Attribute visitChar(char c, Void p) {
+            TypeMirror charType = modelTypes.getPrimitiveType(TypeKind.CHAR);
+            return new Attribute.Constant((Type)charType, c);
+        }
+
+        @Override
+        public Attribute visitDouble(double d, Void p) {
+            TypeMirror doubleType = modelTypes.getPrimitiveType(TypeKind.DOUBLE);
+            return new Attribute.Constant((Type)doubleType, d);
+        }
+
+        @Override
+        public Attribute visitFloat(float f, Void p) {
+            TypeMirror floatType = modelTypes.getPrimitiveType(TypeKind.FLOAT);
+            return new Attribute.Constant((Type)floatType, f);
+        }
+
+        @Override
+        public Attribute visitInt(int i, Void p) {
+            TypeMirror intType = modelTypes.getPrimitiveType(TypeKind.INT);
+            return new Attribute.Constant((Type)intType, i);
+        }
+
+        @Override
+        public Attribute visitLong(long i, Void p) {
+            TypeMirror longType = modelTypes.getPrimitiveType(TypeKind.LONG);
+            return new Attribute.Constant((Type)longType, i);
+        }
+
+        @Override
+        public Attribute visitShort(short s, Void p) {
+            TypeMirror shortType = modelTypes.getPrimitiveType(TypeKind.SHORT);
+            return new Attribute.Constant((Type)shortType, s);
+        }
+
+        @Override
+        public Attribute visitString(String s, Void p) {
+            TypeMirror stringType = elements.getTypeElement("java.lang.String").asType();
+            return new Attribute.Constant((Type)stringType, s);
+        }
+
+        @Override
+        public Attribute visitType(TypeMirror t, Void p) {
+            if (t instanceof Type) {
+                return new Attribute.Class(javacTypes, (Type)t);
+            }
+
+            assert false : "Unexpected type of TypeMirror: " + t.getClass();
+            return null;
+        }
+
+        @Override
+        public Attribute visitEnumConstant(VariableElement c, Void p) {
+            if (c instanceof Symbol.VarSymbol) {
+                Symbol.VarSymbol sym = (Symbol.VarSymbol) c;
+                if (sym.getKind() == ElementKind.ENUM_CONSTANT) {
+                    return new Attribute.Enum(sym.type, sym);
+                }
+            }
+
+            assert false : "Unexpected type of VariableElement: " + c.getClass();
+            return null;
+        }
+
+        @Override
+        public Attribute visitAnnotation(AnnotationMirror a, Void p) {
+            return createCompoundFromAnnotationMirror(processingEnv, a);
+        }
+
+        @Override
+        public Attribute visitArray(java.util.List<? extends AnnotationValue> vals, Void p) {
+            if (!vals.isEmpty()) {
+                List<Attribute> valAttrs = List.nil();
+                for (AnnotationValue av : vals) {
+                    valAttrs = valAttrs.append(av.accept(this, p));
+                }
+                ArrayType arrayType = modelTypes.getArrayType(valAttrs.get(0).type);
+                return new Attribute.Array((Type)arrayType, valAttrs);
+            } else {
+                return new Attribute.Array((Type) meth.getReturnType(), List.<Attribute>nil());
+            }
+        }
+
+        @Override
+        public Attribute visitUnknown(AnnotationValue av, Void p) {
+            assert false : "Unexpected type of AnnotationValue: " + av.getClass();
+            return null;
+        }
+    }
+
+    /**
+     * An interface to abstract a Java 8 and a Java 9 version of how
+     * to get a RET reference.
+     * These methods must then be implemented using reflection in order to
+     * compile in either setting.
+     * Note that we cannot use lambda for this as long as we want to
+     * support Java 7.
+     */
+    interface Call8or9<RET> {
+        RET call8() throws Throwable;
+        RET call9() throws Throwable;
+    }
+
+    /**
+     * Use the SourceVersion to decide whether to call the Java 8 or Java 9 version.
+     * Catch all exceptions and abort if one occurs - the reflection code should
+     * never break once fully debugged.
+     *
+     * @param tc the TAPCall abstraction to encapsulate two methods
+     * @return the created TypeAnnotationPosition
+     */
+    private static <RET> RET call8or9(Call8or9<RET> tc) {
+        try {
+            boolean hasNine;
+            try {
+                hasNine = SourceVersion.valueOf("RELEASE_9") != null;
+            } catch (IllegalArgumentException iae) {
+                hasNine = false;
+            }
+            if (hasNine) {
+                return tc.call9();
+            } else {
+                boolean hasEight;
+                try {
+                    hasEight = SourceVersion.valueOf("RELEASE_8") != null;
+                } catch (IllegalArgumentException iae) {
+                    hasEight = false;
+                }
+                if (hasEight) {
+                    return tc.call8();
+                } else {
+                    assert false : "Checker Framework needs a Java 8 or 9 javac.";
+                    return null;
+                }
+            }
+        } catch (Throwable t) {
+            assert false : "Checker Framework internal error: " + t;
+            t.printStackTrace();
+            return null;
+        }
+    }
+
+    public static TypeAnnotationPosition unknownTAPosition() {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException {
+                        return TypeAnnotationPosition.class.newInstance();
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalArgumentException, IllegalAccessException, NoSuchFieldException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getField("unknown")
+                                .get(null);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodReturnTAPosition(final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.METHOD_RETURN);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodReturn", int.class)
+                                .invoke(null, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodReceiverTAPosition(final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.METHOD_RECEIVER);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodReceiver", int.class)
+                                .invoke(null, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodParameterTAPosition(final int pidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.METHOD_FORMAL_PARAMETER);
+                        TypeAnnotationPosition.class.getField("parameter_index").set(tapos, pidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodParameter", int.class, int.class)
+                                .invoke(null, pidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodThrowsTAPosition(final int tidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.THROWS);
+                        TypeAnnotationPosition.class.getField("type_index").set(tapos, tidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException, NoSuchFieldException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodThrows", List.class, JCLambda.class, int.class, int.class)
+                                .invoke(null, TypeAnnotationPosition.class.getField("emptyPath").get(null), null, tidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition fieldTAPosition(final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.FIELD);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("field", int.class)
+                                .invoke(null, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition classExtendsTAPosition(final int implidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.CLASS_EXTENDS);
+                        TypeAnnotationPosition.class.getField("type_index").set(tapos, implidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("classExtends", int.class, int.class)
+                                .invoke(null, implidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition typeParameterTAPosition(final int tpidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.CLASS_TYPE_PARAMETER);
+                        TypeAnnotationPosition.class.getField("parameter_index").set(tapos, tpidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException, NoSuchFieldException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("typeParameter", List.class, JCLambda.class, int.class, int.class)
+                                .invoke(null, TypeAnnotationPosition.class.getField("emptyPath").get(null), null, tpidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodTypeParameterTAPosition(final int tpidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.METHOD_TYPE_PARAMETER);
+                        TypeAnnotationPosition.class.getField("parameter_index").set(tapos, tpidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException, NoSuchFieldException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodTypeParameter", List.class, JCLambda.class, int.class, int.class)
+                                .invoke(null, TypeAnnotationPosition.class.getField("emptyPath").get(null), null, tpidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition typeParameterBoundTAPosition(final int tpidx, final int bndidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.CLASS_TYPE_PARAMETER_BOUND);
+                        TypeAnnotationPosition.class.getField("parameter_index").set(tapos, tpidx);
+                        TypeAnnotationPosition.class.getField("bound_index").set(tapos, bndidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException, NoSuchFieldException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("typeParameterBound", List.class, JCLambda.class, int.class, int.class, int.class)
+                                .invoke(null, TypeAnnotationPosition.class.getField("emptyPath").get(null), null, tpidx, bndidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition methodTypeParameterBoundTAPosition(final int tpidx, final int bndidx, final int pos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        TypeAnnotationPosition tapos = TypeAnnotationPosition.class.newInstance();
+                        TypeAnnotationPosition.class.getField("type").set(tapos, TargetType.METHOD_TYPE_PARAMETER_BOUND);
+                        TypeAnnotationPosition.class.getField("parameter_index").set(tapos, tpidx);
+                        TypeAnnotationPosition.class.getField("bound_index").set(tapos, bndidx);
+                        TypeAnnotationPosition.class.getField("pos").set(tapos, pos);
+                        return tapos;
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException, NoSuchFieldException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("methodTypeParameterBound", List.class, JCLambda.class, int.class, int.class, int.class)
+                                .invoke(null, TypeAnnotationPosition.class.getField("emptyPath").get(null), null, tpidx, bndidx, pos);
+                    }
+                }
+            );
+    }
+
+    public static TypeAnnotationPosition copyTAPosition(final TypeAnnotationPosition tapos) {
+        return call8or9(
+                new Call8or9<TypeAnnotationPosition>() {
+                    @Override
+                    public TypeAnnotationPosition call8() throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+                        return copyTAPosition8(tapos);
+                    }
+                    @Override
+                    public TypeAnnotationPosition call9() throws IllegalArgumentException, IllegalAccessException, NoSuchFieldException, SecurityException, InvocationTargetException, NoSuchMethodException {
+                        return (TypeAnnotationPosition) TypeAnnotationPosition.class
+                                .getMethod("copy", TypeAnnotationPosition.class)
+                                .invoke(null, tapos);
+                    }
+                }
+            );
+    }
+
+    private static TypeAnnotationPosition copyTAPosition8(TypeAnnotationPosition tapos) throws InstantiationException, IllegalAccessException, IllegalArgumentException, NoSuchFieldException, SecurityException {
+        TypeAnnotationPosition res = TypeAnnotationPosition.class.newInstance();
+        res.isValidOffset = tapos.isValidOffset;
+        TypeAnnotationPosition.class.getField("bound_index").set(res, tapos.bound_index);
+        res.exception_index = tapos.exception_index;
+        res.location = List.from(tapos.location);
+        if (tapos.lvarIndex != null) {
+            res.lvarIndex = Arrays.copyOf(tapos.lvarIndex, tapos.lvarIndex.length);
+        }
+        if (tapos.lvarLength != null) {
+            res.lvarLength = Arrays.copyOf(tapos.lvarLength, tapos.lvarLength.length);
+        }
+        if (tapos.lvarOffset != null) {
+            res.lvarOffset = Arrays.copyOf(tapos.lvarOffset, tapos.lvarOffset.length);
+        }
+        res.offset = tapos.offset;
+        TypeAnnotationPosition.class.getField("onLambda").set(res, tapos.onLambda);
+        TypeAnnotationPosition.class.getField("parameter_index").set(res, tapos.parameter_index);
+        TypeAnnotationPosition.class.getField("pos").set(res, tapos.pos);
+        TypeAnnotationPosition.class.getField("type").set(res, tapos.type);
+        TypeAnnotationPosition.class.getField("type_index").set(res, tapos.type_index);
+        return res;
+    }
+
+    public static Type unannotatedType(final Type in) {
+        return call8or9(
+                new Call8or9<Type>() {
+                    @Override
+                    public Type call8() throws IllegalAccessException, IllegalArgumentException, InvocationTargetException, NoSuchMethodException, SecurityException {
+                        return (Type) Type.class
+                                .getMethod("unannotatedType")
+                                .invoke(in);
+                    }
+                    @Override
+                    public Type call9() {
+                        return in;
+                    }
+                }
+            );
+    }
+
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypesUtils.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypesUtils.java
new file mode 100644
index 0000000000..949bf1362f
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/TypesUtils.java
@@ -0,0 +1,446 @@
+package org.checkerframework.javacutil;
+
+import com.sun.tools.javac.code.Symtab;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeTag;
+import com.sun.tools.javac.model.JavacTypes;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.util.Context;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.NestingKind;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.TypeParameterElement;
+import javax.lang.model.type.ArrayType;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.type.TypeVariable;
+import javax.lang.model.type.WildcardType;
+import javax.lang.model.util.Elements;
+import javax.lang.model.util.Types;
+
+import static com.sun.tools.javac.code.TypeTag.WILDCARD;
+
+/**
+ * A utility class that helps with {@link TypeMirror}s.
+ *
+ */
+// TODO: This class needs significant restructuring
+public final class TypesUtils {
+
+    // Class cannot be instantiated
+    private TypesUtils() { throw new AssertionError("Class TypesUtils cannot be instantiated."); }
+
+    /**
+     * Gets the fully qualified name for a provided type.  It returns an empty
+     * name if type is an anonymous type.
+     *
+     * @param type the declared type
+     * @return the name corresponding to that type
+     */
+    public static Name getQualifiedName(DeclaredType type) {
+        TypeElement element = (TypeElement) type.asElement();
+        return element.getQualifiedName();
+    }
+
+    /**
+     * Checks if the type represents a java.lang.Object declared type.
+     *
+     * @param type  the type
+     * @return true iff type represents java.lang.Object
+     */
+    public static boolean isObject(TypeMirror type) {
+        return isDeclaredOfName(type, "java.lang.Object");
+    }
+
+    /**
+     * Checks if the type represents a java.lang.Class declared type.
+     *
+     * @param type  the type
+     * @return true iff type represents java.lang.Class
+     */
+    public static boolean isClass(TypeMirror type) {
+        return isDeclaredOfName(type, "java.lang.Class");
+    }
+
+    /**
+     * Checks if the type represents a java.lang.String declared type.
+     * TODO: it would be cleaner to use String.class.getCanonicalName(), but
+     *   the two existing methods above don't do that, I guess for performance reasons.
+     *
+     * @param type  the type
+     * @return true iff type represents java.lang.String
+     */
+    public static boolean isString(TypeMirror type) {
+        return isDeclaredOfName(type, "java.lang.String");
+    }
+
+    /**
+     * Checks if the type represents a boolean type, that is either boolean
+     * (primitive type) or java.lang.Boolean.
+     *
+     * @param type the type to test
+     * @return true iff type represents a boolean type
+     */
+    public static boolean isBooleanType(TypeMirror type) {
+        return isDeclaredOfName(type, "java.lang.Boolean")
+                || type.getKind().equals(TypeKind.BOOLEAN);
+    }
+
+    /**
+     * Check if the type represent a declared type of the given qualified name
+     *
+     * @param type the type
+     * @return type iff type represents a declared type of the qualified name
+     */
+    public static boolean isDeclaredOfName(TypeMirror type, CharSequence qualifiedName) {
+        return type.getKind() == TypeKind.DECLARED
+            && getQualifiedName((DeclaredType) type).contentEquals(qualifiedName);
+    }
+
+    public static boolean isBoxedPrimitive(TypeMirror type) {
+        if (type.getKind() != TypeKind.DECLARED) {
+            return false;
+        }
+
+        String qualifiedName = getQualifiedName((DeclaredType)type).toString();
+
+        return (qualifiedName.equals("java.lang.Boolean")
+                || qualifiedName.equals("java.lang.Byte")
+                || qualifiedName.equals("java.lang.Character")
+                || qualifiedName.equals("java.lang.Short")
+                || qualifiedName.equals("java.lang.Integer")
+                || qualifiedName.equals("java.lang.Long")
+                || qualifiedName.equals("java.lang.Double")
+                || qualifiedName.equals("java.lang.Float"));
+    }
+
+    /** @return type represents a Throwable type (e.g. Exception, Error) **/
+    public static boolean isThrowable(TypeMirror type) {
+        while (type != null && type.getKind() == TypeKind.DECLARED) {
+            DeclaredType dt = (DeclaredType) type;
+            TypeElement elem = (TypeElement) dt.asElement();
+            Name name = elem.getQualifiedName();
+            if ("java.lang.Throwable".contentEquals(name)) {
+                return true;
+            }
+            type = elem.getSuperclass();
+        }
+        return false;
+    }
+
+    /**
+     * Returns true iff the argument is an anonymous type.
+     *
+     * @return whether the argument is an anonymous type
+     */
+    public static boolean isAnonymous(TypeMirror type) {
+        return (type instanceof DeclaredType)
+                && (((TypeElement) ((DeclaredType) type).asElement()).getNestingKind()
+                        .equals(NestingKind.ANONYMOUS));
+    }
+
+    /**
+     * Returns true iff the argument is a primitive type.
+     *
+     * @return whether the argument is a primitive type
+     */
+    public static boolean isPrimitive(TypeMirror type) {
+        switch (type.getKind()) {
+        case BOOLEAN:
+        case BYTE:
+        case CHAR:
+        case DOUBLE:
+        case FLOAT:
+        case INT:
+        case LONG:
+        case SHORT:
+            return true;
+        default:
+            return false;
+        }
+    }
+
+    /**
+     * Returns true iff the arguments are both the same primitive types.
+     *
+     * @return  whether the arguments are the same primitive types
+     */
+    public static boolean areSamePrimitiveTypes(TypeMirror left, TypeMirror right) {
+        if (!isPrimitive(left) || !isPrimitive(right)) {
+            return false;
+        }
+
+        return (left.getKind() == right.getKind());
+    }
+
+    /**
+     * Returns true iff the argument is a primitive numeric type.
+     *
+     * @return  whether the argument is a primitive numeric type
+     */
+    public static boolean isNumeric(TypeMirror type) {
+        switch (type.getKind()) {
+        case BYTE:
+        case CHAR:
+        case DOUBLE:
+        case FLOAT:
+        case INT:
+        case LONG:
+        case SHORT:
+            return true;
+        default:
+            return false;
+        }
+    }
+
+    /**
+     * Returns true iff the argument is an integral type.
+     *
+     * @return  whether the argument is an integral type
+     */
+    public static boolean isIntegral(TypeMirror type) {
+        switch (type.getKind()) {
+        case BYTE:
+        case CHAR:
+        case INT:
+        case LONG:
+        case SHORT:
+            return true;
+        default:
+            return false;
+        }
+    }
+
+    /**
+     * Returns true iff the argument is a floating point type.
+     *
+     * @return  whether the argument is a floating point type
+     */
+    public static boolean isFloating(TypeMirror type) {
+        switch (type.getKind()) {
+        case DOUBLE:
+        case FLOAT:
+            return true;
+        default:
+            return false;
+        }
+    }
+
+    /**
+     * Returns the widened numeric type for an arithmetic operation
+     * performed on a value of the left type and the right type.
+     * Defined in JLS 5.6.2.  We return a {@link TypeKind} because
+     * creating a {@link TypeMirror} requires a {@link Types} object
+     * from the {@link javax.annotation.processing.ProcessingEnvironment}.
+     *
+     * @return  the result of widening numeric conversion, or NONE when
+     *          the conversion cannot be performed
+     */
+    public static TypeKind widenedNumericType(TypeMirror left, TypeMirror right) {
+        if (!isNumeric(left) || !isNumeric(right)) {
+            return TypeKind.NONE;
+        }
+
+        TypeKind leftKind = left.getKind();
+        TypeKind rightKind = right.getKind();
+
+        if (leftKind == TypeKind.DOUBLE || rightKind == TypeKind.DOUBLE) {
+            return TypeKind.DOUBLE;
+        }
+
+        if (leftKind == TypeKind.FLOAT || rightKind == TypeKind.FLOAT) {
+            return TypeKind.FLOAT;
+        }
+
+        if (leftKind == TypeKind.LONG || rightKind == TypeKind.LONG) {
+            return TypeKind.LONG;
+        }
+
+        return TypeKind.INT;
+    }
+
+    /**
+     * If the argument is a bounded TypeVariable or WildcardType,
+     * return its non-variable, non-wildcard upper bound.  Otherwise,
+     * return the type itself.
+     *
+     * @param type  a type
+     * @return  the non-variable, non-wildcard upper bound of a type,
+     *    if it has one, or itself if it has no bounds
+     */
+    public static TypeMirror upperBound(TypeMirror type) {
+        do {
+            if (type instanceof TypeVariable) {
+                TypeVariable tvar = (TypeVariable) type;
+                if (tvar.getUpperBound() != null) {
+                    type = tvar.getUpperBound();
+                } else {
+                    break;
+                }
+            } else if (type instanceof WildcardType) {
+                WildcardType wc = (WildcardType) type;
+                if (wc.getExtendsBound() != null) {
+                    type = wc.getExtendsBound();
+                } else {
+                    break;
+                }
+            } else {
+                break;
+            }
+        } while (true);
+        return type;
+    }
+
+    /**
+     * Get the type parameter for this wildcard from the underlying type's bound field
+     * This field is sometimes null, in that case this method will return null
+     * @return the TypeParameterElement the wildcard is an argument to
+     */
+    public static TypeParameterElement wildcardToTypeParam(final Type.WildcardType wildcard) {
+
+        final Element typeParamElement;
+        if (wildcard.bound != null) {
+            typeParamElement = wildcard.bound.asElement();
+        } else {
+            typeParamElement = null;
+        }
+
+        return (TypeParameterElement) typeParamElement;
+    }
+
+    /**
+     * Version of com.sun.tools.javac.code.Types.wildUpperBound(Type)
+     * that works with both jdk8 (called upperBound there) and jdk8u.
+     */
+    // TODO: contrast to upperBound.
+    public static Type wildUpperBound(ProcessingEnvironment env, TypeMirror tm) {
+        Type t = (Type) tm;
+        if (t.hasTag(TypeTag.WILDCARD)) {
+            Context context = ((JavacProcessingEnvironment) env).getContext();
+            Type.WildcardType w = (Type.WildcardType) TypeAnnotationUtils.unannotatedType(t);
+            if (w.isSuperBound()) {
+                Symtab syms = Symtab.instance(context);
+                return w.bound == null ? syms.objectType : w.bound.bound;
+            } else {
+                return wildUpperBound(env, w.type);
+            }
+        } else {
+            return TypeAnnotationUtils.unannotatedType(t);
+        }
+    }
+
+    /**
+     * Version of com.sun.tools.javac.code.Types.wildLowerBound(Type)
+     * that works with both jdk8 (called upperBound there) and jdk8u.
+     */
+    public static Type wildLowerBound(ProcessingEnvironment env, TypeMirror tm) {
+        Type t = (Type) tm;
+        if (t.hasTag(WILDCARD)) {
+            Context context = ((JavacProcessingEnvironment) env).getContext();
+            Symtab syms = Symtab.instance(context);
+            Type.WildcardType w = (Type.WildcardType) TypeAnnotationUtils.unannotatedType(t);
+            return w.isExtendsBound() ? syms.botType : wildLowerBound(env, w.type);
+        } else {
+            return t.unannotatedType();
+        }
+    }
+    /**
+     * Returns the {@link TypeMirror} for a given {@link Class}.
+     */
+    public static TypeMirror typeFromClass(Types types, Elements elements, Class<?> clazz) {
+        if (clazz == void.class) {
+            return types.getNoType(TypeKind.VOID);
+        } else if (clazz.isPrimitive()) {
+            String primitiveName = clazz.getName().toUpperCase();
+            TypeKind primitiveKind = TypeKind.valueOf(primitiveName);
+            return types.getPrimitiveType(primitiveKind);
+        } else if (clazz.isArray()) {
+            TypeMirror componentType = typeFromClass(types, elements, clazz.getComponentType());
+            return types.getArrayType(componentType);
+        } else {
+            TypeElement element = elements.getTypeElement(clazz.getCanonicalName());
+            if (element == null) {
+                ErrorReporter.errorAbort("Unrecognized class: " + clazz);
+                return null; // dead code
+            }
+            return element.asType();
+        }
+    }
+
+    /**
+     * Returns an {@link ArrayType} with elements of type {@code componentType}.
+     */
+    public static ArrayType createArrayType(Types types, TypeMirror componentType) {
+        JavacTypes t = (JavacTypes) types;
+        return t.getArrayType(componentType);
+    }
+
+    /**
+     * Returns true if declaredType is a Class that is used to box primitive type
+     * (e.g. declaredType=java.lang.Double and primitiveType=22.5d )
+     */
+    public static boolean isBoxOf(TypeMirror declaredType, TypeMirror primitiveType) {
+        if (declaredType.getKind() != TypeKind.DECLARED) {
+            return false;
+        }
+
+        final String qualifiedName = getQualifiedName((DeclaredType) declaredType).toString();
+        switch (primitiveType.getKind()) {
+            case BOOLEAN:  return qualifiedName.equals("java.lang.Boolean");
+            case BYTE:     return qualifiedName.equals("java.lang.Byte");
+            case CHAR:     return qualifiedName.equals("java.lang.Character");
+            case DOUBLE:   return qualifiedName.equals("java.lang.Double");
+            case FLOAT:    return qualifiedName.equals("java.lang.Float");
+            case INT:      return qualifiedName.equals("java.lang.Integer");
+            case LONG:     return qualifiedName.equals("java.lang.Long");
+            case SHORT:    return qualifiedName.equals("java.lang.Short");
+
+            default:
+                return false;
+        }
+    }
+
+    /**
+     * Given a bounded type (wildcard or typevar) get the concrete type of its upper bound.  If
+     * the bounded type extends other bounded types, this method will iterate through their bounds
+     * until a class, interface, or intersection is found.
+     * @return a type that is not a wildcard or typevar, or null if this type is an unbounded wildcard
+     */
+    public static TypeMirror findConcreteUpperBound(final TypeMirror boundedType) {
+        TypeMirror effectiveUpper = boundedType;
+        outerLoop : while (true) {
+            switch (effectiveUpper.getKind()) {
+                case WILDCARD:
+                    effectiveUpper = ((javax.lang.model.type.WildcardType) effectiveUpper).getExtendsBound();
+                    if (effectiveUpper == null) {
+                        return null;
+                    }
+                    break;
+
+                case TYPEVAR:
+                    effectiveUpper = ((TypeVariable) effectiveUpper).getUpperBound();
+                    break;
+
+                default:
+                    break outerLoop;
+            }
+        }
+        return effectiveUpper;
+    }
+
+    /**
+     * Returns true if the erased type of subtype is a subtype of the erased type of supertype.
+     *
+     * @param types     Types
+     * @param subtype   possible subtype
+     * @param supertype possible supertype
+     * @return true if the erased type of subtype is a subtype of the erased type of supertype
+     */
+    public static boolean isErasedSubtype(Types types, TypeMirror subtype, TypeMirror supertype) {
+        return types.isSubtype(types.erasure(subtype), types.erasure(supertype));
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/dist/ManualTaglet.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/dist/ManualTaglet.java
new file mode 100644
index 0000000000..e7df75ff54
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/dist/ManualTaglet.java
@@ -0,0 +1,129 @@
+package org.checkerframework.javacutil.dist;
+
+import java.util.Map;
+
+import com.sun.javadoc.Tag;
+import com.sun.tools.doclets.Taglet;
+
+/**
+ * A taglet for processing the {@code @checker_framework.manual} javadoc block tag, which inserts
+ * references to the Checker Framework manual into javadoc.
+ *
+ * <p>
+ *
+ * The {@code @checker_framework.manual} tag is used as follows:
+ *
+ * <ul>
+ * <li>{@code @checker_framework.manual #} expands to a top-level link to the Checker Framework manual
+ * <li>{@code @checker_framework.manual #anchor text} expands to a link with some text to a
+ * particular part of the manual
+ * </ul>
+ */
+public class ManualTaglet implements Taglet {
+
+    @Override
+    public String getName() {
+        return "checker_framework.manual";
+    }
+
+    @Override
+    public boolean inConstructor() {
+        return true;
+    }
+
+    @Override
+    public boolean inField() {
+        return true;
+    }
+
+    @Override
+    public boolean inMethod() {
+        return true;
+    }
+
+    @Override
+    public boolean inOverview() {
+        return true;
+    }
+
+    @Override
+    public boolean inPackage() {
+        return true;
+    }
+
+    @Override
+    public boolean inType() {
+        return true;
+    }
+
+    @Override
+    public boolean isInlineTag() {
+        return false;
+    }
+
+    /**
+     * Formats a link, given an array of tokens.
+     *
+     * @param parts the array of tokens
+     * @return a link to the manual top-level if the array size is one, or a
+     *         link to a part of the manual if it's larger than one
+     */
+    private String formatLink(String[] parts) {
+        String anchor, text;
+        if (parts.length < 2) {
+            anchor = "";
+            text = "Checker Framework";
+        } else {
+            anchor = parts[0];
+            text = parts[1];
+        }
+        return String.format(
+                "<A HREF=\"http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html%s\">%s</A>",
+                anchor, text);
+    }
+
+    /**
+     * Formats the {@code @checker_framework.manual} tag, prepending the tag header to the
+     * tag content.
+     *
+     * @param text the tag content
+     * @return the formatted tag
+     */
+    private String formatHeader(String text) {
+        return String.format(
+                "<DT><B>See the Checker Framework Manual:</B><DD>%s<BR>",
+                text);
+    }
+
+    @Override
+    public String toString(Tag tag) {
+        String[] split = tag.text().split(" ", 2);
+        return formatHeader(formatLink(split));
+    }
+
+    @Override
+    public String toString(Tag[] tags) {
+        if (tags.length == 0) {
+            return "";
+        }
+        StringBuilder sb = new StringBuilder();
+        for (Tag t : tags) {
+            String[] split = t.text().split(" ", 2);
+            if (t != tags[0]) {
+                sb.append(", ");
+            }
+            sb.append(formatLink(split));
+        }
+        return formatHeader(sb.toString());
+    }
+
+    @SuppressWarnings({ "unchecked", "rawtypes" })
+    public static void register(Map tagletMap) {
+        ManualTaglet tag = new ManualTaglet();
+        Taglet t = (Taglet) tagletMap.get(tag.getName());
+        if (t != null) {
+            tagletMap.remove(tag.getName());
+        }
+        tagletMap.put(tag.getName(), tag);
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/DetachedVarSymbol.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/DetachedVarSymbol.java
new file mode 100644
index 0000000000..0edf3944e3
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/DetachedVarSymbol.java
@@ -0,0 +1,45 @@
+package org.checkerframework.javacutil.trees;
+
+import com.sun.source.tree.VariableTree;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.util.Name;
+
+/*>>>
+import org.checkerframework.checker.nullness.qual.Nullable;
+*/
+
+/**
+ * A DetachedVarSymbol represents a variable that is not part of any
+ * AST Tree.  DetachedVarSymbols are created when desugaring source
+ * code constructs and they carry important type information, but some
+ * methods such as TreeInfo.declarationFor do not work on them.
+ */
+
+public class DetachedVarSymbol extends Symbol.VarSymbol {
+
+    protected /*@Nullable*/ VariableTree decl;
+
+    /**
+     * Construct a detached variable symbol, given its flags, name,
+     * type and owner.
+     */
+    public DetachedVarSymbol(long flags, Name name, Type type, Symbol owner) {
+        super(flags, name, type, owner);
+        this.decl = null;
+    }
+
+    /**
+     * Set the declaration tree for the variable.
+     */
+    public void setDeclaration(VariableTree decl) {
+        this.decl = decl;
+    }
+
+    /**
+     * Get the declaration tree for the variable.
+     */
+    public /*@Nullable*/ VariableTree getDeclaration() {
+        return decl;
+    }
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeBuilder.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeBuilder.java
new file mode 100644
index 0000000000..2623f2f2e7
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeBuilder.java
@@ -0,0 +1,687 @@
+package org.checkerframework.javacutil.trees;
+
+import java.util.List;
+
+import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.Name;
+import javax.lang.model.element.TypeElement;
+import javax.lang.model.element.VariableElement;
+import javax.lang.model.type.ArrayType;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeKind;
+import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.ElementFilter;
+import javax.lang.model.util.Elements;
+import javax.lang.model.util.Types;
+
+import org.checkerframework.javacutil.InternalUtils;
+import org.checkerframework.javacutil.TypesUtils;
+
+import com.sun.source.tree.ArrayAccessTree;
+import com.sun.source.tree.AssignmentTree;
+import com.sun.source.tree.BinaryTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.IdentifierTree;
+import com.sun.source.tree.LiteralTree;
+import com.sun.source.tree.MemberSelectTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.StatementTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.TypeCastTree;
+import com.sun.source.tree.VariableTree;
+import com.sun.tools.javac.code.Symbol;
+import com.sun.tools.javac.code.Symtab;
+import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.tree.JCTree;
+import com.sun.tools.javac.tree.TreeInfo;
+import com.sun.tools.javac.tree.TreeMaker;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.Names;
+
+/**
+ * The TreeBuilder permits the creation of new AST Trees using the
+ * non-public Java compiler API TreeMaker.
+ */
+
+public class TreeBuilder {
+    protected final Elements elements;
+    protected final Types modelTypes;
+    protected final com.sun.tools.javac.code.Types javacTypes;
+    protected final TreeMaker maker;
+    protected final Names names;
+    protected final Symtab symtab;
+    protected final ProcessingEnvironment env;
+
+    public TreeBuilder(ProcessingEnvironment env) {
+        this.env = env;
+        Context context = ((JavacProcessingEnvironment)env).getContext();
+        elements = env.getElementUtils();
+        modelTypes = env.getTypeUtils();
+        javacTypes = com.sun.tools.javac.code.Types.instance(context);
+        maker = TreeMaker.instance(context);
+        names = Names.instance(context);
+        symtab = Symtab.instance(context);
+    }
+
+    /**
+     * Builds an AST Tree to access the iterator() method of some iterable
+     * expression.
+     *
+     * @param iterableExpr  an expression whose type is a subtype of Iterable
+     * @return  a MemberSelectTree that accesses the iterator() method of
+     *    the expression
+     */
+    public MemberSelectTree buildIteratorMethodAccess(ExpressionTree iterableExpr) {
+        DeclaredType exprType =
+            (DeclaredType)TypesUtils.upperBound(InternalUtils.typeOf(iterableExpr));
+        assert exprType != null : "expression must be of declared type Iterable<>";
+
+        TypeElement exprElement = (TypeElement)exprType.asElement();
+
+        // Find the iterator() method of the iterable type
+        Symbol.MethodSymbol iteratorMethod = null;
+
+        for (ExecutableElement method :
+                 ElementFilter.methodsIn(elements.getAllMembers(exprElement))) {
+            Name methodName = method.getSimpleName();
+
+            if (method.getParameters().size() == 0) {
+                if (methodName.contentEquals("iterator")) {
+                    iteratorMethod = (Symbol.MethodSymbol)method;
+                }
+            }
+        }
+
+        assert iteratorMethod != null : "no iterator method declared for expression type";
+
+        Type.MethodType methodType = (Type.MethodType)iteratorMethod.asType();
+        Symbol.TypeSymbol methodClass = methodType.asElement();
+        DeclaredType iteratorType = (DeclaredType)methodType.getReturnType();
+        TypeMirror elementType;
+
+        if (iteratorType.getTypeArguments().size() > 0) {
+            elementType = iteratorType.getTypeArguments().get(0);
+            // Remove captured type from a wildcard.
+            if (elementType instanceof Type.CapturedType) {
+                elementType = ((Type.CapturedType)elementType).wildcard;
+            }
+
+            iteratorType =
+                modelTypes.getDeclaredType((TypeElement)modelTypes.asElement(iteratorType),
+                                      elementType);
+        }
+
+
+        // Replace the iterator method's generic return type with
+        // the actual element type of the expression.
+        Type.MethodType updatedMethodType =
+            new Type.MethodType(com.sun.tools.javac.util.List.<Type>nil(),
+                                (Type)iteratorType,
+                                com.sun.tools.javac.util.List.<Type>nil(),
+                                methodClass);
+
+        JCTree.JCFieldAccess iteratorAccess =
+            (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)iterableExpr,
+                         iteratorMethod);
+        iteratorAccess.setType(updatedMethodType);
+
+        return iteratorAccess;
+    }
+
+    /**
+     * Builds an AST Tree to access the hasNext() method of an iterator.
+     *
+     * @param iteratorExpr  an expression whose type is a subtype of Iterator
+     * @return  a MemberSelectTree that accesses the hasNext() method of
+     *    the expression
+     */
+    public MemberSelectTree buildHasNextMethodAccess(ExpressionTree iteratorExpr) {
+        DeclaredType exprType = (DeclaredType)InternalUtils.typeOf(iteratorExpr);
+        assert exprType != null : "expression must be of declared type Iterator<>";
+
+        TypeElement exprElement = (TypeElement)exprType.asElement();
+
+        // Find the hasNext() method of the iterator type
+        Symbol.MethodSymbol hasNextMethod = null;
+
+        for (ExecutableElement method :
+                 ElementFilter.methodsIn(elements.getAllMembers(exprElement))) {
+            Name methodName = method.getSimpleName();
+
+            if (method.getParameters().size() == 0) {
+                if (methodName.contentEquals("hasNext")) {
+                    hasNextMethod = (Symbol.MethodSymbol)method;
+                }
+            }
+        }
+
+        assert hasNextMethod != null : "no hasNext method declared for expression type";
+
+        JCTree.JCFieldAccess hasNextAccess =
+            (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)iteratorExpr,
+                         hasNextMethod);
+        hasNextAccess.setType(hasNextMethod.asType());
+
+        return hasNextAccess;
+    }
+
+    /**
+     * Builds an AST Tree to access the next() method of an iterator.
+     *
+     * @param iteratorExpr  an expression whose type is a subtype of Iterator
+     * @return  a MemberSelectTree that accesses the next() method of
+     *    the expression
+     */
+    public MemberSelectTree buildNextMethodAccess(ExpressionTree iteratorExpr) {
+        DeclaredType exprType = (DeclaredType)InternalUtils.typeOf(iteratorExpr);
+        assert exprType != null : "expression must be of declared type Iterator<>";
+
+        TypeElement exprElement = (TypeElement)exprType.asElement();
+
+        // Find the next() method of the iterator type
+        Symbol.MethodSymbol nextMethod = null;
+
+        for (ExecutableElement method :
+                 ElementFilter.methodsIn(elements.getAllMembers(exprElement))) {
+            Name methodName = method.getSimpleName();
+
+            if (method.getParameters().size() == 0) {
+                if (methodName.contentEquals("next")) {
+                    nextMethod = (Symbol.MethodSymbol)method;
+                }
+            }
+        }
+
+        assert nextMethod != null : "no next method declared for expression type";
+
+        Type.MethodType methodType = (Type.MethodType)nextMethod.asType();
+        Symbol.TypeSymbol methodClass = methodType.asElement();
+        Type elementType;
+
+        if (exprType.getTypeArguments().size() > 0) {
+            elementType = (Type)exprType.getTypeArguments().get(0);
+        } else {
+            elementType = symtab.objectType;
+        }
+
+        // Replace the next method's generic return type with
+        // the actual element type of the expression.
+        Type.MethodType updatedMethodType =
+            new Type.MethodType(com.sun.tools.javac.util.List.<Type>nil(),
+                                elementType,
+                                com.sun.tools.javac.util.List.<Type>nil(),
+                                methodClass);
+
+        JCTree.JCFieldAccess nextAccess =
+            (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)iteratorExpr,
+                         nextMethod);
+        nextAccess.setType(updatedMethodType);
+
+        return nextAccess;
+    }
+
+    /**
+     * Builds an AST Tree to dereference the length field of an array
+     *
+     * @param expression  the array expression whose length is being accessed
+     * @return  a MemberSelectTree to dereference the length of the array
+     */
+    public MemberSelectTree buildArrayLengthAccess(ExpressionTree expression) {
+
+        return (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)expression, symtab.lengthVar);
+    }
+
+    /**
+     * Builds an AST Tree to call a method designated by the argument expression.
+     *
+     * @param methodExpr  an expression denoting a method with no arguments
+     * @return  a MethodInvocationTree to call the argument method
+     */
+    public MethodInvocationTree buildMethodInvocation(ExpressionTree methodExpr) {
+        return maker.App((JCTree.JCExpression)methodExpr);
+    }
+
+    /**
+     * Builds an AST Tree to call a method designated by methodExpr,
+     * with one argument designated by argExpr.
+     *
+     * @param methodExpr  an expression denoting a method with one argument
+     * @param argExpr  an expression denoting an argument to the method
+     * @return  a MethodInvocationTree to call the argument method
+     */
+    public MethodInvocationTree buildMethodInvocation(ExpressionTree methodExpr,
+            ExpressionTree argExpr) {
+        return maker.App((JCTree.JCExpression)methodExpr,
+                com.sun.tools.javac.util.List.of((JCTree.JCExpression)argExpr));
+    }
+
+    /**
+     * Builds an AST Tree to declare and initialize a variable, with no modifiers.
+     *
+     * @param type  the type of the variable
+     * @param name  the name of the variable
+     * @param owner  the element containing the new symbol
+     * @param initializer  the initializer expression
+     * @return  a VariableDeclTree declaring the new variable
+     */
+    public VariableTree buildVariableDecl(TypeMirror type,
+                                          String name,
+                                          Element owner,
+                                          ExpressionTree initializer) {
+        DetachedVarSymbol sym =
+            new DetachedVarSymbol(0, names.fromString(name),
+                                  (Type)type, (Symbol)owner);
+        VariableTree tree = maker.VarDef(sym, (JCTree.JCExpression)initializer);
+        sym.setDeclaration(tree);
+        return tree;
+    }
+
+    /**
+     * Builds an AST Tree to declare and initialize a variable.  The
+     * type of the variable is specified by a Tree.
+     *
+     * @param type  the type of the variable, as a Tree
+     * @param name  the name of the variable
+     * @param owner  the element containing the new symbol
+     * @param initializer  the initializer expression
+     * @return  a VariableDeclTree declaring the new variable
+     */
+    public VariableTree buildVariableDecl(Tree type,
+                                          String name,
+                                          Element owner,
+                                          ExpressionTree initializer) {
+        Type typeMirror = (Type)InternalUtils.typeOf(type);
+        DetachedVarSymbol sym =
+            new DetachedVarSymbol(0, names.fromString(name),
+                                  typeMirror, (Symbol)owner);
+        JCTree.JCModifiers mods = maker.Modifiers(0);
+        JCTree.JCVariableDecl decl = maker.VarDef(mods, sym.name,
+                                                  (JCTree.JCExpression)type,
+                                                  (JCTree.JCExpression)initializer);
+        decl.setType(typeMirror);
+        decl.sym = sym;
+        sym.setDeclaration(decl);
+        return decl;
+    }
+
+    /**
+     * Builds an AST Tree to refer to a variable.
+     *
+     * @param decl  the declaration of the variable
+     * @return  an IdentifierTree to refer to the variable
+     */
+    public IdentifierTree buildVariableUse(VariableTree decl) {
+        return (IdentifierTree)maker.Ident((JCTree.JCVariableDecl)decl);
+    }
+
+    /**
+     * Builds an AST Tree to cast the type of an expression.
+     *
+     * @param type  the type to cast to
+     * @param expr  the expression to be cast
+     * @return  a cast of the expression to the type
+     */
+    public TypeCastTree buildTypeCast(TypeMirror type,
+                                      ExpressionTree expr) {
+        return maker.TypeCast((Type)type, (JCTree.JCExpression)expr);
+    }
+
+    /**
+     * Builds an AST Tree to assign an expression to a variable.
+     *
+     * @param variable  the declaration of the variable to assign to
+     * @param expr      the expression to be assigned
+     * @return  a statement assigning the expression to the variable
+     */
+    public StatementTree buildAssignment(VariableTree variable,
+                                         ExpressionTree expr) {
+        return maker.Assignment(TreeInfo.symbolFor((JCTree)variable),
+                                (JCTree.JCExpression)expr);
+    }
+
+    /**
+     * Builds an AST Tree to assign an RHS expression to an LHS expression.
+     *
+     * @param lhs  the expression to be assigned to
+     * @param rhs  the expression to be assigned
+     * @return  a statement assigning the expression to the variable
+     */
+    public AssignmentTree buildAssignment(ExpressionTree lhs,
+                                          ExpressionTree rhs) {
+        JCTree.JCAssign assign =
+            maker.Assign((JCTree.JCExpression)lhs, (JCTree.JCExpression)rhs);
+        assign.setType((Type)InternalUtils.typeOf(lhs));
+        return assign;
+    }
+
+    /**
+     * Builds an AST Tree representing a literal value of primitive
+     * or String type.
+     */
+    public LiteralTree buildLiteral(Object value) {
+        return maker.Literal(value);
+    }
+
+    /**
+     * Builds an AST Tree to compare two operands with less than.
+     *
+     * @param left  the left operand tree
+     * @param right  the right operand tree
+     * @return  a Tree representing "left &lt; right"
+     */
+    public BinaryTree buildLessThan(ExpressionTree left, ExpressionTree right) {
+        JCTree.JCBinary binary =
+            maker.Binary(JCTree.Tag.LT, (JCTree.JCExpression)left,
+                         (JCTree.JCExpression)right);
+        binary.setType((Type)modelTypes.getPrimitiveType(TypeKind.BOOLEAN));
+        return binary;
+    }
+
+    /**
+     * Builds an AST Tree to dereference an array.
+     *
+     * @param array  the array to dereference
+     * @param index  the index at which to dereference
+     * @return  a Tree representing the dereference
+     */
+    public ArrayAccessTree buildArrayAccess(ExpressionTree array,
+                                            ExpressionTree index) {
+        ArrayType arrayType = (ArrayType)InternalUtils.typeOf(array);
+        JCTree.JCArrayAccess access =
+            maker.Indexed((JCTree.JCExpression)array, (JCTree.JCExpression)index);
+        access.setType((Type)arrayType.getComponentType());
+        return access;
+    }
+
+    /**
+     * Builds an AST Tree to refer to a class name.
+     *
+     * @param elt  an element representing the class
+     * @return  an IdentifierTree referring to the class
+     */
+    public IdentifierTree buildClassUse(Element elt) {
+        return maker.Ident((Symbol)elt);
+    }
+
+    /**
+     * Builds an AST Tree to access the valueOf() method of boxed type
+     * such as Short or Float.
+     *
+     * @param expr  an expression whose type is a boxed type
+     * @return  a MemberSelectTree that accesses the valueOf() method of
+     *    the expression
+     */
+    public MemberSelectTree buildValueOfMethodAccess(Tree expr) {
+        TypeMirror boxedType = InternalUtils.typeOf(expr);
+
+        assert TypesUtils.isBoxedPrimitive(boxedType);
+
+        // Find the valueOf(unboxedType) method of the boxed type
+        Symbol.MethodSymbol valueOfMethod = getValueOfMethod(env, boxedType);
+
+        Type.MethodType methodType = (Type.MethodType)valueOfMethod.asType();
+
+        JCTree.JCFieldAccess valueOfAccess =
+            (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)expr, valueOfMethod);
+        valueOfAccess.setType(methodType);
+
+        return valueOfAccess;
+    }
+
+    /**
+     * Returns the valueOf method of a boxed type such as Short or Float.
+     */
+    public static Symbol.MethodSymbol getValueOfMethod(ProcessingEnvironment env, TypeMirror boxedType) {
+        Symbol.MethodSymbol valueOfMethod = null;
+
+        TypeMirror unboxedType = env.getTypeUtils().unboxedType(boxedType);
+        TypeElement boxedElement = (TypeElement)((DeclaredType)boxedType).asElement();
+        for (ExecutableElement method :
+                 ElementFilter.methodsIn(env.getElementUtils().getAllMembers(boxedElement))) {
+            Name methodName = method.getSimpleName();
+
+            if (methodName.contentEquals("valueOf")) {
+                List<? extends VariableElement> params = method.getParameters();
+                if (params.size() == 1 && env.getTypeUtils().isSameType(params.get(0).asType(), unboxedType)) {
+                    valueOfMethod = (Symbol.MethodSymbol)method;
+                }
+            }
+        }
+
+        assert valueOfMethod != null : "no valueOf method declared for boxed type";
+        return valueOfMethod;
+    }
+
+    /**
+     * Builds an AST Tree to access the *Value() method of a
+     * boxed type such as Short or Float, where * is the corresponding
+     * primitive type (i.e. shortValue or floatValue).
+     *
+     * @param expr  an expression whose type is a boxed type
+     * @return  a MemberSelectTree that accesses the *Value() method of
+     *    the expression
+     */
+    public MemberSelectTree buildPrimValueMethodAccess(Tree expr) {
+        TypeMirror boxedType = InternalUtils.typeOf(expr);
+        TypeElement boxedElement = (TypeElement)((DeclaredType)boxedType).asElement();
+
+        assert TypesUtils.isBoxedPrimitive(boxedType);
+        TypeMirror unboxedType = modelTypes.unboxedType(boxedType);
+
+        // Find the *Value() method of the boxed type
+        String primValueName = unboxedType.toString() + "Value";
+        Symbol.MethodSymbol primValueMethod = null;
+
+        for (ExecutableElement method :
+                 ElementFilter.methodsIn(elements.getAllMembers(boxedElement))) {
+            Name methodName = method.getSimpleName();
+
+            if (methodName.contentEquals(primValueName) &&
+                method.getParameters().size() == 0) {
+                primValueMethod = (Symbol.MethodSymbol)method;
+            }
+        }
+
+        assert primValueMethod != null : "no *Value method declared for boxed type";
+
+        Type.MethodType methodType = (Type.MethodType)primValueMethod.asType();
+
+        JCTree.JCFieldAccess primValueAccess =
+            (JCTree.JCFieldAccess)
+            maker.Select((JCTree.JCExpression)expr, primValueMethod);
+        primValueAccess.setType(methodType);
+
+        return primValueAccess;
+    }
+
+    /**
+     * Map public AST Tree.Kinds to internal javac JCTree.Tags.
+     */
+    public JCTree.Tag kindToTag(Tree.Kind kind) {
+        switch (kind) {
+        case AND:
+            return JCTree.Tag.BITAND;
+        case AND_ASSIGNMENT:
+            return JCTree.Tag.BITAND_ASG;
+        case ANNOTATION:
+            return JCTree.Tag.ANNOTATION;
+        case ANNOTATION_TYPE:
+            return JCTree.Tag.TYPE_ANNOTATION;
+        case ARRAY_ACCESS:
+            return JCTree.Tag.INDEXED;
+        case ARRAY_TYPE:
+            return JCTree.Tag.TYPEARRAY;
+        case ASSERT:
+            return JCTree.Tag.ASSERT;
+        case ASSIGNMENT:
+            return JCTree.Tag.ASSIGN;
+        case BITWISE_COMPLEMENT:
+            return JCTree.Tag.COMPL;
+        case BLOCK:
+            return JCTree.Tag.BLOCK;
+        case BREAK:
+            return JCTree.Tag.BREAK;
+        case CASE:
+            return JCTree.Tag.CASE;
+        case CATCH:
+            return JCTree.Tag.CATCH;
+        case CLASS:
+            return JCTree.Tag.CLASSDEF;
+        case CONDITIONAL_AND:
+            return JCTree.Tag.AND;
+        case CONDITIONAL_EXPRESSION:
+            return JCTree.Tag.CONDEXPR;
+        case CONDITIONAL_OR:
+            return JCTree.Tag.OR;
+        case CONTINUE:
+            return JCTree.Tag.CONTINUE;
+        case DIVIDE:
+            return JCTree.Tag.DIV;
+        case DIVIDE_ASSIGNMENT:
+            return JCTree.Tag.DIV_ASG;
+        case DO_WHILE_LOOP:
+            return JCTree.Tag.DOLOOP;
+        case ENHANCED_FOR_LOOP:
+            return JCTree.Tag.FOREACHLOOP;
+        case EQUAL_TO:
+            return JCTree.Tag.EQ;
+        case EXPRESSION_STATEMENT:
+            return JCTree.Tag.EXEC;
+        case FOR_LOOP:
+            return JCTree.Tag.FORLOOP;
+        case GREATER_THAN:
+            return JCTree.Tag.GT;
+        case GREATER_THAN_EQUAL:
+            return JCTree.Tag.GE;
+        case IDENTIFIER:
+            return JCTree.Tag.IDENT;
+        case IF:
+            return JCTree.Tag.IF;
+        case IMPORT:
+            return JCTree.Tag.IMPORT;
+        case INSTANCE_OF:
+            return JCTree.Tag.TYPETEST;
+        case LABELED_STATEMENT:
+            return JCTree.Tag.LABELLED;
+        case LEFT_SHIFT:
+            return JCTree.Tag.SL;
+        case LEFT_SHIFT_ASSIGNMENT:
+            return JCTree.Tag.SL_ASG;
+        case LESS_THAN:
+            return JCTree.Tag.LT;
+        case LESS_THAN_EQUAL:
+            return JCTree.Tag.LE;
+        case LOGICAL_COMPLEMENT:
+            return JCTree.Tag.NOT;
+        case MEMBER_SELECT:
+            return JCTree.Tag.SELECT;
+        case METHOD:
+            return JCTree.Tag.METHODDEF;
+        case METHOD_INVOCATION:
+            return JCTree.Tag.APPLY;
+        case MINUS:
+            return JCTree.Tag.MINUS;
+        case MINUS_ASSIGNMENT:
+            return JCTree.Tag.MINUS_ASG;
+        case MODIFIERS:
+            return JCTree.Tag.MODIFIERS;
+        case MULTIPLY:
+            return JCTree.Tag.MUL;
+        case MULTIPLY_ASSIGNMENT:
+            return JCTree.Tag.MUL_ASG;
+        case NEW_ARRAY:
+            return JCTree.Tag.NEWARRAY;
+        case NEW_CLASS:
+            return JCTree.Tag.NEWCLASS;
+        case NOT_EQUAL_TO:
+            return JCTree.Tag.NE;
+        case OR:
+            return JCTree.Tag.BITOR;
+        case OR_ASSIGNMENT:
+            return JCTree.Tag.BITOR_ASG;
+        case PARENTHESIZED:
+            return JCTree.Tag.PARENS;
+        case PLUS:
+            return JCTree.Tag.PLUS;
+        case PLUS_ASSIGNMENT:
+            return JCTree.Tag.PLUS_ASG;
+        case POSTFIX_DECREMENT:
+            return JCTree.Tag.POSTDEC;
+        case POSTFIX_INCREMENT:
+            return JCTree.Tag.POSTINC;
+        case PREFIX_DECREMENT:
+            return JCTree.Tag.PREDEC;
+        case PREFIX_INCREMENT:
+            return JCTree.Tag.PREINC;
+        case REMAINDER:
+            return JCTree.Tag.MOD;
+        case REMAINDER_ASSIGNMENT:
+            return JCTree.Tag.MOD_ASG;
+        case RETURN:
+            return JCTree.Tag.RETURN;
+        case RIGHT_SHIFT:
+            return JCTree.Tag.SR;
+        case RIGHT_SHIFT_ASSIGNMENT:
+            return JCTree.Tag.SR_ASG;
+        case SWITCH:
+            return JCTree.Tag.SWITCH;
+        case SYNCHRONIZED:
+            return JCTree.Tag.SYNCHRONIZED;
+        case THROW:
+            return JCTree.Tag.THROW;
+        case TRY:
+            return JCTree.Tag.TRY;
+        case TYPE_CAST:
+            return JCTree.Tag.TYPECAST;
+        case TYPE_PARAMETER:
+            return JCTree.Tag.TYPEPARAMETER;
+        case UNARY_MINUS:
+            return JCTree.Tag.NEG;
+        case UNARY_PLUS:
+            return JCTree.Tag.POS;
+        case UNION_TYPE:
+            return JCTree.Tag.TYPEUNION;
+        case UNSIGNED_RIGHT_SHIFT:
+            return JCTree.Tag.USR;
+        case UNSIGNED_RIGHT_SHIFT_ASSIGNMENT:
+            return JCTree.Tag.USR_ASG;
+        case VARIABLE:
+            return JCTree.Tag.VARDEF;
+        case WHILE_LOOP:
+            return JCTree.Tag.WHILELOOP;
+        case XOR:
+            return JCTree.Tag.BITXOR;
+        case XOR_ASSIGNMENT:
+            return JCTree.Tag.BITXOR_ASG;
+        default:
+            return JCTree.Tag.NO_TAG;
+        }
+    }
+
+    /**
+     * Builds an AST Tree to perform a binary operation.
+     *
+     * @param type  result type of the operation
+     * @param op    AST Tree operator
+     * @param left  the left operand tree
+     * @param right  the right operand tree
+     * @return  a Tree representing "left &lt; right"
+     */
+    public BinaryTree buildBinary(TypeMirror type, Tree.Kind op, ExpressionTree left, ExpressionTree right) {
+        JCTree.Tag jcOp = kindToTag(op);
+        JCTree.JCBinary binary =
+            maker.Binary(jcOp, (JCTree.JCExpression)left,
+                         (JCTree.JCExpression)right);
+        binary.setType((Type)type);
+        return binary;
+    }
+
+}
diff --git a/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeParser.java b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeParser.java
new file mode 100644
index 0000000000..1ac9d09309
--- /dev/null
+++ b/third_party/checker_framework_javacutil/java/org/checkerframework/javacutil/trees/TreeParser.java
@@ -0,0 +1,144 @@
+package org.checkerframework.javacutil.trees;
+
+import java.util.StringTokenizer;
+
+import javax.annotation.processing.ProcessingEnvironment;
+
+import com.sun.source.tree.ExpressionTree;
+import com.sun.tools.javac.processing.JavacProcessingEnvironment;
+import com.sun.tools.javac.tree.JCTree.JCExpression;
+import com.sun.tools.javac.tree.TreeMaker;
+import com.sun.tools.javac.util.Context;
+import com.sun.tools.javac.util.List;
+import com.sun.tools.javac.util.ListBuffer;
+import com.sun.tools.javac.util.Names;
+
+/**
+ * A Utility class for parsing Java expression snippets, and converting them
+ * to proper Javac AST nodes.
+ *
+ * This is useful for parsing {@code EnsuresNonNull*},
+ * and {@code KeyFor} values.
+ *
+ * Currently, it handles four tree types only:
+ * <ul>
+ *  <li>Identifier tree (e.g. {@code id})</li>
+ *  <li>Literal tree (e.g. 2, 3)</li>
+ *  <li>Method invocation tree (e.g. {@code method(2, 3)})</li>
+ *  <li>Member select tree (e.g. {@code Class.field}, {@code instance.method()})
+ *  <li>Array access tree (e.g. {@code array[id]})</li>
+ * </ul>
+ *
+ * Notable limitation: Doesn't handle spaces, or non-method-argument
+ * parenthesis.
+ *
+ * It's implemented via a Recursive-Descend parser.
+ */
+public class TreeParser {
+    private static final String DELIMS = ".[](),";
+    private static final String SENTINAL = "";
+
+    private final TreeMaker maker;
+    private final Names names;
+
+    public TreeParser(ProcessingEnvironment env) {
+        Context context = ((JavacProcessingEnvironment)env).getContext();
+        maker = TreeMaker.instance(context);
+        names = Names.instance(context);
+    }
+
+    /**
+     * Parses the snippet in the string as an internal Javac AST expression
+     * node
+     *
+     * @param s the java snippet
+     * @return  the AST corresponding to the snippet
+     */
+    public ExpressionTree parseTree(String s) {
+        tokenizer = new StringTokenizer(s, DELIMS, true);
+        token = tokenizer.nextToken();
+
+        try {
+            return parseExpression();
+        } catch (Exception e) {
+            throw new ParseError(e);
+        } finally {
+            tokenizer = null;
+            token = null;
+        }
+    }
+
+    StringTokenizer tokenizer = null;
+    String token = null;
+
+    private String nextToken() {
+        token = tokenizer.hasMoreTokens() ? tokenizer.nextToken() : SENTINAL;
+        return token;
+    }
+
+    JCExpression fromToken(String token) {
+        // Optimization
+        if ("true".equals(token)) {
+            return maker.Literal(true);
+        } else if ("false".equals(token)) {
+            return maker.Literal(false);
+        }
+
+        if (Character.isLetter(token.charAt(0))) {
+            return maker.Ident(names.fromString(token));
+        }
+
+        Object value = null;
+        try {
+            value = Integer.valueOf(token);
+        } catch (Exception e2) { try {
+            value = Double.valueOf(token);
+        } catch (Exception ef) {}}
+        assert value != null;
+        return maker.Literal(value);
+    }
+
+    JCExpression parseExpression() {
+        JCExpression tree = fromToken(token);
+
+        while (tokenizer.hasMoreTokens()) {
+            String delim = nextToken();
+            if (".".equals(delim)) {
+                nextToken();
+                tree = maker.Select(tree,
+                        names.fromString(token));
+            } else if ("(".equals(delim)) {
+                nextToken();
+                ListBuffer<JCExpression> args = new ListBuffer<>();
+                while (!")".equals(token)) {
+                    JCExpression arg = parseExpression();
+                    args.append(arg);
+                    if (",".equals(token)) {
+                        nextToken();
+                    }
+                }
+                // For now, handle empty args only
+                assert ")".equals(token);
+                tree = maker.Apply(List.<JCExpression>nil(),
+                        tree, args.toList());
+            } else if ("[".equals(token)) {
+                nextToken();
+                JCExpression index = parseExpression();
+                assert "]".equals(token);
+                tree = maker.Indexed(tree, index);
+            } else {
+                return tree;
+            }
+        }
+
+        return tree;
+    }
+
+    class ParseError extends RuntimeException {
+        private static final long serialVersionUID = 1887754619522101929L;
+
+        ParseError(Throwable cause) {
+            super(cause);
+        }
+    }
+}