Permalink
Browse files

initial import

  • Loading branch information...
0 parents commit 8f0cd175183d33cc175602aed68256a49644f072 @krestenkrab committed Dec 5, 2009
Showing with 8,083 additions and 0 deletions.
  1. +340 −0 COPYING
  2. +100 −0 README
  3. +72 −0 src/verify/ClassFileInfo.java
  4. +309 −0 src/verify/Tool.java
  5. +32 −0 src/verify/VerificationException.java
  6. +975 −0 src/verify/bytecode/AbstractState.java
  7. +154 −0 src/verify/bytecode/AbstractStateQueue.java
  8. +2,075 −0 src/verify/bytecode/BytecodeVerifier.java
  9. +442 −0 src/verify/bytecode/InsnNames.java
  10. +248 −0 src/verify/classfile/ClassFile.java
  11. +79 −0 src/verify/classfile/ClassFileConstants.java
  12. +559 −0 src/verify/classfile/ClassFileParser.java
  13. +295 −0 src/verify/classfile/ConstantPool.java
  14. +174 −0 src/verify/classfile/n2h.java
  15. +135 −0 src/verify/notes.txt
  16. +78 −0 src/verify/path/CacheEntry.java
  17. +156 −0 src/verify/path/DirectoryPathEntry.java
  18. +66 −0 src/verify/path/PathEntry.java
  19. +218 −0 src/verify/path/SearchPath.java
  20. +80 −0 src/verify/path/URLPathEntry.java
  21. +104 −0 src/verify/path/ZipPathEntry.java
  22. +33 −0 src/verify/test/Test.java
  23. +39 −0 src/verify/test/Test2.java
  24. +83 −0 src/verify/type/AddressType.java
  25. +106 −0 src/verify/type/ArrayType.java
  26. +75 −0 src/verify/type/BasicType.java
  27. +44 −0 src/verify/type/ClassInfo.java
  28. +31 −0 src/verify/type/ClassInfoProvider.java
  29. +271 −0 src/verify/type/ClassType.java
  30. +31 −0 src/verify/type/IllegalTypeNameException.java
  31. +64 −0 src/verify/type/IncompatibleTypesException.java
  32. +78 −0 src/verify/type/NewObjectType.java
  33. +40 −0 src/verify/type/NullType.java
  34. +105 −0 src/verify/type/Signature.java
  35. +137 −0 src/verify/type/Type.java
  36. +186 −0 src/verify/type/TypeContext.java
  37. +69 −0 src/verify/type/TypeTags.java
340 COPYING

Large diffs are not rendered by default.

