GSoC - Range Analysis

Dear LLVMers,

I have been working on Douglas’s range analysis, and today, after
toiling with it for two years, we have a very mature and robust
implementation, which is publicly available at
http://code.google.com/p/range-analysis/. We can, at this point,
perform range analysis on very large benchmarks in a few seconds. To
give you an idea, we take less than 10 seconds to globally analyze
SPEC 2006 gcc benchmark with function inlining enabled. And the
analysis is fairly precise. We have a gallery of examples at
http://code.google.com/p/range-analysis/wiki/gallery that will give
you an idea of what kind of information we can find. Our analysis
comes together with a dynamic profiler that points the minimum and
maximum values that each variable assumes during program execution
too. And it uses a live range splitting strategy to obtain data-flow
sparsity that is lightning fast. It is more than 100x faster than the
original implementation of SSI in LLVM 2.7, for instance. There are a
number of LLVMers, outside my university, that use our analysis.
So, I would like to propose a summer of code that consists in (i)
integrating our infra-structure in the LLVM main tree, and (ii)
writing a dead-code elimination pass that uses the analysis as a
client. So far people have been using our analysis to check for buffer
overflows, and to eliminate array bound checks. Yet, I think there is
a lot of potential to optimizations. Dead code elimination at branches
would be one such optimization. Given that the analysis is pretty
mature, I think that it would not be too difficult to integrate it in
the current infra-structure that LLVM offers, e.g., Lazy Values. As
for dead-code, we already can flag variables that have impossible
intervals, in which the lower bound is larger than the upper bound.
So, it is only a matter of adapting it to remove this code.

I would like to hear from you what you think about this Summer of Code
project. If you think it could be interesting, I will write a proposal
richer in details.

Sincerely yours,

Victor

Dear LLVMers,

I have been working on Douglas’s range analysis, and today, after
toiling with it for two years, we have a very mature and robust
implementation, which is publicly available at
http://code.google.com/p/range-analysis/. We can, at this point,
perform range analysis on very large benchmarks in a few seconds. To
give you an idea, we take less than 10 seconds to globally analyze
SPEC 2006 gcc benchmark with function inlining enabled. And the
analysis is fairly precise. We have a gallery of examples at
http://code.google.com/p/range-analysis/wiki/gallery that will give
you an idea of what kind of information we can find. Our analysis
comes together with a dynamic profiler that points the minimum and
maximum values that each variable assumes during program execution
too. And it uses a live range splitting strategy to obtain data-flow
sparsity that is lightning fast. It is more than 100x faster than the
original implementation of SSI in LLVM 2.7, for instance. There are a
number of LLVMers, outside my university, that use our analysis.

What version of LLVM does your analysis use currently?

It sounds like your analysis is fast. Can you show results on how fast it is on various programs? Do you have measurements on how much memory it uses? How large is the largest program you’ve compiled with it?

So, I would like to propose a summer of code that consists in (i)
integrating our infra-structure in the LLVM main tree, and (ii)
writing a dead-code elimination pass that uses the analysis as a
client. So far people have been using our analysis to check for buffer
overflows, and to eliminate array bound checks.

If possible, I think you should first implement the dead-code elimination optimization that uses your analysis to show how much of a performance win your analysis provides for LLVM. If the optimization is sufficiently fast and provides enough of a speedup, then it can be integrated into LLVM (because you will have proof that it is a performance win; that will help convince current developers with commit access to review your code for inclusion).

We in the SAFECode project would be interested in trying your analysis out for eliminating bounds checks. We just haven’t had the time to do that yet (I’m assuming you’re the same person that wanted to do Value Range analysis last year).

Yet, I think there is
a lot of potential to optimizations. Dead code elimination at branches
would be one such optimization. Given that the analysis is pretty
mature, I think that it would not be too difficult to integrate it in
the current infra-structure that LLVM offers, e.g., Lazy Values. As
for dead-code, we already can flag variables that have impossible
intervals, in which the lower bound is larger than the upper bound.
So, it is only a matter of adapting it to remove this code.

Regarding a dead-code elimination algorithm, I can see something like an Aggressive Dead Code Elimination pass using your analysis to prove that certain branches are never taken. One thing you could do would be to write a pass that looks for icmp instructions and uses your analysis to change them to true/false when possible. SCCP, ADCE, and other optimizations would then take care of the rest.

