/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/ |
H A D | benchmark.h | 20 uint32_t low, high; local 32 : "=r" (high), "=r" (low) 37 return ((uint64_t) high) << 32llu | (uint64_t) low;
|
H A D | machine.h | 106 uint32_t low, high; local 108 asm volatile("rdmsr" : "=a"(low), "=d"(high) : "c"(reg)); 109 value = ((uint64_t)high << 32) | (uint64_t)low; 125 static inline void x86_wrmsr_parts(const uint32_t reg, const uint32_t high, const uint32_t low) argument 127 asm volatile("wrmsr" :: "a"(low), "d"(high), "c"(reg)); 132 uint32_t low = (uint32_t)val; local 134 x86_wrmsr_parts(reg, high, low);
|
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | leakageScript.sml | 110 `unif_prog_dist high low random = 111 (\s. if s IN (high CROSS low) CROSS random then 112 1/(&(CARD ((high CROSS low) CROSS random))) else 0)`; 116 `unif_prog_space high low random = 117 ((high CROSS low) CROSS random, 118 POW ((high CROSS low) CROSS random), 119 (\s. SIGMA (unif_prog_dist high low random) s))`; 136 ``!high low random. FINITE high /\ FINITE low /\ FINITE random /\ 137 ~((high CROSS low) CROS [all...] |
H A D | basic_leakage_examplesScript.sml | 117 (if (s' = "low") then [n3] else []))) = 119 (if (s' = "low") then [m3] else [])))) = 125 POP_ASSUM (MP_TAC o Q.SPEC `"low"`) ++ RW_TAC string_ss []]) 129 (* Example 1: out = high + low *) 137 val low = Define value 138 `(low 0 = {(\s:string. if s = "low" then 0 else 0)}) /\ 139 (low (SUC n) = (\s:string. if s = "low" then SUC n else 0)INSERT(low 220 val low = Define value 323 val low = Define value 374 val low = Define value 419 val low = Define value [all...] |
H A D | leakageLib.sml | 73 val unif_prog_space_leakage_computation_reduce_COMPUTE = prove (``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ ~((high CROSS low) CROSS random={}) ==> (leakage (unif_prog_space high low random) f = (1/(&(CARD high * CARD low * CARD random)))* (SIGMA (\(out,h,l). (\x. x * lg (((1/(&(CARD random)))* x))) (SIGMA (\r. if (f((h,l),r)=out) then 1 else 0) random)) 74 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 77 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``, METIS_TAC [unif_prog_space_leakage_computation_reduce]);
|
H A D | dining_cryptosScript.sml | 70 `(set_announcements (high: bool state) (low:bool state) 77 low s) /\ 78 (set_announcements high low random n (SUC i) s = 84 (set_announcements high low random n i) s)`; 87 `(XOR_announces (low:bool state) (0:num) = low (STRCAT "announces" (toString 0))) /\ 88 (XOR_announces low (SUC i) = (low (STRCAT "announces" (toString (SUC i)))) xor 89 (XOR_announces low i))`; 92 `compute_result (low [all...] |
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | hardware.c | 96 uint32_t low, high; local 123 low = x86_rdmsr_low(IA32_PREFETCHER_MSR); 126 low |= IA32_PREFETCHER_MSR_L2; 127 low |= IA32_PREFETCHER_MSR_L2_ADJACENT; 128 low |= IA32_PREFETCHER_MSR_DCU; 129 low |= IA32_PREFETCHER_MSR_DCU_IP; 131 x86_wrmsr(IA32_PREFETCHER_MSR, ((uint64_t)high) << 32 | low);
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/32/mode/ |
H A D | machine.h | 87 uint32_t low; local 99 [low] "=&a" (low) 105 result.value = ((uint64_t)high << 32) | (uint64_t)low;
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/kernel/ |
H A D | x2apic.h | 74 apic_write_icr(word_t high, word_t low) argument 76 uint64_t icr = ((uint64_t)high << 32) | low;
|
H A D | xapic.h | 75 apic_write_icr(word_t high, word_t low) argument 78 apic_write_reg(APIC_ICR1, low);
|
H A D | apic.h | 28 void apic_write_icr(word_t high, word_t low);
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/ |
H A D | machine.h | 227 uint32_t low; local 242 [low] "=&a" (low) 248 result.value = ((uint64_t)high << 32) | (uint64_t)low;
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/object/ |
H A D | ioport.h | 21 void setIOPortMask(void *ioport_bitmap, uint16_t low, uint16_t high, bool_t set);
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bddio.c | 468 number, then the variable number and then the low and high nodes. 470 The nodes {\it must} be saved in a order such that any low or 542 int key,var,low,high,root=0,n; local 546 if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4) 549 if (low >= 2) 550 low = loadhash_get(low); 554 if (low<0 || high<0 || var<0) 557 root = bdd_addref( bdd_ite(bdd_ithvar(var), high, low) );
|
H A D | kernel.h | 83 int low; member in struct:s_BddNode 154 #define LOW(a) (bddnodes[a].low) 157 #define LOWp(p) ((p)->low)
|
H A D | tree.c | 53 int low = t->first; local 56 if (bddvar2level[n] < bddvar2level[low]) 57 low = n; 60 t->seq[bddvar2level[n]-bddvar2level[low]] = n;
|
H A D | kernel.c | 592 on how fast the package is. A low number means harder attempts 1255 int bdd_makenode(unsigned int level, int low, int high) argument 1266 if (low == high) 1267 return low; 1270 hash = NODEHASH(level, low, high); 1275 if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) 1312 hash = NODEHASH(level, low, high); 1332 LOWp(node) = low;
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bdd.sml | 82 val low : bdd -> bdd = app1 (symb "mlbdd_bdd_low") value 193 val low = low bdd value 195 in if equal low FALSE then loop high ((var,true) :: acc) 196 else loop low ((var,false) :: acc) 242 NONE => let val low = low r value 245 rootno low, 247 node low;
|
/seL4-l4v-10.1.1/HOL4/examples/STE/Examples/ |
H A D | And.sml | 31 (* when you expect a low output at the AND gate *)
|
H A D | Or.sml | 45 (* for the case when the output of the or gate is low *)
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/object/ |
H A D | vcpu.c | 67 * and low in various vmcs fields */ 191 check_fixed_value(word_t val, word_t low, word_t high) argument 210 * that should be low by first inverting */ 211 not_low = ~low & ~(~low & ~val); 256 /* Read out the fixed high and low bits from the MSRs */ 315 /* See if the hardware requires bits that require to be high to be low */ 385 * be high that this core requires to be low. This can be checked with 406 applyFixedBits(uint32_t original, uint32_t high, uint32_t low) argument 409 original &= low; 550 invokeEnableIOPort(vcpu_t *vcpu, cte_t *slot, cap_t cap, uint16_t low, uint16_t high) argument 571 uint16_t low, high; local 609 invokeDisableIOPort(vcpu_t *vcpu, uint16_t low, uint16_t high) argument 620 uint16_t low, high; local [all...] |
H A D | ioport.c | 328 setIOPortMask(void *ioport_bitmap, uint16_t low, uint16_t high, bool_t set) argument 333 int low_word = low >> wordRadix; 335 int low_index = low & MASK(wordRadix);
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | mos.ml | 5 % logic where Zz and Er represent low impedence %
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Exn.sml | 78 (* low-level trace *)
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | PackWord8Big.sml | 68 fun fourBytesToWord(highest, higher, lower, low) = 72 Word8.toLargeWord low 74 fun fourBytesToWordX(highest, higher, lower, low) = 78 Word8.toLargeWord low
|