Closed steinerkelvin closed 1 year ago
The problem:
A valid DP0
cell with color/label 0
pointing to memory position 0
has the numeric value 0x00000000000000000000000000000000
(zero), which is the same as an empty/cleared memory cell.
While fixing this bug by shifting all the cell tags by 2 [1], so we don't get any with value 0x00
, we stumbled in another one:
In the same collect
run, both DP0 and DP1 for the same dup-node can be collected. When each is collected, it's replaced by an Era, and an attempt to clear the dup-node itself is scheduled. Both do this scheduling as they can't be sure the dup-node can be cleaned, as the other side could no be erased. In the end of collect
those scheduled clear-ups are resolved:
for dup in dups {
let fst = ask_arg(rt, dup, 0);
let snd = ask_arg(rt, dup, 1);
if fst.get_tag() == CellTag::ERA && snd.get_tag() == CellTag::ERA {
collect(rt, ask_arg(rt, dup, 2));
clear(rt, dup.get_loc(0), 3);
}
}
When this happens, the second attempt to collect the same node will not find a valid node but zeroed cells. With the modification on [1], this triggers an "unknown cell tag panic". This didn't happen in the old code because a zeroed cell interpreted as a valid cell had the 0x00
tag, so it was considered a DP0, and the condition would fail.
[1]:
pub enum CellTag {
DP0 = 0x02,
DP1 = 0x03,
VAR = 0x04,
ARG = 0x05,
ERA = 0x06,
LAM = 0x07,
APP = 0x08,
SUP = 0x09,
CTR = 0x0A,
FUN = 0x0B,
OP2 = 0x0C,
NUM = 0x0D,
NIL = 0x0F,
}
This was fixed by using a HashSet
to store to-be-cleared dup_nodes instead of a Vec
. As this may introduce overhead, maybe we should test if the dup-node can be cleared directly at each DP0/1 clearance.
The code on https://pastebin.com/Rn90V9pE, run with
cargo run -- test file.kdl --sudo
fails withon the "Normalize" IO (function
Runtime::normalize
).It seems to be related with the following kdl function:
Current commit: 0efd48c