The idea of integrating your pass as a lazy value pass sounds good. The question I have is what optimizations benefit from LazyInfo? I only see one or two transforms that use it in LLVM 3.0.

I would like to hear from you what you think about this Summer of Code
project. If you think it could be interesting, I will write a proposal
richer in details.

My interest in range analysis is for using it with SAFECode, but if it can be used for standard compiler optimization and gets integrated into LLVM, all the better for me.

– John T.

What version of LLVM does your analysis use currently?

We are working with LLVM 3.0 (stable release)

It sounds like your analysis is fast. Can you show results on how fast it
is on various programs? Do you have measurements on how much memory it
uses? How large is the largest program you’ve compiled with it?

Yes, we have a very extensive report about it. Take a look into the
pdf at http://code.google.com/p/range-analysis/source/browse/trunk/doc/Manuscript/paper.pdf

In particular, take a look into fig.10, that shows program size vs
runtime. We are truly linear on the program size. The largest program
that we have compiled is SPEC CPU 2006 gcc. It takes less than 10
seconds to analyze it. This is the largest program that we had here.
Its constraint graph has almost 1.5 million nodes.

We in the SAFECode project would be interested in trying your analysis out
for eliminating bounds checks. We just haven’t had the time to do that yet
(I’m assuming you’re the same person that wanted to do Value Range analysis
last year).

No, that was Douglas, a friend of mine. He is in Texas nowadays. Now I
am responsible for the range analysis project at UFMG. There are two
other guys working with me on it too. And there are a few users,
outside our school that use the pass. If you guys are willing to give
our pass a try, we will be more than happy to help you. Notice that we
have put some detailed instructions at
http://code.google.com/p/range-analysis/wiki/HowToUseRangeAnalysisInAnotherPass
about how to use our range analysis.

The idea of integrating your pass as a lazy value pass sounds good. The
question I have is what optimizations benefit from LazyInfo? I only see
one or two transforms that use it in LLVM 3.0.

Yes, I do not think there are many optimizations that use LazyInfo so
far. But maybe, backed by a more aggressive analysis, LazyInfo will be
more effective. I can implement dead-code elimination based on value
ranges, and I think it can be quite effective, even more in code that
is produced out of type-safe languages, such as Java, which is full of
safety checks.

2012/3/29 John Criswell <criswell@illinois.edu>

Hi Victor,

    I have been working on Douglas's range analysis, and today, after
toiling with it for two years, we have a very mature and robust
implementation, which is publicly available at
http://code.google.com/p/range-analysis/.

one of the big problems with Douglas's original range analysis was that it
couldn't handle modulo arithmetic. For example, if an addition does not have
the nsw flag then it had to give up [*]. Did you solve this problem?

Also, the tricky bit of range analysis is handling loops. I suggested to
Douglas that he exploit LLVM's SCEV infrastructure to discover and exploit
how induction variables are evolving rather than trying to create his own
poor man's version using interval arithmetic. How are loops handled now?

Ciao, Duncan.

[*] IIRC it didn't pay any attention to this issue: it just assumed that
arithmetic doesn't wrap - oops.

Hi Victor,

     I have been working on Douglas's range analysis, and today, after
toiling with it for two years, we have a very mature and robust
implementation, which is publicly available at
http://code.google.com/p/range-analysis/.

one of the big problems with Douglas's original range analysis was that it
couldn't handle modulo arithmetic. For example, if an addition does not have
the nsw flag then it had to give up [*]. Did you solve this problem?

As a follow up to this question, can your range analysis be configured so that it treats all arithmetic operations as two's complement arithmetic (i.e., does it take into account that, even with the nsw flag, values can overflow or underflow)?

Also, on which LLVM types does your analysis work? I know it must work on integers, but does it also provide information on floating point or pointer values?

-- John T.

> What version of LLVM does your analysis use currently?

We are working with LLVM 3.0 (stable release)

> It sounds like your analysis is fast. Can you show results on how fast it
> is on various programs? Do you have measurements on how much memory it
> uses? How large is the largest program you've compiled with it?

Yes, we have a very extensive report about it. Take a look into the
pdf at http://code.google.com/p/range-analysis/source/browse/trunk/doc/Manuscript/paper.pdf

I took a brief look at your report. I'm not sure what others in the LLVM community think (and I'd like their input), but I suspect that 10-15 seconds for analyzing GCC means that users would want your analysis enabled at optimization levels higher than -O2.

