diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 14:10:51 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-16 14:10:51 +0200 |
| commit | ba32e5daa1ff343a1a0b89e65c2ba5764c9cef04 (patch) | |
| tree | 585d094836b7b956601b1d12764b84bf83d63e8c /backend/CSE2proof.v | |
| parent | 5450d5054dc84d31c820b6d60c87c628290d5487 (diff) | |
| download | compcert-kvx-ba32e5daa1ff343a1a0b89e65c2ba5764c9cef04.tar.gz compcert-kvx-ba32e5daa1ff343a1a0b89e65c2ba5764c9cef04.zip | |
progress on CSE2 builtins
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 309ccce1..e61cde3d 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1033,7 +1033,16 @@ Proof. assumption. } intuition congruence. -Qed. +Qed. + +Lemma kill_builtin_res_sound: + forall res (m : mem) (rs : regset) vres (rel : RELATION.t) + (REL : sem_rel m rel rs), + (sem_rel m (kill_builtin_res res rel) (regmap_setres res vres rs)). +Proof. + destruct res; simpl; intros; trivial. + apply kill_reg_sound; trivial. +Qed. End SOUNDNESS. Definition match_prog (p tp: RTL.program) := @@ -1578,9 +1587,9 @@ Proof. destruct (forward_map _) as [map |] eqn:MAP in *; trivial. destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some RELATION.top). + apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (kill_mem mpc))). { - replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_builtin_res res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)). { eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. 2: apply apply_instr'_bot. @@ -1591,8 +1600,9 @@ Proof. rewrite MPC. reflexivity. } - apply top_ok. - + apply kill_builtin_res_sound. + apply kill_mem_sound with (m := m). + assumption. (* cond *) - econstructor; split. |