Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 6 | -8/+24 |
| | |||||
* | redundant tests | David Monniaux | 2020-12-09 | 1 | -0/+11 |
| | |||||
* | CSE3 + conditions proof | David Monniaux | 2020-12-09 | 2 | -34/+58 |
| | |||||
* | apply_cond_sound | David Monniaux | 2020-12-09 | 1 | -0/+14 |
| | |||||
* | apply_cond0_sound | David Monniaux | 2020-12-09 | 1 | -1/+25 |
| | |||||
* | apply_cond1_sound | David Monniaux | 2020-12-09 | 1 | -0/+30 |
| | |||||
* | proof for jumptable | David Monniaux | 2020-12-09 | 1 | -1/+27 |
| | |||||
* | one 'admit' less | David Monniaux | 2020-12-09 | 1 | -2/+36 |
| | |||||
* | avancement dans les preuves | David Monniaux | 2020-12-09 | 1 | -1/+34 |
| | |||||
* | CSE3 compiles again, but some admitted lemmas | David Monniaux | 2020-12-09 | 2 | -11/+9 |
| | |||||
* | progress moving to list of items | David Monniaux | 2020-12-09 | 3 | -92/+233 |
| | |||||
* | CSE3 with Abst_same | David Monniaux | 2020-12-08 | 1 | -1/+1 |
| | |||||
* | analysis with Abst_same | David Monniaux | 2020-12-08 | 3 | -22/+39 |
| | |||||
* | CSE3 now runs on its own fixpoint iterator not based on Kildall.v | David Monniaux | 2020-12-08 | 3 | -115/+4 |
| | |||||
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 4 | -555/+242 |
|\ | |||||
| * | fix new register erasing scheme for AArch64 | David Monniaux | 2020-12-08 | 3 | -553/+241 |
| | | |||||
| * | rm instructions now unused | David Monniaux | 2020-12-08 | 1 | -2/+1 |
| | | |||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 157 | -2244/+4035 |
|\| | |||||
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixed | David Monniaux | 2020-12-08 | 18 | -115/+48 |
| |\ | |||||
| | * | Error when using -main without -interp | Xavier Leroy | 2020-12-06 | 1 | -0/+2 |
| | | | | | | | | | | | | | | | | | | Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option. | ||||
| | * | PowerPC modeling of registers destroyed by pseudo-instructions | Xavier Leroy | 2020-12-06 | 2 | -4/+6 |
| | | | | | | | | | | | | Inlined built-in functions destroy GPR0 | ||||
| | * | ARM modeling of registers destroyed by pseudo-instructions | Xavier Leroy | 2020-12-06 | 2 | -4/+6 |
| | | | | | | | | | | | | | | | Pflid destroys IR14 Inlined built-in functions destroy IR14 | ||||
| | * | AArch64 modeling of registers destroyed by pseudo-instructions | Xavier Leroy | 2020-12-06 | 2 | -8/+11 |
| | | | | | | | | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30 | ||||
| | * | Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions | Xavier Leroy | 2020-12-06 | 12 | -99/+23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v. | ||||
| * | | Fixing test/regression for KVXv3.8_kvx | Cyril SIX | 2020-12-07 | 6 | -2/+409 |
| | | | |||||
| * | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 104 | -1053/+11993 |
| |\ \ | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | ||||
| | * | | Comment | Cyril SIX | 2020-12-04 | 1 | -0/+1 |
| | | | | |||||
| | * | | Less aggressive tail duplication | Cyril SIX | 2020-12-04 | 1 | -6/+11 |
| | | | | | | | | | | | | | | | | | | | | In some cases of two imbricated loops, we would tail-duplicate too much, because of the input trace traversing both loop headers. | ||||
| | * | | Clean-up debug | Cyril SIX | 2020-12-04 | 1 | -4/+2 |
| | | | | |||||
| | * | | Fixed infinite loop on find_last_node_before_loop | Cyril SIX | 2020-12-04 | 1 | -3/+6 |
| | | | | | | | | | | | | | | | | Happened when a loop was predicted not to be taken | ||||
| | * | | Slight perf improvement | Cyril SIX | 2020-12-02 | 2 | -4/+4 |
| | | | | |||||
| | * | | [expensive] Behavior change when the loop has two final instructions | Cyril SIX | 2020-12-02 | 1 | -9/+57 |
| | | | | | | | | | | | | | | | | | | | | Right now though the compilation time is too high for glpk, I need to figure out why | ||||
| | * | | Duplicateaux: Generalization of look_ahead | Cyril SIX | 2020-12-01 | 1 | -3/+5 |
| | | | | |||||
| * | | | Fixing compilation for KVX | Cyril SIX | 2020-12-04 | 3 | -2/+7 |
| | | | | |||||
| * | | | still issues with FR in kvx | David Monniaux | 2020-12-03 | 3 | -27/+26 |
| | | | | |||||
| * | | | some fixes for KVX | David Monniaux | 2020-12-03 | 2 | -6/+0 |
| | | | | |||||
| * | | | fix Makefile pour kvx | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
| * | | | un peu de progrès sur le Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
| * | | | Asmgenproof1 pas sur kvx | David Monniaux | 2020-11-19 | 1 | -1/+5 |
| | | | | |||||
| * | | | essai de limitation des paquets Kalray | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
| * | | | rm unneeded open statements in ML | David Monniaux | 2020-11-19 | 1 | -3/+0 |
| | | | | |||||
| * | | | fix Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
| * | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 133 | -2071/+3462 |
| |\ \ \ | | | |/ | | |/| | |||||
| | * | | Updates for release 3.8v3.8 | Xavier Leroy | 2020-11-16 | 3 | -5/+10 |
| | | | | |||||
| | * | | Do not use -warn-error when building from a release tarball | Xavier Leroy | 2020-11-14 | 1 | -2/+9 |
| | | | | | | | | | | | | | | | | | | | | Stopping on warnings is useful for development builds, but unhelpful for released software. | ||||
| | * | | Support Coq 8.12.1 | Xavier Leroy | 2020-11-14 | 2 | -3/+3 |
| | | | | |||||
| | * | | Update README | Xavier Leroy | 2020-11-09 | 1 | -4/+4 |
| | | | | |||||
| | * | | Update Changes | Xavier Leroy | 2020-11-08 | 1 | -0/+48 |
| | | | | |||||
| | * | | Added semantics for the PowerPC sel and mulh built-ins | Bernhard Schommer | 2020-11-07 | 1 | -4/+44 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035 | ||||
| | * | | Added missing printer for PowerPC 64 bit comparison. | Bernhard Schommer | 2020-11-06 | 1 | -0/+8 |
| | | | | | | | | | | | | | | | | | | | | These comparisons are supported in the hybrid 64 bit mode. Bug 30035 |