When I asked for memory usage, I meant the amount of RAM used by the analysis. As far as I can tell, your paper only reports the number of constraints, so it doesn't really tell me how much RAM the analysis uses. That said, your test machine had about 3 GB of RAM, so I assume all your test runs used less than that. Do you have a more precise (and hopefully smaller) upper-bound?

One other thing I've been wondering about is whether your analysis is able to find value ranges for the results of load instructions. Can it do that? If so, I assume it relies on a points-to analysis.

Finally, do you think it would be possible in the future to use parallelism to improve the performance of your analysis?

In particular, take a look into fig.10, that shows program size vs
runtime. We are truly linear on the program size. The largest program
that we have compiled is SPEC CPU 2006 gcc. It takes less than 10
seconds to analyze it. This is the largest program that we had here.
Its constraint graph has almost 1.5 million nodes.

I recommend that your proposal mention that you'll try your analysis on larger and more diverse codes (especially non-benchmark codes). Programs like Apache, Firefox, MySQL, LLVM, and the FreeBSD kernel come to mind. I'm not sure that the GCC SPEC benchmark is considered a monster-sized program these days.

> We in the SAFECode project would be interested in trying your analysis out
> for eliminating bounds checks. We just haven't had the time to do that yet
> (I'm assuming you're the same person that wanted to do Value Range analysis
> last year).

No, that was Douglas, a friend of mine. He is in Texas nowadays.

Fascinating. A former student of ours is a postdoc at UT-Austin. Small world.

Now I
am responsible for the range analysis project at UFMG. There are two
other guys working with me on it too. And there are a few users,
outside our school that use the pass. If you guys are willing to give
our pass a try, we will be more than happy to help you. Notice that we
have put some detailed instructions at
http://code.google.com/p/range-analysis/wiki/HowToUseRangeAnalysisInAnotherPass
about how to use our range analysis.

I'd like to look into that, but my schedule to date hasn't permitted me to do so. We have a new person, though, that might be able to look into that in the coming months. It seems Raphael Ernani Rodrigues may be interested in working on it, too.

> The idea of integrating your pass as a lazy value pass sounds good. The
> question I have is what optimizations benefit from LazyInfo? I only see
> one or two transforms that use it in LLVM 3.0.

Yes, I do not think there are many optimizations that use LazyInfo so
far. But maybe, backed by a more aggressive analysis, LazyInfo will be
more effective. I can implement dead-code elimination based on value
ranges, and I think it can be quite effective, even more in code that
is produced out of type-safe languages, such as Java, which is full of
safety checks.

Regarding your comment about Java, I think you're correct that your range analysis would be better at optimizing Java code. However, LLVM really isn't used for Java, so I'm not sure if that's a strong argument for your proposal. To get the best bang for the buck, I think your analysis will need to work well in optimizing C/C++/Objective-C[++] code.

One thing that concerns me is that your project currently sounds like a small research project: you want to hook your analysis into dead code elimination and see how well it works. I'm not sure if the GSoC people are really looking for a project like that; they may want something with a higher assurance of a payoff.

One thing you could do to mitigate that problem is to do an experiment that *shows* that your analysis has the potential to find more optimization opportunities than what LLVM does today. For example, for dead code elimination, you could run your analysis on optimized LLVM bitcode and find the percentage of icmp/fcmp instructions that can be changed into constants. If you find a large percentage, then it is more likely that your analysis will help dead code elimination or other optimizations.

I'd also recommend that you think of other optimizations that could benefit from range analysis and at least list them in your proposal as optimizations you'll look at if time permits.

-- John T.

Hi Victor,

    I have been working on Douglas's range analysis, and today, after
toiling with it for two years, we have a very mature and robust
implementation, which is publicly available at
http://code.google.com/p/range-analysis/.

can you speed up program runtime significantly using this analysis?

Ciao, Duncan.

Hi John,

Regarding your comment about Java, I think you're correct that your
range analysis would be better at optimizing Java code. However, LLVM
really isn't used for Java, so I'm not sure if that's a strong argument
for your proposal. To get the best bang for the buck, I think your
analysis will need to work well in optimizing C/C++/Objective-C[++] code.

I use LLVM for compiling Ada. Ada turns into LLVM IR which is chock-a-block
full of range checks, so this analysis might be helpful for Ada.

