Check 8-byte-chunk copy distance precondition
diff --git a/internal/cgen/base/io-private.h b/internal/cgen/base/io-private.h
index 11b6274..492d010 100644
--- a/internal/cgen/base/io-private.h
+++ b/internal/cgen/base/io-private.h
@@ -207,9 +207,9 @@
// stronger pre-conditions.
//
// The caller needs to prove that:
-// - distance > 0
-// - distance <= (*ptr_iop_w - io1_w)
// - length <= (io2_w - *ptr_iop_w)
+// - distance >= 1
+// - distance <= (*ptr_iop_w - io1_w)
static inline uint32_t //
wuffs_base__io_writer__limited_copy_u32_from_history_fast(uint8_t** ptr_iop_w,
uint8_t* io1_w,
@@ -242,9 +242,9 @@
// In terms of advancing *ptr_iop_w, length is not rounded up.
//
// The caller needs to prove that:
-// - distance > 0
-// - distance <= (*ptr_iop_w - io1_w)
// - (length + 8) <= (io2_w - *ptr_iop_w)
+// - distance >= 8
+// - distance <= (*ptr_iop_w - io1_w)
static inline uint32_t //
wuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast(
uint8_t** ptr_iop_w,
diff --git a/internal/cgen/data/data.go b/internal/cgen/data/data.go
index d3df782..a617b6b 100644
--- a/internal/cgen/data/data.go
+++ b/internal/cgen/data/data.go
@@ -213,8 +213,8 @@
"" +
"// --------\n\nstatic inline uint64_t //\nwuffs_base__io_writer__copy_from_slice(uint8_t** ptr_iop_w,\n uint8_t* io2_w,\n wuffs_base__slice_u8 src) {\n uint8_t* iop_w = *ptr_iop_w;\n size_t n = src.len;\n if (n > ((size_t)(io2_w - iop_w))) {\n n = (size_t)(io2_w - iop_w);\n }\n if (n > 0) {\n memmove(iop_w, src.ptr, n);\n *ptr_iop_w += n;\n }\n return (uint64_t)(n);\n}\n\nstatic inline void //\nwuffs_base__io_writer__limit(uint8_t** ptr_io2_w,\n uint8_t* iop_w,\n uint64_t limit) {\n if (((uint64_t)(*ptr_io2_w - iop_w)) > limit) {\n *ptr_io2_w = iop_w + limit;\n }\n}\n\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_history(uint8_t** ptr_iop_w,\n uint8_t* io1_w,\n uint8_t* io2_w,\n uint32_t length,\n " +
" uint32_t distance) {\n if (!distance) {\n return 0;\n }\n uint8_t* p = *ptr_iop_w;\n if ((size_t)(p - io1_w) < (size_t)(distance)) {\n return 0;\n }\n uint8_t* q = p - distance;\n size_t n = (size_t)(io2_w - p);\n if ((size_t)(length) > n) {\n length = (uint32_t)(n);\n } else {\n n = (size_t)(length);\n }\n // TODO: unrolling by 3 seems best for the std/deflate benchmarks, but that\n // is mostly because 3 is the minimum length for the deflate format. This\n // function implementation shouldn't overfit to that one format. Perhaps the\n // limited_copy_u32_from_history Wuffs method should also take an unroll hint\n // argument, and the cgen can look if that argument is the constant\n // expression '3'.\n //\n // See also wuffs_base__io_writer__limited_copy_u32_from_history_fast below.\n //\n // Alternatively or additionally, have a sloppy_limited_copy_u32_from_history\n // method that copies 8 bytes at a time, which can more than length bytes?\n for (; n >= 3; " +
- "n -= 3) {\n *p++ = *q++;\n *p++ = *q++;\n *p++ = *q++;\n }\n for (; n; n--) {\n *p++ = *q++;\n }\n *ptr_iop_w = p;\n return length;\n}\n\n// wuffs_base__io_writer__limited_copy_u32_from_history_fast is like the\n// wuffs_base__io_writer__limited_copy_u32_from_history function above, but has\n// stronger pre-conditions.\n//\n// The caller needs to prove that:\n// - distance > 0\n// - distance <= (*ptr_iop_w - io1_w)\n// - length <= (io2_w - *ptr_iop_w)\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_history_fast(uint8_t** ptr_iop_w,\n uint8_t* io1_w,\n uint8_t* io2_w,\n uint32_t length,\n uint32_t distance) {\n uint8_t* p = *ptr_iop_w;\n uint8_t* q = p - distance;\n uint32_t n = length;\n for (; n >= 3; n -= 3) {\n *p++ = *q++;\n *p++ = *q++;\n *p++ = " +
- "*q++;\n }\n for (; n; n--) {\n *p++ = *q++;\n }\n *ptr_iop_w = p;\n return length;\n}\n\n// wuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast is\n// like the wuffs_base__io_writer__limited_copy_u32_from_history_fast function\n// above, but copies 8 byte chunks at a time.\n//\n// In terms of number of bytes copied, length is rounded up to a multiple of 8.\n// As a special case, a zero length rounds up to 8 (even though 0 is already a\n// multiple of 8), since there is always at least one 8 byte chunk copied.\n//\n// In terms of advancing *ptr_iop_w, length is not rounded up.\n//\n// The caller needs to prove that:\n// - distance > 0\n// - distance <= (*ptr_iop_w - io1_w)\n// - (length + 8) <= (io2_w - *ptr_iop_w)\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast(\n uint8_t** ptr_iop_w,\n uint8_t* io1_w,\n uint8_t* io2_w,\n uint32_t length,\n uint32_t distance) {\n uint8_t* p = *ptr_iop_w;\n uint8_t* q = p - distance;\n uint32_t" +
+ "n -= 3) {\n *p++ = *q++;\n *p++ = *q++;\n *p++ = *q++;\n }\n for (; n; n--) {\n *p++ = *q++;\n }\n *ptr_iop_w = p;\n return length;\n}\n\n// wuffs_base__io_writer__limited_copy_u32_from_history_fast is like the\n// wuffs_base__io_writer__limited_copy_u32_from_history function above, but has\n// stronger pre-conditions.\n//\n// The caller needs to prove that:\n// - length <= (io2_w - *ptr_iop_w)\n// - distance >= 1\n// - distance <= (*ptr_iop_w - io1_w)\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_history_fast(uint8_t** ptr_iop_w,\n uint8_t* io1_w,\n uint8_t* io2_w,\n uint32_t length,\n uint32_t distance) {\n uint8_t* p = *ptr_iop_w;\n uint8_t* q = p - distance;\n uint32_t n = length;\n for (; n >= 3; n -= 3) {\n *p++ = *q++;\n *p++ = *q++;\n *p++ = " +
+ "*q++;\n }\n for (; n; n--) {\n *p++ = *q++;\n }\n *ptr_iop_w = p;\n return length;\n}\n\n// wuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast is\n// like the wuffs_base__io_writer__limited_copy_u32_from_history_fast function\n// above, but copies 8 byte chunks at a time.\n//\n// In terms of number of bytes copied, length is rounded up to a multiple of 8.\n// As a special case, a zero length rounds up to 8 (even though 0 is already a\n// multiple of 8), since there is always at least one 8 byte chunk copied.\n//\n// In terms of advancing *ptr_iop_w, length is not rounded up.\n//\n// The caller needs to prove that:\n// - (length + 8) <= (io2_w - *ptr_iop_w)\n// - distance >= 8\n// - distance <= (*ptr_iop_w - io1_w)\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast(\n uint8_t** ptr_iop_w,\n uint8_t* io1_w,\n uint8_t* io2_w,\n uint32_t length,\n uint32_t distance) {\n uint8_t* p = *ptr_iop_w;\n uint8_t* q = p - distance;\n uint32_t" +
" n = length;\n while (1) {\n memcpy(p, q, 8);\n if (n <= 8) {\n p += n;\n break;\n }\n p += 8;\n q += 8;\n n -= 8;\n }\n *ptr_iop_w = p;\n return length;\n}\n\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_reader(uint8_t** ptr_iop_w,\n uint8_t* io2_w,\n uint32_t length,\n const uint8_t** ptr_iop_r,\n const uint8_t* io2_r) {\n uint8_t* iop_w = *ptr_iop_w;\n size_t n = length;\n if (n > ((size_t)(io2_w - iop_w))) {\n n = (size_t)(io2_w - iop_w);\n }\n const uint8_t* iop_r = *ptr_iop_r;\n if (n > ((size_t)(io2_r - iop_r))) {\n n = (size_t)(io2_r - iop_r);\n }\n if (n > 0) {\n memmove(iop_w, iop_r, n);\n *ptr_iop_w += n;\n *ptr_iop_r += n;\n }\n return (uint32_t)(n);\n}\n\nstatic inline uint32_t //\nwuffs_base__io_writer__limited_copy_u32_from_slice(uint8_t** ptr_iop_" +
"w,\n uint8_t* io2_w,\n uint32_t length,\n wuffs_base__slice_u8 src) {\n uint8_t* iop_w = *ptr_iop_w;\n size_t n = src.len;\n if (n > length) {\n n = length;\n }\n if (n > ((size_t)(io2_w - iop_w))) {\n n = (size_t)(io2_w - iop_w);\n }\n if (n > 0) {\n memmove(iop_w, src.ptr, n);\n *ptr_iop_w += n;\n }\n return (uint32_t)(n);\n}\n\nstatic inline wuffs_base__io_buffer* //\nwuffs_base__io_writer__set(wuffs_base__io_buffer* b,\n uint8_t** ptr_iop_w,\n uint8_t** ptr_io0_w,\n uint8_t** ptr_io1_w,\n uint8_t** ptr_io2_w,\n wuffs_base__slice_u8 data) {\n b->data = data;\n b->meta.wi = 0;\n b->meta.ri = 0;\n b->meta.pos = 0;\n b->meta.closed = false;\n\n *ptr_iop_w = data.ptr;\n *ptr_io0_w = data.ptr;\n *ptr_io1_w = data.ptr;\n *ptr_io2_w = data.pt" +
"r + data.len;\n\n return b;\n}\n\n" +
diff --git a/lang/builtin/builtin.go b/lang/builtin/builtin.go
index ef4a241..4bc325b 100644
--- a/lang/builtin/builtin.go
+++ b/lang/builtin/builtin.go
@@ -537,14 +537,14 @@
// TODO: this should have explicit pre-conditions:
// - up_to <= this.length()
- // - distance > 0
+ // - distance >= 1
// - distance <= this.history_length()
// For now, that's all implicitly checked (i.e. hard coded).
"io_writer.limited_copy_u32_from_history_fast!(up_to: u32, distance: u32) u32",
// TODO: this should have explicit pre-conditions:
// - (up_to + 8) <= this.length()
- // - distance > 0
+ // - distance >= 8
// - distance <= this.history_length()
// For now, that's all implicitly checked (i.e. hard coded).
"io_writer.limited_copy_u32_from_history_8_byte_chunks_fast!(up_to: u32, distance: u32) u32",
diff --git a/lang/check/bounds.go b/lang/check/bounds.go
index 2fa3044..46815e7 100644
--- a/lang/check/bounds.go
+++ b/lang/check/bounds.go
@@ -1168,12 +1168,12 @@
}
} else if method == t.IDLimitedCopyU32FromHistory8ByteChunksFast {
- if err := q.canLimitedCopyU32FromHistoryFast(recv, n.Args(), eight); err != nil {
+ if err := q.canLimitedCopyU32FromHistoryFast(recv, n.Args(), eight, eight); err != nil {
return bounds{}, err
}
} else if method == t.IDLimitedCopyU32FromHistoryFast {
- if err := q.canLimitedCopyU32FromHistoryFast(recv, n.Args(), nil); err != nil {
+ if err := q.canLimitedCopyU32FromHistoryFast(recv, n.Args(), nil, one); err != nil {
return bounds{}, err
}
@@ -1286,10 +1286,10 @@
return fmt.Errorf("check: could not prove %s.can_undo_byte()", recv.Str(q.tm))
}
-func (q *checker) canLimitedCopyU32FromHistoryFast(recv *a.Expr, args []*a.Node, adj *big.Int) error {
+func (q *checker) canLimitedCopyU32FromHistoryFast(recv *a.Expr, args []*a.Node, adj *big.Int, minDistance *big.Int) error {
// As per cgen's io-private.h, there are three pre-conditions:
// - (upTo + adj) <= this.length()
- // - distance > 0
+ // - distance >= minDistance
// - distance <= this.history_length()
//
// adj may be nil, in which case (upTo + adj) is just upTo.
@@ -1348,22 +1348,22 @@
upTo.Str(q.tm), adj, recv.Str(q.tm))
}
- // Check "distance > 0".
+ // Check "distance >= minDistance".
check1:
for {
for _, x := range q.facts {
- if x.Operator() != t.IDXBinaryGreaterThan {
+ if x.Operator() != t.IDXBinaryGreaterEq {
continue
}
if lhs := x.LHS().AsExpr(); !lhs.Eq(distance) {
continue
}
- if rcv := x.RHS().AsExpr().ConstValue(); rcv == nil || rcv.Sign() != 0 {
+ if rcv := x.RHS().AsExpr().ConstValue(); (rcv == nil) || (rcv.Cmp(minDistance) < 0) {
continue
}
break check1
}
- return fmt.Errorf("check: could not prove %s > 0", distance.Str(q.tm))
+ return fmt.Errorf("check: could not prove %s >= %v", distance.Str(q.tm), minDistance)
}
// Check "distance <= this.history_length()".
diff --git a/release/c/wuffs-unsupported-snapshot.c b/release/c/wuffs-unsupported-snapshot.c
index d12ea43..604f212 100644
--- a/release/c/wuffs-unsupported-snapshot.c
+++ b/release/c/wuffs-unsupported-snapshot.c
@@ -10191,9 +10191,9 @@
// stronger pre-conditions.
//
// The caller needs to prove that:
-// - distance > 0
-// - distance <= (*ptr_iop_w - io1_w)
// - length <= (io2_w - *ptr_iop_w)
+// - distance >= 1
+// - distance <= (*ptr_iop_w - io1_w)
static inline uint32_t //
wuffs_base__io_writer__limited_copy_u32_from_history_fast(uint8_t** ptr_iop_w,
uint8_t* io1_w,
@@ -10226,9 +10226,9 @@
// In terms of advancing *ptr_iop_w, length is not rounded up.
//
// The caller needs to prove that:
-// - distance > 0
-// - distance <= (*ptr_iop_w - io1_w)
// - (length + 8) <= (io2_w - *ptr_iop_w)
+// - distance >= 8
+// - distance <= (*ptr_iop_w - io1_w)
static inline uint32_t //
wuffs_base__io_writer__limited_copy_u32_from_history_8_byte_chunks_fast(
uint8_t** ptr_iop_w,
diff --git a/std/deflate/decode_huffman_fast32.wuffs b/std/deflate/decode_huffman_fast32.wuffs
index 75c229e..543b074 100644
--- a/std/deflate/decode_huffman_fast32.wuffs
+++ b/std/deflate/decode_huffman_fast32.wuffs
@@ -341,7 +341,7 @@
}
}
// Once again, redundant but explicit assertions.
- assert (dist_minus_1 + 1) > 0
+ assert (dist_minus_1 + 1) >= 1
assert ((dist_minus_1 + 1) as base.u64) <= args.dst.history_length()
assert (length as base.u64) <= args.dst.length()
assert ((length + 8) as base.u64) <= args.dst.length()
diff --git a/std/deflate/decode_huffman_fast64.wuffs b/std/deflate/decode_huffman_fast64.wuffs
index 9e0e8e2..55e72dc 100644
--- a/std/deflate/decode_huffman_fast64.wuffs
+++ b/std/deflate/decode_huffman_fast64.wuffs
@@ -233,7 +233,7 @@
}
}
// Once again, redundant but explicit assertions.
- assert (dist_minus_1 + 1) > 0
+ assert (dist_minus_1 + 1) >= 1
assert ((dist_minus_1 + 1) as base.u64) <= args.dst.history_length()
assert (length as base.u64) <= args.dst.length()
assert ((length + 8) as base.u64) <= args.dst.length()
