Module Initializers


Compile-time evaluation of initializers for global C variables.

Require Import Coqlib Maps Errors.
Require Import Integers Floats Values AST Memory Globalenvs.
Require Import Ctypes Cop Csyntax.

Open Scope error_monad_scope.

Evaluation of compile-time constant expressions


To evaluate constant expressions at compile-time, we use the same value type and the same sem_* functions that are used in CompCert C's semantics (module Csem). However, we interpret pointer values symbolically: Vptr id ofs represents the address of global variable id plus byte offset ofs.

constval a evaluates the constant expression a. If a is a r-value, the returned value denotes: If a is a l-value, the returned value denotes:

Definition do_cast (v: val) (t1 t2: type) : res val :=
  match sem_cast v t1 t2 Mem.empty with
  | Some v' => OK v'
  | None => Error(msg "undefined cast")
  end.

Definition lookup_composite (ce: composite_env) (id: ident) : res composite :=
  match ce!id with
  | Some co => OK co
  | None => Error (MSG "Undefined struct or union " :: CTX id :: nil)
  end.

Fixpoint constval (ce: composite_env) (a: expr) : res val :=
  match a with
  | Eval v ty =>
      match v with
      | Vint _ | Vfloat _ | Vsingle _ | Vlong _ => OK v
      | Vptr _ _ | Vundef => Error(msg "illegal constant")
      end
  | Evalof l ty =>
      match access_mode ty with
      | By_reference | By_copy => constval ce l
      | _ => Error(msg "dereferencing of an l-value")
      end
  | Eaddrof l ty =>
      constval ce l
  | Eunop op r1 ty =>
      do v1 <- constval ce r1;
      match sem_unary_operation op v1 (typeof r1) Mem.empty with
      | Some v => OK v
      | None => Error(msg "undefined unary operation")
      end
  | Ebinop op r1 r2 ty =>
      do v1 <- constval ce r1;
      do v2 <- constval ce r2;
      match sem_binary_operation ce op v1 (typeof r1) v2 (typeof r2) Mem.empty with
      | Some v => OK v
      | None => Error(msg "undefined binary operation")
      end
  | Ecast r ty =>
      do v1 <- constval ce r; do_cast v1 (typeof r) ty
  | Esizeof ty1 ty =>
      OK (Vptrofs (Ptrofs.repr (sizeof ce ty1)))
  | Ealignof ty1 ty =>
      OK (Vptrofs (Ptrofs.repr (alignof ce ty1)))
  | Eseqand r1 r2 ty =>
      do v1 <- constval ce r1;
      do v2 <- constval ce r2;
      match bool_val v1 (typeof r1) Mem.empty with
      | Some true => do_cast v2 (typeof r2) type_bool
      | Some false => OK (Vint Int.zero)
      | None => Error(msg "undefined && operation")
      end
  | Eseqor r1 r2 ty =>
      do v1 <- constval ce r1;
      do v2 <- constval ce r2;
      match bool_val v1 (typeof r1) Mem.empty with
      | Some false => do_cast v2 (typeof r2) type_bool
      | Some true => OK (Vint Int.one)
      | None => Error(msg "undefined || operation")
      end
  | Econdition r1 r2 r3 ty =>
      do v1 <- constval ce r1;
      do v2 <- constval ce r2;
      do v3 <- constval ce r3;
      match bool_val v1 (typeof r1) Mem.empty with
      | Some true => do_cast v2 (typeof r2) ty
      | Some false => do_cast v3 (typeof r3) ty
      | None => Error(msg "condition is undefined")
      end
  | Ecomma r1 r2 ty =>
      do v1 <- constval ce r1; constval ce r2
  | Evar x ty =>
      OK(Vptr x Ptrofs.zero)
  | Ederef r ty =>
      constval ce r
  | Efield l f ty =>
      do (delta, bf) <-
        match typeof l with
        | Tstruct id _ =>
            do co <- lookup_composite ce id; field_offset ce f (co_members co)
        | Tunion id _ =>
            do co <- lookup_composite ce id; union_field_offset ce f (co_members co)
        | _ =>
            Error (msg "ill-typed field access")
        end;
      do v <- constval ce l;
      match bf with
      | Full =>
          OK (if Archi.ptr64
              then Val.addl v (Vlong (Int64.repr delta))
              else Val.add v (Vint (Int.repr delta)))
      | Bits _ _ _ _ =>
          Error(msg "taking the address of a bitfield")
      end
  | Eparen r tycast ty =>
      do v <- constval ce r; do_cast v (typeof r) tycast
  | _ =>
    Error(msg "not a compile-time constant")
  end.

