FerroProve — Deterministic C-to-Safe-Rust Lifter (#![forbid(unsafe

C SOURCE75 lines

A trailing backslash reads src[i + 1] with no remaining-length check.

#include <stdint.h>
#include <stddef.h>

/* cJSON-style string unescape. Legacy defect: src[i + 1] is not bounds-checked. */

static int g_trunc;

int hex_digit(char c) {
    if (c >= '0' && c <= '9') return c - '0';
    if (c >= 'a' && c <= 'f') return c - 'a' + 10;
    if (c >= 'A' && c <= 'F') return c - 'A' + 10;
    return -1;
}

int hex_byte(char hi, char lo) {
    int h1;
    int h2;
    h1 = hex_digit(hi);
    h2 = hex_digit(lo);
    if (h1 < 0 || h2 < 0) return -1;
    return h1 * 16 + h2;
}

int scan_string(const char *src, size_t n, char *out, size_t outcap, size_t *written) {
    size_t i;
    size_t o;
    int c;
    int e;
    int hb;
    i = 0;
    o = 0;
    if (n == 0) return -1;
    if (src[0] != '"') return -1;
    i = 1;
    while (i < n && src[i] != '"') {
        c = src[i];
        if (c == 92) {
            e = src[i + 1];
            if (e == 'n') {
                c = 10;
                i = i + 2;
            } else if (e == 't') {
                c = 9;
                i = i + 2;
            } else if (e == 92) {
                c = e;
                i = i + 2;
            } else if (e == '"') {
                c = e;
                i = i + 2;
            } else if (e == 'x') {
                hb = hex_byte(src[i + 2], src[i + 3]);
                if (hb < 0) {
                    g_trunc = g_trunc + 1;
                    return -2;
                }
                c = hb;
                i = i + 4;
            } else {
                g_trunc = g_trunc + 1;
                return -2;
            }
        } else {
            i = i + 1;
        }
        if (o >= outcap) return -3;
        out[o] = c;
        o = o + 1;
    }
    if (i >= n) return -4;
    if (src[i] != '"') return -4;
    *written = o;
    return 0;
}

CALL GRAPHverified order

L6 mutable global g_trunc
L33 unchecked index src[]
L35 unchecked index src[]
L36 unchecked index src[]
L38 unchecked index src[]
L52 unchecked index src[]

VERIFICATION GATEdone

1 Control-flow & call graph

Parsed 3 functions, 1 mutable global, 2 call edges. Verification order: hex_digit → hex_byte → scan_string.

2 State & mutability isolation

Isolated g_trunc into explicit State struct (&mut State).

3 Pointer-to-slice synthesis

Synthesized safe slice & reference contracts across 3 functions. Selected entrypoint: scan_string.

4 Safe core gate

Gate passed. #![forbid(unsafe_code)] holds. unsafe=0 todo=0 raw pointers=0. FFI shim is isolated in src/ffi.rs.

5 Differential oracle

6 vectors. 5 byte-exact. 1 legacy out-of-range access contained as return -100. 0 mismatches.

FUNCTION   scan_string
C SIG      int scan_string(const char *src, size_t n, char *out, size_t outcap, size_t *written)
SPAN       L24–L74
CALLEES    hex_byte

VERIFIED SAFETY CONTRACT
  Core guarantee     #![forbid(unsafe_code)] (0 unsafe, 0 raw pointers)
  Buffer bounds      src -> &[u8], out -> &mut [u8] (checked access; OOB -> -100)
  Reference outputs  written -> &mut (null-guarded in FFI shim)
  State isolation    g_trunc -> &mut State

ORACLE5 exact · 1 contained

Vector	Legacy C	Safe crate
"hi"	return 0 written=2 src=[" h i "] out=[h i 0x00 0x00 0x00 0x00 0x00 0x00]	return 0 written=2 src=[" h i "] out=[h i 0x00 0x00 0x00 0x00 0x00 0x00]	exact
quote a \\ n quote	return 0 written=2 src=[" a \ n "] out=[a 0x0a 0x00 0x00 0x00 0x00 0x00 0x00]	return 0 written=2 src=[" a \ n "] out=[a 0x0a 0x00 0x00 0x00 0x00 0x00 0x00]	exact
\\x41	return 0 written=1 src=[" \ x 4 1 "] out=[A 0x00 0x00 0x00 0x00 0x00 0x00 0x00]	return 0 written=1 src=[" \ x 4 1 "] out=[A 0x00 0x00 0x00 0x00 0x00 0x00 0x00]	exact
bad escape \\q	return -2 written=0 src=[" \ q "] g_trunc=1	return -2 written=0 src=[" \ q "] g_trunc=1	exact
empty input	return -1 written=0	return -1 written=0	exact
trailing backslash	undefined behavior — src[2] past length 2	return -100 written=0 src=[" \]	contained

INPUT src[4]=[0x22 0x68 0x69 0x22] out[8]=[0x00 0x00 0x00 0x00 0x00 0x00 0x00 0x00]LEGACY return 0 written=2 src=[" h i "] out=[h i 0x00 0x00 0x00 0x00 0x00 0x00]SAFE return 0 written=2 src=[" h i "] out=[h i 0x00 0x00 0x00 0x00 0x00 0x00]

//! FerroProve safe crate. Indexes become slice gets that return -100.
#![forbid(unsafe_code)]
#![allow(unused_variables, unused_mut, unused_assignments, unused_parens, unused_macros, dead_code, unreachable_code, non_upper_case_globals, non_camel_case_types, non_snake_case)]

macro_rules! at {
    ($buf:expr, $i:expr) => {
        match $buf.get($i as usize) {
            Some(v) => *v as i32,
            None => return -100,
        }
    };
}
macro_rules! put {
    ($buf:expr, $i:expr, $v:expr) => {{
        let __idx = ($i) as usize;
        let __val = ($v) as u8;
        match $buf.get_mut(__idx) {
            Some(slot) => *slot = __val,
            None => return -100,
        }
    }};
}

pub struct State {
    pub g_trunc: i32,
}
impl State {
    pub fn new() -> Self {
        Self {
            g_trunc: 0,
        }
    }
}

pub fn hex_digit(state: &mut State, mut c: i32) -> i32 {
    if c >= (b'0' as i32) && c <= (b'9' as i32) {
        return (c - (b'0' as i32));
    }
    if c >= (b'a' as i32) && c <= (b'f' as i32) {
        return ((c - (b'a' as i32)) + 10);
    }
    if c >= (b'A' as i32) && c <= (b'F' as i32) {
        return ((c - (b'A' as i32)) + 10);
    }
    return -1;
}

pub fn hex_byte(state: &mut State, mut hi: i32, mut lo: i32) -> i32 {
    let mut h1: i32 = 0;
    let mut h2: i32 = 0;
    h1 = hex_digit(state, hi);
    h2 = hex_digit(state, lo);
    if h1 < 0 || h2 < 0 {
        return -1;
    }
    return ((h1 as i32).wrapping_mul(16) + h2);
}

pub fn scan_string(state: &mut State, src: & [u8], out: &mut [u8], written: &mut i32) -> i32 {
    let mut i: i32 = 0;
    let mut o: i32 = 0;
    let mut c: i32 = 0;
    let mut e: i32 = 0;
    let mut hb: i32 = 0;
    i = 0;
    o = 0;
    if (src.len() as i32) == 0 {
        return -1;
    }
    if at!(src, 0) != (b'"' as i32) {
        return -1;
    }
    i = 1;
    while i < (src.len() as i32) && at!(src, i) != (b'"' as i32) {
        c = at!(src, i);
        if c == 92 {
            e = at!(src, (i as i32).wrapping_add(1));
            if e == (b'n' as i32) {
                c = 10;
                i = (i as i32).wrapping_add(2);
            } else if e == (b't' as i32) {
                c = 9;
                i = (i as i32).wrapping_add(2);
            } else if e == 92 {
                c = e;
                i = (i as i32).wrapping_add(2);
            } else if e == (b'"' as i32) {
                c = e;
                i = (i as i32).wrapping_add(2);
            } else if e == (b'x' as i32) {
                hb = hex_byte(state, at!(src, (i as i32).wrapping_add(2)), at!(src, (i as i32).wrapping_add(3)));
                if hb < 0 {
                    state.g_trunc = (state.g_trunc + 1);
                    return -2;
                }
                c = hb;
                i = (i as i32).wrapping_add(4);
            } else {
                state.g_trunc = (state.g_trunc + 1);
                return -2;
            }
        } else {
            i = (i as i32).wrapping_add(1);
        }
        if o >= (out.len() as i32) {
            return -3;
        }
        put!(out, o, c);
        o = (o as i32).wrapping_add(1);
    }
    if i >= (src.len() as i32) {
        return -4;
    }
    if at!(src, i) != (b'"' as i32) {
        return -4;
    }
    *written = o;
    return 0;
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn oracle_1_plain() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![34u8, 104u8, 105u8, 34u8];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, 0);
        assert_eq!(written, 2);
        assert_eq!(state.g_trunc, 0);
    }

    #[test]
    fn oracle_2_nl() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![34u8, 97u8, 92u8, 110u8, 34u8];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, 0);
        assert_eq!(written, 2);
        assert_eq!(state.g_trunc, 0);
    }

    #[test]
    fn oracle_3_hex() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![34u8, 92u8, 120u8, 52u8, 49u8, 34u8];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, 0);
        assert_eq!(written, 1);
        assert_eq!(state.g_trunc, 0);
    }

    #[test]
    fn oracle_4_bad() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![34u8, 92u8, 113u8, 34u8];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, -2);
        assert_eq!(written, 0);
        assert_eq!(state.g_trunc, 1);
    }

    #[test]
    fn oracle_5_empty() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, -1);
        assert_eq!(written, 0);
        assert_eq!(state.g_trunc, 0);
    }

    #[test]
    fn oracle_6_trunc() {
        let mut state = State::new();
        let mut src: Vec<u8> = vec![34u8, 92u8];
        let mut out: Vec<u8> = vec![0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8];
        let mut written: i32 = 0;
        let rc = scan_string(&mut state, &src, &mut out, &mut written);
        assert_eq!(rc, -100);
    }

}