smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Add an option to enable targeted checking of specific functions #715

Closed keram88 closed 3 years ago

keram88 commented 3 years ago

This adds the ability to selectively check certain functions in a program, specifically:

shaobo-he commented 3 years ago

The reason I asked this question is we can, though not ideal, disable checking on certain functions via regex negative look ahead

keram88 commented 3 years ago

This actually might be very useful for e.g. matching mangled functions.

On Mon, Apr 5, 2021, 19:54 Shaobo @.***> wrote:

The reason I asked this question is we can, though not ideal, disable checking on certain functions via regex negative look ahead

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/smackers/smack/pull/715#issuecomment-813765951, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABQSABNUFOQ6L5Y6L7IOPITTHJSWLANCNFSM42NV7JVA .

michael-emmi commented 3 years ago

+1 for regex.

You might also (a) consider using regex disjunction instead of a list — whatever is more convenient — and (b) consider whether matching happens at the assembly level — i.e. with "flat" and potentially mangled names — or the source or IR level — i.e. with potentially structured names like "MyModule::myFunction".

keram88 commented 3 years ago

I think I like leaving it as a list of space separated list to remain consistent with the --entry-points flag and allow it to be a list of regex patters. A potential concern is that $ and . are valid characters in identifiers, e.g., used by Kotlin and Rust respectively.

I will have to think more about matching on unmangled names since languages have different mangling schemes (Rust doesn't quite demangle with c++filt for example.)

keram88 commented 3 years ago

I implemented specifying the functions to check using regular expressions. I made it so that the entire function name must be matched in order to avoid surprises should someone want just one function. However, I'm not sure this is necessarily the best way to do it.

shaobo-he commented 3 years ago

LGTM.