aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-271-2/+3
| | | | | | | | | | | | | | | | | | | architectures The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong. Those assumptions become false if the target processor has 64-bit integer registers. This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions: - Stack slots of type Tlong (or more generally of natural alignment 8) are supported. For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping. For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1. - The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers. Actually, it supports any combination of sizes for registers. - To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used. On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame. (E.g. padding could be introduced at different places.) The bulk of this big commit is related to the proof of the Stacking phase. The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic. The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic. Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps. As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before. This eliminates many boring classification lemmas from Conventions1. LTL and Lineartyping were adapted accordingly. Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations. It is used to further simplify the proofs in Conventions1.
* Also enable warnings for doc generator.Bernhard Schommer2016-04-061-2/+2
|
* Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-061-1/+2
|
* Split up tools and options.Bernhard Schommer2016-02-251-1/+4
| | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-281-10/+6
| | | | The new configuration option -clightgen activates the build of clightgen.
* Track the locations of local variables using EF_debug annotations.Xavier Leroy2015-08-231-0/+1
| | | | | | | | | | | | | | SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
* Removed the version from the compcert.ini file and add it again in a ↵Bernhard Schommer2015-07-011-11/+15
| | | | separate file.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+4
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* Merge branch 'master' into dwarfBernhard Schommer2015-03-311-0/+2
|\ | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-0/+2
| | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+1
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-101-3/+3
|\|
| * Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| |
| * Merge github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-191-1/+1
| |\
| * | Removed the linker flag again.Bernhard Schommer2015-01-201-2/+2
| | |
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-231-1/+1
|\ \ \ | | |/ | |/|
| * | Merge branch 'named-structs'Xavier Leroy2015-01-231-1/+1
| |\ \ | | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| | * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-311-1/+1
| | | | | | | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-201-4/+4
|\| |
| * | Renamed LIB into VLIB to avoid clashes with environment variables.Bernhard Schommer2015-01-201-2/+2
| | |
| * | Added variable to the Makefile to specify additional linker commands and ↵Bernhard Schommer2015-01-151-2/+2
| | | | | | | | | | | | changed the configure script to deactivated the checklink build if needed.
* | | Merge branch 'master' into dwarfBernhard Schommer2015-01-121-48/+25
|\| | | | | | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-0/+1
| | | | | | | | | | | | Assorted updates to configure and Makefile.
| * | Merge branch 'master' into pure-makefilesXavier Leroy2014-12-171-10/+12
| |\ \
| * | | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-171-7/+9
| | | | | | | | | | | | | | | | Cleanups in configure.
| * | | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-221-57/+23
| | | | | | | | | | | | | | | | | | | | | | | | produce the executables. configure: add check for GNU make.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-171-15/+8
|\ \ \ \ | | |/ / | |/| | | | | | | | | | Conflicts: powerpc/PrintAsm.ml
| * | | Use cp instead of symbolic links for executables.Xavier Leroy2014-12-171-15/+8
| | | | | | | | | | | | | | | | Now that we search for compcert.ini from Sys.executable, symbolic links cause compcert.ini not to be found.
* | | | Merge branch 'master' into dwarfBernhard Schommer2014-12-111-10/+10
|\| | |
| * | | Preserve single quotes (e.g. in CPREPRO) when generating compcert.iniXavier Leroy2014-12-111-10/+10
| | |/ | |/|
* | | Merge branch 'master' into dwarfBernhard Schommer2014-11-271-0/+1
|\| |
| * | Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-0/+1
| |/ | | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-271-1/+0
|\|
| * Tune behavior wrt warnings:Xavier Leroy2014-10-241-1/+0
| | | | | | | | | | | | - cchecklink was compiled with -warn-error, which is bad for production code - silence warning 3 (deprecated functions) - silence warning 20 (unused function argument) for Coq-extracted files.
* | Merge branch 'master' into dwarfBernhard Schommer2014-10-201-0/+1
|\|
| * Deactivated the warning for deprecated features for compilation of ↵Bernhard Schommer2014-10-201-0/+1
| | | | | | | | cchecklink since it breaks the build with newer ocaml versions.
* | Added a file containing definitions for the types used to store the debug ↵Bernhard Schommer2014-10-131-1/+1
|/ | | | information. The types follow the Current Attributes by Tag Value in Appendix 1 of the Dwarf 2 standard.
* Update Makefile, dependencies, and Changelog after upgrade to Flocq 2.4.0.Xavier Leroy2014-10-091-1/+1
|
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-071-2/+2
|
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-301-21/+23
| | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
* configure: distinguish between ABI and processor model.xleroy2014-07-291-1/+2
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify COQINCLUDESxleroy2014-07-231-3/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2541 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.xleroy2014-07-231-4/+2
| | | | | | | | | The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Redundant -I in CAMLINCLUDESxleroy2014-07-231-2/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2539 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-231-1/+2
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update Coq documentationv2.3xleroy2014-05-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-3/+18
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ia32/Select*: complete the modifications to shifts.xleroy2014-04-111-7/+8
| | | | | | | | | Makefile: missing "clean" actions. Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier) to facilitate testing with different Coq versions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2453 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:xleroy2014-04-061-1/+1
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):xleroy2014-03-281-1/+1
| | | | | | | the new Lineartyping can't keep track of single floats that were spilled. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2438 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-30 22:43:31 +0000