Ctyping: better typing of conditional expressions.

Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.

Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline.  Then, retyping would
no longer be performed in C2C.  We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.

1 files changed, 176 insertions, 28 deletions

diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 2582fff8..834895bc 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -157,31 +157,108 @@ Definition type_deref (ty: type) : res type :=
   | _ => Error (msg "operator prefix *")
   end.
 
+(** Inferring the type of a conditional expression: the merge of the types
+  of the two arms. *)
+
+Definition attr_combine (a1 a2: attr) : attr :=
+  {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile);
+     attr_alignas :=
+       match a1.(attr_alignas), a2.(attr_alignas) with
+       | None, al2 => al2
+       | al1, None => al1
+       | Some n1, Some n2 => Some (N.max n1 n2)
+       end
+  |}.
+
+Definition intsize_eq: forall (x y: intsize), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Definition signedness_eq: forall (x y: signedness), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Definition floatsize_eq: forall (x y: floatsize), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Definition callconv_eq: forall (x y: calling_convention), {x=y} + {x<>y}.
+Proof. decide equality; apply bool_dec. Defined.
+
+Fixpoint type_combine (ty1 ty2: type) : res type :=
+  match ty1, ty2 with
+  | Tvoid, Tvoid => OK Tvoid
+  | Tint sz1 sg1 a1, Tint sz2 sg2 a2 =>
+      if intsize_eq sz1 sz2 && signedness_eq sg1 sg2
+      then OK (Tint sz1 sg1 (attr_combine a1 a2))
+      else Error (msg "incompatible int types")
+  | Tlong sg1 a1, Tlong sg2 a2 =>
+      if signedness_eq sg1 sg2
+      then OK (Tlong sg1 (attr_combine a1 a2))
+      else Error (msg "incompatible long types")
+  | Tfloat sz1 a1, Tfloat sz2 a2 =>
+      if floatsize_eq sz1 sz2
+      then OK (Tfloat sz1 (attr_combine a1 a2))
+      else Error (msg "incompatible float types")
+  | Tpointer t1 a1, Tpointer t2 a2 =>
+      do t <- type_combine t1 t2; OK (Tpointer t (attr_combine a1 a2))
+  | Tarray t1 sz1 a1, Tarray t2 sz2 a2 =>
+      do t <- type_combine t1 t2;
+      if zeq sz1 sz2
+      then OK (Tarray t sz1 (attr_combine a1 a2))
+      else Error (msg "incompatible array types")
+  | Tfunction args1 res1 cc1, Tfunction args2 res2 cc2 =>
+      do res <- type_combine res1 res2;
+      do args <-
+        match args1, args2 with
+        | Tnil, _ => OK args2    (* tolerance for unprototyped functions *)
+        | _, Tnil => OK args1
+        | _, _    => typelist_combine args1 args2
+        end;
+      if callconv_eq cc1 cc2
+      then OK (Tfunction args res cc1)
+      else Error (msg "incompatible function types")
+  | Tstruct id1 a1, Tstruct id2 a2 =>
+      if ident_eq id1 id2
+      then OK (Tstruct id1 (attr_combine a1 a2))
+      else Error (msg "incompatible struct types")
+  | Tunion id1 a1, Tunion id2 a2 =>
+      if ident_eq id1 id2
+      then OK (Tunion id1 (attr_combine a1 a2))
+      else Error (msg "incompatible union types")
+  | _, _ =>
+      Error (msg "incompatible types")
+  end
+
+with typelist_combine (tl1 tl2: typelist) : res typelist :=
+  match tl1, tl2 with
+  | Tnil, Tnil => OK Tnil
+  | Tcons t1 tl1, Tcons t2 tl2 =>
+      do t <- type_combine t1 t2;
+      do tl <- typelist_combine tl1 tl2;
+      OK (Tcons t tl)
+  | _, _ =>
+      Error (msg "incompatible function types")
+  end.
+
 Definition is_void (ty: type) : bool :=
   match ty with Tvoid => true | _ => false end.
 
-Definition type_join (ty1 ty2: type) : res type :=
+Definition type_conditional (ty1 ty2: type) : res type :=
   match typeconv ty1, typeconv ty2 with
   | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) =>
       binarith_type ty1 ty2 "conditional expression"
   | Tpointer t1 a1, Tpointer t2 a2 =>
-      OK (Tpointer (if is_void t1 || is_void t2 then Tvoid else t1) noattr)
+      let t :=
+        if is_void t1 || is_void t2 then Tvoid else
+          match type_combine t1 t2 with
+          | OK t => t
+          | Error _ => Tvoid   (* tolerance *)
+          end
+       in OK (Tpointer t noattr)
   | Tpointer t1 a1, Tint _ _ _ =>
       OK (Tpointer t1 noattr)
   | Tint _ _ _, Tpointer t2 a2 =>
       OK (Tpointer t2 noattr)
-  | Tvoid, Tvoid =>
-      OK Tvoid
-  | Tstruct id1 a1, Tstruct id2 a2 =>
-      if ident_eq id1 id2
-      then OK (Tstruct id1 noattr)
-      else Error (msg "conditional expression")
-  | Tunion id1 a1, Tunion id2 a2 =>
-      if ident_eq id1 id2
-      then OK (Tunion id1 noattr)
-      else Error (msg "conditional expression")
-  | _, _ =>
-      Error (msg "conditional expression")
+  | t1, t2 =>
+      type_combine t1 t2
   end.
 
 (** * Specification of the type system *)
@@ -603,7 +680,7 @@ Definition eseqor (r1 r2: expr) : res expr :=
 Definition econdition (r1 r2 r3: expr) : res expr :=
   do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
   do y1 <- check_bool (typeof r1);
