aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Csem.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge of the clightgen branch:xleroy2012-12-291-1/+0
| | | | | | | | | | | | | | | | | | - 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
* Make Clight independent of CompCert C.xleroy2012-10-081-519/+2
| | | | | | | 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
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-39/+95
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-2/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support for _Alignof(ty) operator from ISO C 2011xleroy2012-02-261-0/+3
| | | | | | | | | | 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
* Merge of the "volatile" branch:xleroy2012-02-041-91/+180
| | | | | | | | | | | | - 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
* Cleaned up old commented-out partsxleroy2011-08-191-34/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved semantics of castsxleroy2011-07-171-0/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵xleroy2011-07-161-127/+96
| | | | | | | | | the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch new-semantics: revised and strengthened top-level statements ↵xleroy2011-07-151-6/+3
| | | | | | of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix treatment of function pointers at function calls in the CompCert C and ↵xleroy2011-07-141-2/+3
| | | | | | Clight semantics git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1680 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch "unsigned-offsets":xleroy2011-04-091-6/+11
| | | | | | | | | | | | | | - 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
* Initializers for global variables: compile-time evaluation of expressions ↵xleroy2011-03-121-1/+1
| | | | | | done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-3/+4
| | | | | | | (May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nettoyages pour docxleroy2010-08-181-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1471 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-2/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:xleroy2010-08-181-1176/+617
| | | | | | | | | | | | | | | | | | | | | | - 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-6/+6
| | | | | | | | | | | | | 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-2/+2
| | | | 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-2/+2
| | | | | | | | - 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
* Suppressed axioms Float.eq_zero_{true,false}, since the latter isxleroy2010-05-091-3/+4
| | | | | | | | | | wrong because of +0.0 / -0.0. Adapted Clight semantics accordingly. (Truth value of a float is defined by comparison Float.cmp Ceq with 0.0, no longer by structural equality.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-0/+7
| | | | | | | 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
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-39/+46
| | | | | | | | | | - 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
* Function types didn't always degrade to pointers like they should. ↵xleroy2010-03-021-1/+1
| | | | | | 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
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-3/+3
| | | | | | | | | Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Last updates for release 1.5.v1.5xleroy2009-08-281-9/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Distinguish two kinds of nonterminating behaviors: silent divergencexleroy2009-08-161-25/+31
| | | | | | | | | | | | | | and reactive divergence. As a consequence: - Removed the Enilinf constructor from traceinf (values of traceinf type are always infinite traces). - Traces are now uniquely defined. - Adapted proofs big step -> small step for Clight and Cminor accordingly. - Strengthened results in driver/Complements accordingly. - Added common/Determinism to collect generic results about deterministic semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-99/+876
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-4/+4
| | | | | | | | lib/Integers.v: added more properties for ARM port. lib/Coqlib.v: added more properties for division and powers of 2. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@928 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-5/+10
| | | | | | | | 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
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-10/+22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs ↵xleroy2008-05-301-1/+1
| | | | | | vers des blocs differents! git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-131-20/+15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@447 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Relaxation de la regle d'evaluation Ecastxleroy2007-10-171-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@420 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les ↵xleroy2007-08-281-185/+292
| | | | | | 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
* Documentationxleroy2007-08-051-24/+89
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-1/+2
| | | | | | | | | | | | 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
* Revu traitement des structures et unions recursives. Dans Cshmgen, ↵xleroy2006-09-111-4/+4
| | | | | | meilleure compilation de exit_if_false. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@94 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Permettre les casts entre types de fonctionxleroy2006-09-061-12/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Csem: l'hypothese de typage sur main est inutile (assuree par wt_program)xleroy2006-09-061-1/+0
| | | | | | | | Ctyping: relaxation de l'hypothese de typage sur main Cshmgenproof3: adaptation a ces changements. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@82 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-8/+2
| | | | | | | | 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
* Fusion de la branche "traces":xleroy2006-09-041-0/+752
- 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
generated by cgit (git 2.34.1) at 2024-07-01 08:19:38 +0000