Goto binary serialization

.github/workflows/kani.yml

@@ -33,7 +33,7 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
-  write-goto-binary-regression:
+  write-json-symtab-regression:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
@@ -49,7 +49,7 @@ jobs:
 
       - name: Execute Kani regression
         env:
-          KANI_ENABLE_WRITE_GOTO_BINARY: 1
+          KANI_ENABLE_WRITE_JSON_SYMTAB: 1
         run: ./scripts/kani-regression.sh
 
   experimental-features-regression:

kani-compiler/Cargo.toml

@@ -39,6 +39,7 @@ default = ['cprover']
 cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde',
     'serde_json', "strum", "strum_macros"]
 unsound_experiments = ["kani_queries/unsound_experiments"]
+write_json_symtab = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

kani-compiler/kani_queries/src/lib.rs

@@ -44,8 +44,8 @@ pub trait UserInput {
     fn set_ignore_global_asm(&mut self, global_asm: bool);
     fn get_ignore_global_asm(&self) -> bool;
 
-    fn set_write_goto_binary(&mut self, write_goto_binary: bool);
-    fn get_write_goto_binary(&self) -> bool;
+    fn set_write_json_symtab(&mut self, write_json_symtab: bool);
+    fn get_write_json_symtab(&self) -> bool;
 
     fn set_reachability_analysis(&mut self, reachability: ReachabilityType);
     fn get_reachability_analysis(&self) -> ReachabilityType;
@@ -66,8 +66,7 @@ pub struct QueryDb {
     emit_vtable_restrictions: bool,
     json_pretty_print: bool,
     ignore_global_asm: bool,
-    /// When set, instructs the compiler to produce the symbol table for CBMC in goto binary format instead of JSON format.
-    write_goto_binary: bool,
+    write_json_symtab: bool,
     reachability_analysis: ReachabilityType,
     stubbing_enabled: bool,
     #[cfg(feature = "unsound_experiments")]
@@ -81,7 +80,7 @@ impl QueryDb {
             emit_vtable_restrictions: false,
             json_pretty_print: false,
             ignore_global_asm: false,
-            write_goto_binary: false,
+            write_json_symtab: false,
             reachability_analysis: ReachabilityType::None,
             stubbing_enabled: false,
             #[cfg(feature = "unsound_experiments")]
@@ -139,12 +138,12 @@ impl UserInput for QueryDb {
         self.stubbing_enabled
     }
 
-    fn set_write_goto_binary(&mut self, write_goto_binary: bool) {
-        self.write_goto_binary = write_goto_binary;
+    fn set_write_json_symtab(&mut self, write_json_symtab: bool) {
+        self.write_json_symtab = write_json_symtab;
     }
 
-    fn get_write_goto_binary(&self) -> bool {
-        self.write_goto_binary
+    fn get_write_json_symtab(&self) -> bool {
+        self.write_json_symtab
     }
 
     #[cfg(feature = "unsound_experiments")]

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -183,15 +183,14 @@ impl CodegenBackend for GotocCodegenBackend {
             let base_filename = outputs.output_path(OutputType::Object);
             let pretty = self.queries.lock().unwrap().get_output_pretty_json();
             write_file(&base_filename, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
-
-            if gcx.queries.get_write_goto_binary() {
+            if gcx.queries.get_write_json_symtab() {
+                write_file(&base_filename, ArtifactType::SymTab, &gcx.symbol_table, pretty);
+                symbol_table_to_gotoc(&tcx, &base_filename);
+            } else {
                 write_goto_binary_file(
                     &base_filename.with_extension(ArtifactType::SymTabGoto),
                     &gcx.symbol_table,
                 );
-            } else {
-                write_file(&base_filename, ArtifactType::SymTab, &gcx.symbol_table, pretty);
-                symbol_table_to_gotoc(&tcx, &base_filename);
             }
             write_file(&base_filename, ArtifactType::TypeMap, &type_map, pretty);
             write_file(&base_filename, ArtifactType::Metadata, &metadata, pretty);

kani-compiler/src/kani_compiler.rs

@@ -140,7 +140,11 @@ impl Callbacks for KaniCompiler {
                 .set_check_assertion_reachability(matches.get_flag(parser::ASSERTION_REACH_CHECKS));
             queries.set_output_pretty_json(matches.get_flag(parser::PRETTY_OUTPUT_FILES));
             queries.set_ignore_global_asm(matches.get_flag(parser::IGNORE_GLOBAL_ASM));
-            queries.set_write_goto_binary(matches.get_flag(parser::WRITE_GOTO_BINARY));
+            if cfg!(feature = "write_json_symtab") {
+                queries.set_write_json_symtab(true);
+            } else {
+                queries.set_write_json_symtab(matches.get_flag(parser::WRITE_JSON_SYMTAB));
+            }
             queries.set_reachability_analysis(matches.reachability_type());
 
             #[cfg(feature = "unsound_experiments")]

kani-compiler/src/parser.rs

@@ -34,8 +34,8 @@ pub const PRETTY_OUTPUT_FILES: &str = "pretty-json-files";
 /// Option used for suppressing global ASM error.
 pub const IGNORE_GLOBAL_ASM: &str = "ignore-global-asm";
 
-/// Option used to write GOTO binaries instead of JSON symtabs.
-pub const WRITE_GOTO_BINARY: &str = "write-goto-binary";
+/// Option used to write JSON symbol tables instead of GOTO binaries.
+pub const WRITE_JSON_SYMTAB: &str = "write-json-symtab";
 
 /// Option name used to select which reachability analysis to perform.
 pub const REACHABILITY: &str = "reachability";
@@ -126,9 +126,9 @@ pub fn parser() -> Command {
                 .action(ArgAction::SetTrue),
         )
         .arg(
-            Arg::new(WRITE_GOTO_BINARY)
-                .long(WRITE_GOTO_BINARY)
-                .help("Instruct the compiler to produce GOTO binaries instead of JSON symtabs.")
+            Arg::new(WRITE_JSON_SYMTAB)
+                .long(WRITE_JSON_SYMTAB)
+                .help("Instruct the compiler to produce GotoC symbol tables in JSON format instead of GOTO binary format.")
                 .action(ArgAction::SetTrue),
         )
         .arg(

kani-driver/src/args.rs

@@ -216,9 +216,9 @@ pub struct KaniArgs {
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub ignore_global_asm: bool,
 
-    /// Write the GotoC symbol table to file in goto binary format instead of JSON.
-    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
-    pub write_goto_binary: bool,
+    /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
+    #[arg(long, hide_short_help = true)]
+    pub write_json_symtab: bool,
 
     /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct.
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]

kani-driver/src/call_single_file.rs

@@ -87,16 +87,9 @@ impl KaniSession {
             flags.push("--ignore-global-asm".into());
         }
 
-        // When running regression runs, the write_goto_binary option is enabled
-        // by defining an environment variable.
-        // The value must be non-empty and different from zero.
-        let enable_write_goto_binary = match std::env::var_os("KANI_ENABLE_WRITE_GOTO_BINARY") {
-            Some(str) => !str.is_empty() && str != "0",
-            None => false,
-        };
         // Users activate it via the command line switch
-        if self.args.write_goto_binary || enable_write_goto_binary {
-            flags.push("--write-goto-binary".into());
+        if self.args.write_json_symtab {
+            flags.push("--write-json-symtab".into());
         }
 
         if self.args.enable_stubbing {

scripts/kani-regression.sh

@@ -32,6 +32,8 @@ ${SCRIPT_DIR}/kani-fmt.sh --check
 # Build all packages in the workspace
 if [[ "" != "${KANI_ENABLE_UNSOUND_EXPERIMENTS-}" ]]; then
   cargo build-dev -- --features unsound_experiments
+elif [[ "" != "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
+  cargo build-dev -- --features write_json_symtab
 else
   cargo build-dev
 fi