[read/write set analysis] Don't allow local or return paths in the fo…

…otprint

Fixes the final crash issue required to analyze all Diem Framework modules.

- Add `Root::Formal` + use a `FunctionEnv` to decide whether to create a `Root::Local` or `Root::Formal`. This change is the bulk of the PR because we need to thread `FunctionEnv`'s to a lot of new places
- In `make_footprint(access_path)`, create an empty footprint if `access_path` is rooted in a local or return value. The `Root::Formal`/`Root::Local` split is required to detect this (since the call site of `make_footprint` can't get a `FunctionEnv`.
- Add minimal repro that triggered the crash.
- Add Diem Framework as a smoke test.

Closes: aptos-labs#8259

language/move-prover/bytecode/src/access_path.rs

@@ -72,7 +72,9 @@ pub struct GlobalKey {
 pub enum Root {
     /// A key in global storage
     Global(GlobalKey), // TODO: this could (and maybe should) be AbsAddr + Offset::Global
-    /// A local variable or formal parameter
+    /// A formal parameter
+    Formal(TempIndex),
+    /// A local variable
     Local(TempIndex),
     /// A return variable
     Return(usize),
@@ -118,6 +120,15 @@ impl Addr {
 
     /// Create a footprint address from access path `ap`
     pub fn footprint(ap: AccessPath) -> Self {
+        assert!(
+            !ap.root.is_return(),
+            "Attempting to create footprint from return access path"
+        );
+        assert!(
+            !ap.root.is_local(),
+            "Attempting to create footprint from local access path"
+        );
+
         Self::Footprint(ap)
     }
 
@@ -159,8 +170,12 @@ impl AbsAddr {
     }
 
     /// Create a footprint address read from formal `temp_index`
-    pub fn formal(formal_index: TempIndex) -> Self {
-        SetDomain::footprint(AccessPath::new_local(formal_index))
+    pub fn formal(formal_index: TempIndex, func_env: &FunctionEnv) -> Self {
+        assert!(
+            func_env.is_parameter(formal_index),
+            "Attempting to create formal from local index"
+        );
+        SetDomain::footprint(AccessPath::from_index(formal_index, func_env))
     }
 
     /// Return `true` if `self` is a constant
@@ -257,7 +272,11 @@ impl AbsAddr {
 
 impl FootprintDomain for AbsAddr {
     fn make_footprint(ap: AccessPath) -> Option<Self> {
-        Some(AbsAddr::footprint(ap))
+        if !ap.root.is_return() && !ap.root.is_local() {
+            Some(AbsAddr::footprint(ap))
+        } else {
+            None
+        }
     }
 }
 
@@ -302,9 +321,13 @@ impl GlobalKey {
 }
 
 impl Root {
-    /// Create a `Root` from local variable `index`
-    pub fn local(index: TempIndex) -> Self {
-        Root::Local(index)
+    /// Create a `Root` from local index `index`
+    pub fn from_index(index: TempIndex, fun: &FunctionEnv) -> Self {
+        if fun.is_parameter(index) {
+            Root::Formal(index)
+        } else {
+            Root::Local(index)
+        }
     }
 
     /// Create a `Root` from global storage key `key`
@@ -321,18 +344,32 @@ impl Root {
     pub fn get_type(&self, fun: &FunctionEnv) -> Type {
         match self {
             Self::Global(g) => g.ty.get_type(),
-            Self::Local(i) => fun.get_local_type(*i),
+            Self::Formal(i) => fun.get_local_type(*i),
+            Self::Local(i) => {
+                if *i < fun.get_local_count() {
+                    fun.get_local_type(*i)
+                } else {
+                    // temporary local generated by stackless bytecode. use dummy type
+                    Type::Error
+                }
+            }
             Self::Return(i) => fun.get_return_type(*i),
         }
     }
 
-    /// Return true if this variable is a formal parameter of `fun`
-    pub fn is_formal(&self, fun: &FunctionEnv) -> bool {
-        match self {
-            Self::Local(i) => fun.is_parameter(*i),
-            Self::Global(_) => false,
-            Self::Return(_) => false,
-        }
+    /// Return true if this variable is a formal parameter
+    pub fn is_formal(&self) -> bool {
+        matches!(self, Self::Formal(_))
+    }
+
+    /// Return `true` if this variable is a return value
+    pub fn is_return(&self) -> bool {
+        matches!(self, Self::Return(_))
+    }
+
+    /// Return `true` if this variable is a lol
+    pub fn is_local(&self) -> bool {
+        matches!(self, Self::Local(_))
     }
 
     /// Replace all footprint paths in `self` using `actuals` and `sub_map`.
@@ -345,7 +382,7 @@ impl Root {
     ) {
         match self {
             Self::Global(g) => g.substitute_footprint(actuals, type_actuals, sub_map),
-            Self::Local(_) | Self::Return(_) => (),
+            Self::Formal(_) | Self::Local(_) | Self::Return(_) => (),
         }
     }
 
@@ -444,8 +481,8 @@ impl AccessPath {
         Self::new_root(Root::Global(GlobalKey::constant(addr, ty)))
     }
 
-    pub fn new_local(i: TempIndex) -> Self {
-        Self::new_root(Root::Local(i))
+    pub fn from_index(i: TempIndex, func_env: &FunctionEnv) -> Self {
+        Self::new_root(Root::from_index(i, func_env))
     }
 
     /// Unpack `self` into its root and offsets
@@ -536,7 +573,7 @@ impl AccessPath {
     ) -> AbsAddr {
         let mut acc = AbsAddr::default();
         match &self.root {
-            Root::Local(i) => {
+            Root::Formal(i) => {
                 acc.join(&self.prepend_addrs(&actuals[*i]));
             }
             Root::Global(g) => {
@@ -551,7 +588,7 @@ impl AccessPath {
                     new_offsets,
                 )));
             }
-            Root::Return(_) => (),
+            Root::Local(_) | Root::Return(_) => (),
         }
         acc
     }
@@ -687,6 +724,7 @@ impl<'a> fmt::Display for RootDisplay<'a> {
         match self.root {
             Root::Global(g) => write!(f, "{}", g.display(self.env)),
             Root::Local(i) => write!(f, "Loc({})", i), // TODO: print name if available
+            Root::Formal(i) => write!(f, "Formal({})", i), // TODO: print name if available
             Root::Return(i) => write!(f, "Ret({})", i),
         }
     }

language/move-prover/bytecode/src/access_path_trie.rs

@@ -237,7 +237,7 @@ impl<T: FootprintDomain> AccessPathTrie<T> {
         let (root, offsets) = ap.into();
         let needs_weak_update = match &root {
             // local base. strong update possible because of Move aliasing semantics
-            Root::Local(_) | Root::Return(_) => false,
+            Root::Local(_) | Root::Formal(_) | Root::Return(_) => false,
             // global base. must do weak update unless g is statically known
             Root::Global(g) => !g.is_statically_known(),
         };
@@ -260,18 +260,23 @@ impl<T: FootprintDomain> AccessPathTrie<T> {
     }
 
     /// Bind `data` to `local_index` in the trie, overwriting the old value of `local_index`
-    pub fn bind_local(&mut self, local_index: TempIndex, data: T) {
-        self.bind_root(Root::local(local_index), data)
+    pub fn bind_local(&mut self, local_index: TempIndex, data: T, fun_env: &FunctionEnv) {
+        self.bind_root(Root::from_index(local_index, fun_env), data)
     }
 
     /// Bind `node` to `local_index` in the trie, overwriting the old value of `local_index`
-    pub fn bind_local_node(&mut self, local_index: TempIndex, node: TrieNode<T>) {
-        self.0.insert(Root::local(local_index), node);
+    pub fn bind_local_node(
+        &mut self,
+        local_index: TempIndex,
+        node: TrieNode<T>,
+        fun_env: &FunctionEnv,
+    ) {
+        self.0.insert(Root::from_index(local_index, fun_env), node);
     }
 
     /// Remove the value bound to the local variable `local_index`
-    pub fn remove_local(&mut self, local_index: TempIndex) {
-        self.0.remove(&Root::Local(local_index));
+    pub fn remove_local(&mut self, local_index: TempIndex, fun_env: &FunctionEnv) {
+        self.0.remove(&Root::from_index(local_index, fun_env));
     }
 
     /// Bind `data` to the return variable `return_index`
@@ -284,20 +289,24 @@ impl<T: FootprintDomain> AccessPathTrie<T> {
     }
 
     /// Retrieve the data associated with `local_index` in the trie. Returns `None` if there is no associated data
-    pub fn get_local(&self, local_index: TempIndex) -> Option<&T> {
-        self.get_local_node(local_index)
+    pub fn get_local(&self, local_index: TempIndex, fun_env: &FunctionEnv) -> Option<&T> {
+        self.get_local_node(local_index, fun_env)
             .map(|n| n.data.as_ref())
             .flatten()
     }
 
     /// Retrieve the node associated with `local_index` in the trie. Returns `None` if there is no associated node
-    pub fn get_local_node(&self, local_index: TempIndex) -> Option<&TrieNode<T>> {
-        self.0.get(&Root::local(local_index))
+    pub fn get_local_node(
+        &self,
+        local_index: TempIndex,
+        fun_env: &FunctionEnv,
+    ) -> Option<&TrieNode<T>> {
+        self.0.get(&Root::from_index(local_index, fun_env))
     }
 
     /// Return `true` if there is a value bound to local variable `local_index`
-    pub fn local_exists(&self, local_index: TempIndex) -> bool {
-        self.0.contains_key(&Root::local(local_index))
+    pub fn local_exists(&self, local_index: TempIndex, fun_env: &FunctionEnv) -> bool {
+        self.0.contains_key(&Root::from_index(local_index, fun_env))
     }
 
     /// Bind caller data in `actuals`, `type_actuals`, and `sub_map` to `self`.