Demangle symbol names in GotoC (-> .demangled.c) (rust-lang#1303)

kani-driver/src/call_goto_instrument.rs

@@ -3,6 +3,8 @@
 
 use anyhow::Result;
 use std::ffi::OsString;
+use std::fs::File;
+use std::io::BufReader;
 use std::path::Path;
 use std::process::Command;
 
@@ -12,7 +14,13 @@ use crate::util::alter_extension;
 
 impl KaniSession {
     /// Postprocess a goto binary (before cbmc, after linking) in-place by calling goto-instrument
-    pub fn run_goto_instrument(&self, input: &Path, output: &Path, function: &str) -> Result<()> {
+    pub fn run_goto_instrument(
+        &self,
+        input: &Path,
+        output: &Path,
+        symtabs: &[impl AsRef<Path>],
+        function: &str,
+    ) -> Result<()> {
         // We actually start by calling goto-cc to start the specialization:
         self.specialize_to_proof_harness(input, output, function)?;
 
@@ -26,13 +34,20 @@ impl KaniSession {
         self.rewrite_back_edges(output)?;
 
         if self.args.gen_c {
+            let c_outfile = alter_extension(output, "c");
+            // We don't put the C file into temporaries to be deleted.
+
+            self.gen_c(output, &c_outfile)?;
+
+            if !self.args.quiet {
+                println!("Generated C code written to {}", c_outfile.to_string_lossy());
+            }
+
+            let c_demangled = alter_extension(output, "demangled.c");
+            self.demangle_c(symtabs, &c_outfile, &c_demangled)?;
             if !self.args.quiet {
-                println!(
-                    "Generated C code written to {}",
-                    alter_extension(output, "c").to_string_lossy()
-                );
+                println!("Demangled GotoC code written to {}", c_demangled.to_string_lossy())
             }
-            self.gen_c(output)?;
         }
 
         Ok(())
@@ -116,19 +131,47 @@ impl KaniSession {
     }
 
     /// Generate a .c file from a goto binary (i.e. --gen-c)
-    pub fn gen_c(&self, file: &Path) -> Result<()> {
-        let output_filename = alter_extension(file, "c");
-        // We don't put the C file into temporaries to be deleted.
-
+    pub fn gen_c(&self, file: &Path, output_file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--dump-c".into(),
             file.to_owned().into_os_string(),
-            output_filename.into_os_string(),
+            output_file.to_owned().into_os_string(),
         ];
 
         self.call_goto_instrument(args)
     }
 
+    /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol tables
+    ///
+    /// Currently, only top-level function names and (most) type names are demangled.
+    /// For local variables, it would be more complicated than a simple search and replace to obtain the demangled name.
+    pub fn demangle_c(
+        &self,
+        symtab_files: &[impl AsRef<Path>],
+        c_file: &Path,
+        demangled_file: &Path,
+    ) -> Result<()> {
+        let mut c_code = std::fs::read_to_string(c_file)?;
+        for symtab_file in symtab_files {
+            let reader = BufReader::new(File::open(symtab_file.as_ref())?);
+            let symtab: serde_json::Value = serde_json::from_reader(reader)?;
+            for (_, symbol) in symtab["symbolTable"].as_object().unwrap() {
+                if let Some(serde_json::Value::String(name)) = symbol.get("name") {
+                    if let Some(serde_json::Value::String(pretty)) = symbol.get("prettyName") {
+                        // Struct names start with "tag-", but this prefix is not used in the GotoC files, so we strip it.
+                        // If there is no such prefix, we leave the name unchanged.
+                        let name = name.strip_prefix("tag-").unwrap_or(name);
+                        if !pretty.is_empty() && pretty != name {
+                            c_code = c_code.replace(name, pretty);
+                        }
+                    }
+                }
+            }
+        }
+        std::fs::write(demangled_file, c_code)?;
+        Ok(())
+    }
+
     /// Non-public helper function to actually do the run of goto-instrument
     fn call_goto_instrument(&self, args: Vec<OsString>) -> Result<()> {
         // TODO get goto-instrument path from self

kani-driver/src/main.rs

@@ -63,7 +63,12 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         let harness_filename = harness.pretty_name.replace("::", "-");
         let report_dir = report_base.join(format!("report-{}", harness_filename));
         let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", harness_filename));
-        ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?;
+        ctx.run_goto_instrument(
+            &linked_obj,
+            &specialized_obj,
+            &outputs.symtabs,
+            &harness.mangled_name,
+        )?;
 
         let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?;
         if result == VerificationStatus::Failure {
@@ -109,7 +114,12 @@ fn standalone_main() -> Result<()> {
             let mut temps = ctx.temporaries.borrow_mut();
             temps.push(specialized_obj.to_owned());
         }
-        ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?;
+        ctx.run_goto_instrument(
+            &linked_obj,
+            &specialized_obj,
+            &[&outputs.symtab],
+            &harness.mangled_name,
+        )?;
 
         let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?;
         if result == VerificationStatus::Failure {

scripts/kani-regression.sh

@@ -36,6 +36,10 @@ cargo test -p cprover_bindings
 cargo test -p kani-compiler
 cargo test -p kani-driver
 
+# Check output files (--gen-c option)
+echo "Check GotoC output file generation"
+time "$KANI_DIR"/tests/output-files/check-output.sh
+
 # Declare testing suite information (suite and mode)
 TESTS=(
     "kani kani"

tests/output-files/.gitignore

@@ -0,0 +1,4 @@
+target/
+Cargo.lock
+*.c
+build/

tests/output-files/check-output.sh

@@ -0,0 +1,81 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+echo
+echo "Starting output file check..."
+echo
+
+# Test for platform
+PLATFORM=$(uname -sp)
+if [[ $PLATFORM == "Linux x86_64" ]]
+then
+  TARGET="x86_64-unknown-linux-gnu"
+elif [[ $PLATFORM == "Darwin i386" ]]
+then
+  TARGET="x86_64-apple-darwin"
+elif [[ $PLATFORM == "Darwin arm" ]]
+then
+  TARGET="aarch64-apple-darwin"
+else
+  echo
+  echo "Test only works on Linux or OSX platforms, skipping..."
+  echo
+  exit 0
+fi
+
+cd $(dirname $0)
+
+echo "Running single-file check..."
+rm -rf *.c
+RUST_BACKTRACE=1 kani --gen-c --enable-unstable singlefile.rs --quiet
+if ! [ -e singlefile.out.c ]
+then
+    echo "Error: no GotoC file generated. Expected: singlefile.out.c"
+    exit 1
+fi
+
+if ! [ -e singlefile.out.demangled.c ]
+then
+    echo "Error: no demangled GotoC file generated. Expected singlefile.out.demangled.c."
+    exit 1
+fi
+
+if ! grep -Fq "struct PrettyStruct pretty_function(struct PrettyStruct" singlefile.out.demangled.c;
+then
+    echo "Error: demangled file singlefile.out.demangled.c did not contain expected demangled struct and function name."
+    exit 1
+fi
+echo "Finished single-file check successfully..."
+echo
+
+(cd multifile
+echo "Running multi-file check..."
+rm -rf build
+RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable --quiet
+cd build/${TARGET}/debug/deps/
+
+if ! [ -e cbmc-for-main.c ]
+then
+    echo "Error: no GotoC file generated. Expected: build/${TARGET}/debug/deps/cbmc-for-main.c"
+    exit 1
+fi
+
+if ! [ -e cbmc-for-main.demangled.c ]
+then
+    echo "Error: no demangled GotoC file generated. Expected build/${TARGET}/debug/deps/cbmc-for-main.demangled.c."
+    exit 1
+fi
+
+if ! grep -Fq "struct PrettyStruct pretty_function(struct PrettyStruct" cbmc-for-main.demangled.c;
+then
+    echo "Error: demangled file build/${TARGET}/debug/deps/cbmc-for-main.demangled.c did not contain expected demangled struct and function name."
+    exit 1
+fi
+echo "Finished multi-file check successfully..."
+)
+
+echo "Finished output file check successfully."
+echo

tests/output-files/multifile/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "multifile"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]

tests/output-files/multifile/src/main.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub struct PrettyStruct;
+
+#[kani::proof]
+fn main() {
+    pretty_function(PrettyStruct);
+}
+
+pub fn pretty_function(argument: PrettyStruct) -> PrettyStruct {
+    argument
+}

tests/output-files/singlefile.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub struct PrettyStruct;
+
+#[kani::proof]
+pub fn main() {
+    pretty_function(PrettyStruct);
+}
+
+pub fn pretty_function(argument: PrettyStruct) -> PrettyStruct {
+    argument
+}