immunant / c2rust

Migrate C code to Rust
https://c2rust.com/
Other
3.79k stars 219 forks source link

analyze: emit inline annotations for debugging #1071

Closed spernsteiner closed 2 months ago

spernsteiner commented 3 months ago

This branch adds a new annotate module that allows providing annotations to be attached to specific lines during rewriting, and uses it to show pointer permissions/flags inline in the rewritten code. For example:

#[no_mangle]
pub unsafe extern "C" fn insertion_sort<'h0>(n: libc::c_int, p: &'h0 mut [(libc::c_int)]) {
// 10: p: typeof(_2) = *mut {g0} i32
// 10: p:   g0 = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
    let mut i: libc::c_int = 1 as libc::c_int;
    while i < n {
        let tmp: libc::c_int = *&(&(&*(p))[((i as isize) as usize) ..])[0];
        // 15: p.offset(i as isize): typeof(_9) = *mut {l9} i32
        // 15: p.offset(i as isize):   l9 = READ | UNIQUE, (empty)
        // 15: p: typeof(_10) = *mut {l11} i32
        // 15: p:   l11 = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
        let mut j: libc::c_int = i;
        while j > 0 as libc::c_int && *&(&(&*(p))[(((j - 1 as libc::c_int) as isize) as usize) ..])[0] > tmp {
        // 19: p.offset((j - 1 ... size): typeof(_21) = *mut {l23} i32
        // 19: p.offset((j - 1 ... size):   l23 = READ | UNIQUE, (empty)
        // 19: p: typeof(_22) = *mut {l25} i32
        // 19: p:   l25 = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
            *&mut (&mut (p)[((j as isize) as usize) ..])[0] = *&(&(&*(p))[(((j - 1 as libc::c_int) as isize) as usize) ..])[0];
            // 24: p.offset((j - 1 ... size): typeof(_30) = *mut {l34} i32
            // 24: p.offset((j - 1 ... size):   l34 = READ | UNIQUE, (empty)
            // 24: p: typeof(_31) = *mut {l36} i32
            // 24: p:   l36 = READ | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
            // 24: p.offset(j as isize): typeof(_37) = *mut {l43} i32
            // 24: p.offset(j as isize):   l43 = READ | WRITE | UNIQUE, (empty)
            // 24: p: typeof(_38) = *mut {l45} i32
            // 24: p:   l45 = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
            j -= 1
        }
        *&mut (&mut (p)[((j as isize) as usize) ..])[0] = tmp;
        // 29: p.offset(j as isize): typeof(_46) = *mut {l54} i32
        // 29: p.offset(j as isize):   l54 = READ | WRITE | UNIQUE, (empty)
        // 29: p: typeof(_47) = *mut {l56} i32
        // 29: p:   l56 = READ | WRITE | UNIQUE | OFFSET_ADD | OFFSET_SUB, (empty)
        i += 1
    }
}

This is helpful for debugging, since it means we no longer need to cross-reference line numbers in the debug output with the source code. It's also easy to add more annotations in the future if it would be useful.