[LLVMdev] Helping the optimizer along (__assume)

[Kenneth Boyd]

Cédric Venet wrote:
> 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.
>>     
>
> 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'm thinking a bit more locally than that; as I'd rather not mess with 
the halting problem.

In the example I gave, I want foo(3) to error even if it is 
unreachable.  But I don't want an extended assert of the compile-time 
false constant, wrapped in the switch statement, to error.

[I'm visualizing this as having two extension intrinsics __precondition 
and __postcondition, and using the algebra of theses intrinsics to 
implement the automated proof.  The compiler gets to inject these at AST 
creation "wherever reasonable".  In particular, each block of the switch 
statement gets an implicit __postcondition at the very beginning, before 
any user code in the block.

The __postcondition(1!=x && 2!=x), implicitly injected at the start of 
the default: block, prevents the __precondition(0 && "not yet 
implemented"), injected by the assert, from immediately erroring.  The 
idea is that is that

__postcondition(1!=x && 2!=x) __precondition(0 && "not yet implemented")

isn't "in normal form", we should first reduce to

__postcondition(1!=x && 2!=x) __precondition(0)

and then commutate:

__precondition(1!=x && 2!=x) __postcondition(1!=x && 2!=x) ]
> ... 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,
That's fine.  Then the assert goes off at runtime only in debug-mode, 
just like before.
> ....
>   
> 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.
>   
Yes.

Kenneth