Searched refs:regs (Results 26 - 50 of 65) sorted by relevance

123

/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dprog_ppcLib.sml35 val regs = map (fn tm => mk_eq(tm,(snd o process T o cdr o car) tm)) rs value
38 val th = foldr (uncurry DISCH) th (regs @ flags)
49 val regs = collect_term_of_type ``:ppc_reg`` g; value
65 val pre_post = map mk_pre_post_assertion (map (fn tm => (tm,T)) (regs @ bits) @ mems)
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A Darm_evalLib.sml336 let val regs = dest_subst_reg t value
337 val l = tl regs
338 val rest = snd (hd regs)
415 let val regs = dest_subst_reg t value
416 val l = tl regs
417 val rest = snd (hd regs)
H A DarmScript.sml44 val _ = Hol_datatype `regs = <| reg : registers; psr : psrs |>`;
47 `arm_state = <| regs : regs; ireg : word32; exception : exceptions |>`;
61 interrupt = Reset of regs | Undef | Prefetch | Dabort of num | Fiq | Irq`;
803 let ireg = state.ireg and r = state.regs
850 let (flags,i,f,m) = DECODE_PSR (CPSR_READ state.regs.psr) in
887 <| regs := r; ireg := inp.ireg;
893 let ireg = state.ireg and r = state.regs in
H A DsystemScript.sml229 let s = <| regs := <| reg := state.registers; psr := state.psrs |>;
347 let s = <| regs := <| reg := state.registers; psr := state.psrs |>;
389 let s = <| regs := <| reg := state.registers; psr := state.psrs |>;
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DregAllocation.sml815 List.foldl (fn (Assem.OPER {dst = d, ...}, regs) =>
816 (List.foldl (fn (Assem.REG r, regs) => Binaryset.add(regs,Assem.REG r)
817 | _ => regs) regs d)
818 | (Assem.MOVE {dst = d, ...}, regs) => Binaryset.add(regs,d)
819 | (_,regs) => regs
H A DrulesScript.sml57 proper = (\(regs,mem):DSTATE. (regs ' 11w = 100w) /\ (regs ' 13w = 100w))`;
H A DmechReasoning.sml46 let val {regs=regs,...} = declFuncs.getFunc f_name;
50 val neg_regs = Binaryset.difference(univ_set,regs)
344 let val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`),
1573 let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`));
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DregAllocation.sml815 List.foldl (fn (Assem.OPER {dst = d, ...}, regs) =>
816 (List.foldl (fn (Assem.REG r, regs) => Binaryset.add(regs,Assem.REG r)
817 | _ => regs) regs d)
818 | (Assem.MOVE {dst = d, ...}, regs) => Binaryset.add(regs,d)
819 | (_,regs) => regs
H A DrulesScript.sml56 proper = (\(regs,mem):DSTATE. (regs ' 11w = 100w) /\ (regs ' 13w = 100w))`;
H A DmechReasoning.sml248 val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), mk_var ("mem", Type `:ADDR |-> DATA`));
1021 let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`));
1110 val {regs=regs,...} = declFuncs.getFunc f_name;
1112 val neg_regs = Binaryset.difference(univ_set,regs)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DregAllocation.sml815 List.foldl (fn (Assem.OPER {dst = d, ...}, regs) =>
816 (List.foldl (fn (Assem.REG r, regs) => Binaryset.add(regs,Assem.REG r)
817 | _ => regs) regs d)
818 | (Assem.MOVE {dst = d, ...}, regs) => Binaryset.add(regs,d)
819 | (_,regs) => regs
H A DbigInstScript.sml436 POP_ASSUM (ASSUME_TAC o Q.SPEC `(regs,mem)`) THEN
459 `?regs mem. run_cfl (BLK (push_list l)) st = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN
461 `locate_ge ((regs ' 13):word32) 1` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN
707 `?st'. run_cfl (BLK (pop_one h)) (regs,mem) = st'` by METIS_TAC [] THEN
746 `?regs mem. st = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN
H A DCFL_RulesScript.sml57 proper = (\(regs,mem):DSTATE. (regs ' 11 = 100w) /\ (regs ' 13 = 100w))`;
H A DCFLScript.sml403 (SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos0,cpsr0,regs,mem):STATE`
407 SIMP_TAC list_ss [get_st_def, Once RUNTO_ADVANCE, SIMP_RULE std_ss [] (Q.SPEC `(pos1,cpsr1,regs,mem):STATE`
/seL4-l4v-master/HOL4/examples/computability/register/
H A DrmModelScript.sml52 I : reg list (input regs);
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dx86assembly_masm32.S82 ; It is probably unnecessary to save the callee-save regs or load the ML regs.
H A Dx86assembly_masm64.S106 ; It is probably unnecessary to save the callee-save regs or load the ML regs.
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A Dcodegen_x86Lib.sml11 fun set_x86_regs regs = (x86_regs := regs);
H A Dreg_allocLib.sml346 val regs = map (fn n => mk_var("r" ^ (int_to_string n),``:word32``)) (rev (kk (n-1))) value
348 val r = map fst (filter (fn (x,xs) => tmem x regs) graph)
349 val q = filter (fn (x,xs) => not (tmem x regs)) graph
434 val new_colour = select_colour x (op_set_diff aconv regs zs) c
536 2. assume infinite number of regs, make
537 regs 5,6,7,etc. --> stack locations 0,1,2,3,etc.
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Demit_eval.sml47 fun mk_arm_state arch regs psrs md mem =
49 (armML.proc numML.ZERO regs,
445 { cycle : bool, pc : bool, ireg : bool, regs : bool, mem : bool,
452 regs = i > 3,
460 if #regs trace then print_reg_updates ii (s1, s2) else ();
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_stepLib.sml389 the_state arch itstate ext thumbee thumb endian flags regs memory =
409 flags, regs, memory]))
514 val regs = mk_reg_mode_updates (the_state,state') value
516 val mregs = list_mk_conj (tmode :: regs @ psrs)
518 (List.length regs, apply_conv (SIMP_CONV (std_ss++boolSimps.CONJ_ss)
H A Darm_random_testingLib.sml69 val regs = List.map mk_word4 value
72 val valid_registers = regs [2,3,4,5,6,7,8,9,10,11,12,13,14]
73 val valid_thumb2_registers = regs [2,3,4,5,6,7,8,9,10,11,12,14]
74 val valid_thumb_registers = regs [2,3,4,5,6,7]
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dstack_analysisLib.sml114 val regs = (case !arch_name of value
119 (map (fn s => mk_var(s,wty)) regs @
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/arm/
H A Dprog_armLib.sml65 val regs = collect_term_of_type ``:word4`` g value
66 val regs = filter wordsSyntax.is_n2w regs value
110 val pre_post = map mk_pre_post_assertion (regs @ bits @ mems)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86CODESIG.sml50 val regs: int value

Completed in 157 milliseconds

123