diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMlexer.mll | 3 | ||||
-rw-r--r-- | backend/CMparser.mly | 22 | ||||
-rw-r--r-- | backend/CMtypecheck.ml | 22 | ||||
-rw-r--r-- | backend/Cminor.v | 14 | ||||
-rw-r--r-- | backend/CminorSel.v | 90 | ||||
-rw-r--r-- | backend/PrintCminor.ml | 5 | ||||
-rw-r--r-- | backend/RTLgen.v | 49 | ||||
-rw-r--r-- | backend/RTLgenaux.ml | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 143 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 85 | ||||
-rw-r--r-- | backend/Selection.v | 56 | ||||
-rw-r--r-- | backend/Selectionproof.v | 144 |
12 files changed, 114 insertions, 521 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index 780d8123..fba85ff2 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -35,13 +35,11 @@ rule token = parse | "/*" { comment lexbuf; token lexbuf } | "absf" { ABSF } | "&" { AMPERSAND } - | "&&" { AMPERSANDAMPERSAND } | "!" { BANG } | "!=" { BANGEQUAL } | "!=f" { BANGEQUALF } | "!=u" { BANGEQUALU } | "|" { BAR } - | "||" { BARBAR } | "^" { CARET } | "case" { CASE } | ":" { COLON } @@ -102,7 +100,6 @@ rule token = parse | "%u" { PERCENTU } | "+" { PLUS } | "+f" { PLUSF } - | "?" { QUESTION } | "}" { RBRACE } | "}}" { RBRACERBRACE } | "]" { RBRACKET } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 4a91a010..aec0a5ef 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -34,7 +34,6 @@ type rexpr = | Runop of unary_operation * rexpr | Rbinop of binary_operation * rexpr * rexpr | Rload of memory_chunk * rexpr - | Rcondition of rexpr * rexpr * rexpr | Rcall of signature * rexpr * rexpr list let temp_counter = ref 0 @@ -59,11 +58,6 @@ let rec convert_rexpr = function let c2 = convert_rexpr e2 in Ebinop(op, c1, c2) | Rload(chunk, e1) -> Eload(chunk, convert_rexpr e1) - | Rcondition(e1, e2, e3) -> - let c1 = convert_rexpr e1 in - let c2 = convert_rexpr e2 in - let c3 = convert_rexpr e3 in - Econdition(c1, c2, c3) | Rcall(sg, e1, el) -> let c1 = convert_rexpr e1 in let cl = convert_rexpr_list el in @@ -135,11 +129,6 @@ let mkwhile expr body = let intconst n = Rconst(Ointconst(coqint_of_camlint n)) -let andbool e1 e2 = - Rcondition(e1, e2, intconst 0l) -let orbool e1 e2 = - Rcondition(e1, intconst 1l, e2) - let exitnum n = nat_of_camlint n let mkswitch expr (cases, dfl) = @@ -202,13 +191,11 @@ let mkmatch expr cases = %token ABSF %token AMPERSAND -%token AMPERSANDAMPERSAND %token BANG %token BANGEQUAL %token BANGEQUALF %token BANGEQUALU %token BAR -%token BARBAR %token CARET %token CASE %token COLON @@ -273,7 +260,6 @@ let mkmatch expr cases = %token PERCENTU %token PLUS %token PLUSF -%token QUESTION %token RBRACE %token RBRACERBRACE %token RBRACKET @@ -301,9 +287,6 @@ let mkmatch expr cases = %left COMMA %left p_let %right EQUAL -%right QUESTION COLON -%left BARBAR -%left AMPERSANDAMPERSAND %left BAR %left CARET %left AMPERSAND @@ -502,7 +485,7 @@ expr: | FLOATOFINT expr { Runop(Ofloatofint, $2) } | FLOATOFINTU expr { Runop(Ofloatofintu, $2) } | TILDE expr { Runop(Onotint, $2) } - | BANG expr { Runop(Onotbool, $2) } + | BANG expr { Rbinop(Ocmpu Ceq, $2, intconst 0l) } | INT8S expr { Runop(Ocast8signed, $2) } | INT8U expr { Runop(Ocast8unsigned, $2) } | INT16S expr { Runop(Ocast16signed, $2) } @@ -544,9 +527,6 @@ expr: | expr GREATERF expr { Rbinop(Ocmpf Cgt, $1, $3) } | expr GREATEREQUALF expr { Rbinop(Ocmpf Cge, $1, $3) } | memory_chunk LBRACKET expr RBRACKET { Rload($1, $3) } - | expr AMPERSANDAMPERSAND expr { andbool $1 $3 } - | expr BARBAR expr { orbool $1 $3 } - | expr QUESTION expr COLON expr { Rcondition($1, $3, $5) } | expr LPAREN expr_list RPAREN COLON signature{ Rcall($6, $1, $3) } ; diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 6e91f5b2..40707854 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -90,8 +90,6 @@ let type_unary_operation = function | Ocast8unsigned -> tint, tint | Ocast16unsigned -> tint, tint | Onegint -> tint, tint - | Oboolval -> tint, tint - | Onotbool -> tint, tint | Onotint -> tint, tint | Onegf -> tfloat, tfloat | Oabsf -> tfloat, tfloat @@ -135,8 +133,6 @@ let name_of_unary_operation = function | Ocast8unsigned -> "cast8unsigned" | Ocast16unsigned -> "cast16unsigned" | Onegint -> "negint" - | Oboolval -> "notbool" - | Onotbool -> "notbool" | Onotint -> "notint" | Onegf -> "negf" | Oabsf -> "absf" @@ -224,24 +220,6 @@ let rec type_expr env lenv e = (name_of_chunk chunk) s)) end; type_chunk chunk - | Econdition(e1, e2, e3) -> - type_condexpr env lenv e1; - let te2 = type_expr env lenv e2 in - let te3 = type_expr env lenv e3 in - begin try - unify te2 te3 - with Error s -> - raise (Error (sprintf "In conditional expression:\n%s" s)) - end; - te2 -(* - | Elet(e1, e2) -> - let te1 = type_expr env lenv e1 in - let te2 = type_expr env (te1 :: lenv) e2 in - te2 - | Eletvar n -> - type_letvar lenv n -*) and type_exprlist env lenv el = match el with diff --git a/backend/Cminor.v b/backend/Cminor.v index 6d288a9e..4bc6b727 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -44,9 +44,7 @@ Inductive unary_operation : Type := | Ocast8signed: unary_operation (**r 8-bit sign extension *) | Ocast16unsigned: unary_operation (**r 16-bit zero extension *) | Ocast16signed: unary_operation (**r 16-bit sign extension *) - | Oboolval: unary_operation (**r 0 if null, 1 if non-null *) | Onegint: unary_operation (**r integer opposite *) - | Onotbool: unary_operation (**r boolean negation *) | Onotint: unary_operation (**r bitwise complement *) | Onegf: unary_operation (**r float opposite *) | Oabsf: unary_operation (**r float absolute value *) @@ -87,8 +85,7 @@ Inductive expr : Type := | Econst : constant -> expr | Eunop : unary_operation -> expr -> expr | Ebinop : binary_operation -> expr -> expr -> expr - | Eload : memory_chunk -> expr -> expr - | Econdition : expr -> expr -> expr -> expr. + | Eload : memory_chunk -> expr -> expr. (** Statements include expression evaluation, assignment to local variables, memory stores, function calls, an if/then/else conditional, infinite @@ -230,9 +227,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | Ocast8signed => Some (Val.sign_ext 8 arg) | Ocast16unsigned => Some (Val.zero_ext 16 arg) | Ocast16signed => Some (Val.sign_ext 16 arg) - | Oboolval => Some(Val.boolval arg) | Onegint => Some (Val.negint arg) - | Onotbool => Some (Val.notbool arg) | Onotint => Some (Val.notint arg) | Onegf => Some (Val.negf arg) | Oabsf => Some (Val.absf arg) @@ -301,12 +296,7 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Eload: forall chunk addr vaddr v, eval_expr addr vaddr -> Mem.loadv chunk m vaddr = Some v -> - eval_expr (Eload chunk addr) v - | eval_Econdition: forall a1 a2 a3 v1 b1 v2, - eval_expr a1 v1 -> - Val.bool_of_val v1 b1 -> - eval_expr (if b1 then a2 else a3) v2 -> - eval_expr (Econdition a1 a2 a3) v2. + eval_expr (Eload chunk addr) v. Inductive eval_exprlist: list expr -> list val -> Prop := | eval_Enil: diff --git a/backend/CminorSel.v b/backend/CminorSel.v index a8e49e87..bb5143c1 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -35,34 +35,26 @@ Require Import Smallstep. languages ([RTL] and below). Moreover, to express sharing of sub-computations, a "let" binding is provided (constructions [Elet] and [Eletvar]), using de Bruijn indices to refer to "let"-bound - variables. Finally, a variant [condexpr] of [expr] - is used to represent expressions which are evaluated for their - boolean value only and not their exact value. -*) + variables. *) Inductive expr : Type := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr - | Econdition : condexpr -> expr -> expr -> expr + | Econdition : condition -> exprlist -> expr -> expr -> expr | Elet : expr -> expr -> expr | Eletvar : nat -> expr -with condexpr : Type := - | CEtrue: condexpr - | CEfalse: condexpr - | CEcond: condition -> exprlist -> condexpr - | CEcondition : condexpr -> condexpr -> condexpr -> condexpr - with exprlist : Type := | Enil: exprlist | Econs: expr -> exprlist -> exprlist. Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. -(** Statements are as in Cminor, except that the condition of an - if/then/else conditional is a [condexpr], and the [Sstore] construct - uses a machine-dependent addressing mode. *) +(** 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. *) Inductive stmt : Type := | Sskip: stmt @@ -72,7 +64,7 @@ Inductive stmt : Type := | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt - | Sifthenelse: condexpr -> stmt -> stmt -> stmt + | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt @@ -147,10 +139,7 @@ Variable ge: genv. (** The evaluation predicates have the same general shape as those of Cminor. Refer to the description of Cminor semantics for - the meaning of the parameters of the predicates. - One additional predicate is introduced: - [eval_condexpr ge sp e m le a b], meaning that the conditional - expression [a] evaluates to the boolean [b]. *) + the meaning of the parameters of the predicates. *) Section EVAL_EXPR. @@ -171,10 +160,11 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_addressing ge sp addr vl = Some vaddr -> Mem.loadv chunk m vaddr = Some v -> eval_expr le (Eload chunk addr al) v - | eval_Econdition: forall le a b c v1 v2, - eval_condexpr le a v1 -> - eval_expr le (if v1 then b else c) v2 -> - eval_expr le (Econdition a b c) v2 + | eval_Econdition: forall le cond al b c vl vb v, + eval_exprlist le al vl -> + eval_condition cond vl m = Some vb -> + eval_expr le (if vb then b else c) v -> + eval_expr le (Econdition cond al b c) v | eval_Elet: forall le a b v1 v2, eval_expr le a v1 -> eval_expr (v1 :: le) b v2 -> @@ -183,20 +173,6 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := nth_error le n = Some v -> eval_expr le (Eletvar n) v -with eval_condexpr: letenv -> condexpr -> bool -> Prop := - | eval_CEtrue: forall le, - eval_condexpr le CEtrue true - | eval_CEfalse: forall le, - eval_condexpr le CEfalse false - | eval_CEcond: forall le cond al vl b, - eval_exprlist le al vl -> - eval_condition cond vl m = Some b -> - eval_condexpr le (CEcond cond al) b - | eval_CEcondition: forall le a b c vb1 vb2, - eval_condexpr le a vb1 -> - eval_condexpr le (if vb1 then b else c) vb2 -> - eval_condexpr le (CEcondition a b c) vb2 - with eval_exprlist: letenv -> exprlist -> list val -> Prop := | eval_Enil: forall le, eval_exprlist le Enil nil @@ -204,9 +180,8 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_expr le a1 v1 -> eval_exprlist le al vl -> eval_exprlist le (Econs a1 al) (v1 :: vl). -Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop. +Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop. Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := | eval_eos_e: forall le e v, @@ -245,7 +220,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont) | Some sk => Some sk | None => find_label lbl s2 k end - | Sifthenelse a s1 s2 => + | Sifthenelse cond al s1 s2 => match find_label lbl s1 k with | Some sk => Some sk | None => find_label lbl s2 k @@ -316,9 +291,10 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) - | step_ifthenelse: forall f a s1 s2 k sp e m b, - eval_condexpr sp e m nil a b -> - step (State f (Sifthenelse a s1 s2) k sp e m) + | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b, + eval_exprlist sp e m nil al vl -> + eval_condition cond vl m = Some b -> + step (State f (Sifthenelse cond al s1 s2) k sp e m) E0 (State f (if b then s1 else s2) k sp e m) | step_loop: forall f s k sp e m, @@ -395,7 +371,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_condexpr eval_exprlist: evalexpr. +Hint Constructors eval_expr eval_exprlist: evalexpr. (** * Lifting of let-bound variables *) @@ -409,22 +385,13 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := | Evar id => Evar id | Eop op bl => Eop op (lift_exprlist p bl) | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) - | Econdition b c d => - Econdition (lift_condexpr p b) (lift_expr p c) (lift_expr p d) + | Econdition cond al b c => + Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c) | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) | Eletvar n => if le_gt_dec p n then Eletvar (S n) else Eletvar n end -with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := - match a with - | CEtrue => CEtrue - | CEfalse => CEfalse - | CEcond cond bl => CEcond cond (lift_exprlist p bl) - | CEcondition b c d => - CEcondition (lift_condexpr p b) (lift_condexpr p c) (lift_condexpr p d) - end - with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := match a with | Enil => Enil @@ -478,29 +445,22 @@ Lemma eval_lift_expr: eval_expr ge sp e m le' (lift_expr p a) v. Proof. intros until w. - apply (eval_expr_ind3 ge sp e m + apply (eval_expr_ind2 ge sp e m (fun le a v => forall p le', insert_lenv le p w le' -> eval_expr ge sp e m le' (lift_expr p a) v) - (fun le a v => - forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp e m le' (lift_condexpr p a) v) (fun le al vl => forall p le', insert_lenv le p w le' -> eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); simpl; intros; eauto with evalexpr. - destruct v1; eapply eval_Econdition; - eauto with evalexpr; simpl; eauto with evalexpr. + eapply eval_Econdition; eauto. destruct vb; eauto. eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. case (le_gt_dec p n); intro. apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. - - destruct vb1; eapply eval_CEcondition; - eauto with evalexpr; simpl; eauto with evalexpr. Qed. Lemma eval_lift: diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml index 66b579e7..858ef219 100644 --- a/backend/PrintCminor.ml +++ b/backend/PrintCminor.ml @@ -40,7 +40,6 @@ let rec precedence = function | Ebinop(Oxor, _, _) -> (7, LtoR) | Ebinop(Oor, _, _) -> (6, LtoR) | Eload _ -> (15, RtoL) - | Econdition _ -> (3, RtoL) (* Naming idents. We assume idents are encoded as in Cminorgen. *) @@ -58,8 +57,6 @@ let name_of_unop = function | Ocast16unsigned -> "int16u" | Ocast16signed -> "int16s" | Onegint -> "-" - | Oboolval -> "(_Bool)" - | Onotbool -> "!" | Onotint -> "~" | Onegf -> "-f" | Oabsf -> "absf" @@ -141,8 +138,6 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_of_binop op) expr (prec2, a2) | Eload(chunk, a1) -> fprintf p "%s[%a]" (name_of_chunk chunk) expr (0, a1) - | Econdition(a1, a2, a3) -> - fprintf p "%a@ ? %a@ : %a" expr (4, a1) expr (4, a2) expr (4, a3) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 86c11772..d3b99bbd 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -416,10 +416,12 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do rl <- alloc_regs map al; do no <- add_instr (Iload chunk addr rl rd nd); transl_exprlist map al rl no - | Econdition b c d => - do nfalse <- transl_expr map d rd nd; - do ntrue <- transl_expr map c rd nd; - transl_condition map b ntrue nfalse + | Econdition cond al b c => + do rl <- alloc_regs map al; + do nfalse <- transl_expr map c rd nd; + do ntrue <- transl_expr map b rd nd; + do nt <- add_instr (Icond cond rl ntrue nfalse); + transl_exprlist map al rl nt | Elet b c => do r <- new_reg; do nc <- transl_expr (add_letvar map r) c rd nd; @@ -428,28 +430,6 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do r <- find_letvar map n; add_move r rd nd end -(** Translation of a conditional expression. Similar to [transl_expr], - but the expression is evaluated for its truth value, and the generated - code branches to one of two possible continuation nodes [ntrue] or - [nfalse] depending on the truth value of [a]. *) - -with transl_condition (map: mapping) (a: condexpr) (ntrue nfalse: node) - {struct a}: mon node := - match a with - | CEtrue => - ret ntrue - | CEfalse => - ret nfalse - | CEcond cond bl => - do rl <- alloc_regs map bl; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map bl rl nt - | CEcondition b c d => - do nd <- transl_condition map d ntrue nfalse; - do nc <- transl_condition map c ntrue nfalse; - transl_condition map b nc nd - end - (** Translation of a list of expressions. The expressions are evaluated left-to-right, and their values stored in the given list of registers. *) @@ -472,7 +452,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) 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. +Parameter more_likely: condition -> stmt -> stmt -> bool. (** Auxiliary for translating [Sswitch] statements. *) @@ -521,7 +501,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) Fixpoint expr_is_2addr_op (e: expr) : bool := match e with | Eop op _ => two_address_op op - | Econdition e1 e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3 + | Econdition cond el e2 e3 => expr_is_2addr_op e2 || expr_is_2addr_op e3 | Elet e1 e2 => expr_is_2addr_op e2 | _ => false end. @@ -587,15 +567,18 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret - | Sifthenelse a strue sfalse => - if more_likely a strue sfalse then + | Sifthenelse cond al strue sfalse => + do rl <- alloc_regs map al; + if more_likely cond strue sfalse then do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; - transl_condition map a ntrue nfalse + do nt <- add_instr (Icond cond rl ntrue nfalse); + transl_exprlist map al rl nt else do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; - transl_condition map a ntrue nfalse + do nt <- add_instr (Icond cond rl ntrue nfalse); + transl_exprlist map al rl nt | Sloop sbody => do n1 <- reserve_instr; do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret; @@ -650,7 +633,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) {struct s} : labelmap * state := match s with | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms) - | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms) + | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms) | Sloop s1 => reserve_labels s1 ms | Sblock s1 => reserve_labels s1 ms | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms) diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 0822587f..245b80cd 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -14,7 +14,7 @@ open Camlcoq open Switch open CminorSel -let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false +let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = false module IntOrd = struct diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e06224a6..659e8d0c 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -520,9 +520,6 @@ Definition transl_expr_prop /\ rs'#rd = v /\ (forall r, In r pr -> rs'#r = rs#r). -(** The simulation properties for lists of expressions and for - conditional expressions are similar. *) - Definition transl_exprlist_prop (le: letenv) (al: exprlist) (vl: list val) : Prop := forall cs f map pr ns nd rl rs @@ -535,18 +532,6 @@ Definition transl_exprlist_prop /\ rs'##rl = vl /\ (forall r, In r pr -> rs'#r = rs#r). -Definition transl_condition_prop - (le: letenv) (a: condexpr) (vb: bool) : Prop := - forall cs f map pr ns ntrue nfalse rs - (MWF: map_wf map) - (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) - (ME: match_env map e le rs), - exists rs', - star step tge (State cs f sp ns rs m) E0 - (State cs f sp (if vb then ntrue else nfalse) rs' m) - /\ match_env map e le rs' - /\ (forall r, In r pr -> rs'#r = rs#r). - (** The correctness of the translation is a huge induction over the Cminor evaluation derivation for the source program. To keep the proof manageable, we put each case of the proof in a separate @@ -632,22 +617,25 @@ Proof. Qed. Lemma transl_expr_Econdition_correct: - forall (le : letenv) (cond : condexpr) (ifso ifnot : expr) - (vcond : bool) (v : val), - eval_condexpr ge sp e m le cond vcond -> - transl_condition_prop le cond vcond -> + forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr) + (vl: list val) (vcond : bool) (v : val), + eval_exprlist ge sp e m le al vl -> + transl_exprlist_prop le al vl -> + eval_condition cond vl m = Some vcond -> eval_expr ge sp e m le (if vcond then ifso else ifnot) v -> transl_expr_prop le (if vcond then ifso else ifnot) v -> - transl_expr_prop le (Econdition cond ifso ifnot) v. + transl_expr_prop le (Econdition cond al ifso ifnot) v. Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. + intros; red; intros; inv TE. inv H14. + exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst). destruct vcond; auto. - exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. + exploit H3; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. (* Exec *) - split. eapply star_trans. eexact EX1. eexact EX2. auto. + split. eapply star_trans. eexact EX1. + eapply star_left. eapply exec_Icond. eauto. rewrite RES1; eauto. reflexivity. + eexact EX2. reflexivity. traceEq. (* Match-env *) split. assumption. (* Result value *) @@ -710,67 +698,6 @@ Proof. apply OTHER1. intuition congruence. Qed. -Lemma transl_condition_CEtrue_correct: - forall (le : letenv), - transl_condition_prop le CEtrue true. -Proof. - intros; red; intros; inv TE. - exists rs. split. apply star_refl. split. auto. auto. -Qed. - -Lemma transl_condition_CEfalse_correct: - forall (le : letenv), - transl_condition_prop le CEfalse false. -Proof. - intros; red; intros; inv TE. - exists rs. split. apply star_refl. split. auto. auto. -Qed. - -Lemma transl_condition_CEcond_correct: - forall (le : letenv) (cond : condition) (args : exprlist) - (vargs : list val) (b : bool), - eval_exprlist ge sp e m le args vargs -> - transl_exprlist_prop le args vargs -> - eval_condition cond vargs m = Some b -> - transl_condition_prop le (CEcond cond args) b. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]]. - exists rs1. -(* Exec *) - split. eapply star_right. eexact EX1. - eapply exec_Icond with (b := b); eauto. - rewrite RES1. auto. - traceEq. -(* Match-env *) - split. assumption. -(* Regs *) - auto. -Qed. - -Lemma transl_condition_CEcondition_correct: - forall (le : letenv) (cond ifso ifnot : condexpr) (vcond v : bool), - eval_condexpr ge sp e m le cond vcond -> - transl_condition_prop le cond vcond -> - eval_condexpr ge sp e m le (if vcond then ifso else ifnot) v -> - transl_condition_prop le (if vcond then ifso else ifnot) v -> - transl_condition_prop le (CEcondition cond ifso ifnot) v. -Proof. - intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot) - (if vcond then ntrue' else nfalse') ntrue nfalse). - destruct vcond; auto. - exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]]. - exists rs2. -(* Execution *) - split. eapply star_trans. eexact EX1. eexact EX2. auto. -(* Match-env *) - split. auto. -(* Regs *) - intros. transitivity (rs1#r); auto. -Qed. - Lemma transl_exprlist_Enil_correct: forall (le : letenv), transl_exprlist_prop le Enil nil. @@ -814,31 +741,8 @@ Theorem transl_expr_correct: eval_expr ge sp e m le a v -> transl_expr_prop le a v. Proof - (eval_expr_ind3 ge sp e m - transl_expr_prop - transl_condition_prop - transl_exprlist_prop - transl_expr_Evar_correct - transl_expr_Eop_correct - transl_expr_Eload_correct - transl_expr_Econdition_correct - transl_expr_Elet_correct - transl_expr_Eletvar_correct - transl_condition_CEtrue_correct - transl_condition_CEfalse_correct - transl_condition_CEcond_correct - transl_condition_CEcondition_correct - transl_exprlist_Enil_correct - transl_exprlist_Econs_correct). - -Theorem transl_condexpr_correct: - forall le a v, - eval_condexpr ge sp e m le a v -> - transl_condition_prop le a v. -Proof - (eval_condexpr_ind3 ge sp e m + (eval_expr_ind2 ge sp e m transl_expr_prop - transl_condition_prop transl_exprlist_prop transl_expr_Evar_correct transl_expr_Eop_correct @@ -846,22 +750,16 @@ Proof transl_expr_Econdition_correct transl_expr_Elet_correct transl_expr_Eletvar_correct - transl_condition_CEtrue_correct - transl_condition_CEfalse_correct - transl_condition_CEcond_correct - transl_condition_CEcondition_correct transl_exprlist_Enil_correct transl_exprlist_Econs_correct). - Theorem transl_exprlist_correct: forall le a v, eval_exprlist ge sp e m le a v -> transl_exprlist_prop le a v. Proof - (eval_exprlist_ind3 ge sp e m + (eval_exprlist_ind2 ge sp e m transl_expr_prop - transl_condition_prop transl_exprlist_prop transl_expr_Evar_correct transl_expr_Eop_correct @@ -869,10 +767,6 @@ Proof transl_expr_Econdition_correct transl_expr_Elet_correct transl_expr_Eletvar_correct - transl_condition_CEtrue_correct - transl_condition_CEfalse_correct - transl_condition_CEcond_correct - transl_condition_CEcondition_correct transl_exprlist_Enil_correct transl_exprlist_Econs_correct). @@ -886,7 +780,7 @@ Fixpoint size_stmt (s: stmt) : nat := match s with | Sskip => 0 | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) - | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1) | Sloop s1 => (size_stmt s1 + 1) | Sblock s1 => (size_stmt s1 + 1) | Sexit n => 0 @@ -1219,11 +1113,10 @@ Proof. econstructor; eauto. econstructor; eauto. (* ifthenelse *) - inv TS. - exploit transl_condexpr_correct; eauto. - intros [rs' [A [B C]]]. + inv TS. inv H13. + exploit transl_exprlist_correct; eauto. intros [rs' [A [B [C D]]]]. econstructor; split. - right; split. eexact A. destruct b; Lt_state. + left. eapply plus_right. eexact A. eapply exec_Icond; eauto. rewrite C; eauto. traceEq. destruct b; econstructor; eauto. (* loop *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index f6c59fcd..579a6c25 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -749,11 +749,11 @@ Inductive tr_expr (c: code): c!n1 = Some (Iload chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst - | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse dst, - tr_condition c map pr b ns ntrue nfalse -> + | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst, + tr_condition c map pr cond bl ns ntrue nfalse -> tr_expr c map pr ifso ntrue nd rd dst -> tr_expr c map pr ifnot nfalse nd rd dst -> - tr_expr c map pr (Econdition b ifso ifnot) ns nd rd dst + tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> tr_expr c map pr b1 ns n1 r None -> @@ -765,26 +765,17 @@ Inductive tr_expr (c: code): tr_move c ns r nd rd -> tr_expr c map pr (Eletvar n) ns nd rd dst -(** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c], +(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth value of the Cminor conditional expression [cond] and terminate on node [ntrue] if the condition holds and on node [nfalse] otherwise. *) with tr_condition (c: code): - mapping -> list reg -> condexpr -> node -> node -> node -> Prop := - | tr_CEtrue: forall map pr ntrue nfalse, - tr_condition c map pr CEtrue ntrue ntrue nfalse - | tr_CEfalse: forall map pr ntrue nfalse, - tr_condition c map pr CEfalse nfalse ntrue nfalse + mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop := | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse) -> - tr_condition c map pr (CEcond cond bl) ns ntrue nfalse - | tr_CEcondition: forall map pr b ifso ifnot ns ntrue nfalse ntrue' nfalse', - tr_condition c map pr b ns ntrue' nfalse' -> - tr_condition c map pr ifso ntrue' ntrue nfalse -> - tr_condition c map pr ifnot nfalse' ntrue nfalse -> - tr_condition c map pr (CEcondition b ifso ifnot) ns ntrue nfalse + tr_condition c map pr cond bl ns ntrue nfalse (** [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 @@ -889,11 +880,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret - | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, tr_stmt c map strue ntrue nd nexits ngoto nret rret -> tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> - tr_condition c map nil a ns ntrue nfalse -> - tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret + tr_condition c map nil cond al ns ntrue nfalse -> + tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend, tr_stmt c map sbody nloop nend nexits ngoto nret rret -> c!ns = Some(Inop nloop) -> @@ -963,9 +954,9 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> - forall map pr a ns ntrue nfalse, - tr_condition s1.(st_code) map pr a ns ntrue nfalse -> - tr_condition s2.(st_code) map pr a ns ntrue nfalse + forall map pr cond al ns ntrue nfalse, + tr_condition s1.(st_code) map pr cond al ns ntrue nfalse -> + tr_condition s2.(st_code) map pr cond al ns ntrue nfalse with tr_exprlist_incr: forall s1 s2, state_incr s1 s2 -> forall map pr al ns nd rl, @@ -1004,13 +995,6 @@ Lemma transl_expr_charact: (VALID2: reg_valid rd s), tr_expr s'.(st_code) map pr a ns nd rd None -with transl_condexpr_charact: - forall a map ntrue nfalse s ns s' pr INCR - (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR) - (VALID: regs_valid pr s) - (WF: map_valid map s), - tr_condition s'.(st_code) map pr a ns ntrue nfalse - with transl_exprlist_charact: forall al map rl nd s ns s' pr INCR (TR: transl_exprlist map al rl nd s = OK ns s' INCR) @@ -1040,9 +1024,10 @@ Proof. (* Econdition *) inv OK. econstructor; eauto with rtlg. - apply tr_expr_incr with s1; auto. + econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. + apply tr_expr_incr with s2; auto. eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. - apply tr_expr_incr with s0; auto. + apply tr_expr_incr with s1; auto. eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. @@ -1065,24 +1050,6 @@ Proof. eapply add_move_charact; eauto. monadInv EQ1. -(* Conditions *) - induction a; intros; try (monadInv TR); saturateTrans. - - (* CEtrue *) - constructor. - (* CEfalse *) - constructor. - (* CEcond *) - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. - (* CEcondition *) - econstructor. - eapply transl_condexpr_charact; eauto with rtlg. - apply tr_condition_incr with s1; auto. - eapply transl_condexpr_charact; eauto with rtlg. - apply tr_condition_incr with s0; auto. - eapply transl_condexpr_charact; eauto with rtlg. - (* Lists *) induction al; intros; try (monadInv TR); saturateTrans. @@ -1127,10 +1094,10 @@ Opaque two_address_op. (* Econdition *) simpl in NOT2ADDR. destruct (orb_false_elim _ _ NOT2ADDR). econstructor; eauto with rtlg. - eapply transl_condexpr_charact; eauto with rtlg. + econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. + apply tr_expr_incr with s2; auto. + eapply IHa1; eauto 2 with rtlg. apply tr_expr_incr with s1; auto. - eapply IHa1; eauto 2 with rtlg. - apply tr_expr_incr with s0; auto. eapply IHa2; eauto 2 with rtlg. (* Elet *) simpl in NOT2ADDR. @@ -1298,19 +1265,21 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply IHstmt1; eauto with rtlg. (* Sifthenelse *) - destruct (more_likely c stmt1 stmt2); monadInv TR. + destruct (more_likely c stmt1 stmt2); monadInv EQ0. econstructor. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s2; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s0; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt2; eauto with rtlg. - eapply transl_condexpr_charact; eauto with rtlg. + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. econstructor. - apply tr_stmt_incr with s0; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s2; auto. eapply IHstmt2; eauto with rtlg. - eapply transl_condexpr_charact; eauto with rtlg. + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* Sloop *) econstructor. apply tr_stmt_incr with s1; auto. diff --git a/backend/Selection.v b/backend/Selection.v index 11654f1f..ff4d8639 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -37,51 +37,12 @@ Require Import SelectOp. Open Local Scope cminorsel_scope. -(** Conversion of conditional expressions *) +(** Conversion of conditions *) -Fixpoint negate_condexpr (e: condexpr): condexpr := +Function condition_of_expr (e: expr) : condition * exprlist := match e with - | CEtrue => CEfalse - | CEfalse => CEtrue - | CEcond c el => CEcond (negate_condition c) el - | CEcondition e1 e2 e3 => - CEcondition e1 (negate_condexpr e2) (negate_condexpr e3) - end. - -Definition is_compare_neq_zero (c: condition) : bool := - match c with - | Ccompimm Cne n => Int.eq n Int.zero - | Ccompuimm Cne n => Int.eq n Int.zero - | _ => false - end. - -Definition is_compare_eq_zero (c: condition) : bool := - match c with - | Ccompimm Ceq n => Int.eq n Int.zero - | Ccompuimm Ceq n => Int.eq n Int.zero - | _ => false - end. - -Definition condexpr_of_expr_base (e: expr) : condexpr := - let (c, args) := cond_of_expr e in CEcond c args. - -Fixpoint condexpr_of_expr (e: expr) : condexpr := - match e with - | Eop (Ointconst n) Enil => - if Int.eq n Int.zero then CEfalse else CEtrue - | Eop (Ocmp c) (e1 ::: Enil) => - if is_compare_neq_zero c then - condexpr_of_expr e1 - else if is_compare_eq_zero c then - negate_condexpr (condexpr_of_expr e1) - else - CEcond c (e1 ::: Enil) - | Eop (Ocmp c) el => - CEcond c el - | Econdition ce e1 e2 => - CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2) - | _ => - condexpr_of_expr_base e + | Eop (Ocmp c) el => (c, el) + | _ => (Ccompuimm Cne Int.zero, e ::: Enil) end. (** Conversion of loads and stores *) @@ -115,8 +76,6 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := | Cminor.Ocast16unsigned => cast16unsigned arg | Cminor.Ocast16signed => cast16signed arg | Cminor.Onegint => negint arg - | Cminor.Oboolval => boolval arg - | Cminor.Onotbool => notbool arg | Cminor.Onotint => notint arg | Cminor.Onegf => negf arg | Cminor.Oabsf => absf arg @@ -160,9 +119,6 @@ Fixpoint sel_expr (a: Cminor.expr) : expr := | Cminor.Eunop op arg => sel_unop op (sel_expr arg) | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2) | Cminor.Eload chunk addr => load chunk (sel_expr addr) - | Cminor.Econdition cond ifso ifnot => - Econdition (condexpr_of_expr (sel_expr cond)) - (sel_expr ifso) (sel_expr ifnot) end. Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist := @@ -222,8 +178,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := end | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => - Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ge ifso) (sel_stmt ge ifnot) + let (cond, args) := condition_of_expr (sel_expr e) in + Sifthenelse cond args (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 diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 79c039fa..2fb56f86 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -40,125 +40,23 @@ Variable sp: val. Variable e: env. Variable m: mem. -(** Conversion of condition expressions. *) - -Lemma negate_condexpr_correct: - forall le a b, - eval_condexpr ge sp e m le a b -> - eval_condexpr ge sp e m le (negate_condexpr a) (negb b). -Proof. - induction 1; simpl. - constructor. - constructor. - econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto. - econstructor. eauto. destruct vb1; auto. -Qed. - -Scheme expr_ind2 := Induction for expr Sort Prop - with exprlist_ind2 := Induction for exprlist Sort Prop. - -Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop := - match el with - | Enil => True - | Econs e el' => P e /\ forall_exprlist P el' - end. - -Lemma expr_induction_principle: - forall (P: expr -> Prop), - (forall i : ident, P (Evar i)) -> - (forall (o : operation) (e : exprlist), - forall_exprlist P e -> P (Eop o e)) -> - (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist), - forall_exprlist P e -> P (Eload m a e)) -> - (forall (c : condexpr) (e : expr), - P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) -> - (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) -> - (forall n : nat, P (Eletvar n)) -> - forall e : expr, P e. -Proof. - intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto. - simpl. auto. - intros. simpl. auto. -Qed. - -Lemma eval_condition_of_expr_base: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_condexpr ge sp e m le (condexpr_of_expr_base a) b. -Proof. - intros. unfold condexpr_of_expr_base. - generalize (eval_cond_of_expr _ _ _ _ _ _ _ _ H H0). - destruct (cond_of_expr a) as [cond args]. - intros [vl [A B]]. - econstructor; eauto. -Qed. - -Lemma is_compare_neq_zero_correct: - forall c v b, - is_compare_neq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> - Val.bool_of_val v b. -Proof. - intros. - destruct c; simpl in H; try discriminate; - destruct c; simpl in H; try discriminate; - generalize (Int.eq_spec i Int.zero); rewrite H; intros; subst. - - simpl in H0. destruct v; inv H0. constructor. - simpl in H0. destruct v; inv H0. constructor. constructor. -Qed. - -Lemma is_compare_eq_zero_correct: - forall c v b, - is_compare_eq_zero c = true -> - eval_condition c (v :: nil) m = Some b -> - Val.bool_of_val v (negb b). -Proof. - intros. apply is_compare_neq_zero_correct with (negate_condition c). - destruct c; simpl in H; simpl; try discriminate; - destruct c; simpl; try discriminate; auto. - rewrite eval_negate_condition. rewrite H0. auto. -Qed. - Lemma eval_condition_of_expr: - forall a le v b, + forall le a v b, eval_expr ge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr ge sp e m le (condexpr_of_expr a) b. + match condition_of_expr a with (cond, args) => + exists vl, + eval_exprlist ge sp e m le args vl /\ + eval_condition cond vl m = Some b + end. Proof. - intro a0; pattern a0. - apply expr_induction_principle; simpl; intros; - try (eapply eval_condition_of_expr_base; eauto; fail). - - destruct o; try (eapply eval_condition_of_expr_base; eauto; fail). - - destruct e0. inv H0. inv H5. simpl in H7. inv H7. inv H1. - destruct (Int.eq i Int.zero); constructor. - eapply eval_condition_of_expr_base; eauto. - - inv H0. simpl in H7. - assert (eval_condition c vl m = Some b). - inv H7. eapply Val.bool_of_val_of_optbool; eauto. - assert (eval_condexpr ge sp e m le (CEcond c e0) b). - eapply eval_CEcond; eauto. - destruct e0; auto. destruct e1; auto. - simpl in H. destruct H. - inv H5. inv H11. - - case_eq (is_compare_neq_zero c); intros. - eapply H; eauto. - apply is_compare_neq_zero_correct with c; auto. - - case_eq (is_compare_eq_zero c); intros. - replace b with (negb (negb b)). apply negate_condexpr_correct. - eapply H; eauto. - apply is_compare_eq_zero_correct with c; auto. - apply negb_involutive. - - auto. - - inv H1. destruct v1; eauto with evalexpr. + intros until a. functional induction (condition_of_expr a); intros. +(* compare *) + inv H. exists vl; split; auto. + simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. +(* default *) + exists (v :: nil); split. constructor. auto. constructor. + simpl. inv H0. auto. auto. Qed. Lemma eval_load: @@ -202,9 +100,7 @@ Proof. apply eval_cast8signed; auto. apply eval_cast16unsigned; auto. apply eval_cast16signed; auto. - apply eval_boolval; auto. apply eval_negint; auto. - apply eval_notbool; auto. apply eval_notint; auto. apply eval_negf; auto. apply eval_absf; auto. @@ -436,14 +332,6 @@ Proof. exploit IHeval_expr; eauto. intros [vaddr' [A B]]. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. exists v'; split; auto. eapply eval_load; eauto. - (* Econdition *) - exploit IHeval_expr1; eauto. intros [v1' [A B]]. - exploit IHeval_expr2; eauto. intros [v2' [C D]]. - replace (sel_expr (if b1 then a2 else a3)) with (if b1 then sel_expr a2 else sel_expr a3) in C. - assert (Val.bool_of_val v1' b1). inv B. auto. inv H0. - exists v2'; split; auto. - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. Qed. Lemma sel_exprlist_correct: @@ -544,6 +432,7 @@ Proof. destruct (find_label lbl (sel_stmt ge s1) (Kseq (sel_stmt ge s2) k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) + destruct (condition_of_expr (sel_expr e)) as [cond args]. simpl. exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; destruct (find_label lbl (sel_stmt ge s1) k') as [[sy ky] | ]; @@ -643,8 +532,11 @@ Proof. (* Sifthenelse *) exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. + exploit eval_condition_of_expr; eauto. + destruct (condition_of_expr (sel_expr a)) as [cond args]. + intros [vl' [C D]]. left; exists (State (sel_function ge f) (if b then sel_stmt ge s1 else sel_stmt ge s2) k' sp e' m'); split. - constructor. eapply eval_condition_of_expr; eauto. + econstructor; eauto. constructor; auto. destruct b; auto. (* Sloop *) left; econstructor; split. constructor. constructor; auto. constructor; auto. |