cleanup some inacurrate or out-of-date code docs (#2802)

Author: tjhance

source/vir/src/ast.rs

@@ -117,9 +117,9 @@ pub struct Visibility {
 
 #[derive(Clone, Debug, Serialize, Deserialize, ToDebugSNode, PartialEq, Eq)]
 pub enum BodyVisibility {
+    /// Function is declared uninterpreted (i.e., "visible nowhere")
     Uninterpreted,
-    /// None for pub
-    /// Some(path) means visible to path and path's descendents
+    /// Body is visible at the given visibility.
     Visibility(Visibility),
 }
 
@@ -190,12 +190,12 @@ pub enum IntRange {
 /// In some places, the decoration of a Typ cannot be considered meaningful due to these
 /// implicit 'identity' coercions:
 ///   - `expr.typ`
-///   - `place.typ`
 ///   - `pattern.typ`
 ///   - `exp.typ` (SST nodes)
 /// But in other places, types must be exactly correct, *including* decoration:
 ///   - type arguments for a Call
 ///   - `pattern_binding.typ` (type of a local variable declaration)
+///   - `place.typ` (See docs for `Place`)
 ///   - Most places where `Typ` is given as an explicit field of a node
 #[derive(
     Debug,
@@ -249,8 +249,6 @@ pub enum TypDecoration {
 pub enum Primitive {
     Array,
     Slice,
-    /// StrSlice type. Currently the vstd StrSlice struct is "seen" as this type
-    /// despite the fact that it is in fact a datatype
     StrSlice,
     Ptr, // Mut ptr, unless Const decoration is applied
     Global,
@@ -353,7 +351,8 @@ pub enum ModeCoercion {
     /// This operation behaves like a datatype constructor with a mode annotation
     /// `from_mode` on its field.
     /// (e.g., Tracked(...) is proof -> exec, Ghost(...) is spec -> exec.
-    /// Like with ordinary constructors, the input can be spec and if so, the whole thing is spec.
+    /// Note that `Tracked` behaves like an exec datatype with a proof-mode field, meaning
+    /// if the input is 'spec', then the whole thing is 'spec'.
     Constructor,
     /// This behaves like a field-getter,
     /// returning the contents of the Tracked or Ghost value.
@@ -574,18 +573,17 @@ pub enum BoundsCheck {
 
 #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)]
 pub enum OverflowBehavior {
-    /// Return an int. This is the only value allowed in SST.
+    /// Return an unbounded int, the exact value of the arithmetic expression.
     Allow,
-    /// Truncate to the given range
+    /// Truncate to the given range.
     Truncate(IntRange),
-    /// Error if the result is outside the given range
+    /// Error if the result is outside the given range.
     Error(IntRange),
 }
 
 #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash, ToDebugSNode)]
 pub enum Div0Behavior {
     /// Return the (unspecified) result of divide- or mod-by-0.
-    /// This is the only value allowed in SST.
     Allow,
     /// Error if the dividend is 0.
     Error,

source/vir/src/resolution_inference.rs

@@ -102,7 +102,7 @@ In order to resolve the field of an enum (e.g., `opt->Some_0` for a varible `opt
 the resolution needs to be conditional on the variant:
 
 ```
-assume(opt is Some ==> has_resolved(opt->Some_0)
+assume(opt is Some ==> has_resolved(opt->Some_0))
 ```
 
 Since resolution is explicitly conditional, we don't need to account for variants
@@ -253,7 +253,8 @@ use air::scope_map::ScopeMap;
 use std::collections::{HashMap, VecDeque};
 use std::sync::Arc;
 
-/// Updates the given function body to include AssumeResolved nodes at the appropriate places.
+/// Updates the given function body to include assume(has_resolved(...)) nodes
+/// at the appropriate places.
 /// On the side, also handles some work related to user_defined_type_invariants.
 ///
 /// This relies on the AstIds of the given Expr being unique, but it also destroys this property
@@ -1329,7 +1330,6 @@ impl<'a> Builder<'a> {
         }
     }
 
-    /// Returns Err(()) if the place expression never returns (can happen if it's a temporary)
     fn build_place_typed(
         &mut self,
         place: &Place,
@@ -1572,6 +1572,17 @@ impl<'a> Builder<'a> {
         }
     }
 
+    /// Get all moves and mutations for the given pattern, using `ByRef::No` for moves
+    /// and `ByRef::MutRef` for mutations.
+    ///
+    /// Example:
+    ///
+    /// ```
+    /// let (a, _, ref mut b) = x.1;
+    /// ```
+    ///
+    /// Returns `[(x.1.0, ByRef::No), (x.1.2, ByRef::MutRef)]` if `x.1.0` is a non-Copy type.
+    /// Otherwise just returns `[(x.1.2, ByRef::MutRef)]`.
     fn moves_and_muts_for_place_being_matched(
         &mut self,
         pattern: &Pattern,
@@ -1970,7 +1981,7 @@ pub struct BoundVar {
     pub typ: Typ,
 }
 
-/// Same as above, but takes a Pattern as input
+/// Get all non-spec vars bound by the pattern.
 pub fn pattern_all_bound_vars_with_ownership(
     pattern: &Pattern,
     modes: &HashMap<VarIdent, Mode>,
@@ -2017,6 +2028,7 @@ pub fn pattern_all_bound_vars_with_ownership(
     v
 }
 
+/// See `moves_and_muts_for_place_being_matched`
 fn moves_and_muts_for_pattern(
     pattern: &Pattern,
     datatypes: &HashMap<Path, Datatype>,
@@ -3845,8 +3857,6 @@ fn add_decls_for_temps(
     // Declare all temp vars at the beginning of the function body
     // (There doesn't seem to be any point in minimizing the scope of such variables,
     // but maybe we should restrict them to individual loops?)
-    // We mark them all mut, though in principle, some of them don't need to be mut,
-    // e.g., the ones that are only here so we can call `assume(HasResolved(...))`.
     let mut stmts = vec![];
     for local in cfg.locals.locals.iter() {
         if let LocalName::Temporary(ast_id, temp_id) = &local.name {