From 9533d9c27b793c7653b03abd1946ddd5ceaf4b49 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 17:53:31 -0800 Subject: [PATCH 1/4] more push/scope/mysteries --- crates/flux-infer/src/infer.rs | 4 ++++ crates/flux-refineck/src/checker.rs | 7 ++++++- crates/flux-refineck/src/lib.rs | 4 +++- crates/flux-refineck/src/type_env.rs | 6 ++++-- 4 files changed, 17 insertions(+), 4 deletions(-) diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index bc5dd7cbb6..abbfe108ea 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -61,6 +61,7 @@ pub enum ConstrReason { Assign, Ret, Fold, + FoldLocal, Assert(&'static str), Div, Rem, @@ -548,6 +549,7 @@ impl Sub { bug!("constraint types should removed by the unpacking"); } (_, TyKind::Exists(ctor_b)) => { + println!("TRACE: tys(1) enter_exists {a:?} <: {b:?}"); infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b)) } (_, TyKind::Constr(pred_b, ty_b)) => { @@ -555,6 +557,7 @@ impl Sub { self.tys(infcx, &a, ty_b) } (TyKind::Indexed(bty_a, idx_a), TyKind::Indexed(bty_b, idx_b)) => { + println!("TRACE: tys(1) enter_exists {a:?} <: {b:?}"); self.btys(infcx, bty_a, bty_b)?; self.idxs_eq(infcx, idx_a, idx_b); Ok(()) @@ -725,6 +728,7 @@ impl Sub { } fn idxs_eq(&mut self, infcx: &mut InferCtxt, a: &Expr, b: &Expr) { + println!("TRACE: idxs_eq {a:?} - {b:?}"); if a == b { return; } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 66eed5ed0a..6e0f67a81c 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -812,6 +812,9 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { at.check_pred(requires, ConstrReason::Call); } + println!("TRACE: check_call (0) {env:?}"); + println!("TRACE: check_call (1) {actuals:?} <: {:?}", fn_sig.inputs()); + // Check arguments for (actual, formal) in iter::zip(actuals, fn_sig.inputs()) { at.fun_arg_subtyping(env, &actual, formal, ConstrReason::Call) @@ -827,9 +830,11 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { .replace_evars(&evars_sol) .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort)); + infcx.push_scope(); env.update_ensures(infcx, &output, self.check_overflow()); - fold_local_ptrs(infcx, env, span)?; + let evars_sol = infcx.pop_scope().with_span(span)?; + infcx.replace_evars(&evars_sol); Ok(output.ret) } diff --git a/crates/flux-refineck/src/lib.rs b/crates/flux-refineck/src/lib.rs index 9573f9c488..39bceb97ce 100644 --- a/crates/flux-refineck/src/lib.rs +++ b/crates/flux-refineck/src/lib.rs @@ -220,7 +220,9 @@ fn report_errors(genv: GlobalEnv, errors: Vec) -> Result<(), ErrorGuarantee ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }), ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }), ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }), - ConstrReason::Fold => genv.sess().emit_err(errors::FoldError { span }), + ConstrReason::Fold | ConstrReason::FoldLocal => { + genv.sess().emit_err(errors::FoldError { span }) + } ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }), ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }), }); diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 8babfd6b39..1e47dc686e 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -228,7 +228,8 @@ impl<'a> TypeEnv<'a> { pub(crate) fn fold_local_ptrs(&mut self, infcx: &mut InferCtxtAt) -> InferResult<()> { for (loc, bound, ty) in self.bindings.local_ptrs() { - infcx.subtyping(&ty, &bound, ConstrReason::Fold)?; + println!("TRACE: fold_local_ptrs AT {loc:?} : {ty:?} <: {bound:?}"); + infcx.subtyping(&ty, &bound, ConstrReason::FoldLocal)?; self.bindings.remove_local(&loc); } Ok(()) @@ -271,7 +272,8 @@ impl<'a> TypeEnv<'a> { // https://github.com/flux-rs/flux/issues/725#issuecomment-2295065634 Ok(result.ty) } else { - tracked_span_bug!("cannot move out of {place:?}"); + // tracked_span_bug!("cannot move out of {place:?}"); + panic!("cannot move out of {place:?}"); } } From a49d975cb2d90cd5673ad41ecdbf303f6afb36fd Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 17:54:24 -0800 Subject: [PATCH 2/4] more push/scope/mysteries --- crates/flux-infer/src/infer.rs | 3 --- crates/flux-refineck/src/checker.rs | 3 --- crates/flux-refineck/src/type_env.rs | 1 - 3 files changed, 7 deletions(-) diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index abbfe108ea..77a3cb95f8 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -549,7 +549,6 @@ impl Sub { bug!("constraint types should removed by the unpacking"); } (_, TyKind::Exists(ctor_b)) => { - println!("TRACE: tys(1) enter_exists {a:?} <: {b:?}"); infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b)) } (_, TyKind::Constr(pred_b, ty_b)) => { @@ -557,7 +556,6 @@ impl Sub { self.tys(infcx, &a, ty_b) } (TyKind::Indexed(bty_a, idx_a), TyKind::Indexed(bty_b, idx_b)) => { - println!("TRACE: tys(1) enter_exists {a:?} <: {b:?}"); self.btys(infcx, bty_a, bty_b)?; self.idxs_eq(infcx, idx_a, idx_b); Ok(()) @@ -728,7 +726,6 @@ impl Sub { } fn idxs_eq(&mut self, infcx: &mut InferCtxt, a: &Expr, b: &Expr) { - println!("TRACE: idxs_eq {a:?} - {b:?}"); if a == b { return; } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 6e0f67a81c..b63164f52a 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -812,9 +812,6 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { at.check_pred(requires, ConstrReason::Call); } - println!("TRACE: check_call (0) {env:?}"); - println!("TRACE: check_call (1) {actuals:?} <: {:?}", fn_sig.inputs()); - // Check arguments for (actual, formal) in iter::zip(actuals, fn_sig.inputs()) { at.fun_arg_subtyping(env, &actual, formal, ConstrReason::Call) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 1e47dc686e..10f5f38b7d 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -228,7 +228,6 @@ impl<'a> TypeEnv<'a> { pub(crate) fn fold_local_ptrs(&mut self, infcx: &mut InferCtxtAt) -> InferResult<()> { for (loc, bound, ty) in self.bindings.local_ptrs() { - println!("TRACE: fold_local_ptrs AT {loc:?} : {ty:?} <: {bound:?}"); infcx.subtyping(&ty, &bound, ConstrReason::FoldLocal)?; self.bindings.remove_local(&loc); } From 84d3741a47aed43c31349c650d6e21605588e089 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 17:54:32 -0800 Subject: [PATCH 3/4] more push/scope/mysteries --- tests/tests/todo/issue-899c.rs | 58 ++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 tests/tests/todo/issue-899c.rs diff --git a/tests/tests/todo/issue-899c.rs b/tests/tests/todo/issue-899c.rs new file mode 100644 index 0000000000..8475c2dee1 --- /dev/null +++ b/tests/tests/todo/issue-899c.rs @@ -0,0 +1,58 @@ +use core::slice::{Iter, SliceIndex}; + + +pub trait Queue { + /// Returns true if the queue is full, false otherwise. + fn is_full(&self) -> bool; + + /// If the queue isn't full, add a new element to the back of the queue. + /// Returns whether the element was added. + #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)] + fn enqueue(&mut self, val: T) -> bool; +} + + +#[flux_rs::extern_spec] +impl [T] { + #[flux_rs::sig(fn(&[T][@len]) -> usize[len])] + fn len(v: &[T]) -> usize; +} + + +#[flux_rs::refined_by(ring_len: int, hd: int, tl: int)] +#[flux_rs::invariant(ring_len > 1)] +pub struct RingBuffer<'a, T: 'a> { + #[field({&mut [T][ring_len] | ring_len > 1})] + ring: &'a mut [T], + #[field({usize[hd] | hd < ring_len})] + head: usize, + #[field({usize[tl] | tl < ring_len})] + tail: usize, +} + +impl Queue for RingBuffer<'_, T> { + fn is_full(&self) -> bool { + self.head == ((self.tail + 1) % self.ring.len()) + } + + #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)] + fn enqueue(&mut self, val: T) -> bool { + if self.is_full() { + // Incrementing tail will overwrite head + false + } else { + self.ring[self.tail] = val; + self.tail = (self.tail + 1) % self.ring.len(); + true + } + } +} + +// This code causes an ICE +fn get_ring_buffer() -> &'static mut RingBuffer<'static, usize> {unimplemented!()} + +fn enqueue_task() { + let rb = get_ring_buffer(); + rb.enqueue(3); +} + From dc4576c2cc5b213167ed76870b6ba92f0c32b874 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 22 Nov 2024 17:55:58 -0800 Subject: [PATCH 4/4] more push/scope/mysteries --- crates/flux-refineck/src/type_env.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 10f5f38b7d..af29db786f 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -271,8 +271,7 @@ impl<'a> TypeEnv<'a> { // https://github.com/flux-rs/flux/issues/725#issuecomment-2295065634 Ok(result.ty) } else { - // tracked_span_bug!("cannot move out of {place:?}"); - panic!("cannot move out of {place:?}"); + tracked_span_bug!("cannot move out of {place:?}"); } }