diff options
| -rw-r--r-- | cfrontend/Csem.v | 1 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 17 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 13 |
3 files changed, 21 insertions, 10 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index ed5a1b4..a76dcb4 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -742,5 +742,4 @@ Definition exec_program (p: program) (t: trace) (r: val) : Prop := exists b, exists f, exists m1, Genv.find_symbol ge p.(prog_main) = Some b /\ Genv.find_funct_ptr ge b = Some f /\ - type_of_fundef f = Tfunction Tnil (Tint I32 Signed) /\ eval_funcall ge m0 f nil t m1 r. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 5037d43..5b4146b 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1478,12 +1478,19 @@ Theorem transl_program_correct: Csem.exec_program prog t r -> Csharpminor.exec_program tprog t r. Proof. - intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF [TYP EVAL]]]]]]. + intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF EVAL]]]]]. inversion WT; subst. - - assert (type_of_fundef f = Tfunction Tnil (Tint I32 Signed)). + + assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). apply wt_program_main. eapply Genv.find_funct_ptr_symbol_inversion; eauto. + elim H; clear H; intros targs TYP. + assert (targs = Tnil). + inversion EVAL; subst; simpl in TYP. + inversion H0; subst. injection TYP. rewrite <- H6. simpl; auto. + inversion TYP; subst targs0 tres. inversion H. simpl in H0. + inversion H0. destruct targs; simpl in H8; congruence. + subst targs. exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]]. exists b; exists tf; exists m1. split. @@ -1491,10 +1498,10 @@ Proof. rewrite (transform_partial_program2_main transl_fundef transl_globvar prog TRANSL). auto. split. auto. split. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD H). simpl; auto. + generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL). generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL). - intro. eapply H0. + intro. eapply H. eapply function_ptr_well_typed; eauto. auto. Qed. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 7c6a379..797033d 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -162,7 +162,7 @@ Record wt_program (p: program) : Prop := mk_wt_program { wt_program_main: forall fd, In (p.(prog_main), fd) p.(prog_funct) -> - type_of_fundef fd = Tfunction Tnil (Tint I32 Signed) + exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed) }. (** ** Type-checking algorithm *) @@ -386,14 +386,18 @@ Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) | External _ _ _ => true end && if ident_eq id main - then eq_type (type_of_fundef fd) (Tfunction Tnil (Tint I32 Signed)) + then match type_of_fundef fd with + | Tfunction targs tres => eq_type tres (Tint I32 Signed) + | _ => false + end else true. Lemma typecheck_fundef_correct: forall main env id fd, typecheck_fundef main env (id, fd) = true -> wt_fundef env fd /\ - (id = main -> type_of_fundef fd = Tfunction Tnil (Tint I32 Signed)). + (id = main -> + exists targs, type_of_fundef fd = Tfunction targs (Tint I32 Signed)). Proof. intros. unfold typecheck_fundef in H; TrueInv. split. @@ -401,7 +405,8 @@ Proof. constructor. apply typecheck_function_correct; auto. constructor. intro. destruct (ident_eq id main). - apply eq_type_correct; auto. + destruct (type_of_fundef fd); try discriminate. + exists t; decEq; auto. apply eq_type_correct; auto. congruence. Qed. |