33
44//! This module defines all compiler extensions that form the Kani compiler.
55//!
6- //! The [KaniCompiler] can be used across multiple rustc driver runs ([`rustc_driver::run_compiler` ]),
6+ //! The [KaniCompiler] can be used across multiple rustc driver runs ([RunCompiler::run() ]),
77//! which is used to implement stubs.
88//!
99//! In the first run, [KaniCompiler::config] will implement the compiler configuration and it will
@@ -25,7 +25,7 @@ use crate::kani_queries::QueryDb;
2525use crate :: session:: init_session;
2626use clap:: Parser ;
2727use rustc_codegen_ssa:: traits:: CodegenBackend ;
28- use rustc_driver:: { Callbacks , Compilation , run_compiler } ;
28+ use rustc_driver:: { Callbacks , Compilation , RunCompiler } ;
2929use rustc_interface:: Config ;
3030use rustc_middle:: ty:: TyCtxt ;
3131use rustc_session:: config:: ErrorOutputType ;
@@ -34,7 +34,7 @@ use std::sync::{Arc, Mutex};
3434use tracing:: debug;
3535
3636/// Run the Kani flavour of the compiler.
37- /// This may require multiple runs of the rustc driver ([`rustc_driver::run_compiler` ]).
37+ /// This may require multiple runs of the rustc driver ([RunCompiler::run ]).
3838pub fn run ( args : Vec < String > ) {
3939 let mut kani_compiler = KaniCompiler :: new ( ) ;
4040 kani_compiler. run ( args) ;
@@ -96,7 +96,10 @@ impl KaniCompiler {
9696 /// actually invoke the rust compiler multiple times.
9797 pub fn run ( & mut self , args : Vec < String > ) {
9898 debug ! ( ?args, "run_compilation_session" ) ;
99- run_compiler ( & args, self ) ;
99+ let queries = self . queries . clone ( ) ;
100+ let mut compiler = RunCompiler :: new ( & args, self ) ;
101+ compiler. set_make_codegen_backend ( Some ( Box :: new ( move |_cfg| backend ( queries) ) ) ) ;
102+ compiler. run ( ) ;
100103 }
101104}
102105
@@ -105,10 +108,6 @@ impl Callbacks for KaniCompiler {
105108 /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init].
106109 fn config ( & mut self , config : & mut Config ) {
107110 let mut args = vec ! [ "kani-compiler" . to_string( ) ] ;
108- config. make_codegen_backend = Some ( Box :: new ( {
109- let queries = self . queries . clone ( ) ;
110- move |_cfg| backend ( queries)
111- } ) ) ;
112111 args. extend ( config. opts . cg . llvm_args . iter ( ) . cloned ( ) ) ;
113112 let args = Arguments :: parse_from ( args) ;
114113 init_session ( & args, matches ! ( config. opts. error_format, ErrorOutputType :: Json { .. } ) ) ;
0 commit comments