SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
130 stars 91 forks source link

Get program Path constraint using Symbolic pathfinder #81

Closed Alim9100 closed 5 months ago

Alim9100 commented 1 year ago

Hello I want to use this tool for getting path constraint of methods, But I want to choose methods in runtime. So I cannot write driver classes statically. Is there a way to choose methods or creating drivers dynamically?

sohah commented 1 year ago

Hi Ali,

You need to write something to get this information out. The path constraint is collected during execution in the PathCondition class. One way to perhaps do what you want is to update the SymbolicListener to filter return instructions that belong to the methods of interest. Then you can dump out the PathCondition of the thread at that point.

Soha

On Tue, May 16, 2023 at 9:59 PM Ali Mohammadi @.***> wrote:

Hello I want to use this tool for getting path constraint of methods, But I want to choose methods in runtime. So I cannot write driver classes statically. Is there a way to choose methods or creating drivers dynamically?

— Reply to this email directly, view it on GitHub https://github.com/SymbolicPathFinder/jpf-symbc/issues/81, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQGE5R5XRGTYNYHVGWVERLXGPMA5ANCNFSM6AAAAAAYEEBLT4 . You are receiving this because you are subscribed to this thread.Message ID: @.***>

Alim9100 commented 1 year ago

Hi, Thanks for your response. Consider the example in the picture. I have two methods, Push and Pop. I execute different trace of these methods. for example Push pop, Push push pop pop,.... . So for each one, I need a driver similar to the picture. Each time I should change the body and parameters of test3 and main method and run the symbolic path finder to get PC. But I need a solution to get path condition without writing driver for each trace. because traces will create at runtime. Do you have any idea? 1 2

sohah commented 5 months ago

As I mentioned in my previous reply, you'd need to update SPF code to expose this information to the driver that you have. If you have any additional questions please contact us back.

@yannicnoller , I think we can close this issue now.