diff options
Diffstat (limited to 'kvx/Op.v')
| -rw-r--r-- | kvx/Op.v | 24 |
1 files changed, 23 insertions, 1 deletions
@@ -219,7 +219,11 @@ Inductive operation : Type := | Oinsfl (stop : Z) (start : Z) | Osel (c0 : condition0) (ty : typ) | Oselimm (c0 : condition0) (imm: int) - | Osellimm (c0 : condition0) (imm: int64). + | Osellimm (c0 : condition0) (imm: int64) + | Oabsdiff + | Oabsdiffimm (imm: int) + | Oabsdiffl + | Oabsdifflimm (imm: int64). (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -476,6 +480,10 @@ Definition eval_operation | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty) | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) + | Oabsdiff, v0::v1::nil => Some(ExtValues.absdiff v0 v1) + | (Oabsdiffimm n1), v0::nil => Some(ExtValues.absdiff v0 (Vint n1)) + | Oabsdiffl, v0::v1::nil => Some(ExtValues.absdiffl v0 v1) + | (Oabsdifflimm n1), v0::nil => Some(ExtValues.absdiffl v0 (Vlong n1)) | _, _ => None end. @@ -691,6 +699,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty) | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint) | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong) + | Oabsdiff => (Tint :: Tint :: nil, Tint) + | Oabsdiffimm _ => (Tint :: nil, Tint) + | Oabsdiffl => (Tlong :: Tlong :: nil, Tlong) + | Oabsdifflimm _ => (Tlong :: nil, Tlong) end. (* FIXME: two Tptr ?! *) @@ -1026,6 +1038,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.select. destruct (eval_condition0 _ _ m). + apply Val.normalize_type. + constructor. + (* oabsdiff *) + - destruct v0; destruct v1; cbn; trivial. + - destruct v0; cbn; trivial. + - destruct v0; destruct v1; cbn; trivial. + - destruct v0; cbn; trivial. Qed. Definition is_trapping_op (op : operation) := @@ -1738,6 +1755,11 @@ Proof. symmetry. eapply eval_condition0_inj; eassumption. + left. trivial. + (* Oabsdiff *) + - apply ExtValues.absdiff_inject; trivial. + - apply ExtValues.absdiff_inject; trivial. + - apply ExtValues.absdiffl_inject; trivial. + - apply ExtValues.absdiffl_inject; trivial. Qed. Lemma eval_addressing_inj: |