diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 21:54:18 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 21:54:18 +0200 |
| commit | 66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2 (patch) | |
| tree | ce2b6bb7c0dc8d00eac6adf7f66388528bfe650a /mppa_k1c/SelectLongproof.v | |
| parent | 17a8d91a82f67d7f62f8cbad41ba76a4b0b82a30 (diff) | |
| download | compcert-kvx-66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2.tar.gz compcert-kvx-66ee59d3dc8a861b468cfaf0ff46fc71dfb8fec2.zip | |
option -faddx (off by default until questions cleared)
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3c9f64d5..58a4c39a 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -124,6 +124,8 @@ Theorem eval_addlimm_shllimm: forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)). Proof. red; unfold addlimm_shllimm; intros. + destruct (Compopts.optim_addx tt). + { destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. - TrivialExists. simpl. f_equal. @@ -178,6 +180,13 @@ Proof. repeat (try eassumption; try econstructor). simpl. reflexivity. + } + { unfold addxl. rewrite Val.addl_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } Qed. Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). @@ -188,7 +197,7 @@ Proof. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. -- destruct (Compopts.optim_fglobaladdroffset _). +- destruct (Compopts.optim_globaladdroffset _). + econstructor; split. EvalOp. simpl; eauto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. @@ -211,6 +220,8 @@ Proof. red. intros. unfold addl_shllimm. + destruct (Compopts.optim_addx tt). + { destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT. - TrivialExists. simpl. @@ -235,7 +246,11 @@ Proof. discriminate. (* Oaddxl *) - TrivialExists; - repeat econstructor; eassumption. + repeat econstructor; eassumption. + } + { TrivialExists; + repeat econstructor; eassumption. + } Qed. Theorem eval_addl: binary_constructor_sound addl Val.addl. |