From 9012c2f05395c450253821557dfc9198df7edcac Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Sun, 6 Nov 2022 09:36:37 +0100 Subject: [PATCH] Try disabling function unfolding triggers. --- prusti-server/src/verification_request.rs | 3 +++ .../tests/verify/fail/demos/append-sorted-error-3.rs | 2 ++ .../tests/verify/fail/pure-fn/wrong-quantifiers.rs | 2 ++ prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs | 2 ++ prusti-tests/tests/verify/pass/larger/first-final.rs | 2 ++ prusti-tests/tests/verify/pass/magic-wands/from_nth.rs | 2 ++ prusti-tests/tests/verify/pass/paper-examples/routes.rs | 2 ++ prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs | 2 ++ prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs | 2 ++ prusti-tests/tests/verify/pass/quick/routes.rs | 2 ++ prusti-utils/src/config.rs | 8 ++++++++ 11 files changed, 29 insertions(+) diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index 244b64c4cfb..8d2b34ba419 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -42,6 +42,9 @@ impl ViperBackendConfig { if config::use_more_complete_exhale() { verifier_args.push("--enableMoreCompleteExhale".to_string()); } + if config::disable_function_unfold_trigger() { + verifier_args.push("--disableFunctionUnfoldTrigger".to_string()); + } if config::counterexample() { verifier_args.push("--counterexample".to_string()); verifier_args.push("mapped".to_string()); diff --git a/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs b/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs index 62a8ae6e32d..1528c23399b 100644 --- a/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs +++ b/prusti-tests/tests/verify/fail/demos/append-sorted-error-3.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(box_patterns, box_syntax)] use prusti_contracts::*; diff --git a/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs b/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs index 433b6356142..27ec4b74946 100644 --- a/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs +++ b/prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(nll)] #![feature(box_patterns)] #![feature(box_syntax)] diff --git a/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs b/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs index 2a5ddda7995..e6f5c27682d 100644 --- a/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs +++ b/prusti-tests/tests/verify/pass/gitlab-issues/issue-39.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + //! Issue #39 "Suspicious `_old_old_1` variable name" #![feature(nll)] diff --git a/prusti-tests/tests/verify/pass/larger/first-final.rs b/prusti-tests/tests/verify/pass/larger/first-final.rs index 93cc1f50e75..6f5a242c591 100644 --- a/prusti-tests/tests/verify/pass/larger/first-final.rs +++ b/prusti-tests/tests/verify/pass/larger/first-final.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(box_patterns)] //! An adaptation of the example from diff --git a/prusti-tests/tests/verify/pass/magic-wands/from_nth.rs b/prusti-tests/tests/verify/pass/magic-wands/from_nth.rs index f45b77ba8ef..5b5c7197419 100644 --- a/prusti-tests/tests/verify/pass/magic-wands/from_nth.rs +++ b/prusti-tests/tests/verify/pass/magic-wands/from_nth.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(box_patterns)] use prusti_contracts::*; diff --git a/prusti-tests/tests/verify/pass/paper-examples/routes.rs b/prusti-tests/tests/verify/pass/paper-examples/routes.rs index 8d67d5a9a11..33278387b6c 100644 --- a/prusti-tests/tests/verify/pass/paper-examples/routes.rs +++ b/prusti-tests/tests/verify/pass/paper-examples/routes.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(box_syntax, box_patterns)] use prusti_contracts::*; diff --git a/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs b/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs index ce18b014e6a..5c65dee337b 100644 --- a/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs +++ b/prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(nll)] #![feature(box_patterns)] #![feature(box_syntax)] diff --git a/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs b/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs index dd5b6146cc4..9fb92ee7b20 100644 --- a/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs +++ b/prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(nll)] #![feature(box_patterns)] #![feature(box_syntax)] diff --git a/prusti-tests/tests/verify/pass/quick/routes.rs b/prusti-tests/tests/verify/pass/quick/routes.rs index e61d28b896b..d3b569b4c5b 100644 --- a/prusti-tests/tests/verify/pass/quick/routes.rs +++ b/prusti-tests/tests/verify/pass/quick/routes.rs @@ -1,3 +1,5 @@ +// compile-flags: -Pdisable_function_unfold_trigger=false + #![feature(box_syntax, box_patterns)] use prusti_contracts::*; diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 00c4b046b33..e661eb2e14d 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -102,6 +102,7 @@ lazy_static::lazy_static! { settings.set_default("assert_timeout", 10_000).unwrap(); settings.set_default("smt_qi_eager_threshold", 1000).unwrap(); settings.set_default("use_more_complete_exhale", true).unwrap(); + settings.set_default("disable_function_unfold_trigger", true).unwrap(); settings.set_default("skip_unsupported_features", false).unwrap(); settings.set_default("internal_errors_as_warnings", false).unwrap(); settings.set_default("allow_unreachable_unsupported_code", false).unwrap(); @@ -510,6 +511,13 @@ pub fn use_more_complete_exhale() -> bool { read_setting("use_more_complete_exhale") } +/// When enabled, disables unfolding of functions together with unfolding +/// predicates. Equivalent to the verifier command-line argument +/// `--disableFunctionUnfoldTrigger`. +pub fn disable_function_unfold_trigger() -> bool { + read_setting("disable_function_unfold_trigger") +} + /// When enabled, prints the items collected for verification. pub fn print_collected_verification_items() -> bool { read_setting("print_collected_verification_items")