// get_sign.rs
// Showcase how we automatically can interface Rust to KLEE
//

#![no_std]
#![no_main]

use klee_sys::klee_make_symbolic;
use panic_klee as _;

fn sum_first_elements(arr: &[u8], index: usize) -> u16 {
    let mut acc: u16 = 0;
    let index = core::cmp::min(arr.len(), index);
    for i in 0..index {
        acc += arr[i as usize] as u16;
    }
    acc
}

#[no_mangle]
fn main() {
    let mut arr = [0u8; 8];
    let mut i: usize = 0;
    klee_make_symbolic!(&mut arr, "arr");
    klee_make_symbolic!(&mut i, "i");
    let b = sum_first_elements(&arr, i);
}

// A) Array indexing is tricky to analyse at compile time.
// Thus Rust (rustc) will inject code for run-time verification
// `panic`ing on index out of range.
//
// (Compare to C/C++, where a "buffer overflow" might pass unnoticed
// causing all sorts of problems.)
//
// Compare the test generated in release `--release` (optimized) to
// test generated in debug/dev mode (un-optimized).
//
// Try to explain in your own words the difference and why?
// (Hint, even if we don't use the result `b`, Rust do not optimize out the call, why?)
//
// [There are 10 path with debug/dev mode and 2 path on release mode.
// In the debug mode/dev 8 of the paths is 8 for each loop, 1 path is for panic when index is out of range.
// The release mode is optimizing out all the loops, which means there are only two paths; one inside the loop
// and one outside. The b is not optimized out because the calculation of b can have side effects and
// code with side effects are not optimized out.]
//
// B) Fix the code so that you don't get an error.
// (It should still compute the sum of the n first elements
// and return the sum of the whole array if index larger than size/length).
// The fix should be in the function (not on the caller side).
//
// [Git commit "B"]
//
// C) In the example, the array is holding only zeroes.
// Figure out a way to make the content symbolic.
// (Hint, declare as mutable, iterate and set each element symbolic.)
// (Hint2, it seems that you can set the whole array symbolic directly
// without messing with an iterator, super!!!.)
//
// [Git commit "C"]
//
// D) Analyze the example using KLEE. Now a new (maybe unexpected) error should occur!
// Notice, the error occurs only in `debug/dev` builds.
//
// Explain what caused the error.
//
// [It seems to be a overflow problem in the varaible acc.]
//
// E) Make a sensible fix to the code.
// Motivate your choice.
//
// [I changed the acc variable to a u16. It will allow bigger values without overflowing.]
//
// [Git commit "D"]
//
// F) Learning outcome.
// 70% of Microsoft security updates over the last decade is directly related to
// memory safety.
//
// Explain in your own words what Microsoft would gain by using Rust.
//
// [your answer here]
//
// Explain in your own words what Microsoft would gain by using `cargo klee`
// on their Rust code.
//
// And YES, Microsoft is rewriting core system functionality in Rust as we speak!