diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 28 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 60 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 52 | ||||
| -rw-r--r-- | cfrontend/Csyntax.v | 40 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 213 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 12 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 6 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 36 |
8 files changed, 299 insertions, 148 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 94f13aa1..71328c71 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -437,10 +437,10 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let convertCallconv va attr = +let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_structret = sr <> [] } + { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) @@ -494,7 +494,7 @@ let rec convertTyp env t = | Some tl -> convertParams env tl end, convertTyp env tres, - convertCallconv va a) + convertCallconv va (targs = None) a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> @@ -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) -> @@ -798,7 +796,8 @@ let rec convertExpr env e = let targs = convertTypArgs env [] args and tres = convertTyp env e.etyp in let sg = - signature_of_type targs tres {cc_vararg = true; cc_structret = false} in + signature_of_type targs tres + {cc_vararg = true; cc_unproto = false; cc_structret = false} in Ebuiltin(EF_external(intern_string "printf", sg), targs, convertExprList env args, tres) @@ -847,7 +846,7 @@ let convertAsm loc env txt outputs inputs clobber = let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = - List.map intern_string clobber in + List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) @@ -1033,11 +1032,12 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Internal {fn_return = ret; - fn_callconv = convertCallconv fd.fd_vararg fd.fd_attrib; - fn_params = params; - fn_vars = vars; - fn_body = body'})) + (id', Gfun(Internal + {fn_return = ret; + fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; + fn_params = params; + fn_vars = vars; + fn_body = body'})) (** External function declaration *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 17c59b97..dfc69412 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -163,7 +163,7 @@ Qed. [f b = Some(b', ofs)] means that C#minor block [b] corresponds to a sub-block of Cminor block [b] at offset [ofs]. - A memory injection [f] defines a relation [val_inject f] between + A memory injection [f] defines a relation [Val.inject f] between values and a relation [Mem.inject f] between memory states. These relations will be used intensively in our proof of simulation between C#minor and Cminor executions. *) @@ -171,7 +171,7 @@ Qed. (** ** Matching between Cshaprminor's temporaries and Cminor's variables *) Definition match_temps (f: meminj) (le: Csharpminor.temp_env) (te: env) : Prop := - forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ val_inject f v v'. + forall id v, le!id = Some v -> exists v', te!(id) = Some v' /\ Val.inject f v v'. Lemma match_temps_invariant: forall f f' le te, @@ -185,7 +185,7 @@ Qed. Lemma match_temps_assign: forall f le te id v tv, match_temps f le te -> - val_inject f v tv -> + Val.inject f v tv -> match_temps f (PTree.set id v le) (PTree.set id tv te). Proof. intros; red; intros. rewrite PTree.gsspec in *. destruct (peq id0 id). @@ -197,7 +197,7 @@ Qed. Inductive match_var (f: meminj) (sp: block): option (block * Z) -> option Z -> Prop := | match_var_local: forall b sz ofs, - val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + Val.inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> match_var f sp (Some(b, sz)) (Some ofs) | match_var_global: match_var f sp None None. @@ -553,7 +553,7 @@ Qed. Lemma match_callstack_set_temp: forall f cenv e le te sp lo hi cs bound tbound m tm tf id v tv, - val_inject f v tv -> + Val.inject f v tv -> match_callstack f m tm (Frame cenv tf e le te sp lo hi :: cs) bound tbound -> match_callstack f m tm (Frame cenv tf e (PTree.set id v le) (PTree.set id tv te) sp lo hi :: cs) bound tbound. Proof. @@ -1119,7 +1119,7 @@ Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.e Lemma bind_parameters_agree_rec: forall f vars vals tvals le1 le2 te, bind_parameters vars vals le1 = Some le2 -> - val_list_inject f vals tvals -> + Val.inject_list f vals tvals -> match_temps f le1 te -> match_temps f le2 (set_params' tvals vars te). Proof. @@ -1213,7 +1213,7 @@ Qed. Lemma bind_parameters_agree: forall f params temps vals tvals le, bind_parameters params vals (create_undef_temps temps) = Some le -> - val_list_inject f vals tvals -> + Val.inject_list f vals tvals -> list_norepet params -> list_disjoint params temps -> match_temps f le (set_locals temps (set_params tvals params)). @@ -1238,7 +1238,7 @@ Theorem match_callstack_function_entry: list_disjoint (Csharpminor.fn_params fn) (Csharpminor.fn_temps fn) -> alloc_variables Csharpminor.empty_env m (Csharpminor.fn_vars fn) e m' -> bind_parameters (Csharpminor.fn_params fn) args (create_undef_temps fn.(fn_temps)) = Some le -> - val_list_inject f args targs -> + Val.inject_list f args targs -> Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) -> match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> Mem.inject f m tm -> @@ -1259,39 +1259,39 @@ Qed. (** * Compatibility of evaluation functions with respect to memory injections. *) Remark val_inject_val_of_bool: - forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). + forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b). Proof. intros; destruct b; constructor. Qed. Remark val_inject_val_of_optbool: - forall f ob, val_inject f (Val.of_optbool ob) (Val.of_optbool ob). + forall f ob, Val.inject f (Val.of_optbool ob) (Val.of_optbool ob). Proof. intros; destruct ob; simpl. destruct b; constructor. constructor. Qed. Ltac TrivialExists := match goal with - | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] => + | [ |- exists y, Some ?x = Some y /\ Val.inject _ _ _ ] => exists x; split; [auto | try(econstructor; eauto)] - | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vint ?x) _ ] => exists (Vint x); split; [eauto with evalexpr | constructor] - | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vfloat ?x) _ ] => exists (Vfloat x); split; [eauto with evalexpr | constructor] - | [ |- exists y, _ /\ val_inject _ (Vlong ?x) _ ] => + | [ |- exists y, _ /\ Val.inject _ (Vlong ?x) _ ] => exists (Vlong x); split; [eauto with evalexpr | constructor] | _ => idtac end. -(** Compatibility of [eval_unop] with respect to [val_inject]. *) +(** Compatibility of [eval_unop] with respect to [Val.inject]. *) Lemma eval_unop_compat: forall f op v1 tv1 v, eval_unop op v1 = Some v -> - val_inject f v1 tv1 -> + Val.inject f v1 tv1 -> exists tv, eval_unop op tv1 = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct op; simpl; intros. inv H; inv H0; simpl; TrivialExists. @@ -1329,17 +1329,17 @@ Proof. inv H0; simpl in H; inv H. simpl. TrivialExists. Qed. -(** Compatibility of [eval_binop] with respect to [val_inject]. *) +(** Compatibility of [eval_binop] with respect to [Val.inject]. *) Lemma eval_binop_compat: forall f op v1 tv1 v2 tv2 v m tm, eval_binop op v1 v2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> Mem.inject f m tm -> exists tv, eval_binop op tv1 tv2 tm = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct op; simpl; intros. inv H; inv H0; inv H1; TrivialExists. @@ -1401,7 +1401,7 @@ Proof. destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). destruct b; simpl; constructor. - symmetry. eapply val_cmpu_bool_inject; eauto. + symmetry. eapply Val.cmpu_bool_inject; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. @@ -1429,7 +1429,7 @@ Lemma var_addr_correct: eval_var_addr ge e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm (var_addr cenv id) tv - /\ val_inject f (Vptr b Int.zero) tv. + /\ Val.inject f (Vptr b Int.zero) tv. Proof. unfold var_addr; intros. assert (match_var f sp e!id cenv!id). @@ -1474,7 +1474,7 @@ Qed. Remark bool_of_val_inject: forall f v tv b, - Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b. + Val.bool_of_val v b -> Val.inject f v tv -> Val.bool_of_val tv b. Proof. intros. inv H0; inv H; constructor; auto. Qed. @@ -1484,7 +1484,7 @@ Lemma transl_constant_correct: Csharpminor.eval_constant cst = Some v -> exists tv, eval_constant tge sp (transl_constant cst) = Some tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. destruct cst; simpl; intros; inv H. exists (Vint i); auto. @@ -1505,7 +1505,7 @@ Lemma transl_expr_correct: (TR: transl_expr cenv a = OK ta), exists tv, eval_expr tge (Vptr sp Int.zero) te tm ta tv - /\ val_inject f v tv. + /\ Val.inject f v tv. Proof. induction 3; intros; simpl in TR; try (monadInv TR). (* Etempvar *) @@ -1543,7 +1543,7 @@ Lemma transl_exprlist_correct: (TR: transl_exprlist cenv a = OK ta), exists tv, eval_exprlist tge (Vptr sp Int.zero) te tm ta tv - /\ val_list_inject f v tv. + /\ Val.inject_list f v tv. Proof. induction 3; intros; monadInv TR. exists (@nil val); split. constructor. constructor. @@ -1610,7 +1610,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv nil cs) (ISCC: Csharpminor.is_call_cont k) - (ARGSINJ: val_list_inject f args targs), + (ARGSINJ: Val.inject_list f args targs), match_states (Csharpminor.Callstate fd args k m) (Callstate tfd targs tk tm) | match_returnstate: @@ -1618,7 +1618,7 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (MINJ: Mem.inject f m tm) (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) (MK: match_cont k tk cenv nil cs) - (RESINJ: val_inject f v tv), + (RESINJ: Val.inject f v tv), match_states (Csharpminor.Returnstate v k m) (Returnstate tv tk tm). @@ -1626,7 +1626,7 @@ Remark val_inject_function_pointer: forall bound v fd f tv, Genv.find_funct ge v = Some fd -> match_globalenvs f bound -> - val_inject f v tv -> + Val.inject f v tv -> tv = v. Proof. intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 2a5d17bc..6284660c 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -1054,13 +1054,13 @@ Hypothesis valid_different_pointers_inj: b1' <> b2' \/ Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). -Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. +Remark val_inject_vtrue: forall f, Val.inject f Vtrue Vtrue. Proof. unfold Vtrue; auto. Qed. -Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. +Remark val_inject_vfalse: forall f, Val.inject f Vfalse Vfalse. Proof. unfold Vfalse; auto. Qed. -Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Remark val_inject_of_bool: forall f b, Val.inject f (Val.of_bool b) (Val.of_bool b). Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. Qed. @@ -1075,8 +1075,8 @@ Ltac TrivialInject := Lemma sem_cast_inject: forall v1 ty1 ty v tv1, sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv. Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. @@ -1093,8 +1093,8 @@ Qed. Lemma sem_unary_operation_inj: forall op v1 ty v tv1, sem_unary_operation op v1 ty m = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) @@ -1118,15 +1118,15 @@ Definition optval_self_injects (ov: option val) : Prop := Remark sem_binarith_inject: forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> + Val.inject f v1 v1' -> Val.inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. - assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). + assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v). { intros. subst ov; simpl in H7. destruct v0; contradiction || constructor. } @@ -1144,8 +1144,8 @@ Qed. Remark sem_shift_inject: forall sem_int sem_long v1 t1 v2 t2 v v1' v2', sem_shift sem_int sem_long v1 t1 v2 t2 = Some v -> - val_inject f v1 v1' -> val_inject f v2 v2' -> - exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'. + Val.inject f v1 v1' -> Val.inject f v2 v2' -> + exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. Proof. intros. exists v. unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate. @@ -1158,9 +1158,9 @@ Qed. Remark sem_cmp_inj: forall cmp v1 tv1 ty1 v2 tv2 ty2 v, sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> + Val.inject f v2 tv2 -> + exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). @@ -1168,21 +1168,21 @@ Proof. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject; eauto. + symmetry. eapply Val.cmpu_bool_inject; eauto. - (* pointer - long *) destruct v2; try discriminate. inv H1. set (v2 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v2 := v2); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v2 := v2); eauto. constructor. - (* long - pointer *) destruct v1; try discriminate. inv H0. set (v1 := Vint (Int.repr (Int64.unsigned i))) in *. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b). simpl. TrivialInject. - symmetry. eapply val_cmpu_bool_inject with (v1 := v1); eauto. constructor. + symmetry. eapply Val.cmpu_bool_inject with (v1 := v1); eauto. constructor. - (* numerical - numerical *) assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). { @@ -1194,8 +1194,8 @@ Qed. Lemma sem_binary_operation_inj: forall cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) @@ -1269,7 +1269,7 @@ Qed. Lemma bool_val_inj: forall v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. @@ -1283,9 +1283,9 @@ End GENERIC_INJECTION. Lemma sem_unary_operation_inject: forall f m m' op v1 ty1 v tv1, sem_unary_operation op v1 ty1 m = Some v -> - val_inject f v1 tv1 -> + Val.inject f v1 tv1 -> Mem.inject f m m' -> - exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_unary_operation_inj; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. @@ -1294,9 +1294,9 @@ Qed. Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> + Val.inject f v1 tv1 -> Val.inject f v2 tv2 -> Mem.inject f m m' -> - exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv. Proof. intros. eapply sem_binary_operation_inj; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. @@ -1308,7 +1308,7 @@ Qed. Lemma bool_val_inject: forall f m m' v ty b tv, bool_val v ty m = Some b -> - val_inject f v tv -> + Val.inject f v tv -> Mem.inject f m m' -> bool_val tv ty m' = Some b. Proof. 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..cde9ad11 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -157,31 +157,111 @@ 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_combine (cc1 cc2: calling_convention) : res calling_convention := + if bool_eq cc1.(cc_vararg) cc2.(cc_vararg) then + OK {| cc_vararg := cc1.(cc_vararg); + cc_unproto := cc1.(cc_unproto) && cc2.(cc_unproto); + cc_structret := cc1.(cc_structret) |} + else + Error (msg "incompatible calling conventions"). + +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 <- + (if cc1.(cc_unproto) then OK args2 else + if cc2.(cc_unproto) then OK args1 else + typelist_combine args1 args2); + do cc <- callconv_combine cc1 cc2; + OK (Tfunction args res cc) + | 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 _ _) => + | (Tint _ _ _ | Tlong _ _ | Tfloat _ _), + (Tint _ _ _ | Tlong _ _ | 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 +683,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 +902,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,30 +979,48 @@ 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. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. + destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. - split; apply typeconv_cast; unfold wt_cast. 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 +1140,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 +1321,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/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index e0fcb210..790877bd 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -358,8 +358,8 @@ Lemma sem_cast_match: forall v1 ty1 ty2 v2 v1' v2', sem_cast v1 ty1 ty2 = Some v2 -> do_cast v1' ty1 ty2 = OK v2' -> - val_inject inj v1' v1 -> - val_inject inj v2' v2. + Val.inject inj v1' v1 -> + Val.inject inj v2' v2. Proof. intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. exploit sem_cast_inject. eexact E. eauto. @@ -369,7 +369,7 @@ Qed. Lemma bool_val_match: forall v ty b v' m, bool_val v ty Mem.empty = Some b -> - val_inject inj v v' -> + Val.inject inj v v' -> bool_val v' ty m = Some b. Proof. intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. @@ -382,13 +382,13 @@ Lemma constval_rvalue: eval_simple_rvalue empty_env m a v -> forall v', constval ge a = OK v' -> - val_inject inj v' v + Val.inject inj v' v with constval_lvalue: forall m a b ofs, eval_simple_lvalue empty_env m a b ofs -> forall v', constval ge a = OK v' -> - val_inject inj v' (Vptr b ofs). + Val.inject inj v' (Vptr b ofs). Proof. (* rvalue *) induction 1; intros vres CV; simpl in CV; try (monadInv CV). @@ -479,7 +479,7 @@ Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> constval ge r = OK v -> - m' = m /\ ty = typeof r /\ val_inject inj v v'. + m' = m /\ ty = typeof r /\ Val.inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 39de282b..d890c820 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -123,7 +123,7 @@ let rec name_cdecl id ty = if not first then Buffer.add_string b ", "; Buffer.add_string b (name_cdecl "" t1); add_args false tl in - add_args true args; + if not cconv.cc_unproto then add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res | Tstruct(name, a) -> @@ -299,9 +299,9 @@ and extended_asm p txt res args clob = begin match clob with | [] -> () | c1 :: cl -> - fprintf p "@ : @[<hov 0>%S" (extern_atom c1); + fprintf p "@ : @[<hov 0>%S" (camlstring_of_coqstring c1); List.iter - (fun c -> fprintf p ",@ %S" (extern_atom c)) + (fun c -> fprintf p ",@ %S" (camlstring_of_coqstring c)) cl; fprintf p "@]" end; diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 3364ec6a..2a50f985 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -107,7 +107,7 @@ Inductive match_var (f: meminj) (cenv: compilenv) (e: env) (m: mem) (te: env) (t (MODE: access_mode ty = By_value chunk) (LOAD: Mem.load chunk m b 0 = Some v) (TLENV: tle!(id) = Some tv) - (VINJ: val_inject f v tv), + (VINJ: Val.inject f v tv), match_var f cenv e m te tle id | match_var_not_lifted: forall b ty b' (ENV: e!id = Some(b, ty)) @@ -130,7 +130,7 @@ Record match_envs (f: meminj) (cenv: compilenv) me_temps: forall id v, le!id = Some v -> - (exists tv, tle!id = Some tv /\ val_inject f v tv) + (exists tv, tle!id = Some tv /\ Val.inject f v tv) /\ (VSet.mem id cenv = true -> v = Vundef); me_inj: forall id1 b1 ty1 id2 b2 ty2, e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2; @@ -327,7 +327,7 @@ Qed. Lemma val_casted_inject: forall f v v' ty, - val_inject f v v' -> val_casted v ty -> val_casted v' ty. + Val.inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. intros. inv H; auto. inv H0; constructor. @@ -383,7 +383,7 @@ Lemma match_envs_assign_lifted: match_envs f cenv e le m lo hi te tle tlo thi -> e!id = Some(b, ty) -> val_casted v ty -> - val_inject f v tv -> + Val.inject f v tv -> assign_loc ge ty m b Int.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. @@ -415,7 +415,7 @@ Qed. Lemma match_envs_set_temp: forall f cenv e le m lo hi te tle tlo thi id v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_temp cenv id = OK x -> match_envs f cenv e (PTree.set id v le) m lo hi te (PTree.set id tv tle) tlo thi. Proof. @@ -436,7 +436,7 @@ Qed. Lemma match_envs_set_opttemp: forall f cenv e le m lo hi te tle tlo thi optid v tv x, match_envs f cenv e le m lo hi te tle tlo thi -> - val_inject f v tv -> + Val.inject f v tv -> check_opttemp cenv optid = OK x -> match_envs f cenv e (set_opttemp optid v le) m lo hi te (set_opttemp optid tv tle) tlo thi. Proof. @@ -993,8 +993,8 @@ Qed. Lemma assign_loc_inject: forall f ty m loc ofs v m' tm loc' ofs' v', assign_loc ge ty m loc ofs v m' -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - val_inject f v v' -> + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + Val.inject f v v' -> Mem.inject f m tm -> exists tm', assign_loc tge ty tm loc' ofs' v' tm' @@ -1095,7 +1095,7 @@ Theorem store_params_correct: forall s tm tle1 tle2 targs, list_norepet (var_names params) -> list_forall2 val_casted args (map snd params) -> - val_list_inject j args targs -> + Val.inject_list j args targs -> match_envs j cenv e le m lo hi te tle1 tlo thi -> Mem.inject j m tm -> (forall id, ~In id (var_names params) -> tle2!id = tle1!id) -> @@ -1388,8 +1388,8 @@ Qed. Lemma deref_loc_inject: forall ty loc ofs v loc' ofs', deref_loc ty m loc ofs v -> - val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> - exists tv, deref_loc ty tm loc' ofs' tv /\ val_inject f v tv. + Val.inject f (Vptr loc ofs) (Vptr loc' ofs') -> + exists tv, deref_loc ty tm loc' ofs' tv /\ Val.inject f v tv. Proof. intros. inv H. (* by value *) @@ -1405,14 +1405,14 @@ Lemma eval_simpl_expr: forall a v, eval_expr ge e le m a v -> compat_cenv (addr_taken_expr a) cenv -> - exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ val_inject f v tv + exists tv, eval_expr tge te tle tm (simpl_expr cenv a) tv /\ Val.inject f v tv with eval_simpl_lvalue: forall a b ofs, eval_lvalue ge e le m a b ofs -> compat_cenv (addr_taken_expr a) cenv -> match a with Evar id ty => VSet.mem id cenv = false | _ => True end -> - exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ val_inject f (Vptr b ofs) (Vptr b' ofs'). + exists b', exists ofs', eval_lvalue tge te tle tm (simpl_expr cenv a) b' ofs' /\ Val.inject f (Vptr b ofs) (Vptr b' ofs'). Proof. destruct 1; simpl; intros. @@ -1512,7 +1512,7 @@ Lemma eval_simpl_exprlist: val_casted_list vl tyl /\ exists tvl, eval_exprlist tge te tle tm (simpl_exprlist cenv al) tyl tvl - /\ val_list_inject f vl tvl. + /\ Val.inject_list f vl tvl. Proof. induction 1; simpl; intros. split. constructor. econstructor; split. constructor. auto. @@ -1729,7 +1729,7 @@ Lemma match_cont_find_funct: forall f cenv k tk m bound tbound vf fd tvf, match_cont f cenv k tk m bound tbound -> Genv.find_funct ge vf = Some fd -> - val_inject f vf tvf -> + Val.inject f vf tvf -> exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd. Proof. intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG. @@ -1761,7 +1761,7 @@ Inductive match_states: state -> state -> Prop := (TRFD: transf_fundef fd = OK tfd) (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (AINJ: val_list_inject j vargs tvargs) + (AINJ: Val.inject_list j vargs tvargs) (FUNTY: type_of_fundef fd = Tfunction targs tres cconv) (ANORM: val_casted_list vargs targs), match_states (Callstate fd vargs k m) @@ -1770,7 +1770,7 @@ Inductive match_states: state -> state -> Prop := forall v k m tv tk tm j (MCONT: forall cenv, match_cont j cenv k tk m (Mem.nextblock m) (Mem.nextblock tm)) (MINJ: Mem.inject j m tm) - (RINJ: val_inject j v tv), + (RINJ: Val.inject j v tv), match_states (Returnstate v k m) (Returnstate tv tk tm). @@ -2171,7 +2171,7 @@ Proof. eauto. eapply list_norepet_append_left; eauto. apply val_casted_list_params. unfold type_of_function in FUNTY. congruence. - apply val_list_inject_incr with j'; eauto. + apply val_inject_list_incr with j'; eauto. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. |