A little function with plenty of slice bound tests

[leonardo]

This little coding problem asks to rotate a square matrix by 90 degrees clockwise:

LeetCode - Rotate Image

A simple Rust port of that C++ solution could be:

pub unsafe fn rotate1(m: &mut [&mut [u32]]) {
    let s = m.len();
    for i in 0 .. s / 2 {
        for j in i .. s - 1 - i {
            assume(i < m.len());
            assume(j < m[i].len());
            let tmp = m[i][j];
            assume(s - 1 - j < m.len());
            assume(i < m[s - 1 - j].len());
            m[i][j] = m[s - 1 - j][i];
            assume(s - 1 - j < m[s - 1 - i].len());
            m[s - 1 - j][i] = m[s - 1 - i][s - 1 - j];
            assume(j < m.len());
            assume(s - 1 - i < m[j].len());
            m[s - 1 - i][s - 1 - j] = m[j][s - 1 - i];
            m[j][s - 1 - i] = tmp;
        }
    }
}

If you remove those assume() you get many slice bound tests.

A const generics version needs none of those assume(), surprisingly in this function the back-end is able to remove all slice bound tests regardless the value of S:

pub fn rotate2<const S: usize>(m: &mut [&mut [u32; S]; S]) {
    for i in 0 .. S / 2 {
        for j in i .. S - 1 - i {
            let tmp = m[i][j];
            m[i][j] = m[S - 1 - j][i];
            m[S - 1 - j][i] = m[S - 1 - i][S - 1 - j];
            m[S - 1 - i][S - 1 - j] = m[j][S - 1 - i];
            m[j][S - 1 - i] = tmp;
        }
    }
}

[mbartlett]

This is because the nested arrays are not forced to be the same length as the outer one and could be smaller, thus causing memory unsafety

[leonardo]

Yes, I should add a pre-condition to assert that all the rows have the same length:

#![feature(core_intrinsics)]
use std::intrinsics::assume;

pub unsafe fn rotate3(m: &mut [&mut [u32]]) {
    let s = m.len();
    assert!(m.iter().all(|r| r.len() == s));

    for i in 0 .. s / 2 {
        for j in i .. s - 1 - i {
            assume(i < m.len());
            assume(j < m[i].len());
            let tmp = m[i][j];
            assume(i < m.len());
            assume(j < m[i].len());
            assume(s - 1 - j < m.len());
            assume(i < m[s - 1 - j].len());
            m[i][j] = m[s - 1 - j][i];
            assume(s - 1 - i < m.len());
            assume(s - 1 - j < m[s - 1 - i].len());
            assume(s - 1 - j < m.len());
            assume(i < m[s - 1 - j].len());
            m[s - 1 - j][i] = m[s - 1 - i][s - 1 - j];
            assume(j < m.len());
            assume(s - 1 - i < m[j].len());
            assume(s - 1 - i < m.len());
            assume(s - 1 - j < m[s - 1 - i].len());
            m[s - 1 - i][s - 1 - j] = m[j][s - 1 - i];
            assume(j < m.len());
            assume(s - 1 - i < m[j].len());
            m[j][s - 1 - i] = tmp;
        }
    }
}

The C# language has built-in tensors, that are guaranteed to have same length rows, etc (CSharp/C# Tutorial - C# Multidimensional Arrays ). This should help the back-end infer some of those assume().