Add support to Cargo.toml metadata tables (rust-lang#740)

Fixes rust-lang#739.

Cargo rmc is able to extract flags from a toml configuration file. In
order to provide a good experience to users that want to add
configurations to their Cargo.toml, we are adding support to the
standard metadata tables supported by cargo.

We still support the [rmc] tables in cases users prefer to use a
different rmc.toml file, but this is discouraged for Cargo.toml files
since it will generate a warning every time a user runs cargo.

Author: celinval

scripts/cargo-rmc

@@ -275,27 +275,41 @@ def parse_args():
         post_process(cl_args)
         return cl_args
 
-# Extract a list of args based on given config toml
+
 def extract_flags_from_toml(path):
+    """Extract a list of args based on given config toml
+       RMC can be configured in the following tables:
+         - rmc
+         - workspace.metadata.rmc
+         - package.metadata.rmc
+       The only field supported today is flags.
+    """
     # Load the flag data from toml
     data = toml.load(path)
 
-    # Extract the rmc flags from the toml, if any present
-    if ("rmc" not in data) or ("flags" not in data["rmc"]):
-        # If no flags are present, just return none
+    # Extract the rmc flags from the toml, if any of the supported tables are present
+    rmc_data = dict()
+    tables = ["workspace.metadata.rmc", "package.metadata.rmc", "rmc"]
+    for table_name in tables:
+        table = data
+        for section in table_name.split("."):
+            table = table.get(section, dict())
+        rmc_data.update(table)
+
+    if "flags" not in rmc_data:
         return []
-    rmc_data = data["rmc"]
+
     flag_data = rmc_data["flags"]
 
     # Extract nested flags
     flags = dict()
 
-    def find_flags(map):
-        for key in map:
-            if isinstance(map[key], dict):
-                find_flags(map[key])
+    def find_flags(args):
+        for key in args:
+            if isinstance(args[key], dict):
+                find_flags(args[key])
             else:
-                flags[key] = map[key]
+                flags[key] = args[key]
     find_flags(flag_data)
 
     # Add config toml flags to flag list

src/rmc-compiler/cbmc/src/lib.rs

@@ -24,7 +24,6 @@
 //!
 //! Speical [id]s include:
 //! 1. [Empty] and [Nil] behaves like [null].
-#![feature(rustc_private)]
 
 mod env;
 pub mod goto_program;
@@ -36,7 +35,5 @@ pub use machine_model::{MachineModel, RoundingMode};
 mod cbmc_string;
 pub use cbmc_string::{InternString, InternStringOption, InternedString};
 
-extern crate rustc_data_structures;
-
 // Rust has difficulty resolving types for None option values: this gives rustc a hint.
 pub const NO_PRETTY_NAME: Option<InternedString> = None;

src/rmc-compiler/rustc_codegen_rmc/src/lib.rs

@@ -5,10 +5,8 @@
 #![feature(crate_visibility_modifier)]
 #![feature(extern_types)]
 #![feature(in_band_lifetimes)]
-#![feature(iter_zip)]
 #![feature(nll)]
 #![recursion_limit = "256"]
-#![feature(destructuring_assignment)]
 #![feature(box_patterns)]
 #![feature(once_cell)]
 #![feature(rustc_private)]

src/test/cargo-rmc/config/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "check-config"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[package.metadata.rmc]
+flags={unwind = "5", unwinding-checks = false, function="check_config"}
+

src/test/cargo-rmc/config/src/lib.rs

@@ -0,0 +1,17 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This testcase requires an unwind threshold of less than 10 and no-unwind-checks in order to
+//! succeed. These parameters are set inside Cargo.toml.
+
+#[cfg(rmc)]
+mod rmc_tests {
+    #[rmc::proof]
+    fn check_config() {
+        let mut counter = 0;
+        while rmc::any() {
+            counter += 1;
+            assert!(counter < 10, "Cargo.toml should've configure rmc to stop at iteration 5");
+        }
+    }
+}