On Jun 21, 2014, at 5:50 AM, Gregory Maxwell <gmaxw...@gmail.com> wrote:
> On Sat, Jun 21, 2014 at 5:18 AM, Diggory Hardy <diggory.ha...@unibas.ch>
> wrote:
>> As far as I am aware, using theorem proving tools[1] to provide limits on
>> value ranges is pretty hard and often computationally intensive to do in
>> simple code. I've only seen prototype systems where the user is expected to
>> write full contracts on exactly how every function may modify every value it
>> could, as well as often providing hints to the prover (especially for
>> loops). So I really don't think this is going to help much.
>
> To be sound is hard to catch lots of cases less so— existing C
> compilers manage to prove enough about ranges to eliminate redundant
> tests pretty often— e.g.
>
> #include <stdio.h>
> int main(int argc, char **argv){
> (void)argv;
> if(argc<16)return 1;
> argc+=1000;
> if(argc<8)printf("This code is not emitted by an optimizing compiler.\n");
> return 0;
> }
>
> GCC 4.8.2 -O2 manages this example fine and I expect is true for other
> modern optimizing C compilers.
LLVM doesn’t actually optimize this, although it does if you remove the
`argc+=1000`. LLVM’s range analysis is quite a bit worse than GCC’s. This is a
fixable problem (the algorithm that GCC uses is pretty simple), but it would
negatively impact compile time by a small amount.
> This is part of the reason that C's undefinedness has real performance
> implications, as sometimes it can only prove loop iteration counts or
> pointer non-aliasing (both useful for vectorization) when it knows
> that indexes cannot overflow.
You only get a benefit from the assumption that indices can’t overflow when you
are using signed indices. If you have the loop
int len = …;
for (int i = 0; i < len; i++) { … }
then there are two possible trip counts for the loop depending on whether `len`
is negative (i.e. whether i wraps or not). I don’t think there is any situation
where it helps signed arithmetic be more efficient than unsigned arithmetic.
This is arguably bad code in C/C++ anyways, since the language strongly
encourages you to use unsigned indices. Rust doesn’t have any analogue of this
problem, because `uint` is used for indexing and coercions are explicit.
Cameron
_______________________________________________
Rust-dev mailing list
Rust-dev@mozilla.org
https://mail.mozilla.org/listinfo/rust-dev
