/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)); 133 uint32_t high = (uint32_t)(val >> 32); 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 CROS [all...] |
H A D | basic_leakage_examplesScript.sml | 129 (* Example 1: out = high + low *) 133 val high = Define value 134 `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\ 135 (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`; 146 then (H s "high") + (L s "low") else 0))`; 148 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 152 ``leakage (unif_prog_space (high (SU 217 val high = Define value 319 val high = Define value 370 val high = Define value 411 val high = 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)) - 75 SIGMA (\(out,l). (\x. x * lg (((1/(&(CARD high * CARD random)))* x))) 76 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) (high CROSS random))) 77 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``, METIS_TAC [unif_prog_space_leakage_computation_reduce]);
|
/seL4-l4v-10.1.1/l4v/misc/regression/ |
H A D | memusage.py | 80 self.high = 0 86 self.high = get_total_usage(self.pid) 90 # Poll the process periodically to track a high water mark of its 100 if usage > self.high: 101 self.high = usage 106 return self.high 147 high = 0 151 high = m.peak_mem_usage() 156 print('Peak usage %d bytes' % high, out=sys.stderr)
|
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/32/mode/ |
H A D | machine.h | 88 uint32_t high; local 98 [high] "=&d" (high), 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 77 apic_write_reg(APIC_ICR2, high);
|
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 | 228 uint32_t high; local 241 [high] "=&d" (high), 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. 471 high node must be defined before it is mentioned. *} 542 int key,var,low,high,root=0,n; local 546 if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4) 551 if (high >= 2) 552 high = loadhash_get(high); 554 if (low<0 || high<0 || var<0) 557 root = bdd_addref( bdd_ite(bdd_ithvar(var), high, low) );
|
H A D | kernel.h | 84 int high; member in struct:s_BddNode 155 #define HIGH(a) (bddnodes[a].high) 158 #define HIGHp(p) ((p)->high)
|
H A D | kernel.c | 593 to avoid resizing and saves space, and a high number reduces 1255 int bdd_makenode(unsigned int level, int low, int high) argument 1266 if (low == high) 1270 hash = NODEHASH(level, low, high); 1275 if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) 1312 hash = NODEHASH(level, low, high); 1333 HIGHp(node) = high;
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | hardware.c | 96 uint32_t low, high; local 124 high = x86_rdmsr_high(IA32_PREFETCHER_MSR); 131 x86_wrmsr(IA32_PREFETCHER_MSR, ((uint64_t)high) << 32 | low);
|
/seL4-l4v-10.1.1/l4v/camkes/glue-spec/document/ |
H A D | intro.tex | 25 abstract high-level specification of the behaviour of an entire \camkes 28 The specification is high-level, because it abstracts from the underlying 31 high-level types. Instantiating this framework we restrict it to the kinds of 34 implement this high-level semantic view is the main proof obligation of the 37 The idea of the specification is to provide a high-level view of the behaviour
|
/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | bitfield_gen.py | 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1185 if high: 1194 def sign_extend_proof(high, base_bits, base_sign_extend): 1195 if high and base_sign_extend: 1251 raise ValueError("Tag field is high-aligned for element %s" 1383 offset, size, high = ref.field_map[field] 1388 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size) 1389 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1419 for (field, offset, size, high) in ref.fields: 1423 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, siz [all...] |
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | bitfield_gen.py | 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1185 if high: 1194 def sign_extend_proof(high, base_bits, base_sign_extend): 1195 if high and base_sign_extend: 1251 raise ValueError("Tag field is high-aligned for element %s" 1383 offset, size, high = ref.field_map[field] 1388 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size) 1389 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1419 for (field, offset, size, high) in ref.fields: 1423 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, siz [all...] |
/seL4-l4v-10.1.1/seL4/tools/ |
H A D | bitfield_gen.py | 1184 def field_mask_proof(base, base_bits, sign_extend, high, size): 1185 if high: 1194 def sign_extend_proof(high, base_bits, base_sign_extend): 1195 if high and base_sign_extend: 1251 raise ValueError("Tag field is high-aligned for element %s" 1383 offset, size, high = ref.field_map[field] 1388 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, size) 1389 sign_extend = sign_extend_proof(high, self.base_bits, self.base_sign_extend) 1419 for (field, offset, size, high) in ref.fields: 1423 mask = field_mask_proof(self.base, self.base_bits, self.base_sign_extend, high, siz [all...] |
/seL4-l4v-10.1.1/HOL4/examples/STE/Examples/ |
H A D | And.sml | 43 (* when you expect a high output at the AND gate *)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | bdd.sml | 83 val high : bdd -> bdd = app1 (symb "mlbdd_bdd_high") value 194 val high = high bdd value 195 in if equal low FALSE then loop high ((var,true) :: acc) 243 val high = high r value 246 rootno high); 248 node high
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/object/ |
H A D | vcpu.c | 66 /* Cache the values that we calculated for bits that need to be set high 191 check_fixed_value(word_t val, word_t low, word_t high) argument 195 /* check if any bits that should be high, are not 196 * high & val represents the set of bits that are 197 * correctly set to high. if this is equal to high 199 * bits were not high we can invert and mask with 200 * high again. Now if this is 0 everythins is fine, 203 not_high = high & ~(high 406 applyFixedBits(uint32_t original, uint32_t high, uint32_t low) argument 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 334 int high_word = high >> wordRadix; 336 int high_index = high & MASK(wordRadix);
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | DatatypeSimps.sig | 84 (* Lifting case distinctions as high as possible *) 89 (* Reverse Lifting case distinctions as high as possible *)
|