[TYPES] Declarative vs imperative

[Robbert Krebbers]

Hello Uday,

On 04/23/2013 08:32 PM, Uday S Reddy wrote:
> In the C standard, the order of evaluation of arguments in function calls is
> unspecified.  However, if I were stupid enough to depend on a particular
> evaluation order that my compiler chooses deterministically, I would have
> hidden bugs in my programs that I wouldn't be able to notice.  If I paid
> good money for a C compiler, I would definitely demand that it should have
> an option to randomize the evaluation order of arguments.

Let me then notice that in the case of C, it is worse than just 
non-determinism. There are also so called sequence point violations, 
which happen if you modify an object more than once (or read after 
you've modified it) in between two sequence points. For example

   int x = 0;
   int main() {
     printf("%d ", (x = 3) + (x = 4));
     printf("%d\n", x);
     return 0;
   }

not just randomly prints "7 3" or "7 4", but instead gives rise to 
undefined behavior, and could print arbitrary nonsense. When compiled 
with gcc at my machine, it for example prints "8 4".

> In fact, at least in one case, I would welcome a compiler that does that.

If you would like to explore non-determinism in C, you should take a 
look at the executable C semantics by Chucky Ellison and Grigore Rosu

   http://code.google.com/p/c-semantics/

It provides an interpreter that can used for exactly what you want to 
do. Also the interpreter of CompCert is also able to explore all 
possible evaluation orders. A patch by me

   http://gallium.inria.fr/blog/non-determinism-and-sequence-points-in-c/

allows it also to be used to detect sequence point violations as well.

Best,

Robbert