Searched refs:r3 (Results 1 - 25 of 114) sorted by relevance

12345

/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Djiraver434.c8 int r2, r3; member in struct:__anon117
14 return ucptr->r2 + ucptr->r3;
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_tests.sml5 "e08cc003" (* add ip, ip, r3 *) ::
11 "e283c001" (* add ip, r3, #1 *) ::
12 "e283c002" (* add ip, r3, #2 *) ::
52 "e0800103" (* add r0, r0, r3, lsl #2 *) ::
56 "e2830010" (* add r0, r3, #16 *) ::
57 "e0830200" (* add r0, r3, r0, lsl #4 *) ::
104 "e0811183" (* add r1, r1, r3, lsl #3 *) ::
110 "e2831001" (* add r1, r3, #1 *) ::
111 "e0831101" (* add r1, r3, r1, lsl #2 *) ::
112 "e0831201" (* add r1, r3, r
[all...]
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Dselftest.sml106 val r3 = reg 3 value
145 adc pc,r3,r4,asr #29
146 .label: adc sp,r3,r4,lsl lr
154 asr r3,#11
155 asr r3,r9
156 asr r3,r9,r4
157 rrx r3
158 rrx r3,r5
159 ror r3,r5
257 ("LDRBNE r2, [r3]",
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/
H A Darm_decomp_demoScript.sml18 ed936a00 (* vldr s12, [r3] *)
21 e59d3000 (* ldr r3, [sp] *)
28 edc37a00 (* vstr s15, [r3] *)`;
33 e3003000 (* movw r3, #0 *)
34 e3403000 (* movt r3, #0 *)
35 ed937a00 (* vldr s14, [r3] *)
36 edd37a03 (* vldr s15, [r3, #12] *)
38 edd35a01 (* vldr s11, [r3, #4] *)
39 edd37a05 (* vldr s15, [r3, #20] *)
40 ed936a02 (* vldr s12, [r3, #
[all...]
H A Darm_core_decompScript.sml16 (* r3 *) word32 =>
45 (ARM_ASSERTION mode r0 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14
51 arm_REG (R_mode mode 3w) r3 *
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A DdivideScript.sml24 if_sub(r5:word32,r4:word32,r2:word32,r3:word32) =
27 let r3 = r3 + r2 in
28 (r5,r4,r2,r3)
29 else (r5,r4,r2,r3)``
32 sub_and_shift(r5:word32,r4:word32,r2:word32,r3:word32) =
33 let (r5,r4,r2,r3) = if_sub (r5,r4,r2,r3) in
35 if r2 = 0w then (r5,r4,r2,r3) else
37 sub_and_shift(r5,r4,r2,r3)``;
[all...]
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) =
23 if r3 = r4 then
25 (r3,r4,r5,r6,r7,r8,df,f)
29 let r3 = f (r7 - 0x4w) in
32 arm_eq_loop (r3,r4,r5,r6,r7,r8,df,f)
34 let r5 = r3 || r4 in
36 let r5 = f (r3 + 0x4w) in
37 let r3 = f r3 i
[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
69 let r3 = r3 - 1w in
70 arm_string_rev(r3,r6,r7,df,f)``
74 let r3 = r7 - r6 in
75 let r3 = r3 >>> 1 in
76 let r6 = r6 + r3 in
78 let r7 = r7 - r3 i
[all...]
H A Dlisp_parseScript.sml24 arm_read_loop (r3:word32,r4:word32,r5:word32,df:word32 set,f:word32->word8) =
25 (let r6 = r3 << 2 in
26 let r3 = r3 + r6 in
27 let r3 = r3 + r3 in
28 let r3 = r3 + r4 in
34 (let r4 = r4 + 0x30w in (r3,r
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/compiler/demo/
H A Dcompiler_demoScript.sml54 copy_byte_loop (r3:word32,r4:word32,dg:word32 set,g:word32->word8) =
55 if r3 = 0w then (r3,r4,dg,g) else
56 let r3 = w2w (g r3) in
58 let g = (r4 =+ w2w r3) g in
59 copy_byte_loop (r3,r4,dg,g)``;
88 call_mod10 (r1:word32,r2:word32,r3) =
90 let r1 = r1 + r3 in
100 let r3
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/test/
H A Dtea.sml239 (\(r0,r1,r2,r3).
244 let r0 = r0 + r3 in
250 (\((r0,r1),(r2,r3,r4,r5),r6).
252 let r7 = ShiftXor (r1,r6,r2,r3) in
256 ((r0,r1),(r2,r3,r4,r5),r6))) : thm
259 (\(r0,(r1,r2),(r3,r4,r5,r6),r7).
260 (let ((r0,r1),(r2,r3,r4,r5),r6) =
262 ((r1,r2),(r3,r4,r5,r6),r7)
265 let ((r1,r2),(r3,r4,r5,r6),r7) =
266 Round ((r1,r2),(r3,r
[all...]
H A Drefined_format.sml12 val (src1,dst1) = (``(r2:word32,r3:word32,r4:word32,r1:word32)``,
13 ``(r1:word32,r2:word32,r3:word32,r4:word32)``
24 let r2 = atom r3 in
25 let r3 = atom r4 in
27 (r1,r2,r3,r4)) =
28 (r2,r3,r4,r1) : thm
31 val (src2,dst2) = (``(r0:word32,r1:word32,r2:word32,r3:word32)``,
32 ``(r1:word32,r2:word32,r3:word32,r4:word32)``
45 let r5 = atom r3 in
46 let r3
[all...]
H A DCADE_example.sml174 (let r3 = r2 + 100 in
176 let r4 = r3 + r4 in
179 r3
183 let r0 = r3 * r0 in
206 ASG (L 1) r3 (r2 + 100) (L 3) |++|
208 (ASG (L 4) r4 (r3 + r4) (L 5) |++|
210 ASG (L 7) r0 r3 (L 6) |++|
213 ASG (L 6) r0 (r3 * r0) (L 2)))),L 2)
214 ((let r3 = r2 + 100 in
216 let r4 = r3
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/decompiler/
H A Dm0_decomp_demoScript.sml9 mov r3, r0 ; first address
10 adds r3, #40 ; last address (10 loads)
14 cmp r0, r3 ; test if done
/seL4-l4v-master/HOL4/src/rational/
H A DratScript.sml1394 |- !r1 r2 r3. r1 < r2 /\ r2 < r3 ==> r1 < r3
1420 ``!r1 r2 r3. rat_les r1 r2 /\ rat_les r2 r3 ==> rat_les r1 r3``,
1423 ``rat_sub r3 r1 = rat_add (rat_sub r3 r2) (rat_sub r2 r1)``
1431 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r2)`` THEN
1452 |- !r1 r2 r3
[all...]
/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/computability/register/
H A DrmToolsScript.sml37 dup0 r1 r2 r3= <|
42 | 3 => Inc r3 (SOME 1)
43 | 4 => Dec r3 (SOME 5) NONE
53 dup r1 r2 r3= <|
59 | 3 => Inc r3 (SOME 1)
60 | 4 => Dec r3 (SOME 5) NONE
409 (dup r1 r2 r3).tf 0 = Dec r2 (SOME 0) (SOME 1) ���
410 (dup r1 r2 r3).tf 1 = Dec r1 (SOME 2) (SOME 4) ���
411 (dup r1 r2 r3).tf 2 = Inc r2 (SOME 3) ���
412 (dup r1 r2 r3)
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml121 garble (r2:word32,r3:word32,r4:word32) =
122 let r1 = r2 + r3 in
123 let r2 = r1 - r3 << 5 in
124 let r3 = r2 * r3 in
126 let r2 = r3 && r2 >>> 30 in
129 let r3 = r2 !! r1 in
130 let r2 = r3 ?? 55w in
131 (r2,r3)`;
157 f (r1,r2) = let .... in f (r2,r3)
[all...]
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/test/
H A DregexTest.sml41 val r3 = Seq (r2, r1); value
56 (19, true, r3, "00011212"),
57 (19, false, r3, "00011213")
89 (101, true, r3, longString ^ "112121212"),
90 (102, false, r3, longString ^ "112121213"),
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Djit_incrementalScript.sml26 (* assign meanings to r1, r2, r3, r4 etc *)
34 r3 edi - preserved (rest of stack)
176 r3 edi - preserved (rest of stack)
184 r3 - pointer to next code to be generated
213 x86_encodes_jump (r3:word32,r6:word32,df:word32 set,f:word32->word8) =
214 let f = (r3 =+ 0x83w) f in
215 let f = (r3 + 1w =+ 0xF1w) f in
216 let f = (r3 + 2w =+ w2w r6) f in
217 let f = (r3 + 3w =+ 0xFFw) f in
218 let f = (r3
[all...]
/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,
18 arm_REG (R_mode mode 3w) r3 *
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,
/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"];
53 E5935000 (* ldr r5,[r3] *)
54 E5936004 (* ldr r6,[r3,#4] *)
57 E4835004 (* L2:str r5,[r3],#4 *)
58 E4836004 (* str r6,[r3],#4 *)
59 E2833004 (* add r3,r3,#4 *)`;
62 E1530004 (* CHENEY:cmp r3,r4 *)
78 E289300C (* add r3,r9,#12 *) (* set i *)
79 00833006 (* addeq r3,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"];
50 E5935000 (* ldr r5,[r3] *)
51 E5936004 (* ldr r6,[r3,#4] *)
54 E4835004 (* L2:str r5,[r3],#4 *)
55 E4836004 (* str r6,[r3],#4 *)`;
58 E1530004 (* CHENEY:cmp r3,r4 *)
74 E2893008 (* add r3,r9,#8 *) (* set i *)
75 00833006 (* addeq r3,r3,r6 *)`;
82 E0835006 (* add r5,r3,r
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/multiword/
H A Dmc_multiwordScript.sml308 (\(l,r1:'a word,r3:'a word,r8:'a word,r9:'a word,r10:'a word,xs,zs).
312 (INR (l,r1:'a word,r3,r8,r9,r10,xs,zs),T))
317 let cond = cond /\ (r3 <> 0w ==> (r3 = 1w)) in
318 let (r8,r3) = single_add_word r8 r9 r3 in
323 (INL (l-1,r1,r3,r8,r9,r10,xs,zs),cond /\ l <> 0n)))``;
328 (\(l,r1:'a word,r3:'a word,r8:'a word,r9:'a word,r10:'a word,xs,ys,zs).
332 (INR (l,r1,r3,r8,r9,r10,xs,ys,zs),T))
339 let cond = cond /\ (r3 <>
[all...]

Completed in 125 milliseconds

12345