diff options
Diffstat (limited to 'arm/Op.v')
| -rw-r--r-- | arm/Op.v | 105 |
1 files changed, 99 insertions, 6 deletions
@@ -140,7 +140,9 @@ Inductive operation : Type := | Olowlong: operation (**r [rd = low-word(r1)] *) | Ohighlong: operation (**r [rd = high-word(r1)] *) (*c Boolean tests: *) - | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | Ocmp: condition -> operation (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | Osel: condition -> typ -> operation. + (**r [rd = rs1] if condition holds, [rd = rs2] otherwise. *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -174,7 +176,7 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq typ_eq; intros. generalize Float.eq_dec Float32.eq_dec; intros. generalize eq_shift; intro. generalize eq_condition; intro. @@ -294,6 +296,7 @@ Definition eval_operation | Olowlong, v1::nil => Some(Val.loword v1) | Ohighlong, v1::nil => Some(Val.hiword v1) | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m)) + | Osel c ty, v1::v2::vl => Some(Val.select (eval_condition c vl m) v1 v2 ty) | _, _ => None end. @@ -419,6 +422,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) | Ocmp c => (type_of_condition c, Tint) + | Osel c ty => (ty :: ty :: type_of_condition c, ty) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -511,8 +515,35 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct (eval_condition c vl m)... destruct b... + unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I. Qed. + +Definition is_trapping_op (op : operation) := + match op with + | Odiv | Odivu + | Oshrximm _ + | Ointoffloat | Ointuoffloat + | Ointofsingle | Ointuofsingle + | Ofloatofint | Ofloatofintu + | Osingleofint | Osingleofintu => true + | _ => false + end. + + +Lemma is_trapping_op_sound: + forall op vl sp m, + op <> Omove -> + is_trapping_op op = false -> + (List.length vl) = (List.length (fst (type_of_operation op))) -> + eval_operation genv sp op vl m <> None. +Proof. + destruct op; intros; simpl in *; try congruence. + all: try (destruct vl as [ | vh1 vl1]; try discriminate). + all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). + all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). + all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). +Qed. End SOUNDNESS. (** * Manipulating and transforming operations *) @@ -532,7 +563,7 @@ Lemma mk_shift_amount_eq: forall n, Int.ltu n Int.iwordsize = true -> s_amount (mk_shift_amount n) = n. Proof. intros; simpl. unfold Int.modu. transitivity (Int.repr (Int.unsigned n)). - decEq. apply Zmod_small. apply Int.ltu_inv; auto. + decEq. apply Z.mod_small. apply Int.ltu_inv; auto. apply Int.repr_unsigned. Qed. @@ -682,19 +713,37 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) +Definition condition_depends_on_memory (c: condition) : bool := + match c with + | Ccompu _ | Ccompushift _ _| Ccompuimm _ _ => true + | _ => false + end. + Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _ | Ccompushift _ _| Ccompuimm _ _) => true + | Ocmp c => condition_depends_on_memory c + | Osel c ty => condition_depends_on_memory c | _ => false end. +Lemma condition_depends_on_memory_correct: + forall c args m1 m2, + condition_depends_on_memory c = false -> + eval_condition c args m1 = eval_condition c args m2. +Proof. + intros. destruct c; simpl; auto; discriminate. +Qed. + Lemma op_depends_on_memory_correct: forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. - intros. destruct c; simpl; auto; congruence. + intros until m2. destruct op; simpl; try congruence; intros C. +- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- destruct args; auto. destruct args; auto. + rewrite (condition_depends_on_memory_correct c args m1 m2 C). + auto. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -929,6 +978,10 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + + apply Val.select_inject; auto. + destruct (eval_condition c vl1 m1) eqn:?; auto. + right; symmetry; eapply eval_condition_inj; eauto. Qed. Lemma eval_addressing_inj: @@ -948,6 +1001,20 @@ Proof. apply Val.offset_ptr_inject; auto. Qed. +Lemma eval_addressing_inj_none: + forall addr sp1 vl1 sp2 vl2, + (forall id ofs, + In id (globals_addressing addr) -> + Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) -> + Val.inject f sp1 sp2 -> + Val.inject_list f vl1 vl2 -> + eval_addressing ge1 sp1 addr vl1 = None -> + eval_addressing ge2 sp2 addr vl2 = None. +Proof. + intros until vl2. intros Hglobal Hinjsp Hinjvl. + destruct addr; simpl in *; + inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate. +Qed. End EVAL_COMPAT. (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *) @@ -1053,6 +1120,19 @@ Proof. destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. Qed. +Lemma eval_addressing_lessdef_none: + forall sp addr vl1 vl2, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = None -> + eval_addressing genv sp addr vl2 = None. +Proof. + intros. rewrite val_inject_list_lessdef in H. + eapply eval_addressing_inj_none with (sp1 := sp). + intros. rewrite <- val_inject_lessdef; auto. + rewrite <- val_inject_lessdef; auto. + eauto. auto. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1105,6 +1185,19 @@ Proof. econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. +Lemma eval_addressing_inject_none: + forall addr vl1 vl2, + Val.inject_list f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None -> + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None. +Proof. + intros. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto. + intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> |