upvote
I think it's worth pointing out the compiler usually won't do much (if any) of this kind of check unless you tell it to.

When you tell it to, you usually have good control around what kind of thing you want it to consider a problem, how much effort you want it to spend trying to prove that, and what should happen with code it can't prove that property for. Most commonly, people just use the "tell me if I've made an obviously dumb infinite loop which does nothing useful while it runs".

E.g. y-cruncher does something other than infinitely loop for no reason so it wouldn't trigger the loop detection logic on most anyone's compilation settings.

On the other hand, a loop which does nothing but run until the last digit of pi would either trigger the compiler to say this is a useless infinite loop or to say it isn't able to prove this loop stops (almost certainly the latter, as such a loop is a great example of going out of your way to fool the compiler).

A loop which sometimes terminates and sometimes doesn't depending on runtime input would depend on your compiler settings, but almost always nobody sets it in a way to say that's a problem (and when they do almost always it's not possible for the compiler to prove one way or the other) if their compiler even supports that kind of analysis.

reply
Interestingly, in C++, a trivial infinite loop is undefined behavior. So the compiler not only doesn’t have to detect it, it is allowed to assume you didn’t do it. [0] This is inconvenient when you actually want a trivial infinite loop. (C++26 was going to fix this, but it seems we may not ever get a C++26…)

[0] https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p28...

reply
to my knowledge, they detect some common intentional and unintentional infinite loop patterns, but not much more:

    for(;;) // intentional

    for(unsigned i=10;i>=0;i--)
    for(int i=0;j<10;i++)
    for(unsigned i=0;i!=100;i+=8)
    // unintentional
in C infinite loops with no side effects are UB, so detecting them is useful for diagnostics.

guaranteed termination also is needed for some optimizations. but since side-effect-less infinite loops are UB in C, a compiler doesn't have to prove that such a loop terminates, it can just assume it does. other languages may differ, but I don't think any of them prove convergence of algorithms.

a don't-mind-the-recursion flag can be `-fno-finite-loops` on clang, or a read or write to a `volatile` variable in standard C.

reply
How does the compiler know whether it's just really long or infinite?

One straightforward approach is to use Hoare logic [1], specifically the method of loop invariants and loop conditions. If you have a loop where the conditions are expressed only in terms of invariants then the conditions will never change truth values during iteration of the loop, thus you have an infinite loop.

Now, some loops are written deliberately like this, i.e. "while (true)", and so there you need to look at whether the body of the loop contains any side effects (reading input, printing, etc). Then you have what is called a "productive infinite loop", such as an event loop or a REPL. Of course you can't prove this sort of loop will ever halt, since the user may never elect to issue the quit command, but these sorts of loops often tend to spend most of their time with the process sleeping until the operating system wakes them up to handle an event.

[1] https://en.wikipedia.org/wiki/Hoare_logic

reply
That’s the point of the halting problem You can’t know if it will halt absolutely
reply
[dead]
reply
[dead]
reply