constval_cast ce a ty evaluates a then converts its value to type ty.

Definition constval_cast (ce: composite_env) (a: expr) (ty: type): res val :=
  do v <- constval ce a; do_cast v (typeof a) ty.

Building and recording initialization data


The following state type is the output of the translation of initializers. It contains the list of initialization data generated so far, the corresponding position in bytes, and the total size expected for the final initialization data, in bytes.

Record state : Type := {
  init: list init_data; (* reversed *)
  curr: Z; (* current position for head of init *)
  total_size: Z (* total expected size *)
}.

A state s can also be viewed as a memory block. The size of the block is s.(total_size), it is initialized with zero bytes, then filled with the initialization data rev s.(init) like Genv.store_init_data_list does.

Definition initial_state (sz: Z) : state :=
  {| init := nil; curr := 0; total_size := sz |}.

We now define abstract "store" operations that operate directly on the state, but whose behavior mimic those of storing in the corresponding memory block. To initialize bitfields, we also need an abstract "load" operation. The operations are optimized for stores that occur at increasing positions, like those that take place during initialization.

Initialization from bytes

Definition int_of_byte (b: byte) := Int.repr (Byte.unsigned b).

Definition Init_byte (b: byte) := Init_int8 (int_of_byte b).

Add a list of bytes to a reversed initialization data list.

Fixpoint add_rev_bytes (l: list byte) (il: list init_data) :=
  match l with
  | nil => il
  | b :: l => add_rev_bytes l (Init_byte b :: il)
  end.

Add n zero bytes to an initialization data list.

Definition add_zeros (n: Z) (il: list init_data) :=
  Z.iter n (fun l => Init_int8 Int.zero :: l) il.

Make sure the depth positions at the top of il are bytes, that is, Init_int8 items. Other numerical items are split into bytes. Init_addrof items cannot be split and result in an error.

