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 --- 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 ++++++++++++++++++- 13 files changed, 845 insertions(+), 479 deletions(-) (limited to 'backend') diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index d1926fda..7ed5b4ab 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 8c3769af..ad92a12e 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 02c3f210..aacbf86f 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 bf20de29..7ac23bfa 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 db414a2c..03ef0926 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 51a45b27..19f4c839 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 193702e6..26f51e3f 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 75901027..27a4908e 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 51f1f276..2aa5ab92 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 c82c0510..32f35bb4 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 9bd37ef5..cd17b9fd 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 55977b47..658e6603 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 75dd9d20..92004a2f 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 := -- cgit