/seL4-l4v-master/seL4/tools/hardware/utils/ |
H A D | __init__.py | 8 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 D | braces.py | 28 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 D | pars_skl.py | 52 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 D | lhs_pars.py | 63 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 D | objdump.py | 16 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 D | syntax.py | 151 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 D | inst_logic.py | 31 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 D | loop_bounds.py | 379 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 D | solver.py | 71 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 D | Word64.sml | 1 (* Only built if LargeWord is 64-bits *)
|
/seL4-l4v-master/seL4/include/arch/arm/arch/ |
H A D | machine.h | 50 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 D | fastpath.h | 14 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 D | decoderScript.sml | 50 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 D | microcode.ml | 47 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 D | prob_pseudoScript.sml | 15 (* Theorems to allow pseudo-random bits to be computed. *)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0.sml | 517 {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 D | boot.h | 130 * 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 D | x64.sml | 770 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 D | BoolArray.sml | 22 (* 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 D | mips.sml | 1709 {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 D | GdiBase.sml | 58 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 D | deprecated.h | 125 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 D | arm.sml | 1771 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 D | bitmap.h | 33 // 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 D | UTF8.sml | 22 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 *)
|