search

Wilfred / bfc

An industrial-grade brainfuck compiler
https://bfc.wilfred.me.uk
GNU General Public License v2.0
508 stars 31 forks source link

Soundness issue in annotate_known_zero #55

Open Wilfred opened 1 year ago

Wilfred commented 1 year ago

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