Searched refs:r7 (Results 1 - 25 of 57) sorted by relevance

123

/seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/
H A Dtypes.h21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/
H A Dtypes.h21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_equalScript.sml14 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
22 arm_eq_loop (r3:word32,r4:word32,r5:word32,r6:word32,r7:word32,r8:word32,df:word32 set,f:word32->word32) =
25 (r3,r4,r5,r6,r7,r8,df,f)
27 let r4 = f (r7 - 0x4w) in
28 let r7 = r7 - 0x4w in
29 let r3 = f (r7 - 0x4w) in
30 let r7 = r7 - 0x4w in
32 arm_eq_loop (r3,r4,r5,r6,r7,r
[all...]
H A Dlisp_printScript.sml61 arm_string_rev(r3:word32,r6,r7,df:word32 set,f:word32->word8) =
62 if r3 = 0w then (r7,df,f) else
64 let r5 = (w2w (f r7)):word32 in
66 let f = (r7 =+ w2w r4) f in
68 let r7 = r7 + 1w in
70 arm_string_rev(r3,r6,r7,df,f)``
73 arm_string_reverse1(r6,r7,df:word32 set,f:word32->word8) =
74 let r3 = r7 - r6 in
78 let r7
[all...]
H A Dlisp_parseScript.sml219 let r7 = r5:word32 in
221 let r8 = r5 - r7 in
222 (r4,r5,r7,r8,df,f)``
276 arm_streq (r4:word32,r5:word32,r6:word32,r7:word32,df:word32 set,dg:word32 set,f:word32->word8,g:word32->word8) =
277 if r7 = 0x0w then
278 (let r5 = r7 + r5 in (r4,r5,r6,r7,df,dg,f,g))
283 (let r7 = r7 - 0x1w in
285 arm_streq (r4,r5,r6,r7,d
[all...]
H A Dlisp_finalScript.sml164 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9"]
211 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
253 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`]
264 THEN EX_TAC [`r4`,`r5`,`r6`,`r7`,`r8`]
272 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
314 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`]
325 THEN EX_TAC [`r4`,`r5`,`r6`,`r7`,`r8`]
422 val imp = Q.INST [`r7`|->`r1`,`rest`|->`(dm,m,dg,g)`] imp
476 THEN EX_TAC [`r3`,`r4`,`r5`,`r6`,`r7`,`r8`,`a`]
486 THEN EX_TAC [`r7`]
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/compiler/demo/
H A Dcompiler_demoScript.sml111 arm_string_rev(r3:word32,r6,r7,df:word32 set,f:word32->word8) =
112 if r3 = 0w then (r7,df,f) else
114 let r5 = (w2w (f r7)):word32 in
116 let f = (r7 =+ w2w r4) f in
118 let r7 = r7 + 1w in
120 arm_string_rev(r3,r6,r7,df,f)``
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Darm_cheney_gcScript.sml19 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
27 E5957000 (* ldr r7,[r5] *)
28 E3170001 (* tst r7,#1 *)
29 04847004 (* streq r7,[r4],#4 *)
31 05957008 (* ldreq r7,[r5,#8] *)
33 04847004 (* streq r7,[r4],#4 *)
34 0244700B (* subeq r7,r4,#11 *)
35 05857000 (* streq r7,[r5] *)
36 E2475001 (* sub r5,r7,#1 *)`;
41 E5967000 (* ldr r7,[r
[all...]
H A Dlisp_gcScript.sml16 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
26 E5957000 (* ldr r7,[r5] *)
27 E2078003 (* and r8,r7,#3 *)
30 14847004 (* strne r7,[r4],#4 *)
32 12447007 (* subne r7,r4,#7 *)
33 15857000 (* strne r7,[r5] *)
34 E2475001 (* sub r5,r7,#1 *)`;
39 E5967000 (* ldr r7,[r6] *)
40 E2078003 (* and r8,r7,#3 *)
43 14847004 (* strne r7,[r
[all...]
H A Darm_cheney_allocScript.sml14 val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
22 (arm_alloc_gc (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
23 (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
26 arm_alloc_gc_pre (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs)``,
35 \\ `?r3i r4i r5i r6i r7i r8i r10i xi xsi. arm_collect (r7,r8,a,x,xs) =
181 (arm_alloc_mem (r5,r6,r7,r8,a,x,xs) = (r3',r4',r5',r6',r7',r8',a',x',xs')) ==>
183 arm_alloc_mem_pre (r5,r6,r7,r8,a,x,xs)``,
194 arm_alloc_gc (ref_addr a i,ref_addr a e,r5,r6,r7,r8,a,x,xs) =
304 (arm_alloc_mem (r5,r6,r7,r
[all...]
/seL4-l4v-master/seL4/src/arch/arm/32/
H A Dhead.S73 * and we put arguments 5 and 6 (DTB address/size) in r7 and r8.
83 pop {r7, r8}
149 push {r0-r3,r7-r8}
151 pop {r0-r3,r7-r8}
162 push {r7, r8}
H A Dtraps.S89 cmp r7, #SYSCALL_CALL
91 cmp r7, #SYSCALL_REPLY_RECV
98 mov r2, r7
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DstraightlineScript.sml12 arm_assert (p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v,
22 arm_REG (R_mode mode 7w) r7 *
50 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v,
52 (pre,p,r0,r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14,n,z,c,v,
H A Dstack_introLib.sml33 val ((th,_,_),_) = f "e1370006" (* teq r7, r6 *)
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_core_decompScript.sml20 (* r7 *) word32 =>
45 (ARM_ASSERTION mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14
55 arm_REG (R_mode mode 7w) r7 *
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_tests.sml106 "e0811007" (* add r1, r1, r7 *) ::
245 "e0874203" (* add r4, r7, r3, lsl #4 *) ::
277 "e2877209" (* add r7, r7, #-1879048192 *) ::
278 "e2877001" (* add r7, r7, #1 *) ::
279 "e2877004" (* add r7, r7, #4 *) ::
280 "e0877018" (* add r7, r7, r
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_initScript.sml200 (SOME (``(r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``,
201 ``(r0:word64,r1:word64,r2:word64,r3:word64,r6:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,r12:word64,r13:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``))
203 mov r3,[r7+24]
204 mov r15,[r7+16]
205 mov r0,[r7+32]
206 mov r1,[r7+40]
207 mov r2,[r7+8]
208 mov r6,[r7]
209 mov r8,[r7+96]
210 mov r9,[r7
[all...]
H A Dlisp_codegenScript.sml121 (SOME (``(r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``,
122 ``(r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``))
124 mov r2,[r7-64]
201 (SOME (``(r0:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``,
202 ``(r0:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``))
204 mov r0,[r7-48]
205 mov r2,[r7-64]
208 dec QWORD [r7-56]
209 inc QWORD [r7-48]
320 (SOME (``(r2:word64,r3:word64,r7
[all...]
H A Dlisp_symbolsScript.sml189 mov r11,[r7-224]
196 mov r11,[r7-224]
216 (SOME (``(r8:word64,r9:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``,
217 ``(r0:word64,r8:word64,r9:word64,r10:word64,r11:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) `
218 4C8B9F20FFFFFF (* mov r11,[r7-224] *)
225 4C8B9F20FFFFFF (* mov r11,[r7-224] *)
491 (zPC p * zR 0x1w r1 * zR 0x7w r7 * ^IO (ior,iow,iod,ioi) io * ~zS * cond (iod = r1))
493 (let io = IO_STATS (w2n r7) io in
494 (zPC ^stats_post_pc * zR 0x1w r1 * zR 0x7w r7 * ^IO (ior,iow,iod,ioi) io * ~zS))``;
1425 (SOME (``(r7
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml667 field_exp_aux (r5:word32,r6:word32,r7:word32) =
668 if r6 = 0w then r7 else
675 field_exp_aux (r5:word32,r6:word32,r7:word32)
678 let r2 = r7 in
681 let r7 = r4 in
686 field_exp_aux (r5:word32,r6:word32,r7:word32)`;
690 let r7 = 1w in
691 let r7 = field_exp_aux (r5,r6,r7) in
692 r7`;
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/test/
H A Dtea.sml252 let r7 = ShiftXor (r1,r6,r2,r3) in
253 let r0 = r0 + r7 in
254 let r7 = ShiftXor (r0,r6,r4,r5) in
255 let r1 = r1 + r7 in
259 (\(r0,(r1,r2),(r3,r4,r5,r6),r7).
262 ((r1,r2),(r3,r4,r5,r6),r7)
265 let ((r1,r2),(r3,r4,r5,r6),r7) =
266 Round ((r1,r2),(r3,r4,r5,r6),r7)
269 Rounds (r0,(r1,r2),(r3,r4,r5,r6),r7)
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Djit_incrementalScript.sml38 r7 ebp - pointer to j map and temp memory
180 r7 ebp - unchanged (pointer to j map and temp memory)
204 x86_access_j (r5,r7:word32,dh:word32 set,h:word32->word32) =
206 let r2 = r2 + r7 in
209 (r1,r2,r5,r7,dh,h)``;
329 x86_newcode (r1:word32,r5:word32,r7:word32,df:word32 set,f:word32->word8,dg:word32 set,g:word32->word8,dh:word32 set,h:word32->word32) =
330 if ~(r1 = 0w) then (r7,df,f,dg,g,dh,h) else
332 let r6 = h (r7 - 4w) in (* pointer to start of bytecode *)
337 let r5 = h (r7 - 32w) in
340 let r3 = h (r7
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/multiword/
H A Dmc_multiwordScript.sml1222 (\(l,r7,r9,r10,r12,xs,ys,zs).
1223 if r7 = 0x0w then (let r10 = r10 + r9 in (INR (l,r10,xs,ys,zs),T))
1225 (let r7 = r7 - 0x1w in
1235 (INL (l-1,r7,r9,r10,r12,xs,ys,zs),cond /\ l <> 0)))
1281 let r7 = r1 in
1282 let r7 = r7 >>> 1 in
1287 let cond = cond /\ mc_mul_pre (l-1,r7,r9,r10,r12,xs,ys,zs) /\ l <> 0 in
1288 let (l,r10,xs,ys,zs) = mc_mul (l-1,r7,r
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Darm_evalScript.sml122 registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
127 name r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
142 (registers r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13
/seL4-l4v-master/HOL4/examples/machine-code/multiword/x64/
H A Dx64_multiwordScript.sml108 val x7 = ("r7",``7w:word4``,``r7:word64``);
1197 x64_mul (r7:word64,r9,r10:word64,r12:word64,xs:word64 list,ys,zs) =
1198 if r7 = 0w then let r10 = r10 + r9 in (r10,xs,ys,zs) else
1199 let r7 = r7 - 1w in
1206 x64_mul (r7,r9,r10,r12,xs,ys,zs)`
1226 let r7 = r1 >>> 1 in
1230 let (r10,xs,ys,zs) = x64_mul (r7,r9,r10,r12,xs,ys,zs) in
1236 let r7
[all...]

Completed in 207 milliseconds

123