aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Integers.v
Commit message (Collapse)AuthorAgeFilesLines
* Native support for bit fields (#400)Xavier Leroy2021-08-221-0/+112
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| | | | | | Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
* Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | 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.
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-22/+25
| | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-520/+520
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
| | | | The proposed proof only uses `zify` for closing the goal. This is needed for Coq PR #10982 which changes the inner working of `zify`.
* AArch64 portXavier Leroy2019-08-081-24/+136
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | | Should simplify reasoning over Boolean equalities.
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
|
* Define integer sign extension for zero bitsXavier Leroy2019-08-071-14/+27
| | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
* More efficient test for powers of twoXavier Leroy2019-05-091-26/+22
| | | | | | The previous implementation used to build the full powers-of-two decomposition of the number. The present implementation recognizes powers of two directly, then takes the log2.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-835/+33
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-10/+10
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
| | | | | | | Since the number of bits is > 0, it is guaranteed that modulus > 1, not just that modulus > 0. (Suggested by Jake Waksbaum @jbaum.)
* Make the checker happy (#272)Vincent Laporte2019-02-121-8/+8
| | | Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
| | | | | The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3. Fix 23199
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+6
|
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-57/+57
| | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Some lemmas.Bernhard Schommer2017-09-211-0/+14
|
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-43/+134
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* RISC-V port and assorted changesXavier Leroy2017-04-281-3/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
| | | | | | | | | | | - 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.
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
| | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-4/+4
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-618/+618
|
* Tweaks to support defunctorization.xleroy2014-07-231-9/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2536 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵xleroy2014-04-091-0/+10
| | | | | | | | | | 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
* Merge of branch value-analysis.xleroy2013-12-201-0/+13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+28
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add another expansion of shrx in terms of shifts and adds (from Hacker's ↵xleroy2013-07-281-42/+72
| | | | | | Delight). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties about subtraction and borrow.xleroy2013-07-151-18/+59
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2298 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More accurate model of condition register flags for ARM and IA32.xleroy2013-07-131-8/+119
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-35/+59
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Decomposing 64-bit "less than" comparisons.xleroy2013-04-291-9/+70
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2217 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-34/+430
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+2
| | | | | | | | for no good reason. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-0/+4
| | | | | | | | submodules. (Extraction does not remove them, then.) common/Switch: replaced use of FMaps by our own Maps. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Forgot theorem "sign_ext_narrow".xleroy2013-02-121-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-1285/+1593
| | | | | | | | bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Some more properties. Refactored some proofs.xleroy2013-02-041-21/+107
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2109 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-5/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integers: specialized function to compute x mod 2^N; used in "repr" toxleroy2012-12-211-114/+177
| | | | | | | | avoid the cost of a general Zmod. Memdata: updated accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2077 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.xleroy2012-07-091-0/+46
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog: updatedxleroy2012-06-281-0/+40
| | | | | | | | | | driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More properties on mul/div/modxleroy2012-06-091-0/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1918 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-141-20/+127
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Changelog, doc: updated for release 1.9v1.9xleroy2011-08-221-8/+7
| | | | | | | lib/Integers, Makefile: unsuccessful experiments with coqchk git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1723 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-26 18:07:03 +0000