| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and
'sp' for riscV.
Bug 23176.
|
|
|
|
|
| |
Registers should not contain the % prefix for ais annotations.
Bug 23176
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When x is known to be either 0 or 1, comparisons such as
x == 0 x != 0 x == 1 x != 1
can be optimized away. This optimization was already performed
for signed comparisons. This commit extends the optimization to
unsigned comparisons as well.
Additionally, for PowerPC only, some unsigned (dis)equality comparisons are
turned into signed comparisons when we know it makes no difference,
i.e. when both arguments are guaranteed not to be pointers. The
reason is that Asmgen can produce shorter instruction sequences for
some signed equality comparisons than for the corresponding unsigned
comparisons.
It's important to optimize unsigned integer comparisons because casts
to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons.
In particular, cascades of casts to _Bool are now reduced to a single
cast much more often than before.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
In 32-bit mode, a symbolic reference "symbol + ofs" (address of "symbol" plus "ofs" bytes) can always be resolved by the linker into a 32-bit quantity that fits the 32-bit displacement field of x86 addressing modes.
Not so in 64-bit mode: first, the displacement field is still 32 bits but the full address is 64 bits; second, the displacement is relative to the RIP instruction pointer. In the "small code model" that CompCert uses for x86-64, excessively large offsets lead to link-time overflows of this 32-bit displacement field.
This commit addresses the issue by limiting the "ofs" part of "symbol + ofs" global addressing models to the range [-2^24, 2^24 - 1]. As explained in the AMD64 ELF ABI document, this is a safe range in the small code model, under the assumption that no global symbol is bigger than 2^24 bytes. GCC seems to be using a wider range [-2^31, 2^24 - 1] but I'd rather be safe.
The limitation of the "ofs" offset is achieved by extending the mechanisms already present to ensure that "ofs" in "reg + ofs" indexed addressing modes fits in 32-bit signed:
- Op.addressing_valid checks that the "ofs" part of "symbol + ofs" addressing modes is in the correct interval;
- SelectOp.addressing turns invalid addressings into lea's + indexed addressings;
- Asmgen.normalize_addrmode_64 turns lea's with invalid addressings into simpler lea's + addq of the large offset.
|
|
|
|
|
|
|
|
| |
addressing
In the original code, the addressing_valid check is skipped if we are in 32 bits, because we know the check is always true. This is correct but not obvious nor future-proof. (In the future we may want to make addressing_valid more strict.)
This commit restructures ConstpropOp.addr_strength_reduction so that the addressing_valid check is always performed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent.
This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/
|
|
|
|
| |
Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
|
| |
|
| |
|
|
|
|
|
|
| |
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).
|