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
/
backend
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer...
David Monniaux
2021-01-07
4
-92
/
+13
|
\
|
*
Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231
Cyril SIX
2021-01-06
2
-3
/
+2
|
*
Solving a stack overflow issue (was failing in yarpgen ran000089 for armhf)
Cyril SIX
2021-01-06
1
-9
/
+9
|
*
Uniformizing a couple of debug print functions
Cyril SIX
2020-12-17
2
-80
/
+2
*
|
-fcse3-trivial-ops
David Monniaux
2021-01-07
2
-3
/
+4
|
/
*
Fixing wrong predictions on imbricated loops
Cyril SIX
2020-12-11
1
-104
/
+114
*
Fixing exponential blowup on get_loop_info.mark_path.explore
Cyril SIX
2020-12-09
1
-33
/
+44
*
Flushing debug output
Cyril SIX
2020-12-09
1
-1
/
+1
*
The last fix for get_loop_info was giving false positives. Fixing that.
Cyril SIX
2020-12-08
1
-2
/
+12
*
Fixing get_loop_info : part 2
Cyril SIX
2020-12-08
1
-8
/
+28
*
Fixing loop detection in get_loop_info - part 1
Cyril SIX
2020-12-08
1
-16
/
+8
*
Moving code
Cyril SIX
2020-12-08
1
-71
/
+72
*
More debug
Cyril SIX
2020-12-08
1
-6
/
+21
*
More debug
Cyril SIX
2020-12-08
1
-3
/
+3
*
Do not duplicate nodes that don't need to when unrolling the body
Cyril SIX
2020-12-08
1
-4
/
+18
*
Fix on find_last_node_before_loop
Cyril SIX
2020-12-08
1
-3
/
+7
*
Merge branch 'kvx-work' into kvx-work-merge3.8
Cyril SIX
2020-12-04
11
-286
/
+1393
|
\
|
*
Comment
Cyril SIX
2020-12-04
1
-0
/
+1
|
*
Less aggressive tail duplication
Cyril SIX
2020-12-04
1
-6
/
+11
|
*
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
|
*
Slight perf improvement
Cyril SIX
2020-12-02
1
-2
/
+2
|
*
[expensive] Behavior change when the loop has two final instructions
Cyril SIX
2020-12-02
1
-9
/
+57
|
*
Duplicateaux: Generalization of look_ahead
Cyril SIX
2020-12-01
1
-3
/
+5
|
*
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
Cyril SIX
2020-12-01
3
-8
/
+161
|
|
\
|
|
*
store2_sound
David Monniaux
2020-11-25
1
-1
/
+1
|
|
*
clever_kill_store_sound
David Monniaux
2020-11-25
1
-7
/
+5
|
|
*
kill_store_sound
David Monniaux
2020-11-25
1
-0
/
+49
|
|
*
two lemmas admitted
David Monniaux
2020-11-25
3
-9
/
+115
|
*
|
Ignore loopback edges on tail-duplicate
Cyril SIX
2020-12-01
1
-0
/
+2
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-24
1
-2
/
+2
|
|
\
|
|
|
*
tiny simplification in Tunnelingaux.ml
Sylvain Boulmé
2020-11-24
1
-2
/
+2
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-19
4
-257
/
+672
|
|
\
|
|
|
*
minor fix in coq2html comment
Sylvain Boulmé
2020-11-16
1
-1
/
+2
|
|
*
Tunneling: improved elimination of conditions
Sylvain Boulmé
2020-11-16
4
-256
/
+670
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-06
2
-27
/
+32
|
|
\
|
|
*
|
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-05
3
-28
/
+109
|
|
\
\
|
*
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-04
1
-1
/
+2
|
|
\
\
\
|
*
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-11-03
4
-35
/
+114
|
|
\
\
\
\
|
*
\
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-31
3
-17
/
+118
|
|
\
\
\
\
\
|
*
\
\
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-30
4
-168
/
+78
|
|
\
\
\
\
\
\
|
*
\
\
\
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-29
4
-48
/
+107
|
|
\
\
\
\
\
\
\
|
*
\
\
\
\
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-28
3
-40
/
+24
|
|
\
\
\
\
\
\
\
\
|
*
\
\
\
\
\
\
\
\
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
David Monniaux
2020-10-27
4
-19
/
+110
|
|
\
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
|
|
improved CSE3
David Monniaux
2020-10-27
1
-12
/
+12
|
*
|
|
|
|
|
|
|
|
|
progress in proofs on new CSE3
David Monniaux
2020-10-27
1
-3
/
+34
|
*
|
|
|
|
|
|
|
|
|
deactivate LICM by default
David Monniaux
2020-10-27
1
-20
/
+11
|
*
|
|
|
|
|
|
|
|
|
begin fixing CSE3 to keep more inductive stuff
David Monniaux
2020-10-27
2
-10
/
+19
|
*
|
|
|
|
|
|
|
|
|
invariant printing more aligned with RTL dumps
David Monniaux
2020-10-27
1
-2
/
+2
|
*
|
|
|
|
|
|
|
|
|
print invariants
David Monniaux
2020-10-27
1
-11
/
+46
[next]