diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 07:47:27 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 07:47:27 +0100 |
| commit | 5787da9e4d024dc3a3190bff0fe29385abbcece9 (patch) | |
| tree | 816032e52ebf326f6225940ebe9264a125512488 /backend/ForwardMovesproof.v | |
| parent | bea5025d84a4207011cbc8c5c435d399aa5bfdef (diff) | |
| download | compcert-kvx-5787da9e4d024dc3a3190bff0fe29385abbcece9.tar.gz compcert-kvx-5787da9e4d024dc3a3190bff0fe29385abbcece9.zip | |
some more proof
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 56 |
1 files changed, 53 insertions, 3 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index 3db67ed6..99b546c7 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -298,7 +298,25 @@ Proof. rewrite subst_args_ok; assumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst 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. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. - (* load notrap2 *) econstructor; split. @@ -308,7 +326,25 @@ Proof. rewrite subst_args_ok; assumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst 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. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. - (* store *) econstructor; split. @@ -318,7 +354,21 @@ Proof. rewrite subst_args_ok; assumption. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := map # pc); trivial. + replace (map # pc) 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. + simpl. tauto. + } + unfold apply_instr'. + unfold get_rb_sem in *. + destruct (map # pc) in *; try contradiction. + rewrite H. + reflexivity. (* call *) - econstructor; split. |