aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Modest optimization of leaf functionsXavier Leroy2017-04-284-46/+241
| | | | | | | | | | Leaf functions are functions that do not call any other function. For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution. This commit suppresses the reloading of LR before returning from a leaf function. LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert. However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed. To support this optimization and its proof: - Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization. - Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR". A number of lemmas that used to show preservation of data registers now show preservation of LR as well.
* Assert instead of unit.Bernhard Schommer2017-04-101-6/+6
| | | | | | Instructions expanded by Asmexpand should never end up in AsmToJSON. Bug 21345
* Filter out functions earlier. Bug 21343Bernhard Schommer2017-04-101-24/+27
|
* Fix name of function. Bug 21378Bernhard Schommer2017-04-071-1/+1
|
* Do not generate code for "inline definitions"Bernhard Schommer2017-04-073-30/+41
| | | | | | | | | ISO C99 states that "inline defintions", functions with inline specifier that are not extern, does not provide an external definition and another compilation unit can contain an external definition. Thus in the case of non-static inline functions no code should be generated. Bug 21343
* Add optimization option finline.Bernhard Schommer2017-04-074-1/+8
| | | | | | The new option f(no-)inline controlls whether inlining is active or not. Bug 21343.
* Another optimization of empty if/else and other useless conditional branchesXavier Leroy2017-04-062-31/+41
| | | | | | | | | | This commit eliminates useless conditional branches during the branch tunneling pass over LTL. Conditional branches where both successors go to the same LTL node are turned into unconditional branches, which will stay or be eliminated by the subsequent Linear pass. One code pattern that triggers this optimization is an empty if/else at the C source level. Commit 4d7a459 eliminates these empty if/else statements early, during the Compcert C -> Clight translation. I think it's good to have both optimizations: - Early elimination makes sure these empty if/else cause no overhead whatsoever, and in particular cannot degrade the precision of later static analyses. - Late elimination catches the case where a nonempty if/else in the source becomes empty as a consequence of optimizations. Future work? If the optimization in Tunneling triggers, it might be worth re-running the Tunneling pass once more, to make sure that the "Lgoto" introduced by the optimization is properly tunneled / skipped over when appropriate.
* attempt to optimize empty if/then/else statementsMichael Schmidt2017-04-063-7/+32
|
* Replace 'decide equality' in powerpc/Op.v. Bug 21332Bernhard Schommer2017-04-031-4/+5
|
* Update the "make check-proof" entry for Coq 8.6Xavier Leroy2017-03-241-3/+2
| | | | `-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
* Added handling if s.sloc <> s1.slocBernhard Schommer2017-03-241-2/+6
| | | | | | If the label is on a different line than the code we can still emit a line directive for the label. Bug 21232
* Emit line stmt after labels in general. Bug 21232Bernhard Schommer2017-03-241-10/+6
|
* Do not emit line info before case stmt.Bernhard Schommer2017-03-241-4/+9
| | | | | | | Since before a case statement is potentially unreachable code due to break, etc. it is better to skip printing line information directly before the case statement and print it afterwards. Bug 21232
* use 'f' as generic function-identifier instead of arbitraty identifier 1 for ↵Michael Schmidt2017-03-231-1/+1
| | | | alloctrace debug-output
* Better fix for problems with quoting in files.Bernhard Schommer2017-03-202-4/+4
| | | | | | Instead of using Filename.quote, string entries are printed with %S. Bug 21216
* Quote directory for comp_dir entry.Bernhard Schommer2017-03-201-2/+2
| | | | | | The compilation directory entry needs quoting since it could be a toplevel directory under windows. Bug 21216
* Merge pull request #175 from silene/IZRXavier Leroy2017-03-0815-150/+121
|\ | | | | | | | | | | | | Adapt proofs to future handling of literal constants in Coq This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
| * Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-0815-150/+121
| | | | | | | | | | | | This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
* | Added missing dltl to dall.Bernhard Schommer2017-03-081-0/+1
|/
* Add a switch to generate a _CoqProject file.Bernhard Schommer2017-02-232-1/+24
|
* Added check for large arrays.Bernhard Schommer2017-02-213-0/+14
| | | | | | | The check tests whether the size calculation of an array overflows or the array covers half of the available address space and reports an error in this case. Bug 21034
* update manpage for new optionsMichael Schmidt2017-02-211-4/+16
|
* Added gcc noinline attribute.Bernhard Schommer2017-02-192-0/+2
| | | | The noinline attribute prevents functions from inlining.
* Added unused attribute and simplified checks.Bernhard Schommer2017-02-172-44/+84
| | | | | | | | | The attribute unused can be used to indicate if a variable or parameter is unused and no warning should be emitted for it. Furthermore this commit simplifies the check by adding a generic function to traverse the program. Bug 19872
* Adopted unused variable and attribtue checkBernhard Schommer2017-02-173-31/+55
| | | | | | | | | The unused variable check now uses two passes. One to collect the used variables and one to report the unused variables. Futhermore attribute checks are extended to composite declaration. Also the check is now performed after elaboration. Bug 19872
* Extended unused vars check for params.Bernhard Schommer2017-02-173-2/+9
| | | | | | The test now also checks whether the parameter are used at all in the function body. Bug 19872
* Added a simple check for unused variables.Bernhard Schommer2017-02-175-2/+88
| | | | | | | | | | | | | | | | | The check test whether the identifier is used at all in the function and if not issue a warning. It is not tested whether the usage is reachable at all, so int i; if (0) i; would not generate a warning. This is the same as gcc/clang does. The warning is disabled per default, but is active if -Wall is given. Bug 19872
* Checks can be applied add several places.Bernhard Schommer2017-02-173-8/+5
| | | | | | There should not be a single check place, since for example unknonw attributes should be check after elaboration and other simplifications.
* Also check the locals. Bug 19872.Bernhard Schommer2017-02-171-3/+7
|
* Added new module for checks on elaborated C codeBernhard Schommer2017-02-173-2/+114
| | | | | | | The new module adds a function which is called during parse after all C transformation have taken place for adding additional checks. Currently only unknown attribute are checked. Bug 19872
* Do not optimize away the 'return 0' at end of 'main'Xavier Leroy2017-02-171-7/+5
| | | | | | As a cosmetic optimization enabled by the static analysis in Cflow, we used to not insert a 'return 0' at end of 'main' if the body of 'main' cannot fall through. Since this optimization is cosmetic (the back-end will remove the 'return 0' if unused) and since we don't fully trust this static analysis, revert this optimization and always insert 'return 0'.
* Control-flow analysis: bug in switch without defaultXavier Leroy2017-02-171-1/+30
| | | | If no 'default' case appears in a 'switch', one is implicit at the end of the switch body, making possible to have a fall-through behavior.
* Merge pull request #172 from AbsInt/std_noreturn_funXavier Leroy2017-02-173-3/+14
|\ | | | | | | Treat as _Noreturn the standard C11 functions that are _Noreturn but not always declared as such in header files.
| * Added _exit.Bernhard Schommer2017-02-171-1/+1
| |
| * Add longjmp. Bug 21009Bernhard Schommer2017-02-171-1/+1
| |
| * Added handling for noreturn std functions.Bernhard Schommer2017-02-163-3/+14
|/ | | | | | | | | | The C11 standard declares exit,abort,_Exit,quick_exit and thrd_exit as _Noreturn however this is not included in older C libs and leads to false negatives in reporting _Noreturn and return type warnings. This can be avoided by enhancing the noreturn check of the Cflow analysis to also test if one of the above functions is called. Bug 21009
* Reverted changes in Cutil and catch in Cflow.Bernhard Schommer2017-02-162-17/+5
| | | | | | Instead of changing the definition of sizeof we now ignore errors raise in the Cflow module. Bug 21005
* Fixed problem with local structs/unions in Cflow.Bernhard Schommer2017-02-161-4/+17
| | | | | | | | Since the function environment does not necessary contain structs and unions defined in sizeof expressions the evaluation should be not constant and the Environment excpetions should be catched. Fix 21005
* drop .cm support from man pageMichael Schmidt2017-02-151-4/+0
|
* Merge pull request #167 from AbsInt/pipe_prerequisiteXavier Leroy2017-02-158-35/+27
|\ | | | | Introduced configuration variable for gnu systems.
| * Introduced configuration variable for gnu systems.Bernhard Schommer2017-02-138-35/+27
| | | | | | | | | | | | | | The variable gnu_toolchain is true if a gnu toolchain is used and false in all other cases. The variable avoids the explicit test whether the system string is diab and should be easier to change. Bug 20521.
* | Merge pull request #162 from AbsInt/return-analysis-2Xavier Leroy2017-02-155-32/+290
|\ \ | | | | | | | | | Improved warnings related to function returns
| * | Cflow: analysis of "switch" was too impreciseXavier Leroy2017-02-071-2/+3
| | | | | | | | | | | | Plus: updated comments.
| * | Revised, more precise implementation of control-flow analysisXavier Leroy2017-02-071-48/+98
| | | | | | | | | | | | The new implementation keeps track of goto labels that are actually branched to. It is less optimized than the previous implementation (no bit vectors) but perhaps easier to read.
| * | Control-flow analysis: wrong flow for "case"/"default" statementsXavier Leroy2017-02-071-4/+6
| | | | | | | | | | | | Those labeled statements can be entered either by fall-through or by the enclosing switch.
| * | More precise warnings about function returnsXavier Leroy2017-02-075-32/+237
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit introduces a control-flow static analysis over C abstract syntax (file cparser/Cflow.ml) and uses it to - warn for non-void functions that can return by falling through the body - warn more precisely for _Noreturn functions that can return - introduce the "return 0" in "main" functions less often (cosmetic). For the control-flow analysis, the following conservative approximations are made: - any "goto" label is reachable - all cases of a "switch" statement are reachable as soon as the "switch" is reachable (i.e. the switch expression takes all values needed to reach every case) - the boolean expressions in "if", "while", "do"-"while" and "for" can take true and false values, unless they are compile-time constants.
* | | Remove tests involving Cminor concrete syntax. Update ChangelogXavier Leroy2017-02-1529-3336/+3
| | | | | | | | | | | | Follow-up to [29653ba]
* | | Merge pull request #170 from AbsInt/remove_cminorXavier Leroy2017-02-159-1379/+3
|\ \ \ | | | | | | | | | | | | | | | | | | | | Remove CompCert's ability to parse and compile source files written in Cminor This facility is no longer used (as far as we know) and is painful to maintain.
| * | | Removed CMinor import. Bug 20992Bernhard Schommer2017-02-149-1379/+3
| | | |
* | | | Removed superfluous semicolon.Bernhard Schommer2017-02-141-1/+1
|/ / /
generated by cgit (git 2.34.1) at 2024-07-02 20:22:42 +0000