diff options
Diffstat (limited to 'backend/SelectLongproof.v')
| -rw-r--r-- | backend/SelectLongproof.v | 195 |
1 files changed, 101 insertions, 94 deletions
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 40c11dd8..cdfb1107 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -12,6 +12,7 @@ (** Correctness of instruction selection for integer division *) +Require Import String. Require Import Coqlib. Require Import AST. Require Import Errors. @@ -29,81 +30,96 @@ Require Import SelectOpproof. Require Import SelectLong. Open Local Scope cminorsel_scope. +Open Local Scope string_scope. (** * Axiomatization of the helper functions *) -Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition external_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, - external_call (EF_external id sg) ge vargs m E0 vres m. + external_call (EF_external name sg) ge vargs m E0 vres m. -Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop := +Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop := forall F V (ge: Genv.t F V) m, - external_call (EF_builtin id sg) ge vargs m E0 vres m. + external_call (EF_builtin name sg) ge vargs m E0 vres m. Axiom i64_helpers_correct : - (forall x z, Val.longoffloat x = Some z -> external_implements i64_dtos sig_f_l (x::nil) z) - /\ (forall x z, Val.longuoffloat x = Some z -> external_implements i64_dtou sig_f_l (x::nil) z) - /\ (forall x z, Val.floatoflong x = Some z -> external_implements i64_stod sig_l_f (x::nil) z) - /\ (forall x z, Val.floatoflongu x = Some z -> external_implements i64_utod sig_l_f (x::nil) z) - /\ (forall x z, Val.singleoflong x = Some z -> external_implements i64_stof sig_l_s (x::nil) z) - /\ (forall x z, Val.singleoflongu x = Some z -> external_implements i64_utof sig_l_s (x::nil) z) - /\ (forall x, builtin_implements i64_neg sig_l_l (x::nil) (Val.negl x)) - /\ (forall x y, builtin_implements i64_add sig_ll_l (x::y::nil) (Val.addl x y)) - /\ (forall x y, builtin_implements i64_sub sig_ll_l (x::y::nil) (Val.subl x y)) - /\ (forall x y, builtin_implements i64_mul sig_ii_l (x::y::nil) (Val.mull' x y)) - /\ (forall x y z, Val.divls x y = Some z -> external_implements i64_sdiv sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.divlu x y = Some z -> external_implements i64_udiv sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modls x y = Some z -> external_implements i64_smod sig_ll_l (x::y::nil) z) - /\ (forall x y z, Val.modlu x y = Some z -> external_implements i64_umod sig_ll_l (x::y::nil) z) - /\ (forall x y, external_implements i64_shl sig_li_l (x::y::nil) (Val.shll x y)) - /\ (forall x y, external_implements i64_shr sig_li_l (x::y::nil) (Val.shrlu x y)) - /\ (forall x y, external_implements i64_sar sig_li_l (x::y::nil) (Val.shrl x y)). - -Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (name: ident) (sg: signature) : Prop := - exists b, Genv.find_symbol ge name = Some b + (forall x z, Val.longoffloat x = Some z -> external_implements "__i64_dtos" sig_f_l (x::nil) z) + /\ (forall x z, Val.longuoffloat x = Some z -> external_implements "__i64_dtou" sig_f_l (x::nil) z) + /\ (forall x z, Val.floatoflong x = Some z -> external_implements "__i64_stod" sig_l_f (x::nil) z) + /\ (forall x z, Val.floatoflongu x = Some z -> external_implements "__i64_utod" sig_l_f (x::nil) z) + /\ (forall x z, Val.singleoflong x = Some z -> external_implements "__i64_stof" sig_l_s (x::nil) z) + /\ (forall x z, Val.singleoflongu x = Some z -> external_implements "__i64_utof" sig_l_s (x::nil) z) + /\ (forall x, builtin_implements "__builtin_negl" sig_l_l (x::nil) (Val.negl x)) + /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y)) + /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y)) + /\ (forall x y, builtin_implements "__builtin_mull" sig_ii_l (x::y::nil) (Val.mull' x y)) + /\ (forall x y z, Val.divls x y = Some z -> external_implements "__i64_sdiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.divlu x y = Some z -> external_implements "__i64_udiv" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modls x y = Some z -> external_implements "__i64_smod" sig_ll_l (x::y::nil) z) + /\ (forall x y z, Val.modlu x y = Some z -> external_implements "__i64_umod" sig_ll_l (x::y::nil) z) + /\ (forall x y, external_implements "__i64_shl" sig_li_l (x::y::nil) (Val.shll x y)) + /\ (forall x y, external_implements "__i64_shr" sig_li_l (x::y::nil) (Val.shrlu x y)) + /\ (forall x y, external_implements "__i64_sar" sig_li_l (x::y::nil) (Val.shrl x y)). + +Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (id: ident) (name: string) (sg: signature) : Prop := + exists b, Genv.find_symbol ge id = Some b /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)). +Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop := + helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l + /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l + /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f + /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f + /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s + /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s + /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l + /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l + /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l + /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l + /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l + /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l + /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l. + (** * Correctness of the instruction selection functions for 64-bit operators *) Section CMCONSTR. Variable ge: genv. -Hypothesis HELPERS: - forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared ge hf. Variable sp: val. Variable e: env. Variable m: mem. -Ltac UseHelper := - generalize i64_helpers_correct; intros; - repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end). +Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto. +Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto. Lemma eval_helper: - forall le id sg args vargs vres, + forall le id name sg args vargs vres, eval_exprlist ge sp e m le args vargs -> - In (id, sg) i64_helpers -> - external_implements id sg vargs vres -> + helper_declared ge id name sg -> + external_implements name sg vargs vres -> eval_expr ge sp e m le (Eexternal id sg args) vres. Proof. - intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto. + intros. destruct H0 as (b & P & Q). econstructor; eauto. Qed. Corollary eval_helper_1: - forall le id sg arg1 varg1 vres, + forall le id name sg arg1 varg1 vres, eval_expr ge sp e m le arg1 varg1 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::nil) vres -> + helper_declared ge id name sg -> + external_implements name sg (varg1::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor. Qed. Corollary eval_helper_2: - forall le id sg arg1 arg2 varg1 varg2 vres, + forall le id name sg arg1 arg2 varg1 varg2 vres, eval_expr ge sp e m le arg1 varg1 -> eval_expr ge sp e m le arg2 varg2 -> - In (id, sg) i64_helpers -> - external_implements id sg (varg1::varg2::nil) vres -> + helper_declared ge id name sg -> + external_implements name sg (varg1::varg2::nil) vres -> eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres. Proof. intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor. @@ -394,51 +410,47 @@ Theorem eval_longoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_longuoffloat: forall le a x y, eval_expr ge sp e m le a x -> Val.longuoffloat x = Some y -> - exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v. Proof. intros; unfold longuoffloat. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_floatoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflong x = Some y -> - exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_floatoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.floatoflongu x = Some y -> - exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold floatoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_longofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v. Proof. intros; unfold longofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -452,7 +464,7 @@ Theorem eval_longuofsingle: forall le a x y, eval_expr ge sp e m le a x -> Val.longuofsingle x = Some y -> - exists v, eval_expr ge sp e m le (longuofsingle a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v. Proof. intros; unfold longuofsingle. destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2. @@ -466,22 +478,20 @@ Theorem eval_singleoflong: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflong x = Some y -> - exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflong. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_singleoflongu: forall le a x y, eval_expr ge sp e m le a x -> Val.singleoflongu x = Some y -> - exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v. + exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v. Proof. intros; unfold singleoflongu. econstructor; split. - eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. - auto. + eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. @@ -578,7 +588,7 @@ Qed. Lemma eval_shllimm: forall n, - unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). + unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)). Proof. unfold shllimm; red; intros. apply eval_shift_imm; intros. @@ -608,11 +618,10 @@ Proof. simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. - simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shll: binary_constructor_sound shll Val.shll. +Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll. Proof. unfold shll; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -620,12 +629,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shllimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrluimm: forall n, - unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). + unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)). Proof. unfold shrluimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -654,10 +663,10 @@ Proof. simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. +Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu. Proof. unfold shrlu; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -665,12 +674,12 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrluimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Lemma eval_shrlimm: forall n, - unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). + unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)). Proof. unfold shrlimm; red; intros. apply eval_shift_imm; intros. + (* n = 0 *) @@ -703,10 +712,10 @@ Proof. erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i). rewrite Int64.ofwords_recompose. auto. auto. + (* n >= 64 *) - econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto. Qed. -Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. +Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl. Proof. unfold shrl; red; intros. destruct (is_intconst b) as [n|] eqn:IC. @@ -714,17 +723,17 @@ Proof. exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0. eapply eval_shrlimm; eauto. - (* General case *) - econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl; red; intros. - set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -743,11 +752,11 @@ Qed. Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. unfold subl; red; intros. - set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)). + set (default := Ebuiltin (EF_builtin "__builtin_subl" sig_ll_l) (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v). { - econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -778,7 +787,7 @@ Proof. exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]]. exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]]. exists (Val.longofwords v6 (Val.loword p)); split. - EvalOp. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. + EvalOp. eapply eval_builtin_2; eauto. UseHelper. intros. unfold le1, p in *; subst; simpl in *. inv L3. inv L4. inv L5. simpl in L6. inv L6. simpl. f_equal. symmetry. apply Int64.decompose_mul. @@ -786,7 +795,7 @@ Proof. Qed. Lemma eval_mullimm: - forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)). + forall n, unary_constructor_sound (fun a => mullimm hf a n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. @@ -816,7 +825,7 @@ Proof. apply eval_mull_base; auto. apply eval_longconst. Qed. -Theorem eval_mull: binary_constructor_sound mull Val.mull. +Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull. Proof. unfold mull; red; intros. destruct (is_longconst a) as [p|] eqn:LC1; @@ -834,10 +843,10 @@ Proof. Qed. Lemma eval_binop_long: - forall id sem le a b x y z, + forall id name sem le a b x y z, (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - external_implements id sig_ll_l (x::y::nil) z -> - In (id, sig_ll_l) i64_helpers -> + helper_declared ge id name sig_ll_l -> + external_implements name sig_ll_l (x::y::nil) z -> eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v. @@ -857,15 +866,14 @@ Theorem eval_divl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divls x y = Some z -> - exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_modl: @@ -873,15 +881,14 @@ Theorem eval_modl: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modls x y = Some z -> - exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v. Proof. intros. eapply eval_binop_long; eauto. intros; subst; simpl in H1. destruct (Int64.eq q Int64.zero || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. auto. - UseHelper. - simpl; auto 20. + DeclHelper. UseHelper. Qed. Theorem eval_divlu: @@ -889,14 +896,14 @@ Theorem eval_divlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.divlu x y = Some z -> - exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold divlu. - set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(i64_udiv) sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. @@ -932,14 +939,14 @@ Theorem eval_modlu: eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> Val.modlu x y = Some z -> - exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. + exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v. Proof. intros. unfold modlu. - set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). + set (default := Eexternal hf.(i64_umod) sig_ll_l (a ::: b ::: Enil)). assert (DEFAULT: exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). { - econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. } destruct (is_longconst a) as [p|] eqn:LC1; destruct (is_longconst b) as [q|] eqn:LC2. |