/seL4-l4v-master/HOL4/examples/computability/register/ |
H A D | register_machineScript.sml | 16 val _ = Datatype `RegMachine = <| insts : instruction list; regs : num |-> num; pc : num |>`; 22 val reg_val_def = Define`reg_val regs n = case FLOOKUP regs n of NONE => 0n | SOME x => x `; 24 val upd_reg_def = Define`upd_reg f n regs = regs |+ (n,f (reg_val regs n))`; 29 Inc n => rm with <|regs updated_by upd_reg SUC n;pc updated_by SUC |> 30 | Dec n => rm with <|regs updated_by upd_reg PRE n;pc updated_by SUC |> 31 | JZ n i b => if reg_val rm.regs n = 0 then rm with 33 regs updated_b [all...] |
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | x64asm_semanticsScript.sml | 19 ; regs : reg -> word64 option 41 write_reg r w s = s with regs := s.regs���r ��� SOME w��� 46 unset_regs (r::rs) s = unset_regs rs (s with regs := s.regs���r ��� NONE���) 84 s.regs r1 = SOME w1 ��� 85 s.regs r2 = SOME w2 ��� 89 s.regs r1 = SOME w1 ��� 90 s.regs r2 = SOME w2 ��� 110 s.regs r [all...] |
H A D | codegen_proofsScript.sml | 42 t.regs R12 = SOME 16w ��� 43 t.regs R13 = SOME 0x7FFFFFFFFFFFFFFFw ��� 44 t.regs R14 = SOME r14 ��� 45 t.regs R15 = SOME r15 ��� 51 ���w ws. xs = Word w :: ws ��� t.regs RAX = SOME w ��� t.stack = ws 201 v_inv (t with regs := r) a w = v_inv t a w 268 t.regs R15 = SOME w ��� 418 regs := (RAX =+ SOME w) t.regs; 925 t.regs R1 [all...] |
/seL4-l4v-master/graph-refine/ |
H A D | inst_logic.py | 33 regs = [] 43 regs.append (bit2) 44 fin_bits.append ('argv%d' % (len (regs))) 47 return (regs, '_'.join (fin_bits)) 127 (regs, ident) = split_inst_name_regs (ident) 134 assert len (regspecs) == len (regs), (fname, regs, regspecs) 135 inp_regs = [reg for (reg, d) in zip (regs, regspecs) if d == 'I'] 136 out_regs = [reg for (reg, d) in zip (regs, regspecs) if d == 'O']
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/examples/ |
H A D | fc_examples.sml | 17 (\(regs,mem). (regs ' 11 = 100w) /\ (regs ' 13 = 100w)) st ==> 43 (\(regs,mem). (regs ' 11 = 100w) /\ (regs ' 13 = 100w)) st ==>
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | declFuncs.sml | 18 regs : int Binaryset.set, localNum : int, def : thm}; 35 ( decls := T.enter(!decls,!k, {name = name, ftype = tp, ir = ir, regs = rs, localNum = n, def = f_def});
|
H A D | preARMScript.sml | 166 !regs mem. P (regs,mem)`, 171 `(!s:STATE. P s) = !pc pcsr regs mem. P (pc,pcsr,(regs,mem))`, 182 read (regs,mem) (exp:EXP) = 186 POS k => mem ' ((MEM_ADDR (regs ' (n2w r))) + (n2w k)) | 187 NEG k => mem ' ((MEM_ADDR (regs ' (n2w r))) - (n2w k)) 191 REG r => regs ' (n2w:num->word4 r) 196 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (MEM_ADDR (regs ' (n2 [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | declFuncs.sml | 18 regs : int Binaryset.set, localNum : int, def : thm}; 35 ( decls := T.enter(!decls,!k, {name = name, ftype = tp, ir = ir, regs = rs, localNum = n, def = f_def});
|
H A D | preARMScript.sml | 162 !regs mem. P (regs,mem)`, 167 `(!s:STATE. P s) = !pc pcsr regs mem. P (pc,pcsr,(regs,mem))`, 178 read (regs,mem) (exp:EXP) = 182 POS k -> mem ' ((ADDR30 (regs ' (n2w r))) + (n2w k)) || 183 NEG k -> mem ' ((ADDR30 (regs ' (n2w r))) - (n2w k)) 187 REG r -> regs ' (n2w:num->word4 r) 192 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (ADDR30 (regs ' (n2 [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | declFuncs.sml | 18 regs : int Binaryset.set, localNum : int, def : thm}; 35 ( decls := T.enter(!decls,!k, {name = name, ftype = tp, ir = ir, regs = rs, localNum = n, def = f_def});
|
H A D | preARMScript.sml | 160 !regs mem. P (regs,mem)`, 165 `(!s:STATE. P s) = !pc pcsr regs mem. P (pc,pcsr,(regs,mem))`, 174 read (regs,mem) (exp:EXP) = 178 POS k -> mem ' (w2n (regs ' r) + k) || 179 NEG k -> mem ' (w2n (regs ' r) - k) 183 REG r -> regs ' r 188 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (w2n (regs ' [all...] |
H A D | funCallScript.sml | 346 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 13 - n2w k),mem)` THEN 348 (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [ 353 WORDS_TAC THEN `w2n (regs ' 13) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 388 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 13 - n2w k),mem)` THEN 389 `locate_ge (read st1 SP) (LENGTH l) /\ (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [ 394 WORDS_TAC THEN `w2n (regs ' 13) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 487 Q.ABBREV_TAC `st1 = (regs |+ (11,regs ' 1 [all...] |
/seL4-l4v-master/seL4/libsel4/include/sel4/ |
H A D | faults.h | 75 LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_TimeoutReply_new(seL4_Bool resume, seL4_UserContext regs, seL4_Word length) argument 79 seL4_SetMR(i, ((seL4_Word *) ®s)[i]);
|
H A D | deprecated.h | 39 } regs; member in union:__anon177
|
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/ |
H A D | deprecated.h | 45 } regs; member in union:__anon215 62 } regs; member in union:__anon217
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_astScript.sml | 72 | Plbzx of ireg => ireg => ireg (* same, with 2 index regs *) 74 | Plfdx of freg => ireg => ireg (* same, with 2 index regs *) 76 | Plfsx of freg => ireg => ireg (* same, with 2 index regs *) 78 | Plhax of ireg => ireg => ireg (* same, with 2 index regs *) 80 | Plhzx of ireg => ireg => ireg (* same, with 2 index regs *) 82 | Plwzx of ireg => ireg => ireg (* same, with 2 index regs *) 102 | Pstbx of ireg => ireg => ireg (* same, with 2 index regs *) 104 | Pstfdx of freg => ireg => ireg (* same, with 2 index regs *) 106 | Pstfsx of freg => ireg => ireg (* same, with 2 index regs *) 108 | Psthx of ireg => ireg => ireg (* same, with 2 index regs *) [all...] |
/seL4-l4v-master/seL4/include/arch/arm/arch/object/ |
H A D | vcpu.h | 76 word_t regs[seL4_VCPUReg_Num]; member in struct:vcpu 143 vcpu->regs[reg] = vcpu_hw_read_reg(reg); 159 vcpu_hw_write_reg(reg, vcpu->regs[reg]); 175 return vcpu->regs[reg]; 184 vcpu->regs[reg] = value;
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sig | 5 { cycle : bool, pc : bool, ireg : bool, regs : bool, mem : bool,
|
H A D | arm_evalScript.sml | 98 mk_arm_state arch regs psrs md mem = 99 <| registers := proc 0 regs;
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
H A D | fpu.h | 100 : "r"(&dest->regs[0]) 145 : "r"(&src->regs[0])
|
H A D | registerset.h | 105 fp_reg_t regs[RISCV_NUM_FP_REGS]; member in struct:user_fpu_state
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sml | 82 val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"] value 85 in find r (zip regs indx) end 148 val regs = ["EAX","ECX","EDX","EBX","ESP","EBP","ESI","EDI"] value 168 [("Reg/Opcode",int_to_string (pos y regs))] 169 else if (x = "r/m32") andalso (mem y regs) then 170 [("R/M",int_to_string (pos y regs)),("Mod","3")]
|
/seL4-l4v-master/HOL4/examples/elliptic/swsep/ |
H A D | swsepScript.sml | 37 val _ = hide "regs"; 588 `REGS_EQUIVALENT m registers regs = 589 (!r. ((regs ' (MREG2REG r)) = (registers (num2register (mode_reg2num m (MREG2REG r))))))` 639 (DECODE_MEXP m (MR r) regs = regs (MREG2register m r)) /\ 640 (DECODE_MEXP m (MC s c) regs = ((w2w c):word32 #>> (2 * w2n s)))` 662 ``!mexp regs mode C. 663 (SND (ADDR_MODE1 regs mode C 665 ((11 >< 0) (addr_mode1_encode (MEXP2addr_model mexp)))) = DECODE_MEXP mode mexp regs)``, 716 (DECODE_SHIFT m (LSL:word4->shift r) (c:word5) (regs [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_emitScript.sml | 168 :: DATATYPE (`regs = <| reg : registers; psr : psrs |>`) 171 :: DATATYPE (`arm_state = <| regs : regs; ireg : word32; 180 :: DATATYPE (`interrupt = Reset regs | Undef | Prefetch |
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 760 | loadWin64Args(arg::args, stackOffset, argOffset, regs, code, extraStack, preCode) = 769 case regs of 770 (areg, _) :: regs' => 771 loadWin64Args(args, stackOffset, newArgOffset+size, regs', 796 case regs of 797 (_, fpReg) :: regs' => 798 loadWin64Args(args, stackOffset, newArgOffset+size, regs', 811 case regs of 812 (_, fpReg) :: regs' => 813 loadWin64Args(args, stackOffset, newArgOffset+size, regs', [all...] |