aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-0/+167
| | | | | | | | Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.) The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque. Fixes #151
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-0/+6
| | | | | | | | | | | | | | | | | | | | This fixes two issues: 1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform. 2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer. (Reported by Michael Schmidt.) The fix: 1- Evaluate the 3rd and 4th arguments at type size_t 2- Support both Vint and Vlong as results of this evaluation 3- Declare these arguments with type 'unsigned long'. Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations. Concerning part 3 of the fix, type size_t would be better for future platforms where size_t is bigger than unsigned long, but some more work is needed to delay the evaluation of C2C.builtins_generic to after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate the cparser/ machine configuration before C2C initializes.
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
| | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+28
| | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
| | | | The cut-and-paste was for compatibility with Coq 8.4
* Removed some implict arguments.Bernhard Schommer2016-09-051-5/+3
| | | | Also changed Local Open to Open Local.
* Moved quoting functions in ResponsefileBernhard Schommer2016-08-162-2/+36
| | | | | | Also corrected some typos and corrected exception handling for expandargv. Bug 18308
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-203-134/+98
| | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-122-20/+0
| | | | | | | Since gnu make and other tools under windows seem to have a limit of around 8000 bytes per command line the arguments should be passed via responsefiles instead. Bug 18308
* Really added the function. Bug 18308Bernhard Schommer2016-07-112-3/+19
|
* Added function to write responsefiles.Bernhard Schommer2016-07-111-0/+24
| | | | | | The arguments are written in the responsefile separated by whitespace. If the argument itself contains a whitespace it is quoted. Bug 18308
* Merge branch 'master' into add-fileBernhard Schommer2016-07-1110-173/+156
|\
| * Port to Coq 8.5pl2Xavier Leroy2016-07-0810-173/+156
| | | | | | | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* | Added responsefile support for commandline.Bernhard Schommer2016-07-081-0/+133
|/ | | | | | | | Commandline can now be passed in a file specifed with @file on the Commandline. The quoting convention is similar to the one used by gcc, etc. Options are separated by whitespaces and options with whitespaecs need to be quoted. Bug 18303
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-211-0/+10
| | | | | | | | Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of ↵Xavier Leroy2016-05-071-0/+80
| | | | | | | | memory blocks Trees are slightly more efficient than Maps, and avoid maintaining the invariant on the default value. lib/Maps: add a generic construction of a (partial) Tree module from an indexed type; use it to define ZTrees (trees indexed by Z integers).
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit ↵Xavier Leroy2016-04-271-0/+244
| | | | | | | | | | | | | | | | | | | 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.
* Merge pull request #92 from AbsInt/cleanupXavier Leroy2016-03-214-8/+18
|\ | | | | This PR activates more OCaml warnings and turns all warnings into errors. Also some unused functions, variables and types are removed.
| * Merge branch 'master' into cleanupBernhard Schommer2016-03-212-34/+189
| |\
| * | Cleanup of AsmToJSON.Bernhard Schommer2016-03-161-2/+10
| | | | | | | | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
| * | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-102-6/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
| * | Code cleanup.Bernhard Schommer2016-03-101-0/+2
| | | | | | | | | | | | | | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* | | Also ignore windows line endings.Bernhard Schommer2016-03-211-1/+2
| |/ |/| | | | | | | | | Windows style line endings can end up in the Tokenize pass. This can lead to some problems for example in pragma processing. Bug 18316
* | Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-062-34/+189
|/ | | | | | | - Coqlib: option_rel to lift a relation to option type. - Coqlib: more lemmas about list_forall2. - Coqlib: introduce type nlist (nonempty lists) and some operations. - Maps: a variant of PTree.elements_extensional that uses option_rel.
* Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-251-0/+9
|
* Started implementing a printer for Clflags.Bernhard Schommer2016-01-251-0/+33
|
* Open files in binary mode.Bernhard Schommer2015-11-301-2/+1
| | | | | | On windows opening files in text mode can result in errors due to non-windows compatible input. Thus open files only in binary mode. Bug 17664
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2018-1698/+1698
|
* Move more functionality in the new interface.Bernhard Schommer2015-09-161-9/+1
| | | | | | Added functions to add more information to the debuging interface, like the struct layout with offsets, bitifiled layout and removed the no longer needed mapping from stamp to atom.
* Added symbol functions for printing of the location for global variables.Bernhard Schommer2015-08-211-0/+7
|
* Tighten and prove correct the underflow/overflow bounds for parsing of FP ↵Xavier Leroy2015-07-062-96/+220
| | | | | | | | | literals. This is a follow-up to commit 350354c. - Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse - Add early checks for overflow and underflow and prove them correct. - Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
* Give a name to the type of atoms.Xavier Leroy2015-04-231-2/+4
|
* remove not used hypotheses in TREEJacques-Henri Jourdan2015-03-251-9/+4
|
* Merge branch 'master' into no-shellBernhard Schommer2015-02-192-0/+139
|\
| * In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-072-0/+139
| | | | | | | | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* | Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-192-0/+150
|/ | | | | Revised parsing of compcert.ini file to split arguments into words like POSIX shell does (including quotes).
* build_from_parsed: simplified code + correctness proof.Xavier Leroy2014-11-151-15/+86
|
* Upgrade to flocq 2.4.0Jacques-Henri Jourdan2014-10-072-292/+106
|
* Add theorem "elements_remove".Xavier Leroy2014-09-241-167/+178
| | | | | Use "elements_remove" to simplify the proof of "cardinal_remove". Simplify some of the proofs over function "xelements".
* More efficient implementations of map, fold, etc.xleroy2014-08-271-164/+109
| | | | | | | (Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.xleroy2014-07-281-73/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:xleroy2014-07-233-1468/+2529
| | | | | | | | | | | | | | | - 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
* Tweaks to support defunctorization.xleroy2014-07-231-9/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2536 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add Proof keyword so that documentation generation worksjjourdan2014-07-041-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2520 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaner, more resilient parsing of pragmas.xleroy2014-06-052-0/+78
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-0/+50
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-091-0/+10
| | | | | | | | | | over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 04:53:58 +0000