From ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 19 Nov 2009 13:32:09 +0000 Subject: Revised lib/Integers.v to make it parametric w.r.t. word size. Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 2 -- powerpc/Asmgenproof1.v | 14 +++++++------- powerpc/ConstpropOp.v | 28 ++++++++++++++-------------- powerpc/ConstpropOpproof.v | 26 +++++++++++++------------- powerpc/Op.v | 40 ++++++++++++++++++++-------------------- powerpc/SelectOp.v | 8 ++++---- powerpc/SelectOpproof.v | 20 ++++++++------------ 7 files changed, 66 insertions(+), 72 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 1582b414..60c3d34d 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -302,9 +302,7 @@ lbl: .long 0x43300000, 0x00000000 lwz r12, lo16(lbl)(r12) mtctr r12 bctr r12 - .const_data lbl: .long table[0], table[1], ... - .text >> Note that [reg] contains 4 times the index of the desired table entry. *) diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 3baeb795..7329e539 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -48,13 +48,13 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat wordsize))) + (Int.repr (Z_of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib. exact (Int.and_mone n). - reflexivity. reflexivity. + apply int_wordsize_divides_modulus. reflexivity. reflexivity. Qed. Lemma low_high_u_xor: @@ -63,13 +63,13 @@ Proof. intros. unfold high_u, low_u. rewrite Int.shl_rolm. rewrite Int.shru_rolm. rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16)) + change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16)) (Int.repr 16)) - (Int.repr (Z_of_nat wordsize))) + (Int.repr (Z_of_nat Int.wordsize))) with (Int.zero). rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib. exact (Int.and_mone n). - reflexivity. reflexivity. + apply int_wordsize_divides_modulus. reflexivity. reflexivity. Qed. Lemma low_high_s: @@ -91,7 +91,7 @@ Proof. unfold Int.sub. assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0). intros a b [k EQ] H1. rewrite EQ. - change modulus with (65536 * 65536). + change Int.modulus with (65536 * 65536). rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto. omega. eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. diff --git a/powerpc/ConstpropOp.v b/powerpc/ConstpropOp.v index 87b2cfa4..ededce07 100644 --- a/powerpc/ConstpropOp.v +++ b/powerpc/ConstpropOp.v @@ -166,11 +166,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | Onand, I n1 :: I n2 :: nil => I(Int.xor (Int.and n1 n2) Int.mone) | Onor, I n1 :: I n2 :: nil => I(Int.xor (Int.or n1 n2) Int.mone) | Onxor, I n1 :: I n2 :: nil => I(Int.xor (Int.xor n1 n2) Int.mone) - | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown - | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown - | Oshrimm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown - | Oshrximm n, I n1 :: nil => if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown - | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown + | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown + | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown + | Oshrimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown + | Oshrximm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown + | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown | Orolm amount mask, I n1 :: nil => I(Int.rolm n1 amount mask) | Onegf, F n1 :: nil => F(Float.neg n1) | Oabsf, F n1 :: nil => F(Float.abs n1) @@ -500,15 +500,15 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | eval_static_operation_case28 n1 n2 => I(Int.xor (Int.xor n1 n2) Int.mone) | eval_static_operation_case29 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown | eval_static_operation_case30 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown | eval_static_operation_case31 n n1 => - if Int.ltu n (Int.repr 32) then I(Int.shr n1 n) else Unknown + if Int.ltu n Int.iwordsize then I(Int.shr n1 n) else Unknown | eval_static_operation_case32 n n1 => - if Int.ltu n (Int.repr 32) then I(Int.shrx n1 n) else Unknown + if Int.ltu n Int.iwordsize then I(Int.shrx n1 n) else Unknown | eval_static_operation_case33 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown | eval_static_operation_case34 amount mask n1 => I(Int.rolm n1 amount mask) | eval_static_operation_case35 n1 => @@ -628,7 +628,7 @@ Definition make_shrimm (n: int) (r: reg) := Definition make_shruimm (n: int) (r: reg) := if Int.eq n Int.zero then (Omove, r :: nil) - else (Orolm (Int.sub (Int.repr 32) n) (Int.shru Int.mone n), r :: nil). + else (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r :: nil). Definition make_mulimm (n: int) (r: reg) := if Int.eq n Int.zero then @@ -789,7 +789,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case9 r1 r2 => (* Oshl *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shlimm n r1 else (op, args) | _ => (op, args) @@ -797,7 +797,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case10 r1 r2 => (* Oshr *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shrimm n r1 else (op, args) | _ => (op, args) @@ -805,7 +805,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case11 r1 r2 => (* Oshru *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shruimm n r1 else (op, args) | _ => (op, args) diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 0c7be7bd..2e28d23f 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -130,19 +130,19 @@ Proof. subst v. unfold Int.not. congruence. subst v. unfold Int.not. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - destruct (Int.ltu n (Int.repr 32)). + destruct (Int.ltu n Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. - destruct (Int.ltu n (Int.repr 32)). + destruct (Int.ltu n Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. @@ -229,7 +229,7 @@ Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. subst n. simpl in *. FuncInv. rewrite Int.shl_zero in H. congruence. - simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros. + simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros. rewrite H1 in H0. rewrite Int.shl_rolm in H0. auto. exact H1. rewrite H1 in H0. discriminate. Qed. @@ -255,7 +255,7 @@ Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. subst n. simpl in *. FuncInv. rewrite Int.shru_zero in H. congruence. - simpl in *. FuncInv. caseEq (Int.ltu n (Int.repr 32)); intros. + simpl in *. FuncInv. caseEq (Int.ltu n Int.iwordsize); intros. rewrite H1 in H0. rewrite Int.shru_rolm in H0. auto. exact H1. rewrite H1 in H0. discriminate. Qed. @@ -276,7 +276,7 @@ Proof. with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H1). - change (Z_of_nat wordsize) with 32. intro. rewrite H2. + change (Z_of_nat Int.wordsize) with 32. intro. rewrite H2. destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H1). auto. exact H2. Qed. @@ -364,7 +364,7 @@ Proof. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H) in H1. simpl in *; FuncInv. destruct (Int.eq i Int.zero). congruence. - change 32 with (Z_of_nat wordsize). + change 32 with (Z_of_nat Int.wordsize). rewrite (Int.is_power2_range _ _ H0). rewrite (Int.divs_pow2 i1 _ _ H0) in H1. auto. assumption. @@ -377,7 +377,7 @@ Proof. with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). apply make_shruimm_correct. simpl. destruct rs#r1; auto. - change 32 with (Z_of_nat wordsize). + change 32 with (Z_of_nat Int.wordsize). rewrite (Int.is_power2_range _ _ H0). generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros. subst i. discriminate. @@ -416,19 +416,19 @@ Proof. assumption. (* Oshl *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shlimm_correct. assumption. assumption. (* Oshr *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shrimm_correct. assumption. assumption. (* Oshru *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shruimm_correct. assumption. assumption. diff --git a/powerpc/Op.v b/powerpc/Op.v index 27e12c2c..c6e196f3 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -224,15 +224,15 @@ Definition eval_operation | Onor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.or n1 n2))) | Onxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.not (Int.xor n1 n2))) | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None | Oshrimm n, Vint n1 :: nil => - if Int.ltu n (Int.repr 32) then Some (Vint (Int.shr n1 n)) else None + if Int.ltu n Int.iwordsize then Some (Vint (Int.shr n1 n)) else None | Oshrximm n, Vint n1 :: nil => - if Int.ltu n (Int.repr 32) then Some (Vint (Int.shrx n1 n)) else None + if Int.ltu n Int.iwordsize then Some (Vint (Int.shrx n1 n)) else None | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None | Orolm amount mask, Vint n1 :: nil => Some (Vint (Int.rolm n1 amount mask)) | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) @@ -522,15 +522,15 @@ Proof. injection H0; intro; subst v; exact I. destruct (Int.eq i0 Int.zero). discriminate. injection H0; intro; subst v; exact I. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i (Int.repr 32)). + destruct (Int.ltu i Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i (Int.repr 32)). + destruct (Int.ltu i Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. destruct v0; exact I. destruct (eval_condition c vl). @@ -694,11 +694,11 @@ Proof. unfold eq_block in H. destruct (zeq b b0); congruence. destruct (Int.eq i0 Int.zero); congruence. destruct (Int.eq i0 Int.zero); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i (Int.repr 32)); congruence. - destruct (Int.ltu i (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i Int.iwordsize); congruence. + destruct (Int.ltu i Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. caseEq (eval_condition c vl); intros; rewrite H0 in H. replace v with (Val.of_bool b). eapply eval_condition_weaken; eauto. @@ -797,11 +797,11 @@ Proof. destruct (eq_block b b0); inv H0. TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. caseEq (eval_condition c vl1); intros. rewrite H1 in H0. rewrite (eval_condition_lessdef c H H1). diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index ef55b8bb..40201e77 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -396,7 +396,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := | rolm_case1 n1 => Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil | rolm_case2 amount1 mask1 t1 => - let amount := Int.and (Int.add amount1 amount2) (Int.repr 31) in + let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in let mask := Int.and (Int.rol mask1 amount2) mask2 in if Int.is_rlw_mask mask then Eop (Orolm amount mask) (t1:::Enil) @@ -408,7 +408,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := Definition shlimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 - else if Int.ltu n2 (Int.repr 32) then + else if Int.ltu n2 Int.iwordsize then rolm e1 n2 (Int.shl Int.mone n2) else Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil). @@ -416,8 +416,8 @@ Definition shlimm (e1: expr) (n2: int) := Definition shruimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 - else if Int.ltu n2 (Int.repr 32) then - rolm e1 (Int.sub (Int.repr 32) n2) (Int.shru Int.mone n2) + else if Int.ltu n2 Int.iwordsize then + rolm e1 (Int.sub Int.iwordsize n2) (Int.shru Int.mone n2) else Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil). diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 77bca504..ae152b38 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -346,11 +346,7 @@ Proof. case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). EvalOp. simpl. subst x. decEq. decEq. - replace (Int.and (Int.add amount1 amount) (Int.repr 31)) - with (Int.modu (Int.add amount1 amount) (Int.repr 32)). - symmetry. apply Int.rolm_rolm. - change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one). - apply Int.modu_and with (Int.repr 5). reflexivity. + symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus. EvalOp. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto. EvalOp. Qed. @@ -358,7 +354,7 @@ Qed. Theorem eval_shlimm: forall le a n x, eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> + Int.ltu n Int.iwordsize = true -> eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). Proof. intros. unfold shlimm. @@ -372,14 +368,14 @@ Qed. Theorem eval_shruimm: forall le a n x, eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> + Int.ltu n Int.iwordsize = true -> eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). Proof. intros. unfold shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. subst n. rewrite Int.shru_zero. auto. rewrite H0. - replace (Int.shru x n) with (Int.rolm x (Int.sub (Int.repr 32) n) (Int.shru Int.mone n)). + replace (Int.shru x n) with (Int.rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n)). apply eval_rolm. auto. symmetry. apply Int.shru_rolm. exact H0. Qed. @@ -391,7 +387,7 @@ Proof. intros; unfold mulimm_base. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). - change (Z_of_nat wordsize) with 32. + change (Z_of_nat Int.wordsize) with 32. destruct (Int.one_bits n). intros. EvalOp. destruct l. @@ -611,7 +607,7 @@ Theorem eval_shl: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). Proof. intros until y; unfold shl; case (shift_match b); intros. @@ -623,7 +619,7 @@ Theorem eval_shru: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). Proof. intros until y; unfold shru; case (shift_match b); intros. @@ -908,7 +904,7 @@ Theorem eval_shr: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). Proof. intros; unfold shr; EvalOp. simpl. rewrite H1. auto. Qed. -- cgit