search

boogie-org / symbooglix

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

GlobalDeadDeclEliminationPass leaves unused functions #23

Closed shaobo-he closed 7 years ago

shaobo-he commented 7 years ago

I found some unused functions left in the output file processed by this pass. The input file is a Boogie program generated by SMACK. I think the reason is that class FindUsedFunctionAndGlobalVariableVisitor visits functions with bodies first and add function calls to used function hashset. While these functions are not actually used if their callers are not used. (https://github.com/symbooglix/symbooglix/blob/master/src/Symbooglix/Transform/GlobalDeadDeclEliminationPass.cs#L278-L287)

delcypher commented 7 years ago

@Guoanshisb Could you provide a minimal example so I can debug this?

shaobo-he commented 7 years ago

Yes, it's http://www.cs.utah.edu/~shaobo/simple.bpl. In the resulting bpl file by running, mono ../symbooglix/src/SymbooglixPassRunner/bin/Debug/spr.exe simple.bpl -e main -p Transform.GlobalDeadDeclEliminationPass, you can see functions like function {:bvbuiltin "bvule"} $ule.bv128.bool(i1: bv128, i2: bv128) : bool; not removed.

delcypher commented 7 years ago

@Guoanshisb Sorry for taking so long to look at this. Thank you for reporting this and identifying the issue for me. I believe this now fixed. There is still an issue with procedures/implementations. I've made #30 for this.