diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2Clight.ml | 164 | ||||
-rw-r--r-- | cfrontend/Csem.v | 12 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 4 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof1.v | 15 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof3.v | 15 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 6 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 18 |
7 files changed, 131 insertions, 103 deletions
diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 2f61d53c..035840b1 100644 --- a/cfrontend/C2Clight.ml +++ b/cfrontend/C2Clight.ml @@ -3,6 +3,7 @@ open Printf open Cparser open Cparser.C open Cparser.Env +open Cparser.Builtins open Camlcoq open AST @@ -37,6 +38,72 @@ let warning msg = eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg +(** ** The builtin environment *) + +let builtins_generic = { + typedefs = [ + (* keeps GCC-specific headers happy, harmless for others *) + "__builtin_va_list", C.TPtr(C.TVoid [], []) + ]; + functions = [ + (* Floating-point absolute value *) + "__builtin_fabs", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* The volatile read/volatile write functions *) + "__builtin_volatile_read_int8unsigned", + (TInt(IUChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int8signed", + (TInt(ISChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16unsigned", + (TInt(IUShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16signed", + (TInt(IShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int32", + (TInt(IInt, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float32", + (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float64", + (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_pointer", + (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_write_int8unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); + "__builtin_volatile_write_int8signed", + (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); + "__builtin_volatile_write_int16unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); + "__builtin_volatile_write_int16signed", + (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); + "__builtin_volatile_write_int32", + (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); + "__builtin_volatile_write_float32", + (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); + "__builtin_volatile_write_float64", + (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); + "__builtin_volatile_write_pointer", + (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); + (* Block copy *) + "__builtin_memcpy", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false); + "__builtin_memcpy_words", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false) + ] +} + +(* Add processor-dependent builtins *) + +let builtins = + { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.functions @ CBuiltins.builtins.functions } + (** ** Functions used to handle string literals *) let stringNum = ref 0 (* number of next global for string literals *) @@ -104,7 +171,10 @@ let declare_stub_function stub_name stub_type = match stub_type with | Tfunction(targs, tres) -> Datatypes.Coq_pair(intern_string stub_name, - External(intern_string stub_name, targs, tres)) + External({ ef_id = intern_string stub_name; + ef_sig = signature_of_type targs tres; + ef_inline = false }, + targs, tres)) | _ -> assert false let declare_stub_functions k = @@ -370,6 +440,8 @@ let volatile_write_fun ty = let convertTopExpr env e = match e.edesc with | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) -> + convertFuncall env (Some (convertExpr env lhs)) fn args +(**** (* Recognize __builtin_fabs and turn it into Clight operator *) begin match fn, args with | {edesc = C.EVar {name = "__builtin_fabs"}}, [arg1] -> @@ -378,6 +450,7 @@ let convertTopExpr env e = | _ -> convertFuncall env (Some (convertExpr env lhs)) fn args end +*****) | C.EBinop(C.Oassign, lhs, rhs, _) -> if Cutil.is_composite_type env lhs.etyp then unsupported "assignment between structs or between unions"; @@ -535,13 +608,23 @@ let convertFundef env fd = (** External function declaration *) +let noninlined_builtin_functions = [ + "__builtin_memcpy"; + "__builtin_memcpy_words" +] + let convertFundecl env (sto, id, ty, optinit) = - match convertTyp env ty with - | Tfunction(args, res) -> - let id' = intern_string id.name in - Datatypes.Coq_pair(id', External(id', args, res)) - | _ -> - assert false + let (args, res) = + match convertTyp env ty with + | Tfunction(args, res) -> (args, res) + | _ -> assert false in + let id' = intern_string id.name in + let ef = + { ef_id = id'; + ef_sig = signature_of_type args res; + ef_inline = List.mem_assoc id.name builtins.functions + && not (List.mem id.name noninlined_builtin_functions) } in + Datatypes.Coq_pair(id', External(ef, args, res)) (** Initializers *) @@ -816,70 +899,3 @@ let atom_alignof a = with Not_found -> None -(** ** The builtin environment *) - -open Cparser.Builtins - -let builtins_generic = { - typedefs = [ - (* keeps GCC-specific headers happy, harmless for others *) - "__builtin_va_list", C.TPtr(C.TVoid [], []) - ]; - functions = [ - (* Floating-point absolute value *) - "__builtin_fabs", - (TFloat(FDouble, []), [TFloat(FDouble, [])], false); - (* The volatile read/volatile write functions *) - "__builtin_volatile_read_int8unsigned", - (TInt(IUChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int8signed", - (TInt(ISChar, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16unsigned", - (TInt(IUShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int16signed", - (TInt(IShort, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_int32", - (TInt(IInt, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float32", - (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_float64", - (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_read_pointer", - (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); - "__builtin_volatile_write_int8unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); - "__builtin_volatile_write_int8signed", - (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); - "__builtin_volatile_write_int16unsigned", - (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); - "__builtin_volatile_write_int16signed", - (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); - "__builtin_volatile_write_int32", - (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); - "__builtin_volatile_write_float32", - (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); - "__builtin_volatile_write_float64", - (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); - "__builtin_volatile_write_pointer", - (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); - (* Block copy *) - "__builtin_memcpy", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false); - "__builtin_memcpy_words", - (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, [])], - false) - ] -} - -(* Add processor-dependent builtins *) - -let builtins = - { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.functions @ CBuiltins.builtins.functions } diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 42884091..212c2add 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -900,9 +900,9 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) - | step_external_function: forall id targs tres vargs k m vres t m', - external_call (external_function id targs tres) ge vargs m t vres m' -> - step (Callstate (External id targs tres) vargs k m) + | step_external_function: forall ef targs tres vargs k m vres t m', + external_call ef ge vargs m t vres m' -> + step (Callstate (External ef targs tres) vargs k m) t (Returnstate vres k m') | step_returnstate_0: forall v f e k m, @@ -1105,9 +1105,9 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := outcome_result_value out f.(fn_return) vres -> Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres - | eval_funcall_external: forall m id targs tres vargs t vres m', - external_call (external_function id targs tres) ge vargs m t vres m' -> - eval_funcall m (External id targs tres) vargs t m' vres. + | eval_funcall_external: forall m ef targs tres vargs t vres m', + external_call ef ge vargs m t vres m' -> + eval_funcall m (External ef targs tres) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cc81d0f4..56bef553 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -620,8 +620,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with | Csyntax.Internal g => do tg <- transl_function g; OK(AST.Internal tg) - | Csyntax.External id args res => - OK(AST.External (external_function id args res)) + | Csyntax.External ef args res => + OK(AST.External ef) end. (** ** Translation of programs *) diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index ebc188e8..73a38246 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -55,27 +55,30 @@ Proof. Qed. Lemma transl_fundef_sig1: - forall f tf args res, + forall tenv f tf args res, + wt_fundef tenv f -> transl_fundef f = OK tf -> classify_fun (type_of_fundef f) = fun_case_f args res -> funsig tf = signature_of_type args res. Proof. - intros. destruct f; monadInv H. + intros. inv H; monadInv H0. monadInv EQ. simpl. - simpl in H0. inversion H0. + simpl in H1. inversion H1. unfold fn_sig; simpl. unfold signature_of_type. f_equal. apply transl_params_types; auto. - simpl. simpl in H0. congruence. + simpl. simpl in H1. inv H1. destruct (ef_sig ef); simpl in *. + unfold signature_of_type. congruence. Qed. Lemma transl_fundef_sig2: - forall f tf args res, + forall tenv f tf args res, + wt_fundef tenv f -> transl_fundef f = OK tf -> type_of_fundef f = Tfunction args res -> funsig tf = signature_of_type args res. Proof. intros. eapply transl_fundef_sig1; eauto. - rewrite H0; reflexivity. + rewrite H1; reflexivity. Qed. Lemma var_kind_by_value: diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index fb1edbe3..0e9e5b13 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1249,7 +1249,8 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply transl_fundef_sig1; eauto. congruence. + eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto. + congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl. auto. @@ -1263,7 +1264,8 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply transl_fundef_sig1; eauto. congruence. + eapply transl_fundef_sig1; eauto. eapply functions_well_typed; eauto. + congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl; auto. @@ -1595,10 +1597,15 @@ Proof. eapply Genv.find_funct_ptr_symbol_inversion; eauto. destruct H as [targs D]. assert (targs = Tnil). - inv H0. inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. + inv H0. + (* internal function *) + inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. simpl in D. congruence. + (* external function *) simpl in D. inv D. - exploit external_call_arity; eauto. destruct targs; simpl; congruence. + exploit external_call_arity; eauto. intro ARITY. + exploit function_ptr_well_typed; eauto. intro WT. inv WT. + rewrite H5 in ARITY. destruct targs; simpl in ARITY; congruence. subst targs. assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). eapply transl_fundef_sig2; eauto. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c82aa9ea..9d0791e7 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -210,7 +210,7 @@ Record function : Type := mkfunction { Inductive fundef : Type := | Internal: function -> fundef - | External: ident -> typelist -> type -> fundef. + | External: external_function -> typelist -> type -> fundef. (** ** Programs *) @@ -639,7 +639,3 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := Definition signature_of_type (args: typelist) (res: type) : signature := mksignature (typlist_of_typelist args) (opttyp_of_type res). - -Definition external_function - (id: ident) (targs: typelist) (tres: type) : AST.external_function := - mkextfun id (signature_of_type targs tres). diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b147fbda..8e089f16 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -155,8 +155,10 @@ Inductive wt_fundef: typenv -> fundef -> Prop := | wt_fundef_Internal: forall env f, wt_function env f -> wt_fundef env (Internal f) - | wt_fundef_External: forall env id args res, - wt_fundef env (External id args res). + | wt_fundef_External: forall env ef args res, + (ef_sig ef).(sig_args) = typlist_of_typelist args -> + (ef_sig ef).(sig_res) = opttyp_of_type res -> + wt_fundef env (External ef args res). Definition add_global_var (env: typenv) (id_v: ident * globvar type) : typenv := @@ -410,8 +412,12 @@ Qed. Definition typecheck_fundef (main: ident) (env: typenv) (id_fd: ident * fundef) : bool := let (id, fd) := id_fd in match fd with - | Internal f => typecheck_function env f - | External _ _ _ => true + | Internal f => + typecheck_function env f + | External ef targs tres => + let s := ef_sig ef in + list_eq_dec typ_eq s.(sig_args) (typlist_of_typelist targs) + && opt_typ_eq s.(sig_res) (opttyp_of_type tres) end && if ident_eq id main then match type_of_fundef fd with @@ -430,8 +436,8 @@ Proof. intros. unfold typecheck_fundef in H; TrueInv. split. destruct fd. - constructor. apply typecheck_function_correct; auto. - constructor. + constructor. apply typecheck_function_correct; auto. + TrueInv. constructor; eapply proj_sumbool_true; eauto. intro. destruct (ident_eq id main). destruct (type_of_fundef fd); try discriminate. exists t; decEq; auto. apply eq_type_correct; auto. |