galoisinc / jvm-verifier Goto Github PK
View Code? Open in Web Editor NEWThe Java Symbolic Simulator, part of SAW.
License: BSD 3-Clause "New" or "Revised" License
The Java Symbolic Simulator, part of SAW.
License: BSD 3-Clause "New" or "Revised" License
Needs updating for support of Java9 and later, where the rt.jar
is replaced with the jrt:/
filesystem notation.
See https://openjdk.java.net/jeps/220 .
Also identified in GaloisInc/saw-script#861 .
The native System.arrayCopy
method in Java isn't currently supported by JSS, and as a native method can't be symbolically executed. We should add an override for it.
We originally developed the JVM .class
file parser with Java 6, and haven't extended it in a while. It can load some files generated from later versions, but not all. We should extend it to support all Java 8 constructs.
The AIGs generated by the Java API function Symbolic.writeAiger
assume definedness. Sometimes this is useful, but it would be convenient to allow generation of AIGs that include the definedness conditions as well.
JSS currently loads all .class files it can find below the current dir on start up. This can be very slow. Instead, we should load the .class files lazily as needed. Some relevant code in src/Verifier/Java/Codebase.hs
was updated in 0b0514f.
The native Arrays.copyOf
method in Java isn't currently supported by JSS, and as a native method can't be symbolically executed. We should add an override for it.
It appears that JSS can't handle switch
statements with more than one case
. I ran into this when I tried to add a new Java example to the tutorial in doc/tutorial/code/FFS.java
in the saw-script
repo and it made SAW crash:
static int ffs_imp2(int i) {
switch (((~i) + 1) ^ i) {
case 0b11111111111111111111111111111110: return 1;
case 0b11111111111111111111111111111100: return 2;
case 0b11111111111111111111111111111000: return 3;
case 0b11111111111111111111111111110000: return 4;
case 0b11111111111111111111111111100000: return 5;
case 0b11111111111111111111111111000000: return 6;
case 0b11111111111111111111111110000000: return 7;
case 0b11111111111111111111111100000000: return 8;
case 0b11111111111111111111111000000000: return 9;
case 0b11111111111111111111110000000000: return 10;
case 0b11111111111111111111100000000000: return 11;
case 0b11111111111111111111000000000000: return 12;
case 0b11111111111111111110000000000000: return 13;
case 0b11111111111111111100000000000000: return 14;
case 0b11111111111111111000000000000000: return 15;
case 0b11111111111111110000000000000000: return 16;
case 0b11111111111111100000000000000000: return 17;
case 0b11111111111111000000000000000000: return 18;
case 0b11111111111110000000000000000000: return 19;
case 0b11111111111100000000000000000000: return 20;
case 0b11111111111000000000000000000000: return 21;
case 0b11111111110000000000000000000000: return 22;
case 0b11111111100000000000000000000000: return 23;
case 0b11111111000000000000000000000000: return 24;
case 0b11111110000000000000000000000000: return 25;
case 0b11111100000000000000000000000000: return 26;
case 0b11111000000000000000000000000000: return 27;
case 0b11110000000000000000000000000000: return 28;
case 0b11100000000000000000000000000000: return 29;
case 0b11000000000000000000000000000000: return 30;
case 0b10000000000000000000000000000000: return 31;
case 0b00000000000000000000000000000000: return i == 0 ? 0 : 32;
}
return 0; // Unreachable.
}
Here are simple crashing and non-crashing examples:
// Crash.
static int ffs_imp3_4(int i) {
switch (i) {
case 0: break;
case 1: break;
}
return 0;
}
// No crash, compare bytecode with ffs_imp3_4.
static int ffs_imp3(int i) {
switch (i) {
case 0: break;
}
return 0;
}
And here is the corresponding Java bytecode -- extracted with javap -c FFS
-- which is what JSS is actually processing. Crash:
static int ffs_imp3_4(int);
Code:
0: iload_0
1: lookupswitch { // 2
0: 28
1: 31
default: 31
}
28: goto 31
31: iconst_0
32: ireturn
No crash:
static int ffs_imp3(int);
Code:
0: iload_0
1: lookupswitch { // 1
0: 20
default: 20
}
20: iconst_0
21: ireturn
The lookupswitch
JVM bytecode is processed by switch
in src/Data/JVM/Symbolic/Translation.hs
, and the problem manifests as an empty stack pop in popValue
in src/Verifier/Java/Simulator.hs
.
I pushed a debug-broken-java-switch-statements
branch with these examples and some printf debugging inserted; I got side tracked failing to build SAW with profiling support to get stack traces. Run saw ffs_java.saw
to see the crash.
Using the word backend results in different AIG output than the SAW backend. This is related, I believe, to different assumptions regarding bit-order; the word backend operates least-significant-bit-first, but the SAW backend conforms to the Cryptol 2 semantics, which is most-significant-bit-first.
There may be other related issues where bit-ordering assumptions affect the results; these should also be teased out.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.