Fixpoint normalize (il: list init_data) (depth: Z) : res (list init_data) :=
  if zle depth 0 then OK il else
    match il with
    | nil =>
        Error (msg "normalize: empty list")
    | Init_int8 n :: il =>
        do il' <- normalize il (depth - 1);
        OK (Init_int8 n :: il')
    | Init_int16 n :: il =>
        do il' <- normalize il (depth - 2);
        OK (add_rev_bytes (encode_int 2%nat (Int.unsigned n)) il')
    | Init_int32 n :: il =>
        do il' <- normalize il (depth - 4);
        OK (add_rev_bytes (encode_int 4%nat (Int.unsigned n)) il')
    | Init_int64 n :: il =>
        do il' <- normalize il (depth - 8);
        OK (add_rev_bytes (encode_int 8%nat (Int64.unsigned n)) il')
    | Init_float32 f :: il =>
        do il' <- normalize il (depth - 4);
        OK (add_rev_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits f))) il')
    | Init_float64 f :: il =>
        do il' <- normalize il (depth - 8);
        OK (add_rev_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits f))) il')
    | Init_addrof _ _ :: il =>
        Error (msg "normalize: Init_addrof")
    | Init_space n :: il =>
        let n := Z.max 0 n in
        if zle n depth then
          do il' <- normalize il (depth - n);
          OK (add_zeros n il')
        else
          OK (add_zeros depth (Init_space (n - depth) :: il))
    end.

Split il into depth bytes and the initialization list that follows. The bytes are returned reversed.

Fixpoint decompose_rec (accu: list byte) (il: list init_data) (depth: Z) : res (list byte * list init_data) :=
  if zle depth 0 then OK (accu, il) else
    match il with
    | Init_int8 n :: il => decompose_rec (Byte.repr (Int.unsigned n) :: accu) il (depth - 1)
    | _ => Error (msg "decompose: wrong shape")
    end.

Definition decompose (il: list init_data) (depth: Z) : res (list byte * list init_data) :=
  decompose_rec nil il depth.

Decompose an initialization list in three parts: depth bytes (reversed), sz bytes (reversed), and the remainder of the initialization list.

Definition trisection (il: list init_data) (depth sz: Z) : res (list byte * list byte * list init_data) :=
  do il0 <- normalize il (depth + sz);
  do (bytes1, il1) <- decompose il0 depth;
  do (bytes2, il2) <- decompose il1 sz;
  OK (bytes1, bytes2, il2).

Graphically: rev il is equal to 
                 <---sz---><--depth-->
+----------------+---------+---------+
|                |         |         |
+----------------+---------+---------+
    rev il2         bytes2    bytes1

Add padding if necessary so that position pos is within the state.

Definition pad_to (s: state) (pos: Z) : state :=
  if zle pos s.(curr)
  then s
  else {| init := Init_space (pos - s.(curr)) :: s.(init);
          curr := pos;
          total_size := s.(total_size) |}.

Store the initialization data i at position pos in state s.

Definition store_data (s: state) (pos: Z) (i: init_data) : res state :=
  let sz := init_data_size i in
  assertion (zle 0 pos && zle (pos + sz) s.(total_size));
  if zle s.(curr) pos then
    OK {| init := i :: (if zlt s.(curr) pos
                        then Init_space (pos - s.(curr)) :: s.(init)
                        else s.(init));
          curr := pos + sz;
          total_size := s.(total_size) |}
  else
    let s' := pad_to s (pos + sz) in
    do x3 <- trisection s'.(init) (s'.(curr) - (pos + sz)) sz;
    let '(bytes1, _, il2) := x3 in
    OK {| init := add_rev_bytes bytes1 (i :: il2);
          curr := s'.(curr);
          total_size := s'.(total_size) |}.

Store the integer n of size isz at position pos in state s.

Definition init_data_for_carrier (isz: intsize) (n: int) :=
  match isz with
  | I8 | IBool => Init_int8 n
  | I16 => Init_int16 n
  | I32 => Init_int32 n
  end.

Definition store_int (s: state) (pos: Z) (isz: intsize) (n: int) : res state :=
  store_data s pos (init_data_for_carrier isz n).

Load the integer of size isz at position pos in state s.

Definition load_int (s: state) (pos: Z) (isz: intsize) : res int :=
  let chunk := chunk_for_carrier isz in
  let sz := size_chunk chunk in
  assertion (zle 0 pos && zle (pos + sz) s.(total_size));
  let s' := pad_to s (pos + sz) in
  do x3 <- trisection s'.(init) (s'.(curr) - (pos + sz)) sz;
  let '(_, bytes2, _) := x3 in
  OK (Int.repr (decode_int bytes2)).

Extract the final initialization data from a state.

Definition init_data_list_of_state (s: state) : res (list init_data) :=
  assertion (zle s.(curr) s.(total_size));
  let s' := pad_to s s.(total_size) in
  OK (List.rev' s'.(init)).

Translation of initializers


Inductive initializer :=
  | Init_single (a: expr)
  | Init_array (il: initializer_list)
  | Init_struct (il: initializer_list)
  | Init_union (f: ident) (i: initializer)
with initializer_list :=
  | Init_nil
  | Init_cons (i: initializer) (il: initializer_list).

Definition length_initializer_list (il: initializer_list) :=
  let fix length (accu: Z) (il: initializer_list) : Z :=
    match il with Init_nil => accu | Init_cons _ il => length (Z.succ accu) il end
  in length 0 il.

Translate an initializing expression a for a scalar variable of type ty. Return the corresponding initialization datum.

Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data :=
  do v <- constval_cast ce a ty;
  match v, ty with
  | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n)
  | Vint n, Tint I16 sg _ => OK(Init_int16 n)
  | Vint n, Tint I32 sg _ => OK(Init_int32 n)
  | Vint n, Tpointer _ _ => assertion (negb Archi.ptr64); OK(Init_int32 n)
  | Vlong n, Tlong _ _ => OK(Init_int64 n)
  | Vlong n, Tpointer _ _ => assertion (Archi.ptr64); OK(Init_int64 n)
  | Vsingle f, Tfloat F32 _ => OK(Init_float32 f)
  | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
  | Vptr id ofs, Tint I32 sg _ => assertion (negb Archi.ptr64); OK(Init_addrof id ofs)
  | Vptr id ofs, Tlong _ _ => assertion (Archi.ptr64); OK(Init_addrof id ofs)
  | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs)
  | Vundef, _ => Error(msg "undefined operation in initializer")
  | _, _ => Error (msg "type mismatch in initializer")
  end.

