diff options
| -rw-r--r-- | aarch64/aarch64_extras.v | 10 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 3 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 69 | ||||
| -rw-r--r-- | mips/mips_extras.v | 6 | ||||
| -rw-r--r-- | riscv/coq.patch | 331 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 407 |
6 files changed, 530 insertions, 296 deletions
diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v index 94851ef5..67d165cd 100644 --- a/aarch64/aarch64_extras.v +++ b/aarch64/aarch64_extras.v @@ -133,4 +133,12 @@ Definition read_ram {rv e} addrsize size `{ArithFact (size >= 0)} (hexRAM : mwor (*val elf_entry : unit -> integer*) Definition elf_entry (_:unit) := 0. (*declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` -*)
\ No newline at end of file +*) + +Lemma mul_quot_8_helper : forall x, 8 * x = 8 * (Z.quot (8 * x) 8). +intro. +rewrite Z.mul_comm. +rewrite Z.quot_mul; auto with zarith. +Qed. +Hint Resolve mul_quot_8_helper : sail. + diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 0b3a2cd8..0f2c0955 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -125,3 +125,6 @@ Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e := x >>= fun y => returnm (projT1 y). +Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := + x >>= fun y => returnm (build_ex (projT1 y)). + diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index def6e248..39fbf247 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -61,14 +61,14 @@ Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) := (* Project away range constraints in comparisons *) -Definition ltb_range_l {P} (l : sigT P) r := Z.ltb (projT1 l) r. -Definition leb_range_l {P} (l : sigT P) r := Z.leb (projT1 l) r. -Definition gtb_range_l {P} (l : sigT P) r := Z.gtb (projT1 l) r. -Definition geb_range_l {P} (l : sigT P) r := Z.geb (projT1 l) r. -Definition ltb_range_r {P} l (r : sigT P) := Z.ltb l (projT1 r). -Definition leb_range_r {P} l (r : sigT P) := Z.leb l (projT1 r). -Definition gtb_range_r {P} l (r : sigT P) := Z.gtb l (projT1 r). -Definition geb_range_r {P} l (r : sigT P) := Z.geb l (projT1 r). +Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r. +Definition leb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.leb (projT1 l) r. +Definition gtb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.gtb (projT1 l) r. +Definition geb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.geb (projT1 l) r. +Definition ltb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.ltb l (projT1 r). +Definition leb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.leb l (projT1 r). +Definition gtb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.gtb l (projT1 r). +Definition geb_range_r {lo hi} l (r : {x & ArithFact (lo <= x /\ x <= hi)}) := Z.geb l (projT1 r). Definition ii := Z. Definition nn := nat. @@ -977,11 +977,28 @@ Ltac unbool_comparisons := (* Split up dependent pairs to get at proofs of properties *) Ltac extract_properties := + (* Properties of local definitions *) repeat match goal with H := (projT1 ?X) |- _ => let x := fresh "x" in let Hx := fresh "Hx" in destruct X as [x Hx] in *; change (projT1 (existT _ x Hx)) with x in *; unfold H in * end; + (* Properties with proofs embedded by build_ex; uses revert/generalize + rather than destruct because it seemed to be more efficient, but + some experimentation would be needed to be sure. *) + repeat ( + match goal with H:context [@build_ex ?T ?n ?P ?prf] |- _ => + let x := fresh "x" in + let zz := constr:(@build_ex T n P prf) in + revert dependent H(*; generalize zz; intros*) + end; + match goal with |- context [@build_ex ?T ?n ?P ?prf] => + let x := fresh "x" in + let zz := constr:(@build_ex T n P prf) in + generalize zz as x + end; + intros); + (* Other properties in the goal *) repeat match goal with |- context [projT1 ?X] => let x := fresh "x" in let Hx := fresh "Hx" in @@ -1008,6 +1025,10 @@ Ltac dump_context := | H:=?X |- _ => idtac H ":=" X; fail | H:?X |- _ => idtac H ":" X; fail end; match goal with |- ?X => idtac "Goal:" X end. +Ltac split_cases := + repeat match goal with + |- context [match ?X with _ => _ end] => destruct X + end. Ltac prepare_for_solver := (*dump_context;*) clear_irrelevant_defns; @@ -1019,21 +1040,39 @@ Ltac prepare_for_solver := autounfold with sail in * |- *; (* You can add Hint Unfold ... : sail to let omega see through fns *) unbool_comparisons; reduce_list_lengths; - reduce_pow. + reduce_pow; + split_cases. + +Lemma trivial_range {x : Z} : ArithFact (x <= x /\ x <= x). +constructor. +auto with zarith. +Qed. + +Lemma ArithFact_self_proof {P} : forall x : {y : Z & ArithFact (P y)}, ArithFact (P (projT1 x)). +intros [x H]. +exact H. +Qed. + +Ltac fill_in_evar_eq := + match goal with |- ArithFact (?x = ?y) => + (is_evar x || is_evar y); + (* compute to allow projections to remove proofs that might not be allowed in the evar *) +(* Disabled because cbn may reduce definitions, even after clearbody + let x := eval cbn in x in + let y := eval cbn in y in*) + idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end. + Ltac solve_arithfact := (* Attempt a simple proof first to avoid lengthy preparation steps (especially as the large proof terms can upset subsequent proofs). *) +intros; (* To solve implications for derive_m *) +try fill_in_evar_eq; +try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end; try (constructor; omega); prepare_for_solver; (*dump_context;*) solve [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end - | match goal with |- ArithFact (?x = ?y) => - (is_evar x || is_evar y); - (* compute to allow projections to remove proofs that might not be allowed in the evar *) - let x := eval cbn in x in - let y := eval cbn in y in - idtac "Warning: unknown equality constraint"; constructor; exact (eq_refl _ : x = y) end | apply ArithFact_mword; assumption | constructor; omega with Z (* The datatypes hints give us some list handling, esp In *) diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 51856d9e..83f39079 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -161,6 +161,12 @@ Definition putchar {T} (_:T) : unit := tt. Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). +Lemma __MIPS_read_lemma : forall width, 8 * width = 8 * (8 * width ÷ 8). +intros. +rewrite Z.mul_comm. +rewrite Z.quot_mul; auto with zarith. +Qed. +Hint Resolve __MIPS_read_lemma : sail. Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8). intros. diff --git a/riscv/coq.patch b/riscv/coq.patch index 51db9e6c..f8d35782 100644 --- a/riscv/coq.patch +++ b/riscv/coq.patch @@ -1,11 +1,14 @@ ---- 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 @@ +--- riscv.v.plain 2018-08-29 16:46:33.534052809 +0100 ++++ riscv.v 2018-08-29 16:48:44.854865657 +0100 +@@ -8409,14 +8409,16 @@ 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 >= +-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 @@ -17,13 +20,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) => -@@ -7726,26 +7725,26 @@ +@@ -8429,27 +8431,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 ) + (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) + returnm ((PTW_Failure + (PTW_Invalid_PTE)) : PTW_Result ) - else + | S level' => @@ -36,7 +40,7 @@ : 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 + 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 := @@ -49,39 +53,33 @@ + (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 -@@ -7754,15 +7753,18 @@ + PTW_Failure +@@ -8459,12 +8461,12 @@ 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) + PTW_Success +- (concat_vec ppn (_get_SV39_Vaddr_PgOfs va), pte, pte_addr, build_ex level, ++ (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)) -+ (Z.of_nat level),is_global)) + PTW_Success + (concat_vec (_get_SV39_PTE_PPNi pte) (_get_SV39_Vaddr_PgOfs va), pte, +- pte_addr, build_ex level, is_global)) ++ pte_addr, build_ex (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) := -@@ -7878,7 +7880,7 @@ +@@ -8590,7 +8592,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) => -@@ -7955,7 +7957,7 @@ - | Sbare => returnm ((TR_Address vAddr) : TR_Result ) +@@ -8670,7 +8672,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 +87,55 @@ returnm ((match w__7 with | TR39_Address (pa) => TR_Address (EXTZ 64 pa) | TR39_Failure (f) => TR_Failure (translationException ac f) -@@ -10861,11 +10863,11 @@ +@@ -11523,7 +11525,7 @@ + (tt)) + else None. + +-Fixpoint execute_WFI '(tt : unit) ++Definition execute_WFI '(tt : unit) + : M (bool) := + read_reg cur_privilege_ref >>= fun w__0 : Privilege => + (match w__0 with +@@ -11555,7 +11557,7 @@ + returnm (true + : bool). + +-Fixpoint execute_THREAD_START '(tt : unit) : bool := true. ++Definition execute_THREAD_START '(tt : unit) : bool := true. + + Fixpoint execute_STORECON (aq : bool) (rl : bool) (rs2 : mword 5) (rs1 : mword 5) (width : word_width) (rd : mword 5) + : M (bool) := +@@ -11684,9 +11686,9 @@ + : M (bool)) + : M (bool). + +-Fixpoint execute_STOP_FETCHING '(tt : unit) : bool := true. ++Definition execute_STOP_FETCHING '(tt : unit) : bool := true. + +-Fixpoint execute_SRET '(tt : unit) ++Definition execute_SRET '(tt : unit) + : M (bool) := + read_reg cur_privilege_ref >>= fun w__0 : Privilege => + match w__0 with +@@ -11930,7 +11932,7 @@ + returnm (true + : bool). + +-Fixpoint execute_NOP '(tt : unit) : bool := true. ++Definition execute_NOP '(tt : unit) : bool := true. + + Fixpoint execute_MULW (rs2 : mword 5) (rs1 : mword 5) (rd : mword 5) + : M (bool) := +@@ -11972,7 +11974,7 @@ + returnm (true + : bool). + +-Fixpoint execute_MRET '(tt : unit) ++Definition execute_MRET '(tt : unit) + : M (bool) := + read_reg cur_privilege_ref >>= fun w__0 : Privilege => + (if ((eq_vec ((privLevel_to_bits w__0) : mword 2) ((privLevel_to_bits Machine) : mword 2))) +@@ -12011,11 +12013,11 @@ (match width with | WORD => mem_read addr 4 aq rl true >>= fun w__2 : MemoryOpResult (mword 32) => @@ -103,7 +149,7 @@ : M (bool) | _ => (internal_error "LOADRES expected WORD or DOUBLE") : M (bool) end) -@@ -10888,19 +10890,19 @@ +@@ -12040,19 +12042,19 @@ (match width with | BYTE => mem_read addr 1 aq rl false >>= fun w__3 : MemoryOpResult (mword 8) => @@ -127,16 +173,54 @@ : M (bool) end) : M (bool) -@@ -11017,7 +11019,7 @@ +@@ -12083,7 +12085,7 @@ + + Fixpoint execute_ILLEGAL (s : mword 32) : M (bool) := handle_illegal tt >> returnm (false : bool). + +-Fixpoint execute_FENCEI '(tt : unit) : bool := true. ++Definition execute_FENCEI '(tt : unit) : bool := true. + + Fixpoint execute_FENCE (pred : mword 4) (succ : mword 4) + : M (bool) := +@@ -12139,7 +12141,7 @@ + returnm (true + : bool). + +-Fixpoint execute_ECALL '(tt : unit) ++Definition execute_ECALL '(tt : unit) + : M (bool) := + read_reg cur_privilege_ref >>= fun w__0 : Privilege => + let t : sync_exception := +@@ -12155,7 +12157,7 @@ + handle_exception w__1 (CTL_TRAP (t)) w__2 >>= fun w__3 : mword 64 => + write_reg nextPC_ref w__3 >> returnm (false : bool). + +-Fixpoint execute_EBREAK '(tt : unit) ++Definition execute_EBREAK '(tt : unit) + : M (bool) := + (read_reg PC_ref : M (mword 64)) >>= fun w__0 : xlenbits => + handle_mem_exception w__0 E_Breakpoint >> returnm (false : bool). +@@ -12177,8 +12179,8 @@ 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))) +- projT1 (sub_range (build_ex 0) +- (build_ex (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) ++ (Z.sub ( 0) ++ ( (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) + : {n : Z & ArithFact (True)})))) else q in - wX (projT1 ((regbits_to_regno rd) : {n : Z & ArithFact (0 <= n /\ (n + 1) <= 32)})) - (EXTS 64 (to_bits 32 q')) >> -@@ -11121,11 +11123,11 @@ + wX +@@ -12205,7 +12207,7 @@ + returnm (true + : bool). + +-Fixpoint execute_C_ILLEGAL '(tt : unit) : M (bool) := handle_illegal tt >> returnm (false : bool). ++Definition execute_C_ILLEGAL '(tt : unit) : M (bool) := handle_illegal tt >> returnm (false : bool). + + Fixpoint execute_C_ADDIW (imm : mword 6) (rsd : mword 5) + : M (bool) := +@@ -12300,11 +12302,11 @@ match width with | WORD => mem_read addr 4 aq (andb aq rl) true >>= fun w__4 : MemoryOpResult (mword 32) => @@ -150,7 +234,7 @@ : MemoryOpResult (mword 64)) | _ => (internal_error "AMO expected WORD or DOUBLE") : M (MemoryOpResult (mword 64)) end >>= fun rval : MemoryOpResult xlenbits => -@@ -11187,134 +11189,140 @@ +@@ -12371,138 +12373,144 @@ returnm (true : bool). @@ -164,183 +248,187 @@ 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))) +- (execute (ITYPE (imm, sp, rd, RISCV_ADDI))) - : M (bool) -+ ( (ITYPE (imm,sp,rd,RISCV_ADDI))) ++ ( (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))) +- (execute (LOAD (imm, rs, rd, false, WORD, false, false))) - : M (bool) -+ ( (LOAD (imm,rs,rd,false,WORD,false,false))) ++ ( (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))) +- (execute (LOAD (imm, rs, rd, false, DOUBLE, false, false))) - : M (bool) -+ ( (LOAD (imm,rs,rd,false,DOUBLE,false,false))) ++ ( (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))) +- (execute (STORE (imm, rs2, rs1, WORD, false, false))) - : M (bool) -+ ( (STORE (imm,rs2,rs1,WORD,false,false))) ++ ( (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))) +- (execute (STORE (imm, rs2, rs1, DOUBLE, false, false))) - : M (bool) -+ ( (STORE (imm,rs2,rs1,DOUBLE,false,false))) ++ ( (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))) +- (execute (ITYPE (imm, rsd, rsd, RISCV_ADDI))) - : M (bool) -+ ( (ITYPE (imm,rsd,rsd,RISCV_ADDI))) ++ ( (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))) +- (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))) +- (execute (ITYPE (imm, zreg, rd, RISCV_ADDI))) - : M (bool) -+ ( (ITYPE (imm,zreg,rd,RISCV_ADDI))) ++ ( (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))) +- (execute (ITYPE (imm, sp, sp, RISCV_ADDI))) - : M (bool) -+ ( (ITYPE (imm,sp,sp,RISCV_ADDI))) ++ ( (ITYPE (imm, sp, sp, RISCV_ADDI))) + | C_LUI (imm,rd) => let res : bits 20 := EXTS 20 imm in -- (execute (UTYPE (res,rd,RISCV_LUI))) +- (execute (UTYPE (res, rd, RISCV_LUI))) - : M (bool) -+ ( (UTYPE (res,rd,RISCV_LUI))) ++ ( (UTYPE (res, rd, RISCV_LUI))) + | C_SRLI (shamt,rsd) => let rsd := creg2reg_bits rsd in -- (execute (SHIFTIOP (shamt,rsd,rsd,RISCV_SRLI))) +- (execute (SHIFTIOP (shamt, rsd, rsd, RISCV_SRLI))) - : M (bool) -+ ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SRLI))) ++ ( (SHIFTIOP (shamt, rsd, rsd, RISCV_SRLI))) + | C_SRAI (shamt,rsd) => let rsd := creg2reg_bits rsd in -- (execute (SHIFTIOP (shamt,rsd,rsd,RISCV_SRAI))) +- (execute (SHIFTIOP (shamt, rsd, rsd, RISCV_SRAI))) - : M (bool) -+ ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SRAI))) ++ ( (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))) +- (execute (ITYPE (EXTS 12 imm, rsd, rsd, RISCV_ANDI))) - : M (bool) -+ ( (ITYPE (EXTS 12 imm,rsd,rsd,RISCV_ANDI))) ++ ( (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))) +- (execute (RTYPE (rs2, rsd, rsd, RISCV_SUB))) - : M (bool) -+ ( (RTYPE (rs2,rsd,rsd,RISCV_SUB))) ++ ( (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))) +- (execute (RTYPE (rs2, rsd, rsd, RISCV_XOR))) - : M (bool) -+ ( (RTYPE (rs2,rsd,rsd,RISCV_XOR))) ++ ( (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))) +- (execute (RTYPE (rs2, rsd, rsd, RISCV_OR))) - : M (bool) -+ ( (RTYPE (rs2,rsd,rsd,RISCV_OR))) ++ ( (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))) +- (execute (RTYPE (rs2, rsd, rsd, RISCV_AND))) - : M (bool) -+ ( (RTYPE (rs2,rsd,rsd,RISCV_AND))) ++ ( (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))) +- (execute (RTYPEW (rs2, rsd, rsd, RISCV_SUBW))) - : M (bool) -+ ( (RTYPEW (rs2,rsd,rsd,RISCV_SUBW))) ++ ( (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))) +- (execute (RTYPEW (rs2, rsd, rsd, RISCV_ADDW))) - : M (bool) -+ ( (RTYPEW (rs2,rsd,rsd,RISCV_ADDW))) ++ ( (RTYPEW (rs2, rsd, rsd, RISCV_ADDW))) + | C_J (imm) => -- (execute (RISCV_JAL (EXTS 21 (concat_vec imm (vec_of_bits [B0] : mword 1)),zreg))) +- (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))) ++ ( (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))) + (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))) + (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) => (execute (SHIFTIOP (shamt, rsd, rsd, RISCV_SLLI))) : M (bool) + -+ | C_SLLI (shamt,rsd) => ( (SHIFTIOP (shamt,rsd,rsd,RISCV_SLLI))) ++ | 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))) +- (execute (LOAD (imm, sp, rd, false, WORD, false, false))) - : M (bool) -+ ( (LOAD (imm,sp,rd,false,WORD,false,false))) ++ ( (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))) +- (execute (LOAD (imm, sp, rd, false, DOUBLE, false, false))) - : M (bool) -+ ( (LOAD (imm,sp,rd,false,DOUBLE,false,false))) ++ ( (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))) +- (execute (STORE (imm, rs2, sp, WORD, false, false))) - : M (bool) -+ ( (STORE (imm,rs2,sp,WORD,false,false))) ++ ( (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))) +- (execute (STORE (imm, rs2, sp, DOUBLE, false, false))) - : M (bool) -+ ( (STORE (imm,rs2,sp,DOUBLE,false,false))) ++ ( (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))) +- (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 +- (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) @@ -350,15 +438,15 @@ | 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) -@@ -11354,6 +11362,7 @@ - | THREAD_START (g__29) => returnm ((execute_THREAD_START g__29) : bool) +@@ -12542,6 +12550,7 @@ + | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0) : bool) | ILLEGAL (s) => (execute_ILLEGAL s) : M (bool) - | C_ILLEGAL (g__30) => (execute_C_ILLEGAL g__30) : M (bool) + | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0) : M (bool) +| _ => Fail "Unexpanded instruction" end. Definition assembly_forwards (arg_ : ast) -@@ -11616,7 +11625,7 @@ +@@ -12804,7 +12813,7 @@ | _ => exit tt : M (string) end) : M (string). @@ -367,7 +455,7 @@ Definition assembly_backwards (arg_ : string) : M (ast) := let _stringappend_1112_ := arg_ in -@@ -29684,7 +29693,7 @@ +@@ -27322,7 +27331,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 +464,7 @@ Definition encdec_forwards (arg_ : ast) : M (mword 32) := (match arg_ with -@@ -31894,7 +31903,7 @@ +@@ -29410,7 +29419,7 @@ : M ((bool * bool)) end) : M ((bool * bool)). @@ -385,7 +473,7 @@ Definition loop '(tt : unit) : M (unit) := let insns_per_tick := plat_insns_per_tick tt in -@@ -31936,7 +31945,7 @@ +@@ -29457,7 +29466,7 @@ returnm (i, step_no))) >>= fun '(i, step_no) => returnm (tt : unit). @@ -394,7 +482,7 @@ Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} : read_kind := let p0_ := arg_ in -@@ -32027,7 +32036,7 @@ +@@ -29548,7 +29557,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. @@ -402,30 +490,11 @@ +(* Definition num_of_barrier_kind (arg_ : barrier_kind) : {e : Z & ArithFact (0 <= e /\ e <= 22)} := - match arg_ with -@@ -32055,7 +32064,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 -@@ -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". -+(* - Definition initial_analysis (instr : ast) - : M ((list regfp * list regfp * list regfp * list niafp * diafp * instruction_kind)) := - let iR := [] : regfps in -@@ -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)). + build_ex(match arg_ with +@@ -30722,5 +30731,5 @@ + B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0; + B0] + : mword 64) |}. - +*) - Let initial_regstate : regstate := - {| tlb39 := None; - htif_exit_code := + End Content. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 74f5adb8..d0533d48 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -239,7 +239,7 @@ let doc_nexp ctx nexp = | _ -> raise (Reporting_basic.err_unreachable l __POS__ ("cannot pretty-print nexp \"" ^ string_of_nexp nexp ^ "\"")) - in atomic (nexp_simp nexp) + in atomic nexp (* Rewrite mangled names of type variables to the original names *) let rec orig_nexp (Nexp_aux (nexp, l)) = @@ -435,9 +435,9 @@ let doc_typ, doc_atomic_typ = Typ_arg_aux (Typ_arg_order ord, _); Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with - | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> - string "mword " ^^ doc_nexp ctx (nexp_simp m) - | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx (nexp_simp m) in + | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> (* TODO: coq-compatible simplification *) + string "mword " ^^ doc_nexp ctx m + | _ -> string "vec" ^^ space ^^ typ elem_typ ^^ space ^^ doc_nexp ctx m in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) -> let tpp = string "register_ref regstate register_value " ^^ typ etyp in @@ -525,13 +525,7 @@ let doc_tannot_lem ctxt env eff typ = then string " : MR " ^^ parens ta ^^ string " _" else string " : M " ^^ parens ta else string " : " ^^ ta - in - if contains_t_pp_var ctxt typ - then - match replace_typ_size ctxt env typ with - | None -> empty - | Some typ -> of_typ typ - else of_typ typ + in of_typ typ let doc_lit (L_aux(lit,l)) = match lit with @@ -647,15 +641,15 @@ let is_auto_decomposed_exist env typ = (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = +let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) = let env = env_of_annot (l,annot) in let typ = Env.expand_synonyms env typ in - match is_auto_decomposed_exist env typ with - | Some typ' -> - let pat_pp = doc_pat ctxt true (pat, typ') in + match exists_as_pairs, is_auto_decomposed_exist env typ with + | true, Some typ' -> + let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp - | None -> + | _ -> match p with (* Special case translation of the None constructor to remove the unit arg *) | P_app(id, _) when string_of_id id = "None" -> string "None" @@ -677,17 +671,17 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = | _ -> assert false in let ppp = doc_unop (doc_id_ctor id) - (parens (separate_map comma (doc_pat ctxt true) (List.combine pats arg_typs))) in + (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in if apat_needed then parens ppp else ppp end | P_app(id, []) -> doc_id_ctor id | P_lit lit -> doc_lit lit | P_wild -> underscore | P_id id -> doc_id id - | P_var(p,_) -> doc_pat ctxt true (p, typ) - | P_as(p,id) -> parens (separate space [doc_pat ctxt true (p, typ); string "as"; doc_id id]) + | P_var(p,_) -> doc_pat ctxt true exists_as_pairs (p, typ) + | P_as(p,id) -> parens (separate space [doc_pat ctxt true exists_as_pairs (p, typ); string "as"; doc_id id]) | P_typ(ptyp,p) -> - let doc_p = doc_pat ctxt true (p, typ) in + let doc_p = doc_pat ctxt true exists_as_pairs (p, typ) in doc_p (* Type annotations aren't allowed everywhere in patterns in Coq *) (*parens (doc_op colon doc_p (doc_typ typ))*) @@ -697,7 +691,7 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = | Some (_,_,t) -> t | None -> raise (Reporting_basic.err_unreachable l __POS__ "vector pattern doesn't have vector type") in - let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true (p,el_typ)) pats) in + let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true exists_as_pairs (p,el_typ)) pats) in if apat_needed then parens ppp else ppp | P_vector_concat pats -> raise (Reporting_basic.err_unreachable l __POS__ @@ -708,25 +702,26 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = | _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern doesn't have tuple type") in (match pats, typs with - | [p], [typ'] -> doc_pat ctxt apat_needed (p, typ') + | [p], [typ'] -> doc_pat ctxt apat_needed exists_as_pairs (p, typ') | [_], _ -> raise (Reporting_basic.err_unreachable l __POS__ "tuple pattern length does not match tuple type length") - | _ -> parens (separate_map comma_sp (doc_pat ctxt false) (List.combine pats typs))) + | _ -> parens (separate_map comma_sp (doc_pat ctxt false exists_as_pairs) (List.combine pats typs))) | P_list pats -> let el_typ = match typ with | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) when Id.compare f (mk_id "list") = 0 -> el_typ | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list") in - brackets (separate_map semi (fun p -> doc_pat ctxt false (p, el_typ)) pats) + brackets (separate_map semi (fun p -> doc_pat ctxt false true (p, el_typ)) pats) | P_cons (p,p') -> let el_typ = match typ with | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) when Id.compare f (mk_id "list") = 0 -> el_typ | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list") in - doc_op (string "::") (doc_pat ctxt true (p, el_typ)) (doc_pat ctxt true (p', typ)) + doc_op (string "::") (doc_pat ctxt true true (p, el_typ)) (doc_pat ctxt true true (p', typ)) | P_string_append _ -> unreachable l __POS__ "Coq doesn't support string append patterns" | P_not _ -> unreachable l __POS__ "Coq doesn't support not patterns" + | P_record (_,_) -> empty (* TODO *) let contains_early_return exp = let e_app (f, args) = @@ -873,6 +868,29 @@ let doc_exp_lem, doc_let_lem = let epp = string "build_ex" ^/^ epp in if aexp_needed then parens epp else epp in + let rec construct_dep_pairs env print_types = + let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) = + match e,t with + | E_tuple exps, Typ_tup typs + | E_cast (_, E_aux (E_tuple exps,_)), Typ_tup typs + -> + parens (separate (string ", ") (List.map2 (aux false) exps typs)) + | _ -> + let typ' = expand_range_type typ in + match destruct_exist env typ' with + | Some _ -> let arg_pp = string "build_ex " ^^ expY exp in + let arg_pp = if print_types + then arg_pp ^/^ doc_tannot_lem ctxt env false typ + else arg_pp + in + if want_parens then parens arg_pp else arg_pp + | None -> + if print_types + then let arg_pp = expV true exp ^/^ doc_tannot_lem ctxt env false typ in + if want_parens then parens arg_pp else arg_pp + else expV want_parens exp + in aux + in let liftR doc = if ctxt.early_ret && effectful (effect_of full_exp) then separate space [string "liftR"; parens (doc)] @@ -1064,109 +1082,112 @@ let doc_exp_lem, doc_let_lem = end | _ -> let env = env_of_annot (l,annot) in - if Env.is_union_constructor f env then - let epp = - match args with - | [] -> doc_id_ctor f - | [arg] -> doc_id_ctor f ^^ space ^^ expV true arg - | _ -> - doc_id_ctor f ^^ space ^^ - parens (separate_map comma (expV false) args) in - if aexp_needed then parens (align epp) else epp - else - let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in - let call, is_extern = - if Env.is_extern f env "coq" - then string (Env.get_extern f env "coq"), true - else doc_id f, false in - let (tqs,fn_ty) = Env.get_val_spec_orig f env in - let arg_typs, ret_typ, eff = match fn_ty with - | Typ_aux (Typ_fn (arg_typ,ret_typ,eff),_) -> - (match arg_typ with - | Typ_aux (Typ_tup typs,_) -> typs, ret_typ, eff - | _ -> [arg_typ], ret_typ, eff) - | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type") + let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in + let call, is_extern, is_ctor = + if Env.is_union_constructor f env then doc_id_ctor f, false, true else + if Env.is_extern f env "coq" + then string (Env.get_extern f env "coq"), true, false + else doc_id f, false, false in + let (tqs,fn_ty) = Env.get_val_spec_orig f env in + let arg_typs, ret_typ, eff = match fn_ty with + | Typ_aux (Typ_fn (arg_typ,ret_typ,eff),_) -> + (match arg_typ with + | Typ_aux (Typ_tup typs,_) -> typs, ret_typ, eff + | _ -> [arg_typ], ret_typ, eff) + | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type") + in + let inst = + match instantiation_of_without_type full_exp with + | x -> x + (* Not all function applications can be inferred, so try falling back to the + type inferred when we know the target type. + TODO: there are probably some edge cases where this won't pick up a need + to cast. *) + | exception _ -> instantiation_of full_exp + in + let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in + + (* Insert existential packing of arguments where necessary *) + let doc_arg want_parens arg typ_from_fn = + let env = env_of arg in + let typ_from_fn = subst_unifiers inst typ_from_fn in + let typ_from_fn = Env.expand_synonyms env typ_from_fn in + (* TODO: more sophisticated check *) + let () = + debug ctxt (lazy (" arg type found " ^ string_of_typ (general_typ_of arg))); + debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn)) in - let inst = - match instantiation_of_without_type full_exp with - | x -> x - (* Not all function applications can be inferred, so try falling back to the - type inferred when we know the target type. - TODO: there are probably some edge cases where this won't pick up a need - to cast. *) - | exception _ -> instantiation_of full_exp + let typ_of_arg = Env.expand_synonyms env (general_typ_of arg) in + let typ_of_arg = expand_range_type typ_of_arg in + let typ_of_arg' = match typ_of_arg with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in + let typ_from_fn' = match typ_from_fn with Typ_aux (Typ_exist (_,_,t),_) -> t | t -> t in + let autocast = + (* Avoid using helper functions which simplify the nexps *) + is_bitvector_typ typ_of_arg' && is_bitvector_typ typ_from_fn' && + match typ_of_arg', typ_from_fn' with + | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_), + Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) -> + not (similar_nexps env n1 n2) + | _ -> false in - let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in - - (* Insert existential unpacking of arguments where necessary *) - let doc_arg arg typ_from_fn = - let arg_pp = expY arg in - let arg_ty_plain = Env.expand_synonyms (env_of arg) (general_typ_of arg) in - let arg_ty = expand_range_type arg_ty_plain in - let typ_from_fn_plain = subst_unifiers inst typ_from_fn in - let typ_from_fn_plain = Env.expand_synonyms (env_of arg) typ_from_fn_plain in - let typ_from_fn = expand_range_type typ_from_fn_plain in - (* TODO: more sophisticated check *) - let () = - debug ctxt (lazy (" arg type found " ^ string_of_typ arg_ty_plain)); - debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn_plain)) - in - match destruct_exist env arg_ty, destruct_exist env typ_from_fn with - | Some _, None -> parens (string "projT1 " ^^ arg_pp) - (* Usually existentials have already been built elsewhere, but this - is useful for (e.g.) ranges *) - | None, Some _ -> parens (string "build_ex " ^^ arg_pp) - | Some _, Some _ when is_range_from_atom (env_of arg) arg_ty_plain typ_from_fn_plain -> - parens (string "to_range " ^^ parens (string "projT1 " ^^ arg_pp)) - | _, _ -> arg_pp + let want_parens1 = want_parens || autocast in + let arg_pp = + construct_dep_pairs env false want_parens1 arg typ_from_fn in - let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in - - (* Decide whether to unpack an existential result, pack one, or cast. - To do this we compare the expected type stored in the checked expression - with the inferred type. *) + if autocast + then let arg_pp = string "autocast" ^^ space ^^ arg_pp in + if want_parens then parens arg_pp else arg_pp + else arg_pp + in + let epp = + if is_ctor + then hang 2 (call ^^ break 1 ^^ parens (flow (comma ^^ break 1) (List.map2 (doc_arg false) args arg_typs))) + else hang 2 (flow (break 1) (call :: List.map2 (doc_arg true) args arg_typs)) in + + (* Decide whether to unpack an existential result, pack one, or cast. + To do this we compare the expected type stored in the checked expression + with the inferred type. *) + let ret_typ_inst = + subst_unifiers inst ret_typ + in + let unpack,autocast = + let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in + let ann_typ = expand_range_type ann_typ in + let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in let ret_typ_inst = - subst_unifiers inst ret_typ + if is_no_Z_proof_fn env f then ret_typ_inst + else snd (replace_atom_return_type ret_typ_inst) in + let () = + debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); + debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in - let unpack,build_ex,autocast = - let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in - let ann_typ = expand_range_type ann_typ in - let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in - let ret_typ_inst = - if is_no_Z_proof_fn env f then ret_typ_inst - else snd (replace_atom_return_type ret_typ_inst) in - let () = - debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); - debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) - in - let unpack, build_ex, in_typ, out_typ = - match ret_typ_inst, ann_typ with - | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) -> - if alpha_equivalent env ret_typ_inst ann_typ - then false,false,t1,t2 - else true,true,t1,t2 - | Typ_aux (Typ_exist (_,_,t1),_),t2 -> true,false,t1,t2 - | t1, Typ_aux (Typ_exist (_,_,t2),_) -> false,true,t1,t2 - | t1, t2 -> false,false,t1,t2 - in - let autocast = - (* Avoid using helper functions which simplify the nexps *) - is_bitvector_typ in_typ && is_bitvector_typ out_typ && - match in_typ, out_typ with - | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_), - Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) -> - not (similar_nexps env n1 n2) - | _ -> false - in unpack,build_ex,autocast + let unpack, in_typ = + match ret_typ_inst with + | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 + | t1 -> false,t1 + in + let out_typ = + match ann_typ with + | Typ_aux (Typ_exist (_,_,t1),_) -> t1 + | t1 -> t1 in - let autocast_id, proj_id, build_id = - if effectful eff - then "autocast_m", "projT1_m", "build_ex_m" - else "autocast", "projT1", "build_ex" in - let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in - let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in - let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in - liftR (if aexp_needed then parens (align epp) else epp) + let autocast = + (* Avoid using helper functions which simplify the nexps *) + is_bitvector_typ in_typ && is_bitvector_typ out_typ && + match in_typ, out_typ with + | Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n1,_);_;_]),_), + Typ_aux (Typ_app (_,[Typ_arg_aux (Typ_arg_nexp n2,_);_;_]),_) -> + not (similar_nexps env n1 n2) + | _ -> false + in unpack,autocast + in + let autocast_id, proj_id = + if effectful eff + then "autocast_m", "projT1_m" + else "autocast", "projT1" in + let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in + let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in + liftR (if aexp_needed then parens (align epp) else epp) end | E_vector_access (v,e) -> raise (Reporting_basic.err_unreachable l __POS__ @@ -1201,23 +1222,34 @@ let doc_exp_lem, doc_let_lem = else liftR epp else if Env.is_register id env then doc_id (append_id id "_ref") else if is_ctor env id then doc_id_ctor id - else maybe_add_exist (doc_id id) - | E_lit lit -> maybe_add_exist (doc_lit lit) + else begin + match Env.lookup_id id env with + | Local (_,typ) -> + let typ = expand_range_type (Env.expand_synonyms env typ) in + let proj = match typ with + | Typ_aux (Typ_exist _,_) -> true + | _ -> false + in if proj then string "projT1" ^^ doc_id id else doc_id id + | _ -> doc_id id + end + | E_lit lit -> doc_lit lit | E_cast(typ,e) -> let epp = expV true e in let env = env_of_annot (l,annot) in - let unpack,build_ex, in_typ, out_typ = + let exist, in_typ, out_typ = let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in let ann_typ = expand_range_type ann_typ in let cast_typ = expand_range_type (Env.expand_synonyms env typ) in + let () = + debug ctxt (lazy ("Cast of type " ^ string_of_typ cast_typ)); + debug ctxt (lazy (" where type expected is " ^ string_of_typ ann_typ)) + in match cast_typ, ann_typ with | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) -> - if alpha_equivalent env cast_typ ann_typ - then false,false,t1,t2 - else true,true,t1,t2 - | Typ_aux (Typ_exist (_,_,t1),_), t2 -> true,false,t1,t2 - | t1, Typ_aux (Typ_exist (_,_,t2),_) -> false,true,t1,t2 - | t1, t2 -> false,false,t1,t2 + true,t1,t2 + | Typ_aux (Typ_exist (_,_,t1),_), t2 -> true,t1,t2 + | t1, Typ_aux (Typ_exist (_,_,t2),_) -> false,t1,t2 + | t1, t2 -> false,t1,t2 in let autocast = (* Avoid using helper functions which simplify the nexps *) @@ -1232,10 +1264,14 @@ let doc_exp_lem, doc_let_lem = if effectful (effect_of e) then "autocast_m", "projT1_m", "build_ex_m" else "autocast", "projT1", "build_ex" in - let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in + let epp = if exist && effectful (effect_of e) + then string "derive_m" ^^ space ^^ epp ^/^ doc_tannot_lem ctxt (env_of e) (effectful (effect_of e)) typ + else + let epp = if exist then parens (string build_id ^^ space ^^ epp) else epp in + let epp = epp ^/^ doc_tannot_lem ctxt (env_of e) (effectful (effect_of e)) typ in + if exist then string proj_id ^^ space ^^ parens epp else epp + in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in - let epp = epp ^/^ doc_tannot_lem ctxt (env_of e) (effectful (effect_of e)) typ in - let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in if aexp_needed then parens epp else epp | E_tuple exps -> parens (align (group (separate_map (comma ^^ break 1) expN exps))) @@ -1346,12 +1382,23 @@ let doc_exp_lem, doc_let_lem = raise (report l __POS__ "E_vars should have been removed before pretty-printing") | E_internal_plet (pat,e1,e2) -> begin - match pat, e1 with + match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), - (E_aux (E_assert (assert_e1,assert_e2),_)) -> + (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in if aexp_needed then parens (align epp) else align epp + (* Special case because we don't handle variables with nested existentials well yet. + TODO: check that id1 is not used in e2' *) + | ((P_aux (P_id id1,_)) | P_aux (P_typ (_, P_aux (P_id id1,_)),_)), + _, + (E_aux (E_let (LB_aux (LB_val (pat', E_aux (E_cast (typ', E_aux (E_id id2,_)),_)),_), e2'),_)) + when Id.compare id1 id2 == 0 -> + let e1_pp = parens (separate space [expN e1; colon; + string (if ctxt.early_ret then "MR" else "M"); + parens (doc_typ ctxt typ')]) in + let middle = separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in + infix 0 1 middle e1_pp (expN e2') | _ -> let epp = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in @@ -1367,18 +1414,42 @@ let doc_exp_lem, doc_let_lem = when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] + | P_aux (P_typ (typ, P_aux (P_id id,_)),_) + | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_) + | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_) + when not (is_enum (env_of e1) id) -> + let full_typ = (expand_range_type typ) in + let binder = match destruct_exist (env_of e1) full_typ with + | Some ([kid], NC_aux (NC_true,_), + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) + when Kid.compare kid kid' == 0 -> + parens (separate space [doc_id id; colon; string "Z"]) + | Some ([kid], nc, + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) + when Kid.compare kid kid' == 0 -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) + | _ -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + in separate space [string ">>= fun"; binder; bigarrow] | _ -> - separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow] + separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in infix 0 1 middle (expV b e1) (expN e2) in if aexp_needed then parens (align epp) else epp end | E_internal_return (e1) -> - let e1pp = expY e1 in - let valpp = if ctxt.build_ex_return - then parens (string "build_ex" ^^ space ^^ e1pp) - else e1pp in + let typ = general_typ_of e1 in + let () = + debug ctxt (lazy ("Monad return of " ^ string_of_exp e1)); + debug ctxt (lazy (" with type " ^ string_of_typ typ)) + in + let valpp = + let env = env_of e1 in + construct_dep_pairs env false (*!!*) true e1 typ + in wrap_parens (align (separate space [string "returnm"; valpp])) | E_sizeof nexp -> (match nexp_simp nexp with @@ -1432,11 +1503,11 @@ let doc_exp_lem, doc_let_lem = (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,pat),_),(E_aux (_,e_ann) as e)) -> prefix 2 1 - (separate space [string "let"; squote ^^ doc_pat ctxt true (pat, typ); coloneq]) + (separate space [string "let"; squote ^^ doc_pat ctxt true false (pat, typ); coloneq]) (top_exp ctxt false (E_aux (E_cast (typ,e),e_ann))) | LB_val(pat,e) -> prefix 2 1 - (separate space [string "let"; squote ^^ doc_pat ctxt true (pat, typ_of e); coloneq]) + (separate space [string "let"; squote ^^ doc_pat ctxt true false (pat, typ_of e); coloneq]) (top_exp ctxt false e) and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) = @@ -1448,7 +1519,7 @@ let doc_exp_lem, doc_let_lem = and doc_case ctxt typ = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat ctxt false (pat,typ);bigarrow]) + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) (group (top_exp ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting_basic.err_unreachable l __POS__ @@ -1737,6 +1808,7 @@ let merge_kids_atoms pats = let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in gone,map + let merge_var_patterns map pats = let map,pats = List.fold_left (fun (map,pats) (pat, typ) -> match pat with @@ -1746,12 +1818,17 @@ let merge_var_patterns map pats = in map, List.rev pats let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = - let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in + let env = env_of_annot annot in + let (tq,typ) = Env.get_val_spec_orig id env in let (arg_typ, ret_typ, eff) = match typ with | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") in let build_ex, ret_typ = replace_atom_return_type ret_typ in + let build_ex = match destruct_exist env (expand_range_type ret_typ) with + | Some _ -> true + | _ -> build_ex + in let ids_to_avoid = all_ids pexp in let kids_used = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in @@ -1782,9 +1859,40 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = when Util.is_none (is_auto_decomposed_exist env exp_typ) && not (is_enum env id) -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) +(* | P_id id + | P_typ (_,P_aux (P_id id,_)) + when not (is_enum env id) -> begin + match destruct_exist env (expand_range_type exp_typ) with + | Some (kids, NC_aux (NC_true,_), typ) -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + | Some (kids, nc, typ) -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) ^^ space ^^ + bquote ^^ braces (doc_arithfact ctxt nc) + | None -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + end*) + | P_id id + | P_typ (_,P_aux (P_id id,_)) + when not (is_enum env id) -> begin + let full_typ = (expand_range_type exp_typ) in + match destruct_exist env full_typ with + | Some ([kid], NC_aux (NC_true,_), + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) + when Kid.compare kid kid' == 0 -> + parens (separate space [doc_id id; colon; string "Z"]) + | Some ([kid], nc, + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) + when Kid.compare kid kid' == 0 -> + (used_a_pattern := true; + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])) + | _ -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + end | _ -> (used_a_pattern := true; - squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ])) + squote ^^ parens (separate space [doc_pat ctxt true true (pat, exp_typ); colon; doc_typ ctxt typ])) in let patspp = separate_map space doc_binder pats in let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in @@ -1980,7 +2088,8 @@ let doc_val pat exp = let env = env_of exp in let typ = expand_range_type (Env.expand_synonyms env (general_typ_of exp)) in let ctxt = { empty_ctxt with debug = List.mem (string_of_id id) (!opt_debug_on) } in - let id, opt_unpack = + let id, opt_unpack = id, None in +(* TODO: Hacked out until I decide what to do ... match destruct_exist env typ with | None -> id, None | Some (kids,nc,typ) -> @@ -1990,13 +2099,13 @@ let doc_val pat exp = (* TODO: name collisions *) mk_id (string_of_id id ^ "_spec"), Some (id, string_of_id id ^ "_prop") - in + in*) let idpp = doc_id id in let basepp = idpp ^^ typpp ^^ space ^^ coloneq ^/^ doc_exp_lem ctxt false exp ^^ dot in match opt_unpack with - | None -> group (string "Let" ^^ space ^^ basepp) ^^ hardline + | None -> group (string "Definition" ^^ space ^^ basepp) ^^ hardline | Some (orig_id, hyp_id) -> group (string "Definition" ^^ space ^^ basepp) ^^ hardline ^^ group (separate space [string "Let"; doc_id orig_id; coloneq; string "projT1"; idpp; dot]) ^^ hardline ^^ hardline |