[rust-dev] Integer overflow, round -2147483648

Gregory Maxwell gmaxwell at gmail.com
Sat Jun 21 05:50:18 PDT 2014


On Sat, Jun 21, 2014 at 5:18 AM, Diggory Hardy <diggory.hardy at 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.

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.


More information about the Rust-dev mailing list