search

boogie-org / symbooglix

Symbolic Execution Engine for Boogie
MIT License
27 stars 4 forks source link

Adding support for specifying loop/recursion unroll bounds #24

Closed zvonimir closed 7 years ago

zvonimir commented 7 years ago

We have made (mainly @liammachado) some traction on integration symbooglix into the SMACK toolflow. One annoying issue that we identified is that symbooglix does not support specifying loop/recursion unroll bounds as a command line argument. This was already discussed here: https://github.com/smackers/smack/pull/155/files/98852f442e711acc042ad7285d7b2864754e127f#r58845496 This is quite inconvenient since at this point we do not have the same (or at least very similar) unroll semantics between Corral and symbooglix. So I am wondering if someone could maybe implement this features, it would be really helpful.

delcypher commented 7 years ago

@zvonimir I should have some time this week to take a look at this.

zvonimir commented 7 years ago

@delcypher I noticed you've been playing with symbooglix recently (thanks!), and so maybe you could take a look at this issue as well. Thx!

delcypher commented 7 years ago

@zvonimir Yes sorry. I haven't forgotten this issue but it's been hard to find time to look at it. I'm trying to fix failing tests right now. The test pass on my machine™ but don't seem to pass in TravisCI. Once I get the tests working again I'll hopefully find some time to implement the loop bound.

delcypher commented 7 years ago

@zvonimir I've now implemented support for a loop bound. This supports nested loops. The loop bound is off by default but can be enabled with the new --max-loop-depth= flag.

Sorry this took so long. I've been very busy with paper deadlines until recently. This feature also required quite a bit of thought to get the design right.

There may be bugs in the implementation because it hasn't been heavily tested so please report any issues you hit.

zvonimir commented 7 years ago

Thanks @delcypher! We'll give it a try ASAP and let you know if we find any bugs.