summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/C2C.ml46
-rw-r--r--cfrontend/CPragmas.ml3
-rw-r--r--cfrontend/Cexec.v4
-rw-r--r--cfrontend/Clight.v4
-rw-r--r--cfrontend/Cminorgen.v3
-rw-r--r--cfrontend/Cminorgenproof.v87
-rw-r--r--cfrontend/Cop.v953
-rw-r--r--cfrontend/Csharpminor.v4
-rw-r--r--cfrontend/Cshmgen.v206
-rw-r--r--cfrontend/Cshmgenproof.v526
-rw-r--r--cfrontend/Ctypes.v13
-rw-r--r--cfrontend/Initializers.v3
-rw-r--r--cfrontend/Initializersproof.v222
-rw-r--r--cfrontend/PrintClight.ml4
-rw-r--r--cfrontend/PrintCsyntax.ml10
-rw-r--r--cfrontend/SimplExpr.v3
-rw-r--r--cfrontend/SimplExprspec.v4
-rw-r--r--cfrontend/SimplLocals.v6
-rw-r--r--cfrontend/SimplLocalsproof.v244
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 *.