diff options
| -rw-r--r-- | .depend | 17 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 144 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 1999 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 6 | ||||
| -rw-r--r-- | extraction/extraction.v | 3 | ||||
| -rw-r--r-- | test/regression/Results/alignas | 4 | ||||
| -rw-r--r-- | test/regression/alignas.c | 6 |
8 files changed, 2101 insertions, 80 deletions
@@ -18,7 +18,7 @@ lib/FSetAVLplus.vo lib/FSetAVLplus.glob lib/FSetAVLplus.v.beautified: lib/FSetAV lib/IntvSets.vo lib/IntvSets.glob lib/IntvSets.v.beautified: lib/IntvSets.v lib/Coqlib.vo common/Errors.vo common/Errors.glob common/Errors.v.beautified: common/Errors.v lib/Coqlib.vo common/AST.vo common/AST.glob common/AST.v.beautified: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo -common/Events.vo common/Events.glob common/Events.v.beautified: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo +common/Events.vo common/Events.glob common/Events.v.beautified: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Globalenvs.vo common/Globalenvs.glob common/Globalenvs.v.beautified: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memtype.vo common/Memtype.glob common/Memtype.v.beautified: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo @@ -45,8 +45,8 @@ backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: backend/RTL.v lib/Coql backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgenspec.vo backend/RTLgenspec.glob backend/RTLgenspec.v.beautified: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenproof.vo backend/RTLgenproof.glob backend/RTLgenproof.v.beautified: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo -backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo -backend/Tailcallproof.vo backend/Tailcallproof.glob backend/Tailcallproof.v.beautified: backend/Tailcallproof.v lib/Coqlib.vo driver/Compopts.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo +backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo +backend/Tailcallproof.vo backend/Tailcallproof.glob backend/Tailcallproof.v.beautified: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo backend/Inlining.vo backend/Inlining.glob backend/Inlining.v.beautified: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inliningspec.vo backend/Inliningspec.glob backend/Inliningspec.v.beautified: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo backend/Inliningproof.vo backend/Inliningproof.glob backend/Inliningproof.v.beautified: backend/Inliningproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/Inlining.vo backend/Inliningspec.vo backend/RTL.vo @@ -98,13 +98,14 @@ $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmge backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo $(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.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 backend/Asmgenproof0.vo backend/Conventions.vo $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.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/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo -cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo +cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: 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.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo +cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Errors.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: 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/Ctyping.vo cfrontend/Ctyping.glob cfrontend/Ctyping.v.beautified: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo common/Errors.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified: 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.beautified: 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.beautified: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo +cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: 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.beautified: 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/Clight.vo cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo @@ -113,13 +114,13 @@ cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: cfronte cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob cfrontend/ClightBigstep.v.beautified: cfrontend/ClightBigstep.v lib/Coqlib.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/Clight.vo cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob cfrontend/SimplLocals.v.beautified: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocalsproof.vo cfrontend/SimplLocalsproof.glob cfrontend/SimplLocalsproof.v.beautified: cfrontend/SimplLocalsproof.v lib/Coqlib.vo common/Errors.vo lib/Ordered.vo common/AST.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocals.vo -cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob cfrontend/Cshmgen.v.beautified: 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/Cshmgen.vo cfrontend/Cshmgen.glob cfrontend/Cshmgen.v.beautified: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Maps.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.beautified: 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.beautified: 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 common/Switch.vo backend/Cminor.vo common/Smallstep.vo cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo lib/Floats.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: 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/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v -driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo +driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Unusedglobproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Compopts.vo driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob flocq/Core/Fcore_Zaux.v.beautified: flocq/Core/Fcore_Zaux.v @@ -104,7 +104,7 @@ BACKEND=\ # C front-end modules (in cfrontend/) -CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \ +CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \ Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ Clight.v ClightBigstep.v SimplLocals.v SimplLocalsproof.v \ diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index ea278ac1..ef621a7c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -127,6 +127,12 @@ let unsupported msg = let warning msg = eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg +let string_of_errmsg msg = + let string_of_err = function + | Errors.MSG s -> camlstring_of_coqstring s + | Errors.CTX i -> extern_atom i + | Errors.POS i -> Z.to_string (Z.Zpos i) + in String.concat "" (List.map string_of_err msg) (** ** The builtin environment *) @@ -448,9 +454,9 @@ let convertFloat f kind = | Z.Z0 -> begin match kind with | FFloat -> - Vsingle (Float.to_single Float.zero) + Ctyping.econst_single (Float.to_single Float.zero) | FDouble | FLongDouble -> - Vfloat Float.zero + Ctyping.econst_float Float.zero end | Z.Zpos mant -> @@ -465,9 +471,9 @@ let convertFloat f kind = begin match kind with | FFloat -> - Vsingle (Float32.from_parsed base mant exp) + Ctyping.econst_single (Float32.from_parsed base mant exp) | FDouble | FLongDouble -> - Vfloat (Float.from_parsed base mant exp) + Ctyping.econst_float (Float.from_parsed base mant exp) end | Z.Zneg _ -> assert false @@ -476,53 +482,59 @@ let convertFloat f kind = let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) +let ewrap = function + | Errors.OK e -> e + | Errors.Error msg -> + error ("retyping error: " ^ string_of_errmsg msg); ezero + let rec convertExpr env e = - let ty = convertTyp env e.etyp in + (*let ty = convertTyp env e.etyp in*) match e.edesc with | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in - Evalof(l, ty) + ewrap (Ctyping.evalof l) - | C.EConst(C.CInt(i, (ILongLong|IULongLong), _)) -> - Eval(Vlong(coqint_of_camlint64 i), ty) | C.EConst(C.CInt(i, k, _)) -> - Eval(Vint(convertInt i), ty) + let sg = if Cutil.is_signed_ikind k then Signed else Unsigned in + if k = ILongLong || k = IULongLong + then Ctyping.econst_long (coqint_of_camlint64 i) sg + else Ctyping.econst_int (convertInt i) sg | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point literal"; - Eval(convertFloat f k, ty) + convertFloat f k | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in Evalof(Evar(name_for_string_literal env s, ty), ty) | C.EConst(C.CWStr s) -> unsupported "wide string literal"; ezero | C.EConst(C.CEnum(id, i)) -> - Eval(Vint(convertInt i), ty) + Ctyping.econst_int (convertInt i) Signed | C.ESizeof ty1 -> - Esizeof(convertTyp env ty1, ty) + Ctyping.esizeof (convertTyp env ty1) | C.EAlignof ty1 -> - Ealignof(convertTyp env ty1, ty) + Ctyping.ealignof (convertTyp env ty1) | C.EUnop(C.Ominus, e1) -> - Eunop(Oneg, convertExpr env e1, ty) + ewrap (Ctyping.eunop Oneg (convertExpr env e1)) | C.EUnop(C.Oplus, e1) -> convertExpr env e1 | C.EUnop(C.Olognot, e1) -> - Eunop(Onotbool, convertExpr env e1, ty) + ewrap (Ctyping.eunop Onotbool (convertExpr env e1)) | C.EUnop(C.Onot, e1) -> - Eunop(Onotint, convertExpr env e1, ty) + ewrap (Ctyping.eunop Onotint (convertExpr env e1)) | C.EUnop(C.Oaddrof, e1) -> - Eaddrof(convertLvalue env e1, ty) + ewrap (Ctyping.eaddrof (convertLvalue env e1)) | C.EUnop(C.Opreincr, e1) -> - coq_Epreincr Incr (convertLvalue env e1) ty + ewrap (Ctyping.epreincr (convertLvalue env e1)) | C.EUnop(C.Opredecr, e1) -> - coq_Epreincr Decr (convertLvalue env e1) ty + ewrap (Ctyping.epredecr (convertLvalue env e1)) | C.EUnop(C.Opostincr, e1) -> - Epostincr(Incr, convertLvalue env e1, ty) + ewrap (Ctyping.epostincr (convertLvalue env e1)) | C.EUnop(C.Opostdecr, e1) -> - Epostincr(Decr, convertLvalue env e1, ty) + ewrap (Ctyping.epostdecr (convertLvalue env e1)) | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor| C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op, @@ -546,7 +558,7 @@ let rec convertExpr env e = | C.Ole -> Ole | C.Oge -> Oge | _ -> assert false in - Ebinop(op', convertExpr env e1, convertExpr env e2, ty) + ewrap (Ctyping.ebinop op' (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Oassign, e1, e2, _) -> let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in @@ -554,12 +566,11 @@ let rec convertExpr env e = && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then warning "assignment to a l-value of volatile composite type. \ The 'volatile' qualifier is ignored."; - Eassign(e1', e2', ty) + ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| C.Oshl_assign|C.Oshr_assign) as op, e1, e2, tyres) -> - let tyres = convertTyp env tyres in let op' = match op with | C.Oadd_assign -> Oadd @@ -575,18 +586,20 @@ let rec convertExpr env e = | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in - Eassignop(op', e1', e2', tyres, ty) + ewrap (Ctyping.eassignop op' e1' e2') | C.EBinop(C.Ocomma, e1, e2, _) -> - Ecomma(convertExpr env e1, convertExpr env e2, ty) + ewrap (Ctyping.ecomma (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Ologand, e1, e2, _) -> - Eseqand(convertExpr env e1, convertExpr env e2, ty) + ewrap (Ctyping.eseqand (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Ologor, e1, e2, _) -> - Eseqor(convertExpr env e1, convertExpr env e2, ty) + ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2)) | C.EConditional(e1, e2, e3) -> - Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty) + ewrap (Ctyping.econdition' (convertExpr env e1) + (convertExpr env e2) (convertExpr env e3) + (convertTyp env e.etyp)) | C.ECast(ty1, e1) -> - Ecast(convertExpr env e1, convertTyp env ty1) + ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero @@ -597,7 +610,7 @@ let rec convertExpr env e = Ebuiltin( EF_annot(intern_string txt, List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), - targs1, convertExprList env args1, ty) + targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; ezero @@ -609,7 +622,8 @@ let rec convertExpr env e = let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ), - Tcons(targ, Tnil), convertExprList env [arg], ty) + Tcons(targ, Tnil), convertExprList env [arg], + convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot_intval (first argument must be string literal)"; ezero @@ -619,15 +633,15 @@ let rec convertExpr env e = make_builtin_memcpy (convertExprList env args) | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> - Eunop(Oabsfloat, convertExpr env arg, ty) + ewrap (Ctyping.eunop Oabsfloat (convertExpr env arg)) | C.ECall({edesc = C.EVar {name = "__builtin_va_start"}} as fn, [arg]) -> Ecall(convertExpr env fn, Econs(va_list_ptr(convertExpr env arg), Enil), - ty) + convertTyp env e.etyp) | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> - make_builtin_va_arg env ty (convertExpr env arg1) + make_builtin_va_arg env (convertTyp env e.etyp) (convertExpr env arg1) | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) -> Ecast (ezero, Tvoid) @@ -643,12 +657,12 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "printf"}}, args) when !Clflags.option_interp -> - let targs = - convertTypArgs env [] args in + let targs = convertTypArgs env [] args + and tres = convertTyp env e.etyp in let sg = - signature_of_type targs ty {cc_vararg = true; cc_structret = false} in + signature_of_type targs tres {cc_vararg = true; cc_structret = false} in Ebuiltin(EF_external(intern_string "printf", sg), - targs, convertExprList env args, ty) + targs, convertExprList env args, tres) | C.ECall(fn, args) -> if not (supported_return_type env e.etyp) then @@ -662,26 +676,25 @@ let rec convertExpr env e = if va && not !Clflags.option_fvararg_calls then unsupported "call to variable-argument function (consider adding option -fvararg-calls)" end; - Ecall(convertExpr env fn, convertExprList env args, ty) + ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args)) and convertLvalue env e = - let ty = convertTyp env e.etyp in match e.edesc with | C.EVar id -> - Evar(intern_string id.name, ty) + Evar(intern_string id.name, convertTyp env e.etyp) | C.EUnop(C.Oderef, e1) -> - Ederef(convertExpr env e1, ty) + ewrap (Ctyping.ederef (convertExpr env e1)) | C.EUnop(C.Odot id, e1) -> - Efield(convertExpr env e1, intern_string id, ty) + ewrap (Ctyping.efield !comp_env (convertExpr env e1) (intern_string id)) | C.EUnop(C.Oarrow id, e1) -> let e1' = convertExpr env e1 in - let ty1 = - match typeof e1' with - | Tpointer(t, _) | Tarray(t, _, _) -> t - | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in - Efield(Evalof(Ederef(e1', ty1), ty1), intern_string id, ty) + let e2' = ewrap (Ctyping.ederef e1') in + let e3' = ewrap (Ctyping.evalof e2') in + ewrap (Ctyping.efield !comp_env e3' (intern_string id)) | C.EBinop(C.Oindex, e1, e2, _) -> - coq_Eindex (convertExpr env e1) (convertExpr env e2) ty + let e1' = convertExpr env e1 and e2' = convertExpr env e2 in + let e3' = ewrap (Ctyping.ebinop Oadd e1' e2') in + ewrap (Ctyping.ederef e3') | _ -> error "illegal l-value"; ezero @@ -737,30 +750,39 @@ let add_lineno prev_loc this_loc s = (** Statements *) +let swrap = function + | Errors.OK s -> s + | Errors.Error msg -> + error ("retyping error: " ^ string_of_errmsg msg); Sskip + let rec convertStmt ploc env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> Sskip | C.Sdo e -> - add_lineno ploc s.sloc (Sdo(convertExpr env e)) + add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e))) | C.Sseq(s1, s2) -> Ssequence(convertStmt ploc env s1, convertStmt s1.sloc env s2) | C.Sif(e, s1, s2) -> let te = convertExpr env e in add_lineno ploc s.sloc - (Sifthenelse(te, convertStmt s.sloc env s1, convertStmt s.sloc env s2)) + (swrap (Ctyping.sifthenelse te + (convertStmt s.sloc env s1) (convertStmt s.sloc env s2))) | C.Swhile(e, s1) -> let te = convertExpr env e in - add_lineno ploc s.sloc (Swhile(te, convertStmt s.sloc env s1)) + add_lineno ploc s.sloc + (swrap (Ctyping.swhile te (convertStmt s.sloc env s1))) | C.Sdowhile(s1, e) -> let te = convertExpr env e in - add_lineno ploc s.sloc (Sdowhile(te, convertStmt s.sloc env s1)) + add_lineno ploc s.sloc + (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1))) | C.Sfor(s1, e, s2, s3) -> let te = convertExpr env e in add_lineno ploc s.sloc - (Sfor(convertStmt s.sloc env s1, te, - convertStmt s.sloc env s2, convertStmt s.sloc env s3)) + (swrap (Ctyping.sfor + (convertStmt s.sloc env s1) te + (convertStmt s.sloc env s2) (convertStmt s.sloc env s3))) | C.Sbreak -> Sbreak | C.Scontinue -> @@ -773,7 +795,8 @@ let rec convertStmt ploc env s = warning "ignored code at beginning of 'switch'"; let te = convertExpr env e in add_lineno ploc s.sloc - (Sswitch(te, convertSwitch s.sloc env (is_longlong env e.etyp) cases)) + (swrap (Ctyping.sswitch te + (convertSwitch s.sloc env (is_longlong env e.etyp) cases))) | C.Slabeled(C.Slabel lbl, s1) -> add_lineno ploc s.sloc (Slabel(intern_string lbl, convertStmt s.sloc env s1)) @@ -876,13 +899,6 @@ let convertFundecl env (sto, id, ty, optinit) = (** Initializers *) -let string_of_errmsg msg = - let string_of_err = function - | Errors.MSG s -> camlstring_of_coqstring s - | Errors.CTX i -> extern_atom i - | Errors.POS i -> Z.to_string (Z.Zpos i) - in String.concat "" (List.map string_of_err msg) - let rec convertInit env init = match init with | C.Init_single e -> diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v new file mode 100644 index 00000000..43d34007 --- /dev/null +++ b/cfrontend/Ctyping.v @@ -0,0 +1,1999 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Typing rules and type-checking for the Compcert C language *) + +Require Import Coqlib. +Require Import String. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import AST. +Require Import Ctypes. +Require Import Cop. +Require Import Csyntax. +Require Import Csem. +Require Import Errors. + +Local Open Scope error_monad_scope. + +Definition strict := false. +Opaque strict. + +(** * Operations over types *) + +(** The type of a member of a composite (struct or union). + The "volatile" attribute carried by the composite propagates + to the type of the member, but not the "alignas" attribute. *) + +Definition attr_add_volatile (vol: bool) (a: attr) := + {| attr_volatile := a.(attr_volatile) || vol; + attr_alignas := a.(attr_alignas) |}. + +Definition type_of_member (a: attr) (f: ident) (m: members) : res type := + do ty <- field_type f m; + OK (change_attributes (attr_add_volatile a.(attr_volatile)) ty). + +(** Type-checking of arithmetic and logical operators *) + +Definition type_unop (op: unary_operation) (ty: type) : res type := + match op with + | Onotbool => + match classify_bool ty with + | bool_default => Error (msg "operator !") + | _ => OK (Tint I32 Signed noattr) + end + | Onotint => + match classify_notint ty with + | notint_case_i sg => OK (Tint I32 sg noattr) + | notint_case_l sg => OK (Tlong sg noattr) + | notint_default => Error (msg "operator ~") + end + | Oneg => + match classify_neg ty with + | neg_case_i sg => OK (Tint I32 sg noattr) + | neg_case_f => OK (Tfloat F64 noattr) + | neg_case_s => OK (Tfloat F32 noattr) + | neg_case_l sg => OK (Tlong sg noattr) + | neg_default => Error (msg "operator prefix -") + end + | Oabsfloat => + match classify_neg ty with + | neg_default => Error (msg "operator __builtin_fabs") + | _ => OK (Tfloat F64 noattr) + end + end. + +Definition binarith_type (ty1 ty2: type) (m: string): res type := + match classify_binarith ty1 ty2 with + | bin_case_i sg => OK (Tint I32 sg noattr) + | bin_case_l sg => OK (Tlong sg noattr) + | bin_case_f => OK (Tfloat F64 noattr) + | bin_case_s => OK (Tfloat F32 noattr) + | bin_default => Error (msg m) + end. + +Definition binarith_int_type (ty1 ty2: type) (m: string): res type := + match classify_binarith ty1 ty2 with + | bin_case_i sg => OK (Tint I32 sg noattr) + | bin_case_l sg => OK (Tlong sg noattr) + | _ => Error (msg m) + end. + +Definition shift_op_type (ty1 ty2: type) (m: string): res type := + match classify_shift ty1 ty2 with + | shift_case_ii sg | shift_case_il sg => OK (Tint I32 sg noattr) + | shift_case_li sg | shift_case_ll sg => OK (Tlong sg noattr) + | shift_default => Error (msg m) + end. + +Definition comparison_type (ty1 ty2: type) (m: string): res type := + match classify_cmp ty1 ty2 with + | cmp_default => + match classify_binarith ty1 ty2 with + | bin_default => Error (msg m) + | _ => OK (Tint I32 Signed noattr) + end + | _ => OK (Tint I32 Signed noattr) + end. + +Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type := + match op with + | Oadd => + match classify_add ty1 ty2 with + | add_case_pi ty | add_case_ip ty + | add_case_pl ty | add_case_lp ty => OK (Tpointer ty noattr) + | add_default => binarith_type ty1 ty2 "operator +" + end + | Osub => + match classify_sub ty1 ty2 with + | sub_case_pi ty | sub_case_pl ty => OK (Tpointer ty noattr) +(* + | sub_case_pp ty1 ty2 => + if type_eq (remove_attributes ty1) (remove_attributes ty2) + then OK (Tint I32 Signed noattr) + else Error (msg "operator - : incompatible pointer types") +*) + | sub_case_pp ty => OK (Tint I32 Signed noattr) + | sub_default => binarith_type ty1 ty2 "operator infix -" + end + | Omul => binarith_type ty1 ty2 "operator infix *" + | Odiv => binarith_type ty1 ty2 "operator /" + | Omod => binarith_int_type ty1 ty2 "operator %" + | Oand => binarith_int_type ty1 ty2 "operator &" + | Oor => binarith_int_type ty1 ty2 "operator |" + | Oxor => binarith_int_type ty1 ty2 "operator ^" + | Oshl => shift_op_type ty1 ty2 "operator <<" + | Oshr => shift_op_type ty1 ty2 "operator >>" + | Oeq => comparison_type ty1 ty2 "operator ==" + | One => comparison_type ty1 ty2 "operator !=" + | Olt => comparison_type ty1 ty2 "operator <" + | Ogt => comparison_type ty1 ty2 "operator >" + | Ole => comparison_type ty1 ty2 "operator <=" + | Oge => comparison_type ty1 ty2 "operator >=" + end. + +Definition type_deref (ty: type) : res type := + match ty with + | Tpointer tyelt _ => OK tyelt + | Tarray tyelt _ _ => OK tyelt + | Tfunction _ _ _ => OK ty + | _ => Error (msg "operator prefix *") + end. + +Definition is_void (ty: type) : bool := + match ty with Tvoid => true | _ => false end. + +Definition type_join (ty1 ty2: type) : res type := + match typeconv ty1, typeconv ty2 with + | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) => + binarith_type ty1 ty2 "conditional expression" + | Tpointer t1 a1, Tpointer t2 a2 => + OK (Tpointer (if is_void t1 || is_void t2 then Tvoid else t1) noattr) + | Tpointer t1 a1, Tint _ _ _ => + OK (Tpointer t1 noattr) + | Tint _ _ _, Tpointer t2 a2 => + OK (Tpointer t2 noattr) + | Tvoid, Tvoid => + OK Tvoid + | Tstruct id1 a1, Tstruct id2 a2 => + if ident_eq id1 id2 + then OK (Tstruct id1 noattr) + else Error (msg "conditional expression") + | Tunion id1 a1, Tunion id2 a2 => + if ident_eq id1 id2 + then OK (Tunion id1 noattr) + else Error (msg "conditional expression") + | _, _ => + Error (msg "conditional expression") + end. + +(** * Specification of the type system *) + +(** Type environments map identifiers to their types. *) + +Definition typenv := PTree.t type. + +Definition wt_cast (from to: type) : Prop := + classify_cast from to <> cast_case_default. + +Definition wt_bool (ty: type) : Prop := + classify_bool ty <> bool_default. + +Definition wt_int (n: int) (sz: intsize) (sg: signedness) : Prop := + match sz, sg with + | IBool, _ => Int.zero_ext 8 n = n + | I8, Unsigned => Int.zero_ext 8 n = n + | I8, Signed => Int.sign_ext 8 n = n + | I16, Unsigned => Int.zero_ext 16 n = n + | I16, Signed => Int.sign_ext 16 n = n + | I32, _ => True + end. + +Inductive wt_val : val -> type -> Prop := + | wt_val_int: forall n sz sg a, + wt_int n sz sg -> + wt_val (Vint n) (Tint sz sg a) + | wt_val_ptr_int: forall b ofs sg a, + wt_val (Vptr b ofs) (Tint I32 sg a) + | wt_val_long: forall n sg a, + wt_val (Vlong n) (Tlong sg a) + | wt_val_float: forall f a, + wt_val (Vfloat f) (Tfloat F64 a) + | wt_val_single: forall f a, + wt_val (Vsingle f) (Tfloat F32 a) + | wt_val_pointer: forall b ofs ty a, + wt_val (Vptr b ofs) (Tpointer ty a) + | wt_val_int_pointer: forall n ty a, + wt_val (Vint n) (Tpointer ty a) + | wt_val_array: forall b ofs ty sz a, + wt_val (Vptr b ofs) (Tarray ty sz a) + | wt_val_function: forall b ofs tyargs tyres cc, + wt_val (Vptr b ofs) (Tfunction tyargs tyres cc) + | wt_val_struct: forall b ofs id a, + wt_val (Vptr b ofs) (Tstruct id a) + | wt_val_union: forall b ofs id a, + wt_val (Vptr b ofs) (Tunion id a) + | wt_val_undef: forall ty, + wt_val Vundef ty + | wt_val_void: forall v, + wt_val v Tvoid. + +Inductive wt_arguments: exprlist -> typelist -> Prop := + | wt_arg_nil: + wt_arguments Enil Tnil + | wt_arg_cons: forall a al ty tyl, + wt_cast (typeof a) ty -> + wt_arguments al tyl -> + wt_arguments (Econs a al) (Tcons ty tyl) + | wt_arg_extra: forall a al, (**r tolerance for varargs *) + strict = false -> + wt_arguments (Econs a al) Tnil. + +Definition subtype (t1 t2: type) : Prop := + forall v, wt_val v t1 -> wt_val v t2. + +Section WT_EXPR_STMT. + +Variable ce: composite_env. +Variable e: typenv. + +Inductive wt_rvalue : expr -> Prop := + | wt_Eval: forall v ty, + wt_val v ty -> + wt_rvalue (Eval v ty) + | wt_Evalof: forall l, + wt_lvalue l -> + wt_rvalue (Evalof l (typeof l)) + | wt_Eaddrof: forall l, + wt_lvalue l -> + wt_rvalue (Eaddrof l (Tpointer (typeof l) noattr)) + | wt_Eunop: forall op r ty, + wt_rvalue r -> + type_unop op (typeof r) = OK ty -> + wt_rvalue (Eunop op r ty) + | wt_Ebinop: forall op r1 r2 ty, + wt_rvalue r1 -> wt_rvalue r2 -> + type_binop op (typeof r1) (typeof r2) = OK ty -> + wt_rvalue (Ebinop op r1 r2 ty) + | wt_Ecast: forall r ty, + wt_rvalue r -> wt_cast (typeof r) ty -> + wt_rvalue (Ecast r ty) + | wt_Eseqand: forall r1 r2, + wt_rvalue r1 -> wt_rvalue r2 -> + wt_bool (typeof r1) -> wt_bool (typeof r2) -> + wt_rvalue (Eseqand r1 r2 (Tint I32 Signed noattr)) + | wt_Eseqor: forall r1 r2, + wt_rvalue r1 -> wt_rvalue r2 -> + wt_bool (typeof r1) -> wt_bool (typeof r2) -> + wt_rvalue (Eseqor r1 r2 (Tint I32 Signed noattr)) + | wt_Econdition: forall r1 r2 r3 ty, + wt_rvalue r1 -> wt_rvalue r2 -> wt_rvalue r3 -> + wt_bool (typeof r1) -> + wt_cast (typeof r2) ty -> wt_cast (typeof r3) ty -> + wt_rvalue (Econdition r1 r2 r3 ty) + | wt_Esizeof: forall ty, + wt_rvalue (Esizeof ty (Tint I32 Unsigned noattr)) + | wt_Ealignof: forall ty, + wt_rvalue (Ealignof ty (Tint I32 Unsigned noattr)) + | wt_Eassign: forall l r, + wt_lvalue l -> wt_rvalue r -> wt_cast (typeof r) (typeof l) -> + wt_rvalue (Eassign l r (typeof l)) + | wt_Eassignop: forall op l r ty, + wt_lvalue l -> wt_rvalue r -> + type_binop op (typeof l) (typeof r) = OK ty -> + wt_cast ty (typeof l) -> + wt_rvalue (Eassignop op l r ty (typeof l)) + | wt_Epostincr: forall id l ty, + wt_lvalue l -> + type_binop (match id with Incr => Oadd | Decr => Osub end) + (typeof l) (Tint I32 Signed noattr) = OK ty -> + wt_cast (incrdecr_type (typeof l)) (typeof l) -> + wt_rvalue (Epostincr id l (typeof l)) + | wt_Ecomma: forall r1 r2, + wt_rvalue r1 -> wt_rvalue r2 -> + wt_rvalue (Ecomma r1 r2 (typeof r2)) + | wt_Ecall: forall r1 rargs tyargs tyres cconv, + wt_rvalue r1 -> wt_exprlist rargs -> + classify_fun (typeof r1) = fun_case_f tyargs tyres cconv -> + wt_arguments rargs tyargs -> + wt_rvalue (Ecall r1 rargs tyres) + | wt_Ebuiltin: forall ef tyargs rargs, + wt_exprlist rargs -> + wt_arguments rargs tyargs -> + (* This is specialized to builtins returning void, the only + case generated by C2C. *) + sig_res (ef_sig ef) = None -> + wt_rvalue (Ebuiltin ef tyargs rargs Tvoid) + | wt_Eparen: forall r tycast ty, + wt_rvalue r -> + wt_cast (typeof r) tycast -> subtype tycast ty -> + wt_rvalue (Eparen r tycast ty) + +with wt_lvalue : expr -> Prop := + | wt_Eloc: forall b ofs ty, + wt_lvalue (Eloc b ofs ty) + | wt_Evar: forall x ty, + e!x = Some ty -> + wt_lvalue (Evar x ty) + | wt_Ederef: forall r ty, + wt_rvalue r -> + type_deref (typeof r) = OK ty -> + wt_lvalue (Ederef r ty) + | wt_Efield: forall r f id a co ty, + wt_rvalue r -> + typeof r = Tstruct id a \/ typeof r = Tunion id a -> + ce!id = Some co -> + type_of_member a f co.(co_members) = OK ty -> + wt_lvalue (Efield r f ty) + +with wt_exprlist : exprlist -> Prop := + | wt_Enil: + wt_exprlist Enil + | wt_Econs: forall r1 rl, + wt_rvalue r1 -> wt_exprlist rl -> wt_exprlist (Econs r1 rl). + +Definition wt_expr_kind (k: kind) (a: expr) := + match k with + | RV => wt_rvalue a + | LV => wt_lvalue a + end. + +Definition expr_kind (a: expr) : kind := + match a with + | Eloc _ _ _ => LV + | Evar _ _ => LV + | Ederef _ _ => LV + | Efield _ _ _ => LV + | _ => RV + end. + +Definition wt_expr (a: expr) := + match expr_kind a with + | RV => wt_rvalue a + | LV => wt_lvalue a + end. + +Variable rt: type. + +Inductive wt_stmt: statement -> Prop := + | wt_Sskip: + wt_stmt Sskip + | wt_Sdo: forall r, + wt_rvalue r -> wt_stmt (Sdo r) + | wt_Ssequence: forall s1 s2, + wt_stmt s1 -> wt_stmt s2 -> wt_stmt (Ssequence s1 s2) + | wt_Sifthenelse: forall r s1 s2, + wt_rvalue r -> wt_stmt s1 -> wt_stmt s2 -> wt_bool (typeof r) -> + wt_stmt (Sifthenelse r s1 s2) + | wt_Swhile: forall r s, + wt_rvalue r -> wt_stmt s -> wt_bool (typeof r) -> + wt_stmt (Swhile r s) + | wt_Sdowhile: forall r s, + wt_rvalue r -> wt_stmt s -> wt_bool (typeof r) -> + wt_stmt (Sdowhile r s) + | wt_Sfor: forall s1 r s2 s3, + wt_rvalue r -> wt_stmt s1 -> wt_stmt s2 -> wt_stmt s3 -> + wt_bool (typeof r) -> + wt_stmt (Sfor s1 r s2 s3) + | wt_Sbreak: + wt_stmt Sbreak + | wt_Scontinue: + wt_stmt Scontinue + | wt_Sreturn_none: + wt_stmt (Sreturn None) + | wt_Sreturn_some: forall r, + wt_rvalue r -> + wt_cast (typeof r) rt -> + wt_stmt (Sreturn (Some r)) + | wt_Sswitch: forall r ls sg sz a, + wt_rvalue r -> + typeof r = Tint sz sg a \/ typeof r = Tlong sg a -> + wt_lblstmts ls -> + wt_stmt (Sswitch r ls) + | wt_Slabel: forall lbl s, + wt_stmt s -> wt_stmt (Slabel lbl s) + | wt_Sgoto: forall lbl, + wt_stmt (Sgoto lbl) + +with wt_lblstmts : labeled_statements -> Prop := + | wt_LSnil: + wt_lblstmts LSnil + | wt_LScons: forall case s ls, + wt_stmt s -> wt_lblstmts ls -> + wt_lblstmts (LScons case s ls). + +End WT_EXPR_STMT. + +Fixpoint bind_vars (e: typenv) (l: list (ident * type)) : typenv := + match l with + | nil => e + | (id, ty) :: l => bind_vars (PTree.set id ty e) l + end. + +Inductive wt_function (ce: composite_env) (e: typenv) : function -> Prop := + | wt_function_intro: forall f, + wt_stmt ce (bind_vars (bind_vars e f.(fn_params)) f.(fn_vars)) f.(fn_return) f.(fn_body) -> + wt_function ce e f. + +Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : typenv := + match l with + | nil => e + | (id, Gfun fd) :: l => bind_globdef (PTree.set id (type_of_fundef fd) e) l + | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l + end. + +Inductive wt_program : program -> Prop := + | wt_program_intro: forall p, + let e := bind_globdef (PTree.empty _) p.(prog_defs) in + (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> + wt_function p.(prog_comp_env) e f) -> + wt_program p. + +Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. +Hint Extern 1 (wt_int _ _ _) => exact I: ty. +Hint Extern 1 (wt_int _ _ _) => reflexivity: ty. + +Ltac DestructCases := + match goal with + | [H: match match ?x with _ => _ end with _ => _ end = Some _ |- _ ] => destruct x; DestructCases + | [H: match match ?x with _ => _ end with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = Some _ |- _ ] => destruct x; DestructCases + | [H: match ?x with _ => _ end = OK _ |- _ ] => destruct x; DestructCases + | [H: Some _ = Some _ |- _ ] => inv H; DestructCases + | [H: None = Some _ |- _ ] => discriminate + | [H: OK _ = OK _ |- _ ] => inv H; DestructCases + | [H: Error _ = OK _ |- _ ] => discriminate + | _ => idtac + end. + +Ltac DestructMatch := + match goal with + | [ |- match match ?x with _ => _ end with _ => _ end ] => destruct x; DestructMatch + | [ |- match ?x with _ => _ end ] => destruct x; DestructMatch + | _ => idtac + end. + +(** * Type checking *) + +Definition check_cast (t1 t2: type) : res unit := + match classify_cast t1 t2 with + | cast_case_default => Error (msg "illegal cast") + | _ => OK tt + end. + +Definition check_bool (t: type) : res unit := + match classify_bool t with + | bool_default => Error (msg "not a boolean") + | _ => OK tt + end. + +Definition check_literal (v: val) (t: type) : res unit := + match v, t with + | Vint n, Tint I32 sg a => OK tt + | Vint n, Tpointer t' a => OK tt + | Vlong n, Tlong sg a => OK tt + | Vsingle f, Tfloat F32 a => OK tt + | Vfloat f, Tfloat F64 a => OK tt + | _, _ => Error (msg "wrong literal") + end. + +Fixpoint check_arguments (el: exprlist) (tyl: typelist) : res unit := + match el, tyl with + | Enil, Tnil => OK tt + | Enil, _ => Error (msg "not enough arguments") + | _, Tnil => if strict then Error (msg "too many arguments") else OK tt + | Econs e1 el, Tcons ty1 tyl => do x <- check_cast (typeof e1) ty1; check_arguments el tyl + end. + +Definition check_rval (e: expr) : res unit := + match e with + | Eloc _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => + Error (msg "not a r-value") + | _ => + OK tt + end. + +Definition check_lval (e: expr) : res unit := + match e with + | Eloc _ _ _ | Evar _ _ | Ederef _ _ | Efield _ _ _ => + OK tt + | _ => + Error (msg "not a l-value") + end. + +Fixpoint check_rvals (el: exprlist) : res unit := + match el with + | Enil => OK tt + | Econs e1 el => do x <- check_rval e1; check_rvals el + end. + +(** Type-checking of expressions is presented as smart constructors + that check type constraints and build the expression with the correct + type annotation. *) + +Definition evar (e: typenv) (x: ident) : res expr := + match e!x with + | Some ty => OK (Evar x ty) + | None => Error (MSG "unbound variable " :: CTX x :: nil) + end. + +Definition ederef (r: expr) : res expr := + do x1 <- check_rval r; + do ty <- type_deref (typeof r); + OK (Ederef r ty). + +Definition efield (ce: composite_env) (r: expr) (f: ident) : res expr := + do x1 <- check_rval r; + match typeof r with + | Tstruct id a | Tunion id a => + match ce!id with + | None => Error (MSG "unbound composite " :: CTX id :: nil) + | Some co => + do ty <- type_of_member a f co.(co_members); + OK (Efield r f ty) + end + | _ => + Error (MSG "argument of ." :: CTX f :: MSG " is not a struct or union" :: nil) + end. + +Definition econst_int (n: int) (sg: signedness) : expr := + (Eval (Vint n) (Tint I32 sg noattr)). + +Definition econst_ptr_int (n: int) (ty: type) : expr := + (Eval (Vint n) (Tpointer ty noattr)). + +Definition econst_long (n: int64) (sg: signedness) : expr := + (Eval (Vlong n) (Tlong sg noattr)). + +Definition econst_float (n: float) : expr := + (Eval (Vfloat n) (Tfloat F64 noattr)). + +Definition econst_single (n: float32) : expr := + (Eval (Vsingle n) (Tfloat F32 noattr)). + +Definition evalof (l: expr) : res expr := + do x <- check_lval l; OK (Evalof l (typeof l)). + +Definition eaddrof (l: expr) : res expr := + do x <- check_lval l; OK (Eaddrof l (Tpointer (typeof l) noattr)). + +Definition eunop (op: unary_operation) (r: expr) : res expr := + do x <- check_rval r; + do ty <- type_unop op (typeof r); + OK (Eunop op r ty). + +Definition ebinop (op: binary_operation) (r1 r2: expr) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; + do ty <- type_binop op (typeof r1) (typeof r2); + OK (Ebinop op r1 r2 ty). + +Definition ecast (ty: type) (r: expr) : res expr := + do x1 <- check_rval r; + do x2 <- check_cast (typeof r) ty; + OK (Ecast r ty). + +Definition eseqand (r1 r2: expr) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; + do y1 <- check_bool (typeof r1); do y2 <- check_bool (typeof r2); + OK (Eseqand r1 r2 type_int32s). + +Definition eseqor (r1 r2: expr) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; + do y1 <- check_bool (typeof r1); do y2 <- check_bool (typeof r2); + OK (Eseqor r1 r2 type_int32s). + +Definition econdition (r1 r2 r3: expr) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3; + do y1 <- check_bool (typeof r1); + do ty <- type_join (typeof r2) (typeof r3); + OK (Econdition r1 r2 r3 ty). + +Definition econdition' (r1 r2 r3: expr) (ty: type) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3; + do y1 <- check_bool (typeof r1); + do y2 <- check_cast (typeof r2) ty; + do y3 <- check_cast (typeof r3) ty; + OK (Econdition r1 r2 r3 ty). + +Definition esizeof (ty: type) : expr := + Esizeof ty (Tint I32 Unsigned noattr). + +Definition ealignof (ty: type) : expr := + Ealignof ty (Tint I32 Unsigned noattr). + +Definition eassign (l r: expr) : res expr := + do x1 <- check_lval l; do x2 <- check_rval r; + do y1 <- check_cast (typeof r) (typeof l); + OK (Eassign l r (typeof l)). + +Definition eassignop (op: binary_operation) (l r: expr) : res expr := + do x1 <- check_lval l; do x2 <- check_rval r; + do ty <- type_binop op (typeof l) (typeof r); + do y1 <- check_cast ty (typeof l); + OK (Eassignop op l r ty (typeof l)). + +Definition epostincrdecr (id: incr_or_decr) (l: expr) : res expr := + do x1 <- check_lval l; + do ty <- type_binop (match id with Incr => Oadd | Decr => Osub end) + (typeof l) type_int32s; + do y1 <- check_cast (incrdecr_type (typeof l)) (typeof l); + OK (Epostincr id l (typeof l)). + +Definition epostincr (l: expr) := epostincrdecr Incr l. +Definition epostdecr (l: expr) := epostincrdecr Decr l. + +Definition epreincr (l: expr) := eassignop Oadd l (Eval (Vint Int.one) type_int32s). +Definition epredecr (l: expr) := eassignop Osub l (Eval (Vint Int.one) type_int32s). + +Definition ecomma (r1 r2: expr) : res expr := + do x1 <- check_rval r1; do x2 <- check_rval r2; + OK (Ecomma r1 r2 (typeof r2)). + +Definition ecall (fn: expr) (args: exprlist) : res expr := + do x1 <- check_rval fn; do x2 <- check_rvals args; + match classify_fun (typeof fn) with + | fun_case_f tyargs tyres cconv => + do y1 <- check_arguments args tyargs; + OK (Ecall fn args tyres) + | _ => + Error (msg "call: not a function") + end. + +Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist) (tyres: type) : res expr := + do x1 <- check_rvals args; + do x2 <- check_arguments args tyargs; + if type_eq tyres Tvoid + && opt_typ_eq (sig_res (ef_sig ef)) None + then OK (Ebuiltin ef tyargs args tyres) + else Error (msg "builtin: wrong type decoration"). + +Definition sdo (a: expr) : res statement := + do x <- check_rval a; OK (Sdo a). + +Definition sifthenelse (a: expr) (s1 s2: statement) : res statement := + do x <- check_rval a; do y <- check_bool (typeof a); OK (Sifthenelse a s1 s2). + +Definition swhile (a: expr) (s: statement) : res statement := + do x <- check_rval a; do y <- check_bool (typeof a); OK (Swhile a s). + +Definition sdowhile (a: expr) (s: statement) : res statement := + do x <- check_rval a; do y <- check_bool (typeof a); OK (Sdowhile a s). + +Definition sfor (s1: statement) (a: expr) (s2 s3: statement) : res statement := + do x <- check_rval a; do y <- check_bool (typeof a); OK (Sfor s1 a s2 s3). + +Definition sreturn (rt: type) (a: expr) : res statement := + do x <- check_rval a; do y <- check_cast (typeof a) rt; + OK (Sreturn (Some a)). + +Definition sswitch (a: expr) (sl: labeled_statements) : res statement := + do x <- check_rval a; + match typeof a with + | Tint _ _ _ | Tlong _ _ => OK (Sswitch a sl) + | _ => Error (msg "wrong type for argument of switch") + end. + +(** Using the smart constructors, we define a type checker that rebuilds + a correctly-type-annotated program. *) + +Fixpoint retype_expr (ce: composite_env) (e: typenv) (a: expr) : res expr := + match a with + | Eval (Vint n) (Tint _ sg _) => + OK (econst_int n sg) + | Eval (Vint n) (Tpointer ty _) => + OK (econst_ptr_int n ty) + | Eval (Vlong n) (Tlong sg _) => + OK (econst_long n sg) + | Eval (Vfloat n) _ => + OK (econst_float n) + | Eval (Vsingle n) _ => + OK (econst_single n) + | Eval _ _ => + Error (msg "bad literal") + | Evar x _ => + evar e x + | Efield r f _ => + do r' <- retype_expr ce e r; efield ce r' f + | Evalof l _ => + do l' <- retype_expr ce e l; evalof l' + | Ederef r _ => + do r' <- retype_expr ce e r; ederef r' + | Eaddrof l _ => + do l' <- retype_expr ce e l; eaddrof l' + | Eunop op r _ => + do r' <- retype_expr ce e r; eunop op r' + | Ebinop op r1 r2 _ => + do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; ebinop op r1' r2' + | Ecast r ty => + do r' <- retype_expr ce e r; ecast ty r' + | Eseqand r1 r2 _ => + do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; eseqand r1' r2' + | Eseqor r1 r2 _ => + do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; eseqor r1' r2' + | Econdition r1 r2 r3 _ => + do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; do r3' <- retype_expr ce e r3; econdition r1' r2' r3' + | Esizeof ty _ => + OK (esizeof ty) + | Ealignof ty _ => + OK (ealignof ty) + | Eassign l r _ => + do l' <- retype_expr ce e l; do r' <- retype_expr ce e r; eassign l' r' + | Eassignop op l r _ _ => + do l' <- retype_expr ce e l; do r' <- retype_expr ce e r; eassignop op l' r' + | Epostincr id l _ => + do l' <- retype_expr ce e l; epostincrdecr id l' + | Ecomma r1 r2 _ => + do r1' <- retype_expr ce e r1; do r2' <- retype_expr ce e r2; ecomma r1' r2' + | Ecall r1 rl _ => + do r1' <- retype_expr ce e r1; do rl' <- retype_exprlist ce e rl; ecall r1' rl' + | Ebuiltin ef tyargs rl tyres => + do rl' <- retype_exprlist ce e rl; ebuiltin ef tyargs rl' tyres + | Eloc _ _ _ => + Error (msg "Eloc in source") + | Eparen _ _ _ => + Error (msg "Eparen in source") + end + +with retype_exprlist (ce: composite_env) (e: typenv) (al: exprlist) : res exprlist := + match al with + | Enil => OK Enil + | Econs a1 al => + do a1' <- retype_expr ce e a1; + do al' <- retype_exprlist ce e al; + do x1 <- check_rval a1'; + OK (Econs a1' al') + end. + +Fixpoint retype_stmt (ce: composite_env) (e: typenv) (rt: type) (s: statement) : res statement := + match s with + | Sskip => + OK Sskip + | Sdo a => + do a' <- retype_expr ce e a; sdo a' + | Ssequence s1 s2 => + do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2; OK (Ssequence s1' s2') + | Sifthenelse a s1 s2 => + do a' <- retype_expr ce e a; + do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2; + sifthenelse a' s1' s2' + | Swhile a s => + do a' <- retype_expr ce e a; + do s' <- retype_stmt ce e rt s; + swhile a' s' + | Sdowhile a s => + do a' <- retype_expr ce e a; + do s' <- retype_stmt ce e rt s; + sdowhile a' s' + | Sfor s1 a s2 s3 => + do a' <- retype_expr ce e a; + do s1' <- retype_stmt ce e rt s1; do s2' <- retype_stmt ce e rt s2; do s3' <- retype_stmt ce e rt s3; + sfor s1' a' s2' s3' + | Sbreak => + OK Sbreak + | Scontinue => + OK Scontinue + | Sreturn None => + OK (Sreturn None) + | Sreturn (Some a) => + do a' <- retype_expr ce e a; + sreturn rt a' + | Sswitch a sl => + do a' <- retype_expr ce e a; + do sl' <- retype_lblstmts ce e rt sl; + sswitch a' sl' + | Slabel lbl s => + do s' <- retype_stmt ce e rt s; OK (Slabel lbl s') + | Sgoto lbl => + OK (Sgoto lbl) + end + +with retype_lblstmts (ce: composite_env) (e: typenv) (rt: type) (sl: labeled_statements) : res labeled_statements := + match sl with + | LSnil => OK LSnil + | LScons case s sl => + do s' <- retype_stmt ce e rt s; do sl' <- retype_lblstmts ce e rt sl; + OK (LScons case s' sl') + end. + +Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res function := + let e := bind_vars (bind_vars e f.(fn_params)) f.(fn_vars) in + do s <- retype_stmt ce e f.(fn_return) f.(fn_body); + OK (mkfunction f.(fn_return) + f.(fn_callconv) + f.(fn_params) + f.(fn_vars) + s). + +(** Soundness of the smart constructors. *) + +Lemma check_cast_sound: + forall t1 t2 x, check_cast t1 t2 = OK x -> wt_cast t1 t2. +Proof. + unfold check_cast, wt_cast; intros. + destruct (classify_cast t1 t2); congruence. +Qed. + +Lemma check_bool_sound: + forall t x, check_bool t = OK x -> wt_bool t. +Proof. + unfold check_bool, wt_bool; intros. + destruct (classify_bool t); congruence. +Qed. + +Hint Resolve check_cast_sound check_bool_sound: ty. + +Lemma check_arguments_sound: + forall el tl x, check_arguments el tl = OK x -> wt_arguments el tl. +Proof. + intros el tl; revert tl el. + induction tl; destruct el; simpl; intros; try discriminate. + constructor. + destruct strict eqn:S; try discriminate. constructor; auto. + monadInv H. constructor; eauto with ty. +Qed. + +Lemma check_rval_sound: + forall a x, check_rval a = OK x -> expr_kind a = RV. +Proof. + unfold check_rval; intros. destruct a; reflexivity || discriminate. +Qed. + +Lemma check_lval_sound: + forall a x, check_lval a = OK x -> expr_kind a = LV. +Proof. + unfold check_lval; intros. destruct a; reflexivity || discriminate. +Qed. + +Lemma binarith_type_cast: + forall t1 t2 m t, + binarith_type t1 t2 m = OK t -> wt_cast t1 t /\ wt_cast t2 t. +Proof. + unfold wt_cast, binarith_type, classify_binarith; intros; DestructCases; + simpl; split; try congruence. destruct f; congruence. +Qed. + +Lemma typeconv_cast: + forall t1 t2, wt_cast (typeconv t1) t2 -> wt_cast t1 t2. +Proof. + unfold typeconv, wt_cast; intros. destruct t1; auto. + assert (classify_cast (Tint I32 Signed a) t2 <> cast_case_default -> + classify_cast (Tint i s a) t2 <> cast_case_default). + { + unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + } + destruct i; auto. +Qed. + +Lemma type_join_cast: + forall t1 t2 t, + type_join t1 t2 = OK t -> wt_cast t1 t /\ wt_cast t2 t. +Proof. + intros. unfold type_join in H. + destruct (typeconv t1) eqn:T1; try discriminate; + destruct (typeconv t2) eqn:T2; inv H. +- unfold wt_cast; simpl; split; congruence. +- eapply binarith_type_cast; eauto. +- eapply binarith_type_cast; eauto. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- eapply binarith_type_cast; eauto. +- eapply binarith_type_cast; eauto. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- destruct (ident_eq i i0); inv H1. + split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +- destruct (ident_eq i i0); inv H1. + split; apply typeconv_cast; unfold wt_cast. + rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. +Qed. + +Section SOUNDNESS_CONSTRUCTORS. + +Variable ce: composite_env. +Variable e: typenv. +Variable rt: type. + +Corollary check_rval_wt: + forall a x, wt_expr ce e a -> check_rval a = OK x -> wt_rvalue ce e a. +Proof. + unfold wt_expr; intros. erewrite check_rval_sound in H by eauto. auto. +Qed. + +Corollary check_lval_wt: + forall a x, wt_expr ce e a -> check_lval a = OK x -> wt_lvalue ce e a. +Proof. + unfold wt_expr; intros. erewrite check_lval_sound in H by eauto. auto. +Qed. + +Hint Resolve check_rval_wt check_lval_wt: ty. +Hint Extern 1 (wt_expr _ _ _) => (unfold wt_expr; simpl): ty. + +Lemma evar_sound: + forall x a, evar e x = OK a -> wt_expr ce e a. +Proof. + unfold evar; intros. destruct (e!x) as [ty|] eqn:E; inv H. eauto with ty. +Qed. + +Lemma ederef_sound: + forall r a, ederef r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma efield_sound: + forall r f a, efield ce r f = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. + destruct (typeof r) eqn:TR; try discriminate; + destruct (ce!i) as [co|] eqn:CE; monadInv EQ0; eauto with ty. +Qed. + +Lemma econst_int_sound: + forall n sg, wt_expr ce e (econst_int n sg). +Proof. + unfold econst_int; auto with ty. +Qed. + +Lemma econst_ptr_int_sound: + forall n ty, wt_expr ce e (econst_ptr_int n ty). +Proof. + unfold econst_ptr_int; auto with ty. +Qed. + +Lemma econst_long_sound: + forall n sg, wt_expr ce e (econst_long n sg). +Proof. + unfold econst_long; auto with ty. +Qed. + +Lemma econst_float_sound: + forall n, wt_expr ce e (econst_float n). +Proof. + unfold econst_float; auto with ty. +Qed. + +Lemma econst_single_sound: + forall n, wt_expr ce e (econst_single n). +Proof. + unfold econst_single; auto with ty. +Qed. + +Lemma evalof_sound: + forall l a, evalof l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma eaddrof_sound: + forall l a, eaddrof l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma eunop_sound: + forall op r a, eunop op r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma ebinop_sound: + forall op r1 r2 a, ebinop op r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma ecast_sound: + forall ty r a, ecast ty r = OK a -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma eseqand_sound: + forall r1 r2 a, eseqand r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma eseqor_sound: + forall r1 r2 a, eseqor r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma econdition_sound: + forall r1 r2 r3 a, econdition r1 r2 r3 = OK a -> + wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a. +Proof. + intros. monadInv H. apply type_join_cast in EQ3. destruct EQ3. eauto 10 with ty. +Qed. + +Lemma econdition'_sound: + forall r1 r2 r3 ty a, econdition' r1 r2 r3 ty = OK a -> + wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma esizeof_sound: + forall ty, wt_expr ce e (esizeof ty). +Proof. + unfold esizeof; auto with ty. +Qed. + +Lemma ealignof_sound: + forall ty, wt_expr ce e (ealignof ty). +Proof. + unfold ealignof; auto with ty. +Qed. + +Lemma eassign_sound: + forall l r a, eassign l r = OK a -> wt_expr ce e l -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma eassignop_sound: + forall op l r a, eassignop op l r = OK a -> wt_expr ce e l -> wt_expr ce e r -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma epostincrdecr_sound: + forall id l a, epostincrdecr id l = OK a -> wt_expr ce e l -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma ecomma_sound: + forall r1 r2 a, ecomma r1 r2 = OK a -> wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e a. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma ecall_sound: + forall fn args a, ecall fn args = OK a -> wt_expr ce e fn -> wt_exprlist ce e args -> wt_expr ce e a. +Proof. + intros. monadInv H. + destruct (classify_fun (typeof fn)) eqn:CF; monadInv EQ2. + econstructor; eauto with ty. eapply check_arguments_sound; eauto. +Qed. + +Lemma ebuiltin_sound: + forall ef tyargs args tyres a, + ebuiltin ef tyargs args tyres = OK a -> wt_exprlist ce e args -> wt_expr ce e a. +Proof. + intros. monadInv H. + destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. + destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + econstructor; eauto. eapply check_arguments_sound; eauto. +Qed. + +Lemma sdo_sound: + forall a s, sdo a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma sifthenelse_sound: + forall a s1 s2 s, sifthenelse a s1 s2 = OK s -> + wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s2 -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma swhile_sound: + forall a s1 s, swhile a s1 = OK s -> + wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma sdowhile_sound: + forall a s1 s, sdowhile a s1 = OK s -> + wt_expr ce e a -> wt_stmt ce e rt s1 -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto with ty. +Qed. + +Lemma sfor_sound: + forall s1 a s2 s3 s, sfor s1 a s2 s3 = OK s -> + wt_stmt ce e rt s1 -> wt_expr ce e a -> wt_stmt ce e rt s2 -> wt_stmt ce e rt s3 -> + wt_stmt ce e rt s. +Proof. + intros. monadInv H. eauto 10 with ty. +Qed. + +Lemma sreturn_sound: + forall a s, sreturn rt a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s. +Proof. + intros. monadInv H; eauto with ty. +Qed. + +Lemma sswitch_sound: + forall a sl s, sswitch a sl = OK s -> + wt_expr ce e a -> wt_lblstmts ce e rt sl -> wt_stmt ce e rt s. +Proof. + intros. monadInv H. destruct (typeof a) eqn:TA; inv EQ0. + eauto with ty. + eapply wt_Sswitch with (sz := I32); eauto with ty. +Qed. + +Lemma retype_expr_sound: + forall a a', retype_expr ce e a = OK a' -> wt_expr ce e a' +with retype_exprlist_sound: + forall al al', retype_exprlist ce e al = OK al' -> wt_exprlist ce e al'. +Proof. +- destruct a; simpl; intros a' RT; try (monadInv RT). ++ destruct v; try discriminate. + destruct ty; inv RT. apply econst_int_sound. apply econst_ptr_int_sound. + destruct ty; inv RT. apply econst_long_sound. + inv RT. apply econst_float_sound. + inv RT. apply econst_single_sound. ++ eapply evar_sound; eauto. ++ eapply efield_sound; eauto. ++ eapply evalof_sound; eauto. ++ eapply ederef_sound; eauto. ++ eapply eaddrof_sound; eauto. ++ eapply eunop_sound; eauto. ++ eapply ebinop_sound; eauto. ++ eapply ecast_sound; eauto. ++ eapply eseqand_sound; eauto. ++ eapply eseqor_sound; eauto. ++ eapply econdition_sound; eauto. ++ apply esizeof_sound. ++ apply ealignof_sound. ++ eapply eassign_sound; eauto. ++ eapply eassignop_sound; eauto. ++ eapply epostincrdecr_sound; eauto. ++ eapply ecomma_sound; eauto. ++ eapply ecall_sound; eauto. ++ eapply ebuiltin_sound; eauto. +- destruct al; simpl; intros al' RT; monadInv RT. ++ constructor. ++ constructor; eauto with ty. +Qed. + +Lemma retype_stmt_sound: + forall s s', retype_stmt ce e rt s = OK s' -> wt_stmt ce e rt s' +with retype_lblstmts_sound: + forall sl sl', retype_lblstmts ce e rt sl = OK sl' -> wt_lblstmts ce e rt sl'. +Proof. +- destruct s; simpl; intros s' RT; try (monadInv RT). ++ constructor. ++ eapply sdo_sound; eauto using retype_expr_sound. ++ constructor; eauto. ++ eapply sifthenelse_sound; eauto using retype_expr_sound. ++ eapply swhile_sound; eauto using retype_expr_sound. ++ eapply sdowhile_sound; eauto using retype_expr_sound. ++ eapply sfor_sound; eauto using retype_expr_sound. ++ constructor. ++ constructor. ++ destruct o; monadInv RT. eapply sreturn_sound; eauto using retype_expr_sound. constructor. ++ eapply sswitch_sound; eauto using retype_expr_sound. ++ constructor; eauto. ++ constructor. +- destruct sl; simpl; intros sl' RT; monadInv RT. ++ constructor. ++ constructor; eauto. +Qed. + +End SOUNDNESS_CONSTRUCTORS. + +Lemma retype_function_sound: + forall ce e f f', retype_function ce e f = OK f' -> wt_function ce e f'. +Proof. + intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. +Qed. + +(** * Subject reduction *) + +(** We show that reductions preserve well-typedness *) + +Lemma pres_cast_int_int: + forall sz sg n, wt_int (cast_int_int sz sg n) sz sg. +Proof. + intros. unfold cast_int_int. destruct sz; simpl. +- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- destruct sg. apply Int.sign_ext_idem; omega. apply Int.zero_ext_idem; omega. +- auto. +- destruct (Int.eq n Int.zero); auto. +Qed. + +Hint Resolve pres_cast_int_int: ty. + +Lemma pres_sem_cast: + forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2. +Proof. + unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Int.eq n Int.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Int64.eq n Int64.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Float.cmp Ceq f Float.zero); auto with ty. +- constructor. apply (pres_cast_int_int I8 s). +- constructor. apply (pres_cast_int_int I16 s). +- destruct (Float32.cmp Ceq f Float32.zero); auto with ty. +- destruct (Int.eq n Int.zero); auto with ty. +Qed. + +Lemma pres_sem_binarith: + forall + (sem_int: signedness -> int -> int -> option val) + (sem_long: signedness -> int64 -> int64 -> option val) + (sem_float: float -> float -> option val) + (sem_single: float32 -> float32 -> option val) + v1 ty1 v2 ty2 v ty msg, + (forall sg n1 n2, + match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> + (forall sg n1 n2, + match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) -> + (forall n1 n2, + match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) -> + (forall n1 n2, + match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) -> + sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 = Some v -> + binarith_type ty1 ty2 msg = OK ty -> + wt_val v ty. +Proof with (try discriminate). + intros. unfold sem_binarith, binarith_type in *. + set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. + destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1... + destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2... + DestructCases. +- specialize (H s i i0). rewrite H3 in H. + destruct v; auto with ty; contradiction. +- specialize (H0 s i i0). rewrite H3 in H0. + destruct v; auto with ty; contradiction. +- specialize (H1 f f0). rewrite H3 in H1. + destruct v; auto with ty; contradiction. +- specialize (H2 f f0). rewrite H3 in H2. + destruct v; auto with ty; contradiction. +Qed. + +Lemma pres_sem_binarith_int: + forall + (sem_int: signedness -> int -> int -> option val) + (sem_long: signedness -> int64 -> int64 -> option val) + v1 ty1 v2 ty2 v ty msg, + (forall sg n1 n2, + match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> + (forall sg n1 n2, + match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) -> + sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 = Some v -> + binarith_int_type ty1 ty2 msg = OK ty -> + wt_val v ty. +Proof. + intros. eapply pres_sem_binarith with (msg := msg); eauto. + simpl; auto. simpl; auto. + unfold binarith_int_type, binarith_type in *. + destruct (classify_binarith ty1 ty2); congruence. +Qed. + +Lemma pres_sem_shift: + forall sem_int sem_long ty1 ty2 m ty v1 v2 v, + shift_op_type ty1 ty2 m = OK ty -> + sem_shift sem_int sem_long v1 ty1 v2 ty2 = Some v -> + wt_val v ty. +Proof. + intros. unfold shift_op_type, sem_shift in *. DestructCases; auto with ty. +Qed. + +Lemma pres_sem_cmp: + forall ty1 ty2 msg ty c v1 v2 m v, + comparison_type ty1 ty2 msg = OK ty -> + sem_cmp c v1 ty1 v2 ty2 m = Some v -> + wt_val v ty. +Proof with (try discriminate). + unfold comparison_type, sem_cmp; intros. + assert (X: forall b, wt_val (Val.of_bool b) (Tint I32 Signed noattr)). + { + intros b; destruct b; constructor; exact I. + } + assert (Y: forall ob, option_map Val.of_bool ob = Some v -> wt_val v (Tint I32 Signed noattr)). + { + intros ob EQ. destruct ob as [b|]; inv EQ. eauto. + } + destruct (classify_cmp ty1 ty2). +- inv H; eauto. +- DestructCases; eauto. +- DestructCases; eauto. +- unfold sem_binarith in H0. + set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. + destruct (sem_cast v1 ty1 ty') as [v1'|]... + destruct (sem_cast v2 ty2 ty') as [v2'|]... + DestructCases; auto. +Qed. + +Lemma pres_sem_binop: + forall ce op ty1 ty2 ty v1 v2 v m, + type_binop op ty1 ty2 = OK ty -> + sem_binary_operation ce op v1 ty1 v2 ty2 m = Some v -> + wt_val v1 ty1 -> wt_val v2 ty2 -> + wt_val v ty. +Proof. + intros until m; intros TY SEM WT1 WT2. + destruct op; simpl in TY; simpl in SEM. +- (* add *) + unfold sem_add in SEM; DestructCases; auto with ty. + eapply pres_sem_binarith; eauto; intros; exact I. +- (* sub *) + unfold sem_sub in SEM; DestructCases; auto with ty. + eapply pres_sem_binarith; eauto; intros; exact I. +- (* mul *) + unfold sem_mul in SEM. eapply pres_sem_binarith; eauto; intros; exact I. +- (* div *) + unfold sem_div in SEM. eapply pres_sem_binarith; eauto; intros. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. +- (* mod *) + unfold sem_mod in SEM. eapply pres_sem_binarith_int; eauto; intros. + simpl; DestructMatch; auto. + simpl; DestructMatch; auto. +- (* and *) + unfold sem_and in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* or *) + unfold sem_or in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* xor *) + unfold sem_xor in SEM. eapply pres_sem_binarith_int; eauto; intros; exact I. +- (* shl *) + unfold sem_shl in SEM. eapply pres_sem_shift; eauto. +- (* shr *) + unfold sem_shr in SEM. eapply pres_sem_shift; eauto. +- (* comparisons *) + eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +- eapply pres_sem_cmp; eauto. +Qed. + +Lemma pres_sem_unop: + forall op ty1 ty v1 v, + type_unop op ty1 = OK ty -> + sem_unary_operation op v1 ty1 = Some v -> + wt_val v1 ty1 -> + wt_val v ty. +Proof. + intros until v; intros TY SEM WT1. + destruct op; simpl in TY; simpl in SEM. +- (* notbool *) + unfold sem_notbool in SEM; DestructCases. + destruct (Int.eq i Int.zero); constructor; auto with ty. + destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. + destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. + destruct (Int.eq i Int.zero); constructor; auto with ty. + constructor; auto with ty. + destruct (Int64.eq i Int64.zero); constructor; auto with ty. +- (* notint *) + unfold sem_notint in SEM; DestructCases; auto with ty. +- (* neg *) + unfold sem_neg in SEM; DestructCases; auto with ty. +- (* absfloat *) + unfold sem_absfloat in SEM; DestructCases; auto with ty. +Qed. + +Lemma wt_load_result: + forall ty chunk v, + access_mode ty = By_value chunk -> + wt_val (Val.load_result chunk v) ty. +Proof. + intros until v; intros AC. destruct ty; simpl in AC; try discriminate. + destruct i; [destruct s|destruct s|idtac|idtac]; inv AC; simpl; destruct v; auto with ty. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + inv AC; simpl; destruct v; auto with ty. + destruct f; inv AC; simpl; destruct v; auto with ty. + inv AC; simpl; destruct v; auto with ty. +Qed. + +Lemma wt_decode_val: + forall ty chunk vl, + access_mode ty = By_value chunk -> + wt_val (decode_val chunk vl) ty. +Proof. + intros until vl; intros ACC. + destruct ty; simpl in ACC; try discriminate. +- destruct i; [destruct s|destruct s|idtac|idtac]; inv ACC; unfold decode_val; + destruct (proj_bytes vl); auto with ty. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + constructor; red. apply Int.sign_ext_idem; omega. + constructor; red. apply Int.zero_ext_idem; omega. + apply wt_load_result. auto. + constructor; red. apply Int.zero_ext_idem; omega. +- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. +- destruct f; inv ACC; unfold decode_val; destruct (proj_bytes vl); auto with ty. +- inv ACC. unfold decode_val. destruct (proj_bytes vl); auto with ty. + apply wt_load_result. auto. +Qed. + +Lemma wt_deref_loc: + forall ge ty m b ofs t v, + deref_loc ge ty m b ofs t v -> + wt_val v ty. +Proof. + induction 1. +- (* by value, non volatile *) + simpl in H1. exploit Mem.load_result; eauto. intros EQ; rewrite EQ. + apply wt_decode_val; auto. +- (* by value, volatile *) + inv H1. + + (* truly volatile *) + eapply wt_load_result; eauto. + + (* not really volatile *) + exploit Mem.load_result; eauto. intros EQ; rewrite EQ. + apply wt_decode_val; auto. +- (* by reference *) + destruct ty; simpl in H; try discriminate; auto with ty. + destruct i; destruct s; discriminate. + destruct f; discriminate. +- (* by copy *) + destruct ty; simpl in H; try discriminate; auto with ty. + destruct i; destruct s; discriminate. + destruct f; discriminate. +Qed. + +Lemma wt_bool_cast: + forall ty, wt_bool ty -> wt_cast ty type_bool. +Proof. + unfold wt_bool, wt_cast; unfold classify_bool; intros. destruct ty; simpl in *; try congruence. destruct f; congruence. +Qed. + +Lemma wt_cast_self: + forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2. +Proof. + unfold wt_cast; intros. destruct t2; simpl in *; try congruence. + destruct i; congruence. + destruct f; congruence. +Qed. + +Lemma binarith_type_int32s: + forall ty1 msg ty2, + binarith_type ty1 type_int32s msg = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + intros. unfold incrdecr_type. + unfold binarith_type, classify_binarith in H; simpl in H. + destruct ty1; simpl; try congruence. + destruct i; destruct s; try congruence. + destruct s; congruence. + destruct f; congruence. +Qed. + +Lemma type_add_int32s: + forall ty1 ty2, + type_binop Oadd ty1 type_int32s = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + simpl; intros. unfold classify_add in H; destruct ty1; simpl in H; + try (eapply binarith_type_int32s; eauto; fail). + destruct i; eapply binarith_type_int32s; eauto. + inv H; auto. + inv H; auto. + inv H; auto. +Qed. + +Lemma type_sub_int32s: + forall ty1 ty2, + type_binop Osub ty1 type_int32s = OK ty2 -> + ty2 = incrdecr_type ty1. +Proof. + simpl; intros. unfold classify_sub in H; destruct ty1; simpl in H; + try (eapply binarith_type_int32s; eauto; fail). + destruct i; eapply binarith_type_int32s; eauto. + inv H; auto. + inv H; auto. + inv H; auto. +Qed. + +Lemma wt_rred: + forall ge tenv a m t a' m', + rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'. +Proof. + induction 1; intros WT; inversion WT. +- (* valof *) simpl in *. constructor. eapply wt_deref_loc; eauto. +- (* addrof *) constructor; auto with ty. +- (* unop *) simpl in H4. inv H2. constructor. eapply pres_sem_unop; eauto. +- (* binop *) + simpl in H6. inv H3. inv H5. constructor. eapply pres_sem_binop; eauto. +- (* cast *) inv H2. constructor. eapply pres_sem_cast; eauto. +- (* sequand true *) subst. constructor. auto. apply wt_bool_cast; auto. + red; intros. inv H0; auto with ty. +- (* sequand false *) constructor. auto with ty. +- (* seqor true *) constructor. auto with ty. +- (* seqor false *) subst. constructor. auto. apply wt_bool_cast; auto. + red; intros. inv H0; auto with ty. +- (* condition *) constructor. destruct b; auto. destruct b; auto. red; auto. +- (* sizeof *) constructor; auto with ty. +- (* alignof *) constructor; auto with ty. +- (* assign *) inversion H5. constructor. eapply pres_sem_cast; eauto. +- (* assignop *) subst tyres l r. constructor. auto. + constructor. constructor. eapply wt_deref_loc; eauto. + auto. auto. auto. +- (* postincr *) simpl in *. subst id0 l. + exploit wt_deref_loc; eauto. intros WTV1. + constructor. + constructor. auto. rewrite <- H0 in H5. constructor. + constructor; auto. constructor. constructor. auto with ty. + subst op. destruct id. + erewrite <- type_add_int32s by eauto. auto. + erewrite <- type_sub_int32s by eauto. auto. + simpl; auto. + constructor; auto. +- (* comma *) auto. +- (* paren *) inv H3. constructor. apply H5. eapply pres_sem_cast; eauto. +- (* builtin *) subst. auto with ty. +Qed. + +Lemma wt_lred: + forall tenv ge e a m a' m', + lred ge e a m a' m' -> wt_lvalue ge tenv a -> wt_lvalue ge tenv a'. +Proof. + induction 1; intros WT; constructor. +Qed. + +Lemma rred_same_type: + forall ge a m t a' m', + rred ge a m t a' m' -> typeof a' = typeof a. +Proof. + induction 1; auto. +Qed. + +Lemma lred_same_type: + forall ge e a m a' m', + lred ge e a m a' m' -> typeof a' = typeof a. +Proof. + induction 1; auto. +Qed. + +Section WT_CONTEXT. + +Variable cenv: composite_env. +Variable tenv: typenv. +Variable a a': expr. +Hypothesis SAMETY: typeof a' = typeof a. + +Lemma wt_subexpr: + forall from to C, + context from to C -> + wt_expr_kind cenv tenv to (C a) -> + wt_expr_kind cenv tenv from a +with wt_subexprlist: + forall from C, + contextlist from C -> + wt_exprlist cenv tenv (C a) -> + wt_expr_kind cenv tenv from a. +Proof. + destruct 1; intros WT; auto; inv WT; eauto. + destruct 1; intros WT; inv WT; eauto. +Qed. + +Lemma typeof_context: + forall from to C, context from to C -> typeof (C a') = typeof (C a). +Proof. + induction 1; simpl; auto. +Qed. + +Lemma wt_arguments_context: + forall k C, contextlist k C -> + forall tyl, wt_arguments (C a) tyl -> wt_arguments (C a') tyl. +Proof. + induction 1; intros. +- inv H0. constructor; auto. rewrite (typeof_context _ _ _ H); auto. + constructor; auto. +- inv H0. constructor; auto. constructor; auto. +Qed. + +Lemma wt_context: + forall from to C, + context from to C -> + wt_expr_kind cenv tenv to (C a) -> + wt_expr_kind cenv tenv from a' -> + wt_expr_kind cenv tenv to (C a') +with wt_contextlist: + forall from C, + contextlist from C -> + wt_exprlist cenv tenv (C a) -> + wt_expr_kind cenv tenv from a' -> + wt_exprlist cenv tenv (C a'). +Proof. +- induction 1; intros WT BASE; + auto; + inv WT; + try (pose (EQTY := typeof_context _ _ _ H); rewrite <- ? EQTY; econstructor; + try (apply IHcontext; assumption); rewrite ? EQTY; eauto). +* red. econstructor; eauto. eapply wt_arguments_context; eauto. +* red. econstructor; eauto. eapply wt_arguments_context; eauto. +- induction 1; intros WT BASE. +* inv WT. constructor. apply (wt_context _ _ _ H); auto. auto. +* inv WT. constructor; auto. +Qed. + +End WT_CONTEXT. + +Section WT_SWITCH. + +Lemma wt_select_switch: + forall n ce e rt sl, + wt_lblstmts ce e rt sl -> wt_lblstmts ce e rt (select_switch n sl). +Proof. + unfold select_switch; intros. + assert (A: wt_lblstmts ce e rt (select_switch_default sl)). + { + revert sl H. induction 1; simpl; intros. + constructor. + destruct case. auto. constructor; auto. + } + assert (B: forall sl', select_switch_case n sl = Some sl' -> wt_lblstmts ce e rt sl'). + { + revert H. generalize sl. induction 1; simpl; intros. + discriminate. + destruct case; eauto. destruct (zeq z n); eauto. inv H1. econstructor; eauto. + } + destruct (select_switch_case n sl); auto. +Qed. + +Lemma wt_seq_of_ls: + forall ce e rt sl, + wt_lblstmts ce e rt sl -> wt_stmt ce e rt (seq_of_labeled_statement sl). +Proof. + induction 1; simpl. + constructor. + constructor; auto. +Qed. + +End WT_SWITCH. + +Section PRESERVATION. + +Variable prog: program. +Hypothesis WTPROG: wt_program prog. +Let ge := globalenv prog. +Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs). + +Hypothesis WT_EXTERNAL: + forall id ef args res cc vargs m t vres m', + In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> + external_call ef ge vargs m t vres m' -> + wt_val vres res. + +Inductive wt_expr_cont: typenv -> function -> cont -> Prop := + | wt_Kdo: forall te f k, + wt_stmt_cont te f k -> + wt_expr_cont te f (Kdo k) + | wt_Kifthenelse: forall te f s1 s2 k, + wt_stmt_cont te f k -> + wt_stmt ge te f.(fn_return) s1 -> wt_stmt ge te f.(fn_return) s2 -> + wt_expr_cont te f (Kifthenelse s1 s2 k) + | wt_Kwhile1: forall te f r s k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) -> + wt_expr_cont te f (Kwhile1 r s k) + | wt_Kdowhile2: forall te f r s k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) -> + wt_expr_cont te f (Kdowhile2 r s k) + | wt_Kfor2: forall te f r s2 s3 k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 -> + classify_bool (typeof r) <> bool_default -> + wt_expr_cont te f (Kfor2 r s2 s3 k) + | wt_Kswitch1: forall te f ls k, + wt_stmt_cont te f k -> + wt_lblstmts ge te f.(fn_return) ls -> + wt_expr_cont te f (Kswitch1 ls k) + | wt_Kreturn: forall te f k, + wt_stmt_cont te f k -> + wt_expr_cont te f (Kreturn k) + +with wt_stmt_cont: typenv -> function -> cont -> Prop := + | wt_Kseq: forall te f s k, + wt_stmt_cont te f k -> + wt_stmt ge te f.(fn_return) s -> + wt_stmt_cont te f (Kseq s k) + | wt_Kwhile2: forall te f r s k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) -> + wt_stmt_cont te f (Kwhile2 r s k) + | wt_Kdowhile1: forall te f r s k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s -> wt_bool (typeof r) -> + wt_stmt_cont te f (Kdowhile1 r s k) + | wt_Kfor3: forall te f r s2 s3 k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 -> + wt_bool (typeof r) -> + wt_stmt_cont te f (Kfor3 r s2 s3 k) + | wt_Kfor4: forall te f r s2 s3 k, + wt_stmt_cont te f k -> + wt_rvalue ge te r -> wt_stmt ge te f.(fn_return) s2 -> wt_stmt ge te f.(fn_return) s3 -> + wt_bool (typeof r) -> + wt_stmt_cont te f (Kfor4 r s2 s3 k) + | wt_Kswitch2: forall te f k, + wt_stmt_cont te f k -> + wt_stmt_cont te f (Kswitch2 k) + | wt_Kstop': forall te f, + wt_stmt_cont te f Kstop + | wt_Kcall': forall te f f' e C ty k, + wt_call_cont (Kcall f' e C ty k) ty -> + ty = f.(fn_return) -> + wt_stmt_cont te f (Kcall f' e C ty k) + +with wt_call_cont: cont -> type -> Prop := + | wt_Kstop: forall ty, + wt_call_cont Kstop ty + | wt_Kcall: forall te f e C ty k, + wt_expr_cont te f k -> + wt_stmt ge te f.(fn_return) f.(fn_body) -> + (forall v, wt_val v ty -> wt_rvalue ge te (C (Eval v ty))) -> + wt_call_cont (Kcall f e C ty k) ty. + +Lemma is_wt_call_cont: + forall te f k, + is_call_cont k -> wt_stmt_cont te f k -> wt_call_cont k f.(fn_return). +Proof. + intros. inv H0; simpl in H; try contradiction. constructor. auto. +Qed. + +Lemma wt_call_cont_stmt_cont: + forall te f k, wt_call_cont k f.(fn_return) -> wt_stmt_cont te f k. +Proof. + intros. inversion H; subst. constructor. constructor; auto. +Qed. + +Lemma call_cont_wt: + forall e f k, wt_stmt_cont e f k -> wt_call_cont (call_cont k) f.(fn_return). +Proof. + induction 1; simpl; auto. + constructor. + congruence. +Qed. + +Lemma call_cont_wt': + forall e f k, wt_stmt_cont e f k -> wt_stmt_cont e f (call_cont k). +Proof. + induction 1; simpl; auto; econstructor; eauto. +Qed. + +Definition wt_fundef (fd: fundef) := + match fd with + | Internal f => wt_function ge gtenv f + | External ef targs tres cc => True + end. + +Definition fundef_return (fd: fundef) : type := + match fd with + | Internal f => f.(fn_return) + | External ef targs tres cc => tres + end. + +Lemma wt_find_funct: + forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd. +Proof. + intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. + intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. +Qed. + +Inductive wt_state: state -> Prop := + | wt_stmt_state: forall f s k e m te + (WTK: wt_stmt_cont te f k) + (WTB: wt_stmt ge te f.(fn_return) f.(fn_body)) + (WTS: wt_stmt ge te f.(fn_return) s), + wt_state (State f s k e m) + | wt_expr_state: forall f r k e m te + (WTK: wt_expr_cont te f k) + (WTB: wt_stmt ge te f.(fn_return) f.(fn_body)) + (WTE: wt_rvalue ge te r), + wt_state (ExprState f r k e m) + | wt_call_state: forall b fd vargs k m + (WTK: wt_call_cont k (fundef_return fd)) + (WTFD: wt_fundef fd) + (FIND: Genv.find_funct ge b = Some fd), + wt_state (Callstate fd vargs k m) + | wt_return_state: forall v k m ty + (WTK: wt_call_cont k ty) + (VAL: wt_val v ty), + wt_state (Returnstate v k m) + | wt_stuck_state: + wt_state Stuckstate. + +Hint Constructors wt_expr_cont wt_stmt_cont wt_stmt wt_state: ty. + +Section WT_FIND_LABEL. + +Scheme wt_stmt_ind2 := Minimality for wt_stmt Sort Prop + with wt_lblstmts2_ind2 := Minimality for wt_lblstmts Sort Prop. + +Lemma wt_find_label: + forall lbl e f s, wt_stmt ge e f.(fn_return) s -> + forall k s' k', + find_label lbl s k = Some (s', k') -> + wt_stmt_cont e f k -> + wt_stmt ge e f.(fn_return) s' /\ wt_stmt_cont e f k'. +Proof. + intros lbl e f s0 WTS0. pattern s0. + apply (wt_stmt_ind2 ge e f.(fn_return)) with + (P0 := fun ls => wt_lblstmts ge e f.(fn_return) ls -> + forall k s' k', + find_label_ls lbl ls k = Some (s', k') -> + wt_stmt_cont e f k -> + wt_stmt ge e f.(fn_return) s' /\ wt_stmt_cont e f k'); + simpl; intros; try discriminate. + + destruct (find_label lbl s1 (Kseq s2 k)) as [[sx kx] | ] eqn:F. + inv H3. eauto with ty. + eauto with ty. + + destruct (find_label lbl s1 k) as [[sx kx] | ] eqn:F. + inv H5. eauto with ty. + eauto with ty. + + eauto with ty. + + eauto with ty. + + destruct (find_label lbl s1 (Kseq (Sfor Sskip r s2 s3) k)) as [[sx kx] | ] eqn:F. + inv H7. eauto with ty. + destruct (find_label lbl s3 (Kfor3 r s2 s3 k)) as [[sx kx] | ] eqn:F2. + inv H7. eauto with ty. + eauto with ty. + + eauto with ty. + + destruct (ident_eq lbl lbl0). + inv H1. auto. + eauto. + + destruct (find_label lbl s (Kseq (seq_of_labeled_statement ls) k)) as [[sx kx] | ] eqn:F. + inv H4. eapply H0; eauto. constructor. auto. apply wt_seq_of_ls; auto. + eauto. + + assumption. +Qed. + +End WT_FIND_LABEL. + + +Lemma preservation_estep: + forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. +Proof. + induction 1; intros WT; inv WT. +- (* lred *) + econstructor; eauto. change (wt_expr_kind ge te RV (C a')). + eapply wt_context with (a := a); eauto. + eapply lred_same_type; eauto. + eapply wt_lred; eauto. change (wt_expr_kind ge te LV a). eapply wt_subexpr; eauto. +- (* rred *) + econstructor; eauto. change (wt_expr_kind ge te RV (C a')). + eapply wt_context with (a := a); eauto. + eapply rred_same_type; eauto. + eapply wt_rred; eauto. change (wt_expr_kind ge te RV a). eapply wt_subexpr; eauto. +- (* call *) + assert (A: wt_expr_kind ge te RV a) by (eapply wt_subexpr; eauto). + simpl in A. inv H. inv A. simpl in H9; rewrite H4 in H9; inv H9. + assert (fundef_return fd = ty). + { destruct fd; simpl in *. + unfold type_of_function in H3. congruence. + congruence. } + econstructor. + rewrite H. econstructor; eauto. + intros. change (wt_expr_kind ge te RV (C (Eval v ty))). + eapply wt_context with (a := Ecall (Eval vf tyf) el ty); eauto. + red; constructor; auto. + eapply wt_find_funct; eauto. + eauto. +- (* stuck *) + constructor. +Qed. + +Lemma preservation_sstep: + forall S t S', sstep ge S t S' -> wt_state S -> wt_state S'. +Proof. + induction 1; intros WT; inv WT. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; destruct b; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- inv WTS; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- econstructor. eapply call_cont_wt; eauto. constructor. +- inv WTS. eauto with ty. +- inv WTK. econstructor. eapply call_cont_wt; eauto. + inv WTE. eapply pres_sem_cast; eauto. +- econstructor. eapply is_wt_call_cont; eauto. constructor. +- inv WTS; eauto with ty. +- inv WTK. econstructor; eauto with ty. + apply wt_seq_of_ls. apply wt_select_switch; auto. +- inv WTK; eauto with ty. +- inv WTK; eauto with ty. +- inv WTS; eauto with ty. +- exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. + intros [A B]. eauto with ty. +- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). + econstructor; eauto. +- inv WTK. eauto with ty. +Qed. + +Theorem preservation: + forall S t S', step ge S t S' -> wt_state S -> wt_state S'. +Proof. + intros. destruct H. eapply preservation_estep; eauto. eapply preservation_sstep; eauto. +Qed. + +Theorem wt_initial_state: + forall S, initial_state prog S -> wt_state S. +Proof. + intros. inv H. econstructor. constructor. + apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. + intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + instantiate (1 := (Vptr b Int.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. +Qed. + +End PRESERVATION. + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 0de0c827..cc72537d 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -73,11 +73,13 @@ val sizeof : Env.t -> typ -> int option val alignof : Env.t -> typ -> int option (* Return the natural alignment of the given type, in bytes. Machine-dependent. [None] is returned if the type is incomplete. *) -val sizeof_ikind: ikind -> int - (* Return the size of the given integer kind. *) val incomplete_type : Env.t -> typ -> bool (* Return true if the given type is incomplete, e.g. declared but not defined struct or union, or array type without a size. *) +val sizeof_ikind: ikind -> int + (* Return the size of the given integer kind. *) +val is_signed_ikind: ikind -> bool + (* Return true if the given integer kind is signed, false if unsigned. *) (* Computing composite_info records *) diff --git a/extraction/extraction.v b/extraction/extraction.v index 0ba4abdd..45239aa5 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -24,6 +24,7 @@ Require Tailcall. Require Allocation. Require Ctypes. Require Csyntax. +Require Ctyping. Require Clight. Require Compiler. Require Parser. @@ -163,6 +164,8 @@ Separate Extraction Csyntax.make_program Clight.make_program Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr + Ctyping.retype_function Ctyping.econdition' + Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin diff --git a/test/regression/Results/alignas b/test/regression/Results/alignas index 1fc87a4c..581a4377 100644 --- a/test/regression/Results/alignas +++ b/test/regression/Results/alignas @@ -2,8 +2,8 @@ a: size = 4, alignment = 16, address mod 16 = 0 b: size = 12, alignment = 16, address mod 16 = 0 bb: size = 12, alignment = 16, address mod 16 = 0 c: size = 32, alignment = 16, address mod 16 = 0 -d: size = 32, alignment = 32, address mod 32 = 0 +d: size = 32, alignment = 64, address mod 64 = 0 e: size = 16, alignment = 16, address mod 16 = 0 -f: size = 32, alignment = 32, address mod 32 = 0 +f: size = 16, alignment = 32, address mod 32 = 0 g: size = 96, alignment = 16, address mod 16 = 0 h: size = 192, alignment = 64, address mod 64 = 0 diff --git a/test/regression/alignas.c b/test/regression/alignas.c index 4e887d3a..a6a2e690 100644 --- a/test/regression/alignas.c +++ b/test/regression/alignas.c @@ -33,7 +33,7 @@ struct s { struct s c; char filler3; -struct s _Alignas(32) d; +struct s _Alignas(64) d; char filler4; /* Union */ @@ -77,8 +77,8 @@ int main() #endif printf("c: size = %u, alignment = %u, address mod 16 = %u\n", (unsigned) sizeof(c), (unsigned) _Alignof(c), ((unsigned) &c) & 0xF); - printf("d: size = %u, alignment = %u, address mod 32 = %u\n", - (unsigned) sizeof(d), (unsigned) _Alignof(d), ((unsigned) &d) & 0x1F); + printf("d: size = %u, alignment = %u, address mod 64 = %u\n", + (unsigned) sizeof(d), (unsigned) _Alignof(d), ((unsigned) &d) & 0x3F); printf("e: size = %u, alignment = %u, address mod 16 = %u\n", (unsigned) sizeof(e), (unsigned) _Alignof(e), ((unsigned) &e) & 0xF); printf("f: size = %u, alignment = %u, address mod 32 = %u\n", |