diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index d8cb0fc2bb2d..5d4b5b9a4e0d 100644 --- a/.github/workflows/kani.yml +++ b/.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: diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 6cc98a6cace6..9f084da7b962 100644 --- a/kani-compiler/Cargo.toml +++ b/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. diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index eca9b3862b3d..fee2521f4908 100644 --- a/kani-compiler/src/args.rs +++ b/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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 25bc0cbe8ad1..ab6d72d94274 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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>; @@ -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(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool) where T: serde::Serialize, diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 0eb2f0d6c999..a46e71b7c5dc 100644 --- a/kani-driver/src/args/mod.rs +++ b/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( diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index b04c283cb163..edc200277113 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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()); }