aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* being more archi-independantLéo Gourdin2021-11-021-2/+2
|
* Porting the BTL non-trap loads approach to RTLLéo Gourdin2021-11-021-2/+2
|
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-3/+3
|\ | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-2/+2
| | | | | | | | | | | | | | 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-1/+1
| | | | | | | | | | | | | | | | | | | | | | 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`.
* | __builtin_expect seems to workDavid Monniaux2020-04-071-2/+2
|/
* RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| | | | | | | `external_call_mem_extends` returns a conjunction of 4 properties, but the destruct pattern was 5 level deep. (Reported by Jeremie Koenig in pull request #278.)
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
| | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-2/+2
| | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-061-4/+23
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-41/+28
|
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-116/+116
|
* Issue with ignoring the result of non-void builtin functions.Xavier Leroy2015-09-151-0/+1
| | | | In RTL and beyond, the result of a builtin function that has return type different from "void" must be BR, never BR_none. Otherwise, we get compile-time fatal errors, either in Asmexpand or in Lineartyping.
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-185/+61
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* Extended arguments to annotations, continued:Xavier Leroy2015-03-271-4/+99
| | | | | - Simplifications in RTLgen. - Updated Cexec.
* Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-271-0/+152
| | | | | | | | | | 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.
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-5/+12
| | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating.
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-76/+59
| | | | | | | | | | | | | (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
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-25/+135
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-70/+140
| | | | | | | | | 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
* Remove some useless "Require".xleroy2012-12-301-5/+6
| | | | | | | Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the clightgen branch:xleroy2012-12-291-98/+126
| | | | | | | | | | | | | | | | | | - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-125/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem branch:xleroy2012-05-211-3/+30
| | | | | | | | | | - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-141-18/+15
| | | | | | | | | | | - 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
* Merge of branch new-semantics: revised and strengthened top-level statements ↵xleroy2011-07-151-20/+10
| | | | | | of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+3
| | | | | | | | | | | | | | - 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
* Various algorithmic improvements that reduce compile times (thanks Alexandre ↵xleroy2010-10-271-1/+2
| | | | | | | | | | | | | | Pilkiewicz): - Lattice: preserve sharing in "combine" operation - Kildall: use splay heaps (lib/Heaps.v) for node sets - RTLgen: add a "nop" before loops so that natural enumeration of nodes coincides with (reverse) postorder - Maps: add PTree.map1 operation, use it in RTL and LTL. - Driver: increase minor heap size git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-2/+15
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-61/+13
| | | | | | | | | | | | | | | | | | | | | | - 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
* Support for inlined built-ins.xleroy2010-06-291-0/+16
| | | | | | | | | | | | | 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
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+1
| | | | | | | | - Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In compilation of Sassign, avoid systematic move from a fresh temp.xleroy2010-05-021-30/+57
| | | | | | | | | Those moves are not always coalesced during coloring. The resulting smaller RTL code also reduces the load on the rest of the back-end. RTLgenspec.v: use spiffy saturateTrans tactic to speed up proof search. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1330 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-60/+72
| | | | | | | | | | - Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added support for jump tables in back end.xleroy2009-11-101-28/+55
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-23/+17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-18/+2
| | | | | | | | | | | - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion partielle de la branche contsem: xleroy2008-07-081-686/+440
| | | | | | | | | | - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Utilisation d'une monade avec types dependants pour garder trace des ↵xleroy2007-10-171-15/+14
| | | | | | proprietes state_incr git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@419 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵xleroy2007-08-281-408/+616
| | | | | | 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
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-798/+786
| | | | | | | | | | | | 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
* Simplification de Cminor: les affectations de variables locales ne sontxleroy2006-09-181-259/+204
| | | | | | | | plus des expressions mais des statements (Eassign -> Sassign). Cela simplifie les preuves et ameliore la qualite du RTL produit. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@111 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche "traces":xleroy2006-09-041-214/+289
| | | | | | | | | | | | | - 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
* Ajout construction Sswitch dans Cminorxleroy2006-06-051-5/+64
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@31 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Dans Cminor et Csharpminor: suppression de stmtlist, ajout de Sskip, Sseq.xleroy2006-04-061-97/+80
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@11 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initial import of compcertxleroy2006-02-091-0/+1302
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 10:46:34 +0000