search

draperlaboratory / VIBES

Verified, Incremental, Binary Editing with Synthesis
MIT License
51 stars 1 forks source link

Require a postcond, or provide a default #130

Open jtpaasch opened 3 years ago

jtpaasch commented 3 years ago

Currently, the user doesn't need to specify a postcond. I'm not sure what WP does if you don't provide a postcondition to check.

If this does something bad, we should require a postcond.

codyroux commented 3 years ago

It provides "true" aka the empty clause.

This is usually what we want when the "interesting" postconditions come from function calls or branch conditions.

codyroux commented 3 years ago

This is really more of a question for CBAT, since VIBES is just passing the arguments along.

codyroux commented 3 years ago

I think the code to create the postcond is here: https://github.com/draperlaboratory/cbat_tools/blob/8891fdeaa7dd79ae2ba37a3476a5a74c603db3e9/wp/lib/bap_wp/src/runner.ml#L297

And the relevant helper functions are here: https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/compare.ml

Messy? Yes.

jtpaasch commented 3 years ago

We used to require that the user specify a property, and if the user did not specify it, we threw an error.

The new behavior is now: if the user specifies no property, then we just silently pass it to WP, which defaults to "true."

@ccasin @philzook58 @codyroux is this the behavior we want?

I myself am inclined to have the old behavior (require that the user specify a property, and throw an error if the user doesn't provide one).