Remove symtab json support (#3695)

I believe the plan was to keep this in case of a regression for about a
year. The time has long gone, so I think it's time to get rid of it.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: celinval

.github/workflows/kani.yml

@@ -31,27 +31,6 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
-  write-json-symtab-regression:
-    runs-on: ubuntu-20.04
-    steps:
-      - name: Checkout Kani
-        uses: actions/checkout@v4
-
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev -- --features write_json_symtab
-
-      - name: Run tests
-        run: |
-          cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast
-          cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast
-          cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast
-
-
   benchcomp-tests:
     runs-on: ubuntu-20.04
     steps:

kani-compiler/Cargo.toml

@@ -34,7 +34,6 @@ tracing-tree = "0.4.0"
 default = ['cprover', 'llbc']
 llbc = ['charon']
 cprover = ['cbmc', 'num', 'serde']
-write_json_symtab = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

kani-compiler/src/args.rs

@@ -51,11 +51,6 @@ pub struct Arguments {
     /// Option used for suppressing global ASM error.
     #[clap(long)]
     pub ignore_global_asm: bool,
-    #[clap(long)]
-    /// Option used to write JSON symbol tables instead of GOTO binaries.
-    ///
-    /// When set, instructs the compiler to produce the symbol table for CBMC in JSON format and use symtab2gb.
-    pub write_json_symtab: bool,
     /// Option name used to select which reachability analysis to perform.
     #[clap(long = "reachability", default_value = "none")]
     pub reachability_analysis: ReachabilityType,

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -46,15 +46,13 @@ use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::{CrateDef, DefId};
 use std::any::Any;
 use std::collections::BTreeMap;
-use std::ffi::OsString;
 use std::fmt::Write;
 use std::fs::File;
 use std::io::BufWriter;
-use std::path::{Path, PathBuf};
-use std::process::Command;
+use std::path::Path;
 use std::sync::{Arc, Mutex};
 use std::time::Instant;
-use tracing::{debug, error, info};
+use tracing::{debug, info};
 
 pub type UnsupportedConstructs = FxHashMap<InternedString, Vec<Location>>;
 
@@ -204,12 +202,7 @@ impl GotocCodegenBackend {
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {
             let pretty = self.queries.lock().unwrap().args().output_pretty_json;
             write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
-            if gcx.queries.args().write_json_symtab {
-                write_file(&symtab_goto, ArtifactType::SymTab, &gcx.symbol_table, pretty);
-                symbol_table_to_gotoc(&tcx, &symtab_goto);
-            } else {
-                write_goto_binary_file(symtab_goto, &gcx.symbol_table);
-            }
+            write_goto_binary_file(symtab_goto, &gcx.symbol_table);
             write_file(&symtab_goto, ArtifactType::TypeMap, &type_map, pretty);
             // If they exist, write out vtable virtual call function pointer restrictions
             if let Some(restrictions) = vtable_restrictions {
@@ -538,40 +531,6 @@ fn codegen_results(
     ))
 }
 
-fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf {
-    let output_filename = base_path.to_path_buf();
-    let input_filename = convert_type(base_path, ArtifactType::SymTabGoto, ArtifactType::SymTab);
-
-    let args = vec![
-        input_filename.clone().into_os_string(),
-        "--out".into(),
-        OsString::from(output_filename.as_os_str()),
-    ];
-    // TODO get symtab2gb path from self
-    let mut cmd = Command::new("symtab2gb");
-    cmd.args(args);
-    info!("[Kani] Running: `{:?} {:?}`", cmd.get_program(), cmd.get_args());
-
-    let result = with_timer(
-        || {
-            cmd.output()
-                .expect(&format!("Failed to generate goto model for {}", input_filename.display()))
-        },
-        "symtab2gb",
-    );
-    if !result.status.success() {
-        error!("Symtab error output:\n{}", String::from_utf8_lossy(&result.stderr));
-        error!("Symtab output:\n{}", String::from_utf8_lossy(&result.stdout));
-        let err_msg = format!(
-            "Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
-            input_filename.display()
-        );
-        tcx.dcx().err(err_msg);
-        tcx.dcx().abort_if_errors();
-    };
-    output_filename
-}
-
 pub fn write_file<T>(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool)
 where
     T: serde::Serialize,

kani-driver/src/args/mod.rs

@@ -573,6 +573,10 @@ impl ValidateArgs for VerificationArgs {
             );
         }
 
+        if self.write_json_symtab {
+            print_obsolete(&self.common_args, "--write-json-symtab");
+        }
+
         if self.visualize {
             if !self.common_args.enable_unstable {
                 return Err(Error::raw(

kani-driver/src/call_single_file.rs

@@ -129,11 +129,6 @@ impl KaniSession {
             flags.push("--ignore-global-asm".into());
         }
 
-        // Users activate it via the command line switch
-        if self.args.write_json_symtab {
-            flags.push("--write-json-symtab".into());
-        }
-
         if self.args.is_stubbing_enabled() {
             flags.push("--enable-stubbing".into());
         }