Lines Matching refs:r3
24 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,r4,r5,r6,df,f))
36 arm_read_loop (r3,r4,r5,df,f)
38 (let r4 = r4 + 0x30w in (r3,r4,r5,r6,df,f)))``
42 let r3 = 0x0w:word32 in
44 let (r3,r4,r5,r6,df,f) = arm_read_loop (r3,r4,r5,df,f) in
45 (r3,r4,r5,r6,df,f)``;
173 let (r3,r4,r5,r6,df,f) = arm_readnum (r4,r5,df,f) in
174 let r3 = r3 << 2 in
175 let r3 = r3 + 0x2w in
176 (r3,r4,r5,r6,df,f)``;
403 arm_symbol_insert (r3,r5,r8,df:word32 set,dg:word32 set,dm:word32 set,f,g,m) =
404 (let m = (r3 =+ r8) m in
408 let r7 = r7 + r3 in
410 let m = (r3 + 0x4w =+ r7) m in
413 let r4 = r3 + 0x8w in
415 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))``
490 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m) =
491 (let r4 = m r3 in
493 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
494 arm_symbol_insert (r3,r5,r8,df,dg,dm,f,g,m)
496 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))
500 let r6 = r3 + 0x8w in
505 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m)
508 let r3 = m (r3 + 0x4w) in
509 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m)))
511 (let r3 = m (r3 + 0x4w) in
512 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m)))``;
662 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m) =
667 let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
668 arm_symbol_add (r3,r5,r8,df,dg,dm,f,g,m)
670 let r3 = r3 + 0x3w in
671 (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m))``;
701 arm_number_symbol (r9,r3,r4,r5,r7,r8,df,dg,dh:word32 set,dm,f,g,h:word32->word32,m) =
704 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
705 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m)
708 let r3 = r3 - r4 in
710 let h = (r9 =+ r3) h in
712 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
714 (let (r3,r4,r5,r6,df,f) = arm_read_number (r4,r5,df,f) in
716 let h = (r9 =+ r3) h in
718 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
720 (let (r3,r4,r5,r6,r7,r8,df,dg,dm,f,g,m) =
721 arm_symbol (r3,r4,r5,df,dg,dm,f,g,m)
724 let r3 = r3 - r4 in
726 let h = (r9 =+ r3) h in
728 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``;
745 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
747 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)
753 (let h = (r9 + 4w =+ r3) h in
754 let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
756 (r9,r3,r4,r5,r7,r8,df,dg,dh,dm,f,g,h,m)
758 let r3 = h (r9 - 4w) in
759 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))
766 (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m)))
770 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m))``;
873 ``!xs x r3 a y. (a,y) IN x /\ ALIGNED r3 /\
874 symbol_table xs x (r3,dm,mi,dg,gi) ==>
879 \\ Cases_on `(a,y) = (r3,h)` THEN1 METIS_TAC [PAIR_EQ]
880 \\ `(a,y) IN (x DELETE (r3,h))` by ASM_SIMP_TAC std_ss [IN_DELETE]
881 \\ `ALIGNED (r3 + n2w (8 + (STRLEN h + 3) DIV 4 * 4))` suffices_by METIS_TAC []
892 ``!s r1 r3 k r6 r7 r8 p x xs df dg dh dm f g h m.
895 symbol_table xs x (r3,dm,m,dg,g) /\ ALIGNED r1 /\
897 symbol_table_dom (all_symbols (sexp_lex s) xs) (r3,dm,dg) ==>
899 arm_lexer_pre (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\
900 (arm_lexer (r1,r3,w2w (f k),k,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
901 (r1i,r3,r4i,r5i,r6i,r7i,r8i,df,dg,dh,dm,f,gi,hi,mi)) /\
902 (p * arm_tokens r1 (sexp_lex s) r3 xi r1i) (fun2set (hi,dh)) /\
904 symbol_table (all_symbols (sexp_lex s) xs) xi (r3,dm,mi,dg,gi) /\
958 [`r1+8w`,`r3`,`k+1w`,`y2`,`r7`,`r8`,`p * one (r1,y2) * one (r1 + 0x4w,y')`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ y2) h'`,`m`])
1021 \\ `(p * one (r1,n) * one (r1 + 0x4w,r3) *
1023 (fun2set ((r1 =+ n) ((r1 + 0x4w =+ r3) h'),dh))` by SEP_WRITE_TAC
1026 [`r1+8w`,`r3`,`x'`,`y`,`r7`,`r8`,`p * one (r1,n) * one (r1 + 0x4w,r3)`,`x`,`xs`,`df`,`dg`,`dh`,`dm`,`f`,`g`,`(r1 =+ n) ((r1 + 4w =+ r3) h')`,`m`])
1040 \\ Q.EXISTS_TAC `n` \\ Q.EXISTS_TAC `r3`
1079 (Q.SPECL [`xs`,`STRING h t1`,`r3`,`f`,`g`] arm_symbol_lemma))))
1093 \\ `(p * one (r1,r3i - r3) * one (r1 + 0x4w,r3) *
1095 (fun2set ((r1 =+ r3i - r3) ((r1 + 0x4w =+ r3) h'),dh))` by SEP_WRITE_TAC
1098 [`r1+8w`,`r3`,`r5i`,`r6i`,`r7i`,`r8i`,`p * one (r1,r3i - r3) * one (r1 + 4w,r3)`,`(r3i - 3w, STRING h t1) INSERT x`,`add_symbol (STRING h t1) xs`,`df`,`dg`,`dh`,`dm`,`f`,`gi`,`(r1 =+ r3i - r3) ((r1 + 4w =+ r3) h')`,`mi`])
1103 \\ `(hi (r1 + 4w) = r3) /\ r1 + 0x4w IN dh` by SEP_READ_TAC
1104 \\ `(hi r1 = r3i-r3) /\ r1 IN dh` by SEP_READ_TAC
1112 \\ Q.EXISTS_TAC `r3i - r3`
1113 \\ Q.EXISTS_TAC `r3`
1481 let r3 = 3w in
1482 let h = (r6 =+ r3) h in
2139 arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2141 let (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2142 arm_lexer (r9,r3,r4,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in
2221 ``!r9 r8 r7 r6 r5 r3 y x s p m h g f dm dh dg df d b.
2224 ALIGNED r9 /\ ALIGNED8 (r3 - r9) /\
2225 symbol_table builtin_symbols x (r3,dm,m,dg,g) /\
2228 symbol_table_dom (all_symbols (sexp_lex s) builtin_symbols) (r3,dm,dg) ==>
2230 arm_parse8_pre (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) /\
2231 (arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) =
2233 (arm_tokens4 (r9 - 8w) [] r3 xi (r9 - 8w) *
2234 lisp_exp (string2sexp s) r7i (r3,xi) *
2235 SEP_FILL (r3,xi) * p) (fun2set (hi,dh)) /\
2238 (r3,dm,mi,dg,gi)``,
2245 \\ `ALIGNED r1i /\ ALIGNED r3 /\ ALIGNED8 (r3 - r1i)` by
2261 \\ `(arm_tokens4 (r1i - 0x8w) (REVERSE (sexp_lex s)) r3 xi (r9 - 8w) *
2262 arm_tokens3 r1i (REVERSE (sexp_lex s)) (r9 + n2w (8 * sexp_lex_space s)) * SEP_FILL (r3,xi) * p)
2274 \\ `(r3, "nil") IN xi /\ (r3 + 0x18w, "quote") IN xi` by
2277 \\ Q.PAT_X_ASSUM `symbol_table (builtin_symbols ++ zs) xi (r3,dm,mi,dg,gi)` MP_TAC
2282 \\ `ALIGNED8 (r3 - (r1i - 8w))` by ASM_SIMP_TAC std_ss [ALIGNED8_STEP]
2286 ``SEP_FILL (r3,xi)``)
2313 ``symbol_table builtin_symbols x (r3,dm,m,dg,g)``
2327 ``symbol_table_dom builtin_symbols (r3,dm,dg)``
2332 val tms = find_terms (can (match_term ``(g:word32->word8) (r3 + n2w m) = n2w n``)) (concl symbol_table_th)
2346 val tms = find_terms (can (match_term ``(m:word32->word32) (r3) = w``)) (concl symbol_table_th)
2354 val ll = pairSyntax.list_mk_pair[mk_var("r3",``:word32``),
2378 val ll2 = pairSyntax.list_mk_pair[mk_var("r3",``:word32``),
2393 val ll3 = pairSyntax.list_mk_pair[mk_var("r3",``:word32``),
2412 ``!r3 dg dm g m.
2413 symbol_table_dom builtin_symbols (r3,dm,dg) ==>
2414 arm_setup_pre (r3,r6,dm,dg,m,g) /\
2416 (arm_setup (r3,r6,dm,dg,m,g) = (r3,r6i,dm,dg,mi,gi)) /\
2417 symbol_table builtin_symbols (builtin_symbols_set r3) (r3,dm,mi,dg,gi)``,
2437 arm_string2sexp' (r3,r4,r5,df,dg,dh,dm,f,g,h,m) =
2442 let r5 = r3 in
2443 let r3 = r9 + r7 in
2445 let r3 = r3 + 24w in
2447 let (r3,r6,dm,dg,m,g) = arm_setup (r3,r6,dm,dg,m,g) in
2451 arm_parse8 (r9,r3,r5,r6,r7,r8,df,dg,dh,dm,f,g,h,m) in
2460 let r3 = r7 in
2467 (r3,r4,r5,r6,r7,r8,r9,df,dg,dh,dm,f,g,h,m)``;
2767 string_mem (STRCAT (sexp2string s) null_string) (r3,f,df) /\ ALIGNED r5 /\
2772 arm_string2sexp'_pre (r3,n2w l,r5,df,dg,dh,dm,f,g,h,m) /\
2773 (arm_string2sexp' (r3,n2w l,r5,df,dg,dh,dm,f,g,h,m) =
2836 (r5 + 0x8w,r5 + n2w (l * 16) + 0x18w,r3,0x28w,n2w (l * 16),n2w (l * 8),
3115 (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g)``]
3183 ~aR 0x0w * aSTRING r3 (sexp2string s) * aPC p * ~aS``
3187 pSTRING r3 (sexp2string s) * pPC p * ~pS``
3191 xSTRING r3 (sexp2string s) * xPC p * ~xS``