Avoid materializing opaque string literals

pulse/Pulse.Lib.C.Array.fst

@@ -27,7 +27,8 @@ let array_spec_initd #a (s: array_spec a) (i: nat) : prop = i < Seq.length s /\
 let array_spec_mask #a (s: array_spec a) (i: nat) : prop = i < Seq.length s /\ ~(OutOfMask? (Seq.index s i))
 let array_spec_idx #a (s: array_spec a) (i: nat { array_spec_initd s i }) : Tot a = let Val x = Seq.index s i in x
 
-let array_literal_to_ref #a #n (_: full_array_lspec a n) : Tot (R.ref a) =
+let string_literal_to_ref #a (_literal_identity: string) :
+  Tot (r:R.ref a { not (r == R.null) }) =
   admit ()
 
 let to_mask #t (s: array_spec t) (i: nat) : prop = array_spec_mask s i

pulse/Pulse.Lib.C.Array.fsti

@@ -39,10 +39,14 @@ let array_spec_full #a (s: array_spec a) =
 let full_array_spec a = s: array_spec a { array_spec_full s }
 let full_array_lspec a (l: nat) = s:full_array_spec a { array_spec_len s == l }
 
-// C string literals have static storage duration. PAL exposes only their address
-// here; clients still need an explicit model before dereferencing a literal
-// returned through an ownership-free (`_plain`) pointer.
-val array_literal_to_ref #a #n (s: full_array_lspec a n) : Tot (R.ref a)
+// C string literals have static storage duration. PAL exposes only their
+// non-null address here; clients still need an explicit ownership model before
+// dereferencing a literal returned through an ownership-free (`_plain`) pointer.
+//
+// The literal identity keeps repeated evaluations of one literal stable without
+// asserting whether distinct literals are merged by the C implementation.
+val string_literal_to_ref #a (literal_identity: string) :
+  Tot (r:R.ref a { not (r == R.null) })
 
 val array_spec_ext #a (s1 s2: array_spec a) :
   Lemma (requires

src/pass/emit.rs

@@ -584,6 +584,7 @@ struct Emitter<'a> {
     /// 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>,
 }
 
 impl<'a> Emitter<'a> {
@@ -601,6 +602,15 @@ impl<'a> Emitter<'a> {
         tmp
     }
 
+    fn string_literal_identity(&mut self, literal: &Rc<Expr>) -> String {
+        let next_id = self.string_literal_ids.len();
+        let id = *self
+            .string_literal_ids
+            .entry(Rc::as_ptr(literal))
+            .or_insert(next_id);
+        format!("{}:{id}", self.current_module)
+    }
+
     /// Emit a Name with full module qualification when it refers to a different module.
     fn emit_name(&mut self, name: Name) -> Doc {
         let mangled = self.nm.mangle(&name).to_string();
@@ -2471,20 +2481,24 @@ impl<'a> Emitter<'a> {
                             TypeT::FixedArray(_, _),
                             TypeT::Pointer(_, PointerKind::Ref | PointerKind::Unknown),
                         ) => {
-                            let fn_name = if matches!(
+                            if matches!(
                                 &val.val,
                                 ExprT::ArrayInit {
                                     is_static: true,
                                     ..
                                 }
                             ) {
                                 // String literals have static storage duration,
-                                // unlike local fixed-size arrays.
-                                "Pulse.Lib.C.Array.array_literal_to_ref"
+                                // unlike local fixed-size arrays. The trusted
+                                // model exposes no contents or ownership.
+                                let literal_identity = self.string_literal_identity(val);
+                                unaryfn(
+                                    Doc::text("Pulse.Lib.C.Array.string_literal_to_ref"),
+                                    Doc::text(format!("{literal_identity:?}")),
+                                )
                             } else {
-                                "Pulse.Lib.C.Array.array_to_ref"
-                            };
-                            unaryfn(Doc::text(fn_name), val_doc)
+                                unaryfn(Doc::text("Pulse.Lib.C.Array.array_to_ref"), val_doc)
+                            }
                         }
                         // `core_ref` (raw `_core_ref` back-pointer) → typed `ref T`:
                         // recover the typed reference. The pointee type is known
@@ -6633,6 +6647,7 @@ pub fn emit_multifile(diags: &mut Diagnostics, tu: &TranslationUnit) -> Vec<Emit
         fn_module_map,
         typedef_override_map,
         tmp_counter: 0,
+        string_literal_ids: HashMap::new(),
     };
 
     for decl in &tu.decls {

test/stringlit/stringlit.c

@@ -1,6 +1,13 @@
 #include "pal.h"
+#include <stdint.h>
 #include <stdlib.h>
 
+#define OBSERVE_MACRO_LITERALS()                                               \
+    do {                                                                       \
+        observe("macro-first");                                                \
+        observe("macro-second");                                               \
+    } while (0)
+
 void write(const _array char *data, size_t nbytes)
     _requires(data._length == nbytes);
 
@@ -10,6 +17,10 @@ void foo() {
     write("hello", 6);
 }
 
+void observe_string_literal() {
+    observe("hello");
+}
+
 void write_compound_literal() {
     write((char[]){'o', 'k', '\0'}, 3);
 }
@@ -18,6 +29,25 @@ void observe_compound_literal() {
     observe((char[]){'o', 'k', '\0'});
 }
 
-_plain const char *get_name() {
+_plain const char *get_name()
+    _ensures(return != NULL)
+{
     return "hello";
 }
+
+_plain const char *get_indexed_name(uint32_t index)
+    _ensures(return != NULL)
+{
+    switch (index) {
+    case 0:
+        return "zero";
+    case 1:
+        return "one";
+    default:
+        return "other";
+    }
+}
+
+void observe_macro_literals() {
+    OBSERVE_MACRO_LITERALS();
+}