From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csharpminor.v | 150 +++++++++++------------------------------------- 1 file changed, 34 insertions(+), 116 deletions(-) (limited to 'cfrontend/Csharpminor.v') diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index f1d22d7e..729814ee 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -9,6 +9,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Cminor. (** Abstract syntax *) @@ -24,52 +25,21 @@ Require Import Globalenvs. Unlike in Cminor (the next intermediate language of the back-end), Csharpminor local variables reside in memory, and their address can be taken using [Eaddrof] expressions. +*) + +Inductive constant : Set := + | Ointconst: int -> constant (**r integer constant *) + | Ofloatconst: float -> constant. (**r floating-point constant *) - Another difference with Cminor is that Csharpminor is entirely - processor-neutral. In particular, Csharpminor uses a standard set of - operations: it does not reflect processor-specific operations nor - addressing modes. *) - -Inductive operation : Set := - | Ointconst: int -> operation (**r integer constant *) - | Ofloatconst: float -> operation (**r floating-point constant *) - | Ocast8unsigned: operation (**r 8-bit zero extension *) - | Ocast8signed: operation (**r 8-bit sign extension *) - | Ocast16unsigned: operation (**r 16-bit zero extension *) - | Ocast16signed: operation (**r 16-bit sign extension *) - | Onotbool: operation (**r boolean negation *) - | Onotint: operation (**r bitwise complement *) - | Oadd: operation (**r integer addition *) - | Osub: operation (**r integer subtraction *) - | Omul: operation (**r integer multiplication *) - | Odiv: operation (**r integer signed division *) - | Odivu: operation (**r integer unsigned division *) - | Omod: operation (**r integer signed modulus *) - | Omodu: operation (**r integer unsigned modulus *) - | Oand: operation (**r bitwise ``and'' *) - | Oor: operation (**r bitwise ``or'' *) - | Oxor: operation (**r bitwise ``xor'' *) - | Oshl: operation (**r left shift *) - | Oshr: operation (**r right signed shift *) - | Oshru: operation (**r right unsigned shift *) - | Onegf: operation (**r float opposite *) - | Oabsf: operation (**r float absolute value *) - | Oaddf: operation (**r float addition *) - | Osubf: operation (**r float subtraction *) - | Omulf: operation (**r float multiplication *) - | Odivf: operation (**r float division *) - | Osingleoffloat: operation (**r float truncation *) - | Ointoffloat: operation (**r integer to float *) - | Ofloatofint: operation (**r float to signed integer *) - | Ofloatofintu: operation (**r float to unsigned integer *) - | Ocmp: comparison -> operation (**r integer signed comparison *) - | Ocmpu: comparison -> operation (**r integer unsigned comparison *) - | Ocmpf: comparison -> operation. (**r float comparison *) +Definition unary_operation : Set := Cminor.unary_operation. +Definition binary_operation : Set := Cminor.binary_operation. Inductive expr : Set := | Evar : ident -> expr (**r reading a scalar variable *) | Eaddrof : ident -> expr (**r taking the address of a variable *) - | Eop : operation -> exprlist -> expr (**r arithmetic operation *) + | Econst : constant -> expr + | Eunop : unary_operation -> expr -> expr + | Ebinop : binary_operation -> expr -> expr -> expr | Eload : memory_chunk -> expr -> expr (**r memory read *) | Ecall : signature -> expr -> exprlist -> expr (**r function call *) | Econdition : expr -> expr -> expr -> expr (**r conditional expression *) @@ -202,78 +172,15 @@ Definition global_var_env (p: program): gvarenv := (** Evaluation of operator applications. *) -Definition eval_compare_null (c: comparison) (n: int) : option val := - if Int.eq n Int.zero - then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end - else None. - -Definition eval_operation (op: operation) (vl: list val) (m: mem): option val := - match op, vl with - | Ointconst n, nil => Some (Vint n) - | Ofloatconst n, nil => Some (Vfloat n) - | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1)) - | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1)) - | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1)) - | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1)) - | Onotbool, Vint n1 :: nil => Some (Val.of_bool (Int.eq n1 Int.zero)) - | Onotbool, Vptr b1 n1 :: nil => Some (Vfalse) - | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1)) - | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) - | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) - | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) - | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None - | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) - | Odiv, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) - | Odivu, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | Omod, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) - | Omodu, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) - | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) - | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) - | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) - | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None - | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None - | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None - | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) - | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) - | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) - | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) - | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) - | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) - | Osingleoffloat, Vfloat f1 :: nil => - Some (Vfloat (Float.singleoffloat f1)) - | Ointoffloat, Vfloat f1 :: nil => - Some (Vint (Float.intoffloat f1)) - | Ofloatofint, Vint n1 :: nil => - Some (Vfloat (Float.floatofint n1)) - | Ofloatofintu, Vint n1 :: nil => - Some (Vfloat (Float.floatofintu n1)) - | Ocmp c, Vint n1 :: Vint n2 :: nil => - Some (Val.of_bool(Int.cmp c n1 n2)) - | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None - else - None - | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2 - | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1 - | Ocmpu c, Vint n1 :: Vint n2 :: nil => - Some (Val.of_bool(Int.cmpu c n1 n2)) - | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil => - Some (Val.of_bool (Float.cmp c f1 f2)) - | _, _ => None +Definition eval_constant (cst: constant) : option val := + match cst with + | Ointconst n => Some (Vint n) + | Ofloatconst n => Some (Vfloat n) end. +Definition eval_unop := Cminor.eval_unop. +Definition eval_binop := Cminor.eval_binop. + (** Allocation of local variables at function entry. Each variable is bound to the reference to a fresh block of the appropriate size. *) @@ -361,11 +268,22 @@ Inductive eval_expr: forall le e m id b, eval_var_addr e id b -> eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero) - | eval_Eop: - forall le e m op al t m1 vl v, - eval_exprlist le e m al t m1 vl -> - eval_operation op vl m1 = Some v -> - eval_expr le e m (Eop op al) t m1 v + | eval_Econst: + forall le e m cst v, + eval_constant cst = Some v -> + eval_expr le e m (Econst cst) E0 m v + | eval_Eunop: + forall le e m op a t m1 v1 v, + eval_expr le e m a t m1 v1 -> + eval_unop op v1 = Some v -> + eval_expr le e m (Eunop op a) t m1 v + | eval_Ebinop: + forall le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v, + eval_expr le e m a1 t1 m1 v1 -> + eval_expr le e m1 a2 t2 m2 v2 -> + eval_binop op v1 v2 m2 = Some v -> + t = t1 ** t2 -> + eval_expr le e m (Ebinop op a1 a2) t m2 v | eval_Eload: forall le e m chunk a t m1 v1 v, eval_expr le e m a t m1 v1 -> -- cgit