-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
12 changed files
with
152 additions
and
107 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,19 +1,22 @@ | ||
## translation validator | ||
|
||
### overview | ||
this tool compares the source function in cpp with the target function in rust, and verifies whether the rust function is a correct translation/semantic equivalent of the cpp function using alive2 in llvm ir level. | ||
|
||
**ps**. you could find all source files to be verified in the `examples/source` directory. | ||
|
||
### prerequisites | ||
- follow the instructions in [alive2](https://github.com/AliveToolkit/alive2) to build and configure alive2, also the specific llvm with RTTI and exceptions turned on. | ||
- I basically build the llvm from source (i.e., the latest main branch) and build the alive2 upon it. | ||
- follow the instructions in [alive2](https://github.com/AliveToolkit/alive2) to build and configure alive2, and also the specific llvm version. | ||
- you should build the llvm from source (i.e., the latest main branch), with RTTI and exceptions turned on. | ||
|
||
- based on the provided `CMakeLists_Template`, create your own `CMakeLists.txt` by replacing the placeholder for the paths. | ||
- based on the provided `CMakeLists_Template`, create your own `CMakeLists.txt` by replacing the placeholder for the paths, you may need to change the `.dylib` to `.so` or `.a` depending on your OS. | ||
|
||
### build | ||
```bash | ||
bash scripts/build.sh | ||
``` | ||
### build and run | ||
through `make build`, `make run`, or `make build_and_run`. | ||
|
||
note: a `compile_commands.json` will be automatically generated in the build directory and moved to the root directory, this is generally used by clangd for code navigation, you may need to reload the window to make it work. | ||
|
||
### run | ||
```bash | ||
bash scripts/run.sh | ||
``` | ||
### generate the ir files | ||
either through `make generate_ir` or `make clean_and_generate_ir`. | ||
|
||
**note**: the source file, e.g., `examples/source/add.rs`, will be converted to `add_rs.ll` and put in the `examples/ir/add/add_rs.ll` path, check the `scripts/src2ir.py` for more details. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,9 +1,5 @@ | ||
pub fn access_array(index: i32) -> i32 { | ||
pub fn access_array(index: u32) -> i32 { | ||
let arr = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]; | ||
|
||
if index < 0 || index >= 10 { | ||
return -1; | ||
} | ||
|
||
arr[index as usize] | ||
arr[10 + index as usize] | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,5 @@ | ||
short div(short a, short b) { | ||
return a / b; | ||
/// ub will be detected by alive2, this is also considered semantically | ||
/// different from the rust version. | ||
int div_by_zero(int a, int b) { | ||
return a / (b - b); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,5 @@ | ||
pub fn div(a: i16, b: i16) -> i16 { | ||
a / b | ||
/// the source cpp module is ub, and the function attrs are different | ||
/// so the verifier fails to compare the two even after switching the order. | ||
pub fn div_by_zero(a: i32, b: i32) -> i32 { | ||
a / (b - b) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,4 @@ | ||
/// ub, order will be switched during verification. | ||
int use_uninit() { | ||
int arr[2]; | ||
arr[1] = 1030; | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,17 +1,15 @@ | ||
#!/bin/bash | ||
|
||
# Enable stricter error handling | ||
# enable stricter error handling | ||
set -euo pipefail | ||
|
||
# Define the path to your executable | ||
# Replace 'your_executable' with the actual name of your program | ||
EXECUTABLE="./build/translation_validator" | ||
|
||
# Check if the executable exists | ||
# check if the executable exists | ||
if [ ! -f "$EXECUTABLE" ]; then | ||
echo "Error: Executable not found. Did you build the project?" | ||
echo "error: executable not found, did you build the project?" | ||
exit 1 | ||
fi | ||
|
||
# Run the executable | ||
# run the executable | ||
"$EXECUTABLE" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.