diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 20:50:02 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 20:50:02 +0100 |
| commit | ea12bb63c4ff63c12a383b8b66dff11fc5dc6e65 (patch) | |
| tree | 3356217effc276d4c09ae4850281e360159834f8 /mppa_k1c/NeedOp.v | |
| parent | fe4318192bb29fa25dc163004701a45879c41ec0 (diff) | |
| download | compcert-kvx-ea12bb63c4ff63c12a383b8b66dff11fc5dc6e65.tar.gz compcert-kvx-ea12bb63c4ff63c12a383b8b66dff11fc5dc6e65.zip | |
plus d'infrastructure pour madd
Diffstat (limited to 'mppa_k1c/NeedOp.v')
| -rw-r--r-- | mppa_k1c/NeedOp.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index 12d7a4f7..801a520e 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -25,6 +25,7 @@ Require Import NeedDomain. Definition op1 (nv: nval) := nv :: nil. Definition op2 (nv: nval) := nv :: nv :: nil. +Definition op3 (nv: nval) := nv :: nv :: nv :: nil. Definition needs_of_condition (cond: condition): list nval := nil. @@ -68,6 +69,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ororimm n => op1 (ror nv n) | Oshruimm n => op1 (shruimm nv n) | Oshrximm n => op1 (default nv) + | Omadd => op3 (modarith nv) + | Omaddimm n => op2 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) @@ -189,6 +192,9 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply ror_sound; auto. + (* madd *) +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. +- apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. Qed. Lemma operation_is_redundant_sound: |