// Copyright 2017 The Australian National University
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

use ir::*;
use op::*;
use ptr::*;
use types::*;

use utils::vec_utils;

use std::fmt;

/// Instruction represents a Mu instruction
#[derive(Debug, Clone)] // this implements Display
pub struct Instruction {
    pub hdr: MuEntityHeader,
    /// the values this instruction holds
    pub value: Option<Vec<P<Value>>>,
    /// ops field list all the children nodes,
    /// and in Instruction_, the children nodes are referred by indices
    /// This design makes it easy for the compiler to iterate through all the
    /// children
    pub ops: Vec<P<TreeNode>>,
    /// used for pattern matching
    pub v: Instruction_
}

// Instruction implements MuEntity
impl_mu_entity!(Instruction);

impl Instruction {
    pub fn clone_with_id(&self, new_id: MuID) -> Instruction {
        let mut clone = self.clone();
        clone.hdr = self.hdr.clone_with_id(new_id);

        clone
    }

    // RTMU add new rt instructions to various spec functions here

    /// is this instruction the terminal inst of its block?
    /// Terminal instructions end Mu blocks, and Mu block ends with a terminal
    /// instruction.
    pub fn is_terminal_inst(&self) -> bool {
        use inst::Instruction_::*;

        match self.v {
            Return(_)
            | ThreadExit
            | Throw(_)
            | TailCall(_)
            | Branch1(_)
            | Branch2 { .. }
            | Watchpoint { .. }
            | WPBranch { .. }
            | Call { .. }
            | CCall { .. }
            | SwapStackExc { .. }
            | SwapStackKill { .. }
            | Switch { .. }
            | ExnInstruction { .. } => true,
            BinOp(_, _, _)
            | BinOpWithStatus(_, _, _, _)
            | CmpOp(_, _, _)
            | ConvOp { .. }
            | ExprCall { .. }
            | ExprCCall { .. }
            | Load { .. }
            | Store { .. }
            | CmpXchg { .. }
            | AtomicRMW { .. }
            | New(_)
            | AllocA(_)
            | NewHybrid(_, _)
            | AllocAHybrid(_, _)
            | NewStack(_)
            | NewThread { .. }
            | NewRTThread { .. }
            | NewFutex
            | DeleteFutex(_)
            | LockFutex(_,_)
            | UnlockFutex(_)
            | AllocAU(_)
            | AllocAUHybrid(_,_)
            | NewReg(_)
            | DeleteReg(_)
            | rAlloc(_, _)
            | rAllocHybrid(_, _, _)
            | eAlloc(_)
            | eAllocHybrid(_, _)
            | eDelete(_)
            | NotifyThread(_)       // TODO remove - not needed anymore
            | ThreadSetPriority(_,_)
            | ThreadGetPriority(_)
            | ThreadSetCPU(_,_)
            | ThreadClearCPU(_,_)
            | ThreadIssetCPU(_,_)
            | GetTime
            | SetTime(_)
            | NewTimer
            | SetTimer { .. }
            | CancelTimer(_)
            | DeleteTimer(_)
            | Sleep(_)
            | NewAttr
            | DeleteAttr(_)
            | ThreadSetAttr(_,_)
            | ThreadGetAttr(_)
            | AttrClearCPU(_,_)
            | AttrIssetCPU(_,_)
            | AttrSetCPU(_,_)
            | AttrZeroCPU(_)
            | AttrSetPriority(_,_)
            | AttrGetPriority(_)
            | eAllocPA(_,_)
            | eAllocHybridPA(_,_,_)
            | BindObject(_)
            | UnbindObject(_)
            | NewRegionPA(_,_)
            | BindRegion(_)
            | UnbindRegion(_)
            | NewFrameCursor(_)
            | GetIRef(_)
            | GetFieldIRef { .. }
            | GetElementIRef { .. }
            | ShiftIRef { .. }
            | GetVarPartIRef { .. }
            | Select { .. }
            | Fence(_)
            | CommonInst_GetThreadLocal
            | CommonInst_SetThreadLocal(_)
            | CommonInst_Pin(_)
            | CommonInst_Unpin(_)
            | CommonInst_GetAddr(_)
            | CommonInst_Tr64IsFp(_)
            | CommonInst_Tr64IsInt(_)
            | CommonInst_Tr64IsRef(_)
            | CommonInst_Tr64FromFp(_)
            | CommonInst_Tr64FromInt(_)
            | CommonInst_Tr64FromRef(_, _)
            | CommonInst_Tr64ToFp(_)
            | CommonInst_Tr64ToInt(_)
            | CommonInst_Tr64ToRef(_)
            | CommonInst_Tr64ToTag(_)
            | Move(_)
            | PrintHex(_)
            | PrintBool(_)
            | PrintTime(_)
            | SetRetval(_)
            | GetVMThreadLocal
            | KillStack(_)
            | CurrentStack
            | RandF(_,_)
            | RandI(_,_)
            | SwapStackExpr { .. } => false,
        }
    }

    /// is this instruction a non-terminal instruction of its block?
    pub fn is_non_terminal_inst(&self) -> bool {
        !self.is_terminal_inst()
    }

    /// does this instruction has side effect?
    /// An instruction has side effect if it affects something other than its
    /// result operands. e.g. affecting memory, stack, thread, etc.
    // FIXME: need to check correctness
    pub fn has_side_effect(&self) -> bool {
        use inst::Instruction_::*;

        match self.v {
            ExprCall { .. }
            | ExprCCall { .. }
            | Load { .. }
            | Store { .. }
            | CmpXchg { .. }
            | AtomicRMW { .. }
            | New(_)
            | AllocA(_)
            | NewHybrid(_, _)
            | AllocAHybrid(_, _)
            | AllocAU(_)
            | AllocAUHybrid(_,_)
            | NewReg(_)
            | DeleteReg(_)
            | rAlloc(_, _)
            | rAllocHybrid(_,_,_)
            | eAlloc(_)
            | eAllocHybrid(_,_)
            | eDelete(_)
            | NewStack(_)
            | NewThread { .. }
            | NewRTThread { .. }
            | NewFutex
            | DeleteFutex(_)
            | LockFutex(_,_)
            | UnlockFutex(_)
            | NotifyThread(_)
            | ThreadSetPriority(_, _)
            | ThreadClearCPU(_, _)
            | ThreadSetCPU(_, _)
//            | AffinityZero(_)
            | SetTime(_)
            | NewTimer
            | SetTimer { .. }
            | CancelTimer(_)
            | DeleteTimer(_)
            | Sleep(_)
            | NewAttr
            | DeleteAttr(_)
            | ThreadSetAttr(_,_)
            | AttrClearCPU(_,_)
            | AttrSetCPU(_,_)
            | AttrZeroCPU(_)
            | AttrSetPriority(_,_)
            | eAllocPA(_,_)
            | eAllocHybridPA(_,_,_)
            | BindObject(_)
            | UnbindObject(_)
            | NewRegionPA(_,_)
            | BindRegion(_)
            | UnbindRegion(_)
            | NewFrameCursor(_)
            | Fence(_)
            | Return(_)
            | ThreadExit
            | Throw(_)
            | TailCall(_)
            | Branch1(_)
            | Branch2 { .. }
            | Watchpoint { .. }
            | WPBranch { .. }
            | Call { .. }
            | CCall { .. }
            | SwapStackExpr { .. }
            | SwapStackExc { .. }
            | SwapStackKill { .. }
            | Switch { .. }
            | ExnInstruction { .. }
            | CommonInst_GetThreadLocal
            | CommonInst_SetThreadLocal(_)
            | CommonInst_Pin(_)
            | CommonInst_Unpin(_)
            | CommonInst_GetAddr(_)
            | PrintHex(_)
            | PrintBool(_)
            | PrintTime(_)
            | SetRetval(_)
            | KillStack(_) => true,
            BinOp(_, _, _)
            | BinOpWithStatus(_, _, _, _)
            | CmpOp(_, _, _)
            | ConvOp { .. }
            | GetIRef(_)
            | GetFieldIRef { .. }
            | GetElementIRef { .. }
            | ShiftIRef { .. }
            | GetVarPartIRef { .. }
            | Select { .. }
            | CommonInst_Tr64IsFp(_)
            | CommonInst_Tr64IsInt(_)
            | CommonInst_Tr64IsRef(_)
            | CommonInst_Tr64FromFp(_)
            | CommonInst_Tr64FromInt(_)
            | CommonInst_Tr64FromRef(_, _)
            | CommonInst_Tr64ToFp(_)
            | CommonInst_Tr64ToInt(_)
            | CommonInst_Tr64ToRef(_)
            | CommonInst_Tr64ToTag(_)
            | Move(_)
            | CurrentStack
            | GetVMThreadLocal
            | ThreadGetPriority(_)
            | GetTime
            | ThreadGetAttr(_)
            | AttrIssetCPU(_,_)
            | AttrGetPriority(_)
            | RandF(_,_)
            | RandI(_,_)
            | ThreadIssetCPU(_, _) => false,
//            | AffinityEqual(_, _)
        }
    }

