Searched refs:low (Results 1 - 25 of 79) sorted by relevance

1234

/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/
H A Dbenchmark.h20 uint32_t low, high; local
32 : "=r" (high), "=r" (low)
37 return ((uint64_t) high) << 32llu | (uint64_t) low;
H A Dmachine.h106 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 DleakageScript.sml110 `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 Dbasic_leakage_examplesScript.sml117 (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 DleakageLib.sml73 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 Ddining_cryptosScript.sml70 `(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 Dhardware.c96 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 Dmachine.h87 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 Dx2apic.h74 apic_write_icr(word_t high, word_t low) argument
76 uint64_t icr = ((uint64_t)high << 32) | low;
H A Dxapic.h75 apic_write_icr(word_t high, word_t low) argument
78 apic_write_reg(APIC_ICR1, low);
H A Dapic.h28 void apic_write_icr(word_t high, word_t low);
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/64/mode/
H A Dmachine.h227 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 Dioport.h21 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 Dbddio.c468 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 Dkernel.h83 int low; member in struct:s_BddNode
154 #define LOW(a) (bddnodes[a].low)
157 #define LOWp(p) ((p)->low)
H A Dtree.c53 int low = t->first; local
56 if (bddvar2level[n] < bddvar2level[low])
57 low = n;
60 t->seq[bddvar2level[n]-bddvar2level[low]] = n;
H A Dkernel.c592 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 Dbdd.sml82 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 DAnd.sml31 (* when you expect a low output at the AND gate *)
H A DOr.sml45 (* for the case when the output of the or gate is low *)
/seL4-l4v-10.1.1/seL4/src/arch/x86/object/
H A Dvcpu.c67 * 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 Dioport.c328 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 Dmos.ml5 % logic where Zz and Er represent low impedence %
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DExn.sml78 (* low-level trace *)
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DPackWord8Big.sml68 fun fourBytesToWord(highest, higher, lower, low) =
72 Word8.toLargeWord low
74 fun fourBytesToWordX(highest, higher, lower, low) =
78 Word8.toLargeWord low

Completed in 255 milliseconds

1234