diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 46 | ||||
| -rw-r--r-- | cfrontend/CPragmas.ml | 3 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 4 | ||||
| -rw-r--r-- | cfrontend/Clight.v | 4 | ||||
| -rw-r--r-- | cfrontend/Cminorgen.v | 3 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 87 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 953 | ||||
| -rw-r--r-- | cfrontend/Csharpminor.v | 4 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 206 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 526 | ||||
| -rw-r--r-- | cfrontend/Ctypes.v | 13 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 3 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 222 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 4 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 10 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 3 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 4 | ||||
| -rw-r--r-- | cfrontend/SimplLocals.v | 6 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 244 |
19 files changed, 1261 insertions, 1084 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3bf459f..0ffbd66 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -160,10 +160,12 @@ let register_stub_function name tres targs = let rec letters_of_type = function | Tnil -> [] | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl + | Tcons(Tlong _, tl) -> "l" :: letters_of_type tl | Tcons(_, tl) -> "i" :: letters_of_type tl in let rec types_of_types = function | Tnil -> Tnil | Tcons(Tfloat _, tl) -> Tcons(Tfloat(F64, noattr), types_of_types tl) + | Tcons(Tlong _, tl) -> Tcons(Tlong(Signed, noattr), types_of_types tl) | Tcons(_, tl) -> Tcons(Tpointer(Tvoid, noattr), types_of_types tl) in let stub_name = name ^ "$" ^ String.concat "" (letters_of_type targs) in @@ -211,6 +213,7 @@ let mergeTypAttr ty a2 = | Tvoid -> ty | Tint(sz, sg, a1) -> Tint(sz, sg, mergeAttr a1 a2) | Tfloat(sz, a1) -> Tfloat(sz, mergeAttr a1 a2) + | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2) | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2) | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2) | Tfunction(targs, tres) -> ty @@ -233,8 +236,7 @@ let convertIkind = function | C.ILong -> (Signed, I32) | C.IULong -> (Unsigned, I32) (* Special-cased in convertTyp below *) - | C.ILongLong -> unsupported "'long long' type"; (Signed, I32) - | C.IULongLong -> unsupported "'unsigned long long' type"; (Unsigned, I32) + | C.ILongLong | C.IULongLong -> assert false let convertFkind = function | C.FFloat -> F32 @@ -243,14 +245,6 @@ let convertFkind = function if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 -let int64_struct a = - let ty = Tint(I32,Unsigned,noattr) in - Tstruct(intern_string "struct __int64", - (if Memdataaux.big_endian - then Fcons(intern_string "hi", ty, Fcons(intern_string "lo", ty, Fnil)) - else Fcons(intern_string "lo", ty, Fcons(intern_string "hi", ty, Fnil))), - a) - (** A cache for structs and unions already converted *) let compositeCache : (C.ident, coq_type) Hashtbl.t = Hashtbl.create 77 @@ -260,8 +254,10 @@ let convertTyp env t = let rec convertTyp seen t = match Cutil.unroll env t with | C.TVoid a -> Tvoid - | C.TInt((C.ILongLong|C.IULongLong), a) when !Clflags.option_flonglong -> - int64_struct (convertAttr a) + | C.TInt(C.ILongLong, a) -> + Tlong(Signed, convertAttr a) + | C.TInt(C.IULongLong, a) -> + Tlong(Unsigned, convertAttr a) | C.TInt(ik, a) -> let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a) | C.TFloat(fk, a) -> @@ -360,14 +356,8 @@ let string_of_type ty = Format.pp_print_flush fb (); Buffer.contents b -let first_class_value env ty = - match Cutil.unroll env ty with - | C.TInt((C.ILongLong|C.IULongLong), _) -> false - | _ -> true - let supported_return_type env ty = match Cutil.unroll env ty with - | C.TInt((C.ILongLong|C.IULongLong), _) -> false | C.TStruct _ | C.TUnion _ -> false | _ -> true @@ -419,10 +409,6 @@ let convertFloat f kind = let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) -let check_assignop msg env e = - if not (first_class_value env e.etyp) then - unsupported (msg ^ " on a l-value of type " ^ string_of_type e.etyp) - let rec convertExpr env e = let ty = convertTyp env e.etyp in match e.edesc with @@ -430,13 +416,11 @@ let rec convertExpr env e = | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in - if not (first_class_value env e.etyp) then - unsupported ("r-value of type " ^ string_of_type e.etyp); Evalof(l, ty) + | C.EConst(C.CInt(i, (ILongLong|IULongLong), _)) -> + Eval(Vlong(coqint_of_camlint64 i), ty) | C.EConst(C.CInt(i, k, _)) -> - if k = C.ILongLong || k = C.IULongLong then - unsupported "'long long' integer literal"; Eval(Vint(convertInt i), ty) | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then @@ -465,21 +449,17 @@ let rec convertExpr env e = | C.EUnop(C.Oaddrof, e1) -> Eaddrof(convertLvalue env e1, ty) | C.EUnop(C.Opreincr, e1) -> - check_assignop "pre-increment" env e1; coq_Epreincr Incr (convertLvalue env e1) ty | C.EUnop(C.Opredecr, e1) -> - check_assignop "pre-decrement" env e1; coq_Epreincr Decr (convertLvalue env e1) ty | C.EUnop(C.Opostincr, e1) -> - check_assignop "post-increment" env e1; Epostincr(Incr, convertLvalue env e1, ty) | C.EUnop(C.Opostdecr, e1) -> - check_assignop "post-decrement" env e1; Epostincr(Decr, convertLvalue env e1, ty) | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor| C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op, - e1, e2, _) -> + e1, e2, tyres) -> let op' = match op with | C.Oadd -> Oadd @@ -503,7 +483,6 @@ let rec convertExpr env e = | C.EBinop(C.Oassign, e1, e2, _) -> let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in - check_assignop "assignment" env e1; Eassign(e1', e2', ty) | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| @@ -525,7 +504,6 @@ let rec convertExpr env e = | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in - check_assignop "assignment-operation" env e1; Eassignop(op', e1', e2', tyres, ty) | C.EBinop(C.Ocomma, e1, e2, _) -> Ecomma(convertExpr env e1, convertExpr env e2, ty) @@ -537,8 +515,6 @@ let rec convertExpr env e = | C.EConditional(e1, e2, e3) -> Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty) | C.ECast(ty1, e1) -> - if not (first_class_value env ty1) then - unsupported ("cast to type " ^ string_of_type ty1); Ecast(convertExpr env e1, convertTyp env ty1) | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml index 7bf80bb..5ae147e 100644 --- a/cfrontend/CPragmas.ml +++ b/cfrontend/CPragmas.ml @@ -49,8 +49,7 @@ let process_reserve_register_pragma name = C2C.error "unknown register in `reserve_register' pragma" | Some r -> if Machregsaux.can_reserve_register r then - Coloringaux.reserved_registers := - r :: !Coloringaux.reserved_registers + IRC.reserved_registers := r :: !IRC.reserved_registers else C2C.error "cannot reserve this register (not a callee-save)" diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ebc27ad..a19a0e2 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -104,6 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval := match v, t with | Vint i, AST.Tint => Some (EVint i) | Vfloat f, AST.Tfloat => Some (EVfloat f) + | Vlong n, AST.Tlong => Some (EVlong n) | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs) | _, _ => None end. @@ -122,6 +123,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := match ev, t with | EVint i, AST.Tint => Some (Vint i) | EVfloat f, AST.Tfloat => Some (Vfloat f) + | EVlong n, AST.Tlong => Some (Vlong n) | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs) | _, _ => None end. @@ -132,6 +134,7 @@ Proof. intros. destruct v; destruct t; simpl in H; inv H. constructor. constructor. + constructor. destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. constructor. apply Genv.invert_find_symbol; auto. Qed. @@ -166,6 +169,7 @@ Proof. intros. destruct ev; destruct t; simpl in H; inv H. constructor. constructor. + constructor. destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. constructor. auto. Qed. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index e9ec7cc..3bd06df 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -48,6 +48,7 @@ Require Import Cop. Inductive expr : Type := | Econst_int: int -> type -> expr (**r integer literal *) | Econst_float: float -> type -> expr (**r float literal *) + | Econst_long: int64 -> type -> expr (**r long integer literal *) | Evar: ident -> type -> expr (**r variable *) | Etempvar: ident -> type -> expr (**r temporary variable *) | Ederef: expr -> type -> expr (**r pointer dereference (unary [*]) *) @@ -68,6 +69,7 @@ Definition typeof (e: expr) : type := match e with | Econst_int _ ty => ty | Econst_float _ ty => ty + | Econst_long _ ty => ty | Evar _ ty => ty | Etempvar _ ty => ty | Ederef _ ty => ty @@ -347,6 +349,8 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Econst_int i ty) (Vint i) | eval_Econst_float: forall f ty, eval_expr (Econst_float f ty) (Vfloat f) + | eval_Econst_long: forall i ty, + eval_expr (Econst_long i ty) (Vlong i) | eval_Etempvar: forall id ty v, le!id = Some v -> eval_expr (Etempvar id ty) v diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index af85971..419ffff 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -171,6 +171,7 @@ Definition of_chunk (chunk: memory_chunk) := | Mint16signed => Int16s | Mint16unsigned => Int16u | Mint32 => Any + | Mint64 => Any | Mfloat32 => Float32 | Mfloat64 => Any | Mfloat64al32 => Any @@ -239,6 +240,8 @@ Definition transl_constant (cst: Csharpminor.constant): (constant * approx) := (Ointconst n, Approx.of_int n) | Csharpminor.Ofloatconst n => (Ofloatconst n, Approx.of_float n) + | Csharpminor.Olongconst n => + (Olongconst n, Any) end. (** Translation of expressions. Return both a Cminor expression and diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a61808a..9d3d255 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1495,6 +1495,8 @@ Ltac TrivialExists := exists (Vint x); split; [eauto with evalexpr | constructor] | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] => exists (Vfloat x); split; [eauto with evalexpr | constructor] + | [ |- exists y, _ /\ val_inject _ (Vlong ?x) _ ] => + exists (Vlong x); split; [eauto with evalexpr | constructor] | _ => idtac end. @@ -1522,6 +1524,15 @@ Proof. inv H0; simpl in H; inv H. simpl. destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H; inv H0; simpl; TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.longoffloat f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. + inv H0; simpl in H; inv H. simpl. TrivialExists. Qed. (** Compatibility of [eval_binop] with respect to [val_inject]. *) @@ -1566,46 +1577,43 @@ Proof. inv H; inv H0; inv H1; TrivialExists. inv H; inv H0; inv H1; TrivialExists. inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. + inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. + inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists. + inv H0; try discriminate; inv H1; try discriminate. simpl in *. + destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. + inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. + inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto. inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. (* cmpu *) - inv H; inv H0; inv H1; TrivialExists. - apply val_inject_val_of_optbool. - apply val_inject_val_of_optbool. - apply val_inject_val_of_optbool. -Opaque Int.add. - unfold Val.cmpu. simpl. - destruct (zeq b1 b0); subst. - (* same blocks *) - rewrite H0 in H. inv H. rewrite zeq_true. - fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)). - fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)). - fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). - fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))). - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto. - rewrite Int.translate_cmpu - by eauto using Mem.weak_valid_pointer_inject_no_overflow. - apply val_inject_val_of_optbool. - (* different source blocks *) - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto. - destruct (zeq b2 b3). - fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). - fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto). - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto). - exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |]. - destruct c; simpl; auto. - rewrite Int.eq_false. constructor. congruence. - rewrite Int.eq_false. constructor. congruence. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto. - apply val_inject_val_of_optbool. - (* cmpf *) + inv H. econstructor; split; eauto. + unfold Val.cmpu. + destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E. + replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b). + destruct b; simpl; constructor. + symmetry. eapply val_cmpu_bool_inject; eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. + simpl; auto. +(* cmpf *) + inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. +(* cmpl *) + inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. +(* cmplu *) inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. Qed. @@ -1843,6 +1851,8 @@ Proof. repeat rewrite Int.zero_ext_and; auto. omega. omega. (* int32 *) exists va; auto. + (* int64 *) + exists va; auto. (* float32 *) exploit eval_uncast_float32; eauto. intros [v' [A B]]. exists v'; split; auto. @@ -2036,6 +2046,7 @@ Proof. destruct cst; simpl; intros; inv H. exists (Vint i); intuition. apply approx_of_int_sound. exists (Vfloat f0); intuition. apply approx_of_float_sound. + exists (Vlong i); intuition. Qed. Lemma transl_expr_correct: diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index af7aaa8..c6e07b7 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -76,23 +76,35 @@ Inductive classify_cast_cases : Type := | cast_case_f2f (sz2:floatsize) (**r float -> float *) | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_l2l (**r long -> long *) + | cast_case_i2l (si1: signedness) (**r int -> long *) + | cast_case_l2i (sz2: intsize) (si2: signedness) (**r long -> int *) + | cast_case_l2f (si1: signedness) (sz2: floatsize) (**r long -> float *) + | cast_case_f2l (si2: signedness) (**r float -> long *) | cast_case_f2bool (**r float -> bool *) + | cast_case_l2bool (**r long -> bool *) | cast_case_p2bool (**r pointer -> bool *) | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) | cast_case_void (**r any -> void *) | cast_case_default. -Function classify_cast (tfrom tto: type) : classify_cast_cases := +Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool + | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tlong _ _, Tlong _ _ => cast_case_l2l + | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 + | Tint IBool _ _, Tlong _ _ => cast_case_l2bool + | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2 + | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2 + | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2 | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 | Tvoid, _ => cast_case_void @@ -131,7 +143,25 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. -Function sem_cast (v: val) (t1 t2: type) : option val := +Definition cast_int_long (si: signedness) (i: int) : int64 := + match si with + | Signed => Int64.repr (Int.signed i) + | Unsigned => Int64.repr (Int.unsigned i) + end. + +Definition cast_long_float (si : signedness) (i: int64) : float := + match si with + | Signed => Float.floatoflong i + | Unsigned => Float.floatoflongu i + end. + +Definition cast_float_long (si : signedness) (f: float) : option int64 := + match si with + | Signed => Float.longoffloat f + | Unsigned => Float.longuoffloat f + end. + +Definition sem_cast (v: val) (t1 t2: type) : option val := match classify_cast t1 t2 with | cast_case_neutral => match v with @@ -174,10 +204,53 @@ Function sem_cast (v: val) (t1 t2: type) : option val := | Vptr _ _ => Some (Vint Int.one) | _ => None end + | cast_case_l2l => + match v with + | Vlong n => Some (Vlong n) + | _ => None + end + | cast_case_i2l si => + match v with + | Vint n => Some(Vlong (cast_int_long si n)) + | _ => None + end + | cast_case_l2i sz si => + match v with + | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n)))) + | _ => None + end + | cast_case_l2bool => + match v with + | Vlong n => + Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one)) + | _ => None + end + | cast_case_l2f si1 sz2 => + match v with + | Vlong i => Some (Vfloat (cast_float_float sz2 (cast_long_float si1 i))) + | _ => None + end + | cast_case_f2l si2 => + match v with + | Vfloat f => + match cast_float_long si2 f with + | Some i => Some (Vlong i) + | None => None + end + | _ => None + end | cast_case_struct id1 fld1 id2 fld2 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + match v with + | Vptr b ofs => + if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + | _ => None + end | cast_case_union id1 fld1 id2 fld2 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + match v with + | Vptr b ofs => + if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + | _ => None + end | cast_case_void => Some v | cast_case_default => @@ -192,13 +265,15 @@ Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) | bool_case_f (**r float *) | bool_case_p (**r pointer *) + | bool_case_l (**r long *) | bool_default. Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p + | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p | Tfloat _ _ => bool_case_f + | Tlong _ _ => bool_case_l | _ => bool_default end. @@ -207,7 +282,7 @@ Definition classify_bool (ty: type) : classify_bool_cases := considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Function bool_val (v: val) (t: type) : option bool := +Definition bool_val (v: val) (t: type) : option bool := match classify_bool t with | bool_case_i => match v with @@ -225,6 +300,11 @@ Function bool_val (v: val) (t: type) : option bool := | Vptr b ofs => Some true | _ => None end + | bool_case_l => + match v with + | Vlong n => Some (negb (Int64.eq n Int64.zero)) + | _ => None + end | bool_default => None end. @@ -239,25 +319,29 @@ Proof. assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p + | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p | Tfloat _ _ => bool_case_f + | Tlong _ _ => bool_case_l | _ => bool_default end). - unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto. - + { + unfold classify_bool; destruct t; simpl; auto. destruct i; auto. + } unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i0 Int.zero); auto. + destruct (Int64.eq i Int64.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. + destruct (Int.eq i0 Int.zero); auto. Qed. (** ** Unary operators *) (** *** Boolean negation *) -Function sem_notbool (v: val) (ty: type) : option val := +Definition sem_notbool (v: val) (ty: type) : option val := match classify_bool ty with | bool_case_i => match v with @@ -275,6 +359,11 @@ Function sem_notbool (v: val) (ty: type) : option val := | Vptr _ _ => Some Vfalse | _ => None end + | bool_case_l => + match v with + | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero)) + | _ => None + end | bool_default => None end. @@ -294,6 +383,7 @@ Qed. Inductive classify_neg_cases : Type := | neg_case_i(s: signedness) (**r int *) | neg_case_f (**r float *) + | neg_case_l(s: signedness) (**r long *) | neg_default. Definition classify_neg (ty: type) : classify_neg_cases := @@ -301,10 +391,11 @@ Definition classify_neg (ty: type) : classify_neg_cases := | Tint I32 Unsigned _ => neg_case_i Unsigned | Tint _ _ _ => neg_case_i Signed | Tfloat _ _ => neg_case_f + | Tlong si _ => neg_case_l si | _ => neg_default end. -Function sem_neg (v: val) (ty: type) : option val := +Definition sem_neg (v: val) (ty: type) : option val := match classify_neg ty with | neg_case_i sg => match v with @@ -316,6 +407,11 @@ Function sem_neg (v: val) (ty: type) : option val := | Vfloat f => Some (Vfloat (Float.neg f)) | _ => None end + | neg_case_l sg => + match v with + | Vlong n => Some (Vlong (Int64.neg n)) + | _ => None + end | neg_default => None end. @@ -323,20 +419,27 @@ Function sem_neg (v: val) (ty: type) : option val := Inductive classify_notint_cases : Type := | notint_case_i(s: signedness) (**r int *) + | notint_case_l(s: signedness) (**r long *) | notint_default. Definition classify_notint (ty: type) : classify_notint_cases := match ty with | Tint I32 Unsigned _ => notint_case_i Unsigned | Tint _ _ _ => notint_case_i Signed + | Tlong si _ => notint_case_l si | _ => notint_default end. -Function sem_notint (v: val) (ty: type): option val := +Definition 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)) + | Vint n => Some (Vint (Int.not n)) + | _ => None + end + | notint_case_l sg => + match v with + | Vlong n => Some (Vlong (Int64.not n)) | _ => None end | notint_default => None @@ -351,59 +454,119 @@ Function sem_notint (v: val) (ty: type): option val := (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. +- Likewise if both arguments are of long integer type. - 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, +- If one argument has integer/long type and the other has float type, we convert the integer argument to float, then perform the float operation. +- If one argument has long integer type and the other integer type, + we convert the integer argument to long, then perform the long operation *) -(** *** Addition *) - -Inductive classify_add_cases : Type := - | add_case_ii(s: signedness) (**r int, int *) - | add_case_ff (**r float, float *) - | add_case_if(s: signedness) (**r int, float *) - | add_case_fi(s: signedness) (**r float, int *) - | add_case_pi(ty: type)(a: attr) (**r pointer, int *) - | add_case_ip(ty: type)(a: attr) (**r int, pointer *) - | add_default. - -Definition classify_add (ty1: type) (ty2: type) := +Inductive binarith_cases: Type := + | bin_case_ii(s: signedness) (**r int, int *) + | bin_case_ff (**r float, float *) + | bin_case_if(s: signedness) (**r int, float *) + | bin_case_fi(s: signedness) (**r float, int *) + | bin_case_ll(s: signedness) (**r long, long *) + | bin_case_il(s1 s2: signedness) (**r int, long *) + | bin_case_li(s1 s2: signedness) (**r long, int *) + | bin_case_lf(s: signedness) (**r long, float *) + | bin_case_fl(s: signedness) (**r float, long *) + | bin_default. + +Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => add_case_ii Signed - | Tfloat _ _, Tfloat _ _ => add_case_ff - | Tint _ sg _, Tfloat _ _ => add_case_if sg - | Tfloat _ _, Tint _ sg _ => add_case_fi sg - | Tpointer ty a, Tint _ _ _ => add_case_pi ty a - | Tint _ _ _, Tpointer ty a => add_case_ip ty a - | _, _ => add_default + | Tint I32 Unsigned _, Tint _ _ _ => bin_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => bin_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => bin_case_ii Signed + | Tfloat _ _, Tfloat _ _ => bin_case_ff + | Tint _ sg _, Tfloat _ _ => bin_case_if sg + | Tfloat _ _, Tint _ sg _ => bin_case_fi sg + | Tlong Signed _, Tlong Signed _ => bin_case_ll Signed + | Tlong _ _, Tlong _ _ => bin_case_ll Unsigned + | Tint _ s1 _, Tlong s2 _ => bin_case_il s1 s2 + | Tlong s1 _, Tint _ s2 _ => bin_case_li s1 s2 + | Tlong sg _, Tfloat _ _ => bin_case_lf sg + | Tfloat _ _, Tlong sg _ => bin_case_fl sg + | _, _ => bin_default 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 *) +Definition sem_binarith + (sem_int: signedness -> int -> int -> option val) + (sem_long: signedness -> int64 -> int64 -> option val) + (sem_float: float -> float -> option val) + (v1: val) (t1: type) (v2: val) (t2: type) : option val := + match classify_binarith t1 t2 with + | bin_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => sem_int sg n1 n2 + | _, _ => None + end + | bin_case_ff => + match v1, v2 with + | Vfloat n1, Vfloat n2 => sem_float n1 n2 + | _, _ => None + end + | bin_case_if sg => + match v1, v2 with + | Vint n1, Vfloat n2 => sem_float (cast_int_float sg n1) n2 + | _, _ => None + end + | bin_case_fi sg => + match v1, v2 with + | Vfloat n1, Vint n2 => sem_float n1 (cast_int_float sg n2) + | _, _ => None + end + | bin_case_ll sg => + match v1, v2 with + | Vlong n1, Vlong n2 => sem_long sg n1 n2 + | _, _ => None + end + | bin_case_il sg1 sg2 => match v1, v2 with - | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) + | Vint n1, Vlong n2 => sem_long sg2 (cast_int_long sg1 n1) n2 | _, _ => None end - | add_case_ff => (**r float addition *) + | bin_case_li sg1 sg2 => match v1, v2 with - | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2)) + | Vlong n1, Vint n2 => sem_long sg1 n1 (cast_int_long sg2 n2) | _, _ => None end - | add_case_if sg => (**r int plus float *) + | bin_case_lf sg => match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2)) + | Vlong n1, Vfloat n2 => sem_float (cast_long_float sg n1) n2 | _, _ => None end - | add_case_fi sg => (**r float plus int *) + | bin_case_fl sg => match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2))) + | Vfloat n1, Vlong n2 => sem_float n1 (cast_long_float sg n2) | _, _ => None end + | bin_default => None + end. + +(** *** Addition *) + +Inductive classify_add_cases : Type := + | add_case_pi(ty: type)(a: attr) (**r pointer, int *) + | add_case_ip(ty: type)(a: attr) (**r int, pointer *) + | add_case_pl(ty: type)(a: attr) (**r pointer, long *) + | add_case_lp(ty: type)(a: attr) (**r long, pointer *) + | add_default. (**r numerical type, numerical type *) + +Definition classify_add (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tpointer ty a, Tint _ _ _ => add_case_pi ty a + | Tint _ _ _, Tpointer ty a => add_case_ip ty a + | Tpointer ty a, Tlong _ _ => add_case_pl ty a + | Tlong _ _, Tpointer ty a => add_case_lp ty a + | _, _ => add_default + end. + +Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_add t1 t2 with | add_case_pi ty _ => (**r pointer plus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => @@ -416,59 +579,57 @@ Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) | _, _ => None end - | add_default => None -end. + | add_case_pl ty _ => (**r pointer plus long *) + match v1,v2 with + | Vptr b1 ofs1, Vlong n2 => + let n2 := Int.repr (Int64.unsigned n2) in + Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | _, _ => None + end + | add_case_lp ty _ => (**r long plus pointer *) + match v1,v2 with + | Vlong n1, Vptr b2 ofs2 => + let n1 := Int.repr (Int64.unsigned n1) in + Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) + | _, _ => None + end + | add_default => + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.add n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2))) + (fun n1 n2 => Some(Vfloat(Float.add n1 n2))) + v1 t1 v2 t2 + end. (** *** Subtraction *) Inductive classify_sub_cases : Type := - | sub_case_ii(s: signedness) (**r int , int *) - | sub_case_ff (**r float , float *) - | sub_case_if(s: signedness) (**r int, float *) - | sub_case_fi(s: signedness) (**r float, int *) - | sub_case_pi(ty: type) (**r pointer, int *) + | sub_case_pi(ty: type)(a: attr) (**r pointer, int *) | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_default. + | sub_case_pl(ty: type)(a: attr) (**r pointer, long *) + | sub_default. (**r numerical type, numerical type *) Definition classify_sub (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => sub_case_ff - | Tint _ sg _, Tfloat _ _ => sub_case_if sg - | Tfloat _ _, Tint _ sg _ => sub_case_fi sg - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty + | Tpointer ty a, Tint _ _ _ => sub_case_pi ty a | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty - | _ ,_ => sub_default + | Tpointer ty a, Tlong _ _ => sub_case_pl ty a + | _, _ => sub_default end. -Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition 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 *) + | sub_case_pi ty attr => (**r pointer minus integer *) match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2)) + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) | _, _ => 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 *) + | sub_case_pl ty attr => (**r pointer minus long *) match v1,v2 with - | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | Vptr b1 ofs1, Vlong n2 => + let n2 := Int.repr (Int64.unsigned n2) in + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) | _, _ => None end | sub_case_pp ty => (**r pointer minus pointer *) @@ -480,255 +641,187 @@ Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := else None | _, _ => None end - | sub_default => None + | sub_default => + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.sub n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2))) + (fun n1 n2 => Some(Vfloat(Float.sub n1 n2))) + v1 t1 v2 t2 end. -(** *** Multiplication *) - -Inductive classify_mul_cases : Type:= - | mul_case_ii(s: signedness) (**r int , int *) - | mul_case_ff (**r float , float *) - | mul_case_if(s: signedness) (**r int, float *) - | mul_case_fi(s: signedness) (**r float, int *) - | mul_default. - -Definition classify_mul (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => mul_case_ff - | Tint _ sg _, Tfloat _ _ => mul_case_if sg - | Tfloat _ _, Tint _ sg _ => mul_case_fi sg - | _,_ => mul_default -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. - -(** *** Division *) - -Inductive classify_div_cases : Type:= - | div_case_ii(s: signedness) (**r int , int *) - | div_case_ff (**r float , float *) - | div_case_if(s: signedness) (**r int, float *) - | div_case_fi(s: signedness) (**r float, int *) - | div_default. - -Definition classify_div (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => div_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => div_case_ff - | Tint _ sg _, Tfloat _ _ => div_case_if sg - | Tfloat _ _, Tint _ sg _ => div_case_fi sg - | _,_ => div_default -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 => +(** *** Multiplication, division, modulus *) + +Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.mul n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2))) + (fun n1 n2 => Some(Vfloat(Float.mul n1 n2))) + v1 t1 v2 t2. + +Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => + match sg with + | Signed => 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. - -(** *** Integer-only binary operations: modulus, bitwise "and", "or", and "xor" *) - -Inductive classify_binint_cases : Type:= - | binint_case_ii(s: signedness) (**r int , int *) - | binint_default. - -Definition classify_binint (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed - | _,_ => binint_default -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 => + then None else Some(Vint(Int.divs n1 n2)) + | Unsigned => + if Int.eq n2 Int.zero + then None else Some(Vint(Int.divu n1 n2)) + end) + (fun sg n1 n2 => + match sg with + | Signed => + if Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone + then None else Some(Vlong(Int64.divs n1 n2)) + | Unsigned => + if Int64.eq n2 Int64.zero + then None else Some(Vlong(Int64.divu n1 n2)) + end) + (fun n1 n2 => Some(Vfloat(Float.div n1 n2))) + v1 t1 v2 t2. + +Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => + match sg with + | Signed => 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. + then None else Some(Vint(Int.mods n1 n2)) + | Unsigned => + if Int.eq n2 Int.zero + then None else Some(Vint(Int.modu n1 n2)) + end) + (fun sg n1 n2 => + match sg with + | Signed => + if Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone + then None else Some(Vlong(Int64.mods n1 n2)) + | Unsigned => + if Int64.eq n2 Int64.zero + then None else Some(Vlong(Int64.modu n1 n2)) + end) + (fun n1 n2 => None) + v1 t1 v2 t2. + +Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.and n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. + +Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.or n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. + +Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_binarith + (fun sg n1 n2 => Some(Vint(Int.xor n1 n2))) + (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2))) + (fun n1 n2 => None) + v1 t1 v2 t2. (** *** Shifts *) +(** Shifts do not perform the usual binary conversions. Instead, + each argument is converted independently, and the signedness + of the result is always that of the first argument. *) + Inductive classify_shift_cases : Type:= - | shift_case_ii(s: signedness) (**r int , int *) + | shift_case_ii(s: signedness) (**r int , int *) + | shift_case_ll(s: signedness) (**r long, long *) + | shift_case_il(s: signedness) (**r int, long *) + | shift_case_li(s: signedness) (**r long, int *) | shift_default. Definition classify_shift (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed + | Tint I32 Unsigned _, Tlong _ _ => shift_case_il Unsigned + | Tint _ _ _, Tlong _ _ => shift_case_il Signed + | Tlong s _, Tint _ _ _ => shift_case_li s + | Tlong s _, Tlong _ _ => shift_case_ll s | _,_ => shift_default -end. + end. -Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_shift + (sem_int: signedness -> int -> int -> int) + (sem_long: signedness -> int64 -> int64 -> int64) + (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 + | Vint n1, Vint n2 => + if Int.ltu n2 Int.iwordsize + then Some(Vint(sem_int sg n1 n2)) else None + | _, _ => None + end + | shift_case_il sg => + match v1, v2 with + | Vint n1, Vlong n2 => + if Int64.ltu n2 (Int64.repr 32) + then Some(Vint(sem_int sg n1 (Int64.loword n2))) else None + | _, _ => None + end + | shift_case_li sg => + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 Int64.iwordsize' + then Some(Vlong(sem_long sg n1 (Int64.repr (Int.unsigned n2)))) else None + | _, _ => None + end + | shift_case_ll sg => + match v1, v2 with + | Vlong n1, Vlong n2 => + if Int64.ltu n2 Int64.iwordsize + then Some(Vlong(sem_long sg 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. +Definition sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_shift + (fun sg n1 n2 => Int.shl n1 n2) + (fun sg n1 n2 => Int64.shl n1 n2) + v1 t1 v2 t2. + +Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val := + sem_shift + (fun sg n1 n2 => match sg with Signed => Int.shr n1 n2 | Unsigned => Int.shru n1 n2 end) + (fun sg n1 n2 => match sg with Signed => Int64.shr n1 n2 | Unsigned => Int64.shru n1 n2 end) + v1 t1 v2 t2. (** *** Comparisons *) -Inductive classify_cmp_cases : Type:= - | cmp_case_ii(s: signedness) (**r int, int *) - | cmp_case_pp (**r pointer, pointer *) - | cmp_case_ff (**r float , float *) - | cmp_case_if(s: signedness) (**r int, float *) - | cmp_case_fi(s: signedness) (**r float, int *) - | cmp_default. +Inductive classify_cmp_cases : Type := + | cmp_case_pp (**r pointer, pointer *) + | cmp_default. (**r numerical, numerical *) Definition classify_cmp (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => cmp_case_ff - | Tint _ sg _, Tfloat _ _ => cmp_case_if sg - | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg | Tpointer _ _ , Tpointer _ _ => cmp_case_pp | Tpointer _ _ , Tint _ _ _ => cmp_case_pp | Tint _ _ _, Tpointer _ _ => cmp_case_pp - | _ , _ => cmp_default + | _, _ => cmp_default end. -Function sem_cmp (c:comparison) +Definition 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 => + option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) +(* match v1,v2 with | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) | Vptr b1 ofs1, Vptr b2 ofs2 => @@ -752,22 +845,16 @@ Function sem_cmp (c:comparison) 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 +*) + | cmp_default => + sem_binarith + (fun sg n1 n2 => + Some(Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end))) + (fun sg n1 n2 => + Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end))) + (fun n1 n2 => + Some(Val.of_bool(Float.cmp c n1 n2))) + v1 t1 v2 t2 end. (** ** Function applications *) @@ -821,3 +908,249 @@ Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) := | Incr => sem_add v ty (Vint Int.one) type_int32s | Decr => sem_sub v ty (Vint Int.one) type_int32s end. + +(** * Compatibility with extensions and injections *) + +Section GENERIC_INJECTION. + +Variable f: meminj. +Variables m m': mem. + +Hypothesis valid_pointer_inj: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.valid_pointer m b1 (Int.unsigned ofs) = true -> + Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + +Hypothesis weak_valid_pointer_inj: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true -> + Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + +Hypothesis weak_valid_pointer_no_overflow: + forall b1 ofs b2 delta, + f b1 = Some(b2, delta) -> + Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true -> + 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + +Hypothesis valid_different_pointers_inj: + forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, + b1 <> b2 -> + Mem.valid_pointer m b1 (Int.unsigned ofs1) = true -> + Mem.valid_pointer m b2 (Int.unsigned ofs2) = true -> + f b1 = Some (b1', delta1) -> + f b2 = Some (b2', delta2) -> + b1' <> b2' \/ + Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + +Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. +Proof. unfold Vtrue; auto. Qed. + +Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. +Proof. unfold Vfalse; auto. Qed. + +Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. +Qed. + +Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. + +Ltac TrivialInject := + match goal with + | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto + | _ => idtac + end. + +Lemma sem_unary_operation_inject: + forall op v1 ty v tv1, + sem_unary_operation op v1 ty = Some v -> + val_inject f v1 tv1 -> + exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. +Proof. + unfold sem_unary_operation; intros. destruct op. + (* notbool *) + unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. + (* notint *) + unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. + (* neg *) + unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. +Qed. + +Definition optval_self_injects (ov: option val) : Prop := + match ov with + | Some (Vptr b ofs) => False + | _ => True + end. + +Remark sem_binarith_inject: + forall sem_int sem_long sem_float v1 t1 v2 t2 v v1' v2', + sem_binarith sem_int sem_long sem_float v1 t1 v2 t2 = Some v -> + val_inject f v1 v1' -> val_inject f v2 v2' -> + (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> + (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> + (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> + exists v', sem_binarith sem_int sem_long sem_float v1' t1 v2' t2 = Some v' /\ val_inject f v v'. +Proof. + intros. + assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v). + { + intros. subst ov; simpl in H6. destruct v0; contradiction || constructor. + } + exists v. + unfold sem_binarith in *; destruct (classify_binarith t1 t2); inv H0; inv H1; discriminate || eauto. +Qed. + +Remark sem_shift_inject: + forall sem_int sem_long v1 t1 v2 t2 v v1' v2', + sem_shift sem_int sem_long v1 t1 v2 t2 = Some v -> + val_inject f v1 v1' -> val_inject f v2 v2' -> + exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'. +Proof. + intros. exists v. + unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate. + destruct (Int.ltu i0 Int.iwordsize); inv H; auto. + destruct (Int64.ltu i0 Int64.iwordsize); inv H; auto. + destruct (Int64.ltu i0 (Int64.repr 32)); inv H; auto. + destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto. +Qed. + +Remark sem_cmp_inj: + forall cmp v1 tv1 ty1 v2 tv2 ty2 v, + sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> + val_inject f v1 tv1 -> + val_inject f v2 tv2 -> + exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. +Proof. + intros. + unfold sem_cmp in *; destruct (classify_cmp ty1 ty2). +- (* pointer - pointer *) + destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H. + replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b). + simpl. TrivialInject. + symmetry. eapply val_cmpu_bool_inject; eauto. +- (* numerical - numerical *) + assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))). + { + destruct b; exact I. + } + eapply sem_binarith_inject; eauto. +Qed. + +Lemma sem_binary_operation_inj: + forall op v1 ty1 v2 ty2 v tv1 tv2, + sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> + val_inject f v1 tv1 -> val_inject f v2 tv2 -> + exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. +Proof. + unfold sem_binary_operation; intros; destruct op. +- (* add *) + unfold sem_add in *; destruct (classify_add ty1 ty2). + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + + eapply sem_binarith_inject; eauto; intros; exact I. +- (* sub *) + unfold sem_sub in *; destruct (classify_sub ty1 ty2). + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. rewrite Int.sub_add_l. auto. + + inv H0; inv H1; inv H. TrivialInject. + destruct (zeq b1 b0); try discriminate. subst b1. + rewrite H0 in H2; inv H2. rewrite zeq_true. + destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. + rewrite Int.sub_shifted. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. + econstructor. eauto. rewrite Int.sub_add_l. auto. + + eapply sem_binarith_inject; eauto; intros; exact I. +- (* mul *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* div *) + eapply sem_binarith_inject; eauto; intros. + destruct sg. + destruct (Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I. + destruct (Int.eq n2 Int.zero); exact I. + destruct sg. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. + destruct (Int64.eq n2 Int64.zero); exact I. + exact I. +- (* mod *) + eapply sem_binarith_inject; eauto; intros. + destruct sg. + destruct (Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I. + destruct (Int.eq n2 Int.zero); exact I. + destruct sg. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I. + destruct (Int64.eq n2 Int64.zero); exact I. + exact I. +- (* and *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* or *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* xor *) + eapply sem_binarith_inject; eauto; intros; exact I. +- (* shl *) + eapply sem_shift_inject; eauto. +- (* shr *) + eapply sem_shift_inject; eauto. + (* comparisons *) +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +- eapply sem_cmp_inj; eauto. +Qed. + +Lemma sem_cast_inject: + forall v1 ty1 ty v tv1, + sem_cast v1 ty1 ty = Some v -> + val_inject f v1 tv1 -> + exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. +Proof. + unfold sem_cast; intros; destruct (classify_cast ty1 ty); + inv H0; inv H; TrivialInject. +- econstructor; eauto. +- destruct (cast_float_int si2 f0); inv H1; TrivialInject. +- destruct (cast_float_long si2 f0); inv H1; TrivialInject. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- econstructor; eauto. +Qed. + +Lemma bool_val_inject: + forall v ty b tv, + bool_val v ty = Some b -> + val_inject f v tv -> + bool_val tv ty = Some b. +Proof. + unfold bool_val; intros. + destruct (classify_bool ty); inv H0; congruence. +Qed. + +End GENERIC_INJECTION. + +Lemma sem_binary_operation_inject: + forall f m m' op v1 ty1 v2 ty2 v tv1 tv2, + sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> + val_inject f v1 tv1 -> val_inject f v2 tv2 -> + Mem.inject f m m' -> + exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. +Proof. + intros. eapply sem_binary_operation_inj; eauto. + intros; eapply Mem.valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. + intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. + intros; eapply Mem.different_pointers_inject; eauto. +Qed. + + + diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index d0bd9f4..718daa1 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -33,7 +33,8 @@ Require Import Smallstep. Inductive constant : Type := | Ointconst: int -> constant (**r integer constant *) - | Ofloatconst: float -> constant. (**r floating-point constant *) + | Ofloatconst: float -> constant (**r floating-point constant *) + | Olongconst: int64 -> constant. (**r long integer constant *) Definition unary_operation : Type := Cminor.unary_operation. Definition binary_operation : Type := Cminor.binary_operation. @@ -238,6 +239,7 @@ Definition eval_constant (cst: constant) : option val := match cst with | Ointconst n => Some (Vint n) | Ofloatconst n => Some (Vfloat n) + | Olongconst n => Some (Vlong n) end. Definition eval_unop := Cminor.eval_unop. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 51f89da..2a27852 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -44,7 +44,7 @@ Open Local Scope error_monad_scope. - The C types of the arguments of the operation. These types are used to insert the necessary numeric conversions and to resolve operation overloading. - Most of these functions return an [option expr], with [None] + Most of these functions return a [res expr], with [Error] denoting a case where the operation is not defined at the given types. *) @@ -52,6 +52,8 @@ Definition make_intconst (n: int) := Econst (Ointconst n). Definition make_floatconst (f: float) := Econst (Ofloatconst f). +Definition make_longconst (f: int64) := Econst (Olongconst f). + Definition make_floatofint (e: expr) (sg: signedness) := match sg with | Signed => Eunop Ofloatofint e @@ -64,6 +66,24 @@ Definition make_intoffloat (e: expr) (sg: signedness) := | Unsigned => Eunop Ointuoffloat e end. +Definition make_longofint (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Olongofint e + | Unsigned => Eunop Olongofintu e + end. + +Definition make_floatoflong (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Ofloatoflong e + | Unsigned => Eunop Ofloatoflongu e + end. + +Definition make_longoffloat (e: expr) (sg: signedness) := + match sg with + | Signed => Eunop Olongoffloat e + | Unsigned => Eunop Olonguoffloat e + end. + (** [make_boolean e ty] returns a Csharpminor expression that evaluates to the boolean value of [e]. *) @@ -80,6 +100,7 @@ Definition make_boolean (e: expr) (ty: type) := | bool_case_i => make_cmp_ne_zero e | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero) + | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero) | bool_default => e (**r should not happen *) end. @@ -88,6 +109,7 @@ Definition make_notbool (e: expr) (ty: type) := | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero)) | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero)) | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero)) + | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero)) | _ => Error (msg "Cshmgen.make_notbool") end. @@ -95,96 +117,144 @@ Definition make_neg (e: expr) (ty: type) := match classify_neg ty with | neg_case_i _ => OK (Eunop Onegint e) | neg_case_f => OK (Eunop Onegf e) + | neg_case_l _ => OK (Eunop Onegl e) | _ => Error (msg "Cshmgen.make_neg") end. Definition make_notint (e: expr) (ty: type) := - Eunop Onotint e. + match classify_notint ty with + | notint_case_i _ => OK (Eunop Onotint e) + | notint_case_l _ => OK (Eunop Onotl e) + | _ => Error (msg "Cshmgen.make_notint") + end. + +Definition make_binarith (iop iopu fop lop lopu: binary_operation) + (e1: expr) (ty1: type) (e2: expr) (ty2: type) := + match classify_binarith ty1 ty2 with + | bin_case_ii Signed => OK (Ebinop iop e1 e2) + | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2) + | bin_case_ff => OK (Ebinop fop e1 e2) + | bin_case_if sg => OK (Ebinop fop (make_floatofint e1 sg) e2) + | bin_case_fi sg => OK (Ebinop fop e1 (make_floatofint e2 sg)) + | bin_case_ll Signed => OK (Ebinop lop e1 e2) + | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2) + | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2) + | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2) + | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2)) + | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2)) + | bin_case_lf sg => OK (Ebinop fop (make_floatoflong e1 sg) e2) + | bin_case_fl sg => OK (Ebinop fop e1 (make_floatoflong e2 sg)) + | bin_default => Error (msg "Cshmgen.make_binarith") + end. Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_ii _ => OK (Ebinop Oadd e1 e2) - | add_case_ff => OK (Ebinop Oaddf e1 e2) - | add_case_if sg => OK (Ebinop Oaddf (make_floatofint e1 sg) e2) - | add_case_fi sg => OK (Ebinop Oaddf e1 (make_floatofint e2 sg)) | add_case_pi ty _ => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_ip ty _ => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) - | add_default => Error (msg "Cshmgen.make_add") + | add_case_pl ty _ => + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) + | add_case_lp ty _ => + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) + | add_default => + make_binarith Oadd Oadd Oaddf Oaddl Oaddl e1 ty1 e2 ty2 end. Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with - | sub_case_ii _ => OK (Ebinop Osub e1 e2) - | sub_case_ff => OK (Ebinop Osubf e1 e2) - | sub_case_if sg => OK (Ebinop Osubf (make_floatofint e1 sg) e2) - | sub_case_fi sg => OK (Ebinop Osubf e1 (make_floatofint e2 sg)) - | sub_case_pi ty => + | sub_case_pi ty _ => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Odivu (Ebinop Osub e1 e2) n) - | sub_default => Error (msg "Cshmgen.make_sub") + | sub_case_pl ty _ => + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) + | sub_default => + make_binarith Osub Osub Osubf Osubl Osubl e1 ty1 e2 ty2 end. Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_mul ty1 ty2 with - | mul_case_ii _ => OK (Ebinop Omul e1 e2) - | mul_case_ff => OK (Ebinop Omulf e1 e2) - | mul_case_if sg => OK (Ebinop Omulf (make_floatofint e1 sg) e2) - | mul_case_fi sg => OK (Ebinop Omulf e1 (make_floatofint e2 sg)) - | mul_default => Error (msg "Cshmgen.make_mul") - end. + make_binarith Omul Omul Omulf Omull Omull e1 ty1 e2 ty2. Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_div ty1 ty2 with - | div_case_ii Unsigned => OK (Ebinop Odivu e1 e2) - | div_case_ii Signed => OK (Ebinop Odiv e1 e2) - | div_case_ff => OK (Ebinop Odivf e1 e2) - | div_case_if sg => OK (Ebinop Odivf (make_floatofint e1 sg) e2) - | div_case_fi sg => OK (Ebinop Odivf e1 (make_floatofint e2 sg)) - | div_default => Error (msg "Cshmgen.make_div") + make_binarith Odiv Odivu Odivf Odivl Odivlu e1 ty1 e2 ty2. + +Definition make_binarith_int (iop iopu lop lopu: binary_operation) + (e1: expr) (ty1: type) (e2: expr) (ty2: type) := + match classify_binarith ty1 ty2 with + | bin_case_ii Signed => OK (Ebinop iop e1 e2) + | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2) + | bin_case_ll Signed => OK (Ebinop lop e1 e2) + | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2) + | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2) + | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2) + | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2)) + | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2)) + | _ => Error (msg "Cshmgen.make_binarith_int") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - match classify_binint ty1 ty2 with - | binint_case_ii Unsigned => OK (Ebinop Omodu e1 e2) - | binint_case_ii Signed => OK (Ebinop Omod e1 e2) - | mod_default => Error (msg "Cshmgen.make_mod") - end. + make_binarith_int Omod Omodu Omodl Omodlu e1 ty1 e2 ty2. Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - OK(Ebinop Oand e1 e2). + make_binarith_int Oand Oand Oandl Oandl e1 ty1 e2 ty2. Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - OK(Ebinop Oor e1 e2). + make_binarith_int Oor Oor Oorl Oorl e1 ty1 e2 ty2. Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - OK(Ebinop Oxor e1 e2). + make_binarith_int Oxor Oxor Oxorl Oxorl e1 ty1 e2 ty2. + +(* +Definition make_shift (iop iopu lop lopu: binary_operation) + (e1: expr) (ty1: type) (e2: expr) (ty2: type) := + match classify_shift ty1 ty2 with + | shift_case_ii Signed => OK (Ebinop iop e1 e2) + | shift_case_ii Unsigned => OK (Ebinop iopu e1 e2) + | shift_case_li Signed => OK (Ebinop lop e1 e2) + | shift_case_li Unsigned => OK (Ebinop lopu e1 e2) + | shift_case_il Signed => OK (Ebinop iop e1 (Eunop Ointoflong e2)) + | shift_case_il Unsigned => OK (Ebinop iopu e1 (Eunop Ointoflong e2)) + | shift_case_ll Signed => OK (Ebinop lop e1 (Eunop Ointoflong e2)) + | shift_case_ll Unsigned => OK (Ebinop lopu e1 (Eunop Ointoflong e2)) + | shift_default => Error (msg "Cshmgen.make_shift") + end. +*) Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - OK(Ebinop Oshl e1 e2). + match classify_shift ty1 ty2 with + | shift_case_ii _ => OK (Ebinop Oshl e1 e2) + | shift_case_li _ => OK (Ebinop Oshll e1 e2) + | shift_case_il _ => OK (Ebinop Oshl e1 (Eunop Ointoflong e2)) + | shift_case_ll _ => OK (Ebinop Oshll e1 (Eunop Ointoflong e2)) + | shift_default => Error (msg "Cshmgen.make_shl") + end. Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_shift ty1 ty2 with - | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2) | shift_case_ii Signed => OK (Ebinop Oshr e1 e2) - | shr_default => Error (msg "Cshmgen.make_shr") + | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2) + | shift_case_li Signed => OK (Ebinop Oshrl e1 e2) + | shift_case_li Unsigned => OK (Ebinop Oshrlu e1 e2) + | shift_case_il Signed => OK (Ebinop Oshr e1 (Eunop Ointoflong e2)) + | shift_case_il Unsigned => OK (Ebinop Oshru e1 (Eunop Ointoflong e2)) + | shift_case_ll Signed => OK (Ebinop Oshrl e1 (Eunop Ointoflong e2)) + | shift_case_ll Unsigned => OK (Ebinop Oshrlu e1 (Eunop Ointoflong e2)) + | shift_default => Error (msg "Cshmgen.make_shr") end. Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with - | cmp_case_ii Signed => OK (Ebinop (Ocmp c) e1 e2) - | cmp_case_ii Unsigned => OK (Ebinop (Ocmpu c) e1 e2) | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2) - | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2) - | cmp_case_if sg => OK (Ebinop (Ocmpf c) (make_floatofint e1 sg) e2) - | cmp_case_fi sg => OK (Ebinop (Ocmpf c) e1 (make_floatofint e2 sg)) - | cmp_default => Error (msg "Cshmgen.make_cmp") + | cmp_default => + make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2 end. (** [make_cast from to e] applies to [e] the numeric conversions needed @@ -208,17 +278,23 @@ Definition make_cast_float (e: expr) (sz: floatsize) := Definition make_cast (from to: type) (e: expr) := match classify_cast from to with - | cast_case_neutral => e - | cast_case_i2i sz2 si2 => make_cast_int e sz2 si2 - | cast_case_f2f sz2 => make_cast_float e sz2 - | cast_case_i2f si1 sz2 => make_cast_float (make_floatofint e si1) sz2 - | cast_case_f2i sz2 si2 => make_cast_int (make_intoffloat e si2) sz2 si2 - | cast_case_f2bool => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) - | cast_case_p2bool => Ebinop (Ocmpu Cne) e (make_intconst Int.zero) - | cast_case_struct id1 fld1 id2 fld2 => e - | cast_case_union id1 fld1 id2 fld2 => e - | cast_case_void => e - | cast_case_default => e + | cast_case_neutral => OK e + | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2) + | cast_case_f2f sz2 => OK (make_cast_float e sz2) + | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2) + | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2) + | cast_case_l2l => OK e + | cast_case_i2l si1 => OK (make_longofint e si1) + | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2) + | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2) + | cast_case_f2l si2 => OK (make_longoffloat e si2) + | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)) + | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) + | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) + | cast_case_struct id1 fld1 id2 fld2 => OK e + | cast_case_union id1 fld1 id2 fld2 => OK e + | cast_case_void => OK e + | cast_case_default => Error (msg "Cshmgen.make_cast") end. (** [make_load addr ty_res] loads a value of type [ty_res] from @@ -259,7 +335,7 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr := match op with | Cop.Onotbool => make_notbool a ta - | Cop.Onotint => OK(make_notint a ta) + | Cop.Onotint => make_notint a ta | Cop.Oneg => make_neg a ta end. @@ -297,6 +373,8 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := OK(make_intconst n) | Clight.Econst_float n _ => OK(make_floatconst n) + | Clight.Econst_long n _ => + OK(make_longconst n) | Clight.Evar id ty => make_load (Eaddrof id) ty | Clight.Etempvar id ty => @@ -315,7 +393,7 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := transl_binop op tb (typeof b) tc (typeof c) | Clight.Ecast b ty => do tb <- transl_expr b; - OK (make_cast (typeof b) ty tb) + make_cast (typeof b) ty tb | Clight.Efield b i ty => match typeof b with | Tstruct _ fld _ => @@ -369,8 +447,9 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist) | nil, Tnil => OK nil | a1 :: a2, Tcons ty1 ty2 => do ta1 <- transl_expr a1; - do ta2 <- transl_arglist a2 ty2; - OK (make_cast (typeof a1) ty1 ta1 :: ta2) + do ta1' <- make_cast (typeof a1) ty1 ta1; + do ta2 <- transl_arglist a2 ty2; + OK (ta1' :: ta2) | _, _ => Error(msg "Cshmgen.transl_arglist: arity mismatch") end. @@ -408,7 +487,8 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) | Clight.Sassign b c => do tb <- transl_lvalue b; do tc <- transl_expr c; - make_store tb (typeof b) (make_cast (typeof c) (typeof b) tc) + do tc' <- make_cast (typeof c) (typeof b) tc; + make_store tb (typeof b) tc' | Clight.Sset x b => do tb <- transl_expr b; OK(Sset x tb) @@ -442,7 +522,8 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) OK (Sexit ncnt) | Clight.Sreturn (Some e) => do te <- transl_expr e; - OK (Sreturn (Some (make_cast (typeof e) tyret te))) + do te' <- make_cast (typeof e) tyret te; + OK (Sreturn (Some te')) | Clight.Sreturn None => OK (Sreturn None) | Clight.Sswitch a sl => @@ -486,9 +567,6 @@ Definition transl_function (f: Clight.function) : res function := (map fst (Clight.fn_temps f)) tbody). -Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} - := list_eq_dec typ_eq. - Definition transl_fundef (f: Clight.fundef) : res fundef := match f with | Clight.Internal g => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index ad5ada6..7c24d0d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -67,157 +67,10 @@ Proof. rewrite H0; reflexivity. Qed. -(* -Lemma var_kind_by_value: - forall ty chunk, - access_mode ty = By_value chunk -> - var_kind_of_type ty = OK(Vscalar chunk). -Proof. - intros ty chunk; destruct ty; simpl; try congruence. - destruct i; try congruence; destruct s; congruence. - destruct f; congruence. -Qed. - -Lemma var_kind_by_reference: - forall ty vk, - access_mode ty = By_reference \/ access_mode ty = By_copy -> - var_kind_of_type ty = OK vk -> - vk = Varray (Ctypes.sizeof ty) (Ctypes.alignof ty). -Proof. - intros ty vk; destruct ty; simpl; try intuition congruence. - destruct i; try congruence; destruct s; intuition congruence. - destruct f; intuition congruence. -Qed. - -Lemma sizeof_var_kind_of_type: - forall ty vk, - var_kind_of_type ty = OK vk -> - Csharpminor.sizeof vk = Ctypes.sizeof ty. -Proof. - intros ty vk. - assert (sizeof (Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) = Ctypes.sizeof ty). - simpl. rewrite Zmax_spec. apply zlt_false. - generalize (Ctypes.sizeof_pos ty). omega. - destruct ty; try (destruct i; try destruct s); try (destruct f); - simpl; intro EQ; inversion EQ; subst vk; auto. -Qed. -*) -(**** -Remark cast_int_int_normalized: - forall sz si a chunk n, - access_mode (Tint sz si a) = By_value chunk -> - val_normalized (Vint (cast_int_int sz si n)) chunk. -Proof. - unfold access_mode, cast_int_int, val_normalized; intros. destruct sz. - destruct si; inv H; simpl. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - destruct si; inv H; simpl. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - inv H. auto. - inv H. destruct (Int.eq n Int.zero); auto. -Qed. - -Remark cast_float_float_normalized: - forall sz a chunk n, - access_mode (Tfloat sz a) = By_value chunk -> - val_normalized (Vfloat (cast_float_float sz n)) chunk. -Proof. - unfold access_mode, cast_float_float, val_normalized; intros. - destruct sz; inv H; simpl. - rewrite Float.singleoffloat_idem. auto. - auto. -Qed. - -Remark cast_neutral_normalized: - forall ty1 ty2 chunk, - classify_cast ty1 ty2 = cast_case_neutral -> - access_mode ty2 = By_value chunk -> - chunk = Mint32. -Proof. - intros. functional inversion H; subst; simpl in H0; congruence. -Qed. - -Remark cast_to_bool_normalized: - forall ty1 ty2 chunk, - classify_cast ty1 ty2 = cast_case_f2bool \/ - classify_cast ty1 ty2 = cast_case_p2bool -> - access_mode ty2 = By_value chunk -> - chunk = Mint8unsigned. -Proof. - intros. destruct ty2; simpl in *; try discriminate. - destruct i; destruct ty1; intuition congruence. - destruct ty1; intuition discriminate. - destruct ty1; intuition discriminate. -Qed. - -Lemma cast_result_normalized: - forall chunk v1 ty1 ty2 v2, - sem_cast v1 ty1 ty2 = Some v2 -> - access_mode ty2 = By_value chunk -> - val_normalized v2 chunk. -Proof. - intros. functional inversion H; subst. - rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto. - rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto. - functional inversion H2; subst. eapply cast_int_int_normalized; eauto. - functional inversion H2; subst. eapply cast_float_float_normalized; eauto. - functional inversion H2; subst. eapply cast_float_float_normalized; eauto. - functional inversion H2; subst. eapply cast_int_int_normalized; eauto. - rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto. - rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto. - rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. destruct (Int.eq i Int.zero); red; auto. - rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto. - functional inversion H2; subst. simpl in H0. congruence. - functional inversion H2; subst. simpl in H0. congruence. - functional inversion H5; subst. simpl in H0. congruence. -Qed. - -Definition val_casted (v: val) (ty: type) : Prop := - exists v0, exists ty0, sem_cast v0 ty0 ty = Some v. - -Lemma val_casted_normalized: - forall v ty chunk, - val_casted v ty -> access_mode ty = By_value chunk -> val_normalized v chunk. -Proof. - intros. destruct H as [v0 [ty0 CAST]]. eapply cast_result_normalized; eauto. -Qed. - -Fixpoint val_casted_list (vl: list val) (tyl: typelist) {struct vl}: Prop := - match vl, tyl with - | nil, Tnil => True - | v1 :: vl', Tcons ty1 tyl' => val_casted v1 ty1 /\ val_casted_list vl' tyl' - | _, _ => False - end. - -Lemma eval_exprlist_casted: - forall ge e le m al tyl vl, - Clight.eval_exprlist ge e le m al tyl vl -> - val_casted_list vl tyl. -Proof. - induction 1; simpl. - auto. - split. exists v1; exists (typeof a); auto. eauto. -Qed. - -*******) - (** * Properties of the translation functions *) (** Transformation of expressions and statements. *) -(* -Lemma is_variable_correct: - forall a id, - is_variable a = Some id -> - a = Clight.Evar id (typeof a). -Proof. - intros until id. unfold is_variable; destruct a; intros; try discriminate. - simpl. congruence. -Qed. -*) - Lemma transl_expr_lvalue: forall ge e le m a loc ofs ta, Clight.eval_lvalue ge e le m a loc ofs -> @@ -283,6 +136,13 @@ Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. +Lemma make_longconst_correct: + forall n e le m, + eval_expr ge e le m (make_longconst n) (Vlong n). +Proof. + intros. unfold make_floatconst. econstructor. reflexivity. +Qed. + Lemma make_floatofint_correct: forall a n sg e le m, eval_expr ge e le m a (Vint n) -> @@ -302,8 +162,38 @@ Proof. destruct sg; econstructor; eauto; simpl; rewrite H0; auto. Qed. -Hint Resolve make_intconst_correct make_floatconst_correct +Lemma make_longofint_correct: + forall a n sg e le m, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_longofint a sg) (Vlong(cast_int_long sg n)). +Proof. + intros. unfold make_longofint, cast_int_long. + destruct sg; econstructor; eauto. +Qed. + +Lemma make_floatoflong_correct: + forall a n sg e le m, + eval_expr ge e le m a (Vlong n) -> + eval_expr ge e le m (make_floatoflong a sg) (Vfloat(cast_long_float sg n)). +Proof. + intros. unfold make_floatoflong, cast_int_long. + destruct sg; econstructor; eauto. +Qed. + +Lemma make_longoffloat_correct: + forall e le m a sg f i, + eval_expr ge e le m a (Vfloat f) -> + cast_float_long sg f = Some i -> + eval_expr ge e le m (make_longoffloat a sg) (Vlong i). +Proof. + unfold cast_float_long, make_longoffloat; intros. + destruct sg; econstructor; eauto; simpl; rewrite H0; auto. +Qed. + +Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct make_floatofint_correct make_intoffloat_correct + make_longofint_correct + make_floatoflong_correct make_longoffloat_correct eval_Eunop eval_Ebinop: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. @@ -357,38 +247,34 @@ Qed. Hint Resolve make_cast_int_correct make_cast_float_correct: cshm. Lemma make_cast_correct: - forall e le m a v ty1 ty2 v', + forall e le m a b v ty1 ty2 v', + make_cast ty1 ty2 a = OK b -> eval_expr ge e le m a v -> sem_cast v ty1 ty2 = Some v' -> - eval_expr ge e le m (make_cast ty1 ty2 a) v'. + eval_expr ge e le m b v'. Proof. - intros. unfold make_cast. functional inversion H0; subst. - (* neutral *) - rewrite H2; auto. - rewrite H2; auto. - (* int -> int *) - rewrite H2. auto with cshm. - (* float -> float *) - rewrite H2. auto with cshm. - (* int -> float *) - rewrite H2. auto with cshm. + intros. unfold make_cast, sem_cast in *; + destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm. (* float -> int *) - rewrite H2. eauto with cshm. + destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. eauto with cshm. + (* float -> long *) + destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. eauto with cshm. (* float -> bool *) - rewrite H2. econstructor; eauto with cshm. - simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto. - rewrite H2. econstructor; eauto with cshm. - simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto. - (* pointer -> bool *) - rewrite H2. econstructor; eauto with cshm. - simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); reflexivity. - rewrite H2. econstructor; eauto with cshm. - (* struct -> struct *) - rewrite H2. auto. - (* union -> union *) - rewrite H2. auto. - (* any -> void *) - rewrite H5. auto. + econstructor; eauto with cshm. + simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. + destruct (Float.cmp Ceq f Float.zero); auto. + (* long -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp. + destruct (Int64.eq i Int64.zero); auto. + (* int -> bool *) + econstructor; eauto with cshm. + simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. + destruct (Int.eq i Int.zero); auto. + (* struct *) + destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto. + (* union *) + destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto. Qed. Lemma make_boolean_correct: @@ -413,6 +299,10 @@ Proof. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. exists Vtrue; split. econstructor; eauto with cshm. constructor. +(* long *) + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + unfold Val.cmpl, Val.cmpl_bool. simpl. + destruct (Int64.eq i Int64.zero); simpl; constructor. Qed. Lemma make_neg_correct: @@ -422,10 +312,8 @@ Lemma make_neg_correct: eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. - intros until m; intro SEM. unfold make_neg. - functional inversion SEM; intros. - rewrite H0 in H4. inv H4. eapply eval_Eunop; eauto with cshm. - rewrite H0 in H4. inv H4. eauto with cshm. + unfold sem_neg, make_neg; intros until m; intros SEM MAKE EV1; + destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. Qed. Lemma make_notbool_correct: @@ -435,20 +323,19 @@ Lemma make_notbool_correct: eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. - intros until m; intro SEM. unfold make_notbool. - functional inversion SEM; intros; rewrite H0 in H4; inversion H4; simpl; - eauto with cshm. + unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; + destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. Qed. Lemma make_notint_correct: forall a tya c va v e le m, sem_notint va tya = Some v -> - make_notint a tya = c -> + make_notint a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. - intros until m; intro SEM. unfold make_notint. - functional inversion SEM; intros. subst. eauto with cshm. + unfold sem_notint, make_notint; intros until m; intros SEM MAKE EV1; + destruct (classify_notint tya); inv MAKE; destruct va; inv SEM; eauto with cshm. Qed. Definition binary_constructor_correct @@ -461,99 +348,206 @@ Definition binary_constructor_correct eval_expr ge e le m b vb -> eval_expr ge e le m c v. +Section MAKE_BIN. + +Variable sem_int: signedness -> int -> int -> option val. +Variable sem_long: signedness -> int64 -> int64 -> option val. +Variable sem_float: float -> float -> option val. +Variables iop iopu fop lop lopu: binary_operation. + +Hypothesis iop_ok: + forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y. +Hypothesis iopu_ok: + forall x y m, eval_binop iopu (Vint x) (Vint y) m = sem_int Unsigned x y. +Hypothesis lop_ok: + forall x y m, eval_binop lop (Vlong x) (Vlong y) m = sem_long Signed x y. +Hypothesis lopu_ok: + forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y. +Hypothesis fop_ok: + forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y. + +Lemma make_binarith_correct: + binary_constructor_correct + (make_binarith iop iopu fop lop lopu) + (sem_binarith sem_int sem_long sem_float). +Proof. + red; unfold make_binarith, sem_binarith; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_binarith tya tyb); inv MAKE; + destruct va; try discriminate; destruct vb; try discriminate. +- destruct s; inv H0; econstructor; eauto with cshm. + rewrite iop_ok; auto. rewrite iopu_ok; auto. +- erewrite <- fop_ok in SEM; eauto with cshm. +- erewrite <- fop_ok in SEM; eauto with cshm. +- erewrite <- fop_ok in SEM; eauto with cshm. +- destruct s; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +- destruct s2; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +- destruct s1; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +- erewrite <- fop_ok in SEM; eauto with cshm. +- erewrite <- fop_ok in SEM; eauto with cshm. +Qed. + +Lemma make_binarith_int_correct: + binary_constructor_correct + (make_binarith_int iop iopu lop lopu) + (sem_binarith sem_int sem_long (fun x y => None)). +Proof. + red; unfold make_binarith_int, sem_binarith; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_binarith tya tyb); inv MAKE; + destruct va; try discriminate; destruct vb; try discriminate. +- destruct s; inv H0; econstructor; eauto with cshm. + rewrite iop_ok; auto. rewrite iopu_ok; auto. +- destruct s; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +- destruct s2; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +- destruct s1; inv H0; econstructor; eauto with cshm. + rewrite lop_ok; auto. rewrite lopu_ok; auto. +Qed. + +End MAKE_BIN. + +Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. + Lemma make_add_correct: binary_constructor_correct make_add sem_add. Proof. - red; intros until m. intro SEM. unfold make_add. - functional inversion SEM; rewrite H0; intros; - inversion H7; eauto with cshm. - eapply eval_Ebinop. eauto. - eapply eval_Ebinop. eauto with cshm. eauto. - simpl. reflexivity. reflexivity. - eapply eval_Ebinop. eauto. - eapply eval_Ebinop. eauto with cshm. eauto. - simpl. reflexivity. simpl. reflexivity. + red; unfold make_add, sem_add; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_add tya tyb); inv MAKE. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- eapply make_binarith_correct; eauto; intros; auto. Qed. Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub. Proof. - red; intros until m. intro SEM. unfold make_sub. - functional inversion SEM; rewrite H0; intros; - inversion H7; eauto with cshm. - eapply eval_Ebinop. eauto. - eapply eval_Ebinop. eauto with cshm. eauto. - simpl. reflexivity. reflexivity. - inversion H9. eapply eval_Ebinop. - eapply eval_Ebinop; eauto. - simpl. unfold eq_block; rewrite H3. reflexivity. - eauto with cshm. simpl. rewrite H8. reflexivity. + red; unfold make_sub, sem_sub; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_sub tya tyb); inv MAKE. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- destruct va; try discriminate; destruct vb; inv SEM. + destruct (zeq b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0. + econstructor; eauto with cshm. rewrite zeq_true. simpl. rewrite E; auto. +- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- eapply make_binarith_correct; eauto; intros; auto. Qed. Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul. Proof. - red; intros until m. intro SEM. unfold make_mul. - functional inversion SEM; rewrite H0; intros; - inversion H7; eauto with cshm. + apply make_binarith_correct; intros; auto. Qed. Lemma make_div_correct: binary_constructor_correct make_div sem_div. Proof. - red; intros until m. intro SEM. unfold make_div. - functional inversion SEM; rewrite H0; intros. - inversion H8. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H7; auto. - inversion H8. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H7; auto. - inversion H7; eauto with cshm. - inversion H7; eauto with cshm. - inversion H7; eauto with cshm. + apply make_binarith_correct; intros; auto. Qed. Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod. - red; intros until m. intro SEM. unfold make_mod. - functional inversion SEM; rewrite H0; intros. - inversion H8. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H7; auto. - inversion H8. eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H7; auto. +Proof. + apply make_binarith_int_correct; intros; auto. Qed. Lemma make_and_correct: binary_constructor_correct make_and sem_and. Proof. - red; intros until m. intro SEM. unfold make_and. - functional inversion SEM. intros. inversion H7. - eauto with cshm. + apply make_binarith_int_correct; intros; auto. Qed. Lemma make_or_correct: binary_constructor_correct make_or sem_or. Proof. - red; intros until m. intro SEM. unfold make_or. - functional inversion SEM. intros. inversion H7. - eauto with cshm. + apply make_binarith_int_correct; intros; auto. Qed. Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor. Proof. - red; intros until m. intro SEM. unfold make_xor. - functional inversion SEM. intros. inversion H7. - eauto with cshm. + apply make_binarith_int_correct; intros; auto. +Qed. + +Ltac comput val := + let x := fresh in set val as x in *; vm_compute in x; subst x. + +Remark small_shift_amount_1: + forall i, + Int64.ltu i Int64.iwordsize = true -> + Int.ltu (Int64.loword i) Int64.iwordsize' = true + /\ Int64.unsigned i = Int.unsigned (Int64.loword i). +Proof. + intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize). + assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). + { + unfold Int64.loword. rewrite Int.unsigned_repr; auto. + comput Int.max_unsigned; omega. + } + split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. +Qed. + +Remark small_shift_amount_2: + forall i, + Int64.ltu i (Int64.repr 32) = true -> + Int.ltu (Int64.loword i) Int.iwordsize = true. +Proof. + intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)). + assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). + { + unfold Int64.loword. rewrite Int.unsigned_repr; auto. + comput Int.max_unsigned; omega. + } + unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. +Qed. + +Lemma small_shift_amount_3: + forall i, + Int.ltu i Int64.iwordsize' = true -> + Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i. +Proof. + intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). + apply Int64.unsigned_repr. comput Int64.max_unsigned; omega. Qed. Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl. Proof. - red; intros until m. intro SEM. unfold make_shl. - functional inversion SEM. intros. inversion H8. - eapply eval_Ebinop; eauto with cshm. - simpl. rewrite H7. auto. + red; unfold make_shl, sem_shl, sem_shift; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_shift tya tyb); inv MAKE; + destruct va; try discriminate; destruct vb; try discriminate. +- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. + econstructor; eauto. simpl; rewrite E; auto. +- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. + exploit small_shift_amount_1; eauto. intros [A B]. + econstructor; eauto with cshm. simpl. rewrite A. + f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto. +- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. + econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. +- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. + econstructor; eauto with cshm. simpl. rewrite E. + unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto. Qed. Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. Proof. - red; intros until m. intro SEM. unfold make_shr. - functional inversion SEM; intros; rewrite H0 in H8; inversion H8. - eapply eval_Ebinop; eauto with cshm. - simpl; rewrite H7; auto. - eapply eval_Ebinop; eauto with cshm. - simpl; rewrite H7; auto. + red; unfold make_shr, sem_shr, sem_shift; + intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_shift tya tyb); inv MAKE; + destruct va; try discriminate; destruct vb; try discriminate. +- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. + destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto. +- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. + exploit small_shift_amount_1; eauto. intros [A B]. + destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A; + f_equal; f_equal. + unfold Int64.shr', Int64.shr; rewrite B; auto. + unfold Int64.shru', Int64.shru; rewrite B; auto. +- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. + destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. +- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. + destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. + unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto. + unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. Lemma make_cmp_correct: @@ -564,35 +558,12 @@ Lemma make_cmp_correct: eval_expr ge e le m b vb -> eval_expr ge e le m c v. Proof. - intros until m. intro SEM. unfold make_cmp. - functional inversion SEM; rewrite H0; intros. - (** ii Signed *) - inversion H8; eauto with cshm. - (* ii Unsigned *) - inversion H8. eauto with cshm. - (* pp int int *) - inversion H8. eauto with cshm. - (* pp ptr ptr *) - inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. - rewrite H3. rewrite H9. auto. - inversion H10. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9. - destruct cmp; simpl in *; inv H; auto. - (* pp ptr int *) - inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite H8. - destruct cmp; simpl in *; inv H; auto. - (* pp int ptr *) - inversion H9. eapply eval_Ebinop; eauto with cshm. - simpl. unfold Val.cmpu. simpl. rewrite H8. - destruct cmp; simpl in *; inv H; auto. - (* ff *) - inversion H8. eauto with cshm. - (* if *) - inversion H8. eauto with cshm. - (* fi *) - inversion H8. eauto with cshm. + unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; + destruct (classify_cmp tya tyb). +- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; + simpl in SEM; inv SEM. + econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto. +- eapply make_binarith_correct; eauto; intros; auto. Qed. Lemma transl_unop_correct: @@ -604,7 +575,7 @@ Lemma transl_unop_correct: Proof. intros. destruct op; simpl in *. eapply make_notbool_correct; eauto. - eapply make_notint_correct with (tya := tya); eauto. congruence. + eapply make_notint_correct; eauto. eapply make_neg_correct; eauto. Qed. @@ -903,6 +874,8 @@ Proof. apply make_intconst_correct. (* const float *) apply make_floatconst_correct. +(* const long *) + apply make_longconst_correct. (* temp var *) constructor; auto. (* addrof *) @@ -957,8 +930,7 @@ Proof. induction 1; intros. monadInv H. constructor. monadInv H2. constructor. - eapply make_cast_correct. eapply transl_expr_correct; eauto. auto. - eauto. + eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. Qed. End EXPR. @@ -1103,8 +1075,8 @@ Proof. (* skip *) auto. (* assign *) - unfold make_store, make_memcpy in EQ2. - destruct (access_mode (typeof e)); inv EQ2; auto. + unfold make_store, make_memcpy in EQ3. + destruct (access_mode (typeof e)); inv EQ3; auto. (* set *) auto. (* call *) @@ -1196,7 +1168,7 @@ Proof. monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). inversion MTR. auto. - subst ts. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof a1)); congruence. + subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence. destruct SAME; subst ts' tk'. econstructor; split. apply plus_one. eapply make_store_correct; eauto. @@ -1327,7 +1299,7 @@ Proof. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. - eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto. + eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_env_free_blocks; eauto. econstructor; eauto. eapply match_cont_call_cont. eauto. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index c05f21a..bf483a0 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -26,7 +26,7 @@ Require Import Errors. union). Numeric types (integers and floats) fully specify the bit size of the type. An integer type is a pair of a signed/unsigned flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size - standing for the C99 [_Bool] type. *) + standing for the C99 [_Bool] type. 64-bit integers are treated separately. *) Inductive signedness : Type := | Signed: signedness @@ -92,6 +92,7 @@ Definition noattr := {| attr_volatile := false |}. Inductive type : Type := | Tvoid: type (**r the [void] type *) | Tint: intsize -> signedness -> attr -> type (**r integer types *) + | Tlong: signedness -> attr -> type (**r 64-bit integer types *) | Tfloat: floatsize -> attr -> type (**r floating-point types *) | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) @@ -131,6 +132,7 @@ Definition attr_of_type (ty: type) := match ty with | Tvoid => noattr | Tint sz si a => a + | Tlong si a => a | Tfloat sz a => a | Tpointer elt a => a | Tarray elt sz a => a @@ -148,8 +150,7 @@ Definition type_bool := Tint IBool Signed noattr. Definition typeconv (ty: type) : type := match ty with - | Tint I32 Unsigned _ => ty - | Tint _ _ a => Tint I32 Signed a + | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a | Tarray t sz a => Tpointer t a | Tfunction _ _ => Tpointer ty noattr | _ => ty @@ -166,6 +167,7 @@ Fixpoint alignof (t: type) : Z := | Tint I16 _ _ => 2 | Tint I32 _ _ => 4 | Tint IBool _ _ => 1 + | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 | Tpointer _ _ => 4 @@ -218,6 +220,7 @@ Fixpoint sizeof (t: type) : Z := | Tint I16 _ _ => 2 | Tint I32 _ _ => 4 | Tint IBool _ _ => 1 + | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 | Tpointer _ _ => 4 @@ -425,6 +428,7 @@ Definition access_mode (ty: type) : mode := | Tint I16 Unsigned _ => By_value Mint16unsigned | Tint I32 _ _ => By_value Mint32 | Tint IBool _ _ => By_value Mint8unsigned + | Tlong _ _ => By_value Mint64 | Tfloat F32 _ => By_value Mfloat32 | Tfloat F64 _ => By_value Mfloat64 | Tvoid => By_nothing @@ -458,6 +462,7 @@ Fixpoint unroll_composite (ty: type) : type := match ty with | Tvoid => ty | Tint _ _ _ => ty + | Tlong _ _ => ty | Tfloat _ _ => ty | Tpointer t1 a => Tpointer (unroll_composite t1) a | Tarray t1 sz a => Tarray (unroll_composite t1) sz a @@ -526,6 +531,7 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist := Definition typ_of_type (t: type) : AST.typ := match t with | Tfloat _ _ => AST.Tfloat + | Tlong _ _ => AST.Tlong | _ => AST.Tint end. @@ -533,6 +539,7 @@ Definition opttyp_of_type (t: type) : option AST.typ := match t with | Tvoid => None | Tfloat _ _ => Some AST.Tfloat + | Tlong _ _ => Some AST.Tlong | _ => Some AST.Tint end. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 7711ade..657f607 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -54,7 +54,7 @@ Fixpoint constval (a: expr) : res val := match a with | Eval v ty => match v with - | Vint _ | Vfloat _ => OK v + | Vint _ | Vfloat _ | Vlong _ => OK v | Vptr _ _ | Vundef => Error(msg "illegal constant") end | Evalof l ty => @@ -152,6 +152,7 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | Vint n, Tint I32 sg _ => OK(Init_int32 n) | Vint n, Tpointer _ _ => OK(Init_int32 n) | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n) + | Vlong n, Tlong _ _ => OK(Init_int64 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) diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 75b73ff..c2ca135 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -333,45 +333,19 @@ Qed. (** * Soundness of the compile-time evaluator *) -(** [match_val v v'] holds if the compile-time value [v] - (with symbolic pointers) matches the run-time value [v'] - (with concrete pointers). *) - -Inductive match_val: val -> val -> Prop := - | match_vint: forall n, - match_val (Vint n) (Vint n) - | match_vfloat: forall f, - match_val (Vfloat f) (Vfloat f) - | match_vptr: forall id b ofs, - Genv.find_symbol ge id = Some b -> - match_val (Vptr (Zpos id) ofs) (Vptr b ofs) - | match_vundef: - match_val Vundef Vundef. - -Lemma match_val_of_bool: - forall b, match_val (Val.of_bool b) (Val.of_bool b). -Proof. - destruct b; constructor. -Qed. - -Hint Constructors match_val: mval. -Hint Resolve match_val_of_bool: mval. - -(** The [match_val] relation commutes with the evaluation functions - from [Csem]. *) - -Lemma sem_unary_match: - forall op ty v1 v v1' v', - sem_unary_operation op v1 ty = Some v -> - sem_unary_operation op v1' ty = Some v' -> - match_val v1 v1' -> - match_val v v'. -Proof. - intros. destruct op; simpl in *. - unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor. - unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval. - unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval. -Qed. +(** A global environment [ge] induces a memory injection mapping + our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers + [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *) + +Definition inj (b: block) := + match b with + | Zpos id => + match Genv.find_symbol ge id with + | Some b' => Some (b', 0) + | None => None + end + | _ => None + end. Lemma mem_empty_not_valid_pointer: forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. @@ -387,104 +361,18 @@ Proof. now rewrite !mem_empty_not_valid_pointer. Qed. -Lemma sem_cmp_match: - forall c v1 ty1 v2 ty2 m v v1' v2' v', - sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> - sem_cmp c v1' ty1 v2' ty2 m = Some v' -> - match_val v1 v1' -> match_val v2 v2' -> - match_val v v'. -Proof. -Opaque zeq. - intros. unfold sem_cmp in *. - destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. -- destruct (Int.eq n Int.zero); try discriminate. - unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. -- destruct (Int.eq n Int.zero); try discriminate. - unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. -- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. -Qed. - -Lemma sem_binary_match: - forall op v1 ty1 v2 ty2 m v v1' v2' v', - sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v -> - sem_binary_operation op v1' ty1 v2' ty2 m = Some v' -> - match_val v1 v1' -> match_val v2 v2' -> - match_val v v'. -Proof. - intros. unfold sem_binary_operation in *; destruct op. -(* add *) - unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* sub *) - unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail). - destruct (zeq (Zpos id) (Zpos id0)); try discriminate. - assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. - destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval. -(* mul *) - unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* div *) - unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H11. constructor. - inv H11. constructor. - inv H11. constructor. -(* mod *) - unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H12. rewrite H11 in H2. inv H2. constructor. -(* and *) - unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* or *) - unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* xor *) - unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* shl *) - unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. -(* shr *) - unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate; - destruct s; inv H1; inv H2; try discriminate. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. -(* comparisons *) - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. -Qed. - Lemma sem_cast_match: - forall v1 ty1 ty2 v2, sem_cast v1 ty1 ty2 = Some v2 -> - forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> - match_val v2' v2. + forall v1 ty1 ty2 v2 v1' v2', + sem_cast v1 ty1 ty2 = Some v2 -> + do_cast v1' ty1 ty2 = OK v2' -> + val_inject inj v1' v1 -> + val_inject inj v2' v2. Proof. - intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:?; inv H1. - unfold sem_cast in H; functional inversion Heqo; subst. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor; auto. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. destruct (cast_float_int si2 f); inv H. inv H7. constructor. - rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. - rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. - rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. - rewrite H5 in H. inv H. auto. + intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. + exploit sem_cast_inject. eexact E. eauto. + intros [v' [A B]]. congruence. Qed. -Lemma bool_val_match: - forall v v' ty, - match_val v v' -> - bool_val v ty = bool_val v' ty. -Proof. - intros. inv H; auto. -Qed. - (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -492,13 +380,13 @@ Lemma constval_rvalue: eval_simple_rvalue empty_env m a v -> forall v', constval a = OK v' -> - match_val v' v + val_inject inj v' v with constval_lvalue: forall m a b ofs, eval_simple_lvalue empty_env m a b ofs -> forall v', constval a = OK v' -> - match_val v' (Vptr b ofs). + val_inject inj v' (Vptr b ofs). Proof. (* rvalue *) induction 1; intros vres CV; simpl in CV; try (monadInv CV). @@ -509,11 +397,18 @@ Proof. (* addrof *) eauto. (* unop *) - revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0. - eapply sem_unary_match; eauto. + destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0. + exploit sem_unary_operation_inject. eexact E. eauto. + intros [v' [A B]]. congruence. (* binop *) - revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2. - eapply sem_binary_match; eauto. + destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. + exploit (sem_binary_operation_inj inj Mem.empty m). + intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. + eauto. eauto. eauto. + intros [v' [A B]]. congruence. (* cast *) eapply sem_cast_match; eauto. (* sizeof *) @@ -521,18 +416,26 @@ Proof. (* alignof *) constructor. (* seqand *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. constructor. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = true) by congruence. subst b. monadInv H5. + eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. constructor. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = false) by congruence. subst b. monadInv H5. + eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ3; auto. - rewrite H0 in EQ3. destruct b; eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b' = b) by congruence. subst b'. + destruct b; eapply sem_cast_match; eauto. (* comma *) auto. (* paren *) @@ -543,12 +446,14 @@ Proof. (* var local *) unfold empty_env in H. rewrite PTree.gempty in H. congruence. (* var_global *) - constructor; auto. + econstructor. unfold inj. rewrite H0. eauto. auto. (* deref *) eauto. (* field struct *) rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x with delta by congruence. constructor. auto. + simpl. replace x with delta by congruence. econstructor; eauto. + rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. + simpl. auto. (* field union *) rewrite H0 in CV. eauto. Qed. @@ -569,7 +474,7 @@ Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> constval r = OK v -> - m' = m /\ ty = typeof r /\ match_val v v'. + m' = m /\ ty = typeof r /\ val_inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. @@ -595,19 +500,23 @@ Proof. inv D. (* int *) destruct ty; try discriminate. - destruct i; inv EQ2. + destruct i0; inv EQ2. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. simpl in H2; inv H2. assumption. inv EQ2. simpl in H2; inv H2. assumption. + (* long *) + destruct ty; inv EQ2. simpl in H2; inv H2. assumption. (* float *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) - assert (data = Init_addrof id ofs0 /\ chunk = Mint32). + unfold inj in H. destruct b1; try discriminate. + assert (data = Init_addrof p ofs1 /\ chunk = Mint32). destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. - destruct H4; subst. rewrite H. assumption. + destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. + rewrite Int.add_zero in H3. auto. (* undef *) discriminate. Qed. @@ -624,12 +533,15 @@ Proof. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. + inv EQ2; reflexivity. + destruct ty; inv EQ2; reflexivity. destruct ty; try discriminate. destruct f0; inv EQ2; reflexivity. destruct b; try discriminate. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. + inv EQ2; reflexivity. Qed. Notation idlsize := Genv.init_data_list_size. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index d61afa3..a8b2b98 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -43,6 +43,7 @@ let rec precedence = function | Efield _ -> (16, LtoR) | Econst_int _ -> (16, NA) | Econst_float _ -> (16, NA) + | Econst_long _ -> (16, NA) | Eunop _ -> (15, RtoL) | Eaddrof _ -> (15, RtoL) | Ecast _ -> (14, RtoL) @@ -79,6 +80,8 @@ let rec expr p (prec, e) = fprintf p "%ld" (camlint_of_coqint n) | Econst_float(f, _) -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Econst_long(n, _) -> + fprintf p "%LdLL" (camlint64_of_coqint n) | Eunop(op, a1, _) -> fprintf p "%s%a" (name_unop op) expr (prec', a1) | Eaddrof(a1, _) -> @@ -258,6 +261,7 @@ let rec collect_expr e = match e with | Econst_int _ -> () | Econst_float _ -> () + | Econst_long _ -> () | Evar _ -> () | Etempvar _ -> () | Ederef(r, _) -> collect_expr r diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index b1ee234..f91dca6 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -64,6 +64,11 @@ let name_floattype sz = | F32 -> "float" | F64 -> "double" +let name_longtype sg = + match sg with + | Signed -> "long long" + | Unsigned -> "unsigned long long" + (* Collecting the names and fields of structs and unions *) module StructUnion = Map.Make(String) @@ -91,6 +96,8 @@ let rec name_cdecl id ty = name_inttype sz sg ^ attributes a ^ name_optid id | Tfloat(sz, a) -> name_floattype sz ^ attributes a ^ name_optid id + | Tlong(sg, a) -> + name_longtype sg ^ attributes a ^ name_optid id | Tpointer(t, a) -> let id' = match t with @@ -174,6 +181,7 @@ let print_value p v = match v with | Vint n -> fprintf p "%ld" (camlint_of_coqint n) | Vfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f) + | Vlong n -> fprintf p "%Ld" (camlint64_of_coqint n) | Vptr(b, ofs) -> fprintf p "<ptr%a>" !print_pointer_hook (b, ofs) | Vundef -> fprintf p "<undef>" @@ -397,6 +405,7 @@ let print_init p = function | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n) | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n) | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n) + | Init_int64 n -> fprintf p "%Ld,@ " (camlint64_of_coqint n) | Init_float32 n -> fprintf p "%F,@ " (camlfloat_of_coqfloat n) | Init_float64 n -> fprintf p "%F,@ " (camlfloat_of_coqfloat n) | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n) @@ -444,6 +453,7 @@ let rec collect_type = function | Tvoid -> () | Tint _ -> () | Tfloat _ -> () + | Tlong _ -> () | Tpointer(t, _) -> collect_type t | Tarray(t, _, _) -> collect_type t | Tfunction(args, res) -> collect_type_list args; collect_type res diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 2dbd97e..98dad93 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -108,6 +108,7 @@ Function eval_simpl_expr (a: expr) : option val := match a with | Econst_int n _ => Some(Vint n) | Econst_float n _ => Some(Vfloat n) + | Econst_long n _ => Some(Vlong n) | Ecast b ty => match eval_simpl_expr b with | None => None @@ -222,6 +223,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement ret (finish dst nil (Econst_int n ty)) | Csyntax.Eval (Vfloat n) ty => ret (finish dst nil (Econst_float n ty)) + | Csyntax.Eval (Vlong n) ty => + ret (finish dst nil (Econst_long n ty)) | Csyntax.Eval _ ty => error (msg "SimplExpr.transl_expr: Eval") | Csyntax.Esizeof ty' ty => diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index b31738b..1e7a84c 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -768,6 +768,10 @@ Opaque makeif. constructor. auto. intros; constructor. constructor. constructor. auto. intros; constructor. + intros. destruct dst; simpl in *; inv H2. + constructor. auto. intros; constructor. + constructor. + constructor. auto. intros; constructor. (* var *) monadInv H; econstructor; split; auto with gensym. UseFinish. constructor. (* field *) diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 18eeea2..edcd5fe 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -46,6 +46,7 @@ Definition make_cast (a: expr) (tto: type) : expr := | cast_case_neutral => a | cast_case_i2i I32 _ => a | cast_case_f2f F64 => a + | cast_case_l2l => a | cast_case_struct _ _ _ _ => a | cast_case_union _ _ _ _ => a | cast_case_void => a @@ -58,6 +59,7 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr := match a with | Econst_int _ _ => a | Econst_float _ _ => a + | Econst_long _ _ => a | Evar id ty => if VSet.mem id cenv then Etempvar id ty else Evar id ty | Etempvar id ty => Etempvar id ty | Ederef a1 ty => Ederef (simpl_expr cenv a1) ty @@ -156,6 +158,7 @@ Fixpoint addr_taken_expr (a: expr): VSet.t := match a with | Econst_int _ _ => VSet.empty | Econst_float _ _ => VSet.empty + | Econst_long _ _ => VSet.empty | Evar id ty => VSet.empty | Etempvar id ty => VSet.empty | Ederef a1 ty => addr_taken_expr a1 @@ -224,8 +227,7 @@ Definition add_lifted (cenv: compilenv) (vars1 vars2: list (ident * type)) := Definition transf_function (f: function) : res function := let cenv := cenv_for f in - do x <- assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) - (var_names f.(fn_temps))); + assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps))); do body' <- simpl_stmt cenv f.(fn_body); OK {| fn_return := f.(fn_return); fn_params := f.(fn_params); diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e3aa4e2..1dcf630 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -202,16 +202,22 @@ Inductive val_casted: val -> type -> Prop := | val_casted_float: forall sz attr n, cast_float_float sz n = n -> val_casted (Vfloat n) (Tfloat sz attr) + | val_casted_long: forall si attr n, + val_casted (Vlong n) (Tlong si attr) | val_casted_ptr_ptr: forall b ofs ty attr, val_casted (Vptr b ofs) (Tpointer ty attr) | val_casted_int_ptr: forall n ty attr, val_casted (Vint n) (Tpointer ty attr) | val_casted_ptr_int: forall b ofs si attr, val_casted (Vptr b ofs) (Tint I32 si attr) - | val_casted_struct: forall id fld attr v, - val_casted v (Tstruct id fld attr) - | val_casted_union: forall id fld attr v, - val_casted v (Tunion id fld attr) + | val_casted_ptr_cptr: forall b ofs id attr, + val_casted (Vptr b ofs) (Tcomp_ptr id attr) + | val_casted_int_cptr: forall n id attr, + val_casted (Vint n) (Tcomp_ptr id attr) + | val_casted_struct: forall id fld attr b ofs, + val_casted (Vptr b ofs) (Tstruct id fld attr) + | val_casted_union: forall id fld attr b ofs, + val_casted (Vptr b ofs) (Tunion id fld attr) | val_casted_void: forall v, val_casted v Tvoid. @@ -240,12 +246,15 @@ Proof. constructor. (* int *) destruct i; destruct ty; simpl in H; try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I16 s). constructor. auto. - constructor. + constructor. + constructor. auto. destruct (cast_float_int s f0); inv H1. constructor. auto. constructor. auto. constructor. @@ -253,7 +262,10 @@ Proof. constructor. constructor; auto. constructor; auto. + constructor; auto. + constructor; auto. constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor. simpl. destruct (Int64.eq i Int64.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f0 Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. @@ -261,20 +273,31 @@ Proof. constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. + constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor; auto. +(* long *) + destruct ty; try discriminate. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; try discriminate. destruct (cast_float_long s f0); inv H. constructor. (* float *) destruct ty; simpl in H; try discriminate; destruct v; inv H. constructor. apply cast_float_float_idem. constructor. apply cast_float_float_idem. + constructor. apply cast_float_float_idem. (* pointer *) destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. (* impossible cases *) discriminate. discriminate. -(* structs,unions *) - constructor. - constructor. -(* impossible cases *) - discriminate. +(* structs *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. +(* unions *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. +(* comp_ptr *) + destruct ty; simpl in H; try discriminate; destruct v; inv H; constructor. Qed. Lemma val_casted_load_result: @@ -293,6 +316,9 @@ Proof. inv H0; auto. inv H0; auto. inv H0; auto. + inv H0; auto. + discriminate. + discriminate. discriminate. discriminate. discriminate. @@ -301,24 +327,18 @@ Qed. Lemma cast_val_casted: forall v ty, val_casted v ty -> sem_cast v ty ty = Some v. Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl. + intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. destruct sz; congruence. congruence. - auto. - auto. - auto. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - auto. Qed. Lemma val_casted_inject: forall f v v' ty, val_inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. - intros. inv H. - auto. - auto. + intros. inv H; auto. inv H0; constructor. inv H0; constructor. Qed. @@ -356,7 +376,10 @@ Proof. destruct v1; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. + destruct v1; inv H0; auto. + destruct v1; try discriminate. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + destruct v1; try discriminate. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. inv H0; auto. Qed. @@ -1324,176 +1347,6 @@ Proof. exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto. Qed. -Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. -Proof. unfold Vtrue; auto. Qed. - -Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. -Proof. unfold Vfalse; auto. Qed. - -Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). -Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. -Qed. - -Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. - -Ltac TrivialInject := - match goal with - | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto -(* - | |- exists v', _ /\ val_inject _ (Vint ?n) _ => exists (Vint n); split; auto - | |- exists v', _ /\ val_inject _ (Vfloat ?n) _ => exists (Vfloat n); split; auto - | |- exists v', _ /\ val_inject _ Vtrue _ => exists Vtrue; split; auto - | |- exists v', _ /\ val_inject _ Vfalse _ => exists Vfalse; split; auto - | |- exists v', _ /\ val_inject _ (Val.of_bool ?b) _ => exists (Val.of_bool b); split; auto -*) - | _ => idtac - end. - -Lemma sem_unary_operation_inject: - forall op v1 ty v tv1, - sem_unary_operation op v1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. -Proof. - unfold sem_unary_operation; intros. destruct op. - (* notbool *) - unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. - (* notint *) - unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. - (* neg *) - unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. -Qed. - -Lemma sem_cmp_inject: - forall cmp v1 tv1 ty1 v2 tv2 ty2 v, - sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv. -Proof. - unfold sem_cmp; intros. - assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v -> - exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv). - intros. exists v; split; auto. - destruct cmp; simpl in H2; inv H2; auto. - - destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.eq i Int.zero); try discriminate; auto. - destruct (Int.eq i Int.zero); try discriminate; auto. - - destruct (zeq b1 b0); subst. - rewrite H0 in H2. inv H2. rewrite zeq_true. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. - simpl H3. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto. - simpl. replace (Int.cmpu cmp (Int.add ofs1 (Int.repr delta)) - (Int.add ofs0 (Int.repr delta))) - with (Int.cmpu cmp ofs1 ofs0). - inv H3; TrivialInject. - symmetry. apply Int.translate_cmpu. - eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. - eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. - destruct (zeq b2 b3); subst. - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto). - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto). - simpl. - exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy. - destruct cmp; simpl in H3; inv H3. - simpl. unfold Int.eq. rewrite zeq_false; auto. - simpl. unfold Int.eq. rewrite zeq_false; auto. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto. - simpl in H3 |- *. auto. -Qed. - -Lemma sem_binary_operation_inject: - forall op v1 ty1 v2 ty2 v tv1 tv2, - sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv. -Proof. - unfold sem_binary_operation; intros. destruct op. -(* add *) - unfold sem_add in *; destruct (classify_add ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. -(* sub *) - unfold sem_sub in *; destruct (classify_sub ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. - rewrite zeq_true. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. - rewrite Int.sub_shifted. TrivialInject. -(* mul *) - unfold sem_mul in *; destruct (classify_mul ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* div *) - unfold sem_div in *; destruct (classify_div ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct ( Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject. - destruct (Int.eq i0 Int.zero); inv H1; TrivialInject. -(* mod *) - unfold sem_mod in *; destruct (classify_binint ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct ( Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject. - destruct (Int.eq i0 Int.zero); inv H1; TrivialInject. -(* and *) - unfold sem_and in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* or *) - unfold sem_or in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* xor *) - unfold sem_xor in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* shl *) - unfold sem_shl in *; destruct (classify_shift ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. -(* shr *) - unfold sem_shr in *; destruct (classify_shift ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. -(* comparisons *) - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. -Qed. - -Lemma sem_cast_inject: - forall v1 ty1 ty v tv1, - sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. -Proof. - unfold sem_cast; intros. - destruct (classify_cast ty1 ty); try discriminate. - inv H0; inv H; TrivialInject. econstructor; eauto. - inv H0; inv H; TrivialInject. - inv H0; inv H; TrivialInject. - inv H0; inv H; TrivialInject. - inv H0; try discriminate. destruct (cast_float_int si2 f0); inv H. TrivialInject. - inv H0; inv H. TrivialInject. - inv H0; inv H. TrivialInject. - TrivialInject. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject. - inv H; TrivialInject. -Qed. - -Lemma bool_val_inject: - forall v ty b tv, - bool_val v ty = Some b -> - val_inject f v tv -> - bool_val tv ty = Some b. -Proof. - unfold bool_val; intros. - destruct (classify_bool ty); inv H0; congruence. -Qed. - Lemma eval_simpl_expr: forall a v, eval_expr ge e le m a v -> @@ -1512,6 +1365,7 @@ Proof. (* const *) exists (Vint i); split; auto. constructor. exists (Vfloat f0); split; auto. constructor. + exists (Vlong i); split; auto. constructor. (* tempvar *) exploit me_temps; eauto. intros [[tv [A B]] C]. exists tv; split; auto. constructor; auto. @@ -2184,7 +2038,7 @@ Proof. (* goto *) generalize TRF; intros TRF'. monadInv TRF'. - exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x0 (call_cont tk)). + exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)). eauto. eapply match_cont_call_cont. eauto. apply compat_cenv_for. rewrite H. intros [ts' [tk' [A [B [C D]]]]]. @@ -2197,12 +2051,10 @@ Proof. generalize EQ; intro EQ'; monadInv EQ'. assert (list_norepet (var_names (fn_params f ++ fn_vars f))). unfold var_names. rewrite map_app. auto. - assert (list_disjoint (var_names (fn_params f)) (var_names (fn_temps f))). - monadInv EQ0. auto. exploit match_envs_alloc_variables; eauto. instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)). - intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H5. - intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H4. + intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4. + intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3. intros [j' [te [tm0 [A [B [C [D [E F]]]]]]]]. exploit store_params_correct. eauto. @@ -2212,7 +2064,7 @@ Proof. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. - exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto. + exploit create_undef_temps_inv; eauto. intros [P Q]. elim (l id id); auto. intros [tel [tm1 [P [Q [R [S T]]]]]]. change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f)) with (cenv_for f) in *. |