register_address_increment
register_address_increment(ctxt, reg, df * op->bytes);
register_address_increment(ctxt, VCPU_REGS_RCX, -1);
register_address_increment(ctxt, VCPU_REGS_RCX, -count);