array.rs

// 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;
    for i in 0..arr.len() {
        acc += arr[i as usize] as u16;
    }
    acc
}

#[no_mangle]
fn main() {
    let mut arr = [0u8; 8];
    klee_make_symbolic!(&mut arr, "arr");
    let mut i: usize = 0;
    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?)
//
// [your answer here]
/*
In debug mode, we get 10 test cases.
9 tests for different indecies, 0-8.
And one for which the index overflows, this is marked with a name of type [test-name-here].abort.err

In release, we only get 2 test cases.
One containing the testvalue zero.
And another containing a testcase for 9.

Why?
Well, the compiler has inserted a check for the value 9 for which it will panic without doing anything else.
Running the test case in gdb will show yhou this in the asm code (shown code is for test index == 0):
│B+ 0x555555555121 <array::main+1>  movq   $0x0,(%rsp)              <-- index = 0
│   0x555555555129 <array::main+9>  lea    0xed4(%rip),%rdx        # 0x555555556004                                                                                                                                                  │
│   0x555555555130 <array::main+16> mov    %rsp,%rdi                                                                                                                                                                                 │
│   0x555555555133 <array::main+19> mov    $0x8,%esi                                                                                                                                                                                 │
│   0x555555555138 <array::main+24> call   *0x2e8a(%rip)        # 0x555555557fc8                                                                                                                                                     │
│  >0x55555555513e <array::main+30> cmpq   $0x9,(%rsp)   <------ The comparison                                                                                                                            │
│   0x555555555143 <array::main+35> jae    0x555555555147 <array::main+39>   <-- Jumps to the panick code if index==9                                                                                                                                                        │
│   0x555555555145 <array::main+37> pop    %rax                                                                                                                                                                                      │
│   0x555555555146 <array::main+38> ret                                                                                                                                                                                              │
│   0x555555555147 <array::main+39> call   0x555555555150 <_ZN4core9panicking18panic_bounds_check17he935ba9af86f066bE>

As to why llvm didn't optimize out the variable and its corresponding function call completely I can only guess.
But a good one might be that due to the fact that llvm otimizes on a basis that the a code section is "inconsequential code" we can defere that the code has meaning, 
atleast to llvm, and that optimzing it out would change the functionalty of the program (and also what it effects).

One guess on what that effect might be is that llvm has picked up on that our code can generate an overflow error, which in-turn generates a interrupt in the cpu.
Getting rid of this would change what the program actually does and is there not allowed to be removed.