<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/80434>80434</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            Top definition is unsound
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            new issue
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          ymand
      </td>
    </tr>
</table>

<pre>
    When `BoolValues` were [refactored](https://github.com/llvm/llvm-project/commit/fc9821a877d4e1443603d67539e4369b3ec72890) so to split out Formulas, `Top` was redefined. In the new definition, a given Top instance has a specific fixed Atom, which violates the invariant that all Top are equivalent, which is crucial for soundness. Indeed, the only reason we didn't implement Top with a singleton was a technical constraint in the SAT solver.

In the old version, when Top is unpacked, it generates a fresh atom. In the new version, an atom is chosen when Top is created. Here's the comment:
```
/// A TopBoolValue represents a boolean that is explicitly unconstrained.
///
/// This is equivalent to an AtomicBoolValue that does not appear anywhere
/// else in a system of formula.
/// Knowing the value is unconstrained is useful when e.g. reasoning about
/// convergence.
```
Unfortunately, this is incorrect. Once Top is used, the atom can leak into the environment and become constrained. This leads to unsoundness, for example:

```
// Key:
// x -> Top(V1) means "x maps to a Top value with atom V1".
// FC means "flow condition"
bool x = ...
bool cond();
bool foo();
// x -> Top(V1)
bool b = ...;
if (b) { ... }
else {
 if (!x) return;
  // x -> V1 and FC = V1
  while(cond())
    x = foo();
  // x -> Top(V2)
}
// FC = !b implies V1
// x -> Top(V1), because comparison equates all Tops and we take the left one
// (the then branch), on which `x` is unchanged.
if (!b) {
  bool wrong = x;
  // x -> V1, unpacked from Top(V1)
  // wrong -> V1
  // From FC, we incorrectly conclude V1 is true from which anything follows...
}
```
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyUVkuP2zYQ_jX0ZRBBprS2fPBhHzVa5NBDt9vziBpZbChSISk__n0xlC17naZAgSC7S87zm28-EUPQe0u0FU8v4ultgWPsnN-ee7TNonbNeftXRxbEKn9xznygGSmIVQ5H8gTi6cVTiyo6T414ehOy6mIcgiiehdwJudvr2I11plwv5M6Yw_XHl8G7v0lFIXfK9b3mX1q1qeQSq_W6KWlZlsUqL5rV-qnYUFmsNnVBai2rTS7kBoKD6CAMRkdwY4Sd8_1oMAj5yqW-uyHViAE8NdRqS00Gv1mIHYGlI6QzHbWz7IGw1wey8O4G0DZEtIqgwwAIYSClW62g1Sdq4DlyJ69w7LTq4KCdwUghhdX2gF6jjRA7jIDGpHjoCej7qA9oyMabrw6g_Kg0Gmidh-BG21gKgctsiBq25LDOmjN4wuAsHAka3Vgh1xF0PxjqycaU5ahjx9VquzcU2TRVH0l1Vis0oJwN0aO2EfQEwx_P7xCcOZDPRP4m8ufp_wtIzjRwIB8uCB27KzwBRjug-jZVqCPsyZJPKCC0nkIHGF3_Ce27QGjTdWq_c4Hsp9DKE0Ye1a_kScj1hCwzhLErLiWKVX75N_2ZmCbkDp45zkxT8DR4CmQjl1Y7ZwjtNBwdgE6D0UpHc4bRzuhQkz0Efczx3umQ_OeZMhPRJmpodcueEjWOAlgXAYeB0APa87Hj3h6ikgnMIB7hOUTqwbVMC-b0Y0Hw1bqjtvsEzSGlSkO56yEdBGpHM6FL2T67cIgdsXZjfIyqnD2Q35NVlP0rzH_a1vk4WoxkzhM7JyS0Vc57UjGD33lxrjQJNxKnkSu0YAi_gbbRpWOyB-2dTSxG20BNyvUE99OY8DaETWCcRzsvCsfmzaET8irc2PFzjsBXOt_spqMTfBHFL1y0kNXHksWlJ7QBhJQn6HFIeTF1NaE97Rp3xOby03xg93pzb407cjPNRWjkZMlMhBOI4g2yLLs7Y1MhKyE3oni5O2-dezj-ae13XvWc4eqlWxCyqrlFsX7hKxDrt-kuEVCsL5YwmQq5PLG1pzh6O8cB-Jz_Y5mmt3tNGT-WV6tjpw0JWd31da0QAC4Q_NjcY_hLe3J2nou-Yc6RhFzWSRY1hbmKnyMlX5lvOIYkMAN6zRJL38dJyyb5DqmzI0HEb5Q4a6iN4OynDWas-C7ystUereouGViJk9yLVX7iT9K0qh3a_Sw1M9bXyVxhSGM8emf3qb_TfwyAc111GVrv-h9JMTtNEa-On-927Lp7TZJPt802ZyanMmNDPG0dIPqRpkRTf2jPsWNxaZ0x7hhmZt-Gdd3IRbMtmk2xwQVtl-t8VVV5VVWLbkttqVZPVG2KetPUFW1WkpA_-1WFyxybhd7KXJa5zOWyKMpyleFySUXV1mVVyjpXJMqcetQm4zdG5vx-oUMYaVvlZVEuDNZkQnroSMnfpXTJe_n0tvDb9C6px30QZW50iOEWJepoaMsScHs4TKNMcrQYvdn-74dPyh6E3KXq_gkAAP__aYHtrw">