Add a rustfmt syntactic check for the Rust project

.github/workflows/syntax-checks.yaml

@@ -47,3 +47,18 @@ jobs:
           BASE_BRANCH: ${{ github.base_ref }}
           MERGE_BRANCH: ${{ github.ref }}
         run: ./.github/workflows/pull-request-check-cpplint.sh
+
+  # This job should take about a minute (est)
+  check-rustfmt:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout CBMC repository 
+        uses: actions/checkout@v3
+      - name: Install latest stable Rust toolchain
+        uses: actions-rs/toolchain@v1
+        with:
+            toolchain: stable
+            override: true
+            components: rustfmt, clippy
+      - name: Run `cargo fmt` on top of Rust API project
+        run: cd src/libcprover-rust; cargo fmt --all -- --check

src/libcprover-rust/build.rs

@@ -20,7 +20,10 @@ fn get_library_build_dir() -> std::io::Result<PathBuf> {
         path.push("lib/");
         return Ok(path);
     }
-    Err(Error::new(ErrorKind::Other, "failed to get build output directory"))
+    Err(Error::new(
+        ErrorKind::Other,
+        "failed to get build output directory",
+    ))
 }
 
 fn get_cadical_build_dir() -> std::io::Result<PathBuf> {
@@ -31,7 +34,10 @@ fn get_cadical_build_dir() -> std::io::Result<PathBuf> {
         path.push("cadical-src/build/");
         return Ok(path);
     }
-    Err(Error::new(ErrorKind::Other, "failed to get build output directory"))
+    Err(Error::new(
+        ErrorKind::Other,
+        "failed to get build output directory",
+    ))
 }
 
 fn get_sat_library() -> std::io::Result<&'static str> {
@@ -40,13 +46,19 @@ fn get_sat_library() -> std::io::Result<&'static str> {
     if let Ok(sat_impl) = env_var_fetch_result {
         let solver_lib = match sat_impl.as_str() {
             "minisat2" => Ok("minisat2-condensed"),
-            "glucose"  => Ok("glucose-condensed"),
-            "cadical"  => Ok("cadical"),
-            _          => Err(Error::new(ErrorKind::Other, "no identifiable solver detected"))
+            "glucose" => Ok("glucose-condensed"),
+            "cadical" => Ok("cadical"),
+            _ => Err(Error::new(
+                ErrorKind::Other,
+                "no identifiable solver detected",
+            )),
         };
         return solver_lib;
     }
-    Err(Error::new(ErrorKind::Other, "SAT_IMPL environment variable not set"))
+    Err(Error::new(
+        ErrorKind::Other,
+        "SAT_IMPL environment variable not set",
+    ))
 }
 
 fn main() {
@@ -65,12 +77,12 @@ fn main() {
 
     let libraries_path = match get_library_build_dir() {
         Ok(path) => path,
-        Err(err) => panic!("Error: {}", err)
+        Err(err) => panic!("Error: {}", err),
     };
 
     let solver_lib = match get_sat_library() {
         Ok(solver) => solver,
-        Err(err) => panic!("Error: {}", err)
+        Err(err) => panic!("Error: {}", err),
     };
 
     // Cadical is being built in its own directory, with the resultant artefacts being
@@ -79,12 +91,18 @@ fn main() {
     if solver_lib == "cadical" {
         let cadical_build_dir = match get_cadical_build_dir() {
             Ok(cadical_directory) => cadical_directory,
-            Err(err) => panic!("Error: {}", err)
+            Err(err) => panic!("Error: {}", err),
         };
-        println!("cargo:rustc-link-search=native={}", cadical_build_dir.display());
+        println!(
+            "cargo:rustc-link-search=native={}",
+            cadical_build_dir.display()
+        );
     }
 
-    println!("cargo:rustc-link-search=native={}", libraries_path.display());
+    println!(
+        "cargo:rustc-link-search=native={}",
+        libraries_path.display()
+    );
     println!("cargo:rustc-link-lib=static=goto-programs");
     println!("cargo:rustc-link-lib=static=util");
     println!("cargo:rustc-link-lib=static=langapi");

src/libcprover-rust/src/lib.rs

@@ -1,4 +1,4 @@
-use cxx::{CxxVector, CxxString};
+use cxx::{CxxString, CxxVector};
 #[cxx::bridge]
 pub mod ffi {
 
@@ -31,7 +31,7 @@ fn print_response(vec: &CxxVector<CxxString>) {
         .iter()
         .map(|s| s.to_string_lossy().into_owned())
         .collect();
-    
+
     for s in vec {
         println!("{}", s);
     }
@@ -54,24 +54,21 @@ mod tests {
 
     #[test]
     fn translate_vector_of_rust_string_to_cpp() {
-        let vec: Vec<String> = vec![
-            "other/example.c".to_owned(),
-            "/tmp/example2.c".to_owned()];
+        let vec: Vec<String> = vec!["other/example.c".to_owned(), "/tmp/example2.c".to_owned()];
 
         let vect = ffi::translate_vector_of_string(vec);
         assert_eq!(vect.len(), 2);
     }
-    
+
     #[test]
     fn it_can_load_model_from_file() {
         let binding = ffi::new_api_session();
         let client = match binding.as_ref() {
             Some(api_ref) => api_ref,
             None => panic!("Failed to acquire API session handle"),
         };
-
-        let vec: Vec<String> = vec![
-            "other/example.c".to_owned()];
+
+        let vec: Vec<String> = vec!["other/example.c".to_owned()];
 
         let vect = ffi::translate_vector_of_string(vec);
         assert_eq!(vect.len(), 1);
@@ -87,11 +84,10 @@ mod tests {
     }
 
     #[test]
-    fn it_can_verify_the_loaded_model() {        
+    fn it_can_verify_the_loaded_model() {
         let client = ffi::new_api_session();
-
-        let vec: Vec<String> = vec![
-            "other/example.c".to_owned()];
+
+        let vec: Vec<String> = vec!["other/example.c".to_owned()];
 
         let vect = ffi::translate_vector_of_string(vec);
         client.load_model_from_files(vect);
@@ -112,9 +108,8 @@ mod tests {
             Some(api_ref) => api_ref,
             None => panic!("Failed to acquire API session handle"),
         };
-
-        let vec: Vec<String> = vec![
-            "other/example.c".to_owned()];
+
+        let vec: Vec<String> = vec!["other/example.c".to_owned()];
 
         let vect = ffi::translate_vector_of_string(vec);
         assert_eq!(vect.len(), 1);