diff --git a/cargo_klee_examples/examples/cyccnt.rs b/cargo_klee_examples/examples/cyccnt.rs index bfb8f4063190ef5d0b4b349d7303110dcffce382..c565c2dd283cdf8220cbcb94468da00de6940234 100644 --- a/cargo_klee_examples/examples/cyccnt.rs +++ b/cargo_klee_examples/examples/cyccnt.rs @@ -19,7 +19,7 @@ fn main() { let end = core.DWT.cyccnt.read(); - let _time = end - start; + let _time = end.wrapping_sub(start); } // A) Running KLEE on embedded code: @@ -167,6 +167,9 @@ fn main() { // What do you get, and why? // // [your answer here] +// start/end = <optimized out> +// start and end are only used once and that is when calculating _time, _time is never used. Thus +// the compiler probably removed start, end and _time because they are never really used. // // As you should have seen, this was not particularly informative, right? // @@ -198,14 +201,23 @@ fn main() { // Value of `start`. // // [your answer here] +// (gdb) print start +// $7 = 512 +// // // Value of `end` // // [your answer here] +// (gdb) print end +// $8 = 0 +// // // Why does these values cause an error debug/dev build but not in a release build? // // [your answer here] +// The result of 0 - 512 = -512 which a u32 can't represent because it is unsigned. Thus the +// compiler panics because the value of _time is wrong. The release build removes this calculation +// because _time is never used, thus it never runs into this problem. // // C) Fix the problem! // @@ -218,6 +230,9 @@ fn main() { // Argue for your solution in your own words. // // [your answer here] +// I switch the subtraction to a wrapping one this will remove the error. I choose this solution +// because it is short and easy to implement. It also calculates the correct diff value as long as +// end has not wrapped around more then once. // // D) Learning outcomes and major takeaways. // @@ -237,6 +252,17 @@ fn main() { // How long time would lines 16/17 take to run to trigger the error? // // [your answer here] +// * I think that these kind of errors are hard to find because I often think of the counter as a number +// when I program and mathematically there is no problem. But variable needs to have a fixed size +// and thus the programmer has to remember to think of the number as having a fixed size. +// +// * The condition that triggers this error is that start > end because cyccnt has wrapped around. +// +// * Cyccnt is a 32 bit registry and counts for ever. When the value becomes more then the 32 bit +// registry can hold it starts over again(wraps around). +// +// * 2^32 / 8MHz = 2^32 / (8*10^6) = 536.870912 seconds (~537 sec) +// // // Of course this is a contrived example, and may not occur in practice. // But, it represents a class of problems/errors/bugs that is