diff options
Diffstat (limited to 'cfrontend/SimplExpr.v')
-rw-r--r-- | cfrontend/SimplExpr.v | 150 |
1 files changed, 110 insertions, 40 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index c7e57a54..bb1dbe38 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -13,17 +13,8 @@ (** Translation from Compcert C to Clight. Side effects are pulled out of Compcert C expressions. *) -Require Import Coqlib. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Clight. +Require Import Coqlib Maps Integers Floats Values AST Memory Errors. +Require Import Ctypes Cop Csyntax Clight. Local Open Scope string_scope. Local Open Scope list_scope. @@ -71,8 +62,6 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200) : gensym_monad_scope. -Local Open Scope gensym_monad_scope. - Parameter first_unused_ident: unit -> ident. Definition initial_generator (x: unit) : generator := @@ -96,6 +85,12 @@ Fixpoint makeseq_rec (s: statement) (l: list statement) : statement := Definition makeseq (l: list statement) : statement := makeseq_rec Sskip l. +Section SIMPL_EXPR. + +Local Open Scope gensym_monad_scope. + +Variable ce: composite_env. + (** Smart constructor for [if ... then ... else]. *) Fixpoint eval_simpl_expr (a: expr) : option val := @@ -144,16 +139,64 @@ Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr := | Decr => Ebinop Osub a (Econst_int Int.one type_int32s) (incrdecr_type ty) end. -(** Generate a [Sset] or [Sbuiltin] operation as appropriate - to dereference a l-value [l] and store its result in temporary variable [id]. *) +(** Given a simple l-value expression [l], determine whether it + designates a bitfield. *) + +Definition is_bitfield_access_aux + (fn: composite_env -> ident -> members -> res (Z * bitfield)) + (id: ident) (fld: ident) : mon bitfield := + match ce!id with + | None => error (MSG "unknown composite " :: CTX id :: nil) + | Some co => + match fn ce fld (co_members co) with + | OK (_, bf) => ret bf + | Error _ => error (MSG "unknown field " :: CTX fld :: nil) + end + end. -Definition chunk_for_volatile_type (ty: type) : option memory_chunk := - if type_is_volatile ty - then match access_mode ty with By_value chunk => Some chunk | _ => None end +Definition is_bitfield_access (l: expr) : mon bitfield := + match l with + | Efield r f _ => + match typeof r with + | Tstruct id _ => is_bitfield_access_aux field_offset id f + | Tunion id _ => is_bitfield_access_aux union_field_offset id f + | _ => error (msg "is_bitfield_access") + end + | _ => ret Full + end. + +(** According to the CompCert C semantics, an access to a l-value of + volatile-qualified type can either + - produce an event in the trace of observable events, or + - produce no event and behave as if no volatile qualifier was there. + + The latter case, where the volatile qualifier is ignored, happens if + - the l-value is a struct or union + - the l-value is an access to a bit field. + + The [chunk_for_volatile_type] function distinguishes between the two + cases. It returns [Some chunk] if the semantics is to produce + an observable event of the [Event_vload chunk] or [Event_vstore chunk] + kind. It returns [None] if the semantics is that of a non-volatile + access. *) + +Definition chunk_for_volatile_type (ty: type) (bf: bitfield) : option memory_chunk := + if type_is_volatile ty then + match access_mode ty with + | By_value chunk => + match bf with + | Full => Some chunk + | Bits _ _ _ _ => None + end + | _ => None + end else None. -Definition make_set (id: ident) (l: expr) : statement := - match chunk_for_volatile_type (typeof l) with +(** Generate a [Sset] or [Sbuiltin] operation as appropriate + to dereference a l-value [l] and store its result in temporary variable [id]. *) + +Definition make_set (bf: bitfield) (id: ident) (l: expr) : statement := + match chunk_for_volatile_type (typeof l) bf with | None => Sset id l | Some chunk => let typtr := Tpointer (typeof l) noattr in @@ -165,13 +208,15 @@ Definition make_set (id: ident) (l: expr) : statement := Definition transl_valof (ty: type) (l: expr) : mon (list statement * expr) := if type_is_volatile ty - then do t <- gensym ty; ret (make_set t l :: nil, Etempvar t ty) + then do t <- gensym ty; + do bf <- is_bitfield_access l; + ret (make_set bf t l :: nil, Etempvar t ty) else ret (nil, l). (** Translation of an assignment. *) -Definition make_assign (l r: expr) : statement := - match chunk_for_volatile_type (typeof l) with +Definition make_assign (bf: bitfield) (l r: expr) : statement := + match chunk_for_volatile_type (typeof l) bf with | None => Sassign l r | Some chunk => @@ -181,6 +226,30 @@ Definition make_assign (l r: expr) : statement := (Eaddrof l typtr :: r :: nil) end. +(** Translation of the value of an assignment expression. + For non-bitfield assignments, it's the value of the right-hand side + converted to the type of the left-hand side. + For assignments to bitfields, an additional normalization to + the width and signedness of the bitfield is required. *) + +Definition make_normalize (sz: intsize) (sg: signedness) (width: Z) (r: expr) := + let intconst (n: Z) := Econst_int (Int.repr n) type_int32s in + if intsize_eq sz IBool || signedness_eq sg Unsigned then + let mask := two_p width - 1 in + Ebinop Oand r (intconst mask) (typeof r) + else + let amount := Int.zwordsize - width in + Ebinop Oshr + (Ebinop Oshl r (intconst amount) type_int32s) + (intconst amount) + (typeof r). + +Definition make_assign_value (bf: bitfield) (r: expr): expr := + match bf with + | Full => r + | Bits sz sg pos width => make_normalize sz sg width r + end. + (** Translation of expressions. Return a pair [(sl, a)] of a list of statements [sl] and a pure expression [a]. - If the [dst] argument is [For_val], the statements [sl] @@ -229,7 +298,7 @@ Definition sd_seqbool_set (ty: type) (sd: set_destination) := Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with - | Csyntax.Eloc b ofs ty => + | Csyntax.Eloc b ofs bf ty => error (msg "SimplExpr.transl_expr: Eloc") | Csyntax.Evar x ty => ret (finish dst nil (Evar x ty)) @@ -335,16 +404,17 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement | Csyntax.Eassign l1 r2 ty => do (sl1, a1) <- transl_expr For_val l1; do (sl2, a2) <- transl_expr For_val r2; + do bf <- is_bitfield_access a1; let ty1 := Csyntax.typeof l1 in let ty2 := Csyntax.typeof r2 in match dst with | For_val | For_set _ => do t <- gensym ty1; ret (finish dst - (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil) - (Etempvar t ty1)) + (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign bf a1 (Etempvar t ty1) :: nil) + (make_assign_value bf (Etempvar t ty1))) | For_effects => - ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil, + ret (sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil, dummy_expr) end | Csyntax.Eassignop op l1 r2 tyres ty => @@ -352,31 +422,33 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl1, a1) <- transl_expr For_val l1; do (sl2, a2) <- transl_expr For_val r2; do (sl3, a3) <- transl_valof ty1 a1; + do bf <- is_bitfield_access a1; match dst with | For_val | For_set _ => do t <- gensym ty1; ret (finish dst (sl1 ++ sl2 ++ sl3 ++ Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: - make_assign a1 (Etempvar t ty1) :: nil) - (Etempvar t ty1)) + make_assign bf a1 (Etempvar t ty1) :: nil) + (make_assign_value bf (Etempvar t ty1))) | For_effects => - ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil, + ret (sl1 ++ sl2 ++ sl3 ++ make_assign bf a1 (Ebinop op a3 a2 tyres) :: nil, dummy_expr) end | Csyntax.Epostincr id l1 ty => let ty1 := Csyntax.typeof l1 in do (sl1, a1) <- transl_expr For_val l1; + do bf <- is_bitfield_access a1; match dst with | For_val | For_set _ => do t <- gensym ty1; ret (finish dst - (sl1 ++ make_set t a1 :: - make_assign a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: nil) + (sl1 ++ make_set bf t a1 :: + make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: nil) (Etempvar t ty1)) | For_effects => do (sl2, a2) <- transl_valof ty1 a1; - ret (sl1 ++ sl2 ++ make_assign a1 (transl_incrdecr id a2 ty1) :: nil, + ret (sl1 ++ sl2 ++ make_assign bf a1 (transl_incrdecr id a2 ty1) :: nil, dummy_expr) end | Csyntax.Ecomma r1 r2 ty => @@ -424,12 +496,6 @@ Definition transl_expression (r: Csyntax.expr) : mon (statement * expr) := Definition transl_expr_stmt (r: Csyntax.expr) : mon statement := do (sl, a) <- transl_expr For_effects r; ret (makeseq sl). -(* -Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement := - do (sl, a) <- transl_expr For_val r; - ret (makeseq (sl ++ makeif a s1 s2 :: nil)). -*) - Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement := do (sl, a) <- transl_expr For_val r; ret (makeseq (sl ++ makeif a s1 s2 :: nil)). @@ -533,8 +599,12 @@ Definition transl_fundef (fd: Csyntax.fundef) : res fundef := OK (External ef targs tres cc) end. +End SIMPL_EXPR. + +Local Open Scope error_monad_scope. + Definition transl_program (p: Csyntax.program) : res program := - do p1 <- AST.transform_partial_program transl_fundef p; + do p1 <- AST.transform_partial_program (transl_fundef p.(prog_comp_env)) p; OK {| prog_defs := AST.prog_defs p1; prog_public := AST.prog_public p1; prog_main := AST.prog_main p1; |