diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 14:20:34 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 14:20:34 +0200 |
commit | 54846ce3ee63b8fff66ac5bf27d1c89ac701ed94 (patch) | |
tree | 305a5d18e95f1513c4d160467786c5527cbb634c | |
parent | d84a003dc41c1ce572e86f399f5a610a78eda15f (diff) | |
download | compcert-kvx-54846ce3ee63b8fff66ac5bf27d1c89ac701ed94.tar.gz compcert-kvx-54846ce3ee63b8fff66ac5bf27d1c89ac701ed94.zip |
fix for Risc-V
-rw-r--r-- | riscV/Asmgen.v | 13 | ||||
-rw-r--r-- | riscV/Asmgenproof.v | 8 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 7 | ||||
-rw-r--r-- | riscV/Op.v | 14 |
4 files changed, 34 insertions, 8 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..ecaca7b3 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -770,9 +770,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 +803,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 +853,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..e2fafb16 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -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 98d5bd33..175e484f 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1318,8 +1318,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', @@ -1327,7 +1327,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, @@ -1343,6 +1343,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 -> |