1
+ use clap:: arg_enum;
1
2
use glob:: glob;
2
3
use haybale:: backend:: * ;
3
4
use haybale:: * ;
5
+ use simple_logger:: SimpleLogger ;
6
+ use std:: collections:: HashMap ;
4
7
use std:: fs:: File ;
5
8
use std:: io:: prelude:: * ;
6
9
use std:: result:: Result ;
7
10
use std:: string:: String ;
11
+ use std:: sync:: { Arc , Mutex } ;
8
12
use std:: thread;
13
+ use structopt:: StructOpt ;
9
14
10
15
extern crate log;
11
- extern crate simple_logger;
12
16
13
17
/// Print all LLVM IR instructions in a given symbolic execution
14
18
pub fn print_instrs < ' p > ( path : & Vec < PathEntry < ' p > > ) -> String {
@@ -89,12 +93,16 @@ pub fn find_longest_path<'p>(
89
93
} )
90
94
}
91
95
92
- enum KernelWorkType {
93
- InterruptHandlers ,
94
- CommandSyscalls ,
95
- SubscribeSyscalls ,
96
- AllowSyscalls ,
97
- MemopSyscall ,
96
+ arg_enum ! {
97
+ #[ derive( Debug ) ]
98
+ enum KernelWorkType {
99
+ Interrupts ,
100
+ Commands ,
101
+ Subscribes ,
102
+ Allows ,
103
+ Memops ,
104
+ All ,
105
+ }
98
106
}
99
107
100
108
/// Function for retrieving the types of Tock functions which this tool is capable of profiling,
@@ -108,24 +116,46 @@ fn retrieve_functions_for_analysis<'p>(
108
116
//let demangled = rustc_demangle::demangle(func_name);
109
117
match kind {
110
118
// TODO: Allow handle_xx_interrupt pattern as well
111
- KernelWorkType :: InterruptHandlers => Box :: new (
119
+ KernelWorkType :: Interrupts => Box :: new (
112
120
project
113
121
. all_functions ( )
114
122
. filter ( |( f, _m) | f. name . contains ( "handle_interrupt" ) ) ,
115
123
) ,
116
- KernelWorkType :: CommandSyscalls => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
124
+ KernelWorkType :: Commands => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
117
125
f. name . contains ( "command" )
118
126
&& f. name . contains ( "Driver" )
119
- && !f. name . contains ( "closure" )
120
- && !f. name . contains ( "command_complete" )
127
+ && !f. name . contains ( "closure" ) //manual exclusion
128
+ && !f. name . contains ( "command_complete" ) //manual exclusion
121
129
} ) ) ,
122
- KernelWorkType :: AllowSyscalls => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
130
+ KernelWorkType :: Allows => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
123
131
f. name . contains ( "allow" ) && f. name . contains ( "Driver" ) && !f. name . contains ( "closure" )
124
132
} ) ) ,
125
- KernelWorkType :: SubscribeSyscalls => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
133
+ KernelWorkType :: Subscribes => Box :: new ( project. all_functions ( ) . filter ( |( f, _m) | {
126
134
f. name . contains ( "subscribe" ) && f. name . contains ( "Driver" ) && !f. name . contains ( "closure" )
127
135
} ) ) ,
128
- KernelWorkType :: MemopSyscall => panic ! ( "Memop support not yet implemented" ) ,
136
+ KernelWorkType :: Memops => panic ! ( "Memop support not yet implemented" ) ,
137
+ KernelWorkType :: All => {
138
+ let command_syscalls =
139
+ retrieve_functions_for_analysis ( & project, KernelWorkType :: Commands ) ;
140
+
141
+ let subscribe_syscalls =
142
+ retrieve_functions_for_analysis ( & project, KernelWorkType :: Subscribes ) ;
143
+ let allow_syscalls = retrieve_functions_for_analysis ( & project, KernelWorkType :: Allows ) ;
144
+
145
+ let interrupt_handlers =
146
+ retrieve_functions_for_analysis ( & project, KernelWorkType :: Interrupts ) ;
147
+ Box :: new (
148
+ command_syscalls
149
+ . chain ( subscribe_syscalls)
150
+ . chain ( allow_syscalls)
151
+ . chain ( interrupt_handlers) ,
152
+ )
153
+
154
+ //functions_to_analyze.extend(allow_syscalls.map(|(f, _m)| &f.name));
155
+ //functions_to_analyze.extend(command_syscalls.map(|(f, _m)| &f.name));
156
+ //functions_to_analyze.extend(subscribe_syscalls.map(|(f, _m)| &f.name));
157
+ //functions_to_analyze.extend(interrupt_handlers.map(|(f, _m)| &f.name));
158
+ }
129
159
}
130
160
}
131
161
@@ -137,26 +167,28 @@ fn analyze_and_save_results(
137
167
bc_dir : & str ,
138
168
board_path_str : & str ,
139
169
func_name : & str ,
140
- ) -> Result < ( ) , String > {
141
- let glob2 = "/**/*.bc" ;
142
- let paths = glob ( & [ bc_dir, glob2] . concat ( ) ) . unwrap ( ) . map ( |x| x. unwrap ( ) ) ;
170
+ timeout_s : u64 ,
171
+ ) -> Result < String , String > {
172
+ let paths = glob ( & [ bc_dir, "/**/*.bc" ] . concat ( ) )
173
+ . unwrap ( )
174
+ . map ( |x| x. unwrap ( ) ) ;
143
175
let project = Project :: from_bc_paths ( paths) ?;
144
176
145
177
let mut config: Config < DefaultBackend > = Config :: default ( ) ;
146
178
config. null_pointer_checking = config:: NullPointerChecking :: None ; // In the Tock kernel, we trust that Rust safety mechanisms prevent null pointer dereferences.
147
179
config. loop_bound = 50 ; // default is 10, raise if larger loops exist
148
- config. solver_query_timeout = Some ( std:: time:: Duration :: new ( 100 , 0 ) ) ; // extend query timeout
180
+ config. solver_query_timeout = Some ( std:: time:: Duration :: new ( timeout_s , 0 ) ) ; // extend query timeout
149
181
config
150
182
. function_hooks
151
183
. add_rust_demangled ( "kernel::debug::panic" , & function_hooks:: abort_hook) ;
152
184
let board_name = board_path_str
153
185
. get ( board_path_str. rfind ( '/' ) . unwrap ( ) + 1 ..)
154
186
. unwrap ( ) ;
155
187
let demangled = rustc_demangle:: demangle ( func_name) . to_string ( ) ;
156
- let filename = "results_ " . to_owned ( ) + board_name + "_ " + & demangled + ".txt" ;
188
+ let filename = "results/ " . to_owned ( ) + board_name + "/ " + & demangled + ".txt" ;
157
189
println ! ( "{:?}" , filename) ;
158
190
let mut file = File :: create ( filename) . unwrap ( ) ;
159
- match find_longest_path ( func_name, & project, config) {
191
+ let ret = match find_longest_path ( func_name, & project, config) {
160
192
Ok ( ( len, state) ) => {
161
193
println ! ( "len: {}" , len) ;
162
194
let data = "len: " . to_owned ( )
@@ -170,109 +202,135 @@ fn analyze_and_save_results(
170
202
file. write_all ( data. as_bytes ( ) ) . unwrap ( ) ;
171
203
//println!("{}", state.pretty_path_source());
172
204
//print_instrs(state.get_path());
205
+ Ok ( len. to_string ( ) )
173
206
}
174
207
Err ( e) => {
175
208
file. write_all ( e. as_bytes ( ) ) . unwrap ( ) ;
209
+ Err ( "Fail" . to_string ( ) )
176
210
}
177
- }
178
- Ok ( ( ) )
211
+ } ;
212
+ ret
179
213
}
180
214
181
- fn main ( ) -> Result < ( ) , String > {
182
- // comment in to enable logs in Haybale. Useful for debugging
183
- // but dramatically slow down executions and increase memory use.
184
- // generally, should be first line of main if included.
185
- //simple_logger::init().unwrap();
186
-
187
- // set to board to be evaluated. Currently, not all tock boards are supported.
188
- // TODO: Fix below to not use rust version of haybale crate (may need build.rs)
189
- let board_path_str = "tock/boards/apollo32" ;
190
- /*use std::process::Command;
191
- let output1 = Command::new("sh")
192
- .arg("-c")
193
- .arg(
194
- "exec bash -l cd ".to_owned()
195
- + &board_path_str
196
- + &" && source ~/.bashrc && make clean && make",
197
- )
198
- .output()
199
- .expect("failed to execute process");
200
- println!("{}", String::from_utf8(output1.stderr).unwrap());
215
+ #[ derive( StructOpt , Debug ) ]
216
+ #[ structopt( name = "basic" ) ]
217
+ struct Opt {
218
+ /// Activate debug mode
219
+ #[ structopt( short, long) ]
220
+ debug : bool ,
201
221
202
- let output2 = Command::new("make")
203
- .arg("-C")
204
- .arg(&board_path_str)
205
- .output()
206
- .expect("failed to execute process");
207
- println!("{}", String::from_utf8(output2.stderr).unwrap());
208
- */
222
+ /// Verbose mode (-v, -vv, -vvv, etc.)
223
+ #[ structopt( short, long, parse( from_occurrences) ) ]
224
+ verbose : u8 ,
209
225
210
- // For now, assume target under analysis,
211
- // located in the tock submodule of this crate
212
- let bc_dir = "tock/target/thumbv7em-none-eabi/release/deps/" ;
213
- //let bc_dir = "tock/target/riscv32imc-unknown-none-elf/release/deps/";
226
+ /// Timeout passed to Haybale runs (in seconds)
227
+ #[ structopt( short, long, default_value = "100" ) ]
228
+ timeout : u64 ,
214
229
215
- // Make a vector to hold the children which are spawned.
216
- let mut functions_to_analyze = vec ! [ ] ;
230
+ /// Name of the tock board to analyze
231
+ #[ structopt( short, long, default_value = "redboard_artemis_nano" ) ]
232
+ board : String ,
217
233
218
- //begin list of all interrupts for apollo3 board/chip:
234
+ /// Types of function for which to find longest path
235
+ #[ structopt( possible_values = & KernelWorkType :: variants( ) , case_insensitive = true , default_value = "all" ) ]
236
+ functions : KernelWorkType ,
237
+ }
219
238
220
- //let func_name = "apollo3::stimer::STimer::handle_interrupt";
221
- //let func_name = "apollo3::iom::Iom::handle_interrupt";
222
- //let func_name = "apollo3::uart::Uart::handle_interrupt";
223
- //let func_name = "apollo3::ble::Ble::handle_interrupt";
224
- //let func_name = "apollo3::gpio::Port::handle_interrupt";
239
+ fn main ( ) -> Result < ( ) , String > {
240
+ let opt = Opt :: from_args ( ) ; // get CLI inputs
225
241
226
- let glob2 = "/**/*.bc" ;
227
- let paths = glob ( & [ bc_dir, glob2] . concat ( ) ) . unwrap ( ) . map ( |x| x. unwrap ( ) ) ;
228
- let project = Project :: from_bc_paths ( paths) ?;
242
+ if opt. verbose >= 1 {
243
+ // Enable logs in Haybale. Useful for debugging
244
+ // but dramatically slow down executions and increase memory use.
245
+ // generally, should be first line of main if included.
246
+ SimpleLogger :: new ( ) . init ( ) . unwrap ( ) ;
247
+ }
229
248
230
- let mut command_syscalls =
231
- retrieve_functions_for_analysis ( & project, KernelWorkType :: CommandSyscalls ) ;
232
- let func_name = & command_syscalls. nth ( 0 ) . unwrap ( ) . 0 . name . clone ( ) ; //led
249
+ // set to board to be evaluated. Currently, not all tock boards are supported.
250
+ // This works because this crate uses the same rust toolchain as Tock.
251
+ let board_path_str = "tock/boards/" . to_string ( ) + & opt. board ;
252
+ println ! ( "Compiling {:?}, please wait..." , board_path_str) ;
233
253
234
- //let func_name = &command_syscalls.nth(1).unwrap().0.name.clone(); //gpio
235
- //let func_name = &command_syscalls.nth(2).unwrap().0.name.clone(); // alarm, fails
236
- //let func_name = &command_syscalls.nth(3).unwrap().0.name.clone(); // i2c, fails bc panic
237
- //let func_name = &command_syscalls.nth(4).unwrap().0.name.clone(); //ble, fails
238
- //let func_name = &command_syscalls.nth(5).unwrap().0.name.clone(); //console, fails
254
+ use std:: process:: Command ;
255
+ assert ! ( Command :: new( "make" )
256
+ . arg( "-C" )
257
+ . arg( & board_path_str)
258
+ . arg( "clean" )
259
+ . output( )
260
+ . expect( "failed to execute make clean" )
261
+ . status
262
+ . success( ) ) ;
263
+ let output = Command :: new ( "make" )
264
+ . arg ( "-C" )
265
+ . arg ( & board_path_str)
266
+ . output ( )
267
+ . expect ( "failed to execute make" ) ;
268
+ assert ! ( output. status. success( ) ) ;
269
+ let str_output = String :: from_utf8 ( output. stderr ) . unwrap ( ) ;
270
+ if !str_output. contains ( "Finished release" ) {
271
+ panic ! ( "Build failed, output: {}" , str_output) ;
272
+ }
239
273
240
- let subscribe_syscalls =
241
- retrieve_functions_for_analysis ( & project, KernelWorkType :: SubscribeSyscalls ) ;
242
- // comments at end indicate which function this corresponds to on the apollo3
243
- //let func_name = &subscribe_syscalls.nth(0).unwrap().0.name.clone(); //dummy impl, 4
244
- //let func_name = &subscribe_syscalls.nth(1).unwrap().0.name.clone(); //gpio
245
- //let func_name = &subscribe_syscalls.nth(2).unwrap().0.name.clone(); //alarm
246
- //let func_name = &subscribe_syscalls.nth(3).unwrap().0.name.clone(); //i2c
247
- //let func_name = &subscribe_syscalls.nth(4).unwrap().0.name.clone(); //ble
248
- //let func_name = &subscribe_syscalls.nth(5).unwrap().0.name.clone(); //console
274
+ // For now, assume target under analysis, located in the tock submodule of this crate.
275
+ // Assume it is a thumbv7 target unless it is one of three whitelisted riscv targets.
249
276
250
- let allow_syscalls = retrieve_functions_for_analysis ( & project, KernelWorkType :: AllowSyscalls ) ;
277
+ let bc_dir = if board_path_str. contains ( "opentitan" )
278
+ || board_path_str. contains ( "arty_e21" )
279
+ || board_path_str. contains ( "hifive1" )
280
+ {
281
+ "tock/target/riscv32imc-unknown-none-elf/release/deps/"
282
+ } else {
283
+ "tock/target/thumbv7em-none-eabi/release/deps/"
284
+ } ;
251
285
252
- //let func_name = &allow_syscalls.nth(0).unwrap().0.name.clone(); //default
253
- //let func_name = &allow_syscalls.nth(1).unwrap().0.name.clone(); //also default??
254
- //let func_name = &allow_syscalls.nth(2).unwrap().0.name.clone(); //also default??
255
- //let func_name = &allow_syscalls.nth(3).unwrap().0.name.clone(); //i2c
256
- //let func_name = &allow_syscalls.nth(4).unwrap().0.name.clone(); //ble, fails
257
- //let func_name = &allow_syscalls.nth(5).unwrap().0.name.clone(); //console, fails
286
+ let paths = glob ( & [ bc_dir, "/**/*.bc" ] . concat ( ) )
287
+ . unwrap ( )
288
+ . map ( |x| x. unwrap ( ) ) ;
289
+ let project = Project :: from_bc_paths ( paths) ?;
258
290
259
- let interrupt_handlers =
260
- retrieve_functions_for_analysis ( & project, KernelWorkType :: InterruptHandlers ) ;
291
+ // Make a vector to hold the children which are spawned.
292
+ let mut functions_to_analyze = vec ! [ ] ;
293
+ let func_name_iter = retrieve_functions_for_analysis ( & project, opt. functions ) ;
294
+ functions_to_analyze. extend ( func_name_iter. map ( |( f, _m) | & f. name ) ) ;
261
295
262
- //functions_to_analyze.extend(allow_syscalls.map(|(f, _m)| &f.name));
263
- //functions_to_analyze.extend(command_syscalls.map(|(f, _m)| &f.name));
264
- //functions_to_analyze.extend(subscribe_syscalls.map(|(f, _m)| &f.name));
265
- functions_to_analyze. extend ( interrupt_handlers. map ( |( f, _m) | & f. name ) ) ;
266
296
let mut children = vec ! [ ] ;
297
+ let all_results = Mutex :: new ( HashMap :: new ( ) ) ;
298
+ let arc = Arc :: new ( all_results) ;
299
+ let timeout = opt. timeout ;
267
300
for f in functions_to_analyze {
268
301
let f = f. clone ( ) ;
302
+ let arc = arc. clone ( ) ;
303
+ let name = board_path_str. clone ( ) ;
269
304
children. push ( thread:: spawn ( move || {
270
- analyze_and_save_results ( bc_dir, board_path_str, & f)
305
+ match analyze_and_save_results ( bc_dir, & name, & f, timeout) {
306
+ Ok ( s) => {
307
+ arc. lock ( ) . map_or ( ( ) , |mut map| {
308
+ map. insert ( f, s) ;
309
+ } ) ;
310
+ }
311
+ _ => { }
312
+ }
271
313
} ) ) ;
272
314
}
273
315
for child in children {
274
- // Wait for the thread to finish. Returns a result.
275
316
let _ = child. join ( ) ;
276
317
}
318
+ // Now, result of each thread is in all_results.
319
+ let filename = "results/" . to_owned ( ) + & opt. board + "/summary.txt" ;
320
+ println ! ( "{:?}" , filename) ;
321
+ let mut file = File :: create ( filename) . unwrap ( ) ;
322
+
323
+ let mut data = String :: new ( ) ;
324
+ let data = arc
325
+ . lock ( )
326
+ . map ( |map| {
327
+ for ( k, v) in map. iter ( ) {
328
+ data = data + k + ": " + v;
329
+ }
330
+ data
331
+ } )
332
+ . unwrap ( ) ;
333
+ file. write_all ( data. as_bytes ( ) ) . unwrap ( ) ;
334
+
277
335
Ok ( ( ) )
278
336
}
0 commit comments