Operational semantics and high-level vs low-level

[Centril]

@ojeda

FYI you may want to take a look at the effort going on to start standardizing similar features for C and C++ (P1315 for C++, soon for C too). If this paper goes through, we may get some "secure clear" primitive/built-in in LLVM which we may be able to take advantage from rustc too, both for explicit clearing (e.g. zeroize ) as well as stack clearing by the compiler.

An approach for the wording would be to lift the provision in [intro.abstract]p1 (i.e. the “as-if” rule) for calls to this function; thus conforming implementations need to emulate the behavior of the abstract machine and therefore produce code equivalent to having called the function, even if it has no effect on the observable behavior of the program. This is the same approach C11 takes for memset_s :

Unlike memset , any call to the memset_s function shall be evaluated strictly according to the rules of the abstract machine as described in (5.1.2.3). That is, any call to the memset_s function shall assume that the memory indicated by s and n may be accessible in the future and thus must contain the values indicated by c .

It's not clear to me what this means and how this could be specified operationally.