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

[Julian Schütte]

A student of mine is currently working on an extension of acteve.

The purpose of acteve is however to generate a set of input events for
increasing code coverage of Android apps. You could use it as a starting
point but it would have to be adapted in large parts to match your use
case, Ding Sun.
If you want to get started with it nevertheless, just drop us a line.

Best,
Julian


On 13.06.2014 07:27, Marc-André Laverdière-Papineau wrote:
> 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
>>>>>>>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20140613/bb20ec9f/attachment.html