index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
scheduling
Commit message (
Expand
)
Author
Age
Files
Lines
*
Adding debug info
nicolas.nardino
2021-06-06
1
-42
/
+53
*
Fixing scope error, and non-exhaustive pattern matching
nicolas.nardino
2021-06-06
1
-5
/
+6
*
function written, now needs testing
nicolas.nardino
2021-06-05
1
-10
/
+40
*
computing live regs at sb entry from its live output regs
nicolas.nardino
2021-06-04
1
-3
/
+21
*
Passing info of live regs to scheduler: beginning
nicolas.nardino
2021-06-04
3
-1
/
+13
*
Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1
Cyril SIX
2021-06-01
7
-31
/
+24
|
\
|
*
Compatibilité Coq 8.13
David Monniaux
2021-04-28
3
-8
/
+3
|
*
Merge remote-tracking branch 'origin/manuscript' into kvx-work
submission_OOPSLA2021_AARCH64_KVX
Cyril SIX
2021-04-13
1
-14
/
+16
|
|
\
|
|
*
Code simplification of get_path_map (no functionality change)
Cyril SIX
2021-01-26
1
-14
/
+16
|
*
|
Remove flags
Léo Gourdin
2021-04-09
1
-3
/
+1
|
*
|
Important commit on expansions' mini CSE, and a draft for addptrofs
Léo Gourdin
2021-04-06
2
-5
/
+2
|
*
|
Remove first nop when doing expansion
Léo Gourdin
2021-03-21
1
-0
/
+1
|
*
|
Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp
Léo Gourdin
2021-03-06
2
-5
/
+5
|
|
\
\
|
|
*
|
Adding a mini CSE pass in the expansion oracle
Léo Gourdin
2021-03-06
2
-4
/
+5
|
*
|
|
Adding fp init expansions
Léo Gourdin
2021-03-02
1
-3
/
+3
|
*
|
|
[Admitted checker] Oracle expansion for float/float32 constant init
Léo Gourdin
2021-03-02
2
-4
/
+4
|
|
/
/
*
/
/
replacing omega with lia in some file
Léo Gourdin
2021-03-29
4
-39
/
+43
|
/
/
*
|
fix ci ?
Léo Gourdin
2021-03-02
1
-1
/
+1
*
|
Try to save values in virtual registers during expansion
Léo Gourdin
2021-03-01
1
-1
/
+1
*
|
Proofs finished for expansion
Léo Gourdin
2021-03-01
1
-22
/
+6
*
|
Debugging fake values finished
Léo Gourdin
2021-03-01
1
-10
/
+19
*
|
proof of fsval_proj_correct
Sylvain Boulmé
2021-03-01
1
-7
/
+27
*
|
Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work
Léo Gourdin
2021-03-01
1
-4
/
+4
|
\
\
|
*
|
bug fix ?
Sylvain Boulmé
2021-03-01
1
-4
/
+4
*
|
|
Proof of fsval condition cmp ok
Léo Gourdin
2021-03-01
1
-968
/
+18
*
|
|
[Admitted checker] Some more proof, version with buggy addirw0
Léo Gourdin
2021-02-25
1
-18
/
+2
*
|
|
some more proof for fake hsval checker expansions
Léo Gourdin
2021-02-25
1
-324
/
+1
*
|
|
[Intermediate] Adding fake hsval for Ccomp expansion
Léo Gourdin
2021-02-23
2
-164
/
+68
*
|
|
Fix imports
Léo Gourdin
2021-02-23
1
-1
/
+1
*
|
|
Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work
Léo Gourdin
2021-02-23
6
-79
/
+202
|
\
|
|
|
*
|
Merge branch 'riscv-work-rules' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...
Léo Gourdin
2021-02-23
1
-2
/
+52
|
|
\
\
|
|
*
|
add target_cbranch_expanse
Sylvain Boulmé
2021-02-23
1
-2
/
+52
|
*
|
|
Separate target_op_simplify for riscV
Léo Gourdin
2021-02-23
1
-19
/
+2
|
|
/
/
|
*
|
fix comments
Sylvain Boulmé
2021-02-23
1
-2
/
+5
|
*
|
starting an interface for target rewriting rules.
Sylvain Boulmé
2021-02-23
1
-9
/
+130
|
*
|
improved pre_output_regs
Sylvain Boulmé
2021-02-22
1
-5
/
+8
|
*
|
a bit more cleaning
Sylvain Boulmé
2021-02-22
5
-44
/
+21
|
*
|
quick fixcomments
Léo Gourdin
2021-02-16
1
-4
/
+1
*
|
|
others case for ccompimm
Léo Gourdin
2021-02-23
1
-53
/
+51
*
|
|
Some more proofs on branch expansion, using make_immed32_sound
Léo Gourdin
2021-02-23
1
-59
/
+221
*
|
|
Branch expansions activated and configured in the checker (but admitted) and ...
Léo Gourdin
2021-02-19
1
-49
/
+146
*
|
|
Proof of Ocmp expansions without immediate and some drafts in comment
Léo Gourdin
2021-02-18
1
-46
/
+471
*
|
|
Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work
Léo Gourdin
2021-02-16
9
-228
/
+405
|
\
|
|
|
*
|
This commit gives a first try to compute pre_output_regs from the livenesss o...
Léo Gourdin
2021-02-15
1
-10
/
+19
|
*
|
[Broken version] Some TODO eliminated
Léo Gourdin
2021-02-15
3
-153
/
+15
|
*
|
[Broken version] Proof of hsistate_simu_spec_correct
Léo Gourdin
2021-02-15
1
-7
/
+10
|
*
|
[Broken version] Intermediate local commit: pre_output_regs_correct proved
Léo Gourdin
2021-02-15
1
-17
/
+28
|
*
|
[Broken version] Intermediate local commit: proof of siexec_snone_por in sche...
Léo Gourdin
2021-02-12
2
-18
/
+68
|
*
|
[Broken version] Intermediate local commit: proof of inst_checker_eqlive OK
Léo Gourdin
2021-02-12
2
-54
/
+131
|
*
|
progress in pre_output_regs_correct
Sylvain Boulmé
2021-02-12
1
-5
/
+53
[next]