Split state variables and symbolic variables. Stricter type checking.

[fruffy]

This PR untangles the mix of symbolic variables and state variables and ensures that only symbolic variables remain part of the IR expressions. Previously, zombies and state variables were the same thing, which could easily lead to bugs and confusion because state variables are accidentally converted into zombie constants.

Now, state variables, which are members need to be resolved in the interpreter. A BUG will be thrown if there are any members left when we enter the final state. This cleanup required several changes.

• The Model class was mixing symbolic variables and state variables, which reference symbolic variables. We split the model into two maps. Each model now contains a set of symbolic variables. The SMT solvers do not produce a model, they produce a map of solved symbolic variables. The model consumes this map and looks up symbolic variables as needed. State variables are references to expressions that are kept in the model. They or may not contain symbolic variables.
• The "Zombie" terminology was confusing. We rename zombies to symbolic variables. We consolidate zombies.h and parts of utils.h into variables.h, which contains all operations related to tools-internal variables.
• Any IR::Member that is encountered when trying to complete the model is a bug. IR::Members are state variables, which should have been resolved at this point.
• Ensure that most helper functions produce const IR::StateVariable&, not IR::Member.
• Clean up the p4tools.def files. Make the constructors of the IR classes less accepting. No Concolic or Symbolic variable can be constructed without also supplying a type.
• This separation also uncovered some latent bugs in the concolic execution framework. The payload size calculation was very brittle. Now we calculate payload size as a final state post-processing step instead. This way we can precisely control how and when we set the payload size. TODO: We should make the payload optional, too. Not all tests need huge packets.
• StateVariables had an "incarnation" parameter, but this parameter was effectively never used and allocated an IR::Member for no reason. Removed.

Other small changes:

• Add a canonical implementation of createTargetUninitialized, such that the method does not have to be copied in every program info class.
• Reduce the size of the execution state class by moving out some static variables into a separate compilation unit.

---

@nikil21 @abhinav2sri

This clears up the distinction between state variables and zombies. Also renames zombies into "symbolic variables" to clear up which type of variable one is working with.

---

The refactoring also appears to improve performance:

Generating 10000 tests for middleblock.p4:
Before:

   Executed in  610.65 secs    fish           external                                                            
   usr time  596.61 secs  862.00 micros  596.61 secs                                                           
   sys time   11.44 secs  271.00 micros   11.43 secs     

After:

Executed in  520.26 secs    fish           external                                                            
   usr time  506.76 secs    0.00 micros  506.76 secs                                                           
   sys time   11.08 secs  972.00 micros   11.08 secs       

A ~15% reduction in time.

[fruffy]

There is a bug in either PTF or the simple switch that cause it too loop packets infinitely under certain conditions. For now, I am disabling this test, but this is something we could look into.

[jnfoster]

This is great. Reviewing now...

[jnfoster]

A big change, but looks good!