From 44c53787ebe07a94e8ff5199692bf98af61cd238 Mon Sep 17 00:00:00 2001 From: Zihao Xu Date: Wed, 11 Dec 2024 00:34:22 -0500 Subject: [PATCH] add factorial & update examples/source, finalize translation validator --- examples/source/add/add.cpp | 6 ++++++ examples/source/add/add.rs | 4 ++++ examples/source/add_u32/add_u32.rs | 3 +++ examples/source/atomic/atomic.cpp | 3 +++ examples/source/different_ret/different_ret.cpp | 3 ++- examples/source/different_ret/different_ret.rs | 1 - examples/source/factorial/factorial.cpp | 3 +++ examples/source/factorial/factorial.rs | 6 ++++++ examples/source/nested_switch/nested_switch.rs | 3 ++- examples/source/null_deref/null_deref.cpp | 1 + examples/source/simple_enum/simple_enum.rs | 9 +++------ examples/source/simple_generic/simple_generic.rs | 2 -- examples/source/simple_ret/simple_ret.cpp | 3 ++- examples/source/simple_ret/simple_ret.rs | 1 - examples/source/simple_struct/simple_struct.rs | 1 - 15 files changed, 35 insertions(+), 14 deletions(-) create mode 100644 examples/source/factorial/factorial.cpp create mode 100644 examples/source/factorial/factorial.rs diff --git a/examples/source/add/add.cpp b/examples/source/add/add.cpp index 59aab49..17cb3a3 100644 --- a/examples/source/add/add.cpp +++ b/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; } diff --git a/examples/source/add/add.rs b/examples/source/add/add.rs index b4a2a9e..8ba81bf 100644 --- a/examples/source/add/add.rs +++ 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 } diff --git a/examples/source/add_u32/add_u32.rs b/examples/source/add_u32/add_u32.rs index 6eec06a..b6af024 100644 --- a/examples/source/add_u32/add_u32.rs +++ 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 } diff --git a/examples/source/atomic/atomic.cpp b/examples/source/atomic/atomic.cpp index 6396f4f..af356a0 100644 --- a/examples/source/atomic/atomic.cpp +++ b/examples/source/atomic/atomic.cpp @@ -1,3 +1,6 @@ +//! unfortunately, Alive2 does NOT support atomic operations and +//! the corresponding LLVM IR instructions. + #include // int fetch_add(std::atomic& counter, int value) { diff --git a/examples/source/different_ret/different_ret.cpp b/examples/source/different_ret/different_ret.cpp index e82f35c..a14ee83 100644 --- a/examples/source/different_ret/different_ret.cpp +++ b/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; } diff --git a/examples/source/different_ret/different_ret.rs b/examples/source/different_ret/different_ret.rs index 318e44e..d75871f 100644 --- a/examples/source/different_ret/different_ret.rs +++ b/examples/source/different_ret/different_ret.rs @@ -1,4 +1,3 @@ -/// incorrect translation pub fn ret() -> i32 { 20021030 } diff --git a/examples/source/factorial/factorial.cpp b/examples/source/factorial/factorial.cpp new file mode 100644 index 0000000..0b62e58 --- /dev/null +++ b/examples/source/factorial/factorial.cpp @@ -0,0 +1,3 @@ +int factorial(int n) { + return n <= 1 ? 1 : n * factorial(n - 1); +} diff --git a/examples/source/factorial/factorial.rs b/examples/source/factorial/factorial.rs new file mode 100644 index 0000000..39dde13 --- /dev/null +++ b/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)) } +} diff --git a/examples/source/nested_switch/nested_switch.rs b/examples/source/nested_switch/nested_switch.rs index 902ce40..2945de0 100644 --- a/examples/source/nested_switch/nested_switch.rs +++ b/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 { diff --git a/examples/source/null_deref/null_deref.cpp b/examples/source/null_deref/null_deref.cpp index 0c0c6ac..1001d85 100644 --- a/examples/source/null_deref/null_deref.cpp +++ b/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; diff --git a/examples/source/simple_enum/simple_enum.rs b/examples/source/simple_enum/simple_enum.rs index 30cb03b..693d267 100644 --- a/examples/source/simple_enum/simple_enum.rs +++ b/examples/source/simple_enum/simple_enum.rs @@ -1,8 +1,5 @@ -//! 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, @@ -10,6 +7,6 @@ pub enum Color { } 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) } } diff --git a/examples/source/simple_generic/simple_generic.rs b/examples/source/simple_generic/simple_generic.rs index 4b2c3a5..0a3819e 100644 --- a/examples/source/simple_generic/simple_generic.rs +++ b/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 diff --git a/examples/source/simple_ret/simple_ret.cpp b/examples/source/simple_ret/simple_ret.cpp index 4a027d6..5907dcc 100644 --- a/examples/source/simple_ret/simple_ret.cpp +++ b/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; } diff --git a/examples/source/simple_ret/simple_ret.rs b/examples/source/simple_ret/simple_ret.rs index 0238783..d75871f 100644 --- a/examples/source/simple_ret/simple_ret.rs +++ b/examples/source/simple_ret/simple_ret.rs @@ -1,4 +1,3 @@ -/// correct translation pub fn ret() -> i32 { 20021030 } diff --git a/examples/source/simple_struct/simple_struct.rs b/examples/source/simple_struct/simple_struct.rs index fd81a94..58c3038 100644 --- a/examples/source/simple_struct/simple_struct.rs +++ b/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?