Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Soundness issue in annotate_known_zero #55

Open
Wilfred opened this issue Jun 18, 2023 · 0 comments
Open

Soundness issue in annotate_known_zero #55

Wilfred opened this issue Jun 18, 2023 · 0 comments

Comments

@Wilfred
Copy link
Owner

Wilfred commented Jun 18, 2023

Quickcheck is sometimes finding a soundness issue with this transform:

Example failures:

[PointerIncrement { amount: 29, position: Some(0) }, Loop { body: [Increment { amount: -1, offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: 2, offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }, Set { amount: -59, offset: 0, position: Some(0) }, Loop { body: [Increment { amount: -1, offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: 2, offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }, Loop { body: [Write { position: Some(0) }, Increment { amount: -2, offset: 0, position: Some(0) }, Loop { body: [Set { amount: 84, offset: 0, position: Some(0) }, PointerIncrement { amount: -44, position: Some(0) }, MultiplyMove { changes: {1: -1}, position: Some(0) }, Set { amount: 17, offset: 0, position: Some(0) }, Read { position: Some(0) }], position: Some(0) }], position: Some(0) }, Loop { body: [Increment { amount: 84, offset: 0, position: Some(0) }, Write { position: Some(0) }, Loop { body: [MultiplyMove { changes: {1: -1}, position: Some(0) }], position: Some(0) }, Read { position: Some(0) }, Write { position: Some(0) }, Set { amount: -65, offset: 0, position: Some(0) }, MultiplyMove { changes: {1: 2, 4: 10}, position: Some(0) }, Read { position: Some(0) }, Loop { body: [PointerIncrement { amount: 1, position: Some(0) }, Loop { body: [MultiplyMove { changes: {1: -1}, position: Some(0) }, Write { position: Some(0) }, Increment { amount: -78, offset: 0, position: Some(0) }], position: Some(0) }, MultiplyMove { changes: {1: -1}, position: Some(0) }, Set { amount: 45, offset: 0, position: Some(0) }, Write { position: Some(0) }, Write { position: Some(0) }, Increment { amount: -90, offset: 0, position: Some(0) }, Write { position: Some(0) }, Increment { amount: 51, offset: 0, position: Some(0) }], position: Some(0) }], position: Some(0) }, MultiplyMove { changes: {4: 10, 1: 2}, position: Some(0) }, Loop { body: [Increment { amount: -1, offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: 2, offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }, MultiplyMove { changes: {1: 2, 4: 10}, position: Some(0) }]
[Increment { amount: 15, offset: 0, position: Some(0) }, Set { amount: 95, offset: 0, position: Some(0) }, PointerIncrement { amount: 13, position: Some(0) }, Set { amount: 59, offset: 0, position: Some(0) }, Set { amount: -58, offset: 0, position: Some(0) }, Loop { body: [Increment { amount: -1, offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: 2, offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }, Loop { body: [Increment { amount: -1, offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: 2, offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }]

The second example can be written in Rust syntax as:

let instrs = vec![
    Increment { amount: Wrapping(15), offset: 0, position: None },
    Set { amount: Wrapping(95), offset: 0, position: None },
    PointerIncrement { amount: 13, position: None },
    Set { amount: Wrapping(59), offset: 0, position: None },
    Set { amount: Wrapping(-58), offset: 0, position: None },
    Loop { body: vec![Increment { amount: Wrapping(-1), offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: Wrapping(2), offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None },
    Loop { body: vec![Increment { amount: Wrapping(-1), offset: 0, position: None }, PointerIncrement { amount: -1, position: None }, Increment { amount: Wrapping(2), offset: 0, position: None }, PointerIncrement { amount: 1, position: None }], position: None }
];

This is sometimes reproducible with the following command:

$ QUICKCHECK_TESTS=50000 cargo t known_zero_is
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant