12
12
//!
13
13
//! Note: We don't cross-compile. Target is the same as the host.
14
14
15
- use crate :: { cp, cp_files , AutoRun } ;
16
- use cargo_metadata:: Message ;
15
+ use crate :: { cp, AutoRun } ;
16
+ use cargo_metadata:: { Artifact , Message } ;
17
17
use std:: ffi:: OsStr ;
18
18
use std:: fs;
19
19
use std:: io:: BufReader ;
@@ -31,12 +31,12 @@ macro_rules! path_buf {
31
31
32
32
#[ cfg( target_os = "linux" ) ]
33
33
fn lib_extension ( ) -> & ' static str {
34
- ". so"
34
+ "so"
35
35
}
36
36
37
37
#[ cfg( target_os = "macos" ) ]
38
38
fn lib_extension ( ) -> & ' static str {
39
- ". dylib"
39
+ "dylib"
40
40
}
41
41
42
42
/// Returns the path to Kani sysroot. I.e.: folder where we store pre-compiled binaries and
@@ -111,96 +111,128 @@ pub fn build_lib() {
111
111
. spawn ( )
112
112
. expect ( "Failed to run `cargo build`." ) ;
113
113
114
- // Remove kani "std" library leftover .
115
- filter_kani_std ( & mut cmd) ;
114
+ // Collect the build artifacts .
115
+ let artifacts = build_artifacts ( & mut cmd) ;
116
116
let _ = cmd. wait ( ) . expect ( "Couldn't get cargo's exit status" ) ;
117
117
118
- // Create sysroot folder.
118
+ // Create sysroot folder hierarchy .
119
119
let sysroot_lib = kani_sysroot_lib ( ) ;
120
120
sysroot_lib. exists ( ) . then ( || fs:: remove_dir_all ( & sysroot_lib) ) ;
121
- fs:: create_dir_all ( & sysroot_lib) . expect ( & format ! ( "Failed to create {sysroot_lib:?}" ) ) ;
121
+ let std_path = path_buf ! ( & sysroot_lib, "rustlib" , target, "lib" ) ;
122
+ fs:: create_dir_all ( & std_path) . expect ( & format ! ( "Failed to create {std_path:?}" ) ) ;
122
123
123
- // Copy Kani libraries to inside sysroot folder.
124
- let target_folder = Path :: new ( target_dir ) ;
125
- let macro_lib = format ! ( "libkani_macros{}" , lib_extension ( ) ) ;
126
- let kani_macros = path_buf ! ( target_folder , "debug" , macro_lib ) ;
127
- cp ( & kani_macros , & sysroot_lib ) . unwrap ( ) ;
124
+ // Copy Kani libraries into sysroot top folder.
125
+ copy_libs ( & artifacts , & sysroot_lib , & is_kani_lib ) ;
126
+ // Copy standard libraries into rustlib/<target>/lib/ folder.
127
+ copy_libs ( & artifacts , & std_path , & is_std_lib ) ;
128
+ }
128
129
129
- let kani_rlib_folder = path_buf ! ( target_folder, target, "debug" ) ;
130
- cp_files ( & kani_rlib_folder, & sysroot_lib, & is_rlib) . unwrap ( ) ;
130
+ /// Check if an artifact is a rust library that can be used by rustc on further crates compilations.
131
+ /// This inspects the kind of targets that this artifact originates from.
132
+ fn is_rust_lib ( artifact : & Artifact ) -> bool {
133
+ artifact. target . kind . iter ( ) . any ( |kind| match kind. as_str ( ) {
134
+ "lib" | "rlib" | "proc-macro" => true ,
135
+ "bin" | "dylib" | "cdylib" | "staticlib" | "custom-build" => false ,
136
+ _ => unreachable ! ( "Unknown crate type {kind}" ) ,
137
+ } )
138
+ }
131
139
132
- // Copy `std` libraries and dependencies to sysroot folder following expected path format.
133
- let src_path = path_buf ! ( target_folder, target, "debug" , "deps" ) ;
140
+ /// Return whether this a kani library.
141
+ /// For a given artifact, check if this is a library or proc_macro, and whether this is a local
142
+ /// crate, i.e., that it is part of the Kani repository.
143
+ fn is_kani_lib ( artifact : & Artifact ) -> bool {
144
+ is_rust_lib ( artifact) && artifact. target . src_path . starts_with ( env ! ( "KANI_REPO_ROOT" ) )
145
+ }
134
146
135
- let dst_path = path_buf ! ( sysroot_lib, "rustlib" , target, "lib" ) ;
136
- fs:: create_dir_all ( & dst_path) . unwrap ( ) ;
137
- cp_files ( & src_path, & dst_path, & is_rlib) . unwrap ( ) ;
147
+ /// Is this a std library or one of its dependencies.
148
+ /// For a given artifact, check if this is a library or proc_macro, and whether its source does
149
+ /// not belong to a Kani library.
150
+ fn is_std_lib ( artifact : & Artifact ) -> bool {
151
+ is_rust_lib ( artifact) && !is_kani_lib ( artifact)
138
152
}
139
153
140
- /// Kani's "std" library may cause a name conflict with the rust standard library. We remove it
141
- /// from the `deps/` folder, since we already store it outside of the `deps/` folder.
142
- /// For that, we retrieve its location from `cargo build` output.
143
- fn filter_kani_std ( cargo_cmd : & mut Child ) {
154
+ /// Copy the library files from the artifacts that match the given `predicate`.
155
+ /// This function will iterate over the list of artifacts generated by the compiler, it will
156
+ /// filter the artifacts according to the given predicate. For the artifacts that satisfy the
157
+ /// predicate, it will copy the following files to the `target` folder.
158
+ /// - `rlib`: Store metadata for future codegen and executable code for concrete executions.
159
+ /// - shared library which are used for proc_macros.
160
+ fn copy_libs < P > ( artifacts : & [ Artifact ] , target : & Path , predicate : P )
161
+ where
162
+ P : FnMut ( & Artifact ) -> bool ,
163
+ {
164
+ assert ! ( target. is_dir( ) , "Expected a folder, but found {}" , target. display( ) ) ;
165
+ for artifact in artifacts. iter ( ) . cloned ( ) . filter ( predicate) {
166
+ artifact
167
+ . filenames
168
+ . iter ( )
169
+ . filter ( |path| {
170
+ path. extension ( ) == Some ( "rlib" ) || path. extension ( ) == Some ( lib_extension ( ) )
171
+ } )
172
+ . for_each ( |lib| cp ( lib. clone ( ) . as_std_path ( ) , target) . unwrap ( ) ) ;
173
+ }
174
+ }
175
+
176
+ /// Collect all the artifacts generated by Cargo build.
177
+ /// This will also include libraries that didn't need to be rebuild.
178
+ fn build_artifacts ( cargo_cmd : & mut Child ) -> Vec < Artifact > {
144
179
let reader = BufReader :: new ( cargo_cmd. stdout . take ( ) . unwrap ( ) ) ;
145
- for message in Message :: parse_stream ( reader) {
146
- match message. unwrap ( ) {
147
- Message :: CompilerMessage ( msg) => {
148
- // Print message as cargo would.
149
- println ! ( "{msg:?}" )
150
- }
151
- Message :: CompilerArtifact ( artifact) => {
152
- // Remove the `rlib` and `rmeta` files for our `std` library from the deps folder.
153
- if artifact. target . name == "std"
154
- && artifact. target . src_path . starts_with ( env ! ( "KANI_REPO_ROOT" ) )
155
- {
156
- let rmeta = artifact. filenames . iter ( ) . find ( |p| p. extension ( ) == Some ( "rmeta" ) ) ;
157
- let mut glob = PathBuf :: from ( rmeta. unwrap ( ) ) ;
158
- glob. set_extension ( "*" ) ;
159
- Command :: new ( "rm" ) . arg ( "-f" ) . arg ( glob. as_os_str ( ) ) . run ( ) . unwrap ( ) ;
180
+ Message :: parse_stream ( reader)
181
+ . filter_map ( |message| {
182
+ match message. unwrap ( ) {
183
+ Message :: CompilerMessage ( msg) => {
184
+ // Print message as cargo would.
185
+ println ! ( "{msg:?}" ) ;
186
+ None
160
187
}
188
+ Message :: CompilerArtifact ( artifact) => Some ( artifact) ,
189
+ Message :: BuildScriptExecuted ( _) | Message :: BuildFinished ( _) => {
190
+ // do nothing
191
+ None
192
+ }
193
+ // Non-exhaustive enum.
194
+ _ => None ,
161
195
}
162
- Message :: BuildScriptExecuted ( _script) => {
163
- // do nothing
164
- }
165
- Message :: BuildFinished ( _finished) => {
166
- // do nothing
167
- }
168
- // Non-exhaustive enum.
169
- _ => ( ) ,
170
- }
171
- }
196
+ } )
197
+ . collect ( )
172
198
}
173
199
174
200
/// Build Kani libraries using the regular rust toolchain standard libraries.
175
201
/// We should be able to remove this once the MIR linker is stable.
176
202
pub fn build_lib_legacy ( ) {
177
203
// Run cargo build with -Z build-std
178
204
let target_dir = env ! ( "KANI_LEGACY_LIBS" ) ;
179
- let args =
180
- [ "build" , "-p" , "std" , "-p" , "kani" , "-p" , "kani_macros" , "--target-dir" , target_dir] ;
181
- Command :: new ( "cargo" )
205
+ let args = [
206
+ "build" ,
207
+ "-p" ,
208
+ "std" ,
209
+ "-p" ,
210
+ "kani" ,
211
+ "-p" ,
212
+ "kani_macros" ,
213
+ "--target-dir" ,
214
+ target_dir,
215
+ "--message-format" ,
216
+ "json-diagnostic-rendered-ansi" ,
217
+ ] ;
218
+ let mut child = Command :: new ( "cargo" )
182
219
. env ( "CARGO_ENCODED_RUSTFLAGS" , [ "--cfg=kani" ] . join ( "\x1f " ) )
183
220
. args ( args)
184
- . run ( )
221
+ . stdout ( Stdio :: piped ( ) )
222
+ . spawn ( )
185
223
. expect ( "Failed to build Kani libraries." ) ;
186
224
225
+ // Collect the build artifacts.
226
+ let artifacts = build_artifacts ( & mut child) ;
227
+ let _ = child. wait ( ) . expect ( "Couldn't get cargo's exit status" ) ;
228
+
187
229
// Create sysroot folder.
188
230
let legacy_lib = kani_sysroot_legacy_lib ( ) ;
189
231
legacy_lib. exists ( ) . then ( || fs:: remove_dir_all ( & legacy_lib) ) ;
190
- fs:: create_dir_all ( & legacy_lib) . expect ( & format ! ( "Failed to create {legacy_lib:?}" ) ) ;
191
-
192
- // Copy Kani libraries to inside the lib folder.
193
- let target_folder = Path :: new ( target_dir) ;
194
- let macro_lib = format ! ( "libkani_macros{}" , lib_extension( ) ) ;
195
- let kani_macros = path_buf ! ( target_folder, "debug" , macro_lib) ;
196
- cp ( & kani_macros, & legacy_lib) . unwrap ( ) ;
197
-
198
- let kani_rlib_folder = path_buf ! ( target_folder, "debug" ) ;
199
- cp_files ( & kani_rlib_folder, & legacy_lib, & is_rlib) . unwrap ( ) ;
200
- }
232
+ fs:: create_dir_all ( & legacy_lib) . expect ( & format ! ( "Failed to create {:?}" , legacy_lib) ) ;
201
233
202
- fn is_rlib ( path : & Path ) -> bool {
203
- path . is_file ( ) && String :: from ( path . file_name ( ) . unwrap ( ) . to_string_lossy ( ) ) . ends_with ( ".rlib" )
234
+ // Copy Kani libraries to inside the legacy-lib folder.
235
+ copy_libs ( & artifacts , & legacy_lib , & is_kani_lib ) ;
204
236
}
205
237
206
238
/// Extra arguments to be given to `cargo build` while building Kani's binaries.
0 commit comments