Merge branch 'master' into json_export

5 files changed, 204 insertions, 53 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 6ecdb14e..a0e6b259 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -626,7 +626,6 @@ let ewrap = function
       error ("retyping error: " ^  string_of_errmsg msg); ezero
 
 let rec convertExpr env e =
-  (*let ty = convertTyp env e.etyp in*)
   match e.edesc with
   | C.EVar _
   | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _)
@@ -734,9 +733,8 @@ let rec convertExpr env e =
       ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2))
 
   | C.EConditional(e1, e2, e3) ->
-      ewrap (Ctyping.econdition' (convertExpr env e1)
-                                     (convertExpr env e2) (convertExpr env e3)
-                                     (convertTyp env e.etyp))
+      ewrap (Ctyping.econdition (convertExpr env e1)
+                                (convertExpr env e2) (convertExpr env e3))
   | C.ECast(ty1, e1) ->
       ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1))
   | C.ECompound(ty1, ie) ->
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 8ea4e077..db059791 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -208,13 +208,22 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is composed of:
+(** A "pre-program", as produced by the elaborator is composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
-- a list of definitions for structure and union names;
-- the corresponding composite environment;
-*)
+- a list of definitions for structure and union names
+
+A program is composed of the same information, plus the corresponding
+composite environment, and a proof that this environment is consistent
+with the composite definitions. *)
+
+Record pre_program : Type := {
+  pprog_defs: list (ident * globdef fundef type);
+  pprog_public: list ident;
+  pprog_main: ident;
+  pprog_types: list composite_definition
+}.
 
 Record program : Type := {
   prog_defs: list (ident * globdef fundef type);
@@ -232,20 +241,15 @@ Definition program_of_program (p: program) : AST.program fundef type :=
 
 Coercion program_of_program: program >-> AST.program.
 
-Program Definition make_program (types: list composite_definition)
-                                (defs: list (ident * globdef fundef type))
-                                (public: list ident)
-                                (main: ident): res program :=
-  match build_composite_env types with
-  | OK env =>
-      OK {| prog_defs := defs;
-            prog_public := public;
-            prog_main := main;
-            prog_types := types;
-            prog_comp_env := env;
+Program Definition program_of_pre_program (p: pre_program) : res program :=
+  match build_composite_env p.(pprog_types) with
+  | Error e => Error e
+  | OK ce =>
+      OK {| prog_defs := p.(pprog_defs);
+            prog_public := p.(pprog_public);
+            prog_main := p.(pprog_main);
+            prog_types := p.(pprog_types);
+            prog_comp_env := ce;
             prog_comp_env_eq := _ |}
-  | Error msg =>
-      Error msg
   end.
 
-
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 *)
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index dec3279e..13d4049e 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -328,12 +328,13 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_string oc bt.base_type_name
 
     let print_compilation_unit oc tag =
+      let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Configuration.version Configuration.arch in
       print_string oc (Sys.getcwd ());
       print_addr oc (get_start_addr ());
       print_addr oc (get_end_addr ());
       print_uleb128 oc 1;
       print_string oc tag.compile_unit_name;
-      print_string oc ("CompCert "^Configuration.version);
+      print_string oc prod_name;
       print_addr oc (get_stmt_list_addr ())
 
     let print_const_type oc ct =
diff --git a/extraction/extraction.v b/extraction/extraction.v
index f7e99545..ecd2853a 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -156,11 +156,11 @@ Separate Extraction
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
-   Csyntax.make_program Clight.make_program
    Initializers.transl_init Initializers.constval
    Csyntax.Eindex Csyntax.Epreincr
-   Ctyping.retype_function Ctyping.econdition'
+   Ctyping.typecheck_program
    Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr
+   Clight.make_program
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg
    RTL.instr_defs RTL.instr_uses
    Machregs.mregs_for_operation Machregs.mregs_for_builtin