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

12345

/seL4-l4v-master/seL4/include/arch/x86/arch/
H A Dbenchmark.h14 uint32_t low, high; local
26 : "=r"(high), "=r"(low)
31 return ((uint64_t) high) << 32llu | (uint64_t) low;
H A Dmachine.h102 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 DleakageScript.sml71 `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 Dbasic_leakage_examplesScript.sml126 (* 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 DleakageLib.sml73 (``!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 Dmemusage.py83 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 Dxapic.h63 static inline void apic_write_icr(word_t high, word_t low) argument
65 apic_write_reg(APIC_ICR2, high);
H A Dx2apic.h62 static inline void apic_write_icr(word_t high, word_t low) argument
64 uint64_t icr = ((uint64_t)high << 32) | low;
H A Dapic.h23 void apic_write_icr(word_t high, word_t low);
/seL4-l4v-master/seL4/include/arch/x86/arch/object/
H A Dioport.h16 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 Dmachine.h84 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 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-master/seL4/src/arch/x86/machine/
H A Dhardware.c90 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 DholyHammer.sig11 (* For running holyhammer in the backgroup with a high time limit *)
/seL4-l4v-master/seL4/include/arch/x86/arch/64/mode/
H A Dmachine.h222 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 Dintro.tex21 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 Dbitfield_gen.py1234 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 Dbitfield_gen.py1234 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 Dbitfield_gen.py1234 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 DAnd.sml43 (* when you expect a high output at the AND gate *)
/seL4-l4v-master/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-master/seL4/src/arch/x86/object/
H A Dvcpu.c60 /* 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 Dioport.c313 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);

Completed in 219 milliseconds

12345