[Soot-list] Traverse a CFG based on a given test case

[Marc-André Laverdière-Papineau]

There is some symbolic execution built on top of Soot.
https://code.google.com/p/acteve/

Saswat is the main guy behind it - I am not aware of anybody else using it.

Another possibility that you have is to port the approach that was  
developed in my lab. That approach detects which parts of code are  
protected by which control variable. The context is boolean permission  
checks, but you can probably model your predicate that way.
http://www.computer.org/csdl/proceedings/wcre/2012/4891/00/4891a247-abs.html
http://www.computer.org/csdl/proceedings/scam/2012/4783/00/4783a044-abs.html

Note that there was an interesting talk at ICSE this year about  
combining static information and symbolic execution in order to make  
the analysis scale. If you go that route, you should probably study  
that paper carefully.

Julian Schütte <julian.schuette at gmx.net> a écrit :

> Hello Ding Sun,
>
> your example uses constants "1" and "3" and the comparison values are
> given by the test case. If this is always the case, you should probably
> go the way Steven proposes.
>
> If your conditions refer to values which you cannot determine
> statically, symbolic execution would be a possible approach. But this is
> nothing you can just straightforward apply to "any" program, as you have
> to cope with state explosion and expressiveness of the constraint solver.
>
> Best,
> Julian
>
> On 12.06.2014 17:40, dingsun wrote:
>> Hi Steven,
>>
>> Thanks for the help.
>>
>> I'm not sure whether I understand correctly.
>>
>> With Soot, I can get a jBody from the CFG and visit every Unit in the
>> CFG.
>>
>> But if given a test case , say (a=1, b=2), in the following program
>> for example, at those IfStmt,  how may I judge which branches the
>> program should go?  It looks like some symbolic execution is needed to
>> assist such judgement. I'm wondering whether there is already some
>> implementation in Soot?
>>
>> >>>>     /*n1*/      void fun(int a, int b){
>> >>>> /*n2*/   if(a>1 && b>3){
>> >>>> /*n3*/      System.out.println("hello123");
>> >>>>            }
>> >>>> /*n4*/      System.out.println("hello456");
>> >>>>           }
>> Best regards,
>> Ding Sun
>>
>> Date: Thu, 12 Jun 2014 14:56:14 +0200
>> From: steven.arzt at cased.de
>> To: soot-list at cs.mcgill.ca
>> Subject: Re: [Soot-list] Traverse a CFG based on a given test case
>>
>> You can try the following sequence of existing transformers in Soot:
>>
>>          CopyPropagator.v().transform(jBody);
>>          ConditionalBranchFolder.v().transform(jBody);
>>          UnreachableCodeEliminator.v().transform(jBody);
>>
>> This should at least take care of the simple cases.
>>
>> Am 11.06.2014 18:09, schrieb Dacong Yan:
>> > I am not aware of anything that you can use directly. Perhaps others
>> > who are more familiar with the code base can help you with that.
>> >
>> > One example you can refer to is
>> >  
>> (https://github.com/Sable/soot/blob/6ece52bdb193aa95180fff8838f14c63cf89cda3/src/soot/dava/toolkits/base/AST/structuredAnalysis/CP.java).
>> > I have never read the code because I just found it by searching
>> > "ConstantPropagation" on github.
>> >
>> > Once you have a solution for constant propagation, you can use that
>> > info to find and ignore dead code (e.g., some branches are no longer
>> > feasible) as you traverse CFG. In other words, you don't have to
>> > create explicitly a new CFG with unreachable code removed.
>> >
>> > On Wed, Jun 11, 2014 at 11:56 AM, dingsun <xyz031702 at hotmail.com>
>> > wrote:
>> >> Hi Yan,
>> >>
>> >> Many thanks for the suggestion!
>> >>
>> >> But shall I know if there is any implementation in Soot to handle this
>> >> issue?
>> >>
>> >> Best regards,
>> >> Ding Sun
>> >>
>> >>> On 2014?6?11?, at 23:51, "Dacong Yan" <tonywinslow1986 at gmail.com>
>> >>> wrote:
>> >>>
>> >>> Hi Ding,
>> >>>
>> >>> I think this paper might help you solve the problem:
>> >>>  Constant propagation with conditional branches
>> >>> (http://dl.acm.org/citation.cfm?id=103136)
>> >>>
>> >>> Thanks,
>> >>> Tony
>> >>>
>> >>>> On Wed, Jun 11, 2014 at 6:22 AM, dingsun <xyz031702 at hotmail.com>
>> >>>> wrote:
>> >>>> Hi All,
>> >>>>
>> >>>> If I have a CFG generated by Soot and a test case, is it possible to
>> >>>> traverse the branches that are accessible by that test case?
>> >>>>
>> >>>> For example, if there is a simple function:
>> >>>>
>> >>>> /*n1*/ void fun(int a, int b){
>> >>>> /*n2*/   if(a>1 && b>3){
>> >>>> /*n3*/      System.out.println("hello123");
>> >>>>            }
>> >>>> /*n4*/      System.out.println("hello456");
>> >>>>           }
>> >>>>
>> >>>> And a given test case:  a=6, b=7,
>> >>>>
>> >>>> is it possible to use this test case to "guide" Soot to traverse the
>> >>>> path:
>> >>>> (n1, n2, n3, n4)
>> >>>> is it possible to use this test case to "guide" Soot to avoid
>> >>>> traversing the
>> >>>> path (n1, n2, n4)
>> >>>>
>> >>>>
>> >>>> Thanks a lot!
>> >>>>
>> >>>> Best regards,
>> >>>> Ding Sun
>> >>>>
>> >>>
>> >>> --
>> >>> Dacong (Tony) Yan
>> >>> Ph.D. Student
>> >>> Computer Science and Engineering
>> >>> The Ohio State University, Columbus
>> >>> http://www.cse.ohio-state.edu/~yan  
>> <http://www.cse.ohio-state.edu/%7Eyan>
>>