Searched refs:bits (Results 1 - 25 of 170) sorted by relevance

1234567

/seL4-l4v-master/seL4/tools/hardware/utils/
H A D__init__.py8 def align_up(num, bits):
10 boundary = 1 << bits
14 def align_down(num, bits):
16 boundary = 1 << bits
/seL4-l4v-master/l4v/tools/haskell-translator/
H A Dbraces.py28 def __init__(self, s, l, r, bits=None):
29 if bits is None:
30 bits = self._get_bits(s, l, r)
31 self.bits = bits
38 bits = ['']
42 if bits[-1]:
43 bits.append('')
45 bits[-1] = bits[
[all...]
H A Dpars_skl.py52 bits = line.split() variable
54 call.filename = find_source(bits[1])
55 call.all_bits = 'all_bits' in bits
56 call.decls_only = 'decls_only' in bits
57 call.instanceproofs = 'instanceproofs' in bits
58 call.bodies_only = 'bodies_only' in bits
60 for bit in bits if '=' in bit])
62 if 'CONTEXT' in bits:
63 n = bits.index('CONTEXT')
64 call.current_context.append(bits[
[all...]
H A Dlhs_pars.py63 bits = l.split(',')
64 for bit in bits:
482 bits = string.split('=>', 1)
483 if len(bits) == 2:
484 lhs = bits[0].strip()
487 string = ' => '.join(instances + [bits[1]])
502 transformed = type_transform(bits[1])
517 bits = bstring.split('->')
519 if len(bits) == 1:
520 bits
[all...]
/seL4-l4v-master/graph-refine/
H A Dobjdump.py16 bits = line.split ()
18 addr = int (bits[0], 16)
19 size = int (bits[-2], 16)
20 section = bits[-3]
21 syms[bits[-1]] = (addr, size, section)
78 bits = line.split ()
79 (addr, v) = (int (bits[0][:-1], 16), int (bits[1], 16))
114 bits = lname.split ()
115 assert bits[
[all...]
H A Dsyntax.py151 These types encode a machine word with the given number of bits, an array of
417 bits = [repr(self.kind), repr(self.typ)]
418 bits.extend(['%s = %r' % b for b in self.binds()])
419 return 'Expr (%s)' % ', '.join(bits)
918 def parse_typ(bits, n, symbolic_types = False):
919 if bits[n] == 'Word' or bits[n] == 'BitVec':
920 return (n + 2, Type('Word', parse_int (bits[n + 1])))
921 elif bits[n] == 'WordArray' or bits[
[all...]
H A Dinst_logic.py31 bits = inst_split_re.split (nm)
34 if len (bits) > 1 and pn_re.match (bits[1]):
35 bits[1] = bits[1][1:]
36 for bit in bits:
113 bits = instname.split('_')
114 assert bits, instname
115 addr = bits[-1]
118 return ('_'.join (bits[
[all...]
H A Dloop_bounds.py379 def parse_ctxt_id (bits, n):
380 return (n + 1, syntax.parse_int (bits[n]))
382 def parse_ctxt (bits, n):
383 return syntax.parse_list (parse_ctxt_id, bits, n)
394 bits = l.split ()
395 if bits[:1] not in [['LoopBound'], ['GlobalLoopBound']]:
397 (n, (addr, bound)) = parse_bound (bits, 1)
398 (n, ctxt) = parse_ctxt (bits, n)
399 prob_hash = parse_int (bits[n])
401 if bits[
[all...]
H A Dsolver.py71 def parse_solver (bits):
75 if len (bits) < 3 or bits[1].lower () not in mode_set:
78 print ' reading %r' % bits
81 name = bits[0]
82 fast = (bits[1].lower () in ['fast', 'online'])
83 args = bits[2].split ()
84 assert os.path.exists (args[0]), (args[0], bits)
114 bits = [bit.strip () for bit in line.split (':', 2)]
115 if bits[
[all...]
/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/
H A DWord64.sml1 (* Only built if LargeWord is 64-bits *)
/seL4-l4v-master/seL4/include/arch/arm/arch/
H A Dmachine.h50 static inline void clearMemory(word_t *ptr, word_t bits) argument
52 memzero(ptr, BIT(bits));
53 cleanCacheRange_PoU((word_t)ptr, (word_t)ptr + BIT(bits) - 1,
57 static inline void clearMemoryRAM(word_t *ptr, word_t bits) argument
59 memzero(ptr, BIT(bits));
60 cleanCacheRange_RAM((word_t)ptr, (word_t)ptr + BIT(bits) - 1,
/seL4-l4v-master/seL4/include/fastpath/
H A Dfastpath.h14 word_t guardBits, radixBits, bits; local
17 bits = 0;
26 cptr2 = cptr << bits;
42 bits += guardBits + radixBits;
44 } while (unlikely(bits < wordBits && cap_capType_equals(cap, cap_cnode_cap)));
46 if (unlikely(bits > wordBits)) {
47 /* Depth mismatch. We've overshot wordBits bits. The lookup we've done is
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/common/
H A DdecoderScript.sml50 assign name x (g:string->bool list, bits:bool list) = SOME ((name =+ x) g,bits)`;
53 assign_drop name i (g:string->bool list, bits:bool list) =
54 if LENGTH bits < i then NONE else SOME ((name =+ TAKE i bits) g, DROP i bits)`;
57 drop_eq v (g:string->bool list, bits:bool list) =
59 if LENGTH bits < i \/ ~(v = TAKE i bits) then NONE else SOME (g, DROP i bits)`;
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/
H A Dmicrocode.ml47 mk_ADDR [b4;b3;b2;b1;b0] n gives a list of the positions of bits that
61 mk_A_ADDR n gives a list of the positions of bits in the A-address
64 mk_B_ADDR n gives a list of the positions of bits in the B-address
72 test_button(n,m) gives a list of the bits that are 1 if the address of the
80 test_acc(n,m) gives a list of the bits that are 1 if the address of the
88 jump n gives a list of the bits that are 1 if the address of the
95 jump_knob n gives a list of the bits that are 1 if the address of the
103 jump_opcode n gives a list of the bits that are 1 if the address of the
113 mk_micro_ins l takes a list of numbers representing the positions of bits
116 appropriate bits o
[all...]
/seL4-l4v-master/HOL4/examples/miller/prob/
H A Dprob_pseudoScript.sml15 (* Theorems to allow pseudo-random bits to be computed. *)
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/
H A Dm0.sml517 {PM = BitsN.bit(x,0), primask'rst = BitsN.bits(31,1) x};
529 {C = BitsN.bit(x,29), ExceptionNumber = BitsN.bits(5,0) x,
532 psr'rst = BitsN.@@(BitsN.bits(23,6) x,BitsN.bits(27,25) x)};
540 BitsN.bits(2,0) psr'rst,BitsN.fromBit T,
541 BitsN.bits(20,3) psr'rst,ExceptionNumber];
564 VECTCLRACTIVE = BitsN.bit(x,1), VECTKEY = BitsN.bits(31,16) x,
565 aircr'rst = BitsN.@@(BitsN.bits(0,0) x,BitsN.bits(14,3) x)};
573 [VECTKEY,BitsN.fromBit ENDIANNESS,BitsN.bits(1
[all...]
/seL4-l4v-master/seL4/include/kernel/
H A Dboot.h130 * the paging structure covering `bits` of the address range - for a 4k page
131 * `bits` would be 12 */
132 static inline BOOT_CODE word_t get_n_paging(v_region_t v_reg, word_t bits) argument
134 vptr_t start = ROUND_DOWN(v_reg.start, bits);
135 vptr_t end = ROUND_UP(v_reg.end, bits);
136 return (end - start) / BIT(bits);
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/
H A Dx64.sml770 PM = BitsN.bit(x,12), RC = BitsN.bits(14,13) x,
771 Reserved = BitsN.bits(31,16) x, UE = BitsN.bit(x,4),
797 ( write'mem8(BitsN.bits(7,0) w,addr)
801 write'mem8(BitsN.bits(15,8) w,x)
809 ( write'mem16(BitsN.bits(15,0) w,addr)
813 write'mem16(BitsN.bits(31,16) w,x)
821 ( write'mem32(BitsN.bits(31,0) w,addr)
825 write'mem32(BitsN.bits(63,32) w,x)
833 ( write'mem64(BitsN.bits(63,0) w,addr)
837 write'mem64(BitsN.bits(12
[all...]
/seL4-l4v-master/HOL4/polyml/basis/
H A DBoolArray.sml22 (* TODO: Use a single word for vectors of size <= number of bits in a word. *)
23 (* We use int here for the length rather than word because the number of bits
43 fun alloc (bits: int) =
46 if bits < 0 orelse bits > maxLen
48 else (Word.fromInt bits + (bitsPerWord - 0w1)) div bitsPerWord
55 (* We will only set the bits that we actually use. Unused bytes will be uninitialised.
106 (* Accumulate the bits into bytes and store into the array. *)
137 (* Move a set of bits from one vector of bytes to another. The bits
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/mips/model/
H A Dmips.sml1709 {Index = BitsN.bits(7,0) x, P = BitsN.bit(x,31),
1710 index'rst = BitsN.bits(30,8) x};
1722 {Random = BitsN.bits(7,0) x, random'rst = BitsN.bits(31,8) x};
1734 {Wired = BitsN.bits(7,0) x, wired'rst = BitsN.bits(31,8) x};
1745 {C = BitsN.bits(5,3) x, D = BitsN.bit(x,2), G = BitsN.bit(x,0),
1746 PFN = BitsN.bits(33,6) x, V = BitsN.bit(x,1),
1747 entrylo'rst = BitsN.bits(63,34) x};
1761 {Mask = BitsN.bits(2
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DGdiBase.sml58 bits: Word8Vector.vector option }
64 fun storeBmp(v: voidStar, {width, height, widthBytes, planes, bitsPerPixel, bits}: BITMAP) =
66 val m = case bits of NONE => Memory.null | SOME b => toCWord8vec b
74 val (_, width, height, widthBytes, planes, bitsPerPixel, bits) =
76 val bits = value
77 if bits = Memory.null
79 else SOME (fromCWord8vec (bits, height * widthBytes))
82 bitsPerPixel = bitsPerPixel, bits = bits}
/seL4-l4v-master/seL4/libsel4/include/sel4/
H A Ddeprecated.h125 seL4_Word bits)
127 return seL4_CNode_CapData_new(guard, bits).words[0];
124 seL4_CapData_Guard_new(seL4_Word guard, seL4_Word bits) argument
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/
H A Darm.sml1771 F = BitsN.bit(x,6), GE = BitsN.bits(19,16) x, I = BitsN.bit(x,7),
1772 IT = BitsN.@@(BitsN.bits(15,10) x,BitsN.bits(26,25) x),
1773 J = BitsN.bit(x,24), M = BitsN.bits(4,0) x, N = BitsN.bit(x,31),
1775 Z = BitsN.bit(x,30), psr'rst = BitsN.bits(23,20) x};
1783 BitsN.fromBit Q,BitsN.bits(1,0) IT,BitsN.fromBit J,psr'rst,GE,
1784 BitsN.bits(7,2) IT,BitsN.fromBit E,BitsN.fromBit A,
1800 [BitsN.bits(6,3) x,BitsN.bits(9,8) x,BitsN.bits(1
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dbitmap.h33 // Allocate the bitmap bits
34 bool Create(size_t bits);
36 // Free the bitmap bits.
48 // Set a range of bits
50 // Clear a range of bits.
54 // How many zero bits (maximum n) are there in the bitmap, starting at location start?
58 // How many set bits are there in the bitmap?
/seL4-l4v-master/HOL4/src/portableML/
H A DUTF8.sml22 val byte3 = 128 + Word.toInt (Word.andb(w, 0wx3F)) (* 3F = 6 bits *)
24 val byte2 = 128 + Word.toInt (Word.andb(w, 0wx3F)) (* 3F = 6 bits *)
27 (* inital E says there are 3 bytes, and with F to extract 4 bits *)
33 val byte4 = 128 + Word.toInt (Word.andb(w, 0wx3F)) (* 3F = 6 bits *)
35 val byte3 = 128 + Word.toInt (Word.andb(w, 0wx3F)) (* 3F = 6 bits *)
37 val byte2 = 128 + Word.toInt (Word.andb(w, 0wx3F)) (* 3F = 6 bits *)
40 (* inital F says there are 4 bytes, and with 7 to extract 3 bits *)

Completed in 450 milliseconds

1234567