/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | prog_ppcLib.sml | 35 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 D | arm_evalLib.sml | 336 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 D | armScript.sml | 44 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 D | systemScript.sml | 229 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 D | regAllocation.sml | 815 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 D | rulesScript.sml | 57 proper = (\(regs,mem):DSTATE. (regs ' 11w = 100w) /\ (regs ' 13w = 100w))`;
|
H A D | mechReasoning.sml | 46 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 D | regAllocation.sml | 815 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 D | rulesScript.sml | 56 proper = (\(regs,mem):DSTATE. (regs ' 11w = 100w) /\ (regs ' 13w = 100w))`;
|
H A D | mechReasoning.sml | 248 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 D | regAllocation.sml | 815 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 D | bigInstScript.sml | 436 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 D | CFL_RulesScript.sml | 57 proper = (\(regs,mem):DSTATE. (regs ' 11 = 100w) /\ (regs ' 13 = 100w))`;
|
H A D | CFLScript.sml | 403 (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 D | rmModelScript.sml | 52 I : reg list (input regs);
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | x86assembly_masm32.S | 82 ; It is probably unnecessary to save the callee-save regs or load the ML regs.
|
H A D | x86assembly_masm64.S | 106 ; 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 D | codegen_x86Lib.sml | 11 fun set_x86_regs regs = (x86_regs := regs);
|
H A D | reg_allocLib.sml | 346 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 D | emit_eval.sml | 47 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 D | arm_stepLib.sml | 389 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 D | arm_random_testingLib.sml | 69 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 D | stack_analysisLib.sml | 114 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 D | prog_armLib.sml | 65 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 D | X86CODESIG.sml | 50 val regs: int value
|