initial rmc commit

Author: danielsn

CODE_OF_CONDUCT.md

@@ -0,0 +1,4 @@
+## Code of Conduct
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
+[email protected] with any additional questions or comments.

CONTRIBUTING.md

@@ -0,0 +1,59 @@
+# Contributing Guidelines
+
+Thank you for your interest in contributing to our project. Whether it's a bug report, new feature, correction, or additional
+documentation, we greatly value feedback and contributions from our community.
+
+Please read through this document before submitting any issues or pull requests to ensure we have all the necessary
+information to effectively respond to your bug report or contribution.
+
+
+## Reporting Bugs/Feature Requests
+
+We welcome you to use the GitHub issue tracker to report bugs or suggest features.
+
+When filing an issue, please check existing open, or recently closed, issues to make sure somebody else hasn't already
+reported the issue. Please try to include as much information as you can. Details like these are incredibly useful:
+
+* A reproducible test case or series of steps
+* The version of our code being used
+* Any modifications you've made relevant to the bug
+* Anything unusual about your environment or deployment
+
+
+## Contributing via Pull Requests
+Contributions via pull requests are much appreciated. Before sending us a pull request, please ensure that:
+
+1. You are working against the latest source on the *main* branch.
+2. You check existing open, and recently merged, pull requests to make sure someone else hasn't addressed the problem already.
+3. You open an issue to discuss any significant work - we would hate for your time to be wasted.
+
+To send us a pull request, please:
+
+1. Fork the repository.
+2. Modify the source; please focus on the specific change you are contributing. If you also reformat all the code, it will be hard for us to focus on your change.
+3. Ensure local tests pass.
+4. Commit to your fork using clear commit messages.
+5. Send us a pull request, answering any default questions in the pull request interface.
+6. Pay attention to any automated CI failures reported in the pull request, and stay involved in the conversation.
+
+GitHub provides additional document on [forking a repository](https://help.github.com/articles/fork-a-repo/) and
+[creating a pull request](https://help.github.com/articles/creating-a-pull-request/).
+
+
+## Finding contributions to work on
+Looking at the existing issues is a great way to find something to contribute on. As our projects, by default, use the default GitHub issue labels (enhancement/bug/duplicate/help wanted/invalid/question/wontfix), looking at any 'help wanted' issues is a great place to start.
+
+
+## Code of Conduct
+This project has adopted the [Amazon Open Source Code of Conduct](https://aws.github.io/code-of-conduct).
+For more information see the [Code of Conduct FAQ](https://aws.github.io/code-of-conduct-faq) or contact
+[email protected] with any additional questions or comments.
+
+
+## Security issue notifications
+If you discover a potential security issue in this project we ask that you notify AWS/Amazon Security via our [vulnerability reporting page](http://aws.amazon.com/security/vulnerability-reporting/). Please do **not** create a public github issue.
+
+
+## Licensing
+
+See the [LICENSE](LICENSE) file for our project's licensing. We will ask you to confirm the licensing of your contribution.

README.md

@@ -0,0 +1,91 @@
+# Rust Model Checker (RMC)
+The Rust Model Checker (RMC) aims to be a bit-precise model-checker for Rust.
+
+## Disclaimer
+RMC is currently in the initial development phase.
+It **does not support all rust language features**.
+Some unsupported (or partially supported) features will cause panics when RMC runs.
+In other cases, RMC will "successfully" compile the rust code under test, but may inaccuratly give either false positives or false negatives.
+If you encounter either false positives, or false negatives, please report them as an issue on this repository.
+
+
+## Security
+See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
+
+## Architecture
+TODO
+
+## Developer guide
+TODO
+
+## License
+### Rust compiler
+RMC is a fork of the rust compiler, which is primarily primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
+
+See [LICENSE-APACHE](LICENSE-APACHE), [LICENSE-MIT](LICENSE-MIT), and
+[UPSTREAM-COPYRIGHT](UPSTREAM-COPYRIGHT) for details.
+
+### RMC additions
+RMC is Rdistributed under the terms of both the MIT license and the Apache License (Version 2.0).
+
+See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT)for details.
+
+## Quickstart
+
+The following will build and test `rmc`:
+
+```
+./scripts/rmc-regression.sh
+```
+
+## Build frontend
+
+```
+cd RustToCBMC
+cp config.toml.example config.toml
+sed -i "" \
+     -e "s/^#debug = .*/debug = true/" \
+     -e "s/^#debug-assertions-std = .*/debug-assertions-std = false/" \
+     -e "s/^#incremental = .*/incremental = true/" \
+     -e "s/^#deny-warnings = .*/deny-warnings = false/" \
+     config.toml
+./x.py build -i --stage 1 library/std
+export RMC_RUSTC=`find \`pwd\`/build -name "rustc" -print | grep stage1`
+export PATH=`pwd`/scripts:$PATH
+```
+
+Note: You almost certainly want to use the local llvm installation instead
+of building llvm from scratch. You do this by setting llvm-config to the
+path of the local llvm-config tool in the target section of config.toml
+for the target you are building. For example, on MacOS,
+```
+brew install llvm
+echo '' >> config.toml
+echo '[target.x86_64-apple-darwin]' >> config.toml
+echo 'llvm-config = "/usr/local/opt/llvm/bin/llvm-config"' >> config.toml
+```
+
+Note: You almost certainly want full debug information for debugging
+under gdb or lldb.  You do this by setting debuginfo-level-rustc to 2.
+```
+sed -i "" \
+     -e "s/^#debuginfo-level-rustc = .*/debuginfo-level-rustc = 2/" \
+     config.toml
+```
+
+## Install CBMC
+
+CBMC has prebuilt releases [available for major platforms](https://github.com/diffblue/cbmc/releases).
+RMC currently works with CBMC versions 5.26 or greater.
+
+### Building CBMC from source
+
+If you want to build CBMC from source, however, do
+```
+git clone https://github.com/diffblue/cbmc.git
+cd cbmc
+cmake -S. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF
+cd build
+make -j
+export PATH=$(pwd)/bin:$PATH
+```

cargo-rmc-tests/.gitignore

@@ -0,0 +1,7 @@
+empty-main/Cargo.lock
+empty-main/out.main
+empty-main/target/
+simple-lib/Cargo.lock
+simple-lib/out.test_one_plus_two
+simple-lib/out.test_sum
+simple-lib/target/

cargo-rmc-tests/empty-main/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "empty-main"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]

cargo-rmc-tests/empty-main/expected.main

@@ -0,0 +1 @@
+VERIFICATION SUCCESSFUL

cargo-rmc-tests/empty-main/src/main.rs

@@ -0,0 +1,3 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+fn main() {}

cargo-rmc-tests/run.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+"""
+Test runner for cargo-rmc-test directories
+
+Given a cargo directory we look for expected.<func> files in the top-level. We
+run cargo-rmc with <func> as the entry point and make sure that every line in
+expected.<func> appears in the actual output.
+"""
+
+
+import argparse
+import glob
+import os
+import sys
+import subprocess
+
+
+def compare_output(expected, actual):
+    """Check that every line in expected appears in actual"""
+    with open(expected) as f, open(actual) as g:
+        expected = f.read().splitlines()
+        actual = g.read().splitlines()
+        def appears_in_actual(line):
+            return line in actual
+        not_found = [ line for line in expected if not appears_in_actual(line) ]
+        for line in not_found:
+            print(f"ERROR expected line missing: {line}", file=sys.stderr)
+        return not_found == []
+
+
+def main():
+    """Check a cargo directory with cargo-rmc against expected outputs"""
+    parser = argparse.ArgumentParser(description="Drive a cargo-rmc test")
+    parser.add_argument("cargo_dir", help="cargo directory to verify")
+    args = parser.parse_args()
+    os.chdir(args.cargo_dir)
+    exit_code = 0
+    for expected_result in glob.glob("expected.*"):
+        func = expected_result.split(".")[1]
+        cmd = ["cargo", "rmc", ".", "--function", func]
+        output = f"out.{func}"
+        print(f"Verifying {args.cargo_dir}{func}".ljust(64+10), end="")
+        with open(output, "w") as f:
+            subprocess.run(cmd, stdout=f, check=True)
+        if compare_output(expected_result, output):
+            print("PASS")
+        else:
+            print("FAIL")
+            exit_code = 1
+    return exit_code
+
+
+if __name__ == "__main__":
+    sys.exit(main())

cargo-rmc-tests/simple-lib/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "simple-lib"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]

cargo-rmc-tests/simple-lib/expected.test_one_plus_two

@@ -0,0 +1 @@
+[test_one_plus_two.assertion.1] line 30 assertion failed: p.sum() == 3: SUCCESS

cargo-rmc-tests/simple-lib/expected.test_sum

@@ -0,0 +1 @@
+[test_sum.assertion.1] line 26 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS

cargo-rmc-tests/simple-lib/src/lib.rs

@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub mod pair;
+pub use pair::Pair;
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn it_works() {
+        assert_eq!(2 + 2, 4);
+    }
+}
+
+#[cfg(rmc)]
+mod rmc_tests {
+    use super::*;
+
+    fn __nondet<T>() -> T {
+        unimplemented!()
+    }
+    #[allow(dead_code)]
+    #[no_mangle]
+    fn test_sum() {
+        let a: u64 = __nondet();
+        let b: u64 = __nondet();
+        let p = Pair::new(a, b);
+        assert!(p.sum() == a.wrapping_add(b));
+    }
+}

cargo-rmc-tests/simple-lib/src/pair.rs

@@ -0,0 +1,33 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub struct Pair(pub u64, pub u64);
+
+impl Pair {
+    pub fn new(a: u64, b: u64) -> Self {
+        Pair(a, b)
+    }
+    pub fn sum(&self) -> u64 {
+        self.0.wrapping_add(self.1)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    #[test]
+    fn one_plus_two() {
+        let p = Pair::new(1, 2);
+        assert_eq!(p.sum(), 3);
+    }
+}
+
+#[cfg(rmc)]
+mod rmc_tests {
+    use super::*;
+    #[allow(dead_code)]
+    #[no_mangle]
+    fn test_one_plus_two() {
+        let p = Pair::new(1, 2);
+        assert!(p.sum() == 3);
+    }
+}