From 5ff8ebb7eea2f1aee002863b97690817c6ba61cb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 6 Jun 2019 11:51:15 +0200
Subject: 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.
---
 backend/Cminortyping.v | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'backend')

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',
-- 
cgit