vir: sanitize non-SMT identifiers at AIR ident construction time (fix #2221)

source/air/src/printer.rs

@@ -589,6 +589,7 @@ impl NodeWriter {
             sise::SpacedStringWriterNodeOptions { break_line_len: if brk { 0 } else { break_len } };
         match node {
             Node::Atom(a) => {
+                assert!(sise::check_atom(a), "invalid atom: {}", a);
                 writer.write_atom(a, opts).unwrap();
             }
             Node::List(l) => {

source/rust_verify_test/tests/regression.rs

@@ -1,4 +1,5 @@
 #![feature(rustc_private)]
+#![allow(mixed_script_confusables)]
 #[macro_use]
 mod common;
 use common::*;
@@ -1587,3 +1588,132 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] raw_identifiers_in_smt_2221 verus_code! {
+        // Raw identifiers (r#keyword) must be sanitized before reaching AIR/SMT-LIB,
+        // since '#' is not a valid SMT-LIB simple-symbol character.
+        // Test a representative set of Rust strict keywords as function names,
+        // parameters, local variables, struct fields, and enum variants.
+
+        struct r#struct {
+            r#type: u32,
+            r#loop: u32,
+        }
+
+        enum r#enum {
+            r#match,
+            r#impl,
+        }
+
+        fn r#match(
+            r#in: u32,
+            r#out: u32,
+            r#for: u32,
+            r#while: u32,
+            r#return: u32,
+            r#break: u32,
+            r#continue: u32,
+            r#if: u32,
+            r#else: u32,
+            r#let: u32,
+            r#mut: u32,
+            r#ref: u32,
+            r#move: u32,
+            r#const: u32,
+            r#static: u32,
+            r#unsafe: u32,
+            r#where: u32,
+            r#async: u32,
+            r#await: u32,
+            r#dyn: u32,
+            r#as: u32,
+            r#use: u32,
+            r#pub: u32,
+            r#mod: u32,
+        ) -> u32
+            requires r#in == r#out
+        {
+            let r#type = r#in;
+            let r#loop = r#for;
+            let r#match = r#while;
+            let r#impl = r#return;
+            let r#enum = r#break;
+            let r#struct = r#continue;
+            let r#trait = r#if;
+            let r#let = r#else;
+            let r#mut = r#let;
+            let r#ref = r#mut;
+            let r#move = r#ref;
+            let r#const = r#move;
+            let r#static = r#const;
+            let r#unsafe = r#static;
+            let r#where = r#unsafe;
+            let r#async = r#where;
+            let r#await = r#async;
+            let r#dyn = r#await;
+            let r#as = r#dyn;
+            let r#use = r#as;
+            let r#pub = r#use;
+            let r#mod = r#pub;
+            assert(r#type == r#out);
+            r#type
+        }
+
+        fn raw_param(r#for: u32) -> u32 { r#for }
+    } => Ok(())
+}
+
+test_verify_one_file! {
+    #[test] unicode_identifiers_in_smt_2221 verus_code! {
+        // Unicode identifiers must be sanitized before reaching AIR/SMT-LIB,
+        // since non-ASCII characters are not valid in SMT-LIB simple symbols.
+        // Test unicode in types, fields, enums, traits, generics, functions,
+        // parameters, locals, constants, and spec/proof functions.
+
+        struct Wrapperα<Tβ> {
+            payloadγ: Tβ,
+            extraδ: u32,
+        }
+
+        enum Choiceε<Tζ> {
+            OptionAη,
+            OptionBθ(Tζ),
+        }
+
+        trait Traitι {
+            spec fn methodκ(&self) -> int;
+        }
+
+        impl Traitι for Wrapperα<u32> {
+            spec fn methodκ(&self) -> int { self.payloadγ as int + self.extraδ as int }
+        }
+
+        spec fn αβγ(x: u32) -> u32 { x }
+
+        const MAXλ: u32 = 42;
+
+        proof fn test_unicode<Genμ>(item: Wrapperα<u32>, choice: Choiceε<u32>)
+            requires item.payloadγ == MAXλ
+        {
+            let baseν = item.payloadγ;
+            let scaledξ = αβγ(1u32);
+            let valueο = MAXλ;
+            assert(baseν == MAXλ);
+            assert(scaledξ == 1u32);
+            assert(valueο == 42);
+            assert(item.methodκ() == MAXλ as int + item.extraδ as int);
+        }
+    } => Ok(_err) => {
+        // Verification succeeds; the only warnings are the mixed_script_confusables
+        // lint about using non-ASCII identifiers, which is a Rust lint unrelated to AIR sanitization.
+        assert!(_err.errors.is_empty(), "unexpected errors: {:?}", _err.errors);
+        for w in &_err.warnings {
+            let msg = &w.message;
+            assert!(
+                msg.contains("mixed script confusables") || msg.contains("warning emitted"),
+                "unexpected warning: {:?}", msg
+            );
+        }
+    }
+}

