evaluate CArray expression

[jkwoods]

The compiler doesn't yet allow evaluating a closed C expression of type CArray, which would be helpful for Lef's C gadget framework. I thought I would implement CStackPtr (using memory loads) and then CArray here, if that's okay and there wasn't already a grand plan to do something else.

[jkwoods]

Nevermind, my intuition for this above was way off. I'd be happy to take pointers and try again, but I have the feeling this is above my expertise.

[alex-ozdemir]

Yeah, this isn't trivial given the current design of arrays/pointers and Mem monad.

Most C-terms just wrap SMT terms, and the job of "evaluate" is to ensure the those terms are variable-free, so that we can drop SMT assertions without (essentially) leaving dangling reference to undefined variables.

However, with arrays/pointers, there is a challenge. These terms do not directly wrap SMT terms. They are just references to terms managed by Mem (so called "stack references"). This means that you can't replace their variable-containing terms with constant terms, because they don't directly have any terms. One option is to essentially push "evaluate" into the Mem monad, and do the replacement there. However, I think that this path leads to madness: it would make the interface to Mem really messy.

I think the better approach is this: make arrays a stack reference or an SMT term instead of just a stack reference. Then evaluate can produce arrays that are SMT terms. Now, how does this interact with existing systems? The simplest integration would be to (a) make assignment work (e.g. assigning an SMT term array to a Mem-reference array) and (b) make basically everything else an error. I have thoughts about how to integrate this change with bounds-checking, ITEs, etc. but you guys probably won't need those integrations right now.