| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
|
|
|
|
|
| |
Instead of using reset_constants use reset_literals which avoids
emptying the jumptables.
Bug 22525
|
|
|
|
|
|
| |
Instead of just storing the constants in a list, they are now
stored in a hashtable. This avoids printing of duplicates.
Bug 22525
|
|
|
|
|
| |
The new_label function is alway equal to PrintAsmaux.new_label.
Bug 22472
|
|\
| |
| |
| | |
Ensure FunInd or Recdef is imported if functional induction is used.
This is necessary for Coq 8.7.0.
|
| |
| |
| |
| |
| |
| | |
Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
|
| | |
|
| |
| |
| |
| |
| |
| | |
This option allows it to dump a list of all used mnemonics into
a file.
Bug 22239
|
| |
| |
| |
| | |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
| |
| |
| |
| | |
Some alignments were wrong. Follow-up to [4d099ef].
|
| |
| |
| |
| | |
It got lost during the addition of the x86-64 port in release 3.0.
|
|/ |
|
|
|
|
|
|
| |
This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses.
Current status: x86 port only, the only new addressing mode handled is reg + offset.
|
|
|
|
|
|
|
|
|
| |
Instead of just dumping the json output it is now a little bit
formatted for better reading.
Furthermore the AsmToJson function for the non powerpc targets now
prints the json value "null" sucht that the resulting json file is
valid json.
|
|
|
|
|
| |
- x86/Op: in 32-bit mode all addressings are valid because offsets are always interpreted as 32-bit signed integers in Asmgen.
- x86/ConstpropOp: in addr_strength_reduction, make sure no invalid addressing mode is generated.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
This port required the following additional changes:
- Integers: More properties about shrx
- SelectOp: now provides smart constructors for mulhs and mulhu
- SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
- Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
- test/: add SIMU make variable to run tests through a simulator
- test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
commit da14495c01cf4f66a928c2feff5c53f09bde837f
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu Apr 13 17:36:10 2017 +0200
RISC-V port, continued
Now working on Asmgen.
commit 36f36eb3a5abfbb8805960443d087b6a83e86005
Author: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed Apr 12 17:26:39 2017 +0200
RISC-V port, first steps
This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
|
|
|
|
| |
Without scopes Coq 8.6 warns, probably rightly so.
|
|
|
|
|
| |
Open Local becomes Local Open. This silences Coq 8.6's warning.
Also: remove one useless Require-inside-a-module that caused another warning.
|
|
|
|
|
|
| |
In 64-bit mode jumptables contain differences of labels Lx-Ly.
The OS X assembler and linker have problems with those differences if the labels are from a given section (here, .text) and the difference is to be put in another section (previously, .const).
Putting the jumptables in .text fixes this issue, and is consistent with what is done for ELF.
|
| |
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
Since the dwarf register names for x86_32 and x86_64 differ it is
wrong to hardcode the dwarf register number for rsp to 4.
Bug 20461
|
|
|
|
|
| |
Address constants need to be 64bit also in the debug information.
Bug 20335
|
|
|
|
|
|
| |
Calls to variadic or unprototyped functions set this register to reflect the number of arguments passed in XMM registers. Thus we must make sure that rax is not used to hold the pointer to the function being called.
(Report by Michael Schmidt.)
|
|
-> 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).
|