From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Switch.v | 143 +++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 131 insertions(+), 12 deletions(-) (limited to 'common') diff --git a/common/Switch.v b/common/Switch.v index 179d4d2..ee8f6aa 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -13,12 +13,18 @@ (* *) (* *********************************************************************) -(** Multi-way branches (``[switch]'') and their compilation - to 2-way comparison trees. *) +(** Multi-way branches (``switch'' statements) and their compilation + to comparison trees. *) Require Import EqNat. +Require Import FMaps. +Require FMapAVL. Require Import Coqlib. Require Import Integers. +Require Import Ordered. + +Module IntMap := FMapAVL.Make(OrderedInt). +Module IntMapF := FMapFacts.Facts(IntMap). (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) @@ -33,22 +39,29 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table) if Int.eq n key then action else switch_target n dfl rem end. -(** Multi-way branches are translated to a 2-way comparison tree. - Each node of the tree performs an equality test or a less-than - test against one of the keys. *) +(** Multi-way branches are translated to comparison trees. + Each node of the tree performs either +- an equality against one of the keys; +- or a "less than" test against one of the keys; +- or a computed branch (jump table) against a range of key values. *) Inductive comptree : Type := | CTaction: nat -> comptree | CTifeq: int -> nat -> comptree -> comptree - | CTiflt: int -> comptree -> comptree -> comptree. + | CTiflt: int -> comptree -> comptree -> comptree + | CTjumptable: int -> int -> list nat -> comptree -> comptree. -Fixpoint comptree_match (n: int) (t: comptree) {struct t}: nat := +Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat := match t with - | CTaction act => act + | CTaction act => Some act | CTifeq key act t' => - if Int.eq n key then act else comptree_match n t' + if Int.eq n key then Some act else comptree_match n t' | CTiflt key t1 t2 => if Int.ltu n key then comptree_match n t1 else comptree_match n t2 + | CTjumptable ofs sz tbl t' => + if Int.ltu (Int.sub n ofs) sz + then list_nth_z tbl (Int.signed (Int.sub n ofs)) + else comptree_match n t' end. (** The translation from a table to a comparison tree is performed @@ -80,12 +93,32 @@ Fixpoint split_eq (pivot: int) (cases: table) else (same, (key, act) :: others) end. +Fixpoint split_between (ofs sz: int) (cases: table) + {struct cases} : IntMap.t nat * table := + match cases with + | nil => (IntMap.empty nat, nil) + | (key, act) :: rem => + let (inside, outside) := split_between ofs sz rem in + if Int.ltu (Int.sub key ofs) sz + then (IntMap.add key act inside, outside) + else (inside, (key, act) :: outside) + end. + Definition refine_low_bound (v lo: Z) := if zeq v lo then lo + 1 else lo. Definition refine_high_bound (v hi: Z) := if zeq v hi then hi - 1 else hi. +Fixpoint validate_jumptable (cases: IntMap.t nat) (default: nat) + (tbl: list nat) (n: int) {struct tbl} : bool := + match tbl with + | nil => true + | act :: rem => + beq_nat act (match IntMap.find n cases with Some a => a | None => default end) + && validate_jumptable cases default rem (Int.add n Int.one) + end. + Fixpoint validate (default: nat) (cases: table) (t: comptree) (lo hi: Z) {struct t} : bool := match t with @@ -112,6 +145,15 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) validate default lcases t1 lo (Int.unsigned pivot - 1) && validate default rcases t2 (Int.unsigned pivot) hi end + | CTjumptable ofs sz tbl t' => + let tbl_len := list_length_z tbl in + match split_between ofs sz cases with + | (inside, outside) => + zle (Int.unsigned sz) tbl_len + && zle tbl_len Int.max_signed + && validate_jumptable inside default tbl ofs + && validate default outside t' lo hi + end end. Definition validate_switch (default: nat) (cases: table) (t: comptree) := @@ -163,11 +205,78 @@ Proof. auto. Qed. +Lemma split_between_prop: + forall v default ofs sz cases inside outside, + split_between ofs sz cases = (inside, outside) -> + switch_target v default cases = + (if Int.ltu (Int.sub v ofs) sz + then match IntMap.find v inside with Some a => a | None => default end + else switch_target v default outside). +Proof. + induction cases; intros until outside; simpl. + intros. inv H. simpl. destruct (Int.ltu (Int.sub v ofs) sz); auto. + destruct a as [key act]. case_eq (split_between ofs sz cases). intros ins outs SEQ. + rewrite (IHcases _ _ SEQ). + case_eq (Int.ltu (Int.sub key ofs) sz); intros; inv H0; simpl. + rewrite IntMapF.add_o. + predSpec Int.eq Int.eq_spec v key. + subst v. rewrite H. rewrite dec_eq_true. auto. + rewrite dec_eq_false; auto. + case_eq (Int.ltu (Int.sub v ofs) sz); intros; auto. + predSpec Int.eq Int.eq_spec v key. + subst v. congruence. + auto. +Qed. + +Lemma validate_jumptable_correct_rec: + forall cases default tbl base v, + validate_jumptable cases default tbl base = true -> + 0 <= Int.signed v < list_length_z tbl -> Int.signed v <= Int.max_signed -> + list_nth_z tbl (Int.signed v) = + Some(match IntMap.find (Int.add base v) cases with Some a => a | None => default end). +Proof. + induction tbl; intros until v; simpl. + unfold list_length_z; simpl. intros. omegaContradiction. + rewrite list_length_z_cons. intros. destruct (andb_prop _ _ H). clear H. + generalize (beq_nat_eq _ _ (sym_equal H2)). clear H2. intro. subst a. + destruct (zeq (Int.signed v) 0). + rewrite Int.add_signed. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_signed. auto. + assert (Int.signed (Int.sub v Int.one) = Int.signed v - 1). + rewrite Int.sub_signed. change (Int.signed Int.one) with 1. + apply Int.signed_repr. split. apply Zle_trans with 0. + vm_compute; congruence. omega. omega. + replace (Int.add base v) with (Int.add (Int.add base Int.one) (Int.sub v Int.one)). + rewrite <- IHtbl. rewrite H. auto. auto. rewrite H. omega. + rewrite H. omega. + rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite Int.add_assoc. + replace (Int.add Int.one (Int.neg Int.one)) with Int.zero. + rewrite Int.add_zero. apply Int.add_commut. + apply Int.mkint_eq. reflexivity. +Qed. + +Lemma validate_jumptable_correct: + forall cases default tbl ofs v sz, + validate_jumptable cases default tbl ofs = true -> + Int.ltu (Int.sub v ofs) sz = true -> + Int.unsigned sz <= list_length_z tbl <= Int.max_signed -> + list_nth_z tbl (Int.signed (Int.sub v ofs)) = + Some(match IntMap.find v cases with Some a => a | None => default end). +Proof. + intros. + exploit Int.ltu_range_test; eauto. omega. intros. + rewrite (validate_jumptable_correct_rec cases default tbl ofs). + rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. rewrite Int.add_zero. auto. + auto. + omega. + omega. +Qed. + Lemma validate_correct_rec: forall default v t cases lo hi, validate default cases t lo hi = true -> lo <= Int.unsigned v <= hi -> - switch_target v default cases = comptree_match v t. + comptree_match v t = Some (switch_target v default cases). Proof. induction t; simpl; intros until hi. (* base case *) @@ -187,7 +296,7 @@ Proof. intros. destruct (andb_prop _ _ H). clear H. rewrite (split_eq_prop v default _ _ _ _ EQ). predSpec Int.eq Int.eq_spec v i. - symmetry. apply beq_nat_eq; auto. + f_equal. apply beq_nat_eq; auto. eapply IHt. eauto. assert (Int.unsigned v <> Int.unsigned i). rewrite <- (Int.repr_unsigned v) in H. @@ -203,11 +312,21 @@ Proof. unfold Int.ltu. destruct (zlt (Int.unsigned v) (Int.unsigned i)). eapply IHt1. eauto. omega. eapply IHt2. eauto. omega. + (* jumptable node *) + case_eq (split_between i i0 cases). intros ins outs EQ V RANGE. + destruct (andb_prop _ _ V). clear V. + destruct (andb_prop _ _ H). clear H. + destruct (andb_prop _ _ H1). clear H1. + rewrite (split_between_prop v _ _ _ _ _ _ EQ). + case_eq (Int.ltu (Int.sub v i) i0); intros. + eapply validate_jumptable_correct; eauto. + split; eapply proj_sumbool_true; eauto. + eapply IHt; eauto. Qed. Definition table_tree_agree (default: nat) (cases: table) (t: comptree) : Prop := - forall v, switch_target v default cases = comptree_match v t. + forall v, comptree_match v t = Some(switch_target v default cases). Theorem validate_switch_correct: forall default t cases, -- cgit v1.2.3