TODO

----------------------------------------------------------------------

add instrinsics: bswap, x.with.overflow, ctpop, ctlz, cttz
add unreachable instruction
add insertvalue/extractvalue
add bitcast?

finish adding undefined behaviors
- nuw for add, sub, mul
- shift overflows
- exact shifts and divs
- mul and div overflows

factor UBs out of instructions to support fixing issue #13 and then to support
refinement proofs

make exploitation of undefined behavior in the LHS conditional on a command line
flag

RHS improvements:
- synthesize arbitrary-width integer constants
- synthesize undef values
- to guess instructions on the RHS, we need to implement the refinement check: 
  LHS assertion => (LHS == RHS) && RHS assertion 
- we can probably use techniques from here: 
  http://www.eecs.berkeley.edu/~jha/pubs/pldi-2011.pdf

external caching:
- add souper version to the cache, refuse to use an incompatible cache
- make sure cached IR doesn't have implicit machine dependencies
- add an option to only populate the cache -- don't call the solver
- write a tool that pulls unsolved entries out of the cache and runs them
  through the solver -- this makes it easy to distribute Souper across a cluster
- keep more information in the RHS of cache entries such as
  - solver that was used
  - whether the solver timed out
  - whether the solver hasn't been run on this one yet
  - optional usage count
- look for any additional opportunties to canonicalize or compress the
  serialized Souper IR
- add deserialization; test it by making sure x==deserialize(serialize(x))

interaction with dataflow analyses
- get intervals from LazyValueInfo, ConstantRange.cpp
- get bit info from computeKnownBits() functions from include/llvm/Analysis/ValueTracking.h
- teach souper to use assume, maybe using Philip's hack

eventually add vector, FP, and memory instructions

----------------------------------------------------------------------