diff options
Diffstat (limited to 'riscv/coq.patch')
| -rw-r--r-- | riscv/coq.patch | 431 |
1 files changed, 431 insertions, 0 deletions
diff --git a/riscv/coq.patch b/riscv/coq.patch new file mode 100644 index 00000000..cd7ad6b3 --- /dev/null +++ b/riscv/coq.patch @@ -0,0 +1,431 @@ +--- 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 @@ + 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 64) => +@@ -7732,26 +7731,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) + 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 PTW_Misaligned +@@ -7760,15 +7759,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 +- level,is_global) ++ (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)) ++ (Z.of_nat level),is_global)) + : PTW_Result)) + : M (PTW_Result) + end) + : M (PTW_Result). + ++Hint Unfold PAGESIZE_BITS : sail. ++Hint Unfold SV39_LEVEL_BITS : sail. ++ + 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 @@ + : 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) => +@@ -7961,7 +7963,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 => ++ (build_ex ( (Z.sub ( SV39_LEVELS) ( 1)))) >>= fun w__7 : TR39_Result => + 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 @@ + (match width with + | WORD => + mem_read addr 4 aq rl true >>= fun w__2 : MemoryOpResult (mword 32) => +- (process_loadres rd vaddr w__2 false) ++ (process_loadres (n := 4) rd vaddr w__2 false) + : M (bool) + | DOUBLE => + mem_read addr 8 aq rl true >>= fun w__4 : MemoryOpResult (mword 64) => +- (process_loadres rd vaddr w__4 false) ++ (process_loadres (n := 8) rd vaddr w__4 false) + : M (bool) + | _ => (internal_error "LOADRES expected WORD or DOUBLE") : M (bool) + end) +@@ -10894,19 +10896,19 @@ + (match width with + | BYTE => + mem_read addr 1 aq rl false >>= fun w__3 : MemoryOpResult (mword 8) => +- (process_load rd vaddr w__3 is_unsigned) ++ (process_load (n := 1) rd vaddr w__3 is_unsigned) + : M (bool) + | HALF => + mem_read addr 2 aq rl false >>= fun w__5 : MemoryOpResult (mword 16) => +- (process_load rd vaddr w__5 is_unsigned) ++ (process_load (n := 2) rd vaddr w__5 is_unsigned) + : M (bool) + | WORD => + mem_read addr 4 aq rl false >>= fun w__7 : MemoryOpResult (mword 32) => +- (process_load rd vaddr w__7 is_unsigned) ++ (process_load (n := 4) rd vaddr w__7 is_unsigned) + : M (bool) + | DOUBLE => + mem_read addr 8 aq rl false >>= fun w__9 : MemoryOpResult (mword 64) => +- (process_load rd vaddr w__9 is_unsigned) ++ (process_load (n := 8) rd vaddr w__9 is_unsigned) + : M (bool) + end) + : M (bool) +@@ -11023,7 +11025,7 @@ + if sumbool_of_bool ((andb s + (Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1)))))) + then +- projT1 (sub_range (build_ex 0) ((ex_int (pow 2 31)) : {n : Z & ArithFact (True)})) ++ (Z.sub ( 0) ((pow 2 31))) + 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 @@ + 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) + | 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) + end >>= fun rval : MemoryOpResult xlenbits => +@@ -11193,134 +11195,140 @@ + 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 ++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) +@@ -11360,6 +11368,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) ++| _ => Fail "Unexpanded instruction" + end. + + Definition assembly_forwards (arg_ : ast) +@@ -11622,7 +11631,7 @@ + | _ => exit tt : M (string) + end) + : M (string). +- ++(* + Definition assembly_backwards (arg_ : string) + : M (ast) := + let _stringappend_1112_ := arg_ in +@@ -29689,7 +29698,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)}))). +- ++*) + Definition encdec_forwards (arg_ : ast) + : M (mword 32) := + (match arg_ with +@@ -31899,7 +31908,7 @@ + : M ((bool * bool)) + end) + : M ((bool * bool)). +- ++(* + Definition loop '(tt : unit) + : M (unit) := + let insns_per_tick := plat_insns_per_tick tt in +@@ -31938,7 +31947,7 @@ + returnm (i, step_no))) >>= fun '(i, step_no) => + returnm (tt + : unit). +- ++*) + Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} + : read_kind := + let p0_ := arg_ in +@@ -32029,7 +32038,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. +- ++(* + Definition num_of_barrier_kind (arg_ : barrier_kind) + : {e : Z & ArithFact (0 <= e /\ e <= 22)} := + match arg_ with +@@ -32057,7 +32066,7 @@ + | Barrier_RISCV_i => build_ex 21 + | Barrier_x86_MFENCE => build_ex 22 + end. +- ++*) + Definition trans_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 2)} + : trans_kind := + let p0_ := arg_ in +@@ -32078,6 +32087,7 @@ + "x10";"x9";"x8";"x7";"x6";"x5";"x4";"x3";"x2";"x1";"x0"]. + Let CIA_fp := RFull "CIA". + Let NIA_fp := RFull "NIA". ++(* + 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 @@ + 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)). +- ++*) + Let initial_regstate : regstate := + {| tlb39 := None; + htif_exit_code := |