Skip to content

[Miscompile] Tuple == / != repeats, skips and reorders side effects in its operands #3797

Open

Description

@amcasey

Kind: Miscompile in the shared pipeline: every QIR profile that accepts the program returns a wrong value.
Affects: every profile
Found in: vs_sim.min_tuple_eq_call_twice.c33264e422, vs_sim.min_tuple_eq_short_circuit.1349fb306c

Bump(q) == (One, 5) should call Bump once. The lowered comparison compares element by
element and evaluates Bump(q) once per element, so X is applied twice and the qubit ends in
Zero.

Q#

operation Bump(q : Qubit) : (Result, Int) {
    X(q);
    (M(q), 5)
}

operation Main() : Result {
    use q = Qubit();
    let _ = Bump(q) == (One, 5);
    MResetZ(q)
}

Outputs

10 shots each. The simulator runs the Q# program directly; each profile compiles it to QIR, which is run with qir-runner.

Run Output Correct?
Simulator 1 yes
Base rejected (Qdk.Qsc.CapabilitiesCk.UseOfDynamicBool) n/a
Adaptive_RI 0 no
Adaptive_RIF 0 no
Adaptive 0 no
Correct output 1

Correct output

Bump runs once, so the qubit is flipped once and measures One.

Other shapes

The element-wise comparison also short-circuits. Here the first elements differ, so
MResetZ(b) is never evaluated and b stays One. The simulator returns 0 and every
profile returns 1:

operation Main() : Result {
    use a = Qubit();
    use b = Qubit();
    X(b);
    let _ = (MResetZ(a), MResetZ(b)) == (One, Zero);
    MResetZ(b)
}

Probable cause

tuple_compare_lower rewrites lhs == rhs into a chain of element comparisons joined with
and (or for !=) (qsc_fir_transforms/src/tuple_compare_lower.rs:158-243). An operand
that isn't a tuple literal is accessed once per element (extract_or_field), so it is evaluated
once per element, and the and/or chain short-circuits elements that should all be evaluated.
Operands with side effects need to be bound to temporaries first.

Reproduce

"""Tuple `==` / `!=` repeats, skips and reorders side effects in its operands

Compiles the Q# program below to QIR for each target profile, runs that QIR with
qir-runner, and runs the same program in the Q# simulator for comparison.
Exits 0 while the bug reproduces: Base, Adaptive_RI, Adaptive_RIF and Adaptive return something other than 1.

Requires: pip install qdk qirrunner
"""

import os
import re
import sys
import tempfile

import qirrunner
from qdk import Context, TargetProfile

SOURCE = """
operation Bump(q : Qubit) : (Result, Int) {
    X(q);
    (M(q), 5)
}

operation Main() : Result {
    use q = Qubit();
    let _ = Bump(q) == (One, 5);
    MResetZ(q)
}
"""
ENTRY = "Main()"
EXPECTED = "1"  # the correct output
AFFECTED = ['Base', 'Adaptive_RI', 'Adaptive_RIF', 'Adaptive']  # runs that show the bug
SHOTS = 10
PROFILES = ["Base", "Adaptive_RI", "Adaptive_RIF", "Adaptive"]


def fmt(value):
    """Formats a simulator value the same way as qir-runner output below."""
    if value is None:
        return "()"
    if type(value).__name__ == "Result":
        return "1" if str(value).endswith("One") else "0"
    if isinstance(value, bool):
        return str(value).lower()
    if isinstance(value, float):
        return repr(value)
    if isinstance(value, (tuple, list)):
        inner = ", ".join(fmt(v) for v in value)
        return f"({inner})" if isinstance(value, tuple) else f"[{inner}]"
    return str(value)


def parse_shots(text):
    """Turns qir-runner's output records into one formatted value per shot."""
    shots, records = [], None
    for line in text.splitlines():
        fields = line.split("\t")
        if fields[0] == "START":
            records = []
        elif fields[0] == "OUTPUT" and records is not None:
            records.append((fields[1], fields[2]))
        elif fields[0] == "END" and records is not None:
            shots.append(to_text(iter(records)) if records else "()")
            if fields[1] != "0":
                shots[-1] = f"exit code {fields[1]}"
            records = None
    return shots


def to_text(records):
    kind, value = next(records)
    if kind in ("TUPLE", "ARRAY"):
        inner = ", ".join(to_text(records) for _ in range(int(value)))
        return f"({inner})" if kind == "TUPLE" else f"[{inner}]"
    if kind == "DOUBLE":
        return repr(float(value))
    if kind == "BOOL":
        return value.lower()
    return value


def run_qir(qir):
    with tempfile.NamedTemporaryFile("w", suffix=".ll", delete=False) as file:
        file.write(qir)
    handler = qirrunner.OutputHandler()
    try:
        qirrunner.run(file.name, shots=SHOTS, rng_seed=1, output_fn=handler.handle)
    except Exception as error:  # qir-runner rejects the module
        message = str(error).strip().splitlines()[0]
        if message.startswith("Failed to link"):  # valid QIR calling functions qir-runner lacks
            return {"qir-runner can't link: " + message.split(": ", 1)[-1]}
        return {"invalid QIR: " + re.sub(r"^\S+\.ll:\d+:\d+: (error: )?", "", message)}
    finally:
        os.unlink(file.name)
    return set(parse_shots(handler.get_output()))


def outputs():
    rows = {}
    ctx = Context(target_profile=TargetProfile.Unrestricted)
    ctx.eval(SOURCE)
    rows["simulator"] = {fmt(v) for v in ctx.run(ENTRY, SHOTS, seed=1)}
    for profile in PROFILES:
        ctx = Context(target_profile=getattr(TargetProfile, profile))
        try:
            ctx.eval(SOURCE)
            qir = str(ctx.compile(ENTRY))
        except Exception as error:  # the profile rejects the program
            rows[profile] = {"does not compile: " + str(error).strip().splitlines()[0]}
            continue
        rows[profile] = run_qir(qir)
    return rows


def main():
    rows = outputs()
    width = max(map(len, rows)) + 2
    for name, values in rows.items():
        print(f"{name:<{width}}{' | '.join(sorted(values))}")
    print(f"{'expected':<{width}}{EXPECTED}")
    wrong = [name for name in AFFECTED if name in rows and rows[name] != {EXPECTED}]
    if wrong:
        print(f"REPRODUCED: {', '.join(wrong)} differ from {EXPECTED}")
        return 0
    print("NOT REPRODUCED")
    return 1


if __name__ == "__main__":
    sys.exit(main())

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions