diff options
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Archi.v | 2 | ||||
| -rw-r--r-- | riscV/Asmgen.v | 45 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 12 | ||||
| -rw-r--r-- | riscV/Asmgenproof1.v | 52 | ||||
| -rw-r--r-- | riscV/CSE2deps.v | 32 | ||||
| -rw-r--r-- | riscV/CSE2depsproof.v | 139 | ||||
| -rw-r--r-- | riscV/DuplicateOpcodeHeuristic.ml | 41 | ||||
| -rw-r--r-- | riscV/Machregsaux.ml | 5 | ||||
| -rw-r--r-- | riscV/Machregsaux.mli | 2 | ||||
| -rw-r--r-- | riscV/Op.v | 76 | ||||
| -rw-r--r-- | riscV/SelectLong.vp | 2 | ||||
| -rw-r--r-- | riscV/SelectLongproof.v | 1 | ||||
| -rw-r--r-- | riscV/SelectOp.vp | 7 | ||||
| -rw-r--r-- | riscV/SelectOpproof.v | 29 | ||||
| -rw-r--r-- | riscV/TargetPrinter.ml | 4 |
15 files changed, 409 insertions, 40 deletions
diff --git a/riscV/Archi.v b/riscV/Archi.v index 1b24e732..1bb80e89 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -71,3 +71,5 @@ Global Opaque ptr64 big_endian splitlong (** Whether to generate position-independent code or not *) Parameter pic_code: unit -> bool. + +Definition has_notrap_loads := false. diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..b431d63d 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -25,6 +25,8 @@ Require Import Op Locations Mach Asm. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct @@ -503,11 +505,16 @@ Definition transl_op OK (Psrliw rd rs n :: k) | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrliw X31 rs (Int.repr 31) :: + Paddw X31 rs X31 :: + Psraiw rd X31 Int.one :: k + else Psraiw X31 rs (Int.repr 31) :: + Psrliw X31 X31 (Int.sub Int.iwordsize n) :: + Paddw X31 rs X31 :: + Psraiw rd X31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -592,11 +599,16 @@ Definition transl_op OK (Psrlil rd rs n :: k) | Oshrxlimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; - OK (if Int.eq n Int.zero then Pmv rd rs :: k else - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrlil X31 rs (Int.repr 63) :: + Paddl X31 rs X31 :: + Psrail rd X31 Int.one :: k + else Psrail X31 rs (Int.repr 63) :: + Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: + Paddl X31 rs X31 :: + Psrail rd X31 n :: k) | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; @@ -770,9 +782,13 @@ Definition transl_memory_access Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: code) := - match chunk with + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => + match chunk with | Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k @@ -799,6 +815,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access (Pfld r) addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -848,8 +865,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_ptr SP f.(fn_link_ofs) X30 c) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 5ec57886..8e9f022c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -285,12 +285,12 @@ Opaque Int.eq. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. - apply opimm32_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. -- destruct (Int.eq n Int.zero); TailNoLabel. +- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. Qed. @@ -359,7 +359,7 @@ Proof. - destruct ep. eapply loadind_label; eauto. eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. - eapply transl_op_label; eauto. -- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. +- destruct t; (try discriminate); destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I. - destruct s0; monadInv H; TailNoLabel. - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). @@ -725,6 +725,12 @@ Local Transparent destroyed_by_op. intros; auto with asmgen. simpl; congruence. +- (* Mload notrap *) (* isn't there a nicer way? *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + - (* Mstore *) assert (eval_addressing tge sp addr (map rs args) = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index c20c4e49..8678a5dc 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1035,17 +1035,23 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrximm *) - clear H. exploit Val.shrx_shr_2; eauto. intros E; subst v; clear EV. + clear H. exploit Val.shrx_shr_3; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. -+ change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. - (* longofintu *) econstructor; split. eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. @@ -1070,17 +1076,24 @@ Opaque Int.eq. intros (rs' & A & B & C). exists rs'; split; eauto. rewrite B; auto with asmgen. - (* shrxlimm *) - clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV. + clear H. exploit Val.shrxl_shrl_3; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. -+ change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. ++ destruct (Int.eq n Int.one). + * econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. + + * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). + econstructor; split. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + eapply exec_straight_step. simpl; reflexivity. auto. + apply exec_straight_one. simpl; reflexivity. auto. + split; intros; Simpl. - (* cond *) exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. @@ -1302,8 +1315,8 @@ Proof. Qed. Lemma transl_load_correct: - forall chunk addr args dst k c (rs: regset) m a v, - transl_load chunk addr args dst k = OK c -> + forall trap chunk addr args dst k c (rs: regset) m a v, + transl_load trap chunk addr args dst k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> exists rs', @@ -1311,7 +1324,8 @@ Lemma transl_load_correct: /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros until v; intros TR EV LOAD. + intros until v; intros TR EV LOAD. + destruct trap; try (simpl in *; discriminate). assert (A: exists mk_instr, transl_memory_access mk_instr addr args k = OK c /\ forall base ofs rs, diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v new file mode 100644 index 00000000..b4b80e2f --- /dev/null +++ b/riscV/CSE2deps.v @@ -0,0 +1,32 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import BoolEqual Coqlib. +Require Import AST Integers Floats. +Require Import Values Memory Globalenvs Events. +Require Import Op. + + +Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw := + (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk)) + && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk)) + && ((ofsw + size_chunk chunkw <=? ofsr) || + (ofsr + size_chunk chunkr <=? ofsw)). + +Definition may_overlap chunk addr args chunk' addr' args' := + match addr, addr', args, args' with + | (Aindexed ofs), (Aindexed ofs'), + (base :: nil), (base' :: nil) => + if peq base base' + then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + else true | _, _, _, _ => true + end. diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v new file mode 100644 index 00000000..f283c8ac --- /dev/null +++ b/riscV/CSE2depsproof.v @@ -0,0 +1,139 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL Maps. + +Require Import Globalenvs Values. +Require Import Linking Values Memory Globalenvs Events Smallstep. +Require Import Registers Op RTL. +Require Import CSE2 CSE2deps. +Require Import Lia. + +Lemma ptrofs_size : + Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat. +Proof. + unfold Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. + trivial. +Qed. + +Lemma ptrofs_modulus : + Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296. +Proof. + unfold Ptrofs.modulus. + rewrite ptrofs_size. + destruct Archi.ptr64; reflexivity. +Qed. + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Section MEMORY_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + Variable base : val. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Aindexed ofsw) (base :: nil) = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Aindexed ofsr) (base :: nil) = Some addrr. + + Lemma load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + rewrite ptrofs_modulus in *. + simpl in *. + inv ADDRR. + inv ADDRW. + destruct base; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + all: try rewrite ptrofs_modulus in *. + all: destruct Archi.ptr64. + + all: intuition lia. + Qed. + + Theorem load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End MEMORY_WRITE. +End SOUNDNESS. + + +Section SOUNDNESS. + Variable F V : Type. + Variable genv: Genv.t F V. + Variable sp : val. + +Lemma may_overlap_sound: + forall m m' : mem, + forall chunk addr args chunk' addr' args' v a a' rs, + (eval_addressing genv sp addr (rs ## args)) = Some a -> + (eval_addressing genv sp addr' (rs ## args')) = Some a' -> + (may_overlap chunk addr args chunk' addr' args') = false -> + (Mem.storev chunk m a v) = Some m' -> + (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m a'). +Proof. + intros until rs. + intros ADDR ADDR' OVERLAP STORE. + destruct addr; destruct addr'; try discriminate. + { (* Aindexed / Aindexed *) + destruct args as [ | base [ | ]]. 1,3: discriminate. + destruct args' as [ | base' [ | ]]. 1,3: discriminate. + simpl in OVERLAP. + destruct (peq base base'). 2: discriminate. + subst base'. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP. + 2: discriminate. + simpl in *. + eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. + } +Qed. + +End SOUNDNESS. diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml new file mode 100644 index 00000000..38702e1b --- /dev/null +++ b/riscV/DuplicateOpcodeHeuristic.ml @@ -0,0 +1,41 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(* open Camlcoq *) +open Op +open Integers + +let opcode_heuristic code cond ifso ifnot is_loop_header = + match cond with + | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with + | Clt | Cle -> Some false + | Cgt | Cge -> Some true + | _ -> None + ) else None + | Ccompf c | Ccompfs c -> (match c with + | Ceq -> Some false + | Cne -> Some true + | _ -> None + ) + | Cnotcompf c | Cnotcompfs c -> (match c with + | Ceq -> Some true + | Cne -> Some false + | _ -> None + ) + | _ -> None diff --git a/riscV/Machregsaux.ml b/riscV/Machregsaux.ml index a48749a5..840943e7 100644 --- a/riscV/Machregsaux.ml +++ b/riscV/Machregsaux.ml @@ -13,3 +13,8 @@ (** Auxiliary functions on machine registers *) let is_scratch_register r = false + +let class_of_type = function + | AST.Tint | AST.Tlong -> 0 + | AST.Tfloat | AST.Tsingle -> 1 + | AST.Tany32 | AST.Tany64 -> assert false diff --git a/riscV/Machregsaux.mli b/riscV/Machregsaux.mli index f3d52849..01b0f9fd 100644 --- a/riscV/Machregsaux.mli +++ b/riscV/Machregsaux.mli @@ -13,3 +13,5 @@ (** Auxiliary functions on machine registers *) val is_scratch_register: string -> bool + +val class_of_type: AST.typ -> int @@ -666,6 +666,42 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct (eval_condition cond vl m)... destruct b... Qed. + +Definition is_trapping_op (op : operation) := + match op with + | Odiv | Odivl | Odivu | Odivlu + | Omod | Omodl | Omodu | Omodlu + | Oshrximm _ | Oshrxlimm _ + | Ointoffloat | Ointuoffloat + | Ointofsingle | Ointuofsingle + | Olongoffloat | Olonguoffloat + | Olongofsingle | Olonguofsingle + | Osingleofint | Osingleofintu + | Osingleoflong | Osingleoflongu + | Ofloatofint | Ofloatofintu + | Ofloatoflong | Ofloatoflongu => true + | _ => false + end. + + +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + +Lemma is_trapping_op_sound: + forall op vl sp m, + is_trapping_op op = false -> + (List.length vl) = args_of_operation op -> + eval_operation genv sp op vl m <> None. +Proof. + unfold args_of_operation. + destruct op; destruct eq_operation; intros; simpl in *; try congruence. + all: try (destruct vl as [ | vh1 vl1]; try discriminate). + all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). + all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). + all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). +Qed. End SOUNDNESS. (** * Manipulating and transforming operations *) @@ -1159,6 +1195,20 @@ Proof. apply Val.offset_ptr_inject; auto. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *; + inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate. +Qed. End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1265,6 +1315,18 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *; + inv Hlessdef; trivial; try discriminate; + inv H0; trivial; try discriminate; + inv H2; trivial; try discriminate. +Qed. End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1317,6 +1379,20 @@ Proof. econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. + +Lemma eval_addressing_inject_none: + forall addr vl1 vl2, + Val.inject_list f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None -> + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None. +Proof. + intros. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> diff --git a/riscV/SelectLong.vp b/riscV/SelectLong.vp index b3e07bf5..0ccc4725 100644 --- a/riscV/SelectLong.vp +++ b/riscV/SelectLong.vp @@ -21,7 +21,7 @@ Require Import Coqlib. Require Import Compopts. Require Import AST Integers Floats. Require Import Op CminorSel. -Require Import SelectOp SplitLong. +Require Import OpHelpers SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v index 78a1935d..d47b6d64 100644 --- a/riscV/SelectLongproof.v +++ b/riscV/SelectLongproof.v @@ -21,6 +21,7 @@ Require Import String Coqlib Maps Integers Floats Errors. Require Archi. Require Import AST Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. +Require Import OpHelpers OpHelpersproof. Require Import SelectOp SelectOpproof SplitLong SplitLongproof. Require Import SelectLong. diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp index 99806006..e9920e46 100644 --- a/riscV/SelectOp.vp +++ b/riscV/SelectOp.vp @@ -452,6 +452,13 @@ Nondetfunction builtin_arg (e: expr) := | _ => BA e end. +(* floats *) +Definition divf_base (e1: expr) (e2: expr) := + Eop Odivf (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + Eop Odivfs (e1 ::: e2 ::: Enil). + (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 593be1ed..7f2014dc 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -22,6 +22,8 @@ Require Import AST Integers Floats. Require Import Values Memory Builtins Globalenvs. Require Import Cminor Op CminorSel. Require Import SelectOp. +Require Import OpHelpers. +Require Import OpHelpersproof. Local Open Scope cminorsel_scope. @@ -73,8 +75,10 @@ Ltac TrivialExists := (** * Correctness of the smart constructors *) Section CMCONSTR. - -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -929,6 +933,27 @@ Proof. - constructor; auto. Qed. +(* floating-point division without HELPERS *) +Theorem eval_divf_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros; unfold divf_base. + TrivialExists. +Qed. + +Theorem eval_divfs_base: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v. +Proof. + intros; unfold divfs_base. + TrivialExists. +Qed. + (** Platform-specific known builtins *) Theorem eval_platform_builtin: diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 64bcea4c..1f02ca71 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -107,7 +107,9 @@ module Target : TARGET = let name_of_section = function | Section_text -> ".text" - | Section_data i | Section_small_data i -> + | Section_data(i, true) -> + failwith "_Thread_local unsupported on this platform" + | Section_data(i, false) | Section_small_data i -> if i then ".data" else common_section () | Section_const i | Section_small_const i -> if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" |