One thing you could do to mitigate that problem is to do an experiment
that *shows* that your analysis has the potential to find more
optimization opportunities than what LLVM does today. For example, for
dead code elimination, you could run your analysis on optimized LLVM
bitcode and find the percentage of icmp/fcmp instructions that can be
changed into constants. If you find a large percentage, then it is more
likely that your analysis will help dead code elimination or other
optimizations.

In short, if you can speed up important programs using your analysis then that
would be a great selling point.

Ciao, Duncan.

I strongly agree. If the analysis doesn't provide a good value proposition, almost nobody will care about it.

A great use case for value range analysis (that I'm personally very interested in) is improving the performance of codes that check for integer overflows:

   http://embed.cs.utah.edu/ioc/

The synergy should be obvious. To improve the performance of these codes, someone will need to write a pass that uses value ranges to optimize the LLVM intrinsics that check for math overflows.

Ideally, the overhead of overflow checking could be reduced to the point where some users might enable it in production codes.

John Regehr

Hi John,

One thing you could do to mitigate that problem is to do an experiment
that *shows* that your analysis has the potential to find more
optimization opportunities than what LLVM does today.

I strongly agree. If the analysis doesn't provide a good value
proposition, almost nobody will care about it.

A great use case for value range analysis (that I'm personally very
interested in) is improving the performance of codes that check for
integer overflows:

    http://embed.cs.utah.edu/ioc/

from what I understand of the analysis, to come to its conclusions it assumes
that there is no overflow. That doesn't make it useless for removing integer
overflow checks: you can successively walk variables, and if you can prove that
there is no overflow of a variable X given your analysis of previously seen
variables, then X can safely be added to the set of analysed variables. Rinse
and repeat. However this probably doesn't work for variables inside loops.

Hopefully Victor can clarify.

Ciao, Duncan.

from what I understand of the analysis, to come to its conclusions it assumes
that there is no overflow. That doesn't make it useless for removing integer
overflow checks: you can successively walk variables, and if you can prove that
there is no overflow of a variable X given your analysis of previously seen
variables, then X can safely be added to the set of analysed variables. Rinse
and repeat. However this probably doesn't work for variables inside loops.

I'd also be interested to hear more from the range analysis authors about this.

Remaining faithful to the C/C++ overflow rules while operating on LLVM IR may be very tricky, particularly with respect to integer promotions and similar constructs, which may have no representation in the IR (even before optimization).

An analysis that is not sound with respect to the original C/C++ semantics would be of little use to anyone.

John

Hi, guys,

thank you for all the feedback. I will try to answer your
questions below. But, if you think that might not be a good GSoC
project, do not hesitate to tell me. I can try to write a different
proposal. Nevertheless, I would like to hear from you what you think
is important to have in the range analysis. By reading your e-mails, I
see that there are still a lot of things that we do not do, and would
be useful to the community:

can you speed up program runtime significantly using this analysis?

No, not yet. We have not used the analysis to implement any
optimization yet. So far we can only flag that variables are
dead-code, but I have not tried to remove this code. And for the C
programs that we have analyzed, the number of variables that are
dead-code, after LLVM optimizes the program, is small. We found
something like 200 dead variables in the whole gcc, for instance.
Notice, however, that the other optimizations had not caught those.

I took a brief look at your report. I’m not sure what others in the
LLVM community think (and I’d like their input), but I suspect that
10-15 seconds for analyzing GCC means that users would want your
analysis enabled at optimization levels higher than -O2.

It is a whole (inter-procedural) program analysis, with function
inlining enabled to give us a limited form of context-sensitiveness.
If I run it intra-procedurally, it takes negligible time per function.
I think its runtime is similar to other LLVM passes.

When I asked for memory usage, I meant the amount of RAM used by the
analysis. As far as I can tell, your paper only reports the number of
constraints, so it doesn’t really tell me how much RAM the analysis
uses.

I just measured it. For SPEC 2006 gcc it took 455MB.

One other thing I’ve been wondering about is whether your analysis is
able to find value ranges for the results of load instructions.

No. We do not do not use pointer analysis.

Finally, do you think it would be possible in the future to use
parallelism to improve the performance of your analysis?

We did not think about it. I think that the algorithm, in the way it
is now, is pretty sequential. We can parallelize the processing of
strong components that do not depend on each other, but I speculate
that there are not many of these.

I recommend that your proposal mention that you’ll try your analysis on
larger and more diverse codes

Yes, we want to find larger benchmarks too.

one of the big problems with Douglas’s original range analysis was that
it couldn’t handle modulo arithmetic.

We still have this problem. Jorge Navas, who is using our analysis, is
working on an implementation that deals with wrapping arithmetics, but
we did not have access to his code yet.

An analysis that is not sound with respect to the original C/C++ semantics
would be of little use to anyone.

You can use our analysis to remove overflows. If we output that a variable
is bound to the range [c1, c2], where c1 > -inf, and c2 < +inf, then you
are guaranteed to be inside these bounds. The imprecision happens when
we output that something is bound to, say, [c1, +inf], c1 > -inf, because,
in this case, you could have that the upper bound of the variable
wraps around, and then you may have it changing the lower limit c1. In
our experiments, about 75% of the non-trivial limits that we output is
[c1, c2], c1 > -inf, and c2 < +inf, and could be used to eliminate
overflow tests. For instance, in gcc we output 40,043 good limits, 22,369
limits [c, +inf], 785 limits [-inf, c], and 116,637 limits [-inf, +inf].

Also, the tricky bit of range analysis is handling loops. I suggested
to Douglas that he exploit LLVM’s SCEV infrastructure to discover and
exploit how induction variables are evolving rather than trying to
create his own poor man’s version using interval arithmetic. How are
loops handled now?

Yes, Douglas told me about this. He actually wrote a small pass that
catches induction variables using SCEV. We still catch tighter
intervals with our range analysis than using SCEV, but we miss some
induction variables that SCEV handles. Integrating SCEV into our
analysis is in the high list of priorities.

from what I understand of the analysis, to come to its conclusions it assumes
that there is no overflow. That doesn't make it useless for removing integer
overflow checks: you can successively walk variables, and if you can prove that
there is no overflow of a variable X given your analysis of previously seen
variables, then X can safely be added to the set of analysed variables. Rinse
and repeat. However this probably doesn't work for variables inside loops.

I'd also be interested to hear more from the range analysis authors about
this.

Remaining faithful to the C/C++ overflow rules while operating on LLVM IR
may be very tricky, particularly with respect to integer promotions and
similar constructs, which may have no representation in the IR (even
before optimization).

An analysis that is not sound with respect to the original C/C++ semantics
would be of little use to anyone.

I actually disagree on the last point. For static array bounds checking with SAFECode, we want to assume that all integer operations can overflow (including those with the nsw attribute). We don't care about the other integer semantic rules from C (like the promotion rules) or whether overflow is language defined or not (for those who don't know, unsigned ints have defined overflow in C; signed ints do not). All we want to know is whether a pointer p is within the bounds of a set of valid objects, and we just need to take integer overflow into account because it can happen on the hardware.

