/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 1244 -- new value for rd for ALU ops, LOAD, LOAD_FP, LR, SC, CSR ops 1604 inline unit writeRD(rd::reg, val::regType) = 1605 { GPR(rd) <- val 1623 unit writeFPRS(rd::reg, val::word) = 1624 { FPRS(rd) <- val 1630 unit writeFPRD(rd::reg, val::regType) = 1631 { FPRD(rd) <- val 2023 -- ADDI rd, rs1, imm 2025 define ArithI > ADDI(rd::reg, rs1::reg, imm::imm12) = 2026 writeRD(rd, GP [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_opsemScript.sml | 44 reg_update ii rd f s1 s2 = 45 seqT (parT s1 s2) (\(x,y). write_reg ii (PPC_IR rd) (f x y))`; 48 uint_reg_update ii rd f s1 s2 = 50 (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_uint_cmp ii (f x y) 0w))`; 53 sint_reg_update ii rd f s1 s2 = 55 (\(x,y). parT_unit (write_reg ii (PPC_IR rd) (f x y)) (ppc_sint_cmp ii (f x y) 0w))`; 82 read_ireg ii rd = read_reg ii (PPC_IR rd)`; 114 reg_store ii size rd s1 s2 = 115 seqT (parT (effective_address s1 s2) (read_ireg ii rd)) [all...] |
H A D | ppc_seq_monadScript.sml | 18 val PREAD_R_def = Define `PREAD_R rd ((r,s,m):ppc_state) = r rd`; 19 val PREAD_S_def = Define `PREAD_S rd ((r,s,m):ppc_state) = s rd`; 20 val PREAD_M_def = Define `PREAD_M rd ((r,s,m):ppc_state) = m rd`; 22 val PWRITE_R_def = Define `PWRITE_R rd x (r,s,m) = ((rd =+ x) r,s,m):ppc_state`; 23 val PWRITE_S_def = Define `PWRITE_S rd x (r,s,m) = (r,(rd [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/ |
H A D | riscv.sml | 3754 fun writeFPRS (rd,val') = 3755 ( write'FPRS(val',rd) 3777 fun writeFPRD (rd,val') = 3778 ( write'FPRD(val',rd) 4400 fun dfn'ADDI (rd,(rs1,imm)) = 4401 ( write'GPR(BitsN.+(GPR rs1,BitsN.signExtend 64 imm),rd) 4411 fun dfn'ADDIW (rd,(rs1,imm)) = 4417 ( write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd) 4430 fun dfn'SLTI (rd,(rs1,imm)) = 4438 (BitsN.fromBool 64 (BitsN.<(v1,BitsN.signExtend 64 imm)),rd) [all...] |
H A D | riscvScript.sml | 4164 ("writeFPRS",TP[Var("rd",FTy 5),Var("val",F32)], 4172 TP[Var("val",F32),Var("rd",FTy 5)]),qVar"state"), 4222 ("writeFPRD",TP[Var("rd",FTy 5),Var("val",F64)], 4230 TP[Var("val",F64),Var("rd",FTy 5)]),qVar"state"), 5652 ("dfn'ADDI",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)], 5662 Var("rd",FTy 5)]),qVar"state"))) 5665 ("dfn'ADDIW",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)], 5685 LN 0,F32)),Var("rd",FTy 5)]),qVar"s"))))) 5688 ("dfn'SLTI",TP[Var("rd",FTy 5),Var("rs1",FTy 5),Var("imm",FTy 12)], 5709 Var("rd",FT [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | float3.c | 27 double rd; local 50 ffi_call(&cif, FFI_FN(floating_1), &rd, values); 52 CHECK(rd - floating_1(f, d, ld) < DBL_EPSILON); 67 ffi_call(&cif, FFI_FN(floating_2), &rd, values); 69 CHECK(rd - floating_2(ld, d, f) < DBL_EPSILON);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | arm_evalScript.sml | 544 `!cond op s rd rn Op2. ~(op ' 3) \/ (op ' 2) ==> 545 (DECODE_ARM (data_proc_encode cond op s rn rd Op2) = data_proc)`, 550 `!cond op s rd rn Op2. 551 (DECODE_ARM (data_proc_encode cond op T rd 0w Op2) = data_proc)`, 561 (!cond s rd rn Op2. DECODE_ARM (enc (f cond s rd rn Op2)) = data_proc)`, 574 (!cond s rd Op2. DECODE_ARM (enc (f cond s rd Op2)) = data_proc)`, 580 `(!cond s rd rm rs. 581 DECODE_ARM (enc (instruction$MUL cond s rd r [all...] |
H A D | instructionSyntax.sml | 126 ``rd:word4`` |-> mk_register (#Rd y), 128 ``(f (c:condition) (s:bool) (rd:word4) 135 ``rd:word4`` |-> mk_register (#Rd y), 138 ``(f (c:condition) (s:bool) (rd:word4) (rn:word4) 150 ``rd:word4`` |-> mk_register (#Rd y), 155 (false,_,false) => ``MUL c s rd rm rs`` 156 | (false,_,true) => ``MLA c s rd rm rs rn`` 157 | (true,false,false) => ``UMULL c s rn rd rm rs`` 158 | (true,false,true) => ``UMLAL c s rn rd rm rs`` 159 | (true,true,false) => ``SMULL c s rn rd r [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/model/ |
H A D | mips.sml | 3290 fun dfn'MOVF (rd,(rs,cc)) = 3294 then write'GPR(GPR rs,rd) 3337 fun dfn'MOVT (rd,(rs,cc)) = 3341 then write'GPR(GPR rs,rd) 3796 fun dfn'ADD (rs,(rt,rd)) = 3806 else write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd) 3810 fun dfn'ADDU (rs,(rt,rd)) = 3818 write'GPR(BitsN.signExtend 64 temp,rd) 3822 fun dfn'SUB (rs,(rt,rd)) = 3832 else write'GPR(BitsN.signExtend 64 (BitsN.bits(31,0) temp),rd) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_parserLib.sml | 1358 fun add_sub_literal m (rd,i) = 1364 val narrow_okay = q <> Wide andalso narrow_register rd andalso 1379 mk_Add_Sub (mk_bool add,mk_word4 15,rd,imm12))) 1385 mk_Add_Sub (mk_bool (opc = mk_word4 4),mk_word4 15,rd,imm12)) 1389 fun narrow_okay_imm m i (rd,rn) = 1394 if is_SP rd then 1397 narrow_register rd andalso ~1020 <= v andalso v <= 1020 andalso 1401 if rd = rn then 1406 m = RSB andalso v = 0 andalso narrow_registers [rd,rn] 1410 (rd,r 1564 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) value 1574 val (rd,rn) = if m = MOV orelse m = MVN then (rdn,r0) else (r0,rdn) value 1598 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r15) else (r15,rdn) value 1607 val (rd,rn) = if mem m [MOV,MVN] then (rdn,r0) else (r0,rdn) value [all...] |
H A D | arm_decoderScript.sml | 30 ``\opc setflags rn rd mode1. 31 DataProcessing (Data_Processing opc setflags rn rd mode1)``); 446 (let rd = (3 :+ b7) (r 0) in 448 (rd = 15w) /\ InITBlock /\ ~LastInITBlock 452 DP 0b1101w F 0w rd (REG 0w 0w (r4 3))) 723 let S = a 4 and rn = ra 0 and rd = rb 8 value 727 (if rd = 15w then 733 DP 0b0000w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 735 DP 0b1110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 737 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd 837 let S = a 4 and rn = ra 0 and rd = rb 8 value [all...] |
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | isqrtLib.sml | 32 (SOME rn, SOME rd) => 37 val SOME rd = sqrt d 42 val ry = mk_ge_thm rd
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/ |
H A D | mips_stepLib.sml | 174 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``, 176 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0]) 184 [[``rd <> 0w: word5``, ``rs <> 0w: word5``, ``rt <> 0w: word5``, 186 (all_comb [`rt` |-> r0, `rs` |-> r0, `rd` |-> r0]) 192 [[``rd <> 0w: word5``, ``rt <> 0w: word5``, 194 (all_comb [`rt` |-> r0, `rd` |-> r0]) 199 [[``rd <> 0w: word5``, ``^st.hi = SOME vHI``, ``^st.lo = SOME vLO``]] 200 [[], [`rd` |-> r0]] 288 val ADD = pEV ``dfn'ADD (rs, rt, rd)`` 289 val SUB = pEV ``dfn'SUB (rs, rt, rd)`` [all...] |
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowser.java | 58 Reader rd; 63 rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream())); 65 rd = new FileReader(path + fname); 67 br = new BufferedReader(rd);
|
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowser.java | 58 Reader rd; 63 rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream())); 65 rd = new FileReader(path + fname); 67 br = new BufferedReader(rd);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | arm_decoderScript.sml | 30 ``\opc setflags rn rd mode1. 31 DataProcessing (Data_Processing opc setflags rn rd mode1)``); 446 (let rd = (3 :+ b7) (r 0) in 448 (rd = 15w) /\ InITBlock /\ ~LastInITBlock 452 DP 0b1101w F 0w rd (REG 0w 0w (r4 3))) 723 let S = a 4 and rn = ra 0 and rd = rb 8 value 727 (if rd = 15w then 733 DP 0b0000w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0))) 735 DP 0b1110w S rn rd (REG (ib3 12 @@ ib2 6) (ib2 4) (rb 0)) 737 DP (if rn = 15w then 0b1101w else 0b1100w) S rn rd 837 let S = a 4 and rn = ra 0 and rd = rb 8 value [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | RJBConv.sml | 14 (* DATE : 3rd February 1993 *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sml | 93 val rd = "r" ^ int_to_string i value 96 val code = ["cmp " ^ rd ^ ", " ^ f j] 104 val rd = "r" ^ int_to_string i value 107 val code = ["tst " ^ rd ^ ", " ^ f j]
|
H A D | codegen_x64Lib.sml | 107 val rd = x64_reg i value 110 val code = ["cmp " ^ rd ^ ", " ^ f j] 118 val rd = x64_reg i value 121 val code = ["test " ^ rd ^ ", " ^ f j]
|
H A D | codegen_x86Lib.sml | 114 val rd = x86_reg i value 117 val code = ["cmp " ^ rd ^ ", " ^ f j] 125 val rd = x86_reg i value 128 val code = ["test " ^ rd ^ ", " ^ f j]
|
/seL4-l4v-10.1.1/HOL4/examples/dev/booth/ |
H A D | boothScript.sml | 24 (* mul,mul2,borrow2,mshift,rm,rd *) 54 let rd = if a then alub else 0w 59 BOOTH mul mul2 borrow2 mshift rm rd`; 64 NEXT (BOOTH mul mul2 borrow2 mshift rm rd) = 67 and alua = rd 70 let rd' = ALU borrow2 mul alua alub 76 BOOTH mul' mul2' borrow2' mshift' rm rd'`; 102 PROJ_RD (BOOTH mul mul2 borrow2 mshift rm rd) = rd`;
|
H A D | boothDevScript.sml | 203 (mul:num, mul2:num, borrow2:bool, mshift:num, rm:word,rd:word). 204 The variable rd stores the result of the multiplication. 227 `NEXTd(mul,mul2,borrow2,mshift,rm:word,rd) = 235 ALUd(borrow2,mul,rd,rm << mshift))`; 293 mshift:num, rm:word32, rd:word32) = rd`; 392 (rd' = ALU q2 q r alub)` by RW_TAC arith_ss []
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | PrecAnalysis.sml | 211 | (ld,rd,lsp:mini_lspec)::more_lsps => 223 if tk' = rd then 234 (A |> c1 rel |> c1 TM |> inc) (lsp, [#3 A]) rd 236 else if sep' = rd then
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegen_x64Lib.sml | 108 val rd = x64_reg i value 111 val code = ["cmp " ^ rd ^ ", " ^ f j] 119 val rd = x64_reg i value 122 val code = ["test " ^ rd ^ ", " ^ f j]
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/ |
H A D | cheriScript.sml | 3973 TP[Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),Var("imm5",FTy 5), 3975 CC[LW(0,6),Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5), 3984 TP[Var("function",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5), 3986 CC[LW(16,6),Var("function",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5), 3996 TP[Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5), 3998 CC[LW(28,6),Var("rs",FTy 5),Var("rt",FTy 5),Var("rd",FTy 5),LW(0,5), 4002 ("form6",TP[Var("rt",FTy 5),Var("rd",FTy 5),Var("function",FTy 6)], 4003 CC[LW(31,6),LW(0,5),Var("rt",FTy 5),Var("rd",FTy 5),LW(0,5), 7577 ("dfn'MOVF",TP[Var("rd",FTy 5),Var("rs",FTy 5),Var("cc",FTy 3)], 7597 qVar"state"),Var("rd",FT [all...] |