| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
|
|
|
|
|
|
|
| |
- 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
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
- Simplifications in RTLgen.
- Updated Cexec.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
global target dependend option to activate the printing only for targets wher it works.
|
| | |
|
|\|
| |
| |
| |
| |
| |
| | |
Conflicts:
arm/PrintAsm.ml
ia32/PrintAsm.ml
powerpc/PrintAsm.ml
|
| |
| |
| |
| | |
default function aligment to be target dependent.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
|\| |
|
| |\
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
|
| | |
| | |
| | |
| | | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
|\| | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is achieved by declaring these functions in C2C.ml, then
re-checking their declarations in the global environment during
the Selection pass.
In passing, the "hf" parameter for SelectLong functions was removed
and replaced by fixed identifiers corresponding to the actual names
of the helper functions.
|
| | |
| | |
| | |
| | | |
global const variable.
|
|\| | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In the presence of separate compilation and linking, an uninitialized
const global variable may be initialized elsewhere with a pointer value,
falsifying the points-to analysis. Report and fix by Chung-Kil Hur
and Jeehoon Kang.
|
|\| |
| |/
|/|
| |
| | |
Conflicts:
powerpc/PrintAsm.ml
|
|/
|
|
|
|
| |
comments.
Refactor printing of .loc debug directives in backend/PrintAnnot.ml
|
|
|
|
| |
definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
|
|
|
|
|
| |
Restrict pointer event values to public global names.
Update proofs accordingly. PowerPC and ARM need updating.
|
|
|
|
| |
For the moment, this field is ignored.
|
|
|
|
| |
them off.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(in CompCert C to Cminor, included)
- Translation of "switch" to decision trees or jumptables made generic
over the sizes of integers and moved to the Cminor->CminorSel pass
instead of CminorSel->RTL as before.
- CminorSel: add "exitexpr" to support the above.
- ValueDomain: more precise analysis of comparisons against an integer
literal. E.g. "x >=u 0" is always true.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
| |
The only platform where we have two variants is ARM, and it's easier
to share the callling convention code between the two than to maintain
both variants separately.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
support saving and restoring registers without knowing
the exact types (int/single/float) of their contents, just
their sizes.
- Memory model: generalize the opaque encoding of pointers to
apply to any value, not just pointers, if chunks Many32/Many64
are selected.
- More properties of FP arithmetic proved.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
(Merge of branch newparser.)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
over booleans.
Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31].
Driver: timer for whole compilation.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
- Use a hashtable instead of an AVL set for adjSet
- Inlining and algebraic simplification of spillCost into selectSpill.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2450 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|