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 --- cfrontend/Cminorgen.v | 89 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 55 insertions(+), 34 deletions(-) (limited to 'cfrontend/Cminorgen.v') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 3a8b8575..a849a9ad 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -62,11 +62,11 @@ Definition for_temp (id: ident) : ident := xI id. global variables, stored in the global symbols with the same names. *) Inductive var_info: Type := - | Var_local: memory_chunk -> var_info - | Var_stack_scalar: memory_chunk -> Z -> var_info - | Var_stack_array: Z -> var_info - | Var_global_scalar: memory_chunk -> var_info - | Var_global_array: var_info. + | Var_local (chunk: memory_chunk) + | Var_stack_scalar (chunk: memory_chunk) (ofs: Z) + | Var_stack_array (ofs sz al: Z) + | Var_global_scalar (chunk: memory_chunk) + | Var_global_array. Definition compilenv := PMap.t var_info. @@ -140,6 +140,7 @@ Definition make_unop (op: unary_operation) (e: expr): expr := Inductive approx : Type := | Any (**r any value *) + | Int1 (**r [0] or [1] *) | Int7 (**r [[0,127]] *) | Int8s (**r [[-128,127]] *) | Int8u (**r [[0,255]] *) @@ -153,41 +154,51 @@ Module Approx. Definition bge (x y: approx) : bool := match x, y with | Any, _ => true - | Int7, Int7 => true - | Int8s, (Int7 | Int8s) => true - | Int8u, (Int7 | Int8u) => true - | Int15, (Int7 | Int8u | Int15) => true - | Int16s, (Int7 | Int8s | Int8u | Int15 | Int16s) => true - | Int16u, (Int7 | Int8u | Int15 | Int16u) => true + | Int1, Int1 => true + | Int7, (Int1 | Int7) => true + | Int8s, (Int1 | Int7 | Int8s) => true + | Int8u, (Int1 | Int7 | Int8u) => true + | Int15, (Int1 | Int7 | Int8u | Int15) => true + | Int16s, (Int1 | Int7 | Int8s | Int8u | Int15 | Int16s) => true + | Int16u, (Int1 | Int7 | Int8u | Int15 | Int16u) => true | Float32, Float32 => true | _, _ => false end. Definition lub (x y: approx) : approx := match x, y with + | Int1, Int1 => Int1 + | Int1, Int7 => Int7 + | Int1, Int8u => Int8u + | Int1, Int8s => Int8s + | Int1, Int15 => Int15 + | Int1, Int16u => Int16u + | Int1, Int16s => Int16s + | Int7, Int1 => Int7 | Int7, Int7 => Int7 | Int7, Int8u => Int8u | Int7, Int8s => Int8s | Int7, Int15 => Int15 | Int7, Int16u => Int16u | Int7, Int16s => Int16s - | Int8u, (Int7|Int8u) => Int8u + | Int8u, (Int1|Int7|Int8u) => Int8u | Int8u, Int15 => Int15 | Int8u, Int16u => Int16u | Int8u, Int16s => Int16s - | Int8s, (Int7|Int8s) => Int8s + | Int8s, (Int1|Int7|Int8s) => Int8s | Int8s, (Int15|Int16s) => Int16s - | Int15, (Int7|Int8u|Int15) => Int15 + | Int15, (Int1|Int7|Int8u|Int15) => Int15 | Int15, Int16u => Int16u | Int15, (Int8s|Int16s) => Int16s - | Int16u, (Int7|Int8u|Int15|Int16u) => Int16u - | Int16s, (Int7|Int8u|Int8s|Int15|Int16s) => Int16s + | Int16u, (Int1|Int7|Int8u|Int15|Int16u) => Int16u + | Int16s, (Int1|Int7|Int8u|Int8s|Int15|Int16s) => Int16s | Float32, Float32 => Float32 | _, _ => Any end. Definition of_int (n: int) := - if Int.eq_dec n (Int.zero_ext 7 n) then Int7 + if Int.eq_dec n Int.zero || Int.eq_dec n Int.one then Int1 + else if Int.eq_dec n (Int.zero_ext 7 n) then Int7 else if Int.eq_dec n (Int.zero_ext 8 n) then Int8u else if Int.eq_dec n (Int.sign_ext 8 n) then Int8s else if Int.eq_dec n (Int.zero_ext 15 n) then Int15 @@ -216,7 +227,8 @@ Definition unop (op: unary_operation) (a: approx) := | Ocast16unsigned => Int16u | Ocast16signed => Int16s | Osingleoffloat => Float32 - | Onotbool => Int7 + | Oboolval => Int1 + | Onotbool => Int1 | _ => Any end. @@ -226,17 +238,20 @@ Definition unop_is_redundant (op: unary_operation) (a: approx) := | Ocast8signed => bge Int8s a | Ocast16unsigned => bge Int16u a | Ocast16signed => bge Int16s a + | Oboolval => bge Int1 a | Osingleoffloat => bge Float32 a | _ => false end. Definition bitwise_and (a1 a2: approx) := - if bge Int8u a1 || bge Int8u a2 then Int8u + if bge Int1 a1 || bge Int1 a2 then Int1 + else if bge Int8u a1 || bge Int8u a2 then Int8u else if bge Int16u a1 || bge Int16u a2 then Int16u else Any. Definition bitwise_or (a1 a2: approx) := - if bge Int8u a1 && bge Int8u a2 then Int8u + if bge Int1 a1 && bge Int1 a2 then Int1 + else if bge Int8u a1 && bge Int8u a2 then Int8u else if bge Int16u a1 && bge Int16u a2 then Int16u else Any. @@ -244,9 +259,9 @@ Definition binop (op: binary_operation) (a1 a2: approx) := match op with | Oand => bitwise_and a1 a2 | Oor | Oxor => bitwise_or a1 a2 - | Ocmp _ => Int7 - | Ocmpu _ => Int7 - | Ocmpf _ => Int7 + | Ocmp _ => Int1 + | Ocmpu _ => Int1 + | Ocmpf _ => Int1 | _ => Any end. @@ -275,7 +290,7 @@ Definition var_addr (cenv: compilenv) (id: ident): res (expr * approx) := match PMap.get id cenv with | Var_local chunk => Error(msg "Cminorgen.var_addr") | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs, Any) - | Var_stack_array ofs => OK (make_stackaddr ofs, Any) + | Var_stack_array ofs sz al => OK (make_stackaddr ofs, Any) | _ => OK (make_globaladdr id, Any) end. @@ -299,16 +314,17 @@ Definition var_set (cenv: compilenv) (** A variant of [var_set] used for initializing function parameters. The value to be stored already resides in the Cminor variable called [id]. *) -Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ) (k: stmt): res stmt := +Definition var_set_self (cenv: compilenv) (id: ident) (k: stmt): res stmt := match PMap.get id cenv with | Var_local chunk => OK k | Var_stack_scalar chunk ofs => OK (Sseq (make_store chunk (make_stackaddr ofs) (Evar (for_var id))) k) - | Var_global_scalar chunk => - OK (Sseq (make_store chunk (make_globaladdr id) (Evar (for_var id))) k) + | Var_stack_array ofs sz al => + OK (Sseq (Sbuiltin None (EF_memcpy sz (Zmin al 4)) + (make_stackaddr ofs :: Evar (for_var id) :: nil)) k) | _ => - Error(msg "Cminorgen.var_set_self.2") + Error(msg "Cminorgen.var_set_self") end. (** Translation of constants. *) @@ -432,6 +448,9 @@ Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) do (te, a) <- transl_expr cenv e; do tel <- transl_exprlist cenv el; OK (Scall (option_map for_temp optid) sig te tel) + | Csharpminor.Sbuiltin optid ef el => + do tel <- transl_exprlist cenv el; + OK (Sbuiltin (option_map for_temp optid) ef tel) | Csharpminor.Sseq s1 s2 => do ts1 <- transl_stmt ret cenv xenv s1; do ts2 <- transl_stmt ret cenv xenv s2; @@ -515,6 +534,8 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := Identset.union (addr_taken_expr e1) (addr_taken_expr e2) | Csharpminor.Scall optid sig e el => Identset.union (addr_taken_expr e) (addr_taken_exprlist el) + | Csharpminor.Sbuiltin optid ef el => + addr_taken_exprlist el | Csharpminor.Sseq s1 s2 => Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2) | Csharpminor.Sifthenelse e s1 s2 => @@ -554,9 +575,9 @@ Definition assign_variable (cenv_stacksize: compilenv * Z) : compilenv * Z := let (cenv, stacksize) := cenv_stacksize in match id_lv with - | (id, Varray sz) => + | (id, Varray sz al) => let ofs := align stacksize (array_alignment sz) in - (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) + (PMap.set id (Var_stack_array ofs sz al) cenv, ofs + Zmax 0 sz) | (id, Vscalar chunk) => if Identset.mem id atk then let sz := size_chunk chunk in @@ -589,7 +610,7 @@ Definition assign_global_variable match info with | (id, mkglobvar vk _ _ _) => PMap.set id (match vk with Vscalar chunk => Var_global_scalar chunk - | Varray _ => Var_global_array + | Varray _ _ => Var_global_array end) ce end. @@ -605,13 +626,13 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv := local variables.) *) Fixpoint store_parameters - (cenv: compilenv) (params: list (ident * memory_chunk)) + (cenv: compilenv) (params: list (ident * var_kind)) {struct params} : res stmt := match params with | nil => OK Sskip - | (id, chunk) :: rem => + | (id, vk) :: rem => do s <- store_parameters cenv rem; - var_set_self cenv id (type_of_chunk chunk) s + var_set_self cenv id s end. (** Translation of a Csharpminor function. We must check that the -- cgit