| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| ... | |
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\|
| |
| |
| |
| | |
Conflicts:
.gitignore
|
| | |
| |
| |
| |
| |
| |
| | |
For consistency with other generated .v files, and because it protects
against editing the generated file, see Github issue #248.
Closes: #248
|
| | |
| |
| |
| | |
Inspired by and adapted from pull request #235 by Benoît Viguier.
|
| | | |
|
| | |
| |
| |
| |
| | |
coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.
|
| | |
| |
| | |
This is useful for the VST project and can be useful for others.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
.vo files are installed if configure options
-install-coqdev or -clightgen or -coqdevdir are given.
Installation directory is $(PREFIX)/lib/compcert/coq by default and
can be changed by configure option -coqdevdir.
Closes: #227
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We were previously at 2.5.2. Quoting the NEWS from upstream:
Version 2.6.1:
- ensured compatibility from Coq 8.4 to 8.8
Version 2.6.0:
- ensured compatibility from Coq 8.4 to 8.7
- removed some hypotheses on some lemmas of Fcore_ulp
- added lemmas to Fprop_plus_error
- improved examples
Also: in preparation for Coq 8.8, silence warning "compatibility-notation"
when building Flocq, because this warning is on by default in 8.8,
and Flocq triggers it a lot.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Asmblock.v:
- Rajout de "header" dans wf_bblock
- Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair
de manipuler des bblocks, plutôt qu'un "code constitué de bblocks".
ça permet de minimiser les modifications dans Asmblockgen.v
- fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le
code OCaml de toute façon (vu la translation Asmblock -> Asm)
- Rajout d'un type instruction qui regroupe les basic et les control ;
facilite certaines définitions
Asmblockgen.v:
- Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce
vers quoi je m'oriente : garder les fonctions existantes de
génération de code ; on leur donne à manger la liste de basics de
Machblock. On traduit le exit (qui peut spiller sur la liste de
basics déjà traduite), et on met la dernière instruction de la trad
du exit (qui doit être un control) dans le exit du bblock.
- Pour le prologue : chaque instruction rajoutée "à la main" est dans
son propre bblock. Voir la notation ::b pour le faire. A terme, il
devrait y avoir moyen "d'accumuler" l'instruction au code généré ;
pour l'instant je préfère ne pas compliquer la génération.
|
| |/ |
|
| |
|
|
|
|
|
| |
Implicit Arguments is deprecated in Coq since 8.6 or so.
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
|
| | |
|
| |
|
|
| |
We simply fully qualify the modules. This is backward compatible.
|
| |
|
|
|
| |
The latter, in conjunction with some values of the umask, gives weird messages
"new permissions are ... not ...".
|
| |
|
|
| |
`-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
|
| |
|
|
| |
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
|
| | |
|
| |
|
|
|
|
|
|
| |
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
|
| |\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
-> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |/
|
|
|
|
|
|
| |
Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418
|
| |
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| |
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
The new configuration option -clightgen activates the build of clightgen.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
separate file.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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).
|
| |\
| |
| |
| |
| |
| | |
Conflicts:
Makefile
driver/Driver.ml
|
| | |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
global target dependend option to activate the printing only for targets wher it works.
|
| |\| |
|
