summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 19:44:10 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-06 19:44:10 +0000
commit708cd2c7767b497b9ac3dae1ce51973195d00acc (patch)
treeadb042e3603452fc7702db0c6eb55825864e0ded /cfrontend
parente231ac08558e959f2ea2664082c62ced9e485c1b (diff)
Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)
Ctyping: relaxation de l'hypothese de typage sur main Cshmgenproof3: adaptation a ces changements. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@82 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/Csem.v1
-rw-r--r--cfrontend/Cshmgenproof3.v17
-rw-r--r--cfrontend/Ctyping.v13
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.