diff --git a/flux-config/src/lib.rs b/flux-config/src/lib.rs index 3117beba34..f46862922a 100644 --- a/flux-config/src/lib.rs +++ b/flux-config/src/lib.rs @@ -63,9 +63,7 @@ pub fn check_overflow() -> bool { #[derive(Debug)] pub struct CrateConfig { - pub log_dir: PathBuf, - pub dump_constraint: bool, - pub dump_checker_trace: bool, + pub check_overflow: bool, } #[derive(Deserialize)] @@ -172,3 +170,9 @@ pub static CONFIG_FILE: LazyLock = LazyLock::new(|| { toml::from_str("").unwrap() } }); + +impl Default for CrateConfig { + fn default() -> Self { + Self { check_overflow: check_overflow() } + } +} diff --git a/flux-docs/src/guide/run.md b/flux-docs/src/guide/run.md index 6e4b9028fe..49e5709e38 100644 --- a/flux-docs/src/guide/run.md +++ b/flux-docs/src/guide/run.md @@ -70,7 +70,7 @@ error[FLUX]: postcondition might not hold | ^^^^^ ``` -as indeed `x - 1` is *not* greater than `x` as required by the output refinement `i32{v: x < v}`. +as indeed `x - 1` is _not_ greater than `x` as required by the output refinement `i32{v: x < v}`. If you fix the error by replacing `x - 1` with `x + 1`, you should get no errors in the output (the output may be empty, but in this case no output is a good @@ -169,6 +169,19 @@ then `flux` will create the directory `./test/` and write `./test/timings`, a fi containing profiling information. It will _not_ dump the MIR because that setting was overridden by setting the environment variable `FLUX_DUMP_MIR=0`. +### Crate Config + +Some flags can be configured on a per-crate basis using the custom inner attribute `#![flux::cfg]`. +This can only be used in nightly and requires enabling the feature `custom_inner_attributes` +For example, to enable overflow checking: + +```rust +#![feature(custom_inner_attributes)] +#![flux:cfg(check_overflow = true)] +``` + +The only flag supported now is overflow checking. + ### Query Caching `FLUX_CACHE=1` persistently caches the safe fixpoint queries for each `DefId` in diff --git a/flux-driver/src/callbacks.rs b/flux-driver/src/callbacks.rs index b16d940388..43c8427dae 100644 --- a/flux-driver/src/callbacks.rs +++ b/flux-driver/src/callbacks.rs @@ -1,3 +1,4 @@ +use config::CrateConfig; use flux_common::{cache::QueryCache, dbg, iter::IterExt}; use flux_config as config; use flux_desugar as desugar; @@ -9,6 +10,7 @@ use flux_middle::{ global_env::GlobalEnv, }; use flux_refineck as refineck; +use refineck::CheckerConfig; use rustc_driver::{Callbacks, Compilation}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::LocalDefId, OwnerId}; @@ -90,7 +92,7 @@ fn check_crate(tcx: TyCtxt, sess: &FluxSession) -> Result<(), ErrorGuaranteed> { tracing::info!("Callbacks::check_wf"); - let mut ck = CrateChecker::new(&mut genv, specs.ignores); + let mut ck = CrateChecker::new(&mut genv, specs.ignores, specs.crate_config); let crate_items = tcx.hir_crate_items(()); let items = crate_items.items().map(|item| item.owner_id.def_id); @@ -312,11 +314,18 @@ struct CrateChecker<'a, 'genv, 'tcx> { genv: &'a mut GlobalEnv<'genv, 'tcx>, ignores: Ignores, cache: QueryCache, + checker_config: CheckerConfig, } impl<'a, 'genv, 'tcx> CrateChecker<'a, 'genv, 'tcx> { - fn new(genv: &'a mut GlobalEnv<'genv, 'tcx>, ignores: Ignores) -> Self { - CrateChecker { genv, ignores, cache: QueryCache::load() } + fn new( + genv: &'a mut GlobalEnv<'genv, 'tcx>, + ignores: Ignores, + crate_config: Option, + ) -> Self { + let crate_config = crate_config.unwrap_or_default(); + let checker_config = CheckerConfig { check_overflow: crate_config.check_overflow }; + CrateChecker { genv, ignores, cache: QueryCache::load(), checker_config } } /// `is_ignored` transitively follows the `def_id`'s parent-chain to check if @@ -343,7 +352,7 @@ impl<'a, 'genv, 'tcx> CrateChecker<'a, 'genv, 'tcx> { match self.genv.tcx.def_kind(def_id) { DefKind::Fn | DefKind::AssocFn => { - refineck::check_fn(self.genv, &mut self.cache, def_id) + refineck::check_fn(self.genv, &mut self.cache, def_id, self.checker_config) } DefKind::Enum => { let adt_def = self.genv.adt_def(def_id.to_def_id()).emit(self.genv.sess)?; diff --git a/flux-driver/src/collector.rs b/flux-driver/src/collector.rs index 90a2137e49..eed397bb83 100644 --- a/flux-driver/src/collector.rs +++ b/flux-driver/src/collector.rs @@ -1,4 +1,4 @@ -use std::{collections::HashMap, path::PathBuf}; +use std::collections::HashMap; use flux_common::iter::IterExt; use flux_config::{self as config, CrateConfig}; @@ -649,7 +649,7 @@ impl FluxAttrKind { #[derive(Debug)] struct CFGSetting { - setting: String, + setting: Symbol, span: Span, } @@ -659,23 +659,21 @@ struct FluxAttrCFG { } macro_rules! try_read_setting { - ($self:expr, $setting:literal, $type:ident, $default:expr) => { - if let Some(CFGSetting { setting, span }) = $self.map.remove($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 parse_result.is_err() { - Err(errors::CFGError { + if let Ok(val) = parse_result { + $cfg.$setting = val; + } else { + return Err(errors::CFGError { span, message: format!( "incorrect type in value for setting `{}`, expected {}", - $setting, + stringify!($setting), stringify!($type) ), - }) - } else { - Ok(parse_result.unwrap()) + }); } - } else { - Ok($default) } }; } @@ -717,14 +715,11 @@ impl FluxAttrCFG { } // TODO: support types of values other than strings - let value = item - .value_str() - .map(Symbol::to_ident_string) - .ok_or_else(|| { - errors::CFGError { span, message: "unsupported value".to_string() } - })?; - - let setting = CFGSetting { setting: value, span: item.span }; + let value = item.name_value_literal().ok_or_else(|| { + errors::CFGError { span, message: "unsupported value".to_string() } + })?; + + let setting = CFGSetting { setting: value.symbol, span: item.span }; self.map.insert(name, setting); return Ok(()); } @@ -740,11 +735,8 @@ impl FluxAttrCFG { } fn try_into_crate_cfg(&mut self) -> Result { - let log_dir = try_read_setting!(self, "log_dir", PathBuf, config::log_dir().clone())?; - let dump_constraint = - try_read_setting!(self, "dump_constraint", bool, config::dump_constraint())?; - let dump_checker_trace = - try_read_setting!(self, "dump_checker_trace", bool, config::dump_checker_trace())?; + let mut crate_config = CrateConfig::default(); + try_read_setting!(self, check_overflow, bool, crate_config); if let Some((name, setting)) = self.map.iter().next() { return Err(errors::CFGError { @@ -753,7 +745,7 @@ impl FluxAttrCFG { }); } - Ok(CrateConfig { log_dir, dump_constraint, dump_checker_trace }) + Ok(crate_config) } } diff --git a/flux-fhir-analysis/src/wf/mod.rs b/flux-fhir-analysis/src/wf/mod.rs index 20bc33b74e..612896a591 100644 --- a/flux-fhir-analysis/src/wf/mod.rs +++ b/flux-fhir-analysis/src/wf/mod.rs @@ -133,6 +133,8 @@ pub(crate) fn check_enum_def( .iter() .try_for_each_exhaust(|invariant| infcx.check_expr(invariant, &fhir::Sort::Bool))?; + // We are reusing the same `InferCtxt` which may contain some variables from the enum params. + // This is not a problem because parameters in the variants with the same name will overwrite them. enum_def .variants .iter() diff --git a/flux-refineck/src/checker.rs b/flux-refineck/src/checker.rs index 55752fd5ba..6289480110 100644 --- a/flux-refineck/src/checker.rs +++ b/flux-refineck/src/checker.rs @@ -38,8 +38,14 @@ use crate::{ type_env::{BasicBlockEnv, BasicBlockEnvShape, TypeEnv}, }; +#[derive(Clone, Copy, Debug)] +pub struct CheckerConfig { + pub check_overflow: bool, +} + pub(crate) struct Checker<'a, 'tcx, M> { genv: &'a GlobalEnv<'a, 'tcx>, + config: CheckerConfig, /// [`DefId`] of the function being checked, either a closure or a regular function. def_id: DefId, /// [`Generics`] of the function being checked. @@ -106,6 +112,7 @@ impl<'a, 'tcx, M> Checker<'a, 'tcx, M> { output: Binder, dominators: &'a Dominators, mode: &'a mut M, + config: CheckerConfig, ) -> Self { let generics = genv.generics_of(def_id).unwrap_or_else(|_| { span_bug!(body.span(), "checking function with unsupported signature") @@ -121,6 +128,7 @@ impl<'a, 'tcx, M> Checker<'a, 'tcx, M> { snapshots: IndexVec::from_fn_n(|_| None, body.basic_blocks.len()), dominators, queue: WorkQueue::empty(body.basic_blocks.len(), dominators), + config, } } } @@ -129,6 +137,7 @@ impl<'a, 'tcx> Checker<'a, 'tcx, ShapeMode> { pub(crate) fn run_in_shape_mode( genv: &GlobalEnv<'a, 'tcx>, def_id: DefId, + config: CheckerConfig, ) -> Result { dbg::shape_mode_span!(genv.tcx, def_id).in_scope(|| { let mut mode = ShapeMode { bb_envs: FxHashMap::default() }; @@ -138,7 +147,7 @@ impl<'a, 'tcx> Checker<'a, 'tcx, ShapeMode> { .with_span(genv.tcx.def_span(def_id))? .subst_identity(); - Checker::run(genv, RefineTree::new().as_subtree(), def_id, &mut mode, fn_sig)?; + Checker::run(genv, RefineTree::new().as_subtree(), def_id, &mut mode, fn_sig, config)?; Ok(ShapeResult(mode.bb_envs)) }) @@ -150,6 +159,7 @@ impl<'a, 'tcx> Checker<'a, 'tcx, RefineMode> { genv: &GlobalEnv<'a, 'tcx>, def_id: DefId, bb_env_shapes: ShapeResult, + config: CheckerConfig, ) -> Result<(RefineTree, KVarStore), CheckerError> { let fn_sig = genv .fn_sig(def_id) @@ -162,7 +172,7 @@ impl<'a, 'tcx> Checker<'a, 'tcx, RefineMode> { dbg::refine_mode_span!(genv.tcx, def_id, bb_envs).in_scope(|| { let mut mode = RefineMode { bb_envs, kvars }; - Checker::run(genv, refine_tree.as_subtree(), def_id, &mut mode, fn_sig)?; + Checker::run(genv, refine_tree.as_subtree(), def_id, &mut mode, fn_sig, config)?; Ok((refine_tree, mode.kvars)) }) @@ -176,6 +186,7 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> { def_id: DefId, mode: &'a mut M, fn_sig: PolyFnSig, + config: CheckerConfig, ) -> Result<(), CheckerError> { let body = genv .mir(def_id.expect_local()) @@ -189,7 +200,8 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> { let dominators = body.dominators(); - let mut ck = Checker::new(genv, def_id, &body, fn_sig.output().clone(), &dominators, mode); + let mut ck = + Checker::new(genv, def_id, &body, fn_sig.output().clone(), &dominators, mode, config); ck.check_goto(rcx, env, body.span(), START_BLOCK)?; while let Some(bb) = ck.queue.pop() { @@ -472,6 +484,7 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> { *def_id, self.mode, fn_pred.to_poly_sig(*def_id), + self.config, )?; } else { todo!("report error") @@ -753,7 +766,7 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> { } } (TyKind::Indexed(bty1, idx1), TyKind::Indexed(bty2, idx2)) => { - let sig = sigs::get_bin_op_sig(bin_op, bty1, bty2); + let sig = sigs::get_bin_op_sig(bin_op, bty1, bty2, self.config.check_overflow); let (e1, e2) = (idx1.expr.clone(), idx2.expr.clone()); if let sigs::Pre::Some(reason, constr) = &sig.pre { self.constr_gen(rcx, source_span).check_pred( diff --git a/flux-refineck/src/lib.rs b/flux-refineck/src/lib.rs index 434adb4e65..950ba8892c 100644 --- a/flux-refineck/src/lib.rs +++ b/flux-refineck/src/lib.rs @@ -30,6 +30,7 @@ mod sigs; mod type_env; use checker::Checker; +pub use checker::CheckerConfig; use constraint_gen::{ConstrReason, Tag}; use flux_common::{cache::QueryCache, dbg}; use flux_config as config; @@ -46,6 +47,7 @@ pub fn check_fn( genv: &GlobalEnv, cache: &mut QueryCache, local_id: LocalDefId, + config: CheckerConfig, ) -> Result<(), ErrorGuaranteed> { let def_id = local_id.to_def_id(); dbg::check_fn_span!(genv.tcx, def_id).in_scope(|| { @@ -60,12 +62,12 @@ pub fn check_fn( } // PHASE 1: infer shape of basic blocks - let shape_result = Checker::run_in_shape_mode(genv, def_id).emit(genv.sess)?; + let shape_result = Checker::run_in_shape_mode(genv, def_id, config).emit(genv.sess)?; tracing::info!("check_fn::shape"); // PHASE 2: generate refinement tree constraint let (mut refine_tree, kvars) = - Checker::run_in_refine_mode(genv, def_id, shape_result).emit(genv.sess)?; + Checker::run_in_refine_mode(genv, def_id, shape_result, config).emit(genv.sess)?; tracing::info!("check_fn::refine"); // PHASE 3: invoke fixpoint on the constraints diff --git a/flux-refineck/src/sigs.rs b/flux-refineck/src/sigs.rs deleted file mode 100644 index 5543b44021..0000000000 --- a/flux-refineck/src/sigs.rs +++ /dev/null @@ -1,340 +0,0 @@ -use std::sync::LazyLock; - -use flux_middle::{ - rty::{BaseTy, BinOp, Expr, IntTy, UintTy}, - rustc::mir, -}; -use itertools::iproduct; -use rustc_hash::FxHashMap; - -use crate::constraint_gen::ConstrReason; - -pub struct Sig { - pub args: [BaseTy; N], - pub pre: Pre, - pub out: Output, -} - -pub enum Pre { - None, - Some(ConstrReason, Box Expr + Sync + Send>), -} - -#[derive(Clone)] -pub enum Output { - Indexed(BaseTy, fn([Expr; N]) -> Expr), - Exists(BaseTy, fn(Expr, [Expr; N]) -> Expr), -} - -struct SigTable { - map: FxHashMap<(T, [BaseTy; N]), Sig>, -} - -pub fn get_bin_op_sig(op: mir::BinOp, bty1: &BaseTy, bty2: &BaseTy) -> &'static Sig<2> { - BIN_OPS.get(op, [bty1.clone(), bty2.clone()]) -} - -type E = Expr; - -macro_rules! define_btys { - ($(let $name:ident = $bty:expr;)*) => { - #[allow(unused_macros)] - macro_rules! bty { - $( - ($name) => { - $bty - }; - )* - } - }; -} - -macro_rules! s { - (fn ($($arg:ident:$ty:ident),+) -> $($rest:tt)+) => {{ - let (pre, out) = s!(($($arg),+) $($rest)+) ; - let args = [$(bty!($ty)),+]; - Sig { args, pre, out } - }}; - (($($args:ident),+) $bty:ident[$out:expr] $($rest:tt)*) => {{ - let bty = bty!($bty); - #[allow(unused_variables)] - let pre = s!(($($args),+) $($rest)*); - #[allow(unused_variables)] - let out = Output::Indexed(bty, |[$($args),+]| $out); - (pre, out) - }}; - (($($args:ident),+) $bty:ident{$v:ident : $out:expr} $($rest:tt)*) => {{ - let bty = bty!($bty); - #[allow(unused_variables)] - let pre = s!(($($args),+) $($rest)*); - #[allow(unused_variables)] - let out = Output::Exists(bty, |$v, [$($args),+]| $out); - (pre, out) - }}; - (($($args:ident),+)) => { - Pre::None - }; - (($($args:ident),+) requires $pre:expr => $tag:path) => { - Pre::Some($tag, Box::new(move |[$($args),+]| $pre)) - }; -} - -/// This set of signatures does not check for overflow. They check for underflow -/// in subtraction. -#[rustfmt::skip] -fn mk_unsigned_bin_ops() -> impl Iterator)> { - use mir::BinOp::*; - UINT_TYS - .into_iter() - .flat_map(|uint_ty| { - define_btys! { - let bool = BaseTy::Bool; - let Uint = BaseTy::Uint(uint_ty); - } - [ - // ARITH - (Add, s!(fn(a: Uint, b: Uint) -> Uint[a + b])), - (Mul, s!(fn(a: Uint, b: Uint) -> Uint[a * b])), - (Sub, s!(fn(a: Uint, b: Uint) -> Uint[a - b] - requires E::ge(a - b, 0) => ConstrReason::Overflow) - ), - (Div, s!(fn(a: Uint, b: Uint) -> Uint[a / b] - requires E::ne(b, 0) => ConstrReason::Div), - ), - (Rem, s!(fn(a:Uint , b: Uint) -> Uint[E::binary_op(BinOp::Mod, a, b)] - requires E::ne(b, 0) => ConstrReason::Rem), - ), - // BIT - (BitAnd, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), - (BitOr, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), - // CMP - (Eq, s!(fn(a: Uint, b: Uint) -> bool[E::eq(a, b)])), - (Ne, s!(fn(a: Uint, b: Uint) -> bool[E::ne(a, b)])), - (Le, s!(fn(a: Uint, b: Uint) -> bool[E::le(a, b)])), - (Ge, s!(fn(a: Uint, b: Uint) -> bool[E::ge(a, b)])), - (Lt, s!(fn(a: Uint, b: Uint) -> bool[E::lt(a, b)])), - (Gt, s!(fn(a: Uint, b: Uint) -> bool[E::gt(a, b)])), - ] - }) -} - -/// This set of signatures checks for overflow and underflow. They work in -/// tandem with the invariant for unsigned ints returned in -/// [`BaseTy::invariants`]. -/// -/// [`BaseTy::invariants`]: flux_middle::rty::BaseTy::invariants -#[rustfmt::skip] -fn mk_unsigned_bin_ops_check_overflow() -> impl Iterator)> { - use mir::BinOp::*; - UINT_TYS - .into_iter() - .flat_map(|uint_ty| { - define_btys! { - let bool = BaseTy::Bool; - let Uint = BaseTy::Uint(uint_ty); - } - let bit_width: u64 = uint_ty.bit_width().unwrap_or(flux_config::pointer_width().bits()); - [ - // ARITH - (Add, s!(fn(a: Uint, b: Uint) -> Uint[a + b] - requires E::le(a + b, E::uint_max(bit_width)) => ConstrReason::Overflow) - ), - (Mul, s!(fn(a: Uint, b: Uint) -> Uint[a * b] - requires E::le(a * b, E::uint_max(bit_width)) => ConstrReason::Overflow) - ), - (Sub, s!(fn(a: Uint, b: Uint) -> Uint[a - b] - requires E::ge(a - b, 0) => ConstrReason::Overflow) - ), - (Div, s!(fn(a: Uint, b: Uint) -> Uint[a / b] - requires E::ne(b, 0) => ConstrReason::Div), - ), - (Rem, s!(fn(a:Uint , b: Uint) -> Uint[E::binary_op(BinOp::Mod, a, b)] - requires E::ne(b, 0) => ConstrReason::Rem), - ), - // BIT - (BitAnd, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), - (BitOr, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), - // CMP - (Eq, s!(fn(a: Uint, b: Uint) -> bool[E::eq(a, b)])), - (Ne, s!(fn(a: Uint, b: Uint) -> bool[E::ne(a, b)])), - (Le, s!(fn(a: Uint, b: Uint) -> bool[E::le(a, b)])), - (Ge, s!(fn(a: Uint, b: Uint) -> bool[E::ge(a, b)])), - (Lt, s!(fn(a: Uint, b: Uint) -> bool[E::lt(a, b)])), - (Gt, s!(fn(a: Uint, b: Uint) -> bool[E::gt(a, b)])), - ] - }) -} - -#[rustfmt::skip] -fn mk_signed_bin_ops() -> impl Iterator)> { - use mir::BinOp::*; - INT_TYS - .into_iter() - .flat_map(|int_ty| { - define_btys! { - let bool = BaseTy::Bool; - let Int = BaseTy::Int(int_ty); - } - [ - // ARITH - (Add, s!(fn(a: Int, b: Int) -> Int[a + b])), - (Sub, s!(fn(a: Int, b: Int) -> Int[a - b])), - (Mul, s!(fn(a: Int, b: Int) -> Int[a * b])), - (Div, s!(fn(a: Int, b: Int) -> Int[a / b] - requires E::ne(b, 0) => ConstrReason::Div), - ), - (Rem, s!(fn(a:Int , b: Int) -> Int{v: E::implies( - E::and([E::ge(&a, 0), E::ge(&b, 0)]), - E::eq(v, E::binary_op(BinOp::Mod, a, b))) } - requires E::ne(b, 0) => ConstrReason::Rem), - ), - // BIT - (BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), - (BitOr, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), - // CMP - (Eq, s!(fn(a: Int, b: Int) -> bool[E::eq(a, b)])), - (Ne, s!(fn(a: Int, b: Int) -> bool[E::ne(a, b)])), - (Le, s!(fn(a: Int, b: Int) -> bool[E::le(a, b)])), - (Ge, s!(fn(a: Int, b: Int) -> bool[E::ge(a, b)])), - (Lt, s!(fn(a: Int, b: Int) -> bool[E::lt(a, b)])), - (Gt, s!(fn(a: Int, b: Int) -> bool[E::gt(a, b)])), - ] - }) -} - -#[rustfmt::skip] -fn mk_signed_bin_ops_check_overflow() -> impl Iterator)> { - use mir::BinOp::*; - INT_TYS - .into_iter() - .flat_map(|int_ty| { - define_btys! { - let bool = BaseTy::Bool; - let Int = BaseTy::Int(int_ty); - } - let bit_width: u64 = int_ty.bit_width().unwrap_or(flux_config::pointer_width().bits()); - [ - // ARITH - (Add, s!(fn(a: Int, b: Int) -> Int[a + b] - requires E::and([ - E::le(&a + &b, E::int_max(bit_width)), - E::ge(a + b, E::int_min(bit_width)) - ]) => ConstrReason::Overflow) - ), - (Sub, s!(fn(a: Int, b: Int) -> Int[a - b] - requires E::and([ - E::le(&a - &b, E::int_max(bit_width)), - E::ge(a - b, E::int_min(bit_width)) - ]) => ConstrReason::Overflow) - ), - (Mul, s!(fn(a: Int, b: Int) -> Int[a * b] - requires E::and([ - E::le(&a - &b, E::int_max(bit_width)), - E::ge(a - b, E::int_min(bit_width)) - ]) => ConstrReason::Overflow) - ), - (Div, s!(fn(a: Int, b: Int) -> Int[a / b] - requires E::ne(b, 0) => ConstrReason::Div), - ), - (Rem, s!(fn(a:Int , b: Int) -> Int{v: E::implies( - E::and([E::ge(&a, 0), E::ge(&b, 0)]), - E::eq(v, E::binary_op(BinOp::Mod, a, b))) } - requires E::ne(b, 0) => ConstrReason::Rem), - ), - // BIT - (BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), - (BitOr, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), - // CMP - (Eq, s!(fn(a: Int, b: Int) -> bool[E::eq(a, b)])), - (Ne, s!(fn(a: Int, b: Int) -> bool[E::ne(a, b)])), - (Le, s!(fn(a: Int, b: Int) -> bool[E::le(a, b)])), - (Ge, s!(fn(a: Int, b: Int) -> bool[E::ge(a, b)])), - (Lt, s!(fn(a: Int, b: Int) -> bool[E::lt(a, b)])), - (Gt, s!(fn(a: Int, b: Int) -> bool[E::gt(a, b)])), - ] - }) -} - -#[rustfmt::skip] -fn mk_bool_bin_ops() -> impl IntoIterator)> { - use mir::BinOp::*; - define_btys! { let bool = BaseTy::Bool; } - [ - // BIT - (BitAnd, s!(fn(a: bool, b: bool) -> bool[E::and([a, b])])), - (BitOr, s!(fn(a: bool, b: bool) -> bool[E::or([a, b])])), - // CMP - (Eq, s!(fn(a: bool, b: bool) -> bool[E::eq(a, b)])), - (Ne, s!(fn(a: bool, b: bool) -> bool[E::ne(a, b)])), - (Le, s!(fn(a: bool, b: bool) -> bool[E::implies(a, b)])), - (Ge, s!(fn(a: bool, b: bool) -> bool[E::implies(b, a)])), - (Lt, s!(fn(a: bool, b: bool) -> bool[E::and([a.not(), b])])), - (Gt, s!(fn(a: bool, b: bool) -> bool[E::and([a, b.not()])])), - ] -} - -#[rustfmt::skip] -fn mk_shift_ops() -> impl IntoIterator)> { - use mir::BinOp::*; - iproduct!(INT_TYS, UINT_TYS) - .flat_map(|(int_ty, uint_ty)|{ - define_btys! { - let Int = BaseTy::Int(int_ty); - let Uint = BaseTy::Uint(uint_ty); - } - [ - (Shl, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })), - (Shl, s!(fn(a: Int, b: Uint) -> Int{ v: E::tt() })), - (Shr, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })), - (Shr, s!(fn(a: Int, b: Uint) -> Int{ v: E::tt() })), - - (Shl, s!(fn(a: Uint, b: Int) -> Uint{ v: E::tt() })), - (Shl, s!(fn(a: Uint, b: Uint) -> Uint{ v: E::tt() })), - (Shr, s!(fn(a: Uint, b: Int) -> Uint{ v: E::tt() })), - (Shr, s!(fn(a: Uint, b: Uint) -> Uint{ v: E::tt() })), - ] - }) -} - -static BIN_OPS: LazyLock> = LazyLock::new(|| { - let mut table = SigTable::new(); - - if flux_config::check_overflow() { - table.extend(mk_signed_bin_ops_check_overflow()); - table.extend(mk_unsigned_bin_ops_check_overflow()); - } else { - table.extend(mk_signed_bin_ops()); - table.extend(mk_unsigned_bin_ops()); - } - table.extend(mk_shift_ops()); - table.extend(mk_bool_bin_ops()); - - table -}); - -impl SigTable { - fn new() -> Self { - Self { map: FxHashMap::default() } - } -} - -impl SigTable -where - T: std::hash::Hash + Eq, -{ - fn extend(&mut self, iter: impl IntoIterator)>) { - self.map.extend( - iter.into_iter() - .map(|(op, sig)| ((op, sig.args.clone()), sig)), - ); - } - - fn get(&self, op: T, btys: [BaseTy; N]) -> &Sig { - &self.map[&(op, btys)] - } -} - -static INT_TYS: [IntTy; 6] = - [IntTy::Isize, IntTy::I8, IntTy::I16, IntTy::I32, IntTy::I64, IntTy::I128]; -static UINT_TYS: [UintTy; 6] = - [UintTy::Usize, UintTy::U8, UintTy::U16, UintTy::U32, UintTy::U64, UintTy::U128]; diff --git a/flux-refineck/src/sigs/default.rs b/flux-refineck/src/sigs/default.rs new file mode 100644 index 0000000000..fa9272ea0d --- /dev/null +++ b/flux-refineck/src/sigs/default.rs @@ -0,0 +1,143 @@ +use std::sync::LazyLock; + +use flux_middle::{ + rty::{BaseTy, BinOp, Expr}, + rustc::mir, +}; +use itertools::iproduct; + +use super::{Sig, SigTable}; +use crate::{ + constraint_gen::ConstrReason, + sigs::{define_btys, s, INT_TYS, UINT_TYS}, +}; + +type E = Expr; + +pub(super) static BIN_OPS: LazyLock> = LazyLock::new(|| { + let mut table = SigTable::new(); + + table.extend(mk_signed_bin_ops()); + table.extend(mk_unsigned_bin_ops()); + table.extend(mk_shift_ops()); + table.extend(mk_bool_bin_ops()); + + table +}); + +/// This set of signatures does not check for overflow. They check for underflow +/// in subtraction. +#[rustfmt::skip] +fn mk_unsigned_bin_ops() -> impl Iterator)> { + use mir::BinOp::*; + UINT_TYS + .into_iter() + .flat_map(|uint_ty| { + define_btys! { + let bool = BaseTy::Bool; + let Uint = BaseTy::Uint(uint_ty); + } + [ + // ARITH + (Add, s!(fn(a: Uint, b: Uint) -> Uint[a + b])), + (Mul, s!(fn(a: Uint, b: Uint) -> Uint[a * b])), + (Sub, s!(fn(a: Uint, b: Uint) -> Uint[a - b] + requires E::ge(a - b, 0) => ConstrReason::Overflow) + ), + (Div, s!(fn(a: Uint, b: Uint) -> Uint[a / b] + requires E::ne(b, 0) => ConstrReason::Div), + ), + (Rem, s!(fn(a:Uint , b: Uint) -> Uint[E::binary_op(BinOp::Mod, a, b)] + requires E::ne(b, 0) => ConstrReason::Rem), + ), + // BIT + (BitAnd, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), + (BitOr, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), + // CMP + (Eq, s!(fn(a: Uint, b: Uint) -> bool[E::eq(a, b)])), + (Ne, s!(fn(a: Uint, b: Uint) -> bool[E::ne(a, b)])), + (Le, s!(fn(a: Uint, b: Uint) -> bool[E::le(a, b)])), + (Ge, s!(fn(a: Uint, b: Uint) -> bool[E::ge(a, b)])), + (Lt, s!(fn(a: Uint, b: Uint) -> bool[E::lt(a, b)])), + (Gt, s!(fn(a: Uint, b: Uint) -> bool[E::gt(a, b)])), + ] + }) +} + +#[rustfmt::skip] +fn mk_signed_bin_ops() -> impl Iterator)> { + use mir::BinOp::*; + INT_TYS + .into_iter() + .flat_map(|int_ty| { + define_btys! { + let bool = BaseTy::Bool; + let Int = BaseTy::Int(int_ty); + } + [ + // ARITH + (Add, s!(fn(a: Int, b: Int) -> Int[a + b])), + (Sub, s!(fn(a: Int, b: Int) -> Int[a - b])), + (Mul, s!(fn(a: Int, b: Int) -> Int[a * b])), + (Div, s!(fn(a: Int, b: Int) -> Int[a / b] + requires E::ne(b, 0) => ConstrReason::Div), + ), + (Rem, s!(fn(a:Int , b: Int) -> Int{v: E::implies( + E::and([E::ge(&a, 0), E::ge(&b, 0)]), + E::eq(v, E::binary_op(BinOp::Mod, a, b))) } + requires E::ne(b, 0) => ConstrReason::Rem), + ), + // BIT + (BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), + (BitOr, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), + // CMP + (Eq, s!(fn(a: Int, b: Int) -> bool[E::eq(a, b)])), + (Ne, s!(fn(a: Int, b: Int) -> bool[E::ne(a, b)])), + (Le, s!(fn(a: Int, b: Int) -> bool[E::le(a, b)])), + (Ge, s!(fn(a: Int, b: Int) -> bool[E::ge(a, b)])), + (Lt, s!(fn(a: Int, b: Int) -> bool[E::lt(a, b)])), + (Gt, s!(fn(a: Int, b: Int) -> bool[E::gt(a, b)])), + ] + }) +} + +#[rustfmt::skip] +pub(crate) fn mk_bool_bin_ops() -> impl IntoIterator)> { + use mir::BinOp::*; + define_btys! { let bool = BaseTy::Bool; } + [ + // BIT + (BitAnd, s!(fn(a: bool, b: bool) -> bool[E::and([a, b])])), + (BitOr, s!(fn(a: bool, b: bool) -> bool[E::or([a, b])])), + // CMP + (Eq, s!(fn(a: bool, b: bool) -> bool[E::eq(a, b)])), + (Ne, s!(fn(a: bool, b: bool) -> bool[E::ne(a, b)])), + (Le, s!(fn(a: bool, b: bool) -> bool[E::implies(a, b)])), + (Ge, s!(fn(a: bool, b: bool) -> bool[E::implies(b, a)])), + (Lt, s!(fn(a: bool, b: bool) -> bool[E::and([a.not(), b])])), + (Gt, s!(fn(a: bool, b: bool) -> bool[E::and([a, b.not()])])), + ] +} + +#[rustfmt::skip] +pub(crate) fn mk_shift_ops() -> impl IntoIterator)> { + use mir::BinOp::*; + iproduct!(INT_TYS, UINT_TYS) + .flat_map(|(int_ty, uint_ty)|{ + define_btys! { + let Int = BaseTy::Int(int_ty); + let Uint = BaseTy::Uint(uint_ty); + } + [ + (Shl, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })), + (Shl, s!(fn(a: Int, b: Uint) -> Int{ v: E::tt() })), + (Shr, s!(fn(a: Int, b: Int) -> Int{ v: E::tt() })), + (Shr, s!(fn(a: Int, b: Uint) -> Int{ v: E::tt() })), + + (Shl, s!(fn(a: Uint, b: Int) -> Uint{ v: E::tt() })), + (Shl, s!(fn(a: Uint, b: Uint) -> Uint{ v: E::tt() })), + (Shr, s!(fn(a: Uint, b: Int) -> Uint{ v: E::tt() })), + (Shr, s!(fn(a: Uint, b: Uint) -> Uint{ v: E::tt() })), + ] + }) +} diff --git a/flux-refineck/src/sigs/mod.rs b/flux-refineck/src/sigs/mod.rs new file mode 100644 index 0000000000..b61bb4cf97 --- /dev/null +++ b/flux-refineck/src/sigs/mod.rs @@ -0,0 +1,116 @@ +mod default; +mod overflow; + +use flux_middle::{ + rty::{BaseTy, Expr, IntTy, UintTy}, + rustc::mir, +}; +use rustc_hash::FxHashMap; + +use crate::constraint_gen::ConstrReason; + +pub struct Sig { + pub args: [BaseTy; N], + pub pre: Pre, + pub out: Output, +} + +pub enum Pre { + None, + Some(ConstrReason, Box Expr + Sync + Send>), +} + +#[derive(Clone)] +pub enum Output { + Indexed(BaseTy, fn([Expr; N]) -> Expr), + Exists(BaseTy, fn(Expr, [Expr; N]) -> Expr), +} + +struct SigTable { + map: FxHashMap<(T, [BaseTy; N]), Sig>, +} + +pub fn get_bin_op_sig( + op: mir::BinOp, + bty1: &BaseTy, + bty2: &BaseTy, + check_overflow: bool, +) -> &'static Sig<2> { + let table = if check_overflow { &overflow::BIN_OPS } else { &default::BIN_OPS }; + table.get(op, [bty1.clone(), bty2.clone()]) +} + +#[macro_export] +macro_rules! _define_btys { + ($(let $name:ident = $bty:expr;)*) => { + #[allow(unused_macros)] + macro_rules! bty { + $( + ($name) => { + $bty + }; + )* + } + }; +} +use crate::_define_btys as define_btys; + +#[macro_export] +macro_rules! _sig { + (fn ($($arg:ident:$ty:ident),+) -> $($rest:tt)+) => {{ + let (pre, out) = s!(($($arg),+) $($rest)+) ; + let args = [$(bty!($ty)),+]; + $crate::sigs::Sig { args, pre, out } + }}; + (($($args:ident),+) $bty:ident[$out:expr] $($rest:tt)*) => {{ + let bty = bty!($bty); + #[allow(unused_variables)] + let pre = s!(($($args),+) $($rest)*); + #[allow(unused_variables)] + let out = $crate::sigs::Output::Indexed(bty, |[$($args),+]| $out); + (pre, out) + }}; + (($($args:ident),+) $bty:ident{$v:ident : $out:expr} $($rest:tt)*) => {{ + let bty = bty!($bty); + #[allow(unused_variables)] + let pre = s!(($($args),+) $($rest)*); + #[allow(unused_variables)] + let out = $crate::sigs::Output::Exists(bty, |$v, [$($args),+]| $out); + (pre, out) + }}; + (($($args:ident),+)) => { + $crate::sigs::Pre::None + }; + (($($args:ident),+) requires $pre:expr => $tag:path) => { + $crate::sigs::Pre::Some($tag, Box::new(move |[$($args),+]| $pre)) + }; +} + +use crate::_sig as s; + +impl SigTable { + fn new() -> Self { + Self { map: FxHashMap::default() } + } +} + +impl SigTable +where + T: std::hash::Hash + Eq, +{ + fn extend(&mut self, iter: impl IntoIterator)>) { + self.map.extend( + iter.into_iter() + .map(|(op, sig)| ((op, sig.args.clone()), sig)), + ); + } + + fn get(&self, op: T, btys: [BaseTy; N]) -> &Sig { + &self.map[&(op, btys)] + } +} + +static INT_TYS: [IntTy; 6] = + [IntTy::Isize, IntTy::I8, IntTy::I16, IntTy::I32, IntTy::I64, IntTy::I128]; +static UINT_TYS: [UintTy; 6] = + [UintTy::Usize, UintTy::U8, UintTy::U16, UintTy::U32, UintTy::U64, UintTy::U128]; diff --git a/flux-refineck/src/sigs/overflow.rs b/flux-refineck/src/sigs/overflow.rs new file mode 100644 index 0000000000..4639da7508 --- /dev/null +++ b/flux-refineck/src/sigs/overflow.rs @@ -0,0 +1,125 @@ +use std::sync::LazyLock; + +use flux_middle::{ + rty::{BaseTy, BinOp, Expr}, + rustc::mir, +}; + +use super::{Sig, SigTable}; +use crate::{ + constraint_gen::ConstrReason, + sigs::{define_btys, s, INT_TYS, UINT_TYS}, +}; + +type E = Expr; + +pub(super) static BIN_OPS: LazyLock> = LazyLock::new(|| { + let mut table = SigTable::new(); + + table.extend(mk_signed_bin_ops()); + table.extend(mk_unsigned_bin_ops()); + table.extend(super::default::mk_shift_ops()); + table.extend(super::default::mk_bool_bin_ops()); + + table +}); + +/// This set of signatures checks for overflow and underflow. They work in +/// tandem with the invariant for unsigned ints returned in +/// [`BaseTy::invariants`]. +/// +/// [`BaseTy::invariants`]: flux_middle::rty::BaseTy::invariants +#[rustfmt::skip] +fn mk_unsigned_bin_ops() -> impl Iterator)> { + use mir::BinOp::*; + UINT_TYS + .into_iter() + .flat_map(|uint_ty| { + define_btys! { + let bool = BaseTy::Bool; + let Uint = BaseTy::Uint(uint_ty); + } + let bit_width: u64 = uint_ty.bit_width().unwrap_or(flux_config::pointer_width().bits()); + [ + // ARITH + (Add, s!(fn(a: Uint, b: Uint) -> Uint[a + b] + requires E::le(a + b, E::uint_max(bit_width)) => ConstrReason::Overflow) + ), + (Mul, s!(fn(a: Uint, b: Uint) -> Uint[a * b] + requires E::le(a * b, E::uint_max(bit_width)) => ConstrReason::Overflow) + ), + (Sub, s!(fn(a: Uint, b: Uint) -> Uint[a - b] + requires E::ge(a - b, 0) => ConstrReason::Overflow) + ), + (Div, s!(fn(a: Uint, b: Uint) -> Uint[a / b] + requires E::ne(b, 0) => ConstrReason::Div), + ), + (Rem, s!(fn(a:Uint , b: Uint) -> Uint[E::binary_op(BinOp::Mod, a, b)] + requires E::ne(b, 0) => ConstrReason::Rem), + ), + // BIT + (BitAnd, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), + (BitOr, s!(fn(a: Uint, b: Uint) -> Uint{v: E::tt()})), + // CMP + (Eq, s!(fn(a: Uint, b: Uint) -> bool[E::eq(a, b)])), + (Ne, s!(fn(a: Uint, b: Uint) -> bool[E::ne(a, b)])), + (Le, s!(fn(a: Uint, b: Uint) -> bool[E::le(a, b)])), + (Ge, s!(fn(a: Uint, b: Uint) -> bool[E::ge(a, b)])), + (Lt, s!(fn(a: Uint, b: Uint) -> bool[E::lt(a, b)])), + (Gt, s!(fn(a: Uint, b: Uint) -> bool[E::gt(a, b)])), + ] + }) +} + +#[rustfmt::skip] +fn mk_signed_bin_ops() -> impl Iterator)> { + use mir::BinOp::*; + INT_TYS + .into_iter() + .flat_map(|int_ty| { + define_btys! { + let bool = BaseTy::Bool; + let Int = BaseTy::Int(int_ty); + } + let bit_width: u64 = int_ty.bit_width().unwrap_or(flux_config::pointer_width().bits()); + [ + // ARITH + (Add, s!(fn(a: Int, b: Int) -> Int[a + b] + requires E::and([ + E::le(&a + &b, E::int_max(bit_width)), + E::ge(a + b, E::int_min(bit_width)) + ]) => ConstrReason::Overflow) + ), + (Sub, s!(fn(a: Int, b: Int) -> Int[a - b] + requires E::and([ + E::le(&a - &b, E::int_max(bit_width)), + E::ge(a - b, E::int_min(bit_width)) + ]) => ConstrReason::Overflow) + ), + (Mul, s!(fn(a: Int, b: Int) -> Int[a * b] + requires E::and([ + E::le(&a - &b, E::int_max(bit_width)), + E::ge(a - b, E::int_min(bit_width)) + ]) => ConstrReason::Overflow) + ), + (Div, s!(fn(a: Int, b: Int) -> Int[a / b] + requires E::ne(b, 0) => ConstrReason::Div), + ), + (Rem, s!(fn(a:Int , b: Int) -> Int{v: E::implies( + E::and([E::ge(&a, 0), E::ge(&b, 0)]), + E::eq(v, E::binary_op(BinOp::Mod, a, b))) } + requires E::ne(b, 0) => ConstrReason::Rem), + ), + // BIT + (BitAnd, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), + (BitOr, s!(fn(a: Int, b: Int) -> Int{v: E::tt()})), + // CMP + (Eq, s!(fn(a: Int, b: Int) -> bool[E::eq(a, b)])), + (Ne, s!(fn(a: Int, b: Int) -> bool[E::ne(a, b)])), + (Le, s!(fn(a: Int, b: Int) -> bool[E::le(a, b)])), + (Ge, s!(fn(a: Int, b: Int) -> bool[E::ge(a, b)])), + (Lt, s!(fn(a: Int, b: Int) -> bool[E::lt(a, b)])), + (Gt, s!(fn(a: Int, b: Int) -> bool[E::gt(a, b)])), + ] + }) +} diff --git a/flux-syntax/src/lib.rs b/flux-syntax/src/lib.rs index 0c76c943a0..4a3edb6d75 100644 --- a/flux-syntax/src/lib.rs +++ b/flux-syntax/src/lib.rs @@ -2,7 +2,6 @@ #![feature(rustc_private, box_patterns, let_chains, type_alias_impl_trait)] extern crate rustc_ast; -extern crate rustc_errors; extern crate rustc_hir; extern crate rustc_middle; extern crate rustc_span; diff --git a/flux-tests/tests/neg/config/test-config00.rs b/flux-tests/tests/neg/config/test-config00.rs index 1c65fb471b..164e9be8f5 100755 --- a/flux-tests/tests/neg/config/test-config00.rs +++ b/flux-tests/tests/neg/config/test-config00.rs @@ -1,7 +1,7 @@ #![feature(register_tool)] #![register_tool(flux)] #![feature(custom_inner_attributes)] -#![flux::cfg(log_dir = "./log", dump_constraint = "do it!")] //~ ERROR invalid flux configuration: incorrect type in value for setting `dump_constraint`, expected bool +#![flux::cfg(check_overflow = "do it!")] //~ ERROR invalid flux configuration: 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/flux-tests/tests/neg/surface/binop_overflow.rs b/flux-tests/tests/neg/surface/binop_overflow.rs index 1ca480588a..048174a8c2 100644 --- a/flux-tests/tests/neg/surface/binop_overflow.rs +++ b/flux-tests/tests/neg/surface/binop_overflow.rs @@ -1,8 +1,6 @@ -// ignore-test -// TODO: Uncomment when we can set flags on a per-test basis. Add the ERROR -// overflow comment on the lines too. -#![feature(register_tool)] +#![feature(register_tool, custom_inner_attributes)] #![register_tool(flux)] +#![flux::cfg(check_overflow = true)] // Arithmetic BinOps // These check for over/underflow diff --git a/flux-tests/tests/pos/surface/binop_overflow.rs b/flux-tests/tests/pos/surface/binop_overflow.rs index eb6706c1bb..d7322dcca7 100644 --- a/flux-tests/tests/pos/surface/binop_overflow.rs +++ b/flux-tests/tests/pos/surface/binop_overflow.rs @@ -1,7 +1,6 @@ -// ignore-test -// TODO: Uncomment when we can set flags on a per-test basis -#![feature(register_tool)] +#![feature(register_tool, custom_inner_attributes)] #![register_tool(flux)] +#![flux::cfg(check_overflow = true)] // Arithmetic BinOps //