diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-13 09:00:12 +0200 |
| commit | 1915258c8b2cd2e171bbce93658047a765232bc9 (patch) | |
| tree | 2f4e5d6acf77a0bc30c9816394a65f868c39a6c0 /cfrontend/Csem.v | |
| parent | 8d2a0c12b27e82c67acc2693ecd6f1e2fede3b88 (diff) | |
| download | compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.tar.gz compcert-kvx-1915258c8b2cd2e171bbce93658047a765232bc9.zip | |
Revised translation of '&&' and '||' to Clight.
The previous translation (in SimplExpr) produced references to the
same temporary variable with two different types (bool and int),
which is not nice if we want to typecheck the generated Clight.
The new translation avoids this and also gets rid of the double
cast to bool then to int. The trick is to change Eparen
(in CompCert C expressions) to take two types: the type to which the
argument must be converted, and the type with which the resulting
expression is seen.
Diffstat (limited to 'cfrontend/Csem.v')
| -rw-r--r-- | cfrontend/Csem.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 55c37c99..06cea006 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -248,7 +248,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := | red_seqand_true: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some true -> rred (Eseqand (Eval v1 ty1) r2 ty) m - E0 (Eparen (Eparen r2 type_bool) ty) m + E0 (Eparen r2 type_bool ty) m | red_seqand_false: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some false -> rred (Eseqand (Eval v1 ty1) r2 ty) m @@ -260,11 +260,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := | red_seqor_false: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some false -> rred (Eseqor (Eval v1 ty1) r2 ty) m - E0 (Eparen (Eparen r2 type_bool) ty) m + E0 (Eparen r2 type_bool ty) m | red_condition: forall v1 ty1 r1 r2 ty b m, bool_val v1 ty1 = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m - E0 (Eparen (if b then r1 else r2) ty) m + E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m @@ -295,9 +295,9 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := typeof r2 = ty -> rred (Ecomma (Eval v ty1) r2 ty) m E0 r2 m - | red_paren: forall v1 ty1 ty m v, - sem_cast v1 ty1 ty = Some v -> - rred (Eparen (Eval v1 ty1) ty) m + | red_paren: forall v1 ty1 ty2 ty m v, + sem_cast v1 ty1 ty2 = Some v -> + rred (Eparen (Eval v1 ty1) ty2 ty) m E0 (Eval v ty) m | red_builtin: forall ef tyargs el ty m vargs t vres m', cast_arguments el tyargs vargs -> @@ -379,8 +379,8 @@ Inductive context: kind -> kind -> (expr -> expr) -> Prop := contextlist k C -> context k RV (fun x => Ebuiltin ef tyargs (C x) ty) | ctx_comma: forall k C e2 ty, context k RV C -> context k RV (fun x => Ecomma (C x) e2 ty) - | ctx_paren: forall k C ty, - context k RV C -> context k RV (fun x => Eparen (C x) ty) + | ctx_paren: forall k C tycast ty, + context k RV C -> context k RV (fun x => Eparen (C x) tycast ty) with contextlist: kind -> (expr -> exprlist) -> Prop := | ctx_list_head: forall k C el, |