From 919f2e769566bd078fdd42998403e11f0d67e8b5 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 19 Feb 2022 22:48:44 -0500 Subject: [PATCH] add safety docs In principle this can be checked by the clippy::undocumented_unsafe_blocks lint, and I used the lint to find the issues. In practice the lint is buggy and so cannot safely be enabled in CI. Hopefully it will be fixed within a few stable version releases; keep your eyes on https://github.com/rust-lang/rust-clippy/issues/8449 . --- mm0-rs/components/mm0_util/src/lib.rs | 6 +- .../components/mm0_util/src/lined_string.rs | 18 +++-- mm0-rs/components/mm0b_parser/src/lib.rs | 1 + mm0-rs/components/mm1_parser/src/lib.rs | 1 + mm0-rs/components/mmcc/src/lib.rs | 1 + mm0-rs/src/compiler.rs | 24 +++++-- mm0-rs/src/doc/mod.rs | 18 ++++- mm0-rs/src/elab.rs | 3 + mm0-rs/src/elab/environment.rs | 7 +- mm0-rs/src/elab/frozen.rs | 71 ++++++++++++++++--- mm0-rs/src/elab/inout.rs | 6 +- mm0-rs/src/elab/lisp.rs | 20 +++++- mm0-rs/src/elab/lisp/eval.rs | 2 +- mm0-rs/src/elab/lisp/parser.rs | 1 + mm0-rs/src/elab/lisp/pretty.rs | 12 +++- mm0-rs/src/elab/lisp/print.rs | 3 +- mm0-rs/src/elab/math_parser.rs | 19 +++-- mm0-rs/src/elab/spans.rs | 15 ++-- mm0-rs/src/lib.rs | 4 +- mm0-rs/src/server.rs | 26 +++++-- 20 files changed, 202 insertions(+), 56 deletions(-) diff --git a/mm0-rs/components/mm0_util/src/lib.rs b/mm0-rs/components/mm0_util/src/lib.rs index 91f8a1f8..35765265 100644 --- a/mm0-rs/components/mm0_util/src/lib.rs +++ b/mm0-rs/components/mm0_util/src/lib.rs @@ -30,6 +30,7 @@ clippy::rc_buffer, clippy::rest_pat_in_fully_bound_structs, clippy::string_add, + clippy::undocumented_unsafe_blocks, clippy::unwrap_used )] // all the clippy lints we don't want @@ -384,10 +385,11 @@ pub struct SliceUninit(Box<[MaybeUninit]>); impl SliceUninit { /// Create a new uninitialized slice of length `size`. + #[inline] #[must_use] pub fn new(size: usize) -> Self { let mut res = Vec::with_capacity(size); - // safety: the newly constructed elements have type MaybeUninit + // Safety: the newly constructed elements have type MaybeUninit // so it's fine to not initialize them unsafe { res.set_len(size) }; Self(res.into_boxed_slice()) @@ -396,6 +398,7 @@ impl SliceUninit { /// Assign the value `val` to location `i` of the slice. Warning: this does not /// call the destructor for `T` on the previous value, so this should be used only /// once per location unless `T` has no `Drop` impl. + #[inline] pub fn set(&mut self, i: usize, val: T) { self.0[i] = MaybeUninit::new(val) } /// Finalizes the construction, returning an initialized `Box<[T]>`. @@ -403,6 +406,7 @@ impl SliceUninit { /// # Safety /// /// This causes undefined behavior if the content is not fully initialized. + #[inline] #[must_use] pub unsafe fn assume_init(self) -> Box<[T]> { unsafe { mem::transmute(self.0) } } } diff --git a/mm0-rs/components/mm0_util/src/lined_string.rs b/mm0-rs/components/mm0_util/src/lined_string.rs index 61343e08..44287fa5 100644 --- a/mm0-rs/components/mm0_util/src/lined_string.rs +++ b/mm0-rs/components/mm0_util/src/lined_string.rs @@ -70,16 +70,26 @@ impl LinedString { lines } + /// Returns the index of the start of the line, and the line number. + #[must_use] + pub fn get_line(&self, line: usize) -> Option { self.lines.get(line).copied() } + + /// Returns the index of the start of the line, and the line number. + #[must_use] + pub fn line_start(&self, idx: usize) -> (usize, usize) { + match self.lines.binary_search(&idx) { + Ok(n) => (idx, n + 1), + Err(n) => (n.checked_sub(1).map_or(0, |i| self.lines[i]), n), + } + } + /// Turn a byte index into an LSP [`Position`] /// /// # Safety /// `idx` must be a valid index in the string. #[must_use] pub fn to_pos(&self, idx: usize) -> Position { - let (pos, line) = match self.lines.binary_search(&idx) { - Ok(n) => (idx, n + 1), - Err(n) => (n.checked_sub(1).map_or(0, |i| self.lines[i]), n), - }; + let (pos, line) = self.line_start(idx); Position { line: line.try_into().expect("too many lines"), character: if self.unicode { diff --git a/mm0-rs/components/mm0b_parser/src/lib.rs b/mm0-rs/components/mm0b_parser/src/lib.rs index c8cb2359..2ccfba65 100644 --- a/mm0-rs/components/mm0b_parser/src/lib.rs +++ b/mm0-rs/components/mm0b_parser/src/lib.rs @@ -31,6 +31,7 @@ clippy::rc_buffer, clippy::rest_pat_in_fully_bound_structs, clippy::string_add, + clippy::undocumented_unsafe_blocks, clippy::unwrap_used )] // all the clippy lints we don't want diff --git a/mm0-rs/components/mm1_parser/src/lib.rs b/mm0-rs/components/mm1_parser/src/lib.rs index 881863dd..2c41f47e 100644 --- a/mm0-rs/components/mm1_parser/src/lib.rs +++ b/mm0-rs/components/mm1_parser/src/lib.rs @@ -34,6 +34,7 @@ clippy::rc_buffer, clippy::rest_pat_in_fully_bound_structs, clippy::string_add, + clippy::undocumented_unsafe_blocks, clippy::unwrap_used, clippy::wrong_pub_self_convention )] diff --git a/mm0-rs/components/mmcc/src/lib.rs b/mm0-rs/components/mmcc/src/lib.rs index 1a22ba5c..fecc5dac 100644 --- a/mm0-rs/components/mmcc/src/lib.rs +++ b/mm0-rs/components/mmcc/src/lib.rs @@ -33,6 +33,7 @@ clippy::rc_buffer, clippy::rest_pat_in_fully_bound_structs, clippy::string_add, + clippy::undocumented_unsafe_blocks, clippy::unwrap_used, )] // all the clippy lints we don't want diff --git a/mm0-rs/src/compiler.rs b/mm0-rs/src/compiler.rs index 2aed89a9..5323ee59 100644 --- a/mm0-rs/src/compiler.rs +++ b/mm0-rs/src/compiler.rs @@ -84,6 +84,10 @@ impl FileContents { pub(crate) fn new_bin_from_file(path: &std::path::Path) -> io::Result { #[cfg(not(target_arch = "wasm32"))] { let file = fs::File::open(path)?; + // Safety: Well, memory mapping files is never totally safe, but we're assuming + // some reasonableness assumptions on the part of the user here. + // If they delete the file from under us then interesting things will happen. + // (I blame linux for not having a sensible locking model.) Ok(Self::new_mmap(unsafe { memmap::MmapOptions::new().map(&file)? })) } #[cfg(target_arch = "wasm32")] { @@ -223,10 +227,13 @@ impl ElabErrorKind { fn make_snippet<'a>(path: &'a FileRef, file: &'a LinedString, pos: Span, msg: &'a str, level: ErrorLevel, footer: Vec>) -> Snippet<'a> { let annotation_type = level.to_annotation_type(); - let Range {start, end} = file.to_range(pos); - let start2 = pos.start - start.character as usize; + let (start, start_line) = file.line_start(pos.start); + let (_, end_line) = file.line_start(pos.end); #[allow(clippy::or_fun_call)] - let end2 = file.to_idx(Position {line: end.line + 1, character: 0}).unwrap_or(file.len()); + let end = file.to_idx(Position { + line: u32::try_from(end_line).expect("too many lines") + 1, + character: 0 + }).unwrap_or(file.len()); Snippet { title: Some(Annotation { id: None, @@ -234,12 +241,15 @@ fn make_snippet<'a>(path: &'a FileRef, file: &'a LinedString, pos: Span, annotation_type, }), slices: vec![Slice { - source: unsafe {std::str::from_utf8_unchecked(&file[(start2..end2).into()])}, - line_start: start.line as usize + 1, + source: { + // Safety: We assume `Span` is coming from the correct file, + unsafe { std::str::from_utf8_unchecked(&file[(start..end).into()]) } + }, + line_start: start_line + 1, origin: Some(path.rel()), - fold: end.line - start.line >= 5, + fold: end_line - start_line >= 5, annotations: vec![SourceAnnotation { - range: (pos.start - start2, pos.end - start2), + range: (pos.start - start, pos.end - start), label: "", annotation_type, }], diff --git a/mm0-rs/src/doc/mod.rs b/mm0-rs/src/doc/mod.rs index 35170d12..76afe3e2 100644 --- a/mm0-rs/src/doc/mod.rs +++ b/mm0-rs/src/doc/mod.rs @@ -289,6 +289,7 @@ impl<'a> LayoutProof<'a> { ProofNode::Thm {thm, ref args, ref res} => { let td = &self.env.thms[thm]; let mut hyps = SliceUninit::new(td.hyps.len()); + assert!(td.args.len() + td.hyps.len() == args.len()); if self.rev { for (i, e) in args[td.args.len()..].iter().enumerate().rev() { hyps.set(i, self.layout(e).into_proof()) @@ -299,7 +300,9 @@ impl<'a> LayoutProof<'a> { } } let res = self.layout(res).into_expr(); - LayoutResult::Proof(self.push_line(unsafe {hyps.assume_init()}, LineKind::Thm(thm), res)) + // Safety: We checked that the length matches, and we initialize + // every element exactly once in forward or reverse order. + LayoutResult::Proof(self.push_line(unsafe { hyps.assume_init() }, LineKind::Thm(thm), res)) } ProofNode::Conv(ref p) => { let n = self.layout(&p.2).into_proof(); @@ -405,7 +408,10 @@ struct CaseInsensitiveName(ArcString); impl<'a> From<&'a ArcString> for &'a CaseInsensitiveName { #[allow(clippy::transmute_ptr_to_ptr)] - fn from(s: &'a ArcString) -> Self { unsafe { mem::transmute(s) } } + fn from(s: &'a ArcString) -> Self { + // Safety: CaseInsensitiveName is repr(transparent) + unsafe { mem::transmute(s) } + } } impl Hash for CaseInsensitiveName { fn hash(&self, state: &mut H) { @@ -531,6 +537,9 @@ impl<'a, W: Write> BuildDoc<'a, W> { ) -> io::Result { let mut path = self.thm_folder.clone(); #[allow(clippy::useless_transmute)] + // Safety: This is a lifetime hack. We need to pass a mutable Environment to render_proof + // because LayoutProof::layout calls Environment::get_atom which mutates the env.data field. + // This is disjoint from the reference to env.thms that we retain here, so it's okay. let td: &Thm = unsafe { mem::transmute(&self.env.thms[tid]) }; self.mangler.mangle(&self.env, tid, |_, s| path.push(&format!("{}.html", s))); let mut file = BufWriter::new(File::create(&path)?); @@ -545,7 +554,9 @@ impl<'a, W: Write> BuildDoc<'a, W> { .expect("writing to a string")); } nav.push_str("index"); if let Some(base) = &self.base_url { use std::fmt::Write; @@ -579,6 +590,7 @@ impl<'a, W: Write> BuildDoc<'a, W> { \n \ StepHypRefExpression\ ")?; + // double borrow here, see safety comment render_proof(self.source, &mut self.env, &mut self.mangler, &mut file, self.order, &td.args, &td.hyps, pf)?; writeln!(file, " \n ")?; diff --git a/mm0-rs/src/elab.rs b/mm0-rs/src/elab.rs index 7e0c6fea..2a803dd0 100644 --- a/mm0-rs/src/elab.rs +++ b/mm0-rs/src/elab.rs @@ -696,6 +696,7 @@ where F: FnMut(FileRef) -> Result>, BoxError> { impl Future for ElabFuture { type Output = (Option>, Vec, Vec, FrozenEnv); fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> Poll { + // Safety: We don't move `this` out of the pin let this = &mut unsafe { self.get_unchecked_mut() }.0; let ElabFutureInner { elab: FrozenElaborator(elab), @@ -706,6 +707,8 @@ where F: FnMut(FileRef) -> Result>, BoxError> { match progress { UnfinishedStmt::None => {}, UnfinishedStmt::Import(sp, p, other) => { + // Safety: `other` is pinned because it is projected from + // `this.progress` which is pinned match ready!(unsafe { Pin::new_unchecked(other) }.poll(cx)) { Ok(ElabResult::Ok(t, errors, env)) => { toks.push(t); diff --git a/mm0-rs/src/elab/environment.rs b/mm0-rs/src/elab/environment.rs index a0b16880..a50f1776 100644 --- a/mm0-rs/src/elab/environment.rs +++ b/mm0-rs/src/elab/environment.rs @@ -539,14 +539,16 @@ impl ObjectKind { /// Because this function calls [`FrozenLispVal::new`], /// the resulting object must not be examined before the elaborator is frozen. #[must_use] pub fn expr(e: LispVal) -> ObjectKind { - ObjectKind::Expr(unsafe {FrozenLispVal::new(e)}) + // Safety: ObjectKind objects are write-only during the construction phase + ObjectKind::Expr(unsafe { FrozenLispVal::new(e) }) } /// Create an [`ObjectKind`] for a [`Proof`]. /// # Safety /// Because this function calls [`FrozenLispVal::new`], /// the resulting object must not be examined before the elaborator is frozen. #[must_use] pub fn proof(e: LispVal) -> ObjectKind { - ObjectKind::Proof(unsafe {FrozenLispVal::new(e)}) + // Safety: ObjectKind objects are write-only during the construction phase + ObjectKind::Proof(unsafe { FrozenLispVal::new(e) }) } } @@ -678,6 +680,7 @@ impl Remap for [A; N] { type Target = [A::Target; N]; fn remap(&self, r: &mut Remapper) -> Self::Target { let arr = self.iter().map(|e| e.remap(r)).collect::>(); + // Safety: We are collecting an iterator with exactly N elements, so it is initialized unsafe { arr.into_inner_unchecked() } } } diff --git a/mm0-rs/src/elab/frozen.rs b/mm0-rs/src/elab/frozen.rs index d19ea682..a25d7ab7 100644 --- a/mm0-rs/src/elab/frozen.rs +++ b/mm0-rs/src/elab/frozen.rs @@ -66,11 +66,15 @@ impl FrozenEnv { /// # Safety /// TODO: this gives out an `&Environment`, even though it is frozen. Don't abuse it #[must_use] pub unsafe fn format_env<'a>(&'a self, source: &'a LinedString) -> FormatEnv<'a> { + // Safety: ensured by caller FormatEnv { source, env: unsafe { self.thaw() } } } /// Get the list of [`Spans`] in the environment. - #[must_use] pub fn spans(&self) -> &[Spans] { &unsafe { self.thaw() }.spans } + #[must_use] pub fn spans(&self) -> &[Spans] { + // Safety: ObjectKind only contains frozen data + &unsafe { self.thaw() }.spans + } /// Get the [`Spans`] object corresponding to the statement that contains the given position, /// if one exists. @@ -80,27 +84,46 @@ impl FrozenEnv { /// Accessor for [`Environment::data`] #[must_use] pub fn data(&self) -> &AtomVec { + // Safety: Data is re-frozen, and the cast is safe because FrozenAtomData is repr(transparent) unsafe { &*<*const _>::cast(&self.thaw().data) } } /// Accessor for [`Environment::sorts`] - #[must_use] pub fn sorts(&self) -> &SortVec { &unsafe { self.thaw() }.sorts } + #[must_use] pub fn sorts(&self) -> &SortVec { + // Safety: `Sort` does not have any `LispVal`s + &unsafe { self.thaw() }.sorts + } /// Accessor for [`Environment::sorts`] #[must_use] pub fn sort(&self, s: SortId) -> &Sort { &self.sorts()[s] } /// Accessor for [`Environment::terms`] - #[must_use] pub fn terms(&self) -> &TermVec { &unsafe { self.thaw() }.terms } + #[must_use] pub fn terms(&self) -> &TermVec { + // Safety: `Term` does not have any `LispVal`s + &unsafe { self.thaw() }.terms + } /// Accessor for [`Environment::terms`] #[must_use] pub fn term(&self, t: TermId) -> &Term { &self.terms()[t] } /// Accessor for [`Environment::thms`] - #[must_use] pub fn thms(&self) -> &ThmVec { &unsafe { self.thaw() }.thms } + #[must_use] pub fn thms(&self) -> &ThmVec { + // Safety: `Thm` does not have any `LispVal`s + &unsafe { self.thaw() }.thms + } /// Accessor for [`Environment::thms`] #[must_use] pub fn thm(&self, t: ThmId) -> &Thm { &self.thms()[t] } /// Accessor for [`Environment::stmts`] - #[must_use] pub fn stmts(&self) -> &[StmtTrace] { &unsafe { self.thaw() }.stmts } + #[must_use] pub fn stmts(&self) -> &[StmtTrace] { + // Safety: `StmtTrace` does not have any `LispVal`s + &unsafe { self.thaw() }.stmts + } /// Parse a string into an atom. - #[must_use] pub fn get_atom(&self, s: &[u8]) -> Option { unsafe { self.thaw() }.atoms.get(s).copied() } + #[must_use] pub fn get_atom(&self, s: &[u8]) -> Option { + // Safety: we don't read any `LispVal`s + unsafe { self.thaw() }.atoms.get(s).copied() + } /// Accessor for [`Environment::pe`] - #[must_use] pub fn pe(&self) -> &ParserEnv { &unsafe { self.thaw() }.pe } + #[must_use] pub fn pe(&self) -> &ParserEnv { + // Safety: `ParserEnv` does not have any `LispVal`s + &unsafe { self.thaw() }.pe + } } /// A wrapper around an [`AtomData`] that is frozen. @@ -117,6 +140,7 @@ impl FrozenAtomData { #[must_use] pub fn decl(&self) -> Option { self.0.decl } /// Accessor for [`AtomData::lisp`] #[must_use] pub fn lisp(&self) -> &Option { + // Safety: Data is re-frozen, and the cast is safe because FrozenLispData is repr(transparent) unsafe { &*<*const _>::cast(&self.0.lisp) } } /// Accessor for [`AtomData::graveyard`] @@ -127,7 +151,8 @@ impl FrozenAtomData { #[derive(Debug)] pub struct FrozenMergeStrategyInner(MergeStrategyInner); /// A wrapper around a [`MergeStrategy`] that is frozen. -pub type FrozenMergeStrategy = Option>; +#[derive(Debug)] +pub struct FrozenMergeStrategy(MergeStrategy); /// A wrapper around a [`LispData`] that is frozen. #[derive(Debug, DeepSizeOf)] @@ -141,12 +166,16 @@ impl FrozenLispData { #[must_use] pub fn doc(&self) -> &Option { &self.0.doc } /// Accessor for [`LispData::doc`] #[must_use] pub fn merge(&self) -> &FrozenMergeStrategy { + // Safety: Input is frozen already unsafe { freeze_merge_strategy(&self.0.merge) } } } impl Deref for FrozenLispData { type Target = FrozenLispVal; - fn deref(&self) -> &FrozenLispVal { unsafe { self.0.val.freeze() } } + fn deref(&self) -> &FrozenLispVal { + // Safety: Input is frozen already + unsafe { self.0.val.freeze() } + } } /// A wrapper around a [`LispVal`] that is frozen. @@ -174,6 +203,7 @@ impl LispKind { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze(&self) -> &FrozenLispKind { + // Safety: The cast is safe because FrozenLispKind is repr(transparent) unsafe { &*<*const _>::cast(self) } } } @@ -183,6 +213,7 @@ impl LispVal { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze(&self) -> &FrozenLispVal { + // Safety: The cast is safe because FrozenLispVal is repr(transparent) unsafe { &*<*const _>::cast(self) } } } @@ -192,6 +223,7 @@ impl LispRef { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze(&self) -> &FrozenLispRef { + // Safety: The cast is safe because FrozenLispRef is repr(transparent) unsafe { &*<*const _>::cast(self) } } } @@ -200,6 +232,7 @@ impl LispRef { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze_merge_strategy(this: &MergeStrategy) -> &FrozenMergeStrategy { + // Safety: The cast is safe because FrozenMergeStrategy is repr(transparent) unsafe { &*<*const _>::cast(this) } } @@ -208,6 +241,7 @@ impl MergeStrategyInner { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze(&self) -> &FrozenMergeStrategyInner { + // Safety: The cast is safe because FrozenMergeStrategyInner is repr(transparent) unsafe { &*<*const _>::cast(self) } } } @@ -217,6 +251,7 @@ impl Proc { /// # Safety /// The data structure should not be modified, even via clones, while this reference is alive. #[must_use] pub unsafe fn freeze(&self) -> &FrozenProc { + // Safety: The cast is safe because FrozenProc is repr(transparent) unsafe { &*<*const _>::cast(self) } } } @@ -320,12 +355,16 @@ impl FrozenLispKind { impl Deref for FrozenLispVal { type Target = FrozenLispKind; - fn deref(&self) -> &FrozenLispKind { unsafe { self.thaw().deref().freeze() } } + fn deref(&self) -> &FrozenLispKind { + // Safety: Input is frozen already + unsafe { self.thaw().deref().freeze() } + } } impl Remap for FrozenMergeStrategyInner { type Target = MergeStrategyInner; fn remap(&self, r: &mut Remapper) -> MergeStrategyInner { + // Safety: Input is frozen already unsafe { match &self.0 { MergeStrategyInner::AtomMap(m) => @@ -337,6 +376,14 @@ impl Remap for FrozenMergeStrategyInner { } } +impl Remap for FrozenMergeStrategy { + type Target = MergeStrategy; + fn remap(&self, r: &mut Remapper) -> MergeStrategy { + // Safety: Input is frozen already + self.0.as_ref().map(|m| Rc::new(unsafe { m.freeze() }.remap(r))) + } +} + impl Remap for FrozenLispData { type Target = LispData; fn remap(&self, r: &mut Remapper) -> LispData { @@ -392,6 +439,7 @@ impl Remap for FrozenLispKind { impl Remap for FrozenLispRef { type Target = LispWeak; fn remap(&self, r: &mut Remapper) -> LispWeak { + // Safety: We ensure `LispWeak` are valid pointers or null, so they are safe to read unsafe { self.thaw().get_weak().map_unsafe(|e| e.freeze().remap(r)) } } } @@ -405,8 +453,10 @@ impl Remap for FrozenProc { Proc::Lambda {pos: pos.remap(r), env: env.remap(r), spec, code: code.remap(r)}, Proc::MatchCont(_) => Proc::MatchCont(Rc::new(Cell::new(false))), Proc::RefineCallback => Proc::RefineCallback, + // Safety: the merge strategy is already frozen Proc::MergeMap(m) => Proc::MergeMap(unsafe {freeze_merge_strategy(m)}.remap(r)), Proc::ProofThunk(x, m) => Proc::ProofThunk(x.remap(r), RefCell::new( + // Safety: the cell is frozen, so we must not change the borrow flag match &*unsafe { m.try_borrow_unguarded() }.expect("failed to deref ref") { Ok(e) => Ok(e.remap(r)), Err(v) => Err(v.remap(r)), @@ -428,6 +478,7 @@ impl FrozenLispRef { /// Dereference a [`FrozenLispRef`]. This can fail if the reference /// is a weak reference and the target is gone. #[must_use] pub fn get(&self) -> Option<&FrozenLispKind> { + // Safety: We ensure `LispWeak` are valid pointers or null, so they are safe to read unsafe { self.thaw().get_unsafe().map(|e| e.freeze()) } } } diff --git a/mm0-rs/src/elab/inout.rs b/mm0-rs/src/elab/inout.rs index 48939e86..d2aa5855 100644 --- a/mm0-rs/src/elab/inout.rs +++ b/mm0-rs/src/elab/inout.rs @@ -412,14 +412,14 @@ impl FrozenEnv { pub fn run_output(&self, w: impl io::Write) -> Result<(), (FileSpan, OutputError)> { let mut handler = None; let mut w = StringWriter {w, hex: None}; - let env = unsafe {self.thaw()}; + // Safety: We only use this environment to read non-lisp data. + let env = unsafe { self.thaw() }; for s in self.stmts() { if let StmtTrace::OutputString(os) = s { let OutputString {span, heap, exprs} = &**os; (|| -> Result<(), OutputError> { let terms = { - handler = Some(unsafe {self.thaw()}.new_string_handler() - .map_err(OutputError::String)?); + handler = Some(env.new_string_handler().map_err(OutputError::String)?); let_unchecked!(Some((_, t)) = &handler, t) }; env.write_output_string(terms, &mut w, heap, exprs) diff --git a/mm0-rs/src/elab/lisp.rs b/mm0-rs/src/elab/lisp.rs index da6c7076..819495b7 100644 --- a/mm0-rs/src/elab/lisp.rs +++ b/mm0-rs/src/elab/lisp.rs @@ -58,10 +58,11 @@ macro_rules! str_enum { } } #[doc=$from_bytes] + #[allow(clippy::undocumented_unsafe_blocks)] // rust-clippy#8449 #[must_use] pub fn from_bytes(s: &[u8]) -> Option { // Safety: the function we defined just above doesn't do anything // dangerous with the &str - Self::from_str(unsafe {std::str::from_utf8_unchecked(s)}) + Self::from_str(unsafe { std::str::from_utf8_unchecked(s) }) } /// Iterate over all the elements in the enum. @@ -511,10 +512,14 @@ impl LispWeak { Self::Strong(e) => e } } + + /// # Safety + /// If the pointer is a weak pointer it must point to valid memory pub(crate) unsafe fn map_unsafe(&self, f: impl FnOnce(&LispKind) -> LispVal) -> LispWeak { match self { LispWeak::Strong(e) => LispWeak::Strong(f(e)), LispWeak::Weak(e) if e.strong_count() == 0 => LispWeak::Weak(Weak::new()), + // Safety: The pointer must be valid LispWeak::Weak(e) => LispWeak::Weak(Rc::downgrade(&f(unsafe { &*e.as_ptr() }).0)), } } @@ -572,12 +577,15 @@ impl LispRef { /// /// [`FrozenLispRef::get`]: super::frozen::FrozenLispRef::get pub(crate) unsafe fn get_unsafe(&self) -> Option<&LispKind> { + // Safety: we can't modify the borrow flag because the data is frozen match unsafe { self.0.try_borrow_unguarded() }.unwrap_or_else(|_| { std::sync::atomic::fence(std::sync::atomic::Ordering::SeqCst); + // Safety: we can't modify the borrow flag because the data is frozen unsafe { self.0.try_borrow_unguarded() }.expect("could not deref refcell") }) { LispWeak::Strong(e) => Some(e), LispWeak::Weak(e) if e.strong_count() == 0 => None, + // Safety: `LispWeak` are null or valid so `as_ptr` is safe LispWeak::Weak(e) => Some(unsafe { &*e.as_ptr() }) } } @@ -1562,7 +1570,10 @@ impl Remap for Mutex { } impl Remap for LispVal { type Target = Self; - fn remap(&self, r: &mut Remapper) -> Self { unsafe { self.freeze() }.remap(r) } + fn remap(&self, r: &mut Remapper) -> Self { + // Safety: Remapping is only done to frozen databases + unsafe { self.freeze() }.remap(r) + } } impl Remap for InferTarget { @@ -1589,5 +1600,8 @@ impl Remap for ProcPos { impl Remap for Proc { type Target = Self; - fn remap(&self, r: &mut Remapper) -> Self { unsafe { self.freeze() }.remap(r) } + fn remap(&self, r: &mut Remapper) -> Self { + // Safety: Remapping is only done to frozen databases + unsafe { self.freeze() }.remap(r) + } } diff --git a/mm0-rs/src/elab/lisp/eval.rs b/mm0-rs/src/elab/lisp/eval.rs index 7f2d6955..9cb7c03d 100644 --- a/mm0-rs/src/elab/lisp/eval.rs +++ b/mm0-rs/src/elab/lisp/eval.rs @@ -1449,7 +1449,7 @@ impl<'a> Evaluator<'a> { match func { &Proc::Builtin(func) => self.evaluate_builtin(tail, sp, func, args)?, Proc::Lambda {pos, env, code, ..} => { - // Unfortunately we're fighting the borrow checker here. The problem is that + // Safety: Unfortunately we're fighting the borrow checker here. The problem is that // ir is borrowed in the Stack type, with most IR being owned outside the // function, but when you apply a lambda, the Proc::LambdaExact constructor // stores an Arc to the code to execute, hence it comes under our control, diff --git a/mm0-rs/src/elab/lisp/parser.rs b/mm0-rs/src/elab/lisp/parser.rs index 73724f77..7e286aca 100644 --- a/mm0-rs/src/elab/lisp/parser.rs +++ b/mm0-rs/src/elab/lisp/parser.rs @@ -321,6 +321,7 @@ impl Remap for Ir { fn remap(&self, r: &mut Remapper) -> Self { match self { &Ir::Global(sp, a) => Ir::Global(sp, a.remap(r)), + // Safety: The input Ir is already frozen Ir::Const(v) => Ir::Const(unsafe { v.freeze() }.remap(r)), &Ir::SetMergeStrategy(sp, a) => Ir::SetMergeStrategy(sp, a.remap(r)), &Ir::GlobalDef(sp, sp2, a) => Ir::GlobalDef(sp, sp2, a.remap(r)), diff --git a/mm0-rs/src/elab/lisp/pretty.rs b/mm0-rs/src/elab/lisp/pretty.rs index 6f46d749..cb78312d 100644 --- a/mm0-rs/src/elab/lisp/pretty.rs +++ b/mm0-rs/src/elab/lisp/pretty.rs @@ -124,7 +124,11 @@ const SOFTLINE_: RefDoc<'static> = pretty::RefDoc(&pretty::Doc::Group(LINE_)); fn covariant<'a>(from: RefDoc<'static>) -> RefDoc<'a> { #[allow(clippy::useless_transmute)] - unsafe {mem::transmute(from)} + // Safety: `RefDoc` is actually covariant. Rust is unable to prove this because of the + // Doc::Column and Doc::Nesting variants, which contain + // &'a (dyn Fn(usize) -> RefDoc<'a, _> + 'a), which is covariant + // in 'a even though rust doesn't try to reason about the changing return type. + unsafe { mem::transmute(from) } } impl<'a> Pretty<'a> { @@ -146,10 +150,12 @@ impl<'a> Pretty<'a> { } fn token(&'a self, tk: &'a [u8]) -> Pp<'a> { - Pp::token(self.alloc, &self.fe, unsafe {std::str::from_utf8_unchecked(tk)}) + // Safety: Tokens come from the ASCII text + Pp::token(self.alloc, &self.fe, unsafe { std::str::from_utf8_unchecked(tk) }) } fn word(&'a self, data: &'a [u8]) -> Pp<'a> { - Pp::word(self.alloc, unsafe {std::str::from_utf8_unchecked(data)}) + // Safety: Words come from the ASCII text + Pp::word(self.alloc, unsafe { std::str::from_utf8_unchecked(data) }) } pub(crate) fn alloc(&'a self, doc: Doc<'a>) -> RefDoc<'a> { diff --git a/mm0-rs/src/elab/lisp/print.rs b/mm0-rs/src/elab/lisp/print.rs index 4b1856b1..8518f06e 100644 --- a/mm0-rs/src/elab/lisp/print.rs +++ b/mm0-rs/src/elab/lisp/print.rs @@ -261,7 +261,8 @@ impl EnvDisplay for SExpr { fn fmt(&self, fe: FormatEnv<'_>, f: &mut fmt::Formatter<'_>) -> fmt::Result { match &self.k { &SExprKind::Atom(a) => { - unsafe {std::str::from_utf8_unchecked(span_atom(fe.source, self.span, a))}.fmt(f) + // Safety: Atoms are ASCII + unsafe { std::str::from_utf8_unchecked(span_atom(fe.source, self.span, a)) }.fmt(f) } SExprKind::List(es) => { let mut it = es.iter(); diff --git a/mm0-rs/src/elab/math_parser.rs b/mm0-rs/src/elab/math_parser.rs index 3cc2bafb..2d444c55 100644 --- a/mm0-rs/src/elab/math_parser.rs +++ b/mm0-rs/src/elab/math_parser.rs @@ -196,10 +196,10 @@ impl<'a> MathParser<'a> { let end = self.literals(&mut args, &info.lits, &mut consts, sp.end)?; let span = (start..end).into(); for sp in consts {self.spans.insert(sp, ObjectKind::Term(info.term, span));} - return Ok(QExpr { - span, - k: QExprKind::App(sp, info.term, unsafe { args.assume_init() }) - }) + // Safety: We checked in elab_gen_nota that the lits array contains every index, + // so every item in `args` gets initialized exactly once by the literals() call + let k = QExprKind::App(sp, info.term, unsafe { args.assume_init() }); + return Ok(QExpr { span, k }) } } } else if ident_start(c) && (sp.start + 1..sp.end).all(|i| ident_rest(self.source[i])) { @@ -256,8 +256,13 @@ impl<'a> MathParser<'a> { tok_end = self.peek_token(); }; let span = (start..end).into(); - for sp in consts {self.spans.insert(sp, ObjectKind::Term(info.term, span));} - lhs = QExpr { span, k: QExprKind::App(tk, info.term, unsafe { args.assume_init() }) }; + for sp in consts { self.spans.insert(sp, ObjectKind::Term(info.term, span)); } + // Safety: We checked in elab_gen_nota that the lits array contains every index, + // and also lits[1] must be Const(..) since lits[0] is Var(..), so even though + // we skip lits[1] in the cases above, every item in `args` gets initialized + // exactly once by the literals() call, because all the indices are in Var(..) entries + let k = QExprKind::App(tk, info.term, unsafe { args.assume_init() }); + lhs = QExpr { span, k }; } Ok(lhs) } @@ -266,4 +271,4 @@ impl<'a> MathParser<'a> { let lhs = self.prefix(p)?; self.lhs(p, lhs) } -} \ No newline at end of file +} diff --git a/mm0-rs/src/elab/spans.rs b/mm0-rs/src/elab/spans.rs index 222cbb81..18f6c44e 100644 --- a/mm0-rs/src/elab/spans.rs +++ b/mm0-rs/src/elab/spans.rs @@ -75,7 +75,10 @@ impl Spans { /// This function must only be called if [`set_stmt`](Self::set_stmt) has previously /// been called. We ensure that this is the case for any [`Spans`] object put into /// [`Environment.spans`]. - #[must_use] pub fn stmt(&self) -> Span { unsafe { self.stmt.assume_init() } } + #[must_use] pub fn stmt(&self) -> Span { + // Safety: by assumption + unsafe { self.stmt.assume_init() } + } /// Get the `decl` field of a [`Spans`]. /// @@ -84,7 +87,10 @@ impl Spans { /// been called. We ensure that this is the case for any [`Spans`] object put into /// [`Environment.spans`], but only for declarations that actually have names. /// (This function is also currently unused.) - #[must_use] pub fn decl(&self) -> AtomId { unsafe { self.decl.assume_init() } } + #[must_use] pub fn decl(&self) -> AtomId { + // Safety: by assumption + unsafe { self.decl.assume_init() } + } /// Insert a new data element at a given span. pub fn insert<'a>(&'a mut self, sp: Span, val: T) -> &'a mut T { @@ -107,9 +113,8 @@ impl Spans { if sp == *sp1 { // return k; // we would like to write this #[allow(clippy::useless_transmute)] - return unsafe { // safety, see above. We know we are in the first case, so 'b = 'a - std::mem::transmute::<&/* 'b */ mut T, &/* 'a */ mut T>(k) - } + // Safety: see above. We know we are in the first case, so 'b = 'a + return unsafe { std::mem::transmute::<&/* 'b */ mut T, &/* 'a */ mut T>(k) } } } let v = & /* 'c */ mut *v; diff --git a/mm0-rs/src/lib.rs b/mm0-rs/src/lib.rs index d5788f9f..22eec831 100644 --- a/mm0-rs/src/lib.rs +++ b/mm0-rs/src/lib.rs @@ -29,7 +29,9 @@ #![warn(clippy::float_arithmetic, clippy::get_unwrap, clippy::inline_asm_x86_att_syntax, clippy::integer_division, clippy::rc_buffer, clippy::rest_pat_in_fully_bound_structs, - clippy::string_add, clippy::unwrap_used)] + clippy::string_add, + // clippy::undocumented_unsafe_blocks, // disabled because of ICE on 1.58.1 stable + clippy::unwrap_used)] // all the clippy lints we don't want #![allow(clippy::cognitive_complexity, clippy::comparison_chain, clippy::default_trait_access, clippy::enum_glob_use, clippy::inline_always, diff --git a/mm0-rs/src/server.rs b/mm0-rs/src/server.rs index 6cb704b7..599b10c1 100644 --- a/mm0-rs/src/server.rs +++ b/mm0-rs/src/server.rs @@ -623,9 +623,10 @@ fn trim_margin(s: &str) -> String { for (i, &c) in s.iter().enumerate() { if c == b'\n' { if nonempty { - out.push_str(unsafe { - std::str::from_utf8_unchecked(&s[last + margin ..= i]) - }); + // Safety: last + margin is at a valid utf8 location + // because it is some number of spaces after a newline, + // and i+1 is because c == b'\n' is a one byte char + unsafe { out.push_str(std::str::from_utf8_unchecked(&s[last + margin ..= i])) } nonempty = false; } else { out.push('\n') @@ -678,6 +679,9 @@ async fn hover(path: FileRef, pos: Position) -> Result, ResponseEr let env = elaborate(path, Some(Position::default()), Default::default(), Default::default()) .await.map_err(|e| response_err(ErrorCode::InternalError, format!("{:?}", e)))?; let env = or!(Ok(None), env.into_response_error()?).1; + // Safety: This is actually unsafe, but the issue is unlikely to come up in practice. + // We are promising here to not Rc::clone the data, but we do below, + // meaning that we could potentially race on the reference count. let env = unsafe { env.thaw() }; let fe = FormatEnv { source: &text, env }; let spans = or!(Ok(None), Spans::find(&env.spans, idx)); @@ -721,6 +725,7 @@ async fn hover(path: FileRef, pos: Position) -> Result, ResponseEr (spans.lc.as_ref()?.vars.get(&a)?.1.sort()?, None) }; let mut out = String::new(); + // Safety: render_fmt doesn't clone the expression fe.pretty(|p| p.expr(unsafe {e.thaw()}).render_fmt(80, &mut out).expect("impossible")); { use std::fmt::Write; write!(out, ": {}", fe.to(&s)).expect("impossible"); } ((sp1, mk_mm0(out)), doc) @@ -743,7 +748,11 @@ async fn hover(path: FileRef, pos: Position) -> Result, ResponseEr out.push((sp, mk_mm0(format!("{}", fe.to(td))))); let mut args = vec![]; for _ in 0..td.args.len() { - args.push(unsafe {u.next()?.thaw()}.clone()); + // Safety: FIXME this is actually unsafe. `Subst` both requires cloned expressions + // and also clones expressions itself, but `FrozenEnv` does not permit us to do so, + // and there can potentially be a data race if multiple threads attempt to do this + // printing at the same time. But this is a hover output so this seems unlikely. + args.push(unsafe { u.next()?.thaw() }.clone()); } let mut subst = Subst::new(env, &td.heap, args); let mut out = String::new(); @@ -888,6 +897,7 @@ async fn document_symbol(path: FileRef) -> Result (file.text.ulock().1.ascii().clone(), env) } }; + // Safety: We don't use the env field on `fe` for anything other than printing let fe = unsafe { env.format_env(&text) }; let f = |sp, name: &ArcString, desc, full, kind| DocumentSymbol { name: String::from_utf8_lossy(name).into(), @@ -927,8 +937,10 @@ async fn document_symbol(path: FileRef) -> Result { let ad = &env.data()[a]; if let Some(ld) = ad.lisp() { + #[allow(clippy::undocumented_unsafe_blocks)] // rust-clippy#8449 if let Some((ref fsp, full)) = *ld.src() { let e = &**ld; + // Safety: We only use the expression for printing and don't Rc::clone it push!(fsp, ad.name(), format!("{}", fe.to(unsafe { e.thaw() })), full, match (|| Some(match e.unwrap() { FrozenLispKind::Atom(_) | @@ -988,9 +1000,11 @@ fn make_completion_item(path: &FileRef, fe: FormatEnv<'_>, ad: &FrozenAtomData, DeclKey::Term(t) => {let td = &fe.terms[t]; done!(format!("{}", fe.to(td)), Constructor, td.doc)} DeclKey::Thm(t) => {let td = &fe.thms[t]; done!(format!("{}", fe.to(td)), Method, td.doc)} }), + #[allow(clippy::undocumented_unsafe_blocks)] // rust-clippy#8449 TraceKind::Global => { let e = ad.lisp().as_ref()?; - Some(done!(format!("{}", fe.to(unsafe {e.thaw()})), match *e.unwrap() { + // Safety: We only use the expression for printing and don't Rc::clone it + Some(done!(format!("{}", fe.to(unsafe { e.thaw() })), match *e.unwrap() { FrozenLispKind::Atom(_) | FrozenLispKind::MVar(_, _) | FrozenLispKind::Goal(_) => CompletionItemKind::Constant, @@ -1027,6 +1041,7 @@ async fn completion(path: FileRef, _pos: Position) -> Result Result