Rbyd prune now working

This commit is contained in:
Christopher Haster
2022-12-26 23:14:36 -06:00
parent 471f12c79a
commit d9b419d36a
2 changed files with 143 additions and 166 deletions
+12 -35
View File
@@ -1470,42 +1470,19 @@ static int lfs_rbyd_commit(lfs_t *lfs, lfs_rbyd_t *rbyd,
jump = branch - jump;
lfs_rtag_t branch_ = branch + delta;
// // prune?
// printf("prune? %x >= %x (%x+%x+1)\n", lfs_rtag_weight(alt), lt+gt+1, lt, gt);
// if (lfs_rtag_weight(alt) >= lt+gt+1) {
// printf("prune!\n");
// LFS_ASSERT(p_alts[0]);
//
// branch = jump;
// branch_ = 0; // TODO is this needed?
// alt = lfs_rtag_black(p_alts[0]);
// jump = p_jumps[0];
// lfs_rbyd_p_pop(p_alts, p_jumps);
// }
// prune?
if (lfs_rtag_weight(alt) >= lt+gt+1) {
printf("prune!\n");
LFS_ASSERT(p_alts[0]);
alt = lfs_rtag_black(p_alts[0]);
branch_ = jump;
jump = p_jumps[0];
lfs_rbyd_p_pop(p_alts, p_jumps);
lfs_rtag_untrim(alt, &lt, &gt);
}
// // prune?
// // TODO ugh, just clean this up later
// if (p_alts[0]
// && lfs_rtag_isred(p_alts[0])
// && lfs_rtag_weight2(alt, p_alts[0]) >= lt+gt+1) {
// LFS_ASSERT(p_alts[0]);
//
// branch = jump;
// alt = lfs_rtag_black(p_alts[0]);
// jump = p_jumps[0];
// lfs_rbyd_p_pop(p_alts, p_jumps);
//
// } else if (lfs_rtag_weight(alt) >= lt+gt+1) {
// // TODO does this get hit?
// // TODO can we simplify these two?
// LFS_ASSERT(p_alts[0]);
//
// branch = jump;
// alt = lfs_rtag_black(p_alts[0]);
// jump = p_jumps[0];
// lfs_rbyd_p_pop(p_alts, p_jumps);
// }
//
// two reds makes a yellow, split?
if (p_alts[0]
&& lfs_rtag_isred(p_alts[0])
+131 -131
View File
@@ -1227,7 +1227,7 @@ code = '''
LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xcccccccc}, 4,
LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xdddddddd}, 4,
LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xeeeeeeee}, 4,
LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xeeeeeeee}, 4, NULL))))))) => 0;
LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
@@ -1261,7 +1261,7 @@ code = '''
LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xcccccccc}, 4,
LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xdddddddd}, 4,
LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xeeeeeeee}, 4,
LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xeeeeeeee}, 4, NULL))))))) => 0;
LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
@@ -1276,132 +1276,132 @@ code = '''
=> LFS_MKRTAG(GSTATE, 5, 0);
'''
#[cases.test_rbyd_sextifoliate]
#in = 'lfs.c'
#code = '''
# lfs_t lfs;
# lfs_init(&lfs, cfg) => 0;
#
# lfs_rbyd_t rbyd_init = {
# .block = 0,
# .trunk = 0,
# .noff = 0,
# .rev = 1,
# .crc = 0,
# .count = 0,
# .erased = true,
# };
# lfs_rbyd_t rbyd;
# lfs_off_t off;
# lfs_size_t size;
#
# // don't prune
# // <b
# // .----'|
# // <b <y |
# // .-'| .-------'| |
# // <y | | <r |
# // .-------'| | | .----' |
# // | <r | | | <y
# // | .----' | => | | .-------'|
# // | | <r | | | <r
# // | | .----'| | | | .----'|
# // | | | <b | | | | <b
# // | | | .-'| | | | | .-'|
# // 1 2 3 4 5 1 2 3 4 5 6
# rbyd = rbyd_init;
# lfs_bd_erase(&lfs, rbyd.block) => 0;
# lfs_rbyd_commit(&lfs, &rbyd,
# LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xaaaaaaaa}, 4,
# LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xbbbbbbbb}, 4,
# LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xcccccccc}, 4,
# LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xdddddddd}, 4,
# LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xeeeeeeee}, 4,
# LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
#
# lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 1, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 2, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 3, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 4, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 5, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 6, 0);
#
# // prune by taking a red alt
# // <b >b
# // .-'| .-'|
# // <y | | <r
# // .-------'| | .-----------|-'|
# // | <r | | | >b
# // | .----' | => | .--------|-'|
# // | | <r | | <r |
# // | | .----'| | | .----'| |
# // | | | <b | | | <b |
# // | | | .-'| | | | .-'| |
# // 1 3 4 5 6 1 3 4 5 6 2
# rbyd = rbyd_init;
# lfs_bd_erase(&lfs, rbyd.block) => 0;
# lfs_rbyd_commit(&lfs, &rbyd,
# LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xaaaaaaaa}, 4,
# LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xbbbbbbbb}, 4,
# LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xcccccccc}, 4,
# LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xdddddddd}, 4,
# LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xeeeeeeee}, 4,
# LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xeeeeeeee}, 4, NULL))))))) => 0;
#
# lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 1, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 2, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 3, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 4, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 5, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 6, 0);
#
# // prune by taking a yellow alt (this needs to prune during the rflip)
# // <b >b
# // .-'| .-'|
# // <y | | >r
# // .-------'| | .--------|-'|
# // | <r | | | >b
# // | .----' | => .--|--------|-'|
# // | | <r | | <r |
# // | | .----'| | | .----'| |
# // | | | <b | | | <b |
# // | | | .-'| | | | .-'| |
# // 2 3 4 5 6 2 3 4 5 6 1
# rbyd = rbyd_init;
# lfs_bd_erase(&lfs, rbyd.block) => 0;
# lfs_rbyd_commit(&lfs, &rbyd,
# LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xaaaaaaaa}, 4,
# LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xbbbbbbbb}, 4,
# LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xcccccccc}, 4,
# LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xdddddddd}, 4,
# LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xeeeeeeee}, 4,
# LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xeeeeeeee}, 4, NULL))))))) => 0;
#
# lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 1, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 2, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 3, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 4, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 5, 0);
# lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
# => LFS_MKRTAG(GSTATE, 6, 0);
#'''
[cases.test_rbyd_sextifoliate]
in = 'lfs.c'
code = '''
lfs_t lfs;
lfs_init(&lfs, cfg) => 0;
lfs_rbyd_t rbyd_init = {
.block = 0,
.trunk = 0,
.noff = 0,
.rev = 1,
.crc = 0,
.count = 0,
.erased = true,
};
lfs_rbyd_t rbyd;
lfs_off_t off;
lfs_size_t size;
// don't prune
// <b
// .----'|
// <b <y |
// .-'| .-------'| |
// <y | | <r |
// .-------'| | | .----' |
// | <r | | | <y
// | .----' | => | | .-------'|
// | | <r | | | <r
// | | .----'| | | | .----'|
// | | | <b | | | | <b
// | | | .-'| | | | | .-'|
// 1 2 3 4 5 1 2 3 4 5 6
rbyd = rbyd_init;
lfs_bd_erase(&lfs, rbyd.block) => 0;
lfs_rbyd_commit(&lfs, &rbyd,
LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xaaaaaaaa}, 4,
LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xbbbbbbbb}, 4,
LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xcccccccc}, 4,
LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xdddddddd}, 4,
LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xeeeeeeee}, 4,
LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 1, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 2, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 3, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 4, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 5, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 6, 0);
// prune by taking a red alt
// <b >b
// .-'| .-'|
// <y | | <r
// .-------'| | .-----------|-'|
// | <r | | | >b
// | .----' | => | .--------|-'|
// | | <r | | <r |
// | | .----'| | | .----'| |
// | | | <b | | | <b |
// | | | .-'| | | | .-'| |
// 1 3 4 5 6 1 3 4 5 6 2
rbyd = rbyd_init;
lfs_bd_erase(&lfs, rbyd.block) => 0;
lfs_rbyd_commit(&lfs, &rbyd,
LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xaaaaaaaa}, 4,
LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xbbbbbbbb}, 4,
LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xcccccccc}, 4,
LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xdddddddd}, 4,
LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xeeeeeeee}, 4,
LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 1, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 2, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 3, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 4, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 5, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 6, 0);
// prune by taking a yellow alt (this needs to prune during the rflip)
// <b >b
// .-'| .-'|
// <y | | >r
// .-------'| | .--------|-'|
// | <r | | | >b
// | .----' | => .--|--------|-'|
// | | <r | | <r |
// | | .----'| | | .----'| |
// | | | <b | | | <b |
// | | | .-'| | | | .-'| |
// 2 3 4 5 6 2 3 4 5 6 1
rbyd = rbyd_init;
lfs_bd_erase(&lfs, rbyd.block) => 0;
lfs_rbyd_commit(&lfs, &rbyd,
LFS_MKRATTR(GSTATE, 2, 0, &(uint32_t){0xaaaaaaaa}, 4,
LFS_MKRATTR(GSTATE, 3, 0, &(uint32_t){0xbbbbbbbb}, 4,
LFS_MKRATTR(GSTATE, 4, 0, &(uint32_t){0xcccccccc}, 4,
LFS_MKRATTR(GSTATE, 5, 0, &(uint32_t){0xdddddddd}, 4,
LFS_MKRATTR(GSTATE, 6, 0, &(uint32_t){0xeeeeeeee}, 4,
LFS_MKRATTR(GSTATE, 1, 0, &(uint32_t){0xffffffff}, 4, NULL))))))) => 0;
lfs_rbyd_fetch(&lfs, &rbyd, rbyd.block, NULL) => 0;
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 1, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 1, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 2, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 2, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 3, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 3, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 4, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 4, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 5, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 5, 0);
lfs_rbyd_lookup(&lfs, &rbyd, LFS_MKRTAG(GSTATE, 6, 0), &off, &size)
=> LFS_MKRTAG(GSTATE, 6, 0);
'''