Searched refs:high (Results 1 - 25 of 107) sorted by relevance

12345

/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));
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 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 CROS
[all...]
H A Dbasic_leakage_examplesScript.sml129 (* 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 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)) -
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 Dmemusage.py80 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 Dmachine.h88 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 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
77 apic_write_reg(APIC_ICR2, high);
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.h228 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 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.
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 Dkernel.h84 int high; member in struct:s_BddNode
155 #define HIGH(a) (bddnodes[a].high)
158 #define HIGHp(p) ((p)->high)
H A Dkernel.c593 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 Dhardware.c96 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 Dintro.tex25 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 Dbitfield_gen.py1184 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 Dbitfield_gen.py1184 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 Dbitfield_gen.py1184 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 DAnd.sml43 (* when you expect a high output at the AND gate *)
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dbdd.sml83 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 Dvcpu.c66 /* 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 Dioport.c328 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 DDatatypeSimps.sig84 (* Lifting case distinctions as high as possible *)
89 (* Reverse Lifting case distinctions as high as possible *)

Completed in 122 milliseconds

12345