| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In the Clight AST, padding bit fields (such as `int : 6;`) in composite
declarations are given an ident that corresponds to the empty string.
Previously, clightgen would give name `_` to this ident, but this is
not valid Coq.
This commit gives name `empty_ident` to the empty ident. This name
does not start with an underscore, so it cannot conflict with the
names for regular idents, which all start with `_`.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.
This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.
Co-authored-by: Amos Robinson <amos@gh.st>
|
| | |
|
| | |
|
|\ \
| | |
| | |
| | | |
into csmith
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
|\ \
| | |
| | |
| | | |
into csmith
|
| | | |
|
| | | |
|
| |\ \
| | | |
| | | |
| | | | |
into csmith
|
| | | | |
|
| |/ /
|/| | |
|
|/ / |
|
|\ \
| | |
| | |
| | |
| | |
| | | |
into csmith
Z
|
| |\ \
| | | |
| | | |
| | | | |
into csmith
|
| | |\ \
| | | | |
| | | | |
| | | | | |
into csmith
|
| | | | | |
|
| | |/ /
| |/| | |
|
| |/ / |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Squashed commit of the following:
commit 808e72db2022d05a4e34818b33cc9af17aaa4df0
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:53:39 2021 +0200
selectOp for comp0
commit f38e1f15359cceb3c0764635336125a1ceae78ff
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:49:45 2021 +0200
SelectOp for ccomp0 ok
commit ca969280380a593aef590a1fe2ec6f0fc112c2f5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:46:01 2021 +0200
progress
commit e60a970f541ae6be30ec51cf95d60eb672ade829
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:40:49 2021 +0200
progres sur ltu etc.
commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:13:07 2021 +0200
change selection
commit c2af349c6dd3e09fec25f3a96e1272377b6450ef
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:03:31 2021 +0200
begin rewrite selector
|
| | | |
|
|\| | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
|/ / |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Squashed commit of the following:
commit cf033ec29391d5358dea1d3b25da1738957478c4
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 18:01:03 2021 +0200
comment for authors
commit 2ff766a18432fd75739abab0b5741ded6b67a2a5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 15:29:25 2021 +0200
activate register pressure by default
commit 67f4ae2b702cc95ed7cef67b726e15abbf18e768
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 15:26:03 2021 +0200
use a more recognizable option name
commit 6121be54b80a55fdadd8b64dfad53357148c9090
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 14:13:50 2021 +0200
fix for KVX
commit 43d4932e8ba9e00eb8c8788c86f56b6bddd46392
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 13:28:26 2021 +0200
setup registers
commit 169a221104c37737f12abe79711009fc0d88ce09
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 13:00:56 2021 +0200
rm useless code
commit d6a846b641787ea6a5ed113b1d7275ffb5028d9c
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 12:54:19 2021 +0200
rm "Admitted"
commit fd4d085aa988a6044f89fc17e8422be23bc87f9d
Merge: 70f5867e 56498b64
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 12:30:25 2021 +0200
Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press
commit 70f5867e441e253869cb3b432af77636a186d1cb
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Jul 16 12:26:27 2021 +0200
rm TODO
commit f86f5df47b69053702661671340b0fcb31506aa3
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jul 8 11:22:17 2021 +0200
add more debug info
commit a4a0b36f56a94c19da301265a4e3acad1fbdf6c4
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jul 8 11:20:49 2021 +0200
Deactivate sched validator (i think)
commit af97fca0f1d824f3becf9c6895f44ad234e262f8
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jul 6 15:32:35 2021 +0200
Add debug info
commit b96a48de58e1969535865b7b345514a24f7178a6
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Mon Jun 28 16:04:44 2021 +0200
Change temporary solution (see prev commits), and add option for it
commit 9ac49c465f9c8969fba00e6242da0c188a6a3080
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Fri Jun 25 09:42:41 2021 +0200
Changed printfs into debugs
commit dfa09586ae40c70769eeda688a0e7f59f611749f
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jun 24 18:33:20 2021 +0200
Another scheduler
commit c5e8595480604c78260017cc771b0e4195fdd182
Merge: 10cbe4b2 cf2aa686
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 22 15:58:10 2021 +0200
Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
commit 10cbe4b28ef6dc5d02c9a5d4d369484e4943a18d
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 22 15:57:21 2021 +0200
Changed default threshold value following tests
commit cf2aa686bcf9a823562fe977df6dd778d5467985
Merge: eddbce33 fe557bf6
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu Jun 17 17:05:30 2021 +0200
Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
commit eddbce33e28c49bf7b9e83ebd5dbf6cb0d770090
Merge: 8f399dfa fae8d9b5
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu Jun 17 17:05:20 2021 +0200
Merge branch 'kvx-sched-w-reg-press' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-sched-w-reg-press
commit 8f399dfa9d794f2f728f523ff1aa7788cc3599b2
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu Jun 17 17:04:52 2021 +0200
fix for Risc-V
commit fe557bf65ec738eaa078bc5e398ff690eb1f2b9e
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jun 17 17:03:53 2021 +0200
changed type of schedule_seq in x86 for compatibility
commit fae8d9b5c5f93d5eda36f800eb0ca1837b237cba
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jun 17 17:00:57 2021 +0200
fix riscv/Machregsaux.mli
commit 9759e94256fd09f4995418b67b7aedbcf84b4b10
Merge: 4413c27d 04b2489d
Author: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu Jun 17 16:52:09 2021 +0200
Merge remote-tracking branch 'origin/kvx-work' into kvx-sched-w-reg-press
commit 4413c27d6c6a3d69df34955d9d453c38b32174c7
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jun 17 15:38:13 2021 +0200
Add option to set thresold and support for riscv
commit 21278bd87e89210bcc287116f6e35fc1b52d0df2
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Wed Jun 16 20:27:31 2021 +0200
Now working, tests show a decrease in spillage
Should still find a proper way to treat the case mentioned in earlier
commits
commit 87c82b6fcf2bf825a8c60fc6a95498aac9f826d4
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 15 14:44:56 2021 +0200
kinda fixed
Spills are definitely reduced, but lots of arbitrary in there:
See previous commit: need to determine what to do if pressure is too
high but no schedulable instruction can reduce it. For now, advance
time for at most 5 cycles, if still no suitable instruction, go back
to CSP
commit 19464b3992eadf7670acc7231896103ab54885e5
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 15 12:07:43 2021 +0200
fixing
Still need to find what to do when pressure is high but there are no
instructions available that decrease it
commit bff4e6ff0b782619b6fcc18751fa575cbb11de68
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Mon Jun 14 17:39:58 2021 +0200
was very wrong, fixing
commit 3eb3751f84348a20b7ce211fdbf1d01a9c4685a8
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Mon Jun 14 14:46:01 2021 +0200
One fewer spill with new sched on `test/.../spille_forw.c`
commit 66e15205c40de54639387a4c9b1cc78994525d55
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Mon Jun 14 13:53:08 2021 +0200
scheduler written, need to test now
commit 2b814b1f9bb30d9c8b59a713f69bced808bca7c7
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Sat Jun 12 10:52:59 2021 +0200
work on the scheduler
commit 1701e43316ee8e69e794a025a8c9979af6bb8c93
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Thu Jun 10 16:31:51 2021 +0200
Work on new schedluer
Renamed a test file, wrote function to compute pressure deltas,
Still need to pass the info in some way; beginning of the actual
scheduler function
commit 386b9053177bb4ef2801cec00b717c400a828139
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 8 16:53:19 2021 +0200
Fix RTLpathScheduleraux.get_live_regs_entry
commit 9b6247b7996f3e0181d27ec0e20daffd28e0884f
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 8 16:06:36 2021 +0200
Another test : one spill when scheduled forward, none if not
commit 52378f0600652a94edcc8c78e4b426243f717a89
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Tue Jun 8 15:11:03 2021 +0200
Add some tests
commit 2249f3c7771c285ccd25f6e94478be388a741da5
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Sun Jun 6 20:49:34 2021 +0200
Adding debug info
commit 9118878bd14e24cc04c2f36cab7aa7271a0f1852
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Sun Jun 6 12:11:15 2021 +0200
Fixing scope error, and non-exhaustive pattern matching
commit 599823a6410f1629f2b8704291839e0974bce83b
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Sat Jun 5 19:52:59 2021 +0200
function written, now needs testing
commit 98a7a04258f2cf6caf9f18925cbeeae2f5b17be4
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Fri Jun 4 16:56:32 2021 +0200
computing live regs at sb entry from its live output regs
commit 7ae1fb0faea68ce5cfe04a232e49659247c244e9
Author: nicolas.nardino <nicolas.nardino@ens-lyon.fr>
Date: Fri Jun 4 14:24:07 2021 +0200
Passing info of live regs to scheduler: beginning
|
| | |
|
| | |
|
| | |
|