diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-06 11:51:15 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-06 11:52:53 +0200 |
| commit | 5ff8ebb7eea2f1aee002863b97690817c6ba61cb (patch) | |
| tree | 65afecd008a5252c6eae53674a2bf5c902a2f53b /backend/Cminortyping.v | |
| parent | 8e3a73448c5ddfa4be3871d7f4fd80281a7549f4 (diff) | |
| download | compcert-kvx-5ff8ebb7eea2f1aee002863b97690817c6ba61cb.tar.gz compcert-kvx-5ff8ebb7eea2f1aee002863b97690817c6ba61cb.zip | |
Cminortyping: relax typechecking of function calls
Sometimes the result of a void function is assigned to a variable.
This can occur with C conditional expressions ?: at type void,
e.g. the "assert" macro of MacOS.
A similar relaxation was already there in RTLtyping.
Diffstat (limited to 'backend/Cminortyping.v')
| -rw-r--r-- | backend/Cminortyping.v | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v index fed8be95..fccbda27 100644 --- a/backend/Cminortyping.v +++ b/backend/Cminortyping.v @@ -124,11 +124,10 @@ Definition type_assign (e: S.typenv) (id: ident) (a: expr) : res S.typenv := S.set e1 id (type_of_chunk chunk) end. -Definition opt_set (e: S.typenv) (optid: option ident) (optty: option typ) : res S.typenv := - match optid, optty with - | None, _ => OK e - | Some id, Some ty => S.set e id ty - | _, _ => Error (msg "inconsistent call") +Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv := + match optid with + | None => OK e + | Some id => S.set e id ty end. Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := @@ -140,7 +139,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Scall optid sg fn args => do e1 <- type_expr e fn Tptr; do e2 <- type_exprlist e1 args sg.(sig_args); - opt_set e2 optid sg.(sig_res) + opt_set e2 optid (proj_sig_res sg) | Stailcall sg fn args => assertion (opt_typ_eq sg.(sig_res) tret); do e1 <- type_expr e fn Tptr; @@ -148,7 +147,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv := | Sbuiltin optid ef args => let sg := ef_sig ef in do e1 <- type_exprlist e args sg.(sig_args); - opt_set e1 optid sg.(sig_res) + opt_set e1 optid (proj_sig_res sg) | Sseq s1 s2 => do e1 <- type_stmt tret e s1; type_stmt tret e1 s2 | Sifthenelse a s1 s2 => @@ -207,7 +206,10 @@ Inductive wt_expr: expr -> typ -> Prop := wt_expr (Eload chunk a1) (type_of_chunk chunk). Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop := - match optid with Some id => optty = Some (env id) | _ => True end. + match optid with + | Some id => match optty with Some ty => ty | None => Tint end = env id + | _ => True + end. Inductive wt_stmt: stmt -> Prop := | wt_Sskip: @@ -358,12 +360,13 @@ Proof. Qed. Hint Resolve opt_set_incr: ty. -Lemma opt_set_sound: forall te optid optty e e', - opt_set e optid optty = OK e' -> S.satisf te e' -> wt_opt_assign te optid optty. +Lemma opt_set_sound: forall te optid sg e e', + opt_set e optid (proj_sig_res sg) = OK e' -> S.satisf te e' -> + wt_opt_assign te optid sg.(sig_res). Proof. - unfold opt_set; intros; red. destruct optid; [destruct optty |]; try (monadInv H). + unfold opt_set; intros; red. destruct optid. - erewrite S.set_sound by eauto. auto. -- auto. +- inv H. auto. Qed. Lemma type_stmt_incr: forall te tret s e e', |