diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 11:17:19 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 11:17:19 +0200 |
| commit | 5809fa295f23952a2d8b043f6da69d61da3568de (patch) | |
| tree | 1e8890f40a837786d824d1a8cd401c16aee93832 /mppa_k1c/Op.v | |
| parent | bb185aa85ddf32feed61d7888c1b199fffdd821f (diff) | |
| download | compcert-kvx-5809fa295f23952a2d8b043f6da69d61da3568de.tar.gz compcert-kvx-5809fa295f23952a2d8b043f6da69d61da3568de.zip | |
progress
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 8293af1e..f6433f90 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -198,7 +198,8 @@ Inductive operation : Type := | Oselectl (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectf (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *) - | Oextfz (stop : Z) (start : Z). + | Oextfz (stop : Z) (start : Z) + | Oextfs (stop : Z) (start : Z). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -500,6 +501,7 @@ Definition eval_operation | (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m) | (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m) | (Oextfz stop start), v0::nil => Some (Val.extfz stop start v0) + | (Oextfs stop start), v0::nil => Some (Val.extfs stop start v0) | _, _ => None end. @@ -693,7 +695,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong) | Oselectf cond => (Tfloat :: Tfloat :: (arg_type_of_condition0 cond) :: nil, Tfloat) | Oselectfs cond => (Tsingle :: Tsingle :: (arg_type_of_condition0 cond) :: nil, Tsingle) - | Oextfz _ _ => (Tint :: nil, Tint) + | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -971,6 +973,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). destruct (_ && _ && _). + destruct v0; simpl; trivial. + constructor. + (* extfs *) + - unfold Val.extfs. + destruct (_ && _ && _). + + destruct v0; simpl; trivial. + + constructor. Qed. End SOUNDNESS. @@ -1586,6 +1593,12 @@ Proof. destruct (_ && _ && _). + inv H4; trivial. + trivial. + + (* extfs *) + - unfold Val.extfs. + destruct (_ && _ && _). + + inv H4; trivial. + + trivial. Qed. Lemma eval_addressing_inj: |