From 2199fd1838ab1c32d55c760e92b97077d8eaae50 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 17 Aug 2009 14:24:34 +0000 Subject: Refactored Selection.v and Selectionproof.v into a machine-dependent part + a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/SelectOp.v | 1195 +++++++++++++++++++++++++++++++++++++++++ arm/SelectOpproof.v | 986 ++++++++++++++++++++++++++++++++++ arm/Selection.v | 1394 ----------------------------------------------- arm/Selectionproof.v | 1459 -------------------------------------------------- 4 files changed, 2181 insertions(+), 2853 deletions(-) create mode 100644 arm/SelectOp.v create mode 100644 arm/SelectOpproof.v delete mode 100644 arm/Selection.v delete mode 100644 arm/Selectionproof.v (limited to 'arm') diff --git a/arm/SelectOp.v b/arm/SelectOp.v new file mode 100644 index 00000000..8ac4ea51 --- /dev/null +++ b/arm/SelectOp.v @@ -0,0 +1,1195 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for operators *) + +(** The instruction selection pass recognizes opportunities for using + combined arithmetic and logical operations and addressing modes + offered by the target processor. For instance, the expression [x + 1] + can take advantage of the "immediate add" instruction of the processor, + and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned + into a "rotate and mask" instruction. + + This file defines functions for building CminorSel expressions and + statements, especially expressions consisting of operator + applications. These functions examine their arguments to choose + cheaper forms of operators whenever possible. + + For instance, [add e1 e2] will return a CminorSel expression semantically + equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a + [Oaddimm] operator if one of the arguments is an integer constant, + or suppress the addition altogether if one of the arguments is the + null integer. In passing, we perform operator reassociation + ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount + of constant propagation. + + On top of the "smart constructor" functions defined below, + module [Selection] implements the actual instruction selection pass. +*) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Cminor. +Require Import Op. +Require Import CminorSel. + +Open Local Scope cminorsel_scope. + +(** ** Integer logical negation *) + +(** The natural way to write smart constructors is by pattern-matching + on their arguments, recognizing cases where cheaper operators + or combined operators are applicable. For instance, integer logical + negation has three special cases (not-and, not-or and not-xor), + along with a default case that uses not-or over its arguments and itself. + This is written naively as follows: +<< +Definition notint (e: expr) := + match e with + | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) + | Eop Onot (t1:::Enil) => t1 + | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) + | _ => Eop Onot (e:::Enil) + end. +>> + However, Coq expands complex pattern-matchings like the above into + elementary matchings over all constructors of an inductive type, + resulting in much duplication of the final catch-all case. + Such duplications generate huge executable code and duplicate + cases in the correctness proofs. + + To limit this duplication, we use the following trick due to + Yves Bertot. We first define a dependent inductive type that + characterizes the expressions that match each of the 4 cases of interest. +*) + +Inductive notint_cases: forall (e: expr), Type := + | notint_case1: + forall s t1, + notint_cases (Eop (Oshift s) (t1:::Enil)) + | notint_case2: + forall t1, + notint_cases (Eop Onot (t1:::Enil)) + | notint_case3: + forall s t1, + notint_cases (Eop (Onotshift s) (t1:::Enil)) + | notint_default: + forall (e: expr), + notint_cases e. + +(** We then define a classification function that takes an expression + and return the case in which it falls. Note that the catch-all case + [notint_default] does not state that it is mutually exclusive with + the first three, more specific cases. The classification function + nonetheless chooses the specific cases in preference to the catch-all + case. *) + +Definition notint_match (e: expr) := + match e as z1 return notint_cases z1 with + | Eop (Oshift s) (t1:::Enil) => + notint_case1 s t1 + | Eop Onot (t1:::Enil) => + notint_case2 t1 + | Eop (Onotshift s) (t1:::Enil) => + notint_case3 s t1 + | e => + notint_default e + end. + +(** Finally, the [notint] function we need is defined by a 4-case match + over the result of the classification function. Thus, no duplication + of the right-hand sides of this match occur, and the proof has only + 4 cases to consider (it proceeds by case over [notint_match e]). + Since the default case is not obviously exclusive with the three + specific cases, it is important that its right-hand side is + semantically correct for all possible values of [e], which is the + case here and for all other smart constructors. *) + +Definition notint (e: expr) := + match notint_match e with + | notint_case1 s t1 => + Eop (Onotshift s) (t1:::Enil) + | notint_case2 t1 => + t1 + | notint_case3 s t1 => + Eop (Oshift s) (t1:::Enil) + | notint_default e => + Eop Onot (e:::Enil) + end. + +(** This programming pattern will be applied systematically for the + other smart constructors in this file. *) + +(** ** Boolean negation *) + +Definition notbool_base (e: expr) := + Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil). + +Fixpoint notbool (e: expr) {struct e} : expr := + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil + | Eop (Ocmp cond) args => + Eop (Ocmp (negate_condition cond)) args + | Econdition e1 e2 e3 => + Econdition e1 (notbool e2) (notbool e3) + | _ => + notbool_base e + end. + +(** ** Integer addition and pointer addition *) + +(** Addition of an integer constant. *) + +(* +Definition addimm (n: int) (e: expr) := + if Int.eq n Int.zero then e else + match e with + | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | _ => Eop (Oaddimm n) (e ::: Enil) + end. +*) + +Inductive addimm_cases: forall (e: expr), Type := + | addimm_case1: + forall m, + addimm_cases (Eop (Ointconst m) Enil) + | addimm_case2: + forall s m, + addimm_cases (Eop (Oaddrsymbol s m) Enil) + | addimm_case3: + forall m, + addimm_cases (Eop (Oaddrstack m) Enil) + | addimm_case4: + forall m t, + addimm_cases (Eop (Oaddimm m) (t ::: Enil)) + | addimm_default: + forall (e: expr), + addimm_cases e. + +Definition addimm_match (e: expr) := + match e as z1 return addimm_cases z1 with + | Eop (Ointconst m) Enil => + addimm_case1 m + | Eop (Oaddrsymbol s m) Enil => + addimm_case2 s m + | Eop (Oaddrstack m) Enil => + addimm_case3 m + | Eop (Oaddimm m) (t ::: Enil) => + addimm_case4 m t + | e => + addimm_default e + end. + +Definition addimm (n: int) (e: expr) := + if Int.eq n Int.zero then e else + match addimm_match e with + | addimm_case1 m => + Eop (Ointconst(Int.add n m)) Enil + | addimm_case2 s m => + Eop (Oaddrsymbol s (Int.add n m)) Enil + | addimm_case3 m => + Eop (Oaddrstack (Int.add n m)) Enil + | addimm_case4 m t => + Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | addimm_default e => + Eop (Oaddimm n) (e ::: Enil) + end. + +(** Addition of two integer or pointer expressions. *) + +(* +Definition add (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) + | Eop(Oaddimm n1) (t1:::Enil)), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) + | _, _ => Eop Oadd (e1:::e2:::Enil) + end. +*) + +Inductive add_cases: forall (e1: expr) (e2: expr), Type := + | add_case1: + forall n1 t2, + add_cases (Eop (Ointconst n1) Enil) (t2) + | add_case2: + forall n1 t1 n2 t2, + add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) + | add_case3: + forall n1 t1 t2, + add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) + | add_case4: + forall t1 n2, + add_cases (t1) (Eop (Ointconst n2) Enil) + | add_case5: + forall t1 n2 t2, + add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) + | add_case6: + forall s t1 t2, + add_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | add_case7: + forall t1 s t2, + add_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | add_default: + forall (e1: expr) (e2: expr), + add_cases e1 e2. + +Definition add_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return add_cases z1 z2 with + | Eop (Ointconst n1) Enil, t2 => + add_case1 n1 t2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + add_case2 n1 t1 n2 t2 + | Eop(Oaddimm n1) (t1:::Enil), t2 => + add_case3 n1 t1 t2 + | t1, Eop (Ointconst n2) Enil => + add_case4 t1 n2 + | t1, Eop (Oaddimm n2) (t2:::Enil) => + add_case5 t1 n2 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + add_case6 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + add_case7 t1 s t2 + | e1, e2 => + add_default e1 e2 + end. + +Definition add (e1: expr) (e2: expr) := + match add_match e1 e2 with + | add_case1 n1 t2 => + addimm n1 t2 + | add_case2 n1 t1 n2 t2 => + addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) + | add_case3 n1 t1 t2 => + addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | add_case4 t1 n2 => + addimm n2 t1 + | add_case5 t1 n2 t2 => + addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | add_case6 s t1 t2 => + Eop (Oaddshift s) (t2:::t1:::Enil) + | add_case7 t1 s t2 => + Eop (Oaddshift s) (t1:::t2:::Enil) + | add_default e1 e2 => + Eop Oadd (e1:::e2:::Enil) + end. + +(** ** Integer and pointer subtraction *) + +(* +Definition sub (e1: expr) (e2: expr) := + match e1, e2 with + | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (intsub n1 n2) (Eop Osub (t1:::t2:::Enil)) + | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Osub (t1:::t2:::Rnil)) + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1::::t2:::Enil)) + | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) + | _, _ => Eop Osub (e1:::e2:::Enil) + end. +*) + +Inductive sub_cases: forall (e1: expr) (e2: expr), Type := + | sub_case1: + forall t1 n2, + sub_cases (t1) (Eop (Ointconst n2) Enil) + | sub_case2: + forall n1 t1 n2 t2, + sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) + | sub_case3: + forall n1 t1 t2, + sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) + | sub_case4: + forall t1 n2 t2, + sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) + | sub_case5: + forall n1 t2, + sub_cases (Eop (Ointconst n1) Enil) (t2) + | sub_case6: + forall s t1 t2, + sub_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | sub_case7: + forall t1 s t2, + sub_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | sub_default: + forall (e1: expr) (e2: expr), + sub_cases e1 e2. + +Definition sub_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return sub_cases z1 z2 with + | t1, Eop (Ointconst n2) Enil => + sub_case1 t1 n2 + | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => + sub_case2 n1 t1 n2 t2 + | Eop (Oaddimm n1) (t1:::Enil), t2 => + sub_case3 n1 t1 t2 + | t1, Eop (Oaddimm n2) (t2:::Enil) => + sub_case4 t1 n2 t2 + | Eop (Ointconst n1) Enil, t2 => + sub_case5 n1 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + sub_case6 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + sub_case7 t1 s t2 + | e1, e2 => + sub_default e1 e2 + end. + +Definition sub (e1: expr) (e2: expr) := + match sub_match e1 e2 with + | sub_case1 t1 n2 => + addimm (Int.neg n2) t1 + | sub_case2 n1 t1 n2 t2 => + addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) + | sub_case3 n1 t1 t2 => + addimm n1 (Eop Osub (t1:::t2:::Enil)) + | sub_case4 t1 n2 t2 => + addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + | sub_case5 n1 t2 => + Eop (Orsubimm n1) (t2:::Enil) + | sub_case6 s t1 t2 => + Eop (Orsubshift s) (t2:::t1:::Enil) + | sub_case7 t1 s t2 => + Eop (Osubshift s) (t1:::t2:::Enil) + | sub_default e1 e2 => + Eop Osub (e1:::e2:::Enil) + end. + +(** ** Immediate shifts *) + +(* +Definition shlimm (e1: expr) := + if Int.eq n Int.zero then e1 else + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) + | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil) + | _ => Eop (Oshift (Olsl n)) (e1:::Enil) + end. +*) + +Inductive shlimm_cases: forall (e1: expr), Type := + | shlimm_case1: + forall n1, + shlimm_cases (Eop (Ointconst n1) Enil) + | shlimm_case2: + forall n1 t1, + shlimm_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) + | shlimm_default: + forall (e1: expr), + shlimm_cases e1. + +Definition shlimm_match (e1: expr) := + match e1 as z1 return shlimm_cases z1 with + | Eop (Ointconst n1) Enil => + shlimm_case1 n1 + | Eop (Oshift (Slsl n1)) (t1:::Enil) => + shlimm_case2 n1 t1 + | e1 => + shlimm_default e1 + end. + +Definition shlimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shlimm_match e1 with + | shlimm_case1 n1 => + Eop (Ointconst(Int.shl n1 n)) Enil + | shlimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Slsl n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Slsl n'')) (t1:::Enil) + end + | shlimm_default e1 => + Eop (Oshift (Slsl n')) (e1:::Enil) + end + end. + +(* +Definition shruimm (e1: expr) := + if Int.eq n Int.zero then e1 else + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) + | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil) + | _ => Eop (Oshift (Olsr n)) (e1:::Enil) + end. +*) + +Inductive shruimm_cases: forall (e1: expr), Type := + | shruimm_case1: + forall n1, + shruimm_cases (Eop (Ointconst n1) Enil) + | shruimm_case2: + forall n1 t1, + shruimm_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) + | shruimm_default: + forall (e1: expr), + shruimm_cases e1. + +Definition shruimm_match (e1: expr) := + match e1 as z1 return shruimm_cases z1 with + | Eop (Ointconst n1) Enil => + shruimm_case1 n1 + | Eop (Oshift (Slsr n1)) (t1:::Enil) => + shruimm_case2 n1 t1 + | e1 => + shruimm_default e1 + end. + +Definition shruimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shruimm_match e1 with + | shruimm_case1 n1 => + Eop (Ointconst(Int.shru n1 n)) Enil + | shruimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Slsr n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Slsr n'')) (t1:::Enil) + end + | shruimm_default e1 => + Eop (Oshift (Slsr n')) (e1:::Enil) + end + end. + +(* +Definition shrimm (e1: expr) := + match e1 with + | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) + | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil) + | _ => Eop (Oshift (Oasr n)) (e1:::Enil) + end. +*) + +Inductive shrimm_cases: forall (e1: expr), Type := + | shrimm_case1: + forall n1, + shrimm_cases (Eop (Ointconst n1) Enil) + | shrimm_case2: + forall n1 t1, + shrimm_cases (Eop (Oshift (Sasr n1)) (t1:::Enil)) + | shrimm_default: + forall (e1: expr), + shrimm_cases e1. + +Definition shrimm_match (e1: expr) := + match e1 as z1 return shrimm_cases z1 with + | Eop (Ointconst n1) Enil => + shrimm_case1 n1 + | Eop (Oshift (Sasr n1)) (t1:::Enil) => + shrimm_case2 n1 t1 + | e1 => + shrimm_default e1 + end. + +Definition shrimm (e1: expr) (n: int) := + if Int.eq n Int.zero then e1 else + match is_shift_amount n with + | None => Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) + | Some n' => + match shrimm_match e1 with + | shrimm_case1 n1 => + Eop (Ointconst(Int.shr n1 n)) Enil + | shrimm_case2 n1 t1 => + match is_shift_amount (Int.add n (s_amount n1)) with + | None => + Eop (Oshift (Sasr n')) (e1:::Enil) + | Some n'' => + Eop (Oshift (Sasr n'')) (t1:::Enil) + end + | shrimm_default e1 => + Eop (Oshift (Sasr n')) (e1:::Enil) + end + end. + +(** ** Integer multiply *) + +Definition mulimm_base (n1: int) (e2: expr) := + match Int.one_bits n1 with + | i :: nil => + shlimm e2 i + | i :: j :: nil => + Elet e2 + (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) + | _ => + Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) + end. + +(* +Definition mulimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then + Eop (Ointconst Int.zero) Enil + else if Int.eq n1 Int.one then + e2 + else match e2 with + | Eop (Ointconst n2) Enil => Eop (Ointconst(intmul n1 n2)) Enil + | Eop (Oaddimm n2) (t2:::Enil) => addimm (intmul n1 n2) (mulimm_base n1 t2) + | _ => mulimm_base n1 e2 + end. +*) + +Inductive mulimm_cases: forall (e2: expr), Type := + | mulimm_case1: + forall (n2: int), + mulimm_cases (Eop (Ointconst n2) Enil) + | mulimm_case2: + forall (n2: int) (t2: expr), + mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) + | mulimm_default: + forall (e2: expr), + mulimm_cases e2. + +Definition mulimm_match (e2: expr) := + match e2 as z1 return mulimm_cases z1 with + | Eop (Ointconst n2) Enil => + mulimm_case1 n2 + | Eop (Oaddimm n2) (t2:::Enil) => + mulimm_case2 n2 t2 + | e2 => + mulimm_default e2 + end. + +Definition mulimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then + Eop (Ointconst Int.zero) Enil + else if Int.eq n1 Int.one then + e2 + else match mulimm_match e2 with + | mulimm_case1 n2 => + Eop (Ointconst(Int.mul n1 n2)) Enil + | mulimm_case2 n2 t2 => + addimm (Int.mul n1 n2) (mulimm_base n1 t2) + | mulimm_default e2 => + mulimm_base n1 e2 + end. + +(* +Definition mul (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 + | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 + | _, _ => Eop Omul (e1:::e2:::Enil) + end. +*) + +Inductive mul_cases: forall (e1: expr) (e2: expr), Type := + | mul_case1: + forall (n1: int) (t2: expr), + mul_cases (Eop (Ointconst n1) Enil) (t2) + | mul_case2: + forall (t1: expr) (n2: int), + mul_cases (t1) (Eop (Ointconst n2) Enil) + | mul_default: + forall (e1: expr) (e2: expr), + mul_cases e1 e2. + +Definition mul_match_aux (e1: expr) (e2: expr) := + match e2 as z2 return mul_cases e1 z2 with + | Eop (Ointconst n2) Enil => + mul_case2 e1 n2 + | e2 => + mul_default e1 e2 + end. + +Definition mul_match (e1: expr) (e2: expr) := + match e1 as z1 return mul_cases z1 e2 with + | Eop (Ointconst n1) Enil => + mul_case1 n1 e2 + | e1 => + mul_match_aux e1 e2 + end. + +Definition mul (e1: expr) (e2: expr) := + match mul_match e1 e2 with + | mul_case1 n1 t2 => + mulimm n1 t2 + | mul_case2 t1 n2 => + mulimm n2 t1 + | mul_default e1 e2 => + Eop Omul (e1:::e2:::Enil) + end. + +(** ** Integer division and modulus *) + +Definition mod_aux (divop: operation) (e1 e2: expr) := + Elet e1 + (Elet (lift e2) + (Eop Osub (Eletvar 1 ::: + Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: + Eletvar 0 ::: + Enil) ::: + Enil))). + +Inductive divu_cases: forall (e2: expr), Type := + | divu_case1: + forall (n2: int), + divu_cases (Eop (Ointconst n2) Enil) + | divu_default: + forall (e2: expr), + divu_cases e2. + +Definition divu_match (e2: expr) := + match e2 as z1 return divu_cases z1 with + | Eop (Ointconst n2) Enil => + divu_case1 n2 + | e2 => + divu_default e2 + end. + +Definition divu (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => shruimm e1 l2 + | None => Eop Odivu (e1:::e2:::Enil) + end + | divu_default e2 => + Eop Odivu (e1:::e2:::Enil) + end. + +Definition modu (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => Eop (Oandimm (Int.sub n2 Int.one)) (e1:::Enil) + | None => mod_aux Odivu e1 e2 + end + | divu_default e2 => + mod_aux Odivu e1 e2 + end. + +Definition divs (e1: expr) (e2: expr) := + match divu_match e2 with + | divu_case1 n2 => + match Int.is_power2 n2 with + | Some l2 => if Int.ltu l2 (Int.repr 31) + then Eop (Oshrximm l2) (e1:::Enil) + else Eop Odiv (e1:::e2:::Enil) + | None => Eop Odiv (e1:::e2:::Enil) + end + | divu_default e2 => + Eop Odiv (e1:::e2:::Enil) + end. + +Definition mods := mod_aux Odiv. (* could be improved *) + + +(** ** Bitwise and, or, xor *) + +(* +Definition and (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) + | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) + | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) + | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) + | _, _ => Eop Oand (e1:::e2:::Enil) + end. +*) + +Inductive and_cases: forall (e1: expr) (e2: expr), Type := + | and_case1: + forall s t1 t2, + and_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | and_case2: + forall t1 s t2, + and_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | and_case3: + forall s t1 t2, + and_cases (Eop (Onotshift s) (t1:::Enil)) (t2) + | and_case4: + forall t1 s t2, + and_cases (t1) (Eop (Onotshift s) (t2:::Enil)) + | and_case5: + forall t1 t2, + and_cases (Eop Onot (t1:::Enil)) (t2) + | and_case6: + forall t1 t2, + and_cases (t1) (Eop Onot (t2:::Enil)) + | and_default: + forall (e1: expr) (e2: expr), + and_cases e1 e2. + +Definition and_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return and_cases z1 z2 with + | Eop (Oshift s) (t1:::Enil), t2 => + and_case1 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + and_case2 t1 s t2 + | Eop (Onotshift s) (t1:::Enil), t2 => + and_case3 s t1 t2 + | t1, Eop (Onotshift s) (t2:::Enil) => + and_case4 t1 s t2 + | Eop Onot (t1:::Enil), t2 => + and_case5 t1 t2 + | t1, Eop Onot (t2:::Enil) => + and_case6 t1 t2 + | e1, e2 => + and_default e1 e2 + end. + +Definition and (e1: expr) (e2: expr) := + match and_match e1 e2 with + | and_case1 s t1 t2 => + Eop (Oandshift s) (t2:::t1:::Enil) + | and_case2 t1 s t2 => + Eop (Oandshift s) (t1:::t2:::Enil) + | and_case3 s t1 t2 => + Eop (Obicshift s) (t2:::t1:::Enil) + | and_case4 t1 s t2 => + Eop (Obicshift s) (t1:::t2:::Enil) + | and_case5 t1 t2 => + Eop Obic (t2:::t1:::Enil) + | and_case6 t1 t2 => + Eop Obic (t1:::t2:::Enil) + | and_default e1 e2 => + Eop Oand (e1:::e2:::Enil) + end. + +Definition same_expr_pure (e1 e2: expr) := + match e1, e2 with + | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false + | _, _ => false + end. + +(* +Definition or (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift (Olsl n1) (t1:::Enil), Eop (Oshift (Olsr n2) (t2:::Enil)) => ... + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oor (e1:::e2:::Enil) + end. +*) + +(* TODO: symmetric of first case *) + +Inductive or_cases: forall (e1: expr) (e2: expr), Type := + | or_case1: + forall n1 t1 n2 t2, + or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil)) + | or_case2: + forall s t1 t2, + or_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | or_case3: + forall t1 s t2, + or_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | or_default: + forall (e1: expr) (e2: expr), + or_cases e1 e2. + +Definition or_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return or_cases z1 z2 with + | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => + or_case1 n1 t1 n2 t2 + | Eop (Oshift s) (t1:::Enil), t2 => + or_case2 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + or_case3 t1 s t2 + | e1, e2 => + or_default e1 e2 + end. + +Definition or (e1: expr) (e2: expr) := + match or_match e1 e2 with + | or_case1 n1 t1 n2 t2 => + if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n2)) (t1:::Enil) + else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) + | or_case2 s t1 t2 => + Eop (Oorshift s) (t2:::t1:::Enil) + | or_case3 t1 s t2 => + Eop (Oorshift s) (t1:::t2:::Enil) + | or_default e1 e2 => + Eop Oor (e1:::e2:::Enil) + end. + +(* +Definition xor (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oxor (e1:::e2:::Enil) + end. +*) + +Inductive xor_cases: forall (e1: expr) (e2: expr), Type := + | xor_case1: + forall s t1 t2, + xor_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | xor_case2: + forall t1 s t2, + xor_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | xor_default: + forall (e1: expr) (e2: expr), + xor_cases e1 e2. + +Definition xor_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return xor_cases z1 z2 with + | Eop (Oshift s) (t1:::Enil), t2 => + xor_case1 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + xor_case2 t1 s t2 + | e1, e2 => + xor_default e1 e2 + end. + +Definition xor (e1: expr) (e2: expr) := + match xor_match e1 e2 with + | xor_case1 s t1 t2 => + Eop (Oxorshift s) (t2:::t1:::Enil) + | xor_case2 t1 s t2 => + Eop (Oxorshift s) (t1:::t2:::Enil) + | xor_default e1 e2 => + Eop Oxor (e1:::e2:::Enil) + end. + +(** ** General shifts *) + +Inductive shift_cases: forall (e1: expr), Type := + | shift_case1: + forall (n2: int), + shift_cases (Eop (Ointconst n2) Enil) + | shift_default: + forall (e1: expr), + shift_cases e1. + +Definition shift_match (e1: expr) := + match e1 as z1 return shift_cases z1 with + | Eop (Ointconst n2) Enil => + shift_case1 n2 + | e1 => + shift_default e1 + end. + +Definition shl (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shlimm e1 n2 + | shift_default e2 => + Eop Oshl (e1:::e2:::Enil) + end. + +Definition shru (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shruimm e1 n2 + | shift_default e2 => + Eop Oshru (e1:::e2:::Enil) + end. + +Definition shr (e1: expr) (e2: expr) := + match shift_match e2 with + | shift_case1 n2 => + shrimm e1 n2 + | shift_default e2 => + Eop Oshr (e1:::e2:::Enil) + end. + +(** ** Truncations and sign extensions *) + +Inductive cast8signed_cases: forall (e1: expr), Type := + | cast8signed_case1: + forall (e2: expr), + cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) + | cast8signed_default: + forall (e1: expr), + cast8signed_cases e1. + +Definition cast8signed_match (e1: expr) := + match e1 as z1 return cast8signed_cases z1 with + | Eop Ocast8signed (e2 ::: Enil) => + cast8signed_case1 e2 + | e1 => + cast8signed_default e1 + end. + +Definition cast8signed (e: expr) := + match cast8signed_match e with + | cast8signed_case1 e1 => e + | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) + end. + +Inductive cast8unsigned_cases: forall (e1: expr), Type := + | cast8unsigned_case1: + forall (e2: expr), + cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) + | cast8unsigned_default: + forall (e1: expr), + cast8unsigned_cases e1. + +Definition cast8unsigned_match (e1: expr) := + match e1 as z1 return cast8unsigned_cases z1 with + | Eop Ocast8unsigned (e2 ::: Enil) => + cast8unsigned_case1 e2 + | e1 => + cast8unsigned_default e1 + end. + +Definition cast8unsigned (e: expr) := + match cast8unsigned_match e with + | cast8unsigned_case1 e1 => e + | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) + end. + +Inductive cast16signed_cases: forall (e1: expr), Type := + | cast16signed_case1: + forall (e2: expr), + cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) + | cast16signed_default: + forall (e1: expr), + cast16signed_cases e1. + +Definition cast16signed_match (e1: expr) := + match e1 as z1 return cast16signed_cases z1 with + | Eop Ocast16signed (e2 ::: Enil) => + cast16signed_case1 e2 + | e1 => + cast16signed_default e1 + end. + +Definition cast16signed (e: expr) := + match cast16signed_match e with + | cast16signed_case1 e1 => e + | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) + end. + +Inductive cast16unsigned_cases: forall (e1: expr), Type := + | cast16unsigned_case1: + forall (e2: expr), + cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) + | cast16unsigned_default: + forall (e1: expr), + cast16unsigned_cases e1. + +Definition cast16unsigned_match (e1: expr) := + match e1 as z1 return cast16unsigned_cases z1 with + | Eop Ocast16unsigned (e2 ::: Enil) => + cast16unsigned_case1 e2 + | e1 => + cast16unsigned_default e1 + end. + +Definition cast16unsigned (e: expr) := + match cast16unsigned_match e with + | cast16unsigned_case1 e1 => e + | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) + end. + +Inductive singleoffloat_cases: forall (e1: expr), Type := + | singleoffloat_case1: + forall (e2: expr), + singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) + | singleoffloat_default: + forall (e1: expr), + singleoffloat_cases e1. + +Definition singleoffloat_match (e1: expr) := + match e1 as z1 return singleoffloat_cases z1 with + | Eop Osingleoffloat (e2 ::: Enil) => + singleoffloat_case1 e2 + | e1 => + singleoffloat_default e1 + end. + +Definition singleoffloat (e: expr) := + match singleoffloat_match e with + | singleoffloat_case1 e1 => e + | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) + end. + +(** ** Comparisons *) + +(* +Definition comp (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => Eop (Ocmp (Ccompimm c n1)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | _, _ => Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) + end. +*) + +Inductive comp_cases: forall (e1: expr) (e2: expr), Type := + | comp_case1: + forall n1 t2, + comp_cases (Eop (Ointconst n1) Enil) (t2) + | comp_case2: + forall t1 n2, + comp_cases (t1) (Eop (Ointconst n2) Enil) + | comp_case3: + forall s t1 t2, + comp_cases (Eop (Oshift s) (t1:::Enil)) (t2) + | comp_case4: + forall t1 s t2, + comp_cases (t1) (Eop (Oshift s) (t2:::Enil)) + | comp_default: + forall (e1: expr) (e2: expr), + comp_cases e1 e2. + +Definition comp_match (e1: expr) (e2: expr) := + match e1 as z1, e2 as z2 return comp_cases z1 z2 with + | Eop (Ointconst n1) Enil, t2 => + comp_case1 n1 t2 + | t1, Eop (Ointconst n2) Enil => + comp_case2 t1 n2 + | Eop (Oshift s) (t1:::Enil), t2 => + comp_case3 s t1 t2 + | t1, Eop (Oshift s) (t2:::Enil) => + comp_case4 t1 s t2 + | e1, e2 => + comp_default e1 e2 + end. + +Definition comp (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) + | comp_case3 s t1 t2 => + Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | comp_case4 t1 s t2 => + Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) + end. + +Definition compu (c: comparison) (e1: expr) (e2: expr) := + match comp_match e1 e2 with + | comp_case1 n1 t2 => + Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) + | comp_case2 t1 n2 => + Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) + | comp_case3 s t1 t2 => + Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) + | comp_case4 t1 s t2 => + Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) + | comp_default e1 e2 => + Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) + end. + +Definition compf (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). + +(** ** Other operators, not optimized. *) + +Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). +Definition negf (e: expr) := Eop Onegf (e ::: Enil). +Definition absf (e: expr) := Eop Oabsf (e ::: Enil). +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). +Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). +Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). +Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). +Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). +Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). +Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). +Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). + +(** ** Recognition of addressing modes for load and store operations *) + +(* +Definition addressing (e: expr) := + match e with + | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) + | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) + | Eop (Oaddshift s) (e1:::e2:::Enil) => (Aindexed2shift s, e1:::e2:::Enil) + | Eop Oadd (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) + | _ => (Aindexed Int.zero, e:::Enil) + end. +*) + +Inductive addressing_cases: forall (e: expr), Type := + | addressing_case2: + forall n, + addressing_cases (Eop (Oaddrstack n) Enil) + | addressing_case3: + forall n e1, + addressing_cases (Eop (Oaddimm n) (e1:::Enil)) + | addressing_case4: + forall s e1 e2, + addressing_cases (Eop (Oaddshift s) (e1:::e2:::Enil)) + | addressing_case5: + forall e1 e2, + addressing_cases (Eop Oadd (e1:::e2:::Enil)) + | addressing_default: + forall (e: expr), + addressing_cases e. + +Definition addressing_match (e: expr) := + match e as z1 return addressing_cases z1 with + | Eop (Oaddrstack n) Enil => + addressing_case2 n + | Eop (Oaddimm n) (e1:::Enil) => + addressing_case3 n e1 + | Eop (Oaddshift s) (e1:::e2:::Enil) => + addressing_case4 s e1 e2 + | Eop Oadd (e1:::e2:::Enil) => + addressing_case5 e1 e2 + | e => + addressing_default e + end. + +(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes + for floating-point accesses, since these are not supported + by the hardware and emulated inefficiently in [ARMgen]. *) + +Definition is_float_addressing (chunk: memory_chunk): bool := + match chunk with + | Mfloat32 => true + | Mfloat64 => true + | _ => false + end. + +Definition addressing (chunk: memory_chunk) (e: expr) := + match addressing_match e with + | addressing_case2 n => + (Ainstack n, Enil) + | addressing_case3 n e1 => + (Aindexed n, e1:::Enil) + | addressing_case4 s e1 e2 => + if is_float_addressing chunk + then (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) + else (Aindexed2shift s, e1:::e2:::Enil) + | addressing_case5 e1 e2 => + if is_float_addressing chunk + then (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) + else (Aindexed2, e1:::e2:::Enil) + | addressing_default e => + (Aindexed Int.zero, e:::Enil) + end. + diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v new file mode 100644 index 00000000..68b49fd8 --- /dev/null +++ b/arm/SelectOpproof.v @@ -0,0 +1,986 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness of instruction selection for operators *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +Section CMCONSTR. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + +(** * Useful lemmas and tactics *) + +(** The following are trivial lemmas and custom tactics that help + perform backward (inversion) and forward reasoning over the evaluation + of operator applications. *) + +Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. + +Ltac TrivialOp cstr := unfold cstr; intros; EvalOp. + +Ltac InvEval1 := + match goal with + | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] => + inv H; InvEval1 + | _ => + idtac + end. + +Ltac InvEval2 := + match goal with + | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] => + simpl in H; inv H + | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] => + simpl in H; FuncInv + | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] => + simpl in H; FuncInv + | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] => + simpl in H; FuncInv + | _ => + idtac + end. + +Ltac InvEval := InvEval1; InvEval2; InvEval2. + +(** * Correctness of the smart constructors *) + +(** We now show that the code generated by "smart constructor" functions + such as [Selection.notint] behaves as expected. Continuing the + [notint] example, we show that if the expression [e] + evaluates to some integer value [Vint n], then [Selection.notint e] + evaluates to a value [Vint (Int.not n)] which is indeed the integer + negation of the value of [e]. + + All proofs follow a common pattern: +- Reasoning by case over the result of the classification functions + (such as [add_match] for integer addition), gathering additional + information on the shape of the argument expressions in the non-default + cases. +- Inversion of the evaluations of the arguments, exploiting the additional + information thus gathered. +- Equational reasoning over the arithmetic operations performed, + using the lemmas from the [Int] and [Float] modules. +- Construction of an evaluation derivation for the expression returned + by the smart constructor. +*) + +Theorem eval_notint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (notint a) (Vint (Int.not x)). +Proof. + unfold notint; intros until x; case (notint_match a); intros; InvEval. + EvalOp. simpl. congruence. + subst x. rewrite Int.not_involutive. auto. + EvalOp. simpl. subst x. rewrite Int.not_involutive. auto. + EvalOp. +Qed. + +Lemma eval_notbool_base: + forall le a v b, + eval_expr ge sp e m le a v -> + Val.bool_of_val v b -> + eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)). +Proof. + TrivialOp notbool_base. simpl. + inv H0. + rewrite Int.eq_false; auto. + rewrite Int.eq_true; auto. + reflexivity. +Qed. + +Hint Resolve Val.bool_of_true_val Val.bool_of_false_val + Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. + +Theorem eval_notbool: + forall le a v b, + eval_expr ge sp e m le a v -> + Val.bool_of_val v b -> + eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)). +Proof. + induction a; simpl; intros; try (eapply eval_notbool_base; eauto). + destruct o; try (eapply eval_notbool_base; eauto). + + destruct e0. InvEval. + inv H0. rewrite Int.eq_false; auto. + simpl; eauto with evalexpr. + rewrite Int.eq_true; simpl; eauto with evalexpr. + eapply eval_notbool_base; eauto. + + inv H. eapply eval_Eop; eauto. + simpl. assert (eval_condition c vl = Some b). + generalize H6. simpl. + case (eval_condition c vl); intros. + destruct b0; inv H1; inversion H0; auto; congruence. + congruence. + rewrite (Op.eval_negate_condition _ _ H). + destruct b; reflexivity. + + inv H. eapply eval_Econdition; eauto. + destruct v1; eauto. +Qed. + +Theorem eval_addimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)). +Proof. + unfold addimm; intros until x. + generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. + subst n. rewrite Int.add_zero. auto. + case (addimm_match a); intros; InvEval; EvalOp; simpl. + rewrite Int.add_commut. auto. + destruct (Genv.find_symbol ge s); discriminate. + destruct sp; simpl in H1; discriminate. + subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. +Qed. + +Theorem eval_addimm_ptr: + forall le n a b ofs, + eval_expr ge sp e m le a (Vptr b ofs) -> + eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)). +Proof. + unfold addimm; intros until ofs. + generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. + subst n. rewrite Int.add_zero. auto. + case (addimm_match a); intros; InvEval; EvalOp; simpl. + destruct (Genv.find_symbol ge s). + rewrite Int.add_commut. congruence. + discriminate. + destruct sp; simpl in H1; try discriminate. + inv H1. simpl. decEq. decEq. + rewrite Int.add_assoc. decEq. apply Int.add_commut. + subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto. +Qed. + +Theorem eval_add: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vint (Int.add x y)). +Proof. + intros until y. + unfold add; case (add_match a b); intros; InvEval. + rewrite Int.add_commut. apply eval_addimm. auto. + replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). + apply eval_addimm. EvalOp. + subst x; subst y. + repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + replace (Int.add x y) with (Int.add (Int.add i y) n1). + apply eval_addimm. EvalOp. + subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + apply eval_addimm. auto. + replace (Int.add x y) with (Int.add (Int.add x i) n2). + apply eval_addimm. EvalOp. + subst y. rewrite Int.add_assoc. auto. + EvalOp. simpl. subst x. rewrite Int.add_commut. auto. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_add_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)). +Proof. + intros until y. unfold add; case (add_match a b); intros; InvEval. + replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). + apply eval_addimm_ptr. subst b0. EvalOp. + subst x; subst y. + repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. + replace (Int.add x y) with (Int.add (Int.add i y) n1). + apply eval_addimm_ptr. subst b0. EvalOp. + subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + apply eval_addimm_ptr. auto. + replace (Int.add x y) with (Int.add (Int.add x i) n2). + apply eval_addimm_ptr. EvalOp. + subst y. rewrite Int.add_assoc. auto. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_add_ptr_2: + forall le a b x p y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)). +Proof. + intros until y. unfold add; case (add_match a b); intros; InvEval. + apply eval_addimm_ptr. auto. + replace (Int.add y x) with (Int.add (Int.add i i0) (Int.add n1 n2)). + apply eval_addimm_ptr. subst b0. EvalOp. + subst x; subst y. + repeat rewrite Int.add_assoc. decEq. + rewrite (Int.add_commut n1 n2). apply Int.add_permut. + replace (Int.add y x) with (Int.add (Int.add y i) n1). + apply eval_addimm_ptr. EvalOp. + subst x. repeat rewrite Int.add_assoc. auto. + replace (Int.add y x) with (Int.add (Int.add i x) n2). + apply eval_addimm_ptr. EvalOp. subst b0; reflexivity. + subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_sub: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm. assumption. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm. EvalOp. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm. EvalOp. + subst x. rewrite Int.sub_add_l. auto. + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm. EvalOp. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. + EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_sub_ptr_int: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm_ptr. assumption. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm_ptr. EvalOp. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm_ptr. EvalOp. + subst x. rewrite Int.sub_add_l. auto. + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm_ptr. EvalOp. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_sub_ptr_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). +Proof. + intros until y. + unfold sub; case (sub_match a b); intros; InvEval. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). + apply eval_addimm. EvalOp. + simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto. + subst x; subst y. + repeat rewrite Int.sub_add_opp. + repeat rewrite Int.add_assoc. decEq. + rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + apply eval_addimm. EvalOp. + simpl. unfold eq_block. rewrite zeq_true. auto. + subst x. rewrite Int.sub_add_l. auto. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + apply eval_addimm. EvalOp. + simpl. unfold eq_block. rewrite zeq_true. auto. + subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. + EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. +Qed. + +Theorem eval_shlimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n (Int.repr 32) = true -> + eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). +Proof. + intros until x. unfold shlimm, is_shift_amount. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. + intros. subst n. rewrite Int.shl_zero. auto. + destruct (is_shift_amount_aux n). simpl. + case (shlimm_match a); intros; InvEval. + EvalOp. + destruct (is_shift_amount_aux (Int.add n (s_amount n1))). + EvalOp. simpl. subst x. + decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shl_shl. + apply s_amount_ltu. auto. + rewrite Int.add_commut. auto. + EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. + simpl. congruence. + EvalOp. + congruence. +Qed. + +Theorem eval_shruimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n (Int.repr 32) = true -> + eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). +Proof. + intros until x. unfold shruimm, is_shift_amount. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. + intros. subst n. rewrite Int.shru_zero. auto. + destruct (is_shift_amount_aux n). simpl. + case (shruimm_match a); intros; InvEval. + EvalOp. + destruct (is_shift_amount_aux (Int.add n (s_amount n1))). + EvalOp. simpl. subst x. + decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shru_shru. + apply s_amount_ltu. auto. + rewrite Int.add_commut. auto. + EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. + simpl. congruence. + EvalOp. + congruence. +Qed. + +Theorem eval_shrimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + Int.ltu n (Int.repr 32) = true -> + eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)). +Proof. + intros until x. unfold shrimm, is_shift_amount. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. + intros. subst n. rewrite Int.shr_zero. auto. + destruct (is_shift_amount_aux n). simpl. + case (shrimm_match a); intros; InvEval. + EvalOp. + destruct (is_shift_amount_aux (Int.add n (s_amount n1))). + EvalOp. simpl. subst x. + decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shr_shr. + apply s_amount_ltu. auto. + rewrite Int.add_commut. auto. + EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. + simpl. congruence. + EvalOp. + congruence. +Qed. + +Lemma eval_mulimm_base: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)). +Proof. + intros; unfold mulimm_base. + generalize (Int.one_bits_decomp n). + generalize (Int.one_bits_range n). + change (Z_of_nat wordsize) with 32. + destruct (Int.one_bits n). + intros. EvalOp. constructor. EvalOp. simpl; reflexivity. + constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. + destruct l. + intros. rewrite H1. simpl. + rewrite Int.add_zero. rewrite <- Int.shl_mul. + apply eval_shlimm. auto. auto with coqlib. + destruct l. + intros. apply eval_Elet with (Vint x). auto. + rewrite H1. simpl. rewrite Int.add_zero. + rewrite Int.mul_add_distr_r. + rewrite <- Int.shl_mul. + rewrite <- Int.shl_mul. + apply eval_add. + apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. + auto with coqlib. + apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. + auto with coqlib. + intros. EvalOp. constructor. EvalOp. simpl; reflexivity. + constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. +Qed. + +Theorem eval_mulimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)). +Proof. + intros until x; unfold mulimm. + generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. + subst n. rewrite Int.mul_zero. + intro. EvalOp. + generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. + subst n. rewrite Int.mul_one. auto. + case (mulimm_match a); intros; InvEval. + EvalOp. rewrite Int.mul_commut. reflexivity. + replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)). + apply eval_addimm. apply eval_mulimm_base. auto. + subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut. + apply eval_mulimm_base. assumption. +Qed. + +Theorem eval_mul: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)). +Proof. + intros until y. + unfold mul; case (mul_match a b); intros; InvEval. + rewrite Int.mul_commut. apply eval_mulimm. auto. + apply eval_mulimm. auto. + EvalOp. +Qed. + +Theorem eval_divs_base: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (Eop Odiv (a ::: b ::: Enil)) (Vint (Int.divs x y)). +Proof. + intros. EvalOp; simpl. + predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. +Qed. + +Theorem eval_divs: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)). +Proof. + intros until y. + unfold divs; case (divu_match b); intros; InvEval. + caseEq (Int.is_power2 y); intros. + caseEq (Int.ltu i (Int.repr 31)); intros. + EvalOp. simpl. unfold Int.ltu. rewrite zlt_true. + rewrite (Int.divs_pow2 x y i H0). auto. + exploit Int.ltu_inv; eauto. + change (Int.unsigned (Int.repr 31)) with 31. + change (Int.unsigned (Int.repr 32)) with 32. + omega. + apply eval_divs_base. auto. EvalOp. auto. + apply eval_divs_base. auto. EvalOp. auto. + apply eval_divs_base; auto. +Qed. + +Lemma eval_mod_aux: + forall divop semdivop, + (forall sp x y, + y <> Int.zero -> + eval_operation ge sp divop (Vint x :: Vint y :: nil) = + Some (Vint (semdivop x y))) -> + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (mod_aux divop a b) + (Vint (Int.sub x (Int.mul (semdivop x y) y))). +Proof. + intros; unfold mod_aux. + eapply eval_Elet. eexact H0. eapply eval_Elet. + apply eval_lift. eexact H1. + eapply eval_Eop. eapply eval_Econs. + eapply eval_Eletvar. simpl; reflexivity. + eapply eval_Econs. eapply eval_Eop. + eapply eval_Econs. eapply eval_Eop. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + apply eval_Enil. + apply H. assumption. + eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. + apply eval_Enil. + simpl; reflexivity. apply eval_Enil. + reflexivity. +Qed. + +Theorem eval_mods: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)). +Proof. + intros; unfold mods. + rewrite Int.mods_divs. + eapply eval_mod_aux; eauto. + intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. + contradiction. auto. +Qed. + +Lemma eval_divu_base: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)). +Proof. + intros. EvalOp. simpl. + predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. +Qed. + +Theorem eval_divu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)). +Proof. + intros until y. + unfold divu; case (divu_match b); intros; InvEval. + caseEq (Int.is_power2 y). + intros. rewrite (Int.divu_pow2 x y i H0). + apply eval_shruimm. auto. + apply Int.is_power2_range with y. auto. + intros. apply eval_divu_base. auto. EvalOp. auto. + eapply eval_divu_base; eauto. +Qed. + +Theorem eval_modu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + y <> Int.zero -> + eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)). +Proof. + intros until y; unfold modu; case (divu_match b); intros; InvEval. + caseEq (Int.is_power2 y). + intros. rewrite (Int.modu_and x y i H0). + EvalOp. + intro. rewrite Int.modu_divu. eapply eval_mod_aux. + intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. + contradiction. auto. + auto. EvalOp. auto. auto. + rewrite Int.modu_divu. eapply eval_mod_aux. + intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. + contradiction. auto. auto. auto. auto. auto. +Qed. + +Theorem eval_and: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (and a b) (Vint (Int.and x y)). +Proof. + intros until y; unfold and; case (and_match a b); intros; InvEval. + rewrite Int.and_commut. EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + rewrite Int.and_commut. EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + rewrite Int.and_commut. EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Remark eval_same_expr: + forall a1 a2 le v1 v2, + same_expr_pure a1 a2 = true -> + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + a1 = a2 /\ v1 = v2. +Proof. + intros until v2. + destruct a1; simpl; try (intros; discriminate). + destruct a2; simpl; try (intros; discriminate). + case (ident_eq i i0); intros. + subst i0. inversion H0. inversion H1. split. auto. congruence. + discriminate. +Qed. + +Lemma eval_or: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). +Proof. + intros until y; unfold or; case (or_match a b); intros; InvEval. + caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) + && same_expr_pure t1 t2); intro. + destruct (andb_prop _ _ H1). + generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)). + rewrite H4. intro. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. + simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror. + destruct n1; auto. destruct n2; auto. auto. + EvalOp. econstructor. EvalOp. simpl. reflexivity. + econstructor; eauto with evalexpr. + simpl. congruence. + EvalOp. simpl. rewrite Int.or_commut. congruence. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_xor: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)). +Proof. + intros until y; unfold xor; case (xor_match a b); intros; InvEval. + rewrite Int.xor_commut. EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + EvalOp. +Qed. + +Theorem eval_shl: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y (Int.repr 32) = true -> + eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). +Proof. + intros until y; unfold shl; case (shift_match b); intros. + InvEval. apply eval_shlimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_shru: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y (Int.repr 32) = true -> + eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). +Proof. + intros until y; unfold shru; case (shift_match b); intros. + InvEval. apply eval_shruimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_shr: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + Int.ltu y (Int.repr 32) = true -> + eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). +Proof. + intros until y; unfold shr; case (shift_match b); intros. + InvEval. apply eval_shrimm; auto. + EvalOp. simpl. rewrite H1. auto. +Qed. + +Theorem eval_cast8signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). +Proof. + intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. + rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. + EvalOp. +Qed. + +Theorem eval_cast8unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). +Proof. + intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. + rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. + EvalOp. +Qed. + +Theorem eval_cast16signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). +Proof. + intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. + rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. + EvalOp. +Qed. + +Theorem eval_cast16unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). +Proof. + intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. + rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. + EvalOp. +Qed. + +Theorem eval_singleoffloat: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). +Proof. + intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. + EvalOp. +Qed. + +Theorem eval_comp_int: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)). +Proof. + intros until y. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. rewrite Int.swap_cmp. rewrite H. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. +Qed. + +Remark eval_compare_null_trans: + forall c x v, + (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + match eval_compare_null c x with + | Some true => Some Vtrue + | Some false => Some Vfalse + | None => None (A:=val) + end = Some v. +Proof. + unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; try discriminate; auto. +Qed. + +Theorem eval_comp_ptr_int: + forall le c a x1 x2 b y v, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vint y) -> + (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. apply eval_compare_null_trans; auto. + EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto. + EvalOp. simpl. apply eval_compare_null_trans; auto. +Qed. + +Remark eval_swap_compare_null_trans: + forall c x v, + (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + match eval_compare_null (swap_comparison c) x with + | Some true => Some Vtrue + | Some false => Some Vfalse + | None => None (A:=val) + end = Some v. +Proof. + unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. + destruct (Int.eq x Int.zero); try discriminate. + destruct c; simpl; try discriminate; auto. +Qed. + +Theorem eval_comp_int_ptr: + forall le c a x b y1 y2 v, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until v. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. apply eval_swap_compare_null_trans; auto. + EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto. + EvalOp. simpl. apply eval_compare_null_trans; auto. +Qed. + +Theorem eval_comp_ptr_ptr: + forall le c a x1 x2 b y1 y2, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + x1 = y1 -> + eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. subst y1. rewrite dec_eq_true. + destruct (Int.cmp c x2 y2); reflexivity. +Qed. + +Theorem eval_comp_ptr_ptr_2: + forall le c a x1 x2 b y1 y2 v, + eval_expr ge sp e m le a (Vptr x1 x2) -> + eval_expr ge sp e m le b (Vptr y1 y2) -> + x1 <> y1 -> + Cminor.eval_compare_mismatch c = Some v -> + eval_expr ge sp e m le (comp c a b) v. +Proof. + intros until y2. + unfold comp; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite dec_eq_false; auto. + destruct c; simpl in H2; inv H2; auto. +Qed. + + +Theorem eval_compu: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). +Proof. + intros until y. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. +Qed. + +Theorem eval_compf: + forall le c a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)). +Proof. + intros. unfold compf. EvalOp. simpl. + destruct (Float.cmp c x y); reflexivity. +Qed. + +Theorem eval_negint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (negint a) (Vint (Int.neg x)). +Proof. intros; unfold negint; EvalOp. Qed. + +Theorem eval_negf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)). +Proof. intros; unfold negf; EvalOp. Qed. + +Theorem eval_absf: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). +Proof. intros; unfold absf; EvalOp. Qed. + +Theorem eval_intoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intoffloat a) (Vint (Float.intoffloat x)). +Proof. intros; unfold intoffloat; EvalOp. Qed. + +Theorem eval_intuoffloat: + forall le a x, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le (intuoffloat a) (Vint (Float.intuoffloat x)). +Proof. intros; unfold intuoffloat; EvalOp. Qed. + +Theorem eval_floatofint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). +Proof. intros; unfold floatofint; EvalOp. Qed. + +Theorem eval_floatofintu: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). +Proof. intros; unfold floatofintu; EvalOp. Qed. + +Theorem eval_addf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). +Proof. intros; unfold addf; EvalOp. Qed. + +Theorem eval_subf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). +Proof. intros; unfold subf; EvalOp. Qed. + +Theorem eval_mulf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)). +Proof. intros; unfold mulf; EvalOp. Qed. + +Theorem eval_divf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). +Proof. intros; unfold divf; EvalOp. Qed. + +Lemma eval_addressing: + forall le chunk a v b ofs, + eval_expr ge sp e m le a v -> + v = Vptr b ofs -> + match addressing chunk a with (mode, args) => + exists vl, + eval_exprlist ge sp e m le args vl /\ + eval_addressing ge sp mode vl = Some v + end. +Proof. + intros until v. unfold addressing; case (addressing_match a); intros; InvEval. + exists (@nil val). split. eauto with evalexpr. simpl. auto. + exists (Vptr b0 i :: nil). split. eauto with evalexpr. + simpl. congruence. + destruct (is_float_addressing chunk). + exists (Vptr b0 ofs :: nil). + split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. + simpl. rewrite Int.add_zero. congruence. + exists (Vptr b0 i :: Vint i0 :: nil). + split. eauto with evalexpr. simpl. congruence. + destruct (is_float_addressing chunk). + exists (Vptr b0 ofs :: nil). + split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. + simpl. rewrite Int.add_zero. congruence. + exists (Vint i :: Vptr b0 i0 :: nil). + split. eauto with evalexpr. simpl. + rewrite Int.add_commut. congruence. + destruct (is_float_addressing chunk). + exists (Vptr b0 ofs :: nil). + split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. + simpl. rewrite Int.add_zero. congruence. + exists (Vptr b0 i :: Vint i0 :: nil). + split. eauto with evalexpr. simpl. congruence. + exists (v :: nil). split. eauto with evalexpr. + subst v. simpl. rewrite Int.add_zero. auto. +Qed. + +End CMCONSTR. diff --git a/arm/Selection.v b/arm/Selection.v deleted file mode 100644 index 12cc1b27..00000000 --- a/arm/Selection.v +++ /dev/null @@ -1,1394 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Instruction selection *) - -(** The instruction selection pass recognizes opportunities for using - combined arithmetic and logical operations and addressing modes - offered by the target processor. For instance, the expression [x + 1] - can take advantage of the "immediate add" instruction of the processor, - and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned - into a "rotate and mask" instruction. - - Instruction selection proceeds by bottom-up rewriting over expressions. - The source language is Cminor and the target language is CminorSel. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Mem. -Require Import Globalenvs. -Require Cminor. -Require Import Op. -Require Import CminorSel. - -Infix ":::" := Econs (at level 60, right associativity) : selection_scope. - -Open Local Scope selection_scope. - -(** * Lifting of let-bound variables *) - -(** Some of the instruction functions generate [Elet] constructs to - share the evaluation of a subexpression. Owing to the use of de - Bruijn indices for let-bound variables, we need to shift de Bruijn - indices when an expression [b] is put in a [Elet a b] context. *) - -Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := - match a with - | 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) - | 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 - | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) - end. - -Definition lift (a: expr): expr := lift_expr O a. - -(** * Smart constructors for operators *) - -(** This section defines functions for building CminorSel expressions - and statements, especially expressions consisting of operator - applications. These functions examine their arguments to choose - cheaper forms of operators whenever possible. - - For instance, [add e1 e2] will return a CminorSel expression semantically - equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a - [Oaddimm] operator if one of the arguments is an integer constant, - or suppress the addition altogether if one of the arguments is the - null integer. In passing, we perform operator reassociation - ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount - of constant propagation. -*) - -(** ** Integer logical negation *) - -(** The natural way to write smart constructors is by pattern-matching - on their arguments, recognizing cases where cheaper operators - or combined operators are applicable. For instance, integer logical - negation has three special cases (not-and, not-or and not-xor), - along with a default case that uses not-or over its arguments and itself. - This is written naively as follows: -<< -Definition notint (e: expr) := - match e with - | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) - | Eop Onot (t1:::Enil) => t1 - | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) - | _ => Eop Onot (e:::Enil) - end. ->> - However, Coq expands complex pattern-matchings like the above into - elementary matchings over all constructors of an inductive type, - resulting in much duplication of the final catch-all case. - Such duplications generate huge executable code and duplicate - cases in the correctness proofs. - - To limit this duplication, we use the following trick due to - Yves Bertot. We first define a dependent inductive type that - characterizes the expressions that match each of the 4 cases of interest. -*) - -Inductive notint_cases: forall (e: expr), Type := - | notint_case1: - forall s t1, - notint_cases (Eop (Oshift s) (t1:::Enil)) - | notint_case2: - forall t1, - notint_cases (Eop Onot (t1:::Enil)) - | notint_case3: - forall s t1, - notint_cases (Eop (Onotshift s) (t1:::Enil)) - | notint_default: - forall (e: expr), - notint_cases e. - -(** We then define a classification function that takes an expression - and return the case in which it falls. Note that the catch-all case - [notint_default] does not state that it is mutually exclusive with - the first three, more specific cases. The classification function - nonetheless chooses the specific cases in preference to the catch-all - case. *) - -Definition notint_match (e: expr) := - match e as z1 return notint_cases z1 with - | Eop (Oshift s) (t1:::Enil) => - notint_case1 s t1 - | Eop Onot (t1:::Enil) => - notint_case2 t1 - | Eop (Onotshift s) (t1:::Enil) => - notint_case3 s t1 - | e => - notint_default e - end. - -(** Finally, the [notint] function we need is defined by a 4-case match - over the result of the classification function. Thus, no duplication - of the right-hand sides of this match occur, and the proof has only - 4 cases to consider (it proceeds by case over [notint_match e]). - Since the default case is not obviously exclusive with the three - specific cases, it is important that its right-hand side is - semantically correct for all possible values of [e], which is the - case here and for all other smart constructors. *) - -Definition notint (e: expr) := - match notint_match e with - | notint_case1 s t1 => - Eop (Onotshift s) (t1:::Enil) - | notint_case2 t1 => - t1 - | notint_case3 s t1 => - Eop (Oshift s) (t1:::Enil) - | notint_default e => - Eop Onot (e:::Enil) - end. - -(** This programming pattern will be applied systematically for the - other smart constructors in this file. *) - -(** ** Boolean negation *) - -Definition notbool_base (e: expr) := - Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil). - -Fixpoint notbool (e: expr) {struct e} : expr := - match e with - | Eop (Ointconst n) Enil => - Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil - | Eop (Ocmp cond) args => - Eop (Ocmp (negate_condition cond)) args - | Econdition e1 e2 e3 => - Econdition e1 (notbool e2) (notbool e3) - | _ => - notbool_base e - end. - -(** ** Integer addition and pointer addition *) - -(** Addition of an integer constant. *) - -(* -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match e with - | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil - | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | _ => Eop (Oaddimm n) (e ::: Enil) - end. -*) - -Inductive addimm_cases: forall (e: expr), Type := - | addimm_case1: - forall m, - addimm_cases (Eop (Ointconst m) Enil) - | addimm_case2: - forall s m, - addimm_cases (Eop (Oaddrsymbol s m) Enil) - | addimm_case3: - forall m, - addimm_cases (Eop (Oaddrstack m) Enil) - | addimm_case4: - forall m t, - addimm_cases (Eop (Oaddimm m) (t ::: Enil)) - | addimm_default: - forall (e: expr), - addimm_cases e. - -Definition addimm_match (e: expr) := - match e as z1 return addimm_cases z1 with - | Eop (Ointconst m) Enil => - addimm_case1 m - | Eop (Oaddrsymbol s m) Enil => - addimm_case2 s m - | Eop (Oaddrstack m) Enil => - addimm_case3 m - | Eop (Oaddimm m) (t ::: Enil) => - addimm_case4 m t - | e => - addimm_default e - end. - -Definition addimm (n: int) (e: expr) := - if Int.eq n Int.zero then e else - match addimm_match e with - | addimm_case1 m => - Eop (Ointconst(Int.add n m)) Enil - | addimm_case2 s m => - Eop (Oaddrsymbol s (Int.add n m)) Enil - | addimm_case3 m => - Eop (Oaddrstack (Int.add n m)) Enil - | addimm_case4 m t => - Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | addimm_default e => - Eop (Oaddimm n) (e ::: Enil) - end. - -(** Addition of two integer or pointer expressions. *) - -(* -Definition add (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | Eop(Oaddimm n1) (t1:::Enil)), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 - | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) - | _, _ => Eop Oadd (e1:::e2:::Enil) - end. -*) - -Inductive add_cases: forall (e1: expr) (e2: expr), Type := - | add_case1: - forall n1 t2, - add_cases (Eop (Ointconst n1) Enil) (t2) - | add_case2: - forall n1 t1 n2 t2, - add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case3: - forall n1 t1 t2, - add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | add_case4: - forall t1 n2, - add_cases (t1) (Eop (Ointconst n2) Enil) - | add_case5: - forall t1 n2 t2, - add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | add_case6: - forall s t1 t2, - add_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | add_case7: - forall t1 s t2, - add_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | add_default: - forall (e1: expr) (e2: expr), - add_cases e1 e2. - -Definition add_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return add_cases z1 z2 with - | Eop (Ointconst n1) Enil, t2 => - add_case1 n1 t2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - add_case2 n1 t1 n2 t2 - | Eop(Oaddimm n1) (t1:::Enil), t2 => - add_case3 n1 t1 t2 - | t1, Eop (Ointconst n2) Enil => - add_case4 t1 n2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => - add_case5 t1 n2 t2 - | Eop (Oshift s) (t1:::Enil), t2 => - add_case6 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - add_case7 t1 s t2 - | e1, e2 => - add_default e1 e2 - end. - -Definition add (e1: expr) (e2: expr) := - match add_match e1 e2 with - | add_case1 n1 t2 => - addimm n1 t2 - | add_case2 n1 t1 n2 t2 => - addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) - | add_case3 n1 t1 t2 => - addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | add_case4 t1 n2 => - addimm n2 t1 - | add_case5 t1 n2 t2 => - addimm n2 (Eop Oadd (t1:::t2:::Enil)) - | add_case6 s t1 t2 => - Eop (Oaddshift s) (t2:::t1:::Enil) - | add_case7 t1 s t2 => - Eop (Oaddshift s) (t1:::t2:::Enil) - | add_default e1 e2 => - Eop Oadd (e1:::e2:::Enil) - end. - -(** ** Integer and pointer subtraction *) - -(* -Definition sub (e1: expr) (e2: expr) := - match e1, e2 with - | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (intsub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Osub (t1:::t2:::Rnil)) - | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1::::t2:::Enil)) - | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) - | _, _ => Eop Osub (e1:::e2:::Enil) - end. -*) - -Inductive sub_cases: forall (e1: expr) (e2: expr), Type := - | sub_case1: - forall t1 n2, - sub_cases (t1) (Eop (Ointconst n2) Enil) - | sub_case2: - forall n1 t1 n2 t2, - sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case3: - forall n1 t1 t2, - sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2) - | sub_case4: - forall t1 n2 t2, - sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil)) - | sub_case5: - forall n1 t2, - sub_cases (Eop (Ointconst n1) Enil) (t2) - | sub_case6: - forall s t1 t2, - sub_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | sub_case7: - forall t1 s t2, - sub_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | sub_default: - forall (e1: expr) (e2: expr), - sub_cases e1 e2. - -Definition sub_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return sub_cases z1 z2 with - | t1, Eop (Ointconst n2) Enil => - sub_case1 t1 n2 - | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => - sub_case2 n1 t1 n2 t2 - | Eop (Oaddimm n1) (t1:::Enil), t2 => - sub_case3 n1 t1 t2 - | t1, Eop (Oaddimm n2) (t2:::Enil) => - sub_case4 t1 n2 t2 - | Eop (Ointconst n1) Enil, t2 => - sub_case5 n1 t2 - | Eop (Oshift s) (t1:::Enil), t2 => - sub_case6 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - sub_case7 t1 s t2 - | e1, e2 => - sub_default e1 e2 - end. - -Definition sub (e1: expr) (e2: expr) := - match sub_match e1 e2 with - | sub_case1 t1 n2 => - addimm (Int.neg n2) t1 - | sub_case2 n1 t1 n2 t2 => - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case3 n1 t1 t2 => - addimm n1 (Eop Osub (t1:::t2:::Enil)) - | sub_case4 t1 n2 t2 => - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) - | sub_case5 n1 t2 => - Eop (Orsubimm n1) (t2:::Enil) - | sub_case6 s t1 t2 => - Eop (Orsubshift s) (t2:::t1:::Enil) - | sub_case7 t1 s t2 => - Eop (Osubshift s) (t1:::t2:::Enil) - | sub_default e1 e2 => - Eop Osub (e1:::e2:::Enil) - end. - -(** ** Immediate shifts *) - -(* -Definition shlimm (e1: expr) := - if Int.eq n Int.zero then e1 else - match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) - | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil) - | _ => Eop (Oshift (Olsl n)) (e1:::Enil) - end. -*) - -Inductive shlimm_cases: forall (e1: expr), Type := - | shlimm_case1: - forall n1, - shlimm_cases (Eop (Ointconst n1) Enil) - | shlimm_case2: - forall n1 t1, - shlimm_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) - | shlimm_default: - forall (e1: expr), - shlimm_cases e1. - -Definition shlimm_match (e1: expr) := - match e1 as z1 return shlimm_cases z1 with - | Eop (Ointconst n1) Enil => - shlimm_case1 n1 - | Eop (Oshift (Slsl n1)) (t1:::Enil) => - shlimm_case2 n1 t1 - | e1 => - shlimm_default e1 - end. - -Definition shlimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - match is_shift_amount n with - | None => Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) - | Some n' => - match shlimm_match e1 with - | shlimm_case1 n1 => - Eop (Ointconst(Int.shl n1 n)) Enil - | shlimm_case2 n1 t1 => - match is_shift_amount (Int.add n (s_amount n1)) with - | None => - Eop (Oshift (Slsl n')) (e1:::Enil) - | Some n'' => - Eop (Oshift (Slsl n'')) (t1:::Enil) - end - | shlimm_default e1 => - Eop (Oshift (Slsl n')) (e1:::Enil) - end - end. - -(* -Definition shruimm (e1: expr) := - if Int.eq n Int.zero then e1 else - match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) - | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil) - | _ => Eop (Oshift (Olsr n)) (e1:::Enil) - end. -*) - -Inductive shruimm_cases: forall (e1: expr), Type := - | shruimm_case1: - forall n1, - shruimm_cases (Eop (Ointconst n1) Enil) - | shruimm_case2: - forall n1 t1, - shruimm_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) - | shruimm_default: - forall (e1: expr), - shruimm_cases e1. - -Definition shruimm_match (e1: expr) := - match e1 as z1 return shruimm_cases z1 with - | Eop (Ointconst n1) Enil => - shruimm_case1 n1 - | Eop (Oshift (Slsr n1)) (t1:::Enil) => - shruimm_case2 n1 t1 - | e1 => - shruimm_default e1 - end. - -Definition shruimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - match is_shift_amount n with - | None => Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) - | Some n' => - match shruimm_match e1 with - | shruimm_case1 n1 => - Eop (Ointconst(Int.shru n1 n)) Enil - | shruimm_case2 n1 t1 => - match is_shift_amount (Int.add n (s_amount n1)) with - | None => - Eop (Oshift (Slsr n')) (e1:::Enil) - | Some n'' => - Eop (Oshift (Slsr n'')) (t1:::Enil) - end - | shruimm_default e1 => - Eop (Oshift (Slsr n')) (e1:::Enil) - end - end. - -(* -Definition shrimm (e1: expr) := - match e1 with - | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) - | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil) - | _ => Eop (Oshift (Oasr n)) (e1:::Enil) - end. -*) - -Inductive shrimm_cases: forall (e1: expr), Type := - | shrimm_case1: - forall n1, - shrimm_cases (Eop (Ointconst n1) Enil) - | shrimm_case2: - forall n1 t1, - shrimm_cases (Eop (Oshift (Sasr n1)) (t1:::Enil)) - | shrimm_default: - forall (e1: expr), - shrimm_cases e1. - -Definition shrimm_match (e1: expr) := - match e1 as z1 return shrimm_cases z1 with - | Eop (Ointconst n1) Enil => - shrimm_case1 n1 - | Eop (Oshift (Sasr n1)) (t1:::Enil) => - shrimm_case2 n1 t1 - | e1 => - shrimm_default e1 - end. - -Definition shrimm (e1: expr) (n: int) := - if Int.eq n Int.zero then e1 else - match is_shift_amount n with - | None => Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) - | Some n' => - match shrimm_match e1 with - | shrimm_case1 n1 => - Eop (Ointconst(Int.shr n1 n)) Enil - | shrimm_case2 n1 t1 => - match is_shift_amount (Int.add n (s_amount n1)) with - | None => - Eop (Oshift (Sasr n')) (e1:::Enil) - | Some n'' => - Eop (Oshift (Sasr n'')) (t1:::Enil) - end - | shrimm_default e1 => - Eop (Oshift (Sasr n')) (e1:::Enil) - end - end. - -(** ** Integer multiply *) - -Definition mulimm_base (n1: int) (e2: expr) := - match Int.one_bits n1 with - | i :: nil => - shlimm e2 i - | i :: j :: nil => - Elet e2 - (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j)) - | _ => - Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil) - end. - -(* -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then - Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then - e2 - else match e2 with - | Eop (Ointconst n2) Enil => Eop (Ointconst(intmul n1 n2)) Enil - | Eop (Oaddimm n2) (t2:::Enil) => addimm (intmul n1 n2) (mulimm_base n1 t2) - | _ => mulimm_base n1 e2 - end. -*) - -Inductive mulimm_cases: forall (e2: expr), Type := - | mulimm_case1: - forall (n2: int), - mulimm_cases (Eop (Ointconst n2) Enil) - | mulimm_case2: - forall (n2: int) (t2: expr), - mulimm_cases (Eop (Oaddimm n2) (t2:::Enil)) - | mulimm_default: - forall (e2: expr), - mulimm_cases e2. - -Definition mulimm_match (e2: expr) := - match e2 as z1 return mulimm_cases z1 with - | Eop (Ointconst n2) Enil => - mulimm_case1 n2 - | Eop (Oaddimm n2) (t2:::Enil) => - mulimm_case2 n2 t2 - | e2 => - mulimm_default e2 - end. - -Definition mulimm (n1: int) (e2: expr) := - if Int.eq n1 Int.zero then - Eop (Ointconst Int.zero) Enil - else if Int.eq n1 Int.one then - e2 - else match mulimm_match e2 with - | mulimm_case1 n2 => - Eop (Ointconst(Int.mul n1 n2)) Enil - | mulimm_case2 n2 t2 => - addimm (Int.mul n1 n2) (mulimm_base n1 t2) - | mulimm_default e2 => - mulimm_base n1 e2 - end. - -(* -Definition mul (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2 - | t1, Eop (Ointconst n2) Enil => mulimm n2 t1 - | _, _ => Eop Omul (e1:::e2:::Enil) - end. -*) - -Inductive mul_cases: forall (e1: expr) (e2: expr), Type := - | mul_case1: - forall (n1: int) (t2: expr), - mul_cases (Eop (Ointconst n1) Enil) (t2) - | mul_case2: - forall (t1: expr) (n2: int), - mul_cases (t1) (Eop (Ointconst n2) Enil) - | mul_default: - forall (e1: expr) (e2: expr), - mul_cases e1 e2. - -Definition mul_match_aux (e1: expr) (e2: expr) := - match e2 as z2 return mul_cases e1 z2 with - | Eop (Ointconst n2) Enil => - mul_case2 e1 n2 - | e2 => - mul_default e1 e2 - end. - -Definition mul_match (e1: expr) (e2: expr) := - match e1 as z1 return mul_cases z1 e2 with - | Eop (Ointconst n1) Enil => - mul_case1 n1 e2 - | e1 => - mul_match_aux e1 e2 - end. - -Definition mul (e1: expr) (e2: expr) := - match mul_match e1 e2 with - | mul_case1 n1 t2 => - mulimm n1 t2 - | mul_case2 t1 n2 => - mulimm n2 t1 - | mul_default e1 e2 => - Eop Omul (e1:::e2:::Enil) - end. - -(** ** Integer division and modulus *) - -Definition mod_aux (divop: operation) (e1 e2: expr) := - Elet e1 - (Elet (lift e2) - (Eop Osub (Eletvar 1 ::: - Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: - Eletvar 0 ::: - Enil) ::: - Enil))). - -Inductive divu_cases: forall (e2: expr), Type := - | divu_case1: - forall (n2: int), - divu_cases (Eop (Ointconst n2) Enil) - | divu_default: - forall (e2: expr), - divu_cases e2. - -Definition divu_match (e2: expr) := - match e2 as z1 return divu_cases z1 with - | Eop (Ointconst n2) Enil => - divu_case1 n2 - | e2 => - divu_default e2 - end. - -Definition divu (e1: expr) (e2: expr) := - match divu_match e2 with - | divu_case1 n2 => - match Int.is_power2 n2 with - | Some l2 => shruimm e1 l2 - | None => Eop Odivu (e1:::e2:::Enil) - end - | divu_default e2 => - Eop Odivu (e1:::e2:::Enil) - end. - -Definition modu (e1: expr) (e2: expr) := - match divu_match e2 with - | divu_case1 n2 => - match Int.is_power2 n2 with - | Some l2 => Eop (Oandimm (Int.sub n2 Int.one)) (e1:::Enil) - | None => mod_aux Odivu e1 e2 - end - | divu_default e2 => - mod_aux Odivu e1 e2 - end. - -Definition divs (e1: expr) (e2: expr) := - match divu_match e2 with - | divu_case1 n2 => - match Int.is_power2 n2 with - | Some l2 => if Int.ltu l2 (Int.repr 31) - then Eop (Oshrximm l2) (e1:::Enil) - else Eop Odiv (e1:::e2:::Enil) - | None => Eop Odiv (e1:::e2:::Enil) - end - | divu_default e2 => - Eop Odiv (e1:::e2:::Enil) - end. - -Definition mods := mod_aux Odiv. (* could be improved *) - - -(** ** Bitwise and, or, xor *) - -(* -Definition and (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) - | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) - | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) - | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) - | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) - | _, _ => Eop Oand (e1:::e2:::Enil) - end. -*) - -Inductive and_cases: forall (e1: expr) (e2: expr), Type := - | and_case1: - forall s t1 t2, - and_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | and_case2: - forall t1 s t2, - and_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | and_case3: - forall s t1 t2, - and_cases (Eop (Onotshift s) (t1:::Enil)) (t2) - | and_case4: - forall t1 s t2, - and_cases (t1) (Eop (Onotshift s) (t2:::Enil)) - | and_case5: - forall t1 t2, - and_cases (Eop Onot (t1:::Enil)) (t2) - | and_case6: - forall t1 t2, - and_cases (t1) (Eop Onot (t2:::Enil)) - | and_default: - forall (e1: expr) (e2: expr), - and_cases e1 e2. - -Definition and_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return and_cases z1 z2 with - | Eop (Oshift s) (t1:::Enil), t2 => - and_case1 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - and_case2 t1 s t2 - | Eop (Onotshift s) (t1:::Enil), t2 => - and_case3 s t1 t2 - | t1, Eop (Onotshift s) (t2:::Enil) => - and_case4 t1 s t2 - | Eop Onot (t1:::Enil), t2 => - and_case5 t1 t2 - | t1, Eop Onot (t2:::Enil) => - and_case6 t1 t2 - | e1, e2 => - and_default e1 e2 - end. - -Definition and (e1: expr) (e2: expr) := - match and_match e1 e2 with - | and_case1 s t1 t2 => - Eop (Oandshift s) (t2:::t1:::Enil) - | and_case2 t1 s t2 => - Eop (Oandshift s) (t1:::t2:::Enil) - | and_case3 s t1 t2 => - Eop (Obicshift s) (t2:::t1:::Enil) - | and_case4 t1 s t2 => - Eop (Obicshift s) (t1:::t2:::Enil) - | and_case5 t1 t2 => - Eop Obic (t2:::t1:::Enil) - | and_case6 t1 t2 => - Eop Obic (t1:::t2:::Enil) - | and_default e1 e2 => - Eop Oand (e1:::e2:::Enil) - end. - -Definition same_expr_pure (e1 e2: expr) := - match e1, e2 with - | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false - | _, _ => false - end. - -(* -Definition or (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Oshift (Olsl n1) (t1:::Enil), Eop (Oshift (Olsr n2) (t2:::Enil)) => ... - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil) - | _, _ => Eop Oor (e1:::e2:::Enil) - end. -*) - -(* TODO: symmetric of first case *) - -Inductive or_cases: forall (e1: expr) (e2: expr), Type := - | or_case1: - forall n1 t1 n2 t2, - or_cases (Eop (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil)) - | or_case2: - forall s t1 t2, - or_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | or_case3: - forall t1 s t2, - or_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | or_default: - forall (e1: expr) (e2: expr), - or_cases e1 e2. - -Definition or_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return or_cases z1 z2 with - | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => - or_case1 n1 t1 n2 t2 - | Eop (Oshift s) (t1:::Enil), t2 => - or_case2 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - or_case3 t1 s t2 - | e1, e2 => - or_default e1 e2 - end. - -Definition or (e1: expr) (e2: expr) := - match or_match e1 e2 with - | or_case1 n1 t1 n2 t2 => - if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) - && same_expr_pure t1 t2 - then Eop (Oshift (Sror n2)) (t1:::Enil) - else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) - | or_case2 s t1 t2 => - Eop (Oorshift s) (t2:::t1:::Enil) - | or_case3 t1 s t2 => - Eop (Oorshift s) (t1:::t2:::Enil) - | or_default e1 e2 => - Eop Oor (e1:::e2:::Enil) - end. - -(* -Definition xor (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) - | _, _ => Eop Oxor (e1:::e2:::Enil) - end. -*) - -Inductive xor_cases: forall (e1: expr) (e2: expr), Type := - | xor_case1: - forall s t1 t2, - xor_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | xor_case2: - forall t1 s t2, - xor_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | xor_default: - forall (e1: expr) (e2: expr), - xor_cases e1 e2. - -Definition xor_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return xor_cases z1 z2 with - | Eop (Oshift s) (t1:::Enil), t2 => - xor_case1 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - xor_case2 t1 s t2 - | e1, e2 => - xor_default e1 e2 - end. - -Definition xor (e1: expr) (e2: expr) := - match xor_match e1 e2 with - | xor_case1 s t1 t2 => - Eop (Oxorshift s) (t2:::t1:::Enil) - | xor_case2 t1 s t2 => - Eop (Oxorshift s) (t1:::t2:::Enil) - | xor_default e1 e2 => - Eop Oxor (e1:::e2:::Enil) - end. - -(** ** General shifts *) - -Inductive shift_cases: forall (e1: expr), Type := - | shift_case1: - forall (n2: int), - shift_cases (Eop (Ointconst n2) Enil) - | shift_default: - forall (e1: expr), - shift_cases e1. - -Definition shift_match (e1: expr) := - match e1 as z1 return shift_cases z1 with - | Eop (Ointconst n2) Enil => - shift_case1 n2 - | e1 => - shift_default e1 - end. - -Definition shl (e1: expr) (e2: expr) := - match shift_match e2 with - | shift_case1 n2 => - shlimm e1 n2 - | shift_default e2 => - Eop Oshl (e1:::e2:::Enil) - end. - -Definition shru (e1: expr) (e2: expr) := - match shift_match e2 with - | shift_case1 n2 => - shruimm e1 n2 - | shift_default e2 => - Eop Oshru (e1:::e2:::Enil) - end. - -Definition shr (e1: expr) (e2: expr) := - match shift_match e2 with - | shift_case1 n2 => - shrimm e1 n2 - | shift_default e2 => - Eop Oshr (e1:::e2:::Enil) - end. - -(** ** Truncations and sign extensions *) - -Inductive cast8signed_cases: forall (e1: expr), Type := - | cast8signed_case1: - forall (e2: expr), - cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) - | cast8signed_default: - forall (e1: expr), - cast8signed_cases e1. - -Definition cast8signed_match (e1: expr) := - match e1 as z1 return cast8signed_cases z1 with - | Eop Ocast8signed (e2 ::: Enil) => - cast8signed_case1 e2 - | e1 => - cast8signed_default e1 - end. - -Definition cast8signed (e: expr) := - match cast8signed_match e with - | cast8signed_case1 e1 => e - | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) - end. - -Inductive cast8unsigned_cases: forall (e1: expr), Type := - | cast8unsigned_case1: - forall (e2: expr), - cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) - | cast8unsigned_default: - forall (e1: expr), - cast8unsigned_cases e1. - -Definition cast8unsigned_match (e1: expr) := - match e1 as z1 return cast8unsigned_cases z1 with - | Eop Ocast8unsigned (e2 ::: Enil) => - cast8unsigned_case1 e2 - | e1 => - cast8unsigned_default e1 - end. - -Definition cast8unsigned (e: expr) := - match cast8unsigned_match e with - | cast8unsigned_case1 e1 => e - | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) - end. - -Inductive cast16signed_cases: forall (e1: expr), Type := - | cast16signed_case1: - forall (e2: expr), - cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) - | cast16signed_default: - forall (e1: expr), - cast16signed_cases e1. - -Definition cast16signed_match (e1: expr) := - match e1 as z1 return cast16signed_cases z1 with - | Eop Ocast16signed (e2 ::: Enil) => - cast16signed_case1 e2 - | e1 => - cast16signed_default e1 - end. - -Definition cast16signed (e: expr) := - match cast16signed_match e with - | cast16signed_case1 e1 => e - | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) - end. - -Inductive cast16unsigned_cases: forall (e1: expr), Type := - | cast16unsigned_case1: - forall (e2: expr), - cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) - | cast16unsigned_default: - forall (e1: expr), - cast16unsigned_cases e1. - -Definition cast16unsigned_match (e1: expr) := - match e1 as z1 return cast16unsigned_cases z1 with - | Eop Ocast16unsigned (e2 ::: Enil) => - cast16unsigned_case1 e2 - | e1 => - cast16unsigned_default e1 - end. - -Definition cast16unsigned (e: expr) := - match cast16unsigned_match e with - | cast16unsigned_case1 e1 => e - | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) - end. - -Inductive singleoffloat_cases: forall (e1: expr), Type := - | singleoffloat_case1: - forall (e2: expr), - singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) - | singleoffloat_default: - forall (e1: expr), - singleoffloat_cases e1. - -Definition singleoffloat_match (e1: expr) := - match e1 as z1 return singleoffloat_cases z1 with - | Eop Osingleoffloat (e2 ::: Enil) => - singleoffloat_case1 e2 - | e1 => - singleoffloat_default e1 - end. - -Definition singleoffloat (e: expr) := - match singleoffloat_match e with - | singleoffloat_case1 e1 => e - | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) - end. - -(** ** Comparisons *) - -(* -Definition comp (e1: expr) (e2: expr) := - match e1, e2 with - | Eop (Ointconst n1) Enil, t2 => Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) - | t1, Eop (Ointconst n2) Enil => Eop (Ocmp (Ccompimm c n1)) (t1:::Enil) - | Eop (Oshift s) (t1:::Enil), t2 => Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) - | t1, Eop (Oshift s) (t2:::Enil) => Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) - | _, _ => Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) - end. -*) - -Inductive comp_cases: forall (e1: expr) (e2: expr), Type := - | comp_case1: - forall n1 t2, - comp_cases (Eop (Ointconst n1) Enil) (t2) - | comp_case2: - forall t1 n2, - comp_cases (t1) (Eop (Ointconst n2) Enil) - | comp_case3: - forall s t1 t2, - comp_cases (Eop (Oshift s) (t1:::Enil)) (t2) - | comp_case4: - forall t1 s t2, - comp_cases (t1) (Eop (Oshift s) (t2:::Enil)) - | comp_default: - forall (e1: expr) (e2: expr), - comp_cases e1 e2. - -Definition comp_match (e1: expr) (e2: expr) := - match e1 as z1, e2 as z2 return comp_cases z1 z2 with - | Eop (Ointconst n1) Enil, t2 => - comp_case1 n1 t2 - | t1, Eop (Ointconst n2) Enil => - comp_case2 t1 n2 - | Eop (Oshift s) (t1:::Enil), t2 => - comp_case3 s t1 t2 - | t1, Eop (Oshift s) (t2:::Enil) => - comp_case4 t1 s t2 - | e1, e2 => - comp_default e1 e2 - end. - -Definition comp (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => - Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) - | comp_case2 t1 n2 => - Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) - | comp_case3 s t1 t2 => - Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) - | comp_case4 t1 s t2 => - Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) - | comp_default e1 e2 => - Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil) - end. - -Definition compu (c: comparison) (e1: expr) (e2: expr) := - match comp_match e1 e2 with - | comp_case1 n1 t2 => - Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) - | comp_case2 t1 n2 => - Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) - | comp_case3 s t1 t2 => - Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) - | comp_case4 t1 s t2 => - Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) - | comp_default e1 e2 => - Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) - end. - -Definition compf (c: comparison) (e1: expr) (e2: expr) := - Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). - -(** ** Conditional expressions *) - -Fixpoint negate_condexpr (e: condexpr): condexpr := - 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. - -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) - | _ => - CEcond (Ccompimm Cne Int.zero) (e:::Enil) - end. - -(** ** Recognition of addressing modes for load and store operations *) - -(* -Definition addressing (e: expr) := - match e with - | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) - | Eop (Oaddshift s) (e1:::e2:::Enil) => (Aindexed2shift s, e1:::e2:::Enil) - | Eop Oadd (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) - | _ => (Aindexed Int.zero, e:::Enil) - end. -*) - -Inductive addressing_cases: forall (e: expr), Type := - | addressing_case2: - forall n, - addressing_cases (Eop (Oaddrstack n) Enil) - | addressing_case3: - forall n e1, - addressing_cases (Eop (Oaddimm n) (e1:::Enil)) - | addressing_case4: - forall s e1 e2, - addressing_cases (Eop (Oaddshift s) (e1:::e2:::Enil)) - | addressing_case5: - forall e1 e2, - addressing_cases (Eop Oadd (e1:::e2:::Enil)) - | addressing_default: - forall (e: expr), - addressing_cases e. - -Definition addressing_match (e: expr) := - match e as z1 return addressing_cases z1 with - | Eop (Oaddrstack n) Enil => - addressing_case2 n - | Eop (Oaddimm n) (e1:::Enil) => - addressing_case3 n e1 - | Eop (Oaddshift s) (e1:::e2:::Enil) => - addressing_case4 s e1 e2 - | Eop Oadd (e1:::e2:::Enil) => - addressing_case5 e1 e2 - | e => - addressing_default e - end. - -(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes - for floating-point accesses, since these are not supported - by the hardware and emulated inefficiently in [ARMgen]. *) - -Definition is_float_addressing (chunk: memory_chunk): bool := - match chunk with - | Mfloat32 => true - | Mfloat64 => true - | _ => false - end. - -Definition addressing (chunk: memory_chunk) (e: expr) := - match addressing_match e with - | addressing_case2 n => - (Ainstack n, Enil) - | addressing_case3 n e1 => - (Aindexed n, e1:::Enil) - | addressing_case4 s e1 e2 => - if is_float_addressing chunk - then (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) - else (Aindexed2shift s, e1:::e2:::Enil) - | addressing_case5 e1 e2 => - if is_float_addressing chunk - then (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) - else (Aindexed2, e1:::e2:::Enil) - | addressing_default e => - (Aindexed Int.zero, e:::Enil) - end. - -Definition load (chunk: memory_chunk) (e1: expr) := - match addressing chunk e1 with - | (mode, args) => Eload chunk mode args - end. - -Definition store (chunk: memory_chunk) (e1 e2: expr) := - match addressing chunk e1 with - | (mode, args) => Sstore chunk mode args e2 - end. - -(** * Translation from Cminor to CminorSel *) - -(** Instruction selection for operator applications *) - -Definition sel_constant (cst: Cminor.constant) : expr := - match cst with - | Cminor.Ointconst n => Eop (Ointconst n) Enil - | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil - | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil - | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil - end. - -Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr := - match op with - | Cminor.Ocast8unsigned => cast8unsigned arg - | Cminor.Ocast8signed => cast8signed arg - | Cminor.Ocast16unsigned => cast16unsigned arg - | Cminor.Ocast16signed => cast16signed arg - | Cminor.Onegint => Eop (Orsubimm Int.zero) (arg ::: Enil) - | Cminor.Onotbool => notbool arg - | Cminor.Onotint => notint arg - | Cminor.Onegf => Eop Onegf (arg ::: Enil) - | Cminor.Oabsf => Eop Oabsf (arg ::: Enil) - | Cminor.Osingleoffloat => singleoffloat arg - | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil) - | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil) - | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil) - | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil) - end. - -Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := - match op with - | Cminor.Oadd => add arg1 arg2 - | Cminor.Osub => sub arg1 arg2 - | Cminor.Omul => mul arg1 arg2 - | Cminor.Odiv => divs arg1 arg2 - | Cminor.Odivu => divu arg1 arg2 - | Cminor.Omod => mods arg1 arg2 - | Cminor.Omodu => modu arg1 arg2 - | Cminor.Oand => and arg1 arg2 - | Cminor.Oor => or arg1 arg2 - | Cminor.Oxor => xor arg1 arg2 - | Cminor.Oshl => shl arg1 arg2 - | Cminor.Oshr => shr arg1 arg2 - | Cminor.Oshru => shru arg1 arg2 - | Cminor.Oaddf => Eop Oaddf (arg1 ::: arg2 ::: Enil) - | Cminor.Osubf => Eop Osubf (arg1 ::: arg2 ::: Enil) - | Cminor.Omulf => Eop Omulf (arg1 ::: arg2 ::: Enil) - | Cminor.Odivf => Eop Odivf (arg1 ::: arg2 ::: Enil) - | Cminor.Ocmp c => comp c arg1 arg2 - | Cminor.Ocmpu c => compu c arg1 arg2 - | Cminor.Ocmpf c => compf c arg1 arg2 - end. - -(** Conversion from Cminor expression to Cminorsel expressions *) - -Fixpoint sel_expr (a: Cminor.expr) : expr := - match a with - | Cminor.Evar id => Evar id - | Cminor.Econst cst => sel_constant cst - | 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 := - match al with - | nil => Enil - | a :: bl => Econs (sel_expr a) (sel_exprlist bl) - end. - -(** Conversion from Cminor statements to Cminorsel statements. *) - -Fixpoint sel_stmt (s: Cminor.stmt) : 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.Scall optid sg fn args => - Scall optid sg (sel_expr fn) (sel_exprlist args) - | Cminor.Stailcall sg fn args => - Stailcall sg (sel_expr fn) (sel_exprlist args) - | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2) - | Cminor.Sifthenelse e ifso ifnot => - Sifthenelse (condexpr_of_expr (sel_expr e)) - (sel_stmt ifso) (sel_stmt ifnot) - | Cminor.Sloop body => Sloop (sel_stmt body) - | Cminor.Sblock body => Sblock (sel_stmt 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 body) - | Cminor.Sgoto lbl => Sgoto lbl - end. - -(** Conversion of functions and programs. *) - -Definition sel_function (f: Cminor.function) : function := - mkfunction - f.(Cminor.fn_sig) - f.(Cminor.fn_params) - f.(Cminor.fn_vars) - f.(Cminor.fn_stackspace) - (sel_stmt f.(Cminor.fn_body)). - -Definition sel_fundef (f: Cminor.fundef) : fundef := - transf_fundef sel_function f. - -Definition sel_program (p: Cminor.program) : program := - transform_program sel_fundef p. - -(** For compatibility with PowerPC *) - -Parameter use_fused_mul: unit -> bool. diff --git a/arm/Selectionproof.v b/arm/Selectionproof.v deleted file mode 100644 index cf7613b6..00000000 --- a/arm/Selectionproof.v +++ /dev/null @@ -1,1459 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness of instruction selection *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Mem. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import Selection. - -Open Local Scope selection_scope. - -Section CMCONSTR. - -Variable ge: genv. -Variable sp: val. -Variable e: env. -Variable m: mem. - -(** * Lifting of let-bound variables *) - -Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop := - | insert_lenv_0: - forall le v, - insert_lenv le O v (v :: le) - | insert_lenv_S: - forall le p w le' v, - insert_lenv le p w le' -> - insert_lenv (v :: le) (S p) w (v :: le'). - -Lemma insert_lenv_lookup1: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p > n)%nat -> - nth_error le' n = Some v. -Proof. - induction 1; intros. - omegaContradiction. - destruct n; simpl; simpl in H0. auto. - apply IHinsert_lenv. auto. omega. -Qed. - -Lemma insert_lenv_lookup2: - forall le p w le', - insert_lenv le p w le' -> - forall n v, - nth_error le n = Some v -> (p <= n)%nat -> - nth_error le' (S n) = Some v. -Proof. - induction 1; intros. - simpl. assumption. - simpl. destruct n. omegaContradiction. - apply IHinsert_lenv. exact H0. omega. -Qed. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition - eval_Elet eval_Eletvar - eval_CEtrue eval_CEfalse eval_CEcond - eval_CEcondition eval_Enil eval_Econs: evalexpr. - -Lemma eval_lift_expr: - forall w le a v, - eval_expr ge sp e m le a v -> - forall p le', insert_lenv le p w le' -> - eval_expr ge sp e m le' (lift_expr p a) v. -Proof. - intro w. - apply (eval_expr_ind3 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_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: - forall le a v w, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m (w::le) (lift a) v. -Proof. - intros. unfold lift. eapply eval_lift_expr. - eexact H. apply insert_lenv_0. -Qed. - -Hint Resolve eval_lift: evalexpr. - -(** * Useful lemmas and tactics *) - -(** The following are trivial lemmas and custom tactics that help - perform backward (inversion) and forward reasoning over the evaluation - of operator applications. *) - -Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. - -Ltac TrivialOp cstr := unfold cstr; intros; EvalOp. - -Ltac InvEval1 := - match goal with - | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] => - inv H; InvEval1 - | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] => - inv H; InvEval1 - | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] => - inv H; InvEval1 - | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] => - inv H; InvEval1 - | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] => - inv H; InvEval1 - | _ => - idtac - end. - -Ltac InvEval2 := - match goal with - | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] => - simpl in H; inv H - | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] => - simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] => - simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] => - simpl in H; FuncInv - | _ => - idtac - end. - -Ltac InvEval := InvEval1; InvEval2; InvEval2. - -(** * Correctness of the smart constructors *) - -(** We now show that the code generated by "smart constructor" functions - such as [Selection.notint] behaves as expected. Continuing the - [notint] example, we show that if the expression [e] - evaluates to some integer value [Vint n], then [Selection.notint e] - evaluates to a value [Vint (Int.not n)] which is indeed the integer - negation of the value of [e]. - - All proofs follow a common pattern: -- Reasoning by case over the result of the classification functions - (such as [add_match] for integer addition), gathering additional - information on the shape of the argument expressions in the non-default - cases. -- Inversion of the evaluations of the arguments, exploiting the additional - information thus gathered. -- Equational reasoning over the arithmetic operations performed, - using the lemmas from the [Int] and [Float] modules. -- Construction of an evaluation derivation for the expression returned - by the smart constructor. -*) - -Theorem eval_notint: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (notint a) (Vint (Int.not x)). -Proof. - unfold notint; intros until x; case (notint_match a); intros; InvEval. - EvalOp. simpl. congruence. - subst x. rewrite Int.not_involutive. auto. - EvalOp. simpl. subst x. rewrite Int.not_involutive. auto. - EvalOp. -Qed. - -Lemma eval_notbool_base: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)). -Proof. - TrivialOp notbool_base. simpl. - inv H0. - rewrite Int.eq_false; auto. - rewrite Int.eq_true; auto. - reflexivity. -Qed. - -Hint Resolve Val.bool_of_true_val Val.bool_of_false_val - Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. - -Theorem eval_notbool: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)). -Proof. - induction a; simpl; intros; try (eapply eval_notbool_base; eauto). - destruct o; try (eapply eval_notbool_base; eauto). - - destruct e0. InvEval. - inv H0. rewrite Int.eq_false; auto. - simpl; eauto with evalexpr. - rewrite Int.eq_true; simpl; eauto with evalexpr. - eapply eval_notbool_base; eauto. - - inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl = Some b). - generalize H6. simpl. - case (eval_condition c vl); intros. - destruct b0; inv H1; inversion H0; auto; congruence. - congruence. - rewrite (Op.eval_negate_condition _ _ H). - destruct b; reflexivity. - - inv H. eapply eval_Econdition; eauto. - destruct v1; eauto. -Qed. - -Theorem eval_addimm: - forall le n a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)). -Proof. - unfold addimm; intros until x. - generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. - subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros; InvEval; EvalOp; simpl. - rewrite Int.add_commut. auto. - destruct (Genv.find_symbol ge s); discriminate. - destruct sp; simpl in H1; discriminate. - subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. -Qed. - -Theorem eval_addimm_ptr: - forall le n a b ofs, - eval_expr ge sp e m le a (Vptr b ofs) -> - eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)). -Proof. - unfold addimm; intros until ofs. - generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. - subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros; InvEval; EvalOp; simpl. - destruct (Genv.find_symbol ge s). - rewrite Int.add_commut. congruence. - discriminate. - destruct sp; simpl in H1; try discriminate. - inv H1. simpl. decEq. decEq. - rewrite Int.add_assoc. decEq. apply Int.add_commut. - subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto. -Qed. - -Theorem eval_add: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (add a b) (Vint (Int.add x y)). -Proof. - intros until y. - unfold add; case (add_match a b); intros; InvEval. - rewrite Int.add_commut. apply eval_addimm. auto. - replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - apply eval_addimm. auto. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. simpl. subst x. rewrite Int.add_commut. auto. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_add_ptr: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)). -Proof. - intros until y. unfold add; case (add_match a b); intros; InvEval. - replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - apply eval_addimm_ptr. auto. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm_ptr. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_add_ptr_2: - forall le a b x p y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vptr p y) -> - eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)). -Proof. - intros until y. unfold add; case (add_match a b); intros; InvEval. - apply eval_addimm_ptr. auto. - replace (Int.add y x) with (Int.add (Int.add i i0) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. - rewrite (Int.add_commut n1 n2). apply Int.add_permut. - replace (Int.add y x) with (Int.add (Int.add y i) n1). - apply eval_addimm_ptr. EvalOp. - subst x. repeat rewrite Int.add_assoc. auto. - replace (Int.add y x) with (Int.add (Int.add i x) n2). - apply eval_addimm_ptr. EvalOp. subst b0; reflexivity. - subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_sub: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros; InvEval. - rewrite Int.sub_add_opp. - apply eval_addimm. assumption. - replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm. EvalOp. - subst x. rewrite Int.sub_add_l. auto. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm. EvalOp. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. - EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_sub_ptr_int: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros; InvEval. - rewrite Int.sub_add_opp. - apply eval_addimm_ptr. assumption. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm_ptr. EvalOp. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm_ptr. EvalOp. - subst x. rewrite Int.sub_add_l. auto. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm_ptr. EvalOp. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_sub_ptr_ptr: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vptr p y) -> - eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros; InvEval. - replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm. EvalOp. - simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm. EvalOp. - simpl. unfold eq_block. rewrite zeq_true. auto. - subst x. rewrite Int.sub_add_l. auto. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm. EvalOp. - simpl. unfold eq_block. rewrite zeq_true. auto. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. -Qed. - -Theorem eval_shlimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). -Proof. - intros until x. unfold shlimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shl_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shlimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shl_shl. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. -Qed. - -Theorem eval_shruimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). -Proof. - intros until x. unfold shruimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shru_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shruimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shru_shru. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. -Qed. - -Theorem eval_shrimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)). -Proof. - intros until x. unfold shrimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shr_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shrimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shr_shr. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. -Qed. - -Lemma eval_mulimm_base: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)). -Proof. - intros; unfold mulimm_base. - generalize (Int.one_bits_decomp n). - generalize (Int.one_bits_range n). - change (Z_of_nat wordsize) with 32. - destruct (Int.one_bits n). - intros. EvalOp. constructor. EvalOp. simpl; reflexivity. - constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. - destruct l. - intros. rewrite H1. simpl. - rewrite Int.add_zero. rewrite <- Int.shl_mul. - apply eval_shlimm. auto. auto with coqlib. - destruct l. - intros. apply eval_Elet with (Vint x). auto. - rewrite H1. simpl. rewrite Int.add_zero. - rewrite Int.mul_add_distr_r. - rewrite <- Int.shl_mul. - rewrite <- Int.shl_mul. - apply eval_add. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - intros. EvalOp. constructor. EvalOp. simpl; reflexivity. - constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. -Qed. - -Theorem eval_mulimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)). -Proof. - intros until x; unfold mulimm. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - subst n. rewrite Int.mul_zero. - intro. EvalOp. - generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. - subst n. rewrite Int.mul_one. auto. - case (mulimm_match a); intros; InvEval. - EvalOp. rewrite Int.mul_commut. reflexivity. - replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)). - apply eval_addimm. apply eval_mulimm_base. auto. - subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut. - apply eval_mulimm_base. assumption. -Qed. - -Theorem eval_mul: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)). -Proof. - intros until y. - unfold mul; case (mul_match a b); intros; InvEval. - rewrite Int.mul_commut. apply eval_mulimm. auto. - apply eval_mulimm. auto. - EvalOp. -Qed. - -Theorem eval_divs_base: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (Eop Odiv (a ::: b ::: Enil)) (Vint (Int.divs x y)). -Proof. - intros. EvalOp; simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. -Qed. - -Theorem eval_divs: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)). -Proof. - intros until y. - unfold divs; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y); intros. - caseEq (Int.ltu i (Int.repr 31)); intros. - EvalOp. simpl. unfold Int.ltu. rewrite zlt_true. - rewrite (Int.divs_pow2 x y i H0). auto. - exploit Int.ltu_inv; eauto. - change (Int.unsigned (Int.repr 31)) with 31. - change (Int.unsigned (Int.repr 32)) with 32. - omega. - apply eval_divs_base. auto. EvalOp. auto. - apply eval_divs_base. auto. EvalOp. auto. - apply eval_divs_base; auto. -Qed. - -Lemma eval_mod_aux: - forall divop semdivop, - (forall sp x y, - y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) = - Some (Vint (semdivop x y))) -> - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (mod_aux divop a b) - (Vint (Int.sub x (Int.mul (semdivop x y) y))). -Proof. - intros; unfold mod_aux. - eapply eval_Elet. eexact H0. eapply eval_Elet. - apply eval_lift. eexact H1. - eapply eval_Eop. eapply eval_Econs. - eapply eval_Eletvar. simpl; reflexivity. - eapply eval_Econs. eapply eval_Eop. - eapply eval_Econs. eapply eval_Eop. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. - apply H. assumption. - eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. - simpl; reflexivity. apply eval_Enil. - reflexivity. -Qed. - -Theorem eval_mods: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)). -Proof. - intros; unfold mods. - rewrite Int.mods_divs. - eapply eval_mod_aux; eauto. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. -Qed. - -Lemma eval_divu_base: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)). -Proof. - intros. EvalOp. simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. -Qed. - -Theorem eval_divu: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)). -Proof. - intros until y. - unfold divu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. auto. - apply Int.is_power2_range with y. auto. - intros. apply eval_divu_base. auto. EvalOp. auto. - eapply eval_divu_base; eauto. -Qed. - -Theorem eval_modu: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)). -Proof. - intros until y; unfold modu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.modu_and x y i H0). - EvalOp. - intro. rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - auto. EvalOp. auto. auto. - rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. auto. auto. auto. auto. -Qed. - -Theorem eval_and: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (and a b) (Vint (Int.and x y)). -Proof. - intros until y; unfold and; case (and_match a b); intros; InvEval. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Remark eval_same_expr: - forall a1 a2 le v1 v2, - same_expr_pure a1 a2 = true -> - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - a1 = a2 /\ v1 = v2. -Proof. - intros until v2. - destruct a1; simpl; try (intros; discriminate). - destruct a2; simpl; try (intros; discriminate). - case (ident_eq i i0); intros. - subst i0. inversion H0. inversion H1. split. auto. congruence. - discriminate. -Qed. - -Lemma eval_or: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). -Proof. - intros until y; unfold or; case (or_match a b); intros; InvEval. - caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) - && same_expr_pure t1 t2); intro. - destruct (andb_prop _ _ H1). - generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)). - rewrite H4. intro. - exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. - simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror. - destruct n1; auto. destruct n2; auto. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. - econstructor; eauto with evalexpr. - simpl. congruence. - EvalOp. simpl. rewrite Int.or_commut. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_xor: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)). -Proof. - intros until y; unfold xor; case (xor_match a b); intros; InvEval. - rewrite Int.xor_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_shl: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). -Proof. - intros until y; unfold shl; case (shift_match b); intros. - InvEval. apply eval_shlimm; auto. - EvalOp. simpl. rewrite H1. auto. -Qed. - -Theorem eval_shru: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). -Proof. - intros until y; unfold shru; case (shift_match b); intros. - InvEval. apply eval_shruimm; auto. - EvalOp. simpl. rewrite H1. auto. -Qed. - -Theorem eval_shr: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). -Proof. - intros until y; unfold shr; case (shift_match b); intros. - InvEval. apply eval_shrimm; auto. - EvalOp. simpl. rewrite H1. auto. -Qed. - -Theorem eval_cast8signed: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). -Proof. - intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. - -Theorem eval_cast8unsigned: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). -Proof. - intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. - -Theorem eval_cast16signed: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). -Proof. - intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.sign_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. - -Theorem eval_cast16unsigned: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). -Proof. - intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. - rewrite Int.zero_ext_idem. reflexivity. vm_compute; auto. - EvalOp. -Qed. - -Theorem eval_singleoffloat: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). -Proof. - intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. - EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - EvalOp. -Qed. - -Theorem eval_comp_int: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)). -Proof. - intros until y. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. rewrite Int.swap_cmp. rewrite H. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. -Qed. - -Remark eval_compare_null_trans: - forall c x v, - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - match eval_compare_null c x with - | Some true => Some Vtrue - | Some false => Some Vfalse - | None => None (A:=val) - end = Some v. -Proof. - unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. - destruct (Int.eq x Int.zero); try discriminate. - destruct c; try discriminate; auto. -Qed. - -Theorem eval_comp_ptr_int: - forall le c a x1 x2 b y v, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vint y) -> - (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (comp c a b) v. -Proof. - intros until v. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. apply eval_compare_null_trans; auto. - EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto. - EvalOp. simpl. apply eval_compare_null_trans; auto. -Qed. - -Remark eval_swap_compare_null_trans: - forall c x v, - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - match eval_compare_null (swap_comparison c) x with - | Some true => Some Vtrue - | Some false => Some Vfalse - | None => None (A:=val) - end = Some v. -Proof. - unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. - destruct (Int.eq x Int.zero); try discriminate. - destruct c; simpl; try discriminate; auto. -Qed. - -Theorem eval_comp_int_ptr: - forall le c a x b y1 y2 v, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (comp c a b) v. -Proof. - intros until v. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. apply eval_swap_compare_null_trans; auto. - EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto. - EvalOp. simpl. apply eval_compare_null_trans; auto. -Qed. - -Theorem eval_comp_ptr_ptr: - forall le c a x1 x2 b y1 y2, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - x1 = y1 -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). -Proof. - intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. subst y1. rewrite dec_eq_true. - destruct (Int.cmp c x2 y2); reflexivity. -Qed. - -Theorem eval_comp_ptr_ptr_2: - forall le c a x1 x2 b y1 y2 v, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - x1 <> y1 -> - Cminor.eval_compare_mismatch c = Some v -> - eval_expr ge sp e m le (comp c a b) v. -Proof. - intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite dec_eq_false; auto. - destruct c; simpl in H2; inv H2; auto. -Qed. - - -Theorem eval_compu: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). -Proof. - intros until y. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite H. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. -Qed. - -Theorem eval_compf: - forall le c a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)). -Proof. - intros. unfold compf. EvalOp. simpl. - destruct (Float.cmp c x y); reflexivity. -Qed. - -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. apply eval_negate_condition. 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_base_condition_of_expr: - 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 - (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) - b. -Proof. - intros. - eapply eval_CEcond. eauto with evalexpr. - inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto. -Qed. - -Lemma is_compare_neq_zero_correct: - forall c v b, - is_compare_neq_zero c = true -> - eval_condition c (v :: nil) = 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; intro; subst i. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. constructor. - - simpl in H0. destruct v; inv H0. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl. - subst i; constructor. constructor; auto. -Qed. - -Lemma is_compare_eq_zero_correct: - forall c v b, - is_compare_eq_zero c = true -> - eval_condition c (v :: nil) = 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. - apply eval_negate_condition; auto. -Qed. - -Lemma eval_condition_of_expr: - forall a le 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. -Proof. - intro a0; pattern a0. - apply expr_induction_principle; simpl; intros; - try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). - - destruct e0. InvEval. - inversion H1. - rewrite Int.eq_false; auto. constructor. - subst i; rewrite Int.eq_true. constructor. - eapply eval_base_condition_of_expr; eauto. - - inv H0. simpl in H7. - assert (eval_condition c vl = Some b). - destruct (eval_condition c vl); try discriminate. - destruct b0; inv H7; inversion H1; congruence. - 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. -Qed. - -Lemma eval_addressing: - forall le chunk a v b ofs, - eval_expr ge sp e m le a v -> - v = Vptr b ofs -> - match addressing chunk a with (mode, args) => - exists vl, - eval_exprlist ge sp e m le args vl /\ - eval_addressing ge sp mode vl = Some v - end. -Proof. - intros until v. unfold addressing; case (addressing_match a); intros; InvEval. - exists (@nil val). split. eauto with evalexpr. simpl. auto. - exists (Vptr b0 i :: nil). split. eauto with evalexpr. - simpl. congruence. - destruct (is_float_addressing chunk). - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - exists (Vptr b0 i :: Vint i0 :: nil). - split. eauto with evalexpr. simpl. congruence. - destruct (is_float_addressing chunk). - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - exists (Vint i :: Vptr b0 i0 :: nil). - split. eauto with evalexpr. simpl. - rewrite Int.add_commut. congruence. - destruct (is_float_addressing chunk). - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - exists (Vptr b0 i :: Vint i0 :: nil). - split. eauto with evalexpr. simpl. congruence. - exists (v :: nil). split. eauto with evalexpr. - subst v. simpl. rewrite Int.add_zero. auto. -Qed. - -Lemma eval_load: - forall le a v chunk v', - eval_expr ge sp e m le a v -> - Mem.loadv chunk m v = Some v' -> - eval_expr ge sp e m le (load chunk a) v'. -Proof. - intros. generalize H0; destruct v; simpl; intro; try discriminate. - unfold load. - generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a). intros [vl [EV EQ]]. - eapply eval_Eload; eauto. -Qed. - -Lemma eval_store: - forall chunk a1 a2 v1 v2 f k m', - eval_expr ge sp e m nil a1 v1 -> - eval_expr ge sp e m nil a2 v2 -> - Mem.storev chunk m v1 v2 = Some m' -> - step ge (State f (store chunk a1 a2) k sp e m) - E0 (State f Sskip k sp e m'). -Proof. - intros. generalize H1; destruct v1; simpl; intro; try discriminate. - unfold store. - generalize (eval_addressing _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a1). intros [vl [EV EQ]]. - eapply step_store; eauto. -Qed. - -(** * Correctness of instruction selection for operators *) - -(** We now prove a semantic preservation result for the [sel_unop] - and [sel_binop] selection functions. The proof exploits - the results of the previous section. *) - -Lemma eval_sel_unop: - forall le op a1 v1 v, - eval_expr ge sp e m le a1 v1 -> - eval_unop op v1 = Some v -> - eval_expr ge sp e m le (sel_unop op a1) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_cast8unsigned; auto. - apply eval_cast8signed; auto. - apply eval_cast16unsigned; auto. - apply eval_cast16signed; auto. - EvalOp. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro. - change true with (negb false). eapply eval_notbool; eauto. subst i; constructor. - change false with (negb true). eapply eval_notbool; eauto. constructor; auto. - change Vfalse with (Val.of_bool (negb true)). - eapply eval_notbool; eauto. constructor. - apply eval_notint; auto. - EvalOp. - EvalOp. - apply eval_singleoffloat; auto. - EvalOp. - EvalOp. - EvalOp. - EvalOp. -Qed. - -Lemma eval_sel_binop: - forall le op a1 a2 v1 v2 v, - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - eval_binop op v1 v2 = Some v -> - eval_expr ge sp e m le (sel_binop op a1 a2) v. -Proof. - destruct op; simpl; intros; FuncInv; try subst v. - apply eval_add; auto. - apply eval_add_ptr_2; auto. - apply eval_add_ptr; auto. - apply eval_sub; auto. - apply eval_sub_ptr_int; auto. - destruct (eq_block b b0); inv H1. - eapply eval_sub_ptr_ptr; eauto. - apply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. - apply eval_modu; eauto. - apply eval_and; auto. - apply eval_or; auto. - apply eval_xor; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shl; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shr; auto. - caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - apply eval_shru; auto. - EvalOp. - EvalOp. - EvalOp. - EvalOp. - apply eval_comp_int; auto. - eapply eval_comp_int_ptr; eauto. - eapply eval_comp_ptr_int; eauto. - destruct (eq_block b b0); inv H1. - eapply eval_comp_ptr_ptr; eauto. - eapply eval_comp_ptr_ptr_2; eauto. - eapply eval_compu; eauto. - eapply eval_compf; eauto. -Qed. - -End CMCONSTR. - -(** * Semantic preservation for instruction selection. *) - -Section PRESERVATION. - -Variable prog: Cminor.program. -Let tprog := sel_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -(** Relationship between the global environments for the original - CminorSel program and the generated RTL program. *) - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, sel_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: Cminor.fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (sel_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf sel_fundef H). -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 f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf sel_fundef H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (sel_fundef f) = Cminor.funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -(** Semantic preservation for expressions. *) - -Lemma sel_expr_correct: - forall sp e m a v, - Cminor.eval_expr ge sp e m a v -> - forall le, - eval_expr tge sp e m le (sel_expr a) v. -Proof. - induction 1; intros; simpl. - (* Evar *) - constructor; auto. - (* Econst *) - destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]). - rewrite symbols_preserved. auto. - (* Eunop *) - eapply eval_sel_unop; eauto. - (* Ebinop *) - eapply eval_sel_binop; eauto. - (* Eload *) - eapply eval_load; eauto. - (* Econdition *) - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. -Qed. - -Hint Resolve sel_expr_correct: evalexpr. - -Lemma sel_exprlist_correct: - forall sp e m a v, - Cminor.eval_exprlist ge sp e m a v -> - forall le, - eval_exprlist tge sp e m le (sel_exprlist a) v. -Proof. - induction 1; intros; simpl; constructor; auto with evalexpr. -Qed. - -Hint Resolve sel_exprlist_correct: evalexpr. - -(** Semantic preservation for terminating function calls and statements. *) - -Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont := - match k with - | Cminor.Kstop => Kstop - | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1) - | Cminor.Kblock k1 => Kblock (sel_cont k1) - | Cminor.Kcall id f sp e k1 => - Kcall id (sel_function f) sp e (sel_cont k1) - end. - -Inductive match_states: Cminor.state -> CminorSel.state -> Prop := - | match_state: forall f s k s' k' sp e m, - s' = sel_stmt s -> - k' = sel_cont k -> - match_states - (Cminor.State f s k sp e m) - (State (sel_function f) s' k' sp e m) - | match_callstate: forall f args k k' m, - k' = sel_cont k -> - match_states - (Cminor.Callstate f args k m) - (Callstate (sel_fundef f) args k' m) - | match_returnstate: forall v k k' m, - k' = sel_cont k -> - match_states - (Cminor.Returnstate v k m) - (Returnstate v k' m). - -Remark call_cont_commut: - forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k). -Proof. - induction k; simpl; auto. -Qed. - -Remark find_label_commut: - forall lbl s k, - find_label lbl (sel_stmt s) (sel_cont k) = - option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk))) - (Cminor.find_label lbl s k). -Proof. - induction s; intros; simpl; auto. - unfold store. destruct (addressing m (sel_expr e)); auto. - change (Kseq (sel_stmt s2) (sel_cont k)) - with (sel_cont (Cminor.Kseq s2 k)). - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto. - rewrite IHs1. rewrite IHs2. - destruct (Cminor.find_label lbl s1 k); auto. - change (Kseq (Sloop (sel_stmt s)) (sel_cont k)) - with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)). - auto. - change (Kblock (sel_cont k)) - with (sel_cont (Cminor.Kblock k)). - auto. - destruct o; auto. - destruct (ident_eq lbl l); auto. -Qed. - -Lemma sel_step_correct: - forall S1 t S2, Cminor.step ge S1 t S2 -> - forall T1, match_states S1 T1 -> - exists T2, step tge T1 t T2 /\ match_states S2 T2. -Proof. - induction 1; intros T1 ME; inv ME; simpl; - try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail). - - (* skip call *) - econstructor; split. - econstructor. destruct k; simpl in H; simpl; auto. - rewrite <- H0; reflexivity. - constructor; auto. - (* store *) - econstructor; split. - eapply eval_store; eauto with evalexpr. - constructor; auto. - (* Scall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. - (* Stailcall *) - econstructor; split. - econstructor; eauto with evalexpr. - apply functions_translated; eauto. - apply sig_function_translated. - constructor; auto. apply call_cont_commut. - (* Sifthenelse *) - exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split. - constructor. eapply eval_condition_of_expr; eauto with evalexpr. - constructor; auto. destruct b; auto. - (* Sreturn None *) - econstructor; split. - econstructor. - constructor; auto. apply call_cont_commut. - (* Sreturn Some *) - econstructor; split. - econstructor. simpl. eauto with evalexpr. - constructor; auto. apply call_cont_commut. - (* Sgoto *) - econstructor; split. - econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. - rewrite H. simpl. reflexivity. - constructor; auto. -Qed. - -Lemma sel_initial_states: - forall S, Cminor.initial_state prog S -> - exists R, initial_state tprog R /\ match_states S R. -Proof. - induction 1. - econstructor; split. - econstructor. - simpl. fold tge. rewrite symbols_preserved. eexact H. - apply function_ptr_translated. eauto. - rewrite <- H1. apply sig_function_translated; auto. - unfold tprog, sel_program. rewrite Genv.init_mem_transf. - constructor; auto. -Qed. - -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. simpl. constructor. -Qed. - -Theorem transf_program_correct: - forall (beh: program_behavior), not_wrong beh -> - Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. -Proof. - unfold CminorSel.exec_program, Cminor.exec_program; intros. - eapply simulation_step_preservation; eauto. - eexact sel_initial_states. - eexact sel_final_states. - exact sel_step_correct. -Qed. - -End PRESERVATION. -- cgit