-  do ty <- type_join (typeof r2) (typeof r3);
+  do ty <- type_conditional (typeof r2) (typeof r3);
   OK (Econdition r1 r2 r3 ty).
 
 Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr :=
@@ -822,6 +899,23 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f
                  f.(fn_vars)
                  s).
 
+Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef :=
+  match fd with
+  | Internal f => do f' <- retype_function ce e f; OK (Internal f')
+  | External id args res cc => OK fd
+  end.
+
+Definition typecheck_program (p: program) : res program :=
+  let e := bind_globdef (PTree.empty _) p.(prog_defs) in
+  let ce := p.(prog_comp_env) in
+  do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs);
+  OK {| prog_defs := defs;
+        prog_public := p.(prog_public);
+        prog_main := p.(prog_main);
+        prog_types := p.(prog_types);
+        prog_comp_env := ce;
+        prog_comp_env_eq := p.(prog_comp_env_eq) |}.
+
 (** Soundness of the smart constructors.  *)
 
 Lemma check_cast_sound:
@@ -882,14 +976,42 @@ Proof.
   destruct i; auto. 
 Qed.
 
-Lemma type_join_cast:
+Lemma type_combine_cast:
   forall t1 t2 t,
-  type_join t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t.
-Proof.
-  intros. unfold type_join in H. 
+  type_combine t1 t2 = OK t ->
+  match t1 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end ->
+  match t2 with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end ->
+  wt_cast t1 t /\ wt_cast t2 t.
+Proof.
+  intros.
+  unfold wt_cast; destruct t1; try discriminate; destruct t2; simpl in H; inv H.
+- simpl; split; congruence.
+- destruct (intsize_eq i i0 && signedness_eq s s0); inv H3.
+  simpl; destruct i; split; congruence.
+- destruct (signedness_eq s s0); inv H3.
+  simpl; split; congruence.
+- destruct (floatsize_eq f f0); inv H3.
+  simpl; destruct f0; split; congruence.
+- monadInv H3. simpl; split; congruence.
+- contradiction.
+- contradiction.
+- destruct (ident_eq i i0); inv H3. simpl; split; congruence.
+- destruct (ident_eq i i0); inv H3. simpl; split; congruence.
+Qed.
+
+Lemma type_conditional_cast:
+  forall t1 t2 t,
+  type_conditional t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t.
+Proof.
+  intros. 
+  assert (A: forall x, match typeconv x with Tarray _ _ _ => False | Tfunction _ _ _ => False | _ => True end).
+  { destruct x; simpl; auto. destruct i; auto. }
+  assert (D: type_combine (typeconv t1) (typeconv t2) = OK t -> wt_cast t1 t /\ wt_cast t2 t).
+  { intros. apply type_combine_cast in H0. destruct H0; split; apply typeconv_cast; auto. 
+    apply A. apply A. }
+  clear A. unfold type_conditional in H.
   destruct (typeconv t1) eqn:T1; try discriminate;
-  destruct (typeconv t2) eqn:T2; inv H.
-- unfold wt_cast; simpl; split; congruence.
+  destruct (typeconv t2) eqn:T2; inv H; auto using D.
 - eapply binarith_type_cast; eauto.
 - eapply binarith_type_cast; eauto.
 - split; apply typeconv_cast; unfold wt_cast. 
@@ -900,12 +1022,6 @@ Proof.
   rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
 - split; apply typeconv_cast; unfold wt_cast. 
   rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
-- destruct (ident_eq i i0); inv H1. 
-  split; apply typeconv_cast; unfold wt_cast. 
-  rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
-- destruct (ident_eq i i0); inv H1. 
-  split; apply typeconv_cast; unfold wt_cast. 
-  rewrite T1; simpl; congruence. rewrite T2; simpl; congruence.
 Qed.
 
 Section SOUNDNESS_CONSTRUCTORS.
@@ -1025,7 +1141,7 @@ Lemma econdition_sound:
   forall r1 r2 r3 a, econdition r1 r2 r3 = OK a ->
   wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.
 Proof.
-  intros. monadInv H. apply type_join_cast in EQ3. destruct EQ3. eauto 10 with ty. 
+  intros. monadInv H. apply type_conditional_cast in EQ3. destruct EQ3. eauto 10 with ty. 
 Qed.
 
 Lemma econdition'_sound:
@@ -1206,6 +1322,38 @@ Proof.
   intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. 
 Qed.
 
+Theorem typecheck_program_sound:
+  forall p p', typecheck_program p = OK p' -> wt_program p'.
+Proof.
+  unfold typecheck_program; intros. monadInv H. 
+  rename x into defs.
+  constructor; simpl.
+  set (ce := prog_comp_env p) in *.
+  set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *.
+  set (e' := bind_globdef (PTree.empty type) defs) in *.
+  assert (MATCH:
+    list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs).
+  {
+    revert EQ; generalize (prog_defs p) defs.
+    induction l as [ | [id gd] l ]; intros l'; simpl; intros.
+    inv EQ. constructor. 
+    destruct gd as [f | v].
+    destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ.
+    constructor; auto. constructor; auto. 
+    monadInv EQ. constructor; auto. destruct v; constructor; auto. }
+  assert (ENVS: e' = e).
+  { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type). 
+    induction l as [ | [id gd] l ]; intros l' t M; inv M.
+    auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto. 
+    unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto. 
+  }
+  rewrite ENVS.
+  intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros.
+  contradiction.
+  destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2. 
+  monadInv H2. eapply retype_function_sound; eauto. congruence. 
+Qed.
+
 (** * Subject reduction *)
 
 (** We show that reductions preserve well-typedness *)