diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 18:01:36 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-27 18:01:36 +0100 |
| commit | 9ec01ece75310b28c79b57697238b57517eb4392 (patch) | |
| tree | 4a8cdc53c29f88547538aad274984fdcfdb011c9 /backend/CSE2.v | |
| parent | 569a32b730608002dbb01088660ecf5bfa19dc02 (diff) | |
| download | compcert-kvx-9ec01ece75310b28c79b57697238b57517eb4392.tar.gz compcert-kvx-9ec01ece75310b28c79b57697238b57517eb4392.zip | |
oper_sound
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 87460f90..a70c3d9f 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -305,6 +305,12 @@ 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. + Section SOUNDNESS. Parameter F V : Type. Parameter genv: Genv.t F V. @@ -509,6 +515,27 @@ Proof. exact KILL. Qed. +Lemma 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 (oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold oper. + destruct in_dec. + { + apply kill_sound; auto. + } + apply oper1_sound; auto. +Qed. + (* Definition apply_instr instr x := match instr with |