aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Added iso646 header for alternate spellings.Bernhard Schommer2016-04-061-0/+49
| | | | | | | The iso646 header defines some macros that expand to common operators. Both clang and gcc ship with them and they are required by the standard. Bug 18645.
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
* Check for type compatibility when initializing TInt arrays with wide strings ↵Michael Schmidt2016-04-061-1/+1
| | | | (§6.7.8), bug 18000
* Revert initialization check, bug 18000Michael Schmidt2016-04-051-8/+0
|
* Match type size with size of wchar_t when initializing TInt arrays with wide ↵Michael Schmidt2016-04-051-1/+1
| | | | strings, bug 18000
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-2/+2
|
* Catch initialization of arrays with single expressions, bug 18000Michael Schmidt2016-04-051-0/+8
|
* Merge pull request #95 from AbsInt/noreturnBernhard Schommer2016-04-0411-26/+150
|\ | | | | Added the _Noreturn keyword.
| * Added the _Noreturn keyword.Bernhard Schommer2016-03-2311-26/+150
| | | | | | | | | | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* | Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-314-6/+10
|/
* Merge pull request #94 from jhjourdan/parentherized_funBernhard Schommer2016-03-232-0/+18
|\ | | | | Fix a bug in the pre-parser.
| * Fix a bug in the pre-parser.Jacques-Henri Jourdan2016-03-232-0/+18
|/
* Also refactor clightgen to work with new warnings. Bug 18394Bernhard Schommer2016-03-231-6/+6
|
* Merge branch 'master' of github.com:AbsInt/CompCertBernhard Schommer2016-03-211-1/+1
|\
| * configure: fix test for CFI directivesXavier Leroy2016-03-211-1/+1
| | | | | | | | The test was failing as a consequence of the split casm -> casm / casm_options.
* | Reverted name for entry back to the old one.Bernhard Schommer2016-03-211-1/+1
|/ | | | | Valex expects Fun Section Literals and not Fun Section Literal. Bug 18394
* Merge pull request #92 from AbsInt/cleanupXavier Leroy2016-03-2168-647/+624
|\ | | | | This PR activates more OCaml warnings and turns all warnings into errors. Also some unused functions, variables and types are removed.
| * Merge branch 'master' into cleanupBernhard Schommer2016-03-2188-5401/+6282
| |\
| * | Revert "Add the -Xalign-value options for diab."Bernhard Schommer2016-03-181-1/+0
| | | | | | | | | | | | This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
| * | Add the -Xalign-value options for diab.Bernhard Schommer2016-03-181-0/+1
| | | | | | | | | | | | | | | | | | The default of the diab compiler is to interpret the alignment as power of two. Bug 18490.
| * | Added an interface file for DebugInformation.Bernhard Schommer2016-03-185-43/+183
| | | | | | | | | | | | | | | | | | The interface hides the implementation details, like the huge number of Hashtbls from the rest of the implementatio. Bug 18394
| * | Added interface for the Asmexpansion.Bernhard Schommer2016-03-165-10/+55
| | | | | | | | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394
| * | Change atom printer to use the common function.Bernhard Schommer2016-03-161-1/+1
| | | | | | | | | | | | | | | | | | The printer for atom constants should also use the printer for singleton objects. Bug 18394
| * | Cleanup of AsmToJSON.Bernhard Schommer2016-03-166-128/+140
| | | | | | | | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
| * | Removed not needed env.Bernhard Schommer2016-03-151-5/+5
| | | | | | | | | | | | | | | | | | The functions for naming string and wstring literals no longer need an env. Bug 18394
| * | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1547-447/+449
| | | | | | | | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
| * | Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
| | | | | | | | | | | | | | | | | | Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394
| * | Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-156-26/+28
| | | | | | | | | | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
| * | Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-116-28/+26
| | | | | | | | | | | | | | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394
| * | Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
| | | | | | | | | | | | | | | Removed unused code and code generating warnings. Bug 18394
| * | Clean up of ia32 target dependend code.Bernhard Schommer2016-03-104-58/+18
| | | | | | | | | | | | | | | Removed some unused functions and opens. Bug 18394
| * | Cleanup of ARM dependedn code.Bernhard Schommer2016-03-102-66/+8
| | | | | | | | | | | | | | | Removed unused functions and avoid warnings. Bug 18394.
| * | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-105-17/+21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
| * | Code cleanup.Bernhard Schommer2016-03-1056-740/+590
| | | | | | | | | | | | | | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* | | Also ignore windows line endings.Bernhard Schommer2016-03-211-1/+2
| |/ |/| | | | | | | | | Windows style line endings can end up in the Tokenize pass. This can lead to some problems for example in pragma processing. Bug 18316
* | Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2073-5026/+5836
|\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This pull request implements "approach A" to separate compilation in CompCert from the paper Lightweight verification of separate compilation by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL 2016, pages 178-190 In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program. This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
| * | Misc updates following the introduction of the new linking frameworkXavier Leroy2016-03-065-39/+44
| | |
| * | Strengthen the main compiler correctness results to account for separate ↵Xavier Leroy2016-03-061-149/+250
| | | | | | | | | | | | | | | | | | compilation and linking Define a "match_prog" relation corresponding to the composition of CompCert's passes. Use it to show semantic preservation (backward/forward simulations) not just for the compilation of whole programs, but also for the separate compilation of multiple units followed by linking.
| * | Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-0611-533/+559
| | |
| * | Define linking for Csyntax and Clight programs.Xavier Leroy2016-03-063-114/+523
| | | | | | | | | | | | Also: factor out the type "program" between Csyntax and Clight, putting it in Ctypes.
| * | Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-0636-2188/+2093
| | |
| * | Put forward_simulation and backward_simulation in Prop instead of TypeXavier Leroy2016-03-062-303/+323
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The original presentation of forward_simulation and backward_simulation diagrams was using records containing types, relations, and properties over these. These records had to live in Type because in Prop the projections could not be defined. This was causing problems with proofs of statements such as (exists x, P x) -> forward_simulation sem1 sem2 because the exists could not be eliminated in a Type context. This commit re-expresses the simulation diagrams as a record of properties (in Prop) and an inductive (in Prop too) that packs the record with the types and relations. The external interface of module Smallstep is unchanged, it's only the proofs in Smallstep and Behaviors that take a slightly different shape.
| * | Add support for EF_runtime externalsXavier Leroy2016-03-069-57/+47
| | | | | | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
| * | Globalenvs: adapt to new linking framework, and revise.Xavier Leroy2016-03-061-1146/+729
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The commutation lemmas between program transformations and Genv operations now take separate compilation into account. For example: Theorem find_funct_ptr_match: forall b f, find_funct_ptr (globalenv p) b = Some f -> exists cunit tf, find_funct_ptr (globalenv tp) b = Some tf /\ match_fundef cunit f tf /\ linkorder cunit ctx. Note how "f" and "tf" are related wrt a compilation unit "cunit" which is not necessarily "ctx" (the context for the whole program), but can be a sub-unit of the this whole program. The other changes in Globalenvs are a long-overdue refactoring and cleanup: - Introduce Senv.equiv (extensional equivalence between two Senv.t) to collect (in one place) the invariance properties relevant to external functions (preservation of names, of public names, and of volatile blocks). - Revise internal representation of Genv.t: one map ident -> globdef F V instead of two maps ident -> F and ident -> globvar V. - More precise characterization of initial memory states: "Genv.init_mem_characterization" uniquely characterizes every byte (memval) of the representation of an initialized global variable. - Necessary and sufficient conditions for the initial memory state to exist. - Revised proofs about init_mem, especially init_mem_inject. - Removed some Genv lemmas that were unused.
| * | AST: extend and adapt to the new linking framework.Xavier Leroy2016-03-061-460/+116
| | | | | | | | | | | | | | | | | | | | | - Add "prog_defmap" to compute the ptree name -> global definition corresponding to a program. - Move "match_program" to Linking. - Clean up and simplify a bit the transf_* functions for program transformations. - Add a new kind of external functions, "EF_runtime". Unlike "EF_external", an "EF_runtime" external function cannot be implemented by an internal function definition in another compilation unit. (Linking returns an error in this case.) We will use "EF_runtime" for the "_i64_*" helper functions, which must not be defined by the program, and instead must remain external.
| * | The basic framework for linking and separate compilation.Xavier Leroy2016-03-061-0/+905
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This framework follows "approach A" from the paper "Lightweight Verification of Separate Compilation" by Kang, Kim, Hur, Dreyer and Vafeiadis, POPL 2016. Syntactic linking (of compilation units and their syntactic elements) is modeled by a type class with two components: - a partial binary operation "link" that returns the syntactic element corresponding to the act of linking together its two arguments. It may fail if the two arguments cannot be linked, e.g. are incompatible definitions of the same name. - a partial order "linkorder x y" that holds if "x" is a sub-unit of a whole program or bigger unit "y", or in other words, if "y" can be obtained by linking "x" with other units. Instances of this type class are provided for the type AST.program and its syntactic elements (globvar, globdef, etc). The "match_program" predicate that provides a relational characterization of compiler passes / program transformations is extended to account for context-dependent transformations and separate compilation: the transformation of a function definition can depend on the compilation unit it occurs in (this is the context), and this compilation unit "ctx" is characterized as any unit that is in the "linkorder ctx prog" relation with the whole source program "prog". Under mild hypotheses, we show that "match_program" commutes with linking: if a1 matches b1, a2 matches b2, and a1 and a2 link together producing a, then b1 and b2 link together, producing a b that matches a. Finally, we extend binary linking to linking of a nonempty list of compilation units; commutation with "match_program" still holds.
| * | Preliminaries: minor extensions to MemoryXavier Leroy2016-03-061-3/+58
| | | | | | | | | | | | | | | - Make Mem.unchanged_on transitive. - Add Mem.drop_perm_unchanged_on.
| * | Preliminaries: extend the Coqlib and Maps libraries.Xavier Leroy2016-03-062-34/+189
| | | | | | | | | | | | | | | | | | | | | - Coqlib: option_rel to lift a relation to option type. - Coqlib: more lemmas about list_forall2. - Coqlib: introduce type nlist (nonempty lists) and some operations. - Maps: a variant of PTree.elements_extensional that uses option_rel.
* | | Add -Xalign-value to enforce correct alignment.Bernhard Schommer2016-03-181-2/+3
| | | | | | | | | | | | | | | | | | The diab compiler seems to interpret the alignment as power of two instead of the value. Bug 18490
* | | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-159-22/+22
| | | | | | | | | | | | | | | | | | As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing.
generated by cgit (git 2.34.1) at 2024-07-01 07:49:28 +0000