Soundness bug with subrange types

[xaaronc]

With the following Lustre program:

type T = subrange [0,1] of int;

function B(x: T) returns (y: T)
let
    y = x;
tel

function A(x: int) returns (y, z: T)
let
    y = x;
    z = B(y);
tel

kind2 correctly identifies the bounds violation in the y = x assignment when using --slice_nodes true:

$ kind2 --slice_nodes true foo.lus
[..]
<Failure> Property y.bound is invalid by property directed reachability for k=0 after 0.051s.

but with --slice_nodes false, it succeeds erroneously:

$ kind2 --slice_nodes false foo.lus 
[..]
<Success> Property y.bound is valid by property directed reachability after 0.060s.

Version kind2 36140a5a

[xaaronc]

I’ve been able to reproduce this bug with the default setting for --slice_nodes, though so far haven’t been able to produce a small example input.

[xaaronc]

Found a simple reproducer:

type U = subrange [0,2] of int;
type T = subrange [-1,1] of int;

node A(x: U) returns (y: U)
let
    y = x;
tel

node B(x: T) returns (z: T; y: U)
let
    y = x;
    z = A(y);
tel

$ kind2 foo2.lus
[..]
<Success> Property z.bound is valid by property directed reachability after 0.050s.
<Success> Property y.bound is valid by property directed reachability after 0.050s.

[daniel-larraz]

Hi Aaron,

Thank you for reporting this bug and providing the small reproducer. It seems the current mechanism for checking subrange bounds is broken. I will review it and make the appropriate changes to fix it, but it will take some time. I'll keep you posted.

Thanks,
Daniel