/seL4-refos-master/kernel/include/arch/x86/arch/ |
H A D | machine.h | 102 uint32_t low, high; local 104 asm volatile("rdmsr" : "=a"(low), "=d"(high) : "c"(reg)); 105 value = ((uint64_t)high << 32) | (uint64_t)low; 121 static inline void x86_wrmsr_parts(const uint32_t reg, const uint32_t high, const uint32_t low) argument 123 asm volatile("wrmsr" :: "a"(low), "d"(high), "c"(reg)); 129 uint32_t high = (uint32_t)(val >> 32); local 130 x86_wrmsr_parts(reg, high, low);
|
/seL4-refos-master/kernel/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 1234 def field_mask_proof(base, base_bits, sign_extend, high, size): 1235 if high: 1245 def sign_extend_proof(high, base_bits, base_sign_extend): 1246 if high and base_sign_extend: 1310 raise ValueError("Tag field is high-aligned for element %s" 1442 offset, size, high = ref.field_map[field] 1448 self.base_sign_extend, high, size) 1449 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1480 for (field, offset, size, high) in ref.fields: 1485 self.base_sign_extend, high, siz [all...] |
/seL4-refos-master/kernel/libsel4/tools/ |
H A D | bitfield_gen.py | 1234 def field_mask_proof(base, base_bits, sign_extend, high, size): 1235 if high: 1245 def sign_extend_proof(high, base_bits, base_sign_extend): 1246 if high and base_sign_extend: 1310 raise ValueError("Tag field is high-aligned for element %s" 1442 offset, size, high = ref.field_map[field] 1448 self.base_sign_extend, high, size) 1449 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1480 for (field, offset, size, high) in ref.fields: 1485 self.base_sign_extend, high, siz [all...] |
/seL4-refos-master/libs/libsel4/tools/ |
H A D | bitfield_gen.py | 1234 def field_mask_proof(base, base_bits, sign_extend, high, size): 1235 if high: 1245 def sign_extend_proof(high, base_bits, base_sign_extend): 1246 if high and base_sign_extend: 1310 raise ValueError("Tag field is high-aligned for element %s" 1442 offset, size, high = ref.field_map[field] 1448 self.base_sign_extend, high, size) 1449 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1480 for (field, offset, size, high) in ref.fields: 1485 self.base_sign_extend, high, siz [all...] |
/seL4-refos-master/kernel/tools/ |
H A D | bitfield_gen.py | 1234 def field_mask_proof(base, base_bits, sign_extend, high, size): 1235 if high: 1245 def sign_extend_proof(high, base_bits, base_sign_extend): 1246 if high and base_sign_extend: 1310 raise ValueError("Tag field is high-aligned for element %s" 1442 offset, size, high = ref.field_map[field] 1448 self.base_sign_extend, high, size) 1449 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1480 for (field, offset, size, high) in ref.fields: 1485 self.base_sign_extend, high, siz [all...] |
/seL4-refos-master/kernel/src/arch/x86/object/ |
H A D | vcpu.c | 60 /* Cache the values that we calculated for bits that need to be set high 179 static bool_t check_fixed_value(word_t val, word_t low, word_t high) argument 183 /* check if any bits that should be high, are not 184 * high & val represents the set of bits that are 185 * correctly set to high. if this is equal to high 187 * bits were not high we can invert and mask with 188 * high again. Now if this is 0 everythins is fine, 191 not_high = high & ~(high 390 applyFixedBits(uint32_t original, uint32_t high, uint32_t low) argument 528 invokeEnableIOPort(vcpu_t *vcpu, cte_t *slot, cap_t cap, uint16_t low, uint16_t high) argument 548 uint16_t low, high; local 585 invokeDisableIOPort(vcpu_t *vcpu, uint16_t low, uint16_t high) argument 595 uint16_t low, high; local [all...] |
H A D | ioport.c | 313 void setIOPortMask(void *ioport_bitmap, uint16_t low, uint16_t high, bool_t set) argument 319 int high_word = high >> wordRadix; 321 int high_index = high & MASK(wordRadix);
|
/seL4-refos-master/projects/seL4_libs/libsel4bench/arch_include/x86/sel4bench/arch/ |
H A D | sel4bench.h | 22 uint32_t low, high; \ 34 "=r"(high), \ 39 (var) = (((uint64_t)high) << 32ull) | ((uint64_t)low); \
|
/seL4-refos-master/kernel/manual/parts/ |
H A D | intro.tex | 29 design, followed by a reference of the high-level API exposed by the
|
H A D | ipc.tex | 137 The kernel will silently ignore any usage of the high 4 bits.
|
H A D | objects.tex | 61 capabilities. This enables software-component isolation with a high
|
H A D | io.tex | 150 a Domain ID as the high 16 bits of the \texttt{badge} argument.
|
/seL4-refos-master/kernel/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 902 seL4_Word low, high; local 903 x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, MCS_COND(0, &high)); 906 *high = seL4_GetMR(1); 909 return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32);
|
/seL4-refos-master/libs/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | syscalls.h | 902 seL4_Word low, high; local 903 x86_sys_recv(seL4_SysX86DangerousRDMSR, msr, &unused0, &unused1, &low, MCS_COND(0, &high)); 906 *high = seL4_GetMR(1); 909 return ((seL4_Uint64)low) | ((seL4_Uint64)high << 32);
|
/seL4-refos-master/projects/refos/impl/apps/nethack/src/nethack-3.4.3/doc/ |
H A D | Guidebook.tex | 971 with another key, modifies it by setting the `meta' [8th, or `high'] 1514 at this task, as are those with a high level of proficiency in the 3072 paltry cost of not getting on the high score list.
|
/seL4-refos-master/apps/nethack/src/nethack-3.4.3/doc/ |
H A D | Guidebook.tex | 971 with another key, modifies it by setting the `meta' [8th, or `high'] 1514 at this task, as are those with a high level of proficiency in the 3072 paltry cost of not getting on the high score list.
|