From e860ffd69f30ebcd8c84e5909b0e4b190946d351 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 18 Aug 2009 06:41:56 +0000 Subject: Forgot to add some files git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 212 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 212 insertions(+) create mode 100644 backend/Selection.v (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v new file mode 100644 index 0000000..4355faf --- /dev/null +++ b/backend/Selection.v @@ -0,0 +1,212 @@ +(* *********************************************************************) +(* *) +(* 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. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +(** Conversion of 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. + +(** Conversion of loads and stores *) + +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. + +(** Instruction selection for operator applications. Most of the work + is done by the processor-specific smart constructors defined + in module [SelectOp]. *) + +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 => negint arg + | Cminor.Onotbool => notbool arg + | Cminor.Onotint => notint arg + | Cminor.Onegf => negf arg + | Cminor.Oabsf => absf arg + | Cminor.Osingleoffloat => singleoffloat arg + | Cminor.Ointoffloat => intoffloat arg + | Cminor.Ointuoffloat => intuoffloat arg + | Cminor.Ofloatofint => floatofint arg + | Cminor.Ofloatofintu => floatofintu arg + 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 => addf arg1 arg2 + | Cminor.Osubf => subf arg1 arg2 + | Cminor.Omulf => mulf arg1 arg2 + | Cminor.Odivf => divf arg1 arg2 + | 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. + + + -- cgit v1.2.3