Klimit config #135
Klimit config #135
Conversation
facebook-github-bot
added
the
CLA Signed
There was a problem hiding this comment.
This is a great start, but there is still room for improvement, so let's do a second round of reviews after you've addressed the review comments. You should also provide details of how you've tested this. The integration test is not enough just by itself since the command line usage is the main point of this. Your description of the PR can also be improved. "--max_analysis_time_for_body -> max_analysis_time_for_body" feels a bit cryptic.
| pub const MAX_ANALYSIS_TIME_FOR_BODY_DEFAULT: u64 = 3; | ||
|
|
||
| #[derive(Debug, Clone)] | ||
| pub struct KLimitConfig { |
There was a problem hiding this comment.
The Config suffix does not really add value here. These are just the k-limits, so KLimits would be an appropriate name.
| use mirai::utils; | ||
| use std::env; | ||
| use std::path::Path; | ||
|
|
||
| fn main() { | ||
| fn main() -> Result<(), Box<std::error::Error>> { |
There was a problem hiding this comment.
We don't want the main routine to return a value, or to cause an exception trace to be presented to the person running Mirai. All errors should be property handled and presented as actionable error messages. The main routine should return an appropriate exit code via std::process::exit, so that batch files that invoke Mirai can take the appropriate action.
| // 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( |
There was a problem hiding this comment.
At this point you want to have an option struct, rather than just the k-limits. It would be better to have a separate module for managing options, with one option being the k-limits.
| @@ -47,15 +49,61 @@ fn main() { | |||
| command_line_arguments.remove(1); | |||
| } | |||
|
|
|||
| let max_inferred_preconditions = command_line_arguments | |||
There was a problem hiding this comment.
There is a lot of duplicated code here that could be factored out. A separate module for managing command line options would be a good way to go.
| .unwrap_or(k_limits::MAX_INFERRED_PRECONDITIONS_DEFAULT); | ||
|
|
||
| let max_path_length = command_line_arguments | ||
| .iter_mut() |
There was a problem hiding this comment.
It does not feel right to iterate over the complete list of command_line_arguments for every option. A better approach may be to keep a hash table of options that you update during a single scan of the command line.
| .iter_mut() | ||
| .position(|s| s == "--max_path_length") | ||
| .map(|i| { | ||
| command_line_arguments.remove(i); |
There was a problem hiding this comment.
Modifying a collection that is being iterated over is generally frowned upon. The remove operation is not cheap either. A better approach would be to construct a new filtered list that excludes the MIRAI options.
| .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 |
There was a problem hiding this comment.
You probably want a helper here that emits an error message if the argument does not parse.
|
Closing because of inactivity. |
Description
Updated k-limits to command line options. A default constructor will initialize an instance of KLimitsConfig with default values specified in k_limits.rs. User can also initialize a custom config instance with the new constructor.
Command line flags are as follows:
--max_analysis_time_for_body -> max_analysis_time_for_body
--max_outer_fixpoint_iterations -> max_outer_fixpoint_iterations
--max_path_length -> max_path_length
--max_inferred_preconditions -> max_inferred_preconditions
Fixes #112 (issue)
Type of change
How Has This Been Tested?
Checklist:
master.