diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 18:14:47 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 18:14:47 +0100 |
commit | fe7d4a81d4999c71f856372716a4a198c46ded8e (patch) | |
tree | a7c2a3d5cc4ded3f34b5d12d92b93e2b1b41d295 /backend/CSE2.v | |
parent | 9ec01ece75310b28c79b57697238b57517eb4392 (diff) | |
download | compcert-kvx-fe7d4a81d4999c71f856372716a4a198c46ded8e.tar.gz compcert-kvx-fe7d4a81d4999c71f856372716a4a198c46ded8e.zip |
gen_oper_sound
Diffstat (limited to 'backend/CSE2.v')
-rw-r--r-- | backend/CSE2.v | 38 |
1 files changed, 37 insertions, 1 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index a70c3d9f..1278d729 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -305,12 +305,20 @@ Definition oper1 (op: operation) (dst : reg) (args : list reg) | Move_case arg' => arg' | Other_case _ => arg end) args)) rel'. + Definition oper (op: operation) (dst : reg) (args : list reg) (rel : RELATION.t) := if List.in_dec peq dst args then kill dst rel else oper1 op dst args rel. +Definition gen_oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match op, args with + | Omove, src::nil => move src dst rel + | _, _ => oper op dst args rel + end. + Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. @@ -536,7 +544,35 @@ Proof. apply oper1_sound; auto. Qed. -(* + +Lemma gen_oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (gen_oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold gen_oper. + destruct op. + { destruct args as [ | h0 t0]. + apply oper_sound; auto. + destruct t0. + { + simpl in *. + replace v with (rs # h0) by congruence. + apply move_sound; auto. + } + apply oper_sound; auto. + } + all: apply oper_sound; auto. +Qed. + (* Definition apply_instr instr x := match instr with | Inop _ |