-- John T.

I actually disagree on the last point. For static array bounds checking with SAFECode, we want to assume that all integer operations can overflow (including those with the nsw attribute). We don't care about the other integer semantic rules from C (like the promotion rules) or whether overflow is language defined or not (for those who don't know, unsigned ints have defined overflow in C; signed ints do not). All we want to know is whether a pointer p is within the bounds of a set of valid objects, and we just need to take integer overflow into account because it can happen on the hardware.

I'd have to see some specific examples to figure out if what you're saying makes sense. All of my experience with integer overflows in C/C++ had lead me to the conclusion that playing games with the semantics usually gets you into hot water.

John

No, not yet. We have not used the analysis to implement any
optimization yet. So far we can only flag that variables are
dead-code, but I have not tried to remove this code. And for the C
programs that we have analyzed, the number of variables that are
dead-code, after LLVM optimizes the program, is small.

Even if only a few variables become dead, it might still be the case that many dynamic branches can be eliminated. I'd encourage you to try this, particularly on the Ada codes that Duncan mentioned and the output of the integer overflow checking tool that I mentioned.

One transformation that we found to be quite useful when implementing a range analysis for C was a debugging mode that inserted range assertions into the generated code. This was an easy way to spot implementation errors that otherwise would have been quite hard to detect.

Do you know how your results compare to GCC's existing value range propagation pass?

Anyway I think this sounds like an interesting project and potentially a useful one.

John

Hi Victor,

> one of the big problems with Douglas's original range analysis was that
> it couldn't handle modulo arithmetic.

We still have this problem. Jorge Navas, who is using our analysis, is
working on an implementation that deals with wrapping arithmetics, but
we did not have access to his code yet.

can you please clarify whether the pass only looks at operations with the
nsw flag (and bails out on others), or just assumes that there is no wrapping
behaviour anywhere. It used to just assume that nothing wrapped, which made
all stated results about bit shrinking, dead variables found etc pointless
since they were based on an incorrect analysis.

