aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplExpr.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/SimplExpr.v')
-rw-r--r--cfrontend/SimplExpr.v150
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;
generated by cgit (git 2.34.1) at 2024-05-17 09:27:30 +0000