From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - Support "switch" statements over 64-bit integers (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 6 + backend/CMlexer.mll | 1 + backend/CMparser.mly | 20 +- backend/CMtypecheck.ml | 4 +- backend/Cminor.v | 19 +- backend/CminorSel.v | 45 ++++- backend/PrintCminor.ml | 11 +- backend/RTLgen.v | 76 ++++--- backend/RTLgenaux.ml | 102 +--------- backend/RTLgenproof.v | 135 ++++++------- backend/RTLgenspec.v | 144 +++++++------- backend/Selection.v | 127 ++++++++---- backend/Selectionproof.v | 459 +++++++++++++++++++++++++++++++------------ backend/ValueDomain.v | 181 ++++++++++++++++- cfrontend/C2C.ml | 4 +- cfrontend/Cexec.v | 8 +- cfrontend/Clight.v | 13 +- cfrontend/ClightBigstep.v | 12 +- cfrontend/Cminorgen.v | 6 +- cfrontend/Cminorgenproof.v | 9 +- cfrontend/Cop.v | 26 ++- cfrontend/Csem.v | 11 +- cfrontend/Csharpminor.v | 20 +- cfrontend/Cshmgen.v | 6 +- cfrontend/Cshmgenproof.v | 12 +- cfrontend/Cstrategy.v | 16 +- cfrontend/Csyntax.v | 2 +- cfrontend/SimplExprproof.v | 4 +- cfrontend/SimplLocalsproof.v | 10 +- common/Switch.v | 336 ++++++++++++++++--------------- common/Switchaux.ml | 99 ++++++++++ extraction/extraction.v | 5 +- 32 files changed, 1220 insertions(+), 709 deletions(-) create mode 100644 common/Switchaux.ml diff --git a/Changelog b/Changelog index 8a2af33..c497f68 100644 --- a/Changelog +++ b/Changelog @@ -26,6 +26,12 @@ pseudo-instructions so that it does not need to be re-done in cchecklink. Updated the cchecklink validator accordingly. +- Language features: support "switch" statements over an argument of + type "long long". + +- Value analysis and constant propagation: more precise treatment of + comparisons against an integer constant. + Release 2.3pl2, 2014-05-15 ========================== diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index d1926fd..7ed5b4a 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -149,6 +149,7 @@ rule token = parse | "*f" { STARF } | "*l" { STARL } | "switch" { SWITCH } + | "switchl" { SWITCHL } | "tailcall" { TAILCALL } | "~" { TILDE } | "~l" { TILDEL } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 8c3769a..ad92a12 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -188,14 +188,14 @@ let longconst n = let exitnum n = Nat.of_int32 n -let mkswitch expr (cases, dfl) = +let mkswitch islong convert expr (cases, dfl) = convert_accu := []; let c = convert_rexpr expr in let rec mktable = function | [] -> [] | (key, exit) :: rem -> - (coqint_of_camlint key, exitnum exit) :: mktable rem in - prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl)) + (convert key, exitnum exit) :: mktable rem in + prepend_seq !convert_accu (Sswitch(islong, c, mktable cases, exitnum dfl)) (*** match (a) { case 0: s0; case 1: s1; case 2: s2; } ---> @@ -222,7 +222,7 @@ let mkmatch_aux expr cases = (coqint_of_camlint key, Nat.of_int n) :: mktable (n + 1) rem in let sw = - Sswitch(expr, mktable 0 cases, Nat.of_int (ncases - 1)) in + Sswitch(false, expr, mktable 0 cases, Nat.of_int (ncases - 1)) in let rec mkblocks body n = function | [] -> assert false | [key, action] -> @@ -366,6 +366,7 @@ let mkmatch expr cases = %token STARL %token STRINGLIT %token SWITCH +%token SWITCHL %token TILDE %token TILDEL %token TAILCALL @@ -531,7 +532,9 @@ stmt: | RETURN SEMICOLON { Sreturn None } | RETURN expr SEMICOLON { mkreturn_some $2 } | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE - { mkswitch $3 $6 } + { mkswitch false Z.of_uint32 $3 $6 } + | SWITCHL LPAREN expr RPAREN LBRACE switchl_cases RBRACE + { mkswitch true Z.of_uint64 $3 $6 } | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE { mkmatch $3 $6 } | TAILCALL expr LPAREN expr_list RPAREN COLON signature SEMICOLON @@ -558,6 +561,13 @@ switch_cases: { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) } ; +switchl_cases: + DEFAULT COLON EXIT INTLIT SEMICOLON + { ([], $4) } + | CASE LONGLIT COLON EXIT INTLIT SEMICOLON switchl_cases + { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) } +; + match_cases: /* empty */ { [] } | CASE INTLIT COLON stmt_list match_cases { ($2, $4) :: $5 } diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 02c3f21..aacbf86 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -313,8 +313,8 @@ let rec type_stmt env blk ret s = | Sexit n -> if Nat.to_int n >= blk then raise (Error (sprintf "Bad exit(%d)\n" (Nat.to_int n))) - | Sswitch(e, cases, deflt) -> - unify (type_expr env [] e) tint + | Sswitch(islong, e, cases, deflt) -> + unify (type_expr env [] e) (if islong then tlong else tint) | Sreturn None -> begin match ret with | None -> () diff --git a/backend/Cminor.v b/backend/Cminor.v index bf20de2..7ac23bf 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -148,7 +148,7 @@ Inductive stmt : Type := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sswitch: expr -> list (int * nat) -> nat -> stmt + | Sswitch: bool -> expr -> list (Z * nat) -> nat -> stmt | Sreturn: option expr -> stmt | Slabel: label -> stmt -> stmt | Sgoto: label -> stmt. @@ -510,9 +510,10 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sexit (S n)) (Kblock k) sp e m) E0 (State f (Sexit n) k sp e m) - | step_switch: forall f a cases default k sp e m n, - eval_expr sp e m a (Vint n) -> - step (State f (Sswitch a cases default) k sp e m) + | step_switch: forall f islong a cases default k sp e m v n, + eval_expr sp e m a v -> + switch_argument islong v n -> + step (State f (Sswitch islong a cases default) k sp e m) E0 (State f (Sexit (switch_target n default cases)) k sp e m) | step_return_0: forall f k sp e m m', @@ -733,9 +734,10 @@ with exec_stmt: forall f sp e m n, exec_stmt f sp e m (Sexit n) E0 e m (Out_exit n) | exec_Sswitch: - forall f sp e m a cases default n, - eval_expr ge sp e m a (Vint n) -> - exec_stmt f sp e m (Sswitch a cases default) + forall f sp e m islong a cases default v n, + eval_expr ge sp e m a v -> + switch_argument islong v n -> + exec_stmt f sp e m (Sswitch islong a cases default) E0 e m (Out_exit (switch_target n default cases)) | exec_Sreturn_none: forall f sp e m, @@ -1051,8 +1053,7 @@ Proof. (* switch *) econstructor; split. - apply star_one. econstructor; eauto. - constructor. + apply star_one. econstructor; eauto. constructor. (* return none *) econstructor; split. apply star_refl. constructor; auto. diff --git a/backend/CminorSel.v b/backend/CminorSel.v index db414a2..03ef092 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -22,7 +22,6 @@ Require Import Memory. Require Import Cminor. Require Import Op. Require Import Globalenvs. -Require Import Switch. Require Import Smallstep. (** * Abstract syntax *) @@ -57,10 +56,21 @@ with condexpr : Type := Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. +(** Conditional expressions [condexpr] are expressions that are evaluated + not for their exact value, but for their [true]/[false] Boolean value. + Likewise, exit expressions [exitexpr] are expressions that evaluate + to an exit number. They are used to compile the [Sswitch] statement + of Cminor. *) + +Inductive exitexpr : Type := + | XEexit: nat -> exitexpr + | XEjumptable: expr -> list nat -> exitexpr + | XEcondition: condexpr -> exitexpr -> exitexpr -> exitexpr + | XElet: expr -> exitexpr -> exitexpr. + (** Statements are as in Cminor, except that the [Sifthenelse] - construct uses a machine-dependent condition (with multiple - arguments), and the [Sstore] construct uses a machine-dependent - addressing mode. *) + construct uses a conditional expression, and the [Sstore] construct + uses a machine-dependent addressing mode. *) Inductive stmt : Type := | Sskip: stmt @@ -74,7 +84,7 @@ Inductive stmt : Type := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sswitch: expr -> list (int * nat) -> nat -> stmt + | Sswitch: exitexpr -> stmt | Sreturn: option expr -> stmt | Slabel: label -> stmt -> stmt | Sgoto: label -> stmt. @@ -214,6 +224,22 @@ Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop. +Inductive eval_exitexpr: letenv -> exitexpr -> nat -> Prop := + | eval_XEexit: forall le x, + eval_exitexpr le (XEexit x) x + | eval_XEjumptable: forall le a tbl n x, + eval_expr le a (Vint n) -> + list_nth_z tbl (Int.unsigned n) = Some x -> + eval_exitexpr le (XEjumptable a tbl) x + | eval_XEcondition: forall le a b c va x, + eval_condexpr le a va -> + eval_exitexpr le (if va then b else c) x -> + eval_exitexpr le (XEcondition a b c) x + | eval_XElet: forall le a b v x, + eval_expr le a v -> + eval_exitexpr (v :: le) b x -> + eval_exitexpr le (XElet a b) x. + Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := | eval_eos_e: forall le e v, eval_expr le e v -> @@ -344,10 +370,10 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sexit (S n)) (Kblock k) sp e m) E0 (State f (Sexit n) k sp e m) - | step_switch: forall f a cases default k sp e m n, - eval_expr sp e m nil a (Vint n) -> - step (State f (Sswitch a cases default) k sp e m) - E0 (State f (Sexit (switch_target n default cases)) k sp e m) + | step_switch: forall f a k sp e m n, + eval_exitexpr sp e m nil a n -> + step (State f (Sswitch a) k sp e m) + E0 (State f (Sexit n) k sp e m) | step_return_0: forall f k sp e m m', Mem.free m sp 0 f.(fn_stackspace) = Some m' -> @@ -517,4 +543,3 @@ Proof. Qed. Hint Resolve eval_lift: evalexpr. - diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 51a45b2..19f4c83 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -272,12 +272,15 @@ let rec print_stmt p s = print_stmt s | Sexit n -> fprintf p "exit %d;" (Nat.to_int n) - | Sswitch(e, cases, dfl) -> - fprintf p "@[switch (%a) {" print_expr e; + | Sswitch(long, e, cases, dfl) -> + fprintf p "@[switch%s (%a) {" + (if long then "l" else "") print_expr e; List.iter (fun (n, x) -> - fprintf p "@ case %ld: exit %d;" - (camlint_of_coqint n) (Nat.to_int x)) + fprintf p "@ case %s%s: exit %d;" + (Z.to_string n) + (if long then "LL" else "") + (Nat.to_int x)) cases; fprintf p "@ default: exit %d;\n" (Nat.to_int dfl); fprintf p "@;<0 -2>}@]" diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 193702e..26f51e3 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -455,19 +455,7 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) transl_expr map b r nc end. -(** Auxiliary for branch prediction. When compiling an if/then/else - statement, we have a choice between translating the ``then'' branch - first or the ``else'' branch first. Linearization of RTL control-flow - graph, performed later, will exploit this choice as a hint about - which branch is most frequently executed. However, this choice has - no impact on program correctness. We delegate the choice to an - external heuristic (written in OCaml), declared below. *) - -Parameter more_likely: condexpr -> stmt -> stmt -> bool. - -(** Auxiliary for translating [Sswitch] statements. *) - -Parameter compile_switch: nat -> table -> comptree. +(** Auxiliary for translating exit expressions. *) Definition transl_exit (nexits: list node) (n: nat) : mon node := match nth_error nexits n with @@ -484,29 +472,39 @@ Fixpoint transl_jumptable (nexits: list node) (tbl: list nat) : mon (list node) ret (n1 :: nl) end. -Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) - {struct t} : mon node := - match t with - | CTaction act => - transl_exit nexits act - | CTifeq key act t' => - do ncont <- transl_switch r nexits t'; - do nfound <- transl_exit nexits act; - add_instr (Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) - | CTiflt key t1 t2 => - do n2 <- transl_switch r nexits t2; - do n1 <- transl_switch r nexits t1; - add_instr (Icond (Ccompuimm Clt key) (r :: nil) n1 n2) - | CTjumptable ofs sz tbl t' => - do rt <- new_reg; - do ttbl <- transl_jumptable nexits tbl; - do n1 <- add_instr (Ijumptable rt ttbl); - do n2 <- transl_switch r nexits t'; - do n3 <- add_instr (Icond (Ccompuimm Clt sz) (rt :: nil) n1 n2); - let op := if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs) in - add_instr (Iop op (r :: nil) rt n3) +(** Translation of an exit expression. Branches to the node corresponding + to the exit number denoted by the expression. *) + +Fixpoint transl_exitexpr (map: mapping) (a: exitexpr) (nexits: list node) + {struct a} : mon node := + match a with + | XEexit n => + transl_exit nexits n + | XEjumptable a tbl => + do r <- alloc_reg map a; + do tbl' <- transl_jumptable nexits tbl; + do n1 <- add_instr (Ijumptable r tbl'); + transl_expr map a r n1 + | XEcondition a b c => + do nc <- transl_exitexpr map c nexits; + do nb <- transl_exitexpr map b nexits; + transl_condexpr map a nb nc + | XElet a b => + do r <- new_reg; + do n1 <- transl_exitexpr (add_letvar map r) b nexits; + transl_expr map a r n1 end. +(** Auxiliary for branch prediction. When compiling an if/then/else + statement, we have a choice between translating the ``then'' branch + first or the ``else'' branch first. Linearization of RTL control-flow + graph, performed later, will exploit this choice as a hint about + which branch is most frequently executed. However, this choice has + no impact on program correctness. We delegate the choice to an + external heuristic (written in OCaml), declared below. *) + +Parameter more_likely: condexpr -> stmt -> stmt -> bool. + (** Translation of statements. [transl_stmt map s nd nexits nret rret] enriches the current CFG with the RTL instructions necessary to execute the CminorSel statement [s], and returns the node of the first @@ -581,14 +579,8 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) transl_stmt map sbody nd (nd :: nexits) ngoto nret rret | Sexit n => transl_exit nexits n - | Sswitch a cases default => - let t := compile_switch default cases in - if validate_switch default cases t then - (do r <- alloc_reg map a; - do ns <- transl_switch r nexits t; - transl_expr map a r ns) - else - error (Errors.msg "RTLgen: wrong switch") + | Sswitch a => + transl_exitexpr map a nexits | Sreturn opt_a => match opt_a, rret with | None, _ => ret nret diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 7590102..27a4908 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -48,6 +48,14 @@ and size_condexpr = function | CElet(a, c) -> size_expr a + size_condexpr c +let rec size_exitexpr = function + | XEexit n -> 0 + | XEjumptable(arg, tbl) -> 2 + size_expr arg + | XEcondition(c1, c2, c3) -> + 1 + size_condexpr c1 + size_exitexpr c2 + size_exitexpr c3 + | XElet(a, c) -> + size_expr a + size_exitexpr c + let rec length_exprs = function | Enil -> 0 | Econs(e1, el) -> 1 + length_exprs el @@ -71,7 +79,7 @@ let rec size_stmt = function | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s | Sexit n -> 1 - | Sswitch(arg, tbl, dfl) -> 2 + size_expr arg + | Sswitch xe -> size_exitexpr xe | Sreturn None -> 2 | Sreturn (Some arg) -> 2 + size_expr arg | Slabel(lbl, s) -> size_stmt s @@ -80,95 +88,3 @@ let rec size_stmt = function let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot -(* Compiling a switch table into a decision tree *) - -module IntOrd = - struct - type t = Integers.Int.int - let compare x y = - if Integers.Int.eq x y then 0 else - if Integers.Int.ltu x y then -1 else 1 - end - -module IntSet = Set.Make(IntOrd) - -let normalize_table tbl = - let rec norm keys accu = function - | [] -> (accu, keys) - | (key, act) :: rem -> - if IntSet.mem key keys - then norm keys accu rem - else norm (IntSet.add key keys) ((key, act) :: accu) rem - in norm IntSet.empty [] tbl - -let compile_switch_as_tree default tbl = - let sw = Array.of_list tbl in - Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw; - let rec build lo hi minval maxval = - match hi - lo with - | 0 -> - CTaction default - | 1 -> - let (key, act) = sw.(lo) in - if Integers.Int.sub maxval minval = Integers.Int.zero - then CTaction act - else CTifeq(key, act, CTaction default) - | 2 -> - let (key1, act1) = sw.(lo) - and (key2, act2) = sw.(lo+1) in - CTifeq(key1, act1, - if Integers.Int.sub maxval minval = Integers.Int.one - then CTaction act2 - else CTifeq(key2, act2, CTaction default)) - | 3 -> - let (key1, act1) = sw.(lo) - and (key2, act2) = sw.(lo+1) - and (key3, act3) = sw.(lo+2) in - CTifeq(key1, act1, - CTifeq(key2, act2, - if Integers.Int.sub maxval minval = coqint_of_camlint 2l - then CTaction act3 - else CTifeq(key3, act3, CTaction default))) - | _ -> - let mid = (lo + hi) / 2 in - let (pivot, _) = sw.(mid) in - CTiflt(pivot, - build lo mid minval (Integers.Int.sub pivot Integers.Int.one), - build mid hi pivot maxval) - in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned - -let uint64_of_coqint n = (* force unsigned interpretation *) - Int64.logand (Int64.of_int32 (camlint_of_coqint n)) 0xFFFF_FFFFL - -let compile_switch_as_jumptable default cases minkey maxkey = - let tblsize = 1 + Int64.to_int (Int64.sub maxkey minkey) in - assert (tblsize >= 0 && tblsize <= Sys.max_array_length); - let tbl = Array.make tblsize default in - List.iter - (fun (key, act) -> - let pos = Int64.to_int (Int64.sub (uint64_of_coqint key) minkey) in - tbl.(pos) <- act) - cases; - CTjumptable(coqint_of_camlint (Int64.to_int32 minkey), - coqint_of_camlint (Int32.of_int tblsize), - Array.to_list tbl, - CTaction default) - -let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) = - let span = Int64.sub maxkey minkey in - assert (span >= 0L); - let tree_size = Int64.mul 4L (Int64.of_int numcases) - and table_size = Int64.add 8L span in - numcases >= 7 (* really small jump tables are less efficient *) - && span < Int64.of_int Sys.max_array_length - && table_size <= tree_size - -let compile_switch default table = - let (tbl, keys) = normalize_table table in - if IntSet.is_empty keys then CTaction default else begin - let minkey = uint64_of_coqint (IntSet.min_elt keys) - and maxkey = uint64_of_coqint (IntSet.max_elt keys) in - if dense_enough (List.length tbl) minkey maxkey - then compile_switch_as_jumptable default tbl minkey maxkey - else compile_switch_as_tree default tbl - end diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 51f1f27..2aa5ab9 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -414,71 +414,6 @@ Proof. split. apply Regmap.gss. intros; apply Regmap.gso; auto. Qed. -(** Correctness of the translation of [switch] statements *) - -Lemma transl_switch_correct: - forall cs sp e m f map r nexits t ns, - tr_switch f.(fn_code) map r nexits t ns -> - forall rs i act, - rs#r = Vint i -> - map_wf map -> - match_env map e nil rs -> - comptree_match i t = Some act -> - exists nd, exists rs', - star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ - nth_error nexits act = Some nd /\ - match_env map e nil rs'. -Proof. - Opaque Int.sub. - induction 1; simpl; intros. -(* action *) - inv H3. exists n; exists rs; intuition. - apply star_refl. -(* ifeq *) - caseEq (Int.eq i key); intro EQ; rewrite EQ in H5. - inv H5. exists nfound; exists rs; intuition. - apply star_one. eapply exec_Icond with (b := true); eauto. - simpl. rewrite H2. simpl. congruence. - exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. - exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond with (b := false); eauto. - simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. -(* iflt *) - caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5. - exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. - exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond with (b := true); eauto. - simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. - exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. - exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond with (b := false); eauto. - simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. -(* jumptable *) - set (rs1 := rs#rt <- (Vint(Int.sub i ofs))). - assert (ME1: match_env map e nil rs1). - unfold rs1. eauto with rtlg. - assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)). - eapply exec_Iop; eauto. - predSpec Int.eq Int.eq_spec ofs Int.zero; simpl. - rewrite H10. rewrite Int.sub_zero_l. congruence. - rewrite H6. simpl. rewrite <- Int.sub_add_opp. auto. - caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9. - exploit H5; eauto. intros [nd [A B]]. - exists nd; exists rs1; intuition. - eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond with (b := true); eauto. - simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. - apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. - reflexivity. traceEq. - exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto. - intros [nd [rs' [EX [NTH ME]]]]. - exists nd; exists rs'; intuition. - eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond with (b := false); eauto. - simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. - eexact EX. reflexivity. traceEq. -Qed. - (** ** Semantic preservation for the translation of expressions *) Section CORRECTNESS_EXPR. @@ -560,10 +495,10 @@ Definition transl_condexpr_prop /\ Mem.extends m tm'. (** The correctness of the translation is a huge induction over - the Cminor evaluation derivation for the source program. To keep + the CminorSel evaluation derivation for the source program. To keep the proof manageable, we put each case of the proof in a separate - lemma. There is one lemma for each Cminor evaluation rule. - It takes as hypotheses the premises of the Cminor evaluation rule, + lemma. There is one lemma for each CminorSel evaluation rule. + It takes as hypotheses the premises of the CminorSel evaluation rule, plus the induction hypotheses, that is, the [transl_expr_prop], etc, corresponding to the evaluations of sub-expressions or sub-statements. *) @@ -978,6 +913,58 @@ Proof transl_condexpr_CEcondition_correct transl_condexpr_CElet_correct). +(** Exit expressions. *) + +Definition transl_exitexpr_prop + (le: letenv) (a: exitexpr) (x: nat) : Prop := + forall tm cs f map ns nexits rs + (MWF: map_wf map) + (TE: tr_exitexpr f.(fn_code) map a ns nexits) + (ME: match_env map e le rs) + (EXT: Mem.extends m tm), + exists nd, exists rs', exists tm', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ nth_error nexits x = Some nd + /\ match_env map e le rs' + /\ Mem.extends m tm'. + +Theorem transl_exitexpr_correct: + forall le a x, + eval_exitexpr ge sp e m le a x -> + transl_exitexpr_prop le a x. +Proof. + induction 1; red; intros; inv TE. +- (* XEexit *) + exists ns, rs, tm. + split. apply star_refl. + auto. +- (* XEjumptable *) + exploit H3; eauto. intros (nd & A & B). + exploit transl_expr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & PRES1 & EXT1). + exists nd, rs1, tm1. + split. eapply star_right. eexact EXEC1. eapply exec_Ijumptable; eauto. inv RES1; auto. traceEq. + auto. +- (* XEcondition *) + exploit transl_condexpr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & EXT1). + exploit IHeval_exitexpr; eauto. + instantiate (2 := if va then n2 else n3). destruct va; eauto. + intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2). + exists nd, rs2, tm2. + split. eapply star_trans. apply plus_star. eexact EXEC1. eexact EXEC2. traceEq. + auto. +- (* XElet *) + exploit transl_expr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & PRES1 & EXT1). + assert (map_wf (add_letvar map r)). + eapply add_letvar_wf; eauto. + exploit IHeval_exitexpr; eauto. eapply match_env_bind_letvar; eauto. + intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2). + exists nd, rs2, tm2. + split. eapply star_trans. eexact EXEC1. eexact EXEC2. traceEq. + split. auto. + split. eapply match_env_unbind_letvar; eauto. + auto. +Qed. + End CORRECTNESS_EXPR. (** ** Measure over CminorSel states *) @@ -1357,15 +1344,11 @@ Proof. (* switch *) inv TS. - exploit validate_switch_correct; eauto. intro CTM. - exploit transl_expr_correct; eauto. - intros [rs' [tm' [A [B [C [D X]]]]]]. - exploit transl_switch_correct; eauto. inv C. auto. - intros [nd [rs'' [E [F G]]]]. + exploit transl_exitexpr_correct; eauto. + intros (nd & rs' & tm' & A & B & C & D). econstructor; split. - right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. - econstructor; eauto. - constructor. auto. + right; split. eexact A. Lt_state. + econstructor; eauto. constructor; auto. (* return none *) inv TS. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index c82c051..32f35bb 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -673,7 +673,7 @@ Hint Resolve reg_map_ok_novar: rtlg. (** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the - value of the Cminor expression [expr] and deposit this value in + value of the CminorSel expression [expr] and deposit this value in register [rd]. [map] is a mapping from Cminor variables to the corresponding RTL registers. [pr] is a list of RTL registers whose values must be preserved during this computation. All registers @@ -730,9 +730,9 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eexternal id sg al) ns nd rd dst -(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c], +(** [tr_condition c map pr a ns ntrue nfalse] holds if the graph [c], starting at node [ns], contains instructions that compute the truth - value of the Cminor conditional expression [a] and terminate + value of the CminorSel conditional expression [a] and terminate on node [ntrue] if the condition holds and on node [nfalse] otherwise. *) with tr_condition (c: code): @@ -754,7 +754,7 @@ with tr_condition (c: code): (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the values - of the list of Cminor expression [exprlist] and deposit these values + of the list of CminorSel expression [exprlist] and deposit these values in registers [rds]. *) with tr_exprlist (c: code): @@ -773,31 +773,32 @@ Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : list_nth_z tbl v = Some act -> exists n, list_nth_z ttbl v = Some n /\ nth_error nexits act = Some n. -Inductive tr_switch - (c: code) (map: mapping) (r: reg) (nexits: list node): - comptree -> node -> Prop := - | tr_switch_action: forall act n, - nth_error nexits act = Some n -> - tr_switch c map r nexits (CTaction act) n - | tr_switch_ifeq: forall key act t' n ncont nfound, - tr_switch c map r nexits t' ncont -> - nth_error nexits act = Some nfound -> - c!n = Some(Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) -> - tr_switch c map r nexits (CTifeq key act t') n - | tr_switch_iflt: forall key t1 t2 n n1 n2, - tr_switch c map r nexits t1 n1 -> - tr_switch c map r nexits t2 n2 -> - c!n = Some(Icond (Ccompuimm Clt key) (r :: nil) n1 n2) -> - tr_switch c map r nexits (CTiflt key t1 t2) n - | tr_switch_jumptable: forall ofs sz tbl t n n1 n2 n3 rt ttbl, - ~reg_in_map map rt -> rt <> r -> - c!n = Some(Iop (if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs)) - (r ::nil) rt n1) -> - c!n1 = Some(Icond (Ccompuimm Clt sz) (rt :: nil) n2 n3) -> - c!n2 = Some(Ijumptable rt ttbl) -> - tr_switch c map r nexits t n3 -> - tr_jumptable nexits tbl ttbl -> - tr_switch c map r nexits (CTjumptable ofs sz tbl t) n. +(** [tr_exitexpr c map pr a ns nexits] holds if the graph [c], + starting at node [ns], contains instructions that compute the exit + number of the CminorSel exit expression [a] and terminate + on the node corresponding to this exit number according to the + mapping [nexits]. *) + +Inductive tr_exitexpr (c: code): + mapping -> exitexpr -> node -> list node -> Prop := + | tr_XEcond: forall map x n nexits, + nth_error nexits x = Some n -> + tr_exitexpr c map (XEexit x) n nexits + | tr_XEjumptable: forall map a tbl ns nexits n1 r tbl', + tr_jumptable nexits tbl tbl' -> + tr_expr c map nil a ns n1 r None -> + c!n1 = Some (Ijumptable r tbl') -> + tr_exitexpr c map (XEjumptable a tbl) ns nexits + | tr_XEcondition: forall map a1 a2 a3 ns nexits n2 n3, + tr_condition c map nil a1 ns n2 n3 -> + tr_exitexpr c map a2 n2 nexits -> + tr_exitexpr c map a3 n3 nexits -> + tr_exitexpr c map (XEcondition a1 a2 a3) ns nexits + | tr_XElet: forall map a b ns nexits r n1, + ~reg_in_map map r -> + tr_expr c map nil a ns n1 r None -> + tr_exitexpr c (add_letvar map r) b n1 nexits -> + tr_exitexpr c map (XElet a b) ns nexits. (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor @@ -866,11 +867,9 @@ Inductive tr_stmt (c: code) (map: mapping): | tr_Sexit: forall n ns nd nexits ngoto nret rret, nth_error nexits n = Some ns -> tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret - | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t, - validate_switch default cases t = true -> - tr_expr c map nil a ns n r None -> - tr_switch c map r nexits t n -> - tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret + | tr_Sswitch: forall a ns nd nexits ngoto nret rret, + tr_exitexpr c map a ns nexits -> + tr_stmt c map (Sswitch a) ns nd nexits ngoto nret rret | tr_Sreturn_none: forall nret nd nexits ngoto rret, tr_stmt c map (Sreturn None) nret nd nexits ngoto nret rret | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret, @@ -1126,13 +1125,15 @@ Proof. constructor. eapply new_reg_not_in_map; eauto. Qed. -Lemma tr_switch_incr: +Lemma tr_exitexpr_incr: forall s1 s2, state_incr s1 s2 -> - forall map r nexits t ns, - tr_switch s1.(st_code) map r nexits t ns -> - tr_switch s2.(st_code) map r nexits t ns. + forall map a ns nexits, + tr_exitexpr s1.(st_code) map a ns nexits -> + tr_exitexpr s2.(st_code) map a ns nexits. Proof. - induction 2; econstructor; eauto with rtlg. + intros s1 s2 EXT. + generalize tr_expr_incr tr_condition_incr; intros I1 I2. + induction 1; econstructor; eauto with rtlg. Qed. Lemma tr_stmt_incr: @@ -1142,10 +1143,9 @@ Lemma tr_stmt_incr: tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret. Proof. intros s1 s2 EXT. - generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3. + generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr; intros I1 I2 I3 I4. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). - induction 1; try (econstructor; eauto; fail). - econstructor; eauto. eapply tr_switch_incr; eauto. + induction 1; econstructor; eauto. Qed. Lemma transl_exit_charact: @@ -1170,35 +1170,31 @@ Proof. congruence. Qed. -Lemma transl_switch_charact: - forall map r nexits t s ns s' incr, - map_valid map s -> reg_valid r s -> - transl_switch r nexits t s = OK ns s' incr -> - tr_switch s'.(st_code) map r nexits t ns. +Lemma transl_exitexpr_charact: + forall nexits a map s ns s' INCR + (TR: transl_exitexpr map a nexits s = OK ns s' INCR) + (WF: map_valid map s), + tr_exitexpr s'.(st_code) map a ns nexits. Proof. - induction t; simpl; intros; saturateTrans. - + induction a; simpl; intros; try (monadInv TR); saturateTrans. +- (* XEexit *) exploit transl_exit_charact; eauto. intros [A B]. - econstructor; eauto. - - monadInv H1. - exploit transl_exit_charact; eauto. intros [A B]. subst s1. - econstructor; eauto 2 with rtlg. - apply tr_switch_incr with s0; eauto with rtlg. - - monadInv H1. - econstructor; eauto 2 with rtlg. - apply tr_switch_incr with s1; eauto with rtlg. - apply tr_switch_incr with s0; eauto with rtlg. - - monadInv H1. - exploit transl_jumptable_charact; eauto. intros [A B]. subst s1. - econstructor. eauto with rtlg. - apply sym_not_equal. apply valid_fresh_different with s; eauto with rtlg. - eauto with rtlg. eauto with rtlg. eauto with rtlg. - apply tr_switch_incr with s3. eauto with rtlg. - eapply IHt with (s := s2); eauto with rtlg. - auto. + econstructor; eauto. +- (* XEjumptable *) + exploit transl_jumptable_charact; eauto. intros [A B]. + econstructor; eauto. + eapply transl_expr_charact; eauto with rtlg. + eauto with rtlg. +- (* XEcondition *) + econstructor. + eapply transl_condexpr_charact; eauto with rtlg. + apply tr_exitexpr_incr with s1; eauto with rtlg. + apply tr_exitexpr_incr with s0; eauto with rtlg. +- (* XElet *) + econstructor; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. + apply tr_exitexpr_incr with s1; auto. eapply IHa; eauto with rtlg. + apply add_letvar_valid; eauto with rtlg. Qed. Lemma transl_stmt_charact: @@ -1285,15 +1281,7 @@ Proof. exploit transl_exit_charact; eauto. intros [A B]. econstructor. eauto. (* Sswitch *) - generalize TR; clear TR. - set (t := compile_switch n l). - caseEq (validate_switch n l t); intro VALID; intros. - monadInv TR. - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. - apply tr_switch_incr with s1; auto with rtlg. - eapply transl_switch_charact with (s := s0); eauto with rtlg. - monadInv TR. + econstructor. eapply transl_exitexpr_charact; eauto. (* Sreturn *) destruct o. destruct rret; inv TR. inv OK. diff --git a/backend/Selection.v b/backend/Selection.v index 9bd37ef..cd17b9f 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -27,6 +27,7 @@ Require Import AST. Require Import Errors. Require Import Integers. Require Import Globalenvs. +Require Import Switch. Require Cminor. Require Import Op. Require Import CminorSel. @@ -34,7 +35,8 @@ Require Import SelectOp. Require Import SelectDiv. Require Import SelectLong. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. +Local Open Scope error_monad_scope. (** Conversion of conditions *) @@ -203,60 +205,119 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Conversion of Cminor [switch] statements to decision trees. *) + +Parameter compile_switch: Z -> nat -> table -> comptree. + +Section SEL_SWITCH. + +Variable make_cmp_eq: expr -> Z -> expr. +Variable make_cmp_ltu: expr -> Z -> expr. +Variable make_sub: expr -> Z -> expr. +Variable make_to_int: expr -> expr. + +Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := + match t with + | CTaction act => + XEexit act + | CTifeq key act t' => + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + (XEexit act) + (sel_switch arg t') + | CTiflt key t1 t2 => + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + (sel_switch arg t1) + (sel_switch arg t2) + | CTjumptable ofs sz tbl t' => + XElet (make_sub (Eletvar arg) ofs) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEjumptable (make_to_int (Eletvar O)) tbl) + (sel_switch (S arg) t')) + end. + +End SEL_SWITCH. + +Definition sel_switch_int := + sel_switch + (fun arg n => comp Ceq arg (Eop (Ointconst (Int.repr n)) Enil)) + (fun arg n => compu Clt arg (Eop (Ointconst (Int.repr n)) Enil)) + (fun arg ofs => sub arg (Eop (Ointconst (Int.repr ofs)) Enil)) + (fun arg => arg). + +Definition sel_switch_long := + sel_switch + (fun arg n => cmpl Ceq arg (longconst (Int64.repr n))) + (fun arg n => cmplu Clt arg (longconst (Int64.repr n))) + (fun arg ofs => subl hf arg (longconst (Int64.repr ofs))) + lowlong. + (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := +Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := match s with - | Cminor.Sskip => Sskip - | Cminor.Sassign id e => Sassign id (sel_expr e) - | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) + | Cminor.Sskip => OK Sskip + | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) + | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - match classify_call ge fn with + OK (match classify_call ge fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) - end + end) | Cminor.Sbuiltin optid ef args => - Sbuiltin optid ef (sel_exprlist args) + OK (Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => - match classify_call ge fn with + OK (match classify_call ge fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) | _ => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args) - end - | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) + end) + | Cminor.Sseq s1 s2 => + do s1' <- sel_stmt ge s1; do s2' <- sel_stmt ge s2; + OK (Sseq s1' s2') | Cminor.Sifthenelse e ifso ifnot => - Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ge ifso) (sel_stmt ge ifnot) - | Cminor.Sloop body => Sloop (sel_stmt ge body) - | Cminor.Sblock body => Sblock (sel_stmt ge body) - | Cminor.Sexit n => Sexit n - | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl - | Cminor.Sreturn None => Sreturn None - | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body) - | Cminor.Sgoto lbl => Sgoto lbl + do ifso' <- sel_stmt ge ifso; do ifnot' <- sel_stmt ge ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + | Cminor.Sloop body => + do body' <- sel_stmt ge body; OK (Sloop body') + | Cminor.Sblock body => + do body' <- sel_stmt ge body; OK (Sblock body') + | Cminor.Sexit n => OK (Sexit n) + | Cminor.Sswitch false e cases dfl => + let t := compile_switch Int.modulus dfl cases in + if validate_switch Int.modulus dfl cases t + then OK (Sswitch (XElet (sel_expr e) (sel_switch_int O t))) + else Error (msg "Selection: bad switch (int)") + | Cminor.Sswitch true e cases dfl => + let t := compile_switch Int64.modulus dfl cases in + if validate_switch Int64.modulus dfl cases t + then OK (Sswitch (XElet (sel_expr e) (sel_switch_long O t))) + else Error (msg "Selection: bad switch (long)") + | Cminor.Sreturn None => OK (Sreturn None) + | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e))) + | Cminor.Slabel lbl body => + do body' <- sel_stmt ge body; OK (Slabel lbl body') + | Cminor.Sgoto lbl => OK (Sgoto lbl) end. End SELECTION. (** Conversion of functions. *) -Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : function := - mkfunction - f.(Cminor.fn_sig) - f.(Cminor.fn_params) - f.(Cminor.fn_vars) - f.(Cminor.fn_stackspace) - (sel_stmt hf ge f.(Cminor.fn_body)). +Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function := + do body' <- sel_stmt hf ge f.(Cminor.fn_body); + OK (mkfunction + f.(Cminor.fn_sig) + f.(Cminor.fn_params) + f.(Cminor.fn_vars) + f.(Cminor.fn_stackspace) + body'). -Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : fundef := - transf_fundef (sel_function hf ge) f. +Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := + transf_partial_fundef (sel_function hf ge) f. (** Conversion of programs. *) -Local Open Scope error_monad_scope. - Definition sel_program (p: Cminor.program) : res program := let ge := Genv.globalenv p in - do hf <- get_helpers ge; OK (transform_program (sel_fundef hf ge) p). + do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 55977b4..658e660 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -22,6 +22,7 @@ Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. +Require Import Switch. Require Import Cminor. Require Import Op. Require Import CminorSel. @@ -33,7 +34,8 @@ Require Import SelectOpproof. Require Import SelectDivproof. Require Import SelectLongproof. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. +Local Open Scope error_monad_scope. (** * Correctness of the instruction selection functions for expressions *) @@ -41,50 +43,54 @@ Open Local Scope cminorsel_scope. Section PRESERVATION. Variable prog: Cminor.program. +Variable tprog: CminorSel.program. Let ge := Genv.globalenv prog. -Variable hf: helper_functions. -Let tprog := transform_program (sel_fundef hf ge) prog. Let tge := Genv.globalenv tprog. +Variable hf: helper_functions. Hypothesis HELPERS: i64_helpers_correct tge hf. +Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. - intros; unfold ge, tge, tprog. apply Genv.find_symbol_transf. + intros. eapply Genv.find_symbol_transf_partial; eauto. Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (sel_fundef hf ge f). + exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. Proof. - intros. - exact (Genv.find_funct_ptr_transf (sel_fundef hf ge) _ _ H). + intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. Lemma functions_translated: forall (v v': val) (f: Cminor.fundef), Genv.find_funct ge v = Some f -> Val.lessdef v v' -> - Genv.find_funct tge v' = Some (sel_fundef hf ge f). + exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. Proof. intros. inv H0. - exact (Genv.find_funct_transf (sel_fundef hf ge) _ _ H). + eapply Genv.find_funct_transf_partial; eauto. simpl in H. discriminate. Qed. Lemma sig_function_translated: - forall f, - funsig (sel_fundef hf ge f) = Cminor.funsig f. + forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. +Proof. + intros. destruct f; monadInv H; auto. monadInv EQ. auto. +Qed. + +Lemma stackspace_function_translated: + forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. - intros. destruct f; reflexivity. + intros. monadInv H. auto. Qed. Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. - intros; unfold ge, tge, tprog, sel_program. - apply Genv.find_var_info_transf. + intros; eapply Genv.find_var_info_transf_partial; eauto. Qed. Lemma helper_implements_preserved: @@ -93,7 +99,7 @@ Lemma helper_implements_preserved: helper_implements tge id sg vargs vres. Proof. intros. destruct H as (b & ef & A & B & C & D). - exploit function_ptr_translated; eauto. simpl. intros. + exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. exists b; exists ef. split. rewrite symbols_preserved. auto. split. auto. @@ -306,6 +312,176 @@ Proof. auto. Qed. +(** Translation of [switch] statements *) + +Inductive Rint: Z -> val -> Prop := + | Rint_intro: forall n, Rint (Int.unsigned n) (Vint n). + +Inductive Rlong: Z -> val -> Prop := + | Rlong_intro: forall n, Rlong (Int64.unsigned n) (Vlong n). + +Section SEL_SWITCH. + +Variable make_cmp_eq: expr -> Z -> expr. +Variable make_cmp_ltu: expr -> Z -> expr. +Variable make_sub: expr -> Z -> expr. +Variable make_to_int: expr -> expr. +Variable modulus: Z. +Variable R: Z -> val -> Prop. + +Hypothesis eval_make_cmp_eq: forall sp e m le a v i n, + eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus -> + eval_expr tge sp e m le (make_cmp_eq a n) (Val.of_bool (zeq i n)). +Hypothesis eval_make_cmp_ltu: forall sp e m le a v i n, + eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus -> + eval_expr tge sp e m le (make_cmp_ltu a n) (Val.of_bool (zlt i n)). +Hypothesis eval_make_sub: forall sp e m le a v i n, + eval_expr tge sp e m le a v -> R i v -> 0 <= n < modulus -> + exists v', eval_expr tge sp e m le (make_sub a n) v' /\ R ((i - n) mod modulus) v'. +Hypothesis eval_make_to_int: forall sp e m le a v i, + eval_expr tge sp e m le a v -> R i v -> + exists v', eval_expr tge sp e m le (make_to_int a) v' /\ Rint (i mod Int.modulus) v'. + +Lemma sel_switch_correct_rec: + forall sp e m varg i x, + R i varg -> + forall t arg le, + wf_comptree modulus t -> + nth_error le arg = Some varg -> + comptree_match modulus i t = Some x -> + eval_exitexpr tge sp e m le (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t) x. +Proof. + intros until x; intros Ri. induction t; simpl; intros until le; intros WF ARG MATCH. +- (* base case *) + inv MATCH. constructor. +- (* eq test *) + inv WF. + assert (eval_expr tge sp e m le (make_cmp_eq (Eletvar arg) key) (Val.of_bool (zeq i key))). + { eapply eval_make_cmp_eq; eauto. constructor; auto. } + eapply eval_XEcondition with (va := zeq i key). + eapply eval_condexpr_of_expr; eauto. destruct (zeq i key); constructor; auto. + destruct (zeq i key); simpl. + + inv MATCH. constructor. + + eapply IHt; eauto. +- (* lt test *) + inv WF. + assert (eval_expr tge sp e m le (make_cmp_ltu (Eletvar arg) key) (Val.of_bool (zlt i key))). + { eapply eval_make_cmp_ltu; eauto. constructor; auto. } + eapply eval_XEcondition with (va := zlt i key). + eapply eval_condexpr_of_expr; eauto. destruct (zlt i key); constructor; auto. + destruct (zlt i key); simpl. + + eapply IHt1; eauto. + + eapply IHt2; eauto. +- (* jump table *) + inv WF. + exploit (eval_make_sub sp e m le). eapply eval_Eletvar. eauto. eauto. + instantiate (1 := ofs). auto. + intros (v' & A & B). + set (i' := (i - ofs) mod modulus) in *. + assert (eval_expr tge sp e m (v' :: le) (make_cmp_ltu (Eletvar O) sz) (Val.of_bool (zlt i' sz))). + { eapply eval_make_cmp_ltu; eauto. constructor; auto. } + econstructor. eauto. + eapply eval_XEcondition with (va := zlt i' sz). + eapply eval_condexpr_of_expr; eauto. destruct (zlt i' sz); constructor; auto. + destruct (zlt i' sz); simpl. + + exploit (eval_make_to_int sp e m (v' :: le) (Eletvar O)). + constructor. simpl; eauto. eauto. intros (v'' & C & D). inv D. + econstructor; eauto. congruence. + + eapply IHt; eauto. +Qed. + +Lemma sel_switch_correct: + forall dfl cases arg sp e m varg i t le, + validate_switch modulus dfl cases t = true -> + eval_expr tge sp e m le arg varg -> + R i varg -> + 0 <= i < modulus -> + eval_exitexpr tge sp e m le + (XElet arg (sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t)) + (switch_target i dfl cases). +Proof. + intros. exploit validate_switch_correct; eauto. omega. intros [A B]. + econstructor. eauto. eapply sel_switch_correct_rec; eauto. +Qed. + +End SEL_SWITCH. + +Lemma sel_switch_int_correct: + forall dfl cases arg sp e m i t le, + validate_switch Int.modulus dfl cases t = true -> + eval_expr tge sp e m le arg (Vint i) -> + eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases). +Proof. + assert (INTCONST: forall n sp e m le, + eval_expr tge sp e m le (Eop (Ointconst n) Enil) (Vint n)). + { intros. econstructor. constructor. auto. } + intros. eapply sel_switch_correct with (R := Rint); eauto. +- intros until n; intros EVAL R RANGE. + exploit eval_comp. eexact EVAL. apply (INTCONST (Int.repr n)). + instantiate (1 := Ceq). intros (vb & A & B). + inv R. unfold Val.cmp in B. simpl in B. revert B. + predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. + rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. + unfold Int.max_unsigned; omega. + unfold proj_sumbool; rewrite zeq_false; auto. + red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence. +- intros until n; intros EVAL R RANGE. + exploit eval_compu. eexact EVAL. apply (INTCONST (Int.repr n)). + instantiate (1 := Clt). intros (vb & A & B). + inv R. unfold Val.cmpu in B. simpl in B. + unfold Int.ltu in B. rewrite Int.unsigned_repr in B. + destruct (zlt (Int.unsigned n0) n); inv B; auto. + unfold Int.max_unsigned; omega. +- intros until n; intros EVAL R RANGE. + exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B). + inv R. simpl in B. inv B. econstructor; split; eauto. + replace ((Int.unsigned n0 - n) mod Int.modulus) + with (Int.unsigned (Int.sub n0 (Int.repr n))). + constructor. + unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. + apply Int.unsigned_repr. unfold Int.max_unsigned; omega. +- intros until i0; intros EVAL R. exists v; split; auto. + inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor. +- constructor. +- apply Int.unsigned_range. +Qed. + +Lemma sel_switch_long_correct: + forall dfl cases arg sp e m i t le, + validate_switch Int64.modulus dfl cases t = true -> + eval_expr tge sp e m le arg (Vlong i) -> + eval_exitexpr tge sp e m le (XElet arg (sel_switch_long hf O t)) (switch_target (Int64.unsigned i) dfl cases). +Proof. + intros. eapply sel_switch_correct with (R := Rlong); eauto. +- intros until n; intros EVAL R RANGE. + eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. + rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. + unfold Int64.max_unsigned; omega. +- intros until n; intros EVAL R RANGE. + eapply eval_cmplu. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. + rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. + unfold Int64.max_unsigned; omega. +- intros until n; intros EVAL R RANGE. + exploit eval_subl. eexact HELPERS. eexact EVAL. apply eval_longconst with (n := Int64.repr n). + intros (vb & A & B). + inv R. simpl in B. inv B. econstructor; split; eauto. + replace ((Int64.unsigned n0 - n) mod Int64.modulus) + with (Int64.unsigned (Int64.sub n0 (Int64.repr n))). + constructor. + unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. + apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega. +- intros until i0; intros EVAL R. + exploit eval_lowlong. eexact EVAL. intros (vb & A & B). + inv R. simpl in B. inv B. econstructor; split; eauto. + replace (Int64.unsigned n mod Int.modulus) with (Int.unsigned (Int64.loword n)). + constructor. + unfold Int64.loword. apply Int.unsigned_repr_eq. +- constructor. +- apply Int64.unsigned_range. +Qed. + (** Compatibility of evaluation functions with the "less defined than" relation. *) Ltac TrivialExists := @@ -433,56 +609,62 @@ Qed. Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := | match_cont_stop: match_cont Cminor.Kstop Kstop - | match_cont_seq: forall s k k', + | match_cont_seq: forall s s' k k', + sel_stmt hf ge s = OK s' -> match_cont k k' -> - match_cont (Cminor.Kseq s k) (Kseq (sel_stmt hf ge s) k') + match_cont (Cminor.Kseq s k) (Kseq s' k') | match_cont_block: forall k k', match_cont k k' -> match_cont (Cminor.Kblock k) (Kblock k') - | match_cont_call: forall id f sp e k e' k', + | match_cont_call: forall id f sp e k f' e' k', + sel_function hf ge f = OK f' -> match_cont k k' -> env_lessdef e e' -> - match_cont (Cminor.Kcall id f sp e k) (Kcall id (sel_function hf ge f) sp e' k'). + match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k'). Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m e' m', - s' = sel_stmt hf ge s -> - match_cont k k' -> - env_lessdef e e' -> - Mem.extends m m' -> + | match_state: forall f f' s k s' k' sp e m e' m' + (TF: sel_function hf ge f = OK f') + (TS: sel_stmt hf ge s = OK s') + (MC: match_cont k k') + (LD: env_lessdef e e') + (ME: Mem.extends m m'), match_states (Cminor.State f s k sp e m) - (State (sel_function hf ge f) s' k' sp e' m') - | match_callstate: forall f args args' k k' m m', - match_cont k k' -> - Val.lessdef_list args args' -> - Mem.extends m m' -> + (State f' s' k' sp e' m') + | match_callstate: forall f f' args args' k k' m m' + (TF: sel_fundef hf ge f = OK f') + (MC: match_cont k k') + (LD: Val.lessdef_list args args') + (ME: Mem.extends m m'), match_states (Cminor.Callstate f args k m) - (Callstate (sel_fundef hf ge f) args' k' m') - | match_returnstate: forall v v' k k' m m', - match_cont k k' -> - Val.lessdef v v' -> - Mem.extends m m' -> + (Callstate f' args' k' m') + | match_returnstate: forall v v' k k' m m' + (MC: match_cont k k') + (LD: Val.lessdef v v') + (ME: Mem.extends m m'), match_states (Cminor.Returnstate v k m) (Returnstate v' k' m') - | match_builtin_1: forall ef args args' optid f sp e k m al e' k' m', - match_cont k k' -> - Val.lessdef_list args args' -> - env_lessdef e e' -> - Mem.extends m m' -> - eval_exprlist tge sp e' m' nil al args' -> + | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m' + (TF: sel_function hf ge f = OK f') + (MC: match_cont k k') + (LDA: Val.lessdef_list args args') + (LDE: env_lessdef e e') + (ME: Mem.extends m m') + (EA: eval_exprlist tge sp e' m' nil al args'), match_states (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) - (State (sel_function hf ge f) (Sbuiltin optid ef al) k' sp e' m') - | match_builtin_2: forall v v' optid f sp e k m e' m' k', - match_cont k k' -> - Val.lessdef v v' -> - env_lessdef e e' -> - Mem.extends m m' -> + (State f' (Sbuiltin optid ef al) k' sp e' m') + | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' + (TF: sel_function hf ge f = OK f') + (MC: match_cont k k') + (LDV: Val.lessdef v v') + (LDE: env_lessdef e e') + (ME: Mem.extends m m'), match_states (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) - (State (sel_function hf ge f) Sskip k' sp (set_optvar optid v' e') m'). + (State f' Sskip k' sp (set_optvar optid v' e') m'). Remark call_cont_commut: forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k'). @@ -491,15 +673,16 @@ Proof. Qed. Remark find_label_commut: - forall lbl s k k', + forall lbl s k s' k', match_cont k k' -> - match Cminor.find_label lbl s k, find_label lbl (sel_stmt hf ge s) k' with + sel_stmt hf ge s = OK s' -> + match Cminor.find_label lbl s k, find_label lbl s' k' with | None, None => True - | Some(s1, k1), Some(s1', k1') => s1' = sel_stmt hf ge s1 /\ match_cont k1 k1' + | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1' | _, _ => False end. Proof. - induction s; intros; simpl; auto. + induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto. (* call *) @@ -507,21 +690,27 @@ Proof. (* tailcall *) destruct (classify_call ge e); simpl; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. + exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; - destruct (find_label lbl (sel_stmt hf ge s1) (Kseq (sel_stmt hf ge s2) k')) as [[sy ky] | ]; + destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; - destruct (find_label lbl (sel_stmt hf ge s1) k') as [[sy ky] | ]; + destruct (find_label lbl x k') as [[sy ky] | ]; intuition. apply IHs2; auto. (* loop *) - apply IHs. constructor; auto. + apply IHs. constructor; auto. simpl; rewrite EQ; auto. auto. (* block *) - apply IHs. constructor; auto. + apply IHs. constructor; auto. auto. +(* switch *) + destruct b. + destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE. + simpl; auto. + destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE. + simpl; auto. (* return *) - destruct o; simpl; auto. + destruct o; inv SE; simpl; auto. (* label *) destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. @@ -539,64 +728,68 @@ Lemma sel_step_correct: (exists T2, step tge T1 t T2 /\ match_states S2 T2) \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. - induction 1; intros T1 ME; inv ME; simpl. - (* skip seq *) - inv H7. left; econstructor; split. econstructor. constructor; auto. - (* skip block *) - inv H7. left; econstructor; split. econstructor. constructor; auto. - (* skip call *) + induction 1; intros T1 ME; inv ME; try (monadInv TS). +- (* skip seq *) + inv MC. left; econstructor; split. econstructor. constructor; auto. +- (* skip block *) + inv MC. left; econstructor; split. econstructor. constructor; auto. +- (* skip call *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. left; econstructor; split. - econstructor. inv H9; simpl in H; simpl; auto. + econstructor. inv MC; simpl in H; simpl; auto. eauto. + erewrite stackspace_function_translated; eauto. constructor; auto. - (* assign *) +- (* assign *) exploit sel_expr_correct; eauto. intros [v' [A B]]. left; econstructor; split. econstructor; eauto. constructor; auto. apply set_var_lessdef; auto. - (* store *) +- (* store *) exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]]. exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]]. exploit Mem.storev_extends; eauto. intros [m2' [P Q]]. left; econstructor; split. eapply eval_store; eauto. constructor; auto. - (* Scall *) +- (* Scall *) exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit classify_call_correct; eauto. destruct (classify_call ge a) as [ | id | ef]. - (* indirect *) ++ (* indirect *) exploit sel_expr_correct; eauto. intros [vf' [A B]]. + exploit functions_translated; eauto. intros (fd' & U & V). left; econstructor; split. econstructor; eauto. econstructor; eauto. - eapply functions_translated; eauto. - apply sig_function_translated. + apply sig_function_translated; auto. constructor; auto. constructor; auto. - (* direct *) ++ (* direct *) intros [b [U V]]. + exploit functions_translated; eauto. intros (fd' & X & Y). left; econstructor; split. - econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. - eapply functions_translated; eauto. subst vf; auto. - apply sig_function_translated. + econstructor; eauto. + subst vf. econstructor; eauto. rewrite symbols_preserved; eauto. + apply sig_function_translated; auto. constructor; auto. constructor; auto. - (* turned into Sbuiltin *) ++ (* turned into Sbuiltin *) intros EQ. subst fd. - right; split. omega. split. auto. + right; split. simpl. omega. split. auto. econstructor; eauto. - (* Stailcall *) +- (* Stailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. + erewrite <- stackspace_function_translated in P by eauto. exploit sel_expr_correct; eauto. intros [vf' [A B]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. + exploit functions_translated; eauto. intros [fd' [E F]]. left; econstructor; split. exploit classify_call_correct; eauto. destruct (classify_call ge a) as [ | id | ef]; intros. - econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated. - destruct H2 as [b [U V]]. - econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply functions_translated; eauto. subst vf; auto. apply sig_function_translated. - econstructor; eauto. econstructor; eauto. eapply functions_translated; eauto. apply sig_function_translated. + econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. + destruct H2 as [b [U V]]. subst vf. inv B. + econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. apply sig_function_translated; auto. + econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) +- (* Sbuiltin *) exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. @@ -605,77 +798,96 @@ Proof. exact symbols_preserved. exact varinfo_preserved. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* Seq *) - left; econstructor; split. constructor. constructor; auto. constructor; auto. - (* Sifthenelse *) +- (* Seq *) + left; econstructor; split. + constructor. constructor; auto. constructor; auto. +- (* Sifthenelse *) exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. - left; exists (State (sel_function hf ge f) (if b then sel_stmt hf ge s1 else sel_stmt hf ge s2) k' sp e' m'); split. + left; exists (State f' (if b then x else x0) k' sp e' m'); split. econstructor; eauto. eapply eval_condexpr_of_expr; eauto. constructor; auto. destruct b; auto. - (* Sloop *) - left; econstructor; split. constructor. constructor; auto. constructor; auto. - (* Sblock *) +- (* Sloop *) + left; econstructor; split. constructor. constructor; auto. + constructor; auto. simpl; rewrite EQ; auto. +- (* Sblock *) left; econstructor; split. constructor. constructor; auto. constructor; auto. - (* Sexit seq *) - inv H7. left; econstructor; split. constructor. constructor; auto. - (* Sexit0 block *) - inv H7. left; econstructor; split. constructor. constructor; auto. - (* SexitS block *) - inv H7. left; econstructor; split. constructor. constructor; auto. - (* Sswitch *) +- (* Sexit seq *) + inv MC. left; econstructor; split. constructor. constructor; auto. +- (* Sexit0 block *) + inv MC. left; econstructor; split. constructor. constructor; auto. +- (* SexitS block *) + inv MC. left; econstructor; split. constructor. constructor; auto. +- (* Sswitch *) + inv H0; simpl in TS. ++ set (ct := compile_switch Int.modulus default cases) in *. + destruct (validate_switch Int.modulus default cases ct) eqn:VALID; inv TS. + exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. + left; econstructor; split. + econstructor. eapply sel_switch_int_correct; eauto. + constructor; auto. ++ set (ct := compile_switch Int64.modulus default cases) in *. + destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS. exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. - left; econstructor; split. econstructor; eauto. constructor; auto. - (* Sreturn None *) + left; econstructor; split. + econstructor. eapply sel_switch_long_correct; eauto. + constructor; auto. +- (* Sreturn None *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. + erewrite <- stackspace_function_translated in P by eauto. left; econstructor; split. econstructor. simpl; eauto. constructor; auto. apply call_cont_commut; auto. - (* Sreturn Some *) +- (* Sreturn Some *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. + erewrite <- stackspace_function_translated in P by eauto. exploit sel_expr_correct; eauto. intros [v' [A B]]. left; econstructor; split. econstructor; eauto. constructor; auto. apply call_cont_commut; auto. - (* Slabel *) +- (* Slabel *) left; econstructor; split. constructor. constructor; auto. - (* Sgoto *) +- (* Sgoto *) + assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')). + { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). - apply call_cont_commut; eauto. + apply call_cont_commut; eauto. eauto. rewrite H. - destruct (find_label lbl (sel_stmt hf ge (Cminor.fn_body f)) (call_cont k'0)) + destruct (find_label lbl (fn_body f') (call_cont k'0)) as [[s'' k'']|] eqn:?; intros; try contradiction. - destruct H0. + destruct H1. left; econstructor; split. econstructor; eauto. constructor; auto. - (* internal function *) +- (* internal function *) + monadInv TF. generalize EQ; intros TF; monadInv TF. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. left; econstructor; split. - econstructor; eauto. - constructor; auto. apply set_locals_lessdef. apply set_params_lessdef; auto. - (* external call *) + econstructor; simpl; eauto. + constructor; simpl; auto. apply set_locals_lessdef. apply set_params_lessdef; auto. +- (* external call *) + monadInv TF. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. - (* external call turned into a Sbuiltin *) +- (* external call turned into a Sbuiltin *) exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. constructor; auto. - (* return *) - inv H2. +- (* return *) + inv MC. left; econstructor; split. econstructor. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; split. omega. split. auto. constructor; auto. +- (* return of an external call turned into a Sbuiltin *) + right; split. simpl; omega. split. auto. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. Qed. @@ -684,11 +896,13 @@ Lemma sel_initial_states: exists R, initial_state tprog R /\ match_states S R. Proof. induction 1. + exploit function_ptr_translated; eauto. intros (f' & A & B). econstructor; split. econstructor. - apply Genv.init_mem_transf; eauto. - simpl. fold tge. rewrite symbols_preserved. eexact H0. - apply function_ptr_translated. eauto. + eapply Genv.init_mem_transf_partial; eauto. + simpl. fold tge. rewrite symbols_preserved. + erewrite transform_partial_program_main by eauto. eexact H0. + eauto. rewrite <- H2. apply sig_function_translated; auto. constructor; auto. constructor. apply Mem.extends_refl. Qed. @@ -697,7 +911,7 @@ Lemma sel_final_states: forall S R r, match_states S R -> Cminor.final_state S r -> final_state R r. Proof. - intros. inv H0. inv H. inv H3. inv H5. constructor. + intros. inv H0. inv H. inv MC. inv LD. constructor. Qed. End PRESERVATION. @@ -712,10 +926,9 @@ Theorem transf_program_correct: Proof. intros. unfold sel_program in H. destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate. - inv H. - eapply forward_simulation_opt. - apply symbols_preserved. - apply sel_initial_states. - apply sel_final_states. - apply sel_step_correct. apply helpers_correct_preserved. apply get_helpers_correct. auto. + apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). + eapply symbols_preserved; eauto. + apply sel_initial_states; auto. + apply sel_final_states; auto. + apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto. Qed. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 75dd9d2..92004a2 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1933,17 +1933,184 @@ Proof. destruct 1; simpl; auto with va. Qed. +(** Comparisons and variation intervals *) + +Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool := + let (lo, hi) := i in + match c with + | Ceq => if zlt n lo || zlt hi n then Maybe false else Btop + | Cne => Btop + | Clt => if zlt hi n then Maybe true else if zle n lo then Maybe false else Btop + | Cle => if zle hi n then Maybe true else if zlt n lo then Maybe false else Btop + | Cgt => if zlt n lo then Maybe true else if zle hi n then Maybe false else Btop + | Cge => if zle n lo then Maybe true else if zlt hi n then Maybe false else Btop + end. + +Definition zcmp (c: comparison) (n1 n2: Z) : bool := + match c with + | Ceq => zeq n1 n2 + | Cne => negb (zeq n1 n2) + | Clt => zlt n1 n2 + | Cle => zle n1 n2 + | Cgt => zlt n2 n1 + | Cge => zle n2 n1 + end. + +Lemma zcmp_intv_sound: + forall c i x n, + fst i <= x <= snd i -> + cmatch (Some (zcmp c x n)) (cmp_intv c i n). +Proof. + intros c [lo hi] x n; simpl; intros R. + destruct c; unfold zcmp, proj_sumbool. +- (* eq *) + destruct (zlt n lo). rewrite zeq_false by omega. constructor. + destruct (zlt hi n). rewrite zeq_false by omega. constructor. + constructor. +- (* ne *) + constructor. +- (* lt *) + destruct (zlt hi n). rewrite zlt_true by omega. constructor. + destruct (zle n lo). rewrite zlt_false by omega. constructor. + constructor. +- (* le *) + destruct (zle hi n). rewrite zle_true by omega. constructor. + destruct (zlt n lo). rewrite zle_false by omega. constructor. + constructor. +- (* gt *) + destruct (zlt n lo). rewrite zlt_true by omega. constructor. + destruct (zle hi n). rewrite zlt_false by omega. constructor. + constructor. +- (* ge *) + destruct (zle n lo). rewrite zle_true by omega. constructor. + destruct (zlt hi n). rewrite zle_false by omega. constructor. + constructor. +Qed. + +Lemma cmp_intv_None: + forall c i n, cmatch None (cmp_intv c i n). +Proof. + unfold cmp_intv; intros. destruct i as [lo hi]. + destruct c. +- (* eq *) + destruct (zlt n lo). constructor. destruct (zlt hi n); constructor. +- (* ne *) + constructor. +- (* lt *) + destruct (zlt hi n). constructor. destruct (zle n lo); constructor. +- (* le *) + destruct (zle hi n). constructor. destruct (zlt n lo); constructor. +- (* gt *) + destruct (zlt n lo). constructor. destruct (zle hi n); constructor. +- (* ge *) + destruct (zle n lo). constructor. destruct (zlt hi n); constructor. +Qed. + +Definition uintv (v: aval) : Z * Z := + match v with + | I n => (Int.unsigned n, Int.unsigned n) + | Uns n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned) + | _ => (0, Int.max_unsigned) + end. + +Lemma uintv_sound: + forall n v, vmatch (Vint n) v -> fst (uintv v) <= Int.unsigned n <= snd (uintv v). +Proof. + intros. inv H; simpl; try (apply Int.unsigned_range_2). +- omega. +- destruct (zlt n0 Int.zwordsize); simpl. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. rewrite Int.zero_ext_mod by omega. + exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. omega. ++ apply Int.unsigned_range_2. +Qed. + +Lemma cmpu_intv_sound: + forall valid c n1 v1 n2, + vmatch (Vint n1) v1 -> + cmatch (Val.cmpu_bool valid c (Vint n1) (Vint n2)) (cmp_intv c (uintv v1) (Int.unsigned n2)). +Proof. + intros. simpl. replace (Int.cmpu c n1 n2) with (zcmp c (Int.unsigned n1) (Int.unsigned n2)). + apply zcmp_intv_sound; apply uintv_sound; auto. + destruct c; simpl; auto. + unfold Int.ltu. destruct (zle (Int.unsigned n1) (Int.unsigned n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.ltu. destruct (zle (Int.unsigned n2) (Int.unsigned n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. +Qed. + +Lemma cmpu_intv_sound_2: + forall valid c n1 v1 n2, + vmatch (Vint n1) v1 -> + cmatch (Val.cmpu_bool valid c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (uintv v1) (Int.unsigned n2)). +Proof. + intros. rewrite <- Val.swap_cmpu_bool. apply cmpu_intv_sound; auto. +Qed. + +Definition sintv (v: aval) : Z * Z := + match v with + | I n => (Int.signed n, Int.signed n) + | Uns n => + if zlt n Int.zwordsize then (0, two_p n - 1) else (Int.min_signed, Int.max_signed) + | Sgn n => + if zlt n Int.zwordsize + then (let x := two_p (n-1) in (-x, x-1)) + else (Int.min_signed, Int.max_signed) + | _ => (Int.min_signed, Int.max_signed) + end. + +Lemma sintv_sound: + forall n v, vmatch (Vint n) v -> fst (sintv v) <= Int.signed n <= snd (sintv v). +Proof. + intros. inv H; simpl; try (apply Int.signed_range). +- omega. +- destruct (zlt n0 Int.zwordsize); simpl. ++ rewrite is_uns_zero_ext in H2. rewrite <- H2. + assert (Int.unsigned (Int.zero_ext n0 n) = Int.unsigned n mod two_p n0) by (apply Int.zero_ext_mod; omega). + exploit (Z_mod_lt (Int.unsigned n) (two_p n0)). apply two_p_gt_ZERO; auto. intros. + replace (Int.signed (Int.zero_ext n0 n)) with (Int.unsigned (Int.zero_ext n0 n)). + rewrite H. omega. + unfold Int.signed. rewrite zlt_true. auto. + assert (two_p n0 <= Int.half_modulus). + { change Int.half_modulus with (two_p (Int.zwordsize - 1)). + apply two_p_monotone. omega. } + omega. ++ apply Int.signed_range. +- destruct (zlt n0 (Int.zwordsize)); simpl. ++ rewrite is_sgn_sign_ext in H2 by auto. rewrite <- H2. + exploit (Int.sign_ext_range n0 n). omega. omega. ++ apply Int.signed_range. +Qed. + +Lemma cmp_intv_sound: + forall c n1 v1 n2, + vmatch (Vint n1) v1 -> + cmatch (Val.cmp_bool c (Vint n1) (Vint n2)) (cmp_intv c (sintv v1) (Int.signed n2)). +Proof. + intros. simpl. replace (Int.cmp c n1 n2) with (zcmp c (Int.signed n1) (Int.signed n2)). + apply zcmp_intv_sound; apply sintv_sound; auto. + destruct c; simpl; rewrite ? Int.eq_signed; auto. + unfold Int.lt. destruct (zle (Int.signed n1) (Int.signed n2)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. + unfold Int.lt. destruct (zle (Int.signed n2) (Int.signed n1)); [rewrite zlt_false|rewrite zlt_true]; auto; omega. +Qed. + +Lemma cmp_intv_sound_2: + forall c n1 v1 n2, + vmatch (Vint n1) v1 -> + cmatch (Val.cmp_bool c (Vint n2) (Vint n1)) (cmp_intv (swap_comparison c) (sintv v1) (Int.signed n2)). +Proof. + intros. rewrite <- Val.swap_cmp_bool. apply cmp_intv_sound; auto. +Qed. + (** Comparisons *) Definition cmpu_bool (c: comparison) (v w: aval) : abool := match v, w with | I i1, I i2 => Just (Int.cmpu c i1 i2) -(* there are cute things to do with Uns/Sgn compared against an integer *) | Ptr _, (I _ | Uns _ | Sgn _) => cmp_different_blocks c | (I _ | Uns _ | Sgn _), Ptr _ => cmp_different_blocks c | Ptr p1, Ptr p2 => pcmp c p1 p2 | Ptr p1, Ifptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) | Ifptr p1, Ptr p2 => club (pcmp c p1 p2) (cmp_different_blocks c) + | _, I i => club (cmp_intv c (uintv v) (Int.unsigned i)) (cmp_different_blocks c) + | I i, _ => club (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i)) (cmp_different_blocks c) | _, _ => Btop end. @@ -1961,22 +2128,28 @@ Proof. { intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } - unfold cmpu_bool; inv H; inv H0; + unfold cmpu_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_different_blocks_none, pcmp_none, - cmatch_lub_l, cmatch_lub_r, pcmp_sound. + cmatch_lub_l, cmatch_lub_r, pcmp_sound, + cmpu_intv_sound, cmpu_intv_sound_2, cmp_intv_None. - constructor. Qed. Definition cmp_bool (c: comparison) (v w: aval) : abool := match v, w with | I i1, I i2 => Just (Int.cmp c i1 i2) + | _, I i => cmp_intv c (sintv v) (Int.signed i) + | I i, _ => cmp_intv (swap_comparison c) (sintv w) (Int.signed i) | _, _ => Btop end. Lemma cmp_bool_sound: forall c v w x y, vmatch v x -> vmatch w y -> cmatch (Val.cmp_bool c v w) (cmp_bool c x y). Proof. - intros. inv H; try constructor; inv H0; constructor. + intros. + unfold cmp_bool; inversion H; subst; inversion H0; subst; + auto using cmatch_top, cmp_intv_sound, cmp_intv_sound_2, cmp_intv_None. +- constructor. Qed. Definition cmpf_bool (c: comparison) (v w: aval) : abool := diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6ee217c..702fcf2 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -765,8 +765,6 @@ let rec convertStmt ploc env s = | C.Scontinue -> Scontinue | C.Sswitch(e, s1) -> - if is_longlong env e.etyp then - unsupported "'switch' on an argument of type 'long long'"; let (init, cases) = groupSwitch (flattenSwitch s1) in if cases = [] then unsupported "ill-formed 'switch' statement"; @@ -810,7 +808,7 @@ and convertSwitch ploc env = function match Ceval.integer_expr env e with | None -> unsupported "'case' label is not a compile-time integer"; None - | Some v -> Some (convertInt v) + | Some v -> Some (Z.of_uint64 v) in LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env rem) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index eea1997..0e07093 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1980,10 +1980,8 @@ Definition do_step (w: world) (s: state) : list (trace * state) := do m' <- Mem.free_list m (blocks_of_env e); ret (Returnstate v' (call_cont k) m') | Kswitch1 sl k => - match v with - | Vint n => ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) - | _ => nil - end + do n <- sem_switch_arg v ty; + ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) | _ => nil end @@ -2089,7 +2087,6 @@ Proof with try (left; right; econstructor; eauto; fail). (* expression is a value *) rewrite (is_val_inv _ _ _ Heqo). destruct k; myinv... - destruct v; myinv... (* expression reduces *) intros. exploit list_in_map_inv; eauto. intros [[C rd] [A B]]. generalize (step_expr_sound e w r RV m). unfold reducts_ok. intros [P Q]. @@ -2189,6 +2186,7 @@ Proof with (unfold ret; auto with coqlib). rewrite H0... rewrite H0; rewrite H1... rewrite H1. red in H0. destruct k; try contradiction... + rewrite H0... destruct H0; subst x... rewrite H0... diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index d9fb650..40206d3 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -111,7 +111,7 @@ Inductive statement : Type := with labeled_statements : Type := (**r cases of a [switch] *) | LSnil: labeled_statements - | LScons: option int -> statement -> labeled_statements -> labeled_statements. + | LScons: option Z -> statement -> labeled_statements -> labeled_statements. (**r [None] is [default], [Some x] is [case x] *) (** The C loops are derived forms. *) @@ -312,14 +312,14 @@ Fixpoint select_switch_default (sl: labeled_statements): labeled_statements := | LScons (Some i) s sl' => select_switch_default sl' end. -Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements := +Fixpoint select_switch_case (n: Z) (sl: labeled_statements): option labeled_statements := match sl with | LSnil => None | LScons None s sl' => select_switch_case n sl' - | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl' end. -Definition select_switch (n: int) (sl: labeled_statements): labeled_statements := +Definition select_switch (n: Z) (sl: labeled_statements): labeled_statements := match select_switch_case n sl with | Some sl' => sl' | None => select_switch_default sl @@ -614,8 +614,9 @@ Inductive step: state -> trace -> state -> Prop := step (State f Sskip k e le m) E0 (Returnstate Vundef k m') - | step_switch: forall f a sl k e le m n, - eval_expr e le m a (Vint n) -> + | step_switch: forall f a sl k e le m v n, + eval_expr e le m a v -> + sem_switch_arg v (typeof a) = Some n -> step (State f (Sswitch a sl) k e le m) E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e le m) | step_skip_break_switch: forall f x k e le m, diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index f7a0e18..d61e4ee 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -151,8 +151,9 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> exec_stmt e le2 m2 (Sloop s1 s2) t3 le3 m3 out -> exec_stmt e le m (Sloop s1 s2) (t1**t2**t3) le3 m3 out - | exec_Sswitch: forall e le m a t n sl le1 m1 out, - eval_expr ge e le m a (Vint n) -> + | exec_Sswitch: forall e le m a t v n sl le1 m1 out, + eval_expr ge e le m a v -> + sem_switch_arg v (typeof a) = Some n -> exec_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t le1 m1 out -> exec_stmt e le m (Sswitch a sl) t le1 m1 (outcome_switch out) @@ -220,8 +221,9 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro exec_stmt e le1 m1 s2 t2 le2 m2 Out_normal -> execinf_stmt e le2 m2 (Sloop s1 s2) t3 -> execinf_stmt e le m (Sloop s1 s2) (t1***t2***t3) - | execinf_Sswitch: forall e le m a t n sl, - eval_expr ge e le m a (Vint n) -> + | execinf_Sswitch: forall e le m a t v n sl, + eval_expr ge e le m a v -> + sem_switch_arg v (typeof a) = Some n -> execinf_stmt e le m (seq_of_labeled_statement (select_switch n sl)) t -> execinf_stmt e le m (Sswitch a sl) t @@ -427,7 +429,7 @@ Proof. auto. (* switch *) - destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. + destruct (H2 f (Kswitch k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_normal => State f Sskip k e le1 m1 diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index ae6ec56..82509b0 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -138,7 +138,7 @@ Fixpoint shift_exit (e: exit_env) (n: nat) {struct e} : nat := | true :: e', S m => S (shift_exit e' m) end. -Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (int * nat) * nat := +Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (Z * nat) * nat := match ls with | LSnil => (nil, k) @@ -193,10 +193,10 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) OK (Sblock ts) | Csharpminor.Sexit n => OK (Sexit (shift_exit xenv n)) - | Csharpminor.Sswitch e ls => + | Csharpminor.Sswitch long e ls => let (tbl, dfl) := switch_table ls O in do te <- transl_expr cenv e; - transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te tbl dfl) + transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch long te tbl dfl) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 3bf790c..7cb604e 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1697,15 +1697,15 @@ Proof. - auto. - destruct (switch_table sl (S base)) as [tbl1 dfl1] eqn:ST. destruct o; simpl. - rewrite Int.eq_sym. destruct (Int.eq i i0). + rewrite dec_eq_sym. destruct (zeq i z). exists O; split; auto. constructor. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. auto. specialize (IHsl (S base) dfl). rewrite ST in IHsl. simpl in *. destruct (select_switch_case i sl). - destruct IHsl as (n & P & Q). exists (S n); split. constructor; auto. omega. + destruct IHsl as (x & P & Q). exists (S x); split. constructor; auto. omega. auto. Qed. @@ -2107,7 +2107,8 @@ Opaque PTree.set. (* switch *) simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - inv VINJ. + assert (SA: switch_argument islong tv n). + { inv H0; inv VINJ; constructor. } exploit switch_descent; eauto. intros [k1 [A B]]. exploit switch_ascent; eauto. eapply (switch_table_select n). rewrite STBL; simpl. intros [k2 [C D]]. diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index ff43cbd..a5d4c66 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -936,7 +936,7 @@ Definition sem_cmp (c:comparison) (** ** Function applications *) -Inductive classify_fun_cases : Type:= +Inductive classify_fun_cases : Type := | fun_case_f (targs: typelist) (tres: type) (cc: calling_convention) (**r (pointer to) function *) | fun_default. @@ -947,6 +947,30 @@ Definition classify_fun (ty: type) := | _ => fun_default end. +(** ** Argument of a [switch] statement *) + +Inductive classify_switch_cases : Type := + | switch_case_i + | switch_case_l + | switch_default. + +Definition classify_switch (ty: type) := + match ty with + | Tint _ _ _ => switch_case_i + | Tlong _ _ => switch_case_l + | _ => switch_default + end. + +Definition sem_switch_arg (v: val) (ty: type): option Z := + match classify_switch ty with + | switch_case_i => + match v with Vint n => Some(Int.unsigned n) | _ => None end + | switch_case_l => + match v with Vlong n => Some(Int64.unsigned n) | _ => None end + | switch_default => + None + end. + (** * Combined semantics of unary and binary operators *) Definition sem_unary_operation diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a43ee00..55c37c9 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -155,14 +155,14 @@ Fixpoint select_switch_default (sl: labeled_statements): labeled_statements := | LScons (Some i) s sl' => select_switch_default sl' end. -Fixpoint select_switch_case (n: int) (sl: labeled_statements): option labeled_statements := +Fixpoint select_switch_case (n: Z) (sl: labeled_statements): option labeled_statements := match sl with | LSnil => None | LScons None s sl' => select_switch_case n sl' - | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl' end. -Definition select_switch (n: int) (sl: labeled_statements): labeled_statements := +Definition select_switch (n: Z) (sl: labeled_statements): labeled_statements := match select_switch_case n sl with | Some sl' => sl' | None => select_switch_default sl @@ -715,8 +715,9 @@ Inductive sstep: state -> trace -> state -> Prop := | step_switch: forall f x sl k e m, sstep (State f (Sswitch x sl) k e m) E0 (ExprState f x (Kswitch1 sl k) e m) - | step_expr_switch: forall f n ty sl k e m, - sstep (ExprState f (Eval (Vint n) ty) (Kswitch1 sl k) e m) + | step_expr_switch: forall f ty sl k e m v n, + sem_switch_arg v ty = Some n -> + sstep (ExprState f (Eval v ty) (Kswitch1 sl k) e m) E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) | step_skip_break_switch: forall f x k e m, x = Sskip \/ x = Sbreak -> diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index d37fa81..c34b10a 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -21,6 +21,7 @@ Require Import Values. Require Import Memory. Require Import Events. Require Import Globalenvs. +Require Import Switch. Require Cminor. Require Import Smallstep. @@ -67,14 +68,14 @@ Inductive stmt : Type := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sswitch: expr -> lbl_stmt -> stmt + | Sswitch: bool -> expr -> lbl_stmt -> stmt | Sreturn: option expr -> stmt | Slabel: label -> stmt -> stmt | Sgoto: label -> stmt with lbl_stmt : Type := | LSnil: lbl_stmt - | LScons: option int -> stmt -> lbl_stmt -> lbl_stmt. + | LScons: option Z -> stmt -> lbl_stmt -> lbl_stmt. (** Functions are composed of a return type, a list of parameter names, a list of local variables with their sizes, a list of temporary variables, @@ -191,14 +192,14 @@ Fixpoint select_switch_default (sl: lbl_stmt): lbl_stmt := | LScons (Some i) s sl' => select_switch_default sl' end. -Fixpoint select_switch_case (n: int) (sl: lbl_stmt): option lbl_stmt := +Fixpoint select_switch_case (n: Z) (sl: lbl_stmt): option lbl_stmt := match sl with | LSnil => None | LScons None s sl' => select_switch_case n sl' - | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl' + | LScons (Some c) s sl' => if zeq c n then Some sl else select_switch_case n sl' end. -Definition select_switch (n: int) (sl: lbl_stmt): lbl_stmt := +Definition select_switch (n: Z) (sl: lbl_stmt): lbl_stmt := match select_switch_case n sl with | Some sl' => sl' | None => select_switch_default sl @@ -230,7 +231,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont) find_label lbl s1 (Kseq (Sloop s1) k) | Sblock s1 => find_label lbl s1 (Kblock k) - | Sswitch a sl => + | Sswitch long a sl => find_label_ls lbl sl k | Slabel lbl' s' => if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k @@ -423,9 +424,10 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sexit (S n)) (Kblock k) e le m) E0 (State f (Sexit n) k e le m) - | step_switch: forall f a cases k e le m n, - eval_expr e le m a (Vint n) -> - step (State f (Sswitch a cases) k e le m) + | step_switch: forall f islong a cases k e le m v n, + eval_expr e le m a v -> + switch_argument islong v n -> + step (State f (Sswitch islong a cases) k e le m) E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e le m) | step_return_0: forall f k e le m m', diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cedfd8b..3b23a54 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -589,7 +589,11 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) | Clight.Sswitch a sl => do ta <- transl_expr a; do tsl <- transl_lbl_stmt tyret 0%nat (S ncnt) sl; - OK (Sblock (Sswitch ta tsl)) + match classify_switch (typeof a) with + | switch_case_i => OK (Sblock (Sswitch false ta tsl)) + | switch_case_l => OK (Sblock (Sswitch true ta tsl)) + | switch_default => Error(msg "Cshmgen.transl_stmt(switch)") + end | Clight.Slabel lbl s => do ts <- transl_statement tyret nbrk ncnt s; OK (Slabel lbl ts) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index a977e0f..fdf5b06 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -118,7 +118,7 @@ Proof. { induction sl; simpl; intros. inv H; auto. - monadInv H; simpl. destruct o. destruct (Int.eq i n). + monadInv H; simpl. destruct o. destruct (zeq z n). econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. apply IHsl; auto. apply IHsl; auto. @@ -1188,6 +1188,9 @@ Proof. (* return *) simpl in TR. destruct o; monadInv TR. auto. auto. (* switch *) + assert (exists b, ts = Sblock (Sswitch b x x0)). + { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. } + destruct H as [b EQ3]; rewrite EQ3; simpl. eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. (* label *) destruct (ident_eq lbl l). @@ -1394,10 +1397,15 @@ Proof. (* switch *) monadInv TR. + assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n). + { unfold sem_switch_arg in H0. + destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto; + destruct v; inv H0; constructor. } + destruct E as (b & A & B). subst ts. exploit transl_expr_correct; eauto. intro EV. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. - apply plus_one. econstructor. eauto. traceEq. + apply plus_one. econstructor; eauto. traceEq. econstructor; eauto. apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. constructor. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index b6d1c87..676f3fa 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -1881,8 +1881,9 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2 ** t3 ** t4) m4 out - | exec_Sswitch: forall e m a sl t1 m1 n t2 m2 out, - eval_expression e m a t1 m1 (Vint n) -> + | exec_Sswitch: forall e m a sl t1 m1 v n t2 m2 out, + eval_expression e m a t1 m1 v -> + sem_switch_arg v (typeof a) = Some n -> exec_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 m2 out -> exec_stmt e m (Sswitch a sl) (t1 ** t2) m2 (outcome_switch out) @@ -2104,8 +2105,9 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := | execinf_Sswitch_expr: forall e m a sl t1, evalinf_expr e m RV a t1 -> execinf_stmt e m (Sswitch a sl) t1 - | execinf_Sswitch_body: forall e m a sl t1 m1 n t2, - eval_expression e m a t1 m1 (Vint n) -> + | execinf_Sswitch_body: forall e m a sl t1 m1 v n t2, + eval_expression e m a t1 m1 v -> + sem_switch_arg v (typeof a) = Some n -> execinf_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 -> execinf_stmt e m (Sswitch a sl) (t1***t2) @@ -2573,7 +2575,7 @@ Proof. auto. (* switch *) - destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]]. + destruct (H3 f (Kswitch2 k)) as [S1 [A1 B1]]. set (S2 := match out with | Out_normal => State f Sskip k e m2 @@ -2584,7 +2586,7 @@ Proof. exists S2; split. eapply star_left. right; eapply step_switch. eapply star_trans. apply H0. - eapply star_left. right; eapply step_expr_switch. + eapply star_left. right; eapply step_expr_switch. eauto. eapply star_trans. eexact A1. unfold S2; inv B1. apply star_one. right; constructor. auto. @@ -3013,7 +3015,7 @@ Proof. eapply forever_N_plus. eapply plus_left. right; constructor. eapply star_right. eapply eval_expression_to_steps; eauto. - right; constructor. + right; constructor. eauto. reflexivity. reflexivity. eapply COS; eauto. traceEq. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index ea1bd86..a926bc3 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -166,7 +166,7 @@ Inductive statement : Type := with labeled_statements : Type := (**r cases of a [switch] *) | LSnil: labeled_statements - | LScons: option int -> statement -> labeled_statements -> labeled_statements. + | LScons: option Z -> statement -> labeled_statements -> labeled_statements. (**r [None] is [default], [Some x] is [case x] *) (** ** Functions *) diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 0a77b19..c907f77 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1003,7 +1003,7 @@ Proof. end). { induction 1; simpl; intros. auto. - destruct c; auto. destruct (Int.eq i n); auto. + destruct c; auto. destruct (zeq z n); auto. econstructor; split; eauto. constructor; auto. } intros. unfold Csem.select_switch, select_switch. specialize (CASE n ls tls H). @@ -2113,7 +2113,7 @@ Proof. left; eapply plus_left. constructor. apply push_seq. traceEq. econstructor; eauto. constructor; auto. (* expr switch *) - inv H7. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + inv H8. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left; eapply plus_two. constructor. econstructor; eauto. traceEq. econstructor; eauto. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 6024de4..67a7e62 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1798,7 +1798,7 @@ Proof. induction ls; simpl; intros; monadInv H; simpl. auto. destruct o. - destruct (Int.eq i n). + destruct (zeq z n). econstructor; split; eauto. simpl; rewrite EQ, EQ1; auto. apply IHls. auto. apply IHls. auto. @@ -1840,7 +1840,7 @@ Proof. { induction ls; simpl; intros. discriminate. - destruct o. destruct (Int.eq i n). inv H0. auto. eauto with compat. + destruct o. destruct (zeq z n). inv H0. auto. eauto with compat. eauto with compat. } intros. specialize (CASE ls). unfold select_switch. @@ -2104,8 +2104,12 @@ Proof. intros. apply match_cont_change_cenv with (cenv_for f); auto. eapply match_cont_free_env; eauto. (* switch *) - exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. inv B. + exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. econstructor; split. apply plus_one. econstructor; eauto. + rewrite typeof_simpl_expr. instantiate (1 := n). + unfold sem_switch_arg in *; + destruct (classify_switch (typeof a)); try discriminate; + inv B; inv H0; auto. econstructor; eauto. erewrite simpl_seq_of_labeled_statement. reflexivity. eapply simpl_select_switch; eauto. diff --git a/common/Switch.v b/common/Switch.v index 3e25851..4723f50 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -20,45 +20,27 @@ Require Import EqNat. Require Import Coqlib. Require Import Maps. Require Import Integers. - -Module IntIndexed <: INDEXED_TYPE. - - Definition t := int. - - Definition index (n: int) : positive := - match Int.unsigned n with - | Z0 => xH - | Zpos p => xO p - | Zneg p => xI p (**r never happens *) - end. - - Lemma index_inj: forall n m, index n = index m -> n = m. - Proof. - unfold index; intros. - rewrite <- (Int.repr_unsigned n). rewrite <- (Int.repr_unsigned m). - f_equal. - destruct (Int.unsigned n); destruct (Int.unsigned m); congruence. - Qed. - - Definition eq := Int.eq_dec. - -End IntIndexed. - -Module IntMap := IMap(IntIndexed). +Require Import Values. (** A multi-way branch is composed of a list of (key, action) pairs, plus a default action. *) -Definition table : Type := list (int * nat). +Definition table : Type := list (Z * nat). -Fixpoint switch_target (n: int) (dfl: nat) (cases: table) +Fixpoint switch_target (n: Z) (dfl: nat) (cases: table) {struct cases} : nat := match cases with | nil => dfl | (key, action) :: rem => - if Int.eq n key then action else switch_target n dfl rem + if zeq n key then action else switch_target n dfl rem end. +Inductive switch_argument: bool -> val -> Z -> Prop := + | switch_argument_32: forall i, + switch_argument false (Vint i) (Int.unsigned i) + | switch_argument_64: forall i, + switch_argument true (Vlong i) (Int64.unsigned i). + (** Multi-way branches are translated to comparison trees. Each node of the tree performs either - an equality against one of the keys; @@ -66,21 +48,27 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table) - 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 - | CTjumptable: int -> int -> list nat -> comptree -> comptree. + | CTaction (act: nat) + | CTifeq (key: Z) (act: nat) (cne: comptree) + | CTiflt (key: Z) (clt: comptree) (cge: comptree) + | CTjumptable (ofs: Z) (sz: Z) (acts: list nat) (cother: comptree). + +Section COMPTREE. -Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat := +Variable modulus: Z. +Hypothesis modulus_pos: modulus > 0. + +Fixpoint comptree_match (n: Z) (t: comptree) {struct t}: option nat := match t with | CTaction act => Some act | CTifeq key act t' => - if Int.eq n key then Some act else comptree_match n t' + if zeq 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 + if zlt 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.unsigned (Int.sub n ofs)) + let delta := (n - ofs) mod modulus in + if zlt delta sz + then list_nth_z tbl (delta mod Int.modulus) else comptree_match n t' end. @@ -91,36 +79,36 @@ Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat := and prove correct Coq functions that take a table and a comparison tree, and check that their semantics are equivalent. *) -Fixpoint split_lt (pivot: int) (cases: table) +Fixpoint split_lt (pivot: Z) (cases: table) {struct cases} : table * table := match cases with | nil => (nil, nil) | (key, act) :: rem => let (l, r) := split_lt pivot rem in - if Int.ltu key pivot + if zlt key pivot then ((key, act) :: l, r) else (l, (key, act) :: r) end. -Fixpoint split_eq (pivot: int) (cases: table) +Fixpoint split_eq (pivot: Z) (cases: table) {struct cases} : option nat * table := match cases with | nil => (None, nil) | (key, act) :: rem => let (same, others) := split_eq pivot rem in - if Int.eq key pivot + if zeq key pivot then (Some act, others) else (same, (key, act) :: others) end. -Fixpoint split_between (dfl: nat) (ofs sz: int) (cases: table) - {struct cases} : IntMap.t nat * table := +Fixpoint split_between (dfl: nat) (ofs sz: Z) (cases: table) + {struct cases} : ZMap.t nat * table := match cases with - | nil => (IntMap.init dfl, nil) + | nil => (ZMap.init dfl, nil) | (key, act) :: rem => let (inside, outside) := split_between dfl ofs sz rem in - if Int.ltu (Int.sub key ofs) sz - then (IntMap.set key act inside, outside) + if zlt ((key - ofs) mod modulus) sz + then (ZMap.set key act inside, outside) else (inside, (key, act) :: outside) end. @@ -130,13 +118,13 @@ Definition refine_low_bound (v lo: Z) := Definition refine_high_bound (v hi: Z) := if zeq v hi then hi - 1 else hi. -Fixpoint validate_jumptable (cases: IntMap.t nat) - (tbl: list nat) (n: int) {struct tbl} : bool := +Fixpoint validate_jumptable (cases: ZMap.t nat) + (tbl: list nat) (n: Z) {struct tbl} : bool := match tbl with | nil => true | act :: rem => - beq_nat act (IntMap.get n cases) - && validate_jumptable cases rem (Int.add n Int.one) + beq_nat act (ZMap.get n cases) + && validate_jumptable cases rem (Zsucc n) end. Fixpoint validate (default: nat) (cases: table) (t: comptree) @@ -147,211 +135,217 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree) | nil => beq_nat act default | (key1, act1) :: _ => - zeq (Int.unsigned key1) lo && zeq lo hi && beq_nat act act1 + zeq key1 lo && zeq lo hi && beq_nat act act1 end | CTifeq pivot act t' => + zle 0 pivot && zlt pivot modulus && match split_eq pivot cases with | (None, _) => false | (Some act', others) => beq_nat act act' && validate default others t' - (refine_low_bound (Int.unsigned pivot) lo) - (refine_high_bound (Int.unsigned pivot) hi) + (refine_low_bound pivot lo) + (refine_high_bound pivot hi) end | CTiflt pivot t1 t2 => + zle 0 pivot && zlt pivot modulus && match split_lt pivot cases with | (lcases, rcases) => - validate default lcases t1 lo (Int.unsigned pivot - 1) - && validate default rcases t2 (Int.unsigned pivot) hi + validate default lcases t1 lo (pivot - 1) + && validate default rcases t2 pivot hi end | CTjumptable ofs sz tbl t' => let tbl_len := list_length_z tbl in + zle 0 ofs && zle 0 sz && zlt (ofs + sz) modulus && + zle sz tbl_len && zlt sz Int.modulus && match split_between default ofs sz cases with | (inside, outside) => - zle (Int.unsigned sz) tbl_len - && zle tbl_len Int.max_signed - && validate_jumptable inside tbl ofs + validate_jumptable inside tbl ofs && validate default outside t' lo hi end end. Definition validate_switch (default: nat) (cases: table) (t: comptree) := - validate default cases t 0 Int.max_unsigned. + validate default cases t 0 (modulus - 1). + +(** Structural properties checked by validation *) + +Inductive wf_comptree: comptree -> Prop := + | wf_action: forall act, + wf_comptree (CTaction act) + | wf_ifeq: forall key act cne, + 0 <= key < modulus -> wf_comptree cne -> wf_comptree (CTifeq key act cne) + | wf_iflt: forall key clt cge, + 0 <= key < modulus -> wf_comptree clt -> wf_comptree cge -> wf_comptree (CTiflt key clt cge) + | wf_jumptable: forall ofs sz acts cother, + 0 <= ofs < modulus -> 0 <= sz < modulus -> + wf_comptree cother -> + wf_comptree (CTjumptable ofs sz acts cother). + +Lemma validate_wf: + forall default t cases lo hi, + validate default cases t lo hi = true -> + wf_comptree t. +Proof. + induction t; simpl; intros; InvBooleans. +- constructor. +- destruct (split_eq key cases) as [[act'|] others]; try discriminate; InvBooleans. + constructor; eauto. +- destruct (split_lt key cases) as [lc rc]; InvBooleans. + constructor; eauto. +- destruct (split_between default ofs sz cases) as [ins out]; InvBooleans. + constructor; eauto; omega. +Qed. -(** Correctness proof for validation. *) +(** Semantic correctness proof for validation. *) Lemma split_eq_prop: forall v default n cases optact cases', split_eq n cases = (optact, cases') -> switch_target v default cases = - (if Int.eq v n + (if zeq v n then match optact with Some act => act | None => default end else switch_target v default cases'). Proof. induction cases; simpl; intros until cases'. - intros. inversion H; subst. simpl. - destruct (Int.eq v n); auto. - destruct a as [key act]. - case_eq (split_eq n cases). intros same other SEQ. - rewrite (IHcases _ _ SEQ). - predSpec Int.eq Int.eq_spec key n; intro EQ; inversion EQ; simpl. - subst n. destruct (Int.eq v key). auto. auto. - predSpec Int.eq Int.eq_spec v key. - subst v. predSpec Int.eq Int.eq_spec key n. congruence. auto. - auto. +- intros. inv H. simpl. destruct (zeq v n); auto. +- destruct a as [key act]. + destruct (split_eq n cases) as [same other] eqn:SEQ. + rewrite (IHcases same other) by auto. + destruct (zeq key n); intros EQ; inv EQ. ++ destruct (zeq v n); auto. ++ simpl. destruct (zeq v key). + * subst v. rewrite zeq_false by auto. auto. + * auto. Qed. Lemma split_lt_prop: forall v default n cases lcases rcases, split_lt n cases = (lcases, rcases) -> switch_target v default cases = - (if Int.ltu v n + (if zlt v n then switch_target v default lcases else switch_target v default rcases). Proof. induction cases; intros until rcases; simpl. - intro. inversion H; subst. simpl. - destruct (Int.ltu v n); auto. - destruct a as [key act]. - case_eq (split_lt n cases). intros lc rc SEQ. - rewrite (IHcases _ _ SEQ). - case_eq (Int.ltu key n); intros; inv H0; simpl. - predSpec Int.eq Int.eq_spec v key. - subst v. rewrite H. auto. - auto. - predSpec Int.eq Int.eq_spec v key. - subst v. rewrite H. auto. - auto. +- intros. inv H. simpl. destruct (zlt v n); auto. +- destruct a as [key act]. + destruct (split_lt n cases) as [lc rc] eqn:SEQ. + rewrite (IHcases lc rc) by auto. + destruct (zlt key n); intros EQ; inv EQ; simpl. ++ destruct (zeq v key). rewrite zlt_true by omega. auto. auto. ++ destruct (zeq v key). rewrite zlt_false by omega. auto. auto. Qed. Lemma split_between_prop: forall v default ofs sz cases inside outside, split_between default ofs sz cases = (inside, outside) -> switch_target v default cases = - (if Int.ltu (Int.sub v ofs) sz - then IntMap.get v inside + (if zlt ((v - ofs) mod modulus) sz + then ZMap.get v inside else switch_target v default outside). Proof. induction cases; intros until outside; simpl; intros SEQ. -- inv SEQ. destruct (Int.ltu (Int.sub v ofs) sz); auto. rewrite IntMap.gi. auto. -- destruct a as [key act]. +- inv SEQ. rewrite ZMap.gi. simpl. destruct (zlt ((v - ofs) mod modulus) sz); auto. +- destruct a as [key act]. destruct (split_between default ofs sz cases) as [ins outs]. - erewrite IHcases; eauto. - destruct (Int.ltu (Int.sub key ofs) sz) eqn:LT; inv SEQ. - + predSpec Int.eq Int.eq_spec v key. - subst v. rewrite LT. rewrite IntMap.gss. auto. - destruct (Int.ltu (Int.sub v ofs) sz). - rewrite IntMap.gso; auto. - auto. - + simpl. destruct (Int.ltu (Int.sub v ofs) sz) eqn:LT'. - rewrite Int.eq_false. auto. congruence. - auto. + erewrite IHcases; eauto. + destruct (zlt ((key - ofs) mod modulus) sz); inv SEQ. ++ rewrite ZMap.gsspec. unfold ZIndexed.eq. + destruct (zeq v key). + subst v. rewrite zlt_true by auto. auto. + auto. ++ simpl. destruct (zeq v key). + subst v. rewrite zlt_false by auto. auto. + auto. Qed. Lemma validate_jumptable_correct_rec: forall cases tbl base v, validate_jumptable cases tbl base = true -> - 0 <= Int.unsigned v < list_length_z tbl -> - list_nth_z tbl (Int.unsigned v) = Some(IntMap.get (Int.add base v) cases). + 0 <= v < list_length_z tbl -> + list_nth_z tbl v = Some(ZMap.get (base + v) cases). 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 H1)). clear H1. intro. subst a. - destruct (zeq (Int.unsigned v) 0). - unfold Int.add. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_unsigned. auto. - assert (Int.unsigned (Int.sub v Int.one) = Int.unsigned v - 1). - unfold Int.sub. change (Int.unsigned Int.one) with 1. - apply Int.unsigned_repr. split. omega. - generalize (Int.unsigned_range_2 v). 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 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. - rewrite Int.add_neg_zero; auto. + induction tbl; simpl; intros. +- unfold list_length_z in H0. simpl in H0. omegaContradiction. +- InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. + destruct (zeq v 0). + + replace (base + v) with base by omega. congruence. + + replace (base + v) with (Z.succ base + Z.pred v) by omega. + apply IHtbl. auto. omega. Qed. Lemma validate_jumptable_correct: forall cases tbl ofs v sz, validate_jumptable cases tbl ofs = true -> - Int.ltu (Int.sub v ofs) sz = true -> - Int.unsigned sz <= list_length_z tbl -> - list_nth_z tbl (Int.unsigned (Int.sub v ofs)) = Some(IntMap.get v cases). + (v - ofs) mod modulus < sz -> + 0 <= sz -> 0 <= ofs -> ofs + sz < modulus -> + 0 <= v < modulus -> + sz <= list_length_z tbl -> + list_nth_z tbl ((v - ofs) mod modulus) = Some(ZMap.get v cases). Proof. intros. - exploit Int.ltu_inv; eauto. intros. - rewrite (validate_jumptable_correct_rec cases 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. + rewrite (validate_jumptable_correct_rec cases tbl ofs); auto. +- f_equal. f_equal. rewrite Zmod_small. omega. + destruct (zle ofs v). omega. + assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus). + { rewrite Zmod_small. omega. omega. } + rewrite Z_mod_plus in M by auto. rewrite M in H0. omega. +- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. Qed. Lemma validate_correct_rec: - forall default v t cases lo hi, + forall default v, + 0 <= v < modulus -> + forall t cases lo hi, validate default cases t lo hi = true -> - lo <= Int.unsigned v <= hi -> + lo <= v <= hi -> comptree_match v t = Some (switch_target v default cases). Proof. -Opaque Int.sub. - induction t; simpl; intros until hi. - (* base case *) + intros default v VRANGE. induction t; simpl; intros until hi. +- (* base case *) destruct cases as [ | [key1 act1] cases1]; intros. - replace n with default. reflexivity. - symmetry. apply beq_nat_eq. auto. - destruct (andb_prop _ _ H). destruct (andb_prop _ _ H1). clear H H1. - assert (Int.unsigned key1 = lo). eapply proj_sumbool_true; eauto. - assert (lo = hi). eapply proj_sumbool_true; eauto. - assert (Int.unsigned v = Int.unsigned key1). omega. - replace n with act1. - simpl. unfold Int.eq. rewrite H5. rewrite zeq_true. auto. - symmetry. apply beq_nat_eq. auto. - (* eq node *) - case_eq (split_eq i cases). intros optact cases' EQ. - destruct optact as [ act | ]. 2: congruence. - intros. destruct (andb_prop _ _ H). clear H. ++ apply beq_nat_true in H. subst act. reflexivity. ++ InvBooleans. apply beq_nat_true in H2. subst. simpl. + destruct (zeq v hi). auto. omegaContradiction. +- (* eq node *) + destruct (split_eq key cases) as [optact others] eqn:EQ. intros. + destruct optact as [act1|]; InvBooleans; try discriminate. + apply beq_nat_true in H. rewrite (split_eq_prop v default _ _ _ _ EQ). - predSpec Int.eq Int.eq_spec v i. - f_equal. apply beq_nat_eq; auto. - eapply IHt. eauto. - assert (Int.unsigned v <> Int.unsigned i). - rewrite <- (Int.repr_unsigned v) in H. - rewrite <- (Int.repr_unsigned i) in H. - congruence. - split. - unfold refine_low_bound. destruct (zeq (Int.unsigned i) lo); omega. - unfold refine_high_bound. destruct (zeq (Int.unsigned i) hi); omega. - (* lt node *) - case_eq (split_lt i cases). intros lcases rcases EQ V RANGE. - destruct (andb_prop _ _ V). clear V. - rewrite (split_lt_prop v default _ _ _ _ EQ). - unfold Int.ltu. destruct (zlt (Int.unsigned v) (Int.unsigned i)). + destruct (zeq v key). + + congruence. + + eapply IHt; eauto. + unfold refine_low_bound, refine_high_bound. split. + destruct (zeq key lo); omega. + destruct (zeq key hi); omega. +- (* lt node *) + destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans. + rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). eapply IHt1. eauto. omega. eapply IHt2. eauto. omega. - (* jumptable node *) - case_eq (split_between default 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. +- (* jumptable node *) + destruct (split_between default ofs sz cases) as [ins outs] eqn:EQ; intros; InvBooleans. rewrite (split_between_prop v _ _ _ _ _ _ EQ). - case_eq (Int.ltu (Int.sub v i) i0); intros. - eapply validate_jumptable_correct; eauto. - eapply proj_sumbool_true; eauto. + assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega). + destruct (zlt ((v - ofs) mod modulus) sz). + rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto. eapply IHt; eauto. Qed. Definition table_tree_agree (default: nat) (cases: table) (t: comptree) : Prop := - forall v, comptree_match v t = Some(switch_target v default cases). + forall v, 0 <= v < modulus -> comptree_match v t = Some(switch_target v default cases). Theorem validate_switch_correct: forall default t cases, validate_switch default cases t = true -> - table_tree_agree default cases t. + wf_comptree t /\ table_tree_agree default cases t. Proof. - unfold validate_switch, table_tree_agree; intros. - eapply validate_correct_rec; eauto. - apply Int.unsigned_range_2. + unfold validate_switch, table_tree_agree; split. + eapply validate_wf; eauto. + intros; eapply validate_correct_rec; eauto. omega. Qed. + +End COMPTREE. diff --git a/common/Switchaux.ml b/common/Switchaux.ml new file mode 100644 index 0000000..15480ae --- /dev/null +++ b/common/Switchaux.ml @@ -0,0 +1,99 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Datatypes +open Camlcoq +open Switch + +(* Compiling a switch table into a decision tree *) + +module ZSet = Set.Make(Z) + +let normalize_table tbl = + let rec norm keys accu = function + | [] -> (accu, keys) + | (key, act) :: rem -> + if ZSet.mem key keys + then norm keys accu rem + else norm (ZSet.add key keys) ((key, act) :: accu) rem + in norm ZSet.empty [] tbl + +let compile_switch_as_tree modulus default tbl = + let sw = Array.of_list tbl in + Array.stable_sort (fun (n1, _) (n2, _) -> Z.compare n1 n2) sw; + let rec build lo hi minval maxval = + match hi - lo with + | 0 -> + CTaction default + | 1 -> + let (key, act) = sw.(lo) in + if Z.sub maxval minval = Z.zero + then CTaction act + else CTifeq(key, act, CTaction default) + | 2 -> + let (key1, act1) = sw.(lo) + and (key2, act2) = sw.(lo+1) in + CTifeq(key1, act1, + if Z.sub maxval minval = Z.one + then CTaction act2 + else CTifeq(key2, act2, CTaction default)) + | 3 -> + let (key1, act1) = sw.(lo) + and (key2, act2) = sw.(lo+1) + and (key3, act3) = sw.(lo+2) in + CTifeq(key1, act1, + CTifeq(key2, act2, + if Z.sub maxval minval = Z.of_uint 2 + then CTaction act3 + else CTifeq(key3, act3, CTaction default))) + | _ -> + let mid = (lo + hi) / 2 in + let (pivot, _) = sw.(mid) in + CTiflt(pivot, + build lo mid minval (Z.sub pivot Z.one), + build mid hi pivot maxval) + in build 0 (Array.length sw) Z.zero modulus + +let compile_switch_as_jumptable default cases minkey maxkey = + let tblsize = 1 + Z.to_int (Z.sub maxkey minkey) in + assert (tblsize >= 0 && tblsize <= Sys.max_array_length); + let tbl = Array.make tblsize default in + List.iter + (fun (key, act) -> + let pos = Z.to_int (Z.sub key minkey) in + tbl.(pos) <- act) + cases; + CTjumptable(minkey, + Z.of_uint tblsize, + Array.to_list tbl, + CTaction default) + +let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = + let span = Z.sub maxkey minkey in + assert (Z.ge span Z.zero); + let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases) + and table_size = Z.add (Z.of_uint 8) span in + numcases >= 7 (* small jump tables are always less efficient *) + && Z.le table_size tree_size + && Z.lt span (Z.of_uint Sys.max_array_length) + +let compile_switch modulus default table = + let (tbl, keys) = normalize_table table in + if ZSet.is_empty keys then CTaction default else begin + let minkey = ZSet.min_elt keys + and maxkey = ZSet.max_elt keys in + if dense_enough (List.length tbl) minkey maxkey + then compile_switch_as_jumptable default tbl minkey maxkey + else compile_switch_as_tree modulus default tbl + end + + diff --git a/extraction/extraction.v b/extraction/extraction.v index d987629..a097bdb 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -16,6 +16,7 @@ Require AST. Require Iteration. Require Floats. Require SelectLong. +Require Selection. Require RTLgen. Require Inlining. Require ValueDomain. @@ -62,9 +63,9 @@ Extract Constant SelectLong.get_helper => Extract Constant SelectLong.get_builtin => "fun s sg -> Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))". +Extract Constant Selection.compile_switch => "Switchaux.compile_switch". (* RTLgen *) -Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. @@ -133,7 +134,7 @@ Load extractionMachdep. (* Avoid name clashes *) Extraction Blacklist List String Int. -(* Cutting the dependancy to R. *) +(* Cutting the dependency to R. *) Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". -- cgit v1.2.3