| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| | |
__builtin_get_spr() and __builtin_set_spr() work, but horrible error
message if the SPR argument is not a constant.
powerpc/AsmToJSON.ml needs updating.
|
| |
| |
| |
| | |
structured builtin arguments and results.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Before, the back-end languages had distinct instructions
- Iannot for annotations, taking structured expressions (annot_arg)
as arguments, and producing no results'
- Ibuiltin for other builtins, using simple pseudoregs/locations/registers
as arguments and results.
This branch enriches Ibuiltin instructions so that they take structured
expressions (builtin_arg and builtin_res) as arguments and results.
This way,
- Annotations fit the general pattern of builtin functions,
so Iannot instructions are removed.
- EF_vload_global and EF_vstore_global become useless, as the
same optimization can be achieved by EF_vload/vstore taking
a structured argument of the "address of global" kind.
- Better code can be generated for builtin_memcpy between stack locations,
or volatile accesses to stack locations.
Finally, this commit also introduces a new kind of external function,
EF_debug, which is like EF_annot but produces no observable events.
It will be used later to transport debug info through the back-end,
without preventing optimizations.
|
|\ \ \
| | |/
| |/|
| | |
| | |
| | |
| | | |
Conflicts:
debug/CtoDwarf.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
|
| | |
| | |
| | |
| | | |
Plus: update comments and credit Bernhard Schommer.
|
| | |
| | |
| | |
| | | |
according to Intel convention (instr destination, argument).
|
|/ / |
|
|/
|
|
| |
More bugs remain.
|
|\
| |
| | |
Merge branch 'asmexpand' of github.com:AbsInt/CompCert
|
| |\ |
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing
changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | | |
integers with Uns or Sgn abstract values.
This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
|
| |/
|/|
| |
| |
| |
| | |
operations with undefined behaviors.
Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
|
|\| |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
|\| |
|
| |
| |
| |
| | |
Val.lessdef, etc.
|
|/ |
|
|
|
|
| |
clobber lists.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
cparser/ExtendedAsm.ml
|
| |
|
| |
|
|\ |
|
| |\
| | |
| | | |
Extended annotations
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
variables whose address is taken.
- CminorSel, RTL: add "annot" instructions.
- CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions.
- AST, Events: simplify EF_annot because constants are now part of the arguments.
Implementation is not complete yet.
|
| |\ \
| | | |
| | | | |
Revised semantics of comparisons between a pointer and 0.
|
| | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
It used to be that a pointer value (Vptr) always compare unequal to the
null pointer (Vint Int.zero). However, this may not be true in the
final machine code when pointer addition overflows and wraps around
to the bit pattern 0. This patch checks the validity of the pointer
being compared with 0, and makes the comparison undefined if the
pointer is out of bounds.
Note: only the IA32 back-end was updated, ARM and PowerPC need updating.
|
|\| |
| | |
| | |
| | |
| | |
| | | |
Conflicts:
Makefile
driver/Driver.ml
|
| | | |
|
| |\ \
| | | |
| | | |
| | | |
| | | | |
Conflicts:
ia32/PrintAsm.ml
|
| |\ \ \ |
|
| | | | | |
|
| | |\ \ \ |
|
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
needed.
|
| | | | | | |
|
| | | | | | |
|
| | |/ / /
| | | | |
| | | | |
| | | | | |
is that every symbol must start with an "_".
|
| |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The passing of struct/union arguments by value implemented in the verified
part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
Here we enrich the StructReturn source-to-source emulation pass
so that it implements the calling conventions defined in these ABIs.
Plus: for x86, implement the returning of struct/union results by value
in a way compatible with the ABI.
|
|\ \ \ \
| | |_|/
| |/| | |
|