Searched refs:regs (Results 1 - 25 of 65) sorted by relevance

123

/seL4-l4v-master/HOL4/examples/computability/register/
H A Dregister_machineScript.sml16 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 Dx64asm_semanticsScript.sml19 ; 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 Dcodegen_proofsScript.sml42 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 Dinst_logic.py33 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 Dfc_examples.sml17 (\(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 DdeclFuncs.sml18 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 DpreARMScript.sml166 !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 DdeclFuncs.sml18 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 DpreARMScript.sml162 !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 DdeclFuncs.sml18 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 DpreARMScript.sml160 !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 DfunCallScript.sml346 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 Dfaults.h75 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 *) &regs)[i]);
H A Ddeprecated.h39 } regs; member in union:__anon177
/seL4-l4v-master/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/
H A Ddeprecated.h45 } regs; member in union:__anon215
62 } regs; member in union:__anon217
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_astScript.sml72 | 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 Dvcpu.h76 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 Demit_eval.sig5 { cycle : bool, pc : bool, ireg : bool, regs : bool, mem : bool,
H A Darm_evalScript.sml98 mk_arm_state arch regs psrs md mem =
99 <| registers := proc 0 regs;
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/
H A Dfpu.h100 : "r"(&dest->regs[0])
145 : "r"(&src->regs[0])
H A Dregisterset.h105 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 Dx86_encodeLib.sml82 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 DswsepScript.sml37 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 Darm_emitScript.sml168 :: 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 DX86FOREIGNCALL.sml760 | 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...]

Completed in 126 milliseconds

123