2 * This file is part of the Palacios Virtual Machine Monitor developed
3 * by the V3VEE Project with funding from the United States National
4 * Science Foundation and the Department of Energy.
6 * The V3VEE Project is a joint project between Northwestern University
7 * and the University of New Mexico. You can find out more at
10 * Copyright (c) 2008, Jack Lange <jarusl@cs.northwestern.edu>
11 * Copyright (c) 2008, The V3VEE Project <http://www.v3vee.org>
12 * All rights reserved.
14 * Author: Jack Lange <jarusl@cs.northwestern.edu>
16 * This is free software. You are permitted to use,
17 * redistribute, and modify it as specified in the file "V3VEE_LICENSE".
20 #include <palacios/vmm_types.h>
25 void __inline__ v3_cpuid(uint_t target, uint_t * eax, uint_t * ebx, uint_t * ecx, uint_t * edx) {
26 __asm__ __volatile__ (
29 "movl %%ebx, %%esi\n\t"
31 : "=a" (*eax), "=S" (*ebx), "=c" (*ecx), "=d" (*edx)
40 void __inline__ v3_set_msr(uint_t msr, uint_t high_byte, uint_t low_byte) {
41 __asm__ __volatile__ (
44 : "c" (msr), "d" (high_byte), "a" (low_byte)
52 void __inline__ v3_get_msr(uint_t msr, uint_t * high_byte, uint_t * low_byte) {
53 __asm__ __volatile__ (
55 : "=d" (*high_byte), "=a" (*low_byte)
62 void __inline__ v3_enable_ints() {
63 __asm__ __volatile__ ("sti");
66 void __inline__ v3_disable_ints() {
67 __asm__ __volatile__ ("cli");