Searched refs:shift (Results 1 - 25 of 101) sorted by relevance

12345

/seL4-l4v-10.1.1/HOL4/src/0/
H A DSubst.sml48 fun shift (0, s) = s function
49 | shift (k, Shift(k',s)) = shift(k+k', s)
50 | shift (k, s) = Shift(k,s)
90 * Cons(shift k (s o s'), mk_cl (Shift(k,s)) x)
91 * or shift k (Cons (s o s', mk_cl s x)) <-- was prefered
97 | (Shift(k,s)) o s' = shift(k, s o s')
99 | (Cons(s,x)) o (Shift(k,s')) = s o shift(k-1, s')
102 then shift(k, s o shift(
[all...]
H A DSubst.sig7 val shift : int * 'a subs -> 'a subs value
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Dparse_struct_array.c68 int ts20110511_1(struct s *sptr, int i, int shift) argument
70 return ((sptr->data[i]) >> shift);
73 int ts20110511_2(struct s *sptr, int shift) argument
75 return ((sptr->sz) >> shift);
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexMarkedScript.sml57 (shift _ (MEps) _ = MEps ) /\
58 (shift m (MSym _ x) c = MSym (m /\ (x = c)) x ) /\
59 (shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\
60 (shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\
61 (shift m (MRep r) c = MRep (shift (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_coretypesScript.sml212 LSL_C (x: 'a word, shift:num) =
213 if shift = 0 then
216 let extended_x = w2n x * (2 ** shift) in
217 (x << shift, BIT (dimindex(:'a)) extended_x)`;
220 LSR_C (x: 'a word, shift:num) =
221 if shift = 0 then
224 (x >>> shift, BIT (shift - 1) (w2n x))`;
227 ASR_C (x: 'a word, shift:num) =
228 if shift
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/
H A Darm_coretypesScript.sml216 LSL_C (x: 'a word, shift:num) =
217 if shift = 0 then
220 let extended_x = w2n x * (2 ** shift) in
221 (x << shift, BIT (dimindex(:'a)) extended_x)`;
224 LSR_C (x: 'a word, shift:num) =
225 if shift = 0 then
228 (x >>> shift, BIT (shift - 1) (w2n x))`;
231 ASR_C (x: 'a word, shift:num) =
232 if shift
[all...]
/seL4-l4v-10.1.1/seL4/include/arch/x86/arch/kernel/
H A Dtlb_bitmap.h57 int shift = i * TLBBITMAP_ENTRIES_PER_ROOT;
58 bitmap |= entry << shift;
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/
H A DoptScript.sml49 (shift skip (Lit l) = Lit l) ���
50 (shift skip (Var n) =
55 (shift skip (Fun e) = Fun (shift (skip + 1) e)) ���
56 (shift skip (App e1 e2) = App (shift skip e1) (shift skip e2)) ���
57 (shift skip (Tick e) = Tick (shift skip e))`;
68 (subst skip e2 (Fun e1) = Fun (subst (skip + 1) (shift
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A DInterval.sml20 fun int_cat w shift i =
21 let val shiftw = Word.fromInt shift
23 val x = clear_top_bits shift i
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/
H A Dtext.scala184 def can_edit(string: String, shift: Offset): Boolean =
185 shift <= start && start < shift + string.length
187 def edit(string: String, shift: Offset): (Option[Edit], String) =
188 if (!can_edit(string, shift)) (Some(this), string)
189 else if (is_insert) (None, insert(start - shift, string))
191 val i = start - shift
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/
H A Dtext.scala184 def can_edit(string: String, shift: Offset): Boolean =
185 shift <= start && start < shift + string.length
187 def edit(string: String, shift: Offset): (Option[Edit], String) =
188 if (!can_edit(string, shift)) (Some(this), string)
189 else if (is_insert) (None, insert(start - shift, string))
191 val i = start - shift
/seL4-l4v-10.1.1/HOL4/examples/misc/
H A DcontMonadScript.sml75 shift f = Cont (runC o f)
81 (a,b) <- reset (do x <- shift (��k. return (3,4));
97 n <- reset (do x <- shift (��k. return (k (k 10))) ;
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/
H A DData.sml3 datatype shift = LSL | LSR | ASR | ROR; type
18 | DpShiftImmediate of {Imm : int, Rm : vregister, Sh : shift}
19 | DpShiftRegister of {Rm : vregister, Rs : vregister, Sh : shift};
23 | DtShiftImmediate of {Imm : int, Rm : vregister, Sh : shift};
H A DinstructionScript.sml21 shift =
30 | Dp_shift_immediate of shift=>word5
31 | Dp_shift_register of shift=>word4`;
36 | Dt_shift_immediate of shift=>word5`;
113 | Dp_shift_immediate shift amount => w2w amount << 7 || shift_encode shift
114 | Dp_shift_register shift Rs => 0x10w || w2w Rs << 8 || shift_encode shift`;
120 | Dt_shift_immediate shift amount =>
121 0x2000000w || w2w amount << 7 || shift_encode shift`;
[all...]
H A DarmScript.sml294 SHIFT_IMMEDIATE2 shift (sh:word2) rm c =
296 0w => LSL rm shift c
297 | 1w => LSR rm (if shift = 0w then 32w else shift) c
298 | 2w => ASR rm (if shift = 0w then 32w else shift) c
299 | _ => if shift = 0w then word_rrx (c,rm) else ROR rm shift c`;
302 SHIFT_REGISTER2 shift (sh:word2) rm c =
304 0w => LSL rm shift
314 and shift = (11 >< 7) opnd2 value
324 and shift = (7 >< 0) (REG_READ reg mode Rs) in value
[all...]
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dcoreutils.sml158 (* shifts: compute the core sets that result from shift/gotoing on
164 (2) then add the shift/gotos on kernal items.
166 We can do (1) the following way. Keep a table which for each shift/goto
170 item list in sorted order for each possible shift symbol. Scan the nonterminal
171 list from back to front. For each nonterminal, prepend the shift/goto list
172 for each shift symbol to the list already in the table.
174 We end up with the list of items in correct order for each shift/goto
182 (* mergeShiftItems: add an item list for a shift/goto symbol to the table *)
190 kept these items sorted by their shift/goto symbol (the first symbol on
201 (* now create a table which for each shift/got
[all...]
/seL4-l4v-10.1.1/seL4/libsel4/tools/
H A Dbitfield_gen.py259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
272 """%(r_shift_op)s %(shift)d;
284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
297 """%(shift)d) & 0x%(mask)x;
327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
344 """%(r_shift_op)s %(shift)d;
358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)
[all...]
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/
H A Dbitfield_gen.py259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
272 """%(r_shift_op)s %(shift)d;
284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
297 """%(shift)d) & 0x%(mask)x;
327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
344 """%(r_shift_op)s %(shift)d;
358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)
[all...]
/seL4-l4v-10.1.1/seL4/tools/
H A Dbitfield_gen.py259 ret = (%(block)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
272 """%(r_shift_op)s %(shift)d;
284 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
286 %(block)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)d) & 0x%(mask)x%(suf)s;
294 %(assert)s((((~0x%(mask)x %(r_shift_op)s %(shift)d) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
297 """%(shift)d) & 0x%(mask)x;
327 ret = (%(union)s.words[%(index)d] & 0x%(mask)x%(suf)s) %(r_shift_op)s %(shift)d;
344 """%(r_shift_op)s %(shift)d;
358 %(assert)s((((~0x%(mask)x%(suf)s %(r_shift_op)s %(shift)d ) | 0x%(high_bits)x) & v%(base)d) == ((%(sign_extend)d && (v%(base)d & (1%(suf)s << (%(extend_bit)d)))) ? 0x%(high_bits)x : 0));
361 %(union)s.words[%(index)d] |= (v%(base)d %(w_shift_op)s %(shift)
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/tile/
H A Dffi.c237 /* Find the smallest shift count that doesn't lose information
243 #define OPS(a, b, shift) \
244 (create_Imm16_X0((a) >> (shift)) | create_Imm16_X1((b) >> (shift)))
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dmemmgr.cpp938 const unsigned shift = (sizeof(void*)-1) * 8; // Takes the high-order byte local
939 uintptr_t r = startS >> shift;
941 const uintptr_t s = endS == 0 ? 256 : endS >> shift;
949 if ((r << shift) != startS)
962 if ((s << shift) != endS)
977 const unsigned shift = (sizeof(void*)-1) * 8;
978 uintptr_t r = startS >> shift;
979 const uintptr_t s = endS == 0 ? 256 : endS >> shift;
986 if ((r << shift) != startS)
999 if ((s << shift) !
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DWord8.sml67 (* Arithmetic shift - sign extends. *)
69 arithmetic shift for Word because the sign bit is in a different
72 shift right down again. *)
89 (* TODO: This could be implemented using shifts. i.e logical shift
90 left by (Word.wordSize-Word8.wordSize) then arithmetic shift
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Dsyntax_style.scala45 def shift(y: Float): Font =
52 if (a > 0.0f) shift(a)
53 else if (b > 0.0f) shift(- b)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dsyntax_style.scala45 def shift(y: Float): Font =
52 if (a > 0.0f) shift(a)
53 else if (b > 0.0f) shift(- b)
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DarmScript.sml248 SHIFT_IMMEDIATE2 shift (sh:word2) rm c =
249 if shift = 0w then
255 if sh = 0w then LSL rm shift c else
256 if sh = 1w then LSR rm shift c else
257 if sh = 2w then ASR rm shift c else
258 (* sh = 3w *) ROR rm shift c`;
261 SHIFT_REGISTER2 shift (sh:word2) rm c =
262 if sh = 0w then LSL rm shift c else
263 if sh = 1w then LSR rm shift c else
264 if sh = 2w then ASR rm shift
272 and shift = (11 >< 7) opnd2 value
282 and shift = (7 >< 0) (REG_READ reg mode Rs) in value
[all...]

Completed in 303 milliseconds

12345