diff options
Diffstat (limited to 'x86/Op.v')
| -rw-r--r-- | x86/Op.v | 115 |
1 files changed, 108 insertions, 7 deletions
@@ -742,6 +742,42 @@ Proof with (try exact I; try reflexivity). 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 | Odivl | Odivu | Odivlu + | Omod | Omodl | Omodu | Omodlu + | Oshrximm _ | Oshrxlimm _ + | Ointoffloat + | Ointofsingle + | Olongoffloat + | Olongofsingle + | Osingleofint + | Osingleoflong + | Ofloatofint + | Ofloatoflong + | Olea _ | Oleal _ (* TODO this is suboptimal *) => true + | _ => false + end. + +Definition args_of_operation op := + if eq_operation op Omove + then 1%nat + else List.length (fst (type_of_operation op)). + +Lemma is_trapping_op_sound: + forall op vl sp m, + is_trapping_op op = false -> + (List.length vl) = args_of_operation op -> + eval_operation genv sp op vl m <> None. +Proof. + unfold args_of_operation. + destruct op; destruct eq_operation; 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 *) @@ -963,7 +999,7 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) -Definition condition_depends_on_memory (c: condition) : bool := +Definition cond_depends_on_memory (c: condition) : bool := match c with | Ccompu _ => negb Archi.ptr64 | Ccompuimm _ _ => negb Archi.ptr64 @@ -974,14 +1010,14 @@ Definition condition_depends_on_memory (c: condition) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp c => condition_depends_on_memory c - | Osel c ty => condition_depends_on_memory c + | Ocmp c => cond_depends_on_memory c + | Osel c ty => cond_depends_on_memory c | _ => false end. -Lemma condition_depends_on_memory_correct: +Lemma cond_depends_on_memory_correct: forall c args m1 m2, - condition_depends_on_memory c = false -> + cond_depends_on_memory c = false -> eval_condition c args m1 = eval_condition c args m2. Proof. intros until m2. @@ -995,12 +1031,36 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence; intros C. -- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- f_equal; f_equal; apply cond_depends_on_memory_correct; auto. - destruct args; auto. destruct args; auto. - rewrite (condition_depends_on_memory_correct c args m1 m2 C). + rewrite (cond_depends_on_memory_correct c args m1 m2 C). auto. Qed. +Lemma cond_valid_pointer_eq: + forall cond args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_condition cond args m1 = eval_condition cond args m2. +Proof. + intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. + all: repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct c; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := @@ -1199,6 +1259,21 @@ Proof. unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj. 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. + Lemma eval_operation_inj: forall op sp1 vl1 sp2 vl2 v1, (forall id ofs, @@ -1425,6 +1500,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 until vl2. intros Hlessdef Heval1. + destruct addr; simpl in *; + inv Hlessdef; trivial; try discriminate; + inv H0; trivial; try discriminate; + inv H2; trivial; try discriminate. +Qed. + End EVAL_LESSDEF. (** Compatibility of the evaluation functions with memory injections. *) @@ -1477,6 +1565,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 -> |