From 142b1f2db3658f4c91cc4cb187212a6e9da7c928 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 29 Oct 2021 13:28:51 -0700 Subject: [PATCH] Create an RMC crate and load it as part of rmc-rustc (#597) * Adding support to new rmc prelude definitions - Create an rmc crate (#231). - Used rust compliant names for the functions (#589). - Changed rmc-rustc to inject the rmc prelude as part of the compilation as well as other rmc configuration flags. - Added options to rmc-rustc to print binary path and flags so it can be used in other scripts. * Add a script to build rmc library * Update tests to use new injected prelude. --- .github/workflows/rmc.yml | 4 +- Cargo.lock | 4 ++ Cargo.toml | 5 +- .../rustc_codegen_rmc/src/overrides/hooks.rs | 54 +++++++++------- .../rustc_codegen_rmc/src/overrides/mod.rs | 2 +- library/rmc/Cargo.toml | 10 +++ library/rmc/src/lib.rs | 53 ++++++++++++++++ scripts/codegen-firecracker.sh | 6 +- scripts/rmc-rustc | 61 ++++++++++++++++--- scripts/rmc.py | 13 ++-- scripts/setup/build_rmc_lib.sh | 14 +++++ scripts/std-lib-regression.sh | 11 ++-- src/test/benchmarks/Vector/append.rs | 4 +- src/test/benchmarks/Vector/insert.rs | 6 +- src/test/benchmarks/Vector/push.rs | 2 +- src/test/benchmarks/Vector/push_and_pop.rs | 4 +- src/test/benchmarks/Vector/remove.rs | 4 +- .../benchmarks/Vector/shrink_and_clear.rs | 12 ++-- src/test/benchmarks/benchmark-prelude.rs | 2 - .../cargo-rmc/simple-config-toml/src/lib.rs | 7 +-- .../simple-config-toml/test_sum.expected | 2 +- src/test/cargo-rmc/simple-extern/src/lib.rs | 5 +- src/test/cargo-rmc/simple-lib/src/lib.rs | 7 +-- .../cargo-rmc/simple-lib/test_sum.expected | 2 +- src/test/expected/closure/expected | 12 ++-- src/test/expected/closure/main.rs | 4 +- src/test/expected/closure3/expected | 6 +- src/test/expected/closure3/main.rs | 4 +- src/test/expected/comp/main.rs | 6 +- src/test/expected/dry-run/expected | 2 +- src/test/expected/dynamic-error-trait/main.rs | 4 +- src/test/expected/nondet/expected | 10 +-- src/test/expected/nondet/main.rs | 4 +- src/test/expected/replace-hashmap/expected | 12 ++-- src/test/expected/replace-hashmap/main.rs | 12 ++-- src/test/expected/replace-vec/expected | 16 ++--- src/test/expected/replace-vec/main.rs | 6 +- src/test/expected/unwind_tip/main.rs | 4 +- src/test/expected/vecdq/main.rs | 6 +- .../micro-http-parsed-request/ignore-main.rs | 10 ++- .../virtio-balloon-compact/ignore-main.rs | 6 +- .../firecracker/virtio-block-parse/main.rs | 16 +++-- src/test/prusti/Binary_search.rs | 4 +- src/test/rmc-prelude.rs | 47 -------------- src/test/rmc/ArithEqualOperators/main.rs | 6 +- src/test/rmc/ArithOperators/main.rs | 4 +- src/test/rmc/Assume/main.rs | 6 +- src/test/rmc/Assume/main_fail.rs | 8 +-- src/test/rmc/BinOp_Offset/main_fail.rs | 6 +- src/test/rmc/BitwiseArithOperators/bool.rs | 6 +- src/test/rmc/BitwiseArithOperators/main.rs | 6 +- src/test/rmc/BitwiseEqualOperators/main.rs | 6 +- src/test/rmc/Bool-BoolOperators/main.rs | 4 +- src/test/rmc/Cast/from_be_bytes.rs | 17 +++--- src/test/rmc/DynTrait/any_cast_int_fail.rs | 4 +- src/test/rmc/DynTrait/boxed_closure_fail.rs | 4 +- src/test/rmc/DynTrait/drop_boxed_dyn.rs | 4 +- .../DynTrait/drop_nested_boxed_dyn_fail.rs | 4 +- src/test/rmc/DynTrait/dyn_fn_mut_fail.rs | 4 +- src/test/rmc/DynTrait/dyn_fn_once_fail.rs | 4 +- .../dyn_fn_param_closure_capture_fail.rs | 6 +- .../rmc/DynTrait/dyn_fn_param_closure_fail.rs | 6 +- src/test/rmc/DynTrait/dyn_fn_param_fail.rs | 6 +- .../DynTrait/generic_duplicate_names_fail.rs | 4 +- .../generic_duplicate_names_impl_fail.rs | 6 +- src/test/rmc/DynTrait/main.rs | 4 +- src/test/rmc/DynTrait/main_fail.rs | 8 +-- src/test/rmc/DynTrait/nested_closures_fail.rs | 17 +++--- .../rmc/DynTrait/vtable_size_align_drop.rs | 2 - .../DynTrait/vtable_size_align_drop_fail.rs | 18 +++--- src/test/rmc/EQ-NE/main.rs | 4 +- src/test/rmc/Enum/result3.rs | 6 +- src/test/rmc/FloatingPoint/main.rs | 4 +- src/test/rmc/FunctionCall_Ret-NoParam/main.rs | 12 ++-- src/test/rmc/FunctionCall_Ret-Param/main.rs | 4 +- .../rmc/IfElseifElse_NonReturning/main.rs | 4 +- src/test/rmc/IfElseifElse_Returning/main.rs | 6 +- src/test/rmc/LT-GT-LE-GE/main.rs | 4 +- src/test/rmc/LoopLoop_NonReturning/main.rs | 4 +- .../main_no_unwind_asserts.rs | 4 +- src/test/rmc/LoopWhile_NonReturning/main.rs | 4 +- .../main_no_unwind_asserts.rs | 4 +- src/test/rmc/NondetVectors/bytes.rs | 20 +++--- src/test/rmc/NondetVectors/fixme_main.rs | 8 +-- src/test/rmc/Pointers_OtherTypes/main.rs | 4 +- .../rmc/SaturatingIntrinsics/fixme_128.rs | 6 +- src/test/rmc/SaturatingIntrinsics/main.rs | 6 +- src/test/rmc/Scopes_NonReturning/main.rs | 4 +- src/test/rmc/Scopes_Returning/main.rs | 6 +- src/test/rmc/Slice/slice_from_raw.rs | 2 - src/test/rmc/i32-Unary-/main.rs | 4 +- src/test/serial/serial.rs | 14 ++--- src/test/serial/serial2.rs | 8 +-- src/test/serial/serial_spec.rs | 8 +-- src/test/smack/basic/arith_assume.rs | 6 +- src/test/smack/basic/arith_assume2.rs | 6 +- src/test/smack/basic/arith_assume3.rs | 6 +- src/test/smack/functions/closure.rs | 4 +- src/test/smack/functions/closure_fail.rs | 4 +- src/test/smack/functions/double.rs | 4 +- src/test/smack/functions/double_fail.rs | 4 +- src/test/smack/generics/generic_function.rs | 12 ++-- src/test/smack/generics/generic_function1.rs | 12 ++-- src/test/smack/generics/generic_function2.rs | 12 ++-- src/test/smack/generics/generic_function3.rs | 12 ++-- src/test/smack/generics/generic_function4.rs | 12 ++-- src/test/smack/generics/generic_function5.rs | 12 ++-- src/test/smack/loops/gauss_sum_nondet.rs | 4 +- src/test/smack/loops/gauss_sum_nondet_fail.rs | 4 +- src/test/smack/loops/iterator.rs | 4 +- src/test/smack/loops/iterator_fail.rs | 4 +- src/test/smack/structures/option.rs | 6 +- src/test/smack/structures/option_fail.rs | 6 +- src/test/smack/structures/point.rs | 10 ++- src/test/smack/structures/point_fail.rs | 10 ++- src/test/stub-tests/HashSet/concrete.rs | 14 ++--- src/test/stub-tests/HashSet/ignore-nondet.rs | 14 ++--- src/test/stub-tests/Vec/append.rs | 2 - src/test/stub-tests/Vec/as_mut_ptr.rs | 2 - src/test/stub-tests/Vec/as_mut_slice.rs | 2 - src/test/stub-tests/Vec/as_ptr.rs | 2 - src/test/stub-tests/Vec/as_slice.rs | 2 - src/test/stub-tests/Vec/capacity.rs | 2 - src/test/stub-tests/Vec/clear.rs | 2 - src/test/stub-tests/Vec/clone.rs | 2 - src/test/stub-tests/Vec/drop.rs | 2 - src/test/stub-tests/Vec/extend.rs | 2 - src/test/stub-tests/Vec/extend_from_slice.rs | 2 - src/test/stub-tests/Vec/from_raw_parts.rs | 2 - src/test/stub-tests/Vec/from_slice.rs | 2 - src/test/stub-tests/Vec/from_str.rs | 2 - src/test/stub-tests/Vec/insert.rs | 2 - src/test/stub-tests/Vec/into_iter.rs | 2 - src/test/stub-tests/Vec/is_empty.rs | 2 - src/test/stub-tests/Vec/len.rs | 2 - src/test/stub-tests/Vec/new.rs | 2 - src/test/stub-tests/Vec/pop.rs | 2 - src/test/stub-tests/Vec/push.rs | 2 - src/test/stub-tests/Vec/remove.rs | 2 - src/test/stub-tests/Vec/reserve.rs | 2 - src/test/stub-tests/Vec/reserve_exact.rs | 2 - src/test/stub-tests/Vec/resize.rs | 2 - src/test/stub-tests/Vec/resize_with.rs | 2 - src/test/stub-tests/Vec/shrink_to.rs | 4 +- src/test/stub-tests/Vec/shrink_to_fit.rs | 2 - src/test/stub-tests/Vec/simple.rs | 2 - src/test/stub-tests/Vec/split_off.rs | 2 - src/test/stub-tests/Vec/swap_remove.rs | 2 - src/test/stub-tests/Vec/truncate.rs | 2 - src/test/stub-tests/Vec/truncate_drop.rs | 2 - src/test/stub-tests/Vec/truncate_reduce.rs | 2 - src/test/stub-tests/Vec/truncate_zero.rs | 2 - src/tools/compiletest/src/runtest.rs | 12 +--- src/tools/dashboard/src/util.rs | 16 +---- 154 files changed, 455 insertions(+), 632 deletions(-) create mode 100644 library/rmc/Cargo.toml create mode 100644 library/rmc/src/lib.rs create mode 100755 scripts/setup/build_rmc_lib.sh delete mode 100644 src/test/rmc-prelude.rs diff --git a/.github/workflows/rmc.yml b/.github/workflows/rmc.yml index f074f89f7e1bb..1c2ae3ec895e9 100644 --- a/.github/workflows/rmc.yml +++ b/.github/workflows/rmc.yml @@ -51,10 +51,12 @@ jobs: export RUST_BACKTRACE=1 ./x.py build -i --stage 1 library/std + - name: Build RMC Library + run: bash -x ./scripts/setup/build_rmc_lib.sh + - name: Execute RMC regression run: ./scripts/rmc-regression.sh - - name: Install dashboard dependencies if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} run: ./scripts/setup/install_dashboard_deps.sh diff --git a/Cargo.lock b/Cargo.lock index e00e197144611..f1a439afa165d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -3310,6 +3310,10 @@ dependencies = [ "rls-span", ] +[[package]] +name = "rmc" +version = "0.1.0" + [[package]] name = "rust-demangler" version = "0.0.1" diff --git a/Cargo.toml b/Cargo.toml index 3cbc95a8ef2e6..dbc3fd6b90f1d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,6 +4,7 @@ members = [ "compiler/rustc", "library/std", "library/test", + "library/rmc", "src/rustdoc-json-types", "src/tools/cargotest", "src/tools/clippy", @@ -55,7 +56,9 @@ exclude = [ # stdarch has its own Cargo workspace "library/stdarch", # dependency tests have their own workspace - "src/test/rmc-dependency-test/dependency3" + "src/test/rmc-dependency-test/dependency3", + # cargo rmc tests should also have their own workspace + "src/test/cargo-rmc" ] [profile.release.package.compiler_builtins] diff --git a/compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 8b4f41a8f65fd..2a62c24dfe460 100644 --- a/compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/compiler/rustc_codegen_rmc/src/overrides/hooks.rs @@ -12,14 +12,13 @@ use super::stubs::{HashMapStub, VecStub}; use crate::utils::{instance_name_is, instance_name_starts_with}; use crate::GotocCtx; use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type}; -use rustc_hir::definitions::DefPathDataName; use rustc_middle::mir::{BasicBlock, Place}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt}; use rustc_span::Span; use std::rc::Rc; -use tracing::debug; +use tracing::{debug, warn}; pub trait GotocTypeHook<'tcx> { fn hook_applies(&self, tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool; @@ -66,19 +65,29 @@ fn output_of_instance_is_never<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx> } } +fn matches_function(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>, attr_name: &str) -> bool { + let attr_sym = rustc_span::symbol::Symbol::intern(attr_name); + if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { + if instance.def.def_id() == *attr_id { + debug!("matched: {:?} {:?}", attr_id, attr_sym); + return true; + } + } + false +} + struct ExpectFail; impl<'tcx> GotocHook<'tcx> for ExpectFail { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let def_path = tcx.def_path(instance.def.def_id()); - if let Some(data) = def_path.data.last() { - match data.data.name() { - DefPathDataName::Named(name) => { - return name.to_string().starts_with("__VERIFIER_expect_fail"); - } - DefPathDataName::Anon { .. } => (), - } + // Deprecate old __VERIFIER notation that doesn't respect rust naming conventions. + // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599 + if instance_name_starts_with(tcx, instance, "__VERIFIER_expect_fail") { + warn!( + "The function __VERIFIER_expect_fail is deprecated. Use rmc::expect_fail instead" + ); + return true; } - false + matches_function(tcx, instance, "RmcExpectFail") } fn handle( @@ -109,16 +118,13 @@ impl<'tcx> GotocHook<'tcx> for ExpectFail { struct Assume; impl<'tcx> GotocHook<'tcx> for Assume { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let def_path = tcx.def_path(instance.def.def_id()); - if let Some(data) = def_path.data.last() { - match data.data.name() { - DefPathDataName::Named(name) => { - return name.to_string().starts_with("__VERIFIER_assume"); - } - DefPathDataName::Anon { .. } => (), - } + // Deprecate old __VERIFIER notation that doesn't respect rust naming conventions. + // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599 + if instance_name_starts_with(tcx, instance, "__VERIFIER_assume") { + warn!("The function __VERIFIER_assume is deprecated. Use rmc::assume instead"); + return true; } - false + matches_function(tcx, instance, "RmcAssume") } fn handle( @@ -149,7 +155,13 @@ struct Nondet; impl<'tcx> GotocHook<'tcx> for Nondet { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - instance_name_starts_with(tcx, instance, "__nondet") + // Deprecate old __nondet since it doesn't match rust naming conventions. + // Complete removal is tracked here: https://github.com/model-checking/rmc/issues/599 + if instance_name_starts_with(tcx, instance, "__nondet") { + warn!("The function __nondet is deprecated. Use rmc::nondet instead"); + return true; + } + matches_function(tcx, instance, "RmcNonDet") } fn handle( diff --git a/compiler/rustc_codegen_rmc/src/overrides/mod.rs b/compiler/rustc_codegen_rmc/src/overrides/mod.rs index 05b4db8eb3c5b..9c02442a60a17 100644 --- a/compiler/rustc_codegen_rmc/src/overrides/mod.rs +++ b/compiler/rustc_codegen_rmc/src/overrides/mod.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module provides a mechanism which RMC can use to override standard codegen. -//! For example, we the RMC provides pseudo-functions, such as __VERIFIER_assume(). +//! For example, we the RMC provides pseudo-functions, such as rmc::assume(). //! These functions should not be codegenned as MIR. //! Instead, we use a "hook" to generate the correct CBMC intrinsic. diff --git a/library/rmc/Cargo.toml b/library/rmc/Cargo.toml new file mode 100644 index 0000000000000..32a76e76b3458 --- /dev/null +++ b/library/rmc/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "rmc" +version = "0.1.0" +edition = "2018" +license = "MIT OR Apache-2.0" + +[dependencies] diff --git a/library/rmc/src/lib.rs b/library/rmc/src/lib.rs new file mode 100644 index 0000000000000..631f1a3729672 --- /dev/null +++ b/library/rmc/src/lib.rs @@ -0,0 +1,53 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(rustc_attrs)] // Used for rustc_diagnostic_item. + +/// Creates an assumption that will be valid after this statement run. Note that the assumption +/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the +/// program will exit successfully. +/// +/// # Example: +/// +/// The code snippet below should never panic. +/// +/// ```rust +/// let i : i32 = rmc::nondet(); +/// rmc::assume(i > 10); +/// if i < 0 { +/// panic!("This will never panic"); +/// } +/// ``` +/// +/// The following code may panic though: +/// +/// ```rust +/// let i : i32 = rmc::nondet(); +/// assert!(i < 0, "This may panic and verification should fail."); +/// rmc::assume(i > 10); +/// ``` +#[inline(never)] +#[rustc_diagnostic_item = "RmcAssume"] +pub fn assume(_cond: bool) {} + +/// This creates an unconstrained value of type `T`. You can assign the return value of this +/// function to a variable that you want to make symbolic. +/// +/// # Example: +/// +/// In the snippet below, we are verifying the behavior of the function `fn_under_verification` +/// under all possible i32 input values. +/// +/// ```rust +/// let inputA = rmc::nondet::(); +/// fn_under_verification(inputA); +/// ``` +#[inline(never)] +#[rustc_diagnostic_item = "RmcNonDet"] +pub fn nondet() -> T { + unimplemented!("RMC nondet") +} + +/// Function used in tests for cases where the condition is not always true. +#[inline(never)] +#[rustc_diagnostic_item = "RmcExpectFail"] +pub fn expect_fail(_cond: bool, _message: &str) {} diff --git a/scripts/codegen-firecracker.sh b/scripts/codegen-firecracker.sh index 0bb538b10524e..71072e48328fd 100755 --- a/scripts/codegen-firecracker.sh +++ b/scripts/codegen-firecracker.sh @@ -24,7 +24,11 @@ echo # At the moment, we only test codegen for the virtio module cd $RMC_DIR/firecracker/src/devices/src/virtio/ # Disable warnings until https://github.com/model-checking/rmc/issues/573 is fixed -RUSTC_LOG=error RUST_BACKTRACE=1 RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" RUSTC=rmc-rustc cargo build --target x86_64-unknown-linux-gnu +export RUSTC_LOG=error +export RUST_BACKTRACE=1 +export RUSTFLAGS=$(${SCRIPT_DIR}/rmc-rustc --rmc-flags) +export RUSTC=$(${SCRIPT_DIR}/rmc-rustc --rmc-path) +cargo build --target x86_64-unknown-linux-gnu echo echo "Finished Firecracker codegen regression successfully..." diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index 96364293936aa..f7e11772b47f0 100755 --- a/scripts/rmc-rustc +++ b/scripts/rmc-rustc @@ -2,19 +2,62 @@ # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. # SPDX-License-Identifier: Apache-2.0 OR MIT +# Usage: +# rmc-rustc (--rmc-flags | --rmc-path) +# - This will print the configurations used to run rmc version of rustc. +# rmc-rustc RUSTC_OPTIONS +# - This will run RUSTC with RMC flags + the given RUSTC_OPTIONS set -eu SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" REPO_DIR="$(dirname $SCRIPT_DIR)" -shopt -s nullglob -RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc) +get_rmc_path() { + shopt -s nullglob + RMC_CANDIDATES=("$REPO_DIR"/build/*/stage1/bin/rustc) -if [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]; then - echo "ERROR: Could not find RMC binary." - echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc" - echo "Was RMC successfully built first?" - exit 1 -fi + if [[ ${#RMC_CANDIDATES[@]} -ne 1 ]]; then + echo "ERROR: Could not find RMC binary." + echo "Looked for: $REPO_DIR/build/*/stage1/bin/rustc" + echo "Was RMC successfully built first?" + exit 1 + fi + echo ${RMC_CANDIDATES[0]} +} + +get_rmc_lib_path() { + if [ -z "${RMC_LIB_PATH:-""}" ] + then + RMC_LIB_CANDIDATES=("$REPO_DIR"/target/*/librmc.rlib) + if [[ ${#RMC_LIB_CANDIDATES[@]} -ne 1 ]]; then + echo "ERROR: Could not find RMC library." + echo "Looked for: \"$REPO_DIR/target/*/librmc.rlib\"" + echo "Was RMC library successfully built first?" + exit 1 + fi + echo $(dirname ${RMC_LIB_CANDIDATES[0]}) + else + echo ${RMC_LIB_PATH} + fi +} + +RMC_PATH=$(get_rmc_path) -"${RMC_CANDIDATES[0]}" "$@" +RMC_FLAGS="--crate-type=lib \ + -Z codegen-backend=gotoc \ + -Z trim-diagnostic-paths=no \ + -Z human_readable_cgu_names \ + --cfg=rmc \ + -L $(get_rmc_lib_path) \ + --extern rmc" + +if [ "${1:-''}" == "--rmc-flags" ] +then + echo ${RMC_FLAGS} +elif [ "${1:-''}" == "--rmc-path" ] +then + echo ${RMC_PATH} +else + # Execute rmc + "${RMC_PATH}" ${RMC_FLAGS} "$@" +fi diff --git a/scripts/rmc.py b/scripts/rmc.py index 1f3a2175aa8e1..53f40fe149847 100644 --- a/scripts/rmc.py +++ b/scripts/rmc.py @@ -149,12 +149,9 @@ def run_cmd( def rustc_flags(mangler, symbol_table_passes): flags = [ - "-Z", "codegen-backend=gotoc", - "-Z", "trim-diagnostic-paths=no", "-Z", f"symbol-mangling-version={mangler}", "-Z", f"symbol_table_passes={' '.join(symbol_table_passes)}", - "-Z", "human_readable_cgu_names", - f"--cfg={RMC_CFG}"] + ] if "RUSTFLAGS" in os.environ: flags += os.environ["RUSTFLAGS"].split(" ") return flags @@ -176,7 +173,7 @@ def compile_single_rust_file( atexit.register(delete_file, output_filename) atexit.register(delete_file, base + ".type_map.json") - build_cmd = [RMC_RUSTC_EXE, "--crate-type=lib"] + rustc_flags(mangler, symbol_table_passes) + build_cmd = [RMC_RUSTC_EXE] + rustc_flags(mangler, symbol_table_passes) if use_abs: build_cmd += ["-Z", "force-unstable-if-unmarked=yes", @@ -199,10 +196,14 @@ def cargo_build(crate, target_dir, verbose=False, debug=False, mangler="v0", dry build_cmd = ["cargo", "build", "--lib", "--target-dir", str(target_dir)] build_env = {"RUSTFLAGS": " ".join(rustflags), "RUSTC": RMC_RUSTC_EXE, - "PATH": os.environ["PATH"], + "PATH": os.environ["PATH"] } if debug: add_rmc_rustc_debug_to_env(build_env) + if verbose: + build_cmd.append("-v") + if dry_run: + print("{}".format(build_env)) return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run) # Adds information about unwinding to the RMC output diff --git a/scripts/setup/build_rmc_lib.sh b/scripts/setup/build_rmc_lib.sh new file mode 100755 index 0000000000000..ccecfab7ecc88 --- /dev/null +++ b/scripts/setup/build_rmc_lib.sh @@ -0,0 +1,14 @@ +#!/bin/bash +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -o errexit +set -o nounset + +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" +SCRIPTS_DIR="$(dirname $SCRIPT_DIR)" +REPO_DIR="$(dirname $SCRIPTS_DIR)" + +export RUSTC=$(${SCRIPTS_DIR}/rmc-rustc --rmc-path) +cargo build --manifest-path "${REPO_DIR}/library/rmc/Cargo.toml" $@ + diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index 553c352c0100d..8b0653aafe3a5 100755 --- a/scripts/std-lib-regression.sh +++ b/scripts/std-lib-regression.sh @@ -40,16 +40,17 @@ fi STD_LIB_LOG="/tmp/StdLibTest/log.txt" echo "Starting cargo build with RMC" -RUSTC_LOG=error \ - RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" \ - RUSTC=rmc-rustc cargo +nightly build -Z build-std --target $TARGET 2>&1 \ +export RUSTC_LOG=error +export RUSTFLAGS=$(${SCRIPT_DIR}/rmc-rustc --rmc-flags) +export RUSTC=$(${SCRIPT_DIR}/rmc-rustc --rmc-path) +cargo +nightly build -Z build-std --target $TARGET 2>&1 \ | tee $STD_LIB_LOG # For now, we expect a linker error, but no modules should fail with a compiler -# panic. +# panic. # # With https://github.com/model-checking/rmc/issues/109, this check can be -# removed to just allow the success of the previous line to determine the +# removed to just allow the success of the previous line to determine the # success of this script (with no $STD_LIB_LOG needed) # TODO: this check is insufficient if the failure is before codegen diff --git a/src/test/benchmarks/Vector/append.rs b/src/test/benchmarks/Vector/append.rs index 33efb7b914ca9..8d6b70d4c4e30 100644 --- a/src/test/benchmarks/Vector/append.rs +++ b/src/test/benchmarks/Vector/append.rs @@ -9,11 +9,11 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } let mut v2: Vec = Vec::with_capacity(times); for i in 0..times { - v2.push(__nondet()); + v2.push(rmc::nondet()); } v.append(&mut v2); assert!(v.len() == times * 2); diff --git a/src/test/benchmarks/Vector/insert.rs b/src/test/benchmarks/Vector/insert.rs index dfc79705793de..f25a49a3c474d 100644 --- a/src/test/benchmarks/Vector/insert.rs +++ b/src/test/benchmarks/Vector/insert.rs @@ -9,11 +9,11 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } - let sentinel = __nondet(); + let sentinel = rmc::nondet(); v.push(sentinel); - v.insert(v.len()/2, __nondet()); + v.insert(v.len()/2, rmc::nondet()); assert!(v.pop() == Some(sentinel)); } diff --git a/src/test/benchmarks/Vector/push.rs b/src/test/benchmarks/Vector/push.rs index 5ff3c0728fc8d..880914b4b8b8b 100644 --- a/src/test/benchmarks/Vector/push.rs +++ b/src/test/benchmarks/Vector/push.rs @@ -9,7 +9,7 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } } diff --git a/src/test/benchmarks/Vector/push_and_pop.rs b/src/test/benchmarks/Vector/push_and_pop.rs index aaa9811be9d36..5a5a941facff4 100644 --- a/src/test/benchmarks/Vector/push_and_pop.rs +++ b/src/test/benchmarks/Vector/push_and_pop.rs @@ -9,7 +9,7 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::new(); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } assert!(v.len() == times); v.push(1); @@ -19,7 +19,7 @@ fn operate_on_vec(times: usize) { fn operate_on_vec_len(times: usize) { let mut v: Vec = Vec::new(); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } assert!(v.len() == times); v.push(1); diff --git a/src/test/benchmarks/Vector/remove.rs b/src/test/benchmarks/Vector/remove.rs index 500bf55145067..0f41df3545344 100644 --- a/src/test/benchmarks/Vector/remove.rs +++ b/src/test/benchmarks/Vector/remove.rs @@ -9,9 +9,9 @@ include!{"../benchmark-prelude.rs"} fn operate_on_vec(times: usize) { let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } - let sentinel = __nondet(); + let sentinel = rmc::nondet(); v.push(sentinel); // We remove elements to perform more memmoves. These are done to fill up // "holes" created due to elements removed from the middle of the Vec. diff --git a/src/test/benchmarks/Vector/shrink_and_clear.rs b/src/test/benchmarks/Vector/shrink_and_clear.rs index f4e8120860962..3a492dcea4e7c 100644 --- a/src/test/benchmarks/Vector/shrink_and_clear.rs +++ b/src/test/benchmarks/Vector/shrink_and_clear.rs @@ -9,28 +9,28 @@ fn operate_on_vec(times: usize) { // Create vector with known capacity let mut v: Vec = Vec::with_capacity(times); for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } assert!(v.len() == times); // Here, Vecs with grow() internally - let i: usize = __nondet(); - __VERIFIER_assume(i >= 0 && i < v.len()); + let i: usize = rmc::nondet(); + rmc::assume(i >= 0 && i < v.len()); let saved = v[i]; // Completely shrink the array to remove additional allocations v.shrink_to_fit(); assert!(v[i] == saved); // Push some new elements to grow() again for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } // Drop all elements in the Vec v.clear(); // Add some more new elements for i in 0..times { - v.push(__nondet()); + v.push(rmc::nondet()); } // Assert! - let sentinel = __nondet(); + let sentinel = rmc::nondet(); v.push(sentinel); assert!(v.pop() == Some(sentinel)); } diff --git a/src/test/benchmarks/benchmark-prelude.rs b/src/test/benchmarks/benchmark-prelude.rs index 03de21f7e87e4..b2b49f6a7afbd 100644 --- a/src/test/benchmarks/benchmark-prelude.rs +++ b/src/test/benchmarks/benchmark-prelude.rs @@ -1,6 +1,4 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!{"../rmc-prelude.rs"} - const TEST_SIZE: usize = 5; diff --git a/src/test/cargo-rmc/simple-config-toml/src/lib.rs b/src/test/cargo-rmc/simple-config-toml/src/lib.rs index 9fda13682d350..ace3ddcd98a5e 100644 --- a/src/test/cargo-rmc/simple-config-toml/src/lib.rs +++ b/src/test/cargo-rmc/simple-config-toml/src/lib.rs @@ -15,14 +15,11 @@ mod tests { mod rmc_tests { use super::*; - fn __nondet() -> T { - unimplemented!() - } #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u64 = __nondet(); - let b: u64 = __nondet(); + let a: u64 = rmc::nondet(); + let b: u64 = rmc::nondet(); let p = Pair::new(a, b); assert!(p.sum() == a.wrapping_add(b)); } diff --git a/src/test/cargo-rmc/simple-config-toml/test_sum.expected b/src/test/cargo-rmc/simple-config-toml/test_sum.expected index 874dde7ec1880..7a1631d92e229 100644 --- a/src/test/cargo-rmc/simple-config-toml/test_sum.expected +++ b/src/test/cargo-rmc/simple-config-toml/test_sum.expected @@ -1 +1 @@ -[rmc_tests::test_sum.assertion.1] line 27 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS +[rmc_tests::test_sum.assertion.1] line 24 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS diff --git a/src/test/cargo-rmc/simple-extern/src/lib.rs b/src/test/cargo-rmc/simple-extern/src/lib.rs index eeff449754998..5448970f70cda 100644 --- a/src/test/cargo-rmc/simple-extern/src/lib.rs +++ b/src/test/cargo-rmc/simple-extern/src/lib.rs @@ -17,13 +17,10 @@ mod tests { mod rmc_tests { use super::*; - fn __nondet() -> T { - unimplemented!() - } #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); if a < 100 { unsafe { diff --git a/src/test/cargo-rmc/simple-lib/src/lib.rs b/src/test/cargo-rmc/simple-lib/src/lib.rs index 9fda13682d350..ace3ddcd98a5e 100644 --- a/src/test/cargo-rmc/simple-lib/src/lib.rs +++ b/src/test/cargo-rmc/simple-lib/src/lib.rs @@ -15,14 +15,11 @@ mod tests { mod rmc_tests { use super::*; - fn __nondet() -> T { - unimplemented!() - } #[allow(dead_code)] #[no_mangle] fn test_sum() { - let a: u64 = __nondet(); - let b: u64 = __nondet(); + let a: u64 = rmc::nondet(); + let b: u64 = rmc::nondet(); let p = Pair::new(a, b); assert!(p.sum() == a.wrapping_add(b)); } diff --git a/src/test/cargo-rmc/simple-lib/test_sum.expected b/src/test/cargo-rmc/simple-lib/test_sum.expected index 874dde7ec1880..7a1631d92e229 100644 --- a/src/test/cargo-rmc/simple-lib/test_sum.expected +++ b/src/test/cargo-rmc/simple-lib/test_sum.expected @@ -1 +1 @@ -[rmc_tests::test_sum.assertion.1] line 27 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS +[rmc_tests::test_sum.assertion.1] line 24 assertion failed: p.sum() == a.wrapping_add(b): SUCCESS diff --git a/src/test/expected/closure/expected b/src/test/expected/closure/expected index 5a70cc7ef7692..cda57e035c3dc 100644 --- a/src/test/expected/closure/expected +++ b/src/test/expected/closure/expected @@ -1,7 +1,7 @@ resume instruction: SUCCESS -line 20 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS -line 20 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS -line 20 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS -line 25 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS -line 25 assertion failed: original_num + 12 == num: SUCCESS -line 25 arithmetic overflow on signed + in var_18 + 12: SUCCESS +line 18 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS +line 18 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS +line 18 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS +line 23 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS +line 23 assertion failed: original_num + 12 == num: SUCCESS +line 23 arithmetic overflow on signed + in var_18 + 12: SUCCESS diff --git a/src/test/expected/closure/main.rs b/src/test/expected/closure/main.rs index 23f6b64462543..df6d0fd138348 100644 --- a/src/test/expected/closure/main.rs +++ b/src/test/expected/closure/main.rs @@ -8,10 +8,8 @@ where some_closure(1, 1); } -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut num: i32 = __nondet(); + let mut num: i32 = rmc::nondet(); let y = 2; if num <= std::i32::MAX - 100 { // avoid overflow diff --git a/src/test/expected/closure3/expected b/src/test/expected/closure3/expected index ccc0abde64a1c..7b940a5705994 100644 --- a/src/test/expected/closure3/expected +++ b/src/test/expected/closure3/expected @@ -1,3 +1,3 @@ -line 16 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS -line 17 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS -line 17 assertion failed: num + 10 == y: SUCCESS +line 14 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS +line 15 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS +line 15 assertion failed: num + 10 == y: SUCCESS diff --git a/src/test/expected/closure3/main.rs b/src/test/expected/closure3/main.rs index a8de5624036d8..fe76b9e14cac0 100644 --- a/src/test/expected/closure3/main.rs +++ b/src/test/expected/closure3/main.rs @@ -7,10 +7,8 @@ where f(10) } -include!("../../rmc-prelude.rs"); - pub fn main() { - let num: i64 = __nondet(); + let num: i64 = rmc::nondet(); if num <= std::i64::MAX - 100 { // avoid overflow let y = call_with_one(|x| x + num); diff --git a/src/test/expected/comp/main.rs b/src/test/expected/comp/main.rs index 86eeb48f4decf..4f49318ba5a9b 100644 --- a/src/test/expected/comp/main.rs +++ b/src/test/expected/comp/main.rs @@ -12,11 +12,9 @@ fn eq2(a: i32, b: i32) { assert!(a - b < a); } -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); - let b = __nondet(); + let a = rmc::nondet(); + let b = rmc::nondet(); if a > -400 && a < 100 && b < 200 && b > 0 { eq1(a, b); eq2(a, b); diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected index 1c7961ad84a15..4c1f4ed8aabe2 100644 --- a/src/test/expected/dry-run/expected +++ b/src/test/expected/dry-run/expected @@ -1,4 +1,4 @@ -rmc-rustc --crate-type=lib -Z codegen-backend=gotoc -Z trim-diagnostic-paths=no -Z symbol-mangling-version=v0 -Z symbol_table_passes= -Z human_readable_cgu_names --cfg=rmc +rmc-rustc -Z symbol-mangling-version=v0 -Z symbol_table_passes= symtab2gb goto-cc --function main cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main diff --git a/src/test/expected/dynamic-error-trait/main.rs b/src/test/expected/dynamic-error-trait/main.rs index b65c54ebae9a3..f92f63601cfc9 100644 --- a/src/test/expected/dynamic-error-trait/main.rs +++ b/src/test/expected/dynamic-error-trait/main.rs @@ -5,8 +5,6 @@ use std::io::{self, Read, Write}; -include!("../../rmc-prelude.rs"); - type Result = std::result::Result; pub struct MemoryMapping { @@ -16,7 +14,7 @@ pub struct MemoryMapping { impl MemoryMapping { pub fn new(size: usize) -> Result { - if __nondet() { + if rmc::nondet() { let mm = MemoryMapping { addr: std::ptr::null_mut(), size: size }; Ok(mm) } else { diff --git a/src/test/expected/nondet/expected b/src/test/expected/nondet/expected index 1c5430c0e112b..f95ec70708bae 100644 --- a/src/test/expected/nondet/expected +++ b/src/test/expected/nondet/expected @@ -1,5 +1,5 @@ -line 9 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS -line 9 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS -line 9 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS -line 9 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS -line 9 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS +line 7 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS +line 7 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS +line 7 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS +line 7 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS +line 7 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS diff --git a/src/test/expected/nondet/main.rs b/src/test/expected/nondet/main.rs index 3646f19de8710..c715efc04ce95 100644 --- a/src/test/expected/nondet/main.rs +++ b/src/test/expected/nondet/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let x: i32 = __nondet(); + let x: i32 = rmc::nondet(); if (x > -500 && x < 500) { // x * x - 2 * x + 1 == 4 -> x == -1 || x == 3 assert!(x * x - 2 * x + 1 != 4 || (x == -1 || x == 3)); diff --git a/src/test/expected/replace-hashmap/expected b/src/test/expected/replace-hashmap/expected index 835bdfb4723a2..9bae4d317d02f 100644 --- a/src/test/expected/replace-hashmap/expected +++ b/src/test/expected/replace-hashmap/expected @@ -1,6 +1,6 @@ -line 31 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS -line 31 arithmetic overflow on unsigned + in self->len + 1: SUCCESS -line 56 assertion failed: a.is_some(): FAILURE -line 57 assertion failed: a.is_none(): FAILURE -line 59 assertion failed: b.is_some(): SUCCESS -line 60 assertion failed: b.is_none(): FAILURE +line 29 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS +line 29 arithmetic overflow on unsigned + in self->len + 1: SUCCESS +line 54 assertion failed: a.is_some(): FAILURE +line 55 assertion failed: a.is_none(): FAILURE +line 57 assertion failed: b.is_some(): SUCCESS +line 58 assertion failed: b.is_none(): FAILURE diff --git a/src/test/expected/replace-hashmap/main.rs b/src/test/expected/replace-hashmap/main.rs index f46a34248b0bd..4cf569dec34d2 100644 --- a/src/test/expected/replace-hashmap/main.rs +++ b/src/test/expected/replace-hashmap/main.rs @@ -5,8 +5,6 @@ use std::borrow::Borrow; use std::collections::hash_map::RandomState; use std::collections::HashMap; use std::hash::Hash; -include!("../../rmc-prelude.rs"); - use std::marker::PhantomData; struct CbmcHashMap { len: usize, @@ -27,24 +25,24 @@ impl CbmcHashMap { impl CbmcHashMap { pub fn insert(&mut self, k: K, v: V) -> Option { self.last = Some(v); - if __nondet() { + if rmc::nondet() { self.len += 1; } - __nondet() + rmc::nondet() } pub fn get(&self, k: &Q) -> Option<&V> where K: Borrow, { - if false { __nondet() } else { self.last.as_ref() } + if false { rmc::nondet() } else { self.last.as_ref() } } } fn make_map_visible() { let mut v: CbmcHashMap = CbmcHashMap::new(); v.len; - v.insert(__nondet(), __nondet()); - let k: K = __nondet(); + v.insert(rmc::nondet(), rmc::nondet()); + let k: K = rmc::nondet(); v.get(&k); } diff --git a/src/test/expected/replace-vec/expected b/src/test/expected/replace-vec/expected index 7a98f73b07a9d..02ab83092bb12 100644 --- a/src/test/expected/replace-vec/expected +++ b/src/test/expected/replace-vec/expected @@ -1,8 +1,8 @@ -line 25 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS -line 35 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS -line 53 assertion failed: v.len() == 1: SUCCESS -line 54 assertion failed: v.len() == 11: FAILURE -line 56 assertion failed: p != None: SUCCESS -line 57 assertion failed: p == None: FAILURE -line 58 assertion failed: p == Some(to_push): SUCCESS -line 59 assertion failed: p == Some(not_pushed): FAILURE +line 23 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS +line 33 attempt to compute `((*_1).0: usize) - const 1_usize`, which would overflow: SUCCESS +line 51 assertion failed: v.len() == 1: SUCCESS +line 52 assertion failed: v.len() == 11: FAILURE +line 54 assertion failed: p != None: SUCCESS +line 55 assertion failed: p == None: FAILURE +line 56 assertion failed: p == Some(to_push): SUCCESS +line 57 assertion failed: p == Some(not_pushed): FAILURE diff --git a/src/test/expected/replace-vec/main.rs b/src/test/expected/replace-vec/main.rs index 8cd3288e54cc1..118e25c49903d 100644 --- a/src/test/expected/replace-vec/main.rs +++ b/src/test/expected/replace-vec/main.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(allocator_api)] -include!("../../rmc-prelude.rs"); - use std::alloc::Allocator; use std::alloc::Global; use std::marker::PhantomData; @@ -34,13 +32,13 @@ impl CbmcVec { } else { self.len -= 1; self.last - //Some(__nondet()) + //Some(rmc::nondet()) } } } fn make_vec_visible() { let mut v: CbmcVec = CbmcVec::new(); - v.push(__nondet()); + v.push(rmc::nondet()); v.len(); v.pop(); } diff --git a/src/test/expected/unwind_tip/main.rs b/src/test/expected/unwind_tip/main.rs index 5647b91952a05..20d1d8094cae9 100644 --- a/src/test/expected/unwind_tip/main.rs +++ b/src/test/expected/unwind_tip/main.rs @@ -3,8 +3,6 @@ // cbmc-flags: --unwind 9 -include!("../../rmc-prelude.rs"); - // This example is a copy of the `cbmc` test in // `src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs` // @@ -13,7 +11,7 @@ include!("../../rmc-prelude.rs"); // In this test, we check that RMC warns the user about unwinding failures // and makes a recommendation to fix the issue. pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); if a < 1024 { loop { diff --git a/src/test/expected/vecdq/main.rs b/src/test/expected/vecdq/main.rs index b05a7bd826103..74df92bcebc83 100644 --- a/src/test/expected/vecdq/main.rs +++ b/src/test/expected/vecdq/main.rs @@ -2,11 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::collections::VecDeque; -include!("../../rmc-prelude.rs"); - pub fn main() { - let x = __nondet(); - let y = __nondet(); + let x = rmc::nondet(); + let y = rmc::nondet(); let mut q: VecDeque = VecDeque::new(); q.push_back(x); q.push_back(y); diff --git a/src/test/firecracker/micro-http-parsed-request/ignore-main.rs b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs index 5eab7fbf423f4..943dd4de0b6ad 100644 --- a/src/test/firecracker/micro-http-parsed-request/ignore-main.rs +++ b/src/test/firecracker/micro-http-parsed-request/ignore-main.rs @@ -3,30 +3,28 @@ // Example from Firecracker micro_http request handling // https://github.com/firecracker-microvm/firecracker/commit/22908c9fb0cd5fb20febc5d18ff1284caa5f3a53 -include!("../../rmc-prelude.rs"); - // Should return a nondet string of up to n characters // Currently RMC does not support strings -fn __nondet_string(n: u32) -> String { +fn rmc::nondet_string(n: u32) -> String { unimplemented!() } // from 4e905f741 fn bug(n: u32) { - let request_uri: String = __nondet_string(n); + let request_uri: String = rmc::nondet_string(n); let _path_tokens: Vec<&str> = request_uri[1..].split_terminator('/').collect(); // ^ slice of empty string panics } // from 22908c9fb fn fix(n: u32) { - let request_uri: String = __nondet_string(n); + let request_uri: String = rmc::nondet_string(n); let _path_tokens: Vec<&str> = request_uri.trim_start_matches('/').split_terminator('/').collect(); } fn main() { - let n: u32 = __nondet(); + let n: u32 = rmc::nondet(); bug(n); fix(n); } diff --git a/src/test/firecracker/virtio-balloon-compact/ignore-main.rs b/src/test/firecracker/virtio-balloon-compact/ignore-main.rs index 44c4d2ad846ed..b49da56798edc 100644 --- a/src/test/firecracker/virtio-balloon-compact/ignore-main.rs +++ b/src/test/firecracker/virtio-balloon-compact/ignore-main.rs @@ -53,12 +53,10 @@ fn expand(ranges: Vec<(u32, u32)>) -> Vec { return v; } -include!("../../rmc-prelude.rs"); - fn main() { let mut input = vec![0; 2]; for i in 0..input.len() { - input[i] = __nondet(); + input[i] = rmc::nondet(); if input[i] == u32::MAX { return; } @@ -69,7 +67,7 @@ fn main() { } assert!(output.len() <= input.len()); let expanded_output = expand(output); - let i: usize = __nondet(); + let i: usize = rmc::nondet(); if i < expanded_output.len() { assert!(expanded_output[i] == input[i]); } diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index aafa4ed622fb6..dc62555aa83a5 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/src/test/firecracker/virtio-block-parse/main.rs @@ -27,12 +27,10 @@ static mut TRACK_READ_OBJ: Option = None; pub struct GuestMemoryMmap {} -include!("../../rmc-prelude.rs"); - impl GuestMemoryMmap { fn checked_offset(&self, base: GuestAddress, offset: usize) -> Option { let mut retval = None; - if __nondet() { + if rmc::nondet() { if let Some(sum) = base.0.checked_add(offset as u64) { retval = Some(GuestAddress(sum)) } @@ -51,15 +49,15 @@ impl GuestMemoryMmap { if let Some(prev_addr) = TRACK_READ_OBJ { assert!(prev_addr.0 != addr.0); } - if __nondet() && TRACK_READ_OBJ.is_none() { + if rmc::nondet() && TRACK_READ_OBJ.is_none() { TRACK_READ_OBJ = Some(addr); } } - __nondet() + rmc::nondet() } fn read_obj_request_header(&self, addr: GuestAddress) -> Result { - __nondet() + rmc::nondet() } } @@ -326,12 +324,12 @@ fn is_nonzero_pow2(x: u16) -> bool { pub fn main() { let mem = GuestMemoryMmap {}; - let queue_size: u16 = __nondet(); + let queue_size: u16 = rmc::nondet(); if !is_nonzero_pow2(queue_size) { return; } - let index: u16 = __nondet(); - let desc_table = GuestAddress(__nondet::() & 0xffff_ffff_ffff_fff0); + let index: u16 = rmc::nondet(); + let desc_table = GuestAddress(rmc::nondet::() & 0xffff_ffff_ffff_fff0); let desc = DescriptorChain::checked_new(&mem, desc_table, queue_size, index); match desc { Some(x) => { diff --git a/src/test/prusti/Binary_search.rs b/src/test/prusti/Binary_search.rs index e3a79aa7dac48..054c87c3bdf94 100644 --- a/src/test/prusti/Binary_search.rs +++ b/src/test/prusti/Binary_search.rs @@ -43,15 +43,13 @@ fn binary_search(arr: &[T], elem: &T) -> Option { None } -include!("../rmc-prelude.rs"); - fn get() -> [i32; 11] { [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11] } pub fn main() { let x = get(); - let y = __nondet(); + let y = rmc::nondet(); if 1 <= y && y <= 11 { assert!(binary_search_wrong(&x, &y) == Some(y as usize - 1)); // this fails diff --git a/src/test/rmc-prelude.rs b/src/test/rmc-prelude.rs deleted file mode 100644 index 0cbec8f7cbb09..0000000000000 --- a/src/test/rmc-prelude.rs +++ /dev/null @@ -1,47 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Passing a --use-abs flag to rmc allows rmc users to replace out parts of the -// standard library with simpler, verification-friendly stubs. The prelude chooses -// a specific abstraction depending on the --abs-type flag given to rmc. -// This is currently only implemented for the Vec abstractionbut a PoC code for -// HashSet is given too. -// -// Eventually we would want to move to a more stable method of performing -// stubbing. -// Tracking issue: https://github.com/model-checking/rmc/issues/455 -// -// The default option "std" uses the standard library implementation. -// rmc uses the fine-grained, std compatible but verification-friendly implementation -// C-FFI and NoBackVec are more experimental abstractions. - -#[cfg(not(use_abs))] -use std::vec::Vec; - -#[cfg(use_abs)] -#[cfg(abs_type = "rmc")] -include! {"../../library/rmc/stubs/Rust/vec/rmc_vec.rs"} - -#[cfg(use_abs)] -#[cfg(abs_type = "no-back")] -include! {"../../library/rmc/stubs/Rust/vec/noback_vec.rs"} - -#[cfg(use_abs)] -#[cfg(abs_type = "c-ffi")] -include! {"../../library/rmc/stubs/Rust/vec/c_vec.rs"} - -#[cfg(use_abs)] -#[cfg(abs_type = "c-ffi")] -include! {"../../library/rmc/stubs/Rust/hashset/c_hashset.rs"} - -fn __VERIFIER_assume(cond: bool) { - unimplemented!() -} - -fn __VERIFIER_expect_fail(cond: bool, message: &str) { - unimplemented!() -} - -fn __nondet() -> T { - unimplemented!() -} diff --git a/src/test/rmc/ArithEqualOperators/main.rs b/src/test/rmc/ArithEqualOperators/main.rs index 6636b3f0557db..755aaf7a834cb 100644 --- a/src/test/rmc/ArithEqualOperators/main.rs +++ b/src/test/rmc/ArithEqualOperators/main.rs @@ -1,11 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); a /= 2; - let mut b: u32 = __nondet(); + let mut b: u32 = rmc::nondet(); b /= 2; let c = b; b += a; diff --git a/src/test/rmc/ArithOperators/main.rs b/src/test/rmc/ArithOperators/main.rs index ec7e23b455b72..9625cc431a177 100644 --- a/src/test/rmc/ArithOperators/main.rs +++ b/src/test/rmc/ArithOperators/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); assert!(a / 2 <= a); assert!(a / 2 * 2 >= a / 2); assert!(a / 2 + 5 + 1 > a / 2 + 5); diff --git a/src/test/rmc/Assume/main.rs b/src/test/rmc/Assume/main.rs index b9a45ba47ce42..802905d01b9eb 100644 --- a/src/test/rmc/Assume/main.rs +++ b/src/test/rmc/Assume/main.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let i: i32 = __nondet(); - __VERIFIER_assume(i < 10); + let i: i32 = rmc::nondet(); + rmc::assume(i < 10); assert!(i < 20); } diff --git a/src/test/rmc/Assume/main_fail.rs b/src/test/rmc/Assume/main_fail.rs index 3f711ddf168f3..3882f1f897b01 100644 --- a/src/test/rmc/Assume/main_fail.rs +++ b/src/test/rmc/Assume/main_fail.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let i: i32 = __nondet(); - __VERIFIER_assume(i < 10); - __VERIFIER_expect_fail(i > 20, "Blocked by assumption above."); + let i: i32 = rmc::nondet(); + rmc::assume(i < 10); + rmc::expect_fail(i > 20, "Blocked by assumption above."); } diff --git a/src/test/rmc/BinOp_Offset/main_fail.rs b/src/test/rmc/BinOp_Offset/main_fail.rs index 49d4c3ea20aaa..0319aa81c2a1d 100644 --- a/src/test/rmc/BinOp_Offset/main_fail.rs +++ b/src/test/rmc/BinOp_Offset/main_fail.rs @@ -2,12 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-verify-fail -include!("../../rmc-prelude.rs"); - pub fn test_offset_in_double_array() { //let table: Vec> = Vec::with_capacity(1); - let table: [[u64; 1]; 1] = [[__nondet::()]]; - table[0][__nondet::()]; // EXPCECTED FAIL + let table: [[u64; 1]; 1] = [[rmc::nondet::()]]; + table[0][rmc::nondet::()]; // EXPCECTED FAIL } pub fn main() { diff --git a/src/test/rmc/BitwiseArithOperators/bool.rs b/src/test/rmc/BitwiseArithOperators/bool.rs index 6c89e8fb6183e..3a9c2165f06cc 100644 --- a/src/test/rmc/BitwiseArithOperators/bool.rs +++ b/src/test/rmc/BitwiseArithOperators/bool.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: bool = __nondet(); - let b: bool = __nondet(); + let a: bool = rmc::nondet(); + let b: bool = rmc::nondet(); let c = a ^ b; assert!((a == b && !c) || (a != b && c)); } diff --git a/src/test/rmc/BitwiseArithOperators/main.rs b/src/test/rmc/BitwiseArithOperators/main.rs index e50724630dca6..13d7c34f05998 100644 --- a/src/test/rmc/BitwiseArithOperators/main.rs +++ b/src/test/rmc/BitwiseArithOperators/main.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { assert!(3 | 5 == 7); assert!(7 & 9 == 1); @@ -9,8 +7,8 @@ pub fn main() { assert!(!8 ^ !0 == 8); let x = 1; - let a: u32 = __nondet(); - let b: u32 = __nondet(); + let a: u32 = rmc::nondet(); + let b: u32 = rmc::nondet(); if a < 100000 && b < 100000 { let c = a + b; if c & x == x { diff --git a/src/test/rmc/BitwiseEqualOperators/main.rs b/src/test/rmc/BitwiseEqualOperators/main.rs index 59b4ac57f0378..728c17f8492e0 100644 --- a/src/test/rmc/BitwiseEqualOperators/main.rs +++ b/src/test/rmc/BitwiseEqualOperators/main.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { let mut x = 0; x |= 1; @@ -14,10 +12,10 @@ pub fn main() { x &= 15; assert!(x == 2); - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); a %= 8; - let mut b: u32 = __nondet(); + let mut b: u32 = rmc::nondet(); b %= 8; let mut c = a; diff --git a/src/test/rmc/Bool-BoolOperators/main.rs b/src/test/rmc/Bool-BoolOperators/main.rs index af04ec381421f..eae78f75247fb 100644 --- a/src/test/rmc/Bool-BoolOperators/main.rs +++ b/src/test/rmc/Bool-BoolOperators/main.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { assert!(true); assert!(true || false); @@ -14,6 +12,6 @@ pub fn main() { assert!(d && true); assert!(!b && d); - let e: bool = __nondet(); + let e: bool = rmc::nondet(); assert!(e || !e); } diff --git a/src/test/rmc/Cast/from_be_bytes.rs b/src/test/rmc/Cast/from_be_bytes.rs index 18459f2cf807f..80193919cd65e 100644 --- a/src/test/rmc/Cast/from_be_bytes.rs +++ b/src/test/rmc/Cast/from_be_bytes.rs @@ -1,17 +1,16 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT use std::convert::TryInto; -include!("../../rmc-prelude.rs"); pub fn main() { let input: &[u8] = &vec![ - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), ]; let buffer = input.as_ref(); let bytes: [u8; 8] = buffer.try_into().unwrap(); diff --git a/src/test/rmc/DynTrait/any_cast_int_fail.rs b/src/test/rmc/DynTrait/any_cast_int_fail.rs index aa5afef81df3c..e1852d20bc999 100644 --- a/src/test/rmc/DynTrait/any_cast_int_fail.rs +++ b/src/test/rmc/DynTrait/any_cast_int_fail.rs @@ -3,8 +3,6 @@ use std::any::Any; -include!("../../rmc-prelude.rs"); - // Cast one dynamic trait object type to another, which is legal because Send // is an auto trait with no associated function (so the underlying vtable is // the same before and after the cast). @@ -15,7 +13,7 @@ include!("../../rmc-prelude.rs"); fn downcast_to_concrete(a: &dyn Any) { match a.downcast_ref::() { Some(i) => { - __VERIFIER_expect_fail(*i == 8, "Wrong underlying concrete value"); + rmc::expect_fail(*i == 8, "Wrong underlying concrete value"); } None => { assert!(false); diff --git a/src/test/rmc/DynTrait/boxed_closure_fail.rs b/src/test/rmc/DynTrait/boxed_closure_fail.rs index 4385ba9b52c1b..7d27d100104a1 100644 --- a/src/test/rmc/DynTrait/boxed_closure_fail.rs +++ b/src/test/rmc/DynTrait/boxed_closure_fail.rs @@ -3,12 +3,10 @@ // rmc-verify-fail // Check that we can codegen a boxed dyn closure and fail an inner assertion -include!("../../rmc-prelude.rs"); - pub fn main() { // Create a boxed once-callable closure let f: Box = Box::new(|x| { - __VERIFIER_expect_fail(x == 2, "Wrong int"); + rmc::expect_fail(x == 2, "Wrong int"); }); // Call it diff --git a/src/test/rmc/DynTrait/drop_boxed_dyn.rs b/src/test/rmc/DynTrait/drop_boxed_dyn.rs index fe63be6ac4c2b..63e3e04cd051a 100644 --- a/src/test/rmc/DynTrait/drop_boxed_dyn.rs +++ b/src/test/rmc/DynTrait/drop_boxed_dyn.rs @@ -3,8 +3,6 @@ // Check drop implementation for a boxed dynamic trait object. -include!("../../rmc-prelude.rs"); - static mut CELL: i32 = 0; trait T { @@ -38,7 +36,7 @@ impl Drop for Concrete2 { pub fn main() { { let x: Box; - if __nondet() { + if rmc::nondet() { x = Box::new(Concrete1 {}); } else { x = Box::new(Concrete2 {}); diff --git a/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs b/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs index 129425e9e2681..6d6ee07ff861f 100644 --- a/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs +++ b/src/test/rmc/DynTrait/drop_nested_boxed_dyn_fail.rs @@ -4,8 +4,6 @@ // rmc-verify-fail // cbmc-flags: --unwind 2 --unwinding-assertions -include!("../../rmc-prelude.rs"); - static mut CELL: i32 = 0; struct Concrete; @@ -38,6 +36,6 @@ pub fn main() { let _nested: Box = Box::new(x); } unsafe { - __VERIFIER_expect_fail(CELL == 2, "wrong cell value"); // Should fail + rmc::expect_fail(CELL == 2, "wrong cell value"); // Should fail } } diff --git a/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs b/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs index 8f75a2c159809..2ba54b860e055 100644 --- a/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_mut_fail.rs @@ -5,8 +5,6 @@ // function definition. Expected to fail because we are comparing // to an incorrect value. -include!("../../rmc-prelude.rs"); - fn takes_dyn_fun(mut fun: Box, x_ptr: &mut i32) { fun(x_ptr) } @@ -18,5 +16,5 @@ pub fn mut_i32_ptr(x: &mut i32) { pub fn main() { let mut x = 1; takes_dyn_fun(Box::new(&mut_i32_ptr), &mut x); - __VERIFIER_expect_fail(x == 3, "Wrong x") + rmc::expect_fail(x == 3, "Wrong x") } diff --git a/src/test/rmc/DynTrait/dyn_fn_once_fail.rs b/src/test/rmc/DynTrait/dyn_fn_once_fail.rs index 94dca5ce23e9e..c5252a555edad 100644 --- a/src/test/rmc/DynTrait/dyn_fn_once_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_once_fail.rs @@ -5,8 +5,6 @@ // function definition. Expected to fail because we are comparing // to an incorrect value. -include!("../../rmc-prelude.rs"); - fn takes_dyn_fun(fun: Box u32>) -> u32 { fun() } @@ -16,5 +14,5 @@ pub fn unit_to_u32() -> u32 { } pub fn main() { - __VERIFIER_expect_fail(takes_dyn_fun(Box::new(&unit_to_u32)) == 3, "Wrong u32") + rmc::expect_fail(takes_dyn_fun(Box::new(&unit_to_u32)) == 3, "Wrong u32") } diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs index 570c3bd0e7b1f..1f7776b7e8237 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure_capture_fail.rs @@ -6,13 +6,11 @@ #![feature(ptr_metadata)] include!("../Helpers/vtable_utils_ignore.rs"); -include!("../../rmc-prelude.rs"); - fn takes_dyn_fun(fun: &dyn Fn() -> i32) { let x = fun(); - __VERIFIER_expect_fail(x != 5, "Wrong return"); + rmc::expect_fail(x != 5, "Wrong return"); /* The closure captures `a` and thus is sized */ - __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 8, "Wrong size"); + rmc::expect_fail(size_from_vtable(vtable!(fun)) != 8, "Wrong size"); } pub fn main() { diff --git a/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs index 6e85ba48f2919..833caef3aeba1 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_closure_fail.rs @@ -5,13 +5,11 @@ #![feature(ptr_metadata)] include!("../Helpers/vtable_utils_ignore.rs"); -include!("../../rmc-prelude.rs"); - fn takes_dyn_fun(fun: &dyn Fn() -> i32) { let x = fun(); - __VERIFIER_expect_fail(x != 5, "Wrong return"); + rmc::expect_fail(x != 5, "Wrong return"); /* The closure does not capture anything and thus has zero size */ - __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); + rmc::expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); } pub fn main() { let closure = || 5; diff --git a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs index fde49c7b3fa4c..b0cb1cb329463 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs @@ -8,14 +8,12 @@ #![feature(ptr_metadata)] include!("../Helpers/vtable_utils_ignore.rs"); -include!("../../rmc-prelude.rs"); - fn takes_dyn_fun(fun: &dyn Fn() -> u32) { let x = fun(); - __VERIFIER_expect_fail(x != 5, "Wrong return"); + rmc::expect_fail(x != 5, "Wrong return"); /* The function dynamic object has no associated data */ - __VERIFIER_expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); + rmc::expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); } pub fn unit_to_u32() -> u32 { diff --git a/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs b/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs index 3b35bd07d7c5f..c6dc3bfc62aec 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names_fail.rs @@ -5,8 +5,6 @@ // generic types give the same Trait::function name pairs. Test the // wrong result for this _fail test. -include!("../../rmc-prelude.rs"); - trait Foo { fn method(&self, t: T) -> T; } @@ -26,5 +24,5 @@ pub fn main() { // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. let result = >::method(b, 22_u32); - __VERIFIER_expect_fail(result == 0, "Wrong result"); + rmc::expect_fail(result == 0, "Wrong result"); } diff --git a/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs b/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs index 1e79dddda0855..7ac194065a55d 100644 --- a/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs +++ b/src/test/rmc/DynTrait/generic_duplicate_names_impl_fail.rs @@ -6,8 +6,6 @@ // gives different concrete impls for i32 and u32. This _fail test // expects the wrong result. -include!("../../rmc-prelude.rs"); - trait Foo { fn method(&self, t: T) -> T; } @@ -33,8 +31,8 @@ pub fn main() { // The vtable for b will now have two Foo::method entries, // one for Foo and one for Foo. let result = >::method(b, 22_u32); - __VERIFIER_expect_fail(result == 0, "Wrong function"); + rmc::expect_fail(result == 0, "Wrong function"); let result = >::method(b, 22_i32); - __VERIFIER_expect_fail(result == 22_i32, "Wrong function"); + rmc::expect_fail(result == 22_i32, "Wrong function"); } diff --git a/src/test/rmc/DynTrait/main.rs b/src/test/rmc/DynTrait/main.rs index 84c1e77584c35..a61e7a94e6791 100644 --- a/src/test/rmc/DynTrait/main.rs +++ b/src/test/rmc/DynTrait/main.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - struct Sheep {} struct Cow {} @@ -31,7 +29,7 @@ fn random_animal(random_number: i64) -> Box { } pub fn main() { - let random_number = __nondet(); + let random_number = rmc::nondet(); let animal = random_animal(random_number); let s = animal.noise(); if (random_number < 5) { diff --git a/src/test/rmc/DynTrait/main_fail.rs b/src/test/rmc/DynTrait/main_fail.rs index f512d8a381279..88d909a593973 100644 --- a/src/test/rmc/DynTrait/main_fail.rs +++ b/src/test/rmc/DynTrait/main_fail.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - struct Sheep {} struct Cow {} @@ -31,12 +29,12 @@ fn random_animal(random_number: i64) -> Box { } pub fn main() { - let random_number = __nondet(); + let random_number = rmc::nondet(); let animal = random_animal(random_number); let s = animal.noise(); if (random_number < 5) { - __VERIFIER_expect_fail(s == 2, "Wrong noise"); + rmc::expect_fail(s == 2, "Wrong noise"); } else { - __VERIFIER_expect_fail(s == 1, "Wrong noise"); + rmc::expect_fail(s == 1, "Wrong noise"); } } diff --git a/src/test/rmc/DynTrait/nested_closures_fail.rs b/src/test/rmc/DynTrait/nested_closures_fail.rs index 76f4c898122af..1e5ca1b3c86c4 100644 --- a/src/test/rmc/DynTrait/nested_closures_fail.rs +++ b/src/test/rmc/DynTrait/nested_closures_fail.rs @@ -6,18 +6,16 @@ // rmc-verify-fail -include!("../../rmc-prelude.rs"); - pub fn main() { // Create a nested boxed once-callable closure let f: Box> = - Box::new(Box::new(|x| __VERIFIER_expect_fail(x != 1, "wrong int"))); + Box::new(Box::new(|x| rmc::expect_fail(x != 1, "wrong int"))); f(1); // Create a pointer to a closure let g = |x: f32, y: i32| { - __VERIFIER_expect_fail(x != 1.0, "wrong float"); - __VERIFIER_expect_fail(y != 2, "wrong int") + rmc::expect_fail(x != 1.0, "wrong float"); + rmc::expect_fail(y != 2, "wrong int") }; let p: &dyn Fn(f32, i32) = &g; p(1.0, 2); @@ -28,15 +26,14 @@ pub fn main() { // Create a boxed pointer to a closure let r: Box<&dyn Fn(f32, i32, bool)> = Box::new(&|x: f32, y: i32, z: bool| { - __VERIFIER_expect_fail(x != 1.0, "wrong float"); - __VERIFIER_expect_fail(y != 2, "wrong int"); - __VERIFIER_expect_fail(!z, "wrong bool"); + rmc::expect_fail(x != 1.0, "wrong float"); + rmc::expect_fail(y != 2, "wrong int"); + rmc::expect_fail(!z, "wrong bool"); }); r(1.0, 2, true); // Another boxed box - let s: Box> = - Box::new(Box::new(|x| __VERIFIER_expect_fail(x != 3, "wrong int"))); + let s: Box> = Box::new(Box::new(|x| rmc::expect_fail(x != 3, "wrong int"))); s(3); // A pointer to the boxed box diff --git a/src/test/rmc/DynTrait/vtable_size_align_drop.rs b/src/test/rmc/DynTrait/vtable_size_align_drop.rs index a394d178d83ca..1a5e2b64d28c7 100644 --- a/src/test/rmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/rmc/DynTrait/vtable_size_align_drop.rs @@ -13,8 +13,6 @@ use std::intrinsics::size_of; use std::ptr::drop_in_place; include!("../Helpers/vtable_utils_ignore.rs"); -include!("../../rmc-prelude.rs"); - // Different sized data fields on each struct struct Sheep { pub sheep_num: i32, diff --git a/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs index 485b573debdc8..6a8634b5b49bc 100644 --- a/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs +++ b/src/test/rmc/DynTrait/vtable_size_align_drop_fail.rs @@ -15,8 +15,6 @@ use std::intrinsics::size_of; use std::ptr::drop_in_place; include!("../Helpers/vtable_utils_ignore.rs"); -include!("../../rmc-prelude.rs"); - // Different sized data fields on each struct struct Sheep { pub sheep_num: i32, @@ -74,19 +72,19 @@ pub fn main() { let data_ptr = data!(animal_sheep); // Note: i32 ptr cast - __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "Wrong data"); // From Sheep + rmc::expect_fail(*(data_ptr as *mut i32) != 7, "Wrong data"); // From Sheep let vtable_ptr = vtable!(animal_sheep); // Drop pointer - __VERIFIER_expect_fail( + rmc::expect_fail( drop_from_vtable(vtable_ptr) != drop_in_place:: as *mut (), "Wrong drop", ); // Size and align as usizes - __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); - __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); + rmc::expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + rmc::expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); } // Check layout/values for Cow unsafe { @@ -96,18 +94,18 @@ pub fn main() { let data_ptr = data!(animal_cow); // Note: i8 ptr cast - __VERIFIER_expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow + rmc::expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow let vtable_ptr = vtable!(animal_cow); // Drop pointer - __VERIFIER_expect_fail( + rmc::expect_fail( drop_from_vtable(vtable_ptr) != drop_in_place:: as *mut (), "Wrong drop", ); // Size and align as usizes - __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); - __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); + rmc::expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + rmc::expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); } } diff --git a/src/test/rmc/EQ-NE/main.rs b/src/test/rmc/EQ-NE/main.rs index f590bad896192..03f41e7135898 100644 --- a/src/test/rmc/EQ-NE/main.rs +++ b/src/test/rmc/EQ-NE/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let x: u32 = __nondet(); + let x: u32 = rmc::nondet(); if x < u32::MAX >> 1 { let y = x * 2; diff --git a/src/test/rmc/Enum/result3.rs b/src/test/rmc/Enum/result3.rs index 03a578dff9ecc..3ebd6149c6bd2 100644 --- a/src/test/rmc/Enum/result3.rs +++ b/src/test/rmc/Enum/result3.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - #[derive(Debug, PartialEq)] pub enum Unit { Unit, @@ -13,10 +11,10 @@ fn foo(input: &Result) -> u32 { } pub fn main() { - let input: Result = __nondet(); + let input: Result = rmc::nondet(); let x = foo(&input); assert!(x == 3 || input != Err(Unit::Unit)); - let input: Result = if __nondet() { Ok(0) } else { Err(Unit::Unit) }; + let input: Result = if rmc::nondet() { Ok(0) } else { Err(Unit::Unit) }; let x = foo(&input); assert!(x != 3 || input == Err(Unit::Unit)); assert!(x != 0 || input == Ok(0)); diff --git a/src/test/rmc/FloatingPoint/main.rs b/src/test/rmc/FloatingPoint/main.rs index a2dfb762161c0..4067d31b603ff 100644 --- a/src/test/rmc/FloatingPoint/main.rs +++ b/src/test/rmc/FloatingPoint/main.rs @@ -1,10 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - macro_rules! test_floats { ($ty:ty) => { - let a: $ty = __nondet(); + let a: $ty = rmc::nondet(); let b = a / 2.0; if a < 0.0 { diff --git a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs index 216c8b12a79d8..ac9430959664a 100644 --- a/src/test/rmc/FunctionCall_Ret-NoParam/main.rs +++ b/src/test/rmc/FunctionCall_Ret-NoParam/main.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { let a = return_u32(); assert!(a < 10); @@ -12,7 +10,7 @@ pub fn main() { assert!(return_f64() < 11.0 && return_f64() > -11.0); } fn return_u32() -> u32 { - let x: u32 = __nondet(); + let x: u32 = rmc::nondet(); if x < 10 { return x; @@ -21,7 +19,7 @@ fn return_u32() -> u32 { } } fn return_u64() -> u64 { - let x: u64 = __nondet(); + let x: u64 = rmc::nondet(); if x > 100 { return x; @@ -30,7 +28,7 @@ fn return_u64() -> u64 { } } fn return_bool() -> bool { - let x: bool = __nondet(); + let x: bool = rmc::nondet(); if x { return x; } else { @@ -39,7 +37,7 @@ fn return_bool() -> bool { } fn return_f32() -> f32 { let x = 10.0; - let y: bool = __nondet(); + let y: bool = rmc::nondet(); if y { return x / 2.0; } else { @@ -47,7 +45,7 @@ fn return_f32() -> f32 { } } fn return_f64() -> f64 { - let x: f64 = __nondet(); + let x: f64 = rmc::nondet(); if x <= 10.0 && x >= -10.0 { return x; } else { diff --git a/src/test/rmc/FunctionCall_Ret-Param/main.rs b/src/test/rmc/FunctionCall_Ret-Param/main.rs index 6c3d1b9f3df93..687f55b280d60 100644 --- a/src/test/rmc/FunctionCall_Ret-Param/main.rs +++ b/src/test/rmc/FunctionCall_Ret-Param/main.rs @@ -8,10 +8,8 @@ // a verification failure (the loop being unwound depends on // a nondet. variable) -include!("../../rmc-prelude.rs"); - pub fn main() { - let x: u32 = __nondet(); + let x: u32 = rmc::nondet(); let pi = 3.14159265359; let x_iters = leibniz_pi(x); diff --git a/src/test/rmc/IfElseifElse_NonReturning/main.rs b/src/test/rmc/IfElseifElse_NonReturning/main.rs index 9609ee5835081..20876dfe471a8 100644 --- a/src/test/rmc/IfElseifElse_NonReturning/main.rs +++ b/src/test/rmc/IfElseifElse_NonReturning/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); if a % 3 == 0 { assert!(a != 4); diff --git a/src/test/rmc/IfElseifElse_Returning/main.rs b/src/test/rmc/IfElseifElse_Returning/main.rs index 667a3d070c300..067f5384cdf72 100644 --- a/src/test/rmc/IfElseifElse_Returning/main.rs +++ b/src/test/rmc/IfElseifElse_Returning/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); let b = if a % 3 == 0 { assert!(a != 5); @@ -18,7 +16,7 @@ pub fn main() { assert!(b < 3); - let c: u32 = __nondet(); + let c: u32 = rmc::nondet(); let d = if c > 100 { c diff --git a/src/test/rmc/LT-GT-LE-GE/main.rs b/src/test/rmc/LT-GT-LE-GE/main.rs index 5e8d156e8bce4..f2e992289cf91 100644 --- a/src/test/rmc/LT-GT-LE-GE/main.rs +++ b/src/test/rmc/LT-GT-LE-GE/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); let b = a / 2; assert!(b <= a); let c = b * 2; diff --git a/src/test/rmc/LoopLoop_NonReturning/main.rs b/src/test/rmc/LoopLoop_NonReturning/main.rs index a2246e6e91d12..0f6c092c73a29 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main.rs @@ -3,10 +3,8 @@ // cbmc-flags: --unwind 10 -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); if a < 1024 { loop { diff --git a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs index 53d5d28813439..a2b110f3216f0 100644 --- a/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs @@ -4,8 +4,6 @@ // rmc-flags: --no-default-checks // cbmc-flags: --unwind 9 -include!("../../rmc-prelude.rs"); - // This example tests the RMC flag `--no-default-checks` // // It is the same as `main.rs` except for the flags passed to RMC and CBMC @@ -24,7 +22,7 @@ include!("../../rmc-prelude.rs"); // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); if a < 1024 { loop { diff --git a/src/test/rmc/LoopWhile_NonReturning/main.rs b/src/test/rmc/LoopWhile_NonReturning/main.rs index f5d5a70783a6e..3e83f719ffbfa 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main.rs @@ -3,10 +3,8 @@ // cbmc-flags: --unwind 11 -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); if a < 1024 { while a > 0 { diff --git a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs index 20ac37b8090f3..1813b40d71156 100644 --- a/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs +++ b/src/test/rmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs @@ -4,8 +4,6 @@ // rmc-flags: --no-default-checks // cbmc-flags: --unwind 10 -include!("../../rmc-prelude.rs"); - // This example tests the RMC flag `--no-default-checks` // // It is the same as `main.rs` except for the flags passed to RMC and CBMC @@ -25,7 +23,7 @@ include!("../../rmc-prelude.rs"); // ** 0 of 1 failed (1 iterations) // VERIFICATION SUCCESSFUL pub fn main() { - let mut a: u32 = __nondet(); + let mut a: u32 = rmc::nondet(); if a < 1024 { while a > 0 { diff --git a/src/test/rmc/NondetVectors/bytes.rs b/src/test/rmc/NondetVectors/bytes.rs index d09f09818400d..20fdb0765d72f 100644 --- a/src/test/rmc/NondetVectors/bytes.rs +++ b/src/test/rmc/NondetVectors/bytes.rs @@ -2,23 +2,21 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::convert::TryInto; -include!("../../rmc-prelude.rs"); - pub fn main() { let input: &[u8] = &vec![ - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), - __nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), + rmc::nondet(), ]; let buffer = input.as_ref(); let bytes: [u8; 8] = buffer.try_into().unwrap(); let value = u64::from_be_bytes(bytes); - let idx: usize = __nondet(); + let idx: usize = rmc::nondet(); if idx < 8 { assert!(u64::to_be_bytes(value)[idx] == input[idx]); } diff --git a/src/test/rmc/NondetVectors/fixme_main.rs b/src/test/rmc/NondetVectors/fixme_main.rs index 572a01854b737..eaad4cf858062 100644 --- a/src/test/rmc/NondetVectors/fixme_main.rs +++ b/src/test/rmc/NondetVectors/fixme_main.rs @@ -1,17 +1,15 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT const FIFO_SIZE: usize = 2; -include!("../../rmc-prelude.rs"); - pub fn main() { - let len: usize = __nondet(); + let len: usize = rmc::nondet(); if !(len <= FIFO_SIZE) { return; } let _buf1: Vec = vec![0u8; len]; //< this works - let elt: u8 = __nondet(); + let elt: u8 = rmc::nondet(); let _buf2: Vec = vec![elt; len]; //< this fails: "memset destination region writeable" - let idx: usize = __nondet(); + let idx: usize = rmc::nondet(); if idx < len { assert!(_buf1[idx] == 0u8); assert!(_buf2[idx] == elt); diff --git a/src/test/rmc/Pointers_OtherTypes/main.rs b/src/test/rmc/Pointers_OtherTypes/main.rs index d078ecda875dc..d4151c2ce197d 100644 --- a/src/test/rmc/Pointers_OtherTypes/main.rs +++ b/src/test/rmc/Pointers_OtherTypes/main.rs @@ -8,8 +8,6 @@ // [main.NaN.1] line 25 NaN on * in var_30 * 0.0f: FAILURE // Tracking issue: https://github.com/model-checking/rmc/issues/307 -include!("../../rmc-prelude.rs"); - pub fn main() { let mut x = 1; add_two(&mut x); @@ -23,7 +21,7 @@ pub fn main() { make_true(&mut z); assert!(z); - let mut a: f32 = __nondet(); + let mut a: f32 = rmc::nondet(); let b = a; div_by_two(&mut a); // NaN diff --git a/src/test/rmc/SaturatingIntrinsics/fixme_128.rs b/src/test/rmc/SaturatingIntrinsics/fixme_128.rs index 0b0c4ed8747fc..004943ce1c119 100644 --- a/src/test/rmc/SaturatingIntrinsics/fixme_128.rs +++ b/src/test/rmc/SaturatingIntrinsics/fixme_128.rs @@ -5,10 +5,8 @@ #![feature(core_intrinsics)] use std::intrinsics; -include!("../../rmc-prelude.rs"); - pub fn main() { - let v: u128 = __nondet(); - let w: u128 = __nondet(); + let v: u128 = rmc::nondet(); + let w: u128 = rmc::nondet(); intrinsics::saturating_add(v, w); } diff --git a/src/test/rmc/SaturatingIntrinsics/main.rs b/src/test/rmc/SaturatingIntrinsics/main.rs index b9e2733aa2f51..9fa58dbc22a3a 100644 --- a/src/test/rmc/SaturatingIntrinsics/main.rs +++ b/src/test/rmc/SaturatingIntrinsics/main.rs @@ -3,12 +3,10 @@ #![feature(core_intrinsics)] use std::intrinsics; -include!("../../rmc-prelude.rs"); - macro_rules! test_saturating_intrinsics { ($ty:ty) => { - let v: $ty = __nondet(); - let w: $ty = __nondet(); + let v: $ty = rmc::nondet(); + let w: $ty = rmc::nondet(); let result = intrinsics::saturating_add(v, w); match (0 <= v, 0 <= w) { (true, true) => { diff --git a/src/test/rmc/Scopes_NonReturning/main.rs b/src/test/rmc/Scopes_NonReturning/main.rs index 9a726251cda81..46ca5f2823653 100644 --- a/src/test/rmc/Scopes_NonReturning/main.rs +++ b/src/test/rmc/Scopes_NonReturning/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: u32 = __nondet(); + let a: u32 = rmc::nondet(); let b = a / 2; let c = a / 2; { diff --git a/src/test/rmc/Scopes_Returning/main.rs b/src/test/rmc/Scopes_Returning/main.rs index 83e93ec7d8355..6400f73f35bca 100644 --- a/src/test/rmc/Scopes_Returning/main.rs +++ b/src/test/rmc/Scopes_Returning/main.rs @@ -1,7 +1,5 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { let x = { 5 }; assert!(x == 5); @@ -20,7 +18,7 @@ pub fn main() { }; assert!(c == 10); - let d: u32 = __nondet(); + let d: u32 = rmc::nondet(); let e = { let f: u32; @@ -34,7 +32,7 @@ pub fn main() { }; assert!(e == d || e == 10); - let g: u32 = __nondet(); + let g: u32 = rmc::nondet(); let h = { if g < 10 { g } else { 10 } }; diff --git a/src/test/rmc/Slice/slice_from_raw.rs b/src/test/rmc/Slice/slice_from_raw.rs index ee6c91940239a..b1036fde7aba6 100644 --- a/src/test/rmc/Slice/slice_from_raw.rs +++ b/src/test/rmc/Slice/slice_from_raw.rs @@ -4,8 +4,6 @@ use std::slice; -include!("../../rmc-prelude.rs"); - // From Listing 19-7: Creating a slice from an arbitrary memory location. https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html pub fn main() { let address = 0x01234usize; diff --git a/src/test/rmc/i32-Unary-/main.rs b/src/test/rmc/i32-Unary-/main.rs index c614670caa421..066ac239eb202 100644 --- a/src/test/rmc/i32-Unary-/main.rs +++ b/src/test/rmc/i32-Unary-/main.rs @@ -1,9 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -include!("../../rmc-prelude.rs"); - pub fn main() { - let a: i32 = __nondet(); + let a: i32 = rmc::nondet(); if -100000 < a && a < 100000 { let b = -a; diff --git a/src/test/serial/serial.rs b/src/test/serial/serial.rs index 468122e5d811f..230ce94db0ca4 100644 --- a/src/test/serial/serial.rs +++ b/src/test/serial/serial.rs @@ -322,15 +322,13 @@ impl Serial { } } -include!("../../rmc-prelude.rs"); - fn main() { { // test_serial_modem() let mut serial = Serial::new_sink(EventFd {}); - let a: u8 = __nondet(); - let b: u8 = __nondet(); - let c: u8 = __nondet(); + let a: u8 = rmc::nondet(); + let b: u8 = rmc::nondet(); + let c: u8 = rmc::nondet(); serial.write(MCR as u64, &[MCR_LOOP_BIT as u8]); serial.write(DATA as u64, &[a]); @@ -354,9 +352,9 @@ fn main() { // // test_serial_data_len() // const LEN: usize = 1; // let mut serial = Serial::new_out(EventFd {}, OutWrapper::new()); - // let a: u8 = __nondet(); - // let b: u8 = __nondet(); - // let c: u8 = __nondet(); + // let a: u8 = rmc::nondet(); + // let b: u8 = rmc::nondet(); + // let c: u8 = rmc::nondet(); // // let missed_writes_before = METRICS.uart.missed_write_count.count(); // // Trying to write data of length different than the one that we initialized the device with diff --git a/src/test/serial/serial2.rs b/src/test/serial/serial2.rs index c1d8b9ff4921b..f05d9f7ca4d2c 100644 --- a/src/test/serial/serial2.rs +++ b/src/test/serial/serial2.rs @@ -322,16 +322,14 @@ impl Serial { } } -include!("../../rmc-prelude.rs"); - fn main() { { // test_serial_data_len() const LEN: usize = 1; let mut serial = Serial::new_out(EventFd {}, OutWrapper::new()); - let a: u8 = __nondet(); - let b: u8 = __nondet(); - let c: u8 = __nondet(); + let a: u8 = rmc::nondet(); + let b: u8 = rmc::nondet(); + let c: u8 = rmc::nondet(); // let missed_writes_before = METRICS.uart.missed_write_count.count(); // Trying to write data of length different than the one that we initialized the device with diff --git a/src/test/serial/serial_spec.rs b/src/test/serial/serial_spec.rs index ceb5b320b9a74..a63a2630d791f 100644 --- a/src/test/serial/serial_spec.rs +++ b/src/test/serial/serial_spec.rs @@ -464,14 +464,12 @@ impl Serial { } } -include!("../../rmc-prelude.rs"); - fn main() { { let mut serial = Serial::new_sink(EventFd {}); - let a: u8 = __nondet(); - let b: u8 = __nondet(); - let c: u8 = __nondet(); + let a: u8 = rmc::nondet(); + let b: u8 = rmc::nondet(); + let c: u8 = rmc::nondet(); serial.write(MCR as u64, &[MCR_LOOP_BIT as u8]); serial.write(DATA as u64, &[a]); diff --git a/src/test/smack/basic/arith_assume.rs b/src/test/smack/basic/arith_assume.rs index ccd7076079281..2abacaccb6b1b 100644 --- a/src/test/smack/basic/arith_assume.rs +++ b/src/test/smack/basic/arith_assume.rs @@ -2,11 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect verified -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); - let b = __nondet(); + let a = rmc::nondet(); + let b = rmc::nondet(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/basic/arith_assume2.rs b/src/test/smack/basic/arith_assume2.rs index ccd7076079281..2abacaccb6b1b 100644 --- a/src/test/smack/basic/arith_assume2.rs +++ b/src/test/smack/basic/arith_assume2.rs @@ -2,11 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // @expect verified -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); - let b = __nondet(); + let a = rmc::nondet(); + let b = rmc::nondet(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/basic/arith_assume3.rs b/src/test/smack/basic/arith_assume3.rs index b279588af7de3..c63397ddc7945 100644 --- a/src/test/smack/basic/arith_assume3.rs +++ b/src/test/smack/basic/arith_assume3.rs @@ -3,11 +3,9 @@ // @expect error // rmc-verify-fail -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); - let b = __nondet(); + let a = rmc::nondet(); + let b = rmc::nondet(); if 4 < a && a < 8 { // a in [5,7] if 5 < b && b < 9 { diff --git a/src/test/smack/functions/closure.rs b/src/test/smack/functions/closure.rs index dbaa4217448e7..ab7c2870603f7 100644 --- a/src/test/smack/functions/closure.rs +++ b/src/test/smack/functions/closure.rs @@ -10,10 +10,8 @@ where some_closure(1); } -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut num: i32 = __nondet(); + let mut num: i32 = rmc::nondet(); if num <= std::i32::MAX - 10 { let original_num = num; { diff --git a/src/test/smack/functions/closure_fail.rs b/src/test/smack/functions/closure_fail.rs index e858e3c878589..371b0ba83343b 100644 --- a/src/test/smack/functions/closure_fail.rs +++ b/src/test/smack/functions/closure_fail.rs @@ -11,10 +11,8 @@ where some_closure(1); } -include!("../../rmc-prelude.rs"); - pub fn main() { - let mut num: i32 = __nondet(); + let mut num: i32 = rmc::nondet(); if num <= std::i32::MAX - 10 { let original_num = num; { diff --git a/src/test/smack/functions/double.rs b/src/test/smack/functions/double.rs index 6774d1e770e51..ed030d8b7b7e0 100644 --- a/src/test/smack/functions/double.rs +++ b/src/test/smack/functions/double.rs @@ -6,10 +6,8 @@ fn double(a: u32) -> u32 { a * 2 } -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); + let a = rmc::nondet(); if a <= std::u32::MAX / 2 { let b = double(a); assert!(b == 2 * a); diff --git a/src/test/smack/functions/double_fail.rs b/src/test/smack/functions/double_fail.rs index 3e3d9597d0070..668b04f085963 100644 --- a/src/test/smack/functions/double_fail.rs +++ b/src/test/smack/functions/double_fail.rs @@ -7,10 +7,8 @@ fn double(a: u32) -> u32 { a * 2 } -include!("../../rmc-prelude.rs"); - pub fn main() { - let a = __nondet(); + let a = rmc::nondet(); if a <= std::u32::MAX / 2 { // avoid overflow let b = double(a); diff --git a/src/test/smack/generics/generic_function.rs b/src/test/smack/generics/generic_function.rs index 8be9bab94a2b9..ee80596929794 100644 --- a/src/test/smack/generics/generic_function.rs +++ b/src/test/smack/generics/generic_function.rs @@ -33,14 +33,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function1.rs b/src/test/smack/generics/generic_function1.rs index d978973735339..eb39959a66c5a 100644 --- a/src/test/smack/generics/generic_function1.rs +++ b/src/test/smack/generics/generic_function1.rs @@ -34,14 +34,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function2.rs b/src/test/smack/generics/generic_function2.rs index a45f5d17a3289..4ccb6b6582c65 100644 --- a/src/test/smack/generics/generic_function2.rs +++ b/src/test/smack/generics/generic_function2.rs @@ -34,14 +34,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function3.rs b/src/test/smack/generics/generic_function3.rs index c2f7f742be1c5..4065966e0495d 100644 --- a/src/test/smack/generics/generic_function3.rs +++ b/src/test/smack/generics/generic_function3.rs @@ -34,14 +34,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function4.rs b/src/test/smack/generics/generic_function4.rs index 52f4f5d3b4fd1..c655cab54d6b2 100644 --- a/src/test/smack/generics/generic_function4.rs +++ b/src/test/smack/generics/generic_function4.rs @@ -34,14 +34,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/generics/generic_function5.rs b/src/test/smack/generics/generic_function5.rs index 1f9369510df59..081c67e4cd814 100644 --- a/src/test/smack/generics/generic_function5.rs +++ b/src/test/smack/generics/generic_function5.rs @@ -34,14 +34,12 @@ fn swapem>(s: U) -> U { s.swap_items() } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x2 = __nondet(); - let y2 = __nondet(); - let x3 = __nondet(); - let y3 = __nondet(); - let z3 = __nondet(); + let x2 = rmc::nondet(); + let y2 = rmc::nondet(); + let x3 = rmc::nondet(); + let y3 = rmc::nondet(); + let z3 = rmc::nondet(); let p2 = Point:: { x: x2, y: y2 }; let p3 = Point3:: { x: x3, y: y3, z: z3 }; diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs index 6f57722d8ea0b..006ec6f50df34 100644 --- a/src/test/smack/loops/gauss_sum_nondet.rs +++ b/src/test/smack/loops/gauss_sum_nondet.rs @@ -4,11 +4,9 @@ // @expect verified // cbmc-flags: --unwind 5 -include!("../../rmc-prelude.rs"); - pub fn main() { let mut sum = 0; - let b: u64 = __nondet(); + let b: u64 = rmc::nondet(); if b < 5 && b > 1 { for i in 0..b { sum += i; diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs index 43045d2f15668..216665b15fdcb 100644 --- a/src/test/smack/loops/gauss_sum_nondet_fail.rs +++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs @@ -5,11 +5,9 @@ // rmc-verify-fail // cbmc-flags: --unwind 5 -include!("../../rmc-prelude.rs"); - pub fn main() { let mut sum = 0; - let b: u64 = __nondet(); + let b: u64 = rmc::nondet(); if b < 5 && b > 1 { for i in 0..b { sum += i; diff --git a/src/test/smack/loops/iterator.rs b/src/test/smack/loops/iterator.rs index 7d810fe79e032..387f81e4bcc53 100644 --- a/src/test/smack/loops/iterator.rs +++ b/src/test/smack/loops/iterator.rs @@ -13,11 +13,9 @@ fn fac(n: u64) -> u64 { } } -include!("../../rmc-prelude.rs"); - pub fn main() { let mut a = 1; - let n = __nondet(); + let n = rmc::nondet(); if n < 5 { for i in 1..n + 1 as u64 { a *= i; diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs index 4a5b537d8582a..08fc810a53a43 100644 --- a/src/test/smack/loops/iterator_fail.rs +++ b/src/test/smack/loops/iterator_fail.rs @@ -13,11 +13,9 @@ fn fac(n: u64) -> u64 { } } -include!("../../rmc-prelude.rs"); - pub fn main() { let mut a = 1; - let n = __nondet(); + let n = rmc::nondet(); if n < 5 { for i in 1..n + 1 as u64 { a *= i; diff --git a/src/test/smack/structures/option.rs b/src/test/smack/structures/option.rs index 9349091cd07ba..9a2ad11f39a42 100644 --- a/src/test/smack/structures/option.rs +++ b/src/test/smack/structures/option.rs @@ -6,10 +6,8 @@ fn safe_div(x: u32, y: u32) -> Option { if y != 0 { Some(x / y) } else { None } } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x = __nondet(); + let x = rmc::nondet(); if x > 0 && x <= 200 { // avoid overflow let a = safe_div(2 * x, x); @@ -17,7 +15,7 @@ pub fn main() { Some(c) => assert!(c == 2), None => assert!(false), }; - let y = __nondet(); + let y = rmc::nondet(); if y > 0 { let b = safe_div(x, y); match b { diff --git a/src/test/smack/structures/option_fail.rs b/src/test/smack/structures/option_fail.rs index 70a835f62f079..1d204297aaa86 100644 --- a/src/test/smack/structures/option_fail.rs +++ b/src/test/smack/structures/option_fail.rs @@ -7,10 +7,8 @@ fn safe_div(x: u32, y: u32) -> Option { if y != 0 { Some(x / y) } else { None } } -include!("../../rmc-prelude.rs"); - pub fn main() { - let x = __nondet(); + let x = rmc::nondet(); if x > 0 && x <= 100 { // avoid overflow let a = safe_div(2 * x, x); @@ -18,7 +16,7 @@ pub fn main() { Some(c) => assert!(c == 2), None => assert!(false), }; - let y = __nondet(); + let y = rmc::nondet(); let b = safe_div(x, y); match b { Some(c) => assert!(c == x / y), diff --git a/src/test/smack/structures/point.rs b/src/test/smack/structures/point.rs index 1550eceda38e5..1306df3d52d9d 100644 --- a/src/test/smack/structures/point.rs +++ b/src/test/smack/structures/point.rs @@ -36,13 +36,11 @@ impl AddAssign for Point { } } -include!("../../rmc-prelude.rs"); - pub fn main() { - let w = __nondet(); - let x = __nondet(); - let y = __nondet(); - let z = __nondet(); + let w = rmc::nondet(); + let x = rmc::nondet(); + let y = rmc::nondet(); + let z = rmc::nondet(); if w <= std::u64::MAX / 2 // avoid overflow && x <= std::u64::MAX / 2 // avoid overflow diff --git a/src/test/smack/structures/point_fail.rs b/src/test/smack/structures/point_fail.rs index 8d6895a9b0c77..97204dc8d54d7 100644 --- a/src/test/smack/structures/point_fail.rs +++ b/src/test/smack/structures/point_fail.rs @@ -37,13 +37,11 @@ impl AddAssign for Point { } } -include!("../../rmc-prelude.rs"); - pub fn main() { - let w = __nondet(); - let x = __nondet(); - let y = __nondet(); - let z = __nondet(); + let w = rmc::nondet(); + let x = rmc::nondet(); + let y = rmc::nondet(); + let z = rmc::nondet(); if w <= std::u64::MAX / 2 // avoid overflow && x <= std::u64::MAX / 2 // avoid overflow diff --git a/src/test/stub-tests/HashSet/concrete.rs b/src/test/stub-tests/HashSet/concrete.rs index 605aa86e5b99a..b1000efb767ab 100644 --- a/src/test/stub-tests/HashSet/concrete.rs +++ b/src/test/stub-tests/HashSet/concrete.rs @@ -2,20 +2,18 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type c-ffi -include!{"../../rmc-prelude.rs"} - fn main() { let mut h: HashSet = HashSet::new(); // TODO: This test should ideally work with nondeterminstic values but for // for the moment it does not. // - // let a: u16 = __nondet(); - // let b: u16 = __nondet(); - // let c: u16 = __nondet(); - // __VERIFIER_assume(a != b); - // __VERIFIER_assume(a != c); - // __VERIFIER_assume(b != c); + // let a: u16 = rmc::nondet(); + // let b: u16 = rmc::nondet(); + // let c: u16 = rmc::nondet(); + // rmc::assume(a != b); + // rmc::assume(a != c); + // rmc::assume(b != c); assert!(h.insert(5)); assert!(h.contains(&5)); diff --git a/src/test/stub-tests/HashSet/ignore-nondet.rs b/src/test/stub-tests/HashSet/ignore-nondet.rs index 494a262613ce9..b2a6ec7faebdd 100644 --- a/src/test/stub-tests/HashSet/ignore-nondet.rs +++ b/src/test/stub-tests/HashSet/ignore-nondet.rs @@ -2,19 +2,17 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type c-ffi -include!{"../../rmc-prelude.rs"} - fn main() { let mut h: HashSet = HashSet::new(); // TODO: This test should ideally work with nondeterminstic values but for // for the moment it does not. - let a: u16 = __nondet(); - let b: u16 = __nondet(); - let c: u16 = __nondet(); - __VERIFIER_assume(a != b); - __VERIFIER_assume(a != c); - __VERIFIER_assume(b != c); + let a: u16 = rmc::nondet(); + let b: u16 = rmc::nondet(); + let c: u16 = rmc::nondet(); + rmc::assume(a != b); + rmc::assume(a != c); + rmc::assume(b != c); assert!(h.insert(a)); assert!(h.contains(&a)); diff --git a/src/test/stub-tests/Vec/append.rs b/src/test/stub-tests/Vec/append.rs index 3301bdf0bbcac..bf8d3d1487dd4 100644 --- a/src/test/stub-tests/Vec/append.rs +++ b/src/test/stub-tests/Vec/append.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn append_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/as_mut_ptr.rs b/src/test/stub-tests/Vec/as_mut_ptr.rs index c7d26663b05f0..287c361c0f0dd 100644 --- a/src/test/stub-tests/Vec/as_mut_ptr.rs +++ b/src/test/stub-tests/Vec/as_mut_ptr.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn as_mut_ptr_test() { let size = 4; diff --git a/src/test/stub-tests/Vec/as_mut_slice.rs b/src/test/stub-tests/Vec/as_mut_slice.rs index e4c0cdeb13d90..b9981e54b3f43 100644 --- a/src/test/stub-tests/Vec/as_mut_slice.rs +++ b/src/test/stub-tests/Vec/as_mut_slice.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn as_mut_slice_test() { let mut buffer = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/as_ptr.rs b/src/test/stub-tests/Vec/as_ptr.rs index aeb370a72b4d9..b32c5eab4f7e9 100644 --- a/src/test/stub-tests/Vec/as_ptr.rs +++ b/src/test/stub-tests/Vec/as_ptr.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn as_ptr_test() { let x = rmc_vec![1, 2, 4]; diff --git a/src/test/stub-tests/Vec/as_slice.rs b/src/test/stub-tests/Vec/as_slice.rs index 916820327bf3a..dba71fee65376 100644 --- a/src/test/stub-tests/Vec/as_slice.rs +++ b/src/test/stub-tests/Vec/as_slice.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn as_slice_test() { use std::io::{self, Write}; diff --git a/src/test/stub-tests/Vec/capacity.rs b/src/test/stub-tests/Vec/capacity.rs index f03e3a94d72ae..f975a6c5cd2a8 100644 --- a/src/test/stub-tests/Vec/capacity.rs +++ b/src/test/stub-tests/Vec/capacity.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn capacity_test() { let mut vec = Vec::with_capacity(10); diff --git a/src/test/stub-tests/Vec/clear.rs b/src/test/stub-tests/Vec/clear.rs index 88ca7fd9f4471..e0ad018f095d0 100644 --- a/src/test/stub-tests/Vec/clear.rs +++ b/src/test/stub-tests/Vec/clear.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn clear_test() { let mut v = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/clone.rs b/src/test/stub-tests/Vec/clone.rs index f71d5620839f8..6232a599a9b34 100644 --- a/src/test/stub-tests/Vec/clone.rs +++ b/src/test/stub-tests/Vec/clone.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn clone_test() { let v = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/drop.rs b/src/test/stub-tests/Vec/drop.rs index 54b34fb677b3f..b0c1b7b79f4c9 100644 --- a/src/test/stub-tests/Vec/drop.rs +++ b/src/test/stub-tests/Vec/drop.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - static mut GLOB: i32 = 1; struct Test { diff --git a/src/test/stub-tests/Vec/extend.rs b/src/test/stub-tests/Vec/extend.rs index 4e3d04d024cc3..4e18a4549831b 100644 --- a/src/test/stub-tests/Vec/extend.rs +++ b/src/test/stub-tests/Vec/extend.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn extend_test() { let mut vec = Vec::new(); diff --git a/src/test/stub-tests/Vec/extend_from_slice.rs b/src/test/stub-tests/Vec/extend_from_slice.rs index bb0fc31b526ad..d66f38cf76c10 100644 --- a/src/test/stub-tests/Vec/extend_from_slice.rs +++ b/src/test/stub-tests/Vec/extend_from_slice.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn extend_from_slice_test() { let mut vec = rmc_vec![1]; diff --git a/src/test/stub-tests/Vec/from_raw_parts.rs b/src/test/stub-tests/Vec/from_raw_parts.rs index a13624f16b008..97b0197392030 100644 --- a/src/test/stub-tests/Vec/from_raw_parts.rs +++ b/src/test/stub-tests/Vec/from_raw_parts.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - use std::ptr; fn main() { diff --git a/src/test/stub-tests/Vec/from_slice.rs b/src/test/stub-tests/Vec/from_slice.rs index 96ed226bed524..d014bbf5a0851 100644 --- a/src/test/stub-tests/Vec/from_slice.rs +++ b/src/test/stub-tests/Vec/from_slice.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn from_slice_test() { assert_eq!(Vec::from(&[1, 2, 3][..]), rmc_vec![1, 2, 3]); diff --git a/src/test/stub-tests/Vec/from_str.rs b/src/test/stub-tests/Vec/from_str.rs index e59ceb08ab078..71d0e7e045d4f 100644 --- a/src/test/stub-tests/Vec/from_str.rs +++ b/src/test/stub-tests/Vec/from_str.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn from_str_test() { assert_eq!(Vec::from("123"), rmc_vec![b'1', b'2', b'3']); diff --git a/src/test/stub-tests/Vec/insert.rs b/src/test/stub-tests/Vec/insert.rs index dd9682f6913c2..4c365ace722f9 100644 --- a/src/test/stub-tests/Vec/insert.rs +++ b/src/test/stub-tests/Vec/insert.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn insert_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/into_iter.rs b/src/test/stub-tests/Vec/into_iter.rs index 74282a3bc746d..75a54f53f8bd0 100644 --- a/src/test/stub-tests/Vec/into_iter.rs +++ b/src/test/stub-tests/Vec/into_iter.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn into_iter_test() { let v = rmc_vec![1, 4, 5]; diff --git a/src/test/stub-tests/Vec/is_empty.rs b/src/test/stub-tests/Vec/is_empty.rs index 083ab49cf5ed5..30d78cc53df2c 100644 --- a/src/test/stub-tests/Vec/is_empty.rs +++ b/src/test/stub-tests/Vec/is_empty.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn is_empty_test() { let mut v = Vec::new(); diff --git a/src/test/stub-tests/Vec/len.rs b/src/test/stub-tests/Vec/len.rs index 33bdb0f1caed3..558bb2965e939 100644 --- a/src/test/stub-tests/Vec/len.rs +++ b/src/test/stub-tests/Vec/len.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type no-back -include!{"../../rmc-prelude.rs"} - fn main() { fn append_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/new.rs b/src/test/stub-tests/Vec/new.rs index 9324237b91fa6..27fdcf6828fde 100644 --- a/src/test/stub-tests/Vec/new.rs +++ b/src/test/stub-tests/Vec/new.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn new_test() { let v: Vec = Vec::new(); diff --git a/src/test/stub-tests/Vec/pop.rs b/src/test/stub-tests/Vec/pop.rs index 067598676fddf..e4a471007d1e5 100644 --- a/src/test/stub-tests/Vec/pop.rs +++ b/src/test/stub-tests/Vec/pop.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn pop_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/push.rs b/src/test/stub-tests/Vec/push.rs index 0dc69f090037c..1315eb2843696 100644 --- a/src/test/stub-tests/Vec/push.rs +++ b/src/test/stub-tests/Vec/push.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn push_test() { let mut vec = rmc_vec![1, 2]; diff --git a/src/test/stub-tests/Vec/remove.rs b/src/test/stub-tests/Vec/remove.rs index f035ea830764f..040b3c628de87 100644 --- a/src/test/stub-tests/Vec/remove.rs +++ b/src/test/stub-tests/Vec/remove.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn remove_test() { let mut v = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/reserve.rs b/src/test/stub-tests/Vec/reserve.rs index 6dfa07ac47fc3..5868a9204609e 100644 --- a/src/test/stub-tests/Vec/reserve.rs +++ b/src/test/stub-tests/Vec/reserve.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn reserve_test() { let mut vec = rmc_vec![1]; diff --git a/src/test/stub-tests/Vec/reserve_exact.rs b/src/test/stub-tests/Vec/reserve_exact.rs index 19b51b30243a5..f575343d29999 100644 --- a/src/test/stub-tests/Vec/reserve_exact.rs +++ b/src/test/stub-tests/Vec/reserve_exact.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn reserve_exact_test() { let mut vec = rmc_vec![1]; diff --git a/src/test/stub-tests/Vec/resize.rs b/src/test/stub-tests/Vec/resize.rs index a3c08ed69d3e5..39d503bc2c32e 100644 --- a/src/test/stub-tests/Vec/resize.rs +++ b/src/test/stub-tests/Vec/resize.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn resize_test() { let mut vec = rmc_vec![1]; diff --git a/src/test/stub-tests/Vec/resize_with.rs b/src/test/stub-tests/Vec/resize_with.rs index 9fc65fa370475..e986a71ed2c0e 100644 --- a/src/test/stub-tests/Vec/resize_with.rs +++ b/src/test/stub-tests/Vec/resize_with.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn resize_with_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/shrink_to.rs b/src/test/stub-tests/Vec/shrink_to.rs index cd474457a3078..595bd2fa70616 100644 --- a/src/test/stub-tests/Vec/shrink_to.rs +++ b/src/test/stub-tests/Vec/shrink_to.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn shrink_to_test() { let mut vec = Vec::with_capacity(10); @@ -11,7 +9,7 @@ fn main() { vec.shrink_to(4); assert!(vec.capacity() >= 4); vec.shrink_to(0); - __VERIFIER_expect_fail(vec.capacity() >= 3, "Capacity shrinked to 0"); + rmc::expect_fail(vec.capacity() >= 3, "Capacity shrinked to 0"); } shrink_to_test() diff --git a/src/test/stub-tests/Vec/shrink_to_fit.rs b/src/test/stub-tests/Vec/shrink_to_fit.rs index bf79b122fa9b0..c3777d27638e0 100644 --- a/src/test/stub-tests/Vec/shrink_to_fit.rs +++ b/src/test/stub-tests/Vec/shrink_to_fit.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn shrink_to_fit_test() { let mut vec = Vec::with_capacity(10); diff --git a/src/test/stub-tests/Vec/simple.rs b/src/test/stub-tests/Vec/simple.rs index 133c8302cade6..cafc0082df53d 100644 --- a/src/test/stub-tests/Vec/simple.rs +++ b/src/test/stub-tests/Vec/simple.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn simple_test() { let mut vec: Vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/split_off.rs b/src/test/stub-tests/Vec/split_off.rs index 0daed5dd74d24..ca83b0e16b3de 100644 --- a/src/test/stub-tests/Vec/split_off.rs +++ b/src/test/stub-tests/Vec/split_off.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn split_off_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/swap_remove.rs b/src/test/stub-tests/Vec/swap_remove.rs index f5aa234db181a..7d8a68260e07e 100644 --- a/src/test/stub-tests/Vec/swap_remove.rs +++ b/src/test/stub-tests/Vec/swap_remove.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn swap_remove_test() { let mut v = rmc_vec![1, 2, 3, 4]; diff --git a/src/test/stub-tests/Vec/truncate.rs b/src/test/stub-tests/Vec/truncate.rs index 4ba74a4867ba6..d230401ef8089 100644 --- a/src/test/stub-tests/Vec/truncate.rs +++ b/src/test/stub-tests/Vec/truncate.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn truncate_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/test/stub-tests/Vec/truncate_drop.rs b/src/test/stub-tests/Vec/truncate_drop.rs index f3f33dadf758e..6a389de4468b9 100644 --- a/src/test/stub-tests/Vec/truncate_drop.rs +++ b/src/test/stub-tests/Vec/truncate_drop.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - static mut GLOB: i32 = 1; struct Test { diff --git a/src/test/stub-tests/Vec/truncate_reduce.rs b/src/test/stub-tests/Vec/truncate_reduce.rs index 2fae0ee621eeb..e91fdf8f17dec 100644 --- a/src/test/stub-tests/Vec/truncate_reduce.rs +++ b/src/test/stub-tests/Vec/truncate_reduce.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn truncate_reduce_test() { let mut vec = rmc_vec![1, 2, 3, 4, 5]; diff --git a/src/test/stub-tests/Vec/truncate_zero.rs b/src/test/stub-tests/Vec/truncate_zero.rs index 9bdf28e8c146c..a90d0a6c91efc 100644 --- a/src/test/stub-tests/Vec/truncate_zero.rs +++ b/src/test/stub-tests/Vec/truncate_zero.rs @@ -1,8 +1,6 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT // rmc-flags: --use-abs --abs-type rmc -include!{"../../rmc-prelude.rs"} - fn main() { fn truncate_zero_test() { let mut vec = rmc_vec![1, 2, 3]; diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs index 9ac112405f0f9..abb5ef296e86c 100644 --- a/src/tools/compiletest/src/runtest.rs +++ b/src/tools/compiletest/src/runtest.rs @@ -2251,17 +2251,7 @@ impl<'test> TestCx<'test> { let mut rustc = Command::new("rmc-rustc"); rustc .args(self.props.compile_flags.clone()) - .args([ - "-Z", - "codegen-backend=gotoc", - "-Z", - "trim-diagnostic-paths=no", - "-Z", - "human_readable_cgu_names", - "--cfg=rmc", - "--crate-type=lib", - "--out-dir", - ]) + .args(["--out-dir"]) .arg(self.output_base_dir()) .arg(&self.testpaths.file); self.add_rmc_dir_to_path(&mut rustc); diff --git a/src/tools/dashboard/src/util.rs b/src/tools/dashboard/src/util.rs index da1b22b4efd03..7b8deabc96462 100644 --- a/src/tools/dashboard/src/util.rs +++ b/src/tools/dashboard/src/util.rs @@ -182,21 +182,7 @@ pub fn add_check_job(litani: &mut Litani, test_props: &TestProps) { pub fn add_codegen_job(litani: &mut Litani, test_props: &TestProps) { let exit_status = if test_props.fail_step == Some(FailStep::Codegen) { 1 } else { 0 }; let mut rmc_rustc = Command::new("rmc-rustc"); - rmc_rustc - .args(&test_props.rustc_args) - .args([ - "-Z", - "codegen-backend=gotoc", - "-Z", - "trim-diagnostic-paths=no", - "--cfg=rmc", - "--out-dir", - "build/tmp", - "-Z", - "human_readable_cgu_names", - "--crate-type=lib", - ]) - .arg(&test_props.path); + rmc_rustc.args(&test_props.rustc_args).args(["--out-dir", "build/tmp"]).arg(&test_props.path); let mut phony_in = test_props.path.clone(); phony_in.set_extension("check");