/seL4-l4v-master/seL4/src/arch/x86/ |
H A D | c_traps.c | 49 ksKernelEntry.word = irq; 56 ksKernelEntry.word = type; 64 ksKernelEntry.word = NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[FaultIP]; 71 ksKernelEntry.word = irq; 78 ksKernelEntry.word = irq; 95 ksKernelEntry.word = sys_num; 127 /* ksKernelEntry.word word is already set to syscall */
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | alignmentScript.sml | 17 val align_def = Define `align p (w: 'a word) = (dimindex (:'a) - 1 '' p) w` 21 byte_align (w: 'a word) = align (LOG2 (dimindex(:'a) DIV 8)) w` 24 byte_aligned (w: 'a word) = aligned (LOG2 (dimindex(:'a) DIV 8)) w` 89 `(p - 1 >< 0) w : 'a word = (dimindex (:'a) - 1 >< 0) w` 104 !p w. aligned p (w: 'a word) <=> (p = 0) \/ ((p - 1 >< 0) w = 0w: 'a word) 130 `!p w:'a word. dimindex(:'a) <= p ==> (aligned p w = (w = 0w))`, 135 `!p w. aligned p (w: 'a word) = (w && n2w (2 ** p - 1) = 0w)`, 150 aligned p (w: 'a word) = (bit_count_upto (MIN (dimindex(:'a)) p) w = 0)`, 165 `!p a: 'a word [all...] |
H A D | blastScript.sml | 190 (BCARRY n ($' (n2w x :'a word)) ($~ o $' (n2w y :'a word)) c = 200 (BSUM n ($' (n2w x :'a word)) ($' (n2w y :'a word)) c = 284 !x y:'a word. x <+ y <=> ~BCARRY (dimindex (:'a)) ($' x) ((~) o ($' y)) T 303 `!n w m : 'a word. 330 ``(a + b = b + c) = (a = c : 'a word)``)] 345 `!w m : 'a word. 353 `!w m : 'a word. 406 `!h w P a:'a word [all...] |
H A D | blastLib.sml | 193 (``words$word_mod:'a word -> 'a word -> 'a word``, 2, 451 fcp_eq_thm : generates a bitwise equality theorem for a given word type. 458 ���!a b:'a word. 521 (SPECL [���w: 'a word���, ���arithmetic$NUMERAL a���] WORD_MUL_LSL)) 570 SPECL [���a: 'a words$word���, ���n2w (NUMERAL n) : 'a word���] 612 ���!l h n w:'a word. 618 ���!l h n w:'a word [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | IntInf.sml | 29 val << : int * Word.word -> int 30 val ~>> : int * Word.word -> int 54 fun loadByte(l: LargeInt.int, i: Int.int):word = RunCall.loadByteFromImmutable(l, Word.fromInt i) 60 fun log2Word(i: word, j: word, n: Int.int) = 135 fun << (i: int, j: Word.word) = 141 fun ~>> (i: int, j: Word.word) = LargeInt.div(i, pow(2, Word.toInt j))
|
H A D | PackRealBig.sml | 37 val realSizeCall: unit -> word = RunCall.rtsCallFast1 "PolyRealSize" 39 val realSize: word = realSizeCall () 43 val System_move_bytes: address*address*word*word*word->unit = RunCall.moveBytes 46 fun swapOrder(src: address, srcOff: word, 47 dest: address, destOff: word, 48 length: word) = 56 fun doMove(src: address, srcOff: word, 57 dest: address, destOff: word, wantBigEndia [all...] |
H A D | VectorSliceOperations.sml | 27 val vecLength: vector -> word 28 val unsafeVecSub: vector * word -> elem 29 val unsafeVecUpdate: vector * word * elem -> unit (* Array only *) 33 datatype slice = Slice of { vector: vector, start: word, length: word }; 62 val wordAsInt: word -> int = RunCall.unsafeCast 66 datatype slice = Slice of { vector: vector, start: word, length: word }; 72 (* Check that the value is non-negative and short and cast it to word. *) 83 (* Check that the value is non-negative and short and cast it to word [all...] |
H A D | PackWord8Big.sml | 27 val subVec : Word8Vector.vector * int -> LargeWord.word 28 val subVecX : Word8Vector.vector * int -> LargeWord.word 29 val subArr : Word8Array.array * int -> LargeWord.word 30 val subArrX : Word8Array.array * int -> LargeWord.word 31 val update : Word8Array.array * int * LargeWord.word -> unit 62 fun twoBytesToWord(hi: Word8.word, lo: Word8.word) = 65 fun twoBytesToWordX(hi: Word8.word, lo: Word8.word) =
|
H A D | BIT_FLAGS.sml | 26 val toWord : flags -> SysWord.word 27 val fromWord : SysWord.word -> flags
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/cheri/step/ |
H A D | cheri_stepScript.sml | 157 (d1 @@ d2 @@ d3 @@ (d4 && ~mask || data && mask)) : 256 word`, 165 (d1 @@ d2 @@ (d3 && ~mask || data && mask) @@ d4) : 256 word`, 173 (d1 @@ (d2 && ~mask || data && mask) @@ d3 @@ d4) : 256 word`, 181 ((d1 && ~mask || data && mask) @@ d2 @@ d3 @@ d4) : 256 word`, 247 ``(h >< l) : 'a word -> 'b word``, 248 ``(=):'a word -> 'a word -> bool``, 249 ``word_bit n: 'a word -> bool``]]) 252 [extract_conv ``(1 >< 0) ((39 >< 3) (vaddr: word64) : 37 word) [all...] |
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patricia_castsScript.sml | 3 (* DESCRIPTION : Support for maps 'a word |-> 'b and string |-> 'a *) 75 PEEKw (t:('a,'b) word_ptree) (w:'a word) = PEEK (THE_PTREE t) (w2n w)`; 80 ADDw (t:('a,'b) word_ptree) (w:'a word,d) = 86 REMOVEw (t:('a,'b) word_ptree) (w:'a word) = 96 MAP (n2w:num->'a word) (TRAVERSE (THE_PTREE t))`; 106 EVERY_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)`; 110 EXISTS_LEAF (\k d. P (n2w k : 'a word) d) (THE_PTREE t)`; 116 `$IN_PTREEw (w:'a word) (t:('a,unit) word_ptree) = 120 `$INSERT_PTREEw (w:'a word) (t:('a,unit) word_ptree) = 131 PTREE_OF_WORDSET (t:('a, unit) word_ptree) (s:'a word se [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v4/mlton/ |
H A D | updateML.sml | 161 fun MEM_WRITE_BYTE mem addr word = 168 addr) word (mem_read (mem,a30))) 171 fun MEM_WRITE_HALF mem addr word = 175 (SET_HALF (word_index addr ONE) word 179 fun MEM_WRITE_WORD mem addr word = mem_write mem (addr30 addr) word
|
/seL4-l4v-master/seL4/src/arch/x86/64/ |
H A D | head.S | 302 .word (3 * 8) - 1 308 .word 0 309 .word 0 314 .word 0 315 .word 0 395 .word (3 * 8) - 1 /* Limit: 3 segments * 8 bytes - 1 byte */
|
/seL4-l4v-master/HOL4/examples/dev/booth/ |
H A D | boothDevScript.sml | 61 val _ = type_abbrev("word",``:word32``); 78 (``\(sw:bool,in1:word,in2:word). if sw then in1 else in2``, 84 (``(UNCURRY ($+ :word->word->word))``,(fn[inp1,inp2] => inp1 ^ " + " ^ inp2)), 87 (``(UNCURRY ($<< :word->num->word))``,(fn[inp1,inp2] => inp1 ^ " << " ^ inp2)), 88 (``(UNCURRY ($- :word->word [all...] |
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Library.sml | 278 (* A tactic that simplifies certain word expressions. *) 281 `(!w : 'a word. 283 (w2w w : 'b word = (dimindex(:'b) - 1 >< 0) w)) /\ 284 (!w : 'a word. 286 (sw2sw w : 'b word = (dimindex(:'b) - 1 >< 0) w))`, 292 ``!w:'a word i. i < dimindex (:'a) ==> (w ' i = ((i >< i) w = 1w:word1))`` 296 ``(!w:'a word n. n < dimword (:'a) ==> (w << n = w <<~ n2w n)) /\ 297 (!w:'a word n. n < dimword (:'a) ==> (w >> n = w >>~ n2w n)) /\ 298 (!w:'a word n. n < dimword (:'a) ==> (w >>> n = w >>>~ n2w n))``
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | arm_emitScript.sml | 113 i2bits_itself (i,N,(:'a)) = (i2bits (i,N)) : 'a word`; 116 signed_sat_itself (i,N,(:'a)) = (signed_sat (i,N)) : 'a word`; 119 unsigned_sat_itself (i,N,(:'a)) = (unsigned_sat (i,N)) : 'a word`; 122 signed_sat_q_itself (i,N,(:'a)) = (signed_sat_q (i,N)) : 'a word # bool`; 125 unsigned_sat_q_itself (i,N,(:'a)) = (unsigned_sat_q (i,N)) : 'a word # bool`; 154 MLSIG ("type word" ^ s ^ " = wordsML.word" ^ s) 166 MLSIG "type 'a word = 'a wordsML.word",
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | PRETTYSIG.sml | 67 val tagPrettyBlock: word 68 and tagPrettyBreak: word 69 and tagPrettyString: word 71 val maxPrettyTag: word
|
H A D | DATATYPEREPSIG.sml | 35 val EnumForm: { tag: word, maxTag: word } -> representations;
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | signedintScript.sml | 231 ``!a. BIT (dimindex (:'a) - 1) (w2n (a:'a word)) = 299 (* sw2i x : Convert the word x to a signed integer *) 300 (* i2sw x : Convert the integer x to a word *) 314 val sw2i_def = Define `sw2i (x:'a word) = 323 else n2w (Num m):'b word`; 706 ``sw2i (x:'a word) = extend (& (w2n x)) (dimindex (:'a))``, 715 (REWRITE_RULE [GSYM sw2i_thm] (Q.SPEC `& (w2n (a:'a word))` 734 (* sw2i_i2sw : |- !x. sw2i ((i2sw x) : 'a word) = extend x (dimindex (:'a)) *) 737 val rwr1 = prove(``& (w2n (x:'a word)) - & (2 ** dimindex (:'a)):int = 743 ~ & (dimword (:'a) - w2n (x:'a word) [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | addressScript.sml | 34 ``!v w. (v ?? w = 0w) = (v = w:'a word)``, 60 ``!n. (n2w n) && 1w = n2w (n MOD 2):'a word``, 67 ``!n. (n2w n) && 3w = n2w (n MOD 4):'a word``, 74 ``!n. (n2w n) && 7w = n2w (n MOD 8):'a word``, 316 ``!n m. (n2w n + n2w m = n2w (n + m):'a word) /\ 317 (x + n2w n + n2w m = x + n2w (n + m):'a word) /\ 318 (x - n2w n - n2w m = x - n2w (n + m):'a word)``, 322 ``!n m. n2w n - (n2w m) :'a word = 334 ``!x n m. x - n2w m + n2w n :'a word = if n < m then x - (n2w (m-n)) else x + n2w (n-m)``, 340 ``!x n m. x + n2w n - n2w m :'a word [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86CODESIG.sml | 28 datatype genReg = GeneralReg of Word8.word * bool 29 and fpReg = FloatingPtReg of Word8.word 30 and xmmReg = SSE2Reg of Word8.word 132 | ArithByteMemConst of { opc: arithOp, address: memoryAddress, source: Word8.word } 133 | ShiftConstant of { shiftType: shiftType, output: genReg, shift: Word8.word, opSize: opSize } 138 | TestByteBits of { arg: genReg regOrMemoryArg, bits: Word8.word } 178 | XMMShiftRight of { output: xmmReg, shift: Word8.word } 179 | FPLoadCtrlWord of memoryAddress (* Load FP control word. *) 180 | FPStoreCtrlWord of memoryAddress (* Store FP control word. *) 181 | XMMLoadCSR of memoryAddress (* Load combined control/status word [all...] |
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | MD5.sml | 24 type word64 = {hi:W32.word,lo:W32.word} 25 type word128 = {A:W32.word, B:W32.word, C:W32.word, D:W32.word} 227 datatype bstate = B0 | B2 of Word8.word | B4 of Word8.word;
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 4 Simple generator for pseudo-random numbers, using unboxed word 16 orelse raise Fail ("Bad platform word size");
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 4 Simple generator for pseudo-random numbers, using unboxed word 16 orelse raise Fail ("Bad platform word size");
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCodeSig.sml | 65 firstIndex: word 88 | BICTagTest of { test: backendIC, tag: word, maxTag: word } 108 | CaseTag of word 117 LoadStoreMLWord of {isImmutable: bool} (* Load/Store an ML word in an ML word cell. *) 119 | LoadStoreC8 (* Load/Store C values - The base address is a boxed SysWord.word value. *) 151 address if this is to/from ML memory or a (boxed) SysWord.word if it is
|