Oops, something went wrong.
100 README
@@ -0,0 +1,100 @@
+
+
+ Kresten's Verifier for Java Byte Codes
+ ======================================
+
+
+ The interface to the verifier is currently very crude.
+ To run it, type
+
+ prompt> java verify.Tool class-or-file-name ...
+
+ If you give it a name of a class file, it will try to figure out
+ the corresponding class name, (removing leading "./", and
+ terminating ".class", and replace '.' with the path seperator).
+
+ To start off, you may want to verify the verifier. On unix, you can
+ write something like this,
+
+ prompt> java verify.Tool `find verify/ -name '*.class'`
+
+
+ As it runs, it will print a '.' for each method checked, and a '#'
+ whenever it loads extra auxillary classes needed.
+
+
+ It has two interesting options.
+
+ --classpath=PATH
+
+ Where path is a : or ; separated path (according to the java
+ property "path.separator"). This specifies the "class path" from
+ which to load classes. The classpath defaults to whatever the Java
+ Runtime decides to make available in the java.class.path property.
+
+ The verifier does not use the Java system's class loader. Rather,
+ it incorporates it's own loading mechanism which is more
+ ligh-weight. Also you don't really need to "load" classes in order
+ to verify them.
+
+
+ The second interesting option is
+
+ --verbose=true
+
+ which will make the verifier print a line of information for each
+ instruction checked. (or perhaps this is just to be considered my
+ debugging output...) It might look like this:
+
+ --[151]----------
+ (##) <[#JXJX#I#I????????> pc=151 new
+ (##@) <[#JXJX#I#I????????> pc=154 dup
+ (##@@) <[#JXJX#I#I????????> pc=155 iconst_1
+ (##@@I) <[#JXJX#I#I????????> pc=156 invokespecial
+ calling java/lang/Boolean.<init> (boolean) void
+
+ For a given sequence of four instructions. The --[151]---- marks
+ an entrypoint for a basic block. The part on the left, in
+ parentheses describes the state of the stack at this particular
+ instruction. Each character represents one "stack item". The
+ right-most element is the top of the stack. Generally, these are
+ the same as the characters encoding types in a field descriptor,
+ "I" is integer, "J" is long, "D" is double and so on. Special are
+ however "X", representing the second half of a long, and "Q", the
+ same thing for doubles. "#" is a normal object, "@" is an
+ uninitialized object (one for which a constructor has not yet been
+ called) and "[" is an array. (See types/TypeTags.java for the full
+ list)
+
+ On the right, in angle brackets, is the "state" of the local
+ variables. These are represented using the same characters as
+ before. Location, which have yet to be assigned a value, are
+ marked with "?". One of the jobs of the verifier is to make sure
+ that such a location is never being read.
+
+ Finally, on the right, you see the current pc (program counter) and
+ the symbolic name of the opcode being checked.
+
+ When the bytecode verifier detects an error, and you did not choose
+ the --verbose=true option already, it will turn it on for you, and
+ re-check the very same method.
+
+ Right now, the interface is rather crude. If you get no specific
+ messages, that means that your code did verify.
+
+
+
+ As a consequence of the way it works, it may discover unreachable
+ code in the instruction sequence. I have not seen javac-generated
+ code with unreachable instructions, but several other compilers
+ produce them all over. In specific, IBM's Jikes compiler does.
+ When the verifier discovers such a sequence, it will print a
+ message like
+
+ unreachable in fooBar(): 3417+4, 7732+2
+
+ Where the +X means how many bytes onward in the byte sequence to
+ find the unreachable code.
+
+
+
@@ -0,0 +1,72 @@
+/*
+ * ClassFileInfo.java -- give ClassFile's ClassInfo interface
+ *
+ * Copyright (C) 1999 by Kresten Krab Thorup <krab@daimi.au.dk>
+ *
+ * This file is part of "Kresten's Verifier for Java Byte Codes"
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Library General Public
+ * License as published by the Free Software Foundation; either
+ * version 2 of the License, or (at your option) any later version.
+ *
+ * This library 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
+ * Library General Public License for more details.
+ *
+ * You should have received a copy of the GNU Library General Public
+ * License along with this library; if not, write to the Free
+ * Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA
+ *
+ */
+
+
+package verify;
+
+import verify.classfile.ClassFile;
+import verify.type.ClassInfo;
+
+public class ClassFileInfo implements ClassInfo {
+
+ private final ClassFile file;
+
+ public ClassFileInfo (ClassFile c) { file = c; }
+
+ public int getAccessFlags ()
+ {
+ return file.access_flags;
+ }
+
+ public String getClassName ()
+ {
+ return file.pool.get_class (file.this_class);
+ }
+
+ public String getSuperClassName ()
+ {
+ if (file.super_class != 0)
+ return file.pool.get_class (file.super_class);
+ else
+ return null;
+ }
+
+ public String[] getSuperInterfaceNames ()
+ {
+ if (file.interfaces_count == 0)
+ return null;
+
+ String[] result = new String[file.interfaces_count];
+ for (int i = 0; i < file.interfaces_count; i++)
+ {
+ result[i] = file.pool.get_class (file.interfaces[i]);
+ }
+
+ return result;
+ }
+
+
+}
+
+
Oops, something went wrong.

0 comments on commit 8f0cd17

Please sign in to comment.