Symbolic execution in chord - it is possible

[grze...@gmail.com]

Hi,

I am evaluating chord as a back-end which could be potentially used for symbolic execution of java program. I cannot find any information regarding this topic on the web, so maybe somebody on this group have similar interests ?

Have anybody tried to put as input some method and get as an output a call graph with constraint on (methods arguments/object states) which fulfill circumstances necessary to reach every branch ?

For example, simple case :

public static void someMethod(SomeObject object, Object someValue){

    if( object == null ){

         throw new IllegalArgumentException();

    }

    if( object.callSomeMethod().contains(someValue) ){

         callAnotherMethod();

    }

    AnotherObject another = object.getSome();

    if( another.shouldCallSth() ){

        callSth();

    }

}  

for this case I would like either :

 - at any branching point (in this case - on an "if" instruction) get the constraints on objects involved of fulfill conditions on the branching point (positive and negative)

 - at every endpoint (return statement or throw point) get conditions on all objects which are necessary to reach that point

I new at this topic, I know that something similar does JavaPathFinder/SymbolicPathFinder, but I like to have several tools to evaluate.

Has anybody experience/idea if it is possible (or exists some symbolic execution plugin for chord) ?

Thanks in advance,

Grzesiek 

[Ariel Rabkin]

I would think Chord is not the best fit here. Chord is designed to
pre-specify the set of elements in the domains of interest to
analysis. And you don't know all the symbolic values up front.

> --
> You received this message because you are subscribed to the Google Groups
> "chord-discuss" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to chord-discus...@googlegroups.com.
> To post to this group, send email to chord-...@googlegroups.com.
> Visit this group at http://groups.google.com/group/chord-discuss.
> For more options, visit https://groups.google.com/d/optout.



--
Ari Rabkin

[grze...@gmail.com]

W dniu wtorek, 3 marca 2015 19:57:27 UTC+1 użytkownik Ari Rabkin napisał:

I would think Chord is not the best fit here. Chord is designed to
pre-specify the set of elements in the domains of interest to
analysis. And you don't know all the symbolic values up front.

--
Ari Rabkin

Hi,

Thanks for answer.

Reagrds,

Grzesiek