/seL4-l4v-master/seL4/include/arch/x86/arch/ |
H A D | benchmark.h | 14 uint32_t low, high; local 26 : "=r"(high), "=r"(low) 31 return ((uint64_t) high) << 32llu | (uint64_t) low;
|
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-l4v-master/HOL4/examples/diningcryptos/ |
H A D | leakageScript.sml | 71 `unif_prog_dist high low random = 72 (\s. if s IN (high CROSS low) CROSS random then 73 1/(&(CARD ((high CROSS low) CROSS random))) else 0)`; 77 `unif_prog_space high low random = 78 ((high CROSS low) CROSS random, 79 POW ((high CROSS low) CROSS random), 80 (\s. SIGMA (unif_prog_dist high low random) s))`; 88 ``!high low random. FINITE high /\ FINITE low /\ FINITE random /\ 89 ~((high CROS [all...] |
H A D | basic_leakage_examplesScript.sml | 126 (* Example 1: out = high + low *) 130 val high = Define value 131 `(high 0 = {(\s:string. if s = "high" then 0 else 0)}) /\ 132 (high (SUC n) = (\s:string. if s = "high" then SUC n else 0)INSERT(high n))`; 143 then (H s "high") + (L s "low") else 0))`; 145 val example1_conv = SIMP_CONV arith_ss [high, low, random, lem1,lem2,lem3]; 149 ``leakage (unif_prog_space (high (SU 214 val high = Define value 316 val high = Define value 367 val high = Define value 408 val high = Define value [all...] |
H A D | leakageLib.sml | 73 (``!high low random f. FINITE high /\ FINITE low /\ FINITE random /\ 74 ~((high CROSS low) CROSS random={}) ==> 75 (leakage (unif_prog_space high low random) f = 76 (1/(&(CARD high * CARD low * CARD random)))* 79 (IMAGE (\s. (f s,FST s)) (high CROSS low CROSS random)) - 80 SIGMA (\(out,l). (\x. x * lg (((1/(&(CARD high * CARD random)))* x))) 81 (SIGMA (\(h,r). if (f((h,l),r)=out) then 1 else 0) (high CROSS random))) 82 (IMAGE (\s. (f s,SND (FST s))) (high CROSS low CROSS random))))``,
|
/seL4-l4v-master/l4v/misc/regression/ |
H A D | memusage.py | 83 self.high = 0 89 self.high = get_total_usage(self.pid) 93 # Poll the process periodically to track a high water mark of its 103 if usage > self.high: 104 self.high = usage 109 return self.high 152 high = 0 156 high = m.peak_mem_usage() 161 print('Peak usage %d bytes' % high, out=sys.stderr)
|
/seL4-l4v-master/seL4/include/arch/x86/arch/kernel/ |
H A D | xapic.h | 63 static inline void apic_write_icr(word_t high, word_t low) argument 65 apic_write_reg(APIC_ICR2, high);
|
H A D | x2apic.h | 62 static inline void apic_write_icr(word_t high, word_t low) argument 64 uint64_t icr = ((uint64_t)high << 32) | low;
|
H A D | apic.h | 23 void apic_write_icr(word_t high, word_t low);
|
/seL4-l4v-master/seL4/include/arch/x86/arch/object/ |
H A D | ioport.h | 16 void setIOPortMask(void *ioport_bitmap, uint16_t low, uint16_t high, bool_t set);
|
/seL4-l4v-master/seL4/include/arch/x86/arch/32/mode/ |
H A D | machine.h | 84 uint32_t high; local 94 [high] "=&d"(high), 101 result.value = ((uint64_t)high << 32) | (uint64_t)low;
|
/seL4-l4v-master/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-master/seL4/src/arch/x86/machine/ |
H A D | hardware.c | 90 uint32_t low, high; local 118 high = x86_rdmsr_high(IA32_PREFETCHER_MSR); 125 x86_wrmsr(IA32_PREFETCHER_MSR, ((uint64_t)high) << 32 | low);
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | holyHammer.sig | 11 (* For running holyhammer in the backgroup with a high time limit *)
|
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/ |
H A D | machine.h | 222 uint32_t high; local 235 [high] "=&d"(high), 242 result.value = ((uint64_t)high << 32) | (uint64_t)low;
|
/seL4-l4v-master/l4v/camkes/glue-spec/document/ |
H A D | intro.tex | 21 abstract high-level specification of the behaviour of an entire \camkes 24 The specification is high-level, because it abstracts from the underlying 27 high-level types. Instantiating this framework we restrict it to the kinds of 30 implement this high-level semantic view is the main proof obligation of the 33 The idea of the specification is to provide a high-level view of the behaviour
|
/seL4-l4v-master/seL4/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-l4v-master/seL4/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-l4v-master/seL4/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-l4v-master/HOL4/examples/STE/Examples/ |
H A D | And.sml | 43 (* when you expect a high output at the AND gate *)
|
/seL4-l4v-master/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-master/seL4/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);
|