aboutsummaryrefslogtreecommitdiffstats
path: root/driver
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | Add missing comment for print_version_file_and_exitChristoph Cullmann2020-07-301-0/+1
| | | |
| | * | No trailing commas for --version-file option.Bernhard Schommer2020-07-091-1/+1
| | | |
| | * | Fix typo.Bernhard Schommer2020-07-081-1/+1
| | | |
| | * | Revert "Use the same version string."Bernhard Schommer2020-07-081-3/+10
| | | | | | | | | | | | | | | | This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790.
| | * | Use the same version string.Bernhard Schommer2020-07-081-10/+3
| | | | | | | | | | | | | | | | | | | | | | | | The version string dumped in the file should be the same as the version string printed by `-version`. The option is also not printed by `-help` since it is for internal use only.
| | * | Remove no longer needed option enforce-buildnrBernhard Schommer2020-07-081-10/+1
| | | |
| | * | Introduce additional "branch" build information.Bernhard Schommer2020-07-081-3/+5
| | | |
| | * | Add option to print version information in fileBernhard Schommer2020-07-081-1/+17
| | | |
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-196/+0
| | | | | | | | | | | | | | | | | | | | | | | | The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/
| | * | Move reserved_registers to CPragmas.Bernhard Schommer2020-04-201-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
* | | | set prepass by defaultDavid Monniaux2020-11-271-1/+1
| |_|/ |/| |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-1/+1
|\ \ \
| * | | Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-161-1/+1
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle.
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-032-0/+4
|\| |
| * | Loop Rotate with -flooprotateCyril SIX2020-11-032-0/+4
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-312-0/+3
|\| |
| * | refining CSE3 nodesDavid Monniaux2020-10-312-0/+3
| | |
| * | deactivate LICMDavid Monniaux2020-10-281-1/+1
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-0/+1
|\| |
| * | Merge branch 'kvx-work' into duplicate-paramCyril SIX2020-10-273-0/+7
| |\ \
| * | | Reworked Duplicate to be parametrizedCyril SIX2020-10-271-0/+1
| | | |
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-273-0/+7
|\ \ \ \ | | |/ / | |/| |
| * | | new option for CSE3 (trivial ops)David Monniaux2020-10-273-0/+7
| |/ /
* | | deactivate LICM by defaultDavid Monniaux2020-10-271-1/+1
| | |
* | | -mtune=David Monniaux2020-10-222-1/+5
| | |
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-183-17/+22
|\| |
| * | Loop body unrolling with -funrollbody nCyril SIX2020-10-162-0/+3
| | |
| * | -O0 desactivates -fpredict and -ftracelinearizeCyril SIX2020-10-141-0/+1
| | |
| * | Updated --helpCyril SIX2020-10-141-9/+5
| | |
| * | new flags: -fpredict, -ftailduplicate n, -funrollsingle n instead of just ↵Cyril SIX2020-10-092-5/+10
| | | | | | | | | | | | -fduplicate n
| * | Changing duplicate verifier to be non optionalCyril SIX2020-10-091-3/+0
| | |
* | | command line selection of prepass schedulerDavid Monniaux2020-07-112-0/+4
| | |
* | | use a command-line optionDavid Monniaux2020-07-082-1/+4
| | |
* | | RTLpathSchedulerproof.all_fundef_liveness_ok is a hypothesis againCyril SIX2020-06-091-0/+2
| | |
* | | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-286-183/+103
|\| | | | | | | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
| * | k1c -> kvx changesDavid Monniaux2020-05-263-3/+3
| | |
| * | -fcse3-glbDavid Monniaux2020-05-063-0/+6
| | |
| * | CSE3 across mergesDavid Monniaux2020-05-063-0/+6
| | |
| * | Merge branch 'mppa-work' of ↵David Monniaux2020-04-234-152/+73
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| | * \ Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-233-4/+11
| | |\ \
| | | * | CSE3 across callsDavid Monniaux2020-04-233-3/+9
| | | | |
| | | * | Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licmDavid Monniaux2020-04-232-0/+2
| | | |\ \
| | | | * | make tracing output optionalDavid Monniaux2020-04-232-0/+2
| | | | | |
| | | | * | fix in CSE3 move propagationDavid Monniaux2020-04-231-20/+20
| | | | | |
| | | * | | use cbn not simplDavid Monniaux2020-04-221-21/+21
| | | | | |
| | * | | | cbn and copyrightDavid Monniaux2020-04-221-9/+9
| | | | | |
| | * | | | use cbn in T instead of simpl in TDavid Monniaux2020-04-221-1/+2
| | | | | |
| | * | | | automated writing Compiler.vDavid Monniaux2020-04-221-111/+8
| | | | | |
| | * | | | generate mkpassDavid Monniaux2020-04-211-18/+1
| | | | | |
| | * | | | Require autogenDavid Monniaux2020-04-211-34/+4
| | | | | |
generated by cgit (git 2.34.1) at 2024-05-20 04:19:41 +0000