Loop invariant checker

[fortunac]

• Adds a flag for checking a loop invariant

  • A user can input an s-expression which represents a list of loop invariants: (((address 0x12:64u) (invariant <smtlib for invariant>)) (...))
  • Assumes that a loop only has one entrance and one exit
  • Currently only supported for a single binary
  • If no invariant is specified for a loop, we default to unrolling

• Some changes to existing code:

  • You have to pass in a function for which nodes to skip for visit_graph. This was needed to pass in the option to skip nodes in the a loop. unreachable_from_start was refactored out, so it is possible to just pass in that.
  • The option to name a constraint created by mk_smtlib2_single. This was used to name the invariant "Loop Invariant (tid)" instead of a z3-expression representing the invariant. If no name is specified, uses the default behavior of naming the constraint after the z3 expression.
  • The type for loop_handler is changed to hold information about both loop unrolling and loop invariant checking.

[codyroux]

Absolutely stellar code!

My comments are a bit of an afterthought: it feels like we're duplicating a bit of the visit_blk functionality, it would be nice to unify that code somehow.

We can leave that as a TODO if a solution is not forthcoming.

[ccasin]

I am playing around with this and it is cool!

One thing that might be nice to start doing: documentation in our examples/test cases. A README.md file in each subdirectory under wp/resources/sample_binaries/loop_invariant that just says in English what the test is supposed to check and what the property means would be helpful.

[fortunac]

I am playing around with this and it is cool!

One thing that might be nice to start doing: documentation in our examples/test cases. A README.md file in each subdirectory under wp/resources/sample_binaries/loop_invariant that just says in English what the test is supposed to check and what the property means would be helpful.

Can definitely do this!