Skip to content

Instantly share code, notes, and snippets.

@seyyedaliayati
Created February 21, 2023 15:49
Show Gist options
  • Save seyyedaliayati/030c9857f99763b178b33e7b5487d697 to your computer and use it in GitHub Desktop.
Save seyyedaliayati/030c9857f99763b178b33e7b5487d697 to your computer and use it in GitHub Desktop.
pub struct BoogieOptions {
/// Path to the boogie executable.
pub boogie_exe: String,
/// Use experimental boogie exe found via env var EXP_BOOGIE_EXE.
pub use_exp_boogie: bool,
/// Path to the z3 executable.
pub z3_exe: String,
/// Whether to use cvc5.
pub use_cvc5: bool,
/// Path to the cvc5 executable.
pub cvc5_exe: String,
/// Whether to generate debug trace code.
pub debug_trace: bool,
/// List of flags to pass on to boogie.
pub boogie_flags: Vec<String>,
/// Whether to use native array theory.
pub use_array_theory: bool,
/// Whether to produce an SMT file for each verification problem.
pub generate_smt: bool,
/// Whether native instead of stratified equality should be used.
pub native_equality: bool,
/// A string determining the type of requires used for parameter type checks. Can be
/// `"requires"` or `"free requires`".
pub type_requires: String,
/// The depth until which stratified functions are expanded.
pub stratification_depth: usize,
/// A string to be used to inline a function of medium size. Can be empty or `{:inline}`.
pub aggressive_func_inline: String,
/// A string to be used to inline a function of small size. Can be empty or `{:inline}`.
pub func_inline: String,
/// A bound to apply to the length of serialization results.
pub serialize_bound: usize,
/// How many times to call the prover backend for the verification problem. This is used for
/// benchmarking.
pub bench_repeat: usize,
/// Whether to use the sequence theory as the internal representation for $Vector type.
pub vector_using_sequences: bool,
/// A seed for the prover.
pub random_seed: usize,
/// The number of cores to use for parallel processing of verification conditions.
pub proc_cores: usize,
/// A (soft) timeout for the solver, per verification condition, in seconds.
pub vc_timeout: usize,
/// Whether Boogie output and log should be saved.
pub keep_artifacts: bool,
/// Eager threshold for quantifier instantiation.
pub eager_threshold: usize,
/// Lazy threshold for quantifier instantiation.
pub lazy_threshold: usize,
/// Whether to use the new Boogie `{:debug ..}` attribute for tracking debug values.
pub stable_test_output: bool,
/// Number of Boogie instances to be run concurrently.
pub num_instances: usize,
/// Whether to run Boogie instances sequentially.
pub sequential_task: bool,
/// A hard timeout for boogie execution; if the process does not terminate within
/// this time frame, it will be killed. Zero for no timeout.
pub hard_timeout_secs: u64,
/// What vector theory to use.
pub vector_theory: VectorTheory,
/// Whether to generate a z3 trace file and where to put it.
pub z3_trace_file: Option<String>,
/// Options to define user-custom native funs.
pub custom_natives: Option<CustomNativeOptions>,
/// Number of iterations to unroll loops.
pub loop_unroll: Option<u64>,
/// Optional aggregate function names for native methods implementing mutable borrow semantics
pub borrow_aggregates: Vec<BorrowAggregate>,
}
// Default values for boogie options:
impl Default for BoogieOptions {
fn default() -> Self {
Self {
bench_repeat: 1,
boogie_exe: read_env_var("BOOGIE_EXE"),
use_exp_boogie: false,
z3_exe: read_env_var("Z3_EXE"),
use_cvc5: false,
cvc5_exe: read_env_var("CVC5_EXE"),
boogie_flags: vec![],
debug_trace: false,
use_array_theory: false,
generate_smt: false,
native_equality: false,
type_requires: "free requires".to_owned(),
stratification_depth: 6,
aggressive_func_inline: "".to_owned(),
func_inline: "{:inline}".to_owned(),
serialize_bound: 0,
vector_using_sequences: false,
random_seed: 1,
proc_cores: 4,
vc_timeout: 40,
keep_artifacts: false,
eager_threshold: 100,
lazy_threshold: 100,
stable_test_output: false,
num_instances: 1,
sequential_task: false,
hard_timeout_secs: 0,
vector_theory: VectorTheory::BoogieArray,
z3_trace_file: None,
custom_natives: None,
loop_unroll: None,
borrow_aggregates: vec![],
}
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment