search

psycopaths / jdart

A dynamic symbolic analysis tool for Java
Apache License 2.0
112 stars 39 forks source link

Collecting constraints of a single path #27

Closed JasonPap closed 6 months ago

JasonPap commented 6 years ago

Hello,

I would like to know how could I collect the constraints of the (single) path that is executed when a function is executed with a specific input. Like what is mentioned in this paper in Section 3.3, Termination.

I have downloaded and configured JPF + JDart, went through the JDart github Wiki and experimented with some of the provided examples (mostly in /examples/features/simple). For example, I have added the following lines at the end of the test_foo.jpf file: concolic.method.foo.config=foo jdart.configs.foo.constraints=(i==0) And it looks like indeed, JDart is only exploring one path as the output says:

. . .
[INFO] ----Constraints Tree Statistics---
[INFO] # paths (total): 1
[INFO] # OK paths: 1
[INFO] # ERROR paths: 0
[INFO] # DONT_KNOW paths: 0

My question is, how can I get the constraints (and in what form) of that single path in the same run? Additionally, are there any other JDart configurations I can do to optimize the process (like tell it to stop when that path is done and not try to go along another path as it will be impossible anyway given my additional constraint)?

I am new to JDart so any additional information/pointer is very welcome.

Thank you, Jason

MeKot commented 5 years ago

Hello, @JasonPap,

I have currently run into the same issue and was wondering if you have managed to solve it by any chance..

JasonPap commented 5 years ago

Hi @MeKot , I ended up doing a very hack-y printer for path conditions and then dropped JDart as I found a different approach to the problem I was trying to solve.

My function was implemented in the InternalConstraintTree class, it took as input a node, checked if it had decision data and if so printed that and then called itself on its child (if you have executed only one path there should only be one child so you have to check whether it is the child corresponding to true or false).

QRXqrx commented 3 years ago

Hi @MeKot , I ended up doing a very hack-y printer for path conditions and then dropped JDart as I found a different approach to the problem I was trying to solve.

My function was implemented in the InternalConstraintTree class, it took as input a node, checked if it had decision data and if so printed that and then called itself on its child (if you have executed only one path there should only be one child so you have to check whether it is the child corresponding to true or false).

Hey, it seems I have the same requirement as you. I have tried to implement the function follow your description: I implement a private helper method within InternalConstraintsTree and I call it in toFinalCTree because I think the "node" in your description refers to the root before transforming into a trimmed constraint tree. However, it turns out the root node always have two children node and both of them don not have a valid decisionData (null) for true or false checking. Is there anything I have made mistakes? Please let me know at your convenience, thank u !