The Java Symbolic Simulator, part of SAW.
License: BSD 3-Clause "New" or "Revised" License
This repository contains the code for the Java Symbolic Simulator
(JSS). It is currently used primarily as a library from SAWScript, but
also produces a stand-alone executable, jss.
For information on using jss, see the tutorial in
doc/japi-tutorial.
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.
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.
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.
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.
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.
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 .
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.
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.
React
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
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
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.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.