5 ms·

I think it’s less like doubting that the given panic works and more like an extremely thorough proof that all possible branches of the control flow have accepta

I think it’s less like doubting that the given panic works and more like an extremely thorough proof that all possible branches of the control flow have acceptable behavior. If you haven’t tested a given control flow, the issue is that it’s possible that the end result is some indeterminate or invalid state for the whole program, not that the given bounds check doesn’t panic the way it’s supposed to. On embedded for example (which is an important usecase for SQLite) this could result in orphaned or broken resources.

thayne 1y ago
But does it matter if that control flow is unreachable? If the check never fails, it is logically equivalent to not having the check. If the code isn't "correct" and the panic is reached, then the equivalent c code would have undefined behavior, which can be much worse than a panic.
- nubbler 1y ago
  In the first case, if it is actually unreachable, I would never want that code ending up in my binary at all. It must be optimised out. Your second case implies that it is reachable.
  - thayne 1y ago
    In the first case, it often is optimized out. But the optimizer isn't perfect, and can't detect every case where it is unreachable. If you have the second case, I would much rather have a panic than undefined behavior. As mentioned in another comment, in c indexing an array is semantically equivalent to: if (i < len(arr)) arr[i] else UB() In fact a c compiler could put in a check and abort if it is out of bounds, like rust does and still be in spec. But the undefined behavior could also cause memory corruption, or cause some other subtle bug.
jonahx 1y ago
> I think it’s less like doubting that the given panic works and more like an extremely thorough proof that all possible branches of the control flow have acceptable behavior. The way I was thinking about it was: if you somehow magically knew that nothing added by the compiler could ever cause a problem, it would be redundant to test those branches. Then wondering why a really well tested compiler wouldn't be equivalent to that. It sounds like the answer is, for the level of soundness sqlite is aspiring to, you can't make those assumptions.

thayne 1y ago

But does it matter if that control flow is unreachable? If the check never fails, it is logically equivalent to not having the check. If the code isn't "correct" and the panic is reached, then the equivalent c code would have undefined behavior, which can be much worse than a panic.

nubbler 1y ago
In the first case, if it is actually unreachable, I would never want that code ending up in my binary at all. It must be optimised out. Your second case implies that it is reachable.
- thayne 1y ago
  In the first case, it often is optimized out. But the optimizer isn't perfect, and can't detect every case where it is unreachable. If you have the second case, I would much rather have a panic than undefined behavior. As mentioned in another comment, in c indexing an array is semantically equivalent to: if (i < len(arr)) arr[i] else UB() In fact a c compiler could put in a check and abort if it is out of bounds, like rust does and still be in spec. But the undefined behavior could also cause memory corruption, or cause some other subtle bug.

jonahx 1y ago

> I think it’s less like doubting that the given panic works and more like an extremely thorough proof that all possible branches of the control flow have acceptable behavior. The way I was thinking about it was: if you somehow magically knew that nothing added by the compiler could ever cause a problem, it would be redundant to test those branches. Then wondering why a really well tested compiler wouldn't be equivalent to that. It sounds like the answer is, for the level of soundness sqlite is aspiring to, you can't make those assumptions.