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 --- powerpc/Asm.v | 8 +------- powerpc/PrintAsm.ml | 49 +++++++++++++++++++++++++++++++------------------ powerpc/SelectOp.vp | 15 ++++++++++++++- powerpc/SelectOpproof.v | 25 +++++++++++++++++++++++++ 4 files changed, 71 insertions(+), 26 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 7174f79d..2d71ca95 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -508,12 +508,6 @@ Definition compare_float (rs: regset) (v1 v2: val) := #CR0_2 <- (Val.cmpf Ceq v1 v2) #CR0_3 <- Vundef. -Definition val_cond_reg (rs: regset) := - Val.or (Val.shl rs#CR0_0 (Vint (Int.repr 31))) - (Val.or (Val.shl rs#CR0_1 (Vint (Int.repr 30))) - (Val.or (Val.shl rs#CR0_2 (Vint (Int.repr 29))) - (Val.shl rs#CR0_3 (Vint (Int.repr 28))))). - (** Execution of a single instruction [i] in initial state [rs] and [m]. Return updated state. For instructions that correspond to actual PowerPC instructions, the cases are @@ -968,7 +962,7 @@ Ltac Equalities := exploit external_call_determ. eexact H3. eexact H8. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. (* trace length *) - inv H; simpl. + red; intros. inv H; simpl. omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index e566e3c8..f6c1c492 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -202,8 +202,8 @@ let name_of_section_MacOS = function let name_of_section_Linux = function | Section_text -> ".text" - | Section_data i -> ".data" (*if i then ".data" else ".bss"*) - | Section_small_data i -> ".sdata" (*if i then ".sdata" else ".sbss"*) + | Section_data i -> if i then ".data" else "COMM" + | Section_small_data i -> if i then ".sdata" else "COMM" | Section_const -> ".rodata" | Section_small_const -> ".sdata2" | Section_string -> ".rodata" @@ -238,7 +238,9 @@ let name_of_section = | Diab -> name_of_section_Diab let section oc sec = - fprintf oc " %s\n" (name_of_section sec) + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name (* Encoding masks for rlwinm instructions *) @@ -663,8 +665,8 @@ let print_instruction oc = function | Plwzx(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmfcrbit(r1, bit) -> - fprintf oc " mfcr %a\n" ireg GPR12; - fprintf oc " rlwinm %a, %a, %d, 31, 31\n" ireg r1 ireg GPR12 (1 + num_crbit bit) + fprintf oc " mfcr %a\n" ireg r1; + fprintf oc " rlwinm %a, %a, %d, 31, 31\n" ireg r1 ireg r1 (1 + num_crbit bit) | Pmflr(r1) -> fprintf oc " mflr %a\n" ireg r1 | Pmr(r1, r2) -> @@ -1012,21 +1014,32 @@ let print_var oc (name, v) = let init = match v.gvar_init with [Init_space _] -> false | _ -> true in let sec = - Sections.section_for_variable name init - and align = + Sections.section_for_variable name init in + let align = match C2C.atom_alignof name with | Some a -> log2 a - | None -> 3 (* 8-alignment is a safe default *) - in - section oc sec; - fprintf oc " .align %d\n" align; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_init_data oc name v.gvar_init; - if target <> MacOS then begin - fprintf oc " .type %a, @object\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name + | None -> 3 in (* 8-alignment is a safe default *) + let name_sec = + name_of_section sec in + if name_sec <> "COMM" then begin + fprintf oc " %s\n" name_sec; + fprintf oc " .align %d\n" align; + if not (C2C.atom_is_static name) then + fprintf oc " .globl %a\n" symbol name; + fprintf oc "%a:\n" symbol name; + print_init_data oc name v.gvar_init; + if target <> MacOS then begin + fprintf oc " .type %a, @object\n" symbol name; + fprintf oc " .size %a, . - %a\n" symbol name symbol name + end + end else begin + let sz = + match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in + fprintf oc " %s %a, %ld, %d\n" + (if C2C.atom_is_static name then ".lcomm" else ".comm") + symbol name + (camlint_of_coqint sz) + (1 lsl align) end let print_program oc p = diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 3bb55449..08968f7c 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -69,7 +69,20 @@ Nondetfunction notint (e: expr) := | _ => Elet e (Eop Onor (Eletvar O ::: Eletvar O ::: Enil)) end. -(** ** Boolean negation *) +(** ** Boolean value and boolean negation *) + +Fixpoint boolval (e: expr) {struct e} : expr := + let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil + | Eop (Ocmp cond) args => + Eop (Ocmp cond) args + | Econdition e1 e2 e3 => + Econdition e1 (boolval e2) (boolval e3) + | _ => + default + end. Fixpoint notbool (e: expr) {struct e} : expr := let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index cc14d339..59f2a419 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -148,6 +148,31 @@ Proof. simpl. destruct x; simpl; auto. rewrite Int.or_idem. auto. Qed. +Theorem eval_boolval: unary_constructor_sound boolval Val.boolval. +Proof. + assert (DFL: + forall le a x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Cne Int.zero)) (a ::: Enil)) v + /\ Val.lessdef (Val.boolval x) v). + intros. TrivialExists. simpl. destruct x; simpl; auto. + + red. induction a; simpl; intros; eauto. destruct o; eauto. +(* intconst *) + destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. +(* cmp *) + inv H. simpl in H5. + destruct (eval_condition c vl m) as []_eqn. + TrivialExists. simpl. inv H5. rewrite Heqo. destruct b; auto. + simpl in H5. inv H5. + exists Vundef; split; auto. EvalOp; simpl. rewrite Heqo; auto. + +(* condition *) + inv H. destruct v1. + exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. + exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. +Qed. + Theorem eval_notbool: unary_constructor_sound notbool Val.notbool. Proof. assert (DFL: -- cgit