fn convert_z3escapes()

in amzn-smt-string-fct-updater/src/transpiler.rs [50:144]


fn convert_z3escapes(s: &str) -> String {
    // small state machine to process the bytes of s
    enum State {
        Base,         // default state
        Esc,          // after '\'
        EscX,         // after '\x'
        EscHex(char), // EscHex(h) = state after '\xh (if h is an hexa digit)
    }

    let mut new_string = String::with_capacity(s.len());
    let mut state = State::Base;

    for c in s.chars() {
        match state {
            State::Base => {
                new_string.push(c);
                if c == '\\' {
                    state = State::Esc;
                }
            }

            State::Esc => match c {
                'x' => state = State::EscX,
                'a' => {
                    new_string.push_str("u{07}");
                    state = State::Base;
                }
                'b' => {
                    new_string.push_str("u{08}");
                    state = State::Base;
                }
                'f' => {
                    new_string.push_str("u{0C}");
                    state = State::Base;
                }
                'n' => {
                    new_string.push_str("u{0A}");
                    state = State::Base;
                }
                'r' => {
                    new_string.push_str("u{0D}");
                    state = State::Base;
                }
                't' => {
                    new_string.push_str("u{09}");
                    state = State::Base;
                }
                'v' => {
                    new_string.push_str("u{0B}");
                    state = State::Base;
                }
                _ => {
                    new_string.push(c);
                    state = State::Base;
                }
            },

            State::EscX => {
                if c.is_ascii_hexdigit() {
                    state = State::EscHex(c);
                } else {
                    new_string.push('x');
                    new_string.push(c);
                    state = State::Base;
                }
            }

            State::EscHex(x) => {
                if c.is_ascii_hexdigit() {
                    new_string.push_str("u{");
                    new_string.push(x);
                    new_string.push(c);
                    new_string.push('}');
                } else {
                    new_string.push('x');
                    new_string.push(x);
                    new_string.push(c);
                };
                state = State::Base;
            }
        }
    }

    // handle any unfinished escape sequence (keep it unchanged)
    match state {
        State::EscX => new_string.push('x'),
        State::EscHex(x) => {
            new_string.push('x');
            new_string.push(x);
        }
        _ => {}
    }

    new_string
}