diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 17:16:48 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 17:16:48 +0200 |
| commit | 7d00b4e01908f9cb67a47a1fa5d248e1b301c143 (patch) | |
| tree | 391634d74f0eb58f3b8f404d6831cc431f2eb0d1 /kvx/ValueAOp.v | |
| parent | 6ef6b018bb947023e5922f6d873ef2be94e3bcb4 (diff) | |
| parent | b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 (diff) | |
| download | compcert-kvx-7d00b4e01908f9cb67a47a1fa5d248e1b301c143.tar.gz compcert-kvx-7d00b4e01908f9cb67a47a1fa5d248e1b301c143.zip | |
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
Diffstat (limited to 'kvx/ValueAOp.v')
| -rw-r--r-- | kvx/ValueAOp.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 0206352e..87554258 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -349,7 +349,7 @@ Proof. intros v x; intro MATCH; inversion MATCH; - simpl; + cbn; constructor. Qed. @@ -361,9 +361,9 @@ Lemma triple_op_float_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma triple_op_single_sound: @@ -374,9 +374,9 @@ Lemma triple_op_single_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma fmaddf_sound : @@ -420,9 +420,9 @@ Proof. intros until aargs; intros VM. inv VM. destruct cond; auto with va. inv H0. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. inv H2. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. destruct cond; auto with va. Qed. @@ -432,7 +432,7 @@ Theorem eval_static_condition0_sound: cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). Proof. intros until aarg; intro VM. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. Qed. Lemma symbol_address_sound: @@ -541,8 +541,8 @@ Proof. + eauto with va. + destruct n; destruct shift; reflexivity. - (* shrx *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. + inv H1; cbn; try constructor. + all: destruct Int.ltu; [cbn | constructor; fail]. all: auto with va. - inv H1; constructor. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with @@ -580,12 +580,12 @@ Proof. (* insf *) - unfold insf, eval_static_insf. destruct (is_bitfield _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* insfl *) - unfold insfl, eval_static_insfl. destruct (is_bitfieldl _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* select *) - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. |