Initializers for global variables: compile-time evaluation of expressions done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 173 insertions, 0 deletions

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
new file mode 100644
index 00000000..926a8267
--- /dev/null
+++ b/cfrontend/Initializers.v
@@ -0,0 +1,173 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Compile-time evaluation of initializers for global C variables. *)
+
+Require Import Coqlib.
+Require Import Errors.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import AST.
+Require Import Memory.
+Require Import Csyntax.
+Require Import Csem.
+
+Open Scope error_monad_scope.
+
+(** * Evaluation of compile-time constant expressions *)
+
+(** Computing the predicates [cast], [is_true], and [is_false]. *)
+
+Definition bool_val (v: val) (t: type) : res bool :=
+  match v, t with
+  | Vint n, Tint sz sg => OK (negb (Int.eq n Int.zero))
+  | Vint n, Tpointer t' => OK (negb (Int.eq n Int.zero))
+  | Vptr b ofs, Tint sz sg => OK true
+  | Vptr b ofs, Tpointer t' => OK true
+  | Vfloat f, Tfloat sz => OK (negb(Float.cmp Ceq f Float.zero))
+  | _, _ => Error(msg "undefined conditional")
+  end.
+
+Definition is_neutral_for_cast (t: type) : bool :=
+  match t with
+  | Tint I32 sg => true
+  | Tpointer ty => true
+  | Tarray ty sz => true
+  | Tfunction targs tres => true
+  | _ => false
+  end.
+
+Definition do_cast (v: val) (t1 t2: type) : res val :=
+  match v, t1, t2 with
+  | Vint i, Tint sz1 si1, Tint sz2 si2 =>
+      OK (Vint (cast_int_int sz2 si2 i))
+  | Vfloat f, Tfloat sz1, Tint sz2 si2 =>
+      match cast_float_int si2 f with
+      | Some i => OK (Vint (cast_int_int sz2 si2 i))
+      | None => Error(msg "overflow in float-to-int cast")
+      end
+  | Vint i, Tint sz1 si1, Tfloat sz2 =>
+      OK (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+  | Vfloat f, Tfloat sz1, Tfloat sz2 =>
+      OK (Vfloat (cast_float_float sz2 f))
+  | Vptr b ofs, _, _ =>
+      if is_neutral_for_cast t1 && is_neutral_for_cast t2
+      then OK(Vptr b ofs) else Error(msg "undefined cast")
+  | Vint n, _, _ =>
+      if is_neutral_for_cast t1 && is_neutral_for_cast t2
+      then OK(Vint n) else Error(msg "undefined cast")
+  | _, _, _ =>
+      Error(msg "undefined cast")
+  end.
+
+(** 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 (Zpos 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:
+- [Vint n], [Vfloat f]: the corresponding number
+- [Vptr id ofs]: address of global variable [id] plus byte offset [ofs]
+- [Vundef]: erroneous expression
+
+If [a] is a l-value, the returned value denotes:
+- [Vptr id ofs]: global variable [id] plus byte offset [ofs]
+*)
+
+Fixpoint constval (a: expr) : res val :=
+  match a with
+  | Eval v ty =>
+      match v with
+      | Vint _ | Vfloat _ => OK v
+      | Vptr _ _ | Vundef => Error(msg "illegal constant")
+      end
+  | Evalof l ty =>
+      match access_mode ty with
+      | By_reference => constval l
+      | _ => Error(msg "dereference operation")
+      end
+  | Eaddrof l ty =>
+      constval l
+  | Eunop op r1 ty =>
+      do v1 <- constval r1;
+      match sem_unary_operation op v1 (typeof r1) with
+      | Some v => OK v
+      | None => Error(msg "undefined unary operation")
+      end
+  | Ebinop op r1 r2 ty =>
+      do v1 <- constval r1;
+      do v2 <- constval r2;
+      match sem_binary_operation 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 v <- constval r; do_cast v (typeof r) ty
+  | Esizeof ty1 ty =>
+      OK (Vint (Int.repr (sizeof ty1)))
+  | Econdition r1 r2 r3 ty =>
+      do v1 <- constval r1;
+      do b1 <- bool_val v1 (typeof r1);
+      do v2 <- constval r2;
+      do v3 <- constval r3;
+      OK (if b1 then v2 else v3)
+  | Ecomma r1 r2 ty =>
+      do v1 <- constval r1; constval r2
+  | Evar x ty =>
+      OK(Vptr (Zpos x) Int.zero)
+  | Ederef r ty =>
+      constval r
+  | Efield l f ty =>
+      match typeof l with
+      | Tstruct id fList =>
+          do delta <- field_offset f fList;
+          do v <- constval l;
+          OK (Val.add v (Vint (Int.repr delta)))
+      | Tunion id fList =>
+          constval l
+      | _ =>
+          Error(msg "ill-typed field access")
+      end
+  | Eparen r ty =>
+      constval r
+  | _ =>
+    Error(msg "not a compile-time constant")
+  end.
+
+(** * Translation of initializers *)
+
+(** Translate an initializing expression [a] for a scalar variable
+  of type [ty].  Return the corresponding [init_data]. *)
+
+Definition transl_init_single (ty: type) (a: expr) : res init_data :=
+  do v1 <- constval a;
+  do v2 <- do_cast v1 (typeof a) ty;
+  match v2, ty with
+  | Vint n, Tint I8 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 _ => OK(Init_int32 n)
+  | Vfloat f, Tfloat F32 => OK(Init_float32 f)
+  | Vfloat f, Tfloat F64 => OK(Init_float64 f)
+  | Vptr (Zpos id) ofs, Tint I32 sg => OK(Init_addrof id ofs)
+  | Vptr (Zpos id) ofs, Tpointer _ => OK(Init_addrof id ofs)
+  | Vundef, _ => Error(msg "undefined operation in initializer")
+  | _, _ => Error (msg "type mismatch in initializer")
+  end.
+
+(** To come later: translation of compound initializers, currently
+  still done in Caml (module [C2C]). *)
+