From 3ec022950ec233a2af418aacd1755fce4d701724 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 19 Feb 2014 09:55:45 +0000 Subject: Add option -Os to optimize for code size rather than for execution speed. Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 25 ++++++++++++------------ Changelog | 2 ++ Makefile | 2 +- arm/ConstpropOp.vp | 1 + arm/ConstpropOpproof.v | 1 + arm/ValueAOp.v | 1 + backend/Constprop.v | 4 ++-- backend/Constpropproof.v | 5 +++-- backend/SelectDiv.vp | 45 ++++++++++++++++++++++++++++---------------- backend/SelectDivproof.v | 42 ++++++++++++++++++++++++----------------- backend/Tailcall.v | 3 +-- backend/Tailcallproof.v | 1 + backend/ValueAnalysis.v | 7 ++++--- backend/ValueDomain.v | 29 +++++++++++++--------------- cparser/Elab.ml | 24 ++++++++++++++--------- driver/Clflags.ml | 1 + driver/Compopts.v | 33 ++++++++++++++++++++++++++++++++ driver/Driver.ml | 4 ++++ driver/Interp.ml | 1 + extraction/extraction.v | 24 +++++++++++------------ ia32/ConstpropOp.vp | 1 + ia32/ConstpropOpproof.v | 1 + ia32/ValueAOp.v | 1 + powerpc/ConstpropOp.vp | 1 + powerpc/ConstpropOpproof.v | 1 + powerpc/SelectOp.vp | 10 +++++++--- powerpc/SelectOpproof.v | 4 +++- powerpc/ValueAOp.v | 1 + test/regression/Makefile | 2 +- test/regression/Results/for1 | 15 +++++++++++++++ test/regression/for1.c | 20 ++++++++++++++++++++ 31 files changed, 215 insertions(+), 97 deletions(-) create mode 100644 driver/Compopts.v create mode 100644 test/regression/Results/for1 create mode 100644 test/regression/for1.c diff --git a/.depend b/.depend index 2b18734..8c02175 100644 --- a/.depend +++ b/.depend @@ -35,7 +35,7 @@ $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH) backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo -$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.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 common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo @@ -44,7 +44,7 @@ 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 common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.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 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 @@ -54,23 +54,23 @@ backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beau backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Subtyping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo -backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo backend/RTL.vo -$(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/ValueDomain.vo backend/RTL.vo -backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo +backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo backend/RTL.vo +$(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/ValueDomain.vo backend/RTL.vo +backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo -backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo +backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo backend/Kildall.vo $(ARCH)/CombineOp.vo -$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo +$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo -$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo +$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob $(ARCH)/$(VARIANT)/Conventions1.v.beautified: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo @@ -91,10 +91,10 @@ $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob $(ARCH)/$( backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Lineartyping.vo backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.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/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo 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 +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo backend/Asmgenproof0.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.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/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 @@ -115,6 +115,7 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob cfrontend/Cshmgenproof.v.b 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 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/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/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 diff --git a/Changelog b/Changelog index d02866a..8984ee8 100644 --- a/Changelog +++ b/Changelog @@ -27,6 +27,8 @@ Language features: just as the last case. - Support for incomplete array as last field of a struct, as specified in ISO C 99. +- Support for declarations within 'for' loops, as specified in ISO C 99. + (E.g. "for (int i = 0; i < 4; i++) ...") - Revised semantics and implementation of _Alignas(N) attribute to better match those of GCC and Clang. - Better tolerance for functions declared without prototypes diff --git a/Makefile b/Makefile index b527a8c..d206461 100644 --- a/Makefile +++ b/Makefile @@ -111,7 +111,7 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Cstrategy.v Cexec.v \ # Putting everything together (in driver/) -DRIVER=Compiler.v Complements.v +DRIVER=Compopts.v Compiler.v Complements.v # All source files diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 0540781..bf08610 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -14,6 +14,7 @@ and conditions. This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index ad7dcd1..90e18f2 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -13,6 +13,7 @@ (** Correctness proof for constant propagation (processor-dependent part). *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index c968213..037b22e 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -11,6 +11,7 @@ (* *********************************************************************) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/backend/Constprop.v b/backend/Constprop.v index 76d8e6c..d2c4d44 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -74,7 +74,7 @@ Definition transf_ros (ae: AE.t) (ros: reg + ident) : reg + ident := Definition const_for_result (a: aval) : option operation := match a with | I n => Some(Ointconst n) - | F n => if generate_float_constants tt then Some(Ofloatconst n) else None + | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | Ptr(Gl symb ofs) => Some(Oaddrsymbol symb ofs) | Ptr(Stk ofs) => Some(Oaddrstack ofs) | _ => None @@ -108,7 +108,7 @@ Fixpoint annot_strength_reduction let (targs'', args'') := annot_strength_reduction ae targs' args' in match ty, areg ae arg with | Tint, I n => (AA_int n :: targs'', args'') - | Tfloat, F n => if generate_float_constants tt + | Tfloat, F n => if Compopts.generate_float_constants tt then (AA_float n :: targs'', args'') else (AA_arg ty :: targs'', arg :: args'') | _, _ => (AA_arg ty :: targs'', arg :: args'') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 41afe8c..d88d6e4 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Compopts. Require Import AST. Require Import Integers. Require Import Values. @@ -157,7 +158,7 @@ Proof. - (* integer *) inv H. inv H0. exists (Vint n); auto. - (* float *) - destruct (generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto. + destruct (Compopts.generate_float_constants tt); inv H. inv H0. exists (Vfloat f); auto. - (* pointer *) destruct p; try discriminate. + (* global *) @@ -235,7 +236,7 @@ Proof. * exists eargs''; split; auto; simpl; f_equal; auto. generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. inv VM. rewrite <- H0 in *. inv H5; auto. - * destruct (generate_float_constants tt); inv H1; auto. + * destruct (Compopts.generate_float_constants tt); inv H1; auto. exists eargs''; split; auto; simpl; f_equal; auto. generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. inv VM. rewrite <- H0 in *. inv H5; auto. diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 1d9168c..938ce5d 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -13,6 +13,7 @@ (** Instruction selection for division and modulus *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -77,10 +78,13 @@ Definition divuimm (e1: expr) (n2: int) := match Int.is_power2 n2 with | Some l => shruimm e1 l | None => - match divu_mul_params (Int.unsigned n2) with - | None => divu_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (divu_mul p m) - end + if optim_for_size tt then + divu_base e1 (Eop (Ointconst n2) Enil) + else + match divu_mul_params (Int.unsigned n2) with + | None => divu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divu_mul p m) + end end. Nondetfunction divu (e1: expr) (e2: expr) := @@ -96,10 +100,13 @@ Definition moduimm (e1: expr) (n2: int) := match Int.is_power2 n2 with | Some l => andimm (Int.sub n2 Int.one) e1 | None => - match divu_mul_params (Int.unsigned n2) with - | None => modu_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) - end + if optim_for_size tt then + modu_base e1 (Eop (Ointconst n2) Enil) + else + match divu_mul_params (Int.unsigned n2) with + | None => modu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) + end end. Nondetfunction modu (e1: expr) (e2: expr) := @@ -123,10 +130,13 @@ Definition divsimm (e1: expr) (n2: int) := then shrximm e1 l else divs_base e1 (Eop (Ointconst n2) Enil) | None => - match divs_mul_params (Int.signed n2) with - | None => divs_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (divs_mul p m) - end + if optim_for_size tt then + divs_base e1 (Eop (Ointconst n2) Enil) + else + match divs_mul_params (Int.signed n2) with + | None => divs_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divs_mul p m) + end end. Nondetfunction divs (e1: expr) (e2: expr) := @@ -142,10 +152,13 @@ Definition modsimm (e1: expr) (n2: int) := then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2) else mods_base e1 (Eop (Ointconst n2) Enil) | None => - match divs_mul_params (Int.signed n2) with - | None => mods_base e1 (Eop (Ointconst n2) Enil) - | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) - end + if optim_for_size tt then + mods_base e1 (Eop (Ointconst n2) Enil) + else + match divs_mul_params (Int.signed n2) with + | None => mods_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) + end end. Nondetfunction mods (e1: expr) (e2: expr) := diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 0719a5e..9228cde 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -369,10 +369,12 @@ Proof. replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). apply eval_shruimm; auto. simpl. erewrite Int.is_power2_range; eauto. -- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. - + exists (Vint (Int.divu i n2)); split; auto. - econstructor; eauto. eapply eval_divu_mul; eauto. +- destruct (Compopts.optim_for_size tt). + eapply eval_divu_base; eauto. EvalOp. + + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + * exists (Vint (Int.divu i n2)); split; auto. + econstructor; eauto. eapply eval_divu_mul; eauto. + * eapply eval_divu_base; eauto. EvalOp. Qed. Theorem eval_divu: @@ -412,13 +414,15 @@ Proof. change (Vint (Int.and i (Int.sub n2 Int.one))) with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))). apply eval_andimm. auto. -- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. - + econstructor; split. - econstructor; eauto. eapply eval_mod_from_div. - eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. - rewrite Int.modu_divu. auto. - red; intros; subst n2; discriminate. +- destruct (Compopts.optim_for_size tt). + eapply eval_modu_base; eauto. EvalOp. + + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + * econstructor; split. + econstructor; eauto. eapply eval_mod_from_div. + eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. + rewrite Int.modu_divu. auto. + red; intros; subst n2; discriminate. + * eapply eval_modu_base; eauto. EvalOp. Qed. Theorem eval_modu: @@ -485,10 +489,12 @@ Proof. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto. + eapply eval_divs_base; eauto. EvalOp. -- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. - + exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. +- destruct (Compopts.optim_for_size tt). + eapply eval_divs_base; eauto. EvalOp. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + * exists (Vint (Int.divs i n2)); split; auto. + econstructor; eauto. eapply eval_divs_mul; eauto. + * eapply eval_divs_base; eauto. EvalOp. Qed. Theorem eval_divs: @@ -524,12 +530,14 @@ Proof. apply eval_mod_from_div. eexact X. simpl; eauto. simpl. auto. + eapply eval_mods_base; eauto. EvalOp. -- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. - + econstructor; split. - econstructor. eauto. apply eval_mod_from_div with (x := i); auto. - eapply eval_divs_mul with (x := i); eauto. - simpl. auto. +- destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + * econstructor; split. + econstructor. eauto. apply eval_mod_from_div with (x := i); auto. + eapply eval_divs_mul with (x := i); eauto. + simpl. auto. + * eapply eval_mods_base; eauto. EvalOp. Qed. Theorem eval_mods: diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 26beb34..25da531 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Compopts. Require Import AST. Require Import Registers. Require Import Op. @@ -98,8 +99,6 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := as explained above. Moreover, we can turn tail calls off using a compilation option. *) -Parameter eliminate_tailcalls: unit -> bool. - Definition transf_function (f: function) : function := if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt then RTL.transf_function (transf_instr f) f diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 77725cf..1965b18 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -13,6 +13,7 @@ (** Recognition of tail calls: correctness proof *) Require Import Coqlib. +Require Import Compopts. Require Import Maps. Require Import AST. Require Import Integers. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index f580438..e293028 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -12,6 +12,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -74,7 +75,7 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func match classify_builtin ef args ae with | Builtin_vload chunk aaddr => let a := - if strict + if va_strict tt then vlub (loadv chunk rm am aaddr) (vnormalize chunk (Ifptr Glob)) else vnormalize chunk Vtop in VA.State (AE.set res a ae) am @@ -1255,11 +1256,11 @@ Proof. * (* true volatile access *) assert (V: vmatch bc v0 (Ifptr Glob)). { inv H4; constructor. econstructor. eapply GE; eauto. } - destruct strict. apply vmatch_lub_r. apply vnormalize_sound. auto. + destruct (va_strict tt). apply vmatch_lub_r. apply vnormalize_sound. auto. apply vnormalize_sound. eapply vmatch_ge; eauto. constructor. constructor. * (* normal memory access *) exploit loadv_sound; eauto. simpl; eauto. intros V. - destruct strict. + destruct (va_strict tt). apply vmatch_lub_l. auto. eapply vnormalize_cast; eauto. eapply vmatch_top; eauto. + (* volatile store *) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index eee4762..239dd47 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -13,6 +13,7 @@ Require Import Coqlib. Require Import Zwf. Require Import Maps. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -25,10 +26,6 @@ Require Import Kildall. Require Import Registers. Require Import RTL. -Parameter strict: bool. -Parameter propagate_float_constants: unit -> bool. -Parameter generate_float_constants : unit -> bool. - Inductive block_class : Type := | BCinvalid | BCglob (id: ident) @@ -819,7 +816,7 @@ Definition vlub (v w: aval) : aval := | I i, Sgn n | Sgn n, I i => sgn (Z.max (ssize i) n) | I i, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), I i => - if strict || Int.eq i Int.zero then Ifptr p else Vtop + if va_strict tt || Int.eq i Int.zero then Ifptr p else Vtop | Uns n1, Uns n2 => Uns (Z.max n1 n2) | Uns n1, Sgn n2 => sgn (Z.max (n1 + 1) n2) | Sgn n1, Uns n2 => sgn (Z.max n1 (n2 + 1)) @@ -837,7 +834,7 @@ Definition vlub (v w: aval) : aval := | Ptr p1, Ifptr p2 => Ifptr(plub p1 p2) | Ifptr p1, Ptr p2 => Ifptr(plub p1 p2) | Ifptr p1, Ifptr p2 => Ifptr(plub p1 p2) - | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if strict then Ifptr p else Vtop + | _, (Ptr p | Ifptr p) | (Ptr p | Ifptr p), _ => if va_strict tt then Ifptr p else Vtop | _, _ => Vtop end. @@ -989,8 +986,8 @@ Lemma pmatch_vplub: forall b ofs x p, pmatch b ofs p -> pmatch b ofs (vplub x p). Proof. intros. - assert (DFL: pmatch b ofs (if strict then p else Ptop)). - { destruct strict; auto. eapply pmatch_top'; eauto. } + assert (DFL: pmatch b ofs (if va_strict tt then p else Ptop)). + { destruct (va_strict tt); auto. eapply pmatch_top'; eauto. } unfold vplub; destruct x; auto; apply pmatch_lub_r; auto. Qed. @@ -1495,7 +1492,7 @@ Definition divs (v w: aval) := | I i2, I i1 => if Int.eq i2 Int.zero || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then if strict then Vbot else itop + then if va_strict tt then Vbot else itop else I (Int.divs i1 i2) | _, _ => itop end. @@ -1513,7 +1510,7 @@ Definition divu (v w: aval) := match w, v with | I i2, I i1 => if Int.eq i2 Int.zero - then if strict then Vbot else itop + then if va_strict tt then Vbot else itop else I (Int.divu i1 i2) | _, _ => itop end. @@ -1531,7 +1528,7 @@ Definition mods (v w: aval) := | I i2, I i1 => if Int.eq i2 Int.zero || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone - then if strict then Vbot else itop + then if va_strict tt then Vbot else itop else I (Int.mods i1 i2) | _, _ => itop end. @@ -1549,7 +1546,7 @@ Definition modu (v w: aval) := match w, v with | I i2, I i1 => if Int.eq i2 Int.zero - then if strict then Vbot else itop + then if va_strict tt then Vbot else itop else I (Int.modu i1 i2) | I i2, _ => uns (usize i2) | _, _ => itop @@ -1693,7 +1690,7 @@ Definition intoffloat (x: aval) := | F f => match Float.intoffloat f with | Some i => I i - | None => if strict then Vbot else itop + | None => if va_strict tt then Vbot else itop end | _ => itop end. @@ -1711,7 +1708,7 @@ Definition intuoffloat (x: aval) := | F f => match Float.intuoffloat f with | Some i => I i - | None => if strict then Vbot else itop + | None => if va_strict tt then Vbot else itop end | _ => itop end. @@ -2823,7 +2820,7 @@ Definition mtop := minit Ptop. Definition load (chunk: memory_chunk) (rm: romem) (m: amem) (p: aptr) : aval := match p with - | Pbot => if strict then Vbot else Vtop + | Pbot => if va_strict tt then Vbot else Vtop | Gl id ofs => match rm!id with | Some ab => ablock_load chunk ab (Int.unsigned ofs) @@ -2882,7 +2879,7 @@ Definition storev (chunk: memory_chunk) (m: amem) (addr: aval) (v: aval): amem : Definition loadbytes (m: amem) (rm: romem) (p: aptr) : aptr := match p with - | Pbot => if strict then Pbot else Ptop + | Pbot => if va_strict tt then Pbot else Ptop | Gl id _ | Glo id => match rm!id with | Some ab => ablock_loadbytes ab diff --git a/cparser/Elab.ml b/cparser/Elab.ml index b99c9af..90662a3 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1765,22 +1765,28 @@ let rec elab_stmt env ctx s = { sdesc = Sdowhile(s1', a'); sloc = elab_loc loc } | FOR(fc, a2, a3, s1, loc) -> - let a1' = + let (a1', env', decls') = match fc with | FC_EXP a1 -> - elab_for_expr loc env a1 + (elab_for_expr loc env a1, env, None) | FC_DECL def -> - error loc "C99 declaration within `for' not supported"; - sskip in + let (dcl, env') = elab_definition true (Env.new_scope env) def in + let loc = elab_loc (get_definitionloc def) in + (sskip, env', + Some(List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl)) in let a2' = if a2 = NOTHING then intconst 1L IInt - else elab_expr loc env a2 in - if not (is_scalar_type env a2'.etyp) then + else elab_expr loc env' a2 in + if not (is_scalar_type env' a2'.etyp) then error loc "the condition of 'for' does not have scalar type"; - let a3' = elab_for_expr loc env a3 in - let s1' = elab_stmt env (ctx_loop ctx) s1 in - { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } + let a3' = elab_for_expr loc env' a3 in + let s1' = elab_stmt env' (ctx_loop ctx) s1 in + let sfor = { sdesc = Sfor(a1', a2', a3', s1'); sloc = elab_loc loc } in + begin match decls' with + | None -> sfor + | Some sl -> { sdesc = Sblock (sl @ [sfor]); sloc = elab_loc loc } + end (* 6.8.4 Switch statement *) | SWITCH(a, s1, loc) -> diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 5d068b6..b1f2bd8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -28,6 +28,7 @@ let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 let option_finline_asm = ref false +let option_Osize = ref false let option_dparse = ref false let option_dcmedium = ref false let option_dclight = ref false diff --git a/driver/Compopts.v b/driver/Compopts.v new file mode 100644 index 0000000..205f768 --- /dev/null +++ b/driver/Compopts.v @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compilation options *) + +(** This file collects Coq functions to query the command-line + options that influence the code generated by the verified + part of CompCert. These functions are mapped by extraction + to accessors for the flags in [Clflags.ml]. *) + +(** Flag [-Os]. For instruction selection (mainly). *) +Parameter optim_for_size: unit -> bool. + +(** Flag [-ffloat-const-prop]. For value analysis and constant propagation. *) +Parameter propagate_float_constants: unit -> bool. +Parameter generate_float_constants: unit -> bool. + +(** For value analysis. Currently always false. *) +Parameter va_strict: unit -> bool. + +(** Flag -ftailcalls. For tail call optimization. *) +Parameter eliminate_tailcalls: unit -> bool. + + diff --git a/driver/Driver.ml b/driver/Driver.ml index 47061cd..8853794 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -426,6 +426,8 @@ Language support options (use -fno- to turn off -f) : -fall Activate all language support options above -fnone Turn off all language support options above Code generation options: (use -fno- to turn off -f) : + -O Optimize for speed [on by default] + -Os Optimize for code size -ffpu Use FP registers for some integer operations [on] -fsmall-data Set maximal size for allocation in small data area -fsmall-const Set maximal size for allocation in small constant area @@ -525,6 +527,8 @@ let cmdline_actions = assembler_options := s :: !assembler_options); "-Wl,", Self (fun s -> push_linker_arg s); + "-Os$", Set option_Osize; + "-O$", Unset option_Osize; "-fsmall-data$", Integer(fun n -> option_small_data := n); "-fsmall-const$", Integer(fun n -> option_small_const := n); "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); diff --git a/driver/Interp.ml b/driver/Interp.ml index 25d363c..5975ae3 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -454,6 +454,7 @@ let diagnose_stuck_expr p ge w f a kont e m = | RV, Ecomma(r1, r2, ty) -> diagnose RV r1 | RV, Eparen(r1, ty) -> diagnose RV r1 | RV, Ecall(r1, rargs, ty) -> diagnose RV r1 ||| diagnose_list rargs + | RV, Ebuiltin(ef, tyargs, rargs, ty) -> diagnose_list rargs | _, _ -> false in if found then true else begin let l = Cexec.step_expr ge do_external_function do_inline_assembly e w k a m in diff --git a/extraction/extraction.v b/extraction/extraction.v index b8442a8..654e80f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -68,18 +68,6 @@ Extraction Inline RTLgen.ret RTLgen.error RTLgen.bind RTLgen.bind2. Extract Inlined Constant Inlining.should_inline => "Inliningaux.should_inline". Extraction Inline Inlining.ret Inlining.bind. -(* ValueDomain *) -Extract Constant ValueDomain.strict => - "false". -Extract Constant ValueDomain.propagate_float_constants => - "fun _ -> !Clflags.option_ffloatconstprop >= 1". -Extract Constant ValueDomain.generate_float_constants => - "fun _ -> !Clflags.option_ffloatconstprop >= 2". - -(* Tailcall *) -Extract Constant Tailcall.eliminate_tailcalls => - "fun _ -> !Clflags.option_ftailcalls". - (* Allocation *) Extract Constant Allocation.regalloc => "Regalloc.regalloc". @@ -90,6 +78,18 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. +(* Compopts *) +Extract Constant Compopts.optim_for_size => + "fun _ -> !Clflags.option_Osize". +Extract Constant Compopts.va_strict => + "fun _ -> false". +Extract Constant Compopts.propagate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 1". +Extract Constant Compopts.generate_float_constants => + "fun _ -> !Clflags.option_ffloatconstprop >= 2". +Extract Constant Compopts.eliminate_tailcalls => + "fun _ -> !Clflags.option_ftailcalls". + (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index 396c94c..aaf08a1 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -14,6 +14,7 @@ This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index d9e6068..148a08d 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -13,6 +13,7 @@ (** Correctness proof for operator strength reduction. *) Require Import Coqlib. +Require Import Compopts. Require Import Integers. Require Import Floats. Require Import Values. diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 022e015..1802e11 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -11,6 +11,7 @@ (* *********************************************************************) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 9dbaa78..6aa0925 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -14,6 +14,7 @@ This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index e7dd3a4..0c88246 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -13,6 +13,7 @@ (** Correctness proof for operator strength reduction. *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index bdb94bd..ad4f3b9 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -37,6 +37,7 @@ *) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -190,9 +191,12 @@ Definition mulimm_base (n1: int) (e2: expr) := | i :: nil => shlimm e2 i | i :: j :: nil => - Elet e2 - (Eop Oadd (shlimm (Eletvar 0) i ::: - shlimm (Eletvar 0) j ::: Enil)) + if optim_for_size tt then + Eop (Omulimm n1) (e2:::Enil) + else + Elet e2 + (Eop Oadd (shlimm (Eletvar 0) i ::: + shlimm (Eletvar 0) j ::: Enil)) | _ => Eop (Omulimm n1) (e2:::Enil) end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 0cfa707..4d26cf6 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. @@ -304,7 +305,8 @@ Proof. replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul. apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib. destruct l. - intros. rewrite H1. simpl. + intros. destruct (optim_for_size tt). TrivialExists. + rewrite H1. simpl. exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]]. exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]]. exists (Val.add v1 v2); split. diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index 3789953..7f16bb3 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -11,6 +11,7 @@ (* *********************************************************************) Require Import Coqlib. +Require Import Compopts. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/test/regression/Makefile b/test/regression/Makefile index c653a01..4d9683c 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -11,7 +11,7 @@ LIBS=$(LIBMATH) TESTS=int32 int64 floats floats-basics \ expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ - sizeof1 sizeof2 binops bool + sizeof1 sizeof2 binops bool for1 # Can run, but only in compiled mode, and have reference output in Results diff --git a/test/regression/Results/for1 b/test/regression/Results/for1 new file mode 100644 index 0000000..72ef7e0 --- /dev/null +++ b/test/regression/Results/for1 @@ -0,0 +1,15 @@ +loop1: 0 +loop1: 1 +loop1: 2 +loop2: 0 +loop2: 1 +loop2: 2 +old i = 3 +loop3: 0 1 +loop3: 1 3 +loop3: 2 5 +old i = 3 +loop4: 0 4 +loop4: 1 3 +loop4: 2 2 +old i = 3 diff --git a/test/regression/for1.c b/test/regression/for1.c new file mode 100644 index 0000000..4563dde --- /dev/null +++ b/test/regression/for1.c @@ -0,0 +1,20 @@ +/* C99 'for' loops with declarations */ + +#include + +int main() +{ + int i; + for (i = 0; i < 3; i++) printf("loop1: %d\n", i); + for (int i = 0; i < 3; i++) printf("loop2: %d\n", i); + printf("old i = %d\n", i); + for (int i = 0, j; i < 3; i++) { + j = i * 2 + 1; printf("loop3: %d %d\n", i, j); + } + printf("old i = %d\n", i); + for (int i = 0, j = i + 4; i < 3; i++, j--) { + printf("loop4: %d %d\n", i, j); + } + printf("old i = %d\n", i); + return 0; +} -- cgit v1.2.3