Igalia / pflua

Packet filtering in Lua
Other
313 stars 39 forks source link

Range-checking off-by-one error. #120

Closed kbara closed 9 years ago

kbara commented 9 years ago
% ../tools/pflua-quickcheck --seed=150860333 --iterations=488 properties/opt_eq_unopt data/wingolog.pcap
The property was falsified.
--- Expanded:
{ "if",
  { "!=",
    "len",
    0 },
  { ">",
    1,
    { "uint32",
      { "+",
        { "uint32",
          { "-",
            4294967295,
            { "uint32",
              { "/",
                1,
                "len" } } } },
        1 } } },
  { "fail" } }
--- Optimized:
{ "if",
  { "!=",
    "len",
    0 },
  { "false" },
  { "fail" } }
On packet 11400: unoptimized was true, optimized was false
Rerun as: pflua-quickcheck --seed=150860333 --iterations=488 properties/opt_eq_unopt data/wingolog.pcap
kbara commented 9 years ago

There are actually at least two bugs here 1) The wrong result 2) If we can optimize out a division, we should also be able to optimize out the check that weŕe not dividing by zero.

wingo commented 9 years ago

In this case we can't optimize out the division though; its result is either 1 or 0, and a len value of 0 would indeed trigger an abort. Not that we should really see a zero-length packet!

kbara commented 9 years ago

Agreed, but in cases where we can optimize out the division, we definitely shouldn't leave the != 0 check in.

wingo commented 9 years ago

Sure, but leaving in the check is not a correctness bug, is all I'm saying :)

kbara commented 9 years ago

Agreed, just an anti-optimization. :)

wingo commented 9 years ago

Fixed in #123.