[LLVMdev] Helping the optimizer along (__assume)

[Cédric Venet]

Kenneth Boyd a écrit :
> Cédric Venet wrote:
>> you never seen assert(0 && "Not yet implemented"); ?
>> You may want to compile a program like this :)
>>   
> As I see it, under the proposed extension a compile-time false constant 
> would error "if the code commits to executing it".
> 
> Heuristically, something like
> 
> void foo(int x)
> {
>     switch(x)
>     {
>     case 1: return;
>     case 2: return;
>     default: assert(0 && "not yet implemented")
>     }
> }
> 
> should itself compile, but then ideally
> 
> foo(3)
> 
> causes a compiler error as it commits to executing the assert.
> 
> Kenneth
> 

Then not only the condition of the assert must be proved false, but the
assert must be proved to be actually reached in all possible code path
(not only be reachable, think about virtual function). I don't really
know the State of art of C++ code proofer but this seems pretty hard to
prove in most real word case. And then think about:

int main(int argc, const char* argv[]) {
  if(argc<2) return -1; // error in command line, exit early
  ...
  assert(0); // false assert
  ...
  return 0;
}

you will never be able to demonstrate that the assert is reached since
it is not reached in all code path, after all how can the compiler know
that the good code path is when argc>=2 and not the contrary ?

Clearly this functionnality is interesting, but there is lot of work to
do on the semantic to make it useful, and potentially need the
adjonction of additionnal user information like: error_code_path or
always_reached.

Regards,

Cédric