Comments (9)
Hi @scg03
I am the guy @ericbodden was talking about. Instead of using a framework, I thought about how to create path constraints and solve them with a SMT solver. Since explaining my approach in detail would probably go beyond the scope of a single comment I try to wrap it up and give you a brief summary and explanation.
When you want to reason about a statement whether it can be reached or not, you have to find all possible paths to that statement and build for each path its corresponding constraints and solve them. To reduce the amount of computation time I start at the statement and go backwards in code. Whenever I encounter a new, unknown variable I introduce a new symbol which has no value itself and store the link between the variable and the symbol in a map. When you come across an assignment statement you have to indroduce yet again new symbols for each variable used in the right side of the assignment and update the symbol which belongs to the left side.
Put simply, you always introduce a new symbol when you do not know the value of a variable you stumble across. (note: not the concrete value but the symbolic one)
Since this may sound a little bit confusing and is kind of hard to express in written text I want to give you a short example:
Example
aVar = 0;
bVar = 42;
aVar = aVar + bVar - 1;
if (aVar == 42) anInteresstingStatement();
Assume we want to know whether anInteresstingStatement() can be reached or not, we start right there and go backwards.
statement | symbol-variable map | path constraints |
---|---|---|
anInteresstingStatement(); | [ ] | [ ] |
if (aVar == 42) | [ (a1) ] | [ ( a1 == 42 ) ] |
aVar = aVar + bVar - 1; | [ (a2), (a1 = a2 + b1 - 1), (b1) ] | [ ( a1 == 42 ) ] |
bVar = 42; | [ (a2), (a1 = a2 + b1 - 1), (b1 = 42) ] | [ ( a1 == 42 ) ] |
aVar = 0; | [ (a2 = 0), (a1 = a2 + b1 - 1), (b1 = 42) ] | [ ( a1 == 42 ) ] |
Since we will only find a single path constraint [ ( a1 == 42 ) ] a SMT solver will easily solve:
( 0 + 42 - 1 == 42 ) is not satisfiable and thus the statement cannot be reached.
I am converting my path constraints to SMT Lib 2.0 which allows me to use a large amount of SMT Solver.
You also have to care about other language constructs such as intra- and inter procedural calls, fields, array, lists, maps, objects, loops and many more.
I hope you get the idea of my approach and can start to work with this.
Best regards,
Robert
from soot.
any on-going project to implement this enhancement?
from soot.
Hi @scg03
We currently have a student integrating symbolic execution into Soot. It's almost finished. What exactly are you looking to do?
from soot.
Hi @ericbodden
I'm looking for a symbolic execution framework for Jimple and Google leaded me to this post. Are you using some existing framework? My plan is to modify CPAChecker to support Jimple.
from soot.
Hello,
When do you think the source code would be open to public?
Thanks,
Shakthi
from soot.
@sbachala2 We are currently publishing the algorithms in the form of a paper. Afterwards, we can discuss how we can disclose the algorithms and/or the code.
from soot.
Thank you for the information.
from soot.
Hi,
I'm interested how look like time plan for this pr.
@StevenArzt could you update status of yours publication and whether code will be disclosed ?
Thanks in advance,
Grzesiek
from soot.
hi, is there any new message about this topic?
from soot.
Related Issues (20)
- Array Index Out of Bounds during Instrumentation
- Does soot support generating jimple files for java>=17? HOT 2
- VisibilityLocalVariableAnnotationTag should provide type information
- VisibilityLocalVariableAnnotationTag should consider annotation target correctly
- How to include annotated classes into the analysis scope?
- java.lang.RuntimeException when ... HOT 1
- soot.SootResolver$SootClassNotFoundException when ...
- java.lang.NullPointerException when ...
- Analysis dex file that exists in the assets folder HOT 1
- JLookupSwitchStmt.toString java.lang.StackOverflowError
- soot.jimple.StaticFieldRef.getField() is null
- Detected non-deterministic results under various configurations HOT 1
- Skip analysis for erroring functions
- In the case of two nested IF statements, the IfStmt returns the wrong lineNumber
- Jimple parsing exception
- java.lang.VerifyError: Verifier rejected class xxx failed to verify: xxx [0x3F] copy1 v2<-v18 type=Integer cat=3 (declaration of 'xxx appears in /data/app/~~rhy3UPO5XTPJh8Mnsx2ouw==/com.awesomeproject-RQOu3jVjveEXAk0l7OyN0g==/base.apk!classes2.dex) HOT 1
- Fields missing in loaded classes from android.jar HOT 3
- Soot resolved an incorrect method signautre HOT 4
- Worker thread execution failed: Failed to apply jb to <com.google.firebase.snippets.FirebaseAuthSnippets: javax.ws.rs.core.Response clearSessionCookieAndRevoke(javax.ws.rs.core.Cookie)>
- Worker thread execution failed: Failed to apply jb to <com.google.firebase.snippets.FirebaseAuthSnippets: javax.ws.rs.core.Response clearSessionCookieAndRevoke(javax.ws.rs.core.Cookie)> HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 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.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
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.
from soot.