Move symtab2gb to codegen step (#1686)

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -30,6 +30,7 @@ use std::fmt::Write;
 use std::io::BufWriter;
 use std::iter::FromIterator;
 use std::path::Path;
+use std::process::Command;
 use std::rc::Rc;
 use tracing::{debug, warn};
 
@@ -152,6 +153,7 @@ impl CodegenBackend for GotocCodegenBackend {
             if let Some(restrictions) = vtable_restrictions {
                 write_file(&base_filename, "restrictions.json", &restrictions, pretty);
             }
+            symbol_table_to_gotoc(&tcx, &base_filename);
         }
         codegen_results(tcx, rustc_metadata, symtab.machine_model())
     }
@@ -388,3 +390,27 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
         }
     }
 }
+
+fn symbol_table_to_gotoc(tcx: &TyCtxt, file: &Path) {
+    let output_filename = file.with_extension("symtab.out");
+    let input_filename = file.with_extension("symtab.json");
+
+    let args = vec![
+        input_filename.clone().into_os_string(),
+        "--out".into(),
+        output_filename.into_os_string(),
+    ];
+    // TODO get symtab2gb path from self
+    let mut cmd = Command::new("symtab2gb");
+    cmd.args(args);
+    debug!("calling: `{:?} {:?}`", cmd.get_program(), cmd.get_args());
+
+    if cmd.status().is_err() {
+        let err_msg = format!(
+            "Failed to generate goto model:\n\tsymtab2gb failed on file {}.",
+            input_filename.display()
+        );
+        tcx.sess.err(&err_msg);
+        tcx.sess.abort_if_errors();
+    }
+}

kani-driver/src/main.rs

@@ -16,7 +16,6 @@ mod call_cbmc_viewer;
 mod call_goto_cc;
 mod call_goto_instrument;
 mod call_single_file;
-mod call_symtab;
 mod cbmc_output_parser;
 mod concrete_playback;
 mod harness_runner;
@@ -44,7 +43,8 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
 
     let mut goto_objs: Vec<PathBuf> = Vec::new();
     for symtab in &outputs.symtabs {
-        goto_objs.push(ctx.symbol_table_to_gotoc(symtab)?);
+        let goto_obj_filename = symtab.with_extension("out");
+        goto_objs.push(goto_obj_filename);
     }
 
     if ctx.args.only_codegen {
@@ -81,7 +81,8 @@ fn standalone_main() -> Result<()> {
 
     let outputs = ctx.compile_single_rust_file(&args.input)?;
 
-    let goto_obj = ctx.symbol_table_to_gotoc(&outputs.symtab)?;
+    let goto_obj = outputs.symtab.with_extension("out");
+    ctx.record_temporary_files(&[&goto_obj]);
 
     if ctx.args.only_codegen {
         return Ok(());

tests/cargo-ui/dry-run/expected

@@ -1,6 +1,5 @@
 KANIFLAGS="--goto-c --log-level=warn --assertion-reach-checks --reachability=legacy -C symbol-mangling-version=v0" RUSTC=
 RUSTFLAGS="--kani-flags" cargo rustc
-symtab2gb 
 goto-cc 
 goto-cc
 --function harness

tests/expected/dry-run/expected

@@ -1,5 +1,4 @@
 kani-compiler --goto-c
-symtab2gb
 goto-cc
 --function harness
 goto-instrument