aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
* | | 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.
* | | GPR#84: extend Cminor parser to handle single-precision FP operationsXavier Leroy2016-03-152-3/+20
| | |
* | | GPR#84: add missing IA32 operators to PrintOpXavier Leroy2016-03-151-0/+3
| | |
* | | Merge pull request #90 from AbsInt/sem-castsXavier Leroy2016-03-1114-323/+368
|\ \ \ | | | | | | | | Make casts of pointers to _Bool semantically well defined
| * | | Make casts of pointers to _Bool semantically well defined (again).Xavier Leroy2016-03-0214-323/+368
| | | | | | | | | | | | | | | | | | | | | | | | In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics. This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue.
* | | | Merge branch 'relaxed-pointer-arithmetic'Bernhard Schommer2016-03-111-6/+21
|\ \ \ \ | |_|_|/ |/| | |
| * | | Relaxing the semantics of pointer arithmetic.Xavier Leroy2016-02-291-6/+21
| | | | | | | | | | | | | | | | | | | | | | | | Support <pointer> +/- <integer> where the pointer value is actually an integer (Vint) that has been converted to pointer type. Such arithmetic, while not defined in ISO C, appears in the wild. If present in static initializers, it used to cause a compile-time failure ("not a compile-time constant"). Hence this relaxation.
* | | | Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| |_|/ |/| | | | | | | | | | | | | | Compare the underlying array types, otherwise we end up in a endless recursion. Bug 18374
* | | Added more support for gcc options.Bernhard Schommer2016-03-021-4/+75
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Added the gcc options for the preprocessor: -Xpreprocessor -M -MM -MF -MG -MP -MT -MQ -nostdinc -imacros -idirafter -isystem -iquote -P -C -CC Also warn for not supported GCC options in the diab case. Bug 18066
* | Merge remote-tracking branch 'origin/configuration-split'Bernhard Schommer2016-02-293-23/+58
|\ \
| * | Split up tools and options.Bernhard Schommer2016-02-253-23/+58
| | | | | | | | | | | | | | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* | | Added gcc's Xassembler option.Bernhard Schommer2016-02-291-3/+8
| | | | | | | | | | | | | | | | | | | | | The Xassembler option passes one option to the assembler and can be used to pass options to the underlying assembler that the gcc driver does not recognize. Bug 18066
* | | Fixed typo. Bug 18066Bernhard Schommer2016-02-291-3/+4
| | |
* | | Added some gcc linker options.Bernhard Schommer2016-02-261-0/+22
|/ / | | | | | | | | | | | | | | | | | | | | CompCert now recognizes the gcc linker options: -nostartfiles -nodefaultlibs -nostdlib -s -Xlinker <opt> -u <symb> Bug 18066.
* | bug 18168, catch cases where variadic arguments are transfered via registersMichael Schmidt2016-02-241-2/+2
| |
* | bug 18168, fix offset computation for var-args in ARM stacklayoutMichael Schmidt2016-02-241-1/+1
| |
* | bug 18209, make message compatible to clangMichael Schmidt2016-02-231-1/+1
| |
* | bug 18209, check that input files existMichael Schmidt2016-02-231-0/+14
|/
* PR#87: include the BSD license in the LICENSE file.Xavier Leroy2016-02-191-1/+28
|
* Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.Xavier Leroy2016-02-181-2/+8
| | | | | | | | | | | Two reasons: - The movs is not supported if rd or rs is r13 (the stack ptr register). Newer versions of GNU as reject it, older versions were probably emulating it. - The purpose of setting the "s" flag on some operations is to enable 16-bit encoding in Thumb2 mode. However, for "mov" it is the non-s form that has a 16-bit encoding; the s form is never more compact.
* Added new option for static linking.Bernhard Schommer2016-02-161-0/+2
| | | | | The new option -static passes the -static flag to the linker. Bug 18066.
* Fixed regression introduced by refactoring of Driver.ml.Bernhard Schommer2016-02-151-3/+7
|
* Merge pull request #86 from AbsInt/clightgen-improvedBernhard Schommer2016-02-054-90/+114
|\ | | | | Better treatment of names in the clightgen tool
| * Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | | | | | clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
| * Restart the name generator at first_unused_ident for every function.Xavier Leroy2016-02-053-58/+38
|/ | | | This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
* Also print braces around the registers.Bernhard Schommer2016-02-041-2/+7
|
* Fixed missing \" in json printing for registers.Bernhard Schommer2016-02-041-2/+2
|
* Added gcc cmd-line option -include.Bernhard Schommer2016-02-031-0/+3
| | | | | | | The -include option is passed to the preprocessor and -include <file> is equivalent to writting #include "<file>" as first line in the primary source file. Bug 18066.
* Merge pull request #85 from AbsInt/option_jsonXavier Leroy2016-02-024-107/+299
|\ | | | | | | Flag -doptions to save machine configuration and command-line flags to a JSON file.
| * Added version and compiler working directory to options dump.Bernhard Schommer2016-01-271-0/+4
| |
| * Added new option -doptions.Bernhard Schommer2016-01-272-4/+58
| | | | | | | | | | | | The new options dumps the compiler options in a json file per. This includes the clflags, compcert.ini and machine settings. Bug 17988.
| * Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-255-135/+201
| |
| * Started implementing a printer for Clflags.Bernhard Schommer2016-01-254-12/+80
| |
* | Make void always incomplete and exit on void members.Bernhard Schommer2016-02-022-2/+8
| | | | | | | | | | | | Since we cannot construct a default initializer for void types we need to exit earlier. Bug 18004.
* | Do test for wrap around on singed ocaml integers.Bernhard Schommer2016-01-281-1/+1
| | | | | | | | | | | | In parse_int it was not tested if the value of v is smaller than zero. This allowed it that certain large integers were accepted due to wrap around.
generated by cgit (git 2.34.1) at 2024-07-04 22:31:03 +0000