From 6431b483760b6b039f97a1749a055a3c181084b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 10 Nov 2021 10:02:07 +0100 Subject: Resurrect a warning for bit fields of enum types Earlier CompCert versions would warn if a bit field of width N and type enum E was too small for the values of the enumeration: whether the field is interpreted as a N-bit signed integer or a N-bit unsigned integer, some values of the enumeration are not representable. This warning was performed in the Bitfields emulation pass, which went away during the reimplementation of bit fields within the verified part of CompCert. In this commit, we resurrect the warning and perform it during the Elab pass. In passing, some of the code that elaborates bit fields was moved to a separate function "check_bitfield". --- cparser/Elab.ml | 48 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 15 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index c2c7f943..60d71b3a 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -629,6 +629,36 @@ let get_nontype_attrs env ty = let nta = List.filter to_be_removed (attributes_of_type_no_expand ty) in (remove_attributes_type env nta ty, nta) +(* Auxiliary for elaborating bitfield declarations. *) + +let check_bitfield loc env id ty ik n = + let max = Int64.of_int(sizeof_ikind ik * 8) in + if n < 0L then begin + error loc "bit-field '%a' has negative width (%Ld)" pp_field id n; + None + end else if n > max then begin + error loc "size of bit-field '%a' (%Ld bits) exceeds its type (%Ld bits)" pp_field id n max; + None + end else if n = 0L && id <> "" then begin + error loc "named bit-field '%a' has zero width" pp_field id; + None + end else begin + begin match unroll env ty with + | TEnum(eid, _) -> + let info = wrap Env.find_enum loc env eid in + let w = Int64.to_int n in + let representable sg = + List.for_all (fun (_, v, _) -> Cutil.int_representable v w sg) + info.Env.ei_members in + if not (representable false || representable true) then + warning loc Unnamed + "not all values of type 'enum %s' can be represented in bit-field '%a' (%d bits are not enough)" + eid.C.name pp_field id w + | _ -> () + end; + Some (Int64.to_int n) + end + (* Elaboration of a type specifier. Returns 6-tuple: (storage class, "inline" flag, "noreturn" flag, "typedef" flag, elaborated type, new env) @@ -1011,23 +1041,11 @@ and elab_field_group env = function error loc "alignment specified for bit-field '%a'" pp_field id; None, env end else begin - let expr,env' =(!elab_expr_f loc env sz) in + let expr,env' = !elab_expr_f loc env sz in match Ceval.integer_expr env' expr with | Some n -> - if n < 0L then begin - error loc "bit-field '%a' has negative width (%Ld)" pp_field id n; - None,env - end else - let max = Int64.of_int(sizeof_ikind ik * 8) in - if n > max then begin - error loc "size of bit-field '%a' (%Ld bits) exceeds its type (%Ld bits)" pp_field id n max; - None,env - end else - if n = 0L && id <> "" then begin - error loc "named bit-field '%a' has zero width" pp_field id; - None,env - end else - Some(Int64.to_int n),env' + let bf = check_bitfield loc env' id ty ik n in + bf,env' | None -> error loc "bit-field '%a' width not an integer constant" pp_field id; None,env -- cgit From 168495d726e623e0b4bd6364f949ae577fa8b52e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 9 Nov 2021 15:57:45 +0100 Subject: Revised checks for multi-character constants 'xyz' The previous code for elaborating character constants has a small bug: the value of a wide character constant consisting of several characters was normalized to type `int`, while, statically, it has type `wchar_t`. If `wchar_t` is `unsigned short`, for example, the constant `L'ab'` would elaborate to 6357090, which is not of type `unsigned short`. This commit fixes the bug by normalizing wide character constants to type `wchar_t`, regardless of how many characters they contain. The previous code was odd in another respect: leading `\0` characters in multi-character constants were ignored. Hence, `'\0bcde'` was accepted while `'abcde'` caused a warning. This commit implements a more predictable behavior: the number of characters in a character literal is limited a priori to sizeof(type of result) / sizeof(type of each character) So, for non-wide character constants we can typically have up to 4 characters (sizeof(int) / sizeof(char)), while for wide character constants we can only have one character. In effect, multiple-character wide character literals are not supported. This is allowed by the ISO C99 standard and seems consistent with GCC and Clang. Finally, a multi-character constant with too many characters was reported either as an error (if the computation overflowed the 64-bit accumulator) or as a warning (otherwise). Here, we make this an error in all cases. GCC and Clang only produce warnings, and truncate the value of the character constant, but an error feels safer. --- cparser/Elab.ml | 43 +++++++++++++++++++------------------------ 1 file changed, 19 insertions(+), 24 deletions(-) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 60d71b3a..eff6f3ba 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -396,34 +396,29 @@ let elab_float_constant f = (v, ty) let elab_char_constant loc wide chars = + let len = List.length chars in let nbits = if wide then 8 * !config.sizeof_wchar else 8 in - (* Treat multi-char constants as a number in base 2^nbits *) let max_digit = Int64.shift_left 1L nbits in - let max_val = Int64.shift_left 1L (64 - nbits) in - let v,_ = - List.fold_left - (fun (acc,err) d -> - if not err then begin - let overflow = acc < 0L || acc >= max_val - and out_of_range = d < 0L || d >= max_digit in - if overflow then - error loc "character constant too long for its type"; - if out_of_range then + (* Treat multi-character constants as a number in base 2^nbits. + It must fit in type int for a normal constant and in type wchar_t + for a wide constant. *) + let v = + if len > (if wide then 1 else !config.sizeof_int) then begin + error loc "%d-character constant too long for its type" len; + 0L + end else + List.fold_left + (fun acc d -> + if d < 0L || d >= max_digit then error loc "escape sequence is out of range (code 0x%LX)" d; - Int64.add (Int64.shift_left acc nbits) d,overflow || out_of_range - end else - Int64.add (Int64.shift_left acc nbits) d,true - ) - (0L,false) chars in - if not (integer_representable v IInt) then - warning loc Unnamed "character constant too long for its type"; - (* C99 6.4.4.4 item 10: single character -> represent at type char - or wchar_t *) + Int64.add (Int64.shift_left acc nbits) d) + 0L chars in + (* C99 6.4.4.4 items 10 and 11: + single-character constant -> represent at type char + multi-character constant -> represent at type int + wide character constant -> represent at type wchar_t *) Ceval.normalize_int v - (if List.length chars = 1 then - if wide then wchar_ikind() else IChar - else - IInt) + (if wide then wchar_ikind() else if len = 1 then IChar else IInt) let elab_string_literal loc wide chars = let nbits = if wide then 8 * !config.sizeof_wchar else 8 in -- cgit From b9dfe18fb99d9fd0e8918c160ee297755c5fca59 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 16 Nov 2021 09:38:54 +0100 Subject: An improved PTree data structure (#420) This PR replaces the "PTree" data structure used in lib/Maps.v by the canonical binary tries data structure proposed by A. W. Appel and described in the paper "Efficient Extensional Binary Tries", https://arxiv.org/abs/2110.05063 The new implementation is more memory-efficient and a bit faster, resulting in reduced compilation times (-5% on typical C programs, up to -10% on very large C functions). It also enjoys the extensionality property (two tries mapping equal keys to equal data are equal), which simplifies some proofs. --- backend/CSEdomain.v | 2 +- backend/ValueDomain.v | 4 +- cfrontend/Cminorgenproof.v | 1 - cfrontend/SimplExprproof.v | 8 +- cfrontend/SimplLocalsproof.v | 1 - common/Globalenvs.v | 9 - common/Memory.v | 11 +- lib/Lattice.v | 314 ++++++----- lib/Maps.v | 1226 ++++++++++++++++++++++++++---------------- 9 files changed, 908 insertions(+), 668 deletions(-) diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v index e96c4cd4..8809094e 100644 --- a/backend/CSEdomain.v +++ b/backend/CSEdomain.v @@ -140,7 +140,7 @@ Proof. - split; simpl; intros. + contradiction. + rewrite PTree.gempty in H; discriminate. - + rewrite PMap.gi in H; contradiction. + + contradiction. - contradiction. - rewrite PTree.gempty in H; discriminate. Qed. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 01f080ff..9bb99eaa 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -3438,7 +3438,7 @@ Lemma ablock_init_sound: forall m b p, smatch m b p -> bmatch m b (ablock_init p). Proof. intros; split; auto; intros. - unfold ablock_load, ablock_init; simpl. rewrite ZTree.gempty. + unfold ablock_load, ablock_init; simpl. eapply vnormalize_cast; eauto. eapply H; eauto. Qed. @@ -4558,7 +4558,7 @@ Lemma ematch_init: ematch (init_regs vl rl) (einit_regs rl). Proof. induction rl; simpl; intros. -- red; intros. rewrite Regmap.gi. simpl AE.get. rewrite PTree.gempty. +- red; intros. rewrite Regmap.gi. simpl. constructor. - destruct vl as [ | v1 vs ]. + assert (ematch (init_regs nil rl) (einit_regs rl)). diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index bc1c92ca..ed45ac23 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -875,7 +875,6 @@ Proof. intros. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. instantiate (1 := f1). red; intros. eelim Mem.fresh_block_alloc; eauto. eapply Mem.valid_block_inject_2; eauto. - intros. apply PTree.gempty. eapply match_callstack_alloc_right; eauto. intros. destruct (In_dec peq id (map fst vars)). apply cenv_remove_gss; auto. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 507e2128..ea89a8ba 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -893,13 +893,9 @@ Qed. Lemma static_bool_val_sound: forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b. Proof. - assert (A: forall b ofs, Mem.weak_valid_pointer Mem.empty b ofs = false). - { unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool; intros. - rewrite ! pred_dec_false by (apply Mem.perm_empty). auto. } intros until b; unfold bool_val. - destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto. -- rewrite A; congruence. -- simpl; rewrite A; congruence. + destruct (classify_bool t); destruct v; destruct Archi.ptr64 eqn:SF; auto; + simpl; congruence. Qed. Lemma step_makeif: diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index c133d8ea..d2943f64 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -935,7 +935,6 @@ Proof. (* local var, lifted *) destruct R as [U V]. exploit H2; eauto. intros [chunk X]. eapply match_var_lifted with (v := Vundef) (tv := Vundef); eauto. - rewrite U; apply PTree.gempty. eapply alloc_variables_initial_value; eauto. red. unfold empty_env; intros. rewrite PTree.gempty in H4; congruence. apply create_undef_temps_charact with ty. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 4c9e7889..f424a69d 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -265,15 +265,6 @@ Qed. Program Definition empty_genv (pub: list ident): t := @mkgenv pub (PTree.empty _) (PTree.empty _) 1%positive _ _ _. -Next Obligation. - rewrite PTree.gempty in H. discriminate. -Qed. -Next Obligation. - rewrite PTree.gempty in H. discriminate. -Qed. -Next Obligation. - rewrite PTree.gempty in H. discriminate. -Qed. Definition globalenv (p: program F V) := add_globals (empty_genv p.(prog_public)) p.(prog_defs). diff --git a/common/Memory.v b/common/Memory.v index fa60455b..03a6572e 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -346,15 +346,6 @@ Program Definition empty: mem := mkmem (PMap.init (ZMap.init Undef)) (PMap.init (fun ofs k => None)) 1%positive _ _ _. -Next Obligation. - repeat rewrite PMap.gi. red; auto. -Qed. -Next Obligation. - rewrite PMap.gi. auto. -Qed. -Next Obligation. - rewrite PMap.gi. auto. -Qed. (** Allocation of a fresh block with the given bounds. Return an updated memory state and the address of the fresh block, which initially contains @@ -631,7 +622,7 @@ Proof. reflexivity. Qed. Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p. Proof. - intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto. + intros. unfold perm, empty; simpl. tauto. Qed. Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. diff --git a/lib/Lattice.v b/lib/Lattice.v index 6fed3f21..aea331a0 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Andrew W. Appel, Princeton University *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -140,7 +141,7 @@ Definition bot : t := PTree.empty _. Lemma get_bot: forall p, get p bot = L.bot. Proof. - unfold bot, get; intros; simpl. rewrite PTree.gempty. auto. + intros; reflexivity. Qed. Lemma ge_bot: forall x, ge x bot. @@ -148,13 +149,7 @@ Proof. unfold ge; intros. rewrite get_bot. apply L.ge_bot. Qed. -(** A [combine] operation over the type [PTree.t L.t] that attempts - to share its result with its arguments. *) - -Section COMBINE. - -Variable f: option L.t -> option L.t -> option L.t. -Hypothesis f_none_none: f None None = None. +(** Equivalence modulo L.eq *) Definition opt_eq (ox oy: option L.t) : Prop := match ox, oy with @@ -194,182 +189,181 @@ Proof. auto. Qed. -Definition tree_eq (m1 m2: PTree.t L.t) : Prop := - forall i, opt_eq (PTree.get i m1) (PTree.get i m2). - -Lemma tree_eq_refl: forall m, tree_eq m m. -Proof. intros; red; intros; apply opt_eq_refl. Qed. - -Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1. -Proof. intros; red; intros; apply opt_eq_sym; auto. Qed. +Local Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym : combine. -Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3. -Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed. - -Lemma tree_eq_node: - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2). -Proof. - intros; red; intros. destruct i; simpl; auto. -Qed. - -Lemma tree_eq_node': - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2). -Proof. - intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. -Qed. +(** A [combine] operation over the type [PTree.t L.t] that attempts + to share its result with its arguments. *) -Lemma tree_eq_node'': - forall l1 o1 r1 l2 o2 r2, - tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 -> - tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2). -Proof. - intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. -Qed. +Section COMBINE. -Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym - tree_eq_refl tree_eq_sym - tree_eq_node tree_eq_node' tree_eq_node'' : combine. +Variable f: option L.t -> option L.t -> option L.t. +Hypothesis f_none_none: f None None = None. -Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t). +Inductive changed : Type := + | Same + | Same1 + | Same2 + | Changed (m: PTree.t L.t). + +Let Node_combine_l (l1: PTree.t L.t) (lres: changed) (o1: option L.t) + (r1: PTree.t L.t) (rres: changed) : changed := + let o' := f o1 None in + match lres, rres with + | Same1, Same1 => + if opt_beq o' o1 then Same1 else Changed (PTree.Node l1 o' r1) + | Same1, Changed r' => Changed (PTree.Node l1 o' r') + | Changed l', Same1 => Changed (PTree.Node l' o' r1) + | Changed l', Changed r' => Changed (PTree.Node l' o' r') + | _, _ => Same (**r impossible cases *) + end. -Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed := - match m with - | PTree.Leaf => - Unchanged - | PTree.Node l o r => - let o' := f o None in - match combine_l l, combine_l r with - | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) - | Unchanged, Changed r' => Changed (PTree.Node' l o' r') - | Changed l', Unchanged => Changed (PTree.Node' l' o' r) - | Changed l', Changed r' => Changed (PTree.Node' l' o' r') - end +Let xcombine_l (m: PTree.t L.t) : changed := + PTree.tree_rec Same1 Node_combine_l m. + +Let Node_combine_r (l1: PTree.t L.t) (lres: changed) (o1: option L.t) + (r1: PTree.t L.t) (rres: changed) : changed := + let o' := f None o1 in + match lres, rres with + | Same2, Same2 => + if opt_beq o' o1 then Same2 else Changed (PTree.Node l1 o' r1) + | Same2, Changed r' => Changed (PTree.Node l1 o' r') + | Changed l', Same2 => Changed (PTree.Node l' o' r1) + | Changed l', Changed r' => Changed (PTree.Node l' o' r') + | _, _ => Same (**r impossible cases *) end. -Lemma combine_l_eq: - forall m, - tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end) - (PTree.xcombine_l f m). -Proof. - induction m; simpl. - auto with combine. - destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r']; - auto with combine. - case_eq (opt_beq (f o None) o); auto with combine. -Qed. - -Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed := - match m with - | PTree.Leaf => - Unchanged - | PTree.Node l o r => - let o' := f None o in - match combine_r l, combine_r r with - | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r) - | Unchanged, Changed r' => Changed (PTree.Node' l o' r') - | Changed l', Unchanged => Changed (PTree.Node' l' o' r) - | Changed l', Changed r' => Changed (PTree.Node' l' o' r') +Let xcombine_r (m: PTree.t L.t) : changed := + PTree.tree_rec Same2 Node_combine_r m. + +Let Node_combine_2 + (l1: PTree.t L.t) (o1: option L.t) (r1: PTree.t L.t) + (l2: PTree.t L.t) (o2: option L.t) (r2: PTree.t L.t) + (lres: changed) (rres: changed) : changed := + let o := f o1 o2 in + match lres, rres with + | Same, Same => + match opt_beq o o1, opt_beq o o2 with + | true, true => Same + | true, false => Same1 + | false, true => Same2 + | false, false => Changed (PTree.Node l1 o r1) end + | Same, Same1 + | Same1, Same + | Same1, Same1 => + if opt_beq o o1 then Same1 else Changed (PTree.Node l1 o r1) + | Same, Same2 + | Same2, Same + | Same2, Same2 => + if opt_beq o o2 then Same2 else Changed (PTree.Node l2 o r2) + | Same, Changed m2 => Changed (PTree.Node l1 o m2) + | Same1, Same2 => Changed (PTree.Node l1 o r2) + | Same1, Changed m2 => Changed (PTree.Node l1 o m2) + | Same2, Same1 => Changed (PTree.Node l2 o r1) + | Same2, Changed m2 => Changed (PTree.Node l2 o m2) + | Changed m1, (Same|Same1) => Changed (PTree.Node m1 o r1) + | Changed m1, Same2 => Changed (PTree.Node m1 o r2) + | Changed m1, Changed m2 => Changed (PTree.Node m1 o m2) end. -Lemma combine_r_eq: - forall m, - tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end) - (PTree.xcombine_r f m). +Definition xcombine := + PTree.tree_rec2 + Same + xcombine_r + xcombine_l + Node_combine_2. + +Definition tree_agree (m1 m2 m: PTree.t L.t) : Prop := + forall i, opt_eq m!i (f m1!i m2!i). + +Lemma tree_agree_node: forall l1 o1 r1 l2 o2 r2 l o r, + tree_agree l1 l2 l -> tree_agree r1 r2 r -> opt_eq (f o1 o2) o -> + tree_agree (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2) (PTree.Node l o r). Proof. - induction m; simpl. - auto with combine. - destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r']; - auto with combine. - case_eq (opt_beq (f None o) o); auto with combine. + intros; red; intros. rewrite ! PTree.gNode. destruct i; auto using opt_eq_sym. Qed. -Inductive changed2 : Type := - | Same - | Same1 - | Same2 - | CC(m: PTree.t L.t). - -Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 := - match m1, m2 with - | PTree.Leaf, PTree.Leaf => - Same - | PTree.Leaf, _ => - match combine_r m2 with - | Unchanged => Same2 - | Changed m => CC m - end - | _, PTree.Leaf => - match combine_l m1 with - | Unchanged => Same1 - | Changed m => CC m - end - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - let o := f o1 o2 in - match xcombine l1 l2, xcombine r1 r2 with - | Same, Same => - match opt_beq o o1, opt_beq o o2 with - | true, true => Same - | true, false => Same1 - | false, true => Same2 - | false, false => CC(PTree.Node' l1 o r1) - end - | Same1, Same | Same, Same1 | Same1, Same1 => - if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1) - | Same2, Same | Same, Same2 | Same2, Same2 => - if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2) - | Same1, Same2 => CC(PTree.Node' l1 o r2) - | (Same|Same1), CC r => CC(PTree.Node' l1 o r) - | Same2, Same1 => CC(PTree.Node' l2 o r1) - | Same2, CC r => CC(PTree.Node' l2 o r) - | CC l, (Same|Same1) => CC(PTree.Node' l o r1) - | CC l, Same2 => CC(PTree.Node' l o r2) - | CC l, CC r => CC(PTree.Node' l o r) - end - end. - -Lemma xcombine_eq: - forall m1 m2, - match xcombine m1 m2 with - | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2) - | Same1 => tree_eq m1 (PTree.combine f m1 m2) - | Same2 => tree_eq m2 (PTree.combine f m1 m2) - | CC m => tree_eq m (PTree.combine f m1 m2) +Local Hint Resolve tree_agree_node : combine. + +Lemma gxcombine_l: forall m, + match xcombine_l m with + | Same1 => forall i, opt_eq m!i (f m!i None) + | Changed m' => forall i, opt_eq m'!i (f m!i None) + | _ => False end. Proof. -Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r. - induction m1; destruct m2; simpl. - split; apply tree_eq_refl. - generalize (combine_r_eq (PTree.Node m2_1 o m2_2)). - destruct (combine_r (PTree.Node m2_1 o m2_2)); auto. - generalize (combine_l_eq (PTree.Node m1_1 o m1_2)). - destruct (combine_l (PTree.Node m1_1 o m1_2)); auto. - generalize (IHm1_1 m2_1) (IHm1_2 m2_2). - destruct (xcombine m1_1 m2_1); - destruct (xcombine m1_2 m2_2); auto with combine; - intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine. + unfold xcombine_l. induction m using PTree.tree_ind. +- simpl; intros. rewrite PTree.gempty, f_none_none. auto. +- rewrite PTree.unroll_tree_rec by auto. + destruct (PTree.tree_rec Same1 Node_combine_l l); + destruct (PTree.tree_rec Same1 Node_combine_l r); + try contradiction; + unfold Node_combine_l; + try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine). + destruct (opt_beq (f o None) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine. +Qed. + +Lemma gxcombine_r: forall m, + match xcombine_r m with + | Same2 => forall i, opt_eq m!i (f None m!i) + | Changed m' => forall i, opt_eq m'!i (f None m!i) + | _ => False + end. +Proof. + unfold xcombine_r. induction m using PTree.tree_ind. +- simpl; intros. rewrite PTree.gempty, f_none_none. auto. +- rewrite PTree.unroll_tree_rec by auto. + destruct (PTree.tree_rec Same2 Node_combine_r l); + destruct (PTree.tree_rec Same2 Node_combine_r r); + try contradiction; + unfold Node_combine_r; + try (intros i; rewrite ! PTree.gNode; destruct i; auto with combine). + destruct (opt_beq (f None o) o) eqn:BEQ; intros i; rewrite ! PTree.gNode; destruct i; auto with combine. +Qed. + +Inductive xcombine_spec (m1 m2: PTree.t L.t) : changed -> Prop := + | XCS_Same: + tree_agree m1 m2 m1 -> tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same + | XCS_Same1: + tree_agree m1 m2 m1 -> xcombine_spec m1 m2 Same1 + | XCS_Same2: + tree_agree m1 m2 m2 -> xcombine_spec m1 m2 Same2 + | XCS_Changed: forall m', + tree_agree m1 m2 m' -> xcombine_spec m1 m2 (Changed m'). + +Local Hint Constructors xcombine_spec : combine. + +Lemma gxcombine: forall m1 m2, xcombine_spec m1 m2 (xcombine m1 m2). +Proof. + Local Opaque opt_eq. + unfold xcombine. + induction m1 using PTree.tree_ind; induction m2 using PTree.tree_ind; intros. +- constructor; red; intros; rewrite ! PTree.gEmpty, f_none_none; auto with combine. +- rewrite PTree.unroll_tree_rec2_EN by auto. set (m2 := PTree.Node l o r). + generalize (gxcombine_r m2); destruct (xcombine_r m2); + try contradiction; constructor; auto. +- rewrite PTree.unroll_tree_rec2_NE by auto. set (m1 := PTree.Node l o r). + generalize (gxcombine_l m1); destruct (xcombine_l m1); + try contradiction; constructor; auto. +- rewrite PTree.unroll_tree_rec2_NN by auto. + clear IHm2 IHm3. specialize (IHm1 l0). specialize (IHm0 r0). + inv IHm1; inv IHm0; unfold Node_combine_2; auto with combine; + destruct (opt_beq (f o o0) o) eqn:E1; destruct (opt_beq (f o o0) o0) eqn:E2; + auto with combine. Qed. Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t := match xcombine m1 m2 with | Same|Same1 => m1 | Same2 => m2 - | CC m => m + | Changed m => m end. -Lemma gcombine: +Theorem gcombine: forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)). Proof. - intros. - assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)). - unfold combine. - generalize (xcombine_eq m1 m2). - destruct (xcombine m1 m2); tauto. - eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl. + intros. unfold combine. + generalize (gxcombine m1 m2); intros XS; inv XS; auto. Qed. End COMBINE. @@ -526,7 +520,7 @@ Definition top := Top_except (PTree.empty L.t). Lemma get_top: forall p, get p top = L.top. Proof. - unfold top; intros; simpl. rewrite PTree.gempty. auto. + unfold top; intros; auto. Qed. Lemma ge_top: forall x, ge top x. diff --git a/lib/Maps.v b/lib/Maps.v index 3f43d102..f3330776 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -2,7 +2,8 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy and Damien Doligez, INRIA Paris-Rocquencourt *) +(* Andrew W. Appel, Princeton University *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -33,7 +34,6 @@ inefficient implementation of maps as functions is also provided. *) -Require Import Equivalence EquivDec. Require Import Coqlib. (* To avoid useless definitions of inductors in extracted code. *) @@ -65,14 +65,6 @@ Module Type TREE. Axiom gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A), get i (set j x m) = if elt_eq i j then Some x else get i m. - (* We could implement the following, but it's not needed for the moment. - Hypothesis gsident: - forall (A: Type) (i: elt) (m: t A) (v: A), - get i m = Some v -> set i v m = m. - Hypothesis grident: - forall (A: Type) (i: elt) (m: t A) (v: A), - get i m = None -> remove i m = m. - *) Axiom grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None. Axiom gro: @@ -187,96 +179,208 @@ Module PTree <: TREE. Definition elt := positive. Definition elt_eq := peq. - Inductive tree (A : Type) : Type := - | Leaf : tree A - | Node : tree A -> option A -> tree A -> tree A. +(** ** Representation of trees *) + +(** The type [tree'] of nonempty trees. Each constructor is of the form + [NodeXYZ], where the bit [X] says whether there is a left subtree, + [Y] whether there is a value at this node, and [Z] whether there is + a right subtree. *) + + Inductive tree' (A: Type) : Type := + | Node001: tree' A -> tree' A + | Node010: A -> tree' A + | Node011: A -> tree' A -> tree' A + | Node100: tree' A -> tree' A + | Node101: tree' A -> tree' A ->tree' A + | Node110: tree' A -> A -> tree' A + | Node111: tree' A -> A -> tree' A -> tree' A. + + Inductive tree (A: Type) : Type := + | Empty : tree A + | Nodes: tree' A -> tree A. + + Arguments Node001 {A} _. + Arguments Node010 {A} _. + Arguments Node011 {A} _ _. + Arguments Node100 {A} _. + Arguments Node101 {A} _ _. + Arguments Node110 {A} _ _. + Arguments Node111 {A} _ _ _. - Arguments Leaf {A}. - Arguments Node [A]. - Scheme tree_ind := Induction for tree Sort Prop. + Arguments Empty {A}. + Arguments Nodes {A} _. + + Scheme tree'_ind := Induction for tree' Sort Prop. Definition t := tree. - Definition empty (A : Type) := (Leaf : t A). + (** A smart constructor for type [tree]: given a (possibly empty) + left subtree, a (possibly absent) value, and a (possibly empty) + right subtree, it builds the corresponding tree. *) + + Definition Node {A} (l: tree A) (o: option A) (r: tree A) : tree A := + match l,o,r with + | Empty, None, Empty => Empty + | Empty, None, Nodes r' => Nodes (Node001 r') + | Empty, Some x, Empty => Nodes (Node010 x) + | Empty, Some x, Nodes r' => Nodes (Node011 x r') + | Nodes l', None, Empty => Nodes (Node100 l') + | Nodes l', None, Nodes r' => Nodes (Node101 l' r') + | Nodes l', Some x, Empty => Nodes (Node110 l' x) + | Nodes l', Some x, Nodes r' => Nodes (Node111 l' x r') + end. - Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A := - match m with - | Leaf => None - | Node l o r => - match i with - | xH => o - | xO ii => get ii l - | xI ii => get ii r - end +(** ** Basic operations: [empty], [get], [set], [remove] *) + + Definition empty (A: Type) : t A := Empty. + + Fixpoint get' {A} (p: positive) (m: tree' A) : option A := + match p, m with + | xH, Node001 _ => None + | xH, Node010 x => Some x + | xH, Node011 x _ => Some x + | xH, Node100 _ => None + | xH, Node101 _ _ => None + | xH, Node110 _ x => Some x + | xH, Node111 _ x _ => Some x + | xO q, Node001 _ => None + | xO q, Node010 _ => None + | xO q, Node011 _ _ => None + | xO q, Node100 m' => get' q m' + | xO q, Node101 m' _ => get' q m' + | xO q, Node110 m' _ => get' q m' + | xO q, Node111 m' _ _ => get' q m' + | xI q, Node001 m' => get' q m' + | xI q, Node010 _ => None + | xI q, Node011 _ m' => get' q m' + | xI q, Node100 m' => None + | xI q, Node101 _ m' => get' q m' + | xI q, Node110 _ _ => None + | xI q, Node111 _ _ m' => get' q m' end. - Fixpoint set (A : Type) (i : positive) (v : A) (m : t A) {struct i} : t A := + Definition get {A} (p: positive) (m: tree A) : option A := match m with - | Leaf => - match i with - | xH => Node Leaf (Some v) Leaf - | xO ii => Node (set ii v Leaf) None Leaf - | xI ii => Node Leaf None (set ii v Leaf) - end - | Node l o r => - match i with - | xH => Node l (Some v) r - | xO ii => Node (set ii v l) o r - | xI ii => Node l o (set ii v r) - end + | Empty => None + | Nodes m' => get' p m' end. - Fixpoint remove (A : Type) (i : positive) (m : t A) {struct i} : t A := - match i with - | xH => - match m with - | Leaf => Leaf - | Node Leaf o Leaf => Leaf - | Node l o r => Node l None r - end - | xO ii => - match m with - | Leaf => Leaf - | Node l None Leaf => - match remove ii l with - | Leaf => Leaf - | mm => Node mm None Leaf - end - | Node l o r => Node (remove ii l) o r - end - | xI ii => - match m with - | Leaf => Leaf - | Node Leaf None r => - match remove ii r with - | Leaf => Leaf - | mm => Node Leaf None mm - end - | Node l o r => Node l o (remove ii r) - end - end. + (** [set0 p x] constructs the singleton tree that maps [p] to [x] + and has no other bindings. *) + + Fixpoint set0 {A} (p: positive) (x: A) : tree' A := + match p with + | xH => Node010 x + | xO q => Node100 (set0 q x) + | xI q => Node001 (set0 q x) + end. + + Fixpoint set' {A} (p: positive) (x: A) (m: tree' A) : tree' A := + match p, m with + | xH, Node001 r => Node011 x r + | xH, Node010 _ => Node010 x + | xH, Node011 _ r => Node011 x r + | xH, Node100 l => Node110 l x + | xH, Node101 l r => Node111 l x r + | xH, Node110 l _ => Node110 l x + | xH, Node111 l _ r => Node111 l x r + | xO q, Node001 r => Node101 (set0 q x) r + | xO q, Node010 y => Node110 (set0 q x) y + | xO q, Node011 y r => Node111 (set0 q x) y r + | xO q, Node100 l => Node100 (set' q x l) + | xO q, Node101 l r => Node101 (set' q x l) r + | xO q, Node110 l y => Node110 (set' q x l) y + | xO q, Node111 l y r => Node111 (set' q x l) y r + | xI q, Node001 r => Node001 (set' q x r) + | xI q, Node010 y => Node011 y (set0 q x) + | xI q, Node011 y r => Node011 y (set' q x r) + | xI q, Node100 l => Node101 l (set0 q x) + | xI q, Node101 l r => Node101 l (set' q x r) + | xI q, Node110 l y => Node111 l y (set0 q x) + | xI q, Node111 l y r => Node111 l y (set' q x r) + end. + + Definition set {A} (p: positive) (x: A) (m: tree A) : tree A := + match m with + | Empty => Nodes (set0 p x) + | Nodes m' => Nodes (set' p x m') + end. + + (** Removal in a nonempty tree produces a possibly empty tree. + To simplify the code, we use the [Node] smart constructor in the + cases where the result can be empty or nonempty, depending on the + results of the recursive calls. *) + + Fixpoint rem' {A} (p: positive) (m: tree' A) : tree A := + match p, m with + | xH, Node001 r => Nodes m + | xH, Node010 _ => Empty + | xH, Node011 _ r => Nodes (Node001 r) + | xH, Node100 l => Nodes m + | xH, Node101 l r => Nodes m + | xH, Node110 l _ => Nodes (Node100 l) + | xH, Node111 l _ r => Nodes (Node101 l r) + | xO q, Node001 r => Nodes m + | xO q, Node010 y => Nodes m + | xO q, Node011 y r => Nodes m + | xO q, Node100 l => Node (rem' q l) None Empty + | xO q, Node101 l r => Node (rem' q l) None (Nodes r) + | xO q, Node110 l y => Node (rem' q l) (Some y) Empty + | xO q, Node111 l y r => Node (rem' q l) (Some y) (Nodes r) + | xI q, Node001 r => Node Empty None (rem' q r) + | xI q, Node010 y => Nodes m + | xI q, Node011 y r => Node Empty (Some y) (rem' q r) + | xI q, Node100 l => Nodes m + | xI q, Node101 l r => Node (Nodes l) None (rem' q r) + | xI q, Node110 l y => Nodes m + | xI q, Node111 l y r => Node (Nodes l) (Some y) (rem' q r) + end. + + (** This use of [Node] causes some run-time overhead, which we eliminate + by partial evaluation within Coq. *) + + Definition remove' := Eval cbv [rem' Node] in @rem'. + + Definition remove {A} (p: positive) (m: tree A) : tree A := + match m with + | Empty => Empty + | Nodes m' => remove' p m' + end. + +(** ** Good variable properties for the basic operations *) Theorem gempty: forall (A: Type) (i: positive), get i (empty A) = None. + Proof. reflexivity. Qed. + + Lemma gEmpty: + forall (A: Type) (i: positive), get i (@Empty A) = None. + Proof. reflexivity. Qed. + + Lemma gss0: forall {A} p (x: A), get' p (set0 p x) = Some x. + Proof. induction p; simpl; auto. Qed. + + Lemma gso0: forall {A} p q (x: A), p<>q -> get' p (set0 q x) = None. Proof. - induction i; simpl; auto. + induction p; destruct q; simpl; intros; auto; try apply IHp; congruence. Qed. Theorem gss: - forall (A: Type) (i: positive) (x: A) (m: t A), get i (set i x m) = Some x. + forall (A: Type) (i: positive) (x: A) (m: tree A), get i (set i x m) = Some x. Proof. - induction i; destruct m; simpl; auto. + intros. destruct m as [|m]; simpl. + - apply gss0. + - revert m; induction i; destruct m; simpl; intros; auto using gss0. Qed. - Lemma gleaf : forall (A : Type) (i : positive), get i (Leaf : t A) = None. - Proof. exact gempty. Qed. - Theorem gso: - forall (A: Type) (i j: positive) (x: A) (m: t A), + forall (A: Type) (i j: positive) (x: A) (m: tree A), i <> j -> get i (set j x m) = get i m. Proof. - induction i; intros; destruct j; destruct m; simpl; - try rewrite <- (gleaf A i); auto; try apply IHi; congruence. + intros. destruct m as [|m]; simpl. + - apply gso0; auto. + - revert m j H; induction i; destruct j,m; simpl; intros; auto; + solve [apply IHi; congruence | apply gso0; congruence | congruence]. Qed. Theorem gsspec: @@ -287,72 +391,32 @@ Module PTree <: TREE. destruct (peq i j); [ rewrite e; apply gss | apply gso; auto ]. Qed. - Theorem gsident: - forall (A: Type) (i: positive) (m: t A) (v: A), - get i m = Some v -> set i v m = m. - Proof. - induction i; intros; destruct m; simpl; simpl in H; try congruence. - rewrite (IHi m2 v H); congruence. - rewrite (IHi m1 v H); congruence. - Qed. - - Theorem set2: - forall (A: Type) (i: elt) (m: t A) (v1 v2: A), - set i v2 (set i v1 m) = set i v2 m. + Lemma gNode: + forall {A} (i: positive) (l: tree A) (x: option A) (r: tree A), + get i (Node l x r) = match i with xH => x | xO j => get j l | xI j => get j r end. Proof. - induction i; intros; destruct m; simpl; try (rewrite IHi); auto. + intros. destruct l, x, r; simpl; auto; destruct i; auto. Qed. - Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf. - Proof. destruct i; simpl; auto. Qed. - Theorem grs: - forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None. - Proof. - induction i; destruct m. - simpl; auto. - destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto. - rewrite (rleaf A i); auto. - cut (get i (remove i (Node ll oo rr)) = None). - destruct (remove i (Node ll oo rr)); auto; apply IHi. - apply IHi. - simpl; auto. - destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto. - rewrite (rleaf A i); auto. - cut (get i (remove i (Node ll oo rr)) = None). - destruct (remove i (Node ll oo rr)); auto; apply IHi. - apply IHi. - simpl; auto. - destruct m1; destruct m2; simpl; auto. + forall (A: Type) (i: positive) (m: tree A), get i (remove i m) = None. + Proof. + Local Opaque Node. + destruct m as [ |m]; simpl. auto. + change (remove' i m) with (rem' i m). + revert m. induction i; destruct m; simpl; auto; rewrite gNode; auto. Qed. Theorem gro: - forall (A: Type) (i j: positive) (m: t A), + forall (A: Type) (i j: positive) (m: tree A), i <> j -> get i (remove j m) = get i m. Proof. - induction i; intros; destruct j; destruct m; - try rewrite (rleaf A (xI j)); - try rewrite (rleaf A (xO j)); - try rewrite (rleaf A 1); auto; - destruct m1; destruct o; destruct m2; - simpl; - try apply IHi; try congruence; - try rewrite (rleaf A j); auto; - try rewrite (gleaf A i); auto. - cut (get i (remove j (Node m2_1 o m2_2)) = get i (Node m2_1 o m2_2)); - [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf A i); auto - | apply IHi; congruence ]. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); - auto. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); - auto. - cut (get i (remove j (Node m1_1 o0 m1_2)) = get i (Node m1_1 o0 m1_2)); - [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf A i); auto - | apply IHi; congruence ]. - destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf A i); - auto. - destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf A i); - auto. + Local Opaque Node. + destruct m as [ |m]; simpl. auto. + change (remove' j m) with (rem' j m). + revert j m. induction i; destruct j, m; simpl; intros; auto; + solve [ congruence + | rewrite gNode; auto; apply IHi; congruence ]. Qed. Theorem grspec: @@ -362,47 +426,304 @@ Module PTree <: TREE. intros. destruct (elt_eq i j). subst j. apply grs. apply gro; auto. Qed. +(** ** Custom case analysis principles and induction principles *) + +(** We can view trees as being of one of two (non-exclusive) + cases: either [Empty] for an empty tree, or [Node l o r] for a + nonempty tree, with [l] and [r] the left and right subtrees + and [o] an optional value. The [Empty] constructor and the [Node] + smart function defined above provide one half of the view: the one + that lets us construct values of type [tree A]. + + We now define the other half of the view: the one that lets us + inspect and recurse over values of type [tree A]. This is achieved + by defining appropriate principles for case analysis and induction. *) + + Definition not_trivially_empty {A} (l: tree A) (o: option A) (r: tree A) := + match l, o, r with + | Empty, None, Empty => False + | _, _, _ => True + end. + + (** A case analysis principle *) + + Section TREE_CASE. + + Context {A B: Type} + (empty: B) + (node: tree A -> option A -> tree A -> B). + + Definition tree_case (m: tree A) : B := + match m with + | Empty => empty + | Nodes (Node001 r) => node Empty None (Nodes r) + | Nodes (Node010 x) => node Empty (Some x) Empty + | Nodes (Node011 x r) => node Empty (Some x) (Nodes r) + | Nodes (Node100 l) => node (Nodes l) None Empty + | Nodes (Node101 l r) => node (Nodes l) None (Nodes r) + | Nodes (Node110 l x) => node (Nodes l) (Some x) Empty + | Nodes (Node111 l x r) => node (Nodes l) (Some x) (Nodes r) + end. + + Lemma unroll_tree_case: forall l o r, + not_trivially_empty l o r -> + tree_case (Node l o r) = node l o r. + Proof. + destruct l, o, r; simpl; intros; auto. contradiction. + Qed. + + End TREE_CASE. + + (** A recursion principle *) + + Section TREE_REC. + + Context {A B: Type} + (empty: B) + (node: tree A -> B -> option A -> tree A -> B -> B). + + Fixpoint tree_rec' (m: tree' A) : B := + match m with + | Node001 r => node Empty empty None (Nodes r) (tree_rec' r) + | Node010 x => node Empty empty (Some x) Empty empty + | Node011 x r => node Empty empty (Some x) (Nodes r) (tree_rec' r) + | Node100 l => node (Nodes l) (tree_rec' l) None Empty empty + | Node101 l r => node (Nodes l) (tree_rec' l) None (Nodes r) (tree_rec' r) + | Node110 l x => node (Nodes l) (tree_rec' l) (Some x) Empty empty + | Node111 l x r => node (Nodes l) (tree_rec' l) (Some x) (Nodes r) (tree_rec' r) + end. + + Definition tree_rec (m: tree A) : B := + match m with + | Empty => empty + | Nodes m' => tree_rec' m' + end. + + Lemma unroll_tree_rec: forall l o r, + not_trivially_empty l o r -> + tree_rec (Node l o r) = node l (tree_rec l) o r (tree_rec r). + Proof. + destruct l, o, r; simpl; intros; auto. contradiction. + Qed. + + End TREE_REC. + + (** A double recursion principle *) + + Section TREE_REC2. + + Context {A B C: Type} + (base: C) + (base1: tree B -> C) + (base2: tree A -> C) + (nodes: forall (l1: tree A) (o1: option A) (r1: tree A) + (l2: tree B) (o2: option B) (r2: tree B) + (lrec: C) (rrec: C), C). + + Fixpoint tree_rec2' (m1: tree' A) (m2: tree' B) : C. + Proof. + destruct m1 as [ r1 | x1 | x1 r1 | l1 | l1 r1 | l1 x1 | l1 x1 r1 ]; + destruct m2 as [ r2 | x2 | x2 r2 | l2 | l2 r2 | l2 x2 | l2 x2 r2 ]; + (apply nodes; + [ solve [ exact (Nodes l1) | exact Empty ] + | solve [ exact (Some x1) | exact None ] + | solve [ exact (Nodes r1) | exact Empty ] + | solve [ exact (Nodes l2) | exact Empty ] + | solve [ exact (Some x2) | exact None ] + | solve [ exact (Nodes r2) | exact Empty ] + | solve [ exact (tree_rec2' l1 l2) | exact (base2 (Nodes l1)) | exact (base1 (Nodes l2)) | exact base ] + | solve [ exact (tree_rec2' r1 r2) | exact (base2 (Nodes r1)) | exact (base1 (Nodes r2)) | exact base ] + ]). + Defined. + + Definition tree_rec2 (a: tree A) (b: tree B) : C := + match a, b with + | Empty, Empty => base + | Empty, _ => base1 b + | _, Empty => base2 a + | Nodes a', Nodes b' => tree_rec2' a' b' + end. + + Lemma unroll_tree_rec2_NE: + forall l1 o1 r1, + not_trivially_empty l1 o1 r1 -> + tree_rec2 (Node l1 o1 r1) Empty = base2 (Node l1 o1 r1). + Proof. + intros. destruct l1, o1, r1; try contradiction; reflexivity. + Qed. + + Lemma unroll_tree_rec2_EN: + forall l2 o2 r2, + not_trivially_empty l2 o2 r2 -> + tree_rec2 Empty (Node l2 o2 r2) = base1 (Node l2 o2 r2). + Proof. + intros. destruct l2, o2, r2; try contradiction; reflexivity. + Qed. + + Lemma unroll_tree_rec2_NN: + forall l1 o1 r1 l2 o2 r2, + not_trivially_empty l1 o1 r1 -> not_trivially_empty l2 o2 r2 -> + tree_rec2 (Node l1 o1 r1) (Node l2 o2 r2) = + nodes l1 o1 r1 l2 o2 r2 (tree_rec2 l1 l2) (tree_rec2 r1 r2). + Proof. + intros. + destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction; reflexivity. + Qed. + + End TREE_REC2. + +(** An induction principle *) + + Section TREE_IND. + + Context {A: Type} (P: tree A -> Type) + (empty: P Empty) + (node: forall l, P l -> forall o r, P r -> not_trivially_empty l o r -> + P (Node l o r)). + + Program Fixpoint tree_ind' (m: tree' A) : P (Nodes m) := + match m with + | Node001 r => @node Empty empty None (Nodes r) (tree_ind' r) _ + | Node010 x => @node Empty empty (Some x) Empty empty _ + | Node011 x r => @node Empty empty (Some x) (Nodes r) (tree_ind' r) _ + | Node100 l => @node (Nodes l) (tree_ind' l) None Empty empty _ + | Node101 l r => @node (Nodes l) (tree_ind' l) None (Nodes r) (tree_ind' r) _ + | Node110 l x => @node (Nodes l) (tree_ind' l) (Some x) Empty empty _ + | Node111 l x r => @node (Nodes l) (tree_ind' l) (Some x) (Nodes r) (tree_ind' r) _ + end. + + Definition tree_ind (m: tree A) : P m := + match m with + | Empty => empty + | Nodes m' => tree_ind' m' + end. + + End TREE_IND. + +(** ** Extensionality property *) + + Lemma tree'_not_empty: + forall {A} (m: tree' A), exists i, get' i m <> None. + Proof. + induction m; simpl; try destruct IHm as [p H]. + - exists (xI p); auto. + - exists xH; simpl; congruence. + - exists xH; simpl; congruence. + - exists (xO p); auto. + - destruct IHm1 as [p H]; exists (xO p); auto. + - exists xH; simpl; congruence. + - exists xH; simpl; congruence. + Qed. + + Corollary extensionality_empty: + forall {A} (m: tree A), + (forall i, get i m = None) -> m = Empty. + Proof. + intros. destruct m as [ | m]; auto. destruct (tree'_not_empty m) as [i GET]. + elim GET. apply H. + Qed. + + Theorem extensionality: + forall (A: Type) (m1 m2: tree A), + (forall i, get i m1 = get i m2) -> m1 = m2. + Proof. + intros A. induction m1 using tree_ind; induction m2 using tree_ind; intros. + - auto. + - symmetry. apply extensionality_empty. intros; symmetry; apply H0. + - apply extensionality_empty. apply H0. + - f_equal. + + apply IHm1_1. intros. specialize (H1 (xO i)); rewrite ! gNode in H1. auto. + + specialize (H1 xH); rewrite ! gNode in H1. auto. + + apply IHm1_2. intros. specialize (H1 (xI i)); rewrite ! gNode in H1. auto. + Qed. + + (** Some consequences of extensionality *) + + Theorem gsident: + forall {A} (i: positive) (m: t A) (v: A), + get i m = Some v -> set i v m = m. + Proof. + intros; apply extensionality; intros j. + rewrite gsspec. destruct (peq j i); congruence. + Qed. + + Theorem set2: + forall {A} (i: elt) (m: t A) (v1 v2: A), + set i v2 (set i v1 m) = set i v2 m. + Proof. + intros; apply extensionality; intros j. + rewrite ! gsspec. destruct (peq j i); auto. + Qed. + +(** ** Boolean equality *) + Section BOOLEAN_EQUALITY. Variable A: Type. Variable beqA: A -> A -> bool. - Fixpoint bempty (m: t A) : bool := - match m with - | Leaf => true - | Node l None r => bempty l && bempty r - | Node l (Some _) r => false - end. + Fixpoint beq' (m1 m2: tree' A) {struct m1} : bool := + match m1, m2 with + | Node001 r1, Node001 r2 => beq' r1 r2 + | Node010 x1, Node010 x2 => beqA x1 x2 + | Node011 x1 r1, Node011 x2 r2 => beqA x1 x2 && beq' r1 r2 + | Node100 l1, Node100 l2 => beq' l1 l2 + | Node101 l1 r1, Node101 l2 r2 => beq' l1 l2 && beq' r1 r2 + | Node110 l1 x1, Node110 l2 x2 => beqA x1 x2 && beq' l1 l2 + | Node111 l1 x1 r1, Node111 l2 x2 r2 => beqA x1 x2 && beq' l1 l2 && beq' r1 r2 + | _, _ => false + end. - Fixpoint beq (m1 m2: t A) {struct m1} : bool := - match m1, m2 with - | Leaf, _ => bempty m2 - | _, Leaf => bempty m1 - | Node l1 o1 r1, Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq l1 l2 && beq r1 r2 + Definition beq (m1 m2: t A) : bool := + match m1, m2 with + | Empty, Empty => true + | Nodes m1', Nodes m2' => beq' m1' m2' + | _, _ => false + end. + + Let beq_optA (o1 o2: option A) : bool := + match o1, o2 with + | None, None => true + | Some a1, Some a2 => beqA a1 a2 + | _, _ => false end. - Lemma bempty_correct: - forall m, bempty m = true <-> (forall x, get x m = None). + Lemma beq_correct_bool: + forall m1 m2, + beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true). Proof. - induction m; simpl. - split; intros. apply gleaf. auto. - destruct o; split; intros. - congruence. - generalize (H xH); simpl; congruence. - destruct (andb_prop _ _ H). rewrite IHm1 in H0. rewrite IHm2 in H1. - destruct x; simpl; auto. - apply andb_true_intro; split. - apply IHm1. intros; apply (H (xO x)). - apply IHm2. intros; apply (H (xI x)). +Local Transparent Node. + assert (beq_NN: forall l1 o1 r1 l2 o2 r2, + not_trivially_empty l1 o1 r1 -> + not_trivially_empty l2 o2 r2 -> + beq (Node l1 o1 r1) (Node l2 o2 r2) = + beq l1 l2 && beq_optA o1 o2 && beq r1 r2). + { intros. + destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction; + simpl; rewrite ? andb_true_r, ? andb_false_r; auto. + rewrite andb_comm; auto. + f_equal; rewrite andb_comm; auto. } + induction m1 using tree_ind; [|induction m2 using tree_ind]. + - intros. simpl; split; intros. + + destruct m2; try discriminate. simpl; auto. + + replace m2 with (@Empty A); auto. apply extensionality; intros x. + specialize (H x). destruct (get x m2); simpl; congruence. + - split; intros. + + destruct (Node l o r); try discriminate. simpl; auto. + + replace (Node l o r) with (@Empty A); auto. apply extensionality; intros x. + specialize (H0 x). destruct (get x (Node l o r)); simpl in *; congruence. + - rewrite beq_NN by auto. split; intros. + + InvBooleans. rewrite ! gNode. destruct x. + * apply IHm0; auto. + * apply IHm1; auto. + * auto. + + apply andb_true_intro; split; [apply andb_true_intro; split|]. + * apply IHm1. intros. specialize (H1 (xO x)); rewrite ! gNode in H1; auto. + * specialize (H1 xH); rewrite ! gNode in H1; auto. + * apply IHm0. intros. specialize (H1 (xI x)); rewrite ! gNode in H1; auto. Qed. - Lemma beq_correct: + Theorem beq_correct: forall m1 m2, beq m1 m2 = true <-> (forall (x: elt), @@ -412,27 +733,15 @@ Module PTree <: TREE. | _, _ => False end). Proof. - induction m1; intros. - - simpl. rewrite bempty_correct. split; intros. - rewrite gleaf. rewrite H. auto. - generalize (H x). rewrite gleaf. destruct (get x m2); tauto. - - destruct m2. - + unfold beq. rewrite bempty_correct. split; intros. - rewrite H. rewrite gleaf. auto. - generalize (H x). rewrite gleaf. destruct (get x (Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). + intros. rewrite beq_correct_bool. unfold beq_optA. split; intros. + - specialize (H x). destruct (get x m1), (get x m2); intuition congruence. + - specialize (H x). destruct (get x m1), (get x m2); intuition auto. Qed. End BOOLEAN_EQUALITY. +(** ** Collective operations *) + Fixpoint prev_append (i j: positive) {struct i} : positive := match i with | xH => j @@ -464,78 +773,92 @@ Module PTree <: TREE. specialize (Hi _ _ H); congruence. Qed. - Fixpoint xmap (A B : Type) (f : positive -> A -> B) (m : t A) (i : positive) - {struct m} : t B := - match m with - | Leaf => Leaf - | Node l o r => Node (xmap f l (xO i)) - (match o with None => None | Some x => Some (f (prev i) x) end) - (xmap f r (xI i)) - end. + Fixpoint map' {A B} (f: positive -> A -> B) (m: tree' A) (i: positive) + {struct m} : tree' B := + match m with + | Node001 r => Node001 (map' f r (xI i)) + | Node010 x => Node010 (f (prev i) x) + | Node011 x r => Node011 (f (prev i) x) (map' f r (xI i)) + | Node100 l => Node100 (map' f l (xO i)) + | Node101 l r => Node101 (map' f l (xO i)) (map' f r (xI i)) + | Node110 l x => Node110 (map' f l (xO i)) (f (prev i) x) + | Node111 l x r => Node111 (map' f l (xO i)) (f (prev i) x) (map' f r (xI i)) + end. - Definition map (A B : Type) (f : positive -> A -> B) m := xmap f m xH. + Definition map {A B} (f: positive -> A -> B) (m: tree A) := + match m with + | Empty => Empty + | Nodes m => Nodes (map' f m xH) + end. - Lemma xgmap: - forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), - get i (xmap f m j) = option_map (f (prev (prev_append i j))) (get i m). - Proof. - induction i; intros; destruct m; simpl; auto. - Qed. + Lemma gmap': + forall {A B} (f: positive -> A -> B) (i j : positive) (m: tree' A), + get' i (map' f m j) = option_map (f (prev (prev_append i j))) (get' i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. Theorem gmap: - forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), + forall {A B} (f: positive -> A -> B) (i: positive) (m: t A), get i (map f m) = option_map (f i) (get i m). Proof. - intros A B f i m. - unfold map. - rewrite xgmap. repeat f_equal. exact (prev_involutive i). + intros; destruct m as [|m]; simpl. auto. rewrite gmap'. repeat f_equal. exact (prev_involutive i). Qed. - Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B := + Fixpoint map1' {A B} (f: A -> B) (m: tree' A) {struct m} : tree' B := + match m with + | Node001 r => Node001 (map1' f r) + | Node010 x => Node010 (f x) + | Node011 x r => Node011 (f x) (map1' f r) + | Node100 l => Node100 (map1' f l) + | Node101 l r => Node101 (map1' f l) (map1' f r) + | Node110 l x => Node110 (map1' f l) (f x) + | Node111 l x r => Node111 (map1' f l) (f x) (map1' f r) + end. + + Definition map1 {A B} (f: A -> B) (m: t A) : t B := match m with - | Leaf => Leaf - | Node l o r => Node (map1 f l) (option_map f o) (map1 f r) + | Empty => Empty + | Nodes m => Nodes (map1' f m) end. Theorem gmap1: - forall (A B: Type) (f: A -> B) (i: elt) (m: t A), + forall {A B} (f: A -> B) (i: elt) (m: t A), get i (map1 f m) = option_map f (get i m). Proof. - induction i; intros; destruct m; simpl; auto. + intros. destruct m as [|m]; simpl. auto. + revert i; induction m; destruct i; simpl; auto. Qed. - Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A := - match l, x, r with - | Leaf, None, Leaf => Leaf - | _, _, _ => Node l x r - end. + Definition map_filter1_nonopt {A B} (f: A -> option B) (m: tree A) : tree B := + tree_rec + Empty + (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec) + m. + + Definition map_filter1 := + Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt. - Lemma gnode': - forall (A: Type) (l r: t A) (x: option A) (i: positive), - get i (Node' l x r) = get i (Node l x r). + Lemma gmap_filter1: + forall {A B} (f: A -> option B) (m: tree A) (i: positive), + get i (map_filter1 f m) = match get i m with None => None | Some a => f a end. Proof. - intros. unfold Node'. - destruct l; destruct x; destruct r; auto. - destruct i; simpl; auto; rewrite gleaf; auto. + change @map_filter1 with @map_filter1_nonopt. unfold map_filter1_nonopt. + intros until f. induction m using tree_ind; intros. + - auto. + - rewrite unroll_tree_rec by auto. rewrite ! gNode; destruct i; auto. Qed. - Fixpoint filter1 (A: Type) (pred: A -> bool) (m: t A) {struct m} : t A := - match m with - | Leaf => Leaf - | Node l o r => - let o' := match o with None => None | Some x => if pred x then o else None end in - Node' (filter1 pred l) o' (filter1 pred r) - end. + Definition filter1 {A} (pred: A -> bool) (m: t A) : t A := + map_filter1 (fun a => if pred a then Some a else None) m. Theorem gfilter1: - forall (A: Type) (pred: A -> bool) (i: elt) (m: t A), + forall {A} (pred: A -> bool) (i: elt) (m: t A), get i (filter1 pred m) = match get i m with None => None | Some x => if pred x then Some x else None end. Proof. - intros until m. revert m i. induction m; simpl; intros. - rewrite gleaf; auto. - rewrite gnode'. destruct i; simpl; auto. destruct o; auto. - Qed. + intros. apply gmap_filter1. + Qed. Section COMBINE. @@ -543,201 +866,152 @@ Module PTree <: TREE. Variable f: option A -> option B -> option C. Hypothesis f_none_none: f None None = None. - Fixpoint xcombine_l (m : t A) {struct m} : t C := - match m with - | Leaf => Leaf - | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r) - end. + Let combine_l := map_filter1 (fun a => f (Some a) None). + Let combine_r := map_filter1 (fun b => f None (Some b)). - Lemma xgcombine_l : - forall (m: t A) (i : positive), - get i (xcombine_l m) = f (get i m) None. - Proof. - induction m; intros; simpl. - repeat rewrite gleaf. auto. - rewrite gnode'. destruct i; simpl; auto. - Qed. + Let combine_nonopt (m1: tree A) (m2: tree B) : tree C := + tree_rec2 + Empty + combine_r + combine_l + (fun l1 o1 r1 l2 o2 r2 lrec rrec => + Node lrec + (match o1, o2 with None, None => None | _, _ => f o1 o2 end) + rrec) + m1 m2. - Fixpoint xcombine_r (m : t B) {struct m} : t C := - match m with - | Leaf => Leaf - | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r) - end. + Definition combine := + Eval cbv [combine_nonopt tree_rec2 tree_rec2'] in combine_nonopt. - Lemma xgcombine_r : - forall (m: t B) (i : positive), - get i (xcombine_r m) = f None (get i m). - Proof. - induction m; intros; simpl. - repeat rewrite gleaf. auto. - rewrite gnode'. destruct i; simpl; auto. - Qed. + Lemma gcombine_l: forall m i, get i (combine_l m) = f (get i m) None. + Proof. + intros; unfold combine_l; rewrite gmap_filter1. destruct (get i m); auto. + Qed. - Fixpoint combine (m1: t A) (m2: t B) {struct m1} : t C := - match m1 with - | Leaf => xcombine_r m2 - | Node l1 o1 r1 => - match m2 with - | Leaf => xcombine_l m1 - | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2) - end - end. + Lemma gcombine_r: forall m i, get i (combine_r m) = f None (get i m). + Proof. + intros; unfold combine_r; rewrite gmap_filter1. destruct (get i m); auto. + Qed. Theorem gcombine: forall (m1: t A) (m2: t B) (i: positive), get i (combine m1 m2) = f (get i m1) (get i m2). Proof. - induction m1; intros; simpl. - rewrite gleaf. apply xgcombine_r. - destruct m2; simpl. - rewrite gleaf. rewrite <- xgcombine_l. auto. - repeat rewrite gnode'. destruct i; simpl; auto. + change combine with combine_nonopt. + induction m1 using tree_ind; induction m2 using tree_ind; intros. + - auto. + - unfold combine_nonopt; rewrite unroll_tree_rec2_EN by auto. apply gcombine_r. + - unfold combine_nonopt; rewrite unroll_tree_rec2_NE by auto. apply gcombine_l. + - unfold combine_nonopt; rewrite unroll_tree_rec2_NN by auto. + rewrite ! gNode; destruct i; auto. destruct o, o0; auto. Qed. End COMBINE. - Lemma xcombine_lr : - forall (A B: Type) (f g : option A -> option A -> option B) (m : t A), - (forall (i j : option A), f i j = g j i) -> - xcombine_l f m = xcombine_r g m. - Proof. - induction m; intros; simpl; auto. - rewrite IHm1; auto. - rewrite IHm2; auto. - rewrite H; auto. - Qed. - Theorem combine_commut: forall (A B: Type) (f g: option A -> option A -> option B), + f None None = None -> g None None = None -> (forall (i j: option A), f i j = g j i) -> forall (m1 m2: t A), combine f m1 m2 = combine g m2 m1. Proof. - intros A B f g EQ1. - assert (EQ2: forall (i j: option A), g i j = f j i). - intros; auto. - induction m1; intros; destruct m2; simpl; - try rewrite EQ1; - repeat rewrite (xcombine_lr f g); - repeat rewrite (xcombine_lr g f); - auto. - rewrite IHm1_1. - rewrite IHm1_2. - auto. - Qed. - - Fixpoint xelements (A : Type) (m : t A) (i : positive) - (k: list (positive * A)) {struct m} - : list (positive * A) := - match m with - | Leaf => k - | Node l None r => - xelements l (xO i) (xelements r (xI i) k) - | Node l (Some x) r => - xelements l (xO i) - ((prev i, x) :: xelements r (xI i) k) - end. + intros. apply extensionality; intros i. rewrite ! gcombine by auto. auto. + Qed. - Definition elements (A: Type) (m : t A) := xelements m xH nil. +(** ** List of all bindings *) - Remark xelements_append: - forall A (m: t A) i k1 k2, - xelements m i (k1 ++ k2) = xelements m i k1 ++ k2. - Proof. - induction m; intros; simpl. - - auto. - - destruct o; rewrite IHm2; rewrite <- IHm1; auto. - Qed. + Fixpoint xelements' {A} (m : tree' A) (i: positive) (k: list (positive * A)) + {struct m} : list (positive * A) := + match m with + | Node001 r => xelements' r (xI i) k + | Node010 x => (prev i, x) :: k + | Node011 x r => (prev i, x) :: xelements' r (xI i) k + | Node100 l => xelements' l (xO i) k + | Node101 l r => xelements' l (xO i) (xelements' r (xI i) k) + | Node110 l x => xelements' l (xO i) ((prev i, x)::k) + | Node111 l x r => xelements' l (xO i) ((prev i, x):: (xelements' r (xI i) k)) + end. - Remark xelements_leaf: - forall A i, xelements (@Leaf A) i nil = nil. + Definition elements {A} (m : t A) : list (positive * A) := + match m with Empty => nil | Nodes m' => xelements' m' xH nil end. + + Definition xelements {A} (m : t A) (i: positive) : list (positive * A) := + match m with Empty => nil | Nodes m' => xelements' m' i nil end. + + Lemma xelements'_append: + forall A (m: tree' A) i k1 k2, + xelements' m i (k1 ++ k2) = xelements' m i k1 ++ k2. Proof. - intros; reflexivity. + induction m; intros; simpl; auto. + - f_equal; auto. + - rewrite IHm2, IHm1. auto. + - rewrite <- IHm. auto. + - rewrite IHm2, <- IHm1. auto. Qed. - Remark xelements_node: - forall A (m1: t A) o (m2: t A) i, - xelements (Node m1 o m2) i nil = - xelements m1 (xO i) nil + Lemma xelements_Node: + forall A (l: tree A) (o: option A) (r: tree A) i, + xelements (Node l o r) i = + xelements l (xO i) ++ match o with None => nil | Some v => (prev i, v) :: nil end - ++ xelements m2 (xI i) nil. + ++ xelements r (xI i). Proof. - intros. simpl. destruct o; simpl; rewrite <- xelements_append; auto. + Local Transparent Node. + intros; destruct l, o, r; simpl; rewrite <- ? xelements'_append; auto. Qed. - Lemma xelements_incl: - forall (A: Type) (m: t A) (i : positive) k x, - In x k -> In x (xelements m i k). - Proof. - induction m; intros; simpl. - auto. - destruct o. - apply IHm1. simpl; right; auto. - auto. - Qed. - - Lemma xelements_correct: - forall (A: Type) (m: t A) (i j : positive) (v: A) k, - get i m = Some v -> In (prev (prev_append i j), v) (xelements m j k). - Proof. - induction m; intros. - rewrite (gleaf A i) in H; congruence. - destruct o; destruct i; simpl; simpl in H. - apply xelements_incl. right. auto. - auto. - inv H. apply xelements_incl. left. reflexivity. - apply xelements_incl. auto. - auto. - inv H. - Qed. + Lemma xelements_correct: + forall A (m: tree A) i j v, + get i m = Some v -> In (prev (prev_append i j), v) (xelements m j). + Proof. + intros A. induction m using tree_ind; intros. + - discriminate. + - rewrite xelements_Node, ! in_app. rewrite gNode in H0. destruct i. + + right; right. apply (IHm2 i (xI j)); auto. + + left. apply (IHm1 i (xO j)); auto. + + right; left. subst o. rewrite prev_append_prev. auto with coqlib. + Qed. Theorem elements_correct: - forall (A: Type) (m: t A) (i: positive) (v: A), + forall A (m: t A) (i: positive) (v: A), get i m = Some v -> In (i, v) (elements m). Proof. intros A m i v H. - generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id. + generalize (xelements_correct m i xH H). rewrite prev_append_prev. auto. Qed. Lemma in_xelements: - forall (A: Type) (m: t A) (i k: positive) (v: A) , - In (k, v) (xelements m i nil) -> + forall A (m: tree A) (i k: positive) (v: A) , + In (k, v) (xelements m i) -> exists j, k = prev (prev_append j i) /\ get j m = Some v. Proof. - induction m; intros. - - rewrite xelements_leaf in H. contradiction. - - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]]. - + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); auto. - + destruct o; simpl in P; intuition auto. inv H. exists xH; auto. - + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); auto. + intros A. induction m using tree_ind; intros. + - elim H. + - rewrite xelements_Node, ! in_app in H0. destruct H0 as [P | [P | P]]. + + exploit IHm1; eauto. intros (j & Q & R). exists (xO j); rewrite gNode; auto. + + destruct o; simpl in P; intuition auto. inv H0. exists xH; rewrite gNode; auto. + + exploit IHm2; eauto. intros (j & Q & R). exists (xI j); rewrite gNode; auto. Qed. Theorem elements_complete: - forall (A: Type) (m: t A) (i: positive) (v: A), + forall A (m: t A) (i: positive) (v: A), In (i, v) (elements m) -> get i m = Some v. Proof. - unfold elements. intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). + intros A m i v H. exploit in_xelements; eauto. intros (j & P & Q). rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. exploit prev_append_inj; eauto. intros; congruence. Qed. - Definition xkeys (A: Type) (m: t A) (i: positive) := - List.map (@fst positive A) (xelements m i nil). - - Remark xkeys_leaf: - forall A i, xkeys (@Leaf A) i = nil. - Proof. - intros; reflexivity. - Qed. + Definition xkeys {A} (m: t A) (i: positive) := List.map fst (xelements m i). - Remark xkeys_node: + Lemma xkeys_Node: forall A (m1: t A) o (m2: t A) i, xkeys (Node m1 o m2) i = xkeys m1 (xO i) ++ match o with None => nil | Some v => prev i :: nil end ++ xkeys m2 (xI i). Proof. - intros. unfold xkeys. rewrite xelements_node. rewrite ! map_app. destruct o; auto. + intros. unfold xkeys. rewrite xelements_Node, ! map_app. destruct o; auto. Qed. Lemma in_xkeys: @@ -754,40 +1028,36 @@ Module PTree <: TREE. forall (A: Type) (m: t A) (i: positive), list_norepet (xkeys m i). Proof. - induction m; intros. - - rewrite xkeys_leaf; constructor. - - assert (NOTIN1: ~ In (prev i) (xkeys m1 (xO i))). + intros A; induction m using tree_ind; intros. + - constructor. + - assert (NOTIN1: ~ In (prev i) (xkeys l (xO i))). { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } - assert (NOTIN2: ~ In (prev i) (xkeys m2 (xI i))). + assert (NOTIN2: ~ In (prev i) (xkeys r (xI i))). { red; intros. exploit in_xkeys; eauto. intros (j & EQ). rewrite prev_append_prev in EQ. simpl in EQ. apply prev_append_inj in EQ. discriminate. } - assert (DISJ: forall x, In x (xkeys m1 (xO i)) -> In x (xkeys m2 (xI i)) -> False). - { intros. exploit in_xkeys. eexact H. intros (j1 & EQ1). - exploit in_xkeys. eexact H0. intros (j2 & EQ2). + assert (DISJ: forall x, In x (xkeys l (xO i)) -> In x (xkeys r (xI i)) -> False). + { intros. exploit in_xkeys. eexact H0. intros (j1 & EQ1). + exploit in_xkeys. eexact H1. intros (j2 & EQ2). rewrite prev_append_prev in *. simpl in *. rewrite EQ2 in EQ1. apply prev_append_inj in EQ1. discriminate. } - rewrite xkeys_node. apply list_norepet_append. auto. + rewrite xkeys_Node. apply list_norepet_append. auto. destruct o; simpl; auto. constructor; auto. - red; intros. red; intros; subst y. destruct o; simpl in H0. - destruct H0. subst x. tauto. eauto. eauto. + red; intros. red; intros; subst y. destruct o; simpl in H1. + destruct H1. subst x. tauto. eauto. eauto. Qed. Theorem elements_keys_norepet: - forall (A: Type) (m: t A), + forall A (m: t A), list_norepet (List.map (@fst elt A) (elements m)). Proof. intros. apply (xelements_keys_norepet m xH). Qed. Remark xelements_empty: - forall (A: Type) (m: t A) i, (forall i, get i m = None) -> xelements m i nil = nil. + forall A (m: t A) i, (forall i, get i m = None) -> xelements m i = nil. Proof. - induction m; intros. - auto. - rewrite xelements_node. rewrite IHm1, IHm2. destruct o; auto. - generalize (H xH); simpl; congruence. - intros. apply (H (xI i0)). - intros. apply (H (xO i0)). + intros. replace m with (@Empty A). auto. + apply extensionality; intros. symmetry; auto. Qed. Theorem elements_canonical_order': @@ -797,19 +1067,18 @@ Module PTree <: TREE. (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (elements m) (elements n). Proof. - intros until n. unfold elements. generalize 1%positive. revert m n. - induction m; intros. - - simpl. rewrite xelements_empty. constructor. - intros. specialize (H i). rewrite gempty in H. inv H; auto. - - destruct n as [ | n1 o' n2 ]. - + rewrite (xelements_empty (Node m1 o m2)). simpl; constructor. - intros. specialize (H i). rewrite gempty in H. inv H; auto. - + rewrite ! xelements_node. repeat apply list_forall2_app. - apply IHm1. intros. apply (H (xO i)). - generalize (H xH); simpl; intros OR; inv OR. - constructor. - constructor. auto. constructor. - apply IHm2. intros. apply (H (xI i)). + intros until n. + change (elements m) with (xelements m xH). change (elements n) with (xelements n xH). + generalize 1%positive. revert m n. + induction m using tree_ind; [ | induction n using tree_ind]; intros until p; intros REL. + - replace n with (@Empty B). constructor. + apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto. + - replace (Node l o r) with (@Empty A). constructor. + apply extensionality; intros. specialize (REL i). simpl in *. inv REL; auto. + - rewrite ! xelements_Node. repeat apply list_forall2_app. + + apply IHm. intros. specialize (REL (xO i)). rewrite ! gNode in REL; auto. + + specialize (REL xH). rewrite ! gNode in REL. inv REL; constructor; auto using list_forall2_nil. + + apply IHm0. intros. specialize (REL (xI i)). rewrite ! gNode in REL; auto. Qed. Theorem elements_canonical_order: @@ -833,57 +1102,48 @@ Module PTree <: TREE. (forall i, get i m = get i n) -> elements m = elements n. Proof. - intros. - exploit (@elements_canonical_order' _ _ (fun (x y: A) => x = y) m n). - intros. rewrite H. destruct (get i n); constructor; auto. - induction 1. auto. destruct a1 as [a2 a3]; destruct b1 as [b2 b3]; simpl in *. - destruct H0. congruence. + intros. replace n with m; auto. apply extensionality; auto. Qed. Lemma xelements_remove: - forall (A: Type) v (m: t A) i j, + forall A v (m: t A) i j, get i m = Some v -> exists l1 l2, - xelements m j nil = l1 ++ (prev (prev_append i j), v) :: l2 - /\ xelements (remove i m) j nil = l1 ++ l2. - Proof. - induction m; intros. - - rewrite gleaf in H; discriminate. - - assert (REMOVE: xelements (remove i (Node m1 o m2)) j nil = - xelements (match i with - | xH => Node m1 None m2 - | xO ii => Node (remove ii m1) o m2 - | xI ii => Node m1 o (remove ii m2) end) - j nil). - { - destruct i; simpl remove. - destruct m1; auto. destruct o; auto. destruct (remove i m2); auto. - destruct o; auto. destruct m2; auto. destruct (remove i m1); auto. - destruct m1; auto. destruct m2; auto. - } - rewrite REMOVE. destruct i; simpl in H. - + destruct (IHm2 i (xI j) H) as (l1 & l2 & EQ & EQ'). - exists (xelements m1 (xO j) nil ++ + xelements m j = l1 ++ (prev (prev_append i j), v) :: l2 + /\ xelements (remove i m) j = l1 ++ l2. + Proof. + intros A; induction m using tree_ind; intros. + - discriminate. + - assert (REMOVE: remove i (Node l o r) = + match i with + | xH => Node l None r + | xO ii => Node (remove ii l) o r + | xI ii => Node l o (remove ii r) + end). + { destruct l, o, r, i; reflexivity. } + rewrite gNode in H0. rewrite REMOVE. destruct i; rewrite ! xelements_Node. + + destruct (IHm0 i (xI j) H0) as (l1 & l2 & EQ & EQ'). + exists (xelements l (xO j) ++ match o with None => nil | Some x => (prev j, x) :: nil end ++ l1); exists l2; split. - rewrite xelements_node, EQ, ! app_ass. auto. - rewrite xelements_node, EQ', ! app_ass. auto. - + destruct (IHm1 i (xO j) H) as (l1 & l2 & EQ & EQ'). + rewrite EQ, ! app_ass. auto. + rewrite EQ', ! app_ass. auto. + + destruct (IHm i (xO j) H0) as (l1 & l2 & EQ & EQ'). exists l1; exists (l2 ++ match o with None => nil | Some x => (prev j, x) :: nil end ++ - xelements m2 (xI j) nil); + xelements r (xI j)); split. - rewrite xelements_node, EQ, ! app_ass. auto. - rewrite xelements_node, EQ', ! app_ass. auto. - + subst o. exists (xelements m1 (xO j) nil); exists (xelements m2 (xI j) nil); split. - rewrite xelements_node. rewrite prev_append_prev. auto. - rewrite xelements_node; auto. + rewrite EQ, ! app_ass. auto. + rewrite EQ', ! app_ass. auto. + + subst o. exists (xelements l (xO j)); exists (xelements r (xI j)); split. + rewrite prev_append_prev. auto. + auto. Qed. Theorem elements_remove: - forall (A: Type) i v (m: t A), + forall A i v (m: t A), get i m = Some v -> exists l1 l2, elements m = l1 ++ (i,v) :: l2 /\ elements (remove i m) = l1 ++ l2. Proof. @@ -891,74 +1151,82 @@ Module PTree <: TREE. rewrite prev_append_prev. auto. Qed. - Fixpoint xfold (A B: Type) (f: B -> positive -> A -> B) - (i: positive) (m: t A) (v: B) {struct m} : B := +(** ** Folding over a tree *) + + Fixpoint fold' {A B} (f: B -> positive -> A -> B) + (i: positive) (m: tree' A) (v: B) {struct m} : B := match m with - | Leaf => v - | Node l None r => - let v1 := xfold f (xO i) l v in - xfold f (xI i) r v1 - | Node l (Some x) r => - let v1 := xfold f (xO i) l v in - let v2 := f v1 (prev i) x in - xfold f (xI i) r v2 + | Node001 r => fold' f (xI i) r v + | Node010 x => f v (prev i) x + | Node011 x r => fold' f (xI i) r (f v (prev i) x) + | Node100 l => fold' f (xO i) l v + | Node101 l r => fold' f (xI i) r (fold' f (xO i) l v) + | Node110 l x => f (fold' f (xO i) l v) (prev i) x + | Node111 l x r => fold' f (xI i) r (f (fold' f (xO i) l v) (prev i) x) end. - Definition fold (A B : Type) (f: B -> positive -> A -> B) (m: t A) (v: B) := - xfold f xH m v. + Definition fold {A B} (f: B -> positive -> A -> B) (m: t A) (v: B) := + match m with Empty => v | Nodes m' => fold' f xH m' v end. - Lemma xfold_xelements: - forall (A B: Type) (f: B -> positive -> A -> B) m i v l, - List.fold_left (fun a p => f a (fst p) (snd p)) l (xfold f i m v) = - List.fold_left (fun a p => f a (fst p) (snd p)) (xelements m i l) v. + Lemma fold'_xelements': + forall A B (f: B -> positive -> A -> B) m i v l, + List.fold_left (fun a p => f a (fst p) (snd p)) l (fold' f i m v) = + List.fold_left (fun a p => f a (fst p) (snd p)) (xelements' m i l) v. Proof. - induction m; intros. - simpl. auto. - destruct o; simpl. - rewrite <- IHm1. simpl. rewrite <- IHm2. auto. - rewrite <- IHm1. rewrite <- IHm2. auto. + induction m; intros; simpl; auto. + rewrite <- IHm1, <- IHm2; auto. + rewrite <- IHm; auto. + rewrite <- IHm1. simpl. rewrite <- IHm2; auto. Qed. Theorem fold_spec: - forall (A B: Type) (f: B -> positive -> A -> B) (v: B) (m: t A), + forall A B (f: B -> positive -> A -> B) (v: B) (m: t A), fold f m v = List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v. Proof. - intros. unfold fold, elements. rewrite <- xfold_xelements. auto. + intros. unfold fold, elements. destruct m; auto. rewrite <- fold'_xelements'. auto. Qed. - Fixpoint fold1 (A B: Type) (f: B -> A -> B) (m: t A) (v: B) {struct m} : B := + Fixpoint fold1' {A B} (f: B -> A -> B) (m: tree' A) (v: B) {struct m} : B := match m with - | Leaf => v - | Node l None r => - let v1 := fold1 f l v in - fold1 f r v1 - | Node l (Some x) r => - let v1 := fold1 f l v in - let v2 := f v1 x in - fold1 f r v2 + | Node001 r => fold1' f r v + | Node010 x => f v x + | Node011 x r => fold1' f r (f v x) + | Node100 l => fold1' f l v + | Node101 l r => fold1' f r (fold1' f l v) + | Node110 l x => f (fold1' f l v) x + | Node111 l x r => fold1' f r (f (fold1' f l v) x) end. - Lemma fold1_xelements: - forall (A B: Type) (f: B -> A -> B) m i v l, - List.fold_left (fun a p => f a (snd p)) l (fold1 f m v) = - List.fold_left (fun a p => f a (snd p)) (xelements m i l) v. + + Definition fold1 {A B} (f: B -> A -> B) (m: t A) (v: B) : B := + match m with Empty => v | Nodes m' => fold1' f m' v end. + + Lemma fold1'_xelements': + forall A B (f: B -> A -> B) m i v l, + List.fold_left (fun a p => f a (snd p)) l (fold1' f m v) = + List.fold_left (fun a p => f a (snd p)) (xelements' m i l) v. Proof. - induction m; intros. - simpl. auto. - destruct o; simpl. - rewrite <- IHm1. simpl. rewrite <- IHm2. auto. + induction m; simpl; intros; auto. rewrite <- IHm1. rewrite <- IHm2. auto. + rewrite <- IHm. auto. + rewrite <- IHm1. simpl. rewrite <- IHm2. auto. Qed. Theorem fold1_spec: - forall (A B: Type) (f: B -> A -> B) (v: B) (m: t A), + forall A B (f: B -> A -> B) (v: B) (m: t A), fold1 f m v = List.fold_left (fun a p => f a (snd p)) (elements m) v. Proof. - intros. apply fold1_xelements with (l := @nil (positive * A)). + intros. destruct m as [|m]. reflexivity. + apply fold1'_xelements' with (l := @nil (positive * A)). Qed. + Arguments empty A : simpl never. + Arguments get {A} p m : simpl never. + Arguments set {A} p x m : simpl never. + Arguments remove {A} p m : simpl never. + End PTree. (** * An implementation of maps over type [positive] *) @@ -984,7 +1252,7 @@ Module PMap <: MAP. Theorem gi: forall (A: Type) (i: positive) (x: A), get i (init x) = x. Proof. - intros. unfold init. unfold get. simpl. rewrite PTree.gempty. auto. + intros. reflexivity. Qed. Theorem gss: @@ -1284,6 +1552,8 @@ Module ZTree := ITree(ZIndexed). (** * Additional properties over trees *) +Require Import Equivalence EquivDec. + Module Tree_Properties(T: TREE). (** Two induction principles over [fold]. *) -- cgit From a29b0c1bc26a6e2a37fa431e9347ed25c1bd1c2b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 16 Nov 2021 10:23:56 +0100 Subject: Maps.v: transparency of Node Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12 --- lib/Maps.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/Maps.v b/lib/Maps.v index f3330776..0d83aa98 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -692,7 +692,7 @@ Module PTree <: TREE. forall m1 m2, beq m1 m2 = true <-> (forall x, beq_optA (get x m1) (get x m2) = true). Proof. -Local Transparent Node. + Local Transparent Node. assert (beq_NN: forall l1 o1 r1 l2 o2 r2, not_trivially_empty l1 o1 r1 -> not_trivially_empty l2 o2 r2 -> @@ -836,6 +836,8 @@ Local Transparent Node. (fun l lrec o r rrec => Node lrec (match o with None => None | Some a => f a end) rrec) m. + Local Transparent Node. + Definition map_filter1 := Eval cbv [map_filter1_nonopt tree_rec tree_rec' Node] in @map_filter1_nonopt. -- cgit From 9c49dafbeb2c01304f3728df111bdf17441f81a7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 16 Nov 2021 16:43:33 +0100 Subject: First update for release 3.10 --- Changelog | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ VERSION | 2 +- doc/index.html | 2 +- 3 files changed, 57 insertions(+), 2 deletions(-) diff --git a/Changelog b/Changelog index d3a4cc4b..f10285c7 100644 --- a/Changelog +++ b/Changelog @@ -1,5 +1,60 @@ +Release 3.10, 2021-11-19 +======================== + +Major improvement: +- Bit fields in structs and unions are now handled in the + formally-verified part of CompCert. (Before, they were being + implemented through an unverified source-to-source translation.) + The CompCert C and Clight languages provide abstract syntax for + bit-field declarations and formal semantics for bit-field accesses. + The translation of bit-field accesses to bit manipulations is + performed in the Cshmgen pass and proved correct. + +Usability: +- The layout of bit-fields in memory now follows the ELF ABI + algorithm, improving ABI compatibility for the CompCert target + platforms that use ELF. +- Handle the `# 0` line directive generated by some C preprocessors (#398). +- Un-define the `__SIZEOF_INT128__` macro that is predefined by some C + preprocessors (#419). +- macOS assembler: use `##` instead of `#` to delimit comments (#399). + +ISO C conformance: +- Stricter checking of multi-character constants `'abc'`. + Multi-wide-character constants `L'ab'` are now rejected, + like GCC and Clang do. +- Ignore (but still warn about) unnamed plain members of structs + and unions (#411). +- Ignore unnamed bit fields when initializing unions. + +Bug fixing: +- x86 64 bits: overflow in offset of `leaq` instructions (#407). +- AArch64, ARM, PowerPC, RISC-V: wrong expansion of `__builtin_memcpy_aligned` + in some cases involving arguments that are stack addresses (#410, #412) +- PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask + instructions (`rldic`, `rldicl`, `rldicr`). +- RISC-V: update the Asm semantics to reflect the fact that + register X1 is destroyed by some builtins. + +Compiler internals: +- The "PTree" data structure (binary tries) was reimplemented, using + a canonical representation that guarantees extensionality and + improves performance. +- Add the ability to give formal semantics to numerical builtins + with small integer return types. +- PowerPC port: share code for memory accesses between Asmgen and Asmexpand +- Declare `__compcert_i64*` helper runtime functions during the C2C + pass, so that they are not visible during source elaboration. + +The clightgen tool: +- Add support for producing Csyntax abstract syntax instead of Clight + abstract syntax (option `-csyntax` to `clightgen`) (#404, #413). + Coq development: +- Added support for Coq 8.14 (#415). +- Added support for OCaml 4.13. - Updated the Flocq library to version 3.4.2. +- Replaced `Global Set Asymmetric Patterns` by more local settings (#408). Release 3.9, 2021-05-10 diff --git a/VERSION b/VERSION index 51212887..5f95604a 100644 --- a/VERSION +++ b/VERSION @@ -1,4 +1,4 @@ -version=3.9 +version=3.10 buildnr= tag= branch= diff --git a/doc/index.html b/doc/index.html index c3912cb2..857457cb 100644 --- a/doc/index.html +++ b/doc/index.html @@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }

The CompCert verified compiler

Commented Coq development

-

Version 3.9, 2021-05-10

+

Version 3.10, 2021-11-19

Introduction

-- cgit From 251df98b77d53143efb99e754fdb11d7c8ba286e Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 17 Nov 2021 13:11:26 +0100 Subject: Remove documentation of bitfield language support option. --- doc/ccomp.1 | 5 ----- 1 file changed, 5 deletions(-) diff --git a/doc/ccomp.1 b/doc/ccomp.1 index 89e8c823..3b1ec4ed 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -327,11 +327,6 @@ Language Support Options .INDENT 0.0 . .TP -.BR \-fbitfields ", " \-fno\-bitfields -Turn on/off support for emulation bit fields in structs. -Disabled by default. -. -.TP .BR \-flongdouble ", " \-fno\-longdouble Turn on/off support for emulation of \fBlong double\fP as \fBdouble\fP. Disabled by default. -- cgit From 2198a280b1150a61be1e514f044da03e69a66af9 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 17 Nov 2021 14:03:22 +0100 Subject: mention AArch64 in man-page --- doc/ccomp.1 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/ccomp.1 b/doc/ccomp.1 index 3b1ec4ed..edae57e1 100644 --- a/doc/ccomp.1 +++ b/doc/ccomp.1 @@ -9,7 +9,7 @@ ccomp \- the CompCert C compiler \fBCompCert C\fP is a compiler for the C programming language. Its intended use is the compilation of life-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. -It produces machine code for the PowerPC (32bit), ARM (32bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures. +It produces machine code for the PowerPC (32bit), ARM (32bit), AArch64 (ARM 64bit), x86 (32bit and 64bit), and RISC-V (32bit and 64bit) architectures. .PP What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program. -- cgit From fd2a2a8c8c2417b259e25a061c7fcfb6ee6f1848 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 19 Nov 2021 10:30:11 +0100 Subject: Second update for release 3.10 --- Changelog | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Changelog b/Changelog index f10285c7..94d85535 100644 --- a/Changelog +++ b/Changelog @@ -30,9 +30,10 @@ ISO C conformance: Bug fixing: - x86 64 bits: overflow in offset of `leaq` instructions (#407). - AArch64, ARM, PowerPC, RISC-V: wrong expansion of `__builtin_memcpy_aligned` - in some cases involving arguments that are stack addresses (#410, #412) + in cases involving arguments that are stack addresses (#410, #412) - PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask - instructions (`rldic`, `rldicl`, `rldicr`). + instructions (`rldic`, `rldicl`, `rldicr`), resulting in assertion + failures later in the compiler. - RISC-V: update the Asm semantics to reflect the fact that register X1 is destroyed by some builtins. @@ -42,13 +43,14 @@ Compiler internals: improves performance. - Add the ability to give formal semantics to numerical builtins with small integer return types. -- PowerPC port: share code for memory accesses between Asmgen and Asmexpand +- PowerPC: share code for memory accesses between Asmgen and Asmexpand - Declare `__compcert_i64*` helper runtime functions during the C2C pass, so that they are not visible during source elaboration. The clightgen tool: - Add support for producing Csyntax abstract syntax instead of Clight - abstract syntax (option `-csyntax` to `clightgen`) (#404, #413). + abstract syntax (option `-csyntax` to `clightgen`) + (contributed by Bart Jacobs; #404, #413). Coq development: - Added support for Coq 8.14 (#415). -- cgit From a79f0f99831aa0b0742bf7cce459cc9353bd7cd0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 26 Nov 2021 10:10:06 +0100 Subject: Support Coq 8.14.1 --- configure | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure b/configure index 7dfc6e30..3a4bc622 100755 --- a/configure +++ b/configure @@ -504,14 +504,14 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0) + 8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0|8.14.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.0" + echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.1" missingtools=true fi;; "") -- cgit