| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
|
|
|
|
|
|
| |
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
|
|\
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/ |
|
|
|
|
|
|
|
|
|
| |
literals.
This is a follow-up to commit 350354c.
- Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse
- Add early checks for overflow and underflow and prove them correct.
- Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
|
| |
|
|\ |
|
| |
| |
| |
| | |
an switch to bail out on earlier on unstructured switch.
|
|/ |
|
|
|
|
|
|
| |
"old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
|
|
|
|
|
| |
(underflow).
Also: spurious '\n' in C2C.warning.
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
- 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.
|
|\ \
| | |
| | | |
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.
|
| | |
|
|/
|
|
| |
ARM is done, IA32 and PowerPC remain to be updated.
|
|
|
|
| |
types must decay to pointer types in the "types" part of Ebuiltin.
|
|
|
|
|
|
| |
Cexec: record names of rules used in every reduction.
Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states.
Csem: fix name of reduction rule "red_call".
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- 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.
|
| |
| |
| |
| | |
induction over composite types.
|
| |
| |
| |
| |
| | |
Use these constructor functions in C2C to rely less on the types produced
by the unverified elaborator.
|
| | |
|
| |
| |
| |
| | |
environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Several definitions in Cutil and elsewhere were accessing the default
value of !Machine.config, before it is properly initialized in Driver.
Delay evaluation of these definitions, and initialize Machine.config
to nonsensical values so that lack of initialization is caught early
(e.g. in Cutil.find_matching_*_kind).
Also, following up on commit [3b8a094], don't use "wchar_t" typedef
to type wide string literals, even if this typedef is in scope.
The risk here is to hide an inconsistency between "wchar_t"'s definition
in standard headers and CompCert's built-in definition.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
|/
|
|
|
|
|
| |
Closes PR#13.
Also: give string literals type unsigned char [] or signed char []
depending on the machine configuration. (Instead of unsigned char [] before.)
|
|
|
|
|
| |
Restrict pointer event values to public global names.
Update proofs accordingly. PowerPC and ARM need updating.
|
|
|
|
| |
For the moment, this field is ignored.
|
|
|
|
|
|
|
|
|
|
|
| |
The previous translation (in SimplExpr) produced references to the
same temporary variable with two different types (bool and int),
which is not nice if we want to typecheck the generated Clight.
The new translation avoids this and also gets rid of the double
cast to bool then to int. The trick is to change Eparen
(in CompCert C expressions) to take two types: the type to which the
argument must be converted, and the type with which the resulting
expression is seen.
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
if an unsupported __builtin_xxx function is used by mistake.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2617 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(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
|