| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
|\| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Before it was "option typ". Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).
One benefit is that external functions get more precise types that
control better their return values. As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
|
|/ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When printing an extended asm code fragment, placeholders %n
are replaced by register names.
Currently we ignore the fact that some assemblers use different
register names depending on the width of the data that resides
in the register.
For example, x86_64 uses %rax for a 64-bit quantity and %eax for
a 32-bit quantity, but CompCert always prints %rax in extended asm
statements. This is problematic if we want to use 32-bit integer
instructions in extended asm, e.g.
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
produces
addl %rax, %rdx
which is syntactically incorrect.
Another example is ARM FP registers: D0 is a double-precision float,
but S0 is a single-precision float.
This commit partially solves this issue by taking into account the
Cminor type of the asm parameter when printing the corresponding register.
Continuing the previous example,
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
now produces
addl %eax, %edx
This is not perfect yet: we use Cminor types, because this is all we
have at hand, and not source C types, hence "char" and "short" parameters
are still printed like "int" parameters, which is not good for x86.
(I.e. we produce %eax where GCC might have produced %al or %ax.)
We'll leave this issue open.
|
|
|
|
|
|
|
|
|
|
| |
The option -fcommon controls whether uninitialized global
variables are placed in the COMMON section. If the option is given
in the negated form, -fno-common, variables are not placed in the
COMMON section. They are placed in the same sections as gcc does.
If the variables are not placed in the COMMON section merging of
tentative definitions is inhibited and multiple definitions lead
to a linker error, as it does for gcc.
|
|
|
|
|
| |
The AbsInt build number no longer contains "release", so it must
be printed additionally.
|
|
|
|
|
|
|
|
|
| |
* Move the expansion of response files to module Commandline,
during the initialization of `Commandline.argv`.
This way we're sure it's done exactly once.
* Make `Commandline.argv` a `string array` instead of a `string array ref`.
We no longer need to update it after initialization!
* Improve reporting of errors during expansion of response files.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
This allows for an easier replacement of the binary address and
avoids that the user specifies his own binary addresses.
Bug 22468
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
Address constants need to be 64bit also in the debug information.
Bug 20335
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
On older version of the binutils the cfi directives are not always
supported so we only print cfi_sections if the corresponding .ini
setting is set to true.
|
| |
|
| |
|
| |
|
|
|
|
| |
Producer as well as target system.
|
| |
|
|
|
|
|
|
|
|
| |
Debuging code.
The old functions to store the symbol for the Global variables and retrive this
is no longer needed since the atom is stored in DebugInformation. Also the
Debug.Abbrev module is no longer needed.
|
|\
| |
| |
| |
| | |
Conflicts:
cparser/Unblock.ml
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As observed by B. Schommer, it is not enough to track scopes for every source line, as blocks can occur on a single line (think macros). Hence:
- Revert debug annotations of kind 1 to contain only line number info.
Generate them only when the line number changes.
- Use debug annotations of kind 6 to record the list of active scopes
(as BA_int integer arguments to __builtin_annot). Generate them
before every nontrivial statement, even if on the same line as others.
- Remove the generation of "variable x is declared in scope N" debug
annotations. This can be tracked separately and more efficiently.
|
| |
| |
| |
| |
| |
| | |
Instead of creating separate annotations for the local variables
we call the Debug.add_lvar_scope and we construct a mapping from
function id + scope id to scope information.
|
|\|
| |
| |
| |
| |
| | |
Conflicts:
debug/CtoDwarf.ml
debug/DwarfPrinter.ml
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
C2C: the code that insert debug builtins with the line numbers is now
in Unblock. Handle calls to __builtin_debug.
Unblock: generate __builtin_debug(1) for line numbers, carrying
the list of active scopes as extra arguments.
Generate __builtin_debug(6) for local variable declarations,
carrying the corresponding scope number as extra argument.
Constprop: avoid duplicating debug arguments that are constants already.
PrintAsmaux: show this extra debug info as comments.
|
| |
| |
| |
| |
| | |
Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
|
| |
| |
| |
| | |
This reverts commit 861292a6c5e58b4f78bef207c717b801b3fc1fed.
|
| |
| |
| |
| |
| |
| | |
Added a new file debug/Debug.ml which will be the interface between for
generating and printing the debuging information. Currently it contains
only the code for the line directived.
|
|\|
| |
| |
| | |
Merge branch 'master' into debug_locations
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| | |
Use EF_debug instead of EF_annot for line number annotations.
Introduce PrintAsmaux.print_debug_info (very incomplete).
powerpc/Asmexpand: revise expand_memcpy_small.
|