| 12345678910111213141516171819202122232425262728293031323334353637383940414243 |
- // SPDX-License-Identifier: GPL-3.0-or-later
- // Copyright © 2019 Ariadne Devos
- /* TODO: apparently, cmov was introduced in i686
- -- portable tissues */
- /* Side-channel considerations: all passed values are not secret. */
- /* Operational semantics: If %0 > %1, do %0 <- %1.
- Functional semantics:
- In case \old(%0) >(*) \old(%1) (branch taken),
- - \old(%1) = min(\old(%0), \old(%1)) (case analysis)
- - \new(%0) = \old(%1) = min(\old(%0), \old(%1)) (assignment, previous lemma)
- Otherwise, the negation holds: \old(%0) <= \old(%1),
- - \old(%0) = min(\old(%0), \old(%1)) (case analysis)
- - \new(%0) = \old(%0) = min(\old(%0), \old(%1)) (no assignment, previous lemma)
- (*) '>=' also suffices.
- Therefore, \new(%0) = min(\old(%0), \old(%1)) (consider both branches)
- -- Assembly sequence
- The Intel / AT&T syntax differences in operand order are
- very confusing. Testing:
- Try "mov $0, %0". It compiles, so the first operand is the source,
- and the latter the destination. That proofs the second operand of
- "cmov??" is correct: it is %0, `*x_set_p` that must be updated.
- Another source of confusion is Intel's distinction between greater / less
- and above / below. The former is signed, the latter unsigned.
- To test: 2 (operand order of cmp) * 2 (above / below).
- Pass: %0,%1,below; %1,%0,above.
- (These two are equivalent: %0 < %1 <-> %1 > 0.
- Sanity check succeeds.)
- cc: condition code is changed by 'cmp'. */
- #define _sHT_min(x_set_p, y) \
- __asm__("cmp %1,%0;cmova %1,%0" : "+r" (*(x_set_p)) : "r" (y) : "cc")
|
