summaryrefslogtreecommitdiff
path: root/riscv
diff options
context:
space:
mode:
Diffstat (limited to 'riscv')
-rw-r--r--riscv/coq.patch58
1 files changed, 29 insertions, 29 deletions
diff --git a/riscv/coq.patch b/riscv/coq.patch
index cd7ad6b3..51db9e6c 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,6 @@
---- riscv.v.orig 2018-08-15 11:35:48.766557392 +0100
-+++ riscv.v 2018-08-15 11:36:59.395492502 +0100
-@@ -7712,14 +7712,13 @@
+--- riscv.v.orig 2018-08-16 12:28:27.055298575 +0100
++++ riscv.v 2018-08-16 13:23:19.684380827 +0100
+@@ -7706,14 +7706,13 @@
returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
: mword 56).
@@ -17,14 +17,14 @@
(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 64) =>
-@@ -7732,26 +7731,26 @@
+@@ -7726,26 +7725,26 @@
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)
+ (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 =>
++ (match level with O =>
returnm ((PTW_Failure PTW_Invalid_PTE)
- : PTW_Result)
+ : PTW_Result )
- else
+ | S level' =>
(walk39 vaddr ac priv mxr do_sum
@@ -50,7 +50,7 @@
if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
(EXTZ 44 (vec_of_bits [B0] : mword 1)))) then
PTW_Failure PTW_Misaligned
-@@ -7760,15 +7759,18 @@
+@@ -7754,15 +7753,18 @@
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
@@ -71,17 +71,17 @@
Definition make_TLB39_Entry (asid : mword 16) (global : bool) (vAddr : mword 39) (pAddr : mword 56) (pte : SV39_PTE) '((existT _ level _) : {n : Z & ArithFact (n >=
0)}) (pteAddr : mword 56)
: M (TLB39_Entry) :=
-@@ -7884,7 +7886,7 @@
+@@ -7878,7 +7880,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_Failure (f) => returnm ((TR39_Failure f) : TR39_Result )
| PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -7961,7 +7963,7 @@
- | Sbare => returnm ((TR_Address vAddr) : TR_Result)
+@@ -7955,7 +7957,7 @@
+ | Sbare => returnm ((TR_Address vAddr) : TR_Result )
| SV39 =>
translate39 (subrange_vec_dec vAddr 38 0) ac effPriv mxr do_sum
- (build_ex (projT1 (sub_range (build_ex SV39_LEVELS) (build_ex 1)))) >>= fun w__7 : TR39_Result =>
@@ -89,7 +89,7 @@
returnm ((match w__7 with
| TR39_Address (pa) => TR_Address (EXTZ 64 pa)
| TR39_Failure (f) => TR_Failure (translationException ac f)
-@@ -10867,11 +10869,11 @@
+@@ -10861,11 +10863,11 @@
(match width with
| WORD =>
mem_read addr 4 aq rl true >>= fun w__2 : MemoryOpResult (mword 32) =>
@@ -103,7 +103,7 @@
: M (bool)
| _ => (internal_error "LOADRES expected WORD or DOUBLE") : M (bool)
end)
-@@ -10894,19 +10896,19 @@
+@@ -10888,19 +10890,19 @@
(match width with
| BYTE =>
mem_read addr 1 aq rl false >>= fun w__3 : MemoryOpResult (mword 8) =>
@@ -127,7 +127,7 @@
: M (bool)
end)
: M (bool)
-@@ -11023,7 +11025,7 @@
+@@ -11017,7 +11019,7 @@
if sumbool_of_bool ((andb s
(Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1))))))
then
@@ -136,21 +136,21 @@
else q in
wX (projT1 ((regbits_to_regno rd) : {n : Z & ArithFact (0 <= n /\ (n + 1) <= 32)}))
(EXTS 64 (to_bits 32 q')) >>
-@@ -11127,11 +11129,11 @@
+@@ -11121,11 +11123,11 @@
match width with
| WORD =>
mem_read addr 4 aq (andb aq rl) true >>= fun w__4 : MemoryOpResult (mword 32) =>
- returnm ((extend_value false w__4)
+ returnm ((extend_value (n := 4) false w__4)
- : MemoryOpResult xlenbits)
+ : MemoryOpResult (mword 64))
| DOUBLE =>
mem_read addr 8 aq (andb aq rl) true >>= fun w__5 : MemoryOpResult (mword 64) =>
- returnm ((extend_value false w__5)
+ returnm ((extend_value (n := 8) false w__5)
- : MemoryOpResult xlenbits)
- | _ => (internal_error "AMO expected WORD or DOUBLE") : M (MemoryOpResult xlenbits)
+ : MemoryOpResult (mword 64))
+ | _ => (internal_error "AMO expected WORD or DOUBLE") : M (MemoryOpResult (mword 64))
end >>= fun rval : MemoryOpResult xlenbits =>
-@@ -11193,134 +11195,140 @@
+@@ -11187,134 +11189,140 @@
returnm (true
: bool).
@@ -350,7 +350,7 @@
| 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)
-@@ -11360,6 +11368,7 @@
+@@ -11354,6 +11362,7 @@
| THREAD_START (g__29) => returnm ((execute_THREAD_START g__29) : bool)
| ILLEGAL (s) => (execute_ILLEGAL s) : M (bool)
| C_ILLEGAL (g__30) => (execute_C_ILLEGAL g__30) : M (bool)
@@ -358,7 +358,7 @@
end.
Definition assembly_forwards (arg_ : ast)
-@@ -11622,7 +11631,7 @@
+@@ -11616,7 +11625,7 @@
| _ => exit tt : M (string)
end)
: M (string).
@@ -367,7 +367,7 @@
Definition assembly_backwards (arg_ : string)
: M (ast) :=
let _stringappend_1112_ := arg_ in
-@@ -29689,7 +29698,7 @@
+@@ -29684,7 +29693,7 @@
: M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
: M (option ((ast * {n : Z & ArithFact (n >= 0)}))))
: M (option ((ast * {n : Z & ArithFact (n >= 0)}))).
@@ -376,7 +376,7 @@
Definition encdec_forwards (arg_ : ast)
: M (mword 32) :=
(match arg_ with
-@@ -31899,7 +31908,7 @@
+@@ -31894,7 +31903,7 @@
: M ((bool * bool))
end)
: M ((bool * bool)).
@@ -385,7 +385,7 @@
Definition loop '(tt : unit)
: M (unit) :=
let insns_per_tick := plat_insns_per_tick tt in
-@@ -31938,7 +31947,7 @@
+@@ -31936,7 +31945,7 @@
returnm (i, step_no))) >>= fun '(i, step_no) =>
returnm (tt
: unit).
@@ -394,7 +394,7 @@
Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)}
: read_kind :=
let p0_ := arg_ in
-@@ -32029,7 +32038,7 @@
+@@ -32027,7 +32036,7 @@
else if sumbool_of_bool ((Z.eqb p0_ 20)) then Barrier_RISCV_w_r
else if sumbool_of_bool ((Z.eqb p0_ 21)) then Barrier_RISCV_i
else Barrier_x86_MFENCE.
@@ -403,7 +403,7 @@
Definition num_of_barrier_kind (arg_ : barrier_kind)
: {e : Z & ArithFact (0 <= e /\ e <= 22)} :=
match arg_ with
-@@ -32057,7 +32066,7 @@
+@@ -32055,7 +32064,7 @@
| Barrier_RISCV_i => build_ex 21
| Barrier_x86_MFENCE => build_ex 22
end.
@@ -412,7 +412,7 @@
Definition trans_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)}
: trans_kind :=
let p0_ := arg_ in
-@@ -32078,6 +32087,7 @@
+@@ -32076,6 +32085,7 @@
"x10";"x9";"x8";"x7";"x6";"x5";"x4";"x3";"x2";"x1";"x0"].
Let CIA_fp := RFull "CIA".
Let NIA_fp := RFull "NIA".
@@ -420,7 +420,7 @@
Definition initial_analysis (instr : ast)
: M ((list regfp * list regfp * list regfp * list niafp * diafp * instruction_kind)) :=
let iR := [] : regfps in
-@@ -32602,7 +32612,7 @@
+@@ -32600,7 +32610,7 @@
end >>= fun '(Nias, aR, iR, ik, oR) =>
returnm ((iR, oR, aR, Nias, Dia, ik)
: (list regfp * list regfp * list regfp * list niafp * diafp * instruction_kind)).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:04:50 +0000