diff options
Diffstat (limited to 'riscv/coq.patch')
| -rw-r--r-- | riscv/coq.patch | 43 |
1 files changed, 20 insertions, 23 deletions
diff --git a/riscv/coq.patch b/riscv/coq.patch index 9ee0fc71..149c60ff 100644 --- a/riscv/coq.patch +++ b/riscv/coq.patch @@ -1,14 +1,11 @@ ---- riscv.v.plain 2018-09-06 11:57:47.900156894 +0100 -+++ riscv.v 2018-09-06 11:57:50.244172679 +0100 -@@ -8383,14 +8383,16 @@ +--- riscv.v.plain 2018-09-12 17:53:51.151611265 +0100 ++++ riscv.v 2018-09-12 17:57:47.097406204 +0100 +@@ -8336,14 +8336,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) -+Hint Unfold PAGESIZE_BITS : sail. -+Hint Unfold SV39_LEVEL_BITS : sail. -+ +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 @@ -19,8 +16,8 @@ + (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)) => -@@ -8403,27 +8405,27 @@ + (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) => +@@ -8356,27 +8355,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 @@ -39,7 +36,7 @@ + : M (PTW_Result) end) : M (PTW_Result) else - checkPTEPermission ac priv mxr do_sum pattr >>= fun w__3 : bool => + (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 @@ -54,7 +51,7 @@ if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask) (EXTZ 44 (vec_of_bits [B0] : mword 1)))) then PTW_Failure -@@ -8433,12 +8435,12 @@ +@@ -8386,12 +8385,12 @@ or_vec (_get_SV39_PTE_PPNi pte) (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in PTW_Success @@ -69,16 +66,16 @@ : PTW_Result)) : M (PTW_Result) end) -@@ -8564,7 +8566,7 @@ +@@ -8517,7 +8516,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 => + (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) => -@@ -12339,138 +12341,144 @@ +@@ -12279,138 +12278,144 @@ returnm (true : bool). @@ -282,7 +279,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) -@@ -12510,6 +12518,7 @@ +@@ -12450,6 +12455,7 @@ | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0) : bool) | ILLEGAL (s) => (execute_ILLEGAL s) : M (bool) | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0) : M (bool) @@ -290,7 +287,7 @@ end. Definition assembly_forwards (arg_ : ast) -@@ -12772,7 +12781,7 @@ +@@ -12712,7 +12718,7 @@ | _ => exit tt : M (string) end) : M (string). @@ -299,7 +296,7 @@ Definition assembly_backwards (arg_ : string) : M (ast) := let _stringappend_756_ := arg_ in -@@ -27038,7 +27047,7 @@ +@@ -27199,7 +27205,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)}))). @@ -308,16 +305,16 @@ Definition encdec_forwards (arg_ : ast) : M (mword 32) := (match arg_ with -@@ -29126,7 +29135,7 @@ - : M ((bool * bool)) - end) - : M ((bool * bool)). +@@ -29293,7 +29299,7 @@ + else returnm (tt : unit)) >> + returnm (stepped + : bool). - +(* Definition loop '(tt : unit) : M (unit) := let insns_per_tick := plat_insns_per_tick tt in -@@ -29173,7 +29182,7 @@ +@@ -29335,7 +29341,7 @@ returnm (i, step_no))) >>= fun '(i, step_no) => returnm (tt : unit). |