Method execute

language/move-prover/bytecode/src/read_write_set_analysis.rs:428–604

(&self, state: &mut Self::State, instr: &Bytecode, _offset: CodeOffset)

    const BACKWARD: bool = false;

    fn execute(&self, state: &mut Self::State, instr: &Bytecode, _offset: CodeOffset) {
        use Bytecode::*;
        use Operation::*;

        let func_env = &self.func_env;
        match instr {
            Call(_, rets, oper, args, _abort_action) => match oper {
                BorrowField(_mid, _sid, _types, fld) => {
                    if state.locals.local_exists(args[0], func_env) {
                        state.assign_offset(rets[0], args[0], Offset::field(*fld), None, func_env);
                    }
                }
                ReadRef => {
                    if state.locals.local_exists(args[0], func_env) {
                        // rets[0] = args[0]
                        state.assign_local(rets[0], args[0], func_env)
                    }
                }
                WriteRef => {
                    state.record_access(args[0], Access::Write, func_env);
                    // *args[0] = args1
                    state.write_ref(args[0], args[1], func_env)
                }
                FreezeRef | BorrowLoc => state.assign_local(rets[0], args[0], func_env),
                BorrowGlobal(mid, sid, types) => {
                    // borrow_global<T>(a). bind ret to a/T
                    let addrs = state
                        .locals
                        .get_local(args[0], func_env)
                        .expect("Unbound address local")
                        .clone();
                    let offset = Offset::global(mid, *sid, types.clone());
                    let mut extended_aps: AbsAddr = AbsAddr::default();
                    for p in addrs.iter() {
                        match p {
                            Addr::Footprint(ap) => {
                                let mut extended_ap = ap.clone();
                                extended_ap.add_offset(offset.clone());
                                extended_aps.insert(Addr::Footprint(extended_ap.clone()));
                                state.locals.update_access_path(extended_ap.clone(), None);
                            }
                            Addr::Constant(c) => {
                                let extended_ap = AccessPath::new_address_constant(
                                    c.clone(),
                                    mid,
                                    *sid,
                                    types.clone(),
                                );
                                extended_aps.insert(Addr::footprint(extended_ap));
                            }
                        }
                    }
                    state.locals.bind_local(rets[0], extended_aps, func_env)
                }
                MoveFrom(mid, sid, types) => {
                    state.add_global_access(args[0], mid, *sid, types, Access::Write, func_env);
                    state.remove_global(args[0], mid, *sid, types, func_env)
                }