diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-21 16:34:06 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-21 16:34:06 +0200 |
commit | 606afe8cc8def940f991d07b8f6adb6bae7ce691 (patch) | |
tree | 29fe6749b270761087514b75ef7116b936398101 | |
parent | 50ed2827867238a98f2036f799d4d6f354a2581c (diff) | |
parent | b686f8df572ea77c8832637bed4e4cd81f0931e2 (diff) | |
download | compcert-606afe8cc8def940f991d07b8f6adb6bae7ce691.tar.gz compcert-606afe8cc8def940f991d07b8f6adb6bae7ce691.zip |
Merge branch 'master' into json_export
-rw-r--r-- | cfrontend/C2C.ml | 6 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 40 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 204 | ||||
-rw-r--r-- | debug/DwarfPrinter.ml | 3 | ||||
-rw-r--r-- | extraction/extraction.v | 4 |
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 |