diff options
| -rw-r--r-- | cfrontend/Cexec.v | 20 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 16 | ||||
| -rw-r--r-- | cfrontend/Cstrategy.v | 76 | ||||
| -rw-r--r-- | cfrontend/Csyntax.v | 7 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 8 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 30 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 4 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 24 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 18 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 28 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 |
11 files changed, 109 insertions, 124 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 0e070934..c33068d9 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -797,7 +797,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - if b then topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0) + if b then topred (Rred (Eparen r2 type_bool ty) m E0) else topred (Rred (Eval (Vint Int.zero) ty) m E0) | None => incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m) @@ -807,7 +807,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | Some(v1, ty1) => do b <- bool_val v1 ty1; if b then topred (Rred (Eval (Vint Int.one) ty) m E0) - else topred (Rred (Eparen (Eparen r2 type_bool) ty) m E0) + else topred (Rred (Eparen r2 type_bool ty) m E0) | None => incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m) end @@ -815,7 +815,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - topred (Rred (Eparen (if b then r2 else r3) ty) m E0) + topred (Rred (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end @@ -869,13 +869,13 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | None => incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) end - | RV, Eparen r1 ty => + | RV, Eparen r1 tycast ty => match is_val r1 with | Some (v1, ty1) => - do v <- sem_cast v1 ty1 ty; + do v <- sem_cast v1 ty1 tycast; topred (Rred (Eval v ty) m E0) | None => - incontext (fun x => Eparen x ty) (step_expr RV r1 m) + incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m) end | RV, Ecall r1 rargs ty => match is_val r1, is_val_list rargs with @@ -1010,8 +1010,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := ty = ty1 /\ deref_loc ge ty m b ofs t v1 /\ possible_trace w t w' | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty - | Eparen (Eval v1 ty1) ty => - exists v, sem_cast v1 ty1 ty = Some v + | Eparen (Eval v1 ty1) tycast ty => + exists v, sem_cast v1 ty1 tycast = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, @@ -1543,7 +1543,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* paren *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_cast v ty' ty) as [v'|] eqn:?... + destruct (sem_cast v ty' tycast) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1791,7 +1791,7 @@ Proof. eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto. destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. (* paren *) - eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto. + eapply reducts_incl_trans with (C' := fun x => Eparen x tycast ty); eauto. destruct (is_val (C a)) as [[v ty']|] eqn:?; eauto. induction 1; simpl; intros. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 55c37c99..06cea006 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -248,7 +248,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := | red_seqand_true: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some true -> rred (Eseqand (Eval v1 ty1) r2 ty) m - E0 (Eparen (Eparen r2 type_bool) ty) m + E0 (Eparen r2 type_bool ty) m | red_seqand_false: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some false -> rred (Eseqand (Eval v1 ty1) r2 ty) m @@ -260,11 +260,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := | red_seqor_false: forall v1 ty1 r2 ty m, bool_val v1 ty1 = Some false -> rred (Eseqor (Eval v1 ty1) r2 ty) m - E0 (Eparen (Eparen r2 type_bool) ty) m + E0 (Eparen r2 type_bool ty) m | red_condition: forall v1 ty1 r1 r2 ty b m, bool_val v1 ty1 = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m - E0 (Eparen (if b then r1 else r2) ty) m + E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m @@ -295,9 +295,9 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := typeof r2 = ty -> rred (Ecomma (Eval v ty1) r2 ty) m E0 r2 m - | red_paren: forall v1 ty1 ty m v, - sem_cast v1 ty1 ty = Some v -> - rred (Eparen (Eval v1 ty1) ty) m + | red_paren: forall v1 ty1 ty2 ty m v, + sem_cast v1 ty1 ty2 = Some v -> + rred (Eparen (Eval v1 ty1) ty2 ty) m E0 (Eval v ty) m | red_builtin: forall ef tyargs el ty m vargs t vres m', cast_arguments el tyargs vargs -> @@ -379,8 +379,8 @@ Inductive context: kind -> kind -> (expr -> expr) -> Prop := contextlist k C -> context k RV (fun x => Ebuiltin ef tyargs (C x) ty) | ctx_comma: forall k C e2 ty, context k RV C -> context k RV (fun x => Ecomma (C x) e2 ty) - | ctx_paren: forall k C ty, - context k RV C -> context k RV (fun x => Eparen (C x) ty) + | ctx_paren: forall k C tycast ty, + context k RV C -> context k RV (fun x => Eparen (C x) tycast ty) with contextlist: kind -> (expr -> exprlist) -> Prop := | ctx_list_head: forall k C el, diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 676f3faf..f8c3963e 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -68,7 +68,7 @@ Fixpoint simple (a: expr) : bool := | Ecomma _ _ _ => false | Ecall _ _ _ => false | Ebuiltin _ _ _ _ => false - | Eparen _ _ => false + | Eparen _ _ _ => false end. Fixpoint simplelist (rl: exprlist) : bool := @@ -199,8 +199,8 @@ Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := leftcontext k RV (fun x => Ebuiltin ef tyargs (C x) ty) | lctx_comma: forall k C e2 ty, leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty) - | lctx_paren: forall k C ty, - leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) ty) + | lctx_paren: forall k C tycast ty, + leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) tycast ty) with leftcontextlist: kind -> (expr -> exprlist) -> Prop := | lctx_list_head: forall k C el, @@ -248,7 +248,7 @@ Inductive estep: state -> trace -> state -> Prop := eval_simple_rvalue e m r1 v -> bool_val v (typeof r1) = Some true -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) - E0 (ExprState f (C (Eparen (Eparen r2 type_bool) ty)) k e m) + E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_seqand_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> @@ -267,14 +267,14 @@ Inductive estep: state -> trace -> state -> Prop := eval_simple_rvalue e m r1 v -> bool_val v (typeof r1) = Some false -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) - E0 (ExprState f (C (Eparen (Eparen r2 type_bool) ty)) k e m) + E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> bool_val v (typeof r1) = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) - E0 (ExprState f (C (Eparen (if b then r2 else r3) ty)) k e m) + E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m) | step_assign: forall f C l r ty k e m b ofs v v' t m', leftcontext RV RV C -> @@ -351,11 +351,11 @@ Inductive estep: state -> trace -> state -> Prop := estep (ExprState f (C (Ecomma r1 r2 ty)) k e m) E0 (ExprState f (C r2) k e m) - | step_paren: forall f C r ty k e m v1 v, + | step_paren: forall f C r tycast ty k e m v1 v, leftcontext RV RV C -> eval_simple_rvalue e m r v1 -> - sem_cast v1 (typeof r) ty = Some v -> - estep (ExprState f (C (Eparen r ty)) k e m) + sem_cast v1 (typeof r) tycast = Some v -> + estep (ExprState f (C (Eparen r tycast ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) | step_call: forall f C rf rargs ty k e m targs tres cconv vf vargs fd, @@ -557,8 +557,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := /\ deref_loc ge ty m b ofs t v1 | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty - | Eparen (Eval v1 ty1) ty => - exists v, sem_cast v1 ty1 ty = Some v + | Eparen (Eval v1 ty1) ty2 ty => + exists v, sem_cast v1 ty1 ty2 = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, @@ -1039,7 +1039,7 @@ Definition simple_side_effect (r: expr) : Prop := | Ecomma r1 r2 _ => simple r1 = true | Ecall r1 rl _ => simple r1 = true /\ simplelist rl = true | Ebuiltin ef tyargs rl _ => simplelist rl = true - | Eparen r1 _ => simple r1 = true + | Eparen r1 _ _ => simple r1 = true | _ => False end. @@ -1114,7 +1114,7 @@ Ltac Base := Base. right; exists (fun x => Ebuiltin ef tyargs (C' x) ty); exists a'. rewrite D; simpl; auto. (* rparen *) - Kind. Rec H RV C (fun x => (Eparen x ty)). Base. + Kind. Rec H RV C (fun x => (Eparen x tycast ty)). Base. (* cons *) destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]]. eapply contextlist'_head; eauto. auto. @@ -1253,7 +1253,7 @@ Proof. left; apply step_rred; eauto. econstructor; eauto. auto. (* paren *) eapply plus_right; eauto. - eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x ty)); eauto. + eapply eval_simple_rvalue_steps with (C := fun x => C(Eparen x tycast ty)); eauto. left; apply step_rred; eauto. econstructor; eauto. auto. (* call *) exploit eval_simple_list_implies; eauto. intros [vl' [A B]]. @@ -1383,7 +1383,7 @@ Proof. econstructor; econstructor; eapply step_builtin; eauto. eapply can_eval_simple_list; eauto. (* paren *) - exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x ty))); eauto. + exploit (simple_can_eval_rval f k e m b (fun x => C(Eparen x tycast ty))); eauto. intros [v1 [E1 S1]]. exploit safe_inv. eexact S1. eauto. simpl. intros [v CAST]. econstructor; econstructor; eapply step_paren; eauto. @@ -1688,23 +1688,21 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := | eval_cast: forall e m a t m' a' ty, eval_expr e m RV a t m' a' -> eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) - | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v, + | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> - sem_cast v2 (typeof a2) type_bool = Some v' -> - sem_cast v' type_bool ty = Some v -> + sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some false -> eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) - | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v' v, + | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> - sem_cast v2 (typeof a2) type_bool = Some v' -> - sem_cast v' type_bool ty = Some v -> + sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> @@ -2257,18 +2255,13 @@ Proof. (* seqand true *) exploit (H0 (fun x => C(Eseqand x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))). + exploit (H4 (fun x => C(Eparen x type_bool ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. simpl; intuition. eapply star_trans. eexact D. eapply star_left. left; eapply step_seqand_true; eauto. rewrite B; auto. - eapply star_trans. eexact G. - set (C' := fun x => C (Eparen x ty)). - change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)). - eapply star_two. - left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor. - rewrite F; eauto. - unfold C'. left; eapply step_paren; eauto. constructor. - eauto. eauto. eauto. traceEq. + eapply star_right. eexact G. + left; eapply step_paren; eauto. rewrite F; eauto. + eauto. eauto. traceEq. (* seqand false *) exploit (H0 (fun x => C(Eseqand x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2278,18 +2271,13 @@ Proof. (* seqor false *) exploit (H0 (fun x => C(Eseqor x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H4 (fun x => C(Eparen (Eparen x type_bool) ty))). + exploit (H4 (fun x => C(Eparen x type_bool ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. simpl; intuition. eapply star_trans. eexact D. eapply star_left. left; eapply step_seqor_false; eauto. rewrite B; auto. - eapply star_trans. eexact G. - set (C' := fun x => C (Eparen x ty)). - change (C (Eparen (Eparen a2' type_bool) ty)) with (C' (Eparen a2' type_bool)). - eapply star_two. - left; eapply step_paren; eauto. unfold C'; eapply leftcontext_compose; eauto. repeat constructor. - rewrite F; eauto. - unfold C'. left; eapply step_paren; eauto. constructor. - eauto. eauto. eauto. traceEq. + eapply star_right. eexact G. + left; eapply step_paren; eauto. rewrite F; eauto. + eauto. eauto. traceEq. (* seqor true *) exploit (H0 (fun x => C(Eseqor x a2 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. @@ -2299,7 +2287,7 @@ Proof. (* condition *) exploit (H0 (fun x => C(Econdition x a2 a3 ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. - exploit (H4 (fun x => C(Eparen x ty))). + exploit (H4 (fun x => C(Eparen x ty ty))). eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. simpl. split; auto. split; auto. eapply star_trans. eexact D. @@ -2684,7 +2672,7 @@ Fixpoint esize (a: expr) : nat := | Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat | Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat | Ebuiltin ef tyargs rl _ => S(esizelist rl) - | Eparen r1 _ => S(esize r1) + | Eparen r1 _ _ => S(esize r1) end with esizelist (el: exprlist) : nat := @@ -2807,7 +2795,7 @@ Proof. eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_seqand_true; eauto. rewrite Q; eauto. reflexivity. - eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto. + eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* seqor left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. @@ -2820,7 +2808,7 @@ Proof. eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_seqor_false; eauto. rewrite Q; eauto. reflexivity. - eapply COE with (C := fun x => (C (Eparen (Eparen x type_bool) ty))). eauto. + eapply COE with (C := fun x => (C (Eparen x type_bool ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* condition top *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. @@ -2833,7 +2821,7 @@ Proof. eapply forever_N_plus. eapply plus_right. eexact R. left; eapply step_condition; eauto. rewrite Q; eauto. reflexivity. - eapply COE with (C := fun x => (C (Eparen x ty))). eauto. + eapply COE with (C := fun x => (C (Eparen x ty ty))). eauto. eapply leftcontext_compose; eauto. repeat constructor. traceEq. (* assign left *) eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index a926bc3b..fa74f11c 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -61,7 +61,7 @@ Inductive expr : Type := (**r builtin function call *) | Eloc (b: block) (ofs: int) (ty: type) (**r memory location, result of evaluating a l-value *) - | Eparen (r: expr) (ty: type) (**r marked subexpression *) + | Eparen (r: expr) (tycast: type) (ty: type) (**r marked subexpression *) with exprlist : Type := | Enil @@ -87,7 +87,8 @@ but appear during reduction. These forms are: - [Eval v] where [v] is a pointer or [Vundef]. ([Eval] of an integer or float value can occur in a source term and represents a numeric literal.) - [Eloc b ofs], which appears during reduction of l-values. -- [Eparen r], which appears during reduction of conditionals [r1 ? r2 : r3]. +- [Eparen r tycast ty], which appears during reduction of conditionals + [r1 ? r2 : r3] as well as sequential `and' / `or'. Some C expressions are derived forms. Array access [r1[r2]] is expressed as [*(r1 + r2)]. @@ -128,7 +129,7 @@ Definition typeof (a: expr) : type := | Ecomma _ _ ty => ty | Ecall _ _ ty => ty | Ebuiltin _ _ _ ty => ty - | Eparen _ ty => ty + | Eparen _ _ ty => ty end. (** ** Statements *) diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 3454ddcf..6f193cd9 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -88,7 +88,7 @@ Fixpoint constval (a: expr) : res val := do v1 <- constval r1; do v2 <- constval r2; match bool_val v1 (typeof r1) with - | Some true => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty + | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") end @@ -96,7 +96,7 @@ Fixpoint constval (a: expr) : res val := do v1 <- constval r1; do v2 <- constval r2; match bool_val v1 (typeof r1) with - | Some false => do v3 <- do_cast v2 (typeof r2) type_bool; do_cast v3 type_bool ty + | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") end @@ -126,8 +126,8 @@ Fixpoint constval (a: expr) : res val := | _ => Error(msg "ill-typed field access") end - | Eparen r ty => - do v <- constval r; do_cast v (typeof r) ty + | Eparen r tycast ty => + do v <- constval r; do_cast v (typeof r) tycast | _ => Error(msg "not a compile-time constant") end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 16004fc0..73fd90b7 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -63,7 +63,7 @@ Fixpoint simple (a: expr) : Prop := | Ecomma r1 r2 _ => simple r1 /\ simple r2 | Ecall _ _ _ => False | Ebuiltin _ _ _ _ => False - | Eparen r1 _ => simple r1 + | Eparen r1 _ _ => simple r1 end. (** A big-step semantics for simple expressions. Similar to the @@ -126,21 +126,19 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) | esr_alignof: forall ty1 ty, eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))) - | esr_seqand_true: forall r1 r2 ty v1 v2 v3 v4, + | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> - sem_cast v3 type_bool ty = Some v4 -> - eval_simple_rvalue (Eseqand r1 r2 ty) v4 + eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero) - | esr_seqor_false: forall r1 r2 ty v1 v2 v3 v4, + | esr_seqor_false: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> - sem_cast v3 type_bool ty = Some v4 -> - eval_simple_rvalue (Eseqor r1 r2 ty) v4 + eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) @@ -152,9 +150,9 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_comma: forall r1 r2 ty v1 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> eval_simple_rvalue (Ecomma r1 r2 ty) v - | esr_paren: forall r ty v v', - eval_simple_rvalue r v -> sem_cast v (typeof r) ty = Some v' -> - eval_simple_rvalue (Eparen r ty) v'. + | esr_paren: forall r tycast ty v v', + eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' -> + eval_simple_rvalue (Eparen r tycast ty) v'. End SIMPLE_EXPRS. @@ -206,10 +204,10 @@ Proof. inv EV. econstructor; eauto. constructor. inv EV. econstructor; eauto. constructor. constructor. inv EV. econstructor; eauto. constructor. - inv EV. inv H2. eapply esr_seqand_true; eauto. constructor. + inv EV. eapply esr_seqand_true; eauto. constructor. inv EV. eapply esr_seqand_false; eauto. constructor. inv EV. eapply esr_seqor_true; eauto. constructor. - inv EV. inv H2. eapply esr_seqor_false; eauto. constructor. + inv EV. eapply esr_seqor_false; eauto. constructor. inv EV. eapply esr_condition; eauto. constructor. inv EV. constructor. inv EV. constructor. @@ -413,16 +411,16 @@ Proof. (* seqand *) 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. + assert (b = true) by congruence. subst b. + 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 *) 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. + assert (b = false) by congruence. subst b. + 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. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 4e0ee7f3..e1b53af8 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -272,8 +272,8 @@ let rec expr p (prec, e) = fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) - | Eparen(a1, ty) -> - fprintf p "(%s) %a" (name_type ty) expr (prec', a1) + | Eparen(a1, tycast, ty) -> + fprintf p "(%s) %a" (name_type tycast) expr (prec', a1) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 05d9c860..df33d727 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -197,8 +197,8 @@ Definition make_assign (l r: expr) : statement := *) Inductive set_destination : Type := - | SDbase (ty: type) (tmp: ident) - | SDcons (ty: type) (tmp: ident) (sd: set_destination). + | SDbase (tycast ty: type) (tmp: ident) + | SDcons (tycast ty: type) (tmp: ident) (sd: set_destination). Inductive destination : Type := | For_val @@ -209,8 +209,8 @@ Definition dummy_expr := Econst_int Int.zero type_int32s. Fixpoint do_set (sd: set_destination) (a: expr) : list statement := match sd with - | SDbase ty tmp => Sset tmp (Ecast a ty) :: nil - | SDcons ty tmp sd' => Sset tmp (Ecast a ty) :: do_set sd' (Etempvar tmp ty) + | SDbase tycast ty tmp => Sset tmp (Ecast a tycast) :: nil + | SDcons tycast ty tmp sd' => Sset tmp (Ecast a tycast) :: do_set sd' (Etempvar tmp ty) end. Definition finish (dst: destination) (sl: list statement) (a: expr) := @@ -221,11 +221,11 @@ Definition finish (dst: destination) (sl: list statement) (a: expr) := end. Definition sd_temp (sd: set_destination) := - match sd with SDbase _ tmp => tmp | SDcons _ tmp _ => tmp end. + match sd with SDbase _ _ tmp => tmp | SDcons _ _ tmp _ => tmp end. Definition sd_seqbool_val (tmp: ident) (ty: type) := - SDcons type_bool tmp (SDbase ty tmp). + SDbase type_bool ty tmp. Definition sd_seqbool_set (ty: type) (sd: set_destination) := - let tmp := sd_temp sd in SDcons type_bool tmp (SDcons ty tmp sd). + let tmp := sd_temp sd in SDcons type_bool ty tmp sd. Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with @@ -311,8 +311,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement match dst with | For_val => do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (SDbase ty t)) r2; - do (sl3, a3) <- transl_expr (For_set (SDbase ty t)) r3; + do (sl2, a2) <- transl_expr (For_set (SDbase ty ty t)) r2; + do (sl3, a3) <- transl_expr (For_set (SDbase ty ty t)) r3; ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, Etempvar t ty) | For_effects => @@ -322,8 +322,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement dummy_expr) | For_set sd => do t <- gensym ty; - do (sl2, a2) <- transl_expr (For_set (SDcons ty t sd)) r2; - do (sl3, a3) <- transl_expr (For_set (SDcons ty t sd)) r3; + do (sl2, a2) <- transl_expr (For_set (SDcons ty ty t sd)) r2; + do (sl3, a3) <- transl_expr (For_set (SDcons ty ty t sd)) r3; ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil, dummy_expr) end @@ -399,7 +399,7 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement | For_effects => ret (sl ++ Sbuiltin None ef tyargs al :: nil, dummy_expr) end - | Csyntax.Eparen r1 ty => + | Csyntax.Eparen r1 tycast ty => error (msg "SimplExpr.transl_expr: paren") end diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index c907f77d..3802b957 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -1301,7 +1301,7 @@ Fixpoint esize (a: Csyntax.expr) : nat := | Csyntax.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat | Csyntax.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat | Csyntax.Ebuiltin ef _ rl _ => S(esizelist rl)%nat - | Csyntax.Eparen r1 _ => S(esize r1) + | Csyntax.Eparen r1 _ _ => S(esize r1) end with esizelist (el: Csyntax.exprlist) : nat := @@ -1404,7 +1404,7 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_val with (a1 := dummy_expr); auto. econstructor; eauto. + apply S. apply tr_paren_val with (a1 := a2); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* for effects *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. @@ -1415,7 +1415,7 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_effects with (a1 := dummy_expr); auto. econstructor; eauto. + apply S. apply tr_paren_effects with (a1 := a2); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* for set *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. @@ -1426,9 +1426,8 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto. - apply tr_paren_set with (a1 := a2) (t := sd_temp sd). - apply tr_expr_monotone with tmp2; eauto. auto. auto. auto. + apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply tr_expr_monotone with tmp2; eauto. auto. auto. (* seqand false *) exploit tr_top_leftcontext; eauto. clear H9. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R S]]]]]]]]. @@ -1514,7 +1513,7 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_val with (a1 := dummy_expr); auto. econstructor; eauto. + apply S. apply tr_paren_val with (a1 := a2); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* for effects *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. @@ -1525,7 +1524,7 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_effects with (a1 := dummy_expr); auto. econstructor; eauto. + apply S. apply tr_paren_effects with (a1 := a2); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* for set *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. @@ -1536,8 +1535,7 @@ Proof. apply push_seq. reflexivity. reflexivity. rewrite <- Kseqlist_app. eapply match_exprstates; eauto. - apply S. apply tr_paren_set with (a1 := dummy_expr) (t := sd_temp sd); auto. - apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. + apply S. apply tr_paren_set with (a1 := a2) (t := sd_temp sd); auto. apply tr_expr_monotone with tmp2; eauto. auto. auto. (* condition *) exploit tr_top_leftcontext; eauto. clear H9. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 1ef2e76d..83ddd1f4 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -176,8 +176,8 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> any tmp | tr_condition_val: forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (SDbase ty t)) e2 sl2 a2 tmp2 -> - tr_expr le (For_set (SDbase ty t)) e3 sl3 a3 tmp3 -> + tr_expr le (For_set (SDbase ty ty t)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDbase ty ty t)) e3 sl3 a3 tmp3 -> list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> @@ -196,8 +196,8 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> any tmp | tr_condition_set: forall le sd t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> - tr_expr le (For_set (SDcons ty t sd)) e2 sl2 a2 tmp2 -> - tr_expr le (For_set (SDcons ty t sd)) e3 sl3 a3 tmp3 -> + tr_expr le (For_set (SDcons ty ty t sd)) e2 sl2 a2 tmp2 -> + tr_expr le (For_set (SDcons ty ty t sd)) e3 sl3 a3 tmp3 -> list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp -> @@ -304,19 +304,19 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty) (sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty)) (Etempvar t ty) tmp - | tr_paren_val: forall le e1 ty sl1 a1 t tmp, - tr_expr le (For_set (SDbase ty t)) e1 sl1 a1 tmp -> + | tr_paren_val: forall le e1 tycast ty sl1 a1 t tmp, + tr_expr le (For_set (SDbase tycast ty t)) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le For_val (Csyntax.Eparen e1 ty) + tr_expr le For_val (Csyntax.Eparen e1 tycast ty) sl1 (Etempvar t ty) tmp - | tr_paren_effects: forall le e1 ty sl1 a1 tmp any, + | tr_paren_effects: forall le e1 tycast ty sl1 a1 tmp any, tr_expr le For_effects e1 sl1 a1 tmp -> - tr_expr le For_effects (Csyntax.Eparen e1 ty) sl1 any tmp - | tr_paren_set: forall le t sd e1 ty sl1 a1 tmp any, - tr_expr le (For_set (SDcons ty t sd)) e1 sl1 a1 tmp -> + tr_expr le For_effects (Csyntax.Eparen e1 tycast ty) sl1 any tmp + | tr_paren_set: forall le t sd e1 tycast ty sl1 a1 tmp any, + tr_expr le (For_set (SDcons tycast ty t sd)) e1 sl1 a1 tmp -> In t tmp -> - tr_expr le (For_set sd) (Csyntax.Eparen e1 ty) sl1 any tmp + tr_expr le (For_set sd) (Csyntax.Eparen e1 tycast ty) sl1 any tmp with tr_exprlist: temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop := | tr_nil: forall le tmp, @@ -669,13 +669,13 @@ Proof. Qed. Lemma dest_for_set_condition_val: - forall tmp ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase ty tmp)) g2. + forall tmp tycast ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2. Proof. intros. destruct H. simpl. auto. Qed. Lemma dest_for_set_condition_set: - forall sd tmp ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons ty tmp sd)) g2. + forall sd tmp tycast ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons tycast ty tmp sd)) g2. Proof. intros. destruct H0. simpl. auto. Qed. diff --git a/driver/Interp.ml b/driver/Interp.ml index db4537cb..e277ebe0 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -452,7 +452,7 @@ let diagnose_stuck_expr p ge w f a kont e m = | RV, Eassignop(op, l1, r2, tyres, ty) -> diagnose LV l1 ||| diagnose RV r2 | RV, Epostincr(id, l, ty) -> diagnose LV l | RV, Ecomma(r1, r2, ty) -> diagnose RV r1 - | RV, Eparen(r1, ty) -> diagnose RV r1 + | RV, Eparen(r1, tycast, ty) -> diagnose RV r1 | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs | _, _ -> false in |