    /// can this instruction throw exception?
    /// an instruction with an exceptional branch can throw exception
    pub fn is_potentially_excepting_instruction(&self) -> bool {
        use inst::Instruction_::*;

        match self.v {
            Watchpoint { .. }
            | Call { .. }
            | CCall { .. }
            | SwapStackExc { .. }
            | ExnInstruction { .. } => true,
            BinOp(_, _, _)
            | BinOpWithStatus(_, _, _, _)
            | CmpOp(_, _, _)
            | ConvOp { .. }
            | ExprCall { .. }
            | ExprCCall { .. }
            | Load { .. }
            | Store { .. }
            | CmpXchg { .. }
            | AtomicRMW { .. }
            | New(_)
            | AllocA(_)
            | NewHybrid(_, _)
            | AllocAHybrid(_, _)
            | NewStack(_)
            | AllocAU(_)
            | AllocAUHybrid(_, _)
            | NewReg(_)
            | DeleteReg(_)
            | rAlloc(_, _)
            | rAllocHybrid(_, _, _)
            | eAlloc(_)
            | eAllocHybrid(_, _)
            | eDelete(_)
            | NewThread { .. }
            | NewRTThread { .. }
            | NewFutex
            | DeleteFutex(_)
            | LockFutex(_, _)
            | UnlockFutex(_)
            | NotifyThread(_)
            | ThreadSetPriority(_, _)
            | ThreadGetPriority(_)
            | ThreadClearCPU(_, _)
            | ThreadSetCPU(_, _)
            | ThreadIssetCPU(_, _)
            | GetTime
            | SetTime(_)
            | NewTimer
            | SetTimer { .. }
            | CancelTimer(_)
            | DeleteTimer(_)
            | Sleep(_)
            | NewAttr
            | DeleteAttr(_)
            | ThreadSetAttr(_, _)
            | ThreadGetAttr(_)
            | AttrClearCPU(_, _)
            | AttrIssetCPU(_, _)
            | AttrSetCPU(_, _)
            | AttrZeroCPU(_)
            | AttrSetPriority(_, _)
            | AttrGetPriority(_)
            | eAllocPA(_, _)
            | eAllocHybridPA(_, _, _)
            | BindObject(_)
            | UnbindObject(_)
            | NewRegionPA(_, _)
            | BindRegion(_)
            | UnbindRegion(_)
            | NewFrameCursor(_)
            | GetIRef(_)
            | GetFieldIRef { .. }
            | GetElementIRef { .. }
            | ShiftIRef { .. }
            | GetVarPartIRef { .. }
            | Fence(_)
            | Return(_)
            | ThreadExit
            | Throw(_)
            | TailCall(_)
            | Branch1(_)
            | Branch2 { .. }
            | Select { .. }
            | WPBranch { .. }
            | Switch { .. }
            | CommonInst_GetThreadLocal
            | CommonInst_SetThreadLocal(_)
            | CommonInst_Pin(_)
            | CommonInst_Unpin(_)
            | CommonInst_GetAddr(_)
            | CommonInst_Tr64IsFp(_)
            | CommonInst_Tr64IsInt(_)
            | CommonInst_Tr64IsRef(_)
            | CommonInst_Tr64FromFp(_)
            | CommonInst_Tr64FromInt(_)
            | CommonInst_Tr64FromRef(_, _)
            | CommonInst_Tr64ToFp(_)
            | CommonInst_Tr64ToInt(_)
            | CommonInst_Tr64ToRef(_)
            | CommonInst_Tr64ToTag(_)
            | Move(_)
            | PrintHex(_)
            | PrintBool(_)
            | PrintTime(_)
            | SetRetval(_)
            | GetVMThreadLocal
            | KillStack(_)
            | CurrentStack
            | RandI(_, _)
            | RandF(_, _)
            | SwapStackExpr { .. }
            | SwapStackKill { .. } => false
        }
    }

    /// does this instruction have an exceptional clause/branch?
    pub fn has_exception_clause(&self) -> bool {
        self.is_potentially_excepting_instruction()
    }

    /// returns exception target(block ID),
    /// returns None if this instruction does not have exceptional branch
    pub fn get_exception_target(&self) -> Option<MuID> {
        use inst::Instruction_::*;
        match self.v {
            Watchpoint { ref resume, .. }
            | Call { ref resume, .. }
            | CCall { ref resume, .. }
            | SwapStackExc { ref resume, .. }
            | ExnInstruction { ref resume, .. } => Some(resume.exn_dest.target.id()),
            BinOp(_, _, _)
            | BinOpWithStatus(_, _, _, _)
            | CmpOp(_, _, _)
            | ConvOp { .. }
            | ExprCall { .. }
            | ExprCCall { .. }
            | Load { .. }
            | Store { .. }
            | CmpXchg { .. }
            | AtomicRMW { .. }
            | New(_)
            | AllocA(_)
            | NewHybrid(_, _)
            | AllocAU(_)
            | AllocAUHybrid(_,_)
            | NewReg(_)
            | DeleteReg(_)
            | rAlloc(_, _)
            | rAllocHybrid(_,_,_)
//            | rAllocT(_)
            | eAlloc(_)
            | eAllocHybrid(_,_)
//            | eAllocT(_)
            | eDelete(_)
//            | eDeleteT(_)
            | AllocAHybrid(_, _)
            | NewStack(_)
            | NewThread { .. }
            | NewRTThread { .. }
            | NewFutex
            | DeleteFutex(_)
            | LockFutex(_,_)
            | UnlockFutex(_)
            | NotifyThread(_)
            | ThreadSetPriority(_,_)  // FIXME - Not sure about these
            | ThreadGetPriority(_)
            | ThreadClearCPU(_,_)
//            | AffinityEqual(_,_)
            | ThreadIssetCPU(_,_)
            | ThreadSetCPU(_,_)
//            | AffinityZero(_)
            | SetTime(_)
            | GetTime
            | NewTimer
            | SetTimer { .. }
            | CancelTimer(_)
            | DeleteTimer(_)
            | Sleep(_)
            | NewAttr
            | DeleteAttr(_)
            | ThreadSetAttr(_,_)
            | ThreadGetAttr(_)
            | AttrClearCPU(_,_)
            | AttrIssetCPU(_,_)
            | AttrSetCPU(_,_)
            | AttrZeroCPU(_)
            | AttrSetPriority(_,_)
            | AttrGetPriority(_)
            | eAllocPA(_,_)
            | eAllocHybridPA(_,_,_)
            | BindObject(_)
            | UnbindObject(_)
            | NewRegionPA(_,_)
            | BindRegion(_)
            | UnbindRegion(_)
            | NewFrameCursor(_)
            | GetIRef(_)
            | GetFieldIRef { .. }
            | GetElementIRef { .. }
            | ShiftIRef { .. }
            | GetVarPartIRef { .. }
            | Fence(_)
            | Return(_)
            | ThreadExit
            | Throw(_)
            | TailCall(_)
            | Branch1(_)
            | Branch2 { .. }
            | Select { .. }
            | WPBranch { .. }
            | Switch { .. }
            | CommonInst_GetThreadLocal
            | CommonInst_SetThreadLocal(_)
            | CommonInst_Pin(_)
            | CommonInst_Unpin(_)
            | CommonInst_GetAddr(_)
            | CommonInst_Tr64IsFp(_)
            | CommonInst_Tr64IsInt(_)
            | CommonInst_Tr64IsRef(_)
            | CommonInst_Tr64FromFp(_)
            | CommonInst_Tr64FromInt(_)
            | CommonInst_Tr64FromRef(_, _)
            | CommonInst_Tr64ToFp(_)
            | CommonInst_Tr64ToInt(_)
            | CommonInst_Tr64ToRef(_)
            | CommonInst_Tr64ToTag(_)
            | Move(_)
            | PrintHex(_)
            | PrintBool(_)
            | PrintTime(_)
            | SetRetval(_)
            | GetVMThreadLocal
            | KillStack(_)
            | CurrentStack
            | RandF(_,_)
            | RandI(_,_)
            | SwapStackExpr { .. }
            | SwapStackKill { .. } => None,
        }
    }

