diff options
-rw-r--r-- | cfrontend/C2C.ml | 18 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 47 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 266 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 3 | ||||
-rw-r--r-- | cparser/Bitfields.ml | 2 | ||||
-rw-r--r-- | cparser/Cutil.ml | 16 | ||||
-rw-r--r-- | cparser/Cutil.mli | 2 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 2 | ||||
-rw-r--r-- | cparser/StructReturn.ml | 2 | ||||
-rw-r--r-- | cparser/Unblock.ml | 2 | ||||
-rw-r--r-- | debug/DebugInformation.ml | 14 | ||||
-rw-r--r-- | debug/DebugTypes.mli | 2 | ||||
-rw-r--r-- | debug/DwarfTypes.mli | 2 | ||||
-rw-r--r-- | debug/Dwarfgen.ml | 12 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 5 |
16 files changed, 251 insertions, 146 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a2db0915..8c7ec6d8 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -983,7 +983,12 @@ let rec convertStmt env s = Scontinue | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in - if init.sdesc <> C.Sskip then + let rec init_debug s = + match s.sdesc with + | Sseq (a,b) -> init_debug a && init_debug b + | C.Sskip -> true + | _ -> Cutil.is_debug_stmt s in + if init.sdesc <> C.Sskip && not (init_debug init) then begin warning "ignored code at beginning of 'switch'"; contains_case init @@ -1103,16 +1108,16 @@ let rec convertInit env init = | C.Init_single e -> Init_single (convertExpr env e) | C.Init_array il -> - Init_array (convertInitList env il) + Init_array (convertInitList env (List.rev il) Init_nil) | C.Init_struct(_, flds) -> - Init_struct (convertInitList env (List.map snd flds)) + Init_struct (convertInitList env (List.rev_map snd flds) Init_nil) | C.Init_union(_, fld, i) -> Init_union (intern_string fld.fld_name, convertInit env i) -and convertInitList env il = +and convertInitList env il accu = match il with - | [] -> Init_nil - | i :: il' -> Init_cons(convertInit env i, convertInitList env il') + | [] -> accu + | i :: il' -> convertInitList env il' (Init_cons(convertInit env i, accu)) let convertInitializer env ty i = match Initializers.transl_init @@ -1313,4 +1318,3 @@ let convertProgram p = if Cerrors.check_errors () then None else Some p' with Env.Error msg -> error (Env.error_message msg); None - diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 7af4792a..b1a39c64 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -172,22 +172,26 @@ Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res ini end. (** Translate an initializer [i] for a variable of type [ty]. - Return the corresponding list of initialization data. *) + [transl_init ce ty i] returns the appropriate list of initialization data. + The intermediate functions [transl_init_rec], [transl_init_array] + and [transl_init_struct] append initialization data to the given + list [k], and build the list of initialization data in reverse order, + so as to remain tail-recursive. *) -Definition padding (frm to: Z) : list init_data := - if zlt frm to then Init_space (to - frm) :: nil else nil. +Definition padding (frm to: Z) (k: list init_data) : list init_data := + if zlt frm to then Init_space (to - frm) :: k else k. -Fixpoint transl_init (ce: composite_env) (ty: type) (i: initializer) - {struct i} : res (list init_data) := +Fixpoint transl_init_rec (ce: composite_env) (ty: type) (i: initializer) + (k: list init_data) {struct i} : res (list init_data) := match i, ty with | Init_single a, _ => - do d <- transl_init_single ce ty a; OK (d :: nil) + do d <- transl_init_single ce ty a; OK (d :: k) | Init_array il, Tarray tyelt nelt _ => - transl_init_array ce tyelt il (Zmax 0 nelt) + transl_init_array ce tyelt il (Zmax 0 nelt) k | Init_struct il, Tstruct id _ => do co <- lookup_composite ce id; match co_su co with - | Struct => transl_init_struct ce ty (co_members co) il 0 + | Struct => transl_init_struct ce ty (co_members co) il 0 k | Union => Error (MSG "struct/union mismatch on " :: CTX id :: nil) end | Init_union f i1, Tunion id _ => @@ -196,39 +200,40 @@ Fixpoint transl_init (ce: composite_env) (ty: type) (i: initializer) | Struct => Error (MSG "union/struct mismatch on " :: CTX id :: nil) | Union => do ty1 <- field_type f (co_members co); - do d <- transl_init ce ty1 i1; - OK (d ++ padding (sizeof ce ty1) (sizeof ce ty)) + do k1 <- transl_init_rec ce ty1 i1 k; + OK (padding (sizeof ce ty1) (sizeof ce ty) k1) end | _, _ => Error (msg "wrong type for compound initializer") end with transl_init_array (ce: composite_env) (ty: type) (il: initializer_list) (sz: Z) - {struct il} : res (list init_data) := + (k: list init_data) {struct il} : res (list init_data) := match il with | Init_nil => - if zeq sz 0 then OK nil - else if zle 0 sz then OK (Init_space (sz * sizeof ce ty) :: nil) + if zeq sz 0 then OK k + else if zle 0 sz then OK (Init_space (sz * sizeof ce ty) :: k) else Error (msg "wrong number of elements in array initializer") | Init_cons i1 il' => - do d1 <- transl_init ce ty i1; - do d2 <- transl_init_array ce ty il' (sz - 1); - OK (d1 ++ d2) + do k1 <- transl_init_rec ce ty i1 k; + transl_init_array ce ty il' (sz - 1) k1 end with transl_init_struct (ce: composite_env) (ty: type) (fl: members) (il: initializer_list) (pos: Z) + (k: list init_data) {struct il} : res (list init_data) := match il, fl with | Init_nil, nil => - OK (padding pos (sizeof ce ty)) + OK (padding pos (sizeof ce ty) k) | Init_cons i1 il', (_, ty1) :: fl' => let pos1 := align pos (alignof ce ty1) in - do d1 <- transl_init ce ty1 i1; - do d2 <- transl_init_struct ce ty fl' il' (pos1 + sizeof ce ty1); - OK (padding pos pos1 ++ d1 ++ d2) + do k1 <- transl_init_rec ce ty1 i1 (padding pos pos1 k); + transl_init_struct ce ty fl' il' (pos1 + sizeof ce ty1) k1 | _, _ => Error (msg "wrong number of elements in struct initializer") end. - +Definition transl_init (ce: composite_env) (ty: type) (i: initializer) + : res (list init_data) := + do k <- transl_init_rec ce ty i nil; OK (List.rev' k). diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 3a7b5593..9c662f5e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -485,6 +485,118 @@ Proof. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. Qed. +(** * Relational specification of the translation of initializers *) + +Definition tr_padding (frm to: Z) : list init_data := + if zlt frm to then Init_space (to - frm) :: nil else nil. + +Inductive tr_init: type -> initializer -> list init_data -> Prop := + | tr_init_sgl: forall ty a d, + transl_init_single ge ty a = OK d -> + tr_init ty (Init_single a) (d :: nil) + | tr_init_arr: forall tyelt nelt attr il d, + tr_init_array tyelt il (Zmax 0 nelt) d -> + tr_init (Tarray tyelt nelt attr) (Init_array il) d + | tr_init_str: forall id attr il co d, + lookup_composite ge id = OK co -> co_su co = Struct -> + tr_init_struct (Tstruct id attr) (co_members co) il 0 d -> + tr_init (Tstruct id attr) (Init_struct il) d + | tr_init_uni: forall id attr f i1 co ty1 d, + lookup_composite ge id = OK co -> co_su co = Union -> field_type f (co_members co) = OK ty1 -> + tr_init ty1 i1 d -> + tr_init (Tunion id attr) (Init_union f i1) + (d ++ tr_padding (sizeof ge ty1) (sizeof ge (Tunion id attr))) + +with tr_init_array: type -> initializer_list -> Z -> list init_data -> Prop := + | tr_init_array_nil_0: forall ty, + tr_init_array ty Init_nil 0 nil + | tr_init_array_nil_pos: forall ty sz, + 0 < sz -> + tr_init_array ty Init_nil sz (Init_space (sz * sizeof ge ty) :: nil) + | tr_init_array_cons: forall ty i il sz d1 d2, + tr_init ty i d1 -> tr_init_array ty il (sz - 1) d2 -> + tr_init_array ty (Init_cons i il) sz (d1 ++ d2) + +with tr_init_struct: type -> members -> initializer_list -> Z -> list init_data -> Prop := + | tr_init_struct_nil: forall ty pos, + tr_init_struct ty nil Init_nil pos (tr_padding pos (sizeof ge ty)) + | tr_init_struct_cons: forall ty f1 ty1 fl i1 il pos d1 d2, + let pos1 := align pos (alignof ge ty1) in + tr_init ty1 i1 d1 -> + tr_init_struct ty fl il (pos1 + sizeof ge ty1) d2 -> + tr_init_struct ty ((f1, ty1) :: fl) (Init_cons i1 il) + pos (tr_padding pos pos1 ++ d1 ++ d2). + +Lemma transl_padding_spec: + forall frm to k, padding frm to k = rev (tr_padding frm to) ++ k. +Proof. + unfold padding, tr_padding; intros. + destruct (zlt frm to); auto. +Qed. + +Lemma transl_init_rec_spec: + forall i ty k res, + transl_init_rec ge ty i k = OK res -> + exists d, tr_init ty i d /\ res = rev d ++ k + +with transl_init_array_spec: + forall il ty sz k res, + transl_init_array ge ty il sz k = OK res -> + exists d, tr_init_array ty il sz d /\ res = rev d ++ k + +with transl_init_struct_spec: + forall il ty fl pos k res, + transl_init_struct ge ty fl il pos k = OK res -> + exists d, tr_init_struct ty fl il pos d /\ res = rev d ++ k. + +Proof. +Local Opaque sizeof. +- destruct i; intros until res; intros TR; simpl in TR. ++ monadInv TR. exists (x :: nil); split; auto. constructor; auto. ++ destruct ty; try discriminate. + destruct (transl_init_array_spec _ _ _ _ _ TR) as (d & A & B). + exists d; split; auto. constructor; auto. ++ destruct ty; try discriminate. monadInv TR. destruct (co_su x) eqn:SU; try discriminate. + destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d & A & B). + exists d; split; auto. econstructor; eauto. ++ destruct ty; try discriminate. + monadInv TR. destruct (co_su x) eqn:SU; monadInv EQ0. + destruct (transl_init_rec_spec _ _ _ _ EQ0) as (d & A & B). + exists (d ++ tr_padding (sizeof ge x0) (sizeof ge (Tunion i0 a))); split. + econstructor; eauto. + rewrite rev_app_distr, app_ass, B. apply transl_padding_spec. + +- destruct il; intros until res; intros TR; simpl in TR. ++ destruct (zeq sz 0). + inv TR. exists (@nil init_data); split; auto. constructor. + destruct (zle 0 sz). + inv TR. econstructor; split. constructor. omega. auto. + discriminate. ++ monadInv TR. + destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). + destruct (transl_init_array_spec _ _ _ _ _ EQ0) as (d2 & A2 & B2). + exists (d1 ++ d2); split. econstructor; eauto. + subst res x. rewrite rev_app_distr, app_ass. auto. + +- destruct il; intros until res; intros TR; simpl in TR. ++ destruct fl; inv TR. econstructor; split. constructor. apply transl_padding_spec. ++ destruct fl as [ | [f1 ty1] fl ]; monadInv TR. + destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). + destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d2 & A2 & B2). + exists (tr_padding pos (align pos (alignof ge ty1)) ++ d1 ++ d2); split. + econstructor; eauto. + rewrite ! rev_app_distr. subst res x. rewrite ! app_ass. rewrite transl_padding_spec. auto. +Qed. + +Theorem transl_init_spec: + forall ty i d, transl_init ge ty i = OK d -> tr_init ty i d. +Proof. + unfold transl_init; intros. monadInv H. + exploit transl_init_rec_spec; eauto. intros (d & A & B). + subst x. unfold rev'; rewrite <- rev_alt. + rewrite rev_app_distr; simpl. rewrite rev_involutive. auto. +Qed. + (** * Soundness of the translation of initializers *) (** Soundness for single initializers. *) @@ -555,9 +667,9 @@ Qed. Notation idlsize := Genv.init_data_list_size. Remark padding_size: - forall frm to, frm <= to -> idlsize (padding frm to) = to - frm. + forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. Proof. - unfold padding; intros. destruct (zlt frm to). + unfold tr_padding; intros. destruct (zlt frm to). simpl. xomega. simpl. omega. Qed. @@ -582,80 +694,55 @@ Qed. Hypothesis ce_consistent: composite_env_consistent ge. -Lemma transl_init_size: +Lemma tr_init_size: forall i ty data, - transl_init ge ty i = OK data -> + tr_init ty i data -> idlsize data = sizeof ge ty - -with transl_init_list_size: - forall il, - (forall ty sz data, - transl_init_array ge ty il sz = OK data -> - idlsize data = sizeof ge ty * sz) - /\ - (forall ty fl pos data, - transl_init_struct ge ty fl il pos = OK data -> - sizeof_struct ge pos fl <= sizeof ge ty -> - idlsize data + pos = sizeof ge ty). - +with tr_init_array_size: + forall ty il sz data, + tr_init_array ty il sz data -> + idlsize data = sizeof ge ty * sz +with tr_init_struct_size: + forall ty fl il pos data, + tr_init_struct ty fl il pos data -> + sizeof_struct ge pos fl <= sizeof ge ty -> + idlsize data + pos = sizeof ge ty. Proof. -- induction i; intros. -+ (* single *) - monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. -+ (* array *) - simpl in H. destruct ty; try discriminate. - simpl. eapply (proj1 (transl_init_list_size il)); eauto. -+ (* struct *) - simpl in H. destruct ty; try discriminate. - monadInv H. destruct (co_su x) eqn:?; try discriminate. - replace (idlsize data) with (idlsize data + 0) by omega. - eapply (proj2 (transl_init_list_size il)). eauto. - unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i) as [co|] eqn:?; inv EQ. +- destruct 1; simpl. ++ erewrite transl_init_single_size by eauto. omega. ++ Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. ++ replace (idlsize d) with (idlsize d + 0) by omega. + eapply tr_init_struct_size; eauto. simpl. + unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). - unfold sizeof_composite. rewrite Heqs. apply align_le. - destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. -+ (* union *) - simpl in H. destruct ty; try discriminate. - monadInv H. destruct (co_su x) eqn:?; try discriminate. - monadInv EQ0. - rewrite idlsize_app. rewrite (IHi _ _ EQ0). - unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i0) as [co|] eqn:?; inv EQ. - rewrite padding_size. omega. - apply Zle_trans with (sizeof_union ge (co_members x)). + unfold sizeof_composite. rewrite H0. apply align_le. + destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. ++ rewrite idlsize_app, padding_size. + exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. + simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. + apply Zle_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). - unfold sizeof_composite. rewrite Heqs. apply align_le. - destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - -- induction il. -+ (* base cases *) - simpl. intuition auto. -* (* arrays *) - destruct (zeq sz 0). inv H. simpl; ring. - destruct (zle 0 sz); inv H. simpl. - rewrite Z.mul_comm. + unfold sizeof_composite. rewrite H0. apply align_le. + destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + +- destruct 1; simpl. ++ omega. ++ rewrite Z.mul_comm. assert (0 <= sizeof ge ty * sz). { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } - zify; omega. -* (* structs *) - destruct fl; inv H. - simpl in H0. rewrite padding_size by omega. omega. -+ (* inductive cases *) - destruct IHil as [A B]. split. -* (* arrays *) - intros. monadInv H. - rewrite idlsize_app. - rewrite (transl_init_size _ _ _ EQ). - rewrite (A _ _ _ EQ1). + xomega. ++ rewrite idlsize_app. + erewrite tr_init_size by eauto. + erewrite tr_init_array_size by eauto. ring. -* (* structs *) - intros. simpl in H. destruct fl as [|[i1 t1]]; monadInv H. - rewrite ! idlsize_app. - simpl in H0. - rewrite padding_size. - rewrite (transl_init_size _ _ _ EQ). - rewrite <- (B _ _ _ _ EQ1). omega. - auto. apply align_le. apply alignof_pos. + +- destruct 1; simpl; intros. ++ rewrite padding_size by auto. omega. ++ rewrite ! idlsize_app, padding_size. + erewrite tr_init_size by eauto. + rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega. + unfold pos1. apply align_le. apply alignof_pos. Qed. (** A semantics for general initializers *) @@ -733,62 +820,57 @@ Qed. Remark store_init_data_list_padding: forall frm to b ofs m, - Genv.store_init_data_list ge m b ofs (padding frm to) = Some m. + Genv.store_init_data_list ge m b ofs (tr_padding frm to) = Some m. Proof. - intros. unfold padding. destruct (zlt frm to); auto. + intros. unfold tr_padding. destruct (zlt frm to); auto. Qed. -Lemma transl_init_sound_gen: +Lemma tr_init_sound: (forall m b ofs ty i m', exec_init m b ofs ty i m' -> - forall data, transl_init ge ty i = OK data -> + forall data, tr_init ty i data -> Genv.store_init_data_list ge m b ofs data = Some m') /\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> - forall data, transl_init_array ge ty il sz = OK data -> + forall data, tr_init_array ty il sz data -> Genv.store_init_data_list ge m b ofs data = Some m') /\(forall m b ofs l il m', exec_init_list m b ofs l il m' -> forall ty fl data pos, l = fields_of_struct fl pos -> - transl_init_struct ge ty fl il pos = OK data -> + tr_init_struct ty fl il pos data -> Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). Proof. Local Opaque sizeof. apply exec_init_scheme; simpl; intros. - (* single *) - monadInv H3. simpl. erewrite transl_init_single_steps by eauto. auto. + inv H3. simpl. erewrite transl_init_single_steps by eauto. auto. - (* array *) - replace (Z.max 0 sz) with sz in H1. eauto. + inv H1. replace (Z.max 0 sz) with sz in H7. eauto. assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. - (* struct *) - unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. + inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. replace ofs with (ofs + 0) by omega. eauto. - (* union *) - unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. - monadInv H4. assert (x = ty) by congruence. subst x. + inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. - (* array, empty *) - destruct (zeq sz 0). - inv H0. auto. - rewrite zle_true in H0 by omega. inv H0. auto. + inv H0; auto. - (* array, nonempty *) - monadInv H3. + inv H3. eapply store_init_data_list_app. eauto. - rewrite (transl_init_size _ _ _ EQ). eauto. + rewrite (tr_init_size _ _ _ H7). eauto. + - (* struct, empty *) - destruct fl as [|[i t]]; simpl in H0; inv H0. - apply store_init_data_list_padding. + inv H0. apply store_init_data_list_padding. - (* struct, nonempty *) - destruct fl as [|[i t]]; simpl in H4; monadInv H4. - simpl in H3; inv H3. + inv H4. simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (align pos0 (alignof ge t) - pos0)) - with (ofs + align pos0 (alignof ge t)) by omega. + replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega. eapply store_init_data_list_app. eauto. - rewrite (transl_init_size _ _ _ EQ). + rewrite (tr_init_size _ _ _ H9). rewrite <- Zplus_assoc. eapply H2. eauto. eauto. apply align_le. apply alignof_pos. Qed. @@ -804,7 +886,7 @@ Proof. intros. set (ge := globalenv p) in *. change (prog_comp_env p) with (genv_cenv ge) in H0. - destruct (transl_init_sound_gen ge) as (A & B & C). + destruct (tr_init_sound ge) as (A & B & C). eapply build_composite_env_consistent. apply prog_comp_env_eq. - eapply A; eauto. + eapply A; eauto. apply transl_init_spec; auto. Qed. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 4f2a8d0c..bb6576aa 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -266,6 +266,9 @@ let rec expr p (prec, e) = fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob + | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> + fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]" + (P.to_int kind) (extern_atom txt) exprlist (false,args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) | Eparen(a1, tycast, ty) -> diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 223ee3ca..bbc39456 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -502,7 +502,7 @@ and transf_post env ctx op e1 bf tyfield = and transf_init env i = match i with | Init_single e -> Init_single (transf_exp env Val e) - | Init_array il -> Init_array (List.map (transf_init env) il) + | Init_array il -> Init_array (List.rev (List.rev_map (transf_init env) il)) | Init_struct(id, fld_init_list) -> let fld_init_list' = List.map (fun (f, i) -> (f, transf_init env i)) fld_init_list in diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index a86c779f..1b0bf65d 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -880,6 +880,18 @@ let is_literal_0 e = | EConst(CInt(0L, _, _)) -> true | _ -> false +(* Check that a C statement is a debug annotation *) + +let is_debug_stmt s = + let is_debug_call = function + | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug" + | _ -> false in + match s.sdesc with + | Sdo {edesc = e;_} -> + is_debug_call e + | _ -> false + + (* Assignment compatibility check over attributes. Standard attributes ("const", "volatile", "restrict") can safely be added (to the rhs type to get the lhs type) but must not be dropped. @@ -1099,7 +1111,3 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } - - - - diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 8b6c609b..b353cba3 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -187,6 +187,8 @@ val type_of_member : Env.t -> field -> typ (* Return the type of accessing the given field [fld]. Normally it's [fld.fld_type] but there is a special case for small unsigned bitfields. *) +val is_debug_stmt : stmt -> bool + (* Is the given statement a call to debug builtin? *) val is_literal_0 : exp -> bool (* Is the given expression the integer literal "0"? *) val is_lvalue : exp -> bool diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index c163989e..6ea5d121 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -360,7 +360,7 @@ let transf_init loc env i = match unroll env ty with | TArray(ty_elt, _, _) -> Some ty_elt | _ -> assert false in - Init_array (List.map (trinit swap_elt) il) + Init_array (List.rev (List.rev_map (trinit swap_elt) il)) | Init_struct(id, fld_init_list) -> let trinit_field (f, i) = let swap_f = diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 4b387b0d..664f6a28 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -142,7 +142,7 @@ and exp_desc env = function and init env = function | Init_single e -> Init_single(exp env e) - | Init_array il -> Init_array (List.map (init env) il) + | Init_array il -> Init_array (List.rev (List.rev_map (init env) il)) | Init_struct(id, il) -> Init_struct(ident env id, List.map (fun (f, i) -> (field env f, init env i)) il) diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 2c6fd1d2..82c0a04c 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -412,7 +412,7 @@ and transf_init env = function | Init_single e -> Init_single (transf_expr env Val e) | Init_array il -> - Init_array (List.map (transf_init env) il) + Init_array (List.rev (List.rev_map (transf_init env) il)) | Init_struct(id, fil) -> Init_struct (id, List.map (fun (fld, i) -> (fld, transf_init env i)) fil) | Init_union(id, fld, i) -> diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 405cf755..ef8bc91c 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -169,7 +169,7 @@ and expand_init islocal env i = | Init_single e -> Init_single (expand_expr islocal env e) | Init_array il -> - Init_array (List.map expand il) + Init_array (List.rev (List.rev_map expand il)) | Init_struct(id, flds) -> Init_struct(id, List.map (fun (f, i) -> (f, expand i)) flds) | Init_union(id, fld, i) -> diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 51fbfde9..ed00ea0d 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -65,7 +65,7 @@ let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] (* Find the type id to an type *) let find_type (ty: typ) = - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in Hashtbl.find lookup_types (typ_to_string ty) @@ -77,7 +77,7 @@ let insert_type (ty: typ) = Hashtbl.add types id d_ty; Hashtbl.add lookup_types name id; id in - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in let rec typ_aux ty = try find_type ty with @@ -255,14 +255,14 @@ let replace_fun id f = (* All local variables *) let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 -(* Mapping from stampt to the debug id of the local variable *) +(* Mapping from stamp to the debug id of the local variable *) let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function id to debug id *) +(* Map from function id + scope id to debug id *) let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function atom to debug id *) -let atom_to_scope: (atom * int, int) Hashtbl.t = Hashtbl.create 7 +(* Map from function atom + scope id atom to debug id *) +let atom_to_scope: (atom * int,int) Hashtbl.t = Hashtbl.create 7 let find_lvar_stamp id = let id = (Hashtbl.find stamp_to_local id) in @@ -299,7 +299,7 @@ let remove_unused id = Hashtbl.remove stamp_to_definition id.stamp with Not_found -> () -let insert_global_declaration env dec= +let insert_global_declaration env dec = add_file (fst dec.gloc); let insert d_dec stamp = let id = next_id () in diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index b2f19f7a..e885fc59 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -147,7 +147,7 @@ type local_variable_information = { lvar_atom: atom option; lvar_file_loc:location; lvar_type: int; - lvar_static: bool; (* Static variable are mapped to symbols *) + lvar_static: bool; (* Static variables are mapped to symbols *) } type scope_information = diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index a4c75201..2af64c0b 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -297,7 +297,7 @@ type debug_entries = | Gnu of gnu_entries (* The target specific functions for printing the debug information *) -module type DWARF_TARGET= +module type DWARF_TARGET = sig val label: out_channel -> int -> unit val section: out_channel -> section_name -> unit diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index d198a92f..7addaba3 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -182,11 +182,11 @@ module Dwarfgenaux (Target: TARGET) = enumeration_name = string_entry e.enum_name; } in let enum = new_entry id (DW_TAG_enumeration_type enum) in - let child = List.map enumerator_to_entry e.enum_enumerators in - add_children enum child + let children = List.map enumerator_to_entry e.enum_enumerators in + add_children enum children let fun_type_to_entry id f = - let children = if f.fun_prototyped then + let children = if not f.fun_prototyped then let u = { unspecified_parameter_artificial = None; } in @@ -195,7 +195,7 @@ module Dwarfgenaux (Target: TARGET) = List.map (fun p -> let fp = { formal_parameter_artificial = None; - formal_parameter_name = name_opt p.param_name; + formal_parameter_name = None; formal_parameter_type = p.param_type; formal_parameter_variable_parameter = None; formal_parameter_location = None; @@ -384,7 +384,9 @@ module Dwarfgenaux (Target: TARGET) = with Not_found -> None,[] let function_parameter_to_entry f_id acc p = - let loc,loc_list = location_entry f_id (get_opt_val p.parameter_atom) in + let loc,loc_list = match p.parameter_atom with + | None -> None,[] + | Some p -> location_entry f_id p in let p = { formal_parameter_artificial = None; formal_parameter_name = name_opt p.parameter_name; diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 80fce39e..02d2dc84 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -93,7 +93,7 @@ let p_freg oc = function let p_preg oc = function | IR ir -> p_ireg oc ir | FR fr -> p_freg oc fr - | _ -> assert false (* This registers should not be used. *) + | _ -> assert false (* This register should not be used. *) let p_atom oc a = p_jstring oc (extern_atom a) @@ -127,7 +127,6 @@ let p_crbit oc c = | CRbit_6 -> 6 in fprintf oc "{\"CRbit\":%d}" number - let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l) let p_list elem oc l = @@ -269,7 +268,7 @@ let p_instruction oc ic = | Plwarx (ir1,ir2,ir3) -> instruction "Plwarx" [Ireg ir1; Ireg ir2; Ireg ir3] | Plwbrx (ir1,ir2,ir3) -> instruction "Plwbrx" [Ireg ir1; Ireg ir2; Ireg ir3] | Pmbar c -> instruction "Pmbar" [Constant (Cint c)] - | Pmfcr ir -> fprintf oc "{%a,\"Args\":[%a]}" inst_name "Pmfcr" p_ireg ir + | Pmfcr ir -> instruction "Pmfcr" [Ireg ir] | Pmfcrbit (ir,crb) -> () (* Should not occur *) | Pmflr ir -> instruction "Pmflr" [Ireg ir] | Pmr (ir1,ir2) -> instruction "Pmr" [Ireg ir1; Ireg ir2] |