From e3d717fda254f17376ecf13c31524cd87bcc751e Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 18 Dec 2024 12:43:45 -0300 Subject: [PATCH] Add flag to configure smt solver (#953) --- book/src/guide/run.md | 1 + crates/flux-config/src/lib.rs | 93 +++++++++--- crates/flux-driver/locales/en-US.ftl | 4 +- crates/flux-driver/src/collector/mod.rs | 135 ++++++++---------- crates/flux-infer/src/fixpoint_encoding.rs | 6 +- crates/flux-infer/src/infer.rs | 20 ++- crates/flux-middle/src/fhir.rs | 26 ---- crates/flux-middle/src/global_env.rs | 30 ++-- crates/flux-middle/src/lib.rs | 3 +- crates/flux-refineck/src/checker.rs | 5 +- crates/flux-refineck/src/invariants.rs | 6 +- crates/flux-refineck/src/lib.rs | 8 +- lib/flux-attrs/src/lib.rs | 2 +- lib/flux-rs/src/lib.rs | 8 +- lib/liquid-fixpoint/src/lib.rs | 17 +++ tests/tests/neg/config/test-config00.rs | 2 +- tests/tests/neg/config/test-config01.rs | 2 +- tests/tests/neg/config/test-config02.rs | 2 +- tests/tests/neg/config/test-config03.rs | 2 +- tests/tests/neg/config/test-config04.rs | 2 +- tests/tests/neg/surface/binop_overflow.rs | 2 +- tests/tests/neg/surface/check_overflow00.rs | 2 +- tests/tests/neg/surface/check_overflow01.rs | 2 +- tests/tests/neg/surface/check_overflow02.rs | 4 +- tests/tests/neg/surface/check_overflow03.rs | 2 +- .../neg/surface/int_bounds_invariants.rs | 2 +- tests/tests/neg/surface/scrape00.rs | 2 +- tests/tests/neg/surface/trait03.rs | 2 +- tests/tests/neg/surface/unop_overflow.rs | 2 +- tests/tests/pos/surface/assume_invariant00.rs | 2 +- tests/tests/pos/surface/binop_overflow.rs | 2 +- tests/tests/pos/surface/check_overflow00.rs | 2 +- tests/tests/pos/surface/check_overflow01.rs | 2 +- tests/tests/pos/surface/check_overflow02.rs | 4 +- tests/tests/pos/surface/check_overflow03.rs | 2 +- tests/tests/pos/surface/check_overflow05.rs | 4 +- .../pos/surface/int_bounds_invariants.rs | 2 +- tests/tests/pos/surface/kmp_overflow.rs | 2 +- .../pos/surface/loop_abstract_refinement.rs | 2 +- .../pos/surface/polymorphic_qualifier.rs | 2 +- tests/tests/pos/surface/scrape00.rs | 2 +- tests/tests/pos/surface/scrape01.rs | 2 +- tests/tests/pos/surface/unop_overflow.rs | 2 +- 43 files changed, 227 insertions(+), 199 deletions(-) diff --git a/book/src/guide/run.md b/book/src/guide/run.md index 51af7491f7..274bccc70e 100644 --- a/book/src/guide/run.md +++ b/book/src/guide/run.md @@ -159,6 +159,7 @@ You can set various `env` variables to customize the behavior of `flux`. - `FLUX_CHECK_OVERFLOW=1` checks for over and underflow on arithmetic integer operations, default `0`. When set to `0`, it still checks for underflow on unsigned integer subtraction. +- `FLUX_SOLVER=z3` Can be either `z3` or `cvc5`. ### Config file diff --git a/crates/flux-config/src/lib.rs b/crates/flux-config/src/lib.rs index cb5ef96c31..94b8c7ab06 100644 --- a/crates/flux-config/src/lib.rs +++ b/crates/flux-config/src/lib.rs @@ -1,4 +1,4 @@ -use std::{io::Read, path::PathBuf, sync::LazyLock}; +use std::{io::Read, path::PathBuf, str::FromStr, sync::LazyLock}; use config::{Environment, File}; use serde::Deserialize; @@ -55,22 +55,20 @@ pub fn cache_path() -> PathBuf { log_dir().join(&CONFIG.cache_file) } -pub fn check_overflow() -> bool { +fn check_overflow() -> bool { CONFIG.check_overflow } -pub fn scrape_quals() -> bool { +fn scrape_quals() -> bool { CONFIG.scrape_quals } -pub fn catch_bugs() -> bool { - CONFIG.catch_bugs +fn solver() -> SmtSolver { + CONFIG.solver } -#[derive(Debug, Clone, Copy)] -pub struct CrateConfig { - pub check_overflow: bool, - pub scrape_quals: bool, +pub fn catch_bugs() -> bool { + CONFIG.catch_bugs } #[derive(Deserialize)] @@ -90,6 +88,7 @@ struct Config { cache_file: String, check_overflow: bool, scrape_quals: bool, + solver: SmtSolver, } #[derive(Default)] @@ -151,6 +150,71 @@ impl TryFrom for PointerWidth { } } +/// Options that change the behavior of refinement type inference locally +#[derive(Clone, Copy, Debug)] +pub struct InferOpts { + /// Enable overflow checking. This affects the signature of primitive operations and the + /// invariants assumed for primitive types. + pub check_overflow: bool, + /// Whether qualifiers should be scraped from the constraint. + pub scrape_quals: bool, + pub solver: SmtSolver, +} + +impl From for InferOpts { + fn from(opts: PartialInferOpts) -> Self { + InferOpts { + check_overflow: opts.check_overflow.unwrap_or_else(check_overflow), + scrape_quals: opts.scrape_quals.unwrap_or_else(scrape_quals), + solver: opts.solver.unwrap_or_else(solver), + } + } +} + +#[derive(Clone, Copy, Default, Deserialize, Debug)] +pub struct PartialInferOpts { + pub check_overflow: Option, + pub scrape_quals: Option, + pub solver: Option, +} + +impl PartialInferOpts { + pub fn merge(&mut self, other: &Self) { + self.check_overflow = self.check_overflow.or(other.check_overflow); + self.scrape_quals = self.scrape_quals.or(other.scrape_quals); + self.solver = self.solver.or(other.solver); + } +} + +#[derive(Clone, Copy, Debug, Deserialize, Default)] +#[serde(try_from = "String")] +pub enum SmtSolver { + #[default] + Z3, + CVC5, +} + +impl FromStr for SmtSolver { + type Err = &'static str; + + fn from_str(s: &str) -> Result { + let s = s.to_ascii_lowercase(); + match s.as_str() { + "z3" => Ok(SmtSolver::Z3), + "cvc5" => Ok(SmtSolver::CVC5), + _ => Err("backend must be one of `z3` or `cvc5`"), + } + } +} + +impl TryFrom for SmtSolver { + type Error = &'static str; + + fn try_from(value: String) -> Result { + value.parse() + } +} + static CONFIG: LazyLock = LazyLock::new(|| { fn build() -> Result { let mut config_builder = config::Config::builder() @@ -163,14 +227,15 @@ static CONFIG: LazyLock = LazyLock::new(|| { .set_default("dump_fhir", false)? .set_default("dump_rty", false)? .set_default("catch_bugs", false)? - .set_default("check_asserts", "assume")? .set_default("pointer_width", "64")? .set_default("check_def", "")? .set_default("check_files", "")? .set_default("cache", false)? .set_default("cache_file", "cache.json")? .set_default("check_overflow", false)? - .set_default("scrape_quals", false)?; + .set_default("scrape_quals", false)? + .set_default("solver", "z3")?; + // Config comes first, environment settings override it. if let Some(config_path) = CONFIG_PATH.as_ref() { config_builder = config_builder.add_source(File::from(config_path.clone())); @@ -213,9 +278,3 @@ pub static CONFIG_FILE: LazyLock = LazyLock::new(|| { toml::from_str("").unwrap() } }); - -impl Default for CrateConfig { - fn default() -> Self { - Self { check_overflow: check_overflow(), scrape_quals: scrape_quals() } - } -} diff --git a/crates/flux-driver/locales/en-US.ftl b/crates/flux-driver/locales/en-US.ftl index 48fb33a595..e96b5fdb97 100644 --- a/crates/flux-driver/locales/en-US.ftl +++ b/crates/flux-driver/locales/en-US.ftl @@ -4,8 +4,8 @@ driver_duplicated_attr = driver_invalid_attr = invalid flux attribute -driver_cfg_error = - invalid flux configuration: {$message} +driver_invalid_attr_map = + invalid attribute: {$message} driver_syntax_err = syntax error: {$msg} diff --git a/crates/flux-driver/src/collector/mod.rs b/crates/flux-driver/src/collector/mod.rs index eacbbf248a..09afc407ad 100644 --- a/crates/flux-driver/src/collector/mod.rs +++ b/crates/flux-driver/src/collector/mod.rs @@ -8,10 +8,10 @@ use flux_common::{ result::{ErrorCollector, ResultExt}, tracked_span_assert_eq, }; -use flux_config::{self as config, CrateConfig}; +use flux_config::{self as config, PartialInferOpts, SmtSolver}; use flux_errors::{Errors, FluxSession}; use flux_middle::{ - fhir::{CheckOverflow, Ignored, Trusted}, + fhir::{Ignored, Trusted}, Specs, }; use flux_syntax::{surface, ParseResult, ParseSess}; @@ -85,13 +85,12 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { fn collect_crate(&mut self) -> Result { let mut attrs = self.parse_attrs_and_report_dups(CRATE_DEF_ID)?; self.collect_ignore_and_trusted(&mut attrs, CRATE_DEF_ID); - self.collect_check_overflow(&mut attrs, CRATE_DEF_ID); + self.collect_infer_opts(&mut attrs, CRATE_DEF_ID); self.specs .flux_items_by_parent .entry(CRATE_OWNER_ID) .or_default() .extend(attrs.items()); - self.specs.crate_config = attrs.crate_config(); Ok(()) } @@ -100,7 +99,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?; self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id); - self.collect_check_overflow(&mut attrs, owner_id.def_id); + self.collect_infer_opts(&mut attrs, owner_id.def_id); match &item.kind { ItemKind::Fn(..) => { @@ -147,7 +146,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?; self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id); - self.collect_check_overflow(&mut attrs, owner_id.def_id); + self.collect_infer_opts(&mut attrs, owner_id.def_id); if let rustc_hir::TraitItemKind::Fn(_, _) = trait_item.kind { self.collect_fn_spec(owner_id, attrs)?; } @@ -160,7 +159,7 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { let mut attrs = self.parse_attrs_and_report_dups(owner_id.def_id)?; self.collect_ignore_and_trusted(&mut attrs, owner_id.def_id); - self.collect_check_overflow(&mut attrs, owner_id.def_id); + self.collect_infer_opts(&mut attrs, owner_id.def_id); if let ImplItemKind::Fn(..) = &impl_item.kind { self.collect_fn_spec(owner_id, attrs)?; @@ -442,12 +441,12 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { ("constant", AttrArgs::Delimited(dargs)) => { self.parse(dargs, ParseSess::parse_constant_info, FluxAttrKind::Constant)? } - ("cfg", AttrArgs::Delimited(..)) => { - let crate_cfg = FluxAttrCFG::parse_cfg(attr_item) + ("opts", AttrArgs::Delimited(..)) => { + let opts = AttrMap::parse(attr_item) .emit(&self.errors)? - .try_into_crate_cfg() + .try_into_infer_opts() .emit(&self.errors)?; - FluxAttrKind::CrateConfig(crate_cfg) + FluxAttrKind::InferOpts(opts) } ("ignore", _) => { FluxAttrKind::Ignore( @@ -470,13 +469,6 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { .into(), ) } - ("check_overflow", _) => { - FluxAttrKind::CheckOverflow( - parse_yes_no_with_reason(attr_item) - .map_err(|_| invalid_attr_err(self))? - .into(), - ) - } ("opaque", AttrArgs::Empty) => FluxAttrKind::Opaque, ("extern_spec", AttrArgs::Empty) => FluxAttrKind::ExternSpec, ("should_fail", AttrArgs::Empty) => FluxAttrKind::ShouldFail, @@ -526,9 +518,9 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> { } } - fn collect_check_overflow(&mut self, attrs: &mut FluxAttrs, def_id: LocalDefId) { - if let Some(check_overflow) = attrs.check_overflow() { - self.specs.check_overflows.insert(def_id, check_overflow); + fn collect_infer_opts(&mut self, attrs: &mut FluxAttrs, def_id: LocalDefId) { + if let Some(check_overflow) = attrs.infer_opts() { + self.specs.infer_opts.insert(def_id, check_overflow); } } } @@ -602,12 +594,11 @@ enum FluxAttrKind { Field(surface::Ty), Constant(surface::ConstantInfo), Variant(surface::VariantDef), - CrateConfig(config::CrateConfig), + InferOpts(config::PartialInferOpts), Invariant(surface::Expr), Ignore(Ignored), ShouldFail, ExternSpec, - CheckOverflow(CheckOverflow), } macro_rules! read_flag { @@ -717,8 +708,8 @@ impl FluxAttrs { read_attr!(self, Variant) } - fn crate_config(&mut self) -> Option { - read_attr!(self, CrateConfig) + fn infer_opts(&mut self) -> Option { + read_attr!(self, InferOpts) } fn invariants(&mut self) -> Vec { @@ -732,10 +723,6 @@ impl FluxAttrs { fn should_fail(&self) -> bool { read_flag!(self, ShouldFail) } - - fn check_overflow(&mut self) -> Option { - read_attr!(self, CheckOverflow) - } } impl FluxAttrKind { @@ -755,96 +742,99 @@ impl FluxAttrKind { FluxAttrKind::Constant(_) => attr_name!(Constant), FluxAttrKind::Variant(_) => attr_name!(Variant), FluxAttrKind::TypeAlias(_) => attr_name!(TypeAlias), - FluxAttrKind::CrateConfig(_) => attr_name!(CrateConfig), + FluxAttrKind::InferOpts(_) => attr_name!(InferOpts), FluxAttrKind::Ignore(_) => attr_name!(Ignore), FluxAttrKind::Invariant(_) => attr_name!(Invariant), FluxAttrKind::ShouldFail => attr_name!(ShouldFail), FluxAttrKind::ExternSpec => attr_name!(ExternSpec), - FluxAttrKind::CheckOverflow(_) => attr_name!(CheckOverflow), } } } #[derive(Debug)] -struct CFGSetting { +struct AttrMapValue { setting: Symbol, span: Span, } #[derive(Debug)] -struct FluxAttrCFG { - map: HashMap, +struct AttrMap { + map: HashMap, } macro_rules! try_read_setting { - ($self:expr, $setting:ident, $type:ident, $cfg:expr) => { - if let Some(CFGSetting { setting, span }) = $self.map.remove(stringify!($setting)) { - let parse_result = setting.as_str().parse::<$type>(); - if let Ok(val) = parse_result { - $cfg.$setting = val; + ($self:expr, $setting:ident, $type:ident, $cfg:expr) => {{ + let val = + if let Some(AttrMapValue { setting, span }) = $self.map.remove(stringify!($setting)) { + let parse_result = setting.as_str().parse::<$type>(); + if let Ok(val) = parse_result { + Some(val) + } else { + return Err(errors::AttrMapErr { + span, + message: format!( + "incorrect type in value for setting `{}`, expected {}", + stringify!($setting), + stringify!($type) + ), + }); + } } else { - return Err(errors::CFGError { - span, - message: format!( - "incorrect type in value for setting `{}`, expected {}", - stringify!($setting), - stringify!($type) - ), - }); - } - } - }; + None + }; + $cfg.$setting = val; + }}; } -type CFGResult = std::result::Result; +type AttrMapErr = std::result::Result; -impl FluxAttrCFG { +impl AttrMap { // TODO: Ugly that we have to access the collector for error reporting - fn parse_cfg(attr_item: &AttrItem) -> CFGResult { - let mut cfg = Self { map: HashMap::new() }; + fn parse(attr_item: &AttrItem) -> AttrMapErr { + let mut map = Self { map: HashMap::new() }; let meta_item_kind = attr_item.meta_kind(); match meta_item_kind { Some(MetaItemKind::List(items)) => { for item in items { - cfg.parse_cfg_item(&item)?; + map.parse_entry(&item)?; } } _ => { - return Err(errors::CFGError { + return Err(errors::AttrMapErr { span: attr_item.span(), message: "bad syntax".to_string(), }) } }; - Ok(cfg) + Ok(map) } - fn parse_cfg_item(&mut self, nested_item: &MetaItemInner) -> CFGResult { + fn parse_entry(&mut self, nested_item: &MetaItemInner) -> AttrMapErr { match nested_item { MetaItemInner::MetaItem(item) => { let name = item.name_or_empty().to_ident_string(); let span = item.span; if !name.is_empty() { if self.map.contains_key(&name) { - return Err(errors::CFGError { + return Err(errors::AttrMapErr { span, - message: format!("duplicated setting `{name}`"), + message: format!("duplicated key `{name}`"), }); } // TODO: support types of values other than strings let value = item.name_value_literal().ok_or_else(|| { - errors::CFGError { span, message: "unsupported value".to_string() } + errors::AttrMapErr { span, message: "unsupported value".to_string() } })?; - let setting = CFGSetting { setting: value.symbol, span: item.span }; + let setting = AttrMapValue { setting: value.symbol, span: item.span }; self.map.insert(name, setting); return Ok(()); } - Err(errors::CFGError { span, message: "bad setting name".to_string() }) + Err(errors::AttrMapErr { span, message: "bad setting name".to_string() }) } MetaItemInner::Lit(_) => { - Err(errors::CFGError { + Err(errors::AttrMapErr { span: nested_item.span(), message: "unsupported item".to_string(), }) @@ -852,19 +842,20 @@ impl FluxAttrCFG { } } - fn try_into_crate_cfg(&mut self) -> CFGResult { - let mut crate_config = CrateConfig::default(); - try_read_setting!(self, check_overflow, bool, crate_config); - try_read_setting!(self, scrape_quals, bool, crate_config); + fn try_into_infer_opts(&mut self) -> AttrMapErr { + let mut infer_opts = PartialInferOpts::default(); + try_read_setting!(self, check_overflow, bool, infer_opts); + try_read_setting!(self, scrape_quals, bool, infer_opts); + try_read_setting!(self, solver, SmtSolver, infer_opts); if let Some((name, setting)) = self.map.iter().next() { - return Err(errors::CFGError { + return Err(errors::AttrMapErr { span: setting.span, message: format!("invalid crate cfg keyword `{name}`"), }); } - Ok(crate_config) + Ok(infer_opts) } } @@ -891,8 +882,8 @@ mod errors { } #[derive(Diagnostic)] - #[diag(driver_cfg_error, code = E0999)] - pub(super) struct CFGError { + #[diag(driver_invalid_attr_map, code = E0999)] + pub(super) struct AttrMapErr { #[primary_span] pub span: Span, pub message: String, diff --git a/crates/flux-infer/src/fixpoint_encoding.rs b/crates/flux-infer/src/fixpoint_encoding.rs index bcc122bee6..34819f202b 100644 --- a/crates/flux-infer/src/fixpoint_encoding.rs +++ b/crates/flux-infer/src/fixpoint_encoding.rs @@ -22,7 +22,7 @@ use flux_middle::{ MaybeExternId, }; use itertools::Itertools; -use liquid_fixpoint::FixpointResult; +use liquid_fixpoint::{FixpointResult, SmtSolver}; use rustc_data_structures::{ fx::FxIndexMap, unord::{UnordMap, UnordSet}, @@ -350,6 +350,7 @@ where cache: &mut FixQueryCache, constraint: fixpoint::Constraint, scrape_quals: bool, + solver: SmtSolver, ) -> QueryResult> { // skip checking trivial constraints if !constraint.is_concrete() { @@ -397,6 +398,7 @@ where constraint, qualifiers, scrape_quals, + solver, data_decls: self.scx.into_data_decls(), }; if config::dump_constraint() { @@ -431,7 +433,7 @@ where } let result = task .run() - .unwrap_or_else(|err| tracked_span_bug!("failed to run fixpoint {err:?}")); + .unwrap_or_else(|err| tracked_span_bug!("failed to run fixpoint: {err:?}")); if config::is_cache_enabled() { cache.insert(key, hash, result.clone()); diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 7c7e54440c..8e3acfb65d 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -1,7 +1,7 @@ use std::{cell::RefCell, fmt, iter}; use flux_common::{bug, dbg, tracked_span_assert_eq, tracked_span_dbg_assert_eq}; -use flux_config as config; +use flux_config::{self as config, InferOpts}; use flux_middle::{ global_env::GlobalEnv, queries::{QueryErr, QueryResult}, @@ -75,16 +75,6 @@ pub enum ConstrReason { Other, } -/// Options that change the behavior of refinement type inference locally -#[derive(Clone, Copy)] -pub struct InferOpts { - /// Enable overflow checking. This affects the signature of primitive operations and the - /// invariants assumed for primitive types. - pub check_overflow: bool, - /// Whether qualifiers should be scraped from the constraint. - pub scrape_quals: bool, -} - pub struct InferCtxtRoot<'genv, 'tcx> { pub genv: GlobalEnv<'genv, 'tcx>, inner: RefCell, @@ -197,7 +187,13 @@ impl<'genv, 'tcx> InferCtxtRoot<'genv, 'tcx> { let mut fcx = FixpointCtxt::new(self.genv, def_id, kvars); let cstr = refine_tree.into_fixpoint(&mut fcx)?; - fcx.check(cache, cstr, self.opts.scrape_quals) + + let backend = match self.opts.solver { + flux_config::SmtSolver::Z3 => liquid_fixpoint::SmtSolver::Z3, + flux_config::SmtSolver::CVC5 => liquid_fixpoint::SmtSolver::CVC5, + }; + + fcx.check(cache, cstr, self.opts.scrape_quals, backend) } pub fn split(self) -> (RefineTree, KVarGen) { diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index a5519fcabd..7d2c890fef 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -94,32 +94,6 @@ impl From for Trusted { } } -/// A boolean-like enum used to mark whether some code should be checked for overflows -#[derive(Debug, Eq, PartialEq, Copy, Clone)] -pub enum CheckOverflow { - Yes, - No, -} - -impl CheckOverflow { - pub fn to_bool(self) -> bool { - match self { - CheckOverflow::Yes => true, - CheckOverflow::No => false, - } - } -} - -impl From for CheckOverflow { - fn from(value: bool) -> Self { - if value { - CheckOverflow::Yes - } else { - CheckOverflow::No - } - } -} - #[derive(Debug, Clone, Copy)] pub struct Generics<'fhir> { pub params: &'fhir [GenericParam<'fhir>], diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 979699345f..32e9ee66ae 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -2,7 +2,7 @@ use std::{alloc, ptr, rc::Rc, slice}; use flux_arc_interner::List; use flux_common::{bug, result::ErrorEmitter}; -use flux_config::CrateConfig; +use flux_config as config; use flux_errors::FluxSession; use flux_rustc_bridge::{self, lowering::Lower, mir, ty}; use rustc_hash::FxHashSet; @@ -413,18 +413,16 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { } } - /// Transitively follow the parent-chain of `def_id` to find the first containing item with an - /// explicit `#[flux::check_overflow(..)]` annotation and return whether that item has an - /// explicitly annotation and whether it requires an overflow check or not. - /// If no explicit annotation is found, return the default for the crate - pub fn check_overflow(self, def_id: LocalDefId) -> bool { - self.traverse_parents(def_id, |did| self.collect_specs().check_overflows.get(&did)) - .map_or_else(|| self.crate_config().check_overflow, |x| x.to_bool()) - } - - // TODO(nilehmann) allow this to be overridden per function - pub fn scrape_quals(self, _def_id: LocalDefId) -> bool { - self.crate_config().scrape_quals + pub fn infer_opts(self, def_id: LocalDefId) -> config::InferOpts { + let mut opts = config::PartialInferOpts::default(); + let specs = self.collect_specs(); + self.traverse_parents(def_id, |did| { + if let Some(o) = specs.infer_opts.get(&did) { + opts.merge(o); + } + None:: + }); + opts.into() } /// Transitively follow the parent-chain of `def_id` to find the first containing item with an @@ -472,7 +470,7 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { fn traverse_parents( self, mut def_id: LocalDefId, - f: impl Fn(LocalDefId) -> Option, + mut f: impl FnMut(LocalDefId) -> Option, ) -> Option { loop { if let Some(v) = f(def_id) { @@ -486,10 +484,6 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { } } } - - pub fn crate_config(self) -> CrateConfig { - self.collect_specs().crate_config.unwrap_or_default() - } } #[derive(Clone, Copy)] diff --git a/crates/flux-middle/src/lib.rs b/crates/flux-middle/src/lib.rs index 23f6b0a475..42e6c68512 100644 --- a/crates/flux-middle/src/lib.rs +++ b/crates/flux-middle/src/lib.rs @@ -373,8 +373,7 @@ pub struct Specs { pub ignores: UnordMap, pub trusted: UnordMap, pub trusted_impl: UnordMap, - pub check_overflows: UnordMap, - pub crate_config: Option, + pub infer_opts: UnordMap, pub should_fail: UnordSet, /// Set of dummy items generated by the extern spec macro we must completely ignore. This is /// not the same as [ignored items] because, for ignored items, we still need to return errors diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 3ea67d94df..5d1e71cfa4 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1,11 +1,10 @@ use std::{collections::hash_map::Entry, iter}; use flux_common::{bug, dbg, index::IndexVec, iter::IterExt, tracked_span_bug}; -use flux_config as config; +use flux_config::{self as config, InferOpts}; use flux_infer::{ infer::{ - ConstrReason, GlobalEnvExt as _, InferCtxt, InferCtxtRoot, InferOpts, InferResult, - SubtypeReason, + ConstrReason, GlobalEnvExt as _, InferCtxt, InferCtxtRoot, InferResult, SubtypeReason, }, refine_tree::{RefineCtxtTrace, Snapshot}, }; diff --git a/crates/flux-refineck/src/invariants.rs b/crates/flux-refineck/src/invariants.rs index 0e05912cd4..ee9821f846 100644 --- a/crates/flux-refineck/src/invariants.rs +++ b/crates/flux-refineck/src/invariants.rs @@ -1,8 +1,9 @@ use flux_common::{iter::IterExt, result::ResultExt}; +use flux_config::InferOpts; use flux_errors::ErrorGuaranteed; use flux_infer::{ fixpoint_encoding::FixQueryCache, - infer::{ConstrReason, GlobalEnvExt, InferOpts, Tag}, + infer::{ConstrReason, GlobalEnvExt, Tag}, }; use flux_middle::{fhir, global_env::GlobalEnv, rty, MaybeExternId}; use rustc_infer::infer::TyCtxtInferExt; @@ -24,8 +25,7 @@ pub fn check_invariants( // and off locally. Then we consider an overflow-checked `T` distinct from a non-checked one and // error/warn in case of a mismatch: overflow-checked types can flow to non-checked code but not // the other way around. - let opts = - InferOpts { check_overflow: genv.check_overflow(def_id.local_id()), scrape_quals: false }; + let opts = genv.infer_opts(def_id.local_id()); adt_def .invariants() .iter() diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs index 22ef53cf16..f5dc579e2e 100644 --- a/crates/flux-refineck/src/lib.rs +++ b/crates/flux-refineck/src/lib.rs @@ -35,7 +35,7 @@ use checker::{trait_impl_subtyping, Checker}; use flux_common::{dbg, result::ResultExt as _}; use flux_infer::{ fixpoint_encoding::FixQueryCache, - infer::{ConstrReason, InferOpts, SubtypeReason, Tag}, + infer::{ConstrReason, SubtypeReason, Tag}, }; use flux_macros::fluent_messages; use flux_middle::{ @@ -106,11 +106,7 @@ pub fn check_fn( return Ok(()); } - // Since we still want the global check overflow, just override it here if it's set - let opts = InferOpts { - check_overflow: genv.check_overflow(local_id), - scrape_quals: genv.scrape_quals(local_id), - }; + let opts = genv.infer_opts(local_id); dbg::check_fn_span!(genv.tcx(), local_id).in_scope(|| { let ghost_stmts = compute_ghost_statements(genv, local_id) diff --git a/lib/flux-attrs/src/lib.rs b/lib/flux-attrs/src/lib.rs index c2f85b1222..046eb4e282 100644 --- a/lib/flux-attrs/src/lib.rs +++ b/lib/flux-attrs/src/lib.rs @@ -17,7 +17,7 @@ pub const FLUX_ATTRS: &[&str] = &[ "trusted_impl", "variant", "should_fail", - "check_overflow", + "opts", ]; pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream { diff --git a/lib/flux-rs/src/lib.rs b/lib/flux-rs/src/lib.rs index d3d2351cd3..f00c9587bd 100644 --- a/lib/flux-rs/src/lib.rs +++ b/lib/flux-rs/src/lib.rs @@ -45,8 +45,8 @@ pub fn opaque(attr: TokenStream, tokens: TokenStream) -> TokenStream { } #[proc_macro_attribute] -pub fn check_overflow(attr: TokenStream, tokens: TokenStream) -> TokenStream { - attr_impl::check_overflow(attr, tokens) +pub fn opts(attr: TokenStream, tokens: TokenStream) -> TokenStream { + attr_impl::opts(attr, tokens) } #[proc_macro_attribute] @@ -128,7 +128,7 @@ mod attr_sysroot { constant, invariant, opaque, - check_overflow, + opts, trusted, trusted_impl, generics, @@ -172,7 +172,7 @@ mod attr_dummy { invariant, constant, opaque, - check_overflow, + opts, trusted, trusted_impl, generics, diff --git a/lib/liquid-fixpoint/src/lib.rs b/lib/liquid-fixpoint/src/lib.rs index 23900cd1cc..ffddc64fd2 100644 --- a/lib/liquid-fixpoint/src/lib.rs +++ b/lib/liquid-fixpoint/src/lib.rs @@ -160,6 +160,22 @@ pub struct Task { pub constraint: Constraint, pub qualifiers: Vec>, pub scrape_quals: bool, + pub solver: SmtSolver, +} + +#[derive(Clone, Copy, Hash)] +pub enum SmtSolver { + Z3, + CVC5, +} + +impl fmt::Display for SmtSolver { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + SmtSolver::Z3 => write!(f, "z3"), + SmtSolver::CVC5 => write!(f, "cvc5"), + } + } } #[derive(Serialize, Deserialize, Debug, Clone)] @@ -214,6 +230,7 @@ impl Task { .arg("--json") .arg("--allowho") .arg("--allowhoqs") + .arg(format!("--solver={}", self.solver)) .stdin(Stdio::piped()) .stdout(Stdio::piped()) .stderr(Stdio::null()) diff --git a/tests/tests/neg/config/test-config00.rs b/tests/tests/neg/config/test-config00.rs index d847a0e96f..f7c38aa6c8 100755 --- a/tests/tests/neg/config/test-config00.rs +++ b/tests/tests/neg/config/test-config00.rs @@ -1,4 +1,4 @@ -#![flux::cfg(check_overflow = "do it!")] //~ ERROR invalid flux configuration: incorrect type in value for setting `check_overflow`, expected bool +#![flux::opts(check_overflow = "do it!")] //~ ERROR invalid attribute: incorrect type in value for setting `check_overflow`, expected bool #[flux::sig(fn(x: i32, y: i32) -> i32)] pub fn test(x: i32, y: i32) -> i32 { diff --git a/tests/tests/neg/config/test-config01.rs b/tests/tests/neg/config/test-config01.rs index c49f75a217..fb28e5361f 100755 --- a/tests/tests/neg/config/test-config01.rs +++ b/tests/tests/neg/config/test-config01.rs @@ -1,4 +1,4 @@ -#![flux::cfg(do_stuff = "true")] //~ ERROR invalid flux configuration: invalid crate cfg keyword `do_stuff` +#![flux::opts(do_stuff = "true")] //~ ERROR invalid attribute: invalid crate cfg keyword `do_stuff` #[flux::sig(fn(x: i32, y: i32) -> i32)] pub fn test(x: i32, y: i32) -> i32 { diff --git a/tests/tests/neg/config/test-config02.rs b/tests/tests/neg/config/test-config02.rs index 522fb628e6..094cafd40e 100755 --- a/tests/tests/neg/config/test-config02.rs +++ b/tests/tests/neg/config/test-config02.rs @@ -1,4 +1,4 @@ -#![flux::cfg(5)] //~ ERROR invalid flux configuration: unsupported item +#![flux::opts(5)] //~ ERROR invalid attribute: unsupported item #[flux::sig(fn(x: i32, y: i32) -> i32)] pub fn test(x: i32, y: i32) -> i32 { diff --git a/tests/tests/neg/config/test-config03.rs b/tests/tests/neg/config/test-config03.rs index 2458f8b99c..85e15653a6 100755 --- a/tests/tests/neg/config/test-config03.rs +++ b/tests/tests/neg/config/test-config03.rs @@ -1,4 +1,4 @@ -#![flux::cfg(fn(x: i32, y:i32) -> i32)] //~ ERROR invalid flux configuration: bad syntax +#![flux::opts(fn(x: i32, y:i32) -> i32)] //~ ERROR invalid attribute: bad syntax #[flux::sig(fn(x: i32, y: i32) -> i32)] pub fn test(x: i32, y: i32) -> i32 { diff --git a/tests/tests/neg/config/test-config04.rs b/tests/tests/neg/config/test-config04.rs index 1f2ceb609a..dbca5c61de 100755 --- a/tests/tests/neg/config/test-config04.rs +++ b/tests/tests/neg/config/test-config04.rs @@ -1,4 +1,4 @@ -#![flux::cfg(log_dir = "./log1", log_dir = "./log2")] //~ ERROR invalid flux configuration: duplicated setting `log_dir` +#![flux::opts(log_dir = "./log1", log_dir = "./log2")] //~ ERROR invalid attribute: duplicated key `log_dir` #[flux::sig(fn(x: i32, y: i32) -> i32)] pub fn test(x: i32, y: i32) -> i32 { diff --git a/tests/tests/neg/surface/binop_overflow.rs b/tests/tests/neg/surface/binop_overflow.rs index 259c35fd91..3132ac581c 100644 --- a/tests/tests/neg/surface/binop_overflow.rs +++ b/tests/tests/neg/surface/binop_overflow.rs @@ -1,4 +1,4 @@ -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] // Arithmetic BinOps // These check for over/underflow diff --git a/tests/tests/neg/surface/check_overflow00.rs b/tests/tests/neg/surface/check_overflow00.rs index a92827c8d0..afcd34d547 100644 --- a/tests/tests/neg/surface/check_overflow00.rs +++ b/tests/tests/neg/surface/check_overflow00.rs @@ -1,4 +1,4 @@ -#[flux::check_overflow] +#[flux::opts(check_overflow = true)] fn add(x: u32, y: u32) -> u32 { x + y //~ ERROR arithmetic operation may overflow } diff --git a/tests/tests/neg/surface/check_overflow01.rs b/tests/tests/neg/surface/check_overflow01.rs index b555e94556..1e149096a9 100644 --- a/tests/tests/neg/surface/check_overflow01.rs +++ b/tests/tests/neg/surface/check_overflow01.rs @@ -1,5 +1,5 @@ // Error on both of these as they may overflow -#![flux::check_overflow] +#![flux::opts(check_overflow = true)] mod my_mod { fn add(x: u32, y: u32) -> u32 { x + y //~ ERROR arithmetic operation may overflow diff --git a/tests/tests/neg/surface/check_overflow02.rs b/tests/tests/neg/surface/check_overflow02.rs index cfb9d1cefd..2b8bc14691 100644 --- a/tests/tests/neg/surface/check_overflow02.rs +++ b/tests/tests/neg/surface/check_overflow02.rs @@ -8,9 +8,9 @@ impl MyStruct { fn add1(&self) -> u32 { self.inner + 1 } - + // Error as this may overflow - #[flux::check_overflow] + #[flux::opts(check_overflow = true)] fn add2(&self) -> u32 { self.inner + 2 //~ERROR arithmetic operation may overflow } diff --git a/tests/tests/neg/surface/check_overflow03.rs b/tests/tests/neg/surface/check_overflow03.rs index 0cb8e918a8..3a41abfb9d 100644 --- a/tests/tests/neg/surface/check_overflow03.rs +++ b/tests/tests/neg/surface/check_overflow03.rs @@ -6,7 +6,7 @@ trait MyTrait { fn add(x: u32, y: u32) -> u32; } -#[flux::check_overflow] +#[flux::opts(check_overflow = true)] impl MyTrait for MyStruct { fn add(x: u32, y: u32) -> u32 { x + y //~ ERROR arithmetic operation may overflow diff --git a/tests/tests/neg/surface/int_bounds_invariants.rs b/tests/tests/neg/surface/int_bounds_invariants.rs index 8b371f40fc..e8ee298456 100644 --- a/tests/tests/neg/surface/int_bounds_invariants.rs +++ b/tests/tests/neg/surface/int_bounds_invariants.rs @@ -1,6 +1,6 @@ // Check that integer bound invariants are not assumed when overflow checking is disabled -#![flux::cfg(check_overflow = false)] +#![flux::opts(check_overflow = false)] #[flux::sig(fn(bool[true]))] fn assert(_: bool) {} diff --git a/tests/tests/neg/surface/scrape00.rs b/tests/tests/neg/surface/scrape00.rs index 058375f1df..bc3520898b 100644 --- a/tests/tests/neg/surface/scrape00.rs +++ b/tests/tests/neg/surface/scrape00.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = false)] +#![flux::opts(scrape_quals = false)] // test that the (fixpoint) `--scrape` mechanism suffices to get // the qualifier needed for the loop invariant below. diff --git a/tests/tests/neg/surface/trait03.rs b/tests/tests/neg/surface/trait03.rs index 5a840d3f3e..338b974e59 100644 --- a/tests/tests/neg/surface/trait03.rs +++ b/tests/tests/neg/surface/trait03.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = true)] // TODO: needed due to odd cyclic constraint? +#![flux::opts(scrape_quals = true)] // TODO: needed due to odd cyclic constraint? use std::vec::IntoIter; diff --git a/tests/tests/neg/surface/unop_overflow.rs b/tests/tests/neg/surface/unop_overflow.rs index 66355e4dd5..7f2161c723 100644 --- a/tests/tests/neg/surface/unop_overflow.rs +++ b/tests/tests/neg/surface/unop_overflow.rs @@ -1,4 +1,4 @@ -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] #[flux::sig(fn(a: i32) -> i32[-a])] pub fn neg_overflow_i32(a: i32) -> i32 { diff --git a/tests/tests/pos/surface/assume_invariant00.rs b/tests/tests/pos/surface/assume_invariant00.rs index 95f0bed8c9..cfc5eebf80 100644 --- a/tests/tests/pos/surface/assume_invariant00.rs +++ b/tests/tests/pos/surface/assume_invariant00.rs @@ -1,6 +1,6 @@ //! Test we assume invariants when unfolding -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] #[flux::sig(fn(bool[true]))] fn assert(_: bool) {} diff --git a/tests/tests/pos/surface/binop_overflow.rs b/tests/tests/pos/surface/binop_overflow.rs index 5d56ddd440..c18b8b68eb 100644 --- a/tests/tests/pos/surface/binop_overflow.rs +++ b/tests/tests/pos/surface/binop_overflow.rs @@ -1,4 +1,4 @@ -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] // Arithmetic BinOps // diff --git a/tests/tests/pos/surface/check_overflow00.rs b/tests/tests/pos/surface/check_overflow00.rs index 1d38a73ffd..6819fb69f9 100644 --- a/tests/tests/pos/surface/check_overflow00.rs +++ b/tests/tests/pos/surface/check_overflow00.rs @@ -1,7 +1,7 @@ const MAX: u32 = std::u32::MAX; // Error on this as it may overflow -#[flux::check_overflow] +#[flux::opts(check_overflow = true)] #[flux::sig(fn (u32[@x], u32[@y], u32[@z]) -> u32[x + y + z] requires x + y + z <= MAX)] fn add_three(x: u32, y: u32, z: u32) -> u32 { x + y + z diff --git a/tests/tests/pos/surface/check_overflow01.rs b/tests/tests/pos/surface/check_overflow01.rs index 8f9cebe577..28decb193b 100644 --- a/tests/tests/pos/surface/check_overflow01.rs +++ b/tests/tests/pos/surface/check_overflow01.rs @@ -1,4 +1,4 @@ -#[flux::check_overflow] +#[flux::opts(check_overflow = true)] mod my_mod { const MAX: u32 = std::u32::MAX; diff --git a/tests/tests/pos/surface/check_overflow02.rs b/tests/tests/pos/surface/check_overflow02.rs index 88e1bb702f..7bb5872b1e 100644 --- a/tests/tests/pos/surface/check_overflow02.rs +++ b/tests/tests/pos/surface/check_overflow02.rs @@ -10,9 +10,9 @@ impl MyStruct { fn add1(&self) -> u32 { self.inner + 1 } - + // Error as this may overflow - #[flux::check_overflow] + #[flux::opts(check_overflow = true)] #[flux::sig(fn (&MyStruct[@inner]) -> u32[inner + 2] requires inner + 2 <= MAX)] fn add2(&self) -> u32 { self.inner + 2 diff --git a/tests/tests/pos/surface/check_overflow03.rs b/tests/tests/pos/surface/check_overflow03.rs index 790748a8b6..0c04db7a6e 100644 --- a/tests/tests/pos/surface/check_overflow03.rs +++ b/tests/tests/pos/surface/check_overflow03.rs @@ -4,7 +4,7 @@ struct MyStruct { inner: u32, } -#[flux::check_overflow] +#[flux::opts(check_overflow = true)] trait MyTrait { #[flux::sig(fn(u32[@x], { u32[@y] | x + y <= MAX }) -> u32[x + y] )] fn add(x: u32, y: u32) -> u32; diff --git a/tests/tests/pos/surface/check_overflow05.rs b/tests/tests/pos/surface/check_overflow05.rs index de566a4b8b..cc45d0091c 100644 --- a/tests/tests/pos/surface/check_overflow05.rs +++ b/tests/tests/pos/surface/check_overflow05.rs @@ -1,5 +1,5 @@ // configure check for the entire thing -#![cfg_attr(flux, flux::cfg(check_overflow = true))] +#![cfg_attr(flux, flux::opts(check_overflow = true))] const MAX: u32 = std::u32::MAX; @@ -8,7 +8,7 @@ fn add(x: u32, y: u32) -> u32 { x + y } -#[flux::check_overflow(no)] +#[flux::opts(check_overflow = false)] fn add_more(x: u32, y: u32, z: u32) -> u32 { x + y + z } diff --git a/tests/tests/pos/surface/int_bounds_invariants.rs b/tests/tests/pos/surface/int_bounds_invariants.rs index f179e00037..75e73477ba 100644 --- a/tests/tests/pos/surface/int_bounds_invariants.rs +++ b/tests/tests/pos/surface/int_bounds_invariants.rs @@ -1,6 +1,6 @@ // Check that integer bound invariants are assumed when overflow checking is enabled -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] #[flux::sig(fn(bool[true]))] fn assert(_: bool) {} diff --git a/tests/tests/pos/surface/kmp_overflow.rs b/tests/tests/pos/surface/kmp_overflow.rs index ff94d03b1f..7aeeef3e67 100644 --- a/tests/tests/pos/surface/kmp_overflow.rs +++ b/tests/tests/pos/surface/kmp_overflow.rs @@ -1,6 +1,6 @@ // Implementation of kmp with overflow checks enabled -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] #[path = "../../lib/rvec.rs"] mod rvec; diff --git a/tests/tests/pos/surface/loop_abstract_refinement.rs b/tests/tests/pos/surface/loop_abstract_refinement.rs index 05ef30590b..4705a78c0a 100644 --- a/tests/tests/pos/surface/loop_abstract_refinement.rs +++ b/tests/tests/pos/surface/loop_abstract_refinement.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = true)] +#![flux::opts(scrape_quals = true)] #![flux::defs { qualifier MyQ1(k: int, i: int, j: int, n: int) { (0 <= k && k < i) || (j <= k && k < n) diff --git a/tests/tests/pos/surface/polymorphic_qualifier.rs b/tests/tests/pos/surface/polymorphic_qualifier.rs index 694e7238b8..b6f7a66c69 100644 --- a/tests/tests/pos/surface/polymorphic_qualifier.rs +++ b/tests/tests/pos/surface/polymorphic_qualifier.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = true)] +#![flux::opts(scrape_quals = true)] #[flux::sig(fn[hrn p: T -> bool](vec: Vec, init: T{ p(init) }) -> T{v: p(v)})] fn maximum(vec: Vec, init: T) -> T { diff --git a/tests/tests/pos/surface/scrape00.rs b/tests/tests/pos/surface/scrape00.rs index b8f5de8304..3085734ba2 100644 --- a/tests/tests/pos/surface/scrape00.rs +++ b/tests/tests/pos/surface/scrape00.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = true)] +#![flux::opts(scrape_quals = true)] // test that the (fixpoint) `--scrape` mechanism suffices to get // the qualifier needed for the loop invariant below. diff --git a/tests/tests/pos/surface/scrape01.rs b/tests/tests/pos/surface/scrape01.rs index f5baed4a41..0d5348f1ec 100644 --- a/tests/tests/pos/surface/scrape01.rs +++ b/tests/tests/pos/surface/scrape01.rs @@ -1,4 +1,4 @@ -#![flux::cfg(scrape_quals = "true")] +#![flux::opts(scrape_quals = "true")] #[path = "../../lib/rvec.rs"] mod rvec; diff --git a/tests/tests/pos/surface/unop_overflow.rs b/tests/tests/pos/surface/unop_overflow.rs index 6f0f369c8f..699fce07f5 100644 --- a/tests/tests/pos/surface/unop_overflow.rs +++ b/tests/tests/pos/surface/unop_overflow.rs @@ -1,4 +1,4 @@ -#![flux::cfg(check_overflow = true)] +#![flux::opts(check_overflow = true)] #[flux::sig(fn(a: i32{a != i32::MIN}) -> i32[-a])] pub fn neg_overflow_i32(a: i32) -> i32 {