> An analysis that is not sound with respect to the original C/C++ semantics
> would be of little use to anyone.

You can use our analysis to remove overflows. If we output that a variable
is bound to the range [c1, c2], where c1 > -inf, and c2 < +inf, then you
are guaranteed to be inside these bounds.

Is this really true? For example, suppose you know that X is in the range
[1, +inf], and now you calculate Y = 1 / X, then you get that Y is in the
range [0, 1]. But there is no guarantee that Y is really in that range:
since X might have overflowed it might for example be equal to -1, in which
case Y would be equal to -1 too, outside the range [0, 1]. In short, I doubt
you can conclude that a variable Y is really in a range [c1, c2] just from the
information that c1 > -inf and c2 < +inf. I think you also need to look at the
history of how you got there.

Ciao, Duncan.

Another excellent use for range analysis would be to warn about signed operations that will definitely overflow.

John

Is this really true? For example, suppose you know that X is in the range
[1, +inf], and now you calculate Y = 1 / X, then you get that Y is in the
range [0, 1]. But there is no guarantee that Y is really in that range:
since X might have overflowed it might for example be equal to -1, in which
case Y would be equal to -1 too, outside the range [0, 1]. In short, I doubt
you can conclude that a variable Y is really in a range [c1, c2] just from the
information that c1 > -inf and c2 < +inf. I think you also need to look at the
history of how you got there.

Duncan these problems can definitely be solved. In your example, we would need to have avoided giving X the wrong interval value in the first place.

The problem with overflow isn't that it makes sound analysis impossible, it's that it can kill precision.

Here's GCC's value range propagation module, which is definitely intended to be sound since it feeds the optimizer:

   http://gcc.gnu.org/svn/gcc/trunk/gcc/tree-vrp.c

John

Hi John,

Is this really true? For example, suppose you know that X is in the range
[1, +inf], and now you calculate Y = 1 / X, then you get that Y is in the
range [0, 1]. But there is no guarantee that Y is really in that range:
since X might have overflowed it might for example be equal to -1, in which
case Y would be equal to -1 too, outside the range [0, 1]. In short, I doubt
you can conclude that a variable Y is really in a range [c1, c2] just from the
information that c1 > -inf and c2 < +inf. I think you also need to look at the
history of how you got there.

Duncan these problems can definitely be solved.

I didn't say it couldn't be solved, I was just pointing out that Victor probably
made a wrong statement.

Ciao, Duncan.

can you please clarify whether the pass only looks at operations with the
nsw flag (and bails out on others), or just assumes that there is no wrapping
behaviour anywhere.

It handles operations in the same way regardless of nsw flag.

Another excellent use for range analysis would be to warn about signed operations that will definitely overflow.

Good idea. I'll include your suggestion in my proposal.

Is this really true? For example, suppose you know that X is in the range
[1, +inf], and now you calculate Y = 1 / X, then you get that Y is in the
range [0, 1]. But there is no guarantee that Y is really in that range:
since X might have overflowed it might for example be equal to -1, in which
case Y would be equal to -1 too, outside the range [0, 1]. In short, I doubt
you can conclude that a variable Y is really in a range [c1, c2] just from the
information that c1 > -inf and c2 < +inf. I think you also need to look at the
history of how you got there.

Duncan, you are right. We thought that we were treating all the
possible cases where we could get an overflow (we handle 18 bitcodes),
but we forgot this bug in division. But I think that after fixing it,
we can still provide an implementation of range analysis that ensures
that [c1, c2], c1, c2 in Z indicate that an overflow did not happen to
arrive in this variable. What do you think? There are only 18
instructions that produce good intervals, so we should be able to
prove that a safe implementation is free of overflows in integer
limits.
Even if we use a different domain, say, rings (the module domain),
it seems rather tricky to me to handle overflows conservatively. Could
any of you recommend us any papers that deal with the wrapping
semantics of integer arithmetics in the context of range analysis? We
here also agree that we should do something more effective to deal
with integer overflows. So far, we want to ensure that all the integer
limits, e.g., [c1, c2], c1, c2 in Z are free of overflows. We thought
that we were doing it, but there are still some bugs to treat in the
analysis, as Duncan has pointed. One problem is that in order to give
this kinds of guarantees, the analysis becomes more conservative than
we wish it would have to be.