Enable overflow tests (#428)

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<Value> = LazyLock::new(|| {
         toml::from_str("").unwrap()
     }
 });
+
+impl Default for CrateConfig {
+    fn default() -> Self {
+        Self { check_overflow: check_overflow() }
+    }
+}

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

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<CrateConfig>,
+    ) -> 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)?;

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<config::CrateConfig, errors::CFGError> {
-        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)
     }
 }
 

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()

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<FnOutput>,
         dominators: &'a Dominators<BasicBlock>,
         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<ShapeResult, CheckerError> {
         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(

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