diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index e14c1e0613a..598226e0599 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -2,10 +2,12 @@ | Name | Rust type | Default value | | --- | --- | --- | +| [`ALLOW_UNREACHABLE_UNSUPPORTED_CODE`](#allow_unreachable_unsupported_code) | `bool` | `false` | | [`ASSERT_TIMEOUT`](#assert_timeout) | `u64` | `10_000` | | [`BE_RUSTC`](#be_rustc) | `bool` | `false` | -| [`CHECK_OVERFLOWS`](#check_overflows) | `bool` | `true` | +| [`CACHE_PATH`](#cache_path) | `String` | `""` | | [`CHECK_FOLDUNFOLD_STATE`](#check_foldunfold_state) | `bool` | `false` | +| [`CHECK_OVERFLOWS`](#check_overflows) | `bool` | `true` | | [`CHECK_PANICS`](#check_panics) | `bool` | `true` | | [`CONTRACTS_LIB`](#contracts_lib) | `String` | `""` | | [`COUNTEREXAMPLE`](#counterexample) | `bool` | `false` | @@ -17,21 +19,34 @@ | [`DUMP_PATH_CTXT_IN_DEBUG_INFO`](#dump_path_ctxt_in_debug_info) | `bool` | `false` | | [`DUMP_REBORROWING_DAG_IN_DEBUG_INFO`](#dump_reborrowing_dag_in_debug_info) | `bool` | `false` | | [`DUMP_VIPER_PROGRAM`](#dump_viper_program) | `bool` | `false` | +<<<<<<< unify-flags +| [`ENABLE_CACHE`](#enable_cache) | `bool` | `true` | +| [`ENABLE_PURIFICATION_OPTIMIZATION`](#enable_purification_optimization) | `bool` | `false` | +======= | [`ENABLE_GHOST_CONSTRAINTS`](#enable_ghost_constraints) | `bool` | `false` | +>>>>>>> master | [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) | `bool` | `false` | +| [`ENCODE_BITVECTORS`](#encode_bitvectors) | `bool` | `false` | | [`ENCODE_UNSIGNED_NUM_CONSTRAINT`](#encode_unsigned_num_constraint) | `bool` | `false` | | [`EXTRA_JVM_ARGS`](#extra_jvm_args) | `Vec` | `vec![]` | | [`EXTRA_VERIFIER_ARGS`](#extra_verifier_args) | `Vec` | `vec![]` | | [`FOLDUNFOLD_STATE_FILTER`](#foldunfold_state_filter) | `String` | `""` | | [`FULL_COMPILATION`](#full_compilation) | `bool` | `false` | | [`HIDE_UUIDS`](#hide_uuids) | `bool` | `false` | +| [`IGNORE_REGIONS`](#ignore_regions) | `bool` | `false` | +| [`INTERN_NAMES`](#intern_names) | `bool` | `true` | | [`JSON_COMMUNICATION`](#json_communication) | `bool` | `false` | | [`LOG`](#log) | `Option` | `None` | -| [`LOG_DIR`](#log_dir) | `String` | `"./log/"` | +| [`LOG_DIR`](#log_dir) | `String` | `"log"` | | [`LOG_STYLE`](#log_style) | `String` | `"auto"` | +| [`MAX_LOG_FILE_NAME_LENGTH`](#max_log_file_name_length) | `usize` | `60` | | [`NO_VERIFY`](#no_verify) | `bool` | `false` | -| [`PRINT_COLLECTED_VERFICATION_ITEMS`](#print_collected_verfication_items) | `bool` | `false` | +| [`NO_VERIFY_DEPS`](#no_verify_deps) | `bool` | `false` | +| [`ONLY_MEMORY_SAFETY`](#only_memory_safety) | `bool` | `false` | +| [`OPTIMIZATIONS`](#optimizations) | `Vec` | "all" | +| [`PRINT_COLLECTED_VERIFICATION_ITEMS`](#print_collected_verification_items) | `bool` | `false` | | [`PRINT_DESUGARED_SPECS`](#print_desugared_specs) | `bool` | `false` | +| [`PRINT_HASH`](#print_hash) | `bool` | `false` | | [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | `bool` | `false` | | [`QUIET`](#quiet) | `bool` | `false` | | [`SERVER_ADDRESS`](#server_address) | `Option` | `None` | @@ -39,11 +54,17 @@ | [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option` | `None` | | [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | | [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | +| [`UNSAFE_CORE_PROOF`](#unsafe_core_proof) | `bool` | `false` | | [`USE_MORE_COMPLETE_EXHALE`](#use_more_complete_exhale) | `bool` | `true` | +| [`VERIFICATION_DEADLINE`](#verification_deadline) | `Option` | `None` | | [`VERIFY_ONLY_BASIC_BLOCK_PATH`](#verify_only_basic_block_path) | `Vec` | `vec![]` | | [`VERIFY_ONLY_PREAMBLE`](#verify_only_preamble) | `bool` | `false` | | [`VIPER_BACKEND`](#viper_backend) | `String` | `"Silicon"` | +## `ALLOW_UNREACHABLE_UNSUPPORTED_CODE` + +When enabled, unsupported code is encoded as `assert false`. This way error messages are reported only for unsupported code that is actually reachable. + ## `ASSERT_TIMEOUT` Maximum time (in milliseconds) for the verifier to spend on a single assertion. Set to `0` to disable timeout. Maps to the verifier command-line argument `--assertTimeout`. @@ -52,14 +73,18 @@ Maximum time (in milliseconds) for the verifier to spend on a single assertion. When enabled, Prusti will behave like `rustc`. -## `CHECK_OVERFLOWS` +## `CACHE_PATH` -When enabled, binary operations and numeric casts will be checked for overflows. See [integer type encoding](../encoding/types-heap.md#i-u-char). +Path to a cache file, where verification cache will be loaded from and saved to. The default empty string disables saving any cache to disk. A path to a file which does not yet exist will result in using an empty cache, but then creating and saving to that location on exit. ## `CHECK_FOLDUNFOLD_STATE` When enabled, additional, *slow*, checks for the `fold`/`unfold` algorithm will be generated. +## `CHECK_OVERFLOWS` + +When enabled, binary operations and numeric casts will be checked for overflows. See [integer type encoding](../encoding/types-heap.md#i-u-char). + ## `CHECK_PANICS` When enabled, Prusti will check for an absence of `panic!`s. @@ -106,6 +131,23 @@ When enabled, reborrowing DAGs will be output in debug files. When enabled, the encoded Viper program will be output. +<<<<<<< unify-flags +## `ENCODE_BITVECTORS` + +When enabled, bitwise integer operations are encoded using bitvectors. + +**Note:** This option is highly experimental. + +## `ENABLE_CACHE` + +When enabled, verification requests (to verify individual `fn`s) are cached to improve future verification. By default the cache is only saved in memory (of the `prusti-server` if enabled). For long-running verification projects use [`CACHE_PATH`](#cache_path) to save to disk. + +## `ENABLE_PURIFICATION_OPTIMIZATION` + +When enabled, impure methods are optimized using the purification optimization, which tries to convert heap operations to pure (snapshot-based) operations. + +**Note:** This option is highly experimental. +======= ## `ENABLE_GHOST_CONSTRAINTS` Enables ghost constraints in Prusti specifications. @@ -114,6 +156,7 @@ Ghost constraints allow for specifications which are only active if a certain "c on a generic type parameter) is satisfied. **This is an experimental feature**, because it is currently possible to introduce unsound verification behavior. +>>>>>>> master ## `ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH` @@ -145,9 +188,17 @@ When enabled, compilation will continue and a binary will be generated after Pru When enabled, UUIDs of expressions and specifications printed with [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) are hidden. +## `IGNORE_REGIONS` + +When enabled, debug files dumped by `rustc` will not contain lifetime regions. + +## `INTERN_NAMES` + +When enabled, Viper identifiers are interned to shorten them when possible. + ## `JSON_COMMUNICATION` -When enabled, communication with the server will be encoded as JSON instead of bincode. +When enabled, communication with the server will be encoded as JSON instead of the default bincode. ## `LOG` @@ -161,25 +212,58 @@ Path to directory in which log files and dumped output will be stored. Log style. See [`env_logger` documentation](https://docs.rs/env_logger/0.7.1/env_logger/index.html#disabling-colors). +## `MAX_LOG_FILE_NAME_LENGTH` + +Maximum allowed length of a log file name. If this is exceeded, the file name is truncated. + ## `NO_VERIFY` When enabled, verification is skipped altogether. +## `NO_VERIFY_DEPS` + +When enabled, verification is skipped for dependencies. + +## `ONLY_MEMORY_SAFETY` + +When enabled, only the core proof is verified. + +**Note:** This should be used only when `UNSAFE_CORE_PROOF` is enabled. + +## `OPTIMIZATIONS` + +Comma-separated list of optimizations to enable, or `"all"` to enable all. Possible values in the list are: + +- `"inline_constant_functions"` +- `"delete_unused_predicates"` +- `"optimize_folding"` +- `"remove_empty_if"` +- `"purify_vars"` +- `"fix_quantifiers"` +- `"fix_unfoldings"` +- `"remove_unused_vars"` +- `"remove_trivial_assertions"` +- `"clean_cfg"` + +## `PRINT_COLLECTED_VERIFICATION_ITEMS` + +When enabled, prints the items collected for verification. + ## `PRINT_DESUGARED_SPECS` When enabled, prints the AST with desugared specifications. -## `PRINT_TYPECKD_SPECS` +## `PRINT_HASH` -When enabled, prints the type-checked specifications. +When enabled, prints the hash of a verification request (the hash is used for caching). This is a debugging option which does not perform verification — it is similar to [`NO_VERIFY`](#no_verify), except that this flag stops the verification process at a later stage. -## `PRINT_COLLECTED_VERFICATION_ITEMS` +## `PRINT_TYPECKD_SPECS` -When enabled, prints the items collected for verification. +When enabled, prints the type-checked specifications. ## `QUIET` -When enabled, user messages are not printed. Otherwise, `message` outputs into `stderr`. +When enabled, user messages are not printed. Otherwise, messages output into `stderr`. ## `SERVER_ADDRESS` @@ -189,11 +273,11 @@ When set to `"MOCK"`, the server is run off-thread, effectively mocking connecti ## `SERVER_MAX_CONCURRENCY` -The maximum amount of verification requests the server will work on concurrently. If not set, defaults to the number of (logical) cores on the system. +Maximum amount of verification requests the server will work on concurrently. If not set, defaults to the number of (logical) cores on the system. ## `SERVER_MAX_STORED_VERIFIERS` -The maximum amount of instantiated Viper verifiers the server will keep around for reuse. If not set, defaults to `SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS`. It also doesn't make much sense to set this option to less than that, since then the server will likely have to keep creating new verifiers, reducing the performance gained from reuse. +Maximum amount of instantiated Viper verifiers the server will keep around for reuse. If not set, defaults to `SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS`. It also doesn't make much sense to set this option to less than that, since then the server will likely have to keep creating new verifiers, reducing the performance gained from reuse. **Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache. @@ -205,10 +289,22 @@ When enabled, the encoded program is simplified before it is passed to the Viper When enabled, features not supported by Prusti will be reported as warnings rather than errors. +## `UNSAFE_CORE_PROOF` + +When enabled, the new core proof is used, suitable for unsafe code + +**Note:** This option is currently very incomplete. + ## `USE_MORE_COMPLETE_EXHALE` When enabled, a more complete `exhale` version is used in the verifier. See [`consolidate`](https://github.com/viperproject/silicon/blob/f48de7f6e2d90d9020812869c713a5d3e2035995/src/main/scala/rules/StateConsolidator.scala#L29-L46). Equivalent to the verifier command-line argument `--enableMoreCompleteExhale`. +## `VERIFICATION_DEADLINE` + +Deadline (in seconds) within which Prusti should encode and verify the program. + +Prusti panics if it fails to meet this deadline. This flag is intended to be used for tests that aim to catch performance regressions. + ## `VERIFY_ONLY_BASIC_BLOCK_PATH` Verify only the single execution path goes through the given basic blocks. All basic blocks not on this execution path are replaced with `assume false`. Must be enabled using the [`ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH`](#enable_verify_only_basic_block_path) flag. diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index f2e8ae48bd3..f9908c519c8 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -97,10 +97,10 @@ lazy_static! { settings.set_default("no_verify_deps", false).unwrap(); settings.set_default("full_compilation", false).unwrap(); settings.set_default("json_communication", false).unwrap(); - settings.set_default("optimizations","all").unwrap(); + settings.set_default("optimizations", "all").unwrap(); settings.set_default("intern_names", true).unwrap(); settings.set_default("enable_purification_optimization", false).unwrap(); - settings.set_default("enable_manual_axiomatization", false).unwrap(); + // settings.set_default("enable_manual_axiomatization", false).unwrap(); settings.set_default::>("verification_deadline", None).unwrap(); settings.set_default("unsafe_core_proof", false).unwrap(); settings.set_default("only_memory_safety", false).unwrap(); @@ -209,17 +209,28 @@ where read_optional_setting(name).unwrap_or_else(|| panic!("Failed to read setting {:?}", name)) } -/// Should Prusti behave exactly like rustc? +// The following methods are all convenience wrappers for the actual call to +// `read_setting` (+ optionally some light sanitisation or processing). Please +// keep the documentation on each method in sync with `flags.md` in the dev +// guide! + +/// When enabled, Prusti will behave like `rustc`. pub fn be_rustc() -> bool { read_setting("be_rustc") } -/// Generate additional, *slow*, checks for the foldunfold algorithm +/// When enabled, additional, *slow*, checks for the `fold`/`unfold` algorithm +/// will be generated. pub fn check_foldunfold_state() -> bool { read_setting("check_foldunfold_state") } -/// The Viper backend that should be used for the verification +/// Verification backend to use. Possible values: +/// +/// - `Carbon` - verification-condition-generation-based backend +/// [Carbon](https://github.com/viperproject/carbon). +/// - `Silicon` - symbolic-execution-based backend +/// [Silicon](https://github.com/viperproject/silicon/). pub fn viper_backend() -> String { read_setting::("viper_backend") .to_lowercase() @@ -227,216 +238,260 @@ pub fn viper_backend() -> String { .to_string() } -/// Should we check absence of panics? +/// When enabled, Prusti will check for an absence of `panic!`s. pub fn check_panics() -> bool { read_setting("check_panics") } -/// Should we simplify the encoding before passing it to Viper? +/// When enabled, the encoded program is simplified before it is passed to +/// the Viper backend. pub fn simplify_encoding() -> bool { read_setting("simplify_encoding") } -/// Should we dump debug files? +/// When enabled, debug files will be created. pub fn dump_debug_info() -> bool { read_setting("dump_debug_info") } -/// Should we dump debug files for fold/unfold generation? +/// When enabled, the state of the fold-unfold algorithm after each step will +/// be dumped to a file. pub fn dump_debug_info_during_fold() -> bool { read_setting("dump_debug_info_during_fold") } -/// Should the dumped debug files not contain lifetime regions? +/// When enabled, debug files dumped by `rustc` will not contain lifetime +/// regions. pub fn ignore_regions() -> bool { read_setting("ignore_regions") } -/// What is the longest allowed length of a log file name? If this is exceeded, -/// the file name is truncated. +/// Maximum allowed length of a log file name. If this is exceeded, the file +/// name is truncated. pub fn max_log_file_name_length() -> usize { read_setting("max_log_file_name_length") } -/// Should we dump the branch context state in debug files? +/// When enabled, branch context state will be output in debug files. pub fn dump_path_ctxt_in_debug_info() -> bool { read_setting("dump_path_ctxt_in_debug_info") } -/// Should we dump the reborrowing DAGs in debug files? +/// When enabled, reborrowing DAGs will be output in debug files. pub fn dump_reborrowing_dag_in_debug_info() -> bool { read_setting("dump_reborrowing_dag_in_debug_info") } -/// Should we dump borrowck info? +/// When enabled, borrow checking info will be output. pub fn dump_borrowck_info() -> bool { read_setting("dump_borrowck_info") } -/// Should we dump the Viper program? +/// When enabled, the encoded Viper program will be output. pub fn dump_viper_program() -> bool { read_setting("dump_viper_program") } -/// The Viper backend that should be used for the verification +/// Filter for `fold`/`unfold` nodes when debug info is dumped. pub fn foldunfold_state_filter() -> String { read_setting("foldunfold_state_filter") } -/// In which folder should we store log/dumps? +/// Path to directory in which log files and dumped output will be stored. pub fn log_dir() -> PathBuf { PathBuf::from(read_setting::("log_dir")) } -/// In which folder should we store the Verification cache +/// Path to a cache file, where verification cache will be loaded from and +/// saved to. The default empty string disables saving any cache to disk. +/// A path to a file which does not yet exist will result in using an empty +/// cache, but then creating and saving to that location on exit. pub fn cache_path() -> PathBuf { PathBuf::from(read_setting::("cache_path")) } -/// Check binary operations for overflows +/// When enabled, binary operations and numeric casts will be checked for +/// overflows. pub fn check_overflows() -> bool { read_setting("check_overflows") } -/// Encode (and check) that unsigned integers are non-negative. +/// When enabled, non-negativity of unsigned integers will be encoded and +/// checked. pub fn encode_unsigned_num_constraint() -> bool { read_setting("encode_unsigned_num_constraint") } -/// Enable (highly hacky) support for bitvectors. +/// When enabled, bitwise integer operations are encoded using bitvectors. +/// +/// **Note:** this option is highly experimental. pub fn encode_bitvectors() -> bool { read_setting("encode_bitvectors") } -/// Location of 'libprusti_contracts*.rlib' +/// Path to `libprusti_contracts*.rlib`. pub fn contracts_lib() -> String { read_setting("contracts_lib") } -/// Get extra JVM arguments +/// Additional arguments to pass to the JVM when launching a verifier backend. pub fn extra_jvm_args() -> Vec { read_setting("extra_jvm_args") } -/// Get extra arguments for the verifier +/// Additional arguments to pass to the verifier backend. pub fn extra_verifier_args() -> Vec { read_setting("extra_verifier_args") } -/// Should we hide user messages? +/// When enabled, user messages are not printed. Otherwise, message output +/// into `stderr`. pub fn quiet() -> bool { read_setting("quiet") } -/// The assert timeout (in milliseconds) passed to Silicon. +/// Maximum time (in milliseconds) for the verifier to spend on a single +/// assertion. Set to `0` to disable timeout. Maps to the verifier command-line +/// argument `--assertTimeout`. pub fn assert_timeout() -> u64 { read_setting("assert_timeout") } -/// Use the Silicon configuration option `--enableMoreCompleteExhale`. +/// When enabled, a more complete `exhale` version is used in the verifier. +/// See [`consolidate`](https://github.com/viperproject/silicon/blob/f48de7f6e2d90d9020812869c713a5d3e2035995/src/main/scala/rules/StateConsolidator.scala#L29-L46). +/// Equivalent to the verifier command-line argument +/// `--enableMoreCompleteExhale`. pub fn use_more_complete_exhale() -> bool { read_setting("use_more_complete_exhale") } -/// Should Prusti print the items collected for verification. +/// When enabled, prints the items collected for verification. pub fn print_collected_verification_items() -> bool { read_setting("print_collected_verification_items") } -/// Should Prusti print the AST with desugared specifications. +/// When enabled, prints the AST with desugared specifications. pub fn print_desugared_specs() -> bool { read_setting("print_desugared_specs") } -/// Should Prusti print the type-checked specifications. +/// When enabled, prints the type-checked specifications. pub fn print_typeckd_specs() -> bool { read_setting("print_typeckd_specs") } -/// Should Prusti hide the UUIDs of expressions and specifications. +/// When enabled, UUIDs of expressions and specifications printed with +/// `PRINT_TYPECKD_SPECS` are hidden. pub fn hide_uuids() -> bool { read_setting("hide_uuids") } -/// Should Prusti produce a counterexample. -pub fn produce_counterexample() -> bool { +/// When enabled, Prusti will try to find and print a counterexample for any +/// failed assertion or specification. +pub fn counterexample() -> bool { read_setting("counterexample") } -/// Should Prusti print VerificationRequest hashes. +/// When enabled, prints the hash of a verification request (the hash is used +/// for caching). This is a debugging option which does not perform +/// verification -- it is similar to `NO_VERIFY`, except that this flag stops +/// the verification process at a later stage. pub fn print_hash() -> bool { read_setting("print_hash") } -/// Should Prusti ignore cached verification results. +/// When enabled, verification requests (to verify individual `fn`s) are cached +/// to improve future verification. By default the cache is only saved in +/// memory (of the `prusti-server` if enabled). For long-running verification +/// projects use `CACHE_PATH` to save to disk. pub fn enable_cache() -> bool { read_setting("enable_cache") } -/** -The maximum amount of instantiated viper verifiers the server will keep around for reuse. -If not set, this defaults to `SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS`. -It also doesn't make much sense to set this to less than that, since then the server will likely have to keep creating new verifiers, reducing the performance gained from reuse. -**Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache. -*/ +/// Maximum amount of instantiated Viper verifiers the server will keep around +/// for reuse. If not set, defaults to +/// `SERVER_MAX_CONCURRENT_VERIFICATION_OPERATIONS`. It also doesn't make much +/// sense to set this option to less than that, since then the server will +/// likely have to keep creating new verifiers, reducing the performance gained +/// from reuse. +/// +/// **Note:** This does _not_ limit how many verification requests the server +/// handles concurrently, only the size of what is essentially its verifier +/// cache. pub fn server_max_stored_verifiers() -> Option { // TODO: default to below in prusti-server // TODO: warn if lower than below read_optional_setting("server_max_stored_verifiers") } -/// The maximum amount of verification requests the server will work on concurrently. -/// -/// If not set, this defaults to the number of (logical) cores on the system +/// Maximum amount of verification requests the server will work on +/// concurrently. If not set, defaults to the number of (logical) cores on +/// the system. pub fn server_max_concurrency() -> Option { read_optional_setting("server_max_concurrency") } -/// When set, Prusti will connect to this server and use it for its verification backend (i.e. the things using the JVM/Viper). -/// Set to "MOCK" to run the server off-thread, effectively mocking connecting to a server without having to start it up separately. -/// e.g. "127.0.0.1:2468" +/// When set to an address and port (e.g. `"127.0.0.1:2468"`), Prusti will +/// connect to the given server and use it for its verification backend. +/// +/// When set to `"MOCK"`, the server is run off-thread, effectively mocking +/// connecting to a server without having to start it up separately. pub fn server_address() -> Option { read_optional_setting("server_address") } -/// If true, communication with the server will be encoded as json and not the default of bincode. +/// When enabled, communication with the server will be encoded as JSON +/// instead of the default bincode. pub fn json_communication() -> bool { read_setting("json_communication") } -/// Disable mangling of generated Viper names. +/// When enabled, Viper name mangling will be disabled. /// -/// **Note:** This is very likely to result in invalid programs being -/// generated because of name collisions. +/// **Note:** This is very likely to result in invalid programs being generated +/// because of name collisions. pub fn disable_name_mangling() -> bool { read_setting("disable_name_mangling") } -/// Verify only the preamble: domains, functions, and predicates. +/// When enabled, only the preamble will be verified: domains, functions, +/// and predicates. /// /// **Note:** With this flag enabled, no methods are verified! pub fn verify_only_preamble() -> bool { read_setting("verify_only_preamble") } -/// Verify only the path given in ``VERIFY_ONLY_BASIC_BLOCK_PATH``. +/// When enabled, only the path given in `VERIFY_ONLY_BASIC_BLOCK_PATH` will +/// be verified. /// -/// **Note:** This flag is only for debugging Prusti! +/// **Note:** This flag is only for debugging Prusti. pub fn enable_verify_only_basic_block_path() -> bool { read_setting("enable_verify_only_basic_block_path") } /// Verify only the single execution path goes through the given basic blocks. +/// All basic blocks not on this execution path are replaced with `assume false`. +/// Must be enabled using the `ENABLE_VERIFY_ONLY_BASIC_BLOCK_PATH` flag. /// -/// All basic blocks not on this execution path are replaced with -/// ``assume false``. -/// -/// **Note:** This flag is only for debugging Prusti! +/// **Note:** This option is only for debugging Prusti. pub fn verify_only_basic_block_path() -> Vec { read_setting("verify_only_basic_block_path") } -/// Which optimizations should be enabled +/// Comma-separated list of optimizations to enable, or `"all"` to enable all. +/// Possible values in the list are: +/// +/// - `"inline_constant_functions"` +/// - `"delete_unused_predicates"` +/// - `"optimize_folding"` +/// - `"remove_empty_if"` +/// - `"purify_vars"` +/// - `"fix_quantifiers"` +/// - `"fix_unfoldings"` +/// - `"remove_unused_vars"` +/// - `"remove_trivial_assertions"` +/// - `"clean_cfg"` pub fn optimizations() -> Optimizations { let optimizations_string = read_setting::("optimizations"); @@ -463,80 +518,80 @@ pub fn optimizations() -> Optimizations { opt } -/// Enable purification optimization for impure functions. +/// When enabled, impure methods are optimized using the purification +/// optimization, which tries to convert heap operations to pure (snapshot- +/// based) operations. +/// +/// **Note:** this option is highly experimental. pub fn enable_purification_optimization() -> bool { read_setting("enable_purification_optimization") } -/// Enable manual axiomatization of pure functions. -/// -/// **Note:** this is currently very incomplete and may introduce unsoudnesses. -pub fn enable_manual_axiomatization() -> bool { - read_setting("enable_manual_axiomatization") -} - -/// Set the deadline in seconds within which Prusti should encode and verify the -/// program. +/// Deadline (in seconds) within which Prusti should encode and verify +/// the program. /// -/// Prusti panics if it fails to meet this deadline. This flag is intended to be -/// used for tests that aim to catch performance regressions. +/// Prusti panics if it fails to meet this deadline. This flag is intended to +/// be used for tests that aim to catch performance regressions. pub fn verification_deadline() -> Option { read_setting::>("verification_deadline").map(|value| { value.try_into().expect("verification_deadline must be a valid u64") }) } -/// Use the new core proof suitable for unsafe code. +/// When enabled, the new core proof is used, suitable for unsafe code /// -/// **Note:** this is currently very incomplete. +/// **Note:** This option is currently very incomplete. pub fn unsafe_core_proof() -> bool { read_setting("unsafe_core_proof") } -/// Verify only the core proof. +/// When enabled, only the core proof is verified. /// -/// Note: This should be used together with `unsafe_core_proof=True`. +/// **Note:** This should be used only when `UNSAFE_CORE_PROOF` is enabled. pub fn only_memory_safety() -> bool { read_setting("only_memory_safety") } -/// Replace the given basic blocks with ``assume false``. +/// The given basic blocks will be replaced with `assume false`. pub fn delete_basic_blocks() -> Vec { read_setting("delete_basic_blocks") } -/// Skip features that are unsupported or partially supported +/// When enabled, features not supported by Prusti will be reported as warnings +/// rather than errors. pub fn skip_unsupported_features() -> bool { read_setting("skip_unsupported_features") } -/// Report internal errors as warnings instead of errors. Used for testing. +/// When enabled, internal errors are reported as warnings instead of errors. +/// Used for testing. pub fn internal_errors_as_warnings() -> bool { read_setting("internal_errors_as_warnings") } -/// Encode unsupported code as `assert false`, so that we report error messages -/// only for unsupported code that is actually reachable. +/// When enabled, unsupported code is encoded as `assert false`. This way error +/// messages are reported only for unsupported code that is actually reachable. pub fn allow_unreachable_unsupported_code() -> bool { read_setting("allow_unreachable_unsupported_code") } -/// Skip the verification +/// When enabled, verification is skipped altogether. pub fn no_verify() -> bool { read_setting("no_verify") } -/// Skip the verification of dependencies +/// When enabled, verification is skipped for dependencies. pub fn no_verify_deps() -> bool { read_setting("no_verify_deps") } -/// Continue the compilation and generate the binary after Prusti terminates +/// When enabled, compilation will continue and a binary will be generated +/// after Prusti terminates. pub fn full_compilation() -> bool { read_setting("full_compilation") } -/// Intern Viper identifiers to shorten them when possible. +/// When enabled, Viper identifiers are interned to shorten them when possible. pub fn intern_names() -> bool { read_setting("intern_names") } diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index 56207f36745..91f63f3b2b1 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -45,7 +45,7 @@ impl Default for ViperBackendConfig { if config::use_more_complete_exhale() { verifier_args.push("--enableMoreCompleteExhale".to_string()); } - if config::produce_counterexample() { + if config::counterexample() { verifier_args.push("--counterexample".to_string()); verifier_args.push("mapped".to_string()); } diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index f99d04937eb..af7e5b998d9 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -5561,7 +5561,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // no discriminant if num_variants > 1 { // remember where discriminant can be found for counterexamples - if config::produce_counterexample() { + if config::counterexample() { let enum_id = encoded_src.to_string(); self.encoder.add_discriminant_info( enum_id, diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs index 6b9c7498a26..3634ae759b5 100644 --- a/prusti-viper/src/verifier.rs +++ b/prusti-viper/src/verifier.rs @@ -316,7 +316,7 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { let mut prusti_error = error_manager.translate_verification_error(&verification_error); // annotate with counterexample, if requested - if config::produce_counterexample() { + if config::counterexample() { if let Some(silicon_counterexample) = &verification_error.counterexample { if let Some(def_id) = error_manager.get_def_id(&verification_error) { let counterexample = counterexample_translation::backtranslate(