Avoid materializing opaque string literals - #179
Conversation
PAL intentionally models a string literal decayed to an ownership-free _plain pointer as an opaque address. The resulting ref carries no points-to resource, so verified code may pass, return, or compare it but cannot dereference it; callers that need contents must use an explicit ownership-bearing model such as _array. The previous primitive accepted the complete literal array specification even though its result exposed no relation to those contents. Building that unused argument generated character-conversion terms and proof obligations for every literal. Replace it with a compact identity token assigned deterministically to each literal AST node during emission. Because string_literal_to_ref is an abstract pure function, repeated evaluations of one token produce a stable address, while references from different tokens have no asserted equality or inequality, permitting implementation-defined literal merging without collapsing distinct literals to one term. Expose the C guarantee that literal addresses are non-null, but still provide no ownership. Extend stringlit coverage with direct decay to a _plain argument, non-null borrowed returns, a switch returning several independently identified literals, and two literals from one macro expansion that must receive distinct tokens. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
|
This seems like a bad idea. We want to be able to reason about the contents of string literals in the future, and this pretty much blocks the obvious way there.
Does this happen once when we use the string literal, or every single time we run the Pulse prover? I would do the following: generate an auxiliary (F*-)global variable We already know that we can handle large arrays (with a couple thousand elements) efficiently, see the global array tactics example. If the character literals generate a VC, then we should fix that so that they emit |
| /// Maps typedef names that are OpaqueTypeDecls to their Type_* module (overrides Typedef_*). | ||
| typedef_override_map: HashMap<Rc<str>, String>, | ||
| tmp_counter: usize, | ||
| string_literal_ids: HashMap<*const Expr, usize>, |
There was a problem hiding this comment.
| string_literal_ids: HashMap<*const Expr, usize>, | |
| string_literal_ids: HashMap<Rc<Expr>, usize>, |
We should not rely on pointer equality
|
Alternatively we could also translate string literals to pure const global arrays in an IR pass. |
|
Just to be clear: adding an identity argument to array_literal_to_ref to avoid spurious proofs of pointer equality is great, it's the other changes that need work. |
2 participants
PAL intentionally models a string literal decayed to an ownership-free _plain pointer as an opaque address. The resulting ref carries no points-to resource, so verified code may pass, return, or compare it but cannot dereference it; callers that need contents must use an explicit ownership-bearing model such as _array.
The previous primitive accepted the complete literal array specification even though its result exposed no relation to those contents. Building that unused argument generated character-conversion terms and proof obligations for every literal. Replace it with a compact identity token assigned deterministically to each literal AST node during emission.
Because string_literal_to_ref is an abstract pure function, repeated evaluations of one token produce a stable address, while references from different tokens have no asserted equality or inequality, permitting implementation-defined literal merging without collapsing distinct literals to one term. Expose the C guarantee that literal addresses are non-null, but still provide no ownership.
Extend stringlit coverage with direct decay to a _plain argument, non-null borrowed returns, a switch returning several independently identified literals, and two literals from one macro expansion that must receive distinct tokens.