From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: Merge of the "volatile" branch: - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) (limited to 'backend/Cminor.v') diff --git a/backend/Cminor.v b/backend/Cminor.v index c9ee5b5c..6d288a9e 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -44,6 +44,7 @@ Inductive unary_operation : Type := | Ocast8signed: unary_operation (**r 8-bit sign extension *) | Ocast16unsigned: unary_operation (**r 16-bit zero extension *) | Ocast16signed: unary_operation (**r 16-bit sign extension *) + | Oboolval: unary_operation (**r 0 if null, 1 if non-null *) | Onegint: unary_operation (**r integer opposite *) | Onotbool: unary_operation (**r boolean negation *) | Onotint: unary_operation (**r bitwise complement *) @@ -103,6 +104,7 @@ Inductive stmt : Type := | Sstore : memory_chunk -> expr -> expr -> stmt | Scall : option ident -> signature -> expr -> list expr -> stmt | Stailcall: signature -> expr -> list expr -> stmt + | Sbuiltin : option ident -> external_function -> list expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -228,6 +230,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val := | Ocast8signed => Some (Val.sign_ext 8 arg) | Ocast16unsigned => Some (Val.zero_ext 16 arg) | Ocast16signed => Some (Val.sign_ext 16 arg) + | Oboolval => Some(Val.boolval arg) | Onegint => Some (Val.negint arg) | Onotbool => Some (Val.notbool arg) | Onotint => Some (Val.notint arg) @@ -401,6 +404,12 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) E0 (Callstate fd vargs (call_cont k) m') + | step_builtin: forall f optid ef bl k sp e m vargs t vres m', + eval_exprlist sp e m bl vargs -> + external_call ef ge vargs m t vres m' -> + step (State f (Sbuiltin optid ef bl) k sp e m) + t (State f Sskip k sp (set_optvar optid vres e) m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) @@ -505,9 +514,11 @@ Proof. intros. subst. inv H0. exists s1; auto. inversion H; subst; auto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State f Sskip k sp (set_optvar optid vres2 e) m2). econstructor; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - inv H; simpl; try omega. eapply external_call_trace_length; eauto. + red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto. Qed. (** * Alternate operational semantics (big-step) *) @@ -608,6 +619,12 @@ with exec_stmt: eval_funcall m fd vargs t m' vres -> e' = set_optvar optid vres e -> exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal + | exec_Sbuiltin: + forall f sp e m optid ef bl t m' vargs vres e', + eval_exprlist ge sp e m bl vargs -> + external_call ef ge vargs m t vres m' -> + e' = set_optvar optid vres e -> + exec_stmt f sp e m (Sbuiltin optid ef bl) t e' m' Out_normal | exec_Sifthenelse: forall f sp e m a s1 s2 v b t e' m' out, eval_expr ge sp e m a v -> @@ -884,6 +901,11 @@ Proof. constructor. reflexivity. traceEq. subst e'. constructor. +(* builtin *) + econstructor; split. + apply star_one. econstructor; eauto. + subst e'. constructor. + (* ifthenelse *) destruct (H2 k) as [S [A B]]. exists S; split. -- cgit