Make Clight independent of CompCert C.

Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v


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

1 files changed, 2 insertions, 519 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index ddfbeaf..44a7325 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -25,528 +25,11 @@ Require Import AST.
 Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Ctypes.
+Require Import Cop.
 Require Import Csyntax.
 Require Import Smallstep.
 
-(** * Semantics of type-dependent operations *)
-
-(** Semantics of casts.  [sem_cast v1 t1 t2 = Some v2] if value [v1],
-  viewed with static type [t1], can be cast to type [t2],
-  resulting in value [v2].  *)
-
-Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
-  match sz, sg with
-  | I8, Signed => Int.sign_ext 8 i
-  | I8, Unsigned => Int.zero_ext 8 i
-  | I16, Signed => Int.sign_ext 16 i
-  | I16, Unsigned => Int.zero_ext 16 i 
-  | I32, _ => i
-  | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
-  end.
-
-Definition cast_int_float (si : signedness) (i: int) : float :=
-  match si with
-  | Signed => Float.floatofint i
-  | Unsigned => Float.floatofintu i
-  end.
-
-Definition cast_float_int (si : signedness) (f: float) : option int :=
-  match si with
-  | Signed => Float.intoffloat f
-  | Unsigned => Float.intuoffloat f
-  end.
-
-Definition cast_float_float (sz: floatsize) (f: float) : float :=
-  match sz with
-  | F32 => Float.singleoffloat f
-  | F64 => f
-  end.
-
-Function sem_cast (v: val) (t1 t2: type) : option val :=
-  match classify_cast t1 t2 with
-  | cast_case_neutral =>
-      match v with
-      | Vint _ | Vptr _ _ => Some v
-      | _ => None
-      end
-  | cast_case_i2i sz2 si2 =>
-      match v with
-      | Vint i => Some (Vint (cast_int_int sz2 si2 i))
-      | _ => None
-      end
-  | cast_case_f2f sz2 =>
-      match v with
-      | Vfloat f => Some (Vfloat (cast_float_float sz2 f))
-      | _ => None
-      end
-  | cast_case_i2f si1 sz2 =>
-      match v with
-      | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
-      | _ => None
-      end
-  | cast_case_f2i sz2 si2 =>
-      match v with
-      | Vfloat f =>
-          match cast_float_int si2 f with
-          | Some i => Some (Vint (cast_int_int sz2 si2 i))
-          | None => None
-          end
-      | _ => None
-      end
-  | cast_case_f2bool =>
-      match v with
-      | Vfloat f =>
-          Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one))
-      | _ => None
-      end
-  | cast_case_p2bool =>
-      match v with
-      | Vint i => Some (Vint (cast_int_int IBool Signed i))
-      | Vptr _ _ => Some (Vint Int.one)
-      | _ => None
-      end
-  | cast_case_struct id1 fld1 id2 fld2 =>
-      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
-  | cast_case_union id1 fld1 id2 fld2 =>
-      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
-  | cast_case_void =>
-      Some v
-  | cast_case_default =>
-      None
-  end.
-
-(** Interpretation of values as truth values.
-  Non-zero integers, non-zero floats and non-null pointers are
-  considered as true.  The integer zero (which also represents
-  the null pointer) and the float 0.0 are false. *)
-
-Definition bool_val (v: val) (t: type) : option bool :=
-  match classify_bool t with
-  | bool_case_i =>
-      match v with
-      | Vint n => Some (negb (Int.eq n Int.zero))
-      | _ => None
-      end
-  | bool_case_f =>
-      match v with
-      | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero))
-      | _ => None
-      end
-  | bool_case_p =>
-      match v with
-      | Vint n => Some (negb (Int.eq n Int.zero))
-      | Vptr b ofs => Some true
-      | _ => None
-      end
-  | bool_default => None
-  end.
-
-(** The following [sem_] functions compute the result of an operator
-  application.  Since operators are overloaded, the result depends
-  both on the static types of the arguments and on their run-time values.
-  For binary operations, the "usual binary conversions", adapted to a 32-bit
-  platform, state that:
-- If both arguments are of integer type, an integer operation is performed.
-  For operations that behave differently at unsigned and signed types
-  (e.g. division, modulus, comparisons), the unsigned operation is selected
-  if at least one of the arguments is of type "unsigned int32", otherwise
-  the signed operation is performed.
-- If both arguments are of float type, a float operation is performed.
-  We choose to perform all float arithmetic in double precision,
-  even if both arguments are single-precision floats.
-- If one argument has integer type and the other has float type,
-  we convert the integer argument to float, then perform the float operation.
- *)
-
-Function sem_neg (v: val) (ty: type) : option val :=
-  match classify_neg ty with
-  | neg_case_i sg =>
-      match v with
-      | Vint n => Some (Vint (Int.neg n))
-      | _ => None
-      end
-  | neg_case_f =>
-      match v with
-      | Vfloat f => Some (Vfloat (Float.neg f))
-      | _ => None
-      end
-  | neg_default => None
-  end.
-
-Function sem_notint (v: val) (ty: type): option val :=
-  match classify_notint ty with
-  | notint_case_i sg =>
-      match v with
-      | Vint n => Some (Vint (Int.xor n Int.mone))
-      | _ => None
-      end
-  | notint_default => None
-  end.
-
-Function sem_notbool (v: val) (ty: type) : option val :=
-  match classify_bool ty with
-  | bool_case_i =>
-      match v with
-      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | _ => None
-      end
-  | bool_case_f =>
-      match v with
-      | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero))
-      | _ => None
-      end
-  | bool_case_p =>
-      match v with
-      | Vint n => Some (Val.of_bool (Int.eq n Int.zero))
-      | Vptr _ _ => Some Vfalse
-      | _ => None
-      end
-  | bool_default => None
-  end.
-
-Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_add t1 t2 with 
-  | add_case_ii sg =>                   (**r integer addition *)
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
-      | _,  _ => None
-      end
-  | add_case_ff =>                      (**r float addition *)
-      match v1, v2 with
-      | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
-      | _,  _ => None
-      end
-  | add_case_if sg =>                   (**r int plus float *)
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | add_case_fi sg =>                   (**r float plus int *)
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | add_case_pi ty _ =>                 (**r pointer plus integer *)
-      match v1,v2 with
-      | Vptr b1 ofs1, Vint n2 => 
-        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
-      | _,  _ => None
-      end   
-  | add_case_ip ty _ =>                 (**r integer plus pointer *)
-      match v1,v2 with
-      | Vint n1, Vptr b2 ofs2 => 
-        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
-      | _,  _ => None
-      end   
-  | add_default => None
-end.
-
-Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_sub t1 t2 with
-  | sub_case_ii sg =>            (**r integer subtraction *)
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
-      | _,  _ => None
-      end 
-  | sub_case_ff =>               (**r float subtraction *)
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
-      | _,  _ => None
-      end
-  | sub_case_if sg =>            (**r int minus float *)
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | sub_case_fi sg =>            (**r float minus int *)
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | sub_case_pi ty =>            (**r pointer minus integer *)
-      match v1,v2 with
-      | Vptr b1 ofs1, Vint n2 => 
-            Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
-      | _,  _ => None
-      end
-  | sub_case_pp ty =>          (**r pointer minus pointer *)
-      match v1,v2 with
-      | Vptr b1 ofs1, Vptr b2 ofs2 =>
-          if zeq b1 b2 then
-            if Int.eq (Int.repr (sizeof ty)) Int.zero then None
-            else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty))))
-          else None
-      | _, _ => None
-      end
-  | sub_default => None
-  end.
- 
-Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
- match classify_mul t1 t2 with
-  | mul_case_ii sg =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
-      | _,  _ => None
-      end
-  | mul_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
-      | _,  _ => None
-      end
-  | mul_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | mul_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | mul_default =>
-      None
-end.
-
-Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-   match classify_div t1 t2 with
-  | div_case_ii Unsigned =>
-      match v1,v2 with
-      | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-      | _,_ => None
-      end
-  | div_case_ii Signed =>
-      match v1,v2 with
-       | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero
-          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
-          then None else Some (Vint(Int.divs n1 n2))
-      | _,_ => None
-      end
-  | div_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
-      | _,  _ => None
-      end 
-  | div_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | div_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | div_default =>
-      None
-end.
-
-Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii Unsigned =>
-      match v1, v2 with
-      | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
-      | _, _ => None
-      end
-  | binint_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero
-          || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
-          then None else Some (Vint (Int.mods n1 n2))
-      | _, _ => None
-      end
-  | binint_default =>
-      None
-  end.
-
-Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
-
-Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
-
-Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
-
-Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_shift t1 t2 with
-  | shift_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 =>
-         if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
-      | _, _ => None
-      end
-  | shift_default => None
-  end.
-
-Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
-  match classify_shift t1 t2 with 
-  | shift_case_ii Unsigned =>
-      match v1,v2 with 
-      | Vint n1, Vint n2 =>
-          if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
-      | _,_ => None
-      end
-   | shift_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1,  Vint n2 =>
-          if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
-      | _,  _ => None
-      end
-   | shift_default =>
-      None
-   end.
-
-Function sem_cmp_mismatch (c: comparison): option val :=
-  match c with
-  | Ceq =>  Some Vfalse
-  | Cne =>  Some Vtrue
-  | _   => None
-  end.
-
-Function sem_cmp (c:comparison)
-                  (v1: val) (t1: type) (v2: val) (t2: type)
-                  (m: mem): option val :=
-  match classify_cmp t1 t2 with
-  | cmp_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
-      | _,  _ => None
-      end
-  | cmp_case_ii Unsigned =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
-      | _,  _ => None
-      end
-  | cmp_case_pp =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
-      | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if Mem.valid_pointer m b1 (Int.unsigned ofs1)
-          && Mem.valid_pointer m b2 (Int.unsigned ofs2) then
-            if zeq b1 b2
-            then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
-            else sem_cmp_mismatch c
-          else None
-      | Vptr b ofs, Vint n =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
-      | Vint n, Vptr b ofs =>
-          if Int.eq n Int.zero then sem_cmp_mismatch c else None
-      | _,  _ => None
-      end
-  | cmp_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))  
-      | _,  _ => None
-      end
-  | cmp_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | cmp_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | cmp_default => None
-  end.
-
-Definition sem_unary_operation
-            (op: unary_operation) (v: val) (ty: type): option val :=
-  match op with
-  | Onotbool => sem_notbool v ty
-  | Onotint => sem_notint v ty
-  | Oneg => sem_neg v ty
-  end.
-
-Definition sem_binary_operation
-    (op: binary_operation)
-    (v1: val) (t1: type) (v2: val) (t2:type)
-    (m: mem): option val :=
-  match op with
-  | Oadd => sem_add v1 t1 v2 t2
-  | Osub => sem_sub v1 t1 v2 t2 
-  | Omul => sem_mul v1 t1 v2 t2
-  | Omod => sem_mod v1 t1 v2 t2
-  | Odiv => sem_div v1 t1 v2 t2 
-  | Oand => sem_and v1 t1 v2 t2
-  | Oor  => sem_or v1 t1 v2 t2
-  | Oxor  => sem_xor v1 t1 v2 t2
-  | Oshl => sem_shl v1 t1 v2 t2
-  | Oshr  => sem_shr v1 t1 v2 t2   
-  | Oeq => sem_cmp Ceq v1 t1 v2 t2 m
-  | One => sem_cmp Cne v1 t1 v2 t2 m
-  | Olt => sem_cmp Clt v1 t1 v2 t2 m
-  | Ogt => sem_cmp Cgt v1 t1 v2 t2 m
-  | Ole => sem_cmp Cle v1 t1 v2 t2 m
-  | Oge => sem_cmp Cge v1 t1 v2 t2 m
-  end.
-
-Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) :=
-  match id with
-  | Incr => sem_add v ty (Vint Int.one) type_int32s
-  | Decr => sem_sub v ty (Vint Int.one) type_int32s
-  end.
-
-(** Common-sense relations between boolean operators *)
-
-Lemma cast_bool_bool_val:
-  forall v t,
-  sem_cast v t (Tint IBool Signed noattr) =
-  match bool_val v t with None => None | Some b => Some(Val.of_bool b) end.
-Proof.
-  intros.
-  assert (A: classify_bool t =
-    match t with
-    | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p
-    | Tfloat _ _ => bool_case_f
-    | _ => bool_default
-    end).
-  unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto.
-
-  unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
-  destruct (Int.eq i0 Int.zero); auto. 
-  destruct (Float.cmp Ceq f0 Float.zero); auto.
-  destruct (Int.eq i Int.zero); auto. 
-  destruct (Int.eq i Int.zero); auto. 
-  destruct (Int.eq i Int.zero); auto. 
-Qed.
-
-Lemma notbool_bool_val:
-  forall v t,
-  sem_notbool v t =
-  match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end.
-Proof.
-  intros. unfold sem_notbool, bool_val. 
-  destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto.
-Qed.
-
 (** * Operational semantics *)
 
 (** The semantics uses two environments.  The global environment