diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 159 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 9 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 1 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 13 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 6 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 38 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 3 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 1 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 |
9 files changed, 201 insertions, 31 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 7c6a4994..3dc40a1e 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -47,16 +47,29 @@ let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 let atom_is_static a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_static + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_static | C.Storage_thread_local_static -> true + | _ -> false with Not_found -> false let atom_is_extern a = try - (Hashtbl.find decl_atom a).a_storage = C.Storage_extern + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_extern| C.Storage_thread_local_extern -> true + | _ -> false with Not_found -> false +let atom_is_thread_local a = + try + match (Hashtbl.find decl_atom a).a_storage with + | C.Storage_thread_local_extern| C.Storage_thread_local_static + | C.Storage_thread_local -> true + | _ -> false + with Not_found -> + false + let atom_alignof a = try (Hashtbl.find decl_atom a).a_alignment @@ -165,13 +178,14 @@ let ais_annot_functions = true);] else [] - + let builtins_generic = { builtin_typedefs = []; builtin_functions = - ais_annot_functions - @ + ais_annot_functions @ [ + "__builtin_expect", + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); (* Integer arithmetic *) "__builtin_bswap64", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); @@ -257,7 +271,92 @@ let builtins_generic = { "__builtin_unreachable", (TVoid [], [], false); "__builtin_expect", - (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false) + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); + (* Helper functions for int64 arithmetic *) + "__compcert_i64_dtos", + (TInt(ILongLong, []), + [TFloat(FDouble, [])], + false); + "__compcert_i64_dtou", + (TInt(IULongLong, []), + [TFloat(FDouble, [])], + false); + "__compcert_i64_stod", + (TFloat(FDouble, []), + [TInt(ILongLong, [])], + false); + "__compcert_i64_utod", + (TFloat(FDouble, []), + [TInt(IULongLong, [])], + false); + "__compcert_i64_stof", + (TFloat(FFloat, []), + [TInt(ILongLong, [])], + false); + "__compcert_i64_utof", + (TFloat(FFloat, []), + [TInt(IULongLong, [])], + false); + "__compcert_i64_sdiv", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__compcert_i64_udiv", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__compcert_i64_smod", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__compcert_i64_umod", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__compcert_i64_shl", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false); + "__compcert_i64_shr", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IInt, [])], + false); + "__compcert_i64_sar", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(IInt, [])], + false); + "__compcert_i64_smulh", + (TInt(ILongLong, []), + [TInt(ILongLong, []); TInt(ILongLong, [])], + false); + "__compcert_i64_umulh", + (TInt(IULongLong, []), + [TInt(IULongLong, []); TInt(IULongLong, [])], + false); + "__compcert_i32_sdiv", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_udiv", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); + "__compcert_i32_smod", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_umod", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); + "__compcert_f32_div", + (TFloat(FFloat,[]), + [TFloat(FFloat,[]); TFloat(FFloat,[])], + false); + "__compcert_f64_div", + (TFloat(FDouble,[]), + [TFloat(FDouble,[]); TFloat(FDouble,[])], + false); ] } @@ -857,6 +956,14 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, args) -> + (match args with + | [e1; e2] -> + ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2)) + | _ -> + error "__builtin_expect wants two arguments"; + ezero) + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> error "too few arguments to function call, expected at least 2, have 0"; ezero @@ -949,8 +1056,8 @@ let rec convertExpr env e = ewrap (Ctyping.eselection (convertExpr env arg1) (convertExpr env arg2) (convertExpr env arg3)) - | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) -> - convertExpr env arg1 + (*| C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) -> + convertExpr env arg1*) | C.ECall({edesc = C.EVar {name = "printf"}}, args) when !Clflags.option_interp -> @@ -1198,7 +1305,8 @@ let convertFundef loc env fd = let vars = List.map (fun (sto, id, ty, init) -> - if sto = Storage_extern || sto = Storage_static then + if sto = Storage_extern || sto = Storage_thread_local_extern + || sto = Storage_static || sto = Storage_thread_local_static then unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; @@ -1236,6 +1344,13 @@ let convertFundef loc env fd = let re_builtin = Str.regexp "__builtin_" +(* BEGIN CHECK *) +let re_runtime64 = Str.regexp "__compcert_i64" +let re_runtime32 = Str.regexp "__compcert_i32" +let re_runtimef32 = Str.regexp "__compcert_f32" +let re_runtimef64 = Str.regexp "__compcert_f64" +(* END CHECK *) + let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = match convertTyp env ty with @@ -1246,7 +1361,15 @@ let convertFundecl env (sto, id, ty, optinit) = let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then AST.EF_malloc else - if id.name = "free" then AST.EF_free else + if id.name = "free" then AST.EF_free else + (* BEGIN CHECK *) + if Str.string_match re_runtime64 id.name 0 + || Str.string_match re_runtime32 id.name 0 + || Str.string_match re_runtimef64 id.name 0 + || Str.string_match re_runtimef32 id.name 0 + then AST.EF_runtime(id'', sg) + else + (* END CHECK *) if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) @@ -1292,7 +1415,8 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [AST.Init_space sz] + if sto = C.Storage_extern || sto = C.Storage_thread_local_extern + then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let initialized = @@ -1301,11 +1425,16 @@ let convertGlobvar loc env (sto, id, ty, optinit) = then Sections.Init_reloc else Sections.Init in let (section, access) = - Sections.for_variable env loc id' ty initialized in + Sections.for_variable env loc id' ty initialized + (match sto with + | Storage_thread_local | Storage_thread_local_extern + | Storage_thread_local_static -> true + | _ -> false) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); - if sto <> C.Storage_extern && Cutil.incomplete_type env ty then + if sto <> C.Storage_extern && sto <> C.Storage_thread_local_extern + && Cutil.incomplete_type env ty then error "'%s' has incomplete type" id.name; Hashtbl.add decl_atom id' { a_storage = sto; @@ -1479,7 +1608,7 @@ let cleanupGlobals p = if IdentSet.mem fd.fd_name !strong then error "multiple definitions of %s" fd.fd_name.name; strong := IdentSet.add fd.fd_name !strong - | C.Gdecl(Storage_extern, id, ty, init) -> + | C.Gdecl((Storage_extern|Storage_thread_local_extern), id, ty, init) -> extern := IdentSet.add id !extern | C.Gdecl(sto, id, ty, Some i) -> if IdentSet.mem id !strong then @@ -1498,7 +1627,7 @@ let cleanupGlobals p = match g.gdesc with | C.Gdecl(sto, id, ty, init) -> let better_def_exists = - if sto = Storage_extern then + if sto = Storage_extern || sto = Storage_thread_local_extern then IdentSet.mem id !strong || IdentSet.mem id !weak else if init = None then IdentSet.mem id !strong diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 52037ac0..cc3058a9 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -556,6 +556,10 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := Some(w, E0, Vundef, m). +Definition do_ef_profiling (id : profiling_id) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + Some(w, E0, Vundef, m). + Definition do_builtin_or_external (name: string) (sg: signature) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match lookup_builtin_function name sg with @@ -578,6 +582,7 @@ Definition do_external (ef: external_function): | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs + | EF_profiling id kind => do_ef_profiling id end. Lemma do_ef_external_sound: @@ -645,6 +650,8 @@ Proof with try congruence. eapply do_inline_assembly_sound; eauto. - (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. +- (* EF_profiling *) + unfold do_ef_profiling. mydestr. split; constructor. Qed. Lemma do_ef_external_complete: @@ -699,6 +706,8 @@ Proof. eapply do_inline_assembly_complete; eauto. - (* EF_debug *) inv H. inv H0. reflexivity. +- (* EF_profiling *) + inv H. inv H0. reflexivity. Qed. (** * Reduction of expressions *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ed45ac23..4afb9285 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1334,6 +1334,7 @@ Lemma eval_binop_compat: /\ Val.inject f v tv. Proof. destruct op; simpl; intros; inv H. +- TrivialExists. apply Val.normalize_inject; auto. - TrivialExists. apply Val.add_inject; auto. - TrivialExists. apply Val.sub_inject; auto. - TrivialExists. inv H0; inv H1; constructor. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 0d7bcc3a..2f8b5e7c 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -34,6 +34,7 @@ Inductive unary_operation : Type := | Oabsfloat : unary_operation. (**r floating-point absolute value *) Inductive binary_operation : Type := + | Oexpect : binary_operation (**r return first argument *) | Oadd : binary_operation (**r addition (binary [+]) *) | Osub : binary_operation (**r subtraction (binary [-]) *) | Omul : binary_operation (**r multiplication (binary [*]) *) @@ -764,6 +765,14 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val : (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) v1 t1 v2 t2 m. +Definition sem_expect (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint n1)) + (fun sg n1 n2 => Some(Vlong n1)) + (fun n1 n2 => Some(Vfloat n1)) + (fun n1 n2 => Some(Vsingle n1)) + v1 t1 v2 t2 m. + Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => @@ -1051,6 +1060,7 @@ Definition sem_binary_operation (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with + | Oexpect => sem_expect v1 t1 v2 t2 m | Oadd => sem_add cenv v1 t1 v2 t2 m | Osub => sem_sub cenv v1 t1 v2 t2 m | Omul => sem_mul v1 t1 v2 t2 m @@ -1345,6 +1355,9 @@ Lemma sem_binary_operation_inj: 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. +- (* expect *) + unfold sem_expect in *. + eapply sem_binarith_inject; eauto; intros; exact I. - (* add *) assert (A: forall cenv ty si v1' v2' tv1' tv2', Val.inject f v1' tv1' -> Val.inject f v2' tv2' -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 9e804176..173b8c8c 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -259,6 +259,11 @@ Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) := let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))). +Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) := + make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint) + (Oexpect AST.Tfloat) (Oexpect AST.Tsingle) + (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2. + Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2 @@ -463,6 +468,7 @@ Definition transl_binop (ce: composite_env) (a: expr) (ta: type) (b: expr) (tb: type) : res expr := match op with + | Cop.Oexpect => make_expect a ta b tb | Cop.Oadd => make_add ce a ta b tb | Cop.Osub => make_sub ce a ta b tb | Cop.Omul => make_mul a ta b tb diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 98293888..d8653544 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -607,6 +607,11 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. +Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect. +Proof. + apply make_binarith_correct; intros; auto. +Qed. + Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. assert (A: forall ty si a b c e le m va vb v, @@ -910,22 +915,23 @@ Lemma transl_binop_correct: eval_expr ge e le m c v. Proof. intros. destruct op; simpl in *. - eapply make_add_correct; eauto. - eapply make_sub_correct; eauto. - eapply make_mul_correct; eauto. - eapply make_div_correct; eauto. - eapply make_mod_correct; eauto. - eapply make_and_correct; eauto. - eapply make_or_correct; eauto. - eapply make_xor_correct; eauto. - eapply make_shl_correct; eauto. - eapply make_shr_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. - eapply make_cmp_correct; eauto. +- eapply make_expect_correct; eauto. +- eapply make_add_correct; eauto. +- eapply make_sub_correct; eauto. +- eapply make_mul_correct; eauto. +- eapply make_div_correct; eauto. +- eapply make_mod_correct; eauto. +- eapply make_and_correct; eauto. +- eapply make_or_correct; eauto. +- eapply make_xor_correct; eauto. +- eapply make_shl_correct; eauto. +- eapply make_shr_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. +- eapply make_cmp_correct; eauto. Qed. Remark int_ltu_true: diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 97ed1ed3..834b1931 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -112,6 +112,7 @@ Definition comparison_type (ty1 ty2: type) (m: string): res type := Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := match op with + | Oexpect => binarith_type ty1 ty2 "__builtin_expect" | Oadd => match classify_add ty1 ty2 with | add_case_pi ty _ | add_case_ip _ ty @@ -1548,6 +1549,8 @@ Lemma pres_sem_binop: Proof. intros until m; intros TY SEM WT1 WT2. destruct op; simpl in TY; simpl in SEM. +- (* expect *) + unfold sem_expect in SEM. eapply pres_sem_binarith; eauto; intros; exact I. - (* add *) unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty. eapply pres_sem_binarith; eauto; intros; exact I. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index a9ecb342..7ca64741 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -63,6 +63,7 @@ let precedence = function | Ebinop(Oand, _, _, _) -> (8, LtoR) | Ebinop(Oxor, _, _, _) -> (7, LtoR) | Ebinop(Oor, _, _, _) -> (6, LtoR) + | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* Expressions *) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 16cdfc41..5fa9ea17 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -31,6 +31,7 @@ let name_unop = function | Oabsfloat -> "__builtin_fabs" let name_binop = function + | Oexpect -> "expect" | Oadd -> "+" | Osub -> "-" | Omul -> "*" @@ -159,6 +160,7 @@ let rec precedence = function | Ebinop(Oand, _, _, _) -> (8, LtoR) | Ebinop(Oxor, _, _, _) -> (7, LtoR) | Ebinop(Oor, _, _, _) -> (6, LtoR) + | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* fixme *) | Eseqand _ -> (5, LtoR) | Eseqor _ -> (4, LtoR) | Econdition _ -> (3, RtoL) |