source/vir/src/def.rs

@@ -92,6 +92,8 @@ const BITVEC_TMP_DECL_SEPARATOR: &str = "$$$$bitvectmp";
 const USER_DEF_TYPE_INV_TMP_DECL_SEPARATOR: &str = "$$$$userdeftypeinvpass";
 const KRATE_SEPARATOR: &str = "!";
 const PATH_SEPARATOR: &str = ".";
+// Extra ASCII symbols allowed in AIR/SMT-LIB symbols (besides alphanumeric)
+const AIR_EXTRA_SYMBOLS: &str = "~!@$%^&*_-+=<>.?/";
 const PATHS_SEPARATOR: &str = "/";
 const VARIANT_SEPARATOR: &str = "/";
 const VARIANT_FIELD_SEPARATOR: &str = "/";
@@ -303,9 +305,44 @@ pub const SPLIT_POST_FAILURE: &str = "split postcondition failure";
 
 pub const PERVASIVE_ASSERT: &[&str] = &["pervasive", "assert"];
 
+/// Prefix added to mangled identifiers so they are easily recognizable in AIR output.
+const MANGLE_PREFIX: &str = "$V$";
+
+/// Sanitize an identifier string for use in AIR/SMT-LIB.
+/// AIR atoms may only contain ASCII alphanumeric characters and:
+///   ~ ! @ $ % ^ & * _ - + = < > . ? /
+/// We leave '_' untouched (so normal identifiers are unchanged) and encode any
+/// other illegal character as `${hex}$`.  This is injective because `$` is not a
+/// valid character in Rust identifiers, so an encoded identifier can never collide
+/// with an unencoded one, and the hex encoding itself is unambiguous.
+///
+/// If the identifier has already been mangled (e.g. when an AIR ident is reused
+/// as part of a larger generated name like a qid), we return it unchanged.
+pub fn sanitize_to_air_ident(name: &str) -> String {
+    if name.starts_with(MANGLE_PREFIX) {
+        return name.to_string();
+    }
+    let mut res = String::with_capacity(name.len() + MANGLE_PREFIX.len());
+    let needs_encode =
+        name.chars().any(|c| !c.is_ascii_alphanumeric() && !AIR_EXTRA_SYMBOLS.contains(c));
+    if !needs_encode {
+        return name.to_string();
+    }
+    res.push_str(MANGLE_PREFIX);
+    for c in name.chars() {
+        if c.is_ascii_alphanumeric() || AIR_EXTRA_SYMBOLS.contains(c) {
+            res.push(c);
+        } else {
+            res.push('$');
+            res.push_str(&format!("{:x}", c as u32));
+            res.push('$');
+        }
+    }
+    res
+}
+
 pub fn krate_to_string(krate: &Ident) -> String {
     // rustc allows crate names to begin with digits and to contain unicode
-    // TODO: Rust identifiers can in general contain unicode; we should handle this in general
     let krate = krate.escape_default().to_string();
     let krate = krate.replace('\\', PREFIX_ESCAPE);
     let krate = krate.replace('{', PREFIX_ESCAPE);
@@ -520,19 +557,19 @@ pub fn global_type() -> Path {
 }
 
 pub fn prefix_dcr_id(ident: &Path) -> Ident {
-    Arc::new(PREFIX_DCR_ID.to_string() + &path_to_string(ident))
+    Arc::new(PREFIX_DCR_ID.to_string() + &sanitize_to_air_ident(&path_to_string(ident)))
 }
 
 pub fn prefix_type_id(ident: &Path) -> Ident {
-    Arc::new(PREFIX_TYPE_ID.to_string() + &path_to_string(ident))
+    Arc::new(PREFIX_TYPE_ID.to_string() + &sanitize_to_air_ident(&path_to_string(ident)))
 }
 
 pub fn prefix_dyn_id(ident: &Path) -> Ident {
-    Arc::new(PREFIX_DYN_ID.to_string() + &path_to_string(ident))
+    Arc::new(PREFIX_DYN_ID.to_string() + &sanitize_to_air_ident(&path_to_string(ident)))
 }
 
 pub fn prefix_fndef_type_id(fun: &Fun) -> Ident {
-    Arc::new(PREFIX_FNDEF_TYPE_ID.to_string() + &fun_to_string(fun))
+    Arc::new(PREFIX_FNDEF_TYPE_ID.to_string() + &sanitize_to_air_ident(&fun_to_string(fun)))
 }
 
 pub fn prefix_tuple_type(i: usize) -> Path {
@@ -572,7 +609,13 @@ pub(crate) fn impl_closure(kind: ClosureKind, id: usize) -> Ident {
 
 pub fn projection(decoration: bool, trait_path: &Path, name: &Ident) -> Ident {
     let proj = if decoration { PREFIX_PROJECT_DECORATION } else { PREFIX_PROJECT };
-    Arc::new(format!("{}{}{}{}", proj, path_to_string(trait_path), PROJECT_SEPARATOR, name))
+    Arc::new(format!(
+        "{}{}{}{}",
+        proj,
+        sanitize_to_air_ident(&path_to_string(trait_path)),
+        PROJECT_SEPARATOR,
+        sanitize_to_air_ident(name)
+    ))
 }
 
 pub fn projection_pointee_metadata(decoration: bool) -> Ident {
@@ -588,11 +631,15 @@ pub fn proj_param(i: usize) -> Ident {
 }
 
 pub fn trait_bound(trait_path: &Path) -> Ident {
-    Arc::new(format!("{}{}", PREFIX_TRAIT_BOUND, path_to_string(trait_path)))
+    Arc::new(format!(
+        "{}{}",
+        PREFIX_TRAIT_BOUND,
+        sanitize_to_air_ident(&path_to_string(trait_path))
+    ))
 }
 
 pub fn to_dyn(trait_path: &Path) -> Ident {
-    Arc::new(format!("{}{}", PREFIX_TO_DYN, path_to_string(trait_path)))
+    Arc::new(format!("{}{}", PREFIX_TO_DYN, sanitize_to_air_ident(&path_to_string(trait_path))))
 }
 
 pub fn sized_bound() -> Ident {
@@ -604,11 +651,11 @@ pub fn prefix_type_id_fun(i: usize) -> Ident {
 }
 
 pub fn prefix_box(ident: &Path) -> Ident {
-    Arc::new(PREFIX_BOX.to_string() + &path_to_string(ident))
+    Arc::new(PREFIX_BOX.to_string() + &sanitize_to_air_ident(&path_to_string(ident)))
 }
 
 pub fn prefix_unbox(ident: &Path) -> Ident {
-    Arc::new(PREFIX_UNBOX.to_string() + &path_to_string(ident))
+    Arc::new(PREFIX_UNBOX.to_string() + &sanitize_to_air_ident(&path_to_string(ident)))
 }
 
 pub fn prefix_fuel_id(ident: &Ident) -> Ident {
@@ -686,7 +733,12 @@ pub fn encode_dt_as_path(dt: &Dt) -> Path {
 
 pub fn variant_ident(dt: &Dt, variant: &str) -> Ident {
     let path = encode_dt_as_path(dt);
-    Arc::new(format!("{}{}{}", path_to_string(&path), VARIANT_SEPARATOR, variant))
+    Arc::new(format!(
+        "{}{}{}",
+        sanitize_to_air_ident(&path_to_string(&path)),
+        VARIANT_SEPARATOR,
+        sanitize_to_air_ident(variant)
+    ))
 }
 
 pub fn is_variant_ident(datatype: &Dt, variant: &str) -> Ident {
@@ -701,11 +753,11 @@ pub fn variant_field_ident_internal(
 ) -> Ident {
     Arc::new(format!(
         "{}{}{}{}{}",
-        path_to_string(path),
+        sanitize_to_air_ident(&path_to_string(path)),
         VARIANT_SEPARATOR,
-        variant.as_str(),
+        sanitize_to_air_ident(variant.as_str()),
         if internal { VARIANT_FIELD_INTERNAL_SEPARATOR } else { VARIANT_FIELD_SEPARATOR },
-        field.as_str()
+        sanitize_to_air_ident(field.as_str())
     ))
 }
 
@@ -786,6 +838,7 @@ pub fn new_user_qid_name(fun_name: &str, q_count: u64) -> String {
     // In SMTLIB, unquoted attribute values cannot contain colons,
     // and sise cannot handle quoting with vertical bars
     let fun_name = str::replace(&fun_name, ":", "_");
+    let fun_name = sanitize_to_air_ident(&fun_name);
     let qid = format!("{}{}_{}", air::profiler::USER_QUANT_PREFIX, fun_name, q_count);
     qid
 }
@@ -796,6 +849,7 @@ pub fn new_internal_qid(ctx: &crate::context::Ctx, name: String) -> Option<Ident
     // and sise cannot handle quoting with vertical bars
     let name = str::replace(&name, ":", "_");
     let name = str::replace(&name, "%", "__");
+    let name = sanitize_to_air_ident(&name);
     let qid = format!("{}{}_definition", air::profiler::INTERNAL_QUANT_PREFIX, name);
 
     if let Some(fun) = ctx.fun.as_ref() {
@@ -1082,7 +1136,7 @@ pub fn unique_var_name(
     uniq_id: crate::ast::VarIdentDisambiguate,
 ) -> String {
     use {crate::ast::VarIdentDisambiguate, std::fmt::Write};
-    let mut out = user_given_name;
+    let mut out = sanitize_to_air_ident(&user_given_name);
     match uniq_id {
         VarIdentDisambiguate::AirLocal => {}
         VarIdentDisambiguate::NoBodyParam => {
@@ -1174,7 +1228,7 @@ pub fn nonstatic_call_path(vstd_crate_name: &Option<Ident>, is_proof: bool) -> P
 }
 
 pub fn static_name(fun: &Fun) -> Ident {
-    Arc::new(PREFIX_STATIC.to_string() + &fun_to_string(fun))
+    Arc::new(PREFIX_STATIC.to_string() + &sanitize_to_air_ident(&fun_to_string(fun)))
 }
 
 pub fn break_label(i: u64) -> Ident {

source/vir/src/sst_to_air.rs

@@ -18,8 +18,9 @@ use crate::def::{
     SpanKind, Spanned, U_HI, encode_dt_as_path, fun_to_string, is_variant_ident, new_internal_qid,
     new_user_qid_name, path_to_string, prefix_box, prefix_ensures, prefix_fuel_id,
     prefix_no_unwind_when, prefix_open_inv, prefix_pre_var, prefix_requires, prefix_spec_fn_type,
-    prefix_unbox, snapshot_ident, static_name, suffix_global_id, suffix_local_unique_id,
-    suffix_typ_param_ids, variant_field_ident, variant_field_ident_internal, variant_ident,
+    prefix_unbox, sanitize_to_air_ident, snapshot_ident, static_name, suffix_global_id,
+    suffix_local_unique_id, suffix_typ_param_ids, variant_field_ident,
+    variant_field_ident_internal, variant_ident,
 };
 use crate::messages::{Span, error, error_with_label};
 use crate::poly::{MonoTyp, MonoTypX, MonoTyps, typ_as_mono, typ_is_poly};
@@ -61,12 +62,12 @@ pub struct PostConditionInfo {
 
 #[inline(always)]
 pub(crate) fn fun_to_air_ident(fun: &Fun) -> Ident {
-    Arc::new(fun_to_string(fun))
+    Arc::new(sanitize_to_air_ident(&fun_to_string(fun)))
 }
 
 #[inline(always)]
 pub(crate) fn path_to_air_ident(path: &Path) -> Ident {
-    Arc::new(path_to_string(path))
+    Arc::new(sanitize_to_air_ident(&path_to_string(path)))
 }
 
 #[inline(always)]