    /// can this instruction throw exception?
    /// (whether or not it containjs a ctach for it)
    pub fn is_potentially_throwing(&self) -> bool {
        use inst::Instruction_::*;

        match self.v {
            // Note: commented out ones are ones where we haven't implemented exceptions yet
            Watchpoint { .. } |
            Call { .. } |
            CCall { .. } |
            SwapStackExc { .. } |
            SwapStackExpr { .. } |
            ExnInstruction { .. } |
            ExprCall { .. } |
            ExprCCall { .. } |
            //Load { .. } |
            //Store { .. } |
            //CmpXchg { .. } |
            //AtomicRMW { .. } |
            //New(_) |
            //NewHybrid(_, _) |
            Throw(_)  => true,

            // BinOp(op, _, _) |
            // BinOpWithStatus(op, _, _, _) if op.may_throw() => true,
            BinOp(_, _, _) |
            BinOpWithStatus(_, _, _, _) |
            CmpOp(_, _, _) |
            ConvOp { .. } |
            AllocA(_) |
            AllocAHybrid(_, _) |
            NewStack(_) |
            NewThread { .. } |
            NewRTThread { .. } |
            NewFutex
            | DeleteFutex(_)
            | LockFutex(_,_)
            | UnlockFutex(_)
            | NotifyThread(_) |
            ThreadSetPriority(_,_) |
            NewFrameCursor(_) |
            GetIRef(_) |
            GetFieldIRef { .. } |
            GetElementIRef { .. } |
            ShiftIRef { .. } |
            GetVarPartIRef { .. } |
            Fence(_) |
            Return(_) |
            ThreadExit |
            TailCall(_) |
            Branch1(_) |
            Branch2 { .. } |
            Select { .. } |
            WPBranch { .. } |
            Switch { .. } |
            CommonInst_GetThreadLocal |
            CommonInst_SetThreadLocal(_) |
            CommonInst_Pin(_) |
            CommonInst_Unpin(_) |
            CommonInst_GetAddr(_) |
            CommonInst_Tr64IsFp(_) |
            CommonInst_Tr64IsInt(_) |
            CommonInst_Tr64IsRef(_) |
            CommonInst_Tr64FromFp(_) |
            CommonInst_Tr64FromInt(_) |
            CommonInst_Tr64FromRef(_, _) |
            CommonInst_Tr64ToFp(_) |
            CommonInst_Tr64ToInt(_) |
            CommonInst_Tr64ToRef(_) |
            CommonInst_Tr64ToTag(_) |
            Move(_) |
            PrintHex(_) |
            PrintBool(_) |
            PrintTime(_) |
            SetRetval(_) |
            GetVMThreadLocal |
            KillStack(_) |
            CurrentStack |
            SwapStackKill { .. } => false,

            _ => false
        }
    }

