Searched refs:word (Results 51 - 75 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/seL4/src/arch/x86/
H A Dc_traps.c49 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 DalignmentScript.sml17 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 DblastScript.sml190 (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 DblastLib.sml193 (``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 DIntInf.sml29 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 DPackRealBig.sml37 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 DVectorSliceOperations.sml27 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 DPackWord8Big.sml27 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 DBIT_FLAGS.sml26 val toWord : flags -> SysWord.word
27 val fromWord : SysWord.word -> flags
/seL4-l4v-master/HOL4/examples/l3-machine-code/cheri/step/
H A Dcheri_stepScript.sml157 (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 Dpatricia_castsScript.sml3 (* 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 DupdateML.sml161 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 Dhead.S302 .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 DboothDevScript.sml61 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 DLibrary.sml278 (* 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 Darm_emitScript.sml113 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 DPRETTYSIG.sml67 val tagPrettyBlock: word
68 and tagPrettyBreak: word
69 and tagPrettyString: word
71 val maxPrettyTag: word
H A DDATATYPEREPSIG.sml35 val EnumForm: { tag: word, maxTag: word } -> representations;
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DsignedintScript.sml231 ``!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 DaddressScript.sml34 ``!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 DX86CODESIG.sml28 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 DMD5.sml24 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 DRandom.sml4 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 DRandom.sml4 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 DBackendIntermediateCodeSig.sml65 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

Completed in 154 milliseconds

1234567891011>>