Initialize a bitfield Bits sz sg p w with expression a.

Definition transl_init_bitfield (ce: composite_env) (s: state)
                                (ty: type) (sz: intsize) (p w: Z)
                                (i: initializer) (pos: Z) : res state :=
  match i with
  | Init_single a =>
      do v <- constval_cast ce a ty;
      match v with
      | Vint n =>
          do c <- load_int s pos sz;
          let c' := Int.bitfield_insert (first_bit sz p w) w c n in
          store_int s pos sz c'
      | Vundef =>
          Error (msg "undefined operation in bitfield initializer")
      | _ =>
          Error (msg "type mismatch in bitfield initializer")
      end
  | _ =>
      Error (msg "bitfield initialized by composite initializer")
  end.

Padding bitfields and bitfields with zero width are not initialized.

Definition member_not_initialized (m: member) : bool :=
  match m with
  | Member_plain _ _ => false
  | Member_bitfield _ _ _ _ w p => p || zle w 0
  end.

Translate an initializer i for a variable of type ty and store the corresponding list of initialization data in state s at position pos. Return the updated state.

Fixpoint transl_init_rec (ce: composite_env) (s: state)
                         (ty: type) (i: initializer) (pos: Z)
                         {struct i} : res state :=
  match i, ty with
  | Init_single a, _ =>
      do d <- transl_init_single ce ty a; store_data s pos d
  | Init_array il, Tarray tyelt nelt _ =>
      assertion (zle (length_initializer_list il) (Z.max 0 nelt));
      transl_init_array ce s tyelt il pos
  | Init_struct il, Tstruct id _ =>
      do co <- lookup_composite ce id;
      match co_su co with
      | Struct => transl_init_struct ce s (co_members co) il pos 0
      | Union => Error (MSG "struct/union mismatch on " :: CTX id :: nil)
      end
  | Init_union f i1, Tunion id _ =>
      do co <- lookup_composite ce id;
      match co_su co with
      | Struct => Error (MSG "union/struct mismatch on " :: CTX id :: nil)
      | Union => do ty1 <- field_type f (co_members co);
                  do (delta, layout) <- union_field_offset ce f (co_members co);
                  match layout with
                  | Full =>
                      transl_init_rec ce s ty1 i1 (pos + delta)
                  | Bits sz sg p w =>
                      transl_init_bitfield ce s ty1 sz p w i1 (pos + delta)
                  end
      end
  | _, _ =>
      Error (msg "wrong type for compound initializer")
  end

with transl_init_array (ce: composite_env) (s: state)
                       (tyelt: type) (il: initializer_list) (pos: Z)
                       {struct il} : res state :=
  match il with
  | Init_nil =>
      OK s
  | Init_cons i1 il' =>
      do s1 <- transl_init_rec ce s tyelt i1 pos;
      transl_init_array ce s1 tyelt il' (pos + sizeof ce tyelt)
  end

with transl_init_struct (ce: composite_env) (s: state)
                        (ms: members) (il: initializer_list)
                        (base: Z) (pos: Z)
                        {struct il} : res state :=
  match il with
  | Init_nil =>
      OK s
  | Init_cons i1 il' =>
      let fix init (ms: members) (pos: Z) {struct ms} : res state :=
        match ms with
        | nil =>
            Error (msg "too many elements in struct initializer")
        | m :: ms' =>
            if member_not_initialized m then
              init ms' (next_field ce pos m)
            else
              do (delta, layout) <- layout_field ce pos m;
              do s1 <-
                match layout with
                | Full =>
                    transl_init_rec ce s (type_member m) i1 (base + delta)
                | Bits sz sg p w =>
                    transl_init_bitfield ce s (type_member m) sz p w i1 (base + delta)
                end;
                transl_init_struct ce s1 ms' il' base (next_field ce pos m)
         end in
      init ms pos
  end.

The entry point.

Definition transl_init (ce: composite_env) (ty: type) (i: initializer)
                       : res (list init_data) :=
  let s0 := initial_state (sizeof ce ty) in
  do s1 <- transl_init_rec ce s0 ty i 0;
  init_data_list_of_state s1.
Generated by coq2html