diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /cfrontend/Cshmgen.v | |
parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
download | compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.tar.gz compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.zip |
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgen.v')
-rw-r--r-- | cfrontend/Cshmgen.v | 89 |
1 files changed, 56 insertions, 33 deletions
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 937ea78a..6ec3757b 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -253,6 +253,14 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := (** * Reading and writing variables *) +(** Determine if a C expression is a variable *) + +Definition is_variable (e: Csyntax.expr) : option ident := + match e with + | Expr (Csyntax.Evar id) _ => Some id + | _ => None + end. + (** [var_get id ty] returns Csharpminor code that evaluates to the value of C variable [id] with type [ty]. Note that C variables of array or function type evaluate to the address @@ -277,7 +285,19 @@ Definition var_set (id: ident) (ty: type) (rhs: expr) := | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil) end. -(** * Translation of operators *) +(** Auxiliary for translating call statements *) + +Definition transl_lhs_call (opta: option Csyntax.expr) : res (option ident) := + match opta with + | None => OK None + | Some a => + match is_variable a with + | None => Error (msg "LHS of function call is not a variable") + | Some id => OK (Some id) + end + end. + +(** ** Translation of operators *) Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr := match op with @@ -350,15 +370,6 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr := do tc <- transl_expr c; do ts <- make_add tb (typeof b) tc (typeof c); make_load ts ty - | Expr (Csyntax.Ecall b cl) _ => - match (classify_fun (typeof b)) with - | fun_case_f args res => - do tb <- transl_expr b; - do tcl <- transl_exprlist cl; - OK(Ecall (signature_of_type args res) tb tcl) - | _ => - Error(msg "Cshmgen.transl_expr(call)") - end | Expr (Csyntax.Eandbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; @@ -413,31 +424,23 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr := end | _ => Error(msg "Cshmgen.transl_lvalue") - end + end. (** [transl_exprlist al] returns a list of Csharpminor expressions that compute the values of the list [al] of Csyntax expressions. Used for function applications. *) -with transl_exprlist (al: Csyntax.exprlist): res exprlist := +Fixpoint transl_exprlist (al: list Csyntax.expr): res (list expr) := match al with - | Csyntax.Enil => OK Enil - | Csyntax.Econs a1 a2 => + | nil => OK nil + | a1 :: a2 => do ta1 <- transl_expr a1; do ta2 <- transl_exprlist a2; - OK (Econs ta1 ta2) + OK (ta1 :: ta2) end. (** * Translation of statements *) -(** Determine if a C expression is a variable *) - -Definition is_variable (e: Csyntax.expr) : option ident := - match e with - | Expr (Csyntax.Evar id) _ => Some id - | _ => None - end. - (** [exit_if_false e] return the statement that tests the boolean value of the Clight expression [e]. If [e] evaluates to false, an [exit 0] is performed. If [e] evaluates to true, the generated @@ -512,15 +515,18 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int | LScase ni _ rem => (ni, k) :: switch_table rem (k+1) end. +Definition is_Sskip: + forall (s: Csyntax.statement), {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}. +Proof. + destruct s; ((left; reflexivity) || (right; congruence)). +Qed. + Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt := match s with | Csyntax.Sskip => OK Sskip - | Csyntax.Sexpr e => - do te <- transl_expr e; - OK (Sexpr te) | Csyntax.Sassign b c => - match (is_variable b) with + match is_variable b with | Some id => do tc <- transl_expr c; var_set id (typeof b) tc @@ -529,6 +535,15 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r do tc <- transl_expr c; make_store tb (typeof b) tc end + | Csyntax.Scall opta b cl => + match classify_fun (typeof b) with + | fun_case_f args res => + do optid <- transl_lhs_call opta; + do tb <- transl_expr b; + do tcl <- transl_exprlist cl; + OK(Scall optid (signature_of_type args res) tb tcl) + | _ => Error(msg "Cshmgen.transl_stmt(call)") + end | Csyntax.Ssequence s1 s2 => do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; @@ -547,11 +562,17 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r do ts1 <- transl_statement 1%nat 0%nat s1; OK (Sblock (Sloop (Sseq (Sblock ts1) te))) | Csyntax.Sfor e1 e2 e3 s1 => - do te1 <- transl_statement nbrk ncnt e1; - do te2 <- exit_if_false e2; - do te3 <- transl_statement nbrk ncnt e3; - do ts1 <- transl_statement 1%nat 0%nat s1; - OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + if is_Sskip e1 then + (do te2 <- exit_if_false e2; + do te3 <- transl_statement nbrk ncnt e3; + do ts1 <- transl_statement 1%nat 0%nat s1; + OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + else + (do te1 <- transl_statement nbrk ncnt e1; + do te2 <- exit_if_false e2; + do te3 <- transl_statement nbrk ncnt e3; + do ts1 <- transl_statement 1%nat 0%nat s1; + OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))) | Csyntax.Sbreak => OK (Sexit nbrk) | Csyntax.Scontinue => @@ -579,7 +600,7 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts)) end. -(** * Translation of functions and programs *) +(*** Translation of functions *) Definition prefix_var_name (id: ident) : errmsg := MSG "In local variable " :: CTX id :: MSG ":\n" :: nil. @@ -603,6 +624,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef := OK(AST.External (external_function id args res)) end. +(** ** Translation of programs *) + Definition transl_globvar (ty: type) := var_kind_of_type ty. Definition transl_program (p: Csyntax.program) : res program := |