    fn debug_str(&self, ops: &Vec<P<TreeNode>>) -> String {
        match &self.v {
            &Instruction_::BinOp(op, op1, op2) => {
                format!("{}<{}> {} {}", op, ops[op1].ty(), ops[op1], ops[op2])
            }
            &Instruction_::BinOpWithStatus(op, status, op1, op2) => format!(
                "{}{}<{}> {} {}",
                op,
                status,
                ops[op1].ty(),
                ops[op1],
                ops[op2]
            ),
            &Instruction_::CmpOp(op, op1, op2) => {
                format!("{}<{}> {} {}", op, ops[op1].ty(), ops[op1], ops[op2])
            }
            &Instruction_::ConvOp {
                operation,
                ref from_ty,
                ref to_ty,
                operand
            } => format!(
                "{} <{} {}> {}",
                operation, from_ty, to_ty, ops[operand]
            ),
            &Instruction_::ExprCall { ref data, is_abort } => {
                if is_abort {
                    panic!("ABORT is not supported");
                }
                format!("CALL{}", data.debug_str(ops))
            }
            &Instruction_::ExprCCall { ref data, is_abort } => {
                if is_abort {
                    panic!("ABORT is not supported");
                }
                format!("CCALL{}", data.debug_str(ops))
            }
            &Instruction_::Load {
                is_ptr,
                mem_loc,
                order
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "LOAD{} {}<{}> {}",
                    ptr,
                    order,
                    ops[mem_loc].ty().get_referent_ty().unwrap(),
                    ops[mem_loc]
                )
            }
            &Instruction_::Store {
                value,
                is_ptr,
                mem_loc,
                order
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "STORE{} {}<{}> {} {}",
                    ptr,
                    order,
                    ops[mem_loc].ty().get_referent_ty().unwrap(),
                    ops[mem_loc],
                    ops[value]
                )
            }
            &Instruction_::CmpXchg {
                is_ptr,
                is_weak,
                success_order,
                fail_order,
                mem_loc,
                expected_value,
                desired_value
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                let weak = select_value!(is_weak, " WEAK", "");
                format!(
                    "CMPXCHG{}{} {} {}<{}> {} {} {}",
                    ptr,
                    weak,
                    success_order,
                    fail_order,
                    ops[mem_loc].ty().get_referent_ty().unwrap(),
                    ops[mem_loc],
                    ops[expected_value],
                    ops[desired_value]
                )
            }
            &Instruction_::AtomicRMW {
                is_ptr,
                order,
                op,
                mem_loc,
                value
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "ATOMICRMW{} {} {}<{}> {} {}",
                    ptr,
                    order,
                    op,
                    ops[mem_loc].ty().get_referent_ty().unwrap(),
                    ops[mem_loc],
                    ops[value]
                )
            }
            &Instruction_::New(ref ty) => format!("NEW<{}>", ty),
            &Instruction_::AllocA(ref ty) => format!("ALLOCA<{}>", ty),
            &Instruction_::NewHybrid(ref ty, len) => {
                format!("NEWHYBRID<{} {}> {}", ty, ops[len].ty(), ops[len])
            }
            &Instruction_::AllocAHybrid(ref ty, len) => {
                format!("ALLOCAHYBRID<{} {}> {}", ty, ops[len].ty(), ops[len])
            }
            &Instruction_::NewStack(func) => format!(
                "COMMINST @uvm.new_stack<[{}]>({})",
                ops[func].ty().get_sig().unwrap(),
                ops[func]
            ),
            &Instruction_::NewReg(size) => {
                format!("COMMINST @uvm.new_region({})", ops[size])
            }
            &Instruction_::DeleteReg(regref) => {
                format!("COMMINST @uvm.delete_region({})", ops[regref])
            }
            &Instruction_::AllocAU(ref ty) => {
                format!("COMMINST @uvm.AllocAU({})", ty.id())
            }
            &Instruction_::AllocAUHybrid(ref ty, var_len) => format!(
                "COMMINST @uvm.AllocAUHybrid({}, {})",
                ty.id(),
                ops[var_len]
            ),
            &Instruction_::rAlloc(regref, ref ty) => {
                format!("COMMINST @uvm.rAlloc({}, {})", ops[regref], ty.id())
            }
            &Instruction_::rAllocHybrid(regref, ref ty, var_len) => format!(
                "COMMINST @uvm.rAllocHybrid({}, {}, {})",
                ops[regref],
                ty.id(),
                ops[var_len]
            ),
            //            &Instruction_::rAllocT(regref, ty) => format!(
            //                "COMMINST @uvm.rAllocT({}, {})",
            //                ops[regref],
            //                ops[ty]
            //            ),
            &Instruction_::eAlloc(ref ty) => {
                format!("COMMINST @uvm.eAlloc({})", ty.id())
            }
            &Instruction_::eAllocHybrid(ref ty, var_len) => format!(
                "COMMINST @uvm.eAllocHybrid({}, {})",
                ty.id(),
                ops[var_len]
            ),
            //            &Instruction_::eAllocT( ty) => format!(
            //                "COMMINST @uvm.eAllocT({})",
            //                ops[ty]
            //            ),
            &Instruction_::eDelete(obj) => {
                format!("COMMINST @uvm.eDelete({})", ops[obj])
            }
            //            &Instruction_::eDeleteT( obj) => format!(
            //                "COMMINST @uvm.eDeleteT({})",
            //                ops[obj]
            //            ),
            &Instruction_::NewThread {
                stack,
                thread_local,
                is_exception,
                ref args
            } => {
                let new_stack_clause =
                    format_new_stack_clause(is_exception, args, ops);
                let thread_local = thread_local
                    .map(|t| format!(" THREADLOCAL({})", ops[t]))
                    .unwrap_or("".to_string());
                format!(
                    "NEWTHREAD {}{} {}",
                    ops[stack], thread_local, new_stack_clause,
                )
            }

            &Instruction_::NewFutex => format!("NEWFUTEX"),
            &Instruction_::DeleteFutex(futexref) => {
                format!("DELETEFUTEX {}", ops[futexref])
            }
            &Instruction_::LockFutex(futexref, timeout) => {
                format!("LockFUTEX ({}, {})", ops[futexref], ops[timeout])
            }
            &Instruction_::UnlockFutex(futexref) => {
                format!("UNLOCKFUTEX {}", ops[futexref])
            }

            &Instruction_::NewRTThread {
                attr,
                stack,
                thread_local,
                is_exception,
                ref args
            } => {
                let new_stack_clause =
                    format_new_stack_clause(is_exception, args, ops);
                let thread_local = thread_local
                    .map(|t| format!(" THREADLOCAL({})", ops[t]))
                    .unwrap_or("".to_string());
                format!(
                    "NEWRTTHREAD {}, {}, {}, {}",
                    ops[attr], ops[stack], thread_local, new_stack_clause,
                )
            }

            &Instruction_::NotifyThread(thread) => {
                format!("COMMINST @uvm.notifythread({})", ops[thread])
            }
            &Instruction_::ThreadSetPriority(thread, priority) => format!(
                "COMMINST @uvm.threadsetpriority({}, {})",
                ops[thread], ops[priority]
            ),
            &Instruction_::ThreadGetPriority(thread) => {
                format!("COMMINST @uvm.threadgetpriority({})", ops[thread])
            }
            &Instruction_::ThreadClearCPU(thread, cpu) => format!(
                "COMMINST @uvm.threadclearcpu({}, {})",
                ops[thread], ops[cpu]
            ),
            &Instruction_::ThreadSetCPU(thread, cpu) => format!(
                "COMMINST @uvm.threadsetcpu({}, {})",
                ops[thread], ops[cpu]
            ),
            &Instruction_::ThreadIssetCPU(thread, cpu) => format!(
                "COMMINST @uvm.threadissetcpu({}, {})",
                ops[thread], ops[cpu]
            ),
            &Instruction_::GetTime => format!("COMMINST @uvm.gettime()",),
            &Instruction_::SetTime(time) => {
                format!("COMMINST @uvm.settime({})", ops[time])
            }
            &Instruction_::NewTimer => format!("COMMINST @uvm.newtimer"),
            &Instruction_::SetTimer {
                tmr,
                tm,
                prd,
                ref data
            } => format!(
                "COMMINST @uvm.settimer({}, {}, {}) ",
                ops[tmr], ops[tm], ops[prd]
            ),
            &Instruction_::CancelTimer(tmr) => {
                format!("COMMINST @uvm.canceltimer({})", ops[tmr])
            }
            &Instruction_::DeleteTimer(tmr) => {
                format!("COMMINST @uvm.deletetimer({})", ops[tmr])
            }
            &Instruction_::Sleep(dur) => {
                format!("COMMINST @uvm.sleep_ns({})", ops[dur])
            }

            &Instruction_::NewAttr => format!("NEWATTR()"),
            &Instruction_::DeleteAttr(aref) => {
                format!("DELETEATTR({})", ops[aref])
            }
            &Instruction_::ThreadSetAttr(tref, aref) => {
                format!("SETATTR({}, {})", ops[tref], ops[aref])
            }
            &Instruction_::ThreadGetAttr(tref) => {
                format!("GETATTR({})", ops[tref])
            }
            &Instruction_::AttrSetPriority(aref, p) => format!(
                "COMMINST @uvm.attr.setpriority({}, {})",
                ops[aref], ops[p]
            ),
            &Instruction_::AttrGetPriority(aref) => {
                format!("COMMINST @uvm.attr.getpriority({})", ops[aref])
            }
            &Instruction_::AttrSetCPU(aref, c) => {
                format!("COMMINST @uvm.attr.setcpu({}, {})", ops[aref], ops[c])
            }
            &Instruction_::AttrClearCPU(aref, c) => format!(
                "COMMINST @uvm.attr.clearcpu({}, {})",
                ops[aref], ops[c]
            ),
            &Instruction_::AttrIssetCPU(aref, c) => format!(
                "COMMINST @uvm.attr.issetcpu({}, {})",
                ops[aref], ops[c]
            ),
            &Instruction_::AttrZeroCPU(aref) => {
                format!("COMMINST @uvm.attr.zerocpu({})", ops[aref])
            }
            &Instruction_::eAllocPA(ref ty, addr) => format!(
                "COMMINST @uvm.emm.eallocpa({}, {})",
                ty.id(),
                ops[addr]
            ),
            &Instruction_::eAllocHybridPA(ref ty, len, addr) => format!(
                "COMMINST @uvm.emm.eallochybridpa({}, {}, {})",
                ty.id(),
                ops[len],
                ops[addr]
            ),
            &Instruction_::BindObject(obj) => {
                format!("COMMINST @uvm.emm.bindobject({})", ops[obj])
            }
            &Instruction_::UnbindObject(obj) => {
                format!("COMMINST @uvm.emm.unbindobject({})", ops[obj])
            }
            &Instruction_::NewRegionPA(size, addr) => format!(
                "COMMINST @uvm.regions.newregionpa({}, {})",
                ops[size], ops[addr]
            ),
            &Instruction_::BindRegion(reg) => {
                format!("COMMINST @uvm.regions.bindregion({})", ops[reg])
            }
            &Instruction_::UnbindRegion(reg) => {
                format!("COMMINST @uvm.regions.unbindregion({})", ops[reg])
            }

            &Instruction_::NewFrameCursor(stack) => {
                format!("COMMINST @uvm.meta.new_cursor({})", ops[stack])
            }
            &Instruction_::GetIRef(reference) => format!(
                "GETIREF<{}> {}",
                ops[reference].ty().get_referent_ty().unwrap(),
                ops[reference]
            ),
            &Instruction_::GetFieldIRef {
                is_ptr,
                base,
                index
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "GETFIELDIREF{}<{} {}> {}",
                    ptr,
                    ops[base].ty().get_referent_ty().unwrap(),
                    index,
                    ops[base]
                )
            }
            &Instruction_::GetElementIRef {
                is_ptr,
                base,
                index
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "GETELEMIREF{}<{} {}>{} {}",
                    ptr,
                    ops[base].ty().get_referent_ty().unwrap(),
                    ops[index].ty(),
                    ops[base],
                    ops[index]
                )
            }
            &Instruction_::ShiftIRef {
                is_ptr,
                base,
                offset
            } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "SHIFTIREF{}<{} {}>{} {}",
                    ptr,
                    ops[base].ty().get_referent_ty().unwrap(),
                    ops[offset].ty(),
                    ops[base],
                    ops[offset]
                )
            }
            &Instruction_::GetVarPartIRef { is_ptr, base } => {
                let ptr = select_value!(is_ptr, " PTR", "");
                format!(
                    "GETVARPARTIREF{}<{}> {}",
                    ptr,
                    ops[base].ty().get_referent_ty().unwrap(),
                    ops[base]
                )
            }

            &Instruction_::Fence(order) => format!("FENCE {}", order),

            &Instruction_::Return(ref vals) => {
                if vals.len() == 0 {
                    format!("RET")
                } else if vals.len() == 1 {
                    format!("RET {}", ops[vals[0]])
                } else {
                    format!("RET ({})", op_vector_str(vals, ops))
                }
            }
            &Instruction_::ThreadExit => {
                "COMMINST @uvm.thread_exit".to_string()
            }
            &Instruction_::CurrentStack => {
                "COMMINST @uvm.current_stack".to_string()
            }
            &Instruction_::KillStack(s) => {
                format!("COMMINST @uvm.kill_stack({})", ops[s])
            }
            &Instruction_::Throw(exn_obj) => format!("THROW {}", ops[exn_obj]),
            &Instruction_::TailCall(ref call) => {
                format!("TAILCALL{}", call.debug_str(ops))
            }
            &Instruction_::Branch1(ref dest) => {
                format!("BRANCH {}", dest.debug_str(ops))
            }
            &Instruction_::Branch2 {
                cond,
                ref true_dest,
                ref false_dest,
                ..
            } => format!(
                "BRANCH2 {} {} {}",
                ops[cond],
                true_dest.debug_str(ops),
                false_dest.debug_str(ops)
            ),
            &Instruction_::Select {
                cond,
                true_val,
                false_val
            } => format!(
                "SELECT<{} {}> {} {} {}",
                ops[cond].ty(),
                ops[true_val].ty(),
                ops[cond],
                ops[true_val],
                ops[false_val]
            ),
            &Instruction_::Watchpoint {
                id,
                ref disable_dest,
                ref resume
            } => {
                match id {
                    Some(id) => {
                        format!(
                            // TODO: WPEXC should be optional
                            "WATCHPOINT {}<{}> {} {} WPEXC({})",
                            id,
                            format_value_types(&self.value),
                            disable_dest.as_ref().unwrap().debug_str(ops),
                            resume.normal_dest.debug_str(ops),
                            resume.exn_dest.debug_str(ops)
                        )
                    }
                    //TRAP < Ts > excClause keepAliveClause
                    None => format!(
                        "TRAP<{}> {}",
                        format_value_types(&self.value),
                        resume.debug_str(ops)
                    )
                }
            }
            &Instruction_::WPBranch {
                wp,
                ref disable_dest,
                ref enable_dest
            } => format!(
                "WPBRANCH {} {} {}",
                wp,
                disable_dest.debug_str(ops),
                enable_dest.debug_str(ops)
            ),
            &Instruction_::Call {
                ref data,
                ref resume
            } => {
                format!("CALL{} {}", data.debug_str(ops), resume.debug_str(ops))
            }
            &Instruction_::CCall {
                ref data,
                ref resume
            } => format!(
                "CCALL{} {}",
                data.debug_str(ops),
                resume.debug_str(ops)
            ),
            &Instruction_::SwapStackExpr {
                stack,
                is_exception,
                ref args
            } => format!(
                "SWAPSTACK {} RET_WITH<{}> {}",
                ops[stack],
                format_value_types(&self.value),
                format_new_stack_clause(is_exception, args, ops)
            ),
            &Instruction_::SwapStackExc {
                stack,
                is_exception,
                ref args,
                ref resume
            } => format!(
                "SWAPSTACK {} RET_WITH<{}> {} {}",
                ops[stack],
                format_value_types(&self.value),
                format_new_stack_clause(is_exception, args, ops),
                resume.debug_str(ops)
            ),

            &Instruction_::SwapStackKill {
                stack,
                is_exception,
                ref args
            } => format!(
                "SWAPSTACK {} KILL_OLD {}",
                ops[stack],
                format_new_stack_clause(is_exception, args, ops)
            ),

            &Instruction_::Switch {
                cond,
                ref default,
                ref branches
            } => {
                //SWITCH < T > opnd default { ( value dest ) rep }
                let mut ret = format!(
                    "SWITCH<{}> {} {} {{",
                    ops[cond].ty(),
                    ops[cond],
                    default.debug_str(ops)
                );
                for i in 0..branches.len() {
                    let (op, ref dest) = branches[i];
                    ret.push_str(
                        format!("{} {}", ops[op], dest.debug_str(ops)).as_str()
                    );
                    if i != branches.len() - 1 {
                        ret.push_str(" ");
                    }
                }
                ret.push_str("}");

                ret
            }
            &Instruction_::ExnInstruction {
                ref inner,
                ref resume
            } => format!("{} {}", inner.debug_str(ops), resume.debug_str(ops)),

            // common inst
            &Instruction_::CommonInst_GetThreadLocal => {
                format!("COMMINST @uvm.get_threadlocal")
            }
            &Instruction_::CommonInst_SetThreadLocal(op) => {
                format!("COMMINST @uvm.set_threadlocal({})", ops[op])
            }

            &Instruction_::CommonInst_Pin(op) => format!(
                "COMMINST @uvm.native.pin<{}>({})",
                ops[op].ty(),
                ops[op]
            ),
            &Instruction_::CommonInst_Unpin(op) => format!(
                "COMMINST @uvm.native.unpin<{}>({})",
                ops[op].ty(),
                ops[op]
            ),
            &Instruction_::CommonInst_GetAddr(op) => format!(
                "COMMINST @uvm.native.get_addr<{}>({})",
                ops[op].ty(),
                ops[op]
            ),
            // Tagerf64
            &Instruction_::CommonInst_Tr64IsFp(op) => {
                format!("COMMINST @uvm.tr64.is_fp({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64IsInt(op) => {
                format!("COMMINST @uvm.tr64.is_int({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64IsRef(op) => {
                format!("COMMINST @uvm.tr64.is_ref({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64FromFp(op) => {
                format!("COMMINST @uvm.tr64.from_fp({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64FromInt(op) => {
                format!("COMMINST @uvm.tr64.from_int({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64FromRef(op1, op2) => format!(
                "COMMINST @uvm.tr64.from_ref({} {})",
                ops[op1], ops[op2]
            ),
            &Instruction_::CommonInst_Tr64ToFp(op) => {
                format!("COMMINST @uvm.tr64.to_fp({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64ToInt(op) => {
                format!("COMMINST @uvm.tr64.to_int({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64ToRef(op) => {
                format!("COMMINST @uvm.tr64.to_ref({})", ops[op])
            }
            &Instruction_::CommonInst_Tr64ToTag(op) => {
                format!("COMMINST @uvm.tr64.to_tag({})", ops[op])
            }

            // move
            &Instruction_::Move(from) => {
                format!("MOVE<{}> {}", ops[from].ty(), ops[from])
            }
            // print hex
            &Instruction_::PrintHex(i) => {
                format!("PRINTHEX<{}> {}", ops[i].ty(), ops[i])
            }
            &Instruction_::PrintBool(i) => {
                format!("PRINTBOOL<{}> {}", ops[i].ty(), ops[i])
            }
            &Instruction_::PrintTime(i) => {
                format!("PRINTTIME<{}> {}", ops[i].ty(), ops[i])
            }
            // set retval
            &Instruction_::SetRetval(val) => format!("SETRETVAL {}", ops[val]),
            &Instruction_::RandI(min, max) => {
                format!("RandI ({}, {})", ops[min], ops[max])
            }
            &Instruction_::RandF(min, max) => {
                format!("RandF ({}, {})", ops[min], ops[max])
            }
            // get vm thread local
            &Instruction_::GetVMThreadLocal => format!("GETVMTHREADLOCAL")
        }
    }
}

const PRINT_INST_NAME: bool = false;

impl fmt::Display for Instruction {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        let ref ops = self.ops;
        let value = match &self.value {
            &Some(ref v) if v.len() == 0 => format!(""),
            &Some(ref v) if v.len() == 1 => format!("{} = ", v[0]),
            &Some(ref v) => format!("({}) = ", vec_utils::as_str_sp(&v)),
            &None => format!("")
        };

        if PRINT_INST_NAME {
            write!(f, "{}[{}]{}", value, self.hdr, self.debug_str(ops))
        } else {
            write!(f, "{}{}", value, self.debug_str(ops))
        }
    }
}

/// Instruction_ is used for pattern matching for Instruction
#[allow(non_camel_case_types)]
#[derive(Debug, Clone)]
pub enum Instruction_ {
    // non-terminal instruction
    /// binary operations
    BinOp(BinOp, OpIndex, OpIndex),
    /// binary operations with status flag (overflow, sign, etc. )
    BinOpWithStatus(BinOp, BinOpStatus, OpIndex, OpIndex),

    /// comparison operations
    CmpOp(CmpOp, OpIndex, OpIndex),

    /// conversion operations (casting)
    ConvOp {
        operation: ConvOp,
        from_ty: P<MuType>,
        to_ty: P<MuType>,
        operand: OpIndex
    },

    /// a non-terminating Call instruction (the call does not have an
    /// exceptional branch) This instruction is not in the Mu spec, but is
    /// documented in the HOL formal spec
    ExprCall {
        data: CallData,
        is_abort: bool // T to abort, F to rethrow
    },

    /// a non-terminating CCall instruction (the call does not have an
    /// exceptional branch) This instruction is not in the Mu spec, but is
    /// documented in the HOL formal spec
    ExprCCall {
        data: CallData,
        is_abort: bool
    },

    /// load instruction
    Load {
        is_ptr: bool,
        order: MemoryOrder,
        mem_loc: OpIndex
    },

    /// store instruction
    Store {
        is_ptr: bool,
        order: MemoryOrder,
        mem_loc: OpIndex,
        value: OpIndex
    },

    /// compare and exchange, yields a pair value (oldvalue, boolean (T =
    /// success, F = failure))
    CmpXchg {
        is_ptr: bool,
        is_weak: bool,
        success_order: MemoryOrder,
        fail_order: MemoryOrder,
        mem_loc: OpIndex,
        expected_value: OpIndex,
        desired_value: OpIndex
    },

    /// atomic read-modify-write, yields old memory value
    AtomicRMW {
        is_ptr: bool, // T for iref, F for ptr
        order: MemoryOrder,
        op: AtomicRMWOp,
        mem_loc: OpIndex,
        value: OpIndex // operand for op
    },

    /// allocate an object (non hybrid type) in the heap, yields a reference of
    /// the type
    New(P<MuType>),

    /// allocate an object (non hybrid type) on the stack, yields an iref of
    /// the type
    AllocA(P<MuType>),

    /// allocate an object (non hybrid type) on the stack, yields an uptr of
    /// the type
    AllocAU(P<MuType>),
    AllocAUHybrid(P<MuType>, OpIndex),

    /// allocate a hybrid type object in the heap, yields ref
    /// args: the type of the hybrid, hybrid part length
    NewHybrid(P<MuType>, OpIndex),

    /// allocate an emm region
    /// args: region size
    NewReg(OpIndex),
    NewRegionPA(OpIndex, OpIndex),

    /// deallocate a whole emm region
    /// args: regionref to the target region
    DeleteReg(OpIndex),

    BindRegion(OpIndex),
    UnbindRegion(OpIndex),

    /// allocates an untraced object on an emm region
    /// args: 1. a regionref to the target emm region
    /// args: 2. the object type
    /// returns: a uptr to the allocated object
    rAlloc(OpIndex, P<MuType>),
    rAllocHybrid(OpIndex, P<MuType>, OpIndex),

    //    /// allocates a traced object on an emm region
    //    /// args: 1. a regionref to the target emm region
    //    /// args: 2. the object type
    //    /// returns: an iref to the allocated object
    //    rAllocT(OpIndex, P<MuType>),
    /// allocate an untraced object on the emm
    /// args: type of the object
    /// returns: a uptr to the object
    eAlloc(P<MuType>),
    eAllocHybrid(P<MuType>, OpIndex),
    eAllocPA(P<MuType>, OpIndex),
    eAllocHybridPA(P<MuType>, OpIndex, OpIndex),

    BindObject(OpIndex),
    UnbindObject(OpIndex),

    /// deallocate an untraced emm object
    /// args: an uptr to the object
    eDelete(OpIndex),

    /// allocate a hybrid type object on the stack, yields iref
    /// args: the type of the hybrid, hybrid part length
    AllocAHybrid(P<MuType>, OpIndex),

    /// create a new Mu stack, yields stack ref
    /// args: functionref of the entry function
    NewStack(OpIndex),

    /// kill the given Mu stack
    KillStack(OpIndex),

    /// return stackref for the current stack
    CurrentStack,

    /// create a new Mu thread, yields thread reference
    /// args: stackref of a Mu stack, a list of arguments
    //    #[cfg(not(feature = "realtime"))]
    NewThread {
        stack: OpIndex,
        thread_local: Option<OpIndex>,
        is_exception: bool,
        args: Vec<OpIndex>
    },

    /// create a new Mu thread, yields thread reference
    /// args: stackref of a Mu stack, a list of arguments
    //    #[cfg(feature = "realtime")]
    NewRTThread {
        attr: OpIndex,
        stack: OpIndex,
        thread_local: Option<OpIndex>,
        is_exception: bool,
        args: Vec<OpIndex>
    },

    NewAttr,
    DeleteAttr(OpIndex),
    ThreadSetAttr(OpIndex, OpIndex),
    ThreadGetAttr(OpIndex),
    AttrSetPriority(OpIndex, OpIndex),
    AttrGetPriority(OpIndex),
    AttrSetCPU(OpIndex, OpIndex),
    AttrClearCPU(OpIndex, OpIndex),
    AttrIssetCPU(OpIndex, OpIndex),
    AttrZeroCPU(OpIndex),

    NewFutex,
    DeleteFutex(OpIndex),
    LockFutex(OpIndex, OpIndex),
    UnlockFutex(OpIndex),

    //    #[cfg(feature = "realtime")]
    /// notify a thread to start running
    /// args: threadref for the target thread
    NotifyThread(OpIndex),
    /// set the priority of a target thread
    /// args:
    /// - threadref for the target thread
    /// - the new priority value (int64)
    ThreadSetPriority(OpIndex, OpIndex),
    /// get the current priority of a target thread
    /// args:
    /// - threadref for the target thread
    /// returns:
    /// - an int64 representing the current priority value
    ThreadGetPriority(OpIndex),

    //    AffinityZero(OpIndex),
    /// add a cpu to the cpu set of a thread
    /// args:
    /// - threadref of the target thread
    /// - number of the cpu to add (e.g. #0 is the 1st cpu)
    ThreadSetCPU(OpIndex, OpIndex),
    /// remove a cpu from the cpu set of a thread
    /// args:
    /// - threadref of the target thread
    /// - number of the cpu to remove (e.g. #0 is the 1st cpu)
    ThreadClearCPU(OpIndex, OpIndex),

    /// check whether a cpu is a member of the cpu set of a thread
    /// args:
    /// - threadref of the target thread
    /// - number of the cpu to check (e.g. #0 is the 1st cpu)
    ThreadIssetCPU(OpIndex, OpIndex),

    //    AffinityEqual(OpIndex, OpIndex),
    GetTime,
    SetTime(OpIndex),

    NewTimer,
    SetTimer {
        tmr: OpIndex,
        tm: OpIndex,
        prd: OpIndex,
        data: CallData
    },
    CancelTimer(OpIndex),
    DeleteTimer(OpIndex),
    Sleep(OpIndex),

    /// create a frame cursor reference
    /// args: stackref of a Mu stack
    NewFrameCursor(OpIndex), // stack

    /// get internal reference of a reference
    /// args: a reference
    GetIRef(OpIndex),

    /// get internal reference of an iref (or uptr) to a struct/hybrid fix part
    GetFieldIRef {
        is_ptr: bool,
        base: OpIndex, // iref or uptr
        index: usize   // constant
    },

    /// get internal reference of an element of an iref (or uptr) to an array
    GetElementIRef {
        is_ptr: bool,
        base: OpIndex,
        index: OpIndex // can be constant or ssa var
    },

    /// offset an iref (or uptr) (offset is an index)
    ShiftIRef {
        is_ptr: bool,
        base: OpIndex,
        offset: OpIndex
    },

    /// get internal reference to an element in hybrid var part
    GetVarPartIRef {
        is_ptr: bool,
        base: OpIndex
    },

    /// a fence of certain memory order
    Fence(MemoryOrder),

    // terminal instruction
    /// return instruction
    /// args: a list of return values
    Return(Vec<OpIndex>),

    /// thread exit
    ThreadExit,

    /// throw an exception
    Throw(OpIndex),

    /// tail call a function (reuse current frame)
    TailCall(CallData),

    /// unconditional branch
    Branch1(Destination),

    /// conditional branch
    Branch2 {
        cond: OpIndex,
        true_dest: Destination,
        false_dest: Destination,
        true_prob: f32
    },

    /// returns value1 if condition is true, otherwise returns value2
    Select {
        cond: OpIndex,
        true_val: OpIndex,
        false_val: OpIndex
    },

    /// a watchpoint
    /// * Watchpoint NONE ResumptionData: serves as an unconditional trap. Trap
    ///   to client, and resume with ResumptionData
    /// * Watchpoint (WPID dest) ResumptionData:
    ///   * when disabled, jump to dest
    ///   * when enabled, trap to client and resume
    Watchpoint {
        id: Option<WPID>,
        disable_dest: Option<Destination>,
        resume: ResumptionData
    },

    /// a watchpoint branch, branch to different destinations based on
    /// enabled/disabled
    WPBranch {
        wp: WPID,
        disable_dest: Destination,
        enable_dest: Destination
    },

    /// a call instruction that may throw an exception
    Call {
        data: CallData,
        resume: ResumptionData
    },

    /// a ccall instruction that may throw an exception
    CCall {
        data: CallData,
        resume: ResumptionData
    },

    /// A swap stack with an exception clause (i.e. uses the RET_WITH form)
    SwapStackExc {
        stack: OpIndex,
        is_exception: bool,
        args: Vec<OpIndex>,
        resume: ResumptionData
    },

    /// A swap stack without an exception clause that is not a terminator
    /// (i.e. uses the RET_WITH form)
    SwapStackExpr {
        stack: OpIndex,
        is_exception: bool,
        args: Vec<OpIndex>
    },

    /// A swapstack without an exception clause that is a terminator (i.e. one
    /// with KILL_OLD)
    SwapStackKill {
        stack: OpIndex,
        is_exception: bool,
        args: Vec<OpIndex>
    },

    /// a multiway branch
    Switch {
        cond: OpIndex,
        default: Destination,
        branches: Vec<(OpIndex, Destination)>
    },

    /// a wrapper for any instruction that may throw an exception
    //  This is not used at the moment
    ExnInstruction {
        inner: Box<Instruction>,
        resume: ResumptionData
    },

    /// common inst: get thread local
    CommonInst_GetThreadLocal,
    /// common inst: set thread local
    CommonInst_SetThreadLocal(OpIndex),

    /// common inst: pin an object (prevent it being moved and reclaimed by
    /// GC), yields a uptr
    CommonInst_Pin(OpIndex),
    /// common inst: unpin an object (the object is automatically managed by
    /// GC)
    CommonInst_Unpin(OpIndex),
    /// common inst: get address of a global cell or a pinned object
    CommonInst_GetAddr(OpIndex),

    /// common inst: is the tagref a floating point?
    CommonInst_Tr64IsFp(OpIndex),
    /// common inst: is the tagref an int?
    CommonInst_Tr64IsInt(OpIndex),
    /// common inst: is the tagref a ref?
    CommonInst_Tr64IsRef(OpIndex),
    /// common inst: creates a tagref from floating point (double)
    CommonInst_Tr64FromFp(OpIndex),
    /// common inst: creates a tagref from int<52>
    CommonInst_Tr64FromInt(OpIndex),
    /// common inst: creates a tagref from reference (a ref-void typed ref, 6
    /// bits tag)
    CommonInst_Tr64FromRef(OpIndex, OpIndex),
    /// common inst: converts a tagref to floating point (double)
    CommonInst_Tr64ToFp(OpIndex),
    /// common inst: converts a tagref to integer (int<52>)
    CommonInst_Tr64ToInt(OpIndex),
    /// common inst: converts a tagref to reference
    CommonInst_Tr64ToRef(OpIndex),
    /// common inst: converts a tagref to a tag (int<64>)
    CommonInst_Tr64ToTag(OpIndex),

    /// internal use: move from value to value
    Move(OpIndex),
    /// internal use: print op as hex value
    PrintHex(OpIndex),
    PrintBool(OpIndex),
    PrintTime(OpIndex),
    /// internal use: set return value for main
    SetRetval(OpIndex),
    /// internal use: get zebu thread local
    GetVMThreadLocal,
    /// Int64 random genenrator
    RandI(OpIndex, OpIndex),
    /// f64 random generator
    RandF(OpIndex, OpIndex)
}

fn format_value_types(value: &Option<Vec<P<Value>>>) -> String {
    match value {
        &Some(ref v) => {
            let mut tys = format!("");
            for i in 0..v.len() {
                tys.push_str(format!("{}", v[i].ty).as_str());
                if i != v.len() - 1 {
                    tys.push_str(" ");
                }
            }
            tys
        }
        &None => "".to_string()
    }
}

fn format_new_stack_clause(
    is_exception: bool,
    args: &Vec<OpIndex>,
    ops: &Vec<P<TreeNode>>
) -> String {
    if is_exception {
        assert!(args.len() == 1);
        format!("THROW_EXC {}", ops[args[0]])
    } else {
        let mut arg_tys = format!("");
        let mut arg_vals = format!("");
        for i in 0..args.len() {
            let ref op = ops[args[i]];
            arg_tys.push_str(format!("{}", op.ty()).as_str());
            arg_vals.push_str(format!("{}", op).as_str());
            if i != args.len() - 1 {
                arg_tys.push_str(" ");
                arg_vals.push_str(" ");
            }
        }
        format!("PASS_VALUES<{}>({})", arg_tys, arg_vals)
    }
}
/// BinOpStatus represents status flags from a binary operation
#[derive(Copy, Clone)]
pub struct BinOpStatus {
    /// negative flag
    pub flag_n: bool,
    /// zero flag
    pub flag_z: bool,
    /// carry flag
    pub flag_c: bool,
    /// overflow flag
    pub flag_v: bool
}
impl fmt::Display for BinOpStatus {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "[")?;
        if self.flag_n {
            write!(f, "#N ")?;
        }
        if self.flag_z {
            write!(f, "#Z ")?;
        }
        if self.flag_c {
            write!(f, "#C ")?;
        }
        if self.flag_v {
            write!(f, "#V ")?;
        }
        Ok(())
    }
}

impl BinOpStatus {
    pub fn none() -> BinOpStatus {
        BinOpStatus {
            flag_n: false,
            flag_z: false,
            flag_c: false,
            flag_v: false
        }
    }

    pub fn n() -> BinOpStatus {
        BinOpStatus {
            flag_n: true,
            flag_z: false,
            flag_c: false,
            flag_v: false
        }
    }

    pub fn z() -> BinOpStatus {
        BinOpStatus {
            flag_n: false,
            flag_z: true,
            flag_c: false,
            flag_v: false
        }
    }

    pub fn c() -> BinOpStatus {
        BinOpStatus {
            flag_n: false,
            flag_z: false,
            flag_c: true,
            flag_v: false
        }
    }

    pub fn v() -> BinOpStatus {
        BinOpStatus {
            flag_n: false,
            flag_z: false,
            flag_c: false,
            flag_v: true
        }
    }
}

impl fmt::Debug for BinOpStatus {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        if self.flag_n {
            write!(f, "#N").unwrap();
        }
        if self.flag_z {
            write!(f, "#Z").unwrap();
        }
        if self.flag_c {
            write!(f, "#C").unwrap();
        }
        if self.flag_v {
            write!(f, "#V").unwrap();
        }
        Ok(())
    }
}

