Now that my application works, I’m trying to remove some dynamic checks to
static checks and so I’m looking for a way to do it. The goal is faster
code, and prevention of code errors in maintenance if some new person plays
with it.
The code basically accepts a 127 byte frame, where the first byte is size,
and the last byte is a CRC. For now, ignore that the first byte can be
bigger than 127, as a 1 in the left most bit has a special meaning we can
ignore for discussion.
The code below reads one frame from the USB. There are three functions that
effectively ensure the values are nats within the size, so that the
constraints in the code are satisfied.
The problem is these can’t prevent a bug. If I call loop with a value too
big, it will just clamp it and run. That will prevent a memory problem, but
not an error.
The question boils down to something like how to get the compiler to see
something like:
n7m2(!packetInCount - TWO)
and know that because it is TWO smaller, it satisfies the constraint of the
array.
Is there a way to define constraints in such a way it can make this check?
macdef packetIn =
$extval(arrayref(uint8, 127),“packetIn”)
macdef packetInCount =
$extval(ref(uint8),“packetInCount”)
macdef packetInHeader =
$extval(ref(uint8),“packetInHeader”)
extern fun{} n7 (x: uint8): natLte(127)
implement{} n7 (x) = cast{natLte(127)}(x land u8(0x7F))
extern fun{} n7m1 (x: uint8): natLte(126)
implement{} n7m1 (x) = if x > u8(126) then cast{natLte(126)}(126) else
cast{natLte(126)}(x)
extern fun{} n7m2 (x: uint8): natLte(125)
implement{} n7m2 (x) = if x > u8(125) then cast{natLte(125)}(125) else
cast{natLte(125)}(x)
fun read_frame(): bool = let
val () = !packetInCount := serial_poll_for_byte() // Discarded the
multi-frame bit
val ok = if !packetInCount >= THREE // Three is the minimum packet size
other than zero.
then let
fun loop {n: nat | n <= 125} .. (cnt: int(n), cksum:
uint8): uint8 =
if cnt > 0
then let
val byte = serial_poll_for_byte()
val () = packetIn[n7m2(!packetInCount - u8(cnt) - ONE)]
:= byte
in loop (cnt - 1, pec_add(cksum, byte)) end
else cksum
val cksum = loop (n7m2(!packetInCount - TWO), pec_add(ZERO,
!packetInCount))
val packetInChecksum = serial_poll_for_byte()
val () = packetIn[n7m1(!packetInCount - ONE)] :=
packetInChecksum
in cksum = packetInChecksum end
else false
in
ok
end
