| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.
The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.
The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".
All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.
The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.
Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.
The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).
Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.
This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.
Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.
|
|
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- 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.
|
|
|
|
| |
Also: factor out the type "program" between Csyntax and Clight, putting it in Ctypes.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- C function types and Cminor signatures annotated by calling conventions.
esp. vararg / not vararg
- Cshmgen: generate correct code for function call where there are
more arguments than listed in the function prototype. This is
still undefined behavior according to the formal semantics,
but correct code is generated.
- C2C, */PrintAsm.ml: remove "printf$iif" hack.
- powerpc/, checklink/: don't generate stubs for variadic functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Update ARM port.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
| |
and __alignof__(ty), __alignof__(expr) from GCC.
- Resurrected __builtin_memcpy_aligned, useful for files generated
by Scade KCG 6.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
| |
- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
(Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Csyntax, Csem: source C language has side-effects within expressions,
performs implicit casts, and has nondeterministic reduction semantics
for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
(previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
and matching -dxxx command-line flags.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
and a machine-dependent part (ARCH/SYS/Conventions1).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
| |
Clight and C#minor. Recognize __builtin_fabs and turn it into this operator.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
Introduced and used Csyntax.typeconv to address this issue and reduce the number of cases in the classify functions
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1266 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
caml/PrintCsyntax.ml: afficher les formes a[b] et a->fld.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@789 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
|
|
|
|
| |
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
| |
meilleure compilation de exit_if_false.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
Adaptation frontend, backend en consequence.
Integration passe C -> C#minor dans common/Main.v.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|