Skip to content

Commit

Permalink
Port verify_only_defpath and report_viper_messages flags
Browse files Browse the repository at this point in the history
Defpath only verification does not work since test_entrypoint currently
just puts the entire program into the request regardless of the
verification tasks at hand.
Update the flags in the documentation.
PR: viperproject#1334
trktby committed Jun 13, 2024
1 parent 0849d35 commit 5270e09
Showing 5 changed files with 129 additions and 8 deletions.
26 changes: 25 additions & 1 deletion docs/dev-guide/src/config/flags.md
Original file line number Diff line number Diff line change
@@ -56,13 +56,16 @@
| [`PRINT_HASH`](#print_hash) | `bool` | `false` | A |
| [`PRINT_TYPECKD_SPECS`](#print_typeckd_specs) | `bool` | `false` | A |
| [`QUIET`](#quiet) | `bool` | `false` | A* |
| [`REPORT_VIPER_MESSAGES`](#report_viper_messages) | `bool` | `false` | A |
| [`SERVER_ADDRESS`](#server_address) | `Option<String>` | `None` | A |
| [`SERVER_MAX_CONCURRENCY`](#server_max_concurrency) | `Option<usize>` | `None` | A |
| [`SERVER_MAX_STORED_VERIFIERS`](#server_max_stored_verifiers) | `Option<usize>` | `None` | A |
| [`SHOW_IDE_INFO`](#show_ide_info) | `bool` | `false` | A |
| [`SIMPLIFY_ENCODING`](#simplify_encoding) | `bool` | `true` | A |
| [`SKIP_UNSUPPORTED_FEATURES`](#skip_unsupported_features) | `bool` | `false` | A |
| [`SKIP_VERIFICATION`](#skip_verification) | `bool` | `false` | A |
| [`SMT_QI_BOUND_GLOBAL`](#smt_qi_bound_global) | `Option<u64>` | `None` | A |
[`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option<u64>` | `None` | A |
| [`SMT_QI_BOUND_GLOBAL_KIND`](#smt_qi_bound_global_kind) | `Option<u64>` | `None` | A |
| [`SMT_QI_BOUND_TRACE`](#smt_qi_bound_trace) | `Option<u64>` | `None` | A |
| [`SMT_QI_BOUND_TRACE_KIND`](#smt_qi_bound_trace_kind) | `Option<u64>` | `None` | A |
| [`SMT_QI_IGNORE_BUILTIN`](#smt_qi_ignore_builtin) | `bool` | `true` | A |
@@ -76,6 +79,7 @@
| [`USE_SMT_WRAPPER`](#use_smt_wrapper) | `bool` | `false` | A |
| [`VERIFICATION_DEADLINE`](#verification_deadline) | `Option<u64>` | `None` | A |
| [`VERIFY_ONLY_BASIC_BLOCK_PATH`](#verify_only_basic_block_path) | `Vec<String>` | `vec![]` | A |
| [`VERIFY_ONLY_DEFPATH`](#verify_only_defpath) | `Option<String>` | `None` | A |
| [`VERIFY_ONLY_PREAMBLE`](#verify_only_preamble) | `bool` | `false` | A |
| [`VIPER_BACKEND`](#viper_backend) | `String` | `"Silicon"` | A |
| [`VIPER_HOME`](#viper_home) | `Option<String>` | `None` | A |
@@ -357,6 +361,14 @@ When enabled, user messages are not printed. Otherwise, messages output into `st

> **Note:** `cargo prusti` sets this flag with `DEFAULT_PRUSTI_QUIET=true`.
## `REPORT_VIPER_MESSAGES`

When enabled for both server and client, certain supported Viper messages will be reported to the user.

## `VERIFY_ONLY_DEFPATH`

When set to the defpath of a local method, prusti will only verify the specified method. A fake error will be generated to avoid caching of a success.

## `SERVER_ADDRESS`

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.
@@ -373,6 +385,10 @@ Maximum amount of instantiated Viper verifiers the server will keep around for r

> **Note:** This does _not_ limit how many verification requests the server handles concurrently, only the size of what is essentially its verifier cache.
## `SHOW_IDE_INFO`

When enabled, we emit various json data structures containing information about the program, its encoding, and the results of the verification. This flag intended for prusti-assistant (IDE).

## `SIMPLIFY_ENCODING`

When enabled, the encoded program is simplified before it is passed to the Viper backend.
@@ -381,6 +397,10 @@ 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.

## `SKIP_VERIFICATION`

When enabled, verification will be skipped. Opposed to `NO_VERIFY`, this flag will cause fake errors to stop the compiler from caching the result.

## `SMT_QI_BOUND_GLOBAL`

If not `None`, checks that the number of global quantifier instantiations reported by the SMT wrapper is smaller than the specified bound.
@@ -468,6 +488,10 @@ Verify only the single execution path goes through the given basic blocks. All b

> **Note:** This option is only for debugging Prusti.
## `VERIFY_ONLY_DEFPATH`

When set to the defpath of a local method, prusti will only verify the specified method. A fake error will be generated to avoid caching of a success.

## `VERIFY_ONLY_PREAMBLE`

When enabled, only the preamble will be verified: domains, functions, and predicates.
64 changes: 63 additions & 1 deletion prusti-server/src/backend.rs
Original file line number Diff line number Diff line change
@@ -51,9 +51,71 @@ impl<'a> Backend<'a> {

stopwatch.start_next("viper verification");

verifier.verify(viper_program)
if config::report_viper_messages() {
verify_and_poll_msgs(verifier, context, viper_arc, viper_program, sender)
} else {
verifier.verify(viper_program)
}
})
}
}
}
}

fn verify_and_poll_msgs(
verifier: &mut viper::Verifier,
verification_context: &viper::VerificationContext,
viper_arc: &Arc<Viper>,
viper_program: viper::Program,
sender: mpsc::Sender<ServerMessage>,
) -> VerificationResultKind {
let mut kind = VerificationResultKind::Success;

// get the reporter global reference outside of the thread scope because it needs to
// be dropped by thread attached to the jvm. This is also why we pass it as reference
// and not per value
let env = &verification_context.env();
let jni = JniUtils::new(env);
let verifier_wrapper = silver::verifier::Verifier::with(env);
let reporter = jni.unwrap_result(verifier_wrapper.call_reporter(*verifier.verifier_instance()));
let rep_glob_ref = env.new_global_ref(reporter).unwrap();

debug!("Starting viper message polling thread");

// start thread for polling messages
thread::scope(|scope| {
let polling_thread = scope.spawn(|| polling_function(viper_arc, &rep_glob_ref, sender));
kind = verifier.verify(viper_program);
polling_thread.join().unwrap();
});
debug!("Viper message polling thread terminated");
kind
}

fn polling_function(
viper_arc: &Arc<Viper>,
rep_glob_ref: &jni::objects::GlobalRef,
sender: mpsc::Sender<ServerMessage>,
) {
let verification_context = viper_arc.attach_current_thread();
let env = verification_context.env();
let jni = JniUtils::new(env);
let reporter_instance = rep_glob_ref.as_obj();
let reporter_wrapper = silver::reporter::PollingReporter::with(env);
loop {
while reporter_wrapper
.call_hasNewMessage(reporter_instance)
.unwrap()
{
let msg = reporter_wrapper
.call_getNewMessage(reporter_instance)
.unwrap();
debug!("Polling thread received {}", jni.class_name(msg).as_str());
match jni.class_name(msg).as_str() {
"viper.silver.reporter.VerificationTerminationMessage" => return,
_ => (),
}
}
thread::sleep(time::Duration::from_millis(10));
}
}
1 change: 0 additions & 1 deletion prusti-server/src/lib.rs
Original file line number Diff line number Diff line change
@@ -188,7 +188,6 @@ fn handle_termination_message(
DUMMY_SP.into(),
)
.emit(env_diagnostic);
// .emit(&self.env.diagnostic);
*overall_result = VerificationResult::Failure;
}
}
14 changes: 14 additions & 0 deletions prusti-utils/src/config.rs
Original file line number Diff line number Diff line change
@@ -103,6 +103,7 @@ lazy_static::lazy_static! {
settings.set_default("quiet", false).unwrap();
settings.set_default("assert_timeout", 10_000).unwrap();
settings.set_default("smt_qi_eager_threshold", 1000).unwrap();
settings.set_default("report_viper_messages", false).unwrap();
settings.set_default("use_more_complete_exhale", true).unwrap();
settings.set_default("skip_unsupported_features", false).unwrap();
settings.set_default("internal_errors_as_warnings", false).unwrap();
@@ -173,6 +174,7 @@ lazy_static::lazy_static! {
// Flags specifically for Prusti-Assistant:
settings.set_default("show_ide_info", false).unwrap();
settings.set_default("skip_verification", false).unwrap();
settings.set_default::<Option<String>>("verify_only_defpath", None).unwrap();

// Get the list of all allowed flags.
let mut allowed_keys = get_keys(&settings);
@@ -506,6 +508,12 @@ pub fn smt_qi_eager_threshold() -> u64 {
read_setting("smt_qi_eager_threshold")
}

/// Whether to report the messages produced by the viper backend (e.g. quantifier instantiations,
/// quantifier triggers)
pub fn report_viper_messages() -> bool {
read_setting("report_viper_messages")
}

/// Maximum time (in milliseconds) for the verifier to spend on checks.
/// Set to None uses the verifier's default value. Maps to the verifier command-line
/// argument `--checkTimeout`.
@@ -1047,4 +1055,10 @@ pub fn show_ide_info() -> bool {
/// of issue #1261
pub fn skip_verification() -> bool {
read_setting("skip_verification")
}

/// Used for selective verification, can be passed a String containing
/// the DefPath of the method to be verified
pub fn verify_only_defpath() -> Option<String> {
read_setting("verify_only_defpath")
}
32 changes: 27 additions & 5 deletions prusti/src/callbacks.rs
Original file line number Diff line number Diff line change
@@ -29,6 +29,7 @@ use prusti_rustc_interface::{
session::{EarlyErrorHandler, Session},
span::DUMMY_SP,
};
use ::log::debug;

#[derive(Default)]
pub struct PrustiCompilerCalls;
@@ -199,11 +200,32 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {

// collect and output Information used by IDE:
if !config::no_verify() && !config::skip_verification() {
let verification_task = VerificationTask {
procedures: annotated_procedures,
types,
};
verify(env, def_spec, verification_task);
if let Some(target_def_path) = config::verify_only_defpath() {
// if we do selective verification, then definitely only
// for methods of the primary package. Check needed because
// of the fake_error, otherwise verification stops early
// with local dependencies
if is_primary_package {
let procedures = annotated_procedures
.into_iter()
.filter(|x| env.name.get_unique_item_name(*x) == target_def_path)
.collect();
debug!("selected procedures: {:?}", procedures);
let selective_task = VerificationTask { procedures, types };
// fake_error because otherwise a verification-success
// (for a single method for example) will cause this result
// to be cached by compiler at the moment
verify(env, def_spec, selective_task);
// FIXME: problematic because env is moved above
// fake_error(&env);
}
} else {
let verification_task = VerificationTask {
procedures: annotated_procedures,
types,
};
verify(env, def_spec, verification_task);
}
} else if config::skip_verification() && !config::no_verify() && is_primary_package {
// add a fake error, reason explained in issue #1261
fake_error(&env);

0 comments on commit 5270e09

Please sign in to comment.