use super::ir::{LocalVarDecl, LocalVarId};
type Planes = (Vec<u64>, Vec<u64>);
fn mask_top(limbs: &mut [u64], width: u32) {
let rem = width % 64;
if rem != 0
&& let Some(top) = limbs.last_mut()
{
*top &= (1u64 << rem) - 1;
}
}
fn resize_plane(src: &[u64], from_width: u32, signed: bool, to_width: u32) -> Vec<u64> {
let to_n = (to_width as usize).div_ceil(64).max(1);
let mut out = src.to_vec();
out.resize(to_n.max(src.len()), 0);
let top = from_width - 1;
let sign_set = signed && src[(top / 64) as usize] >> (top % 64) & 1 == 1;
if sign_set {
let (limb, rem) = ((from_width / 64) as usize, from_width % 64);
let mut start = limb;
if rem != 0 {
out[limb] |= !0u64 << rem;
start += 1;
}
for w in &mut out[start..] {
*w = !0;
}
}
out.truncate(to_n);
mask_top(&mut out, to_width);
out
}
pub fn read_planes(frame: &[Option<i64>], at: LocalVarId, decl: &LocalVarDecl) -> Option<Planes> {
let h = at.0 as usize;
let first = frame.get(h).copied().flatten()?;
let n = decl.limbs();
let word = |i: usize| frame.get(h + i).copied().flatten().unwrap_or(0) as u64;
if !decl.is_wide() {
return Some((vec![first as u64], vec![0]));
}
Some((
(0..n).map(word).collect(),
(0..n).map(|j| word(n + j)).collect(),
))
}
fn write_planes(frame: &mut [Option<i64>], at: LocalVarId, decl: &LocalVarDecl, planes: &Planes) {
let (h, n) = (at.0 as usize, decl.limbs());
for j in 0..n {
frame[h + j] = Some(planes.0[j] as i64);
frame[h + n + j] = Some(planes.1[j] as i64);
}
}
fn narrow_planes(v: i64, decl: &LocalVarDecl) -> Planes {
let mut word = [v as u64];
mask_top(&mut word, decl.width);
(word.to_vec(), vec![0])
}
pub fn copy_local(
dst_frame: &mut [Option<i64>],
dst: LocalVarId,
dst_decl: &LocalVarDecl,
src_frame: &[Option<i64>],
src: LocalVarId,
src_decl: &LocalVarDecl,
) {
let d = dst.0 as usize;
if !src_decl.is_wide() && !dst_decl.is_wide() {
dst_frame[d] = src_frame[src.0 as usize].map(|v| dst_decl.cast(v));
return;
}
let Some((vals, unks)) = read_planes(src_frame, src, src_decl) else {
for slot in &mut dst_frame[d..d + dst_decl.slots()] {
*slot = None;
}
return;
};
let (vals, unks) = if src_decl.is_wide() {
(vals, unks)
} else {
narrow_planes(src_frame[src.0 as usize].unwrap_or(0), src_decl)
};
let (from, sg, to) = (src_decl.width, src_decl.signed, dst_decl.width);
if dst_decl.is_wide() {
let planes = (
resize_plane(&vals, from, sg, to),
resize_plane(&unks, from, sg, to),
);
write_planes(dst_frame, dst, dst_decl, &planes);
} else {
dst_frame[d] = Some(dst_decl.cast(vals[0] as i64));
}
}
pub fn step_local(
frame: &mut [Option<i64>],
var: LocalVarId,
decl: &LocalVarDecl,
delta: i64,
) -> Option<()> {
let (vals, unks) = read_planes(frame, var, decl)?;
let n = decl.limbs();
let planes = if unks.iter().any(|&u| u != 0) {
let mut all = vec![!0u64; n];
mask_top(&mut all, decl.width);
(vec![0; n], all)
} else {
let mut carry = false;
let mut out = Vec::with_capacity(n);
for (j, &v) in vals.iter().enumerate() {
let add = if j == 0 {
delta as u64
} else if delta < 0 {
!0
} else {
0
};
let (s, c1) = v.overflowing_add(add);
let (s, c2) = s.overflowing_add(u64::from(carry));
carry = c1 | c2;
out.push(s);
}
mask_top(&mut out, decl.width);
(out, vec![0; n])
};
write_planes(frame, var, decl, &planes);
Some(())
}
#[cfg(test)]
mod tests {
use super::*;
use crate::sva::ir::Automaton;
fn frame_with(a: &Automaton, var: LocalVarId, vals: &[u64], unks: &[u64]) -> Vec<Option<i64>> {
let mut f = vec![None; a.local_vars.len()];
let d = *a.local_var(var);
write_planes(&mut f, var, &d, &(vals.to_vec(), unks.to_vec()));
f
}
#[test]
fn a_wide_variable_gets_value_then_unknown_limb_slots() {
let mut a = Automaton::empty();
let n = a.new_local_var(8, false);
let w = a.new_local_var(130, true);
let m = a.new_local_var(64, false);
assert_eq!((n.0, w.0, m.0), (0, 1, 7), "130 bits = 3 limbs = 6 slots");
assert_eq!(a.local_vars.len(), 8);
let d = a.local_var(w);
assert_eq!((d.width, d.signed, d.limbs(), d.slots()), (130, true, 3, 6));
for k in 1..6 {
assert_eq!(
a.local_vars[1 + k],
LocalVarDecl {
width: 64,
signed: false
},
"limb slot {k} is a plain 64-bit slot"
);
}
}
#[test]
fn a_wide_copy_extends_by_the_sources_signedness() {
let mut a = Automaton::empty();
let s70 = a.new_local_var(70, true);
let u130 = a.new_local_var(130, false);
let s130 = a.new_local_var(130, true);
let n8 = a.new_local_var(8, true);
let mut f = frame_with(&a, s70, &[!0, 0x3f], &[0, 0]);
f.resize(a.local_vars.len(), None);
let (d70, d130, d8) = (*a.local_var(s70), *a.local_var(u130), *a.local_var(n8));
let src = f.clone();
copy_local(&mut f, u130, &d130, &src, s70, &d70);
let (v, u) = read_planes(&f, u130, &d130).unwrap();
assert_eq!(v, [!0, !0, 3], "a signed source sign-extends into 130 bits");
assert_eq!(u, [0, 0, 0]);
let mut b = Automaton::empty();
let us70 = b.new_local_var(70, false);
let ud130 = b.new_local_var(130, false);
let (dus, dud) = (*b.local_var(us70), *b.local_var(ud130));
let src = frame_with(&b, us70, &[!0, 0x3f], &[0, 0]);
let mut f2 = vec![None; b.local_vars.len()];
copy_local(&mut f2, ud130, &dud, &src, us70, &dus);
assert_eq!(read_planes(&f2, ud130, &dud).unwrap().0, [!0, 0x3f, 0]);
let src = f.clone();
copy_local(&mut f, n8, &d8, &src, s130, a.local_var(s130));
assert_eq!(f[n8.0 as usize], None, "an unassigned source stays so");
let src = f.clone();
copy_local(&mut f, n8, &d8, &src, u130, &d130);
assert_eq!(f[n8.0 as usize], Some(-1), "0xff in a signed 8-bit slot");
let mut g = vec![None; a.local_vars.len()];
g[n8.0 as usize] = Some(-2);
let src = g.clone();
copy_local(&mut g, s70, &d70, &src, n8, &d8);
assert_eq!(read_planes(&g, s70, &d70).unwrap().0, [!0 - 1, 0x3f]);
}
#[test]
fn an_unknown_sign_bit_extends_as_unknown() {
let mut a = Automaton::empty();
let s70 = a.new_local_var(70, true);
let w130 = a.new_local_var(130, false);
let f = frame_with(&a, s70, &[0, 0], &[0, 1 << 5]);
let (d70, d130) = (*a.local_var(s70), *a.local_var(w130));
let mut out = vec![None; a.local_vars.len()];
copy_local(&mut out, w130, &d130, &f, s70, &d70);
let (v, u) = read_planes(&out, w130, &d130).unwrap();
assert_eq!(v, [0, 0, 0]);
assert_eq!(u, [0, !0 << 5, 3], "bits 69..129 are x");
}
#[test]
fn a_step_carries_across_limbs_and_wraps_at_the_width() {
let mut a = Automaton::empty();
let w = a.new_local_var(130, false);
let d = *a.local_var(w);
let mut f = frame_with(&a, w, &[!0, !0, 3], &[0, 0, 0]);
step_local(&mut f, w, &d, 1).unwrap();
assert_eq!(read_planes(&f, w, &d).unwrap().0, [0, 0, 0], "wraps to 0");
step_local(&mut f, w, &d, -1).unwrap();
assert_eq!(read_planes(&f, w, &d).unwrap().0, [!0, !0, 3]);
let mut f = frame_with(&a, w, &[!0, 0, 0], &[0, 0, 0]);
step_local(&mut f, w, &d, 1).unwrap();
assert_eq!(read_planes(&f, w, &d).unwrap().0, [0, 1, 0], "carry");
let mut u = vec![None; a.local_vars.len()];
assert!(step_local(&mut u, w, &d, 1).is_none(), "unassigned");
}
#[test]
fn a_step_of_a_variable_with_an_unknown_bit_is_all_x() {
let mut a = Automaton::empty();
let w = a.new_local_var(70, false);
let d = *a.local_var(w);
let mut f = frame_with(&a, w, &[5, 0], &[0, 1]);
step_local(&mut f, w, &d, 1).unwrap();
let (v, u) = read_planes(&f, w, &d).unwrap();
assert_eq!((v, u), (vec![0, 0], vec![!0, 0x3f]));
}
}