@@ -19,7 +19,7 @@ mod setup;
19
19
use std:: env;
20
20
use std:: ffi:: OsString ;
21
21
use std:: os:: unix:: prelude:: CommandExt ;
22
- use std:: path:: PathBuf ;
22
+ use std:: path:: { Path , PathBuf } ;
23
23
use std:: process:: Command ;
24
24
25
25
use anyhow:: { bail, Context , Result } ;
@@ -77,12 +77,16 @@ fn exec(bin: &str) -> Result<()> {
77
77
let pyroot = kani_dir. join ( "pyroot" ) ;
78
78
let bin_kani = kani_dir. join ( "bin" ) ;
79
79
let bin_pyroot = pyroot. join ( "bin" ) ;
80
- let bin_toolchain = kani_dir. join ( "toolchain" ) . join ( "bin" ) ;
81
80
82
81
// Allow python scripts to find dependencies under our pyroot
83
82
let pythonpath = prepend_search_path ( & [ pyroot] , env:: var_os ( "PYTHONPATH" ) ) ?;
84
83
// Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH
85
- let path = prepend_search_path ( & [ bin_kani, bin_pyroot, bin_toolchain] , env:: var_os ( "PATH" ) ) ?;
84
+ let path = prepend_search_path ( & [ bin_kani, bin_pyroot] , env:: var_os ( "PATH" ) ) ?;
85
+
86
+ // Ensure our environment variables for linker search paths won't cause failures, before we execute:
87
+ fixup_dynamic_linking_environment ( ) ;
88
+ // Override our `RUSTUP_TOOLCHAIN` with the version Kani links against
89
+ set_kani_rust_toolchain ( & kani_dir) ?;
86
90
87
91
let mut cmd = Command :: new ( program) ;
88
92
cmd. args ( env:: args_os ( ) . skip ( 1 ) ) . env ( "PYTHONPATH" , pythonpath) . env ( "PATH" , path) . arg0 ( bin) ;
@@ -103,3 +107,82 @@ fn prepend_search_path(paths: &[PathBuf], original: Option<OsString>) -> Result<
103
107
}
104
108
}
105
109
}
110
+
111
+ /// `rustup` sets dynamic linker paths when it proxies to the target Rust toolchain. It's not fully
112
+ /// clear why. `rustup run` exists, which may aid in running Rust binaries that dynamically link to
113
+ /// the Rust standard library with `-C prefer-dynamic`. This might be why. All toolchain binaries
114
+ /// have `RUNPATH` set, so it's not needed by e.g. rustc. (Same for Kani)
115
+ ///
116
+ /// However, this causes problems for us when the default Rust toolchain is nightly. Then
117
+ /// `LD_LIBRARY_PATH` is set to a nightly `lib` that may contain a different version of
118
+ /// `librustc_driver-*.so` that might have the same name. This takes priority over the `RUNPATH` of
119
+ /// `kani-compiler` and causes the linker to use a slightly different version of rustc than Kani
120
+ /// was built against. This manifests in errors like:
121
+ /// `kani-compiler: symbol lookup error: ... undefined symbol`
122
+ ///
123
+ /// Consequently, let's remove from our linking environment anything that looks like a toolchain
124
+ /// path that rustup set. Then we can safely invoke our binaries. Note also that we update
125
+ /// `PATH` in [`exec`] to include our favored Rust toolchain, so we won't re-drive `rustup` when
126
+ /// `kani-driver` later invokes `cargo`.
127
+ fn fixup_dynamic_linking_environment ( ) {
128
+ #[ cfg( not( target_os = "macos" ) ) ]
129
+ const LOADER_PATH : & str = "LD_LIBRARY_PATH" ;
130
+ #[ cfg( target_os = "macos" ) ]
131
+ const LOADER_PATH : & str = "DYLD_FALLBACK_LIBRARY_PATH" ;
132
+
133
+ if let Some ( paths) = env:: var_os ( LOADER_PATH ) {
134
+ // unwrap safety: we're just filtering, so it should always succeed
135
+ let new_val =
136
+ env:: join_paths ( env:: split_paths ( & paths) . filter ( unlike_toolchain_path) ) . unwrap ( ) ;
137
+ env:: set_var ( LOADER_PATH , new_val) ;
138
+ }
139
+ }
140
+
141
+ /// Determines if a path looks unlike a toolchain library path. These often looks like:
142
+ /// `/home/user/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib`
143
+ // Ignore this lint (recommending Path instead of PathBuf),
144
+ // we want to take the right argument type for use in `filter` above.
145
+ #[ allow( clippy:: ptr_arg) ]
146
+ fn unlike_toolchain_path ( path : & PathBuf ) -> bool {
147
+ let mut components = path. iter ( ) . rev ( ) ;
148
+
149
+ // effectively matching `*/toolchains/*/lib`
150
+ !( components. next ( ) == Some ( std:: ffi:: OsStr :: new ( "lib" ) )
151
+ && components. next ( ) . is_some ( )
152
+ && components. next ( ) == Some ( std:: ffi:: OsStr :: new ( "toolchains" ) ) )
153
+ }
154
+
155
+ /// We should currently see a `RUSTUP_TOOLCHAIN` that was set by whatever default
156
+ /// toolchain the user has. We override our own environment variable (that is passed
157
+ /// down to children) with the toolchain Kani uses instead.
158
+ fn set_kani_rust_toolchain ( kani_dir : & Path ) -> Result < ( ) > {
159
+ let toolchain_verison = setup:: get_rust_toolchain_version ( kani_dir) ?;
160
+ env:: set_var ( "RUSTUP_TOOLCHAIN" , toolchain_verison) ;
161
+ Ok ( ( ) )
162
+ }
163
+
164
+ #[ cfg( test) ]
165
+ mod tests {
166
+ use super :: * ;
167
+
168
+ #[ test]
169
+ fn check_unlike_toolchain_path ( ) {
170
+ fn trial ( s : & str ) -> bool {
171
+ unlike_toolchain_path ( & PathBuf :: from ( s) )
172
+ }
173
+ // filter these out:
174
+ assert ! ( !trial( "/home/user/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib" ) ) ;
175
+ assert ! ( !trial( "/home/user/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/" ) ) ;
176
+ assert ! ( !trial( "/home/user/.rustup/toolchains/nightly/lib" ) ) ;
177
+ assert ! ( !trial( "/home/user/.rustup/toolchains/stable/lib" ) ) ;
178
+ // minimally:
179
+ assert ! ( !trial( "toolchains/nightly/lib" ) ) ;
180
+ // keep these:
181
+ assert ! ( trial( "/home/user/.rustup/toolchains" ) ) ;
182
+ assert ! ( trial( "/usr/lib" ) ) ;
183
+ assert ! ( trial( "/home/user/lib/toolchains" ) ) ;
184
+ // don't error on these:
185
+ assert ! ( trial( "" ) ) ;
186
+ assert ! ( trial( "/" ) ) ;
187
+ }
188
+ }
0 commit comments