summaryrefslogtreecommitdiff
path: root/riscv/coq.patch
diff options
context:
space:
mode:
Diffstat (limited to 'riscv/coq.patch')
-rw-r--r--riscv/coq.patch334
1 files changed, 0 insertions, 334 deletions
diff --git a/riscv/coq.patch b/riscv/coq.patch
deleted file mode 100644
index 6c40e6e2..00000000
--- a/riscv/coq.patch
+++ /dev/null
@@ -1,334 +0,0 @@
---- riscv.v 2018-10-22 18:20:01.512785981 +0100
-+++ riscv.v.good 2018-10-22 18:19:27.556562080 +0100
-@@ -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 := "".
-
-@@ -10432,14 +10435,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)) =>
-@@ -10452,27 +10454,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
-@@ -10482,10 +10484,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)
-@@ -10611,7 +10613,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) =>
-@@ -14651,137 +14653,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_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_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)
- | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd) : M (bool)
-@@ -14821,6 +14830,7 @@
- | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0) : bool)
- | ILLEGAL (s) => (execute_ILLEGAL s) : M (bool)
- | C_ILLEGAL (s) => (execute_C_ILLEGAL s) : M (bool)
-+| _ => Fail "Unexpanded instruction"
- end.
-
- Definition assembly_forwards (arg_ : ast)
-@@ -35792,7 +35802,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
-@@ -35832,7 +35842,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 :=
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:44:15 +0000