Skip to content

Commit

Permalink
Updated format and moved config to single source Issue facebookexperi…
Browse files Browse the repository at this point in the history 
…mental#112
  • Loading branch information
Raidon committed Apr 17, 2019
1 parent 34591d3 commit 33e1dd4
Show file tree
Hide file tree
Showing 4 changed files with 87 additions and 46 deletions.
34 changes: 28 additions & 6 deletions checker/src/k_limits.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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,
)
}
}
74 changes: 40 additions & 34 deletions checker/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<std::error::Error>>{
fn main() -> Result<(), Box<std::error::Error>> {
// Initialize loggers.
if env::var("RUST_LOG").is_ok() {
rustc_driver::init_rustc_env_logger();
Expand All @@ -48,52 +49,57 @@ fn main() -> Result<(),Box<std::error::Error>>{
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,
Expand Down
21 changes: 17 additions & 4 deletions checker/src/visitors.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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());
}

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions checker/tests/integration_tests.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(
Expand Down

0 comments on commit 33e1dd4

Please sign in to comment.