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 From 2f46b5c2420fec2d349a1ac192c8877d7737b72e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 Dec 2021 09:31:59 +0100 Subject: physical equality --- scheduling/BTL_SEimpl.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v index 0cbc46e6..9b48c7d2 100644 --- a/scheduling/BTL_SEimpl.v +++ b/scheduling/BTL_SEimpl.v @@ -1241,9 +1241,14 @@ Qed. Global Opaque option_eq_check. Hint Resolve option_eq_check_correct:wlp. -Import PTree. +Import PTree. Fixpoint PTree_eq_check' {A} (d1 d2: PTree.tree' A): ?? unit := + DO phy <~ phys_eq d1 d2;; + if phy + then + RET tt + else match d1, d2 with | Node001 r1, Node001 r2 => PTree_eq_check' r1 r2 | Node010 x1, Node010 x2 => -- cgit From 86fa4cc62f34f8fda7ea324c692101a97b4b8166 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 6 Dec 2021 15:30:13 +0100 Subject: update info on authors/papers --- README.md | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 3990048e..88e37055 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,7 @@ the [user's manual](https://compcert.org/man/). This is a special version with additions from Verimag and Kalray : * A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details. +* Scheduling passes for ARMv8 (aarch64) and RISC-V. * Some general-purpose optimization phases (e.g. profiling). * see [`PROFILING.md`](PROFILING.md) for details on the profiling system @@ -28,13 +29,24 @@ The people responsible for this version are * Sylvain Boulmé (Grenoble-INP, Verimag) * David Monniaux (CNRS, Verimag) * Cyril Six (Kalray) +* Léo Gourdin (UGA, Verimag) + +with contributions of: + +* Justus Fasse (M2R UGA, now at KU Leuven). +* Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon). ## Papers, docs, etc on this CompCert version * [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend (also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)). +* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). * [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux. -* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx) +* [Formally Verified Superblock Scheduling](https://hal.archives-ouvertes.fr/hal-03200774), a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino. +* [Optimized and formally-verified compilation for a VLIW processor](https://hal.archives-ouvertes.fr/tel-03326923), Phd Thesis of Cyril Six in 2021. +* [Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3](https://hal.archives-ouvertes.fr/tel-03356701), Habilitation Thesis of Sylvain Boulmé in 2021. +* [Code Transformations to Increase Prepass Scheduling Opportunities in CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf), MSc Thesis of Justus Fasse in 2021. +* [Register-Pressure-Aware Prepass-Scheduling for CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf), BSc Thesis of Nicolas Nardino in 2021. ## License CompCert is not free software. This non-commercial release can only -- cgit From 6ed58d0f7a800b3ce1ca815b7b348a9cbf7af0eb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 18:51:59 +0100 Subject: update the README and INSTALL documents --- INSTALL.md | 47 ++++++++++++++++++++++++++++++++++++++--------- README.md | 27 +++++++++++++++++++++------ 2 files changed, 59 insertions(+), 15 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index f072a211..5e2e800d 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -16,6 +16,7 @@ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install. ``` ## Post-install + Run ``` eval `opam config env` @@ -26,8 +27,8 @@ Add this to your `.bashrc` or `.bash_profile` ``` Switch to a recent OCaml compiler version ``` -opam switch create 4.09.0 -opam switch 4.09.0 +opam switch create 4.12.0 +opam switch 4.12.0 ``` Install dependencies available through opam ``` @@ -37,18 +38,20 @@ opam install coq menhir Note: it may happen that a newer version of Coq is not supported yet. You may downgrade to solve the problem: ``` -opam pin add coq 8.11.0 # example of Coq version +opam pin add coq 8.12.2 # example of Coq version ``` ## Compilation -Pre-compilation configure replace the placeholder with your desired platform -(for Kalray Coolidge it is `kvx-cos`) + +You can choose change the installation directory by modifying the +`config_simple.sh` file before running the configuration script. + +Then, use the configuration script corresponding to your desired platform: +(for Kalray Coolidge it is `config_kvx.sh`) ``` -./configure -prefix ~/.usr +./config_.sh ``` -`PREFIX` is where CompCert will be installed after `make install` - If using Kalray's platform, make sure that the kvx tools are on your path Compile (adapt -j# to the number of cores and available RAM) ``` @@ -56,8 +59,22 @@ make -j12 make install ``` +## Tests + +## Documentation + +You can generate the documentation locally with: +``` +make documentation +``` + +Note that you need to install [coq2html](https://github.com/xavierleroy/coq2html) +before doing so. + ## Utilization -`ccomp` binaries are installed at `$(PREFIX)/bin` + +`ccomp` binaries are installed at `$(CCOMP_INSTALL_PREFIX)/bin` +(variable defined in `config_simple.sh`). Make sure to add that to your path to ease its use Now you may use it like a regular compiler ``` @@ -66,9 +83,21 @@ ccomp -O3 test.c -o test.bin ``` ## Changing platform + If you decide to change the platform, for instance from kvx-cos to kvx-mbr, you should change the `compcert.ini` file with the respective tools and then run ``` make install ``` +## Cleaning + +To clean only object files while keeping the platform configuration: +``` +make clean +``` + +To clean everything (to then reconfigure for another platform): +``` +make distclean +``` diff --git a/README.md b/README.md index 88e37055..4912eb3d 100644 --- a/README.md +++ b/README.md @@ -17,12 +17,22 @@ refer to the [Web site](https://compcert.org/) and especially the [user's manual](https://compcert.org/man/). ## Verimag-Kalray version + This is a special version with additions from Verimag and Kalray : -* A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details. -* Scheduling passes for ARMv8 (aarch64) and RISC-V. -* Some general-purpose optimization phases (e.g. profiling). - * see [`PROFILING.md`](PROFILING.md) for details on the profiling system +* A backend for the Coolidge VLIW KVX processor. +* Postpass scheduling passes for KVX, ARMv8 (aarch64) and RISC-V along with a + preprocessing peephole optimizer. +* Improved subexpression elimination: two passes CSE2 and CSE3. Both go through + loops and feature a small alias analysis. +* A generic prepass scheduling optimizer with a multi-purpose preprocessing + front-end: rewritings, register renaming, if-lifting and some generic code + transformations such as loop-rotation, loop-unrolling, or tail-duplication. +* A profiling system: see [`PROFILING.md`](PROFILING.md) for details. +* Static branch prediction. +* And some experimental features that are work in progress. + +_Please refer to the resources listed below for more information._ The people responsible for this version are @@ -36,17 +46,22 @@ with contributions of: * Justus Fasse (M2R UGA, now at KU Leuven). * Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon). +## Installing + +Please follow the instructions in `INSTALL.md` + ## Papers, docs, etc on this CompCert version -* [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend +* [The documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). +* [A 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend (also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)). -* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). * [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux. * [Formally Verified Superblock Scheduling](https://hal.archives-ouvertes.fr/hal-03200774), a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino. * [Optimized and formally-verified compilation for a VLIW processor](https://hal.archives-ouvertes.fr/tel-03326923), Phd Thesis of Cyril Six in 2021. * [Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3](https://hal.archives-ouvertes.fr/tel-03356701), Habilitation Thesis of Sylvain Boulmé in 2021. * [Code Transformations to Increase Prepass Scheduling Opportunities in CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf), MSc Thesis of Justus Fasse in 2021. * [Register-Pressure-Aware Prepass-Scheduling for CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf), BSc Thesis of Nicolas Nardino in 2021. +* [Formally verified postpass scheduling with peephole optimization for AArch64](https://www.lirmm.fr/afadl2021/papers/afadl2021_paper_9.pdf), a short AFADL'21 paper, by Gourdin. ## License CompCert is not free software. This non-commercial release can only -- cgit From 47cdb65b2290df66690d34d6a09745fb364ef392 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 18:53:24 +0100 Subject: install link --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4912eb3d..6406cd27 100644 --- a/README.md +++ b/README.md @@ -48,7 +48,7 @@ with contributions of: ## Installing -Please follow the instructions in `INSTALL.md` +Please follow the instructions in [`INSTALL.md`](INSTALL.md) ## Papers, docs, etc on this CompCert version -- cgit From 820e1ecbca864982ebc7b8efc453d057e374a4f7 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 21:34:46 +0100 Subject: [Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6 starting a new index-verimag.html on BTL doc --- .gitlab-ci.yml | 4 +- doc/index-verimag.html | 395 ++++++++++++++++++++++++++++++++++++++++++++++ scheduling/BTL_SEtheory.v | 52 +++--- 3 files changed, 423 insertions(+), 28 deletions(-) create mode 100644 doc/index-verimag.html diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9534282d..2f0d598d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -317,8 +317,8 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil - source /opt/kalray/accesscore/kalray.sh && make documentation - mkdir public - cp -r doc/* public/ - - tools/fix_html_date.sh doc/index-kvx.html " (" ")" > public/index.html - - rm public/index-kvx.html + - tools/fix_html_date.sh doc/index-verimag.html " (" ")" > public/index.html + - rm public/index-verimag.html artifacts: paths: - public diff --git a/doc/index-verimag.html b/doc/index-verimag.html new file mode 100644 index 00000000..242fa1cd --- /dev/null +++ b/doc/index-verimag.html @@ -0,0 +1,395 @@ + + + +The CompCert verified compiler + + + + + + + +

The CompCert verified compiler

+

Commented Coq development

+

Version 3.9, 2021-05-10

+ +

VERIMAG fork version 2021-29-10

+ +

The CompCert Verimag's fork

+

This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. + The unmodified parts of this table appear in gray. +
+
+ A high-level view of this CompCert backend is provided by the following documents: +

+

+ +

Introduction

+ + +

CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly +code from CompCert C, a large subset of the C programming language. +The particularity of this compiler is that it is written mostly within +the specification language of the Coq proof assistant, and its +correctness --- the fact that the generated assembly code is +semantically equivalent to its source program --- was entirely proved +within the Coq proof assistant.

+ +

High-level descriptions of the CompCert compiler and its proof of +correctness can be found in the following papers (in increasing order of technical details):

+ + +

This Web site gives a commented listing of the underlying Coq +specifications and proofs. Proof scripts are folded by default, but +can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the five target architectures. The +PowerPC versions of these modules are shown below; the AArch64, ARM, +x86 and RISC-V versions can be found in the source distribution. +

+ +

This development is a work in progress; some parts have +substantially changed since the overview papers above were +written.

+ +

The complete sources for CompCert can be downloaded from +the Git repository +or the CompCert Web site. +

+ +

This document and the CompCert sources are copyright Institut +National de Recherche en Informatique et en Automatique (INRIA) and +AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the +following license. +

+ + +

Table of contents

+ + +

General-purpose libraries, data structures and algorithms

+ +
    +
  • Coqlib: addendum to the Coq standard library. +
  • Maps: finite maps. +
  • Integers: machine integers. +
  • Floats: machine floating-point numbers. +
  • Iteration: various forms of "while" loops. +
  • Ordered: construction of +ordered types. +
  • Lattice: construction of +semi-lattices. +
  • Kildall: resolution of dataflow +inequations by fixpoint iteration. +
  • UnionFind: a persistent union-find data structure. +
  • Postorder: postorder numbering of a directed graph. +
 + +

The Impure library (of Boulmé)

+
    +
  • ImpConfig: declares the Impure monad and defines its extraction.
    • +
  • ImpCore: defines notations for the Impure monad and a wlp_simplify tactic (to reason about Impure functions in a Hoare-logic style).
    • +
  • ImpLoops, ImpIO, ImpHCons: declare Impure oracles and define operators from these oracles. ImpExtern exports all these impure operators.
    • +
  • ImpMonads: axioms of "impure computations" and some Coq models of these axioms.
    • +
  • ImpPrelude: declares the data types exchanged with Impure oracles.
    • +
+ +

The abstractbb library, introduced for Aarch64 and KVX cores

+This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends. +
    +
  • AbstractBasicBlocksDef: an IR for verifying some semantic properties on basic-blocks. +
  • Parallelizability: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. +
  • ImpSimuTest: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines SeqSimuTheory with hash-consing and uses the Impure library to reason on physical equality and handling of imperative code in Coq. +
+

Definitions and theorems used in many parts of the development

+ +
    +
  • Errors: the Error monad. +
  • AST: identifiers, whole programs and other +common elements of abstract syntaxes. +
  • Linking: generic framework to define syntactic linking over the CompCert languages. +
  • Values: run-time values. +
  • Events: observable events and traces. +
  • Memory: memory model.
    +See also: Memdata (in-memory representation of data). +
  • Globalenvs: global execution environments. +
  • Smallstep: tools for small-step semantics. +
  • Behaviors: from small-step semantics to observable behaviors of programs. +
  • Determinism: determinism properties of small-step semantics. +
  • Op: operators, addressing modes and their +semantics. +
  • Builtins: semantics of built-in functions.
    +See also: Builtins0 (target-independent part), Builtins1 (target-dependent part). +
  • Unityping: a solver for atomic unification constraints. +
+ +

Source, intermediate and target languages: syntax and semantics

+ +
    +
  • The CompCert C source language: +syntax and +semantics and +determinized semantics and +type system.
    +See also: type expressions and +operators (syntax and semantics).
    +See also: reference interpreter. +
  • Clight: a simpler version of CompCert C where expressions contain no side-effects. +
  • Csharpminor: low-level + structured language. +
  • Cminor: low-level structured +language, with explicit stack allocation of certain local variables. +
  • CminorSel: like Cminor, +with machine-specific operators and addressing modes. +
  • RTL: register transfer language (3-address +code, control-flow graph, infinitely many pseudo-registers).
    +See also: Registers (representation of +pseudo-registers). +
  • LTL: location transfer language (3-address +code, control-flow graph of basic blocks, finitely many physical registers, infinitely +many stack slots).
    +See also: Locations (representation of +locations) and Machregs (description of processor registers). +
  • Linear: like LTL, but the CFG is +replaced by a linear list of instructions with explicit branches and labels. +
  • Mach: like Linear, with a more concrete +view of the activation record. +
  • Asm: abstract syntax for PowerPC assembly +code. +
+ +

Compiler passes

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
PassSource & targetCompiler codeCorrectness proof
Pulling side-effects out of expressions;
+ fixing an evaluation order		CompCert C to ClightSimplExprSimplExprspec
+ SimplExprproof
Pulling non-adressable scalar local variables out of memoryClight to ClightSimplLocalsSimplLocalsproof
Simplification of control structures;
+ explication of type-dependent computations		Clight to CsharpminorCshmgenCshmgenproof
Stack allocation of local variables
+ whose address is taken;
+ simplification of switch statements		Csharpminor to CminorCminorgenCminorgenproof
Recognition of operators
and addressing modes;
+ if-conversion		Cminor to CminorSelSelection
+ SelectOp
+ SelectLong
+ SelectDiv
+ SplitLong		Selectionproof
+ SelectOpproof
+ SelectLongproof
+ SelectDivproof
+ SplitLongproof
Construction of the CFG,
3-address code generation		CminorSel to RTLRTLgenRTLgenspec
+ RTLgenproof
Recognition of tail callsRTL to RTLTailcallTailcallproof
Function inliningRTL to RTLInliningInliningspec
+ Inliningproof
Postorder renumbering of the CFGRTL to RTLRenumberRenumberproof
Constant propagationRTL to RTLConstprop
+ ConstpropOp		Constpropproof
+ ConstproppOproof
Common subexpression eliminationRTL to RTLCSE
+ CombineOp		CSEproof
+ CombineOpproof
Redundancy eliminationRTL to RTLDeadcodeDeadcodeproof
Removal of unused static globalsRTL to RTLUnusedglobUnusedglobproof
Register allocation (validation a posteriori)RTL to LTLAllocationAllocproof
Branch tunnelingLTL to LTLTunnelingTunnelingproof
Linearization of the CFGLTL to LinearLinearizeLinearizeproof
Removal of unreferenced labelsLinear to LinearCleanupLabelsCleanupLabelsproof
Synthesis of debugging informationLinear to LinearDebugvarDebugvarproof
Laying out the activation recordsLinear to MachStacking
+ Bounds
+ Stacklayout		Stackingproof
+ Separation
Emission of assembly codeMach to AsmAsmgenAsmgenproof0
+ Asmgenproof1
+ Asmgenproof
+ +

All together (there are many more passes than on vanilla CompCert: their order is specified in Compiler)

+ +
    +
  • Compiler: composing the passes together; +whole-compiler semantic preservation theorems. + +
  • Complements: interesting consequences of the semantic preservation theorems. +
+ +

Static analyses

+ +The following static analyses are performed over the RTL intermediate +representation to support optimizations such as constant propagation, +CSE, and dead code elimination. +
    +
  • Liveness: liveness analysis. +
  • ValueAnalysis: value and alias analysis
    +See also: ValueDomain: the abstract domain for value analysis.
    +See also: ValueAOp: processor-dependent parts of value analysis. +
  • Deadcode: neededness analysis
    +See also: NeedDomain: the abstract domain for neededness analysis.
    +See also: NeedOp: processor-dependent parts of neededness analysis. +
+ +

Type systems

+ +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. +
    +
  • Ctyping: typing for CompCert C + type-checking functions. +
  • RTLtyping: typing for RTL + type +reconstruction. +
  • Lineartyping: typing for Linear. +
+ + + + diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 55afc19a..b0765f09 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -122,9 +122,9 @@ with eval_smem ctx (sm: smem): option mem := (** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block - (their semantics only depends on the initial memory of the block). + (their semantics only depends on the initial memory of the block). - The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. + The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. *) Lemma valid_pointer_preserv ctx sm: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. @@ -308,31 +308,31 @@ Proof. Qed. Lemma eval_builtin_sval_arg ctx bs: - forall ba m v, - eval_builtin_sval ctx bs = Some ba -> - eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> - eval_builtin_sarg ctx m bs v. + forall ba m v, + eval_builtin_sval ctx bs = Some ba -> + eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> + eval_builtin_sarg ctx m bs v. Proof. - induction bs; simpl; - try (intros ba m v H; inversion H; subst; clear H; - intros H; inversion H; subst; - econstructor; auto; fail). - - intros ba m v; destruct (eval_sval _ _) eqn: SV; - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; auto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. - - intros ba m v. - destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. - destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. - intros H; inversion H; subst; clear H. - intros H; inversion H; subst. - econstructor; eauto. + induction bs; simpl; + try (intros ba m v H; inversion H; subst; clear H; + intros H; inversion H; subst; + econstructor; auto; fail). + - intros ba m v; destruct (eval_sval _ _) eqn: SV; + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; auto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. + - intros ba m v. + destruct (eval_builtin_sval _ bs1) eqn: SV1; try congruence. + destruct (eval_builtin_sval _ bs2) eqn: SV2; try congruence. + intros H; inversion H; subst; clear H. + intros H; inversion H; subst. + econstructor; eauto. Qed. Lemma eval_builtin_sarg_sval ctx m v: forall bs, -- cgit From edc7505f0b1b617cda01648316ea02b58d268411 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 23:15:51 +0100 Subject: improvement in html doc (not finished yet) --- doc/index-verimag.html | 167 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 145 insertions(+), 22 deletions(-) diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 242fa1cd..1eb857d9 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -26,7 +26,7 @@ a:active {color : Red; text-decoration : underline; }

Commented Coq development

Version 3.9, 2021-05-10

-

VERIMAG fork version 2021-29-10

+

VERIMAG fork version 2021-29-10

The CompCert Verimag's fork

This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. @@ -34,18 +34,37 @@ a:active {color : Red; text-decoration : underline; }

A high-level view of this CompCert backend is provided by the following documents: + +

+ +

The people responsible for this version are

+ +
    +
  • Sylvain Boulmé (Grenoble-INP, Verimag)
    • +
  • David Monniaux (CNRS, Verimag)
    • +
  • Cyril Six (Kalray)
    • +
  • Léo Gourdin (UGA, Verimag)
    • +
+ + +

with contributions of:

+ +

Introduction

@@ -120,13 +139,15 @@ inequations by fixpoint iteration.
  • ImpPrelude: declares the data types exchanged with Impure oracles.
    • -

    The abstractbb library, introduced for Aarch64 and KVX cores

    +

    The abstractbb library, introduced for Aarch64 and KVX cores

    This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends.
    • AbstractBasicBlocksDef: an IR for verifying some semantic properties on basic-blocks.
    • Parallelizability: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
    • ImpSimuTest: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines SeqSimuTheory with hash-consing and uses the Impure library to reason on physical equality and handling of imperative code in Coq.
    + +

    Definitions and theorems used in many parts of the development

      @@ -182,11 +203,31 @@ replaced by a linear list of instructions with explicit branches and labels. view of the activation record.
    • Asm: abstract syntax for PowerPC assembly code. + + +

      Languages introduced in the VERIMAG version

      + +Generic (or possibly adaptable) Intermediate Representations (IR): +
        +
      • BTL: an IR dedicated to defensive certification of middle-end optimizations (before register allocation). + BTL stands for "Block Transfer Language". +
      • Machblock: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). + This IR is generic over the processor and used for KVX and Aarch64. +
      • Asmblock: a variant of Asm, with a big-step semantics of basic-blocks. + This IR is an intermediate step between Machblock and Asm on backends featuring postpass scheduling (KVX and Aarch64). +
      • AbstractBasicBlocks: the AbstractBasicBlocks Domain Specific Language (DSL) used in the postpass scheduling verification. + This DSL is only used as a library on KVX and Aarch64. +
      + +Specific to KVX: +
        +
      • Asmvliw: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. +
      • kvx/Asm: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of Asmvliw for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).

      Compiler passes

      - +
      @@ -301,6 +342,60 @@ code. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -311,8 +406,8 @@ code. - - + + @@ -346,22 +441,50 @@ code. Separation - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + - +
      Pass Source & targetUnusedglobproof
      Passes introduced for profiling (for later use in trace selection)
      Insert profiling annotations (for recording experiments -- see PROFILE.md). + RTL to RTLProfilingProfilingproof
      Update ICond nodes (from recorded experiments -- see PROFILE.md). + RTL to RTLProfilingExploitProfilingExploitproof
      Passes introduced for superblock prepass scheduling
      Code duplications (trace selection, loop unrollings, etc) + RTL to RTLDuplicate (generic checker)Duplicateproof (generic proof)
      + Duplicatepasses (several passes from several oracles)
      Superblock selection (with Liveness information)RTL to RTLPathRTLpathLivegenRTLpathLivegenproof
      Superblock prepass schedulingRTLPath to RTLPathRTLpathSchedulerRTLpathSchedulerproof
      + with RTLpathSE_theory (the theory of symbolic execution on RTLpath)
      + and RTLpathSE_simu_specs (the low-level specifications of the simulation checker)
      + and RTLpathSE_impl (the simulation checker with hash-consing)
      Forgeting superblocksRTLPath to RTLRTLpath.transf_programRTLpathproof
      Passes from register allocation
      Register allocation (validation a posteriori) RTL to LTL
      Branch tunneling LTL to LTLTunnelingTunnelingproofLTLTunnelingLTLTunnelingproof
      Emission of assembly codeMach to Asm
      Passes introduced for KVX VLIW
      Reconstruction of basic-blocks at Mach levelMach to MachblockMachblockgenForwardSimulationBlock
      + Machblockgenproof
      Emission of purely sequential assembly codeMachblock to AsmblockAsmblockgenAsmblockgenproof0
      + Asmblockgenproof1
      + Asmblockgenproof
      Bundling (and basic-block scheduling)Asmblock to AsmvliwPostpassScheduling
      + using Asmblockdeps
      + and the abstractbb library      		PostpassSchedulingproof
      Flattening bundles (only a bureaucratic operation)Asmvliw to Asm AsmgenAsmgenproof0
      - Asmgenproof1
      - Asmgenproof      		Asmgenproof (whole simulation proof from Mach to Asm)

      All together (there are many more passes than on vanilla CompCert: their order is specified in Compiler)

      + +
      • Compiler: composing the passes together; whole-compiler semantic preservation theorems. -
      • Complements: interesting consequences of the semantic preservation theorems.
      -- cgit From 7ebac668dfbe050688590bfbc1aaa910ebd4f652 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 23:22:34 +0100 Subject: improve doc CI --- .gitlab-ci.yml | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 2f0d598d..728bd3c3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -311,14 +311,19 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil - opam repo add coq-released https://coq.inria.fr/opam/released - opam install coq-coq2html script: + - mkdir public - source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" - make -j "$NJOBS" clightgen - source /opt/kalray/accesscore/kalray.sh && make documentation - - mkdir public - - cp -r doc/* public/ - - tools/fix_html_date.sh doc/index-verimag.html " (" ")" > public/index.html - - rm public/index-verimag.html + - cp -rf doc/* public/ + - make distclean + - ./config_aarch64.sh + - make -j "$NJOBS" + - make -j "$NJOBS" clightgen + - make documentation + - cp -rf doc/* public/ + - mv doc/index-verimag.html public/index.html artifacts: paths: - public -- cgit From 9370eee7cdbe07888aa749f4f9153c1cab3bff56 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 23:30:23 +0100 Subject: fix --- .gitlab-ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 728bd3c3..b200eba6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -330,6 +330,7 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil rules: - if: '$CI_COMMIT_BRANCH == "master"' when: always + - when: manual build_aarch64_coq13: stage: build -- cgit From dac0aadbb00447f4bbfe40586d32ccffe6703222 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 23:32:46 +0100 Subject: Revert "fix" This reverts commit 9370eee7cdbe07888aa749f4f9153c1cab3bff56. --- .gitlab-ci.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b200eba6..728bd3c3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -330,7 +330,6 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil rules: - if: '$CI_COMMIT_BRANCH == "master"' when: always - - when: manual build_aarch64_coq13: stage: build -- cgit From 2ed836d9fd798c17b0858468bda07bfa70dc9e43 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 7 Dec 2021 11:49:31 +0100 Subject: doc --- .gitlab-ci.yml | 5 - doc/index-verimag.html | 263 ++++++++++++++++++++++++++++++++++++++++++------- 2 files changed, 226 insertions(+), 42 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 728bd3c3..d44c881c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -316,11 +316,6 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" - make -j "$NJOBS" clightgen - source /opt/kalray/accesscore/kalray.sh && make documentation - - cp -rf doc/* public/ - - make distclean - - ./config_aarch64.sh - - make -j "$NJOBS" - - make -j "$NJOBS" clightgen - make documentation - cp -rf doc/* public/ - mv doc/index-verimag.html public/index.html diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 1eb857d9..56b16991 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -24,9 +24,9 @@ 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

       -

      VERIMAG fork version 2021-29-10

      +

      VERIMAG fork version 2021-12-07

      The CompCert Verimag's fork

      This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. @@ -304,8 +304,97 @@ Specific to KVX: Inliningproof + + Passes introduced for profiling (for later use in trace selection) + + + Insert profiling annotations (for recording experiments -- see PROFILE.md). + + RTL to RTL + Profiling + Profilingproof + + + Update ICond nodes (from recorded experiments -- see PROFILE.md). + + RTL to RTL + ProfilingExploit + ProfilingExploitproof + + + + FirstNop: Inserting a no-op instruction at each RTL function entrypoint + RTL to RTL + FirstNop + FirstNopproof + + - Postorder renumbering of the CFG + Postorder renumbering of the CFG (1) + RTL to RTL + Renumber + Renumberproof + + + + [CSE1] Common subexpression elimination (1) + RTL to RTL + CSE
      + CombineOp + CSEproof
      + CombineOpproof + + + + [Duplicate pass] Static Prediction + Unroll single + + Add static prediction information to Icond nodes
      + Unrolls a single iteration of innermost loops + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
      + Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (2) + RTL to RTL + Renumber + Renumberproof + + + + [Duplicate pass] Tail Duplication + + Performs tail duplication on interesting traces to form superblocks + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
      + Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (3) + RTL to RTL + Renumber + Renumberproof + + + + [Duplicate pass] Unroll body + + Unrolling the body of innermost loops + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
      + Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (4) RTL to RTL Renumber Renumberproof @@ -321,7 +410,14 @@ Specific to KVX: - Common subexpression elimination + Postorder renumbering of the CFG (5) + RTL to RTL + Renumber + Renumberproof + + + + [CSE1] Common subexpression elimination (1) RTL to RTL CSE
      CombineOp @@ -329,67 +425,159 @@ Specific to KVX: CombineOpproof + + [CSE2] Common subexpression elimination + RTL to RTL + CSE2
      + + CSE2proof
      + + + + + [CSE3] Common subexpression elimination (1) + RTL to RTL + CSE3
      + + CSE3proof
      + + + + + KillUselessMoves: removing useless moves instructions after CSE3 + RTL to RTL + KillUselessMoves
      + + KillUselessMovesproof
      + + + + + Forwarding Moves + RTL to RTL + ForwardMoves
      + + ForwardMovesproof
      + + + - Redundancy elimination + Redundancy elimination (1) RTL to RTL Deadcode Deadcodeproof + + + RTL Tunneling + RTL to RTL + RTLTunneling
      + + RTLTunnelingproof
      + + + - Removal of unused static globals + Postorder renumbering of the CFG (6) RTL to RTL - Unusedglob - Unusedglobproof + Renumber + Renumberproof - Passes introduced for profiling (for later use in trace selection) - + [Duplicate pass] Loop Rotate - Insert profiling annotations (for recording experiments -- see PROFILE.md). + Loop rotation RTL to RTL - Profiling - Profilingproof + Duplicate (generic checker) + Duplicateproof (generic proof)
      + Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (7) + RTL to RTL + Renumber + Renumberproof + - Update ICond nodes (from recorded experiments -- see PROFILE.md). + Loop Invariant Code Motion RTL to RTL - ProfilingExploit - ProfilingExploitproof + LICM + LICMproof + + + + Postorder renumbering of the CFG (8) + RTL to RTL + Renumber + Renumberproof + + - Passes introduced for superblock prepass scheduling + [CSE3] Common subexpression elimination (2) + RTL to RTL + CSE3
      + + CSE3proof
      + + + + + Redundancy elimination (2) + RTL to RTL + Deadcode + Deadcodeproof + - Code duplications (trace selection, loop unrollings, etc) + Allnontrap: transforming loads to non-trapping ones + RTL to RTL + Allnontrap
      + Allnontrapproof
      + + + + + Removal of unused static globals RTL to RTL - Duplicate (generic checker) - Duplicateproof (generic proof)
      - Duplicatepasses (several passes from several oracles) + Unusedglob + Unusedglobproof + - Superblock selection (with Liveness information) - RTL to RTLPath - RTLpathLivegen - RTLpathLivegenproof + Passes introduced for BTL + + + Block selection (with Liveness information) + RTL to BTL + RTLtoBTL + RTLtoBTLproof
      + BTLmatchRTL
      + BTL_Livecheck + Superblock prepass scheduling - RTLPath to RTLPath - RTLpathScheduler - RTLpathSchedulerproof
      - with RTLpathSE_theory (the theory of symbolic execution on RTLpath)
      - and RTLpathSE_simu_specs (the low-level specifications of the simulation checker)
      - and RTLpathSE_impl (the simulation checker with hash-consing) + BTL to BTL + BTL_Scheduler + BTL_Schedulerproof
      + with BTL_SEtheory (the theory of symbolic execution on BTL_)
      + and BTL_SEsimuref (the low-level specifications of the simulation checker)
      + and BTL_SEimpl (the simulation checker with hash-consing) - Forgeting superblocks - RTLPath to RTL - RTLpath.transf_program - RTLpathproof + Forgeting blocks + BTL to RTL + BTLtoRTL + BTLtoRTLproof
      + BTLmatchRTL + @@ -442,7 +630,7 @@ Specific to KVX: - Passes introduced for KVX VLIW + Passes introduced for backends with postpass scheduling Reconstruction of basic-blocks at Mach level @@ -467,7 +655,8 @@ Specific to KVX: PostpassScheduling
      using Asmblockdeps
      and the abstractbb library - PostpassSchedulingproof + PostpassSchedulingproof
      + Asmblockprops -- cgit From 97893db9b4199d93d22c3975de2ef711b1cf4d68 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 7 Dec 2021 14:08:06 +0100 Subject: ci fix for pages? --- .gitlab-ci.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d44c881c..c8ccedb8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -302,7 +302,7 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil - sudo apt-get -o Acquire::Check-Valid-Until=false -o Acquire::Check-Date=false update - sudo apt-get -y install sshpass openssh-client libzip4 lttng-tools liblttng-ctl-dev liblttng-ust-dev babeltrace - ./.download_from_Kalray.sh - - rm -f download/*dkms*.deb download/*eclipse*.deb download/*llvm*.deb download/*board-mgmt* download/*oce-host* download/*pocl* download/*flash-util* download/*barebox* + - (cd download ; rm -f *dkms*.deb *eclipse*.deb *llvm*.deb *board-mgmt* *oce-host* *pocl* *flash-util* *barebox* *-kann-* *-kaf-* *-stb-* *-opencv* *-eigen* *-task* *-blis* *-lz4*) - sudo dpkg -i download/*.deb - rm -rf download - eval `opam config env` @@ -316,7 +316,6 @@ pages: # TODO: change to "deploy" when "build" succeeds (or integrate with "buil - source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" - make -j "$NJOBS" clightgen - source /opt/kalray/accesscore/kalray.sh && make documentation - - make documentation - cp -rf doc/* public/ - mv doc/index-verimag.html public/index.html artifacts: -- cgit From 5d1cda3081d6dbf7a39548bfea376c2ea24531b3 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 8 Dec 2021 13:37:58 +0100 Subject: LICENSE --- doc/index-verimag.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 56b16991..4ca4a7bc 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -105,7 +105,7 @@ or the CompCert Web site.

      This document and the CompCert sources are copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the -following license. +following license.

      -- cgit From 89562c917e61c56a167ba13b86021b286cb7e257 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 8 Dec 2021 13:59:00 +0100 Subject: Allocproof link --- doc/index-verimag.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 4ca4a7bc..daed4d6d 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -588,7 +588,7 @@ Specific to KVX: Register allocation (validation a posteriori) RTL to LTL Allocation - Allocproof + Allocationproof -- cgit