#[derive(PartialEq, Eq, Copy, Clone, Debug)]
pub enum MemoryOrder {
    NotAtomic,
    Relaxed,
    Consume,
    Acquire,
    Release,
    AcqRel,
    SeqCst
}

impl fmt::Display for MemoryOrder {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        use self::MemoryOrder::*;
        write!(
            f,
            "{}",
            match *self {
                NotAtomic => "",
                Relaxed => "RELAXED",
                Consume => "CONSUME",
                Acquire => "ACQUIRE",
                Release => "RELEASE",
                AcqRel => "ACQ_REL",
                SeqCst => "SEQ_CST"
            }
        )
    }
}

pub const C_CALL_CONVENTION: CallConvention =
    CallConvention::Foreign(ForeignFFI::C);
pub const MU_CALL_CONVENTION: CallConvention = CallConvention::Mu;

#[derive(Copy, Clone, PartialEq, Debug)]
pub enum CallConvention {
    Mu,
    Foreign(ForeignFFI)
}
impl fmt::Display for CallConvention {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        if *self == C_CALL_CONVENTION {
            write!(f, "#DEFAULT")
        } else if *self == MU_CALL_CONVENTION {
            write!(f, "#MU")
        } else {
            unimplemented!()
        }
    }
}

#[derive(Copy, Clone, Debug, PartialEq)]
pub enum ForeignFFI {
    C
}

