add factorial & update examples/source, finalize translation validator

examples/source/add/add.cpp

@@ -1,3 +1,9 @@
+/// according to the cpp language specification, overflow of the addition
+/// operation of two signed integers is considered undefined behavior (UB).
+/// that's why `clang++` will add the `noundef` attribute to the return value
+/// and use `add nsw` instead of normal `add` instruction - in a purely syntactic
+/// way that strictly follows the cpp language specification.
+/// see `examples/ir_fixed/add/` for more details.
 int add(int a, int b) {
     return a + b;
 }

examples/source/add/add.rs

@@ -1,3 +1,7 @@
+/// though rust panics when overflow happens, Alive2 assumes the **scope**
+/// of input parameters will not result in such overflow according to the
+/// cpp language specification.
+/// see `examples/source/add/add.cpp` for more details.
 pub fn add(a: i32, b: i32) -> i32 {
     a + b
 }

examples/source/add_u32/add_u32.rs

@@ -1,3 +1,6 @@
+/// for the addition of two unsigned integers, Alive2 correctly identifies
+/// the different behaviors between source C++ (implicitly wrapping) and
+/// target Rust (panics when overflow happens).
 pub fn add(a: u32, b: u32) -> u32 {
     a + b
 }

examples/source/atomic/atomic.cpp

@@ -1,3 +1,6 @@
+//! unfortunately, Alive2 does NOT support atomic operations and
+//! the corresponding LLVM IR instructions.
+
 #include <atomic>
 
 // int fetch_add(std::atomic<int>& counter, int value) {

examples/source/different_ret/different_ret.cpp

@@ -1,4 +1,5 @@
-/// incorrect translation
+/// a trivial example where the return values from the
+/// source C++ and target Rust are different.
 int ret() {
     return 20170618;
 }

examples/source/different_ret/different_ret.rs

@@ -1,4 +1,3 @@
-/// incorrect translation
 pub fn ret() -> i32 {
     20021030
 }

examples/source/factorial/factorial.cpp

@@ -0,0 +1,3 @@
+int factorial(int n) {
+    return n <= 1 ? 1 : n * factorial(n - 1);
+}

examples/source/factorial/factorial.rs

@@ -0,0 +1,6 @@
+/// nested function call is not supported by alive2,
+/// so that the recursive call to `factorial` will be trivially
+/// marked as undefined behavior (UB) and rejected by alive2.
+pub fn factorial(n: i32) -> i32 {
+    if n <= 1 { 1 } else { n.wrapping_mul(factorial(n - 1)) }
+}

examples/source/nested_switch/nested_switch.rs

@@ -1,5 +1,6 @@
 /// the extern "C" and `i8` are the same as in `switch_case.rs`.
-/// note that 
+/// note that we need to use `wrapping_mul` and `wrapping_add`
+/// to make alive2 happy.
 #[inline(never)]
 pub extern "C" fn process_tokens(type_: i8, value: i32) -> i32 {
     match type_ as u8 as char {

examples/source/null_deref/null_deref.cpp

@@ -1,3 +1,4 @@
+/// the source C++ will always trigger undefined behavior (UB)
 int null_deref() {
     const int *ptr = nullptr;
     return *ptr;

examples/source/simple_enum/simple_enum.rs

@@ -1,15 +1,12 @@
-//! generated by claude-3.5-sonnet at Nov 20, 2024
-//! validation result: a seemingly correct translation of `simple_enum.cpp`
-
-#[repr(i32)]  // Use same representation as C++ enum
-#[derive(Clone, Copy)]  // Make it work like C++ value type
+#[repr(i32)]            // use same representation as C++ enum
+#[derive(Clone, Copy)]  // make it work like C++ value type
 pub enum Color {
     Red = 0,
     Green = 1,
     Blue = 2,
 }
 
 pub fn create_color(x: i32) -> Color {
-    // Directly transmute the integer to enum, matching C++'s behavior
+    // directly transmute the integer to enum, matching C++'s behavior
     unsafe { std::mem::transmute(x) }
 }

examples/source/simple_generic/simple_generic.rs

@@ -1,5 +1,3 @@
-//! translated by claude-3.5-sonnet at Nov 21, 2024
-
 use std::ops::Add;
 
 // generic add function

examples/source/simple_ret/simple_ret.cpp

@@ -1,4 +1,5 @@
-/// correct translation
+/// a trivial example where the return value of the source C++
+/// and target Rust are the same.
 int ret() {
     return 20021030;
 }

examples/source/simple_ret/simple_ret.rs

@@ -1,4 +1,3 @@
-/// correct translation
 pub fn ret() -> i32 {
     20021030
 }

examples/source/simple_struct/simple_struct.rs

@@ -1,4 +1,3 @@
-//! generated by claude-3.5-sonnet at Nov 20, 2024
 //! validation result: the two programs do not type check when evaluated by alive2 at llvm ir level,
 //! but are they semantically equivalent at the function level?