From c6d2ef0c5c896a82295c1fb8a717ea29ee3c0e4d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Oct 2012 07:12:33 +0000 Subject: 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 --- cfrontend/Csem.v | 521 +------------------------------------------------------ 1 file changed, 2 insertions(+), 519 deletions(-) (limited to 'cfrontend/Csem.v') 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 -- cgit v1.2.3