#[derive(Clone, Debug)]
pub struct CallData {
    pub func: OpIndex,
    pub args: Vec<OpIndex>,
    pub convention: CallConvention
}

impl CallData {
    fn debug_str(&self, ops: &Vec<P<TreeNode>>) -> String {
        let func = &ops[self.func];
        let conv = if self.convention == CallConvention::Mu {
            "".to_string()
        } else {
            format!(" {}", self.convention)
        };
        format!(
            "{}<{}> {} ({})",
            conv,
            func.ty().get_sig().unwrap(),
            func,
            op_vector_str(&self.args, ops)
        )
    }
}

#[derive(Clone, Debug)]
pub struct ResumptionData {
    pub normal_dest: Destination,
    pub exn_dest: Destination
}

impl ResumptionData {
    fn debug_str(&self, ops: &Vec<P<TreeNode>>) -> String {
        format!(
            "EXC ({} {})",
            self.normal_dest.debug_str(ops),
            self.exn_dest.debug_str(ops)
        )
    }
}

#[derive(Clone, Debug)]
pub struct Destination {
    pub target: MuEntityRef,
    pub args: Vec<DestArg>
}

impl Destination {
    fn debug_str(&self, ops: &Vec<P<TreeNode>>) -> String {
        let mut ret = format!("{}", self.target);
        ret.push('(');
        for i in 0..self.args.len() {
            let ref arg = self.args[i];
            ret.push_str(arg.debug_str(ops).as_str());
            if i != self.args.len() - 1 {
                ret.push_str(" ");
            }
        }
        ret.push(')');

        ret
    }

