Skip to content

Update flags in dev guide #931

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Aurel300 merged 2 commits into from
Apr 26, 2022
Merged

Update flags in dev guide #931

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0fd9885
update flags in dev guide
Aurel300 Mar 29, 2022
f3c2dcf
Merge branch 'master' into unify-flags
Aurel300 Apr 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 109 additions & 13 deletions docs/dev-guide/src/config/flags.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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` |
Expand All @@ -17,33 +19,52 @@
| [`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<String>` | `vec![]` |
| [`EXTRA_VERIFIER_ARGS`](#extra_verifier_args) | `Vec<String>` | `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<String>` | `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<String>` | "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<String>` | `None` |
| [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option<usize>` | `None` |
| [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option<usize>` | `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<u64>` | `None` |
| [`VERIFY_ONLY_BASIC_BLOCK_PATH`](#verify_only_basic_block_path) | `Vec<String>` | `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`.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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`

Expand Down Expand Up @@ -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`

Expand All @@ -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 &mdash; 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`

Expand All @@ -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.

Expand All @@ -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.
Expand Down
Loading