Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Java support #125

Merged
merged 103 commits into from
Feb 8, 2019
Merged

Java support #125

merged 103 commits into from
Feb 8, 2019

Conversation

Phat3
Copy link
Member

@Phat3 Phat3 commented Jan 27, 2019

Add support for Java bytecode analysis using string constraints

@Phat3 Phat3 requested a review from ltfish January 27, 2019 06:47
zardus
zardus requested changes Jan 27, 2019
View reviewed changes
Copy link
Member

@zardus zardus left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Amazing! I added a few comments throughout, if you could take a look.

Excited to get this merged!

claripy/ast/base.py Outdated Show resolved Hide resolved
claripy/backends/__init__.py Outdated Show resolved Hide resolved
claripy/frontends/portfolio_frontend.py Outdated Show resolved Hide resolved
claripy/backends/__init__.py Show resolved Hide resolved
ltfish
ltfish requested changes Feb 4, 2019
View reviewed changes
claripy/__init__.py Outdated Show resolved Hide resolved
claripy/ast/strings.py Outdated Show resolved Hide resolved
claripy/ast/strings.py Outdated Show resolved Hide resolved
claripy/backends/__init__.py Outdated Show resolved Hide resolved
claripy/backends/backend_concrete.py Outdated Show resolved Hide resolved
claripy/operations.py Outdated Show resolved Hide resolved
claripy/simplifications.py Outdated Show resolved Hide resolved
claripy/smtlib_utils.py Outdated Show resolved Hide resolved
tests/test_backend_smt.py Show resolved Hide resolved
tests/test_solver.py Outdated Show resolved Hide resolved
Phat3 and others added 27 commits February 8, 2019 00:02
@Phat3 @ltfish
Add dummy concat operation with strings
42f9954 
Addedd a dummy concat operation fro strings (both symbolic and concrete) in order
to understand the entire calling chain in claripy

Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add Extract operation for strings
3d125f4 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Fix typo during find/replace
64baa25 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add equality/inequality operations for strings
db4150f 
Added all the equality (=) and inequality (<, >, !=, ...) operations for strings.
Now the AST is constructed in a correct way for all these operations.

Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Implemented full chain for constraint dump in smt format
9f3ce4a 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add support for multiple constraints
ce2189f 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add substr operation on concrete strings
740dbe6 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add support for string replace
25c8037 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add concrete simplification for replace and substr
ce67f7a 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add simplification for strconcat
0ad4e4d 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Removed TODOs
d1a1bf3 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Working on length constraint
9a44a65 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add not equal operation for strings
35cbac1 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Lukas-Dresel @ltfish
start of CVC4 backend
9c61b27
@Phat3 @ltfish
Add length constraint on strings
db6e370 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Lukas-Dresel @ltfish
moved general smtlib things back to smt backend
e6a4f6c
@Phat3 @ltfish
Add input normalization during equality check
d2800dc 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add manage of extra_constraints in get_smtlib_script_satisfiability
ea447ab 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add Or operation dumnp in smt format
34f2191 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add LT, GE, GT, LE comparison dump in SMT format
ffe9b0e 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add StrContains and simplification
1b5cc91 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Lukas-Dresel @ltfish
solving kind of works now using CVC4
6588c3b
@Lukas-Dresel @ltfish
added expected test cases for the CVC4 backend
584394c
@Lukas-Dresel @ltfish
made the solver_required argument able to be passed through
bcdbb96
@Lukas-Dresel @ltfish
added solver requirement to CVC4 backend
9c6629d
@Phat3 @ltfish
Moving away assertion_stack
ea38b01 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Removed completely assertion stack
4b115b6 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
Lukas-Dresel and others added 17 commits February 8, 2019 00:22
@Lukas-Dresel @ltfish
made claripy aware of actual solver response, as in SAT/UNSAT/UNKNOWN
fbb71a0
@Lukas-Dresel @ltfish
added composite solver tests
08e5835
@Phat3 @ltfish
REmoved dummy string reverse operation
cba82eb
@Phat3 @ltfish
Ported to py3k... but problem with pysmt parsing during get_model [us…
fec5a7c 
…e z3 4.8 at least]

Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Porting to py3k done
31ed01c 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add isDigit operation for strings and test cases
0cb444d 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add IntToStr operation and test cases
4593077 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add And and Not operations
11722c3 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@conand @ltfish
Implement lazy spawning and process terminate
46970b2
@conand @ltfish
BV from Bool
fb6e180
@Phat3 @ltfish
Add pysmt as claripy dependency
5dcb044 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add warning suppression hacky fix
45740ee 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
CVC4 bundled inside claripy
78dffdd 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Add cvc4 as a python dependency
6e07cac 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Remove useless field from ast.base.py
fa074dd 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Fix code style comment
c96f0d1 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@Phat3 @ltfish
Removed portfolio solver
88cfdd6 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
Phat3 and others added 2 commits February 8, 2019 00:31
@Phat3 @ltfish
Remove optional class from all smt backends
1c87be2 
Signed-off-by: Sebastiano Mariani <mariani.sebastiano@gmail.com>
@ltfish
Remove DeclareConst.
789f8c0
@ltfish ltfish self-assigned this Feb 8, 2019
@ltfish ltfish added the feature label Feb 8, 2019
@ltfish ltfish merged commit 61e4a49 into master Feb 8, 2019
@ltfish ltfish deleted the feat/mixed_java branch February 8, 2019 18:26
@rhelmot rhelmot mentioned this pull request Mar 25, 2019
Closed
@rhelmot rhelmot mentioned this pull request Apr 19, 2020
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zardus zardus zardus requested changes

@ltfish ltfish ltfish approved these changes

Assignees

@ltfish ltfish

Labels
feature
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@Phat3 @zardus @ltfish @Lukas-Dresel @conand