    pub fn get_arguments_as_node(
        &self,
        ops: &Vec<P<TreeNode>>
    ) -> Vec<P<TreeNode>> {
        vec_utils::map(&self.args, |x| match x {
            &DestArg::Normal(i) => ops[i].clone(),
            &DestArg::Freshbound(_) => unimplemented!()
        })
    }

    pub fn get_arguments(&self, ops: &Vec<P<TreeNode>>) -> Vec<P<Value>> {
        vec_utils::map(&self.args, |x| match x {
            &DestArg::Normal(i) => ops[i].clone_value(),
            &DestArg::Freshbound(_) => unimplemented!()
        })
    }
}

#[derive(Clone, Debug)]
pub enum DestArg {
    /// a normal destination argument is an SSA value (appears in the ops field
    /// of the instruction)
    Normal(OpIndex),
    /// a freshbound argument is an undeclared/anonymous value (currently not
    /// support this)
    Freshbound(usize)
}

impl DestArg {
    fn debug_str(&self, ops: &Vec<P<TreeNode>>) -> String {
        match self {
            &DestArg::Normal(index) => format!("{}", ops[index]),
            &DestArg::Freshbound(n) => format!("${}", n)
        }
    }
}

fn op_vector_str(vec: &Vec<OpIndex>, ops: &Vec<P<TreeNode>>) -> String {
    let mut ret = String::new();
    for i in 0..vec.len() {
        let index = vec[i];
        ret.push_str(format!("{}", ops[index]).as_str());
        if i != vec.len() - 1 {
            ret.push_str(" ");
        }
    }
    ret
}