Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
Take this piece of code:
It's easy to see why the first variant has zero bounds checks. However, reslicing can be expensive in a hot loop, so sometimes the code is rewritten to use indexes.
This is what the second variant does. I do realise that the two loops aren't equivalent - for example, if
Still, it seems to me like it should insert one, not four, since I've added the BCE hint. My first thought was that it couldn't prove that
I encountered this in the base64 encoder:
Rewriting the loop to use reslicing like
I think there's probably a way to rewrite the loop index logic to trick BCE, but I think the compiler could be made smarter here. I'm not sure whether that should be an enhancement in the prove pass, or in the bounds check elimination pass.
I believe this also affects the
As before, I tried combining unsigned integers and BCE hints, but no results. I also tried juggling with the for loop conditions, but that didn't make a difference either.
I just realised that removing bounds checks from a loop that jumps more than one position per iteration might not be as easy as it sounds, because of overflows. Imagine:
I presume this trouble disappears if we make the index variable unsigned, since an overflow will just get the index back to 0, which will definitely be within bounds.