From 33e1dd4f68669f05db91768d5ba701f9b4b8f967 Mon Sep 17 00:00:00 2001 From: Raidon Date: Tue, 16 Apr 2019 23:42:20 -0400 Subject: [PATCH] Updated format and moved config to single source Issue #112 --- checker/src/k_limits.rs | 34 +++++++++++--- checker/src/main.rs | 74 ++++++++++++++++-------------- checker/src/visitors.rs | 21 +++++++-- checker/tests/integration_tests.rs | 4 +- 4 files changed, 87 insertions(+), 46 deletions(-) diff --git a/checker/src/k_limits.rs b/checker/src/k_limits.rs index c7d43ada..0b331ad5 100644 --- a/checker/src/k_limits.rs +++ b/checker/src/k_limits.rs @@ -5,16 +5,33 @@ // Somewhat arbitrary constants used to limit things in the abstract interpreter that may // take too long or use too much memory. +/// Helps to limit the size of summaries. +pub const MAX_INFERRED_PRECONDITIONS: usize = 50; + +/// Prevents the fixed point loop from creating ever more new abstract values of type Expression::Variable. +pub const MAX_PATH_LENGTH: usize = 10; + +/// The point at which diverging summaries experience exponential blowup right now. +pub const MAX_OUTER_FIXPOINT_ITERATIONS: usize = 3; + +/// The maximum number of seconds that MIRAI is willing to analyze a function body for. +pub const MAX_ANALYSIS_TIME_FOR_BODY: u64 = 3; + #[derive(Debug, Clone)] pub struct KLimitConfig { - pub max_inferred_preconditions: usize, // Helps to limit the size of summaries. - pub max_path_length: usize, // Prevents the fixed point loop from creating ever more new abstract values of type Expression::Variable. - pub max_outer_fixpoint_iterations: usize, // The point at which diverging summaries experience exponential blowup right now. - pub max_analysis_time_for_body: u64, // The maximum number of seconds that MIRAI is willing to analyze a function body for. + pub max_inferred_preconditions: usize, + pub max_path_length: usize, + pub max_outer_fixpoint_iterations: usize, + pub max_analysis_time_for_body: u64, } impl KLimitConfig { - pub fn new(max_inferred_preconditions: usize, max_path_length: usize, max_outer_fixpoint_iterations: usize, max_analysis_time_for_body: u64) -> KLimitConfig { + pub fn new( + max_inferred_preconditions: usize, + max_path_length: usize, + max_outer_fixpoint_iterations: usize, + max_analysis_time_for_body: u64, + ) -> KLimitConfig { KLimitConfig { max_inferred_preconditions, max_path_length, @@ -26,6 +43,11 @@ impl KLimitConfig { impl Default for KLimitConfig { fn default() -> Self { - Self::new(50,10,3,3) + Self::new( + self::MAX_INFERRED_PRECONDITIONS, + self::MAX_PATH_LENGTH, + self::MAX_OUTER_FIXPOINT_ITERATIONS, + self::MAX_ANALYSIS_TIME_FOR_BODY, + ) } } diff --git a/checker/src/main.rs b/checker/src/main.rs index 52436ca2..f3cc624f 100644 --- a/checker/src/main.rs +++ b/checker/src/main.rs @@ -20,12 +20,13 @@ extern crate rustc_driver; extern crate rustc_interface; use mirai::callbacks; +use mirai::k_limits; use mirai::k_limits::KLimitConfig; use mirai::utils; use std::env; use std::path::Path; -fn main() -> Result<(),Box>{ +fn main() -> Result<(), Box> { // Initialize loggers. if env::var("RUST_LOG").is_ok() { rustc_driver::init_rustc_env_logger(); @@ -48,52 +49,57 @@ fn main() -> Result<(),Box>{ command_line_arguments.remove(1); } - println!("{:#?}",command_line_arguments); - let max_inferred_preconditions = command_line_arguments - .iter_mut() - .position(|s| s == "--max_inferred_preconditions") - .map(|i| { - command_line_arguments.remove(i); - usize::from_str_radix(&command_line_arguments.remove(i),10)//return corresponding value - }) - .transpose()?.unwrap_or(50); + .iter_mut() + .position(|s| s == "--max_inferred_preconditions") + .map(|i| { + command_line_arguments.remove(i); + usize::from_str_radix(&command_line_arguments.remove(i), 10) //return corresponding value + }) + .transpose()? + .unwrap_or(k_limits::MAX_INFERRED_PRECONDITIONS); let max_path_length = command_line_arguments - .iter_mut() - .position(|s| s == "--max_path_length") - .map(|i| { - command_line_arguments.remove(i); - usize::from_str_radix(&command_line_arguments.remove(i),10)//return corresponding value - }) - .transpose()?.unwrap_or(10); + .iter_mut() + .position(|s| s == "--max_path_length") + .map(|i| { + command_line_arguments.remove(i); + usize::from_str_radix(&command_line_arguments.remove(i), 10) //return corresponding value + }) + .transpose()? + .unwrap_or(k_limits::MAX_PATH_LENGTH); let max_outer_fixpoint_iterations = command_line_arguments - .iter_mut() - .position(|s| s == "--max_outer_fixpoint_iterations") - .map(|i| { - command_line_arguments.remove(i); - usize::from_str_radix(&command_line_arguments.remove(i),10)//return corresponding value - }) - .transpose()?.unwrap_or(3); + .iter_mut() + .position(|s| s == "--max_outer_fixpoint_iterations") + .map(|i| { + command_line_arguments.remove(i); + usize::from_str_radix(&command_line_arguments.remove(i), 10) //return corresponding value + }) + .transpose()? + .unwrap_or(k_limits::MAX_OUTER_FIXPOINT_ITERATIONS); let max_analysis_time_for_body = command_line_arguments - .iter_mut() - .position(|s| s == "--max_analysis_time_for_body") - .map(|i| { - command_line_arguments.remove(i); - u64::from_str_radix(&command_line_arguments.remove(i),10)//return corresponding value - }) - .transpose()?.unwrap_or(3); - + .iter_mut() + .position(|s| s == "--max_analysis_time_for_body") + .map(|i| { + command_line_arguments.remove(i); + u64::from_str_radix(&command_line_arguments.remove(i), 10) //return corresponding value + }) + .transpose()? + .unwrap_or(k_limits::MAX_ANALYSIS_TIME_FOR_BODY); // Tell compiler where to find the std library and so on. // The compiler relies on the standard rustc driver to tell it, so we have to do likewise. command_line_arguments.push(String::from("--sysroot")); command_line_arguments.push(utils::find_sysroot()); - let config = KLimitConfig::new(max_inferred_preconditions,max_path_length,max_outer_fixpoint_iterations,max_analysis_time_for_body); - + let config = KLimitConfig::new( + max_inferred_preconditions, + max_path_length, + max_outer_fixpoint_iterations, + max_analysis_time_for_body, + ); let result = rustc_driver::report_ices_to_stderr_if_any(move || { rustc_driver::run_compiler( &command_line_arguments, diff --git a/checker/src/visitors.rs b/checker/src/visitors.rs index 618c80c6..c8cfd9aa 100644 --- a/checker/src/visitors.rs +++ b/checker/src/visitors.rs @@ -156,7 +156,11 @@ impl<'a, 'b: 'a, 'tcx: 'b, E> MirVisitor<'a, 'b, 'tcx, E> { (*p) == source_path || p.is_rooted_by(&source_path) }) { let tpath = path - .replace_root(&source_path, target_path.clone(),self.k_limits.max_path_length) + .replace_root( + &source_path, + target_path.clone(), + self.k_limits.max_path_length, + ) .refine_paths(&mut self.current_environment); let rvalue = value.refine_paths(&mut self.current_environment); self.current_environment.update_value_at(tpath, rvalue); @@ -389,7 +393,11 @@ impl<'a, 'b: 'a, 'tcx: 'b, E> MirVisitor<'a, 'b, 'tcx, E> { .iter() .filter(|(p, _)| p.is_rooted_by(&result_root)) { - let promoted_path = path.replace_root(&result_root, promoted_root.clone(),self.k_limits.max_path_length); + let promoted_path = path.replace_root( + &result_root, + promoted_root.clone(), + self.k_limits.max_path_length, + ); state_with_parameters.update_value_at(promoted_path, value.clone()); } @@ -1172,7 +1180,11 @@ impl<'a, 'b: 'a, 'tcx: 'b, E> MirVisitor<'a, 'b, 'tcx, E> { .filter(|(p, _)| (*p) == source_path || p.is_rooted_by(&source_path)) { let tpath = path - .replace_root(&source_path, target_path.clone(),self.k_limits.max_path_length) + .replace_root( + &source_path, + target_path.clone(), + self.k_limits.max_path_length, + ) .refine_paths(&mut self.current_environment); let rvalue = value .refine_parameters(arguments) @@ -1537,7 +1549,8 @@ impl<'a, 'b: 'a, 'tcx: 'b, E> MirVisitor<'a, 'b, 'tcx, E> { .iter() .filter(|(p, _)| p.is_rooted_by(&rpath)) { - let qualified_path = path.replace_root(&rpath, target_path.clone(),self.k_limits.max_path_length); + let qualified_path = + path.replace_root(&rpath, target_path.clone(), self.k_limits.max_path_length); if move_elements { debug!("moving {:?} to {:?}", value, qualified_path); value_map = value_map.remove(&path); diff --git a/checker/tests/integration_tests.rs b/checker/tests/integration_tests.rs index 29b4c979..2f950997 100644 --- a/checker/tests/integration_tests.rs +++ b/checker/tests/integration_tests.rs @@ -24,8 +24,8 @@ extern crate syntax; extern crate tempdir; use mirai::callbacks; -use mirai::utils; use mirai::k_limits::KLimitConfig; +use mirai::utils; use rustc_rayon::iter::IntoParallelIterator; use rustc_rayon::iter::ParallelIterator; use std::fs; @@ -135,7 +135,7 @@ fn invoke_driver( annotations_option, ]; - let config = KLimitConfig::new(); + let config = KLimitConfig::new(50, 10, 3, 3); let mut call_backs = callbacks::MiraiCallbacks::test_runner(config); let result = std::panic::catch_unwind(move || { rustc_driver::run_compiler(