--- riscv.v.plain 2018-11-20 14:53:45.400922942 +0000 +++ riscv.v 2018-11-20 15:08:45.661714873 +0000 @@ -1260,6 +1260,9 @@ let v64 : bits 64 := EXTS 64 v in subrange_vec_dec (shift_bits_right v64 shift) 31 0. +Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} := + build_ex (Z.of_nat (n_leading_spaces s)). +(* Fixpoint n_leading_spaces (s : string) : {n : Z & ArithFact (n >= 0)} := build_ex(let p0_ := s in @@ -1273,7 +1276,7 @@ (string_drop s (build_ex 1))))))) : {n : Z & ArithFact (n >= 0)})))) - else 0). + else 0).*) Definition spc_forwards '(tt : unit) : string := " ". @@ -1284,7 +1287,7 @@ let 'n := projT1 (n_leading_spaces s) in let p0_ := n in if sumbool_of_bool ((Z.eqb p0_ 0)) then None - else Some ((tt, n)). + else Some ((tt, build_ex n)). Definition opt_spc_forwards '(tt : unit) : string := "". @@ -10451,14 +10454,13 @@ returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS)) : mword 56). -Fixpoint walk39 (vaddr : mword 39) (ac : AccessType) (priv : Privilege) (mxr : bool) (do_sum : bool) (ptb : mword 56) '(existT _ level _ : {n : Z & ArithFact (n >= - 0)}) (global : bool) +Fixpoint walk39 (vaddr : mword 39) (ac : AccessType) (priv : Privilege) (mxr : bool) (do_sum : bool) (ptb : mword 56) (level : nat) (global : bool) : M (PTW_Result) := let va := Mk_SV39_Vaddr vaddr in let pt_ofs : paddr39 := shiftl (EXTZ 56 - (subrange_vec_dec (shiftr (_get_SV39_Vaddr_VPNi va) (Z.mul level SV39_LEVEL_BITS)) + (subrange_vec_dec (shiftr (_get_SV39_Vaddr_VPNi va) (Z.mul (Z.of_nat level) SV39_LEVEL_BITS)) (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in let pte_addr := add_vec ptb pt_ofs in (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) => @@ -10471,27 +10473,27 @@ let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true) : mword 1)) in (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE)) : PTW_Result ) else if ((isPTEPtr pbits)) then - (if sumbool_of_bool ((Z.eqb level 0)) then + (match level with O => returnm ((PTW_Failure (PTW_Invalid_PTE)) : PTW_Result ) - else + | S level' => (walk39 vaddr ac priv mxr do_sum (EXTZ 56 (shiftl (_get_SV39_PTE_PPNi pte) PAGESIZE_BITS)) - (build_ex (projT1 (sub_range (build_ex level) (build_ex 1)))) is_global) - : M (PTW_Result)) + level' is_global) + : M (PTW_Result) end) : M (PTW_Result) else (checkPTEPermission ac priv mxr do_sum pattr) >>= fun w__3 : bool => returnm ((if ((negb w__3)) then PTW_Failure (PTW_No_Permission) - else if sumbool_of_bool ((Z.gtb level 0)) then + else if sumbool_of_bool (Nat.ltb O level) then let mask := sub_vec_int (shiftl (xor_vec (_get_SV39_PTE_PPNi pte) (xor_vec (_get_SV39_PTE_PPNi pte) (EXTZ 44 (vec_of_bits [B1] : mword 1)))) - (Z.mul level SV39_LEVEL_BITS)) 1 in + (Z.mul (Z.of_nat level) SV39_LEVEL_BITS)) 1 in if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask) (EXTZ 44 (vec_of_bits [B0] : mword 1)))) then PTW_Failure @@ -10501,10 +10503,10 @@ or_vec (_get_SV39_PTE_PPNi pte) (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in PTW_Success - ((concat_vec ppn (_get_SV39_Vaddr_PgOfs va), pte, pte_addr, build_ex level, is_global)) + ((concat_vec ppn (_get_SV39_Vaddr_PgOfs va), pte, pte_addr, build_ex (Z.of_nat level), is_global)) else PTW_Success - ((concat_vec (_get_SV39_PTE_PPNi pte) (_get_SV39_Vaddr_PgOfs va), pte, pte_addr, build_ex level, is_global))) + ((concat_vec (_get_SV39_PTE_PPNi pte) (_get_SV39_Vaddr_PgOfs va), pte, pte_addr, build_ex (Z.of_nat level), is_global))) : PTW_Result)) : M (PTW_Result) end) @@ -10630,7 +10632,7 @@ : M (TR39_Result) | None => (curPTB39 tt) >>= fun w__6 : mword 56 => - (walk39 vAddr ac priv mxr do_sum w__6 (build_ex level) false) >>= fun w__7 : PTW_Result => + (walk39 vAddr ac priv mxr do_sum w__6 (Z.to_nat level) false) >>= fun w__7 : PTW_Result => (match w__7 with | PTW_Failure (f) => returnm ((TR39_Failure (f)) : TR39_Result ) | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) => @@ -14670,138 +14672,144 @@ returnm (true : bool). -Fixpoint execute (merge_var : ast) -: M (bool) := - match merge_var with +Definition expand_ast (i : ast) : ast := +match i with | C_ADDI4SPN (rdc,nzimm) => let imm : bits 12 := concat_vec (vec_of_bits [B0;B0] : mword 2) (concat_vec nzimm (vec_of_bits [B0;B0] : mword 2)) in let rd := creg2reg_bits rdc in - (execute (ITYPE ((imm, sp, rd, RISCV_ADDI)))) - : M (bool) + ((ITYPE ((imm, sp, rd, RISCV_ADDI)))) + | C_LW (uimm,rsc,rdc) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0] : mword 2)) in let rd := creg2reg_bits rdc in let rs := creg2reg_bits rsc in - (execute (LOAD ((imm, rs, rd, false, WORD, false, false)))) - : M (bool) + ((LOAD ((imm, rs, rd, false, WORD, false, false)))) + | C_LD (uimm,rsc,rdc) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0] : mword 3)) in let rd := creg2reg_bits rdc in let rs := creg2reg_bits rsc in - (execute (LOAD ((imm, rs, rd, false, DOUBLE, false, false)))) - : M (bool) + ((LOAD ((imm, rs, rd, false, DOUBLE, false, false)))) + | C_SW (uimm,rsc1,rsc2) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0] : mword 2)) in let rs1 := creg2reg_bits rsc1 in let rs2 := creg2reg_bits rsc2 in - (execute (STORE ((imm, rs2, rs1, WORD, false, false)))) - : M (bool) + ((STORE ((imm, rs2, rs1, WORD, false, false)))) + | C_SD (uimm,rsc1,rsc2) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0] : mword 3)) in let rs1 := creg2reg_bits rsc1 in let rs2 := creg2reg_bits rsc2 in - (execute (STORE ((imm, rs2, rs1, DOUBLE, false, false)))) - : M (bool) + ((STORE ((imm, rs2, rs1, DOUBLE, false, false)))) + | C_ADDI (nzi,rsd) => let imm : bits 12 := EXTS 12 nzi in - (execute (ITYPE ((imm, rsd, rsd, RISCV_ADDI)))) - : M (bool) + ((ITYPE ((imm, rsd, rsd, RISCV_ADDI)))) + | C_JAL (imm) => - (execute (RISCV_JAL ((EXTS 21 (concat_vec imm (vec_of_bits [B0] : mword 1)), ra)))) - : M (bool) + ((RISCV_JAL ((EXTS 21 (concat_vec imm (vec_of_bits [B0] : mword 1)), ra)))) + | C_LI (imm,rd) => let imm : bits 12 := EXTS 12 imm in - (execute (ITYPE ((imm, zreg, rd, RISCV_ADDI)))) - : M (bool) + ((ITYPE ((imm, zreg, rd, RISCV_ADDI)))) + | C_ADDI16SP (imm) => let imm : bits 12 := EXTS 12 (concat_vec imm (vec_of_bits [B0;B0;B0;B0] : mword 4)) in - (execute (ITYPE ((imm, sp, sp, RISCV_ADDI)))) - : M (bool) + ((ITYPE ((imm, sp, sp, RISCV_ADDI)))) + | C_LUI (imm,rd) => let res : bits 20 := EXTS 20 imm in - (execute (UTYPE ((res, rd, RISCV_LUI)))) - : M (bool) + ((UTYPE ((res, rd, RISCV_LUI)))) + | C_SRLI (shamt,rsd) => let rsd := creg2reg_bits rsd in - (execute (SHIFTIOP ((shamt, rsd, rsd, RISCV_SRLI)))) - : M (bool) + ((SHIFTIOP ((shamt, rsd, rsd, RISCV_SRLI)))) + | C_SRAI (shamt,rsd) => let rsd := creg2reg_bits rsd in - (execute (SHIFTIOP ((shamt, rsd, rsd, RISCV_SRAI)))) - : M (bool) + ((SHIFTIOP ((shamt, rsd, rsd, RISCV_SRAI)))) + | C_ANDI (imm,rsd) => let rsd := creg2reg_bits rsd in - (execute (ITYPE ((EXTS 12 imm, rsd, rsd, RISCV_ANDI)))) - : M (bool) + ((ITYPE ((EXTS 12 imm, rsd, rsd, RISCV_ANDI)))) + | C_SUB (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPE ((rs2, rsd, rsd, RISCV_SUB)))) - : M (bool) + ((RTYPE ((rs2, rsd, rsd, RISCV_SUB)))) + | C_XOR (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPE ((rs2, rsd, rsd, RISCV_XOR)))) - : M (bool) + ((RTYPE ((rs2, rsd, rsd, RISCV_XOR)))) + | C_OR (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPE ((rs2, rsd, rsd, RISCV_OR)))) - : M (bool) + ((RTYPE ((rs2, rsd, rsd, RISCV_OR)))) + | C_AND (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPE ((rs2, rsd, rsd, RISCV_AND)))) - : M (bool) + ((RTYPE ((rs2, rsd, rsd, RISCV_AND)))) + | C_SUBW (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPEW ((rs2, rsd, rsd, RISCV_SUBW)))) - : M (bool) + ((RTYPEW ((rs2, rsd, rsd, RISCV_SUBW)))) + | C_ADDW (rsd,rs2) => let rsd := creg2reg_bits rsd in let rs2 := creg2reg_bits rs2 in - (execute (RTYPEW ((rs2, rsd, rsd, RISCV_ADDW)))) - : M (bool) + ((RTYPEW ((rs2, rsd, rsd, RISCV_ADDW)))) + | C_J (imm) => - (execute (RISCV_JAL ((EXTS 21 (concat_vec imm (vec_of_bits [B0] : mword 1)), zreg)))) - : M (bool) + ((RISCV_JAL ((EXTS 21 (concat_vec imm (vec_of_bits [B0] : mword 1)), zreg)))) + | C_BEQZ (imm,rs) => - (execute + ( (BTYPE ((EXTS 13 (concat_vec imm (vec_of_bits [B0] : mword 1)), zreg, creg2reg_bits rs, RISCV_BEQ)))) - : M (bool) + | C_BNEZ (imm,rs) => - (execute + ( (BTYPE ((EXTS 13 (concat_vec imm (vec_of_bits [B0] : mword 1)), zreg, creg2reg_bits rs, RISCV_BNE)))) - : M (bool) - | C_SLLI (shamt,rsd) => (execute (SHIFTIOP ((shamt, rsd, rsd, RISCV_SLLI)))) : M (bool) + + | C_SLLI (shamt,rsd) => ((SHIFTIOP ((shamt, rsd, rsd, RISCV_SLLI)))) | C_LWSP (uimm,rd) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0] : mword 2)) in - (execute (LOAD ((imm, sp, rd, false, WORD, false, false)))) - : M (bool) + ((LOAD ((imm, sp, rd, false, WORD, false, false)))) + | C_LDSP (uimm,rd) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0] : mword 3)) in - (execute (LOAD ((imm, sp, rd, false, DOUBLE, false, false)))) - : M (bool) + ((LOAD ((imm, sp, rd, false, DOUBLE, false, false)))) + | C_SWSP (uimm,rs2) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0] : mword 2)) in - (execute (STORE ((imm, rs2, sp, WORD, false, false)))) - : M (bool) + ((STORE ((imm, rs2, sp, WORD, false, false)))) + | C_SDSP (uimm,rs2) => let imm : bits 12 := EXTZ 12 (concat_vec uimm (vec_of_bits [B0;B0;B0] : mword 3)) in - (execute (STORE ((imm, rs2, sp, DOUBLE, false, false)))) - : M (bool) + ((STORE ((imm, rs2, sp, DOUBLE, false, false)))) + | C_JR (rs1) => - (execute (RISCV_JALR ((EXTZ 12 (vec_of_bits [B0] : mword 1), rs1, zreg)))) : M (bool) + ((RISCV_JALR ((EXTZ 12 (vec_of_bits [B0] : mword 1), rs1, zreg)))) | C_JALR (rs1) => - (execute (RISCV_JALR ((EXTZ 12 (vec_of_bits [B0] : mword 1), rs1, ra)))) : M (bool) - | C_MV (rd,rs2) => (execute (RTYPE ((rs2, zreg, rd, RISCV_ADD)))) : M (bool) - | C_EBREAK (tt) => (execute (EBREAK (tt))) : M (bool) - | C_ADD (rsd,rs2) => (execute (RTYPE ((rs2, rsd, rsd, RISCV_ADD)))) : M (bool) + ((RISCV_JALR ((EXTZ 12 (vec_of_bits [B0] : mword 1), rs1, ra)))) + | C_MV (rd,rs2) => ((RTYPE ((rs2, zreg, rd, RISCV_ADD)))) + | C_EBREAK (tt) => ((EBREAK (tt))) + | C_ADD (rsd,rs2) => ((RTYPE ((rs2, rsd, rsd, RISCV_ADD)))) +| i => i +end. + +Fixpoint execute (merge_var : ast) +: M (bool) := +let merge_var := expand_ast merge_var in + match merge_var with | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op) : M (bool) | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd) : M (bool) | BTYPE (imm,rs2,rs1,op) => (execute_BTYPE imm rs2 rs1 op) : M (bool) @@ -14841,6 +14849,7 @@ | ILLEGAL (s) => (execute_ILLEGAL s) : M (bool) | C_ILLEGAL (s) => (execute_C_ILLEGAL s) : M (bool) | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd) : M (bool) +| _ => Fail "Unexpanded instruction" end. Definition assembly_forwards (arg_ : ast) @@ -35883,7 +35892,7 @@ returnm (stepped : bool). -Definition loop '(tt : unit) +(*Definition loop '(tt : unit) : M (unit) := let insns_per_tick := plat_insns_per_tick tt in let i : Z := 0 in @@ -35923,7 +35932,7 @@ : M (Z)) >>= fun i : Z => returnm (i, step_no))) >>= fun '(i, step_no) => returnm (tt - : unit). + : unit).*) Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} : read_kind :=