aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Collapse)AuthorAgeFilesLines
* Avancement PostpassSchedulingproofCyril SIX2019-01-251-5/+69
|
* Progrès dans PostpassSchedulingproofCyril SIX2019-01-251-6/+46
|
* Un peu d'avancement sur PostpassSchedulingproofCyril SIX2019-01-241-9/+27
|
* Cleaning dans PostpassSchedulingproofCyril SIX2019-01-231-43/+20
|
* 3ème cas de transf_step_correct de PostpassSchedulingproof finiCyril SIX2019-01-231-5/+6
|
* Proof of builtin case for transf_step_correct in PostpassSchedulingproofCyril SIX2019-01-231-1/+25
|
* Adding a predicate that a builtin must be alone in its basicblockCyril SIX2019-01-233-88/+168
|
* Changement de modèle de preuve pour le 1er cas du tranf_step_correct de ↵Cyril SIX2019-01-231-14/+47
| | | | PostpassSchedulingproof
* Léger avancement PostpassSchedulingproof.vCyril SIX2019-01-221-1/+7
|
* Added sxwd and zxwd supportCyril SIX2019-01-227-36/+30
|
* Un poil d'avancement sur PostpassSchedulingproof.v. Corrections à faire sur ↵Cyril SIX2019-01-211-1/+47
| | | | le modèle
* fix bug when using reoptimization (sat4j)David Monniaux2019-01-181-9/+13
|
* -O0 will not perform postpass schedulingCyril SIX2019-01-181-1/+1
|
* Minor bug in encode_immCyril SIX2019-01-181-2/+2
|
* Minor bug fixesCyril SIX2019-01-171-2/+2
|
* Ommited a ;; in va_arg_start macroCyril SIX2019-01-171-0/+1
|
* Corrected a bug in Pallocframe expansion with va_argsCyril SIX2019-01-172-3/+7
|
* Merge correctionsCyril SIX2019-01-172-74/+75
|
* Merge branch 'mppa_k1c' into mppa_postpassCyril SIX2019-01-174-79/+80
|\
| * Added an error message for 32-bits division and moduloCyril SIX2018-12-111-13/+13
| |
| * Fixed div64 and mod64Cyril SIX2018-12-111-0/+1
| |
| * Fixed that fnegd and negd had been invertedCyril SIX2018-12-071-1/+1
| |
| * Fixed bundles (back to 1 instruction per bundle)Cyril SIX2018-12-071-65/+65
| |
* | Corrected a bug in PostlassSchedulingOracle:intlist provoking cyclesCyril SIX2019-01-171-1/+1
| |
* | Added the rest of the instructions info (manually)Cyril SIX2019-01-161-47/+160
| |
* | More instruction definitions in the oracleCyril SIX2019-01-162-12/+36
| |
* | Debugged latency generation. We are able to produce bundlesCyril SIX2019-01-151-23/+78
| |
* | Pfreeframe and Pallocframe raise "OpaqueInstruction". Splitting bb to ↵Cyril SIX2019-01-151-18/+55
| | | | | | | | isolate opaque instructions
* | Added RA as possible location + control flow infoCyril SIX2019-01-111-6/+12
| |
* | Adding Mem as a possible location for accessesCyril SIX2019-01-111-23/+31
| |
* | Merge branch 'unittest' of ↵Cyril SIX2019-01-111-2/+3
|\ \ | | | | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into unittest Conflicts: mppa_k1c/PostpassSchedulingOracle.ml
| * | flush stdoutSylvain Boulmé2019-01-111-0/+1
| | |
| * | quick and dirty Makefile fixesSylvain Boulmé2019-01-111-2/+3
| | |
* | | Replaced the faulty bundlize_solution functionCyril SIX2019-01-111-28/+43
|/ /
* | [BROKEN] trying to link the test in mppa_k1c/unittest/postpass_testCyril SIX2019-01-114-35/+43
| |
* | [BROKEN] Added infos about sd, infinite loop somewhereCyril SIX2019-01-091-5/+23
| |
* | Adding more Asmblock instructions to PostpassSchedulingOracleCyril SIX2019-01-081-14/+108
| |
* | Raccordement de InstructionScheduler.ml à PostpassSchedulingOracle.mlCyril SIX2019-01-081-4/+94
| |
* | Latency constraints building done in PostpassSchedulingOracle.mlCyril SIX2019-01-081-16/+28
| |
* | Reorganized PostpassOracle to separate asmblock instructions from real ↵Cyril SIX2019-01-081-72/+111
| | | | | | | | instructions
* | Fixed warnings in InstructionSchedulerCyril SIX2019-01-082-21/+24
| |
* | Finished the immediate recognition part, started latency constraintsCyril SIX2019-01-071-19/+78
| |
* | [BROKEN] Début d'oracleCyril SIX2018-12-203-1/+1068
| |
* | Added a simple postpass oracle that splits a bblock into single instruction ↵Cyril SIX2018-12-175-4/+32
| | | | | | | | bundles
* | Generalizing PostpassScheduling to include bblock splittingCyril SIX2018-12-053-41/+98
| |
* | Moving size_blocks from Asmblockgen to AsmblockCyril SIX2018-12-052-9/+8
| |
* | Renaming PostpassSchedulingProof -> PostpassSchedulingproofCyril SIX2018-12-051-0/+0
| |
* | Added definitions and proof sketch for PostpassSchedulingCyril SIX2018-12-042-40/+110
| |
* | Tout début de développement d'un postpass Asmblock en CoqCyril SIX2018-12-032-0/+135
|/
* Introducing ;; as Pcomma in Asm.vCyril SIX2018-12-032-65/+67
|
generated by cgit (git 2.34.1) at 2024-07-06 16:41:51 +0000