aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--caml/Cil2Csyntax.ml9
-rw-r--r--caml/PrintCsyntax.ml15
-rw-r--r--cfrontend/Csem.v15
-rw-r--r--cfrontend/Cshmgen.v10
-rw-r--r--cfrontend/Cshmgenproof1.v4
-rw-r--r--cfrontend/Cshmgenproof3.v54
-rw-r--r--cfrontend/Csyntax.v92
-rw-r--r--cfrontend/Ctyping.v8
8 files changed, 160 insertions, 47 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index f736fb0c..7224610c 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -391,10 +391,6 @@ and convertExp = function
let e = convertLval lv in
(* array A of type T replaced by (T* )A *)
Expr (Ecast (tPtr, e), tPtr)
-(*
- (* array A replaced by &(A[0]) *)
- Expr (Eaddrof (Expr (Eindex (e, const0), t')), tPtr)
-*)
| _ -> internal_error "convertExp: StartOf applied to a \
lvalue whose type is not an array"
@@ -427,8 +423,9 @@ and convertLval lv =
end
| Index (e', ofs) ->
match t with
- | Tarray (t', _) -> let e'' = Eindex (e, convertExp e') in
- processOffset (Expr (e'', t')) ofs
+ | Tarray (t', _) ->
+ let e'' = Ederef(Expr (Ebinop(Oadd, e, convertExp e'), t)) in
+ processOffset (Expr (e'', t')) ofs
| _ -> internal_error "processOffset: Index on a non-array"
in
(* convert the lvalue *)
diff --git a/caml/PrintCsyntax.ml b/caml/PrintCsyntax.ml
index 9ea5b4b8..6aaa5397 100644
--- a/caml/PrintCsyntax.ml
+++ b/caml/PrintCsyntax.ml
@@ -143,7 +143,7 @@ let parenthesis_level (Expr (e, ty)) =
| Omul | Odiv | Omod -> 40
end
| Ecast _ -> 30
- | Eindex(_, _) -> 20
+ | Econdition(_, _, _) -> 80
| Eandbool(_, _) -> 80
| Eorbool(_, _) -> 80
| Esizeof _ -> 20
@@ -160,6 +160,12 @@ let rec print_expr p (Expr (eb, ty) as e) =
fprintf p "%s" (extern_atom id)
| Eunop(op, e1) ->
fprintf p "%s%a" (name_unop op) print_expr_prec (level, e1)
+ | Ederef (Expr (Ebinop(Oadd, e1, e2), _)) ->
+ fprintf p "@[<hov 2>%a@,[%a]@]"
+ print_expr_prec (level, e1)
+ print_expr_prec (level, e2)
+ | Ederef (Expr (Efield(e1, id), _)) ->
+ fprintf p "%a->%s" print_expr_prec (level, e1) (extern_atom id)
| Ederef e ->
fprintf p "*%a" print_expr_prec (level, e)
| Eaddrof e ->
@@ -173,10 +179,11 @@ let rec print_expr p (Expr (eb, ty) as e) =
fprintf p "@[<hov 2>(%s)@,%a@]"
(name_type ty)
print_expr_prec (level, e1)
- | Eindex(e1, e2) ->
- fprintf p "@[<hov 2>%a@,[%a]@]"
+ | Econdition(e1, e2, e3) ->
+ fprintf p "@[<hov 0>%a@ ? %a@ : %a@]"
print_expr_prec (level, e1)
print_expr_prec (level, e2)
+ print_expr_prec (level, e3)
| Eandbool(e1, e2) ->
fprintf p "@[<hov 0>%a@ && %a@]"
print_expr_prec (level, e1)
@@ -418,7 +425,7 @@ let rec collect_expr (Expr(ed, ty)) =
| Eaddrof e -> collect_expr e
| Ebinop(op, e1, e2) -> collect_expr e1; collect_expr e2
| Ecast(ty, e1) -> collect_type ty; collect_expr e1
- | Eindex(e1, e2) -> collect_expr e1; collect_expr e2
+ | Econdition(e1, e2, e3) -> collect_expr e1; collect_expr e2; collect_expr e3
| Eandbool(e1, e2) -> collect_expr e1; collect_expr e2
| Eorbool(e1, e2) -> collect_expr e1; collect_expr e2
| Esizeof ty -> collect_type ty
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5e4f4e37..22139127 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -564,6 +564,16 @@ Inductive eval_expr: expr -> val -> Prop :=
eval_expr a2 v2 ->
sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
eval_expr (Expr (Ebinop op a1 a2) ty) v
+ | eval_Econdition_true: forall a1 a2 a3 ty v1 v2,
+ eval_expr a1 v1 ->
+ is_true v1 (typeof a1) ->
+ eval_expr a2 v2 ->
+ eval_expr (Expr (Econdition a1 a2 a3) ty) v2
+ | eval_Econdition_false: forall a1 a2 a3 ty v1 v3,
+ eval_expr a1 v1 ->
+ is_false v1 (typeof a1) ->
+ eval_expr a3 v3 ->
+ eval_expr (Expr (Econdition a1 a2 a3) ty) v3
| eval_Eorbool_1: forall a1 a2 ty v1,
eval_expr a1 v1 ->
is_true v1 (typeof a1) ->
@@ -604,11 +614,6 @@ with eval_lvalue: expr -> block -> int -> Prop :=
| eval_Ederef: forall a ty l ofs,
eval_expr a (Vptr l ofs) ->
eval_lvalue (Expr (Ederef a) ty) l ofs
- | eval_Eindex: forall a1 a2 ty v1 v2 l ofs,
- eval_expr a1 v1 ->
- eval_expr a2 v2 ->
- sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
- eval_lvalue (Expr (Eindex a1 a2) ty) l ofs
| eval_Efield_struct: forall a i ty l ofs id fList delta,
eval_lvalue a l ofs ->
typeof a = Tstruct id fList ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 20eb17f4..64a58ad0 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -383,11 +383,11 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr :=
| Expr (Csyntax.Ecast ty b) _ =>
do tb <- transl_expr b;
OK (make_cast (typeof b) ty tb)
- | Expr (Csyntax.Eindex b c) ty =>
+ | Expr (Csyntax.Econdition b c d) _ =>
do tb <- transl_expr b;
do tc <- transl_expr c;
- do ts <- make_add tb (typeof b) tc (typeof c);
- make_load ts ty
+ do td <- transl_expr d;
+ OK(Econdition (make_boolean tb (typeof b)) tc td)
| Expr (Csyntax.Eandbool b c) _ =>
do tb <- transl_expr b;
do tc <- transl_expr c;
@@ -425,10 +425,6 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr :=
OK (Eaddrof id)
| Expr (Csyntax.Ederef b) _ =>
transl_expr b
- | Expr (Csyntax.Eindex b c) _ =>
- do tb <- transl_expr b;
- do tc <- transl_expr c;
- make_add tb (typeof b) tc (typeof c)
| Expr (Csyntax.Efield b i) ty =>
match typeof b with
| Tstruct _ fld =>
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 87cdb21d..2c010cb4 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -197,9 +197,7 @@ Proof.
intros. inversion H; subst; clear H; simpl in H0.
left; exists id; auto.
left; exists id; auto.
- monadInv H0. right. exists x; split; auto.
- simpl. monadInv H0. right. exists x1; split; auto.
- simpl. rewrite EQ; rewrite EQ1. simpl. auto.
+ monadInv H0. right. exists x; split; auto.
rewrite H4 in H0. monadInv H0. right.
exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto.
simpl. rewrite H4. rewrite EQ. rewrite EQ1. auto.
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index a25c5b8b..75dbc145 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -482,7 +482,7 @@ Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop :=
(TR: transl_exprlist al = OK tal),
Csharpminor.eval_exprlist tprog te m tal vl.
-(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop).*)
+(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop). *)
Lemma transl_Econst_int_correct:
forall (i : int) (ty : type),
@@ -565,6 +565,38 @@ Proof.
eapply transl_binop_correct; eauto.
Qed.
+Lemma transl_Econdition_true_correct:
+ forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v2 : val),
+ Csem.eval_expr ge e m a1 v1 ->
+ eval_expr_prop a1 v1 ->
+ is_true v1 (typeof a1) ->
+ Csem.eval_expr ge e m a2 v2 ->
+ eval_expr_prop a2 v2 ->
+ eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v2.
+Proof.
+ intros; red; intros. inv WT. monadInv TR.
+ exploit make_boolean_correct_true. eapply H0; eauto. eauto.
+ intros [vb [EVAL ISTRUE]].
+ eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto.
+ simpl. eauto.
+Qed.
+
+Lemma transl_Econdition_false_correct:
+ forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v3 : val),
+ Csem.eval_expr ge e m a1 v1 ->
+ eval_expr_prop a1 v1 ->
+ is_false v1 (typeof a1) ->
+ Csem.eval_expr ge e m a3 v3 ->
+ eval_expr_prop a3 v3 ->
+ eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v3.
+Proof.
+ intros; red; intros. inv WT. monadInv TR.
+ exploit make_boolean_correct_false. eapply H0; eauto. eauto.
+ intros [vb [EVAL ISTRUE]].
+ eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto.
+ simpl. eauto.
+Qed.
+
Lemma transl_Eorbool_1_correct:
forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
Csem.eval_expr ge e m a1 v1 ->
@@ -681,20 +713,6 @@ Proof.
eauto.
Qed.
-Lemma transl_Eindex_correct:
- forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 : val) (l : block)
- (ofs : int),
- Csem.eval_expr ge e m a1 v1 ->
- eval_expr_prop a1 v1 ->
- Csem.eval_expr ge e m a2 v2 ->
- eval_expr_prop a2 v2 ->
- sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) ->
- eval_lvalue_prop (Expr (Eindex a1 a2) ty) l ofs.
-Proof.
- intros; red; intros. inversion WT; clear WT; subst. simpl in TR. monadInv TR.
- eapply (make_add_correct tprog); eauto.
-Qed.
-
Lemma transl_Efield_struct_correct:
forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
(ofs : int) (id : ident) (fList : fieldlist) (delta : Z),
@@ -736,6 +754,8 @@ Proof
transl_Esizeof_correct
transl_Eunop_correct
transl_Ebinop_correct
+ transl_Econdition_true_correct
+ transl_Econdition_false_correct
transl_Eorbool_1_correct
transl_Eorbool_2_correct
transl_Eandbool_1_correct
@@ -744,7 +764,6 @@ Proof
transl_Evar_local_correct
transl_Evar_global_correct
transl_Ederef_correct
- transl_Eindex_correct
transl_Efield_struct_correct
transl_Efield_union_correct).
@@ -761,6 +780,8 @@ Proof
transl_Esizeof_correct
transl_Eunop_correct
transl_Ebinop_correct
+ transl_Econdition_true_correct
+ transl_Econdition_false_correct
transl_Eorbool_1_correct
transl_Eorbool_2_correct
transl_Eandbool_1_correct
@@ -769,7 +790,6 @@ Proof
transl_Evar_local_correct
transl_Evar_global_correct
transl_Ederef_correct
- transl_Eindex_correct
transl_Efield_struct_correct
transl_Efield_union_correct).
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index ee1b8617..ac790470 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -150,7 +150,7 @@ with expr_descr : Set :=
| Eunop: unary_operation -> expr -> expr_descr (**r unary operation *)
| Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *)
| Ecast: type -> expr -> expr_descr (**r type cast ([(ty) e]) *)
- | Eindex: expr -> expr -> expr_descr (**r array indexing ([e1[e2]]) *)
+ | Econdition: expr -> expr -> expr -> expr_descr (**r conditional ([e1 ? e2 : e3]) *)
| Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *)
| Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *)
| Esizeof: type -> expr_descr (**r size of a type *)
@@ -331,6 +331,16 @@ Proof.
generalize (align_le pos (alignof t) (alignof_pos t)). omega.
Qed.
+Lemma sizeof_struct_incr:
+ forall fld pos, pos <= sizeof_struct fld pos.
+Proof.
+ induction fld; intros; simpl. omega.
+ eapply Zle_trans. 2: apply IHfld.
+ apply Zle_trans with (align pos (alignof t)).
+ apply align_le. apply alignof_pos.
+ assert (sizeof t > 0) by apply sizeof_pos. omega.
+Qed.
+
(** Byte offset for a field in a struct or union.
Field are laid out consecutively, and padding is inserted
to align each field to the natural alignment for its type. *)
@@ -350,6 +360,86 @@ Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
Definition field_offset (id: ident) (fld: fieldlist) : res Z :=
field_offset_rec id fld 0.
+Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type :=
+ match fld with
+ | Fnil => Error (MSG "Unknown field " :: CTX id :: nil)
+ | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld'
+ end.
+
+(** Some sanity checks about field offsets. First, field offsets are
+ within the range of acceptable offsets. *)
+
+Remark field_offset_rec_in_range:
+ forall id ofs ty fld pos,
+ field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty ->
+ pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
+Proof.
+ intros until ty. induction fld; simpl.
+ congruence.
+ destruct (ident_eq id i); intros.
+ inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
+ exploit IHfld; eauto. intros [A B]. split; auto.
+ eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
+ apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
+Qed.
+
+Lemma field_offset_in_range:
+ forall id fld ofs ty,
+ field_offset id fld = OK ofs -> field_type id fld = OK ty ->
+ 0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
+Proof.
+ intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
+Qed.
+
+(** Second, two distinct fields do not overlap *)
+
+Lemma field_offset_no_overlap:
+ forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
+ field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
+ field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
+ id1 <> id2 ->
+ ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
+Proof.
+ intros until ty2. intros fld0 A B C D NEQ.
+ assert (forall fld pos,
+ field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
+ field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
+ ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
+ induction fld; intro pos; simpl. congruence.
+ destruct (ident_eq id1 i); destruct (ident_eq id2 i).
+ congruence.
+ subst i. intros. inv H; inv H0.
+ exploit field_offset_rec_in_range; eauto. tauto.
+ subst i. intros. inv H1; inv H2.
+ exploit field_offset_rec_in_range; eauto. tauto.
+ intros. eapply IHfld; eauto.
+
+ apply H with fld0 0; auto.
+Qed.
+
+(** Third, if a struct is a prefix of another, the offsets of fields
+ in common is the same. *)
+
+Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
+ match fld1 with
+ | Fnil => fld2
+ | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2)
+ end.
+
+Lemma field_offset_prefix:
+ forall id ofs fld2 fld1,
+ field_offset id fld1 = OK ofs ->
+ field_offset id (fieldlist_app fld1 fld2) = OK ofs.
+Proof.
+ intros until fld2.
+ assert (forall fld1 pos,
+ field_offset_rec id fld1 pos = OK ofs ->
+ field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
+ induction fld1; intros pos; simpl. congruence.
+ destruct (ident_eq id i); auto.
+ intros. unfold field_offset; auto.
+Qed.
+
(** The [access_mode] function describes how a variable of the given
type must be accessed:
- [By_value ch]: access by value, i.e. by loading from the address
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index b4dd2904..c03552c6 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -56,9 +56,9 @@ Inductive wt_expr: expr -> Prop :=
| wt_Ecast: forall e ty ty',
wt_expr e ->
wt_expr (Expr (Ecast ty' e) ty)
- | wt_Eindex: forall e1 e2 ty,
- wt_expr e1 -> wt_expr e2 ->
- wt_expr (Expr (Eindex e1 e2) ty)
+ | wt_Econdition: forall e1 e2 e3 ty,
+ wt_expr e1 -> wt_expr e2 -> wt_expr e3 ->
+ wt_expr (Expr (Econdition e1 e2 e3) ty)
| wt_Eandbool: forall e1 e2 ty,
wt_expr e1 -> wt_expr e2 ->
wt_expr (Expr (Eandbool e1 e2) ty)
@@ -296,7 +296,7 @@ with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool :=
| Csyntax.Eunop op b => typecheck_expr b
| Csyntax.Ebinop op b c => typecheck_expr b && typecheck_expr c
| Csyntax.Ecast ty b => typecheck_expr b
- | Csyntax.Eindex b c => typecheck_expr b && typecheck_expr c
+ | Csyntax.Econdition b c d => typecheck_expr b && typecheck_expr c && typecheck_expr d
| Csyntax.Eandbool b c => typecheck_expr b && typecheck_expr c
| Csyntax.Eorbool b c => typecheck_expr b && typecheck_expr c
| Csyntax.Esizeof ty => true
generated by cgit (git 2.34.1) at 2024-06-02 17:29:18 +0000