search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

What's the latest upstream commit of KLEE? #380

Open yxliang01 opened 3 years ago

yxliang01 commented 3 years ago

This was created as a fork of KLEE repo. But, due to incorrect linking of issues, this has been now not a fork, making it hard to know what the latest upstream commit being ported is. Latest relevant PR I can see is #145 .

rasoolmaghareh commented 3 years ago

@yxliang01 Yes, #145 has been the latest attempt to merge with the upstream commits. At the current moment we are quite behind in this aspect. The most important point is that the recent changes to KLEE (e.g. the floating point support) might not be easily reflected in the deleteion interpolation algorithm.

yxliang01 commented 3 years ago

Thanks @rasoolmaghareh . Last time I checked the floating point support PR, it wasn't merged and it was mentioned that the support would be broken into different parts and merge progressively. So, I don't expect it will be done any time soon. Meanwhile, I think merging with upstream is quite important that there has been a lot of optimizations and improvements done since then, simply porting them might already bring nontrivial speedup I'm guessing. The porting can also be done progressively I guess, so unsupported new features maybe can simply be disabled for now, keeping in sync with upstream isn't easy I believe.

Maybe one more question instead of me creating yet another issue, what is the maintenance status of this repo? I'm asking since I might be working on something based on TracerX :smile:

rasoolmaghareh commented 3 years ago

At the current moment, we don't have the manpower to merge upstream commits but definitely, this should be done when we reach a stable interpolation algorithm. We are currently more focused on the WP interpolation algorithm (not merged into the master branch yet). The master branch has a stable version of the interpolation algorithm but we are trying to enhance it. I suggest talking to @ArpitaDutta for the details.

It is great to hear that you will be working on TracerX. We would definitely love new team members to join. :)

yxliang01 commented 3 years ago

Thanks for the info. I'm wondering how much impact by the WIP work expected and if it's huge, any estimate? Or, for any new work, would you suggest me just based on the current master instead?

Thanks also for the warm welcome :)

rasoolmaghareh commented 3 years ago

We hope the new WIP WP branch can have an exponential impact in reducing the analysis time for a reasonable group of the benchmarks. We hope to be able to finish it in the next couple of months.

Besides the application area that I think you would be working on, we always think it would be good if you can engage in the implementation of the core algorithms. This way you would have a better insight into how TracerX works which would be helpful in implementing customized algorithms for specific application areas too.

yxliang01 commented 3 years ago

Exponential impact sounds cool! I also agree that engaging in the implementation of the core algorithm is a good thing to do. For now, I'm still trying to understand this project deeper, so maybe the concrete arrangement can be decided after that.

rasoolmaghareh commented 3 years ago

Sure. We will be in touch.