diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 17:46:45 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 17:46:45 +0200 |
commit | a095ac045485f5693d937864f7990ab5de427f1d (patch) | |
tree | 2abc2af9bb9a96648325f6a86286d5ab1785abd9 /mppa_k1c/SelectOpproof.v | |
parent | a17d3c0419ef5531142c4826d962009c9ba81fbc (diff) | |
download | compcert-kvx-a095ac045485f5693d937864f7990ab5de427f1d.tar.gz compcert-kvx-a095ac045485f5693d937864f7990ab5de427f1d.zip |
more maddx
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 583b6f02..25b34fb9 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -183,6 +183,66 @@ Proof. auto. Qed. +Theorem eval_addimm_shlimm: + forall sh k2, unary_constructor_sound (addimm_shlimm sh k2) (fun x => ExtValues.addx sh x (Vint k2)). +Proof. + red; unfold addimm_shlimm; intros. + destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. + - TrivialExists. simpl. + f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e1. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e1. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e2. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e2. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e3. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e3. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e4. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e4. + rewrite Int.repr_unsigned. + reflexivity. + } + discriminate. + - unfold addx. rewrite Val.add_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. +Qed. + Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -198,6 +258,12 @@ Proof. + econstructor; split. EvalOp. simpl; eauto. destruct sp; simpl; auto. + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. + + pose proof eval_addimm_shlimm as ADDX. + unfold unary_constructor_sound in ADDX. + unfold addx in ADDX. + rewrite Val.add_commut. + subst x. + apply ADDX; assumption. + TrivialExists. Qed. |