diff options
| -rw-r--r-- | .depend | 26 | ||||
| -rw-r--r-- | LICENSE | 15 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 4 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 2 | ||||
| -rw-r--r-- | cfrontend/Clight.v | 61 | ||||
| -rw-r--r-- | cfrontend/Cop.v | 822 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 521 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 63 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 22 | ||||
| -rw-r--r-- | cfrontend/Cstrategy.v | 2 | ||||
| -rw-r--r-- | cfrontend/Csyntax.v | 789 | ||||
| -rw-r--r-- | cfrontend/Ctypes.v | 546 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 2 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 3 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 2 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 12 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 2 | ||||
| -rw-r--r-- | doc/index.html | 5 | ||||
| -rw-r--r-- | driver/Interp.ml | 2 |
22 files changed, 1522 insertions, 1385 deletions
@@ -98,18 +98,20 @@ $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.v $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo -cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo -cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo -cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo -cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo -cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo -cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo -cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo -cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo +cfrontend/Ctypes.vo cfrontend/Ctypes.glob: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo +cfrontend/Cop.vo cfrontend/Cop.glob: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo +cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo +cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo +cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo +cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo +cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo +cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo +cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo +cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo @@ -22,13 +22,14 @@ option) any later version: backend/CMtypecheck.ml common/Mem.v backend/CMtypecheck.mli common/Smallstep.v cfrontend/C2C.ml common/Switch.v - cfrontend/Csem.v common/Values.v - cfrontend/Csyntax.v lib/Coqlib.v - cfrontend/Cstrategy.v lib/Floats.v - cfrontend/Clight.v lib/Integers.v - cfrontend/PrintCsyntax.ml lib/Maps.v - cfrontend/PrintClight.ml lib/Parmov.v - lib/Camlcoq.ml + cfrontend/Cop.v common/Values.v + cfrontend/Ctypes.v lib/Coqlib.v + cfrontend/Csem.v lib/Floats.v + cfrontend/Csyntax.v lib/Integers.v + cfrontend/Cstrategy.v lib/Maps.v + cfrontend/Clight.v lib/Parmov.v + cfrontend/PrintCsyntax.ml lib/Camlcoq.ml + cfrontend/PrintClight.ml all files in the runtime/ directory all files in the cparser/ directory @@ -90,7 +90,7 @@ BACKEND=\ # C front-end modules (in cfrontend/) -CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \ +CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \ Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ Clight.v Cshmgen.v Cshmgenproof.v \ diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c9beaf7..9a93017 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -22,6 +22,8 @@ open Builtins open Camlcoq open AST open Values +open Ctypes +open Cop open Csyntax open Initializers @@ -723,7 +725,7 @@ let convertGlobvar env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')] + if sto = C.Storage_extern then [] else [Init_space(Ctypes.sizeof ty')] | Some i -> convertInitializer env ty i in let align = diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 9391d8e..b6ea1e0 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -25,6 +25,8 @@ Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Determinism. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. Require Cstrategy. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index a8624e9..f95cbe6 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -28,12 +28,11 @@ Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. -Require Import Csyntax. -Require Import Csem. +Require Import Ctypes. +Require Import Cop. (** * Abstract syntax *) - (** ** Expressions *) (** Clight expressions correspond to the "pure" subset of C expressions. @@ -84,8 +83,9 @@ Definition typeof (e: expr) : type := (** Clight statements are similar to those of Compcert C, with the addition of assigment (of a rvalue to a lvalue), assignment to a temporary, and function call (with assignment of the result to a temporary). - The three C loops are replaced by a single infinite loop [Sloop s1 s2] - that executes [s1] then [s2] repeatedly. A [continue] in [s1] branches to [s2]. *) + The three C loops are replaced by a single infinite loop [Sloop s1 + s2] that executes [s1] then [s2] repeatedly. A [continue] in [s1] + branches to [s2]. *) Definition label := ident. @@ -145,16 +145,6 @@ Inductive fundef : Type := | Internal: function -> fundef | External: external_function -> typelist -> type -> fundef. -(** ** Programs *) - -(** A program is a collection of named functions, plus a collection - of named global variables, carrying their types and optional initialization - data. See module [AST] for more details. *) - -Definition program : Type := AST.program fundef type. - -(** * Operations over types *) - (** The type of a function definition. *) Definition type_of_function (f: function) : type := @@ -166,6 +156,14 @@ Definition type_of_fundef (f: fundef) : type := | External id args res => Tfunction args res end. +(** ** Programs *) + +(** A program is a collection of named functions, plus a collection + of named global variables, carrying their types and optional initialization + data. See module [AST] for more details. *) + +Definition program : Type := AST.program fundef type. + (** * Operational semantics *) (** The semantics uses two environments. The global environment @@ -174,9 +172,9 @@ Definition type_of_fundef (f: fundef) : type := Definition genv := Genv.t fundef type. -(** The local environment maps local variables to block references - and types. The current value of the variable is stored in the associated memory - block. *) +(** The local environment maps local variables to block references and + types. The current value of the variable is stored in the + associated memory block. *) Definition env := PTree.t (block * type). (* map variable -> location & type *) @@ -226,6 +224,25 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> assign_loc ty m b ofs (Vptr b' ofs') m'. +(** Allocation of function-local variables. + [alloc_variables e1 m1 vars e2 m2] allocates one memory block + for each variable declared in [vars], and associates the variable + name with this block. [e1] and [m1] are the initial local environment + and memory state. [e2] and [m2] are the final local environment + and memory state. *) + +Inductive alloc_variables: env -> mem -> + list (ident * type) -> + env -> mem -> Prop := + | alloc_variables_nil: + forall e m, + alloc_variables e m nil e m + | alloc_variables_cons: + forall e m id ty vars m1 b1 m2 e2, + Mem.alloc m 0 (sizeof ty) = (m1, b1) -> + alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 -> + alloc_variables e m ((id, ty) :: vars) e2 m2. + (** Initialization of local variables that are parameters to a function. [bind_parameters e m1 params args m2] stores the values [args] in the memory blocks corresponding to the variables [params]. @@ -252,6 +269,14 @@ Fixpoint create_undef_temps (temps: list (ident * type)) : temp_env := | (id, t) :: temps' => PTree.set id Vundef (create_undef_temps temps') end. +(** Return the list of blocks in the codomain of [e], with low and high bounds. *) + +Definition block_of_binding (id_b_ty: ident * (block * type)) := + match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end. + +Definition blocks_of_env (e: env) : list (block * Z * Z) := + List.map block_of_binding (PTree.elements e). + (** Optional assignment to a temporary *) Definition set_opttemp (optid: option ident) (v: val) (le: temp_env) := diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v new file mode 100644 index 0000000..9d581b6 --- /dev/null +++ b/cfrontend/Cop.v @@ -0,0 +1,822 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Arithmetic and logical operators for the Compcert C and Clight languages *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Ctypes. + +(** * Syntax of operators. *) + +Inductive unary_operation : Type := + | Onotbool : unary_operation (**r boolean negation ([!] in C) *) + | Onotint : unary_operation (**r integer complement ([~] in C) *) + | Oneg : unary_operation. (**r opposite (unary [-]) *) + +Inductive binary_operation : Type := + | Oadd : binary_operation (**r addition (binary [+]) *) + | Osub : binary_operation (**r subtraction (binary [-]) *) + | Omul : binary_operation (**r multiplication (binary [*]) *) + | Odiv : binary_operation (**r division ([/]) *) + | Omod : binary_operation (**r remainder ([%]) *) + | Oand : binary_operation (**r bitwise and ([&]) *) + | Oor : binary_operation (**r bitwise or ([|]) *) + | Oxor : binary_operation (**r bitwise xor ([^]) *) + | Oshl : binary_operation (**r left shift ([<<]) *) + | Oshr : binary_operation (**r right shift ([>>]) *) + | Oeq: binary_operation (**r comparison ([==]) *) + | One: binary_operation (**r comparison ([!=]) *) + | Olt: binary_operation (**r comparison ([<]) *) + | Ogt: binary_operation (**r comparison ([>]) *) + | Ole: binary_operation (**r comparison ([<=]) *) + | Oge: binary_operation. (**r comparison ([>=]) *) + +Inductive incr_or_decr : Type := Incr | Decr. + +(** * Type classification and semantics of operators. *) + +(** Most C operators are overloaded (they apply to arguments of various + types) and their semantics depend on the types of their arguments. + The following [classify_*] functions take as arguments the types + of the arguments of an operation. They return enough information + to resolve overloading for this operator applications, such as + ``both arguments are floats'', or ``the first is a pointer + and the second is an integer''. This classification is used in the + compiler (module [Cshmgen]) to resolve overloading statically. + + The [sem_*] functions below compute the result of an operator + application. Since operators are overloaded, the result depends + both on the static types of the arguments and on their run-time values. + The corresponding [classify_*] function is first called on the + types of the arguments to resolve static overloading. It is then + followed by a case analysis on the values of the arguments. *) + +(** ** Casts and truth values *) + +Inductive classify_cast_cases : Type := + | cast_case_neutral (**r int|pointer -> int32|pointer *) + | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) + | cast_case_f2f (sz2:floatsize) (**r float -> float *) + | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) + | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_f2bool (**r float -> bool *) + | cast_case_p2bool (**r pointer -> bool *) + | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) + | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) + | cast_case_void (**r any -> void *) + | cast_case_default. + +Function classify_cast (tfrom tto: type) : classify_cast_cases := + match tto, tfrom with + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool + | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool + | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 + | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 + | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 + | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 + | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral + | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 + | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 + | Tvoid, _ => cast_case_void + | _, _ => cast_case_default + end. + +(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], + viewed with static type [t1], can be cast to type [t2], + resulting in value [v2]. *) + +Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := + match sz, sg with + | I8, Signed => Int.sign_ext 8 i + | I8, Unsigned => Int.zero_ext 8 i + | I16, Signed => Int.sign_ext 16 i + | I16, Unsigned => Int.zero_ext 16 i + | I32, _ => i + | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one + end. + +Definition cast_int_float (si : signedness) (i: int) : float := + match si with + | Signed => Float.floatofint i + | Unsigned => Float.floatofintu i + end. + +Definition cast_float_int (si : signedness) (f: float) : option int := + match si with + | Signed => Float.intoffloat f + | Unsigned => Float.intuoffloat f + end. + +Definition cast_float_float (sz: floatsize) (f: float) : float := + match sz with + | F32 => Float.singleoffloat f + | F64 => f + end. + +Function sem_cast (v: val) (t1 t2: type) : option val := + match classify_cast t1 t2 with + | cast_case_neutral => + match v with + | Vint _ | Vptr _ _ => Some v + | _ => None + end + | cast_case_i2i sz2 si2 => + match v with + | Vint i => Some (Vint (cast_int_int sz2 si2 i)) + | _ => None + end + | cast_case_f2f sz2 => + match v with + | Vfloat f => Some (Vfloat (cast_float_float sz2 f)) + | _ => None + end + | cast_case_i2f si1 sz2 => + match v with + | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | _ => None + end + | cast_case_f2i sz2 si2 => + match v with + | Vfloat f => + match cast_float_int si2 f with + | Some i => Some (Vint (cast_int_int sz2 si2 i)) + | None => None + end + | _ => None + end + | cast_case_f2bool => + match v with + | Vfloat f => + Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) + | _ => None + end + | cast_case_p2bool => + match v with + | Vint i => Some (Vint (cast_int_int IBool Signed i)) + | Vptr _ _ => Some (Vint Int.one) + | _ => None + end + | cast_case_struct id1 fld1 id2 fld2 => + if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + | cast_case_union id1 fld1 id2 fld2 => + if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + | cast_case_void => + Some v + | cast_case_default => + None + end. + +(** The following describes types that can be interpreted as a boolean: + integers, floats, pointers. It is used for the semantics of + the [!] and [?] operators, as well as the [if], [while], [for] statements. *) + +Inductive classify_bool_cases : Type := + | bool_case_i (**r integer *) + | bool_case_f (**r float *) + | bool_case_p (**r pointer *) + | bool_default. + +Definition classify_bool (ty: type) : classify_bool_cases := + match typeconv ty with + | Tint _ _ _ => bool_case_i + | Tpointer _ _ => bool_case_p + | Tfloat _ _ => bool_case_f + | _ => bool_default + end. + +(** Interpretation of values as truth values. + Non-zero integers, non-zero floats and non-null pointers are + considered as true. The integer zero (which also represents + the null pointer) and the float 0.0 are false. *) + +Function bool_val (v: val) (t: type) : option bool := + match classify_bool t with + | bool_case_i => + match v with + | Vint n => Some (negb (Int.eq n Int.zero)) + | _ => None + end + | bool_case_f => + match v with + | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero)) + | _ => None + end + | bool_case_p => + match v with + | Vint n => Some (negb (Int.eq n Int.zero)) + | Vptr b ofs => Some true + | _ => None + end + | bool_default => None + end. + +(** Common-sense relation between Boolean value and casting to [_Bool] type. *) + +Lemma cast_bool_bool_val: + forall v t, + sem_cast v t (Tint IBool Signed noattr) = + match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. +Proof. + intros. + assert (A: classify_bool t = + match t with + | Tint _ _ _ => bool_case_i + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p + | Tfloat _ _ => bool_case_f + | _ => bool_default + end). + unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto. + + unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. + destruct (Int.eq i0 Int.zero); auto. + destruct (Float.cmp Ceq f0 Float.zero); auto. + destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i Int.zero); auto. + destruct (Int.eq i Int.zero); auto. +Qed. + +(** ** Unary operators *) + +(** *** Boolean negation *) + +Function sem_notbool (v: val) (ty: type) : option val := + match classify_bool ty with + | bool_case_i => + match v with + | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) + | _ => None + end + | bool_case_f => + match v with + | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) + | _ => None + end + | bool_case_p => + match v with + | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) + | Vptr _ _ => Some Vfalse + | _ => None + end + | bool_default => None + end. + +(** Common-sense relation between Boolean value and Boolean negation. *) + +Lemma notbool_bool_val: + forall v t, + sem_notbool v t = + match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. +Proof. + intros. unfold sem_notbool, bool_val. + destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. +Qed. + +(** *** Opposite *) + +Inductive classify_neg_cases : Type := + | neg_case_i(s: signedness) (**r int *) + | neg_case_f (**r float *) + | neg_default. + +Definition classify_neg (ty: type) : classify_neg_cases := + match ty with + | Tint I32 Unsigned _ => neg_case_i Unsigned + | Tint _ _ _ => neg_case_i Signed + | Tfloat _ _ => neg_case_f + | _ => neg_default + end. + +Function sem_neg (v: val) (ty: type) : option val := + match classify_neg ty with + | neg_case_i sg => + match v with + | Vint n => Some (Vint (Int.neg n)) + | _ => None + end + | neg_case_f => + match v with + | Vfloat f => Some (Vfloat (Float.neg f)) + | _ => None + end + | neg_default => None + end. + +(** *** Bitwise complement *) + +Inductive classify_notint_cases : Type := + | notint_case_i(s: signedness) (**r int *) + | notint_default. + +Definition classify_notint (ty: type) : classify_notint_cases := + match ty with + | Tint I32 Unsigned _ => notint_case_i Unsigned + | Tint _ _ _ => notint_case_i Signed + | _ => notint_default + end. + +Function sem_notint (v: val) (ty: type): option val := + match classify_notint ty with + | notint_case_i sg => + match v with + | Vint n => Some (Vint (Int.xor n Int.mone)) + | _ => None + end + | notint_default => None + end. + +(** ** Binary operators *) + +(** For binary operations, the "usual binary conversions", adapted to a 32-bit + platform, state that: +- If both arguments are of integer type, an integer operation is performed. + For operations that behave differently at unsigned and signed types + (e.g. division, modulus, comparisons), the unsigned operation is selected + if at least one of the arguments is of type "unsigned int32", otherwise + the signed operation is performed. +- If both arguments are of float type, a float operation is performed. + We choose to perform all float arithmetic in double precision, + even if both arguments are single-precision floats. +- If one argument has integer type and the other has float type, + we convert the integer argument to float, then perform the float operation. +*) + +(** *** Addition *) + +Inductive classify_add_cases : Type := + | add_case_ii(s: signedness) (**r int, int *) + | add_case_ff (**r float, float *) + | add_case_if(s: signedness) (**r int, float *) + | add_case_fi(s: signedness) (**r float, int *) + | add_case_pi(ty: type)(a: attr) (**r pointer, int *) + | add_case_ip(ty: type)(a: attr) (**r int, pointer *) + | add_default. + +Definition classify_add (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => add_case_ii Signed + | Tfloat _ _, Tfloat _ _ => add_case_ff + | Tint _ sg _, Tfloat _ _ => add_case_if sg + | Tfloat _ _, Tint _ sg _ => add_case_fi sg + | Tpointer ty a, Tint _ _ _ => add_case_pi ty a + | Tint _ _ _, Tpointer ty a => add_case_ip ty a + | _, _ => add_default + end. + +Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_add t1 t2 with + | add_case_ii sg => (**r integer addition *) + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) + | _, _ => None + end + | add_case_ff => (**r float addition *) + match v1, v2 with + | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2)) + | _, _ => None + end + | add_case_if sg => (**r int plus float *) + match v1, v2 with + | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2)) + | _, _ => None + end + | add_case_fi sg => (**r float plus int *) + match v1, v2 with + | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2))) + | _, _ => None + end + | add_case_pi ty _ => (**r pointer plus integer *) + match v1,v2 with + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | _, _ => None + end + | add_case_ip ty _ => (**r integer plus pointer *) + match v1,v2 with + | Vint n1, Vptr b2 ofs2 => + Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) + | _, _ => None + end + | add_default => None +end. + +(** *** Subtraction *) + +Inductive classify_sub_cases : Type := + | sub_case_ii(s: signedness) (**r int , int *) + | sub_case_ff (**r float , float *) + | sub_case_if(s: signedness) (**r int, float *) + | sub_case_fi(s: signedness) (**r float, int *) + | sub_case_pi(ty: type) (**r pointer, int *) + | sub_case_pp(ty: type) (**r pointer, pointer *) + | sub_default. + +Definition classify_sub (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed + | Tfloat _ _ , Tfloat _ _ => sub_case_ff + | Tint _ sg _, Tfloat _ _ => sub_case_if sg + | Tfloat _ _, Tint _ sg _ => sub_case_fi sg + | Tpointer ty _, Tint _ _ _ => sub_case_pi ty + | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty + | _ ,_ => sub_default + end. + +Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_sub t1 t2 with + | sub_case_ii sg => (**r integer subtraction *) + match v1,v2 with + | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2)) + | _, _ => None + end + | sub_case_ff => (**r float subtraction *) + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2)) + | _, _ => None + end + | sub_case_if sg => (**r int minus float *) + match v1, v2 with + | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2)) + | _, _ => None + end + | sub_case_fi sg => (**r float minus int *) + match v1, v2 with + | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2))) + | _, _ => None + end + | sub_case_pi ty => (**r pointer minus integer *) + match v1,v2 with + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | _, _ => None + end + | sub_case_pp ty => (**r pointer minus pointer *) + match v1,v2 with + | Vptr b1 ofs1, Vptr b2 ofs2 => + if zeq b1 b2 then + if Int.eq (Int.repr (sizeof ty)) Int.zero then None + else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty)))) + else None + | _, _ => None + end + | sub_default => None + end. + +(** *** Multiplication *) + +Inductive classify_mul_cases : Type:= + | mul_case_ii(s: signedness) (**r int , int *) + | mul_case_ff (**r float , float *) + | mul_case_if(s: signedness) (**r int, float *) + | mul_case_fi(s: signedness) (**r float, int *) + | mul_default. + +Definition classify_mul (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed + | Tfloat _ _ , Tfloat _ _ => mul_case_ff + | Tint _ sg _, Tfloat _ _ => mul_case_if sg + | Tfloat _ _, Tint _ sg _ => mul_case_fi sg + | _,_ => mul_default +end. + +Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_mul t1 t2 with + | mul_case_ii sg => + match v1,v2 with + | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2)) + | _, _ => None + end + | mul_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2)) + | _, _ => None + end + | mul_case_if sg => + match v1, v2 with + | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2)) + | _, _ => None + end + | mul_case_fi sg => + match v1, v2 with + | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2))) + | _, _ => None + end + | mul_default => + None +end. + +(** *** Division *) + +Inductive classify_div_cases : Type:= + | div_case_ii(s: signedness) (**r int , int *) + | div_case_ff (**r float , float *) + | div_case_if(s: signedness) (**r int, float *) + | div_case_fi(s: signedness) (**r float, int *) + | div_default. + +Definition classify_div (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => div_case_ii Signed + | Tfloat _ _ , Tfloat _ _ => div_case_ff + | Tint _ sg _, Tfloat _ _ => div_case_if sg + | Tfloat _ _, Tint _ sg _ => div_case_fi sg + | _,_ => div_default +end. + +Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_div t1 t2 with + | div_case_ii Unsigned => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) + | _,_ => None + end + | div_case_ii Signed => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone + then None else Some (Vint(Int.divs n1 n2)) + | _,_ => None + end + | div_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2)) + | _, _ => None + end + | div_case_if sg => + match v1, v2 with + | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2)) + | _, _ => None + end + | div_case_fi sg => + match v1, v2 with + | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2))) + | _, _ => None + end + | div_default => + None +end. + +(** *** Integer-only binary operations: modulus, bitwise "and", "or", and "xor" *) + +Inductive classify_binint_cases : Type:= + | binint_case_ii(s: signedness) (**r int , int *) + | binint_default. + +Definition classify_binint (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned + | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed + | _,_ => binint_default +end. + +Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_binint t1 t2 with + | binint_case_ii Unsigned => + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) + | _, _ => None + end + | binint_case_ii Signed => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero + || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone + then None else Some (Vint (Int.mods n1 n2)) + | _, _ => None + end + | binint_default => + None + end. + +Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_binint t1 t2 with + | binint_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2)) + | _, _ => None + end + | binint_default => None + end. + +Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_binint t1 t2 with + | binint_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2)) + | _, _ => None + end + | binint_default => None + end. + +Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_binint t1 t2 with + | binint_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2)) + | _, _ => None + end + | binint_default => None + end. + +(** *** Shifts *) + +Inductive classify_shift_cases : Type:= + | shift_case_ii(s: signedness) (**r int , int *) + | shift_default. + +Definition classify_shift (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned + | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed + | _,_ => shift_default +end. + +Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_shift t1 t2 with + | shift_case_ii sg => + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None + | _, _ => None + end + | shift_default => None + end. + +Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val := + match classify_shift t1 t2 with + | shift_case_ii Unsigned => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None + | _,_ => None + end + | shift_case_ii Signed => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None + | _, _ => None + end + | shift_default => + None + end. + +(** *** Comparisons *) + +Inductive classify_cmp_cases : Type:= + | cmp_case_ii(s: signedness) (**r int, int *) + | cmp_case_pp (**r pointer, pointer *) + | cmp_case_ff (**r float , float *) + | cmp_case_if(s: signedness) (**r int, float *) + | cmp_case_fi(s: signedness) (**r float, int *) + | cmp_default. + +Definition classify_cmp (ty1: type) (ty2: type) := + match typeconv ty1, typeconv ty2 with + | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned + | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned + | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed + | Tfloat _ _ , Tfloat _ _ => cmp_case_ff + | Tint _ sg _, Tfloat _ _ => cmp_case_if sg + | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg + | Tpointer _ _ , Tpointer _ _ => cmp_case_pp + | Tpointer _ _ , Tint _ _ _ => cmp_case_pp + | Tint _ _ _, Tpointer _ _ => cmp_case_pp + | _ , _ => cmp_default + end. + +Function sem_cmp_mismatch (c: comparison): option val := + match c with + | Ceq => Some Vfalse + | Cne => Some Vtrue + | _ => None + end. + +Function sem_cmp (c:comparison) + (v1: val) (t1: type) (v2: val) (t2: type) + (m: mem): option val := + match classify_cmp t1 t2 with + | cmp_case_ii Signed => + match v1,v2 with + | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) + | _, _ => None + end + | cmp_case_ii Unsigned => + match v1,v2 with + | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) + | _, _ => None + end + | cmp_case_pp => + match v1,v2 with + | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) + | Vptr b1 ofs1, Vptr b2 ofs2 => + if Mem.valid_pointer m b1 (Int.unsigned ofs1) + && Mem.valid_pointer m b2 (Int.unsigned ofs2) then + if zeq b1 b2 + then Some (Val.of_bool (Int.cmpu c ofs1 ofs2)) + else sem_cmp_mismatch c + else None + | Vptr b ofs, Vint n => + if Int.eq n Int.zero then sem_cmp_mismatch c else None + | Vint n, Vptr b ofs => + if Int.eq n Int.zero then sem_cmp_mismatch c else None + | _, _ => None + end + | cmp_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2)) + | _, _ => None + end + | cmp_case_if sg => + match v1, v2 with + | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2)) + | _, _ => None + end + | cmp_case_fi sg => + match v1, v2 with + | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2))) + | _, _ => None + end + | cmp_default => None + end. + +(** ** Function applications *) + +Inductive classify_fun_cases : Type:= + | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *) + | fun_default. + +Definition classify_fun (ty: type) := + match ty with + | Tfunction args res => fun_case_f args res + | Tpointer (Tfunction args res) _ => fun_case_f args res + | _ => fun_default + end. + +(** * Combined semantics of unary and binary operators *) + +Definition sem_unary_operation + (op: unary_operation) (v: val) (ty: type): option val := + match op with + | Onotbool => sem_notbool v ty + | Onotint => sem_notint v ty + | Oneg => sem_neg v ty + end. + +Definition sem_binary_operation + (op: binary_operation) + (v1: val) (t1: type) (v2: val) (t2:type) + (m: mem): option val := + match op with + | Oadd => sem_add v1 t1 v2 t2 + | Osub => sem_sub v1 t1 v2 t2 + | Omul => sem_mul v1 t1 v2 t2 + | Omod => sem_mod v1 t1 v2 t2 + | Odiv => sem_div v1 t1 v2 t2 + | Oand => sem_and v1 t1 v2 t2 + | Oor => sem_or v1 t1 v2 t2 + | Oxor => sem_xor v1 t1 v2 t2 + | Oshl => sem_shl v1 t1 v2 t2 + | Oshr => sem_shr v1 t1 v2 t2 + | Oeq => sem_cmp Ceq v1 t1 v2 t2 m + | One => sem_cmp Cne v1 t1 v2 t2 m + | Olt => sem_cmp Clt v1 t1 v2 t2 m + | Ogt => sem_cmp Cgt v1 t1 v2 t2 m + | Ole => sem_cmp Cle v1 t1 v2 t2 m + | Oge => sem_cmp Cge v1 t1 v2 t2 m + end. + +Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) := + match id with + | Incr => sem_add v ty (Vint Int.one) type_int32s + | Decr => sem_sub v ty (Vint Int.one) type_int32s + end. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index ddfbeaf..44a7325 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -25,528 +25,11 @@ Require Import AST. Require Import Memory. Require Import Events. Require Import Globalenvs. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Smallstep. -(** * Semantics of type-dependent operations *) - -(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], - viewed with static type [t1], can be cast to type [t2], - resulting in value [v2]. *) - -Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := - match sz, sg with - | I8, Signed => Int.sign_ext 8 i - | I8, Unsigned => Int.zero_ext 8 i - | I16, Signed => Int.sign_ext 16 i - | I16, Unsigned => Int.zero_ext 16 i - | I32, _ => i - | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one - end. - -Definition cast_int_float (si : signedness) (i: int) : float := - match si with - | Signed => Float.floatofint i - | Unsigned => Float.floatofintu i - end. - -Definition cast_float_int (si : signedness) (f: float) : option int := - match si with - | Signed => Float.intoffloat f - | Unsigned => Float.intuoffloat f - end. - -Definition cast_float_float (sz: floatsize) (f: float) : float := - match sz with - | F32 => Float.singleoffloat f - | F64 => f - end. - -Function sem_cast (v: val) (t1 t2: type) : option val := - match classify_cast t1 t2 with - | cast_case_neutral => - match v with - | Vint _ | Vptr _ _ => Some v - | _ => None - end - | cast_case_i2i sz2 si2 => - match v with - | Vint i => Some (Vint (cast_int_int sz2 si2 i)) - | _ => None - end - | cast_case_f2f sz2 => - match v with - | Vfloat f => Some (Vfloat (cast_float_float sz2 f)) - | _ => None - end - | cast_case_i2f si1 sz2 => - match v with - | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) - | _ => None - end - | cast_case_f2i sz2 si2 => - match v with - | Vfloat f => - match cast_float_int si2 f with - | Some i => Some (Vint (cast_int_int sz2 si2 i)) - | None => None - end - | _ => None - end - | cast_case_f2bool => - match v with - | Vfloat f => - Some(Vint(if Float.cmp Ceq f Float.zero then Int.zero else Int.one)) - | _ => None - end - | cast_case_p2bool => - match v with - | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) - | _ => None - end - | cast_case_struct id1 fld1 id2 fld2 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None - | cast_case_union id1 fld1 id2 fld2 => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None - | cast_case_void => - Some v - | cast_case_default => - None - end. - -(** Interpretation of values as truth values. - Non-zero integers, non-zero floats and non-null pointers are - considered as true. The integer zero (which also represents - the null pointer) and the float 0.0 are false. *) - -Definition bool_val (v: val) (t: type) : option bool := - match classify_bool t with - | bool_case_i => - match v with - | Vint n => Some (negb (Int.eq n Int.zero)) - | _ => None - end - | bool_case_f => - match v with - | Vfloat f => Some (negb (Float.cmp Ceq f Float.zero)) - | _ => None - end - | bool_case_p => - match v with - | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => Some true - | _ => None - end - | bool_default => None - end. - -(** The following [sem_] functions compute the result of an operator - application. Since operators are overloaded, the result depends - both on the static types of the arguments and on their run-time values. - For binary operations, the "usual binary conversions", adapted to a 32-bit - platform, state that: -- If both arguments are of integer type, an integer operation is performed. - For operations that behave differently at unsigned and signed types - (e.g. division, modulus, comparisons), the unsigned operation is selected - if at least one of the arguments is of type "unsigned int32", otherwise - the signed operation is performed. -- If both arguments are of float type, a float operation is performed. - We choose to perform all float arithmetic in double precision, - even if both arguments are single-precision floats. -- If one argument has integer type and the other has float type, - we convert the integer argument to float, then perform the float operation. - *) - -Function sem_neg (v: val) (ty: type) : option val := - match classify_neg ty with - | neg_case_i sg => - match v with - | Vint n => Some (Vint (Int.neg n)) - | _ => None - end - | neg_case_f => - match v with - | Vfloat f => Some (Vfloat (Float.neg f)) - | _ => None - end - | neg_default => None - end. - -Function sem_notint (v: val) (ty: type): option val := - match classify_notint ty with - | notint_case_i sg => - match v with - | Vint n => Some (Vint (Int.xor n Int.mone)) - | _ => None - end - | notint_default => None - end. - -Function sem_notbool (v: val) (ty: type) : option val := - match classify_bool ty with - | bool_case_i => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | _ => None - end - | bool_case_f => - match v with - | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) - | _ => None - end - | bool_case_p => - match v with - | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr _ _ => Some Vfalse - | _ => None - end - | bool_default => None - end. - -Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_add t1 t2 with - | add_case_ii sg => (**r integer addition *) - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) - | _, _ => None - end - | add_case_ff => (**r float addition *) - match v1, v2 with - | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2)) - | _, _ => None - end - | add_case_if sg => (**r int plus float *) - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2)) - | _, _ => None - end - | add_case_fi sg => (**r float plus int *) - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2))) - | _, _ => None - end - | add_case_pi ty _ => (**r pointer plus integer *) - match v1,v2 with - | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) - | _, _ => None - end - | add_case_ip ty _ => (**r integer plus pointer *) - match v1,v2 with - | Vint n1, Vptr b2 ofs2 => - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) - | _, _ => None - end - | add_default => None -end. - -Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_sub t1 t2 with - | sub_case_ii sg => (**r integer subtraction *) - match v1,v2 with - | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2)) - | _, _ => None - end - | sub_case_ff => (**r float subtraction *) - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2)) - | _, _ => None - end - | sub_case_if sg => (**r int minus float *) - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2)) - | _, _ => None - end - | sub_case_fi sg => (**r float minus int *) - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2))) - | _, _ => None - end - | sub_case_pi ty => (**r pointer minus integer *) - match v1,v2 with - | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) - | _, _ => None - end - | sub_case_pp ty => (**r pointer minus pointer *) - match v1,v2 with - | Vptr b1 ofs1, Vptr b2 ofs2 => - if zeq b1 b2 then - if Int.eq (Int.repr (sizeof ty)) Int.zero then None - else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty)))) - else None - | _, _ => None - end - | sub_default => None - end. - -Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_mul t1 t2 with - | mul_case_ii sg => - match v1,v2 with - | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2)) - | _, _ => None - end - | mul_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2)) - | _, _ => None - end - | mul_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2)) - | _, _ => None - end - | mul_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2))) - | _, _ => None - end - | mul_default => - None -end. - -Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_div t1 t2 with - | div_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | _,_ => None - end - | div_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero - || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone - then None else Some (Vint(Int.divs n1 n2)) - | _,_ => None - end - | div_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2)) - | _, _ => None - end - | div_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2)) - | _, _ => None - end - | div_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2))) - | _, _ => None - end - | div_default => - None -end. - -Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii Unsigned => - match v1, v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) - | _, _ => None - end - | binint_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.eq n2 Int.zero - || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone - then None else Some (Vint (Int.mods n1 n2)) - | _, _ => None - end - | binint_default => - None - end. - -Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2)) - | _, _ => None - end - | binint_default => None - end. - -Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2)) - | _, _ => None - end - | binint_default => None - end. - -Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_binint t1 t2 with - | binint_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2)) - | _, _ => None - end - | binint_default => None - end. - -Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val := - match classify_shift t1 t2 with - | shift_case_ii sg => - match v1, v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None - | _, _ => None - end - | shift_default => None - end. - -Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val := - match classify_shift t1 t2 with - | shift_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None - | _,_ => None - end - | shift_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None - | _, _ => None - end - | shift_default => - None - end. - -Function sem_cmp_mismatch (c: comparison): option val := - match c with - | Ceq => Some Vfalse - | Cne => Some Vtrue - | _ => None - end. - -Function sem_cmp (c:comparison) - (v1: val) (t1: type) (v2: val) (t2: type) - (m: mem): option val := - match classify_cmp t1 t2 with - | cmp_case_ii Signed => - match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) - | _, _ => None - end - | cmp_case_ii Unsigned => - match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) - | _, _ => None - end - | cmp_case_pp => - match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) - | Vptr b1 ofs1, Vptr b2 ofs2 => - if Mem.valid_pointer m b1 (Int.unsigned ofs1) - && Mem.valid_pointer m b2 (Int.unsigned ofs2) then - if zeq b1 b2 - then Some (Val.of_bool (Int.cmpu c ofs1 ofs2)) - else sem_cmp_mismatch c - else None - | Vptr b ofs, Vint n => - if Int.eq n Int.zero then sem_cmp_mismatch c else None - | Vint n, Vptr b ofs => - if Int.eq n Int.zero then sem_cmp_mismatch c else None - | _, _ => None - end - | cmp_case_ff => - match v1,v2 with - | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2)) - | _, _ => None - end - | cmp_case_if sg => - match v1, v2 with - | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2)) - | _, _ => None - end - | cmp_case_fi sg => - match v1, v2 with - | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2))) - | _, _ => None - end - | cmp_default => None - end. - -Definition sem_unary_operation - (op: unary_operation) (v: val) (ty: type): option val := - match op with - | Onotbool => sem_notbool v ty - | Onotint => sem_notint v ty - | Oneg => sem_neg v ty - end. - -Definition sem_binary_operation - (op: binary_operation) - (v1: val) (t1: type) (v2: val) (t2:type) - (m: mem): option val := - match op with - | Oadd => sem_add v1 t1 v2 t2 - | Osub => sem_sub v1 t1 v2 t2 - | Omul => sem_mul v1 t1 v2 t2 - | Omod => sem_mod v1 t1 v2 t2 - | Odiv => sem_div v1 t1 v2 t2 - | Oand => sem_and v1 t1 v2 t2 - | Oor => sem_or v1 t1 v2 t2 - | Oxor => sem_xor v1 t1 v2 t2 - | Oshl => sem_shl v1 t1 v2 t2 - | Oshr => sem_shr v1 t1 v2 t2 - | Oeq => sem_cmp Ceq v1 t1 v2 t2 m - | One => sem_cmp Cne v1 t1 v2 t2 m - | Olt => sem_cmp Clt v1 t1 v2 t2 m - | Ogt => sem_cmp Cgt v1 t1 v2 t2 m - | Ole => sem_cmp Cle v1 t1 v2 t2 m - | Oge => sem_cmp Cge v1 t1 v2 t2 m - end. - -Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) := - match id with - | Incr => sem_add v ty (Vint Int.one) type_int32s - | Decr => sem_sub v ty (Vint Int.one) type_int32s - end. - -(** Common-sense relations between boolean operators *) - -Lemma cast_bool_bool_val: - forall v t, - sem_cast v t (Tint IBool Signed noattr) = - match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. -Proof. - intros. - assert (A: classify_bool t = - match t with - | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p - | Tfloat _ _ => bool_case_f - | _ => bool_default - end). - unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto. - - unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. - destruct (Int.eq i0 Int.zero); auto. - destruct (Float.cmp Ceq f0 Float.zero); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i Int.zero); auto. -Qed. - -Lemma notbool_bool_val: - forall v t, - sem_notbool v t = - match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. -Proof. - intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. -Qed. - (** * Operational semantics *) (** The semantics uses two environments. The global environment diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index f611902..c5e9b8d 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -25,7 +25,8 @@ Require Import Errors. Require Import Integers. Require Import Floats. Require Import AST. -Require Import Csyntax. +Require Import Ctypes. +Require Import Cop. Require Import Clight. Require Import Cminor. Require Import Csharpminor. @@ -56,10 +57,10 @@ Definition var_kind_of_type (ty: type): res var_kind := | Tfloat F64 _ => OK(Vscalar Mfloat64) | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)") | Tpointer _ _ => OK(Vscalar Mint32) - | Tarray _ _ _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty)) + | Tarray _ _ _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)") - | Tstruct _ fList _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty)) - | Tunion _ fList _ => OK(Varray (Csyntax.sizeof ty) (Csyntax.alignof ty)) + | Tstruct _ fList _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) + | Tunion _ fList _ => OK(Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) | Tcomp_ptr _ _ => OK(Vscalar Mint32) end. @@ -137,10 +138,10 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := | add_case_if sg => OK (Ebinop Oaddf (make_floatofint e1 sg) e2) | add_case_fi sg => OK (Ebinop Oaddf e1 (make_floatofint e2 sg)) | add_case_pi ty _ => - let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_ip ty _ => - let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) | add_default => Error (msg "Cshmgen.make_add") end. @@ -152,10 +153,10 @@ Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := | sub_case_if sg => OK (Ebinop Osubf (make_floatofint e1 sg) e2) | sub_case_fi sg => OK (Ebinop Osubf e1 (make_floatofint e2 sg)) | sub_case_pi ty => - let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => - let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Odivu (Ebinop Osub e1 e2) n) | sub_default => Error (msg "Cshmgen.make_sub") end. @@ -268,7 +269,7 @@ Definition make_load (addr: expr) (ty_res: type) := by-copy assignment of a value of Clight type [ty]. *) Definition make_memcpy (dst src: expr) (ty: type) := - Sbuiltin None (EF_memcpy (Csyntax.sizeof ty) (Csyntax.alignof ty)) + Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof ty)) (dst :: src :: nil). (** [make_store addr ty rhs] stores the value of the @@ -321,33 +322,33 @@ Definition var_set (id: ident) (ty: type) (rhs: expr) := (** ** Translation of operators *) -Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr := +Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr := match op with - | Csyntax.Onotbool => make_notbool a ta - | Csyntax.Onotint => OK(make_notint a ta) - | Csyntax.Oneg => make_neg a ta + | Cop.Onotbool => make_notbool a ta + | Cop.Onotint => OK(make_notint a ta) + | Cop.Oneg => make_neg a ta end. -Definition transl_binop (op: Csyntax.binary_operation) +Definition transl_binop (op: Cop.binary_operation) (a: expr) (ta: type) (b: expr) (tb: type) : res expr := match op with - | Csyntax.Oadd => make_add a ta b tb - | Csyntax.Osub => make_sub a ta b tb - | Csyntax.Omul => make_mul a ta b tb - | Csyntax.Odiv => make_div a ta b tb - | Csyntax.Omod => make_mod a ta b tb - | Csyntax.Oand => make_and a ta b tb - | Csyntax.Oor => make_or a ta b tb - | Csyntax.Oxor => make_xor a ta b tb - | Csyntax.Oshl => make_shl a ta b tb - | Csyntax.Oshr => make_shr a ta b tb - | Csyntax.Oeq => make_cmp Ceq a ta b tb - | Csyntax.One => make_cmp Cne a ta b tb - | Csyntax.Olt => make_cmp Clt a ta b tb - | Csyntax.Ogt => make_cmp Cgt a ta b tb - | Csyntax.Ole => make_cmp Cle a ta b tb - | Csyntax.Oge => make_cmp Cge a ta b tb + | Cop.Oadd => make_add a ta b tb + | Cop.Osub => make_sub a ta b tb + | Cop.Omul => make_mul a ta b tb + | Cop.Odiv => make_div a ta b tb + | Cop.Omod => make_mod a ta b tb + | Cop.Oand => make_and a ta b tb + | Cop.Oor => make_or a ta b tb + | Cop.Oxor => make_xor a ta b tb + | Cop.Oshl => make_shl a ta b tb + | Cop.Oshr => make_shr a ta b tb + | Cop.Oeq => make_cmp Ceq a ta b tb + | Cop.One => make_cmp Cne a ta b tb + | Cop.Olt => make_cmp Clt a ta b tb + | Cop.Ogt => make_cmp Cgt a ta b tb + | Cop.Ole => make_cmp Cle a ta b tb + | Cop.Oge => make_cmp Cge a ta b tb end. (** * Translation of expressions *) @@ -424,7 +425,7 @@ with transl_lvalue (a: Clight.expr) {struct a} : res expr := end. (** [transl_arglist al tyl] returns a list of Csharpminor expressions - that compute the values of the list [al] of Csyntax expressions, + that compute the values of the list [al] of Clight expressions, casted to the corresponding types in [tyl]. Used for function applications. *) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 51511b9..9f73467 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -23,8 +23,8 @@ Require Import Events. Require Import Memory. Require Import Globalenvs. Require Import Smallstep. -Require Import Csyntax. -Require Import Csem. +Require Import Ctypes. +Require Import Cop. Require Import Clight. Require Import Cminor. Require Import Csharpminor. @@ -94,7 +94,7 @@ Lemma var_kind_by_reference: forall ty vk, access_mode ty = By_reference \/ access_mode ty = By_copy -> var_kind_of_type ty = OK vk -> - vk = Varray (Csyntax.sizeof ty) (Csyntax.alignof ty). + vk = Varray (Ctypes.sizeof ty) (Ctypes.alignof ty). Proof. intros ty vk; destruct ty; simpl; try intuition congruence. destruct i; try congruence; destruct s; intuition congruence. @@ -104,12 +104,12 @@ Qed. Lemma sizeof_var_kind_of_type: forall ty vk, var_kind_of_type ty = OK vk -> - Csharpminor.sizeof vk = Csyntax.sizeof ty. + Csharpminor.sizeof vk = Ctypes.sizeof ty. Proof. intros ty vk. - assert (sizeof (Varray (Csyntax.sizeof ty) (Csyntax.alignof ty)) = Csyntax.sizeof ty). + assert (sizeof (Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) = Ctypes.sizeof ty). simpl. rewrite Zmax_spec. apply zlt_false. - generalize (Csyntax.sizeof_pos ty). omega. + generalize (Ctypes.sizeof_pos ty). omega. destruct ty; try (destruct i; try destruct s); try (destruct f); simpl; intro EQ; inversion EQ; subst vk; auto. Qed. @@ -860,7 +860,7 @@ Qed. Lemma match_env_same_blocks: forall e te, match_env e te -> - blocks_of_env te = Csem.blocks_of_env e. + blocks_of_env te = Clight.blocks_of_env e. Proof. intros. set (R := fun (x: (block * type)) (y: (block * var_kind)) => @@ -879,10 +879,10 @@ Proof. assert (vk' = vk) by congruence. subst vk'. exists (b, ty); split; auto. red. auto. - unfold blocks_of_env, Csem.blocks_of_env. + unfold blocks_of_env, Clight.blocks_of_env. generalize H0. induction 1. auto. simpl. f_equal; auto. - unfold block_of_binding, Csem.block_of_binding. + unfold block_of_binding, Clight.block_of_binding. destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 vk2]]. simpl in *. destruct H1 as [A [B C]]. subst blk2 id2. f_equal. apply sizeof_var_kind_of_type. auto. @@ -891,7 +891,7 @@ Qed. Lemma match_env_free_blocks: forall e te m m', match_env e te -> - Mem.free_list m (Csem.blocks_of_env e) = Some m' -> + Mem.free_list m (Clight.blocks_of_env e) = Some m' -> Mem.free_list m (blocks_of_env te) = Some m'. Proof. intros. rewrite (match_env_same_blocks _ _ H). auto. @@ -912,7 +912,7 @@ Qed. Lemma match_env_alloc_variables: forall e1 m1 vars e2 m2, - Csem.alloc_variables e1 m1 vars e2 m2 -> + Clight.alloc_variables e1 m1 vars e2 m2 -> forall te1 tvars, match_env e1 te1 -> transl_vars vars = OK tvars -> diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 5be17ed..179361d 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -28,6 +28,8 @@ Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 86bba85..5155689 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -21,174 +21,11 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import AST. - -(** * Abstract syntax *) - -(** ** Types *) - -(** Compcert C types are similar to those of C. They include numeric types, - pointers, arrays, function types, and composite types (struct and - union). Numeric types (integers and floats) fully specify the - bit size of the type. An integer type is a pair of a signed/unsigned - flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size - standing for the C99 [_Bool] type. *) - -Inductive signedness : Type := - | Signed: signedness - | Unsigned: signedness. - -Inductive intsize : Type := - | I8: intsize - | I16: intsize - | I32: intsize - | IBool: intsize. - -(** Float types come in two sizes: 32 bits (single precision) - and 64-bit (double precision). *) - -Inductive floatsize : Type := - | F32: floatsize - | F64: floatsize. - -(** Every type carries a set of attributes. Currently, only one - attribute is modeled: [volatile]. *) - -Record attr : Type := mk_attr { - attr_volatile: bool -}. - -Definition noattr := {| attr_volatile := false |}. - -(** The syntax of type expressions. Some points to note: -- Array types [Tarray n] carry the size [n] of the array. - Arrays with unknown sizes are represented by pointer types. -- Function types [Tfunction targs tres] specify the number and types - of the function arguments (list [targs]), and the type of the - function result ([tres]). Variadic functions and old-style unprototyped - functions are not supported. -- In C, struct and union types are named and compared by name. - This enables the definition of recursive struct types such as -<< - struct s1 { int n; struct * s1 next; }; ->> - Note that recursion within types must go through a pointer type. - For instance, the following is not allowed in C. -<< - struct s2 { int n; struct s2 next; }; ->> - In Compcert C, struct and union types [Tstruct id fields] and - [Tunion id fields] are compared by structure: the [fields] - argument gives the names and types of the members. The identifier - [id] is a local name which can be used in conjuction with the - [Tcomp_ptr] constructor to express recursive types. [Tcomp_ptr id] - stands for a pointer type to the nearest enclosing [Tstruct] - or [Tunion] type named [id]. For instance. the structure [s1] - defined above in C is expressed by -<< - Tstruct "s1" (Fcons "n" (Tint I32 Signed) - (Fcons "next" (Tcomp_ptr "s1") - Fnil)) ->> - Note that the incorrect structure [s2] above cannot be expressed at - all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing - structure or union, but not to the structure or union directly. -*) - -Inductive type : Type := - | Tvoid: type (**r the [void] type *) - | Tint: intsize -> signedness -> attr -> type (**r integer types *) - | Tfloat: floatsize -> attr -> type (**r floating-point types *) - | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) - | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) - | Tfunction: typelist -> type -> type (**r function types *) - | Tstruct: ident -> fieldlist -> attr -> type (**r struct types *) - | Tunion: ident -> fieldlist -> attr -> type (**r union types *) - | Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *) - -with typelist : Type := - | Tnil: typelist - | Tcons: type -> typelist -> typelist - -with fieldlist : Type := - | Fnil: fieldlist - | Fcons: ident -> type -> fieldlist -> fieldlist. - -Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} -with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} -with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. -Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. - assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. - assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec. - generalize ident_eq zeq. intros E1 E2. - decide equality. - decide equality. - generalize ident_eq. intros E1. - decide equality. -Defined. - -Opaque type_eq typelist_eq fieldlist_eq. - -(** Extract the attributes of a type. *) - -Definition attr_of_type (ty: type) := - match ty with - | Tvoid => noattr - | Tint sz si a => a - | Tfloat sz a => a - | Tpointer elt a => a - | Tarray elt sz a => a - | Tfunction args res => noattr - | Tstruct id fld a => a - | Tunion id fld a => a - | Tcomp_ptr id a => a - end. - -Definition type_int32s := Tint I32 Signed noattr. -Definition type_bool := Tint IBool Signed noattr. - -(** The usual unary conversion. Promotes small integer types to [signed int32] - and degrades array types and function types to pointer types. *) - -Definition typeconv (ty: type) : type := - match ty with - | Tint I32 Unsigned _ => ty - | Tint _ _ a => Tint I32 Signed a - | Tarray t sz a => Tpointer t a - | Tfunction _ _ => Tpointer ty noattr - | _ => ty - end. +Require Import Ctypes. +Require Import Cop. (** ** Expressions *) -(** Arithmetic and logical operators. *) - -Inductive unary_operation : Type := - | Onotbool : unary_operation (**r boolean negation ([!] in C) *) - | Onotint : unary_operation (**r integer complement ([~] in C) *) - | Oneg : unary_operation. (**r opposite (unary [-]) *) - -Inductive binary_operation : Type := - | Oadd : binary_operation (**r addition (binary [+]) *) - | Osub : binary_operation (**r subtraction (binary [-]) *) - | Omul : binary_operation (**r multiplication (binary [*]) *) - | Odiv : binary_operation (**r division ([/]) *) - | Omod : binary_operation (**r remainder ([%]) *) - | Oand : binary_operation (**r bitwise and ([&]) *) - | Oor : binary_operation (**r bitwise or ([|]) *) - | Oxor : binary_operation (**r bitwise xor ([^]) *) - | Oshl : binary_operation (**r left shift ([<<]) *) - | Oshr : binary_operation (**r right shift ([>>]) *) - | Oeq: binary_operation (**r comparison ([==]) *) - | One: binary_operation (**r comparison ([!=]) *) - | Olt: binary_operation (**r comparison ([<]) *) - | Ogt: binary_operation (**r comparison ([>]) *) - | Ole: binary_operation (**r comparison ([<=]) *) - | Oge: binary_operation. (**r comparison ([>=]) *) - -Inductive incr_or_decr : Type := Incr | Decr. - (** Compcert C expressions are almost identical to those of C. The only omission is string literals. Some operators are treated as derived forms: array indexing, pre-increment, pre-decrement, and @@ -356,24 +193,8 @@ Inductive fundef : Type := | Internal: function -> fundef | External: external_function -> typelist -> type -> fundef. -(** ** Programs *) - -(** A program is a collection of named functions, plus a collection - of named global variables, carrying their types and optional initialization - data. See module [AST] for more details. *) - -Definition program : Type := AST.program fundef type. - -(** * Operations over types *) - (** The type of a function definition. *) -Fixpoint type_of_params (params: list (ident * type)) : typelist := - match params with - | nil => Tnil - | (id, ty) :: rem => Tcons ty (type_of_params rem) - end. - Definition type_of_function (f: function) : type := Tfunction (type_of_params (fn_params f)) (fn_return f). @@ -383,606 +204,10 @@ Definition type_of_fundef (f: fundef) : type := | External id args res => Tfunction args res end. -(** Natural alignment of a type, in bytes. *) - -Fixpoint alignof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' _ _ => alignof t' - | Tfunction _ _ => 1 - | Tstruct _ fld _ => alignof_fields fld - | Tunion _ fld _ => alignof_fields fld - | Tcomp_ptr _ _ => 4 - end - -with alignof_fields (f: fieldlist) : Z := - match f with - | Fnil => 1 - | Fcons id t f' => Zmax (alignof t) (alignof_fields f') - end. - -Scheme type_ind2 := Induction for type Sort Prop - with fieldlist_ind2 := Induction for fieldlist Sort Prop. - -Lemma alignof_1248: - forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8 -with alignof_fields_1248: - forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8. -Proof. - induction t; simpl; auto. - destruct i; auto. - destruct f; auto. - induction f; simpl; auto. - rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto. -Qed. - -Lemma alignof_pos: - forall t, alignof t > 0. -Proof. - intros. generalize (alignof_1248 t). omega. -Qed. - -Lemma alignof_fields_pos: - forall f, alignof_fields f > 0. -Proof. - intros. generalize (alignof_fields_1248 f). omega. -Qed. - -(** Size of a type, in bytes. *) - -Fixpoint sizeof (t: type) : Z := - match t with - | Tvoid => 1 - | Tint I8 _ _ => 1 - | Tint I16 _ _ => 2 - | Tint I32 _ _ => 4 - | Tint IBool _ _ => 1 - | Tfloat F32 _ => 4 - | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 - | Tarray t' n _ => sizeof t' * Zmax 1 n - | Tfunction _ _ => 1 - | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) - | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) - | Tcomp_ptr _ _ => 4 - end - -with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := - match fld with - | Fnil => pos - | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t) - end - -with sizeof_union (fld: fieldlist) : Z := - match fld with - | Fnil => 0 - | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld') - end. - -Lemma sizeof_pos: - forall t, sizeof t > 0. -Proof. - intro t0. - apply (type_ind2 (fun t => sizeof t > 0) - (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0)); - intros; simpl; auto; try omega. - destruct i; omega. - destruct f; omega. - apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. - destruct H. - generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_struct f 0)). omega. - generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). - generalize (Zmax1 1 (sizeof_union f)). omega. - split. omega. auto. - destruct H0. split; intros. - generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. - apply H1. - 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. - -Lemma sizeof_alignof_compat: - forall t, (alignof t | sizeof t). -Proof. - induction t; simpl; try (apply Zdivide_refl). - apply Zdivide_mult_l. auto. - apply align_divides. apply alignof_fields_pos. - apply align_divides. apply alignof_fields_pos. -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. *) - -Open Local Scope string_scope. - -Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) - {struct fld} : res Z := - match fld with - | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) - | Fcons id' t fld' => - if ident_eq id id' - then OK (align pos (alignof t)) - else field_offset_rec id fld' (align pos (alignof t) + sizeof t) - end. - -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 sid fld a fid ofs ty, - field_offset fid fld = OK ofs -> field_type fid fld = OK ty -> - 0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a). -Proof. - intros. exploit field_offset_rec_in_range; eauto. intros [A B]. - split. auto. simpl. eapply Zle_trans. eauto. - eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_fields_pos. -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. eexact H1. eauto. tauto. - subst i. intros. inv H1; inv H2. - exploit field_offset_rec_in_range. eexact H. 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 common fields - are 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. - -(** Fourth, the position of each field respects its alignment. *) - -Lemma field_offset_aligned: - forall id fld ofs ty, - field_offset id fld = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs). -Proof. - assert (forall id ofs ty fld pos, - field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs)). - induction fld; simpl; intros. - discriminate. - destruct (ident_eq id i). inv H; inv H0. - apply align_divides. apply alignof_pos. - eapply IHfld; eauto. - intros. eapply H with (pos := 0); eauto. -Qed. - -(** The [access_mode] function describes how a l-value of the given -type must be accessed: -- [By_value ch]: access by value, i.e. by loading from the address - of the l-value using the memory chunk [ch]; -- [By_reference]: access by reference, i.e. by just returning - the address of the l-value (used for arrays and functions); -- [By_copy]: access is by reference, assignment is by copy - (used for [struct] and [union] types) -- [By_nothing]: no access is possible, e.g. for the [void] type. -*) - -Inductive mode: Type := - | By_value: memory_chunk -> mode - | By_reference: mode - | By_copy: mode - | By_nothing: mode. - -Definition access_mode (ty: type) : mode := - match ty with - | Tint I8 Signed _ => By_value Mint8signed - | Tint I8 Unsigned _ => By_value Mint8unsigned - | Tint I16 Signed _ => By_value Mint16signed - | Tint I16 Unsigned _ => By_value Mint16unsigned - | Tint I32 _ _ => By_value Mint32 - | Tint IBool _ _ => By_value Mint8unsigned - | Tfloat F32 _ => By_value Mfloat32 - | Tfloat F64 _ => By_value Mfloat64 - | Tvoid => By_nothing - | Tpointer _ _ => By_value Mint32 - | Tarray _ _ _ => By_reference - | Tfunction _ _ => By_reference - | Tstruct _ _ _ => By_copy - | Tunion _ _ _ => By_copy - | Tcomp_ptr _ _ => By_nothing -end. - -(** For the purposes of the semantics and the compiler, a type denotes - a volatile access if it carries the [volatile] attribute and it is - accessed by value. *) - -Definition type_is_volatile (ty: type) : bool := - match access_mode ty with - | By_value _ => attr_volatile (attr_of_type ty) - | _ => false - end. - -(** Unroll the type of a structure or union field, substituting - [Tcomp_ptr] by a pointer to the structure. *) - -Section UNROLL_COMPOSITE. - -Variable cid: ident. -Variable comp: type. - -Fixpoint unroll_composite (ty: type) : type := - match ty with - | Tvoid => ty - | Tint _ _ _ => ty - | Tfloat _ _ => ty - | Tpointer t1 a => Tpointer (unroll_composite t1) a - | Tarray t1 sz a => Tarray (unroll_composite t1) sz a - | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2) - | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a - | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a - | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty - end - -with unroll_composite_list (tl: typelist) : typelist := - match tl with - | Tnil => Tnil - | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl') - end - -with unroll_composite_fields (fld: fieldlist) : fieldlist := - match fld with - | Fnil => Fnil - | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld') - end. - -Lemma alignof_unroll_composite: - forall ty, alignof (unroll_composite ty) = alignof ty. -Proof. - apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty) - (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld)); - simpl; intros; auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - destruct (ident_eq i cid); auto. - decEq; auto. -Qed. - -Lemma sizeof_unroll_composite: - forall ty, sizeof (unroll_composite ty) = sizeof ty. -Proof. -Opaque alignof. - apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty) - (fun fld => - sizeof_union (unroll_composite_fields fld) = sizeof_union fld - /\ forall pos, - sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); - simpl; intros; auto. - congruence. - destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto. - destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)). - simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto. - destruct (ident_eq i cid); auto. - destruct H0. split. congruence. - intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto. -Qed. - -End UNROLL_COMPOSITE. - -(** Classification of arithmetic operations and comparisons. - The following [classify_] functions take as arguments the types - of the arguments of an operation. They return enough information - to resolve overloading for this operator applications, such as - ``both arguments are floats'', or ``the first is a pointer - and the second is an integer''. These functions are used to resolve - overloading both in the dynamic semantics (module [Csem]), in the - type system (module [Ctyping]), and in the compiler (module - [Cshmgen]). -*) - -Inductive classify_neg_cases : Type := - | neg_case_i(s: signedness) (**r int *) - | neg_case_f (**r float *) - | neg_default. - -Definition classify_neg (ty: type) : classify_neg_cases := - match ty with - | Tint I32 Unsigned _ => neg_case_i Unsigned - | Tint _ _ _ => neg_case_i Signed - | Tfloat _ _ => neg_case_f - | _ => neg_default - end. - -Inductive classify_notint_cases : Type := - | notint_case_i(s: signedness) (**r int *) - | notint_default. - -Definition classify_notint (ty: type) : classify_notint_cases := - match ty with - | Tint I32 Unsigned _ => notint_case_i Unsigned - | Tint _ _ _ => notint_case_i Signed - | _ => notint_default - end. - -(** The following describes types that can be interpreted as a boolean: - integers, floats, pointers. It is used for the semantics of - the [!] and [?] operators, as well as the [if], [while], [for] statements. *) - -Inductive classify_bool_cases : Type := - | bool_case_i (**r integer *) - | bool_case_f (**r float *) - | bool_case_p (**r pointer *) - | bool_default. - -Definition classify_bool (ty: type) : classify_bool_cases := - match typeconv ty with - | Tint _ _ _ => bool_case_i - | Tpointer _ _ => bool_case_p - | Tfloat _ _ => bool_case_f - | _ => bool_default - end. - -Inductive classify_add_cases : Type := - | add_case_ii(s: signedness) (**r int, int *) - | add_case_ff (**r float, float *) - | add_case_if(s: signedness) (**r int, float *) - | add_case_fi(s: signedness) (**r float, int *) - | add_case_pi(ty: type)(a: attr) (**r pointer, int *) - | add_case_ip(ty: type)(a: attr) (**r int, pointer *) - | add_default. - -Definition classify_add (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => add_case_ii Signed - | Tfloat _ _, Tfloat _ _ => add_case_ff - | Tint _ sg _, Tfloat _ _ => add_case_if sg - | Tfloat _ _, Tint _ sg _ => add_case_fi sg - | Tpointer ty a, Tint _ _ _ => add_case_pi ty a - | Tint _ _ _, Tpointer ty a => add_case_ip ty a - | _, _ => add_default - end. - -Inductive classify_sub_cases : Type := - | sub_case_ii(s: signedness) (**r int , int *) - | sub_case_ff (**r float , float *) - | sub_case_if(s: signedness) (**r int, float *) - | sub_case_fi(s: signedness) (**r float, int *) - | sub_case_pi(ty: type) (**r pointer, int *) - | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_default. - -Definition classify_sub (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => sub_case_ff - | Tint _ sg _, Tfloat _ _ => sub_case_if sg - | Tfloat _ _, Tint _ sg _ => sub_case_fi sg - | Tpointer ty _, Tint _ _ _ => sub_case_pi ty - | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty - | _ ,_ => sub_default - end. - -Inductive classify_mul_cases : Type:= - | mul_case_ii(s: signedness) (**r int , int *) - | mul_case_ff (**r float , float *) - | mul_case_if(s: signedness) (**r int, float *) - | mul_case_fi(s: signedness) (**r float, int *) - | mul_default. - -Definition classify_mul (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => mul_case_ff - | Tint _ sg _, Tfloat _ _ => mul_case_if sg - | Tfloat _ _, Tint _ sg _ => mul_case_fi sg - | _,_ => mul_default -end. - -Inductive classify_div_cases : Type:= - | div_case_ii(s: signedness) (**r int , int *) - | div_case_ff (**r float , float *) - | div_case_if(s: signedness) (**r int, float *) - | div_case_fi(s: signedness) (**r float, int *) - | div_default. - -Definition classify_div (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => div_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => div_case_ff - | Tint _ sg _, Tfloat _ _ => div_case_if sg - | Tfloat _ _, Tint _ sg _ => div_case_fi sg - | _,_ => div_default -end. - -(** The following is common to binary integer-only operators: - modulus, bitwise "and", "or", and "xor". *) - -Inductive classify_binint_cases : Type:= - | binint_case_ii(s: signedness) (**r int , int *) - | binint_default. - -Definition classify_binint (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned - | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed - | _,_ => binint_default -end. - -(** The following is common to shift operators [<<] and [>>]. *) - -Inductive classify_shift_cases : Type:= - | shift_case_ii(s: signedness) (**r int , int *) - | shift_default. - -Definition classify_shift (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned - | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed - | _,_ => shift_default -end. - -Inductive classify_cmp_cases : Type:= - | cmp_case_ii(s: signedness) (**r int, int *) - | cmp_case_pp (**r pointer, pointer *) - | cmp_case_ff (**r float , float *) - | cmp_case_if(s: signedness) (**r int, float *) - | cmp_case_fi(s: signedness) (**r float, int *) - | cmp_default. - -Definition classify_cmp (ty1: type) (ty2: type) := - match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned - | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed - | Tfloat _ _ , Tfloat _ _ => cmp_case_ff - | Tint _ sg _, Tfloat _ _ => cmp_case_if sg - | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg - | Tpointer _ _ , Tpointer _ _ => cmp_case_pp - | Tpointer _ _ , Tint _ _ _ => cmp_case_pp - | Tint _ _ _, Tpointer _ _ => cmp_case_pp - | _ , _ => cmp_default - end. - -Inductive classify_fun_cases : Type:= - | fun_case_f (targs: typelist) (tres: type) (**r (pointer to) function *) - | fun_default. - -Definition classify_fun (ty: type) := - match ty with - | Tfunction args res => fun_case_f args res - | Tpointer (Tfunction args res) _ => fun_case_f args res - | _ => fun_default - end. - -Inductive classify_cast_cases : Type := - | cast_case_neutral (**r int|pointer -> int32|pointer *) - | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) - | cast_case_f2f (sz2:floatsize) (**r float -> float *) - | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) - | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) - | cast_case_f2bool (**r float -> bool *) - | cast_case_p2bool (**r pointer -> bool *) - | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) - | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) - | cast_case_void (**r any -> void *) - | cast_case_default. - -Function classify_cast (tfrom tto: type) : classify_cast_cases := - match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral - | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool - | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool - | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 - | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2 - | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2 - | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2 - | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral - | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 - | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 - | Tvoid, _ => cast_case_void - | _, _ => cast_case_default - end. - -(** Translating C types to Cminor types, function signatures, - and external functions. *) - -Definition typ_of_type (t: type) : AST.typ := - match t with - | Tfloat _ _ => AST.Tfloat - | _ => AST.Tint - end. - -Definition opttyp_of_type (t: type) : option AST.typ := - match t with - | Tvoid => None - | Tfloat _ _ => Some AST.Tfloat - | _ => Some AST.Tint - end. +(** ** Programs *) -Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := - match tl with - | Tnil => nil - | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl - end. +(** A program is a collection of named functions, plus a collection + of named global variables, carrying their types and optional initialization + data. See module [AST] for more details. *) -Definition signature_of_type (args: typelist) (res: type) : signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res). +Definition program : Type := AST.program fundef type. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v new file mode 100644 index 0000000..c05f21a --- /dev/null +++ b/cfrontend/Ctypes.v @@ -0,0 +1,546 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Type expressions for the Compcert C and Clight languages *) + +Require Import Coqlib. +Require Import AST. +Require Import Errors. + +(** * Syntax of types *) + +(** Compcert C types are similar to those of C. They include numeric types, + pointers, arrays, function types, and composite types (struct and + union). Numeric types (integers and floats) fully specify the + bit size of the type. An integer type is a pair of a signed/unsigned + flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size + standing for the C99 [_Bool] type. *) + +Inductive signedness : Type := + | Signed: signedness + | Unsigned: signedness. + +Inductive intsize : Type := + | I8: intsize + | I16: intsize + | I32: intsize + | IBool: intsize. + +(** Float types come in two sizes: 32 bits (single precision) + and 64-bit (double precision). *) + +Inductive floatsize : Type := + | F32: floatsize + | F64: floatsize. + +(** Every type carries a set of attributes. Currently, only one + attribute is modeled: [volatile]. *) + +Record attr : Type := mk_attr { + attr_volatile: bool +}. + +Definition noattr := {| attr_volatile := false |}. + +(** The syntax of type expressions. Some points to note: +- Array types [Tarray n] carry the size [n] of the array. + Arrays with unknown sizes are represented by pointer types. +- Function types [Tfunction targs tres] specify the number and types + of the function arguments (list [targs]), and the type of the + function result ([tres]). Variadic functions and old-style unprototyped + functions are not supported. +- In C, struct and union types are named and compared by name. + This enables the definition of recursive struct types such as +<< + struct s1 { int n; struct * s1 next; }; +>> + Note that recursion within types must go through a pointer type. + For instance, the following is not allowed in C. +<< + struct s2 { int n; struct s2 next; }; +>> + In Compcert C, struct and union types [Tstruct id fields] and + [Tunion id fields] are compared by structure: the [fields] + argument gives the names and types of the members. The identifier + [id] is a local name which can be used in conjuction with the + [Tcomp_ptr] constructor to express recursive types. [Tcomp_ptr id] + stands for a pointer type to the nearest enclosing [Tstruct] + or [Tunion] type named [id]. For instance. the structure [s1] + defined above in C is expressed by +<< + Tstruct "s1" (Fcons "n" (Tint I32 Signed) + (Fcons "next" (Tcomp_ptr "s1") + Fnil)) +>> + Note that the incorrect structure [s2] above cannot be expressed at + all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing + structure or union, but not to the structure or union directly. +*) + +Inductive type : Type := + | Tvoid: type (**r the [void] type *) + | Tint: intsize -> signedness -> attr -> type (**r integer types *) + | Tfloat: floatsize -> attr -> type (**r floating-point types *) + | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) + | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) + | Tfunction: typelist -> type -> type (**r function types *) + | Tstruct: ident -> fieldlist -> attr -> type (**r struct types *) + | Tunion: ident -> fieldlist -> attr -> type (**r union types *) + | Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *) + +with typelist : Type := + | Tnil: typelist + | Tcons: type -> typelist -> typelist + +with fieldlist : Type := + | Fnil: fieldlist + | Fcons: ident -> type -> fieldlist -> fieldlist. + +Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} +with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} +with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. +Proof. + assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality. + assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality. + assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality. + assert (forall (x y: attr), {x=y} + {x<>y}). decide equality. apply bool_dec. + generalize ident_eq zeq. intros E1 E2. + decide equality. + decide equality. + generalize ident_eq. intros E1. + decide equality. +Defined. + +Opaque type_eq typelist_eq fieldlist_eq. + +(** Extract the attributes of a type. *) + +Definition attr_of_type (ty: type) := + match ty with + | Tvoid => noattr + | Tint sz si a => a + | Tfloat sz a => a + | Tpointer elt a => a + | Tarray elt sz a => a + | Tfunction args res => noattr + | Tstruct id fld a => a + | Tunion id fld a => a + | Tcomp_ptr id a => a + end. + +Definition type_int32s := Tint I32 Signed noattr. +Definition type_bool := Tint IBool Signed noattr. + +(** The usual unary conversion. Promotes small integer types to [signed int32] + and degrades array types and function types to pointer types. *) + +Definition typeconv (ty: type) : type := + match ty with + | Tint I32 Unsigned _ => ty + | Tint _ _ a => Tint I32 Signed a + | Tarray t sz a => Tpointer t a + | Tfunction _ _ => Tpointer ty noattr + | _ => ty + end. + +(** * Operations over types *) + +(** Natural alignment of a type, in bytes. *) + +Fixpoint alignof (t: type) : Z := + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' _ _ => alignof t' + | Tfunction _ _ => 1 + | Tstruct _ fld _ => alignof_fields fld + | Tunion _ fld _ => alignof_fields fld + | Tcomp_ptr _ _ => 4 + end + +with alignof_fields (f: fieldlist) : Z := + match f with + | Fnil => 1 + | Fcons id t f' => Zmax (alignof t) (alignof_fields f') + end. + +Scheme type_ind2 := Induction for type Sort Prop + with fieldlist_ind2 := Induction for fieldlist Sort Prop. + +Lemma alignof_1248: + forall t, alignof t = 1 \/ alignof t = 2 \/ alignof t = 4 \/ alignof t = 8 +with alignof_fields_1248: + forall f, alignof_fields f = 1 \/ alignof_fields f = 2 \/ alignof_fields f = 4 \/ alignof_fields f = 8. +Proof. + induction t; simpl; auto. + destruct i; auto. + destruct f; auto. + induction f; simpl; auto. + rewrite Zmax_spec. destruct (zlt (alignof_fields f) (alignof t)); auto. +Qed. + +Lemma alignof_pos: + forall t, alignof t > 0. +Proof. + intros. generalize (alignof_1248 t). omega. +Qed. + +Lemma alignof_fields_pos: + forall f, alignof_fields f > 0. +Proof. + intros. generalize (alignof_fields_1248 f). omega. +Qed. + +(** Size of a type, in bytes. *) + +Fixpoint sizeof (t: type) : Z := + match t with + | Tvoid => 1 + | Tint I8 _ _ => 1 + | Tint I16 _ _ => 2 + | Tint I32 _ _ => 4 + | Tint IBool _ _ => 1 + | Tfloat F32 _ => 4 + | Tfloat F64 _ => 8 + | Tpointer _ _ => 4 + | Tarray t' n _ => sizeof t' * Zmax 1 n + | Tfunction _ _ => 1 + | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t) + | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t) + | Tcomp_ptr _ _ => 4 + end + +with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := + match fld with + | Fnil => pos + | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t) + end + +with sizeof_union (fld: fieldlist) : Z := + match fld with + | Fnil => 0 + | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld') + end. + +Lemma sizeof_pos: + forall t, sizeof t > 0. +Proof. + intro t0. + apply (type_ind2 (fun t => sizeof t > 0) + (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0)); + intros; simpl; auto; try omega. + destruct i; omega. + destruct f; omega. + apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega. + destruct H. + generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). + generalize (Zmax1 1 (sizeof_struct f 0)). omega. + generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). + generalize (Zmax1 1 (sizeof_union f)). omega. + split. omega. auto. + destruct H0. split; intros. + generalize (Zmax2 (sizeof t) (sizeof_union f)). omega. + apply H1. + 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. + +Lemma sizeof_alignof_compat: + forall t, (alignof t | sizeof t). +Proof. + induction t; simpl; try (apply Zdivide_refl). + apply Zdivide_mult_l. auto. + apply align_divides. apply alignof_fields_pos. + apply align_divides. apply alignof_fields_pos. +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. *) + +Open Local Scope string_scope. + +Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) + {struct fld} : res Z := + match fld with + | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) + | Fcons id' t fld' => + if ident_eq id id' + then OK (align pos (alignof t)) + else field_offset_rec id fld' (align pos (alignof t) + sizeof t) + end. + +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 sid fld a fid ofs ty, + field_offset fid fld = OK ofs -> field_type fid fld = OK ty -> + 0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a). +Proof. + intros. exploit field_offset_rec_in_range; eauto. intros [A B]. + split. auto. simpl. eapply Zle_trans. eauto. + eapply Zle_trans. eapply Zle_max_r. apply align_le. apply alignof_fields_pos. +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. eexact H1. eauto. tauto. + subst i. intros. inv H1; inv H2. + exploit field_offset_rec_in_range. eexact H. 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 common fields + are 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. + +(** Fourth, the position of each field respects its alignment. *) + +Lemma field_offset_aligned: + forall id fld ofs ty, + field_offset id fld = OK ofs -> field_type id fld = OK ty -> + (alignof ty | ofs). +Proof. + assert (forall id ofs ty fld pos, + field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> + (alignof ty | ofs)). + induction fld; simpl; intros. + discriminate. + destruct (ident_eq id i). inv H; inv H0. + apply align_divides. apply alignof_pos. + eapply IHfld; eauto. + intros. eapply H with (pos := 0); eauto. +Qed. + +(** The [access_mode] function describes how a l-value of the given +type must be accessed: +- [By_value ch]: access by value, i.e. by loading from the address + of the l-value using the memory chunk [ch]; +- [By_reference]: access by reference, i.e. by just returning + the address of the l-value (used for arrays and functions); +- [By_copy]: access is by reference, assignment is by copy + (used for [struct] and [union] types) +- [By_nothing]: no access is possible, e.g. for the [void] type. +*) + +Inductive mode: Type := + | By_value: memory_chunk -> mode + | By_reference: mode + | By_copy: mode + | By_nothing: mode. + +Definition access_mode (ty: type) : mode := + match ty with + | Tint I8 Signed _ => By_value Mint8signed + | Tint I8 Unsigned _ => By_value Mint8unsigned + | Tint I16 Signed _ => By_value Mint16signed + | Tint I16 Unsigned _ => By_value Mint16unsigned + | Tint I32 _ _ => By_value Mint32 + | Tint IBool _ _ => By_value Mint8unsigned + | Tfloat F32 _ => By_value Mfloat32 + | Tfloat F64 _ => By_value Mfloat64 + | Tvoid => By_nothing + | Tpointer _ _ => By_value Mint32 + | Tarray _ _ _ => By_reference + | Tfunction _ _ => By_reference + | Tstruct _ _ _ => By_copy + | Tunion _ _ _ => By_copy + | Tcomp_ptr _ _ => By_nothing +end. + +(** For the purposes of the semantics and the compiler, a type denotes + a volatile access if it carries the [volatile] attribute and it is + accessed by value. *) + +Definition type_is_volatile (ty: type) : bool := + match access_mode ty with + | By_value _ => attr_volatile (attr_of_type ty) + | _ => false + end. + +(** Unroll the type of a structure or union field, substituting + [Tcomp_ptr] by a pointer to the structure. *) + +Section UNROLL_COMPOSITE. + +Variable cid: ident. +Variable comp: type. + +Fixpoint unroll_composite (ty: type) : type := + match ty with + | Tvoid => ty + | Tint _ _ _ => ty + | Tfloat _ _ => ty + | Tpointer t1 a => Tpointer (unroll_composite t1) a + | Tarray t1 sz a => Tarray (unroll_composite t1) sz a + | Tfunction t1 t2 => Tfunction (unroll_composite_list t1) (unroll_composite t2) + | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a + | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a + | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty + end + +with unroll_composite_list (tl: typelist) : typelist := + match tl with + | Tnil => Tnil + | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl') + end + +with unroll_composite_fields (fld: fieldlist) : fieldlist := + match fld with + | Fnil => Fnil + | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld') + end. + +Lemma alignof_unroll_composite: + forall ty, alignof (unroll_composite ty) = alignof ty. +Proof. + apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty) + (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld)); + simpl; intros; auto. + destruct (ident_eq i cid); auto. + destruct (ident_eq i cid); auto. + destruct (ident_eq i cid); auto. + decEq; auto. +Qed. + +Lemma sizeof_unroll_composite: + forall ty, sizeof (unroll_composite ty) = sizeof ty. +Proof. +Opaque alignof. + apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty) + (fun fld => + sizeof_union (unroll_composite_fields fld) = sizeof_union fld + /\ forall pos, + sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); + simpl; intros; auto. + congruence. + destruct H. rewrite <- (alignof_unroll_composite (Tstruct i f a)). + simpl. destruct (ident_eq i cid); simpl. auto. rewrite H0; auto. + destruct H. rewrite <- (alignof_unroll_composite (Tunion i f a)). + simpl. destruct (ident_eq i cid); simpl. auto. rewrite H; auto. + destruct (ident_eq i cid); auto. + destruct H0. split. congruence. + intros. rewrite alignof_unroll_composite. rewrite H1. rewrite H. auto. +Qed. + +End UNROLL_COMPOSITE. + +(** Extracting a type list from a function parameter declaration. *) + +Fixpoint type_of_params (params: list (ident * type)) : typelist := + match params with + | nil => Tnil + | (id, ty) :: rem => Tcons ty (type_of_params rem) + end. + +(** Translating C types to Cminor types and function signatures. *) + +Definition typ_of_type (t: type) : AST.typ := + match t with + | Tfloat _ _ => AST.Tfloat + | _ => AST.Tint + end. + +Definition opttyp_of_type (t: type) : option AST.typ := + match t with + | Tvoid => None + | Tfloat _ _ => Some AST.Tfloat + | _ => Some AST.Tint + end. + +Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := + match tl with + | Tnil => nil + | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl + end. + +Definition signature_of_type (args: typelist) (res: type) : signature := + mksignature (typlist_of_typelist args) (opttyp_of_type res). diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 41dbe3f..641ea3c 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -19,6 +19,8 @@ Require Import Floats. Require Import Values. Require Import AST. Require Import Memory. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index a68013e..9bc1dd7 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -24,6 +24,8 @@ Require Import Memory. Require Import Globalenvs. Require Import Events. Require Import Smallstep. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. Require Import Initializers. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ae8e31d..7b9f3d3 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -21,7 +21,8 @@ open Datatypes open Values open AST open PrintAST -open Csyntax +open Ctypes +open Cop open PrintCsyntax open Clight diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 2c803bb..5490321 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -22,6 +22,8 @@ open Datatypes open Values open AST open Globalenvs +open Ctypes +open Cop open Csyntax let name_unop = function diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 6886d81..159ba99 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -19,6 +19,8 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import AST. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. Require Cstrategy. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 8a50fcb..40177f3 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -24,6 +24,8 @@ Require Import Memory. Require Import Events. Require Import Smallstep. Require Import Globalenvs. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Import Csem. Require Import Cstrategy. @@ -1883,6 +1885,14 @@ Proof. intros. inv H. auto. inv H0. auto. Qed. +Lemma alloc_variables_preserved: + forall e m params e' m', + Csem.alloc_variables e m params e' m' -> + alloc_variables e m params e' m'. +Proof. + induction 1; econstructor; eauto. +Qed. + Lemma bind_parameters_preserved: forall e m params args m', Csem.bind_parameters ge e m params args m' -> @@ -2138,7 +2148,7 @@ Proof. econstructor; split. left; apply plus_one. eapply step_internal_function. rewrite C; rewrite D; auto. - rewrite C; rewrite D; eauto. + rewrite C; rewrite D. eapply alloc_variables_preserved; eauto. rewrite C. eapply bind_parameters_preserved; eauto. constructor; auto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 3f9d7e9..5df0398 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -20,6 +20,8 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import AST. +Require Import Ctypes. +Require Import Cop. Require Import Csyntax. Require Cstrategy. Require Import Clight. diff --git a/doc/index.html b/doc/index.html index c6be1c2..095f082 100644 --- a/doc/index.html +++ b/doc/index.html @@ -116,8 +116,11 @@ semantics. <A HREF="html/Csyntax.html">syntax</A> and <A HREF="html/Csem.html">semantics</A> and <A HREF="html/Cstrategy.html">determinized semantics</A>.<BR> -See also: <A HREF="html/Cexec.html">reference interpreter</A>. +See also: <A HREF="html/Ctypes.html">type expressions</A> and +<A HREF="html/Cop.html">operators (syntax and semantics)</A> and +<A HREF="html/Cexec.html">reference interpreter</A>. <LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects. +<A HREF="html/Cop.html">operators (syntax and semantics)</A>. <LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level structured language. <LI> <A HREF="html/Cminor.html">Cminor</A>: low-level structured diff --git a/driver/Interp.ml b/driver/Interp.ml index 4061515..fc0526a 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -26,6 +26,8 @@ open Values open Memory open Globalenvs open Events +open Ctypes +open Cop open Csyntax open Csem open Clflags |